TestCopyingReplayer

working on 0
One Step Simplification
working on 1
impRight
working on 2
andLeft
working on 3
andLeft
working on 4
andLeft
working on 5
andLeft
working on 6
andLeft
working on 7
andLeft
working on 8
andLeft
working on 9
notLeft
working on 10
notLeft
working on 11
eqSymm
working on 12
replace_known_right
working on 13
One Step Simplification
working on 14
replace_known_right
working on 15
One Step Simplification
working on 16
polySimp_elimSub
working on 17
mul_literals
working on 18
polySimp_addComm0
working on 19
inEqSimp_commuteLeq
working on 20
inEqSimp_commuteLeq
working on 21
assignment
working on 22
One Step Simplification
working on 23
methodBodyExpand
working on 24
One Step Simplification
working on 25
variableDeclaration
working on 26
variableDeclaration
working on 27
assignment
working on 28
One Step Simplification
working on 29
variableDeclaration
working on 30
variableDeclaration
working on 31
assignment_read_length
working on 32
One Step Simplification
working on 34
for_to_while
working on 35
variableDeclaration
working on 36
variableDeclaration
working on 37
assignment
working on 38
One Step Simplification
working on 39
elim_double_block
working on 40
Loop Invariant
working on 41
andRight
working on 44
andRight
working on 46
andRight
working on 48
andRight
working on 50
andRight
working on 52
andRight
working on 54
andRight
working on 56
andRight
working on 58
andRight
working on 60
One Step Simplification
working on 62
closeTrue
working on 63
working on 61
andRight
working on 64
One Step Simplification
working on 66
leq_literals
working on 67
closeTrue
working on 68
working on 65
One Step Simplification
working on 69
inEqSimp_leqRight
working on 70
add_zero_right
working on 71
polySimp_mulComm0
working on 72
inEqSimp_ltToLeq
working on 73
add_zero_right
working on 74
polySimp_mulComm0
working on 75
inEqSimp_sepNegMonomial1
working on 76
polySimp_mulLiterals
working on 77
polySimp_elimOne
working on 78
inEqSimp_sepNegMonomial0
working on 79
polySimp_mulLiterals
working on 80
polySimp_elimOne
working on 81
inEqSimp_contradInEq1
working on 82
qeq_literals
working on 83
One Step Simplification
working on 84
closeFalse
working on 85
working on 59
andRight
working on 86
One Step Simplification
working on 88
sub_literals
working on 89
leq_literals
working on 90
closeTrue
working on 91
working on 87
One Step Simplification
working on 92
sub_literals
working on 93
inEqSimp_leqRight
working on 94
add_zero_right
working on 95
polySimp_mulComm0
working on 96
inEqSimp_ltToLeq
working on 97
add_zero_right
working on 98
polySimp_mulComm0
working on 99
inEqSimp_sepNegMonomial1
working on 100
polySimp_mulLiterals
working on 101
polySimp_elimOne
working on 102
inEqSimp_sepNegMonomial0
working on 103
polySimp_mulLiterals
working on 104
polySimp_elimOne
working on 105
inEqSimp_exactShadow3
working on 106
mul_literals
working on 107
inEqSimp_sepPosMonomial1
working on 108
mul_literals
working on 109
inEqSimp_contradInEq1
working on 110
qeq_literals
working on 111
One Step Simplification
working on 112
closeFalse
working on 113
working on 57
orRight
working on 114
One Step Simplification
working on 115
One Step Simplification
working on 116
closeTrue
working on 117
working on 55
orRight
working on 118
andRight
working on 119
One Step Simplification
working on 121
closeTrue
working on 122
working on 120
One Step Simplification
working on 123
closeTrue
working on 124
working on 53
One Step Simplification
working on 125
equal_literals
working on 126
One Step Simplification
working on 127
notRight
working on 128
andLeft
working on 129
irrflConcrete1
working on 130
closeFalse
working on 131
working on 51
One Step Simplification
working on 132
closeTrue
working on 133
working on 49
One Step Simplification
working on 134
allRight
working on 135
impRight
working on 136
andLeft
working on 137
andLeft
working on 138
inEqSimp_ltToLeq
working on 139
add_zero_right
working on 140
polySimp_mulComm0
working on 141
inEqSimp_ltToLeq
working on 142
times_zero
working on 143
add_literals
working on 144
inEqSimp_ltToLeq
working on 145
polySimp_mulComm0
working on 146
polySimp_addComm1
working on 147
inEqSimp_commuteLeq
working on 148
inEqSimp_sepNegMonomial0
working on 149
polySimp_mulLiterals
working on 150
polySimp_elimOne
working on 151
inEqSimp_sepPosMonomial0
working on 152
mul_literals
working on 153
inEqSimp_sepNegMonomial0
working on 154
polySimp_mulLiterals
working on 155
polySimp_elimOne
working on 156
inEqSimp_contradInEq1
working on 157
qeq_literals
working on 158
One Step Simplification
working on 159
closeFalse
working on 160
working on 47
One Step Simplification
working on 161
allRight
working on 162
impRight
working on 163
andLeft
working on 164
eqSymm
working on 165
polySimp_elimSub
working on 166
mul_literals
working on 167
polySimp_addComm0
working on 168
inEqSimp_ltToLeq
working on 169
add_zero_right
working on 170
polySimp_mulComm0
working on 171
inEqSimp_ltToLeq
working on 172
times_zero
working on 173
add_literals
working on 174
inEqSimp_ltToLeq
working on 175
polySimp_mulComm0
working on 176
inEqSimp_sepNegMonomial0
working on 177
polySimp_mulLiterals
working on 178
polySimp_elimOne
working on 179
inEqSimp_sepPosMonomial0
working on 180
mul_literals
working on 181
inEqSimp_sepPosMonomial0
working on 182
polySimp_mulComm0
working on 183
polySimp_rightDist
working on 184
polySimp_mulLiterals
working on 185
mul_literals
working on 186
polySimp_elimOne
working on 187
inEqSimp_exactShadow3
working on 188
mul_literals
working on 189
polySimp_addAssoc
working on 190
add_literals
working on 191
inEqSimp_sepPosMonomial1
working on 192
mul_literals
working on 193
inEqSimp_contradInEq0
working on 194
qeq_literals
working on 195
One Step Simplification
working on 196
closeFalse
working on 197
working on 45
One Step Simplification
working on 198
closeTrue
working on 199
working on 42
One Step Simplification
working on 200
One Step Simplification
working on 201
andLeft
working on 202
impRight
working on 203
andLeft
working on 204
andLeft
working on 205
andLeft
working on 206
andLeft
working on 207
andLeft
working on 208
andLeft
working on 209
andLeft
working on 210
andLeft
working on 211
eqSymm
working on 212
eqSymm
working on 213
eqSymm
working on 214
eqSymm
working on 215
eqSymm
working on 216
eqSymm
working on 217
eqSymm
working on 218
polySimp_elimSub
working on 219
polySimp_elimSub
working on 220
polySimp_elimSub
working on 221
polySimp_elimSub
working on 222
polySimp_elimSub
working on 223
polySimp_elimSub
working on 224
polySimp_elimSub
working on 225
mul_literals
working on 226
polySimp_elimSub
working on 227
mul_literals
working on 228
polySimp_addComm0
working on 229
polySimp_addComm0
working on 230
polySimp_addComm0
working on 231
polySimp_addComm0
working on 232
inEqSimp_commuteLeq
working on 233
inEqSimp_commuteLeq
working on 234
inEqSimp_commuteLeq
working on 235
inEqSimp_commuteLeq
working on 236
inEqSimp_commuteLeq
working on 237
inEqSimp_commuteLeq
working on 238
inEqSimp_commuteLeq
working on 239
inEqSimp_commuteLeq
working on 240
inEqSimp_commuteLeq
working on 241
inEqSimp_commuteLeq
working on 242
inEqSimp_commuteLeq
working on 243
inEqSimp_commuteLeq
working on 244
variableDeclaration
working on 245
variableDeclaration
working on 246
variableDeclaration
working on 247
variableDeclaration
working on 248
assignment
working on 249
One Step Simplification
working on 250
variableDeclaration
working on 251
variableDeclaration
working on 252
variableDeclaration
working on 253
assignment
working on 254
One Step Simplification
working on 255
variableDeclaration
working on 256
blockThrow
working on 257
blockReturn
working on 258
boxToDiamond
working on 259
One Step Simplification
working on 260
notLeft
working on 261
commute_or
working on 262
commute_and
working on 263
cnf_rightDist
working on 264
andLeft
working on 265
commute_or
working on 266
commute_and_2
working on 267
commute_and
working on 268
commute_and_2
working on 269
less_than
working on 270
variableDeclaration
working on 271
variableDeclaration
working on 272
assignment
working on 273
One Step Simplification
working on 274
variableDeclaration
working on 275
variableDeclaration
working on 276
assignment_read_length
working on 277
One Step Simplification
working on 279
lesser than distinction
working on 280
One Step Simplification
working on 281
methodCallEmpty
working on 282
emptyModality
working on 283
One Step Simplification
working on 284
notRight
working on 285
ifElseUnfold
working on 286
variableDeclaration
working on 287
less_than
working on 288
variableDeclaration
working on 289
variableDeclaration
working on 290
assignment
working on 291
One Step Simplification
working on 292
variableDeclaration
working on 293
variableDeclaration
working on 294
assignment_read_length
working on 295
One Step Simplification
working on 297
lesser than distinction
working on 298
One Step Simplification
working on 299
replace_known_left
working on 300
One Step Simplification
working on 301
arrayLengthNotNegative
working on 302
arrayLengthNotNegative
working on 303
arrayLengthIsAnInt
working on 304
arrayLengthIsAnInt
working on 305
ifElseSplit
working on 306
One Step Simplification
working on 308
One Step Simplification
working on 309
true_left
working on 310
ifElseUnfold
working on 311
variableDeclaration
working on 312
inequality
working on 313
variableDeclaration
working on 314
variableDeclaration
working on 315
assignment_array2
working on 316
One Step Simplification
working on 319
variableDeclaration
working on 320
variableDeclaration
working on 321
assignmentUnfoldRight
working on 322
variableDeclaration
working on 323
variableDeclaration
working on 324
assignment
working on 325
One Step Simplification
working on 326
variableDeclaration
working on 327
variableDeclaration
working on 328
subtraction
working on 329
One Step Simplification
working on 330
translateJavaSub
working on 331
polySimp_elimSub
working on 332
assignment_array2
working on 333
One Step Simplification
working on 336
inequality comparison
working on 337
One Step Simplification
working on 338
eqSymm
working on 339
ifElseSplit
working on 340
One Step Simplification
working on 342
One Step Simplification
working on 343
notLeft
working on 344
ifElseUnfold
working on 345
variableDeclaration
working on 346
equality comparison
working on 347
One Step Simplification
working on 348
ifElseSplit
working on 349
One Step Simplification
working on 351
One Step Simplification
working on 352
replace_known_left
working on 353
One Step Simplification
working on 354
true_left
working on 355
replace_known_left
working on 356
One Step Simplification
working on 357
replace_known_left
working on 358
One Step Simplification
working on 359
true_left
working on 360
replace_known_left
working on 361
One Step Simplification
working on 362
true_left
working on 363
assignment
working on 364
One Step Simplification
working on 365
assignment
working on 366
One Step Simplification
working on 367
blockEmpty
working on 368
applyEq
working on 369
times_zero
working on 370
add_zero_right
working on 371
inEqSimp_commuteLeq
working on 372
applyEq
working on 373
inEqSimp_commuteLeq
working on 374
applyEq
working on 375
times_zero
working on 376
add_zero_right
working on 377
eqSymm
working on 378
applyEq
working on 379
applyEq
working on 380
applyEq
working on 381
applyEq
working on 382
times_zero
working on 383
add_zero_right
working on 384
applyEq
working on 385
equal_literals
working on 386
One Step Simplification
working on 387
notLeft
working on 388
applyEq
working on 389
replace_known_left
working on 390
One Step Simplification
working on 391
applyEq
working on 392
applyEq
working on 393
applyEq
working on 394
postincrement
working on 395
unusedLabel
working on 396
cast
working on 397
variableDeclaration
working on 398
variableDeclaration
working on 399
remove_parentheses_right
working on 400
addition
working on 401
One Step Simplification
working on 402
translateJavaAdd
working on 403
polySimp_addComm0
working on 404
cast
working on 405
assignment
working on 406
One Step Simplification
working on 407
tryEmpty
working on 408
methodCallEmpty
working on 409
emptyModality
working on 410
One Step Simplification
working on 411
andRight
working on 412
andRight
working on 414
andRight
working on 416
andRight
working on 418
andRight
working on 420
andRight
working on 422
andRight
working on 424
andRight
working on 426
inEqSimp_ltRight
working on 428
polySimp_mulComm0
working on 429
polySimp_pullOutFactor2
working on 430
add_literals
working on 431
times_zero
working on 432
qeq_literals
working on 433
true_left
working on 434
inEqSimp_leqRight
working on 435
polySimp_mulComm0
working on 436
inEqSimp_ltToLeq
working on 437
polySimp_mulComm0
working on 438
polySimp_addComm1
working on 439
inEqSimp_ltToLeq
working on 440
polySimp_mulComm0
working on 441
inEqSimp_ltToLeq
working on 442
polySimp_mulComm0
working on 443
polySimp_addComm1
working on 444
inEqSimp_ltToLeq
working on 445
polySimp_mulComm0
working on 446
inEqSimp_ltToLeq
working on 447
add_zero_right
working on 448
polySimp_mulComm0
working on 449
inEqSimp_ltToLeq
working on 450
polySimp_mulComm0
working on 451
applyEq
working on 452
polySimp_addComm1
working on 453
inEqSimp_sepNegMonomial0
working on 454
polySimp_mulLiterals
working on 455
polySimp_elimOne
working on 456
inEqSimp_sepPosMonomial0
working on 457
polySimp_mulComm0
working on 458
polySimp_rightDist
working on 459
mul_literals
working on 460
polySimp_mulLiterals
working on 461
polySimp_elimOne
working on 462
inEqSimp_sepNegMonomial0
working on 463
polySimp_mulLiterals
working on 464
polySimp_elimOne
working on 465
inEqSimp_sepPosMonomial0
working on 466
polySimp_mulComm0
working on 467
polySimp_rightDist
working on 468
mul_literals
working on 469
polySimp_mulLiterals
working on 470
polySimp_elimOne
working on 471
inEqSimp_sepNegMonomial0
working on 472
polySimp_mulLiterals
working on 473
polySimp_elimOne
working on 474
inEqSimp_sepPosMonomial0
working on 475
polySimp_mulComm0
working on 476
polySimp_rightDist
working on 477
mul_literals
working on 478
polySimp_mulLiterals
working on 479
polySimp_elimOne
working on 480
inEqSimp_sepNegMonomial1
working on 481
polySimp_mulLiterals
working on 482
polySimp_elimOne
working on 483
inEqSimp_subsumption1
working on 484
leq_literals
working on 485
One Step Simplification
working on 486
true_left
working on 487
inEqSimp_contradInEq0
working on 488
andLeft
working on 489
inEqSimp_homoInEq1
working on 490
polySimp_mulComm0
working on 491
polySimp_rightDist
working on 492
mul_literals
working on 493
polySimp_addAssoc
working on 494
polySimp_addComm0
working on 495
polySimp_pullOutFactor1b
working on 496
add_literals
working on 497
times_zero
working on 498
add_literals
working on 499
leq_literals
working on 500
closeFalse
working on 501
working on 427
andRight
working on 502
inEqSimp_geqRight
working on 504
times_zero
working on 505
add_zero_right
working on 506
polySimp_addAssoc
working on 507
add_literals
working on 508
inEqSimp_ltRight
working on 509
polySimp_mulComm0
working on 510
polySimp_pullOutFactor2
working on 511
add_literals
working on 512
times_zero
working on 513
qeq_literals
working on 514
true_left
working on 515
inEqSimp_ltToLeq
working on 516
polySimp_mulComm0
working on 517
polySimp_addComm1
working on 518
inEqSimp_ltToLeq
working on 519
polySimp_mulComm0
working on 520
inEqSimp_ltToLeq
working on 521
add_zero_right
working on 522
polySimp_mulComm0
working on 523
inEqSimp_ltToLeq
working on 524
polySimp_mulComm0
working on 525
inEqSimp_ltToLeq
working on 526
polySimp_mulComm0
working on 527
inEqSimp_ltToLeq
working on 528
polySimp_mulComm0
working on 529
polySimp_addComm1
working on 530
inEqSimp_sepPosMonomial0
working on 531
mul_literals
working on 532
inEqSimp_sepNegMonomial0
working on 533
polySimp_mulLiterals
working on 534
polySimp_elimOne
working on 535
inEqSimp_sepPosMonomial0
working on 536
polySimp_mulComm0
working on 537
polySimp_rightDist
working on 538
mul_literals
working on 539
polySimp_mulLiterals
working on 540
polySimp_elimOne
working on 541
inEqSimp_sepNegMonomial0
working on 542
polySimp_mulLiterals
working on 543
polySimp_elimOne
working on 544
inEqSimp_sepPosMonomial0
working on 545
polySimp_mulComm0
working on 546
polySimp_rightDist
working on 547
mul_literals
working on 548
polySimp_mulLiterals
working on 549
polySimp_elimOne
working on 550
inEqSimp_sepPosMonomial0
working on 551
polySimp_mulComm0
working on 552
polySimp_rightDist
working on 553
mul_literals
working on 554
polySimp_mulLiterals
working on 555
polySimp_elimOne
working on 556
inEqSimp_sepNegMonomial0
working on 557
polySimp_mulLiterals
working on 558
polySimp_elimOne
working on 559
inEqSimp_subsumption1
working on 560
inEqSimp_homoInEq0
working on 561
polySimp_pullOutFactor1b
working on 562
add_literals
working on 563
times_zero
working on 564
add_zero_right
working on 565
qeq_literals
working on 566
One Step Simplification
working on 567
true_left
working on 568
inEqSimp_contradInEq0
working on 569
qeq_literals
working on 570
One Step Simplification
working on 571
closeFalse
working on 572
working on 503
inEqSimp_ltRight
working on 573
polySimp_mulComm0
working on 574
polySimp_pullOutFactor2
working on 575
add_literals
working on 576
times_zero
working on 577
qeq_literals
working on 578
true_left
working on 579
inEqSimp_geqRight
working on 580
polySimp_rightDist
working on 581
mul_literals
working on 582
polySimp_addAssoc
working on 583
add_literals
working on 584
add_zero_left
working on 585
inEqSimp_ltToLeq
working on 586
polySimp_mulComm0
working on 587
polySimp_addComm1
working on 588
inEqSimp_ltToLeq
working on 589
polySimp_mulComm0
working on 590
inEqSimp_ltToLeq
working on 591
polySimp_mulComm0
working on 592
polySimp_addComm1
working on 593
inEqSimp_ltToLeq
working on 594
polySimp_mulComm0
working on 595
inEqSimp_ltToLeq
working on 596
polySimp_mulComm0
working on 597
inEqSimp_ltToLeq
working on 598
add_zero_right
working on 599
polySimp_mulComm0
working on 600
applyEq
working on 601
inEqSimp_sepNegMonomial0
working on 602
polySimp_mulLiterals
working on 603
polySimp_elimOne
working on 604
inEqSimp_sepPosMonomial0
working on 605
polySimp_mulComm0
working on 606
polySimp_rightDist
working on 607
polySimp_mulLiterals
working on 608
mul_literals
working on 609
polySimp_elimOne
working on 610
inEqSimp_sepNegMonomial0
working on 611
polySimp_mulLiterals
working on 612
polySimp_elimOne
working on 613
inEqSimp_sepPosMonomial0
working on 614
polySimp_mulComm0
working on 615
polySimp_rightDist
working on 616
polySimp_mulLiterals
working on 617
mul_literals
working on 618
polySimp_elimOne
working on 619
inEqSimp_sepPosMonomial0
working on 620
polySimp_mulComm0
working on 621
polySimp_rightDist
working on 622
polySimp_mulLiterals
working on 623
mul_literals
working on 624
polySimp_elimOne
working on 625
inEqSimp_sepNegMonomial0
working on 626
polySimp_mulLiterals
working on 627
polySimp_elimOne
working on 628
inEqSimp_sepPosMonomial0
working on 629
polySimp_mulLiterals
working on 630
polySimp_elimOne
working on 631
inEqSimp_contradInEq0
working on 632
andLeft
working on 633
inEqSimp_homoInEq1
working on 634
polySimp_pullOutFactor1b
working on 635
add_literals
working on 636
times_zero
working on 637
add_literals
working on 638
leq_literals
working on 639
closeFalse
working on 640
working on 425
andRight
working on 641
mul_literals
working on 643
polySimp_addComm1
working on 644
add_literals
working on 645
add_zero_left
working on 646
inEqSimp_ltRight
working on 647
polySimp_mulComm0
working on 648
polySimp_pullOutFactor2
working on 649
add_literals
working on 650
times_zero
working on 651
qeq_literals
working on 652
true_left
working on 653
inEqSimp_leqRight
working on 654
add_zero_right
working on 655
polySimp_mulComm0
working on 656
inEqSimp_ltToLeq
working on 657
polySimp_mulComm0
working on 658
inEqSimp_ltToLeq
working on 659
polySimp_mulComm0
working on 660
inEqSimp_ltToLeq
working on 661
add_zero_right
working on 662
polySimp_mulComm0
working on 663
inEqSimp_ltToLeq
working on 664
polySimp_mulComm0
working on 665
polySimp_addComm1
working on 666
inEqSimp_ltToLeq
working on 667
polySimp_mulComm0
working on 668
polySimp_addComm1
working on 669
inEqSimp_ltToLeq
working on 670
polySimp_mulComm0
working on 671
inEqSimp_sepNegMonomial1
working on 672
polySimp_mulLiterals
working on 673
polySimp_elimOne
working on 674
inEqSimp_sepPosMonomial0
working on 675
polySimp_mulComm0
working on 676
polySimp_rightDist
working on 677
mul_literals
working on 678
polySimp_mulLiterals
working on 679
polySimp_elimOne
working on 680
inEqSimp_sepPosMonomial0
working on 681
polySimp_mulComm0
working on 682
polySimp_rightDist
working on 683
mul_literals
working on 684
polySimp_mulLiterals
working on 685
polySimp_elimOne
working on 686
inEqSimp_sepNegMonomial0
working on 687
polySimp_mulLiterals
working on 688
polySimp_elimOne
working on 689
inEqSimp_sepNegMonomial0
working on 690
polySimp_mulLiterals
working on 691
polySimp_elimOne
working on 692
inEqSimp_sepNegMonomial0
working on 693
polySimp_mulLiterals
working on 694
polySimp_elimOne
working on 695
inEqSimp_sepPosMonomial0
working on 696
polySimp_mulComm0
working on 697
polySimp_rightDist
working on 698
mul_literals
working on 699
polySimp_mulLiterals
working on 700
polySimp_elimOne
working on 701
inEqSimp_subsumption1
working on 702
inEqSimp_homoInEq0
working on 703
polySimp_pullOutFactor1b
working on 704
add_literals
working on 705
times_zero
working on 706
add_zero_right
working on 707
qeq_literals
working on 708
One Step Simplification
working on 709
true_left
working on 710
inEqSimp_subsumption1
working on 711
leq_literals
working on 712
One Step Simplification
working on 713
true_left
working on 714
inEqSimp_contradInEq0
working on 715
qeq_literals
working on 716
One Step Simplification
working on 717
closeFalse
working on 718
working on 642
mul_literals
working on 719
polySimp_addComm1
working on 720
add_literals
working on 721
add_zero_left
working on 722
close
working on 723
working on 423
orRight
working on 724
inEqSimp_ltRight
working on 725
polySimp_rightDist
working on 726
mul_literals
working on 727
polySimp_pullOutFactor2b
working on 728
add_literals
working on 729
times_zero
working on 730
add_literals
working on 731
qeq_literals
working on 732
closeFalse
working on 733
working on 421
inEqSimp_ltRight
working on 734
polySimp_mulComm0
working on 735
polySimp_pullOutFactor2
working on 736
add_literals
working on 737
times_zero
working on 738
qeq_literals
working on 739
true_left
working on 740
inEqSimp_ltRight
working on 741
polySimp_mulComm0
working on 742
polySimp_addComm0
working on 743
inEqSimp_ltToLeq
working on 744
polySimp_mulComm0
working on 745
polySimp_addComm1
working on 746
inEqSimp_ltToLeq
working on 747
polySimp_mulComm0
working on 748
polySimp_addComm1
working on 749
inEqSimp_ltToLeq
working on 750
polySimp_mulComm0
working on 751
inEqSimp_ltToLeq
working on 752
polySimp_mulComm0
working on 753
inEqSimp_ltToLeq
working on 754
add_zero_right
working on 755
polySimp_mulComm0
working on 756
inEqSimp_ltToLeq
working on 757
polySimp_mulComm0
working on 758
applyEq
working on 759
inEqSimp_sepNegMonomial0
working on 760
polySimp_mulLiterals
working on 761
polySimp_elimOne
working on 762
inEqSimp_sepNegMonomial0
working on 763
polySimp_mulLiterals
working on 764
polySimp_elimOne
working on 765
inEqSimp_sepPosMonomial0
working on 766
polySimp_mulComm0
working on 767
polySimp_rightDist
working on 768
mul_literals
working on 769
polySimp_mulLiterals
working on 770
polySimp_elimOne
working on 771
inEqSimp_sepPosMonomial0
working on 772
polySimp_mulComm0
working on 773
polySimp_rightDist
working on 774
mul_literals
working on 775
polySimp_mulLiterals
working on 776
polySimp_elimOne
working on 777
inEqSimp_sepNegMonomial0
working on 778
polySimp_mulLiterals
working on 779
polySimp_elimOne
working on 780
inEqSimp_sepPosMonomial0
working on 781
polySimp_mulComm0
working on 782
polySimp_rightDist
working on 783
mul_literals
working on 784
polySimp_mulLiterals
working on 785
polySimp_elimOne
working on 786
inEqSimp_sepNegMonomial1
working on 787
polySimp_mulLiterals
working on 788
polySimp_elimOne
working on 789
inEqSimp_subsumption1
working on 790
leq_literals
working on 791
One Step Simplification
working on 792
true_left
working on 793
inEqSimp_subsumption1
working on 794
inEqSimp_homoInEq0
working on 795
polySimp_pullOutFactor1b
working on 796
add_literals
working on 797
times_zero
working on 798
add_zero_right
working on 799
qeq_literals
working on 800
One Step Simplification
working on 801
true_left
working on 802
inEqSimp_contradInEq0
working on 803
andLeft
working on 804
inEqSimp_homoInEq1
working on 805
polySimp_pullOutFactor1b
working on 806
add_literals
working on 807
times_zero
working on 808
add_literals
working on 809
leq_literals
working on 810
closeFalse
working on 811
working on 419
equal_literals
working on 812
One Step Simplification
working on 813
notRight
working on 814
inEqSimp_ltRight
working on 815
polySimp_mulComm0
working on 816
polySimp_pullOutFactor2
working on 817
add_literals
working on 818
times_zero
working on 819
qeq_literals
working on 820
true_left
working on 821
inEqSimp_ltToLeq
working on 822
polySimp_mulComm0
working on 823
inEqSimp_ltToLeq
working on 824
polySimp_mulComm0
working on 825
inEqSimp_ltToLeq
working on 826
add_zero_right
working on 827
polySimp_mulComm0
working on 828
inEqSimp_ltToLeq
working on 829
polySimp_mulComm0
working on 830
inEqSimp_ltToLeq
working on 831
polySimp_mulComm0
working on 832
polySimp_addComm1
working on 833
inEqSimp_ltToLeq
working on 834
polySimp_mulComm0
working on 835
polySimp_addComm1
working on 836
applyEq
working on 837
applyEq
working on 838
applyEq
working on 839
applyEq
working on 840
applyEq
working on 841
applyEq
working on 842
polySimp_pullOutFactor1b
working on 843
add_literals
working on 844
times_zero
working on 845
add_literals
working on 846
leq_literals
working on 847
closeFalse
working on 848
working on 417
allRight
working on 849
impRight
working on 850
andLeft
working on 851
andLeft
working on 852
inEqSimp_ltRight
working on 853
polySimp_mulComm0
working on 854
polySimp_pullOutFactor2
working on 855
add_literals
working on 856
times_zero
working on 857
qeq_literals
working on 858
true_left
working on 859
inEqSimp_ltToLeq
working on 860
polySimp_mulComm0
working on 861
inEqSimp_ltToLeq
working on 862
polySimp_mulComm0
working on 863
polySimp_addComm1
working on 864
inEqSimp_ltToLeq
working on 865
add_zero_right
working on 866
polySimp_mulComm0
working on 867
inEqSimp_ltToLeq
working on 868
polySimp_mulComm0
working on 869
inEqSimp_ltToLeq
working on 870
polySimp_mulComm0
working on 871
inEqSimp_ltToLeq
working on 872
polySimp_mulComm0
working on 873
polySimp_addComm1
working on 874
inEqSimp_ltToLeq
working on 875
polySimp_rightDist
working on 876
mul_literals
working on 877
polySimp_addAssoc
working on 878
add_literals
working on 879
add_zero_left
working on 880
inEqSimp_ltToLeq
working on 881
polySimp_mulComm0
working on 882
inEqSimp_sepPosMonomial0
working on 883
polySimp_mulComm0
working on 884
polySimp_rightDist
working on 885
mul_literals
working on 886
polySimp_mulLiterals
working on 887
polySimp_elimOne
working on 888
inEqSimp_sepNegMonomial0
working on 889
polySimp_mulLiterals
working on 890
polySimp_elimOne
working on 891
inEqSimp_sepNegMonomial0
working on 892
polySimp_mulLiterals
working on 893
polySimp_elimOne
working on 894
inEqSimp_sepPosMonomial0
working on 895
polySimp_mulComm0
working on 896
polySimp_rightDist
working on 897
mul_literals
working on 898
polySimp_mulLiterals
working on 899
polySimp_elimOne
working on 900
inEqSimp_sepPosMonomial0
working on 901
polySimp_mulComm0
working on 902
polySimp_rightDist
working on 903
mul_literals
working on 904
polySimp_mulLiterals
working on 905
polySimp_elimOne
working on 906
inEqSimp_sepNegMonomial0
working on 907
polySimp_mulLiterals
working on 908
polySimp_elimOne
working on 909
inEqSimp_sepPosMonomial0
working on 910
polySimp_mulLiterals
working on 911
polySimp_elimOne
working on 912
inEqSimp_sepPosMonomial0
working on 913
polySimp_mulComm0
working on 914
polySimp_rightDist
working on 915
mul_literals
working on 916
polySimp_mulLiterals
working on 917
polySimp_elimOne
working on 918
inEqSimp_subsumption1
working on 919
leq_literals
working on 920
One Step Simplification
working on 921
true_left
working on 922
inEqSimp_subsumption1
working on 923
inEqSimp_homoInEq0
working on 924
polySimp_pullOutFactor1b
working on 925
add_literals
working on 926
times_zero
working on 927
add_zero_right
working on 928
qeq_literals
working on 929
One Step Simplification
working on 930
true_left
working on 931
inEqSimp_subsumption0
working on 932
inEqSimp_homoInEq0
working on 933
polySimp_mulComm0
working on 934
polySimp_rightDist
working on 935
mul_literals
working on 936
polySimp_addAssoc
working on 937
polySimp_addComm0
working on 938
polySimp_pullOutFactor1b
working on 939
add_literals
working on 940
times_zero
working on 941
add_zero_right
working on 942
qeq_literals
working on 943
One Step Simplification
working on 944
true_left
working on 945
inEqSimp_exactShadow3
working on 946
times_zero
working on 947
add_zero_left
working on 948
inEqSimp_sepPosMonomial1
working on 949
mul_literals
working on 950
inEqSimp_subsumption1
working on 951
leq_literals
working on 952
One Step Simplification
working on 953
true_left
working on 954
nnf_imp2or
working on 955
nnf_imp2or
working on 956
nnf_notAnd
working on 957
inEqSimp_notGeq
working on 958
polySimp_rightDist
working on 959
mul_literals
working on 960
polySimp_addAssoc
working on 961
add_literals
working on 962
add_zero_left
working on 963
inEqSimp_sepPosMonomial0
working on 964
polySimp_mulLiterals
working on 965
polySimp_elimOne
working on 966
inEqSimp_notLeq
working on 967
polySimp_rightDist
working on 968
mul_literals
working on 969
polySimp_addAssoc
working on 970
add_literals
working on 971
add_zero_left
working on 972
inEqSimp_sepPosMonomial1
working on 973
polySimp_mulLiterals
working on 974
polySimp_elimOne
working on 975
nnf_notAnd
working on 976
inEqSimp_notGeq
working on 977
times_zero
working on 978
add_zero_right
working on 979
inEqSimp_sepPosMonomial0
working on 980
mul_literals
working on 981
nnf_notAnd
working on 982
inEqSimp_notLeq
working on 983
polySimp_rightDist
working on 984
mul_literals
working on 985
polySimp_addAssoc
working on 986
add_literals
working on 987
add_zero_left
working on 988
inEqSimp_sepPosMonomial1
working on 989
polySimp_mulLiterals
working on 990
polySimp_elimOne
working on 991
inEqSimp_notLeq
working on 992
polySimp_rightDist
working on 993
mul_literals
working on 994
polySimp_addAssoc
working on 995
add_literals
working on 996
add_zero_left
working on 997
inEqSimp_sepPosMonomial1
working on 998
polySimp_mulLiterals
working on 999
polySimp_elimOne
working on 1000
commute_or
working on 1001
commute_or_2
working on 1002
commute_or
working on 1003
allLeft
working on 1004
replace_known_right
working on 1005
One Step Simplification
working on 1006
inEqSimp_commuteGeq
working on 1007
inEqSimp_contradInEq1
working on 1008
qeq_literals
working on 1009
One Step Simplification
working on 1010
inEqSimp_contradInEq0
working on 1011
inEqSimp_homoInEq1
working on 1012
polySimp_mulComm0
working on 1013
polySimp_rightDist
working on 1014
mul_literals
working on 1015
polySimp_addAssoc
working on 1016
polySimp_addComm0
working on 1017
polySimp_pullOutFactor1b
working on 1018
add_literals
working on 1019
times_zero
working on 1020
add_zero_right
working on 1021
leq_literals
working on 1022
One Step Simplification
working on 1023
inEqSimp_exactShadow3
working on 1024
polySimp_rightDist
working on 1025
mul_literals
working on 1026
inEqSimp_sepPosMonomial1
working on 1027
polySimp_mulComm0
working on 1028
polySimp_rightDist
working on 1029
mul_literals
working on 1030
polySimp_mulLiterals
working on 1031
polySimp_elimOne
working on 1032
inEqSimp_contradInEq0
working on 1033
andLeft
working on 1034
inEqSimp_homoInEq1
working on 1035
polySimp_mulComm0
working on 1036
polySimp_rightDist
working on 1037
mul_literals
working on 1038
polySimp_addAssoc
working on 1039
polySimp_addComm1
working on 1040
add_literals
working on 1041
polySimp_pullOutFactor1b
working on 1042
add_literals
working on 1043
times_zero
working on 1044
add_zero_right
working on 1045
leq_literals
working on 1046
closeFalse
working on 1047
working on 415
allRight
working on 1048
impRight
working on 1049
andLeft
working on 1050
inEqSimp_ltRight
working on 1051
polySimp_mulComm0
working on 1052
polySimp_pullOutFactor2
working on 1053
add_literals
working on 1054
times_zero
working on 1055
qeq_literals
working on 1056
true_left
working on 1057
inEqSimp_ltToLeq
working on 1058
polySimp_mulComm0
working on 1059
inEqSimp_ltToLeq
working on 1060
polySimp_mulComm0
working on 1061
polySimp_addComm1
working on 1062
inEqSimp_ltToLeq
working on 1063
polySimp_mulComm0
working on 1064
polySimp_addComm1
working on 1065
inEqSimp_ltToLeq
working on 1066
polySimp_mulComm0
working on 1067
inEqSimp_ltToLeq
working on 1068
polySimp_mulComm0
working on 1069
inEqSimp_ltToLeq
working on 1070
add_zero_right
working on 1071
polySimp_mulComm0
working on 1072
inEqSimp_ltToLeq
working on 1073
polySimp_rightDist
working on 1074
mul_literals
working on 1075
polySimp_addAssoc
working on 1076
add_literals
working on 1077
add_zero_left
working on 1078
inEqSimp_ltToLeq
working on 1079
polySimp_mulComm0
working on 1080
polySimp_addComm1
working on 1081
inEqSimp_sepPosMonomial0
working on 1082
polySimp_mulComm0
working on 1083
polySimp_rightDist
working on 1084
mul_literals
working on 1085
polySimp_mulLiterals
working on 1086
polySimp_elimOne
working on 1087
inEqSimp_sepNegMonomial0
working on 1088
polySimp_mulLiterals
working on 1089
polySimp_elimOne
working on 1090
inEqSimp_sepNegMonomial0
working on 1091
polySimp_mulLiterals
working on 1092
polySimp_elimOne
working on 1093
inEqSimp_sepPosMonomial0
working on 1094
polySimp_mulComm0
working on 1095
polySimp_rightDist
working on 1096
mul_literals
working on 1097
polySimp_mulLiterals
working on 1098
polySimp_elimOne
working on 1099
inEqSimp_sepPosMonomial0
working on 1100
polySimp_mulComm0
working on 1101
polySimp_rightDist
working on 1102
mul_literals
working on 1103
polySimp_mulLiterals
working on 1104
polySimp_elimOne
working on 1105
inEqSimp_sepNegMonomial0
working on 1106
polySimp_mulLiterals
working on 1107
polySimp_elimOne
working on 1108
inEqSimp_sepPosMonomial0
working on 1109
polySimp_mulLiterals
working on 1110
polySimp_elimOne
working on 1111
inEqSimp_sepNegMonomial0
working on 1112
polySimp_mulLiterals
working on 1113
polySimp_elimOne
working on 1114
inEqSimp_subsumption1
working on 1115
leq_literals
working on 1116
One Step Simplification
working on 1117
true_left
working on 1118
inEqSimp_subsumption1
working on 1119
inEqSimp_homoInEq0
working on 1120
polySimp_pullOutFactor1b
working on 1121
add_literals
working on 1122
times_zero
working on 1123
add_zero_right
working on 1124
qeq_literals
working on 1125
One Step Simplification
working on 1126
true_left
working on 1127
inEqSimp_contradInEq0
working on 1128
andLeft
working on 1129
inEqSimp_homoInEq1
working on 1130
polySimp_pullOutFactor1b
working on 1131
add_literals
working on 1132
times_zero
working on 1133
add_zero_right
working on 1134
leq_literals
working on 1135
closeFalse
working on 1136
working on 413
polySimp_mulComm0
working on 1137
polySimp_rightDist
working on 1138
mul_literals
working on 1139
precOfInt
working on 1140
inEqSimp_ltRight
working on 1141
polySimp_mulComm0
working on 1142
polySimp_pullOutFactor2
working on 1143
add_literals
working on 1144
times_zero
working on 1145
qeq_literals
working on 1146
true_left
working on 1147
inEqSimp_ltToLeq
working on 1148
polySimp_mulComm0
working on 1149
inEqSimp_ltToLeq
working on 1150
polySimp_mulComm0
working on 1151
polySimp_addComm1
working on 1152
inEqSimp_ltToLeq
working on 1153
polySimp_mulComm0
working on 1154
inEqSimp_ltToLeq
working on 1155
add_zero_right
working on 1156
polySimp_mulComm0
working on 1157
inEqSimp_ltToLeq
working on 1158
polySimp_mulComm0
working on 1159
polySimp_addComm1
working on 1160
inEqSimp_ltToLeq
working on 1161
polySimp_mulComm0
working on 1162
inEqSimp_ltToLeq
working on 1163
polySimp_rightDist
working on 1164
polySimp_mulAssoc
working on 1165
polySimp_mulComm0
working on 1166
polySimp_mulLiterals
working on 1167
polySimp_elimOne
working on 1168
polySimp_addAssoc
working on 1169
polySimp_addAssoc
working on 1170
polySimp_addComm1
working on 1171
polySimp_addAssoc
working on 1172
polySimp_addComm1
working on 1173
add_literals
working on 1174
add_zero_left
working on 1175
polySimp_pullOutFactor1
working on 1176
add_literals
working on 1177
times_zero
working on 1178
add_zero_left
working on 1179
inEqSimp_homoInEq0
working on 1180
times_zero
working on 1181
add_zero_right
working on 1182
applyEq
working on 1183
polySimp_pullOutFactor2
working on 1184
add_literals
working on 1185
times_zero
working on 1186
leq_literals
working on 1187
One Step Simplification
working on 1188
inEqSimp_geqRight
working on 1189
times_zero
working on 1190
add_zero_right
working on 1191
polySimp_addAssoc
working on 1192
polySimp_addAssoc
working on 1193
add_literals
working on 1194
add_zero_left
working on 1195
applyEq
working on 1196
inEqSimp_sepPosMonomial0
working on 1197
polySimp_mulComm0
working on 1198
polySimp_rightDist
working on 1199
mul_literals
working on 1200
polySimp_mulLiterals
working on 1201
polySimp_elimOne
working on 1202
inEqSimp_sepNegMonomial0
working on 1203
polySimp_mulLiterals
working on 1204
polySimp_elimOne
working on 1205
inEqSimp_sepPosMonomial0
working on 1206
polySimp_mulComm0
working on 1207
polySimp_rightDist
working on 1208
mul_literals
working on 1209
polySimp_mulLiterals
working on 1210
polySimp_elimOne
working on 1211
inEqSimp_sepNegMonomial0
working on 1212
polySimp_mulLiterals
working on 1213
polySimp_elimOne
working on 1214
inEqSimp_sepNegMonomial0
working on 1215
polySimp_mulLiterals
working on 1216
polySimp_elimOne
working on 1217
inEqSimp_sepPosMonomial0
working on 1218
polySimp_mulComm0
working on 1219
polySimp_rightDist
working on 1220
mul_literals
working on 1221
polySimp_mulLiterals
working on 1222
polySimp_elimOne
working on 1223
inEqSimp_sepPosMonomial0
working on 1224
polySimp_mulLiterals
working on 1225
polySimp_elimOne
working on 1226
inEqSimp_subsumption1
working on 1227
leq_literals
working on 1228
One Step Simplification
working on 1229
true_left
working on 1230
inEqSimp_subsumption1
working on 1231
inEqSimp_homoInEq0
working on 1232
polySimp_pullOutFactor1b
working on 1233
add_literals
working on 1234
times_zero
working on 1235
add_zero_right
working on 1236
qeq_literals
working on 1237
One Step Simplification
working on 1238
true_left
working on 1239
inEqSimp_contradInEq0
working on 1240
andLeft
working on 1241
inEqSimp_homoInEq1
working on 1242
polySimp_pullOutFactor1b
working on 1243
add_literals
working on 1244
times_zero
working on 1245
add_literals
working on 1246
leq_literals
working on 1247
closeFalse
working on 1248
working on 350
One Step Simplification
working on 1249
One Step Simplification
working on 1250
notLeft
working on 1251
replace_known_right
working on 1252
One Step Simplification
working on 1253
replace_known_left
working on 1254
One Step Simplification
working on 1255
andLeft
working on 1256
replace_known_left
working on 1257
One Step Simplification
working on 1258
true_left
working on 1259
replace_known_right
working on 1260
One Step Simplification
working on 1261
notLeft
working on 1262
replace_known_right
working on 1263
One Step Simplification
working on 1264
assignment
working on 1265
One Step Simplification
working on 1266
assignment
working on 1267
One Step Simplification
working on 1268
blockBreakNoLabel
working on 1269
applyEq
working on 1270
mul_literals
working on 1271
polySimp_addComm0
working on 1272
applyEq
working on 1273
mul_literals
working on 1274
polySimp_addComm0
working on 1275
applyEq
working on 1276
mul_literals
working on 1277
polySimp_addComm0
working on 1278
applyEq
working on 1279
equal_literals
working on 1280
false_right
working on 1281
applyEq
working on 1282
blockBreakLabel
working on 1283
blockEmpty
working on 1284
tryEmpty
working on 1285
methodCallEmpty
working on 1286
emptyModality
working on 1287
One Step Simplification
working on 1288
methodCallReturn
working on 1289
One Step Simplification
working on 1290
assignment
working on 1291
One Step Simplification
working on 1292
methodCallEmpty
working on 1293
tryEmpty
working on 1294
emptyModality
working on 1295
andRight
working on 1296
impRight
working on 1298
andRight
working on 1299
One Step Simplification
working on 1301
One Step Simplification
working on 1302
true_left
working on 1303
inEqSimp_geqRight
working on 1304
mul_literals
working on 1305
add_literals
working on 1306
inEqSimp_ltToLeq
working on 1307
polySimp_mulComm0
working on 1308
polySimp_addComm1
working on 1309
inEqSimp_ltToLeq
working on 1310
polySimp_mulComm0
working on 1311
polySimp_addComm1
working on 1312
inEqSimp_ltToLeq
working on 1313
add_zero_right
working on 1314
polySimp_mulComm0
working on 1315
inEqSimp_ltToLeq
working on 1316
polySimp_mulComm0
working on 1317
inEqSimp_ltToLeq
working on 1318
polySimp_mulComm0
working on 1319
inEqSimp_ltToLeq
working on 1320
polySimp_mulComm0
working on 1321
polySimp_addComm1
working on 1322
inEqSimp_ltToLeq
working on 1323
polySimp_mulComm0
working on 1324
inEqSimp_ltToLeq
working on 1325
polySimp_mulComm0
working on 1326
inEqSimp_homoInEq0
working on 1327
times_zero
working on 1328
add_zero_right
working on 1329
inEqSimp_sepPosMonomial0
working on 1330
mul_literals
working on 1331
inEqSimp_sepNegMonomial0
working on 1332
polySimp_mulLiterals
working on 1333
polySimp_elimOne
working on 1334
inEqSimp_sepNegMonomial0
working on 1335
polySimp_mulLiterals
working on 1336
polySimp_elimOne
working on 1337
inEqSimp_sepNegMonomial0
working on 1338
polySimp_mulLiterals
working on 1339
polySimp_elimOne
working on 1340
inEqSimp_sepPosMonomial0
working on 1341
polySimp_mulComm0
working on 1342
polySimp_rightDist
working on 1343
mul_literals
working on 1344
polySimp_mulLiterals
working on 1345
polySimp_elimOne
working on 1346
inEqSimp_sepPosMonomial0
working on 1347
polySimp_mulComm0
working on 1348
polySimp_rightDist
working on 1349
mul_literals
working on 1350
polySimp_mulLiterals
working on 1351
polySimp_elimOne
working on 1352
inEqSimp_sepNegMonomial0
working on 1353
polySimp_mulLiterals
working on 1354
polySimp_elimOne
working on 1355
inEqSimp_sepPosMonomial0
working on 1356
polySimp_mulComm0
working on 1357
polySimp_rightDist
working on 1358
mul_literals
working on 1359
polySimp_mulLiterals
working on 1360
polySimp_elimOne
working on 1361
inEqSimp_sepPosMonomial0
working on 1362
polySimp_mulComm0
working on 1363
polySimp_rightDist
working on 1364
mul_literals
working on 1365
polySimp_mulLiterals
working on 1366
polySimp_elimOne
working on 1367
inEqSimp_sepPosMonomial1
working on 1368
mul_literals
working on 1369
inEqSimp_contradEq7
working on 1370
polySimp_mulComm0
working on 1371
polySimp_pullOutFactor1b
working on 1372
add_literals
working on 1373
times_zero
working on 1374
add_zero_right
working on 1375
leq_literals
working on 1376
One Step Simplification
working on 1377
false_right
working on 1378
inEqSimp_subsumption1
working on 1379
leq_literals
working on 1380
One Step Simplification
working on 1381
true_left
working on 1382
inEqSimp_contradInEq0
working on 1383
qeq_literals
working on 1384
One Step Simplification
working on 1385
closeFalse
working on 1386
working on 1300
One Step Simplification
working on 1387
One Step Simplification
working on 1388
true_left
working on 1389
qeq_literals
working on 1390
One Step Simplification
working on 1391
notRight
working on 1392
andLeft
working on 1393
inEqSimp_ltToLeq
working on 1394
polySimp_mulComm0
working on 1395
inEqSimp_ltToLeq
working on 1396
polySimp_mulComm0
working on 1397
polySimp_addComm1
working on 1398
inEqSimp_ltToLeq
working on 1399
polySimp_mulComm0
working on 1400
inEqSimp_ltToLeq
working on 1401
polySimp_mulComm0
working on 1402
polySimp_addComm1
working on 1403
inEqSimp_ltToLeq
working on 1404
polySimp_mulComm0
working on 1405
inEqSimp_ltToLeq
working on 1406
add_zero_right
working on 1407
polySimp_mulComm0
working on 1408
inEqSimp_ltToLeq
working on 1409
polySimp_mulComm0
working on 1410
polySimp_addComm1
working on 1411
inEqSimp_ltToLeq
working on 1412
polySimp_mulComm0
working on 1413
inEqSimp_ltToLeq
working on 1414
polySimp_mulComm0
working on 1415
polySimp_addComm1
working on 1416
add_literals
working on 1417
add_zero_left
working on 1418
inEqSimp_ltToLeq
working on 1419
mul_literals
working on 1420
add_literals
working on 1421
inEqSimp_ltToLeq
working on 1422
polySimp_mulComm0
working on 1423
inEqSimp_homoInEq0
working on 1424
times_zero
working on 1425
add_zero_right
working on 1426
inEqSimp_sepPosMonomial0
working on 1427
polySimp_mulComm0
working on 1428
polySimp_rightDist
working on 1429
mul_literals
working on 1430
polySimp_mulLiterals
working on 1431
polySimp_elimOne
working on 1432
inEqSimp_sepNegMonomial0
working on 1433
polySimp_mulLiterals
working on 1434
polySimp_elimOne
working on 1435
inEqSimp_sepPosMonomial0
working on 1436
polySimp_mulComm0
working on 1437
polySimp_rightDist
working on 1438
polySimp_mulLiterals
working on 1439
mul_literals
working on 1440
polySimp_elimOne
working on 1441
inEqSimp_sepNegMonomial0
working on 1442
polySimp_mulLiterals
working on 1443
polySimp_elimOne
working on 1444
inEqSimp_sepPosMonomial0
working on 1445
polySimp_mulComm0
working on 1446
polySimp_rightDist
working on 1447
mul_literals
working on 1448
polySimp_mulLiterals
working on 1449
polySimp_elimOne
working on 1450
inEqSimp_sepNegMonomial0
working on 1451
polySimp_mulLiterals
working on 1452
polySimp_elimOne
working on 1453
inEqSimp_sepNegMonomial0
working on 1454
polySimp_mulLiterals
working on 1455
polySimp_elimOne
working on 1456
inEqSimp_sepPosMonomial0
working on 1457
polySimp_mulComm0
working on 1458
polySimp_rightDist
working on 1459
mul_literals
working on 1460
polySimp_mulLiterals
working on 1461
polySimp_elimOne
working on 1462
inEqSimp_invertInEq0
working on 1463
times_zero
working on 1464
polySimp_mulLiterals
working on 1465
polySimp_elimOne
working on 1466
inEqSimp_sepPosMonomial0
working on 1467
mul_literals
working on 1468
inEqSimp_sepPosMonomial0
working on 1469
polySimp_mulComm0
working on 1470
polySimp_rightDist
working on 1471
polySimp_mulLiterals
working on 1472
mul_literals
working on 1473
polySimp_elimOne
working on 1474
inEqSimp_sepPosMonomial1
working on 1475
mul_literals
working on 1476
inEqSimp_contradEq7
working on 1477
polySimp_mulComm0
working on 1478
polySimp_pullOutFactor1b
working on 1479
add_literals
working on 1480
times_zero
working on 1481
add_zero_right
working on 1482
leq_literals
working on 1483
One Step Simplification
working on 1484
false_right
working on 1485
inEqSimp_subsumption1
working on 1486
leq_literals
working on 1487
One Step Simplification
working on 1488
true_left
working on 1489
inEqSimp_subsumption1
working on 1490
inEqSimp_homoInEq0
working on 1491
polySimp_pullOutFactor1b
working on 1492
add_literals
working on 1493
times_zero
working on 1494
add_zero_right
working on 1495
qeq_literals
working on 1496
One Step Simplification
working on 1497
true_left
working on 1498
inEqSimp_subsumption1
working on 1499
leq_literals
working on 1500
One Step Simplification
working on 1501
true_left
working on 1502
inEqSimp_exactShadow3
working on 1503
polySimp_rightDist
working on 1504
mul_literals
working on 1505
inEqSimp_sepPosMonomial1
working on 1506
polySimp_mulComm0
working on 1507
polySimp_rightDist
working on 1508
polySimp_mulLiterals
working on 1509
mul_literals
working on 1510
polySimp_elimOne
working on 1511
inEqSimp_exactShadow3
working on 1512
polySimp_rightDist
working on 1513
mul_literals
working on 1514
inEqSimp_sepPosMonomial1
working on 1515
polySimp_mulComm0
working on 1516
polySimp_rightDist
working on 1517
mul_literals
working on 1518
polySimp_mulLiterals
working on 1519
polySimp_elimOne
working on 1520
inEqSimp_subsumption1
working on 1521
inEqSimp_homoInEq0
working on 1522
polySimp_mulComm0
working on 1523
polySimp_rightDist
working on 1524
mul_literals
working on 1525
polySimp_addAssoc
working on 1526
polySimp_addComm1
working on 1527
add_literals
working on 1528
polySimp_pullOutFactor1b
working on 1529
add_literals
working on 1530
times_zero
working on 1531
add_zero_right
working on 1532
qeq_literals
working on 1533
One Step Simplification
working on 1534
true_left
working on 1535
inEqSimp_exactShadow3
working on 1536
times_zero
working on 1537
add_zero_left
working on 1538
inEqSimp_sepPosMonomial1
working on 1539
mul_literals
working on 1540
inEqSimp_exactShadow3
working on 1541
mul_literals
working on 1542
inEqSimp_sepPosMonomial1
working on 1543
mul_literals
working on 1544
inEqSimp_subsumption1
working on 1545
leq_literals
working on 1546
One Step Simplification
working on 1547
true_left
working on 1548
nnf_imp2or
working on 1549
nnf_imp2or
working on 1550
nnf_imp2or
working on 1551
nnf_imp2or
working on 1552
nnf_notAnd
working on 1553
inEqSimp_notLeq
working on 1554
polySimp_rightDist
working on 1555
mul_literals
working on 1556
polySimp_addAssoc
working on 1557
add_literals
working on 1558
add_zero_left
working on 1559
inEqSimp_sepPosMonomial1
working on 1560
polySimp_mulLiterals
working on 1561
polySimp_elimOne
working on 1562
inEqSimp_notGeq
working on 1563
polySimp_rightDist
working on 1564
mul_literals
working on 1565
polySimp_addAssoc
working on 1566
add_literals
working on 1567
add_zero_left
working on 1568
inEqSimp_sepPosMonomial0
working on 1569
polySimp_mulLiterals
working on 1570
polySimp_elimOne
working on 1571
nnf_notAnd
working on 1572
inEqSimp_notGeq
working on 1573
times_zero
working on 1574
add_literals
working on 1575
inEqSimp_sepPosMonomial0
working on 1576
mul_literals
working on 1577
nnf_notAnd
working on 1578
inEqSimp_notGeq
working on 1579
times_zero
working on 1580
add_literals
working on 1581
inEqSimp_sepPosMonomial0
working on 1582
mul_literals
working on 1583
inEqSimp_notLeq
working on 1584
mul_literals
working on 1585
add_literals
working on 1586
inEqSimp_sepPosMonomial1
working on 1587
mul_literals
working on 1588
inEqSimp_or_tautInEq0
working on 1589
add_literals
working on 1590
qeq_literals
working on 1591
One Step Simplification
working on 1592
true_left
working on 1593
nnf_notAnd
working on 1594
inEqSimp_notLeq
working on 1595
polySimp_rightDist
working on 1596
mul_literals
working on 1597
polySimp_addAssoc
working on 1598
add_literals
working on 1599
add_zero_left
working on 1600
inEqSimp_sepPosMonomial1
working on 1601
polySimp_mulLiterals
working on 1602
polySimp_elimOne
working on 1603
inEqSimp_notGeq
working on 1604
times_zero
working on 1605
add_literals
working on 1606
inEqSimp_sepPosMonomial0
working on 1607
mul_literals
working on 1608
nnf_notAnd
working on 1609
inEqSimp_notLeq
working on 1610
polySimp_rightDist
working on 1611
mul_literals
working on 1612
polySimp_addAssoc
working on 1613
add_literals
working on 1614
add_zero_left
working on 1615
inEqSimp_sepPosMonomial1
working on 1616
polySimp_mulLiterals
working on 1617
polySimp_elimOne
working on 1618
inEqSimp_notLeq
working on 1619
polySimp_rightDist
working on 1620
mul_literals
working on 1621
polySimp_addAssoc
working on 1622
add_literals
working on 1623
add_zero_left
working on 1624
inEqSimp_sepPosMonomial1
working on 1625
polySimp_mulLiterals
working on 1626
polySimp_elimOne
working on 1627
commute_or
working on 1628
commute_or_2
working on 1629
commute_or
working on 1630
allLeft
working on 1631
replace_known_right
working on 1632
One Step Simplification
working on 1633
inEqSimp_commuteGeq
working on 1634
inEqSimp_contradInEq1
working on 1635
qeq_literals
working on 1636
One Step Simplification
working on 1637
inEqSimp_contradInEq0
working on 1638
andLeft
working on 1639
inEqSimp_homoInEq1
working on 1640
polySimp_pullOutFactor1b
working on 1641
add_literals
working on 1642
times_zero
working on 1643
add_zero_right
working on 1644
leq_literals
working on 1645
closeFalse
working on 1646
working on 1297
impRight
working on 1647
orRight
working on 1648
One Step Simplification
working on 1649
closeFalse
working on 1650
working on 341
One Step Simplification
working on 1651
One Step Simplification
working on 1652
blockEmpty
working on 1653
postincrement
working on 1654
unusedLabel
working on 1655
cast
working on 1656
variableDeclaration
working on 1657
variableDeclaration
working on 1658
remove_parentheses_right
working on 1659
addition
working on 1660
One Step Simplification
working on 1661
translateJavaAdd
working on 1662
polySimp_addComm0
working on 1663
cast
working on 1664
assignment
working on 1665
One Step Simplification
working on 1666
tryEmpty
working on 1667
methodCallEmpty
working on 1668
emptyModality
working on 1669
One Step Simplification
working on 1670
andRight
working on 1671
andRight
working on 1673
andRight
working on 1675
andRight
working on 1677
andRight
working on 1679
andRight
working on 1681
andRight
working on 1683
inEqSimp_geqRight
working on 1685
times_zero
working on 1686
add_zero_right
working on 1687
polySimp_addAssoc
working on 1688
add_literals
working on 1689
inEqSimp_ltToLeq
working on 1690
polySimp_mulComm0
working on 1691
inEqSimp_ltToLeq
working on 1692
polySimp_mulComm0
working on 1693
polySimp_addComm1
working on 1694
inEqSimp_ltToLeq
working on 1695
polySimp_mulComm0
working on 1696
polySimp_addComm1
working on 1697
inEqSimp_ltToLeq
working on 1698
polySimp_mulComm0
working on 1699
inEqSimp_ltToLeq
working on 1700
polySimp_mulComm0
working on 1701
inEqSimp_ltToLeq
working on 1702
add_zero_right
working on 1703
polySimp_mulComm0
working on 1704
inEqSimp_ltToLeq
working on 1705
polySimp_mulComm0
working on 1706
inEqSimp_ltToLeq
working on 1707
polySimp_mulComm0
working on 1708
polySimp_addComm1
working on 1709
inEqSimp_homoInEq0
working on 1710
times_zero
working on 1711
add_zero_right
working on 1712
inEqSimp_sepPosMonomial0
working on 1713
mul_literals
working on 1714
inEqSimp_sepPosMonomial0
working on 1715
polySimp_mulComm0
working on 1716
polySimp_rightDist
working on 1717
polySimp_mulLiterals
working on 1718
mul_literals
working on 1719
polySimp_elimOne
working on 1720
inEqSimp_sepNegMonomial0
working on 1721
polySimp_mulLiterals
working on 1722
polySimp_elimOne
working on 1723
inEqSimp_sepNegMonomial0
working on 1724
polySimp_mulLiterals
working on 1725
polySimp_elimOne
working on 1726
inEqSimp_sepPosMonomial0
working on 1727
polySimp_mulComm0
working on 1728
polySimp_rightDist
working on 1729
mul_literals
working on 1730
polySimp_mulLiterals
working on 1731
polySimp_elimOne
working on 1732
inEqSimp_sepPosMonomial0
working on 1733
polySimp_mulComm0
working on 1734
polySimp_rightDist
working on 1735
mul_literals
working on 1736
polySimp_mulLiterals
working on 1737
polySimp_elimOne
working on 1738
inEqSimp_sepNegMonomial0
working on 1739
polySimp_mulLiterals
working on 1740
polySimp_elimOne
working on 1741
inEqSimp_sepPosMonomial0
working on 1742
polySimp_mulComm0
working on 1743
polySimp_rightDist
working on 1744
mul_literals
working on 1745
polySimp_mulLiterals
working on 1746
polySimp_elimOne
working on 1747
inEqSimp_sepNegMonomial0
working on 1748
polySimp_mulLiterals
working on 1749
polySimp_elimOne
working on 1750
inEqSimp_sepNegMonomial1
working on 1751
polySimp_mulLiterals
working on 1752
polySimp_elimOne
working on 1753
inEqSimp_contradInEq0
working on 1754
qeq_literals
working on 1755
One Step Simplification
working on 1756
closeFalse
working on 1757
working on 1684
inEqSimp_geqRight
working on 1758
polySimp_rightDist
working on 1759
mul_literals
working on 1760
polySimp_addAssoc
working on 1761
add_literals
working on 1762
add_zero_left
working on 1763
inEqSimp_ltToLeq
working on 1764
polySimp_mulComm0
working on 1765
inEqSimp_ltToLeq
working on 1766
polySimp_mulComm0
working on 1767
inEqSimp_ltToLeq
working on 1768
polySimp_mulComm0
working on 1769
inEqSimp_ltToLeq
working on 1770
add_zero_right
working on 1771
polySimp_mulComm0
working on 1772
inEqSimp_ltToLeq
working on 1773
polySimp_mulComm0
working on 1774
polySimp_addComm1
working on 1775
inEqSimp_ltToLeq
working on 1776
polySimp_mulComm0
working on 1777
polySimp_addComm1
working on 1778
inEqSimp_ltToLeq
working on 1779
polySimp_mulComm0
working on 1780
polySimp_addComm1
working on 1781
inEqSimp_ltToLeq
working on 1782
polySimp_mulComm0
working on 1783
inEqSimp_homoInEq0
working on 1784
times_zero
working on 1785
add_zero_right
working on 1786
inEqSimp_sepPosMonomial0
working on 1787
polySimp_mulLiterals
working on 1788
polySimp_elimOne
working on 1789
inEqSimp_sepPosMonomial0
working on 1790
polySimp_mulComm0
working on 1791
polySimp_rightDist
working on 1792
mul_literals
working on 1793
polySimp_mulLiterals
working on 1794
polySimp_elimOne
working on 1795
inEqSimp_sepPosMonomial0
working on 1796
polySimp_mulComm0
working on 1797
polySimp_rightDist
working on 1798
polySimp_mulLiterals
working on 1799
mul_literals
working on 1800
polySimp_elimOne
working on 1801
inEqSimp_sepPosMonomial0
working on 1802
polySimp_mulComm0
working on 1803
polySimp_rightDist
working on 1804
polySimp_mulLiterals
working on 1805
mul_literals
working on 1806
polySimp_elimOne
working on 1807
inEqSimp_sepNegMonomial0
working on 1808
polySimp_mulLiterals
working on 1809
polySimp_elimOne
working on 1810
inEqSimp_sepNegMonomial0
working on 1811
polySimp_mulLiterals
working on 1812
polySimp_elimOne
working on 1813
inEqSimp_sepNegMonomial0
working on 1814
polySimp_mulLiterals
working on 1815
polySimp_elimOne
working on 1816
inEqSimp_sepNegMonomial0
working on 1817
polySimp_mulLiterals
working on 1818
polySimp_elimOne
working on 1819
inEqSimp_sepPosMonomial0
working on 1820
polySimp_mulComm0
working on 1821
polySimp_rightDist
working on 1822
polySimp_mulLiterals
working on 1823
mul_literals
working on 1824
polySimp_elimOne
working on 1825
inEqSimp_sepNegMonomial1
working on 1826
polySimp_mulLiterals
working on 1827
polySimp_elimOne
working on 1828
inEqSimp_subsumption1
working on 1829
inEqSimp_homoInEq0
working on 1830
polySimp_pullOutFactor1b
working on 1831
add_literals
working on 1832
times_zero
working on 1833
add_zero_right
working on 1834
qeq_literals
working on 1835
One Step Simplification
working on 1836
true_left
working on 1837
inEqSimp_contradInEq0
working on 1838
andLeft
working on 1839
inEqSimp_homoInEq1
working on 1840
polySimp_pullOutFactor1b
working on 1841
add_literals
working on 1842
times_zero
working on 1843
add_zero_right
working on 1844
leq_literals
working on 1845
closeFalse
working on 1846
working on 1682
andRight
working on 1847
inEqSimp_leqRight
working on 1849
add_zero_right
working on 1850
polySimp_rightDist
working on 1851
polySimp_mulLiterals
working on 1852
polySimp_elimOne
working on 1853
polySimp_rightDist
working on 1854
mul_literals
working on 1855
polySimp_addAssoc
working on 1856
polySimp_addAssoc
working on 1857
add_literals
working on 1858
inEqSimp_ltToLeq
working on 1859
add_zero_right
working on 1860
polySimp_mulComm0
working on 1861
inEqSimp_ltToLeq
working on 1862
polySimp_mulComm0
working on 1863
polySimp_addComm1
working on 1864
inEqSimp_ltToLeq
working on 1865
polySimp_mulComm0
working on 1866
polySimp_addComm1
working on 1867
inEqSimp_ltToLeq
working on 1868
polySimp_mulComm0
working on 1869
inEqSimp_ltToLeq
working on 1870
polySimp_mulComm0
working on 1871
inEqSimp_ltToLeq
working on 1872
polySimp_mulComm0
working on 1873
inEqSimp_ltToLeq
working on 1874
polySimp_mulComm0
working on 1875
polySimp_addComm1
working on 1876
inEqSimp_ltToLeq
working on 1877
polySimp_mulComm0
working on 1878
inEqSimp_homoInEq0
working on 1879
times_zero
working on 1880
add_zero_right
working on 1881
inEqSimp_sepPosMonomial1
working on 1882
polySimp_mulComm0
working on 1883
polySimp_rightDist
working on 1884
polySimp_mulLiterals
working on 1885
mul_literals
working on 1886
polySimp_elimOne
working on 1887
inEqSimp_sepNegMonomial0
working on 1888
polySimp_mulLiterals
working on 1889
polySimp_elimOne
working on 1890
inEqSimp_sepNegMonomial0
working on 1891
polySimp_mulLiterals
working on 1892
polySimp_elimOne
working on 1893
inEqSimp_sepNegMonomial0
working on 1894
polySimp_mulLiterals
working on 1895
polySimp_elimOne
working on 1896
inEqSimp_sepPosMonomial0
working on 1897
polySimp_mulComm0
working on 1898
polySimp_rightDist
working on 1899
mul_literals
working on 1900
polySimp_mulLiterals
working on 1901
polySimp_elimOne
working on 1902
inEqSimp_sepPosMonomial0
working on 1903
polySimp_mulComm0
working on 1904
polySimp_rightDist
working on 1905
mul_literals
working on 1906
polySimp_mulLiterals
working on 1907
polySimp_elimOne
working on 1908
inEqSimp_sepPosMonomial0
working on 1909
polySimp_mulComm0
working on 1910
polySimp_rightDist
working on 1911
polySimp_mulLiterals
working on 1912
mul_literals
working on 1913
polySimp_elimOne
working on 1914
inEqSimp_sepNegMonomial0
working on 1915
polySimp_mulLiterals
working on 1916
polySimp_elimOne
working on 1917
inEqSimp_sepPosMonomial0
working on 1918
polySimp_mulComm0
working on 1919
polySimp_rightDist
working on 1920
polySimp_mulLiterals
working on 1921
mul_literals
working on 1922
polySimp_elimOne
working on 1923
inEqSimp_sepNegMonomial1
working on 1924
polySimp_mulLiterals
working on 1925
polySimp_elimOne
working on 1926
inEqSimp_subsumption1
working on 1927
leq_literals
working on 1928
One Step Simplification
working on 1929
true_left
working on 1930
inEqSimp_contradInEq0
working on 1931
andLeft
working on 1932
inEqSimp_homoInEq1
working on 1933
polySimp_pullOutFactor1b
working on 1934
add_literals
working on 1935
times_zero
working on 1936
add_zero_right
working on 1937
leq_literals
working on 1938
closeFalse
working on 1939
working on 1848
inEqSimp_geqRight
working on 1940
polySimp_rightDist
working on 1941
polySimp_mulLiterals
working on 1942
polySimp_elimOne
working on 1943
polySimp_rightDist
working on 1944
mul_literals
working on 1945
polySimp_addAssoc
working on 1946
polySimp_addAssoc
working on 1947
add_literals
working on 1948
add_zero_left
working on 1949
inEqSimp_ltToLeq
working on 1950
polySimp_mulComm0
working on 1951
polySimp_addComm1
working on 1952
inEqSimp_ltToLeq
working on 1953
polySimp_mulComm0
working on 1954
polySimp_addComm1
working on 1955
inEqSimp_ltToLeq
working on 1956
polySimp_mulComm0
working on 1957
inEqSimp_ltToLeq
working on 1958
polySimp_mulComm0
working on 1959
inEqSimp_ltToLeq
working on 1960
polySimp_mulComm0
working on 1961
polySimp_addComm1
working on 1962
inEqSimp_ltToLeq
working on 1963
add_zero_right
working on 1964
polySimp_mulComm0
working on 1965
inEqSimp_ltToLeq
working on 1966
polySimp_mulComm0
working on 1967
inEqSimp_ltToLeq
working on 1968
polySimp_mulComm0
working on 1969
inEqSimp_homoInEq0
working on 1970
times_zero
working on 1971
add_zero_right
working on 1972
inEqSimp_sepPosMonomial0
working on 1973
polySimp_mulComm0
working on 1974
polySimp_rightDist
working on 1975
polySimp_mulAssoc
working on 1976
polySimp_mulComm0
working on 1977
polySimp_mulLiterals
working on 1978
polySimp_elimOne
working on 1979
inEqSimp_sepNegMonomial0
working on 1980
polySimp_mulLiterals
working on 1981
polySimp_elimOne
working on 1982
inEqSimp_sepNegMonomial0
working on 1983
polySimp_mulLiterals
working on 1984
polySimp_elimOne
working on 1985
inEqSimp_sepPosMonomial0
working on 1986
polySimp_mulComm0
working on 1987
polySimp_rightDist
working on 1988
mul_literals
working on 1989
polySimp_mulLiterals
working on 1990
polySimp_elimOne
working on 1991
inEqSimp_sepPosMonomial0
working on 1992
polySimp_mulComm0
working on 1993
polySimp_rightDist
working on 1994
mul_literals
working on 1995
polySimp_mulLiterals
working on 1996
polySimp_elimOne
working on 1997
inEqSimp_sepNegMonomial0
working on 1998
polySimp_mulLiterals
working on 1999
polySimp_elimOne
working on 2000
inEqSimp_sepNegMonomial0
working on 2001
polySimp_mulLiterals
working on 2002
polySimp_elimOne
working on 2003
inEqSimp_sepPosMonomial0
working on 2004
polySimp_mulComm0
working on 2005
polySimp_rightDist
working on 2006
polySimp_mulLiterals
working on 2007
mul_literals
working on 2008
polySimp_elimOne
working on 2009
inEqSimp_sepPosMonomial0
working on 2010
polySimp_mulComm0
working on 2011
polySimp_rightDist
working on 2012
polySimp_mulLiterals
working on 2013
mul_literals
working on 2014
polySimp_elimOne
working on 2015
inEqSimp_sepNegMonomial1
working on 2016
polySimp_mulLiterals
working on 2017
polySimp_elimOne
working on 2018
inEqSimp_subsumption1
working on 2019
inEqSimp_homoInEq0
working on 2020
polySimp_pullOutFactor1b
working on 2021
add_literals
working on 2022
times_zero
working on 2023
add_zero_right
working on 2024
qeq_literals
working on 2025
One Step Simplification
working on 2026
true_left
working on 2027
inEqSimp_subsumption1
working on 2028
leq_literals
working on 2029
One Step Simplification
working on 2030
true_left
working on 2031
inEqSimp_antiSymm
working on 2032
applyEq
working on 2033
applyEq
working on 2034
inEqSimp_homoInEq1
working on 2035
polySimp_pullOutFactor1
working on 2036
add_literals
working on 2037
times_zero
working on 2038
leq_literals
working on 2039
true_left
working on 2040
applyEq
working on 2041
applyEq
working on 2042
inEqSimp_homoInEq0
working on 2043
polySimp_pullOutFactor1
working on 2044
add_literals
working on 2045
times_zero
working on 2046
qeq_literals
working on 2047
true_left
working on 2048
applyEq
working on 2049
inEqSimp_sepNegMonomial1
working on 2050
polySimp_mulLiterals
working on 2051
polySimp_elimOne
working on 2052
inEqSimp_exactShadow3
working on 2053
polySimp_rightDist
working on 2054
mul_literals
working on 2055
polySimp_addAssoc
working on 2056
polySimp_pullOutFactor2b
working on 2057
add_literals
working on 2058
times_zero
working on 2059
add_zero_right
working on 2060
inEqSimp_sepNegMonomial1
working on 2061
polySimp_mulLiterals
working on 2062
polySimp_elimOne
working on 2063
inEqSimp_contradEq3
working on 2064
times_zero
working on 2065
add_zero_right
working on 2066
qeq_literals
working on 2067
One Step Simplification
working on 2068
notLeft
working on 2069
replace_known_right
working on 2070
One Step Simplification
working on 2071
replace_known_right
working on 2072
One Step Simplification
working on 2073
replace_known_left
working on 2074
One Step Simplification
working on 2075
inEqSimp_contradEq3
working on 2076
times_zero
working on 2077
add_zero_right
working on 2078
qeq_literals
working on 2079
One Step Simplification
working on 2080
replace_known_left
working on 2081
One Step Simplification
working on 2082
applyEq
working on 2083
mul_literals
working on 2084
polySimp_addComm0
working on 2085
applyEq
working on 2086
mul_literals
working on 2087
polySimp_addComm0
working on 2088
applyEq
working on 2089
inEqSimp_commuteLeq
working on 2090
applyEq
working on 2091
leq_literals
working on 2092
closeFalse
working on 2093
working on 1680
orRight
working on 2094
andRight
working on 2095
replace_known_right
working on 2097
One Step Simplification
working on 2098
closeFalse
working on 2099
working on 2096
replace_known_right
working on 2100
One Step Simplification
working on 2101
replace_known_right
working on 2102
One Step Simplification
working on 2103
replace_known_left
working on 2104
One Step Simplification
working on 2105
replace_known_right
working on 2106
One Step Simplification
working on 2107
notLeft
working on 2108
replace_known_right
working on 2109
One Step Simplification
working on 2110
replace_known_left
working on 2111
One Step Simplification
working on 2112
inEqSimp_ltRight
working on 2113
polySimp_rightDist
working on 2114
mul_literals
working on 2115
inEqSimp_ltToLeq
working on 2116
polySimp_mulComm0
working on 2117
polySimp_addComm1
working on 2118
inEqSimp_ltToLeq
working on 2119
polySimp_mulComm0
working on 2120
inEqSimp_ltToLeq
working on 2121
polySimp_mulComm0
working on 2122
inEqSimp_ltToLeq
working on 2123
polySimp_mulComm0
working on 2124
polySimp_addComm1
working on 2125
inEqSimp_ltToLeq
working on 2126
add_zero_right
working on 2127
polySimp_mulComm0
working on 2128
inEqSimp_ltToLeq
working on 2129
polySimp_mulComm0
working on 2130
inEqSimp_ltToLeq
working on 2131
polySimp_mulComm0
working on 2132
inEqSimp_ltToLeq
working on 2133
polySimp_mulComm0
working on 2134
polySimp_addComm1
working on 2135
inEqSimp_homoInEq0
working on 2136
times_zero
working on 2137
add_zero_right
working on 2138
applyEq
working on 2139
mul_literals
working on 2140
polySimp_addComm0
working on 2141
applyEq
working on 2142
mul_literals
working on 2143
polySimp_addComm0
working on 2144
applyEq
working on 2145
equal_literals
working on 2146
false_right
working on 2147
applyEq
working on 2148
mul_literals
working on 2149
polySimp_addComm0
working on 2150
inEqSimp_sepPosMonomial1
working on 2151
polySimp_mulComm0
working on 2152
polySimp_rightDist
working on 2153
polySimp_mulLiterals
working on 2154
mul_literals
working on 2155
polySimp_elimOne
working on 2156
inEqSimp_sepNegMonomial0
working on 2157
polySimp_mulLiterals
working on 2158
polySimp_elimOne
working on 2159
inEqSimp_sepPosMonomial0
working on 2160
polySimp_mulComm0
working on 2161
polySimp_rightDist
working on 2162
mul_literals
working on 2163
polySimp_mulLiterals
working on 2164
polySimp_elimOne
working on 2165
inEqSimp_sepPosMonomial0
working on 2166
polySimp_mulComm0
working on 2167
polySimp_rightDist
working on 2168
mul_literals
working on 2169
polySimp_mulLiterals
working on 2170
polySimp_elimOne
working on 2171
inEqSimp_sepNegMonomial0
working on 2172
polySimp_mulLiterals
working on 2173
polySimp_elimOne
working on 2174
inEqSimp_sepNegMonomial0
working on 2175
polySimp_mulLiterals
working on 2176
polySimp_elimOne
working on 2177
inEqSimp_sepPosMonomial0
working on 2178
polySimp_mulComm0
working on 2179
polySimp_rightDist
working on 2180
mul_literals
working on 2181
polySimp_mulLiterals
working on 2182
polySimp_elimOne
working on 2183
inEqSimp_sepPosMonomial0
working on 2184
polySimp_mulComm0
working on 2185
polySimp_rightDist
working on 2186
mul_literals
working on 2187
polySimp_mulLiterals
working on 2188
polySimp_elimOne
working on 2189
inEqSimp_sepNegMonomial0
working on 2190
polySimp_mulLiterals
working on 2191
polySimp_elimOne
working on 2192
inEqSimp_sepPosMonomial1
working on 2193
mul_literals
working on 2194
inEqSimp_contradEq7
working on 2195
polySimp_mulComm0
working on 2196
polySimp_pullOutFactor1b
working on 2197
add_literals
working on 2198
times_zero
working on 2199
add_zero_right
working on 2200
leq_literals
working on 2201
One Step Simplification
working on 2202
false_right
working on 2203
inEqSimp_subsumption1
working on 2204
leq_literals
working on 2205
One Step Simplification
working on 2206
true_left
working on 2207
inEqSimp_subsumption1
working on 2208
inEqSimp_homoInEq0
working on 2209
polySimp_pullOutFactor1b
working on 2210
add_literals
working on 2211
times_zero
working on 2212
add_zero_right
working on 2213
qeq_literals
working on 2214
One Step Simplification
working on 2215
true_left
working on 2216
inEqSimp_subsumption1
working on 2217
leq_literals
working on 2218
One Step Simplification
working on 2219
true_left
working on 2220
inEqSimp_contradInEq0
working on 2221
andLeft
working on 2222
inEqSimp_homoInEq1
working on 2223
polySimp_mulComm0
working on 2224
polySimp_rightDist
working on 2225
mul_literals
working on 2226
polySimp_addAssoc
working on 2227
polySimp_addComm1
working on 2228
add_literals
working on 2229
polySimp_pullOutFactor1b
working on 2230
add_literals
working on 2231
times_zero
working on 2232
add_zero_right
working on 2233
leq_literals
working on 2234
closeFalse
working on 2235
working on 1678
inEqSimp_ltToLeq
working on 2236
polySimp_mulComm0
working on 2237
polySimp_addComm1
working on 2238
inEqSimp_ltToLeq
working on 2239
polySimp_mulComm0
working on 2240
polySimp_addComm1
working on 2241
inEqSimp_ltToLeq
working on 2242
polySimp_mulComm0
working on 2243
polySimp_addComm1
working on 2244
inEqSimp_ltToLeq
working on 2245
polySimp_mulComm0
working on 2246
inEqSimp_ltToLeq
working on 2247
polySimp_mulComm0
working on 2248
inEqSimp_ltToLeq
working on 2249
polySimp_mulComm0
working on 2250
inEqSimp_ltToLeq
working on 2251
polySimp_mulComm0
working on 2252
polySimp_addComm1
working on 2253
inEqSimp_ltToLeq
working on 2254
add_zero_right
working on 2255
polySimp_mulComm0
working on 2256
inEqSimp_ltToLeq
working on 2257
polySimp_mulComm0
working on 2258
inEqSimp_homoInEq0
working on 2259
times_zero
working on 2260
add_zero_right
working on 2261
inEqSimp_sepNegMonomial0
working on 2262
polySimp_mulLiterals
working on 2263
polySimp_elimOne
working on 2264
inEqSimp_sepNegMonomial0
working on 2265
polySimp_mulLiterals
working on 2266
polySimp_elimOne
working on 2267
inEqSimp_sepNegMonomial0
working on 2268
polySimp_mulLiterals
working on 2269
polySimp_elimOne
working on 2270
inEqSimp_sepPosMonomial0
working on 2271
polySimp_mulComm0
working on 2272
polySimp_rightDist
working on 2273
mul_literals
working on 2274
polySimp_mulLiterals
working on 2275
polySimp_elimOne
working on 2276
inEqSimp_sepPosMonomial0
working on 2277
polySimp_mulComm0
working on 2278
polySimp_rightDist
working on 2279
mul_literals
working on 2280
polySimp_mulLiterals
working on 2281
polySimp_elimOne
working on 2282
inEqSimp_sepPosMonomial0
working on 2283
polySimp_mulComm0
working on 2284
polySimp_rightDist
working on 2285
mul_literals
working on 2286
polySimp_mulLiterals
working on 2287
polySimp_elimOne
working on 2288
inEqSimp_sepNegMonomial0
working on 2289
polySimp_mulLiterals
working on 2290
polySimp_elimOne
working on 2291
inEqSimp_sepNegMonomial0
working on 2292
polySimp_mulLiterals
working on 2293
polySimp_elimOne
working on 2294
inEqSimp_sepPosMonomial0
working on 2295
polySimp_mulComm0
working on 2296
polySimp_rightDist
working on 2297
mul_literals
working on 2298
polySimp_mulLiterals
working on 2299
polySimp_elimOne
working on 2300
inEqSimp_sepNegMonomial1
working on 2301
polySimp_mulLiterals
working on 2302
polySimp_elimOne
working on 2303
inEqSimp_subsumption1
working on 2304
leq_literals
working on 2305
One Step Simplification
working on 2306
true_left
working on 2307
inEqSimp_subsumption1
working on 2308
inEqSimp_homoInEq0
working on 2309
polySimp_pullOutFactor1b
working on 2310
add_literals
working on 2311
times_zero
working on 2312
add_zero_right
working on 2313
qeq_literals
working on 2314
One Step Simplification
working on 2315
true_left
working on 2316
inEqSimp_exactShadow3
working on 2317
mul_literals
working on 2318
inEqSimp_sepPosMonomial1
working on 2319
mul_literals
working on 2320
inEqSimp_subsumption1
working on 2321
leq_literals
working on 2322
One Step Simplification
working on 2323
true_left
working on 2324
inEqSimp_exactShadow3
working on 2325
polySimp_rightDist
working on 2326
mul_literals
working on 2327
inEqSimp_sepPosMonomial1
working on 2328
polySimp_mulComm0
working on 2329
polySimp_rightDist
working on 2330
mul_literals
working on 2331
polySimp_mulLiterals
working on 2332
polySimp_elimOne
working on 2333
nnf_imp2or
working on 2334
nnf_imp2or
working on 2335
nnf_notAnd
working on 2336
inEqSimp_notGeq
working on 2337
times_zero
working on 2338
add_literals
working on 2339
inEqSimp_sepPosMonomial0
working on 2340
mul_literals
working on 2341
nnf_notAnd
working on 2342
inEqSimp_notGeq
working on 2343
polySimp_rightDist
working on 2344
mul_literals
working on 2345
polySimp_addAssoc
working on 2346
add_literals
working on 2347
add_zero_left
working on 2348
inEqSimp_sepPosMonomial0
working on 2349
polySimp_mulLiterals
working on 2350
polySimp_elimOne
working on 2351
inEqSimp_notLeq
working on 2352
polySimp_rightDist
working on 2353
mul_literals
working on 2354
polySimp_addAssoc
working on 2355
add_literals
working on 2356
add_zero_left
working on 2357
inEqSimp_sepPosMonomial1
working on 2358
polySimp_mulLiterals
working on 2359
polySimp_elimOne
working on 2360
nnf_notAnd
working on 2361
inEqSimp_notLeq
working on 2362
polySimp_rightDist
working on 2363
mul_literals
working on 2364
polySimp_addAssoc
working on 2365
add_literals
working on 2366
add_zero_left
working on 2367
inEqSimp_sepPosMonomial1
working on 2368
polySimp_mulLiterals
working on 2369
polySimp_elimOne
working on 2370
inEqSimp_notLeq
working on 2371
polySimp_rightDist
working on 2372
mul_literals
working on 2373
polySimp_addAssoc
working on 2374
add_literals
working on 2375
add_zero_left
working on 2376
inEqSimp_sepPosMonomial1
working on 2377
polySimp_mulLiterals
working on 2378
polySimp_elimOne
working on 2379
commute_and
working on 2380
close
working on 2381
working on 1676
allRight
working on 2382
impRight
working on 2383
andLeft
working on 2384
andLeft
working on 2385
inEqSimp_ltToLeq
working on 2386
polySimp_mulComm0
working on 2387
polySimp_addComm1
working on 2388
inEqSimp_ltToLeq
working on 2389
add_zero_right
working on 2390
polySimp_mulComm0
working on 2391
inEqSimp_ltToLeq
working on 2392
polySimp_mulComm0
working on 2393
inEqSimp_ltToLeq
working on 2394
polySimp_mulComm0
working on 2395
inEqSimp_ltToLeq
working on 2396
polySimp_mulComm0
working on 2397
polySimp_addComm1
working on 2398
inEqSimp_ltToLeq
working on 2399
polySimp_mulComm0
working on 2400
inEqSimp_ltToLeq
working on 2401
polySimp_mulComm0
working on 2402
polySimp_addComm1
working on 2403
inEqSimp_ltToLeq
working on 2404
polySimp_mulComm0
working on 2405
inEqSimp_ltToLeq
working on 2406
polySimp_rightDist
working on 2407
mul_literals
working on 2408
polySimp_addAssoc
working on 2409
add_literals
working on 2410
add_zero_left
working on 2411
inEqSimp_ltToLeq
working on 2412
polySimp_mulComm0
working on 2413
polySimp_addComm1
working on 2414
inEqSimp_homoInEq0
working on 2415
times_zero
working on 2416
add_zero_right
working on 2417
inEqSimp_sepNegMonomial0
working on 2418
polySimp_mulLiterals
working on 2419
polySimp_elimOne
working on 2420
inEqSimp_sepNegMonomial0
working on 2421
polySimp_mulLiterals
working on 2422
polySimp_elimOne
working on 2423
inEqSimp_sepPosMonomial0
working on 2424
polySimp_mulComm0
working on 2425
polySimp_rightDist
working on 2426
polySimp_mulLiterals
working on 2427
mul_literals
working on 2428
polySimp_elimOne
working on 2429
inEqSimp_sepPosMonomial0
working on 2430
polySimp_mulComm0
working on 2431
polySimp_rightDist
working on 2432
polySimp_mulLiterals
working on 2433
mul_literals
working on 2434
polySimp_elimOne
working on 2435
inEqSimp_sepNegMonomial0
working on 2436
polySimp_mulLiterals
working on 2437
polySimp_elimOne
working on 2438
inEqSimp_sepPosMonomial0
working on 2439
polySimp_mulComm0
working on 2440
polySimp_rightDist
working on 2441
polySimp_mulLiterals
working on 2442
mul_literals
working on 2443
polySimp_elimOne
working on 2444
inEqSimp_sepNegMonomial0
working on 2445
polySimp_mulLiterals
working on 2446
polySimp_elimOne
working on 2447
inEqSimp_sepPosMonomial0
working on 2448
polySimp_mulComm0
working on 2449
polySimp_rightDist
working on 2450
polySimp_mulLiterals
working on 2451
mul_literals
working on 2452
polySimp_elimOne
working on 2453
inEqSimp_sepPosMonomial0
working on 2454
polySimp_mulLiterals
working on 2455
polySimp_elimOne
working on 2456
inEqSimp_sepNegMonomial0
working on 2457
polySimp_mulLiterals
working on 2458
polySimp_elimOne
working on 2459
inEqSimp_sepNegMonomial1
working on 2460
polySimp_mulLiterals
working on 2461
polySimp_elimOne
working on 2462
inEqSimp_subsumption1
working on 2463
inEqSimp_homoInEq0
working on 2464
polySimp_pullOutFactor1b
working on 2465
add_literals
working on 2466
times_zero
working on 2467
add_zero_right
working on 2468
qeq_literals
working on 2469
One Step Simplification
working on 2470
true_left
working on 2471
inEqSimp_subsumption1
working on 2472
leq_literals
working on 2473
One Step Simplification
working on 2474
true_left
working on 2475
inEqSimp_exactShadow3
working on 2476
polySimp_rightDist
working on 2477
mul_literals
working on 2478
inEqSimp_sepPosMonomial1
working on 2479
polySimp_mulComm0
working on 2480
polySimp_rightDist
working on 2481
polySimp_mulLiterals
working on 2482
mul_literals
working on 2483
polySimp_elimOne
working on 2484
inEqSimp_exactShadow3
working on 2485
times_zero
working on 2486
add_zero_left
working on 2487
inEqSimp_exactShadow3
working on 2488
mul_literals
working on 2489
inEqSimp_sepPosMonomial1
working on 2490
mul_literals
working on 2491
inEqSimp_subsumption1
working on 2492
leq_literals
working on 2493
One Step Simplification
working on 2494
true_left
working on 2495
nnf_imp2or
working on 2496
nnf_imp2or
working on 2497
nnf_notAnd
working on 2498
inEqSimp_notGeq
working on 2499
times_zero
working on 2500
add_literals
working on 2501
inEqSimp_sepPosMonomial0
working on 2502
mul_literals
working on 2503
nnf_notAnd
working on 2504
inEqSimp_notGeq
working on 2505
polySimp_rightDist
working on 2506
mul_literals
working on 2507
polySimp_addAssoc
working on 2508
add_literals
working on 2509
add_zero_left
working on 2510
inEqSimp_sepPosMonomial0
working on 2511
polySimp_mulLiterals
working on 2512
polySimp_elimOne
working on 2513
inEqSimp_notLeq
working on 2514
polySimp_rightDist
working on 2515
mul_literals
working on 2516
polySimp_addAssoc
working on 2517
add_literals
working on 2518
add_zero_left
working on 2519
inEqSimp_sepPosMonomial1
working on 2520
polySimp_mulLiterals
working on 2521
polySimp_elimOne
working on 2522
nnf_notAnd
working on 2523
inEqSimp_notLeq
working on 2524
polySimp_rightDist
working on 2525
mul_literals
working on 2526
polySimp_addAssoc
working on 2527
add_literals
working on 2528
add_zero_left
working on 2529
inEqSimp_sepPosMonomial1
working on 2530
polySimp_mulLiterals
working on 2531
polySimp_elimOne
working on 2532
inEqSimp_notLeq
working on 2533
polySimp_rightDist
working on 2534
mul_literals
working on 2535
polySimp_addAssoc
working on 2536
add_literals
working on 2537
add_zero_left
working on 2538
inEqSimp_sepPosMonomial1
working on 2539
polySimp_mulLiterals
working on 2540
polySimp_elimOne
working on 2541
commute_and
working on 2542
commute_or
working on 2543
commute_or_2
working on 2544
commute_or
working on 2545
equiv_left
working on 2546
replace_known_left
working on 2548
One Step Simplification
working on 2549
true_left
working on 2550
replace_known_left
working on 2551
One Step Simplification
working on 2552
true_left
working on 2553
replace_known_left
working on 2554
One Step Simplification
working on 2555
true_left
working on 2556
applyEq
working on 2557
times_zero
working on 2558
add_zero_right
working on 2559
eqSymm
working on 2560
applyEq
working on 2561
applyEq
working on 2562
inEqSimp_commuteLeq
working on 2563
applyEq
working on 2564
inEqSimp_commuteLeq
working on 2565
applyEq
working on 2566
applyEq
working on 2567
times_zero
working on 2568
add_zero_right
working on 2569
applyEq
working on 2570
inEqSimp_homoInEq1
working on 2571
polySimp_pullOutFactor1b
working on 2572
add_literals
working on 2573
times_zero
working on 2574
add_zero_right
working on 2575
leq_literals
working on 2576
One Step Simplification
working on 2577
notLeft
working on 2578
applyEq
working on 2579
applyEq
working on 2580
equal_literals
working on 2581
false_right
working on 2582
inEqSimp_subsumption1
working on 2583
inEqSimp_homoInEq0
working on 2584
polySimp_pullOutFactor1b
working on 2585
add_literals
working on 2586
times_zero
working on 2587
add_zero_right
working on 2588
qeq_literals
working on 2589
One Step Simplification
working on 2590
true_left
working on 2591
allLeft
working on 2592
replace_known_right
working on 2593
One Step Simplification
working on 2594
inEqSimp_commuteGeq
working on 2595
inEqSimp_contradInEq1
working on 2596
inEqSimp_homoInEq1
working on 2597
polySimp_pullOutFactor1b
working on 2598
add_literals
working on 2599
times_zero
working on 2600
add_zero_right
working on 2601
leq_literals
working on 2602
One Step Simplification
working on 2603
inEqSimp_contradInEq1
working on 2604
qeq_literals
working on 2605
One Step Simplification
working on 2606
inEqSimp_antiSymm
working on 2607
applyEq
working on 2608
eqSymm
working on 2609
applyEq
working on 2610
inEqSimp_homoInEq0
working on 2611
polySimp_pullOutFactor1
working on 2612
add_literals
working on 2613
times_zero
working on 2614
qeq_literals
working on 2615
true_left
working on 2616
applyEq
working on 2617
applyEq
working on 2618
inEqSimp_homoInEq1
working on 2619
polySimp_pullOutFactor1
working on 2620
add_literals
working on 2621
times_zero
working on 2622
leq_literals
working on 2623
true_left
working on 2624
applyEq
working on 2625
applyEq
working on 2626
eqSymm
working on 2627
close
working on 2628
working on 2547
replace_known_right
working on 2629
One Step Simplification
working on 2630
replace_known_right
working on 2631
One Step Simplification
working on 2632
replace_known_right
working on 2633
One Step Simplification
working on 2634
replace_known_left
working on 2635
One Step Simplification
working on 2636
applyEq
working on 2637
mul_literals
working on 2638
polySimp_addComm0
working on 2639
applyEq
working on 2640
mul_literals
working on 2641
polySimp_addComm0
working on 2642
applyEq
working on 2643
equal_literals
working on 2644
false_right
working on 2645
applyEq
working on 2646
inEqSimp_commuteLeq
working on 2647
inEqSimp_contradEq7
working on 2648
polySimp_mulComm0
working on 2649
polySimp_pullOutFactor1b
working on 2650
add_literals
working on 2651
times_zero
working on 2652
add_zero_right
working on 2653
leq_literals
working on 2654
One Step Simplification
working on 2655
false_right
working on 2656
inEqSimp_subsumption1
working on 2657
inEqSimp_homoInEq0
working on 2658
polySimp_mulComm0
working on 2659
polySimp_rightDist
working on 2660
mul_literals
working on 2661
polySimp_addAssoc
working on 2662
polySimp_addComm1
working on 2663
add_literals
working on 2664
polySimp_pullOutFactor1b
working on 2665
add_literals
working on 2666
times_zero
working on 2667
add_zero_right
working on 2668
qeq_literals
working on 2669
One Step Simplification
working on 2670
true_left
working on 2671
inEqSimp_subsumption1
working on 2672
leq_literals
working on 2673
One Step Simplification
working on 2674
true_left
working on 2675
inEqSimp_exactShadow3
working on 2676
polySimp_rightDist
working on 2677
mul_literals
working on 2678
polySimp_addComm1
working on 2679
polySimp_addAssoc
working on 2680
add_literals
working on 2681
inEqSimp_sepNegMonomial1
working on 2682
polySimp_mulLiterals
working on 2683
polySimp_elimOne
working on 2684
inEqSimp_subsumption0
working on 2685
inEqSimp_homoInEq0
working on 2686
polySimp_mulComm0
working on 2687
polySimp_rightDist
working on 2688
mul_literals
working on 2689
polySimp_addAssoc
working on 2690
polySimp_addComm0
working on 2691
polySimp_pullOutFactor1b
working on 2692
add_literals
working on 2693
times_zero
working on 2694
add_zero_right
working on 2695
qeq_literals
working on 2696
One Step Simplification
working on 2697
true_left
working on 2698
inEqSimp_exactShadow3
working on 2699
times_zero
working on 2700
add_zero_left
working on 2701
inEqSimp_sepPosMonomial1
working on 2702
mul_literals
working on 2703
inEqSimp_exactShadow3
working on 2704
polySimp_rightDist
working on 2705
mul_literals
working on 2706
inEqSimp_sepPosMonomial1
working on 2707
polySimp_mulComm0
working on 2708
polySimp_rightDist
working on 2709
mul_literals
working on 2710
polySimp_mulLiterals
working on 2711
polySimp_elimOne
working on 2712
inEqSimp_exactShadow3
working on 2713
times_zero
working on 2714
add_zero_left
working on 2715
inEqSimp_sepPosMonomial1
working on 2716
mul_literals
working on 2717
inEqSimp_subsumption1
working on 2718
leq_literals
working on 2719
One Step Simplification
working on 2720
true_left
working on 2721
allLeft
working on 2722
replace_known_right
working on 2723
One Step Simplification
working on 2724
inEqSimp_commuteGeq
working on 2725
inEqSimp_contradInEq0
working on 2726
inEqSimp_homoInEq1
working on 2727
polySimp_mulComm0
working on 2728
polySimp_rightDist
working on 2729
mul_literals
working on 2730
polySimp_addAssoc
working on 2731
polySimp_addComm0
working on 2732
polySimp_pullOutFactor1b
working on 2733
add_literals
working on 2734
times_zero
working on 2735
add_zero_right
working on 2736
leq_literals
working on 2737
One Step Simplification
working on 2738
inEqSimp_contradInEq1
working on 2739
inEqSimp_homoInEq1
working on 2740
polySimp_pullOutFactor1b
working on 2741
add_literals
working on 2742
times_zero
working on 2743
add_zero_right
working on 2744
leq_literals
working on 2745
One Step Simplification
working on 2746
inEqSimp_contradInEq0
working on 2747
qeq_literals
working on 2748
One Step Simplification
working on 2749
closeFalse
working on 2750
working on 1674
allRight
working on 2751
impRight
working on 2752
andLeft
working on 2753
inEqSimp_ltToLeq
working on 2754
polySimp_mulComm0
working on 2755
inEqSimp_ltToLeq
working on 2756
polySimp_mulComm0
working on 2757
inEqSimp_ltToLeq
working on 2758
add_zero_right
working on 2759
polySimp_mulComm0
working on 2760
inEqSimp_ltToLeq
working on 2761
polySimp_mulComm0
working on 2762
inEqSimp_ltToLeq
working on 2763
polySimp_mulComm0
working on 2764
inEqSimp_ltToLeq
working on 2765
polySimp_mulComm0
working on 2766
polySimp_addComm1
working on 2767
inEqSimp_ltToLeq
working on 2768
polySimp_mulComm0
working on 2769
polySimp_addComm1
working on 2770
inEqSimp_ltToLeq
working on 2771
polySimp_mulComm0
working on 2772
polySimp_addComm1
working on 2773
inEqSimp_ltToLeq
working on 2774
polySimp_mulComm0
working on 2775
inEqSimp_ltToLeq
working on 2776
polySimp_rightDist
working on 2777
mul_literals
working on 2778
polySimp_addAssoc
working on 2779
add_literals
working on 2780
add_zero_left
working on 2781
inEqSimp_homoInEq0
working on 2782
mul_literals
working on 2783
add_zero_right
working on 2784
inEqSimp_sepPosMonomial0
working on 2785
polySimp_mulComm0
working on 2786
polySimp_rightDist
working on 2787
polySimp_mulLiterals
working on 2788
mul_literals
working on 2789
polySimp_elimOne
working on 2790
inEqSimp_sepPosMonomial0
working on 2791
polySimp_mulComm0
working on 2792
polySimp_rightDist
working on 2793
polySimp_mulLiterals
working on 2794
mul_literals
working on 2795
polySimp_elimOne
working on 2796
inEqSimp_sepNegMonomial0
working on 2797
polySimp_mulLiterals
working on 2798
polySimp_elimOne
working on 2799
inEqSimp_sepPosMonomial0
working on 2800
polySimp_mulComm0
working on 2801
polySimp_rightDist
working on 2802
polySimp_mulLiterals
working on 2803
mul_literals
working on 2804
polySimp_elimOne
working on 2805
inEqSimp_sepPosMonomial0
working on 2806
polySimp_mulComm0
working on 2807
polySimp_rightDist
working on 2808
polySimp_mulLiterals
working on 2809
mul_literals
working on 2810
polySimp_elimOne
working on 2811
inEqSimp_sepNegMonomial0
working on 2812
polySimp_mulLiterals
working on 2813
polySimp_elimOne
working on 2814
inEqSimp_sepNegMonomial0
working on 2815
polySimp_mulLiterals
working on 2816
polySimp_elimOne
working on 2817
inEqSimp_sepNegMonomial0
working on 2818
polySimp_mulLiterals
working on 2819
polySimp_elimOne
working on 2820
inEqSimp_sepPosMonomial0
working on 2821
polySimp_mulComm0
working on 2822
polySimp_rightDist
working on 2823
polySimp_mulLiterals
working on 2824
mul_literals
working on 2825
polySimp_elimOne
working on 2826
inEqSimp_sepPosMonomial0
working on 2827
polySimp_mulLiterals
working on 2828
polySimp_elimOne
working on 2829
inEqSimp_sepNegMonomial1
working on 2830
polySimp_mulLiterals
working on 2831
polySimp_elimOne
working on 2832
inEqSimp_subsumption1
working on 2833
leq_literals
working on 2834
One Step Simplification
working on 2835
true_left
working on 2836
inEqSimp_subsumption1
working on 2837
inEqSimp_homoInEq0
working on 2838
polySimp_pullOutFactor1b
working on 2839
add_literals
working on 2840
times_zero
working on 2841
add_zero_right
working on 2842
qeq_literals
working on 2843
One Step Simplification
working on 2844
true_left
working on 2845
inEqSimp_exactShadow3
working on 2846
polySimp_rightDist
working on 2847
mul_literals
working on 2848
inEqSimp_sepPosMonomial1
working on 2849
polySimp_mulComm0
working on 2850
polySimp_rightDist
working on 2851
mul_literals
working on 2852
polySimp_mulLiterals
working on 2853
polySimp_elimOne
working on 2854
inEqSimp_exactShadow3
working on 2855
mul_literals
working on 2856
inEqSimp_sepPosMonomial1
working on 2857
mul_literals
working on 2858
inEqSimp_subsumption1
working on 2859
leq_literals
working on 2860
One Step Simplification
working on 2861
true_left
working on 2862
nnf_imp2or
working on 2863
nnf_imp2or
working on 2864
nnf_notAnd
working on 2865
inEqSimp_notGeq
working on 2866
times_zero
working on 2867
add_literals
working on 2868
inEqSimp_sepPosMonomial0
working on 2869
mul_literals
working on 2870
nnf_notAnd
working on 2871
inEqSimp_notLeq
working on 2872
polySimp_rightDist
working on 2873
mul_literals
working on 2874
polySimp_addAssoc
working on 2875
add_literals
working on 2876
add_zero_left
working on 2877
inEqSimp_sepPosMonomial1
working on 2878
polySimp_mulLiterals
working on 2879
polySimp_elimOne
working on 2880
inEqSimp_notGeq
working on 2881
polySimp_rightDist
working on 2882
mul_literals
working on 2883
polySimp_addAssoc
working on 2884
add_literals
working on 2885
add_zero_left
working on 2886
inEqSimp_sepPosMonomial0
working on 2887
polySimp_mulLiterals
working on 2888
polySimp_elimOne
working on 2889
nnf_notAnd
working on 2890
inEqSimp_notLeq
working on 2891
polySimp_rightDist
working on 2892
mul_literals
working on 2893
polySimp_addAssoc
working on 2894
add_literals
working on 2895
add_zero_left
working on 2896
inEqSimp_sepPosMonomial1
working on 2897
polySimp_mulLiterals
working on 2898
polySimp_elimOne
working on 2899
inEqSimp_notLeq
working on 2900
polySimp_rightDist
working on 2901
mul_literals
working on 2902
polySimp_addAssoc
working on 2903
add_literals
working on 2904
add_zero_left
working on 2905
inEqSimp_sepPosMonomial1
working on 2906
polySimp_mulLiterals
working on 2907
polySimp_elimOne
working on 2908
commute_and
working on 2909
commute_or
working on 2910
commute_or_2
working on 2911
commute_or
working on 2912
equiv_left
working on 2913
replace_known_left
working on 2915
One Step Simplification
working on 2916
true_left
working on 2917
replace_known_left
working on 2918
One Step Simplification
working on 2919
true_left
working on 2920
replace_known_left
working on 2921
One Step Simplification
working on 2922
true_left
working on 2923
applyEq
working on 2924
times_zero
working on 2925
add_zero_right
working on 2926
applyEq
working on 2927
inEqSimp_commuteLeq
working on 2928
applyEq
working on 2929
applyEq
working on 2930
applyEq
working on 2931
times_zero
working on 2932
add_zero_right
working on 2933
eqSymm
working on 2934
applyEq
working on 2935
inEqSimp_commuteLeq
working on 2936
applyEq
working on 2937
applyEq
working on 2938
equal_literals
working on 2939
One Step Simplification
working on 2940
notLeft
working on 2941
applyEq
working on 2942
inEqSimp_homoInEq1
working on 2943
polySimp_pullOutFactor1b
working on 2944
add_literals
working on 2945
times_zero
working on 2946
add_zero_right
working on 2947
leq_literals
working on 2948
One Step Simplification
working on 2949
false_right
working on 2950
inEqSimp_subsumption1
working on 2951
inEqSimp_homoInEq0
working on 2952
polySimp_pullOutFactor1b
working on 2953
add_literals
working on 2954
times_zero
working on 2955
add_zero_right
working on 2956
qeq_literals
working on 2957
One Step Simplification
working on 2958
true_left
working on 2959
inEqSimp_exactShadow3
working on 2960
mul_literals
working on 2961
polySimp_addAssoc
working on 2962
add_literals
working on 2963
inEqSimp_sepPosMonomial1
working on 2964
mul_literals
working on 2965
inEqSimp_exactShadow3
working on 2966
polySimp_rightDist
working on 2967
mul_literals
working on 2968
polySimp_addAssoc
working on 2969
polySimp_addComm1
working on 2970
add_literals
working on 2971
inEqSimp_sepPosMonomial1
working on 2972
polySimp_mulComm0
working on 2973
polySimp_rightDist
working on 2974
mul_literals
working on 2975
polySimp_mulLiterals
working on 2976
polySimp_elimOne
working on 2977
inEqSimp_contradInEq0
working on 2978
andLeft
working on 2979
inEqSimp_homoInEq1
working on 2980
polySimp_pullOutFactor1b
working on 2981
add_literals
working on 2982
times_zero
working on 2983
add_zero_right
working on 2984
leq_literals
working on 2985
closeFalse
working on 2986
working on 2914
replace_known_right
working on 2987
One Step Simplification
working on 2988
replace_known_right
working on 2989
One Step Simplification
working on 2990
replace_known_right
working on 2991
One Step Simplification
working on 2992
replace_known_left
working on 2993
One Step Simplification
working on 2994
applyEq
working on 2995
equal_literals
working on 2996
false_right
working on 2997
applyEq
working on 2998
mul_literals
working on 2999
polySimp_addComm0
working on 3000
applyEq
working on 3001
mul_literals
working on 3002
polySimp_addComm0
working on 3003
applyEq
working on 3004
inEqSimp_commuteLeq
working on 3005
inEqSimp_contradEq7
working on 3006
polySimp_mulComm0
working on 3007
polySimp_pullOutFactor1b
working on 3008
add_literals
working on 3009
times_zero
working on 3010
add_zero_right
working on 3011
leq_literals
working on 3012
One Step Simplification
working on 3013
false_right
working on 3014
inEqSimp_subsumption1
working on 3015
inEqSimp_homoInEq0
working on 3016
polySimp_mulComm0
working on 3017
polySimp_rightDist
working on 3018
mul_literals
working on 3019
polySimp_addAssoc
working on 3020
polySimp_addComm1
working on 3021
add_literals
working on 3022
polySimp_pullOutFactor1b
working on 3023
add_literals
working on 3024
times_zero
working on 3025
add_zero_right
working on 3026
qeq_literals
working on 3027
One Step Simplification
working on 3028
true_left
working on 3029
inEqSimp_subsumption1
working on 3030
leq_literals
working on 3031
One Step Simplification
working on 3032
true_left
working on 3033
inEqSimp_exactShadow3
working on 3034
polySimp_rightDist
working on 3035
mul_literals
working on 3036
inEqSimp_sepPosMonomial1
working on 3037
polySimp_mulComm0
working on 3038
polySimp_rightDist
working on 3039
mul_literals
working on 3040
polySimp_mulLiterals
working on 3041
polySimp_elimOne
working on 3042
inEqSimp_exactShadow3
working on 3043
times_zero
working on 3044
add_zero_left
working on 3045
inEqSimp_sepPosMonomial1
working on 3046
mul_literals
working on 3047
inEqSimp_exactShadow3
working on 3048
mul_literals
working on 3049
add_zero_left
working on 3050
inEqSimp_sepPosMonomial1
working on 3051
mul_literals
working on 3052
inEqSimp_exactShadow3
working on 3053
mul_literals
working on 3054
inEqSimp_sepPosMonomial1
working on 3055
mul_literals
working on 3056
allLeft
working on 3057
replace_known_right
working on 3058
One Step Simplification
working on 3059
inEqSimp_commuteLeq
working on 3060
inEqSimp_contradInEq0
working on 3061
inEqSimp_homoInEq1
working on 3062
polySimp_mulComm0
working on 3063
polySimp_rightDist
working on 3064
mul_literals
working on 3065
polySimp_addAssoc
working on 3066
polySimp_addComm0
working on 3067
polySimp_pullOutFactor1b
working on 3068
add_literals
working on 3069
times_zero
working on 3070
add_zero_right
working on 3071
leq_literals
working on 3072
One Step Simplification
working on 3073
inEqSimp_antiSymm
working on 3074
applyEq
working on 3075
inEqSimp_homoInEq1
working on 3076
polySimp_pullOutFactor1
working on 3077
add_literals
working on 3078
times_zero
working on 3079
leq_literals
working on 3080
true_left
working on 3081
applyEq
working on 3082
applyEq
working on 3083
eqSymm
working on 3084
applyEq
working on 3085
inEqSimp_homoInEq0
working on 3086
polySimp_pullOutFactor1
working on 3087
add_literals
working on 3088
times_zero
working on 3089
qeq_literals
working on 3090
true_left
working on 3091
applyEq
working on 3092
applyEq
working on 3093
eqSymm
working on 3094
close
working on 3095
working on 1672
polySimp_mulComm0
working on 3096
polySimp_rightDist
working on 3097
mul_literals
working on 3098
precOfInt
working on 3099
inEqSimp_ltToLeq
working on 3100
polySimp_mulComm0
working on 3101
polySimp_addComm1
working on 3102
inEqSimp_ltToLeq
working on 3103
polySimp_mulComm0
working on 3104
inEqSimp_ltToLeq
working on 3105
polySimp_mulComm0
working on 3106
inEqSimp_ltToLeq
working on 3107
polySimp_mulComm0
working on 3108
polySimp_addComm1
working on 3109
inEqSimp_ltToLeq
working on 3110
add_zero_right
working on 3111
polySimp_mulComm0
working on 3112
inEqSimp_ltToLeq
working on 3113
polySimp_mulComm0
working on 3114
inEqSimp_ltToLeq
working on 3115
polySimp_mulComm0
working on 3116
polySimp_addComm1
working on 3117
inEqSimp_ltToLeq
working on 3118
polySimp_mulComm0
working on 3119
inEqSimp_ltToLeq
working on 3120
polySimp_rightDist
working on 3121
polySimp_mulAssoc
working on 3122
polySimp_mulComm0
working on 3123
polySimp_mulLiterals
working on 3124
polySimp_elimOne
working on 3125
polySimp_addAssoc
working on 3126
polySimp_addAssoc
working on 3127
polySimp_addComm1
working on 3128
polySimp_pullOutFactor2b
working on 3129
add_literals
working on 3130
times_zero
working on 3131
add_zero_right
working on 3132
polySimp_addAssoc
working on 3133
polySimp_addComm1
working on 3134
add_literals
working on 3135
add_zero_left
working on 3136
polySimp_pullOutFactor1
working on 3137
add_literals
working on 3138
times_zero
working on 3139
leq_literals
working on 3140
One Step Simplification
working on 3141
inEqSimp_leqRight
working on 3142
add_zero_right
working on 3143
polySimp_rightDist
working on 3144
polySimp_rightDist
working on 3145
polySimp_mulLiterals
working on 3146
mul_literals
working on 3147
polySimp_elimOne
working on 3148
polySimp_addAssoc
working on 3149
polySimp_addAssoc
working on 3150
add_literals
working on 3151
add_zero_left
working on 3152
inEqSimp_homoInEq0
working on 3153
times_zero
working on 3154
add_zero_right
working on 3155
inEqSimp_sepNegMonomial0
working on 3156
polySimp_mulLiterals
working on 3157
polySimp_elimOne
working on 3158
inEqSimp_sepPosMonomial0
working on 3159
polySimp_mulComm0
working on 3160
polySimp_rightDist
working on 3161
mul_literals
working on 3162
polySimp_mulLiterals
working on 3163
polySimp_elimOne
working on 3164
inEqSimp_sepPosMonomial0
working on 3165
polySimp_mulComm0
working on 3166
polySimp_rightDist
working on 3167
polySimp_mulLiterals
working on 3168
mul_literals
working on 3169
polySimp_elimOne
working on 3170
inEqSimp_sepNegMonomial0
working on 3171
polySimp_mulLiterals
working on 3172
polySimp_elimOne
working on 3173
inEqSimp_sepNegMonomial0
working on 3174
polySimp_mulLiterals
working on 3175
polySimp_elimOne
working on 3176
inEqSimp_sepPosMonomial0
working on 3177
polySimp_mulComm0
working on 3178
polySimp_rightDist
working on 3179
mul_literals
working on 3180
polySimp_mulLiterals
working on 3181
polySimp_elimOne
working on 3182
inEqSimp_sepNegMonomial0
working on 3183
polySimp_mulLiterals
working on 3184
polySimp_elimOne
working on 3185
inEqSimp_sepPosMonomial0
working on 3186
polySimp_mulComm0
working on 3187
polySimp_rightDist
working on 3188
mul_literals
working on 3189
polySimp_mulLiterals
working on 3190
polySimp_elimOne
working on 3191
inEqSimp_sepNegMonomial1
working on 3192
polySimp_mulLiterals
working on 3193
polySimp_elimOne
working on 3194
inEqSimp_sepNegMonomial1
working on 3195
polySimp_mulLiterals
working on 3196
polySimp_elimOne
working on 3197
inEqSimp_subsumption1
working on 3198
inEqSimp_homoInEq0
working on 3199
polySimp_pullOutFactor1b
working on 3200
add_literals
working on 3201
times_zero
working on 3202
add_zero_right
working on 3203
qeq_literals
working on 3204
One Step Simplification
working on 3205
true_left
working on 3206
inEqSimp_contradInEq1
working on 3207
andLeft
working on 3208
inEqSimp_homoInEq1
working on 3209
polySimp_pullOutFactor1b
working on 3210
add_literals
working on 3211
times_zero
working on 3212
add_zero_right
working on 3213
leq_literals
working on 3214
closeFalse
working on 3215
working on 334
One Step Simplification
working on 3216
closeFalse
working on 3217
working on 335
One Step Simplification
working on 3218
false_right
working on 3219
inEqSimp_ltToLeq
working on 3220
polySimp_mulComm0
working on 3221
polySimp_addComm1
working on 3222
inEqSimp_ltToLeq
working on 3223
polySimp_mulComm0
working on 3224
polySimp_addComm1
working on 3225
inEqSimp_ltToLeq
working on 3226
polySimp_mulComm0
working on 3227
polySimp_addComm1
working on 3228
inEqSimp_ltToLeq
working on 3229
polySimp_mulComm0
working on 3230
inEqSimp_ltToLeq
working on 3231
polySimp_mulComm0
working on 3232
inEqSimp_ltToLeq
working on 3233
polySimp_mulComm0
working on 3234
inEqSimp_ltToLeq
working on 3235
polySimp_mulComm0
working on 3236
inEqSimp_ltToLeq
working on 3237
add_zero_right
working on 3238
polySimp_mulComm0
working on 3239
inEqSimp_ltToLeq
working on 3240
times_zero
working on 3241
add_zero_right
working on 3242
polySimp_addAssoc
working on 3243
inEqSimp_homoInEq0
working on 3244
times_zero
working on 3245
add_zero_right
working on 3246
inEqSimp_sepNegMonomial0
working on 3247
polySimp_mulLiterals
working on 3248
polySimp_elimOne
working on 3249
inEqSimp_sepNegMonomial0
working on 3250
polySimp_mulLiterals
working on 3251
polySimp_elimOne
working on 3252
inEqSimp_sepNegMonomial0
working on 3253
polySimp_mulLiterals
working on 3254
polySimp_elimOne
working on 3255
inEqSimp_sepPosMonomial0
working on 3256
polySimp_mulComm0
working on 3257
polySimp_rightDist
working on 3258
polySimp_mulLiterals
working on 3259
mul_literals
working on 3260
polySimp_elimOne
working on 3261
inEqSimp_sepPosMonomial0
working on 3262
polySimp_mulComm0
working on 3263
polySimp_rightDist
working on 3264
polySimp_mulLiterals
working on 3265
mul_literals
working on 3266
polySimp_elimOne
working on 3267
inEqSimp_sepPosMonomial0
working on 3268
polySimp_mulComm0
working on 3269
polySimp_rightDist
working on 3270
polySimp_mulLiterals
working on 3271
mul_literals
working on 3272
polySimp_elimOne
working on 3273
inEqSimp_sepPosMonomial0
working on 3274
polySimp_mulComm0
working on 3275
polySimp_rightDist
working on 3276
mul_literals
working on 3277
polySimp_mulLiterals
working on 3278
polySimp_elimOne
working on 3279
inEqSimp_sepNegMonomial0
working on 3280
polySimp_mulLiterals
working on 3281
polySimp_elimOne
working on 3282
inEqSimp_sepNegMonomial0
working on 3283
polySimp_mulLiterals
working on 3284
polySimp_elimOne
working on 3285
inEqSimp_sepNegMonomial1
working on 3286
polySimp_mulLiterals
working on 3287
polySimp_elimOne
working on 3288
inEqSimp_subsumption1
working on 3289
inEqSimp_homoInEq0
working on 3290
polySimp_pullOutFactor1b
working on 3291
add_literals
working on 3292
times_zero
working on 3293
add_zero_right
working on 3294
qeq_literals
working on 3295
One Step Simplification
working on 3296
true_left
working on 3297
inEqSimp_contradInEq0
working on 3298
inEqSimp_homoInEq1
working on 3299
polySimp_pullOutFactor1b
working on 3300
add_literals
working on 3301
times_zero
working on 3302
add_zero_right
working on 3303
leq_literals
working on 3304
One Step Simplification
working on 3305
inEqSimp_subsumption1
working on 3306
leq_literals
working on 3307
One Step Simplification
working on 3308
true_left
working on 3309
inEqSimp_antiSymm
working on 3310
applyEq
working on 3311
inEqSimp_homoInEq0
working on 3312
polySimp_pullOutFactor1
working on 3313
add_literals
working on 3314
times_zero
working on 3315
qeq_literals
working on 3316
true_left
working on 3317
applyEq
working on 3318
inEqSimp_homoInEq1
working on 3319
polySimp_pullOutFactor1
working on 3320
add_literals
working on 3321
times_zero
working on 3322
leq_literals
working on 3323
true_left
working on 3324
applyEq
working on 3325
applyEq
working on 3326
applyEq
working on 3327
inEqSimp_sepNegMonomial1
working on 3328
polySimp_mulLiterals
working on 3329
polySimp_elimOne
working on 3330
inEqSimp_exactShadow3
working on 3331
mul_literals
working on 3332
polySimp_addAssoc
working on 3333
inEqSimp_sepNegMonomial1
working on 3334
polySimp_mulLiterals
working on 3335
polySimp_elimOne
working on 3336
inEqSimp_subsumption0
working on 3337
inEqSimp_homoInEq0
working on 3338
polySimp_mulComm0
working on 3339
polySimp_rightDist
working on 3340
mul_literals
working on 3341
polySimp_addAssoc
working on 3342
polySimp_addComm0
working on 3343
polySimp_pullOutFactor1b
working on 3344
add_literals
working on 3345
times_zero
working on 3346
add_zero_right
working on 3347
qeq_literals
working on 3348
One Step Simplification
working on 3349
true_left
working on 3350
inEqSimp_exactShadow3
working on 3351
polySimp_rightDist
working on 3352
mul_literals
working on 3353
polySimp_addAssoc
working on 3354
polySimp_pullOutFactor2b
working on 3355
add_literals
working on 3356
times_zero
working on 3357
add_zero_right
working on 3358
inEqSimp_sepNegMonomial1
working on 3359
polySimp_mulLiterals
working on 3360
polySimp_elimOne
working on 3361
inEqSimp_contradEq3
working on 3362
mul_literals
working on 3363
add_literals
working on 3364
qeq_literals
working on 3365
One Step Simplification
working on 3366
replace_known_left
working on 3367
One Step Simplification
working on 3368
replace_known_left
working on 3369
One Step Simplification
working on 3370
true_left
working on 3371
replace_known_left
working on 3372
One Step Simplification
working on 3373
true_left
working on 3374
applyEq
working on 3375
applyEq
working on 3376
equal_literals
working on 3377
One Step Simplification
working on 3378
notLeft
working on 3379
applyEq
working on 3380
inEqSimp_homoInEq0
working on 3381
times_zero
working on 3382
add_zero_right
working on 3383
applyEq
working on 3384
times_zero
working on 3385
add_zero_right
working on 3386
applyEq
working on 3387
leq_literals
working on 3388
closeFalse
working on 3389
working on 317
One Step Simplification
working on 3390
closeFalse
working on 3391
working on 318
One Step Simplification
working on 3392
false_right
working on 3393
inEqSimp_ltToLeq
working on 3394
polySimp_mulComm0
working on 3395
inEqSimp_ltToLeq
working on 3396
polySimp_mulComm0
working on 3397
inEqSimp_ltToLeq
working on 3398
polySimp_mulComm0
working on 3399
polySimp_addComm1
working on 3400
inEqSimp_ltToLeq
working on 3401
add_zero_right
working on 3402
polySimp_mulComm0
working on 3403
inEqSimp_ltToLeq
working on 3404
polySimp_mulComm0
working on 3405
inEqSimp_ltToLeq
working on 3406
polySimp_mulComm0
working on 3407
polySimp_addComm1
working on 3408
inEqSimp_ltToLeq
working on 3409
polySimp_mulComm0
working on 3410
inEqSimp_ltToLeq
working on 3411
polySimp_mulComm0
working on 3412
polySimp_addComm1
working on 3413
inEqSimp_ltToLeq
working on 3414
times_zero
working on 3415
add_zero_right
working on 3416
inEqSimp_homoInEq0
working on 3417
times_zero
working on 3418
add_zero_right
working on 3419
inEqSimp_sepPosMonomial0
working on 3420
polySimp_mulComm0
working on 3421
polySimp_rightDist
working on 3422
polySimp_mulLiterals
working on 3423
mul_literals
working on 3424
polySimp_elimOne
working on 3425
inEqSimp_sepPosMonomial0
working on 3426
polySimp_mulComm0
working on 3427
polySimp_rightDist
working on 3428
polySimp_mulLiterals
working on 3429
mul_literals
working on 3430
polySimp_elimOne
working on 3431
inEqSimp_sepNegMonomial0
working on 3432
polySimp_mulLiterals
working on 3433
polySimp_elimOne
working on 3434
inEqSimp_sepNegMonomial0
working on 3435
polySimp_mulLiterals
working on 3436
polySimp_elimOne
working on 3437
inEqSimp_sepPosMonomial0
working on 3438
polySimp_mulComm0
working on 3439
polySimp_rightDist
working on 3440
mul_literals
working on 3441
polySimp_mulLiterals
working on 3442
polySimp_elimOne
working on 3443
inEqSimp_sepNegMonomial0
working on 3444
polySimp_mulLiterals
working on 3445
polySimp_elimOne
working on 3446
inEqSimp_sepPosMonomial0
working on 3447
polySimp_mulComm0
working on 3448
polySimp_rightDist
working on 3449
polySimp_mulLiterals
working on 3450
mul_literals
working on 3451
polySimp_elimOne
working on 3452
inEqSimp_sepNegMonomial0
working on 3453
polySimp_mulLiterals
working on 3454
polySimp_elimOne
working on 3455
inEqSimp_sepPosMonomial0
working on 3456
mul_literals
working on 3457
inEqSimp_sepNegMonomial1
working on 3458
polySimp_mulLiterals
working on 3459
polySimp_elimOne
working on 3460
inEqSimp_contradInEq1
working on 3461
inEqSimp_homoInEq1
working on 3462
polySimp_pullOutFactor1b
working on 3463
add_literals
working on 3464
times_zero
working on 3465
add_zero_right
working on 3466
leq_literals
working on 3467
One Step Simplification
working on 3468
inEqSimp_subsumption1
working on 3469
leq_literals
working on 3470
One Step Simplification
working on 3471
true_left
working on 3472
inEqSimp_subsumption1
working on 3473
inEqSimp_homoInEq0
working on 3474
polySimp_pullOutFactor1b
working on 3475
add_literals
working on 3476
times_zero
working on 3477
add_zero_right
working on 3478
qeq_literals
working on 3479
One Step Simplification
working on 3480
true_left
working on 3481
inEqSimp_contradInEq0
working on 3482
qeq_literals
working on 3483
One Step Simplification
working on 3484
closeFalse
working on 3485
working on 307
One Step Simplification
working on 3486
One Step Simplification
working on 3487
closeFalse
working on 3488
working on 296
One Step Simplification
working on 3489
closeFalse
working on 3490
working on 278
false_right
working on 3491
One Step Simplification
working on 3492
closeFalse
working on 3493
working on 43
One Step Simplification
working on 3494
One Step Simplification
working on 3495
andLeft
working on 3496
andLeft
working on 3497
andLeft
working on 3498
andLeft
working on 3499
andLeft
working on 3500
andLeft
working on 3501
andLeft
working on 3502
andLeft
working on 3503
andLeft
working on 3504
eqSymm
working on 3505
eqSymm
working on 3506
eqSymm
working on 3507
polySimp_elimSub
working on 3508
polySimp_elimSub
working on 3509
polySimp_elimSub
working on 3510
mul_literals
working on 3511
polySimp_addComm0
working on 3512
inEqSimp_commuteLeq
working on 3513
inEqSimp_commuteLeq
working on 3514
inEqSimp_commuteLeq
working on 3515
inEqSimp_commuteLeq
working on 3516
inEqSimp_commuteLeq
working on 3517
inEqSimp_commuteLeq
working on 3518
variableDeclaration
working on 3519
variableDeclaration
working on 3520
commute_or
working on 3521
cnf_rightDist
working on 3522
andLeft
working on 3523
commute_or
working on 3524
commute_and
working on 3525
commute_and_2
working on 3526
commute_and
working on 3527
commute_and_2
working on 3528
less_than
working on 3529
variableDeclaration
working on 3530
variableDeclaration
working on 3531
assignment
working on 3532
One Step Simplification
working on 3533
variableDeclaration
working on 3534
variableDeclaration
working on 3535
assignment_read_length
working on 3536
One Step Simplification
working on 3538
lesser than distinction
working on 3539
One Step Simplification
working on 3540
methodCallEmpty
working on 3541
emptyModality
working on 3542
One Step Simplification
working on 3543
impRight
working on 3544
notLeft
working on 3545
methodCallReturn
working on 3546
assignment
working on 3547
One Step Simplification
working on 3548
methodCallEmpty
working on 3549
tryEmpty
working on 3550
emptyModality
working on 3551
andRight
working on 3552
impRight
working on 3554
andRight
working on 3555
One Step Simplification
working on 3557
One Step Simplification
working on 3558
true_left
working on 3559
inEqSimp_ltRight
working on 3560
polySimp_mulComm0
working on 3561
polySimp_addComm0
working on 3562
inEqSimp_geqRight
working on 3563
polySimp_mulComm0
working on 3564
inEqSimp_ltToLeq
working on 3565
polySimp_mulComm0
working on 3566
polySimp_addComm1
working on 3567
inEqSimp_ltToLeq
working on 3568
add_zero_right
working on 3569
polySimp_mulComm0
working on 3570
inEqSimp_ltToLeq
working on 3571
polySimp_mulComm0
working on 3572
inEqSimp_ltToLeq
working on 3573
polySimp_mulComm0
working on 3574
inEqSimp_ltToLeq
working on 3575
polySimp_mulComm0
working on 3576
polySimp_addComm1
working on 3577
inEqSimp_ltToLeq
working on 3578
polySimp_mulComm0
working on 3579
inEqSimp_ltToLeq
working on 3580
polySimp_mulComm0
working on 3581
inEqSimp_homoInEq0
working on 3582
mul_literals
working on 3583
add_zero_right
working on 3584
inEqSimp_sepNegMonomial1
working on 3585
polySimp_mulLiterals
working on 3586
polySimp_elimOne
working on 3587
inEqSimp_sepPosMonomial0
working on 3588
polySimp_mulComm0
working on 3589
polySimp_rightDist
working on 3590
polySimp_mulLiterals
working on 3591
mul_literals
working on 3592
polySimp_elimOne
working on 3593
inEqSimp_sepNegMonomial0
working on 3594
polySimp_mulLiterals
working on 3595
polySimp_elimOne
working on 3596
inEqSimp_sepNegMonomial0
working on 3597
polySimp_mulLiterals
working on 3598
polySimp_elimOne
working on 3599
inEqSimp_sepPosMonomial0
working on 3600
polySimp_mulComm0
working on 3601
polySimp_rightDist
working on 3602
polySimp_mulLiterals
working on 3603
mul_literals
working on 3604
polySimp_elimOne
working on 3605
inEqSimp_sepPosMonomial0
working on 3606
polySimp_mulComm0
working on 3607
polySimp_rightDist
working on 3608
polySimp_mulLiterals
working on 3609
mul_literals
working on 3610
polySimp_elimOne
working on 3611
inEqSimp_sepNegMonomial0
working on 3612
polySimp_mulLiterals
working on 3613
polySimp_elimOne
working on 3614
inEqSimp_sepPosMonomial0
working on 3615
polySimp_mulComm0
working on 3616
polySimp_rightDist
working on 3617
polySimp_mulLiterals
working on 3618
mul_literals
working on 3619
polySimp_elimOne
working on 3620
inEqSimp_sepPosMonomial0
working on 3621
polySimp_mulComm0
working on 3622
polySimp_rightDist
working on 3623
polySimp_mulLiterals
working on 3624
mul_literals
working on 3625
polySimp_elimOne
working on 3626
inEqSimp_sepNegMonomial1
working on 3627
polySimp_mulLiterals
working on 3628
polySimp_elimOne
working on 3629
inEqSimp_contradEq3
working on 3630
polySimp_mulComm0
working on 3631
polySimp_pullOutFactor1b
working on 3632
add_literals
working on 3633
times_zero
working on 3634
add_zero_right
working on 3635
qeq_literals
working on 3636
One Step Simplification
working on 3637
replace_known_left
working on 3638
One Step Simplification
working on 3639
inEqSimp_contradEq3
working on 3640
polySimp_mulComm0
working on 3641
polySimp_pullOutFactor1b
working on 3642
add_literals
working on 3643
times_zero
working on 3644
add_zero_right
working on 3645
qeq_literals
working on 3646
One Step Simplification
working on 3647
notLeft
working on 3648
replace_known_right
working on 3649
One Step Simplification
working on 3650
replace_known_left
working on 3651
One Step Simplification
working on 3652
applyEq
working on 3653
inEqSimp_commuteLeq
working on 3654
applyEq
working on 3655
equal_literals
working on 3656
false_right
working on 3657
applyEq
working on 3658
mul_literals
working on 3659
polySimp_addComm0
working on 3660
inEqSimp_contradEq3
working on 3661
polySimp_mulComm0
working on 3662
polySimp_pullOutFactor1b
working on 3663
add_literals
working on 3664
times_zero
working on 3665
add_zero_right
working on 3666
qeq_literals
working on 3667
One Step Simplification
working on 3668
inEqSimp_contradInEq1
working on 3669
andLeft
working on 3670
inEqSimp_homoInEq1
working on 3671
polySimp_mulComm0
working on 3672
polySimp_rightDist
working on 3673
mul_literals
working on 3674
polySimp_addAssoc
working on 3675
polySimp_addComm1
working on 3676
add_literals
working on 3677
polySimp_pullOutFactor1b
working on 3678
add_literals
working on 3679
times_zero
working on 3680
add_zero_right
working on 3681
leq_literals
working on 3682
closeFalse
working on 3683
working on 3556
One Step Simplification
working on 3684
One Step Simplification
working on 3685
true_left
working on 3686
inEqSimp_ltRight
working on 3687
polySimp_mulComm0
working on 3688
polySimp_addComm0
working on 3689
inEqSimp_ltToLeq
working on 3690
polySimp_mulComm0
working on 3691
inEqSimp_ltToLeq
working on 3692
polySimp_mulComm0
working on 3693
polySimp_addComm1
working on 3694
inEqSimp_ltToLeq
working on 3695
polySimp_mulComm0
working on 3696
polySimp_addComm1
working on 3697
inEqSimp_ltToLeq
working on 3698
polySimp_mulComm0
working on 3699
inEqSimp_ltToLeq
working on 3700
polySimp_mulComm0
working on 3701
inEqSimp_ltToLeq
working on 3702
polySimp_mulComm0
working on 3703
inEqSimp_ltToLeq
working on 3704
add_zero_right
working on 3705
polySimp_mulComm0
working on 3706
inEqSimp_ltToLeq
working on 3707
polySimp_mulComm0
working on 3708
polySimp_addComm1
working on 3709
inEqSimp_ltToLeq
working on 3710
polySimp_mulComm0
working on 3711
inEqSimp_ltToLeq
working on 3712
polySimp_mulComm0
working on 3713
inEqSimp_homoInEq0
working on 3714
mul_literals
working on 3715
add_zero_right
working on 3716
inEqSimp_sepNegMonomial1
working on 3717
polySimp_mulLiterals
working on 3718
polySimp_elimOne
working on 3719
inEqSimp_sepPosMonomial0
working on 3720
polySimp_mulComm0
working on 3721
polySimp_rightDist
working on 3722
mul_literals
working on 3723
polySimp_mulLiterals
working on 3724
polySimp_elimOne
working on 3725
inEqSimp_sepNegMonomial0
working on 3726
polySimp_mulLiterals
working on 3727
polySimp_elimOne
working on 3728
inEqSimp_sepNegMonomial0
working on 3729
polySimp_mulLiterals
working on 3730
polySimp_elimOne
working on 3731
inEqSimp_sepPosMonomial0
working on 3732
polySimp_mulComm0
working on 3733
polySimp_rightDist
working on 3734
mul_literals
working on 3735
polySimp_mulLiterals
working on 3736
polySimp_elimOne
working on 3737
inEqSimp_sepPosMonomial0
working on 3738
polySimp_mulComm0
working on 3739
polySimp_rightDist
working on 3740
mul_literals
working on 3741
polySimp_mulLiterals
working on 3742
polySimp_elimOne
working on 3743
inEqSimp_sepPosMonomial0
working on 3744
polySimp_mulComm0
working on 3745
polySimp_rightDist
working on 3746
mul_literals
working on 3747
polySimp_mulLiterals
working on 3748
polySimp_elimOne
working on 3749
inEqSimp_sepNegMonomial0
working on 3750
polySimp_mulLiterals
working on 3751
polySimp_elimOne
working on 3752
inEqSimp_sepNegMonomial0
working on 3753
polySimp_mulLiterals
working on 3754
polySimp_elimOne
working on 3755
inEqSimp_sepPosMonomial0
working on 3756
polySimp_mulComm0
working on 3757
polySimp_rightDist
working on 3758
polySimp_mulLiterals
working on 3759
mul_literals
working on 3760
polySimp_elimOne
working on 3761
inEqSimp_sepPosMonomial0
working on 3762
polySimp_mulComm0
working on 3763
polySimp_rightDist
working on 3764
mul_literals
working on 3765
polySimp_mulLiterals
working on 3766
polySimp_elimOne
working on 3767
inEqSimp_sepNegMonomial1
working on 3768
polySimp_mulLiterals
working on 3769
polySimp_elimOne
working on 3770
inEqSimp_antiSymm
working on 3771
applyEq
working on 3772
inEqSimp_homoInEq1
working on 3773
polySimp_addComm1
working on 3774
applyEq
working on 3775
inEqSimp_homoInEq0
working on 3776
polySimp_pullOutFactor1
working on 3777
add_literals
working on 3778
times_zero
working on 3779
qeq_literals
working on 3780
true_left
working on 3781
applyEq
working on 3782
replace_known_left
working on 3783
One Step Simplification
working on 3784
applyEq
working on 3785
eqSymm
working on 3786
applyEq
working on 3787
eqSymm
working on 3788
applyEq
working on 3789
inEqSimp_homoInEq1
working on 3790
polySimp_pullOutFactor1
working on 3791
add_literals
working on 3792
times_zero
working on 3793
leq_literals
working on 3794
true_left
working on 3795
applyEq
working on 3796
inEqSimp_commuteLeq
working on 3797
applyEq
working on 3798
eqSymm
working on 3799
applyEq
working on 3800
inEqSimp_sepPosMonomial0
working on 3801
polySimp_mulComm0
working on 3802
polySimp_rightDist
working on 3803
mul_literals
working on 3804
polySimp_mulLiterals
working on 3805
polySimp_elimOne
working on 3806
inEqSimp_subsumption1
working on 3807
leq_literals
working on 3808
One Step Simplification
working on 3809
true_left
working on 3810
inEqSimp_or_weaken0
working on 3811
polySimp_addAssoc
working on 3812
add_literals
working on 3813
add_zero_left
working on 3814
One Step Simplification
working on 3815
nnf_imp2or
working on 3816
nnf_imp2or
working on 3817
nnf_imp2or
working on 3818
nnf_notAnd
working on 3819
inEqSimp_notGeq
working on 3820
polySimp_rightDist
working on 3821
mul_literals
working on 3822
polySimp_addAssoc
working on 3823
add_literals
working on 3824
add_zero_left
working on 3825
inEqSimp_sepPosMonomial0
working on 3826
polySimp_mulLiterals
working on 3827
polySimp_elimOne
working on 3828
inEqSimp_notLeq
working on 3829
polySimp_rightDist
working on 3830
mul_literals
working on 3831
polySimp_addAssoc
working on 3832
add_literals
working on 3833
add_zero_left
working on 3834
inEqSimp_sepPosMonomial1
working on 3835
polySimp_mulLiterals
working on 3836
polySimp_elimOne
working on 3837
nnf_notAnd
working on 3838
inEqSimp_notGeq
working on 3839
times_zero
working on 3840
add_literals
working on 3841
inEqSimp_sepPosMonomial0
working on 3842
mul_literals
working on 3843
nnf_notAnd
working on 3844
inEqSimp_notLeq
working on 3845
polySimp_rightDist
working on 3846
mul_literals
working on 3847
polySimp_addAssoc
working on 3848
add_literals
working on 3849
add_zero_left
working on 3850
inEqSimp_sepPosMonomial1
working on 3851
polySimp_mulLiterals
working on 3852
polySimp_elimOne
working on 3853
inEqSimp_notGeq
working on 3854
times_zero
working on 3855
add_literals
working on 3856
inEqSimp_sepPosMonomial0
working on 3857
mul_literals
working on 3858
nnf_notAnd
working on 3859
inEqSimp_notLeq
working on 3860
polySimp_rightDist
working on 3861
mul_literals
working on 3862
polySimp_addAssoc
working on 3863
add_literals
working on 3864
add_zero_left
working on 3865
inEqSimp_sepPosMonomial1
working on 3866
polySimp_mulLiterals
working on 3867
polySimp_elimOne
working on 3868
inEqSimp_notLeq
working on 3869
polySimp_rightDist
working on 3870
mul_literals
working on 3871
polySimp_addAssoc
working on 3872
add_literals
working on 3873
add_zero_left
working on 3874
inEqSimp_sepPosMonomial1
working on 3875
polySimp_mulLiterals
working on 3876
polySimp_elimOne
working on 3877
commute_and
working on 3878
commute_or
working on 3879
commute_or_2
working on 3880
commute_or
working on 3881
equiv_right
working on 3882
allRight
working on 3884
cutUpperBound
working on 3885
crossInst
working on 3887
orRight
working on 3888
andLeft
working on 3889
orRight
working on 3890
eqSymm
working on 3891
replace_known_left
working on 3892
One Step Simplification
working on 3893
true_left
working on 3894
replace_known_left
working on 3895
One Step Simplification
working on 3896
inEqSimp_leqRight
working on 3897
mul_literals
working on 3898
add_literals
working on 3899
add_zero_left
working on 3900
inEqSimp_geqRight
working on 3901
polySimp_mulComm0
working on 3902
polySimp_addComm1
working on 3903
inEqSimp_commuteGeq
working on 3904
applyEq
working on 3905
applyEq
working on 3906
applyEq
working on 3907
applyEq
working on 3908
applyEq
working on 3909
applyEq
working on 3910
applyEq
working on 3911
applyEq
working on 3912
eqSymm
working on 3913
applyEq
working on 3914
applyEq
working on 3915
polySimp_pullOutFactor1b
working on 3916
add_literals
working on 3917
times_zero
working on 3918
add_zero_right
working on 3919
leq_literals
working on 3920
closeFalse
working on 3921
working on 3886
crossInst
working on 3922
orRight
working on 3923
notLeft
working on 3924
andLeft
working on 3925
orRight
working on 3926
eqSymm
working on 3927
replace_known_left
working on 3928
One Step Simplification
working on 3929
true_left
working on 3930
replace_known_left
working on 3931
One Step Simplification
working on 3932
inEqSimp_leqRight
working on 3933
mul_literals
working on 3934
add_literals
working on 3935
add_zero_left
working on 3936
inEqSimp_geqRight
working on 3937
polySimp_mulComm0
working on 3938
polySimp_addComm1
working on 3939
inEqSimp_commuteGeq
working on 3940
applyEq
working on 3941
eqSymm
working on 3942
applyEq
working on 3943
applyEq
working on 3944
applyEq
working on 3945
applyEq
working on 3946
eqSymm
working on 3947
replace_known_right
working on 3948
One Step Simplification
working on 3949
inEqSimp_sepNegMonomial0
working on 3950
polySimp_mulLiterals
working on 3951
polySimp_elimOne
working on 3952
inEqSimp_contradEq7
working on 3953
polySimp_mulComm0
working on 3954
polySimp_pullOutFactor1b
working on 3955
add_literals
working on 3956
times_zero
working on 3957
add_zero_right
working on 3958
leq_literals
working on 3959
One Step Simplification
working on 3960
false_right
working on 3961
inEqSimp_contradInEq1
working on 3962
qeq_literals
working on 3963
One Step Simplification
working on 3964
inEqSimp_contradInEq1
working on 3965
inEqSimp_homoInEq1
working on 3966
polySimp_pullOutFactor1b
working on 3967
add_literals
working on 3968
times_zero
working on 3969
add_zero_right
working on 3970
leq_literals
working on 3971
One Step Simplification
working on 3972
inEqSimp_exactShadow3
working on 3973
times_zero
working on 3974
add_zero_left
working on 3975
inEqSimp_subsumption1
working on 3976
leq_literals
working on 3977
One Step Simplification
working on 3978
true_left
working on 3979
inEqSimp_exactShadow3
working on 3980
polySimp_rightDist
working on 3981
mul_literals
working on 3982
polySimp_addComm1
working on 3983
inEqSimp_sepNegMonomial1
working on 3984
polySimp_mulLiterals
working on 3985
polySimp_elimOne
working on 3986
inEqSimp_contradInEq0
working on 3987
andLeft
working on 3988
inEqSimp_homoInEq1
working on 3989
polySimp_mulComm0
working on 3990
polySimp_rightDist
working on 3991
mul_literals
working on 3992
polySimp_addAssoc
working on 3993
polySimp_addComm0
working on 3994
polySimp_pullOutFactor1b
working on 3995
add_literals
working on 3996
times_zero
working on 3997
add_zero_right
working on 3998
leq_literals
working on 3999
closeFalse
working on 4000
working on 3883
replace_known_right
working on 4001
One Step Simplification
working on 4002
replace_known_left
working on 4003
One Step Simplification
working on 4004
replace_known_left
working on 4005
One Step Simplification
working on 4006
true_left
working on 4007
replace_known_right
working on 4008
One Step Simplification
working on 4009
notLeft
working on 4010
inEqSimp_geqRight
working on 4011
times_zero
working on 4012
add_zero_right
working on 4013
applyEq
working on 4014
equal_literals
working on 4015
false_right
working on 4016
applyEq
working on 4017
applyEq
working on 4018
inEqSimp_commuteLeq
working on 4019
applyEq
working on 4020
applyEq
working on 4021
times_zero
working on 4022
add_zero_right
working on 4023
applyEq
working on 4024
applyEq
working on 4025
One Step Simplification
working on 4026
true_left
working on 4027
applyEq
working on 4028
inEqSimp_homoInEq0
working on 4029
polySimp_pullOutFactor1
working on 4030
add_literals
working on 4031
times_zero
working on 4032
qeq_literals
working on 4033
true_left
working on 4034
inEqSimp_sepPosMonomial0
working on 4035
mul_literals
working on 4036
inEqSimp_contradInEq0
working on 4037
qeq_literals
working on 4038
One Step Simplification
working on 4039
closeFalse
working on 4040
working on 3553
impRight
working on 4041
orRight
working on 4042
One Step Simplification
working on 4043
closeFalse
working on 4044
working on 3537
One Step Simplification
working on 4045
closeFalse
working on 4046
working on 33
One Step Simplification
working on 4047
closeFalse
working on 4048