%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : KLE170+1.006 : TPTP v8.1.0. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n025.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Sun Jul 17 01:37:39 EDT 2022
% Result : Theorem 64.00s 64.40s
% Output : Refutation 64.00s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : KLE170+1.006 : TPTP v8.1.0. Released v5.2.0.
% 0.04/0.13 % Command : bliksem %s
% 0.13/0.34 % Computer : n025.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % DateTime : Thu Jun 16 11:38:56 EDT 2022
% 0.13/0.34 % CPUTime :
% 20.03/20.48 *** allocated 10000 integers for termspace/termends
% 20.03/20.48 *** allocated 10000 integers for clauses
% 20.03/20.48 *** allocated 10000 integers for justifications
% 20.03/20.48 Bliksem 1.12
% 20.03/20.48
% 20.03/20.48
% 20.03/20.48 Automatic Strategy Selection
% 20.03/20.48
% 20.03/20.48
% 20.03/20.48 Clauses:
% 20.03/20.48
% 20.03/20.48 { addition( X, Y ) = addition( Y, X ) }.
% 20.03/20.48 { addition( Z, addition( Y, X ) ) = addition( addition( Z, Y ), X ) }.
% 20.03/20.48 { addition( X, zero ) = X }.
% 20.03/20.48 { addition( X, X ) = X }.
% 20.03/20.48 { multiplication( X, multiplication( Y, Z ) ) = multiplication(
% 20.03/20.48 multiplication( X, Y ), Z ) }.
% 20.03/20.48 { multiplication( X, one ) = X }.
% 20.03/20.48 { multiplication( one, X ) = X }.
% 20.03/20.48 { multiplication( X, addition( Y, Z ) ) = addition( multiplication( X, Y )
% 20.03/20.48 , multiplication( X, Z ) ) }.
% 20.03/20.48 { multiplication( addition( X, Y ), Z ) = addition( multiplication( X, Z )
% 20.03/20.48 , multiplication( Y, Z ) ) }.
% 20.03/20.48 { multiplication( X, zero ) = zero }.
% 20.03/20.48 { multiplication( zero, X ) = zero }.
% 20.03/20.48 { ! leq( X, Y ), addition( X, Y ) = Y }.
% 20.03/20.48 { ! addition( X, Y ) = Y, leq( X, Y ) }.
% 20.03/20.48 { leq( addition( one, multiplication( X, star( X ) ) ), star( X ) ) }.
% 20.03/20.48 { leq( addition( one, multiplication( star( X ), X ) ), star( X ) ) }.
% 20.03/20.48 { ! leq( addition( multiplication( X, Y ), Z ), Y ), leq( multiplication(
% 20.03/20.48 star( X ), Z ), Y ) }.
% 20.03/20.48 { ! leq( addition( multiplication( X, Y ), Z ), X ), leq( multiplication( Z
% 20.03/20.48 , star( Y ) ), X ) }.
% 20.03/20.48 { ! leq( multiplication( a, multiplication( a, multiplication( a,
% 20.03/20.48 multiplication( a, multiplication( a, a ) ) ) ) ), star( a ) ) }.
% 20.03/20.48
% 20.03/20.48 percentage equality = 0.590909, percentage horn = 1.000000
% 20.03/20.48 This is a problem with some equality
% 20.03/20.48
% 20.03/20.48
% 20.03/20.48
% 20.03/20.48 Options Used:
% 20.03/20.48
% 20.03/20.48 useres = 1
% 20.03/20.48 useparamod = 1
% 20.03/20.48 useeqrefl = 1
% 20.03/20.48 useeqfact = 1
% 20.03/20.48 usefactor = 1
% 20.03/20.48 usesimpsplitting = 0
% 20.03/20.48 usesimpdemod = 5
% 20.03/20.48 usesimpres = 3
% 20.03/20.48
% 20.03/20.48 resimpinuse = 1000
% 20.03/20.48 resimpclauses = 20000
% 20.03/20.48 substype = eqrewr
% 20.03/20.48 backwardsubs = 1
% 20.03/20.48 selectoldest = 5
% 20.03/20.48
% 20.03/20.48 litorderings [0] = split
% 20.03/20.48 litorderings [1] = extend the termordering, first sorting on arguments
% 20.03/20.48
% 20.03/20.48 termordering = kbo
% 20.03/20.48
% 20.03/20.48 litapriori = 0
% 20.03/20.48 termapriori = 1
% 20.03/20.48 litaposteriori = 0
% 20.03/20.48 termaposteriori = 0
% 20.03/20.48 demodaposteriori = 0
% 20.03/20.48 ordereqreflfact = 0
% 20.03/20.48
% 20.03/20.48 litselect = negord
% 20.03/20.48
% 20.03/20.48 maxweight = 15
% 20.03/20.48 maxdepth = 30000
% 20.03/20.48 maxlength = 115
% 20.03/20.48 maxnrvars = 195
% 20.03/20.48 excuselevel = 1
% 20.03/20.48 increasemaxweight = 1
% 20.03/20.48
% 20.03/20.48 maxselected = 10000000
% 20.03/20.48 maxnrclauses = 10000000
% 20.03/20.48
% 20.03/20.48 showgenerated = 0
% 20.03/20.48 showkept = 0
% 20.03/20.48 showselected = 0
% 20.03/20.48 showdeleted = 0
% 20.03/20.48 showresimp = 1
% 20.03/20.48 showstatus = 2000
% 20.03/20.48
% 20.03/20.48 prologoutput = 0
% 20.03/20.48 nrgoals = 5000000
% 20.03/20.48 totalproof = 1
% 20.03/20.48
% 20.03/20.48 Symbols occurring in the translation:
% 20.03/20.48
% 20.03/20.48 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 20.03/20.48 . [1, 2] (w:1, o:18, a:1, s:1, b:0),
% 20.03/20.48 ! [4, 1] (w:0, o:12, a:1, s:1, b:0),
% 20.03/20.48 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 20.03/20.48 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 20.03/20.48 addition [37, 2] (w:1, o:42, a:1, s:1, b:0),
% 20.03/20.48 zero [39, 0] (w:1, o:9, a:1, s:1, b:0),
% 20.03/20.48 multiplication [40, 2] (w:1, o:44, a:1, s:1, b:0),
% 20.03/20.48 one [41, 0] (w:1, o:10, a:1, s:1, b:0),
% 20.03/20.48 leq [42, 2] (w:1, o:43, a:1, s:1, b:0),
% 20.03/20.48 star [43, 1] (w:1, o:17, a:1, s:1, b:0),
% 20.03/20.48 a [44, 0] (w:1, o:11, a:1, s:1, b:0).
% 20.03/20.48
% 20.03/20.48
% 20.03/20.48 Starting Search:
% 20.03/20.48
% 20.03/20.48 *** allocated 15000 integers for clauses
% 20.03/20.48 *** allocated 22500 integers for clauses
% 20.03/20.48 *** allocated 33750 integers for clauses
% 20.03/20.48 *** allocated 50625 integers for clauses
% 20.03/20.48 *** allocated 15000 integers for termspace/termends
% 20.03/20.48 *** allocated 75937 integers for clauses
% 20.03/20.48 Resimplifying inuse:
% 20.03/20.48 Done
% 20.03/20.48
% 20.03/20.48 *** allocated 22500 integers for termspace/termends
% 20.03/20.48 *** allocated 113905 integers for clauses
% 20.03/20.48 *** allocated 33750 integers for termspace/termends
% 20.03/20.48
% 20.03/20.48 Intermediate Status:
% 20.03/20.48 Generated: 21503
% 20.03/20.48 Kept: 2007
% 20.03/20.48 Inuse: 224
% 20.03/20.48 Deleted: 56
% 20.03/20.48 Deletedinuse: 34
% 20.03/20.48
% 20.03/20.48 Resimplifying inuse:
% 20.03/20.48 Done
% 20.03/20.48
% 20.03/20.48 *** allocated 170857 integers for clauses
% 20.03/20.48 *** allocated 50625 integers for termspace/termends
% 20.03/20.48 Resimplifying inuse:
% 20.03/20.48 Done
% 20.03/20.48
% 20.03/20.48 *** allocated 256285 integers for clauses
% 20.03/20.48 *** allocated 75937 integers for termspace/termends
% 20.03/20.48
% 20.03/20.48 Intermediate Status:
% 20.03/20.48 Generated: 41876
% 20.03/20.48 Kept: 4156
% 20.03/20.48 Inuse: 335
% 20.03/20.48 Deleted: 85
% 20.03/20.48 Deletedinuse: 36
% 20.03/20.48
% 20.03/20.48 Resimplifying inuse:
% 20.03/20.48 Done
% 20.03/20.48
% 20.03/20.48 Resimplifying inuse:
% 20.03/20.48 Done
% 20.03/20.48
% 20.03/20.48 *** allocated 384427 integers for clauses
% 64.00/64.40 *** allocated 113905 integers for termspace/termends
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 70625
% 64.00/64.40 Kept: 6174
% 64.00/64.40 Inuse: 385
% 64.00/64.40 Deleted: 94
% 64.00/64.40 Deletedinuse: 36
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 *** allocated 170857 integers for termspace/termends
% 64.00/64.40 *** allocated 576640 integers for clauses
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 90885
% 64.00/64.40 Kept: 8181
% 64.00/64.40 Inuse: 454
% 64.00/64.40 Deleted: 118
% 64.00/64.40 Deletedinuse: 36
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 116121
% 64.00/64.40 Kept: 10188
% 64.00/64.40 Inuse: 542
% 64.00/64.40 Deleted: 137
% 64.00/64.40 Deletedinuse: 42
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 *** allocated 864960 integers for clauses
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 138774
% 64.00/64.40 Kept: 12192
% 64.00/64.40 Inuse: 609
% 64.00/64.40 Deleted: 169
% 64.00/64.40 Deletedinuse: 56
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 *** allocated 256285 integers for termspace/termends
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 170895
% 64.00/64.40 Kept: 14196
% 64.00/64.40 Inuse: 724
% 64.00/64.40 Deleted: 180
% 64.00/64.40 Deletedinuse: 56
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 198512
% 64.00/64.40 Kept: 16259
% 64.00/64.40 Inuse: 787
% 64.00/64.40 Deleted: 189
% 64.00/64.40 Deletedinuse: 56
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 *** allocated 1297440 integers for clauses
% 64.00/64.40 *** allocated 384427 integers for termspace/termends
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 225076
% 64.00/64.40 Kept: 18351
% 64.00/64.40 Inuse: 844
% 64.00/64.40 Deleted: 203
% 64.00/64.40 Deletedinuse: 57
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying clauses:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 240971
% 64.00/64.40 Kept: 20408
% 64.00/64.40 Inuse: 872
% 64.00/64.40 Deleted: 2158
% 64.00/64.40 Deletedinuse: 57
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 258463
% 64.00/64.40 Kept: 22416
% 64.00/64.40 Inuse: 909
% 64.00/64.40 Deleted: 2160
% 64.00/64.40 Deletedinuse: 59
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 285403
% 64.00/64.40 Kept: 24473
% 64.00/64.40 Inuse: 936
% 64.00/64.40 Deleted: 2160
% 64.00/64.40 Deletedinuse: 59
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 316799
% 64.00/64.40 Kept: 26493
% 64.00/64.40 Inuse: 998
% 64.00/64.40 Deleted: 2160
% 64.00/64.40 Deletedinuse: 59
% 64.00/64.40
% 64.00/64.40 *** allocated 576640 integers for termspace/termends
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 *** allocated 1946160 integers for clauses
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 333465
% 64.00/64.40 Kept: 28495
% 64.00/64.40 Inuse: 1026
% 64.00/64.40 Deleted: 2160
% 64.00/64.40 Deletedinuse: 59
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 356632
% 64.00/64.40 Kept: 30503
% 64.00/64.40 Inuse: 1060
% 64.00/64.40 Deleted: 2160
% 64.00/64.40 Deletedinuse: 59
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 384998
% 64.00/64.40 Kept: 32536
% 64.00/64.40 Inuse: 1118
% 64.00/64.40 Deleted: 2160
% 64.00/64.40 Deletedinuse: 59
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 415257
% 64.00/64.40 Kept: 34547
% 64.00/64.40 Inuse: 1181
% 64.00/64.40 Deleted: 2164
% 64.00/64.40 Deletedinuse: 63
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 496779
% 64.00/64.40 Kept: 36606
% 64.00/64.40 Inuse: 1261
% 64.00/64.40 Deleted: 2166
% 64.00/64.40 Deletedinuse: 63
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 544693
% 64.00/64.40 Kept: 38631
% 64.00/64.40 Inuse: 1341
% 64.00/64.40 Deleted: 2169
% 64.00/64.40 Deletedinuse: 64
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 *** allocated 864960 integers for termspace/termends
% 64.00/64.40 Resimplifying clauses:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 *** allocated 2919240 integers for clauses
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 585689
% 64.00/64.40 Kept: 40737
% 64.00/64.40 Inuse: 1413
% 64.00/64.40 Deleted: 4132
% 64.00/64.40 Deletedinuse: 64
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 613492
% 64.00/64.40 Kept: 42828
% 64.00/64.40 Inuse: 1427
% 64.00/64.40 Deleted: 4132
% 64.00/64.40 Deletedinuse: 64
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 648393
% 64.00/64.40 Kept: 44845
% 64.00/64.40 Inuse: 1484
% 64.00/64.40 Deleted: 4132
% 64.00/64.40 Deletedinuse: 64
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 668899
% 64.00/64.40 Kept: 46846
% 64.00/64.40 Inuse: 1507
% 64.00/64.40 Deleted: 4134
% 64.00/64.40 Deletedinuse: 66
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 689999
% 64.00/64.40 Kept: 48892
% 64.00/64.40 Inuse: 1525
% 64.00/64.40 Deleted: 4135
% 64.00/64.40 Deletedinuse: 67
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 745416
% 64.00/64.40 Kept: 51018
% 64.00/64.40 Inuse: 1579
% 64.00/64.40 Deleted: 4135
% 64.00/64.40 Deletedinuse: 67
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 777400
% 64.00/64.40 Kept: 53396
% 64.00/64.40 Inuse: 1617
% 64.00/64.40 Deleted: 4138
% 64.00/64.40 Deletedinuse: 68
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 795901
% 64.00/64.40 Kept: 55400
% 64.00/64.40 Inuse: 1642
% 64.00/64.40 Deleted: 4139
% 64.00/64.40 Deletedinuse: 68
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 825118
% 64.00/64.40 Kept: 57412
% 64.00/64.40 Inuse: 1683
% 64.00/64.40 Deleted: 4139
% 64.00/64.40 Deletedinuse: 68
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 *** allocated 1297440 integers for termspace/termends
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 863624
% 64.00/64.40 Kept: 59416
% 64.00/64.40 Inuse: 1739
% 64.00/64.40 Deleted: 4140
% 64.00/64.40 Deletedinuse: 68
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying clauses:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 898601
% 64.00/64.40 Kept: 61692
% 64.00/64.40 Inuse: 1808
% 64.00/64.40 Deleted: 6020
% 64.00/64.40 Deletedinuse: 69
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 *** allocated 4378860 integers for clauses
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 915820
% 64.00/64.40 Kept: 63717
% 64.00/64.40 Inuse: 1821
% 64.00/64.40 Deleted: 6020
% 64.00/64.40 Deletedinuse: 69
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 932061
% 64.00/64.40 Kept: 65937
% 64.00/64.40 Inuse: 1836
% 64.00/64.40 Deleted: 6020
% 64.00/64.40 Deletedinuse: 69
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 942453
% 64.00/64.40 Kept: 67955
% 64.00/64.40 Inuse: 1846
% 64.00/64.40 Deleted: 6020
% 64.00/64.40 Deletedinuse: 69
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 981840
% 64.00/64.40 Kept: 70062
% 64.00/64.40 Inuse: 1859
% 64.00/64.40 Deleted: 6020
% 64.00/64.40 Deletedinuse: 69
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 1030525
% 64.00/64.40 Kept: 72172
% 64.00/64.40 Inuse: 1879
% 64.00/64.40 Deleted: 6020
% 64.00/64.40 Deletedinuse: 69
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 1086674
% 64.00/64.40 Kept: 74238
% 64.00/64.40 Inuse: 1907
% 64.00/64.40 Deleted: 6022
% 64.00/64.40 Deletedinuse: 69
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 1107124
% 64.00/64.40 Kept: 76257
% 64.00/64.40 Inuse: 1939
% 64.00/64.40 Deleted: 6023
% 64.00/64.40 Deletedinuse: 70
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 1141616
% 64.00/64.40 Kept: 78282
% 64.00/64.40 Inuse: 1976
% 64.00/64.40 Deleted: 6027
% 64.00/64.40 Deletedinuse: 72
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying clauses:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 1165450
% 64.00/64.40 Kept: 80284
% 64.00/64.40 Inuse: 2000
% 64.00/64.40 Deleted: 7506
% 64.00/64.40 Deletedinuse: 72
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 1186757
% 64.00/64.40 Kept: 82289
% 64.00/64.40 Inuse: 2025
% 64.00/64.40 Deleted: 7506
% 64.00/64.40 Deletedinuse: 72
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 1216046
% 64.00/64.40 Kept: 84347
% 64.00/64.40 Inuse: 2056
% 64.00/64.40 Deleted: 7506
% 64.00/64.40 Deletedinuse: 72
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40
% 64.00/64.40 Intermediate Status:
% 64.00/64.40 Generated: 1251755
% 64.00/64.40 Kept: 86371
% 64.00/64.40 Inuse: 2097
% 64.00/64.40 Deleted: 7506
% 64.00/64.40 Deletedinuse: 72
% 64.00/64.40
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40 Done
% 64.00/64.40
% 64.00/64.40 *** allocated 1946160 integers for termspace/termends
% 64.00/64.40 Resimplifying inuse:
% 64.00/64.40
% 64.00/64.40 Bliksems!, er is een bewijs:
% 64.00/64.40 % SZS status Theorem
% 64.00/64.40 % SZS output start Refutation
% 64.00/64.40
% 64.00/64.40 (0) {G0,W7,D3,L1,V2,M1} I { addition( X, Y ) = addition( Y, X ) }.
% 64.00/64.40 (1) {G0,W11,D4,L1,V3,M1} I { addition( Z, addition( Y, X ) ) ==> addition(
% 64.00/64.40 addition( Z, Y ), X ) }.
% 64.00/64.40 (3) {G0,W5,D3,L1,V1,M1} I { addition( X, X ) ==> X }.
% 64.00/64.40 (4) {G0,W11,D4,L1,V3,M1} I { multiplication( X, multiplication( Y, Z ) )
% 64.00/64.40 ==> multiplication( multiplication( X, Y ), Z ) }.
% 64.00/64.40 (5) {G0,W5,D3,L1,V1,M1} I { multiplication( X, one ) ==> X }.
% 64.00/64.40 (6) {G0,W5,D3,L1,V1,M1} I { multiplication( one, X ) ==> X }.
% 64.00/64.40 (7) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Y ),
% 64.00/64.40 multiplication( X, Z ) ) ==> multiplication( X, addition( Y, Z ) ) }.
% 64.00/64.40 (8) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Z ),
% 64.00/64.40 multiplication( Y, Z ) ) ==> multiplication( addition( X, Y ), Z ) }.
% 64.00/64.40 (11) {G0,W8,D3,L2,V2,M2} I { ! leq( X, Y ), addition( X, Y ) ==> Y }.
% 64.00/64.40 (12) {G0,W8,D3,L2,V2,M2} I { ! addition( X, Y ) ==> Y, leq( X, Y ) }.
% 64.00/64.40 (13) {G0,W9,D5,L1,V1,M1} I { leq( addition( one, multiplication( X, star( X
% 64.00/64.40 ) ) ), star( X ) ) }.
% 64.00/64.40 (14) {G0,W9,D5,L1,V1,M1} I { leq( addition( one, multiplication( star( X )
% 64.00/64.40 , X ) ), star( X ) ) }.
% 64.00/64.40 (15) {G0,W13,D4,L2,V3,M2} I { ! leq( addition( multiplication( X, Y ), Z )
% 64.00/64.40 , Y ), leq( multiplication( star( X ), Z ), Y ) }.
% 64.00/64.40 (17) {G1,W14,D7,L1,V0,M1} I;d(4);d(4);d(4);d(4) { ! leq( multiplication(
% 64.00/64.40 multiplication( multiplication( multiplication( multiplication( a, a ), a
% 64.00/64.40 ), a ), a ), a ), star( a ) ) }.
% 64.00/64.40 (20) {G1,W3,D2,L1,V1,M1} R(12,3) { leq( X, X ) }.
% 64.00/64.40 (22) {G1,W8,D3,L2,V2,M2} P(0,12) { ! addition( Y, X ) ==> Y, leq( X, Y )
% 64.00/64.41 }.
% 64.00/64.41 (23) {G1,W14,D4,L2,V3,M2} P(1,12) { ! addition( addition( X, Y ), Z ) ==>
% 64.00/64.41 addition( Y, Z ), leq( X, addition( Y, Z ) ) }.
% 64.00/64.41 (24) {G1,W11,D4,L1,V3,M1} P(1,0) { addition( addition( X, Y ), Z ) =
% 64.00/64.41 addition( addition( Y, Z ), X ) }.
% 64.00/64.41 (29) {G2,W10,D3,L2,V2,M2} R(11,22) { addition( X, Y ) ==> Y, ! addition( Y
% 64.00/64.41 , X ) ==> Y }.
% 64.00/64.41 (32) {G1,W14,D4,L2,V3,M2} P(11,1) { addition( addition( X, Y ), Z ) ==>
% 64.00/64.41 addition( Y, Z ), ! leq( X, addition( Y, Z ) ) }.
% 64.00/64.41 (33) {G1,W12,D4,L2,V3,M2} P(11,1) { addition( addition( Z, X ), Y ) ==>
% 64.00/64.41 addition( Z, Y ), ! leq( X, Y ) }.
% 64.00/64.41 (35) {G1,W8,D3,L2,V2,M2} P(11,0) { addition( Y, X ) ==> Y, ! leq( X, Y )
% 64.00/64.41 }.
% 64.00/64.41 (63) {G1,W16,D4,L2,V3,M2} P(7,12) { ! multiplication( X, addition( Y, Z ) )
% 64.00/64.41 ==> multiplication( X, Z ), leq( multiplication( X, Y ), multiplication
% 64.00/64.41 ( X, Z ) ) }.
% 64.00/64.41 (64) {G1,W11,D4,L1,V3,M1} P(7,0);d(7) { multiplication( X, addition( Y, Z )
% 64.00/64.41 ) = multiplication( X, addition( Z, Y ) ) }.
% 64.00/64.41 (65) {G1,W11,D4,L1,V2,M1} P(5,7) { addition( X, multiplication( X, Y ) ) =
% 64.00/64.41 multiplication( X, addition( one, Y ) ) }.
% 64.00/64.41 (94) {G1,W16,D4,L2,V3,M2} P(8,12) { ! multiplication( addition( X, Z ), Y )
% 64.00/64.41 ==> multiplication( Z, Y ), leq( multiplication( X, Y ), multiplication
% 64.00/64.41 ( Z, Y ) ) }.
% 64.00/64.41 (162) {G1,W14,D4,L3,V3,M3} P(11,15) { ! leq( Z, Y ), leq( multiplication(
% 64.00/64.41 star( X ), Z ), Y ), ! leq( multiplication( X, Y ), Z ) }.
% 64.00/64.41 (167) {G1,W11,D4,L2,V2,M2} P(5,15) { ! leq( addition( multiplication( X, Y
% 64.00/64.41 ), one ), Y ), leq( star( X ), Y ) }.
% 64.00/64.41 (228) {G2,W8,D3,L2,V3,M2} P(11,23);q { leq( X, addition( Y, Z ) ), ! leq( X
% 64.00/64.41 , Y ) }.
% 64.00/64.41 (232) {G2,W5,D3,L1,V2,M1} P(3,23);q { leq( X, addition( X, Y ) ) }.
% 64.00/64.41 (239) {G3,W7,D4,L1,V3,M1} P(1,232) { leq( X, addition( addition( X, Y ), Z
% 64.00/64.41 ) ) }.
% 64.00/64.41 (240) {G3,W5,D3,L1,V2,M1} P(0,232) { leq( X, addition( Y, X ) ) }.
% 64.00/64.41 (241) {G4,W9,D4,L1,V2,M1} R(240,11);d(1) { addition( addition( X, Y ), X )
% 64.00/64.41 ==> addition( Y, X ) }.
% 64.00/64.41 (242) {G4,W9,D4,L1,V3,M1} P(8,240) { leq( multiplication( Z, Y ),
% 64.00/64.41 multiplication( addition( X, Z ), Y ) ) }.
% 64.00/64.41 (244) {G4,W9,D4,L1,V3,M1} P(7,240) { leq( multiplication( X, Z ),
% 64.00/64.41 multiplication( X, addition( Y, Z ) ) ) }.
% 64.00/64.41 (251) {G4,W7,D4,L1,V3,M1} P(24,240) { leq( Z, addition( addition( Y, Z ), X
% 64.00/64.41 ) ) }.
% 64.00/64.41 (479) {G2,W9,D2,L3,V2,M3} P(35,11) { ! leq( X, Y ), X = Y, ! leq( Y, X )
% 64.00/64.41 }.
% 64.00/64.41 (503) {G5,W8,D3,L2,V3,M2} P(33,251) { leq( Y, addition( X, Z ) ), ! leq( Y
% 64.00/64.41 , Z ) }.
% 64.00/64.41 (513) {G5,W8,D3,L2,V3,M2} P(11,251) { leq( Y, Z ), ! leq( addition( X, Y )
% 64.00/64.41 , Z ) }.
% 64.00/64.41 (526) {G4,W8,D3,L2,V3,M2} P(11,239) { leq( X, Z ), ! leq( addition( X, Y )
% 64.00/64.41 , Z ) }.
% 64.00/64.41 (719) {G5,W4,D3,L1,V1,M1} R(526,14) { leq( one, star( X ) ) }.
% 64.00/64.41 (724) {G5,W15,D3,L3,V4,M3} P(32,526) { leq( addition( X, Y ), T ), ! leq(
% 64.00/64.41 addition( Y, Z ), T ), ! leq( X, addition( Y, Z ) ) }.
% 64.00/64.41 (729) {G5,W12,D4,L2,V4,M2} P(8,526) { leq( multiplication( X, Y ), T ), !
% 64.00/64.41 leq( multiplication( addition( X, Z ), Y ), T ) }.
% 64.00/64.41 (730) {G5,W12,D4,L2,V4,M2} P(7,526) { leq( multiplication( X, Y ), T ), !
% 64.00/64.41 leq( multiplication( X, addition( Y, Z ) ), T ) }.
% 64.00/64.41 (731) {G5,W9,D2,L3,V3,M3} P(11,526) { leq( X, Z ), ! leq( Y, Z ), ! leq( X
% 64.00/64.41 , Y ) }.
% 64.00/64.41 (732) {G6,W7,D3,L1,V2,M1} F(724);d(241);r(20) { leq( addition( Y, X ),
% 64.00/64.41 addition( X, Y ) ) }.
% 64.00/64.41 (733) {G6,W7,D4,L1,V1,M1} R(719,35) { addition( star( X ), one ) ==> star(
% 64.00/64.41 X ) }.
% 64.00/64.41 (736) {G6,W7,D4,L1,V1,M1} R(719,11) { addition( one, star( X ) ) ==> star(
% 64.00/64.41 X ) }.
% 64.00/64.41 (792) {G7,W9,D4,L1,V3,M1} R(503,732);d(1) { leq( addition( X, Y ), addition
% 64.00/64.41 ( addition( Z, Y ), X ) ) }.
% 64.00/64.41 (812) {G6,W12,D4,L2,V4,M2} P(7,503) { leq( T, multiplication( X, addition(
% 64.00/64.41 Y, Z ) ) ), ! leq( T, multiplication( X, Z ) ) }.
% 64.00/64.41 (880) {G6,W7,D4,L1,V1,M1} R(513,14) { leq( multiplication( star( X ), X ),
% 64.00/64.41 star( X ) ) }.
% 64.00/64.41 (881) {G6,W7,D4,L1,V1,M1} R(513,13) { leq( multiplication( X, star( X ) ),
% 64.00/64.41 star( X ) ) }.
% 64.00/64.41 (885) {G6,W12,D4,L2,V4,M2} P(7,513) { leq( multiplication( X, Z ), T ), !
% 64.00/64.41 leq( multiplication( X, addition( Y, Z ) ), T ) }.
% 64.00/64.41 (1592) {G7,W6,D4,L1,V2,M1} P(736,63);q;d(5) { leq( Y, multiplication( Y,
% 64.00/64.41 star( X ) ) ) }.
% 64.00/64.41 (1595) {G2,W10,D3,L2,V3,M2} P(11,63);q { leq( multiplication( Z, X ),
% 64.00/64.41 multiplication( Z, Y ) ), ! leq( X, Y ) }.
% 64.00/64.41 (1751) {G3,W7,D4,L1,V2,M1} P(65,232) { leq( X, multiplication( X, addition
% 64.00/64.41 ( one, Y ) ) ) }.
% 64.00/64.41 (1764) {G4,W7,D4,L1,V2,M1} P(64,1751) { leq( X, multiplication( X, addition
% 64.00/64.41 ( Y, one ) ) ) }.
% 64.00/64.41 (2878) {G7,W6,D4,L1,V2,M1} P(736,94);q;d(6) { leq( Y, multiplication( star
% 64.00/64.41 ( X ), Y ) ) }.
% 64.00/64.41 (2881) {G2,W10,D3,L2,V3,M2} P(11,94);q { leq( multiplication( X, Z ),
% 64.00/64.41 multiplication( Y, Z ) ), ! leq( X, Y ) }.
% 64.00/64.41 (2886) {G8,W8,D5,L1,V3,M1} R(2878,228) { leq( X, addition( multiplication(
% 64.00/64.41 star( Y ), X ), Z ) ) }.
% 64.00/64.41 (3030) {G9,W9,D4,L2,V3,M2} P(11,2886) { leq( Y, Z ), ! leq( multiplication
% 64.00/64.41 ( star( X ), Y ), Z ) }.
% 64.00/64.41 (7357) {G8,W8,D4,L1,V2,M1} P(733,792) { leq( addition( Y, one ), addition(
% 64.00/64.41 star( X ), Y ) ) }.
% 64.00/64.41 (8643) {G10,W4,D3,L1,V1,M1} R(3030,880) { leq( X, star( X ) ) }.
% 64.00/64.41 (8657) {G11,W8,D3,L2,V1,M2} R(8643,479) { star( X ) ==> X, ! leq( star( X )
% 64.00/64.41 , X ) }.
% 64.00/64.41 (8658) {G11,W7,D3,L2,V2,M2} R(8643,731) { leq( X, star( Y ) ), ! leq( X, Y
% 64.00/64.41 ) }.
% 64.00/64.41 (8659) {G11,W7,D3,L2,V2,M2} R(8643,731) { leq( X, Y ), ! leq( star( X ), Y
% 64.00/64.41 ) }.
% 64.00/64.41 (8662) {G11,W7,D4,L1,V1,M1} R(8643,35) { addition( star( X ), X ) ==> star
% 64.00/64.41 ( X ) }.
% 64.00/64.41 (8665) {G11,W7,D4,L1,V1,M1} R(8643,11) { addition( X, star( X ) ) ==> star
% 64.00/64.41 ( X ) }.
% 64.00/64.41 (8809) {G12,W10,D3,L3,V3,M3} R(8658,731) { ! leq( X, Y ), leq( Z, star( Y )
% 64.00/64.41 ), ! leq( Z, X ) }.
% 64.00/64.41 (8911) {G12,W10,D3,L3,V2,M3} R(8659,479) { ! leq( star( X ), Y ), X = Y, !
% 64.00/64.41 leq( Y, X ) }.
% 64.00/64.41 (8974) {G12,W8,D4,L1,V2,M1} P(8662,242) { leq( multiplication( X, Y ),
% 64.00/64.41 multiplication( star( X ), Y ) ) }.
% 64.00/64.41 (8976) {G12,W6,D3,L1,V1,M1} P(8662,7357) { leq( addition( X, one ), star( X
% 64.00/64.41 ) ) }.
% 64.00/64.41 (8982) {G12,W8,D3,L2,V1,M2} P(29,8662);d(8665) { star( X ) ==> X, ! star( X
% 64.00/64.41 ) ==> X }.
% 64.00/64.41 (9463) {G7,W8,D4,L1,V1,M1} R(162,881);r(20) { leq( multiplication( star( X
% 64.00/64.41 ), star( X ) ), star( X ) ) }.
% 64.00/64.41 (10042) {G8,W8,D4,L1,V1,M1} R(9463,479);r(1592) { multiplication( star( X )
% 64.00/64.41 , star( X ) ) ==> star( X ) }.
% 64.00/64.41 (10046) {G9,W6,D4,L1,V1,M1} P(10042,167);d(733);r(20) { leq( star( star( X
% 64.00/64.41 ) ), star( X ) ) }.
% 64.00/64.41 (10049) {G13,W9,D3,L2,V1,M2} P(8982,10042) { multiplication( X, X ) ==> X,
% 64.00/64.41 ! star( X ) ==> X }.
% 64.00/64.41 (10063) {G12,W6,D4,L1,V1,M1} R(10046,8657) { star( star( X ) ) ==> star( X
% 64.00/64.41 ) }.
% 64.00/64.41 (73429) {G13,W10,D4,L1,V3,M1} R(812,8974) { leq( multiplication( X, Y ),
% 64.00/64.41 multiplication( star( X ), addition( Z, Y ) ) ) }.
% 64.00/64.41 (74356) {G14,W9,D4,L1,V2,M1} P(8662,73429) { leq( multiplication( Y, X ),
% 64.00/64.41 multiplication( star( Y ), star( X ) ) ) }.
% 64.00/64.41 (74418) {G15,W6,D3,L1,V1,M1} P(10049,74356);d(10063);q { leq(
% 64.00/64.41 multiplication( X, X ), star( X ) ) }.
% 64.00/64.41 (74437) {G16,W9,D3,L2,V2,M2} R(74418,8809);d(10063) { ! leq( X,
% 64.00/64.41 multiplication( Y, Y ) ), leq( X, star( Y ) ) }.
% 64.00/64.41 (74450) {G16,W10,D4,L1,V2,M1} R(74418,2881) { leq( multiplication(
% 64.00/64.41 multiplication( X, X ), Y ), multiplication( star( X ), Y ) ) }.
% 64.00/64.41 (75176) {G17,W9,D3,L2,V2,M2} R(74437,1595) { leq( multiplication( X, Y ),
% 64.00/64.41 star( X ) ), ! leq( Y, X ) }.
% 64.00/64.41 (75242) {G17,W10,D4,L1,V2,M1} R(74437,244) { leq( multiplication( addition
% 64.00/64.41 ( X, Y ), Y ), star( addition( X, Y ) ) ) }.
% 64.00/64.41 (75482) {G18,W9,D4,L1,V1,M1} R(75176,8976);d(10063) { leq( multiplication(
% 64.00/64.41 star( X ), addition( X, one ) ), star( X ) ) }.
% 64.00/64.41 (76864) {G19,W9,D4,L1,V1,M1} R(75482,8911);d(10063);r(1764) {
% 64.00/64.41 multiplication( star( X ), addition( X, one ) ) ==> star( X ) }.
% 64.00/64.41 (76901) {G20,W9,D4,L1,V1,M1} P(76864,64) { multiplication( star( X ),
% 64.00/64.41 addition( one, X ) ) ==> star( X ) }.
% 64.00/64.41 (79673) {G18,W8,D4,L1,V2,M1} R(75242,729) { leq( multiplication( X, Y ),
% 64.00/64.41 star( addition( X, Y ) ) ) }.
% 64.00/64.41 (79802) {G19,W8,D4,L1,V2,M1} P(0,79673) { leq( multiplication( X, Y ), star
% 64.00/64.41 ( addition( Y, X ) ) ) }.
% 64.00/64.41 (79902) {G20,W10,D4,L1,V2,M1} P(241,79802) { leq( multiplication( X,
% 64.00/64.41 addition( X, Y ) ), star( addition( Y, X ) ) ) }.
% 64.00/64.41 (80414) {G21,W8,D4,L1,V2,M1} R(79902,730) { leq( multiplication( X, X ),
% 64.00/64.41 star( addition( Y, X ) ) ) }.
% 64.00/64.41 (80528) {G22,W9,D3,L2,V2,M2} P(35,80414) { leq( multiplication( Y, Y ),
% 64.00/64.41 star( X ) ), ! leq( Y, X ) }.
% 64.00/64.41 (80849) {G23,W10,D3,L2,V2,M2} P(10063,80528) { leq( multiplication( Y, Y )
% 64.00/64.41 , star( X ) ), ! leq( Y, star( X ) ) }.
% 64.00/64.41 (83443) {G21,W10,D4,L1,V1,M1} P(76901,74450) { leq( multiplication(
% 64.00/64.41 multiplication( X, X ), addition( one, X ) ), star( X ) ) }.
% 64.00/64.41 (86754) {G22,W8,D4,L1,V1,M1} R(83443,885) { leq( multiplication(
% 64.00/64.41 multiplication( X, X ), X ), star( X ) ) }.
% 64.00/64.41 (86799) {G24,W14,D7,L1,V1,M1} R(86754,80849);d(4);d(4) { leq(
% 64.00/64.41 multiplication( multiplication( multiplication( multiplication(
% 64.00/64.41 multiplication( X, X ), X ), X ), X ), X ), star( X ) ) }.
% 64.00/64.41 (87688) {G25,W0,D0,L0,V0,M0} S(17);r(86799) { }.
% 64.00/64.41
% 64.00/64.41
% 64.00/64.41 % SZS output end Refutation
% 64.00/64.41 found a proof!
% 64.00/64.41
% 64.00/64.41
% 64.00/64.41 Unprocessed initial clauses:
% 64.00/64.41
% 64.00/64.41 (87690) {G0,W7,D3,L1,V2,M1} { addition( X, Y ) = addition( Y, X ) }.
% 64.00/64.41 (87691) {G0,W11,D4,L1,V3,M1} { addition( Z, addition( Y, X ) ) = addition
% 64.00/64.41 ( addition( Z, Y ), X ) }.
% 64.00/64.41 (87692) {G0,W5,D3,L1,V1,M1} { addition( X, zero ) = X }.
% 64.00/64.41 (87693) {G0,W5,D3,L1,V1,M1} { addition( X, X ) = X }.
% 64.00/64.41 (87694) {G0,W11,D4,L1,V3,M1} { multiplication( X, multiplication( Y, Z ) )
% 64.00/64.41 = multiplication( multiplication( X, Y ), Z ) }.
% 64.00/64.41 (87695) {G0,W5,D3,L1,V1,M1} { multiplication( X, one ) = X }.
% 64.00/64.41 (87696) {G0,W5,D3,L1,V1,M1} { multiplication( one, X ) = X }.
% 64.00/64.41 (87697) {G0,W13,D4,L1,V3,M1} { multiplication( X, addition( Y, Z ) ) =
% 64.00/64.41 addition( multiplication( X, Y ), multiplication( X, Z ) ) }.
% 64.00/64.41 (87698) {G0,W13,D4,L1,V3,M1} { multiplication( addition( X, Y ), Z ) =
% 64.00/64.41 addition( multiplication( X, Z ), multiplication( Y, Z ) ) }.
% 64.00/64.41 (87699) {G0,W5,D3,L1,V1,M1} { multiplication( X, zero ) = zero }.
% 64.00/64.41 (87700) {G0,W5,D3,L1,V1,M1} { multiplication( zero, X ) = zero }.
% 64.00/64.41 (87701) {G0,W8,D3,L2,V2,M2} { ! leq( X, Y ), addition( X, Y ) = Y }.
% 64.00/64.41 (87702) {G0,W8,D3,L2,V2,M2} { ! addition( X, Y ) = Y, leq( X, Y ) }.
% 64.00/64.41 (87703) {G0,W9,D5,L1,V1,M1} { leq( addition( one, multiplication( X, star
% 64.00/64.41 ( X ) ) ), star( X ) ) }.
% 64.00/64.41 (87704) {G0,W9,D5,L1,V1,M1} { leq( addition( one, multiplication( star( X
% 64.00/64.41 ), X ) ), star( X ) ) }.
% 64.00/64.41 (87705) {G0,W13,D4,L2,V3,M2} { ! leq( addition( multiplication( X, Y ), Z
% 64.00/64.41 ), Y ), leq( multiplication( star( X ), Z ), Y ) }.
% 64.00/64.41 (87706) {G0,W13,D4,L2,V3,M2} { ! leq( addition( multiplication( X, Y ), Z
% 64.00/64.41 ), X ), leq( multiplication( Z, star( Y ) ), X ) }.
% 64.00/64.41 (87707) {G0,W14,D7,L1,V0,M1} { ! leq( multiplication( a, multiplication( a
% 64.00/64.41 , multiplication( a, multiplication( a, multiplication( a, a ) ) ) ) ),
% 64.00/64.41 star( a ) ) }.
% 64.00/64.41
% 64.00/64.41
% 64.00/64.41 Total Proof:
% 64.00/64.41
% 64.00/64.41 subsumption: (0) {G0,W7,D3,L1,V2,M1} I { addition( X, Y ) = addition( Y, X
% 64.00/64.41 ) }.
% 64.00/64.41 parent0: (87690) {G0,W7,D3,L1,V2,M1} { addition( X, Y ) = addition( Y, X )
% 64.00/64.41 }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (1) {G0,W11,D4,L1,V3,M1} I { addition( Z, addition( Y, X ) )
% 64.00/64.41 ==> addition( addition( Z, Y ), X ) }.
% 64.00/64.41 parent0: (87691) {G0,W11,D4,L1,V3,M1} { addition( Z, addition( Y, X ) ) =
% 64.00/64.41 addition( addition( Z, Y ), X ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (3) {G0,W5,D3,L1,V1,M1} I { addition( X, X ) ==> X }.
% 64.00/64.41 parent0: (87693) {G0,W5,D3,L1,V1,M1} { addition( X, X ) = X }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (4) {G0,W11,D4,L1,V3,M1} I { multiplication( X, multiplication
% 64.00/64.41 ( Y, Z ) ) ==> multiplication( multiplication( X, Y ), Z ) }.
% 64.00/64.41 parent0: (87694) {G0,W11,D4,L1,V3,M1} { multiplication( X, multiplication
% 64.00/64.41 ( Y, Z ) ) = multiplication( multiplication( X, Y ), Z ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (5) {G0,W5,D3,L1,V1,M1} I { multiplication( X, one ) ==> X }.
% 64.00/64.41 parent0: (87695) {G0,W5,D3,L1,V1,M1} { multiplication( X, one ) = X }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (6) {G0,W5,D3,L1,V1,M1} I { multiplication( one, X ) ==> X }.
% 64.00/64.41 parent0: (87696) {G0,W5,D3,L1,V1,M1} { multiplication( one, X ) = X }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (87733) {G0,W13,D4,L1,V3,M1} { addition( multiplication( X, Y ),
% 64.00/64.41 multiplication( X, Z ) ) = multiplication( X, addition( Y, Z ) ) }.
% 64.00/64.41 parent0[0]: (87697) {G0,W13,D4,L1,V3,M1} { multiplication( X, addition( Y
% 64.00/64.41 , Z ) ) = addition( multiplication( X, Y ), multiplication( X, Z ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (7) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Y )
% 64.00/64.41 , multiplication( X, Z ) ) ==> multiplication( X, addition( Y, Z ) ) }.
% 64.00/64.41 parent0: (87733) {G0,W13,D4,L1,V3,M1} { addition( multiplication( X, Y ),
% 64.00/64.41 multiplication( X, Z ) ) = multiplication( X, addition( Y, Z ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (87741) {G0,W13,D4,L1,V3,M1} { addition( multiplication( X, Z ),
% 64.00/64.41 multiplication( Y, Z ) ) = multiplication( addition( X, Y ), Z ) }.
% 64.00/64.41 parent0[0]: (87698) {G0,W13,D4,L1,V3,M1} { multiplication( addition( X, Y
% 64.00/64.41 ), Z ) = addition( multiplication( X, Z ), multiplication( Y, Z ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (8) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Z )
% 64.00/64.41 , multiplication( Y, Z ) ) ==> multiplication( addition( X, Y ), Z ) }.
% 64.00/64.41 parent0: (87741) {G0,W13,D4,L1,V3,M1} { addition( multiplication( X, Z ),
% 64.00/64.41 multiplication( Y, Z ) ) = multiplication( addition( X, Y ), Z ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (11) {G0,W8,D3,L2,V2,M2} I { ! leq( X, Y ), addition( X, Y )
% 64.00/64.41 ==> Y }.
% 64.00/64.41 parent0: (87701) {G0,W8,D3,L2,V2,M2} { ! leq( X, Y ), addition( X, Y ) = Y
% 64.00/64.41 }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 1 ==> 1
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (12) {G0,W8,D3,L2,V2,M2} I { ! addition( X, Y ) ==> Y, leq( X
% 64.00/64.41 , Y ) }.
% 64.00/64.41 parent0: (87702) {G0,W8,D3,L2,V2,M2} { ! addition( X, Y ) = Y, leq( X, Y )
% 64.00/64.41 }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 1 ==> 1
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (13) {G0,W9,D5,L1,V1,M1} I { leq( addition( one,
% 64.00/64.41 multiplication( X, star( X ) ) ), star( X ) ) }.
% 64.00/64.41 parent0: (87703) {G0,W9,D5,L1,V1,M1} { leq( addition( one, multiplication
% 64.00/64.41 ( X, star( X ) ) ), star( X ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (14) {G0,W9,D5,L1,V1,M1} I { leq( addition( one,
% 64.00/64.41 multiplication( star( X ), X ) ), star( X ) ) }.
% 64.00/64.41 parent0: (87704) {G0,W9,D5,L1,V1,M1} { leq( addition( one, multiplication
% 64.00/64.41 ( star( X ), X ) ), star( X ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (15) {G0,W13,D4,L2,V3,M2} I { ! leq( addition( multiplication
% 64.00/64.41 ( X, Y ), Z ), Y ), leq( multiplication( star( X ), Z ), Y ) }.
% 64.00/64.41 parent0: (87705) {G0,W13,D4,L2,V3,M2} { ! leq( addition( multiplication( X
% 64.00/64.41 , Y ), Z ), Y ), leq( multiplication( star( X ), Z ), Y ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 1 ==> 1
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (87890) {G1,W14,D7,L1,V0,M1} { ! leq( multiplication( a,
% 64.00/64.41 multiplication( a, multiplication( a, multiplication( multiplication( a,
% 64.00/64.41 a ), a ) ) ) ), star( a ) ) }.
% 64.00/64.41 parent0[0]: (4) {G0,W11,D4,L1,V3,M1} I { multiplication( X, multiplication
% 64.00/64.41 ( Y, Z ) ) ==> multiplication( multiplication( X, Y ), Z ) }.
% 64.00/64.41 parent1[0; 8]: (87707) {G0,W14,D7,L1,V0,M1} { ! leq( multiplication( a,
% 64.00/64.41 multiplication( a, multiplication( a, multiplication( a, multiplication(
% 64.00/64.41 a, a ) ) ) ) ), star( a ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := a
% 64.00/64.41 Y := a
% 64.00/64.41 Z := a
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (87909) {G1,W14,D7,L1,V0,M1} { ! leq( multiplication( a,
% 64.00/64.41 multiplication( a, multiplication( multiplication( a, multiplication( a,
% 64.00/64.41 a ) ), a ) ) ), star( a ) ) }.
% 64.00/64.41 parent0[0]: (4) {G0,W11,D4,L1,V3,M1} I { multiplication( X, multiplication
% 64.00/64.41 ( Y, Z ) ) ==> multiplication( multiplication( X, Y ), Z ) }.
% 64.00/64.41 parent1[0; 6]: (87890) {G1,W14,D7,L1,V0,M1} { ! leq( multiplication( a,
% 64.00/64.41 multiplication( a, multiplication( a, multiplication( multiplication( a,
% 64.00/64.41 a ), a ) ) ) ), star( a ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := a
% 64.00/64.41 Y := multiplication( a, a )
% 64.00/64.41 Z := a
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (87926) {G1,W14,D7,L1,V0,M1} { ! leq( multiplication( a,
% 64.00/64.41 multiplication( a, multiplication( multiplication( multiplication( a, a )
% 64.00/64.41 , a ), a ) ) ), star( a ) ) }.
% 64.00/64.41 parent0[0]: (4) {G0,W11,D4,L1,V3,M1} I { multiplication( X, multiplication
% 64.00/64.41 ( Y, Z ) ) ==> multiplication( multiplication( X, Y ), Z ) }.
% 64.00/64.41 parent1[0; 7]: (87909) {G1,W14,D7,L1,V0,M1} { ! leq( multiplication( a,
% 64.00/64.41 multiplication( a, multiplication( multiplication( a, multiplication( a,
% 64.00/64.41 a ) ), a ) ) ), star( a ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := a
% 64.00/64.41 Y := a
% 64.00/64.41 Z := a
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (87940) {G1,W14,D7,L1,V0,M1} { ! leq( multiplication( a,
% 64.00/64.41 multiplication( multiplication( a, multiplication( multiplication( a, a )
% 64.00/64.41 , a ) ), a ) ), star( a ) ) }.
% 64.00/64.41 parent0[0]: (4) {G0,W11,D4,L1,V3,M1} I { multiplication( X, multiplication
% 64.00/64.41 ( Y, Z ) ) ==> multiplication( multiplication( X, Y ), Z ) }.
% 64.00/64.41 parent1[0; 4]: (87926) {G1,W14,D7,L1,V0,M1} { ! leq( multiplication( a,
% 64.00/64.41 multiplication( a, multiplication( multiplication( multiplication( a, a )
% 64.00/64.41 , a ), a ) ) ), star( a ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := a
% 64.00/64.41 Y := multiplication( multiplication( a, a ), a )
% 64.00/64.41 Z := a
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (87942) {G1,W14,D7,L1,V0,M1} { ! leq( multiplication( a,
% 64.00/64.41 multiplication( multiplication( multiplication( a, multiplication( a, a )
% 64.00/64.41 ), a ), a ) ), star( a ) ) }.
% 64.00/64.41 parent0[0]: (4) {G0,W11,D4,L1,V3,M1} I { multiplication( X, multiplication
% 64.00/64.41 ( Y, Z ) ) ==> multiplication( multiplication( X, Y ), Z ) }.
% 64.00/64.41 parent1[0; 5]: (87940) {G1,W14,D7,L1,V0,M1} { ! leq( multiplication( a,
% 64.00/64.41 multiplication( multiplication( a, multiplication( multiplication( a, a )
% 64.00/64.41 , a ) ), a ) ), star( a ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := a
% 64.00/64.41 Y := multiplication( a, a )
% 64.00/64.41 Z := a
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (87944) {G1,W14,D7,L1,V0,M1} { ! leq( multiplication( a,
% 64.00/64.41 multiplication( multiplication( multiplication( multiplication( a, a ), a
% 64.00/64.41 ), a ), a ) ), star( a ) ) }.
% 64.00/64.41 parent0[0]: (4) {G0,W11,D4,L1,V3,M1} I { multiplication( X, multiplication
% 64.00/64.41 ( Y, Z ) ) ==> multiplication( multiplication( X, Y ), Z ) }.
% 64.00/64.41 parent1[0; 6]: (87942) {G1,W14,D7,L1,V0,M1} { ! leq( multiplication( a,
% 64.00/64.41 multiplication( multiplication( multiplication( a, multiplication( a, a )
% 64.00/64.41 ), a ), a ) ), star( a ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := a
% 64.00/64.41 Y := a
% 64.00/64.41 Z := a
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (87945) {G1,W14,D7,L1,V0,M1} { ! leq( multiplication(
% 64.00/64.41 multiplication( a, multiplication( multiplication( multiplication( a, a )
% 64.00/64.41 , a ), a ) ), a ), star( a ) ) }.
% 64.00/64.41 parent0[0]: (4) {G0,W11,D4,L1,V3,M1} I { multiplication( X, multiplication
% 64.00/64.41 ( Y, Z ) ) ==> multiplication( multiplication( X, Y ), Z ) }.
% 64.00/64.41 parent1[0; 2]: (87944) {G1,W14,D7,L1,V0,M1} { ! leq( multiplication( a,
% 64.00/64.41 multiplication( multiplication( multiplication( multiplication( a, a ), a
% 64.00/64.41 ), a ), a ) ), star( a ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := a
% 64.00/64.41 Y := multiplication( multiplication( multiplication( a, a ), a ), a )
% 64.00/64.41 Z := a
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (87946) {G1,W14,D7,L1,V0,M1} { ! leq( multiplication(
% 64.00/64.41 multiplication( multiplication( a, multiplication( multiplication( a, a )
% 64.00/64.41 , a ) ), a ), a ), star( a ) ) }.
% 64.00/64.41 parent0[0]: (4) {G0,W11,D4,L1,V3,M1} I { multiplication( X, multiplication
% 64.00/64.41 ( Y, Z ) ) ==> multiplication( multiplication( X, Y ), Z ) }.
% 64.00/64.41 parent1[0; 3]: (87945) {G1,W14,D7,L1,V0,M1} { ! leq( multiplication(
% 64.00/64.41 multiplication( a, multiplication( multiplication( multiplication( a, a )
% 64.00/64.41 , a ), a ) ), a ), star( a ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := a
% 64.00/64.41 Y := multiplication( multiplication( a, a ), a )
% 64.00/64.41 Z := a
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (87947) {G1,W14,D7,L1,V0,M1} { ! leq( multiplication(
% 64.00/64.41 multiplication( multiplication( multiplication( a, multiplication( a, a )
% 64.00/64.41 ), a ), a ), a ), star( a ) ) }.
% 64.00/64.41 parent0[0]: (4) {G0,W11,D4,L1,V3,M1} I { multiplication( X, multiplication
% 64.00/64.41 ( Y, Z ) ) ==> multiplication( multiplication( X, Y ), Z ) }.
% 64.00/64.41 parent1[0; 4]: (87946) {G1,W14,D7,L1,V0,M1} { ! leq( multiplication(
% 64.00/64.41 multiplication( multiplication( a, multiplication( multiplication( a, a )
% 64.00/64.41 , a ) ), a ), a ), star( a ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := a
% 64.00/64.41 Y := multiplication( a, a )
% 64.00/64.41 Z := a
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (87948) {G1,W14,D7,L1,V0,M1} { ! leq( multiplication(
% 64.00/64.41 multiplication( multiplication( multiplication( multiplication( a, a ), a
% 64.00/64.41 ), a ), a ), a ), star( a ) ) }.
% 64.00/64.41 parent0[0]: (4) {G0,W11,D4,L1,V3,M1} I { multiplication( X, multiplication
% 64.00/64.41 ( Y, Z ) ) ==> multiplication( multiplication( X, Y ), Z ) }.
% 64.00/64.41 parent1[0; 5]: (87947) {G1,W14,D7,L1,V0,M1} { ! leq( multiplication(
% 64.00/64.41 multiplication( multiplication( multiplication( a, multiplication( a, a )
% 64.00/64.41 ), a ), a ), a ), star( a ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := a
% 64.00/64.41 Y := a
% 64.00/64.41 Z := a
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (17) {G1,W14,D7,L1,V0,M1} I;d(4);d(4);d(4);d(4) { ! leq(
% 64.00/64.41 multiplication( multiplication( multiplication( multiplication(
% 64.00/64.41 multiplication( a, a ), a ), a ), a ), a ), star( a ) ) }.
% 64.00/64.41 parent0: (87948) {G1,W14,D7,L1,V0,M1} { ! leq( multiplication(
% 64.00/64.41 multiplication( multiplication( multiplication( multiplication( a, a ), a
% 64.00/64.41 ), a ), a ), a ), star( a ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (87951) {G0,W8,D3,L2,V2,M2} { ! Y ==> addition( X, Y ), leq( X, Y
% 64.00/64.41 ) }.
% 64.00/64.41 parent0[0]: (12) {G0,W8,D3,L2,V2,M2} I { ! addition( X, Y ) ==> Y, leq( X,
% 64.00/64.41 Y ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (87952) {G0,W5,D3,L1,V1,M1} { X ==> addition( X, X ) }.
% 64.00/64.41 parent0[0]: (3) {G0,W5,D3,L1,V1,M1} I { addition( X, X ) ==> X }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 resolution: (87953) {G1,W3,D2,L1,V1,M1} { leq( X, X ) }.
% 64.00/64.41 parent0[0]: (87951) {G0,W8,D3,L2,V2,M2} { ! Y ==> addition( X, Y ), leq( X
% 64.00/64.41 , Y ) }.
% 64.00/64.41 parent1[0]: (87952) {G0,W5,D3,L1,V1,M1} { X ==> addition( X, X ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (20) {G1,W3,D2,L1,V1,M1} R(12,3) { leq( X, X ) }.
% 64.00/64.41 parent0: (87953) {G1,W3,D2,L1,V1,M1} { leq( X, X ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (87954) {G0,W8,D3,L2,V2,M2} { ! Y ==> addition( X, Y ), leq( X, Y
% 64.00/64.41 ) }.
% 64.00/64.41 parent0[0]: (12) {G0,W8,D3,L2,V2,M2} I { ! addition( X, Y ) ==> Y, leq( X,
% 64.00/64.41 Y ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (87955) {G1,W8,D3,L2,V2,M2} { ! X ==> addition( X, Y ), leq( Y, X
% 64.00/64.41 ) }.
% 64.00/64.41 parent0[0]: (0) {G0,W7,D3,L1,V2,M1} I { addition( X, Y ) = addition( Y, X )
% 64.00/64.41 }.
% 64.00/64.41 parent1[0; 3]: (87954) {G0,W8,D3,L2,V2,M2} { ! Y ==> addition( X, Y ), leq
% 64.00/64.41 ( X, Y ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (87958) {G1,W8,D3,L2,V2,M2} { ! addition( X, Y ) ==> X, leq( Y, X
% 64.00/64.41 ) }.
% 64.00/64.41 parent0[0]: (87955) {G1,W8,D3,L2,V2,M2} { ! X ==> addition( X, Y ), leq( Y
% 64.00/64.41 , X ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (22) {G1,W8,D3,L2,V2,M2} P(0,12) { ! addition( Y, X ) ==> Y,
% 64.00/64.41 leq( X, Y ) }.
% 64.00/64.41 parent0: (87958) {G1,W8,D3,L2,V2,M2} { ! addition( X, Y ) ==> X, leq( Y, X
% 64.00/64.41 ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 1 ==> 1
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (87960) {G0,W8,D3,L2,V2,M2} { ! Y ==> addition( X, Y ), leq( X, Y
% 64.00/64.41 ) }.
% 64.00/64.41 parent0[0]: (12) {G0,W8,D3,L2,V2,M2} I { ! addition( X, Y ) ==> Y, leq( X,
% 64.00/64.41 Y ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (87961) {G1,W14,D4,L2,V3,M2} { ! addition( X, Y ) ==> addition(
% 64.00/64.41 addition( Z, X ), Y ), leq( Z, addition( X, Y ) ) }.
% 64.00/64.41 parent0[0]: (1) {G0,W11,D4,L1,V3,M1} I { addition( Z, addition( Y, X ) )
% 64.00/64.41 ==> addition( addition( Z, Y ), X ) }.
% 64.00/64.41 parent1[0; 5]: (87960) {G0,W8,D3,L2,V2,M2} { ! Y ==> addition( X, Y ), leq
% 64.00/64.41 ( X, Y ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := X
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := Z
% 64.00/64.41 Y := addition( X, Y )
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (87962) {G1,W14,D4,L2,V3,M2} { ! addition( addition( Z, X ), Y )
% 64.00/64.41 ==> addition( X, Y ), leq( Z, addition( X, Y ) ) }.
% 64.00/64.41 parent0[0]: (87961) {G1,W14,D4,L2,V3,M2} { ! addition( X, Y ) ==> addition
% 64.00/64.41 ( addition( Z, X ), Y ), leq( Z, addition( X, Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (23) {G1,W14,D4,L2,V3,M2} P(1,12) { ! addition( addition( X, Y
% 64.00/64.41 ), Z ) ==> addition( Y, Z ), leq( X, addition( Y, Z ) ) }.
% 64.00/64.41 parent0: (87962) {G1,W14,D4,L2,V3,M2} { ! addition( addition( Z, X ), Y )
% 64.00/64.41 ==> addition( X, Y ), leq( Z, addition( X, Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := Z
% 64.00/64.41 Z := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 1 ==> 1
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (87963) {G0,W11,D4,L1,V3,M1} { addition( addition( X, Y ), Z ) ==>
% 64.00/64.41 addition( X, addition( Y, Z ) ) }.
% 64.00/64.41 parent0[0]: (1) {G0,W11,D4,L1,V3,M1} I { addition( Z, addition( Y, X ) )
% 64.00/64.41 ==> addition( addition( Z, Y ), X ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Z
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (87966) {G1,W11,D4,L1,V3,M1} { addition( addition( X, Y ), Z )
% 64.00/64.41 ==> addition( addition( Y, Z ), X ) }.
% 64.00/64.41 parent0[0]: (0) {G0,W7,D3,L1,V2,M1} I { addition( X, Y ) = addition( Y, X )
% 64.00/64.41 }.
% 64.00/64.41 parent1[0; 6]: (87963) {G0,W11,D4,L1,V3,M1} { addition( addition( X, Y ),
% 64.00/64.41 Z ) ==> addition( X, addition( Y, Z ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := addition( Y, Z )
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (24) {G1,W11,D4,L1,V3,M1} P(1,0) { addition( addition( X, Y )
% 64.00/64.41 , Z ) = addition( addition( Y, Z ), X ) }.
% 64.00/64.41 parent0: (87966) {G1,W11,D4,L1,V3,M1} { addition( addition( X, Y ), Z )
% 64.00/64.41 ==> addition( addition( Y, Z ), X ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (87980) {G0,W8,D3,L2,V2,M2} { Y ==> addition( X, Y ), ! leq( X, Y
% 64.00/64.41 ) }.
% 64.00/64.41 parent0[1]: (11) {G0,W8,D3,L2,V2,M2} I { ! leq( X, Y ), addition( X, Y )
% 64.00/64.41 ==> Y }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (87981) {G1,W8,D3,L2,V2,M2} { ! X ==> addition( X, Y ), leq( Y, X
% 64.00/64.41 ) }.
% 64.00/64.41 parent0[0]: (22) {G1,W8,D3,L2,V2,M2} P(0,12) { ! addition( Y, X ) ==> Y,
% 64.00/64.41 leq( X, Y ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 resolution: (87982) {G1,W10,D3,L2,V2,M2} { X ==> addition( Y, X ), ! X ==>
% 64.00/64.41 addition( X, Y ) }.
% 64.00/64.41 parent0[1]: (87980) {G0,W8,D3,L2,V2,M2} { Y ==> addition( X, Y ), ! leq( X
% 64.00/64.41 , Y ) }.
% 64.00/64.41 parent1[1]: (87981) {G1,W8,D3,L2,V2,M2} { ! X ==> addition( X, Y ), leq( Y
% 64.00/64.41 , X ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (87984) {G1,W10,D3,L2,V2,M2} { ! addition( X, Y ) ==> X, X ==>
% 64.00/64.41 addition( Y, X ) }.
% 64.00/64.41 parent0[1]: (87982) {G1,W10,D3,L2,V2,M2} { X ==> addition( Y, X ), ! X ==>
% 64.00/64.41 addition( X, Y ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (87985) {G1,W10,D3,L2,V2,M2} { addition( Y, X ) ==> X, ! addition
% 64.00/64.41 ( X, Y ) ==> X }.
% 64.00/64.41 parent0[1]: (87984) {G1,W10,D3,L2,V2,M2} { ! addition( X, Y ) ==> X, X ==>
% 64.00/64.41 addition( Y, X ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (29) {G2,W10,D3,L2,V2,M2} R(11,22) { addition( X, Y ) ==> Y, !
% 64.00/64.41 addition( Y, X ) ==> Y }.
% 64.00/64.41 parent0: (87985) {G1,W10,D3,L2,V2,M2} { addition( Y, X ) ==> X, ! addition
% 64.00/64.41 ( X, Y ) ==> X }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 1 ==> 1
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (87986) {G0,W8,D3,L2,V2,M2} { Y ==> addition( X, Y ), ! leq( X, Y
% 64.00/64.41 ) }.
% 64.00/64.41 parent0[1]: (11) {G0,W8,D3,L2,V2,M2} I { ! leq( X, Y ), addition( X, Y )
% 64.00/64.41 ==> Y }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (87988) {G1,W14,D4,L2,V3,M2} { addition( X, Y ) ==> addition(
% 64.00/64.41 addition( Z, X ), Y ), ! leq( Z, addition( X, Y ) ) }.
% 64.00/64.41 parent0[0]: (1) {G0,W11,D4,L1,V3,M1} I { addition( Z, addition( Y, X ) )
% 64.00/64.41 ==> addition( addition( Z, Y ), X ) }.
% 64.00/64.41 parent1[0; 4]: (87986) {G0,W8,D3,L2,V2,M2} { Y ==> addition( X, Y ), ! leq
% 64.00/64.41 ( X, Y ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := X
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := Z
% 64.00/64.41 Y := addition( X, Y )
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (87989) {G1,W14,D4,L2,V3,M2} { addition( addition( Z, X ), Y ) ==>
% 64.00/64.41 addition( X, Y ), ! leq( Z, addition( X, Y ) ) }.
% 64.00/64.41 parent0[0]: (87988) {G1,W14,D4,L2,V3,M2} { addition( X, Y ) ==> addition(
% 64.00/64.41 addition( Z, X ), Y ), ! leq( Z, addition( X, Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (32) {G1,W14,D4,L2,V3,M2} P(11,1) { addition( addition( X, Y )
% 64.00/64.41 , Z ) ==> addition( Y, Z ), ! leq( X, addition( Y, Z ) ) }.
% 64.00/64.41 parent0: (87989) {G1,W14,D4,L2,V3,M2} { addition( addition( Z, X ), Y )
% 64.00/64.41 ==> addition( X, Y ), ! leq( Z, addition( X, Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := Z
% 64.00/64.41 Z := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 1 ==> 1
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (87991) {G0,W11,D4,L1,V3,M1} { addition( addition( X, Y ), Z ) ==>
% 64.00/64.41 addition( X, addition( Y, Z ) ) }.
% 64.00/64.41 parent0[0]: (1) {G0,W11,D4,L1,V3,M1} I { addition( Z, addition( Y, X ) )
% 64.00/64.41 ==> addition( addition( Z, Y ), X ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Z
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (87997) {G1,W12,D4,L2,V3,M2} { addition( addition( X, Y ), Z )
% 64.00/64.41 ==> addition( X, Z ), ! leq( Y, Z ) }.
% 64.00/64.41 parent0[1]: (11) {G0,W8,D3,L2,V2,M2} I { ! leq( X, Y ), addition( X, Y )
% 64.00/64.41 ==> Y }.
% 64.00/64.41 parent1[0; 8]: (87991) {G0,W11,D4,L1,V3,M1} { addition( addition( X, Y ),
% 64.00/64.41 Z ) ==> addition( X, addition( Y, Z ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := Z
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (33) {G1,W12,D4,L2,V3,M2} P(11,1) { addition( addition( Z, X )
% 64.00/64.41 , Y ) ==> addition( Z, Y ), ! leq( X, Y ) }.
% 64.00/64.41 parent0: (87997) {G1,W12,D4,L2,V3,M2} { addition( addition( X, Y ), Z )
% 64.00/64.41 ==> addition( X, Z ), ! leq( Y, Z ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Z
% 64.00/64.41 Y := X
% 64.00/64.41 Z := Y
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 1 ==> 1
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88044) {G0,W8,D3,L2,V2,M2} { Y ==> addition( X, Y ), ! leq( X, Y
% 64.00/64.41 ) }.
% 64.00/64.41 parent0[1]: (11) {G0,W8,D3,L2,V2,M2} I { ! leq( X, Y ), addition( X, Y )
% 64.00/64.41 ==> Y }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88045) {G1,W8,D3,L2,V2,M2} { X ==> addition( X, Y ), ! leq( Y, X
% 64.00/64.41 ) }.
% 64.00/64.41 parent0[0]: (0) {G0,W7,D3,L1,V2,M1} I { addition( X, Y ) = addition( Y, X )
% 64.00/64.41 }.
% 64.00/64.41 parent1[0; 2]: (88044) {G0,W8,D3,L2,V2,M2} { Y ==> addition( X, Y ), ! leq
% 64.00/64.41 ( X, Y ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88048) {G1,W8,D3,L2,V2,M2} { addition( X, Y ) ==> X, ! leq( Y, X
% 64.00/64.41 ) }.
% 64.00/64.41 parent0[0]: (88045) {G1,W8,D3,L2,V2,M2} { X ==> addition( X, Y ), ! leq( Y
% 64.00/64.41 , X ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (35) {G1,W8,D3,L2,V2,M2} P(11,0) { addition( Y, X ) ==> Y, !
% 64.00/64.41 leq( X, Y ) }.
% 64.00/64.41 parent0: (88048) {G1,W8,D3,L2,V2,M2} { addition( X, Y ) ==> X, ! leq( Y, X
% 64.00/64.41 ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 1 ==> 1
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88050) {G0,W8,D3,L2,V2,M2} { ! Y ==> addition( X, Y ), leq( X, Y
% 64.00/64.41 ) }.
% 64.00/64.41 parent0[0]: (12) {G0,W8,D3,L2,V2,M2} I { ! addition( X, Y ) ==> Y, leq( X,
% 64.00/64.41 Y ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88051) {G1,W16,D4,L2,V3,M2} { ! multiplication( X, Y ) ==>
% 64.00/64.41 multiplication( X, addition( Z, Y ) ), leq( multiplication( X, Z ),
% 64.00/64.41 multiplication( X, Y ) ) }.
% 64.00/64.41 parent0[0]: (7) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Y ),
% 64.00/64.41 multiplication( X, Z ) ) ==> multiplication( X, addition( Y, Z ) ) }.
% 64.00/64.41 parent1[0; 5]: (88050) {G0,W8,D3,L2,V2,M2} { ! Y ==> addition( X, Y ), leq
% 64.00/64.41 ( X, Y ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Z
% 64.00/64.41 Z := Y
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := multiplication( X, Z )
% 64.00/64.41 Y := multiplication( X, Y )
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88052) {G1,W16,D4,L2,V3,M2} { ! multiplication( X, addition( Z, Y
% 64.00/64.41 ) ) ==> multiplication( X, Y ), leq( multiplication( X, Z ),
% 64.00/64.41 multiplication( X, Y ) ) }.
% 64.00/64.41 parent0[0]: (88051) {G1,W16,D4,L2,V3,M2} { ! multiplication( X, Y ) ==>
% 64.00/64.41 multiplication( X, addition( Z, Y ) ), leq( multiplication( X, Z ),
% 64.00/64.41 multiplication( X, Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (63) {G1,W16,D4,L2,V3,M2} P(7,12) { ! multiplication( X,
% 64.00/64.41 addition( Y, Z ) ) ==> multiplication( X, Z ), leq( multiplication( X, Y
% 64.00/64.41 ), multiplication( X, Z ) ) }.
% 64.00/64.41 parent0: (88052) {G1,W16,D4,L2,V3,M2} { ! multiplication( X, addition( Z,
% 64.00/64.41 Y ) ) ==> multiplication( X, Y ), leq( multiplication( X, Z ),
% 64.00/64.41 multiplication( X, Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Z
% 64.00/64.41 Z := Y
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 1 ==> 1
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88053) {G0,W13,D4,L1,V3,M1} { multiplication( X, addition( Y, Z )
% 64.00/64.41 ) ==> addition( multiplication( X, Y ), multiplication( X, Z ) ) }.
% 64.00/64.41 parent0[0]: (7) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Y ),
% 64.00/64.41 multiplication( X, Z ) ) ==> multiplication( X, addition( Y, Z ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88055) {G1,W13,D4,L1,V3,M1} { multiplication( X, addition( Z, Y
% 64.00/64.41 ) ) ==> addition( multiplication( X, Y ), multiplication( X, Z ) ) }.
% 64.00/64.41 parent0[0]: (0) {G0,W7,D3,L1,V2,M1} I { addition( X, Y ) = addition( Y, X )
% 64.00/64.41 }.
% 64.00/64.41 parent1[0; 3]: (88053) {G0,W13,D4,L1,V3,M1} { multiplication( X, addition
% 64.00/64.41 ( Y, Z ) ) ==> addition( multiplication( X, Y ), multiplication( X, Z ) )
% 64.00/64.41 }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := Z
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88057) {G1,W11,D4,L1,V3,M1} { multiplication( X, addition( Y, Z
% 64.00/64.41 ) ) ==> multiplication( X, addition( Z, Y ) ) }.
% 64.00/64.41 parent0[0]: (7) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Y ),
% 64.00/64.41 multiplication( X, Z ) ) ==> multiplication( X, addition( Y, Z ) ) }.
% 64.00/64.41 parent1[0; 6]: (88055) {G1,W13,D4,L1,V3,M1} { multiplication( X, addition
% 64.00/64.41 ( Z, Y ) ) ==> addition( multiplication( X, Y ), multiplication( X, Z ) )
% 64.00/64.41 }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Z
% 64.00/64.41 Z := Y
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Z
% 64.00/64.41 Z := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (64) {G1,W11,D4,L1,V3,M1} P(7,0);d(7) { multiplication( X,
% 64.00/64.41 addition( Y, Z ) ) = multiplication( X, addition( Z, Y ) ) }.
% 64.00/64.41 parent0: (88057) {G1,W11,D4,L1,V3,M1} { multiplication( X, addition( Y, Z
% 64.00/64.41 ) ) ==> multiplication( X, addition( Z, Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88059) {G0,W13,D4,L1,V3,M1} { multiplication( X, addition( Y, Z )
% 64.00/64.41 ) ==> addition( multiplication( X, Y ), multiplication( X, Z ) ) }.
% 64.00/64.41 parent0[0]: (7) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Y ),
% 64.00/64.41 multiplication( X, Z ) ) ==> multiplication( X, addition( Y, Z ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88060) {G1,W11,D4,L1,V2,M1} { multiplication( X, addition( one,
% 64.00/64.41 Y ) ) ==> addition( X, multiplication( X, Y ) ) }.
% 64.00/64.41 parent0[0]: (5) {G0,W5,D3,L1,V1,M1} I { multiplication( X, one ) ==> X }.
% 64.00/64.41 parent1[0; 7]: (88059) {G0,W13,D4,L1,V3,M1} { multiplication( X, addition
% 64.00/64.41 ( Y, Z ) ) ==> addition( multiplication( X, Y ), multiplication( X, Z ) )
% 64.00/64.41 }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := one
% 64.00/64.41 Z := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88062) {G1,W11,D4,L1,V2,M1} { addition( X, multiplication( X, Y )
% 64.00/64.41 ) ==> multiplication( X, addition( one, Y ) ) }.
% 64.00/64.41 parent0[0]: (88060) {G1,W11,D4,L1,V2,M1} { multiplication( X, addition(
% 64.00/64.41 one, Y ) ) ==> addition( X, multiplication( X, Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (65) {G1,W11,D4,L1,V2,M1} P(5,7) { addition( X, multiplication
% 64.00/64.41 ( X, Y ) ) = multiplication( X, addition( one, Y ) ) }.
% 64.00/64.41 parent0: (88062) {G1,W11,D4,L1,V2,M1} { addition( X, multiplication( X, Y
% 64.00/64.41 ) ) ==> multiplication( X, addition( one, Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88065) {G0,W8,D3,L2,V2,M2} { ! Y ==> addition( X, Y ), leq( X, Y
% 64.00/64.41 ) }.
% 64.00/64.41 parent0[0]: (12) {G0,W8,D3,L2,V2,M2} I { ! addition( X, Y ) ==> Y, leq( X,
% 64.00/64.41 Y ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88066) {G1,W16,D4,L2,V3,M2} { ! multiplication( X, Y ) ==>
% 64.00/64.41 multiplication( addition( Z, X ), Y ), leq( multiplication( Z, Y ),
% 64.00/64.41 multiplication( X, Y ) ) }.
% 64.00/64.41 parent0[0]: (8) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Z ),
% 64.00/64.41 multiplication( Y, Z ) ) ==> multiplication( addition( X, Y ), Z ) }.
% 64.00/64.41 parent1[0; 5]: (88065) {G0,W8,D3,L2,V2,M2} { ! Y ==> addition( X, Y ), leq
% 64.00/64.41 ( X, Y ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Z
% 64.00/64.41 Y := X
% 64.00/64.41 Z := Y
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := multiplication( Z, Y )
% 64.00/64.41 Y := multiplication( X, Y )
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88067) {G1,W16,D4,L2,V3,M2} { ! multiplication( addition( Z, X )
% 64.00/64.41 , Y ) ==> multiplication( X, Y ), leq( multiplication( Z, Y ),
% 64.00/64.41 multiplication( X, Y ) ) }.
% 64.00/64.41 parent0[0]: (88066) {G1,W16,D4,L2,V3,M2} { ! multiplication( X, Y ) ==>
% 64.00/64.41 multiplication( addition( Z, X ), Y ), leq( multiplication( Z, Y ),
% 64.00/64.41 multiplication( X, Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (94) {G1,W16,D4,L2,V3,M2} P(8,12) { ! multiplication( addition
% 64.00/64.41 ( X, Z ), Y ) ==> multiplication( Z, Y ), leq( multiplication( X, Y ),
% 64.00/64.41 multiplication( Z, Y ) ) }.
% 64.00/64.41 parent0: (88067) {G1,W16,D4,L2,V3,M2} { ! multiplication( addition( Z, X )
% 64.00/64.41 , Y ) ==> multiplication( X, Y ), leq( multiplication( Z, Y ),
% 64.00/64.41 multiplication( X, Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Z
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 1 ==> 1
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88069) {G1,W14,D4,L3,V3,M3} { ! leq( Z, Y ), ! leq(
% 64.00/64.41 multiplication( X, Y ), Z ), leq( multiplication( star( X ), Z ), Y ) }.
% 64.00/64.41 parent0[1]: (11) {G0,W8,D3,L2,V2,M2} I { ! leq( X, Y ), addition( X, Y )
% 64.00/64.41 ==> Y }.
% 64.00/64.41 parent1[0; 2]: (15) {G0,W13,D4,L2,V3,M2} I { ! leq( addition(
% 64.00/64.41 multiplication( X, Y ), Z ), Y ), leq( multiplication( star( X ), Z ), Y
% 64.00/64.41 ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := multiplication( X, Y )
% 64.00/64.41 Y := Z
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (162) {G1,W14,D4,L3,V3,M3} P(11,15) { ! leq( Z, Y ), leq(
% 64.00/64.41 multiplication( star( X ), Z ), Y ), ! leq( multiplication( X, Y ), Z )
% 64.00/64.41 }.
% 64.00/64.41 parent0: (88069) {G1,W14,D4,L3,V3,M3} { ! leq( Z, Y ), ! leq(
% 64.00/64.41 multiplication( X, Y ), Z ), leq( multiplication( star( X ), Z ), Y ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 1 ==> 2
% 64.00/64.41 2 ==> 1
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88072) {G1,W11,D4,L2,V2,M2} { leq( star( X ), Y ), ! leq(
% 64.00/64.41 addition( multiplication( X, Y ), one ), Y ) }.
% 64.00/64.41 parent0[0]: (5) {G0,W5,D3,L1,V1,M1} I { multiplication( X, one ) ==> X }.
% 64.00/64.41 parent1[1; 1]: (15) {G0,W13,D4,L2,V3,M2} I { ! leq( addition(
% 64.00/64.41 multiplication( X, Y ), Z ), Y ), leq( multiplication( star( X ), Z ), Y
% 64.00/64.41 ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := star( X )
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := one
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (167) {G1,W11,D4,L2,V2,M2} P(5,15) { ! leq( addition(
% 64.00/64.41 multiplication( X, Y ), one ), Y ), leq( star( X ), Y ) }.
% 64.00/64.41 parent0: (88072) {G1,W11,D4,L2,V2,M2} { leq( star( X ), Y ), ! leq(
% 64.00/64.41 addition( multiplication( X, Y ), one ), Y ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 1
% 64.00/64.41 1 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88074) {G1,W14,D4,L2,V3,M2} { ! addition( Y, Z ) ==> addition(
% 64.00/64.41 addition( X, Y ), Z ), leq( X, addition( Y, Z ) ) }.
% 64.00/64.41 parent0[0]: (23) {G1,W14,D4,L2,V3,M2} P(1,12) { ! addition( addition( X, Y
% 64.00/64.41 ), Z ) ==> addition( Y, Z ), leq( X, addition( Y, Z ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88077) {G1,W15,D3,L3,V3,M3} { ! addition( X, Y ) ==> addition( X
% 64.00/64.41 , Y ), ! leq( Z, X ), leq( Z, addition( X, Y ) ) }.
% 64.00/64.41 parent0[1]: (11) {G0,W8,D3,L2,V2,M2} I { ! leq( X, Y ), addition( X, Y )
% 64.00/64.41 ==> Y }.
% 64.00/64.41 parent1[0; 6]: (88074) {G1,W14,D4,L2,V3,M2} { ! addition( Y, Z ) ==>
% 64.00/64.41 addition( addition( X, Y ), Z ), leq( X, addition( Y, Z ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Z
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := Z
% 64.00/64.41 Y := X
% 64.00/64.41 Z := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqrefl: (88126) {G0,W8,D3,L2,V3,M2} { ! leq( Z, X ), leq( Z, addition( X,
% 64.00/64.41 Y ) ) }.
% 64.00/64.41 parent0[0]: (88077) {G1,W15,D3,L3,V3,M3} { ! addition( X, Y ) ==> addition
% 64.00/64.41 ( X, Y ), ! leq( Z, X ), leq( Z, addition( X, Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (228) {G2,W8,D3,L2,V3,M2} P(11,23);q { leq( X, addition( Y, Z
% 64.00/64.41 ) ), ! leq( X, Y ) }.
% 64.00/64.41 parent0: (88126) {G0,W8,D3,L2,V3,M2} { ! leq( Z, X ), leq( Z, addition( X
% 64.00/64.41 , Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := Z
% 64.00/64.41 Z := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 1
% 64.00/64.41 1 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88128) {G1,W14,D4,L2,V3,M2} { ! addition( Y, Z ) ==> addition(
% 64.00/64.41 addition( X, Y ), Z ), leq( X, addition( Y, Z ) ) }.
% 64.00/64.41 parent0[0]: (23) {G1,W14,D4,L2,V3,M2} P(1,12) { ! addition( addition( X, Y
% 64.00/64.41 ), Z ) ==> addition( Y, Z ), leq( X, addition( Y, Z ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88131) {G1,W12,D3,L2,V2,M2} { ! addition( X, Y ) ==> addition( X
% 64.00/64.41 , Y ), leq( X, addition( X, Y ) ) }.
% 64.00/64.41 parent0[0]: (3) {G0,W5,D3,L1,V1,M1} I { addition( X, X ) ==> X }.
% 64.00/64.41 parent1[0; 6]: (88128) {G1,W14,D4,L2,V3,M2} { ! addition( Y, Z ) ==>
% 64.00/64.41 addition( addition( X, Y ), Z ), leq( X, addition( Y, Z ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := X
% 64.00/64.41 Z := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqrefl: (88134) {G0,W5,D3,L1,V2,M1} { leq( X, addition( X, Y ) ) }.
% 64.00/64.41 parent0[0]: (88131) {G1,W12,D3,L2,V2,M2} { ! addition( X, Y ) ==> addition
% 64.00/64.41 ( X, Y ), leq( X, addition( X, Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (232) {G2,W5,D3,L1,V2,M1} P(3,23);q { leq( X, addition( X, Y )
% 64.00/64.41 ) }.
% 64.00/64.41 parent0: (88134) {G0,W5,D3,L1,V2,M1} { leq( X, addition( X, Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88136) {G1,W7,D4,L1,V3,M1} { leq( X, addition( addition( X, Y )
% 64.00/64.41 , Z ) ) }.
% 64.00/64.41 parent0[0]: (1) {G0,W11,D4,L1,V3,M1} I { addition( Z, addition( Y, X ) )
% 64.00/64.41 ==> addition( addition( Z, Y ), X ) }.
% 64.00/64.41 parent1[0; 2]: (232) {G2,W5,D3,L1,V2,M1} P(3,23);q { leq( X, addition( X, Y
% 64.00/64.41 ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Z
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := X
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := addition( Y, Z )
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (239) {G3,W7,D4,L1,V3,M1} P(1,232) { leq( X, addition(
% 64.00/64.41 addition( X, Y ), Z ) ) }.
% 64.00/64.41 parent0: (88136) {G1,W7,D4,L1,V3,M1} { leq( X, addition( addition( X, Y )
% 64.00/64.41 , Z ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88137) {G1,W5,D3,L1,V2,M1} { leq( X, addition( Y, X ) ) }.
% 64.00/64.41 parent0[0]: (0) {G0,W7,D3,L1,V2,M1} I { addition( X, Y ) = addition( Y, X )
% 64.00/64.41 }.
% 64.00/64.41 parent1[0; 2]: (232) {G2,W5,D3,L1,V2,M1} P(3,23);q { leq( X, addition( X, Y
% 64.00/64.41 ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (240) {G3,W5,D3,L1,V2,M1} P(0,232) { leq( X, addition( Y, X )
% 64.00/64.41 ) }.
% 64.00/64.41 parent0: (88137) {G1,W5,D3,L1,V2,M1} { leq( X, addition( Y, X ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88139) {G0,W8,D3,L2,V2,M2} { Y ==> addition( X, Y ), ! leq( X, Y
% 64.00/64.41 ) }.
% 64.00/64.41 parent0[1]: (11) {G0,W8,D3,L2,V2,M2} I { ! leq( X, Y ), addition( X, Y )
% 64.00/64.41 ==> Y }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 resolution: (88141) {G1,W9,D4,L1,V2,M1} { addition( X, Y ) ==> addition( Y
% 64.00/64.41 , addition( X, Y ) ) }.
% 64.00/64.41 parent0[1]: (88139) {G0,W8,D3,L2,V2,M2} { Y ==> addition( X, Y ), ! leq( X
% 64.00/64.41 , Y ) }.
% 64.00/64.41 parent1[0]: (240) {G3,W5,D3,L1,V2,M1} P(0,232) { leq( X, addition( Y, X ) )
% 64.00/64.41 }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := addition( X, Y )
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88142) {G1,W9,D4,L1,V2,M1} { addition( X, Y ) ==> addition(
% 64.00/64.41 addition( Y, X ), Y ) }.
% 64.00/64.41 parent0[0]: (1) {G0,W11,D4,L1,V3,M1} I { addition( Z, addition( Y, X ) )
% 64.00/64.41 ==> addition( addition( Z, Y ), X ) }.
% 64.00/64.41 parent1[0; 4]: (88141) {G1,W9,D4,L1,V2,M1} { addition( X, Y ) ==> addition
% 64.00/64.41 ( Y, addition( X, Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := X
% 64.00/64.41 Z := Y
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88143) {G1,W9,D4,L1,V2,M1} { addition( addition( Y, X ), Y ) ==>
% 64.00/64.41 addition( X, Y ) }.
% 64.00/64.41 parent0[0]: (88142) {G1,W9,D4,L1,V2,M1} { addition( X, Y ) ==> addition(
% 64.00/64.41 addition( Y, X ), Y ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (241) {G4,W9,D4,L1,V2,M1} R(240,11);d(1) { addition( addition
% 64.00/64.41 ( X, Y ), X ) ==> addition( Y, X ) }.
% 64.00/64.41 parent0: (88143) {G1,W9,D4,L1,V2,M1} { addition( addition( Y, X ), Y ) ==>
% 64.00/64.41 addition( X, Y ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88145) {G1,W9,D4,L1,V3,M1} { leq( multiplication( X, Y ),
% 64.00/64.41 multiplication( addition( Z, X ), Y ) ) }.
% 64.00/64.41 parent0[0]: (8) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Z ),
% 64.00/64.41 multiplication( Y, Z ) ) ==> multiplication( addition( X, Y ), Z ) }.
% 64.00/64.41 parent1[0; 4]: (240) {G3,W5,D3,L1,V2,M1} P(0,232) { leq( X, addition( Y, X
% 64.00/64.41 ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Z
% 64.00/64.41 Y := X
% 64.00/64.41 Z := Y
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := multiplication( X, Y )
% 64.00/64.41 Y := multiplication( Z, Y )
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (242) {G4,W9,D4,L1,V3,M1} P(8,240) { leq( multiplication( Z, Y
% 64.00/64.41 ), multiplication( addition( X, Z ), Y ) ) }.
% 64.00/64.41 parent0: (88145) {G1,W9,D4,L1,V3,M1} { leq( multiplication( X, Y ),
% 64.00/64.41 multiplication( addition( Z, X ), Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Z
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88147) {G1,W9,D4,L1,V3,M1} { leq( multiplication( X, Y ),
% 64.00/64.41 multiplication( X, addition( Z, Y ) ) ) }.
% 64.00/64.41 parent0[0]: (7) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Y ),
% 64.00/64.41 multiplication( X, Z ) ) ==> multiplication( X, addition( Y, Z ) ) }.
% 64.00/64.41 parent1[0; 4]: (240) {G3,W5,D3,L1,V2,M1} P(0,232) { leq( X, addition( Y, X
% 64.00/64.41 ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Z
% 64.00/64.41 Z := Y
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := multiplication( X, Y )
% 64.00/64.41 Y := multiplication( X, Z )
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (244) {G4,W9,D4,L1,V3,M1} P(7,240) { leq( multiplication( X, Z
% 64.00/64.41 ), multiplication( X, addition( Y, Z ) ) ) }.
% 64.00/64.41 parent0: (88147) {G1,W9,D4,L1,V3,M1} { leq( multiplication( X, Y ),
% 64.00/64.41 multiplication( X, addition( Z, Y ) ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Z
% 64.00/64.41 Z := Y
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88148) {G1,W11,D4,L1,V3,M1} { addition( addition( Y, Z ), X ) =
% 64.00/64.41 addition( addition( X, Y ), Z ) }.
% 64.00/64.41 parent0[0]: (24) {G1,W11,D4,L1,V3,M1} P(1,0) { addition( addition( X, Y ),
% 64.00/64.41 Z ) = addition( addition( Y, Z ), X ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88149) {G2,W7,D4,L1,V3,M1} { leq( X, addition( addition( X, Y )
% 64.00/64.41 , Z ) ) }.
% 64.00/64.41 parent0[0]: (88148) {G1,W11,D4,L1,V3,M1} { addition( addition( Y, Z ), X )
% 64.00/64.41 = addition( addition( X, Y ), Z ) }.
% 64.00/64.41 parent1[0; 2]: (240) {G3,W5,D3,L1,V2,M1} P(0,232) { leq( X, addition( Y, X
% 64.00/64.41 ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := addition( Y, Z )
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88150) {G2,W7,D4,L1,V3,M1} { leq( X, addition( addition( Z, X )
% 64.00/64.41 , Y ) ) }.
% 64.00/64.41 parent0[0]: (88148) {G1,W11,D4,L1,V3,M1} { addition( addition( Y, Z ), X )
% 64.00/64.41 = addition( addition( X, Y ), Z ) }.
% 64.00/64.41 parent1[0; 2]: (88149) {G2,W7,D4,L1,V3,M1} { leq( X, addition( addition( X
% 64.00/64.41 , Y ), Z ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Z
% 64.00/64.41 Y := X
% 64.00/64.41 Z := Y
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (251) {G4,W7,D4,L1,V3,M1} P(24,240) { leq( Z, addition(
% 64.00/64.41 addition( Y, Z ), X ) ) }.
% 64.00/64.41 parent0: (88150) {G2,W7,D4,L1,V3,M1} { leq( X, addition( addition( Z, X )
% 64.00/64.41 , Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Z
% 64.00/64.41 Y := X
% 64.00/64.41 Z := Y
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88152) {G1,W8,D3,L2,V2,M2} { X ==> addition( X, Y ), ! leq( Y, X
% 64.00/64.41 ) }.
% 64.00/64.41 parent0[0]: (35) {G1,W8,D3,L2,V2,M2} P(11,0) { addition( Y, X ) ==> Y, !
% 64.00/64.41 leq( X, Y ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88154) {G1,W9,D2,L3,V2,M3} { X ==> Y, ! leq( X, Y ), ! leq( Y, X
% 64.00/64.41 ) }.
% 64.00/64.41 parent0[1]: (11) {G0,W8,D3,L2,V2,M2} I { ! leq( X, Y ), addition( X, Y )
% 64.00/64.41 ==> Y }.
% 64.00/64.41 parent1[0; 2]: (88152) {G1,W8,D3,L2,V2,M2} { X ==> addition( X, Y ), ! leq
% 64.00/64.41 ( Y, X ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (479) {G2,W9,D2,L3,V2,M3} P(35,11) { ! leq( X, Y ), X = Y, !
% 64.00/64.41 leq( Y, X ) }.
% 64.00/64.41 parent0: (88154) {G1,W9,D2,L3,V2,M3} { X ==> Y, ! leq( X, Y ), ! leq( Y, X
% 64.00/64.41 ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 1
% 64.00/64.41 1 ==> 0
% 64.00/64.41 2 ==> 2
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88157) {G2,W8,D3,L2,V3,M2} { leq( X, addition( Y, Z ) ), ! leq(
% 64.00/64.41 X, Z ) }.
% 64.00/64.41 parent0[0]: (33) {G1,W12,D4,L2,V3,M2} P(11,1) { addition( addition( Z, X )
% 64.00/64.41 , Y ) ==> addition( Z, Y ), ! leq( X, Y ) }.
% 64.00/64.41 parent1[0; 2]: (251) {G4,W7,D4,L1,V3,M1} P(24,240) { leq( Z, addition(
% 64.00/64.41 addition( Y, Z ), X ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Z
% 64.00/64.41 Z := Y
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := Z
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (503) {G5,W8,D3,L2,V3,M2} P(33,251) { leq( Y, addition( X, Z )
% 64.00/64.41 ), ! leq( Y, Z ) }.
% 64.00/64.41 parent0: (88157) {G2,W8,D3,L2,V3,M2} { leq( X, addition( Y, Z ) ), ! leq(
% 64.00/64.41 X, Z ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := X
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 1 ==> 1
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88161) {G1,W8,D3,L2,V3,M2} { leq( X, Z ), ! leq( addition( Y, X
% 64.00/64.41 ), Z ) }.
% 64.00/64.41 parent0[1]: (11) {G0,W8,D3,L2,V2,M2} I { ! leq( X, Y ), addition( X, Y )
% 64.00/64.41 ==> Y }.
% 64.00/64.41 parent1[0; 2]: (251) {G4,W7,D4,L1,V3,M1} P(24,240) { leq( Z, addition(
% 64.00/64.41 addition( Y, Z ), X ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := addition( Y, X )
% 64.00/64.41 Y := Z
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := Z
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (513) {G5,W8,D3,L2,V3,M2} P(11,251) { leq( Y, Z ), ! leq(
% 64.00/64.41 addition( X, Y ), Z ) }.
% 64.00/64.41 parent0: (88161) {G1,W8,D3,L2,V3,M2} { leq( X, Z ), ! leq( addition( Y, X
% 64.00/64.41 ), Z ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := X
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 1 ==> 1
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88166) {G1,W8,D3,L2,V3,M2} { leq( X, Z ), ! leq( addition( X, Y
% 64.00/64.41 ), Z ) }.
% 64.00/64.41 parent0[1]: (11) {G0,W8,D3,L2,V2,M2} I { ! leq( X, Y ), addition( X, Y )
% 64.00/64.41 ==> Y }.
% 64.00/64.41 parent1[0; 2]: (239) {G3,W7,D4,L1,V3,M1} P(1,232) { leq( X, addition(
% 64.00/64.41 addition( X, Y ), Z ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := addition( X, Y )
% 64.00/64.41 Y := Z
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (526) {G4,W8,D3,L2,V3,M2} P(11,239) { leq( X, Z ), ! leq(
% 64.00/64.41 addition( X, Y ), Z ) }.
% 64.00/64.41 parent0: (88166) {G1,W8,D3,L2,V3,M2} { leq( X, Z ), ! leq( addition( X, Y
% 64.00/64.41 ), Z ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 1 ==> 1
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 resolution: (88170) {G1,W4,D3,L1,V1,M1} { leq( one, star( X ) ) }.
% 64.00/64.41 parent0[1]: (526) {G4,W8,D3,L2,V3,M2} P(11,239) { leq( X, Z ), ! leq(
% 64.00/64.41 addition( X, Y ), Z ) }.
% 64.00/64.41 parent1[0]: (14) {G0,W9,D5,L1,V1,M1} I { leq( addition( one, multiplication
% 64.00/64.41 ( star( X ), X ) ), star( X ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := one
% 64.00/64.41 Y := multiplication( star( X ), X )
% 64.00/64.41 Z := star( X )
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (719) {G5,W4,D3,L1,V1,M1} R(526,14) { leq( one, star( X ) )
% 64.00/64.41 }.
% 64.00/64.41 parent0: (88170) {G1,W4,D3,L1,V1,M1} { leq( one, star( X ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88172) {G2,W15,D3,L3,V4,M3} { ! leq( addition( Y, Z ), T ), !
% 64.00/64.41 leq( X, addition( Y, Z ) ), leq( addition( X, Y ), T ) }.
% 64.00/64.41 parent0[0]: (32) {G1,W14,D4,L2,V3,M2} P(11,1) { addition( addition( X, Y )
% 64.00/64.41 , Z ) ==> addition( Y, Z ), ! leq( X, addition( Y, Z ) ) }.
% 64.00/64.41 parent1[1; 2]: (526) {G4,W8,D3,L2,V3,M2} P(11,239) { leq( X, Z ), ! leq(
% 64.00/64.41 addition( X, Y ), Z ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := addition( X, Y )
% 64.00/64.41 Y := Z
% 64.00/64.41 Z := T
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (724) {G5,W15,D3,L3,V4,M3} P(32,526) { leq( addition( X, Y ),
% 64.00/64.41 T ), ! leq( addition( Y, Z ), T ), ! leq( X, addition( Y, Z ) ) }.
% 64.00/64.41 parent0: (88172) {G2,W15,D3,L3,V4,M3} { ! leq( addition( Y, Z ), T ), !
% 64.00/64.41 leq( X, addition( Y, Z ) ), leq( addition( X, Y ), T ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 T := T
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 1
% 64.00/64.41 1 ==> 2
% 64.00/64.41 2 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88175) {G1,W12,D4,L2,V4,M2} { ! leq( multiplication( addition( X
% 64.00/64.41 , Z ), Y ), T ), leq( multiplication( X, Y ), T ) }.
% 64.00/64.41 parent0[0]: (8) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Z ),
% 64.00/64.41 multiplication( Y, Z ) ) ==> multiplication( addition( X, Y ), Z ) }.
% 64.00/64.41 parent1[1; 2]: (526) {G4,W8,D3,L2,V3,M2} P(11,239) { leq( X, Z ), ! leq(
% 64.00/64.41 addition( X, Y ), Z ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Z
% 64.00/64.41 Z := Y
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := multiplication( X, Y )
% 64.00/64.41 Y := multiplication( Z, Y )
% 64.00/64.41 Z := T
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (729) {G5,W12,D4,L2,V4,M2} P(8,526) { leq( multiplication( X,
% 64.00/64.41 Y ), T ), ! leq( multiplication( addition( X, Z ), Y ), T ) }.
% 64.00/64.41 parent0: (88175) {G1,W12,D4,L2,V4,M2} { ! leq( multiplication( addition( X
% 64.00/64.41 , Z ), Y ), T ), leq( multiplication( X, Y ), T ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 T := T
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 1
% 64.00/64.41 1 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88177) {G1,W12,D4,L2,V4,M2} { ! leq( multiplication( X, addition
% 64.00/64.41 ( Y, Z ) ), T ), leq( multiplication( X, Y ), T ) }.
% 64.00/64.41 parent0[0]: (7) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Y ),
% 64.00/64.41 multiplication( X, Z ) ) ==> multiplication( X, addition( Y, Z ) ) }.
% 64.00/64.41 parent1[1; 2]: (526) {G4,W8,D3,L2,V3,M2} P(11,239) { leq( X, Z ), ! leq(
% 64.00/64.41 addition( X, Y ), Z ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := multiplication( X, Y )
% 64.00/64.41 Y := multiplication( X, Z )
% 64.00/64.41 Z := T
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (730) {G5,W12,D4,L2,V4,M2} P(7,526) { leq( multiplication( X,
% 64.00/64.41 Y ), T ), ! leq( multiplication( X, addition( Y, Z ) ), T ) }.
% 64.00/64.41 parent0: (88177) {G1,W12,D4,L2,V4,M2} { ! leq( multiplication( X, addition
% 64.00/64.41 ( Y, Z ) ), T ), leq( multiplication( X, Y ), T ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 T := T
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 1
% 64.00/64.41 1 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88179) {G1,W9,D2,L3,V3,M3} { ! leq( Y, Z ), ! leq( X, Y ), leq(
% 64.00/64.41 X, Z ) }.
% 64.00/64.41 parent0[1]: (11) {G0,W8,D3,L2,V2,M2} I { ! leq( X, Y ), addition( X, Y )
% 64.00/64.41 ==> Y }.
% 64.00/64.41 parent1[1; 2]: (526) {G4,W8,D3,L2,V3,M2} P(11,239) { leq( X, Z ), ! leq(
% 64.00/64.41 addition( X, Y ), Z ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (731) {G5,W9,D2,L3,V3,M3} P(11,526) { leq( X, Z ), ! leq( Y, Z
% 64.00/64.41 ), ! leq( X, Y ) }.
% 64.00/64.41 parent0: (88179) {G1,W9,D2,L3,V3,M3} { ! leq( Y, Z ), ! leq( X, Y ), leq(
% 64.00/64.41 X, Z ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 1
% 64.00/64.41 1 ==> 2
% 64.00/64.41 2 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 factor: (88182) {G5,W16,D4,L2,V2,M2} { leq( addition( addition( X, Y ), X
% 64.00/64.41 ), addition( X, Y ) ), ! leq( addition( X, Y ), addition( X, Y ) ) }.
% 64.00/64.41 parent0[1, 2]: (724) {G5,W15,D3,L3,V4,M3} P(32,526) { leq( addition( X, Y )
% 64.00/64.41 , T ), ! leq( addition( Y, Z ), T ), ! leq( X, addition( Y, Z ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := addition( X, Y )
% 64.00/64.41 Y := X
% 64.00/64.41 Z := Y
% 64.00/64.41 T := addition( X, Y )
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88183) {G5,W14,D3,L2,V2,M2} { leq( addition( Y, X ), addition( X
% 64.00/64.41 , Y ) ), ! leq( addition( X, Y ), addition( X, Y ) ) }.
% 64.00/64.41 parent0[0]: (241) {G4,W9,D4,L1,V2,M1} R(240,11);d(1) { addition( addition(
% 64.00/64.41 X, Y ), X ) ==> addition( Y, X ) }.
% 64.00/64.41 parent1[0; 1]: (88182) {G5,W16,D4,L2,V2,M2} { leq( addition( addition( X,
% 64.00/64.41 Y ), X ), addition( X, Y ) ), ! leq( addition( X, Y ), addition( X, Y ) )
% 64.00/64.41 }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 resolution: (88184) {G2,W7,D3,L1,V2,M1} { leq( addition( X, Y ), addition
% 64.00/64.41 ( Y, X ) ) }.
% 64.00/64.41 parent0[1]: (88183) {G5,W14,D3,L2,V2,M2} { leq( addition( Y, X ), addition
% 64.00/64.41 ( X, Y ) ), ! leq( addition( X, Y ), addition( X, Y ) ) }.
% 64.00/64.41 parent1[0]: (20) {G1,W3,D2,L1,V1,M1} R(12,3) { leq( X, X ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := addition( Y, X )
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (732) {G6,W7,D3,L1,V2,M1} F(724);d(241);r(20) { leq( addition
% 64.00/64.41 ( Y, X ), addition( X, Y ) ) }.
% 64.00/64.41 parent0: (88184) {G2,W7,D3,L1,V2,M1} { leq( addition( X, Y ), addition( Y
% 64.00/64.41 , X ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88185) {G1,W8,D3,L2,V2,M2} { X ==> addition( X, Y ), ! leq( Y, X
% 64.00/64.41 ) }.
% 64.00/64.41 parent0[0]: (35) {G1,W8,D3,L2,V2,M2} P(11,0) { addition( Y, X ) ==> Y, !
% 64.00/64.41 leq( X, Y ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 resolution: (88186) {G2,W7,D4,L1,V1,M1} { star( X ) ==> addition( star( X
% 64.00/64.41 ), one ) }.
% 64.00/64.41 parent0[1]: (88185) {G1,W8,D3,L2,V2,M2} { X ==> addition( X, Y ), ! leq( Y
% 64.00/64.41 , X ) }.
% 64.00/64.41 parent1[0]: (719) {G5,W4,D3,L1,V1,M1} R(526,14) { leq( one, star( X ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := star( X )
% 64.00/64.41 Y := one
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88187) {G2,W7,D4,L1,V1,M1} { addition( star( X ), one ) ==> star
% 64.00/64.41 ( X ) }.
% 64.00/64.41 parent0[0]: (88186) {G2,W7,D4,L1,V1,M1} { star( X ) ==> addition( star( X
% 64.00/64.41 ), one ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (733) {G6,W7,D4,L1,V1,M1} R(719,35) { addition( star( X ), one
% 64.00/64.41 ) ==> star( X ) }.
% 64.00/64.41 parent0: (88187) {G2,W7,D4,L1,V1,M1} { addition( star( X ), one ) ==> star
% 64.00/64.41 ( X ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88188) {G0,W8,D3,L2,V2,M2} { Y ==> addition( X, Y ), ! leq( X, Y
% 64.00/64.41 ) }.
% 64.00/64.41 parent0[1]: (11) {G0,W8,D3,L2,V2,M2} I { ! leq( X, Y ), addition( X, Y )
% 64.00/64.41 ==> Y }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 resolution: (88189) {G1,W7,D4,L1,V1,M1} { star( X ) ==> addition( one,
% 64.00/64.41 star( X ) ) }.
% 64.00/64.41 parent0[1]: (88188) {G0,W8,D3,L2,V2,M2} { Y ==> addition( X, Y ), ! leq( X
% 64.00/64.41 , Y ) }.
% 64.00/64.41 parent1[0]: (719) {G5,W4,D3,L1,V1,M1} R(526,14) { leq( one, star( X ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := one
% 64.00/64.41 Y := star( X )
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88190) {G1,W7,D4,L1,V1,M1} { addition( one, star( X ) ) ==> star
% 64.00/64.41 ( X ) }.
% 64.00/64.41 parent0[0]: (88189) {G1,W7,D4,L1,V1,M1} { star( X ) ==> addition( one,
% 64.00/64.41 star( X ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (736) {G6,W7,D4,L1,V1,M1} R(719,11) { addition( one, star( X )
% 64.00/64.41 ) ==> star( X ) }.
% 64.00/64.41 parent0: (88190) {G1,W7,D4,L1,V1,M1} { addition( one, star( X ) ) ==> star
% 64.00/64.41 ( X ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 resolution: (88192) {G6,W9,D4,L1,V3,M1} { leq( addition( X, Y ), addition
% 64.00/64.41 ( Z, addition( Y, X ) ) ) }.
% 64.00/64.41 parent0[1]: (503) {G5,W8,D3,L2,V3,M2} P(33,251) { leq( Y, addition( X, Z )
% 64.00/64.41 ), ! leq( Y, Z ) }.
% 64.00/64.41 parent1[0]: (732) {G6,W7,D3,L1,V2,M1} F(724);d(241);r(20) { leq( addition(
% 64.00/64.41 Y, X ), addition( X, Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Z
% 64.00/64.41 Y := addition( X, Y )
% 64.00/64.41 Z := addition( Y, X )
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88193) {G1,W9,D4,L1,V3,M1} { leq( addition( X, Y ), addition(
% 64.00/64.41 addition( Z, Y ), X ) ) }.
% 64.00/64.41 parent0[0]: (1) {G0,W11,D4,L1,V3,M1} I { addition( Z, addition( Y, X ) )
% 64.00/64.41 ==> addition( addition( Z, Y ), X ) }.
% 64.00/64.41 parent1[0; 4]: (88192) {G6,W9,D4,L1,V3,M1} { leq( addition( X, Y ),
% 64.00/64.41 addition( Z, addition( Y, X ) ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (792) {G7,W9,D4,L1,V3,M1} R(503,732);d(1) { leq( addition( X,
% 64.00/64.41 Y ), addition( addition( Z, Y ), X ) ) }.
% 64.00/64.41 parent0: (88193) {G1,W9,D4,L1,V3,M1} { leq( addition( X, Y ), addition(
% 64.00/64.41 addition( Z, Y ), X ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88195) {G1,W12,D4,L2,V4,M2} { leq( X, multiplication( Y,
% 64.00/64.41 addition( Z, T ) ) ), ! leq( X, multiplication( Y, T ) ) }.
% 64.00/64.41 parent0[0]: (7) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Y ),
% 64.00/64.41 multiplication( X, Z ) ) ==> multiplication( X, addition( Y, Z ) ) }.
% 64.00/64.41 parent1[0; 2]: (503) {G5,W8,D3,L2,V3,M2} P(33,251) { leq( Y, addition( X, Z
% 64.00/64.41 ) ), ! leq( Y, Z ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := Z
% 64.00/64.41 Z := T
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := multiplication( Y, Z )
% 64.00/64.41 Y := X
% 64.00/64.41 Z := multiplication( Y, T )
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (812) {G6,W12,D4,L2,V4,M2} P(7,503) { leq( T, multiplication(
% 64.00/64.41 X, addition( Y, Z ) ) ), ! leq( T, multiplication( X, Z ) ) }.
% 64.00/64.41 parent0: (88195) {G1,W12,D4,L2,V4,M2} { leq( X, multiplication( Y,
% 64.00/64.41 addition( Z, T ) ) ), ! leq( X, multiplication( Y, T ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := T
% 64.00/64.41 Y := X
% 64.00/64.41 Z := Y
% 64.00/64.41 T := Z
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 1 ==> 1
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 resolution: (88196) {G1,W7,D4,L1,V1,M1} { leq( multiplication( star( X ),
% 64.00/64.41 X ), star( X ) ) }.
% 64.00/64.41 parent0[1]: (513) {G5,W8,D3,L2,V3,M2} P(11,251) { leq( Y, Z ), ! leq(
% 64.00/64.41 addition( X, Y ), Z ) }.
% 64.00/64.41 parent1[0]: (14) {G0,W9,D5,L1,V1,M1} I { leq( addition( one, multiplication
% 64.00/64.41 ( star( X ), X ) ), star( X ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := one
% 64.00/64.41 Y := multiplication( star( X ), X )
% 64.00/64.41 Z := star( X )
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (880) {G6,W7,D4,L1,V1,M1} R(513,14) { leq( multiplication(
% 64.00/64.41 star( X ), X ), star( X ) ) }.
% 64.00/64.41 parent0: (88196) {G1,W7,D4,L1,V1,M1} { leq( multiplication( star( X ), X )
% 64.00/64.41 , star( X ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 resolution: (88197) {G1,W7,D4,L1,V1,M1} { leq( multiplication( X, star( X
% 64.00/64.41 ) ), star( X ) ) }.
% 64.00/64.41 parent0[1]: (513) {G5,W8,D3,L2,V3,M2} P(11,251) { leq( Y, Z ), ! leq(
% 64.00/64.41 addition( X, Y ), Z ) }.
% 64.00/64.41 parent1[0]: (13) {G0,W9,D5,L1,V1,M1} I { leq( addition( one, multiplication
% 64.00/64.41 ( X, star( X ) ) ), star( X ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := one
% 64.00/64.41 Y := multiplication( X, star( X ) )
% 64.00/64.41 Z := star( X )
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (881) {G6,W7,D4,L1,V1,M1} R(513,13) { leq( multiplication( X,
% 64.00/64.41 star( X ) ), star( X ) ) }.
% 64.00/64.41 parent0: (88197) {G1,W7,D4,L1,V1,M1} { leq( multiplication( X, star( X ) )
% 64.00/64.41 , star( X ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88199) {G1,W12,D4,L2,V4,M2} { ! leq( multiplication( X, addition
% 64.00/64.41 ( Y, Z ) ), T ), leq( multiplication( X, Z ), T ) }.
% 64.00/64.41 parent0[0]: (7) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Y ),
% 64.00/64.41 multiplication( X, Z ) ) ==> multiplication( X, addition( Y, Z ) ) }.
% 64.00/64.41 parent1[1; 2]: (513) {G5,W8,D3,L2,V3,M2} P(11,251) { leq( Y, Z ), ! leq(
% 64.00/64.41 addition( X, Y ), Z ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := multiplication( X, Y )
% 64.00/64.41 Y := multiplication( X, Z )
% 64.00/64.41 Z := T
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (885) {G6,W12,D4,L2,V4,M2} P(7,513) { leq( multiplication( X,
% 64.00/64.41 Z ), T ), ! leq( multiplication( X, addition( Y, Z ) ), T ) }.
% 64.00/64.41 parent0: (88199) {G1,W12,D4,L2,V4,M2} { ! leq( multiplication( X, addition
% 64.00/64.41 ( Y, Z ) ), T ), leq( multiplication( X, Z ), T ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 T := T
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 1
% 64.00/64.41 1 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88201) {G1,W16,D4,L2,V3,M2} { ! multiplication( X, Z ) ==>
% 64.00/64.41 multiplication( X, addition( Y, Z ) ), leq( multiplication( X, Y ),
% 64.00/64.41 multiplication( X, Z ) ) }.
% 64.00/64.41 parent0[0]: (63) {G1,W16,D4,L2,V3,M2} P(7,12) { ! multiplication( X,
% 64.00/64.41 addition( Y, Z ) ) ==> multiplication( X, Z ), leq( multiplication( X, Y
% 64.00/64.41 ), multiplication( X, Z ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88203) {G2,W17,D4,L2,V2,M2} { ! multiplication( X, star( Y ) )
% 64.00/64.41 ==> multiplication( X, star( Y ) ), leq( multiplication( X, one ),
% 64.00/64.41 multiplication( X, star( Y ) ) ) }.
% 64.00/64.41 parent0[0]: (736) {G6,W7,D4,L1,V1,M1} R(719,11) { addition( one, star( X )
% 64.00/64.41 ) ==> star( X ) }.
% 64.00/64.41 parent1[0; 8]: (88201) {G1,W16,D4,L2,V3,M2} { ! multiplication( X, Z ) ==>
% 64.00/64.41 multiplication( X, addition( Y, Z ) ), leq( multiplication( X, Y ),
% 64.00/64.41 multiplication( X, Z ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := one
% 64.00/64.41 Z := star( Y )
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqrefl: (88204) {G0,W8,D4,L1,V2,M1} { leq( multiplication( X, one ),
% 64.00/64.41 multiplication( X, star( Y ) ) ) }.
% 64.00/64.41 parent0[0]: (88203) {G2,W17,D4,L2,V2,M2} { ! multiplication( X, star( Y )
% 64.00/64.41 ) ==> multiplication( X, star( Y ) ), leq( multiplication( X, one ),
% 64.00/64.41 multiplication( X, star( Y ) ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88205) {G1,W6,D4,L1,V2,M1} { leq( X, multiplication( X, star( Y
% 64.00/64.41 ) ) ) }.
% 64.00/64.41 parent0[0]: (5) {G0,W5,D3,L1,V1,M1} I { multiplication( X, one ) ==> X }.
% 64.00/64.41 parent1[0; 1]: (88204) {G0,W8,D4,L1,V2,M1} { leq( multiplication( X, one )
% 64.00/64.41 , multiplication( X, star( Y ) ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (1592) {G7,W6,D4,L1,V2,M1} P(736,63);q;d(5) { leq( Y,
% 64.00/64.41 multiplication( Y, star( X ) ) ) }.
% 64.00/64.41 parent0: (88205) {G1,W6,D4,L1,V2,M1} { leq( X, multiplication( X, star( Y
% 64.00/64.41 ) ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88207) {G1,W16,D4,L2,V3,M2} { ! multiplication( X, Z ) ==>
% 64.00/64.41 multiplication( X, addition( Y, Z ) ), leq( multiplication( X, Y ),
% 64.00/64.41 multiplication( X, Z ) ) }.
% 64.00/64.41 parent0[0]: (63) {G1,W16,D4,L2,V3,M2} P(7,12) { ! multiplication( X,
% 64.00/64.41 addition( Y, Z ) ) ==> multiplication( X, Z ), leq( multiplication( X, Y
% 64.00/64.41 ), multiplication( X, Z ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88208) {G1,W17,D3,L3,V3,M3} { ! multiplication( X, Y ) ==>
% 64.00/64.41 multiplication( X, Y ), ! leq( Z, Y ), leq( multiplication( X, Z ),
% 64.00/64.41 multiplication( X, Y ) ) }.
% 64.00/64.41 parent0[1]: (11) {G0,W8,D3,L2,V2,M2} I { ! leq( X, Y ), addition( X, Y )
% 64.00/64.41 ==> Y }.
% 64.00/64.41 parent1[0; 7]: (88207) {G1,W16,D4,L2,V3,M2} { ! multiplication( X, Z ) ==>
% 64.00/64.41 multiplication( X, addition( Y, Z ) ), leq( multiplication( X, Y ),
% 64.00/64.41 multiplication( X, Z ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Z
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Z
% 64.00/64.41 Z := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqrefl: (88209) {G0,W10,D3,L2,V3,M2} { ! leq( Z, Y ), leq( multiplication
% 64.00/64.41 ( X, Z ), multiplication( X, Y ) ) }.
% 64.00/64.41 parent0[0]: (88208) {G1,W17,D3,L3,V3,M3} { ! multiplication( X, Y ) ==>
% 64.00/64.41 multiplication( X, Y ), ! leq( Z, Y ), leq( multiplication( X, Z ),
% 64.00/64.41 multiplication( X, Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (1595) {G2,W10,D3,L2,V3,M2} P(11,63);q { leq( multiplication(
% 64.00/64.41 Z, X ), multiplication( Z, Y ) ), ! leq( X, Y ) }.
% 64.00/64.41 parent0: (88209) {G0,W10,D3,L2,V3,M2} { ! leq( Z, Y ), leq( multiplication
% 64.00/64.41 ( X, Z ), multiplication( X, Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Z
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 1
% 64.00/64.41 1 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88211) {G2,W7,D4,L1,V2,M1} { leq( X, multiplication( X, addition
% 64.00/64.41 ( one, Y ) ) ) }.
% 64.00/64.41 parent0[0]: (65) {G1,W11,D4,L1,V2,M1} P(5,7) { addition( X, multiplication
% 64.00/64.41 ( X, Y ) ) = multiplication( X, addition( one, Y ) ) }.
% 64.00/64.41 parent1[0; 2]: (232) {G2,W5,D3,L1,V2,M1} P(3,23);q { leq( X, addition( X, Y
% 64.00/64.41 ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := multiplication( X, Y )
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (1751) {G3,W7,D4,L1,V2,M1} P(65,232) { leq( X, multiplication
% 64.00/64.41 ( X, addition( one, Y ) ) ) }.
% 64.00/64.41 parent0: (88211) {G2,W7,D4,L1,V2,M1} { leq( X, multiplication( X, addition
% 64.00/64.41 ( one, Y ) ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88212) {G2,W7,D4,L1,V2,M1} { leq( X, multiplication( X, addition
% 64.00/64.41 ( Y, one ) ) ) }.
% 64.00/64.41 parent0[0]: (64) {G1,W11,D4,L1,V3,M1} P(7,0);d(7) { multiplication( X,
% 64.00/64.41 addition( Y, Z ) ) = multiplication( X, addition( Z, Y ) ) }.
% 64.00/64.41 parent1[0; 2]: (1751) {G3,W7,D4,L1,V2,M1} P(65,232) { leq( X,
% 64.00/64.41 multiplication( X, addition( one, Y ) ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := one
% 64.00/64.41 Z := Y
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (1764) {G4,W7,D4,L1,V2,M1} P(64,1751) { leq( X, multiplication
% 64.00/64.41 ( X, addition( Y, one ) ) ) }.
% 64.00/64.41 parent0: (88212) {G2,W7,D4,L1,V2,M1} { leq( X, multiplication( X, addition
% 64.00/64.41 ( Y, one ) ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88215) {G1,W16,D4,L2,V3,M2} { ! multiplication( Y, Z ) ==>
% 64.00/64.41 multiplication( addition( X, Y ), Z ), leq( multiplication( X, Z ),
% 64.00/64.41 multiplication( Y, Z ) ) }.
% 64.00/64.41 parent0[0]: (94) {G1,W16,D4,L2,V3,M2} P(8,12) { ! multiplication( addition
% 64.00/64.41 ( X, Z ), Y ) ==> multiplication( Z, Y ), leq( multiplication( X, Y ),
% 64.00/64.41 multiplication( Z, Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Z
% 64.00/64.41 Z := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88217) {G2,W17,D4,L2,V2,M2} { ! multiplication( star( X ), Y )
% 64.00/64.41 ==> multiplication( star( X ), Y ), leq( multiplication( one, Y ),
% 64.00/64.41 multiplication( star( X ), Y ) ) }.
% 64.00/64.41 parent0[0]: (736) {G6,W7,D4,L1,V1,M1} R(719,11) { addition( one, star( X )
% 64.00/64.41 ) ==> star( X ) }.
% 64.00/64.41 parent1[0; 7]: (88215) {G1,W16,D4,L2,V3,M2} { ! multiplication( Y, Z ) ==>
% 64.00/64.41 multiplication( addition( X, Y ), Z ), leq( multiplication( X, Z ),
% 64.00/64.41 multiplication( Y, Z ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := one
% 64.00/64.41 Y := star( X )
% 64.00/64.41 Z := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqrefl: (88218) {G0,W8,D4,L1,V2,M1} { leq( multiplication( one, Y ),
% 64.00/64.41 multiplication( star( X ), Y ) ) }.
% 64.00/64.41 parent0[0]: (88217) {G2,W17,D4,L2,V2,M2} { ! multiplication( star( X ), Y
% 64.00/64.41 ) ==> multiplication( star( X ), Y ), leq( multiplication( one, Y ),
% 64.00/64.41 multiplication( star( X ), Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88219) {G1,W6,D4,L1,V2,M1} { leq( X, multiplication( star( Y ),
% 64.00/64.41 X ) ) }.
% 64.00/64.41 parent0[0]: (6) {G0,W5,D3,L1,V1,M1} I { multiplication( one, X ) ==> X }.
% 64.00/64.41 parent1[0; 1]: (88218) {G0,W8,D4,L1,V2,M1} { leq( multiplication( one, Y )
% 64.00/64.41 , multiplication( star( X ), Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (2878) {G7,W6,D4,L1,V2,M1} P(736,94);q;d(6) { leq( Y,
% 64.00/64.41 multiplication( star( X ), Y ) ) }.
% 64.00/64.41 parent0: (88219) {G1,W6,D4,L1,V2,M1} { leq( X, multiplication( star( Y ),
% 64.00/64.41 X ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88221) {G1,W16,D4,L2,V3,M2} { ! multiplication( Y, Z ) ==>
% 64.00/64.41 multiplication( addition( X, Y ), Z ), leq( multiplication( X, Z ),
% 64.00/64.41 multiplication( Y, Z ) ) }.
% 64.00/64.41 parent0[0]: (94) {G1,W16,D4,L2,V3,M2} P(8,12) { ! multiplication( addition
% 64.00/64.41 ( X, Z ), Y ) ==> multiplication( Z, Y ), leq( multiplication( X, Y ),
% 64.00/64.41 multiplication( Z, Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Z
% 64.00/64.41 Z := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88222) {G1,W17,D3,L3,V3,M3} { ! multiplication( X, Y ) ==>
% 64.00/64.41 multiplication( X, Y ), ! leq( Z, X ), leq( multiplication( Z, Y ),
% 64.00/64.41 multiplication( X, Y ) ) }.
% 64.00/64.41 parent0[1]: (11) {G0,W8,D3,L2,V2,M2} I { ! leq( X, Y ), addition( X, Y )
% 64.00/64.41 ==> Y }.
% 64.00/64.41 parent1[0; 6]: (88221) {G1,W16,D4,L2,V3,M2} { ! multiplication( Y, Z ) ==>
% 64.00/64.41 multiplication( addition( X, Y ), Z ), leq( multiplication( X, Z ),
% 64.00/64.41 multiplication( Y, Z ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Z
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := Z
% 64.00/64.41 Y := X
% 64.00/64.41 Z := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqrefl: (88223) {G0,W10,D3,L2,V3,M2} { ! leq( Z, X ), leq( multiplication
% 64.00/64.41 ( Z, Y ), multiplication( X, Y ) ) }.
% 64.00/64.41 parent0[0]: (88222) {G1,W17,D3,L3,V3,M3} { ! multiplication( X, Y ) ==>
% 64.00/64.41 multiplication( X, Y ), ! leq( Z, X ), leq( multiplication( Z, Y ),
% 64.00/64.41 multiplication( X, Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (2881) {G2,W10,D3,L2,V3,M2} P(11,94);q { leq( multiplication(
% 64.00/64.41 X, Z ), multiplication( Y, Z ) ), ! leq( X, Y ) }.
% 64.00/64.41 parent0: (88223) {G0,W10,D3,L2,V3,M2} { ! leq( Z, X ), leq( multiplication
% 64.00/64.41 ( Z, Y ), multiplication( X, Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := Z
% 64.00/64.41 Z := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 1
% 64.00/64.41 1 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 resolution: (88224) {G3,W8,D5,L1,V3,M1} { leq( X, addition( multiplication
% 64.00/64.41 ( star( Y ), X ), Z ) ) }.
% 64.00/64.41 parent0[1]: (228) {G2,W8,D3,L2,V3,M2} P(11,23);q { leq( X, addition( Y, Z )
% 64.00/64.41 ), ! leq( X, Y ) }.
% 64.00/64.41 parent1[0]: (2878) {G7,W6,D4,L1,V2,M1} P(736,94);q;d(6) { leq( Y,
% 64.00/64.41 multiplication( star( X ), Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := multiplication( star( Y ), X )
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (2886) {G8,W8,D5,L1,V3,M1} R(2878,228) { leq( X, addition(
% 64.00/64.41 multiplication( star( Y ), X ), Z ) ) }.
% 64.00/64.41 parent0: (88224) {G3,W8,D5,L1,V3,M1} { leq( X, addition( multiplication(
% 64.00/64.41 star( Y ), X ), Z ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88226) {G1,W9,D4,L2,V3,M2} { leq( X, Z ), ! leq( multiplication
% 64.00/64.41 ( star( Y ), X ), Z ) }.
% 64.00/64.41 parent0[1]: (11) {G0,W8,D3,L2,V2,M2} I { ! leq( X, Y ), addition( X, Y )
% 64.00/64.41 ==> Y }.
% 64.00/64.41 parent1[0; 2]: (2886) {G8,W8,D5,L1,V3,M1} R(2878,228) { leq( X, addition(
% 64.00/64.41 multiplication( star( Y ), X ), Z ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := multiplication( star( Y ), X )
% 64.00/64.41 Y := Z
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (3030) {G9,W9,D4,L2,V3,M2} P(11,2886) { leq( Y, Z ), ! leq(
% 64.00/64.41 multiplication( star( X ), Y ), Z ) }.
% 64.00/64.41 parent0: (88226) {G1,W9,D4,L2,V3,M2} { leq( X, Z ), ! leq( multiplication
% 64.00/64.41 ( star( Y ), X ), Z ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := X
% 64.00/64.41 Z := Z
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 1 ==> 1
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88229) {G7,W8,D4,L1,V2,M1} { leq( addition( X, one ), addition(
% 64.00/64.41 star( Y ), X ) ) }.
% 64.00/64.41 parent0[0]: (733) {G6,W7,D4,L1,V1,M1} R(719,35) { addition( star( X ), one
% 64.00/64.41 ) ==> star( X ) }.
% 64.00/64.41 parent1[0; 5]: (792) {G7,W9,D4,L1,V3,M1} R(503,732);d(1) { leq( addition( X
% 64.00/64.41 , Y ), addition( addition( Z, Y ), X ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := one
% 64.00/64.41 Z := star( Y )
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (7357) {G8,W8,D4,L1,V2,M1} P(733,792) { leq( addition( Y, one
% 64.00/64.41 ), addition( star( X ), Y ) ) }.
% 64.00/64.41 parent0: (88229) {G7,W8,D4,L1,V2,M1} { leq( addition( X, one ), addition(
% 64.00/64.41 star( Y ), X ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 resolution: (88230) {G7,W4,D3,L1,V1,M1} { leq( X, star( X ) ) }.
% 64.00/64.41 parent0[1]: (3030) {G9,W9,D4,L2,V3,M2} P(11,2886) { leq( Y, Z ), ! leq(
% 64.00/64.41 multiplication( star( X ), Y ), Z ) }.
% 64.00/64.41 parent1[0]: (880) {G6,W7,D4,L1,V1,M1} R(513,14) { leq( multiplication( star
% 64.00/64.41 ( X ), X ), star( X ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := X
% 64.00/64.41 Z := star( X )
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (8643) {G10,W4,D3,L1,V1,M1} R(3030,880) { leq( X, star( X ) )
% 64.00/64.41 }.
% 64.00/64.41 parent0: (88230) {G7,W4,D3,L1,V1,M1} { leq( X, star( X ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 resolution: (88232) {G3,W8,D3,L2,V1,M2} { ! leq( star( X ), X ), star( X )
% 64.00/64.41 = X }.
% 64.00/64.41 parent0[2]: (479) {G2,W9,D2,L3,V2,M3} P(35,11) { ! leq( X, Y ), X = Y, !
% 64.00/64.41 leq( Y, X ) }.
% 64.00/64.41 parent1[0]: (8643) {G10,W4,D3,L1,V1,M1} R(3030,880) { leq( X, star( X ) )
% 64.00/64.41 }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := star( X )
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (8657) {G11,W8,D3,L2,V1,M2} R(8643,479) { star( X ) ==> X, !
% 64.00/64.41 leq( star( X ), X ) }.
% 64.00/64.41 parent0: (88232) {G3,W8,D3,L2,V1,M2} { ! leq( star( X ), X ), star( X ) =
% 64.00/64.41 X }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 1
% 64.00/64.41 1 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 resolution: (88233) {G6,W7,D3,L2,V2,M2} { leq( X, star( Y ) ), ! leq( X, Y
% 64.00/64.41 ) }.
% 64.00/64.41 parent0[1]: (731) {G5,W9,D2,L3,V3,M3} P(11,526) { leq( X, Z ), ! leq( Y, Z
% 64.00/64.41 ), ! leq( X, Y ) }.
% 64.00/64.41 parent1[0]: (8643) {G10,W4,D3,L1,V1,M1} R(3030,880) { leq( X, star( X ) )
% 64.00/64.41 }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := star( Y )
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (8658) {G11,W7,D3,L2,V2,M2} R(8643,731) { leq( X, star( Y ) )
% 64.00/64.41 , ! leq( X, Y ) }.
% 64.00/64.41 parent0: (88233) {G6,W7,D3,L2,V2,M2} { leq( X, star( Y ) ), ! leq( X, Y )
% 64.00/64.41 }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 1 ==> 1
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 resolution: (88236) {G6,W7,D3,L2,V2,M2} { leq( X, Y ), ! leq( star( X ), Y
% 64.00/64.41 ) }.
% 64.00/64.41 parent0[2]: (731) {G5,W9,D2,L3,V3,M3} P(11,526) { leq( X, Z ), ! leq( Y, Z
% 64.00/64.41 ), ! leq( X, Y ) }.
% 64.00/64.41 parent1[0]: (8643) {G10,W4,D3,L1,V1,M1} R(3030,880) { leq( X, star( X ) )
% 64.00/64.41 }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := star( X )
% 64.00/64.41 Z := Y
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (8659) {G11,W7,D3,L2,V2,M2} R(8643,731) { leq( X, Y ), ! leq(
% 64.00/64.41 star( X ), Y ) }.
% 64.00/64.41 parent0: (88236) {G6,W7,D3,L2,V2,M2} { leq( X, Y ), ! leq( star( X ), Y )
% 64.00/64.41 }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 1 ==> 1
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88237) {G1,W8,D3,L2,V2,M2} { X ==> addition( X, Y ), ! leq( Y, X
% 64.00/64.41 ) }.
% 64.00/64.41 parent0[0]: (35) {G1,W8,D3,L2,V2,M2} P(11,0) { addition( Y, X ) ==> Y, !
% 64.00/64.41 leq( X, Y ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Y
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 resolution: (88238) {G2,W7,D4,L1,V1,M1} { star( X ) ==> addition( star( X
% 64.00/64.41 ), X ) }.
% 64.00/64.41 parent0[1]: (88237) {G1,W8,D3,L2,V2,M2} { X ==> addition( X, Y ), ! leq( Y
% 64.00/64.41 , X ) }.
% 64.00/64.41 parent1[0]: (8643) {G10,W4,D3,L1,V1,M1} R(3030,880) { leq( X, star( X ) )
% 64.00/64.41 }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := star( X )
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88239) {G2,W7,D4,L1,V1,M1} { addition( star( X ), X ) ==> star( X
% 64.00/64.41 ) }.
% 64.00/64.41 parent0[0]: (88238) {G2,W7,D4,L1,V1,M1} { star( X ) ==> addition( star( X
% 64.00/64.41 ), X ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (8662) {G11,W7,D4,L1,V1,M1} R(8643,35) { addition( star( X ),
% 64.00/64.41 X ) ==> star( X ) }.
% 64.00/64.41 parent0: (88239) {G2,W7,D4,L1,V1,M1} { addition( star( X ), X ) ==> star(
% 64.00/64.41 X ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88240) {G0,W8,D3,L2,V2,M2} { Y ==> addition( X, Y ), ! leq( X, Y
% 64.00/64.41 ) }.
% 64.00/64.41 parent0[1]: (11) {G0,W8,D3,L2,V2,M2} I { ! leq( X, Y ), addition( X, Y )
% 64.00/64.41 ==> Y }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 resolution: (88241) {G1,W7,D4,L1,V1,M1} { star( X ) ==> addition( X, star
% 64.00/64.41 ( X ) ) }.
% 64.00/64.41 parent0[1]: (88240) {G0,W8,D3,L2,V2,M2} { Y ==> addition( X, Y ), ! leq( X
% 64.00/64.41 , Y ) }.
% 64.00/64.41 parent1[0]: (8643) {G10,W4,D3,L1,V1,M1} R(3030,880) { leq( X, star( X ) )
% 64.00/64.41 }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := star( X )
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88242) {G1,W7,D4,L1,V1,M1} { addition( X, star( X ) ) ==> star( X
% 64.00/64.41 ) }.
% 64.00/64.41 parent0[0]: (88241) {G1,W7,D4,L1,V1,M1} { star( X ) ==> addition( X, star
% 64.00/64.41 ( X ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (8665) {G11,W7,D4,L1,V1,M1} R(8643,11) { addition( X, star( X
% 64.00/64.41 ) ) ==> star( X ) }.
% 64.00/64.41 parent0: (88242) {G1,W7,D4,L1,V1,M1} { addition( X, star( X ) ) ==> star(
% 64.00/64.41 X ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 resolution: (88243) {G6,W10,D3,L3,V3,M3} { leq( X, star( Y ) ), ! leq( Z,
% 64.00/64.41 Y ), ! leq( X, Z ) }.
% 64.00/64.41 parent0[1]: (8658) {G11,W7,D3,L2,V2,M2} R(8643,731) { leq( X, star( Y ) ),
% 64.00/64.41 ! leq( X, Y ) }.
% 64.00/64.41 parent1[0]: (731) {G5,W9,D2,L3,V3,M3} P(11,526) { leq( X, Z ), ! leq( Y, Z
% 64.00/64.41 ), ! leq( X, Y ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Z
% 64.00/64.41 Z := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (8809) {G12,W10,D3,L3,V3,M3} R(8658,731) { ! leq( X, Y ), leq
% 64.00/64.41 ( Z, star( Y ) ), ! leq( Z, X ) }.
% 64.00/64.41 parent0: (88243) {G6,W10,D3,L3,V3,M3} { leq( X, star( Y ) ), ! leq( Z, Y )
% 64.00/64.41 , ! leq( X, Z ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := Z
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 1
% 64.00/64.41 1 ==> 0
% 64.00/64.41 2 ==> 2
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 resolution: (88245) {G3,W10,D3,L3,V2,M3} { X = Y, ! leq( Y, X ), ! leq(
% 64.00/64.41 star( X ), Y ) }.
% 64.00/64.41 parent0[0]: (479) {G2,W9,D2,L3,V2,M3} P(35,11) { ! leq( X, Y ), X = Y, !
% 64.00/64.41 leq( Y, X ) }.
% 64.00/64.41 parent1[0]: (8659) {G11,W7,D3,L2,V2,M2} R(8643,731) { leq( X, Y ), ! leq(
% 64.00/64.41 star( X ), Y ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (8911) {G12,W10,D3,L3,V2,M3} R(8659,479) { ! leq( star( X ), Y
% 64.00/64.41 ), X = Y, ! leq( Y, X ) }.
% 64.00/64.41 parent0: (88245) {G3,W10,D3,L3,V2,M3} { X = Y, ! leq( Y, X ), ! leq( star
% 64.00/64.41 ( X ), Y ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 1
% 64.00/64.41 1 ==> 2
% 64.00/64.41 2 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88248) {G5,W8,D4,L1,V2,M1} { leq( multiplication( X, Y ),
% 64.00/64.41 multiplication( star( X ), Y ) ) }.
% 64.00/64.41 parent0[0]: (8662) {G11,W7,D4,L1,V1,M1} R(8643,35) { addition( star( X ), X
% 64.00/64.41 ) ==> star( X ) }.
% 64.00/64.41 parent1[0; 5]: (242) {G4,W9,D4,L1,V3,M1} P(8,240) { leq( multiplication( Z
% 64.00/64.41 , Y ), multiplication( addition( X, Z ), Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := star( X )
% 64.00/64.41 Y := Y
% 64.00/64.41 Z := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (8974) {G12,W8,D4,L1,V2,M1} P(8662,242) { leq( multiplication
% 64.00/64.41 ( X, Y ), multiplication( star( X ), Y ) ) }.
% 64.00/64.41 parent0: (88248) {G5,W8,D4,L1,V2,M1} { leq( multiplication( X, Y ),
% 64.00/64.41 multiplication( star( X ), Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88251) {G9,W6,D3,L1,V1,M1} { leq( addition( X, one ), star( X )
% 64.00/64.41 ) }.
% 64.00/64.41 parent0[0]: (8662) {G11,W7,D4,L1,V1,M1} R(8643,35) { addition( star( X ), X
% 64.00/64.41 ) ==> star( X ) }.
% 64.00/64.41 parent1[0; 4]: (7357) {G8,W8,D4,L1,V2,M1} P(733,792) { leq( addition( Y,
% 64.00/64.41 one ), addition( star( X ), Y ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (8976) {G12,W6,D3,L1,V1,M1} P(8662,7357) { leq( addition( X,
% 64.00/64.41 one ), star( X ) ) }.
% 64.00/64.41 parent0: (88251) {G9,W6,D3,L1,V1,M1} { leq( addition( X, one ), star( X )
% 64.00/64.41 ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88252) {G2,W10,D3,L2,V2,M2} { Y ==> addition( X, Y ), ! addition
% 64.00/64.41 ( Y, X ) ==> Y }.
% 64.00/64.41 parent0[0]: (29) {G2,W10,D3,L2,V2,M2} R(11,22) { addition( X, Y ) ==> Y, !
% 64.00/64.41 addition( Y, X ) ==> Y }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := Y
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88257) {G3,W10,D4,L2,V1,M2} { X ==> star( X ), ! addition( X,
% 64.00/64.41 star( X ) ) ==> X }.
% 64.00/64.41 parent0[0]: (8662) {G11,W7,D4,L1,V1,M1} R(8643,35) { addition( star( X ), X
% 64.00/64.41 ) ==> star( X ) }.
% 64.00/64.41 parent1[0; 2]: (88252) {G2,W10,D3,L2,V2,M2} { Y ==> addition( X, Y ), !
% 64.00/64.41 addition( Y, X ) ==> Y }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := star( X )
% 64.00/64.41 Y := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88260) {G4,W8,D3,L2,V1,M2} { ! star( X ) ==> X, X ==> star( X )
% 64.00/64.41 }.
% 64.00/64.41 parent0[0]: (8665) {G11,W7,D4,L1,V1,M1} R(8643,11) { addition( X, star( X )
% 64.00/64.41 ) ==> star( X ) }.
% 64.00/64.41 parent1[1; 2]: (88257) {G3,W10,D4,L2,V1,M2} { X ==> star( X ), ! addition
% 64.00/64.41 ( X, star( X ) ) ==> X }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 eqswap: (88262) {G4,W8,D3,L2,V1,M2} { star( X ) ==> X, ! star( X ) ==> X
% 64.00/64.41 }.
% 64.00/64.41 parent0[1]: (88260) {G4,W8,D3,L2,V1,M2} { ! star( X ) ==> X, X ==> star( X
% 64.00/64.41 ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (8982) {G12,W8,D3,L2,V1,M2} P(29,8662);d(8665) { star( X ) ==>
% 64.00/64.41 X, ! star( X ) ==> X }.
% 64.00/64.41 parent0: (88262) {G4,W8,D3,L2,V1,M2} { star( X ) ==> X, ! star( X ) ==> X
% 64.00/64.41 }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 1 ==> 1
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 resolution: (88265) {G2,W13,D4,L2,V1,M2} { ! leq( star( X ), star( X ) ),
% 64.00/64.41 leq( multiplication( star( X ), star( X ) ), star( X ) ) }.
% 64.00/64.41 parent0[2]: (162) {G1,W14,D4,L3,V3,M3} P(11,15) { ! leq( Z, Y ), leq(
% 64.00/64.41 multiplication( star( X ), Z ), Y ), ! leq( multiplication( X, Y ), Z )
% 64.00/64.41 }.
% 64.00/64.41 parent1[0]: (881) {G6,W7,D4,L1,V1,M1} R(513,13) { leq( multiplication( X,
% 64.00/64.41 star( X ) ), star( X ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 Y := star( X )
% 64.00/64.41 Z := star( X )
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 resolution: (88266) {G2,W8,D4,L1,V1,M1} { leq( multiplication( star( X ),
% 64.00/64.41 star( X ) ), star( X ) ) }.
% 64.00/64.41 parent0[0]: (88265) {G2,W13,D4,L2,V1,M2} { ! leq( star( X ), star( X ) ),
% 64.00/64.41 leq( multiplication( star( X ), star( X ) ), star( X ) ) }.
% 64.00/64.41 parent1[0]: (20) {G1,W3,D2,L1,V1,M1} R(12,3) { leq( X, X ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := star( X )
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (9463) {G7,W8,D4,L1,V1,M1} R(162,881);r(20) { leq(
% 64.00/64.41 multiplication( star( X ), star( X ) ), star( X ) ) }.
% 64.00/64.41 parent0: (88266) {G2,W8,D4,L1,V1,M1} { leq( multiplication( star( X ),
% 64.00/64.41 star( X ) ), star( X ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 resolution: (88267) {G3,W16,D4,L2,V1,M2} { multiplication( star( X ), star
% 64.00/64.41 ( X ) ) = star( X ), ! leq( star( X ), multiplication( star( X ), star( X
% 64.00/64.41 ) ) ) }.
% 64.00/64.41 parent0[0]: (479) {G2,W9,D2,L3,V2,M3} P(35,11) { ! leq( X, Y ), X = Y, !
% 64.00/64.41 leq( Y, X ) }.
% 64.00/64.41 parent1[0]: (9463) {G7,W8,D4,L1,V1,M1} R(162,881);r(20) { leq(
% 64.00/64.41 multiplication( star( X ), star( X ) ), star( X ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := multiplication( star( X ), star( X ) )
% 64.00/64.41 Y := star( X )
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 resolution: (88269) {G4,W8,D4,L1,V1,M1} { multiplication( star( X ), star
% 64.00/64.41 ( X ) ) = star( X ) }.
% 64.00/64.41 parent0[1]: (88267) {G3,W16,D4,L2,V1,M2} { multiplication( star( X ), star
% 64.00/64.41 ( X ) ) = star( X ), ! leq( star( X ), multiplication( star( X ), star( X
% 64.00/64.41 ) ) ) }.
% 64.00/64.41 parent1[0]: (1592) {G7,W6,D4,L1,V2,M1} P(736,63);q;d(5) { leq( Y,
% 64.00/64.41 multiplication( Y, star( X ) ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 Y := star( X )
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (10042) {G8,W8,D4,L1,V1,M1} R(9463,479);r(1592) {
% 64.00/64.41 multiplication( star( X ), star( X ) ) ==> star( X ) }.
% 64.00/64.41 parent0: (88269) {G4,W8,D4,L1,V1,M1} { multiplication( star( X ), star( X
% 64.00/64.41 ) ) = star( X ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88273) {G2,W13,D4,L2,V1,M2} { ! leq( addition( star( X ), one )
% 64.00/64.41 , star( X ) ), leq( star( star( X ) ), star( X ) ) }.
% 64.00/64.41 parent0[0]: (10042) {G8,W8,D4,L1,V1,M1} R(9463,479);r(1592) {
% 64.00/64.41 multiplication( star( X ), star( X ) ) ==> star( X ) }.
% 64.00/64.41 parent1[0; 3]: (167) {G1,W11,D4,L2,V2,M2} P(5,15) { ! leq( addition(
% 64.00/64.41 multiplication( X, Y ), one ), Y ), leq( star( X ), Y ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := star( X )
% 64.00/64.41 Y := star( X )
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 paramod: (88274) {G3,W11,D4,L2,V1,M2} { ! leq( star( X ), star( X ) ), leq
% 64.00/64.41 ( star( star( X ) ), star( X ) ) }.
% 64.00/64.41 parent0[0]: (733) {G6,W7,D4,L1,V1,M1} R(719,35) { addition( star( X ), one
% 64.00/64.41 ) ==> star( X ) }.
% 64.00/64.41 parent1[0; 2]: (88273) {G2,W13,D4,L2,V1,M2} { ! leq( addition( star( X ),
% 64.00/64.41 one ), star( X ) ), leq( star( star( X ) ), star( X ) ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 resolution: (88275) {G2,W6,D4,L1,V1,M1} { leq( star( star( X ) ), star( X
% 64.00/64.41 ) ) }.
% 64.00/64.41 parent0[0]: (88274) {G3,W11,D4,L2,V1,M2} { ! leq( star( X ), star( X ) ),
% 64.00/64.41 leq( star( star( X ) ), star( X ) ) }.
% 64.00/64.41 parent1[0]: (20) {G1,W3,D2,L1,V1,M1} R(12,3) { leq( X, X ) }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 substitution1:
% 64.00/64.41 X := star( X )
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41 subsumption: (10046) {G9,W6,D4,L1,V1,M1} P(10042,167);d(733);r(20) { leq(
% 64.00/64.41 star( star( X ) ), star( X ) ) }.
% 64.00/64.41 parent0: (88275) {G2,W6,D4,L1,V1,M1} { leq( star( star( X ) ), star( X ) )
% 64.00/64.41 }.
% 64.00/64.41 substitution0:
% 64.00/64.41 X := X
% 64.00/64.41 end
% 64.00/64.41 permutation0:
% 64.00/64.41 0 ==> 0
% 64.00/64.41 end
% 64.00/64.41
% 64.00/64.41
% 64.00/64.41 ==> (10049) {G13,W9,D3,L2,V1,M2} P(8982,10042) { multiplication( X, X ) ==>
% 64.00/64.41 X, ! star( X ) ==> X }.
% 64.00/64.41
% 64.00/64.41
% 64.00/64.41
% 64.00/64.41 !!! Internal Problem: OH, OH, COULD NOT DERIVE GOAL !!!
% 64.00/64.41
% 64.00/64.41 Bliksem ended
%------------------------------------------------------------------------------