%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : KLE011+4 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n003.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:36:36 EDT 2022
% Result : Theorem 5.62s 6.02s
% Output : Refutation 5.62s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.15 % Problem : KLE011+4 : TPTP v8.1.0. Released v4.0.0.
% 0.08/0.16 % Command : bliksem %s
% 0.16/0.37 % Computer : n003.cluster.edu
% 0.16/0.37 % Model : x86_64 x86_64
% 0.16/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.37 % Memory : 8042.1875MB
% 0.16/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.37 % CPULimit : 300
% 0.16/0.37 % DateTime : Thu Jun 16 10:52:11 EDT 2022
% 0.16/0.38 % CPUTime :
% 5.62/6.02 *** allocated 10000 integers for termspace/termends
% 5.62/6.02 *** allocated 10000 integers for clauses
% 5.62/6.02 *** allocated 10000 integers for justifications
% 5.62/6.02 Bliksem 1.12
% 5.62/6.02
% 5.62/6.02
% 5.62/6.02 Automatic Strategy Selection
% 5.62/6.02
% 5.62/6.02
% 5.62/6.02 Clauses:
% 5.62/6.02
% 5.62/6.02 { addition( X, Y ) = addition( Y, X ) }.
% 5.62/6.02 { addition( Z, addition( Y, X ) ) = addition( addition( Z, Y ), X ) }.
% 5.62/6.02 { addition( X, zero ) = X }.
% 5.62/6.02 { addition( X, X ) = X }.
% 5.62/6.02 { multiplication( X, multiplication( Y, Z ) ) = multiplication(
% 5.62/6.02 multiplication( X, Y ), Z ) }.
% 5.62/6.02 { multiplication( X, one ) = X }.
% 5.62/6.02 { multiplication( one, X ) = X }.
% 5.62/6.02 { multiplication( X, addition( Y, Z ) ) = addition( multiplication( X, Y )
% 5.62/6.02 , multiplication( X, Z ) ) }.
% 5.62/6.02 { multiplication( addition( X, Y ), Z ) = addition( multiplication( X, Z )
% 5.62/6.02 , multiplication( Y, Z ) ) }.
% 5.62/6.02 { multiplication( X, zero ) = zero }.
% 5.62/6.02 { multiplication( zero, X ) = zero }.
% 5.62/6.02 { ! leq( X, Y ), addition( X, Y ) = Y }.
% 5.62/6.02 { ! addition( X, Y ) = Y, leq( X, Y ) }.
% 5.62/6.02 { ! test( X ), complement( skol1( X ), X ) }.
% 5.62/6.02 { ! complement( Y, X ), test( X ) }.
% 5.62/6.02 { ! complement( Y, X ), multiplication( X, Y ) = zero }.
% 5.62/6.02 { ! complement( Y, X ), alpha1( X, Y ) }.
% 5.62/6.02 { ! multiplication( X, Y ) = zero, ! alpha1( X, Y ), complement( Y, X ) }.
% 5.62/6.02 { ! alpha1( X, Y ), multiplication( Y, X ) = zero }.
% 5.62/6.02 { ! alpha1( X, Y ), addition( X, Y ) = one }.
% 5.62/6.02 { ! multiplication( Y, X ) = zero, ! addition( X, Y ) = one, alpha1( X, Y )
% 5.62/6.02 }.
% 5.62/6.02 { ! test( X ), ! c( X ) = Y, complement( X, Y ) }.
% 5.62/6.02 { ! test( X ), ! complement( X, Y ), c( X ) = Y }.
% 5.62/6.02 { test( X ), c( X ) = zero }.
% 5.62/6.02 { ! test( X ), ! test( Y ), c( addition( X, Y ) ) = multiplication( c( X )
% 5.62/6.02 , c( Y ) ) }.
% 5.62/6.02 { ! test( X ), ! test( Y ), c( multiplication( X, Y ) ) = addition( c( X )
% 5.62/6.02 , c( Y ) ) }.
% 5.62/6.02 { test( skol3 ) }.
% 5.62/6.02 { test( skol2 ) }.
% 5.62/6.02 { ! leq( one, addition( addition( multiplication( addition( skol3, c( skol3
% 5.62/6.02 ) ), skol2 ), multiplication( addition( skol2, c( skol2 ) ), skol3 ) ),
% 5.62/6.02 multiplication( c( skol2 ), c( skol3 ) ) ) ), ! leq( addition( addition(
% 5.62/6.02 multiplication( addition( skol3, c( skol3 ) ), skol2 ), multiplication(
% 5.62/6.02 addition( skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), c(
% 5.62/6.02 skol3 ) ) ), one ) }.
% 5.62/6.02
% 5.62/6.02 percentage equality = 0.470588, percentage horn = 0.965517
% 5.62/6.02 This is a problem with some equality
% 5.62/6.02
% 5.62/6.02
% 5.62/6.02
% 5.62/6.02 Options Used:
% 5.62/6.02
% 5.62/6.02 useres = 1
% 5.62/6.02 useparamod = 1
% 5.62/6.02 useeqrefl = 1
% 5.62/6.02 useeqfact = 1
% 5.62/6.02 usefactor = 1
% 5.62/6.02 usesimpsplitting = 0
% 5.62/6.02 usesimpdemod = 5
% 5.62/6.02 usesimpres = 3
% 5.62/6.02
% 5.62/6.02 resimpinuse = 1000
% 5.62/6.02 resimpclauses = 20000
% 5.62/6.02 substype = eqrewr
% 5.62/6.02 backwardsubs = 1
% 5.62/6.02 selectoldest = 5
% 5.62/6.02
% 5.62/6.02 litorderings [0] = split
% 5.62/6.02 litorderings [1] = extend the termordering, first sorting on arguments
% 5.62/6.02
% 5.62/6.02 termordering = kbo
% 5.62/6.02
% 5.62/6.02 litapriori = 0
% 5.62/6.02 termapriori = 1
% 5.62/6.02 litaposteriori = 0
% 5.62/6.02 termaposteriori = 0
% 5.62/6.02 demodaposteriori = 0
% 5.62/6.02 ordereqreflfact = 0
% 5.62/6.02
% 5.62/6.02 litselect = negord
% 5.62/6.02
% 5.62/6.02 maxweight = 15
% 5.62/6.02 maxdepth = 30000
% 5.62/6.02 maxlength = 115
% 5.62/6.02 maxnrvars = 195
% 5.62/6.02 excuselevel = 1
% 5.62/6.02 increasemaxweight = 1
% 5.62/6.02
% 5.62/6.02 maxselected = 10000000
% 5.62/6.02 maxnrclauses = 10000000
% 5.62/6.02
% 5.62/6.02 showgenerated = 0
% 5.62/6.02 showkept = 0
% 5.62/6.02 showselected = 0
% 5.62/6.02 showdeleted = 0
% 5.62/6.02 showresimp = 1
% 5.62/6.02 showstatus = 2000
% 5.62/6.02
% 5.62/6.02 prologoutput = 0
% 5.62/6.02 nrgoals = 5000000
% 5.62/6.02 totalproof = 1
% 5.62/6.02
% 5.62/6.02 Symbols occurring in the translation:
% 5.62/6.02
% 5.62/6.02 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 5.62/6.02 . [1, 2] (w:1, o:23, a:1, s:1, b:0),
% 5.62/6.02 ! [4, 1] (w:0, o:15, a:1, s:1, b:0),
% 5.62/6.02 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 5.62/6.02 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 5.62/6.02 addition [37, 2] (w:1, o:47, a:1, s:1, b:0),
% 5.62/6.02 zero [39, 0] (w:1, o:9, a:1, s:1, b:0),
% 5.62/6.02 multiplication [40, 2] (w:1, o:49, a:1, s:1, b:0),
% 5.62/6.02 one [41, 0] (w:1, o:10, a:1, s:1, b:0),
% 5.62/6.02 leq [42, 2] (w:1, o:48, a:1, s:1, b:0),
% 5.62/6.02 test [44, 1] (w:1, o:21, a:1, s:1, b:0),
% 5.62/6.02 complement [46, 2] (w:1, o:50, a:1, s:1, b:0),
% 5.62/6.02 c [47, 1] (w:1, o:22, a:1, s:1, b:0),
% 5.62/6.02 alpha1 [48, 2] (w:1, o:51, a:1, s:1, b:1),
% 5.62/6.02 skol1 [49, 1] (w:1, o:20, a:1, s:1, b:1),
% 5.62/6.02 skol2 [50, 0] (w:1, o:13, a:1, s:1, b:1),
% 5.62/6.02 skol3 [51, 0] (w:1, o:14, a:1, s:1, b:1).
% 5.62/6.02
% 5.62/6.02
% 5.62/6.02 Starting Search:
% 5.62/6.02
% 5.62/6.02 *** allocated 15000 integers for clauses
% 5.62/6.02 *** allocated 22500 integers for clauses
% 5.62/6.02 *** allocated 33750 integers for clauses
% 5.62/6.02 *** allocated 50625 integers for clauses
% 5.62/6.02 *** allocated 15000 integers for termspace/termends
% 5.62/6.02 *** allocated 75937 integers for clauses
% 5.62/6.02 Resimplifying inuse:
% 5.62/6.02 Done
% 5.62/6.02
% 5.62/6.02 *** allocated 22500 integers for termspace/termends
% 5.62/6.02 *** allocated 113905 integers for clauses
% 5.62/6.02 *** allocated 33750 integers for termspace/termends
% 5.62/6.02 *** allocated 170857 integers for clauses
% 5.62/6.02
% 5.62/6.02 Intermediate Status:
% 5.62/6.02 Generated: 13268
% 5.62/6.02 Kept: 2063
% 5.62/6.02 Inuse: 216
% 5.62/6.02 Deleted: 39
% 5.62/6.02 Deletedinuse: 22
% 5.62/6.02
% 5.62/6.02 Resimplifying inuse:
% 5.62/6.02 Done
% 5.62/6.02
% 5.62/6.02 *** allocated 50625 integers for termspace/termends
% 5.62/6.02 Resimplifying inuse:
% 5.62/6.02 Done
% 5.62/6.02
% 5.62/6.02 *** allocated 256285 integers for clauses
% 5.62/6.02
% 5.62/6.02 Intermediate Status:
% 5.62/6.02 Generated: 28514
% 5.62/6.02 Kept: 4069
% 5.62/6.02 Inuse: 453
% 5.62/6.02 Deleted: 161
% 5.62/6.02 Deletedinuse: 61
% 5.62/6.02
% 5.62/6.02 Resimplifying inuse:
% 5.62/6.02 Done
% 5.62/6.02
% 5.62/6.02 *** allocated 75937 integers for termspace/termends
% 5.62/6.02 *** allocated 384427 integers for clauses
% 5.62/6.02 Resimplifying inuse:
% 5.62/6.02 Done
% 5.62/6.02
% 5.62/6.02
% 5.62/6.02 Intermediate Status:
% 5.62/6.02 Generated: 44761
% 5.62/6.02 Kept: 6071
% 5.62/6.02 Inuse: 650
% 5.62/6.02 Deleted: 203
% 5.62/6.02 Deletedinuse: 71
% 5.62/6.02
% 5.62/6.02 Resimplifying inuse:
% 5.62/6.02 Done
% 5.62/6.02
% 5.62/6.02 *** allocated 113905 integers for termspace/termends
% 5.62/6.02 Resimplifying inuse:
% 5.62/6.02 Done
% 5.62/6.02
% 5.62/6.02 *** allocated 576640 integers for clauses
% 5.62/6.02
% 5.62/6.02 Intermediate Status:
% 5.62/6.02 Generated: 64160
% 5.62/6.02 Kept: 8090
% 5.62/6.02 Inuse: 764
% 5.62/6.02 Deleted: 235
% 5.62/6.02 Deletedinuse: 76
% 5.62/6.02
% 5.62/6.02 Resimplifying inuse:
% 5.62/6.02 Done
% 5.62/6.02
% 5.62/6.02 Resimplifying inuse:
% 5.62/6.02 Done
% 5.62/6.02
% 5.62/6.02 *** allocated 170857 integers for termspace/termends
% 5.62/6.02
% 5.62/6.02 Intermediate Status:
% 5.62/6.02 Generated: 75849
% 5.62/6.02 Kept: 10091
% 5.62/6.02 Inuse: 873
% 5.62/6.02 Deleted: 317
% 5.62/6.02 Deletedinuse: 146
% 5.62/6.02
% 5.62/6.02 Resimplifying inuse:
% 5.62/6.02 Done
% 5.62/6.02
% 5.62/6.02 Resimplifying inuse:
% 5.62/6.02 Done
% 5.62/6.02
% 5.62/6.02 *** allocated 864960 integers for clauses
% 5.62/6.02
% 5.62/6.02 Intermediate Status:
% 5.62/6.02 Generated: 82687
% 5.62/6.02 Kept: 12098
% 5.62/6.02 Inuse: 902
% 5.62/6.02 Deleted: 464
% 5.62/6.02 Deletedinuse: 288
% 5.62/6.02
% 5.62/6.02 Resimplifying inuse:
% 5.62/6.02 Done
% 5.62/6.02
% 5.62/6.02 Resimplifying inuse:
% 5.62/6.02 Done
% 5.62/6.02
% 5.62/6.02 *** allocated 256285 integers for termspace/termends
% 5.62/6.02
% 5.62/6.02 Intermediate Status:
% 5.62/6.02 Generated: 100263
% 5.62/6.02 Kept: 14188
% 5.62/6.02 Inuse: 992
% 5.62/6.02 Deleted: 513
% 5.62/6.02 Deletedinuse: 304
% 5.62/6.02
% 5.62/6.02 Resimplifying inuse:
% 5.62/6.02 Done
% 5.62/6.02
% 5.62/6.02 Resimplifying inuse:
% 5.62/6.02 Done
% 5.62/6.02
% 5.62/6.02
% 5.62/6.02 Intermediate Status:
% 5.62/6.02 Generated: 123775
% 5.62/6.02 Kept: 16192
% 5.62/6.02 Inuse: 1120
% 5.62/6.02 Deleted: 684
% 5.62/6.02 Deletedinuse: 314
% 5.62/6.02
% 5.62/6.02 Resimplifying inuse:
% 5.62/6.02 Done
% 5.62/6.02
% 5.62/6.02 Resimplifying inuse:
% 5.62/6.02 Done
% 5.62/6.02
% 5.62/6.02
% 5.62/6.02 Intermediate Status:
% 5.62/6.02 Generated: 140994
% 5.62/6.02 Kept: 18192
% 5.62/6.02 Inuse: 1256
% 5.62/6.02 Deleted: 731
% 5.62/6.02 Deletedinuse: 315
% 5.62/6.02
% 5.62/6.02 *** allocated 1297440 integers for clauses
% 5.62/6.02 Resimplifying inuse:
% 5.62/6.02 Done
% 5.62/6.02
% 5.62/6.02 Resimplifying inuse:
% 5.62/6.02 Done
% 5.62/6.02
% 5.62/6.02 Resimplifying clauses:
% 5.62/6.02
% 5.62/6.02 Bliksems!, er is een bewijs:
% 5.62/6.02 % SZS status Theorem
% 5.62/6.02 % SZS output start Refutation
% 5.62/6.02
% 5.62/6.02 (0) {G0,W7,D3,L1,V2,M1} I { addition( X, Y ) = addition( Y, X ) }.
% 5.62/6.02 (1) {G0,W11,D4,L1,V3,M1} I { addition( Z, addition( Y, X ) ) ==> addition(
% 5.62/6.02 addition( Z, Y ), X ) }.
% 5.62/6.02 (3) {G0,W5,D3,L1,V1,M1} I { addition( X, X ) ==> X }.
% 5.62/6.02 (5) {G0,W5,D3,L1,V1,M1} I { multiplication( X, one ) ==> X }.
% 5.62/6.02 (6) {G0,W5,D3,L1,V1,M1} I { multiplication( one, X ) ==> X }.
% 5.62/6.02 (7) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Y ),
% 5.62/6.02 multiplication( X, Z ) ) ==> multiplication( X, addition( Y, Z ) ) }.
% 5.62/6.02 (8) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Z ),
% 5.62/6.02 multiplication( Y, Z ) ) ==> multiplication( addition( X, Y ), Z ) }.
% 5.62/6.02 (11) {G0,W8,D3,L2,V2,M2} I { ! leq( X, Y ), addition( X, Y ) ==> Y }.
% 5.62/6.02 (12) {G0,W8,D3,L2,V2,M2} I { ! addition( X, Y ) ==> Y, leq( X, Y ) }.
% 5.62/6.02 (13) {G0,W6,D3,L2,V1,M2} I { ! test( X ), complement( skol1( X ), X ) }.
% 5.62/6.02 (15) {G0,W8,D3,L2,V2,M2} I { ! complement( Y, X ), multiplication( X, Y )
% 5.62/6.02 ==> zero }.
% 5.62/6.02 (16) {G0,W6,D2,L2,V2,M2} I { ! complement( Y, X ), alpha1( X, Y ) }.
% 5.62/6.02 (17) {G0,W11,D3,L3,V2,M3} I { ! multiplication( X, Y ) ==> zero, ! alpha1(
% 5.62/6.02 X, Y ), complement( Y, X ) }.
% 5.62/6.02 (18) {G0,W8,D3,L2,V2,M2} I { ! alpha1( X, Y ), multiplication( Y, X ) ==>
% 5.62/6.02 zero }.
% 5.62/6.02 (19) {G0,W8,D3,L2,V2,M2} I { ! alpha1( X, Y ), addition( X, Y ) ==> one }.
% 5.62/6.02 (20) {G0,W13,D3,L3,V2,M3} I { ! multiplication( Y, X ) ==> zero, ! addition
% 5.62/6.02 ( X, Y ) ==> one, alpha1( X, Y ) }.
% 5.62/6.02 (22) {G0,W9,D3,L3,V2,M3} I { ! test( X ), ! complement( X, Y ), c( X ) = Y
% 5.62/6.02 }.
% 5.62/6.02 (26) {G0,W2,D2,L1,V0,M1} I { test( skol3 ) }.
% 5.62/6.02 (27) {G0,W2,D2,L1,V0,M1} I { test( skol2 ) }.
% 5.62/6.02 (28) {G0,W42,D7,L2,V0,M2} I { ! leq( one, addition( addition(
% 5.62/6.02 multiplication( addition( skol3, c( skol3 ) ), skol2 ), multiplication(
% 5.62/6.02 addition( skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), c(
% 5.62/6.02 skol3 ) ) ) ), ! leq( addition( addition( multiplication( addition( skol3
% 5.62/6.02 , c( skol3 ) ), skol2 ), multiplication( addition( skol2, c( skol2 ) ),
% 5.62/6.02 skol3 ) ), multiplication( c( skol2 ), c( skol3 ) ) ), one ) }.
% 5.62/6.02 (34) {G1,W9,D4,L1,V2,M1} P(3,1) { addition( addition( Y, X ), X ) ==>
% 5.62/6.02 addition( Y, X ) }.
% 5.62/6.02 (50) {G1,W17,D5,L1,V4,M1} P(7,1) { addition( addition( T, multiplication( X
% 5.62/6.02 , Y ) ), multiplication( X, Z ) ) ==> addition( T, multiplication( X,
% 5.62/6.02 addition( Y, Z ) ) ) }.
% 5.62/6.02 (51) {G1,W11,D4,L1,V2,M1} P(5,7) { addition( X, multiplication( X, Y ) ) =
% 5.62/6.02 multiplication( X, addition( one, Y ) ) }.
% 5.62/6.02 (52) {G1,W11,D4,L1,V2,M1} P(5,7) { addition( multiplication( X, Y ), X ) =
% 5.62/6.02 multiplication( X, addition( Y, one ) ) }.
% 5.62/6.02 (63) {G1,W17,D5,L1,V4,M1} P(8,1) { addition( addition( T, multiplication( X
% 5.62/6.02 , Y ) ), multiplication( Z, Y ) ) ==> addition( T, multiplication(
% 5.62/6.02 addition( X, Z ), Y ) ) }.
% 5.62/6.02 (64) {G1,W11,D4,L1,V2,M1} P(6,8) { addition( X, multiplication( Y, X ) ) =
% 5.62/6.02 multiplication( addition( one, Y ), X ) }.
% 5.62/6.02 (80) {G1,W8,D3,L2,V2,M2} P(11,0) { addition( Y, X ) ==> Y, ! leq( X, Y )
% 5.62/6.02 }.
% 5.62/6.02 (149) {G1,W3,D2,L1,V1,M1} R(12,3) { leq( X, X ) }.
% 5.62/6.02 (154) {G1,W14,D4,L2,V3,M2} P(1,12) { ! addition( addition( X, Y ), Z ) ==>
% 5.62/6.02 addition( Y, Z ), leq( X, addition( Y, Z ) ) }.
% 5.62/6.02 (183) {G1,W4,D3,L1,V0,M1} R(13,26) { complement( skol1( skol3 ), skol3 )
% 5.62/6.02 }.
% 5.62/6.02 (184) {G1,W4,D3,L1,V0,M1} R(13,27) { complement( skol1( skol2 ), skol2 )
% 5.62/6.02 }.
% 5.62/6.02 (187) {G2,W4,D3,L1,V0,M1} R(183,16) { alpha1( skol3, skol1( skol3 ) ) }.
% 5.62/6.02 (191) {G2,W4,D3,L1,V0,M1} R(184,16) { alpha1( skol2, skol1( skol2 ) ) }.
% 5.62/6.02 (194) {G2,W6,D4,L1,V0,M1} R(15,184) { multiplication( skol2, skol1( skol2 )
% 5.62/6.02 ) ==> zero }.
% 5.62/6.02 (195) {G2,W6,D4,L1,V0,M1} R(15,183) { multiplication( skol3, skol1( skol3 )
% 5.62/6.02 ) ==> zero }.
% 5.62/6.02 (236) {G3,W6,D4,L1,V0,M1} R(18,191) { multiplication( skol1( skol2 ), skol2
% 5.62/6.02 ) ==> zero }.
% 5.62/6.02 (237) {G3,W6,D4,L1,V0,M1} R(18,187) { multiplication( skol1( skol3 ), skol3
% 5.62/6.02 ) ==> zero }.
% 5.62/6.02 (262) {G3,W6,D4,L1,V0,M1} R(19,191) { addition( skol2, skol1( skol2 ) ) ==>
% 5.62/6.02 one }.
% 5.62/6.02 (263) {G3,W6,D4,L1,V0,M1} R(19,187) { addition( skol3, skol1( skol3 ) ) ==>
% 5.62/6.02 one }.
% 5.62/6.02 (515) {G1,W62,D8,L2,V0,M2} R(28,12);d(1);d(1) { ! leq( addition( addition(
% 5.62/6.02 multiplication( addition( skol3, c( skol3 ) ), skol2 ), multiplication(
% 5.62/6.02 addition( skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), c(
% 5.62/6.02 skol3 ) ) ), one ), ! addition( addition( addition( one, multiplication(
% 5.62/6.02 addition( skol3, c( skol3 ) ), skol2 ) ), multiplication( addition( skol2
% 5.62/6.02 , c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), c( skol3 ) ) ) ==>
% 5.62/6.02 addition( addition( multiplication( addition( skol3, c( skol3 ) ), skol2
% 5.62/6.02 ), multiplication( addition( skol2, c( skol2 ) ), skol3 ) ),
% 5.62/6.02 multiplication( c( skol2 ), c( skol3 ) ) ) }.
% 5.62/6.02 (2384) {G4,W6,D4,L1,V0,M1} P(262,34) { addition( one, skol1( skol2 ) ) ==>
% 5.62/6.02 one }.
% 5.62/6.02 (2391) {G4,W6,D4,L1,V0,M1} P(262,0) { addition( skol1( skol2 ), skol2 ) ==>
% 5.62/6.02 one }.
% 5.62/6.02 (2396) {G5,W8,D5,L1,V1,M1} P(2384,64);d(6) { addition( X, multiplication(
% 5.62/6.02 skol1( skol2 ), X ) ) ==> X }.
% 5.62/6.02 (2426) {G5,W4,D3,L1,V0,M1} R(2391,20);d(194);q { alpha1( skol1( skol2 ),
% 5.62/6.02 skol2 ) }.
% 5.62/6.02 (2438) {G5,W5,D3,L1,V0,M1} P(2391,34) { addition( one, skol2 ) ==> one }.
% 5.62/6.02 (2441) {G6,W4,D3,L1,V0,M1} R(2426,17);d(236);q { complement( skol2, skol1(
% 5.62/6.02 skol2 ) ) }.
% 5.62/6.02 (2446) {G7,W5,D3,L1,V0,M1} R(2441,22);r(27) { c( skol2 ) ==> skol1( skol2 )
% 5.62/6.02 }.
% 5.62/6.02 (2503) {G6,W7,D4,L1,V1,M1} P(2438,51);d(5) { addition( X, multiplication( X
% 5.62/6.02 , skol2 ) ) ==> X }.
% 5.62/6.02 (2514) {G6,W5,D3,L1,V0,M1} P(2438,0) { addition( skol2, one ) ==> one }.
% 5.62/6.02 (2747) {G4,W6,D4,L1,V0,M1} P(263,0) { addition( skol1( skol3 ), skol3 ) ==>
% 5.62/6.02 one }.
% 5.62/6.02 (2782) {G5,W4,D3,L1,V0,M1} R(2747,20);d(195);q { alpha1( skol1( skol3 ),
% 5.62/6.02 skol3 ) }.
% 5.62/6.02 (2794) {G5,W5,D3,L1,V0,M1} P(2747,34) { addition( one, skol3 ) ==> one }.
% 5.62/6.02 (2797) {G6,W4,D3,L1,V0,M1} R(2782,17);d(237);q { complement( skol3, skol1(
% 5.62/6.02 skol3 ) ) }.
% 5.62/6.02 (2802) {G7,W5,D3,L1,V0,M1} R(2797,22);r(26) { c( skol3 ) ==> skol1( skol3 )
% 5.62/6.02 }.
% 5.62/6.02 (2859) {G6,W7,D4,L1,V1,M1} P(2794,51);d(5) { addition( X, multiplication( X
% 5.62/6.02 , skol3 ) ) ==> X }.
% 5.62/6.02 (2870) {G6,W5,D3,L1,V0,M1} P(2794,0) { addition( skol3, one ) ==> one }.
% 5.62/6.02 (2875) {G7,W7,D4,L1,V1,M1} P(2870,52);d(5) { addition( multiplication( X,
% 5.62/6.02 skol3 ), X ) ==> X }.
% 5.62/6.02 (4122) {G2,W5,D3,L1,V2,M1} P(3,154);q { leq( X, addition( X, Y ) ) }.
% 5.62/6.02 (4179) {G3,W7,D4,L1,V3,M1} P(1,4122) { leq( X, addition( addition( X, Y ),
% 5.62/6.02 Z ) ) }.
% 5.62/6.02 (18502) {G8,W7,D3,L1,V2,M1} P(2875,4179) { leq( multiplication( X, skol3 )
% 5.62/6.02 , addition( X, Y ) ) }.
% 5.62/6.02 (18564) {G9,W5,D3,L1,V0,M1} P(2514,18502) { leq( multiplication( skol2,
% 5.62/6.02 skol3 ), one ) }.
% 5.62/6.02 (18605) {G10,W7,D4,L1,V0,M1} R(18564,80) { addition( one, multiplication(
% 5.62/6.02 skol2, skol3 ) ) ==> one }.
% 5.62/6.02 (18875) {G7,W13,D5,L1,V2,M1} P(2859,63) { addition( X, multiplication(
% 5.62/6.02 addition( X, Y ), skol3 ) ) ==> addition( X, multiplication( Y, skol3 ) )
% 5.62/6.02 }.
% 5.62/6.02 (19903) {G11,W13,D5,L1,V1,M1} P(18605,63) { addition( one, multiplication(
% 5.62/6.02 addition( skol2, X ), skol3 ) ) ==> addition( one, multiplication( X,
% 5.62/6.02 skol3 ) ) }.
% 5.62/6.02 (20404) {G12,W0,D0,L0,V0,M0} S(515);d(2802);d(2802);d(263);d(263);d(6);d(
% 5.62/6.02 2503);d(18875);d(19903);d(50);d(50);d(2446);d(2446);d(263);d(263);d(5);d(
% 5.62/6.02 2396);d(262);d(6);d(18875);d(50);d(263);d(5);d(262);q;r(149) { }.
% 5.62/6.02
% 5.62/6.02
% 5.62/6.02 % SZS output end Refutation
% 5.62/6.02 found a proof!
% 5.62/6.02
% 5.62/6.02
% 5.62/6.02 Unprocessed initial clauses:
% 5.62/6.02
% 5.62/6.02 (20406) {G0,W7,D3,L1,V2,M1} { addition( X, Y ) = addition( Y, X ) }.
% 5.62/6.02 (20407) {G0,W11,D4,L1,V3,M1} { addition( Z, addition( Y, X ) ) = addition
% 5.62/6.02 ( addition( Z, Y ), X ) }.
% 5.62/6.02 (20408) {G0,W5,D3,L1,V1,M1} { addition( X, zero ) = X }.
% 5.62/6.02 (20409) {G0,W5,D3,L1,V1,M1} { addition( X, X ) = X }.
% 5.62/6.02 (20410) {G0,W11,D4,L1,V3,M1} { multiplication( X, multiplication( Y, Z ) )
% 5.62/6.02 = multiplication( multiplication( X, Y ), Z ) }.
% 5.62/6.02 (20411) {G0,W5,D3,L1,V1,M1} { multiplication( X, one ) = X }.
% 5.62/6.02 (20412) {G0,W5,D3,L1,V1,M1} { multiplication( one, X ) = X }.
% 5.62/6.02 (20413) {G0,W13,D4,L1,V3,M1} { multiplication( X, addition( Y, Z ) ) =
% 5.62/6.02 addition( multiplication( X, Y ), multiplication( X, Z ) ) }.
% 5.62/6.02 (20414) {G0,W13,D4,L1,V3,M1} { multiplication( addition( X, Y ), Z ) =
% 5.62/6.02 addition( multiplication( X, Z ), multiplication( Y, Z ) ) }.
% 5.62/6.02 (20415) {G0,W5,D3,L1,V1,M1} { multiplication( X, zero ) = zero }.
% 5.62/6.02 (20416) {G0,W5,D3,L1,V1,M1} { multiplication( zero, X ) = zero }.
% 5.62/6.02 (20417) {G0,W8,D3,L2,V2,M2} { ! leq( X, Y ), addition( X, Y ) = Y }.
% 5.62/6.02 (20418) {G0,W8,D3,L2,V2,M2} { ! addition( X, Y ) = Y, leq( X, Y ) }.
% 5.62/6.02 (20419) {G0,W6,D3,L2,V1,M2} { ! test( X ), complement( skol1( X ), X ) }.
% 5.62/6.02 (20420) {G0,W5,D2,L2,V2,M2} { ! complement( Y, X ), test( X ) }.
% 5.62/6.02 (20421) {G0,W8,D3,L2,V2,M2} { ! complement( Y, X ), multiplication( X, Y )
% 5.62/6.02 = zero }.
% 5.62/6.02 (20422) {G0,W6,D2,L2,V2,M2} { ! complement( Y, X ), alpha1( X, Y ) }.
% 5.62/6.02 (20423) {G0,W11,D3,L3,V2,M3} { ! multiplication( X, Y ) = zero, ! alpha1(
% 5.62/6.02 X, Y ), complement( Y, X ) }.
% 5.62/6.02 (20424) {G0,W8,D3,L2,V2,M2} { ! alpha1( X, Y ), multiplication( Y, X ) =
% 5.62/6.02 zero }.
% 5.62/6.02 (20425) {G0,W8,D3,L2,V2,M2} { ! alpha1( X, Y ), addition( X, Y ) = one }.
% 5.62/6.02 (20426) {G0,W13,D3,L3,V2,M3} { ! multiplication( Y, X ) = zero, ! addition
% 5.62/6.02 ( X, Y ) = one, alpha1( X, Y ) }.
% 5.62/6.02 (20427) {G0,W9,D3,L3,V2,M3} { ! test( X ), ! c( X ) = Y, complement( X, Y
% 5.62/6.02 ) }.
% 5.62/6.02 (20428) {G0,W9,D3,L3,V2,M3} { ! test( X ), ! complement( X, Y ), c( X ) =
% 5.62/6.02 Y }.
% 5.62/6.02 (20429) {G0,W6,D3,L2,V1,M2} { test( X ), c( X ) = zero }.
% 5.62/6.02 (20430) {G0,W14,D4,L3,V2,M3} { ! test( X ), ! test( Y ), c( addition( X, Y
% 5.62/6.02 ) ) = multiplication( c( X ), c( Y ) ) }.
% 5.62/6.02 (20431) {G0,W14,D4,L3,V2,M3} { ! test( X ), ! test( Y ), c( multiplication
% 5.62/6.02 ( X, Y ) ) = addition( c( X ), c( Y ) ) }.
% 5.62/6.02 (20432) {G0,W2,D2,L1,V0,M1} { test( skol3 ) }.
% 5.62/6.02 (20433) {G0,W2,D2,L1,V0,M1} { test( skol2 ) }.
% 5.62/6.02 (20434) {G0,W42,D7,L2,V0,M2} { ! leq( one, addition( addition(
% 5.62/6.02 multiplication( addition( skol3, c( skol3 ) ), skol2 ), multiplication(
% 5.62/6.02 addition( skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), c(
% 5.62/6.02 skol3 ) ) ) ), ! leq( addition( addition( multiplication( addition( skol3
% 5.62/6.02 , c( skol3 ) ), skol2 ), multiplication( addition( skol2, c( skol2 ) ),
% 5.62/6.02 skol3 ) ), multiplication( c( skol2 ), c( skol3 ) ) ), one ) }.
% 5.62/6.02
% 5.62/6.02
% 5.62/6.02 Total Proof:
% 5.62/6.02
% 5.62/6.02 subsumption: (0) {G0,W7,D3,L1,V2,M1} I { addition( X, Y ) = addition( Y, X
% 5.62/6.02 ) }.
% 5.62/6.02 parent0: (20406) {G0,W7,D3,L1,V2,M1} { addition( X, Y ) = addition( Y, X )
% 5.62/6.02 }.
% 5.62/6.02 substitution0:
% 5.62/6.02 X := X
% 5.62/6.02 Y := Y
% 5.62/6.02 end
% 5.62/6.02 permutation0:
% 5.62/6.02 0 ==> 0
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 subsumption: (1) {G0,W11,D4,L1,V3,M1} I { addition( Z, addition( Y, X ) )
% 5.62/6.02 ==> addition( addition( Z, Y ), X ) }.
% 5.62/6.02 parent0: (20407) {G0,W11,D4,L1,V3,M1} { addition( Z, addition( Y, X ) ) =
% 5.62/6.02 addition( addition( Z, Y ), X ) }.
% 5.62/6.02 substitution0:
% 5.62/6.02 X := X
% 5.62/6.02 Y := Y
% 5.62/6.02 Z := Z
% 5.62/6.02 end
% 5.62/6.02 permutation0:
% 5.62/6.02 0 ==> 0
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 subsumption: (3) {G0,W5,D3,L1,V1,M1} I { addition( X, X ) ==> X }.
% 5.62/6.02 parent0: (20409) {G0,W5,D3,L1,V1,M1} { addition( X, X ) = X }.
% 5.62/6.02 substitution0:
% 5.62/6.02 X := X
% 5.62/6.02 end
% 5.62/6.02 permutation0:
% 5.62/6.02 0 ==> 0
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 subsumption: (5) {G0,W5,D3,L1,V1,M1} I { multiplication( X, one ) ==> X }.
% 5.62/6.02 parent0: (20411) {G0,W5,D3,L1,V1,M1} { multiplication( X, one ) = X }.
% 5.62/6.02 substitution0:
% 5.62/6.02 X := X
% 5.62/6.02 end
% 5.62/6.02 permutation0:
% 5.62/6.02 0 ==> 0
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 subsumption: (6) {G0,W5,D3,L1,V1,M1} I { multiplication( one, X ) ==> X }.
% 5.62/6.02 parent0: (20412) {G0,W5,D3,L1,V1,M1} { multiplication( one, X ) = X }.
% 5.62/6.02 substitution0:
% 5.62/6.02 X := X
% 5.62/6.02 end
% 5.62/6.02 permutation0:
% 5.62/6.02 0 ==> 0
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 eqswap: (20456) {G0,W13,D4,L1,V3,M1} { addition( multiplication( X, Y ),
% 5.62/6.02 multiplication( X, Z ) ) = multiplication( X, addition( Y, Z ) ) }.
% 5.62/6.02 parent0[0]: (20413) {G0,W13,D4,L1,V3,M1} { multiplication( X, addition( Y
% 5.62/6.02 , Z ) ) = addition( multiplication( X, Y ), multiplication( X, Z ) ) }.
% 5.62/6.02 substitution0:
% 5.62/6.02 X := X
% 5.62/6.02 Y := Y
% 5.62/6.02 Z := Z
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 subsumption: (7) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Y )
% 5.62/6.02 , multiplication( X, Z ) ) ==> multiplication( X, addition( Y, Z ) ) }.
% 5.62/6.02 parent0: (20456) {G0,W13,D4,L1,V3,M1} { addition( multiplication( X, Y ),
% 5.62/6.02 multiplication( X, Z ) ) = multiplication( X, addition( Y, Z ) ) }.
% 5.62/6.02 substitution0:
% 5.62/6.02 X := X
% 5.62/6.02 Y := Y
% 5.62/6.02 Z := Z
% 5.62/6.02 end
% 5.62/6.02 permutation0:
% 5.62/6.02 0 ==> 0
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 eqswap: (20464) {G0,W13,D4,L1,V3,M1} { addition( multiplication( X, Z ),
% 5.62/6.02 multiplication( Y, Z ) ) = multiplication( addition( X, Y ), Z ) }.
% 5.62/6.02 parent0[0]: (20414) {G0,W13,D4,L1,V3,M1} { multiplication( addition( X, Y
% 5.62/6.02 ), Z ) = addition( multiplication( X, Z ), multiplication( Y, Z ) ) }.
% 5.62/6.02 substitution0:
% 5.62/6.02 X := X
% 5.62/6.02 Y := Y
% 5.62/6.02 Z := Z
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 subsumption: (8) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Z )
% 5.62/6.02 , multiplication( Y, Z ) ) ==> multiplication( addition( X, Y ), Z ) }.
% 5.62/6.02 parent0: (20464) {G0,W13,D4,L1,V3,M1} { addition( multiplication( X, Z ),
% 5.62/6.02 multiplication( Y, Z ) ) = multiplication( addition( X, Y ), Z ) }.
% 5.62/6.02 substitution0:
% 5.62/6.02 X := X
% 5.62/6.02 Y := Y
% 5.62/6.02 Z := Z
% 5.62/6.02 end
% 5.62/6.02 permutation0:
% 5.62/6.02 0 ==> 0
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 subsumption: (11) {G0,W8,D3,L2,V2,M2} I { ! leq( X, Y ), addition( X, Y )
% 5.62/6.02 ==> Y }.
% 5.62/6.02 parent0: (20417) {G0,W8,D3,L2,V2,M2} { ! leq( X, Y ), addition( X, Y ) = Y
% 5.62/6.02 }.
% 5.62/6.02 substitution0:
% 5.62/6.02 X := X
% 5.62/6.02 Y := Y
% 5.62/6.02 end
% 5.62/6.02 permutation0:
% 5.62/6.02 0 ==> 0
% 5.62/6.02 1 ==> 1
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 subsumption: (12) {G0,W8,D3,L2,V2,M2} I { ! addition( X, Y ) ==> Y, leq( X
% 5.62/6.02 , Y ) }.
% 5.62/6.02 parent0: (20418) {G0,W8,D3,L2,V2,M2} { ! addition( X, Y ) = Y, leq( X, Y )
% 5.62/6.02 }.
% 5.62/6.02 substitution0:
% 5.62/6.02 X := X
% 5.62/6.02 Y := Y
% 5.62/6.02 end
% 5.62/6.02 permutation0:
% 5.62/6.02 0 ==> 0
% 5.62/6.02 1 ==> 1
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 subsumption: (13) {G0,W6,D3,L2,V1,M2} I { ! test( X ), complement( skol1( X
% 5.62/6.02 ), X ) }.
% 5.62/6.02 parent0: (20419) {G0,W6,D3,L2,V1,M2} { ! test( X ), complement( skol1( X )
% 5.62/6.02 , X ) }.
% 5.62/6.02 substitution0:
% 5.62/6.02 X := X
% 5.62/6.02 end
% 5.62/6.02 permutation0:
% 5.62/6.02 0 ==> 0
% 5.62/6.02 1 ==> 1
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 subsumption: (15) {G0,W8,D3,L2,V2,M2} I { ! complement( Y, X ),
% 5.62/6.02 multiplication( X, Y ) ==> zero }.
% 5.62/6.02 parent0: (20421) {G0,W8,D3,L2,V2,M2} { ! complement( Y, X ),
% 5.62/6.02 multiplication( X, Y ) = zero }.
% 5.62/6.02 substitution0:
% 5.62/6.02 X := X
% 5.62/6.02 Y := Y
% 5.62/6.02 end
% 5.62/6.02 permutation0:
% 5.62/6.02 0 ==> 0
% 5.62/6.02 1 ==> 1
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 subsumption: (16) {G0,W6,D2,L2,V2,M2} I { ! complement( Y, X ), alpha1( X,
% 5.62/6.02 Y ) }.
% 5.62/6.02 parent0: (20422) {G0,W6,D2,L2,V2,M2} { ! complement( Y, X ), alpha1( X, Y
% 5.62/6.02 ) }.
% 5.62/6.02 substitution0:
% 5.62/6.02 X := X
% 5.62/6.02 Y := Y
% 5.62/6.02 end
% 5.62/6.02 permutation0:
% 5.62/6.02 0 ==> 0
% 5.62/6.02 1 ==> 1
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 subsumption: (17) {G0,W11,D3,L3,V2,M3} I { ! multiplication( X, Y ) ==>
% 5.62/6.02 zero, ! alpha1( X, Y ), complement( Y, X ) }.
% 5.62/6.02 parent0: (20423) {G0,W11,D3,L3,V2,M3} { ! multiplication( X, Y ) = zero, !
% 5.62/6.02 alpha1( X, Y ), complement( Y, X ) }.
% 5.62/6.02 substitution0:
% 5.62/6.02 X := X
% 5.62/6.02 Y := Y
% 5.62/6.02 end
% 5.62/6.02 permutation0:
% 5.62/6.02 0 ==> 0
% 5.62/6.02 1 ==> 1
% 5.62/6.02 2 ==> 2
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 subsumption: (18) {G0,W8,D3,L2,V2,M2} I { ! alpha1( X, Y ), multiplication
% 5.62/6.02 ( Y, X ) ==> zero }.
% 5.62/6.02 parent0: (20424) {G0,W8,D3,L2,V2,M2} { ! alpha1( X, Y ), multiplication( Y
% 5.62/6.02 , X ) = zero }.
% 5.62/6.02 substitution0:
% 5.62/6.02 X := X
% 5.62/6.02 Y := Y
% 5.62/6.02 end
% 5.62/6.02 permutation0:
% 5.62/6.02 0 ==> 0
% 5.62/6.02 1 ==> 1
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 subsumption: (19) {G0,W8,D3,L2,V2,M2} I { ! alpha1( X, Y ), addition( X, Y
% 5.62/6.02 ) ==> one }.
% 5.62/6.02 parent0: (20425) {G0,W8,D3,L2,V2,M2} { ! alpha1( X, Y ), addition( X, Y )
% 5.62/6.02 = one }.
% 5.62/6.02 substitution0:
% 5.62/6.02 X := X
% 5.62/6.02 Y := Y
% 5.62/6.02 end
% 5.62/6.02 permutation0:
% 5.62/6.02 0 ==> 0
% 5.62/6.02 1 ==> 1
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 subsumption: (20) {G0,W13,D3,L3,V2,M3} I { ! multiplication( Y, X ) ==>
% 5.62/6.02 zero, ! addition( X, Y ) ==> one, alpha1( X, Y ) }.
% 5.62/6.02 parent0: (20426) {G0,W13,D3,L3,V2,M3} { ! multiplication( Y, X ) = zero, !
% 5.62/6.02 addition( X, Y ) = one, alpha1( X, Y ) }.
% 5.62/6.02 substitution0:
% 5.62/6.02 X := X
% 5.62/6.02 Y := Y
% 5.62/6.02 end
% 5.62/6.02 permutation0:
% 5.62/6.02 0 ==> 0
% 5.62/6.02 1 ==> 1
% 5.62/6.02 2 ==> 2
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 subsumption: (22) {G0,W9,D3,L3,V2,M3} I { ! test( X ), ! complement( X, Y )
% 5.62/6.02 , c( X ) = Y }.
% 5.62/6.02 parent0: (20428) {G0,W9,D3,L3,V2,M3} { ! test( X ), ! complement( X, Y ),
% 5.62/6.02 c( X ) = Y }.
% 5.62/6.02 substitution0:
% 5.62/6.02 X := X
% 5.62/6.02 Y := Y
% 5.62/6.02 end
% 5.62/6.02 permutation0:
% 5.62/6.02 0 ==> 0
% 5.62/6.02 1 ==> 1
% 5.62/6.02 2 ==> 2
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 subsumption: (26) {G0,W2,D2,L1,V0,M1} I { test( skol3 ) }.
% 5.62/6.02 parent0: (20432) {G0,W2,D2,L1,V0,M1} { test( skol3 ) }.
% 5.62/6.02 substitution0:
% 5.62/6.02 end
% 5.62/6.02 permutation0:
% 5.62/6.02 0 ==> 0
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 subsumption: (27) {G0,W2,D2,L1,V0,M1} I { test( skol2 ) }.
% 5.62/6.02 parent0: (20433) {G0,W2,D2,L1,V0,M1} { test( skol2 ) }.
% 5.62/6.02 substitution0:
% 5.62/6.02 end
% 5.62/6.02 permutation0:
% 5.62/6.02 0 ==> 0
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 subsumption: (28) {G0,W42,D7,L2,V0,M2} I { ! leq( one, addition( addition(
% 5.62/6.02 multiplication( addition( skol3, c( skol3 ) ), skol2 ), multiplication(
% 5.62/6.02 addition( skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), c(
% 5.62/6.02 skol3 ) ) ) ), ! leq( addition( addition( multiplication( addition( skol3
% 5.62/6.02 , c( skol3 ) ), skol2 ), multiplication( addition( skol2, c( skol2 ) ),
% 5.62/6.02 skol3 ) ), multiplication( c( skol2 ), c( skol3 ) ) ), one ) }.
% 5.62/6.02 parent0: (20434) {G0,W42,D7,L2,V0,M2} { ! leq( one, addition( addition(
% 5.62/6.02 multiplication( addition( skol3, c( skol3 ) ), skol2 ), multiplication(
% 5.62/6.02 addition( skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), c(
% 5.62/6.02 skol3 ) ) ) ), ! leq( addition( addition( multiplication( addition( skol3
% 5.62/6.02 , c( skol3 ) ), skol2 ), multiplication( addition( skol2, c( skol2 ) ),
% 5.62/6.02 skol3 ) ), multiplication( c( skol2 ), c( skol3 ) ) ), one ) }.
% 5.62/6.02 substitution0:
% 5.62/6.02 end
% 5.62/6.02 permutation0:
% 5.62/6.02 0 ==> 0
% 5.62/6.02 1 ==> 1
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 eqswap: (20696) {G0,W11,D4,L1,V3,M1} { addition( addition( X, Y ), Z ) ==>
% 5.62/6.02 addition( X, addition( Y, Z ) ) }.
% 5.62/6.02 parent0[0]: (1) {G0,W11,D4,L1,V3,M1} I { addition( Z, addition( Y, X ) )
% 5.62/6.02 ==> addition( addition( Z, Y ), X ) }.
% 5.62/6.02 substitution0:
% 5.62/6.02 X := Z
% 5.62/6.02 Y := Y
% 5.62/6.02 Z := X
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 paramod: (20702) {G1,W9,D4,L1,V2,M1} { addition( addition( X, Y ), Y ) ==>
% 5.62/6.02 addition( X, Y ) }.
% 5.62/6.02 parent0[0]: (3) {G0,W5,D3,L1,V1,M1} I { addition( X, X ) ==> X }.
% 5.62/6.02 parent1[0; 8]: (20696) {G0,W11,D4,L1,V3,M1} { addition( addition( X, Y ),
% 5.62/6.02 Z ) ==> addition( X, addition( Y, Z ) ) }.
% 5.62/6.02 substitution0:
% 5.62/6.02 X := Y
% 5.62/6.02 end
% 5.62/6.02 substitution1:
% 5.62/6.02 X := X
% 5.62/6.02 Y := Y
% 5.62/6.02 Z := Y
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 subsumption: (34) {G1,W9,D4,L1,V2,M1} P(3,1) { addition( addition( Y, X ),
% 5.62/6.02 X ) ==> addition( Y, X ) }.
% 5.62/6.02 parent0: (20702) {G1,W9,D4,L1,V2,M1} { addition( addition( X, Y ), Y ) ==>
% 5.62/6.02 addition( X, Y ) }.
% 5.62/6.02 substitution0:
% 5.62/6.02 X := Y
% 5.62/6.02 Y := X
% 5.62/6.02 end
% 5.62/6.02 permutation0:
% 5.62/6.02 0 ==> 0
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 eqswap: (20708) {G0,W11,D4,L1,V3,M1} { addition( addition( X, Y ), Z ) ==>
% 5.62/6.02 addition( X, addition( Y, Z ) ) }.
% 5.62/6.02 parent0[0]: (1) {G0,W11,D4,L1,V3,M1} I { addition( Z, addition( Y, X ) )
% 5.62/6.02 ==> addition( addition( Z, Y ), X ) }.
% 5.62/6.02 substitution0:
% 5.62/6.02 X := Z
% 5.62/6.02 Y := Y
% 5.62/6.02 Z := X
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 paramod: (20712) {G1,W17,D5,L1,V4,M1} { addition( addition( X,
% 5.62/6.02 multiplication( Y, Z ) ), multiplication( Y, T ) ) ==> addition( X,
% 5.62/6.02 multiplication( Y, addition( Z, T ) ) ) }.
% 5.62/6.02 parent0[0]: (7) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Y ),
% 5.62/6.02 multiplication( X, Z ) ) ==> multiplication( X, addition( Y, Z ) ) }.
% 5.62/6.02 parent1[0; 12]: (20708) {G0,W11,D4,L1,V3,M1} { addition( addition( X, Y )
% 5.62/6.02 , Z ) ==> addition( X, addition( Y, Z ) ) }.
% 5.62/6.02 substitution0:
% 5.62/6.02 X := Y
% 5.62/6.02 Y := Z
% 5.62/6.02 Z := T
% 5.62/6.02 end
% 5.62/6.02 substitution1:
% 5.62/6.02 X := X
% 5.62/6.02 Y := multiplication( Y, Z )
% 5.62/6.02 Z := multiplication( Y, T )
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 subsumption: (50) {G1,W17,D5,L1,V4,M1} P(7,1) { addition( addition( T,
% 5.62/6.02 multiplication( X, Y ) ), multiplication( X, Z ) ) ==> addition( T,
% 5.62/6.02 multiplication( X, addition( Y, Z ) ) ) }.
% 5.62/6.02 parent0: (20712) {G1,W17,D5,L1,V4,M1} { addition( addition( X,
% 5.62/6.02 multiplication( Y, Z ) ), multiplication( Y, T ) ) ==> addition( X,
% 5.62/6.02 multiplication( Y, addition( Z, T ) ) ) }.
% 5.62/6.02 substitution0:
% 5.62/6.02 X := T
% 5.62/6.02 Y := X
% 5.62/6.02 Z := Y
% 5.62/6.02 T := Z
% 5.62/6.02 end
% 5.62/6.02 permutation0:
% 5.62/6.02 0 ==> 0
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 eqswap: (20716) {G0,W13,D4,L1,V3,M1} { multiplication( X, addition( Y, Z )
% 5.62/6.02 ) ==> addition( multiplication( X, Y ), multiplication( X, Z ) ) }.
% 5.62/6.02 parent0[0]: (7) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Y ),
% 5.62/6.02 multiplication( X, Z ) ) ==> multiplication( X, addition( Y, Z ) ) }.
% 5.62/6.02 substitution0:
% 5.62/6.02 X := X
% 5.62/6.02 Y := Y
% 5.62/6.02 Z := Z
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 paramod: (20717) {G1,W11,D4,L1,V2,M1} { multiplication( X, addition( one,
% 5.62/6.02 Y ) ) ==> addition( X, multiplication( X, Y ) ) }.
% 5.62/6.02 parent0[0]: (5) {G0,W5,D3,L1,V1,M1} I { multiplication( X, one ) ==> X }.
% 5.62/6.02 parent1[0; 7]: (20716) {G0,W13,D4,L1,V3,M1} { multiplication( X, addition
% 5.62/6.02 ( Y, Z ) ) ==> addition( multiplication( X, Y ), multiplication( X, Z ) )
% 5.62/6.02 }.
% 5.62/6.02 substitution0:
% 5.62/6.02 X := X
% 5.62/6.02 end
% 5.62/6.02 substitution1:
% 5.62/6.02 X := X
% 5.62/6.02 Y := one
% 5.62/6.02 Z := Y
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 eqswap: (20719) {G1,W11,D4,L1,V2,M1} { addition( X, multiplication( X, Y )
% 5.62/6.02 ) ==> multiplication( X, addition( one, Y ) ) }.
% 5.62/6.02 parent0[0]: (20717) {G1,W11,D4,L1,V2,M1} { multiplication( X, addition(
% 5.62/6.02 one, Y ) ) ==> addition( X, multiplication( X, Y ) ) }.
% 5.62/6.02 substitution0:
% 5.62/6.02 X := X
% 5.62/6.02 Y := Y
% 5.62/6.02 end
% 5.62/6.02
% 5.62/6.02 subsumption: (51) {G1,W11,D4,L1,V2,M1} P(5,7) { addition( X, multiplication
% 5.62/6.02 ( X, Y ) ) = multiplication( X, addition( one, Y ) ) }.
% 5.62/6.02 parent0: (20719) {G1,W11,D4,L1,V2,M1} { addition( X, multiplication( X, Y
% 5.62/6.03 ) ) ==> multiplication( X, addition( one, Y ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20722) {G0,W13,D4,L1,V3,M1} { multiplication( X, addition( Y, Z )
% 5.62/6.03 ) ==> addition( multiplication( X, Y ), multiplication( X, Z ) ) }.
% 5.62/6.03 parent0[0]: (7) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Y ),
% 5.62/6.03 multiplication( X, Z ) ) ==> multiplication( X, addition( Y, Z ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 Z := Z
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20724) {G1,W11,D4,L1,V2,M1} { multiplication( X, addition( Y,
% 5.62/6.03 one ) ) ==> addition( multiplication( X, Y ), X ) }.
% 5.62/6.03 parent0[0]: (5) {G0,W5,D3,L1,V1,M1} I { multiplication( X, one ) ==> X }.
% 5.62/6.03 parent1[0; 10]: (20722) {G0,W13,D4,L1,V3,M1} { multiplication( X, addition
% 5.62/6.03 ( Y, Z ) ) ==> addition( multiplication( X, Y ), multiplication( X, Z ) )
% 5.62/6.03 }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 Z := one
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20726) {G1,W11,D4,L1,V2,M1} { addition( multiplication( X, Y ), X
% 5.62/6.03 ) ==> multiplication( X, addition( Y, one ) ) }.
% 5.62/6.03 parent0[0]: (20724) {G1,W11,D4,L1,V2,M1} { multiplication( X, addition( Y
% 5.62/6.03 , one ) ) ==> addition( multiplication( X, Y ), X ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (52) {G1,W11,D4,L1,V2,M1} P(5,7) { addition( multiplication( X
% 5.62/6.03 , Y ), X ) = multiplication( X, addition( Y, one ) ) }.
% 5.62/6.03 parent0: (20726) {G1,W11,D4,L1,V2,M1} { addition( multiplication( X, Y ),
% 5.62/6.03 X ) ==> multiplication( X, addition( Y, one ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20728) {G0,W11,D4,L1,V3,M1} { addition( addition( X, Y ), Z ) ==>
% 5.62/6.03 addition( X, addition( Y, Z ) ) }.
% 5.62/6.03 parent0[0]: (1) {G0,W11,D4,L1,V3,M1} I { addition( Z, addition( Y, X ) )
% 5.62/6.03 ==> addition( addition( Z, Y ), X ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := Z
% 5.62/6.03 Y := Y
% 5.62/6.03 Z := X
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20732) {G1,W17,D5,L1,V4,M1} { addition( addition( X,
% 5.62/6.03 multiplication( Y, Z ) ), multiplication( T, Z ) ) ==> addition( X,
% 5.62/6.03 multiplication( addition( Y, T ), Z ) ) }.
% 5.62/6.03 parent0[0]: (8) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Z ),
% 5.62/6.03 multiplication( Y, Z ) ) ==> multiplication( addition( X, Y ), Z ) }.
% 5.62/6.03 parent1[0; 12]: (20728) {G0,W11,D4,L1,V3,M1} { addition( addition( X, Y )
% 5.62/6.03 , Z ) ==> addition( X, addition( Y, Z ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := Y
% 5.62/6.03 Y := T
% 5.62/6.03 Z := Z
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 X := X
% 5.62/6.03 Y := multiplication( Y, Z )
% 5.62/6.03 Z := multiplication( T, Z )
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (63) {G1,W17,D5,L1,V4,M1} P(8,1) { addition( addition( T,
% 5.62/6.03 multiplication( X, Y ) ), multiplication( Z, Y ) ) ==> addition( T,
% 5.62/6.03 multiplication( addition( X, Z ), Y ) ) }.
% 5.62/6.03 parent0: (20732) {G1,W17,D5,L1,V4,M1} { addition( addition( X,
% 5.62/6.03 multiplication( Y, Z ) ), multiplication( T, Z ) ) ==> addition( X,
% 5.62/6.03 multiplication( addition( Y, T ), Z ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := T
% 5.62/6.03 Y := X
% 5.62/6.03 Z := Y
% 5.62/6.03 T := Z
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20736) {G0,W13,D4,L1,V3,M1} { multiplication( addition( X, Z ), Y
% 5.62/6.03 ) ==> addition( multiplication( X, Y ), multiplication( Z, Y ) ) }.
% 5.62/6.03 parent0[0]: (8) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Z ),
% 5.62/6.03 multiplication( Y, Z ) ) ==> multiplication( addition( X, Y ), Z ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Z
% 5.62/6.03 Z := Y
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20737) {G1,W11,D4,L1,V2,M1} { multiplication( addition( one, X )
% 5.62/6.03 , Y ) ==> addition( Y, multiplication( X, Y ) ) }.
% 5.62/6.03 parent0[0]: (6) {G0,W5,D3,L1,V1,M1} I { multiplication( one, X ) ==> X }.
% 5.62/6.03 parent1[0; 7]: (20736) {G0,W13,D4,L1,V3,M1} { multiplication( addition( X
% 5.62/6.03 , Z ), Y ) ==> addition( multiplication( X, Y ), multiplication( Z, Y ) )
% 5.62/6.03 }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := Y
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 X := one
% 5.62/6.03 Y := Y
% 5.62/6.03 Z := X
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20739) {G1,W11,D4,L1,V2,M1} { addition( Y, multiplication( X, Y )
% 5.62/6.03 ) ==> multiplication( addition( one, X ), Y ) }.
% 5.62/6.03 parent0[0]: (20737) {G1,W11,D4,L1,V2,M1} { multiplication( addition( one,
% 5.62/6.03 X ), Y ) ==> addition( Y, multiplication( X, Y ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (64) {G1,W11,D4,L1,V2,M1} P(6,8) { addition( X, multiplication
% 5.62/6.03 ( Y, X ) ) = multiplication( addition( one, Y ), X ) }.
% 5.62/6.03 parent0: (20739) {G1,W11,D4,L1,V2,M1} { addition( Y, multiplication( X, Y
% 5.62/6.03 ) ) ==> multiplication( addition( one, X ), Y ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := Y
% 5.62/6.03 Y := X
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20741) {G0,W8,D3,L2,V2,M2} { Y ==> addition( X, Y ), ! leq( X, Y
% 5.62/6.03 ) }.
% 5.62/6.03 parent0[1]: (11) {G0,W8,D3,L2,V2,M2} I { ! leq( X, Y ), addition( X, Y )
% 5.62/6.03 ==> Y }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20742) {G1,W8,D3,L2,V2,M2} { X ==> addition( X, Y ), ! leq( Y, X
% 5.62/6.03 ) }.
% 5.62/6.03 parent0[0]: (0) {G0,W7,D3,L1,V2,M1} I { addition( X, Y ) = addition( Y, X )
% 5.62/6.03 }.
% 5.62/6.03 parent1[0; 2]: (20741) {G0,W8,D3,L2,V2,M2} { Y ==> addition( X, Y ), ! leq
% 5.62/6.03 ( X, Y ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := Y
% 5.62/6.03 Y := X
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 X := Y
% 5.62/6.03 Y := X
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20745) {G1,W8,D3,L2,V2,M2} { addition( X, Y ) ==> X, ! leq( Y, X
% 5.62/6.03 ) }.
% 5.62/6.03 parent0[0]: (20742) {G1,W8,D3,L2,V2,M2} { X ==> addition( X, Y ), ! leq( Y
% 5.62/6.03 , X ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (80) {G1,W8,D3,L2,V2,M2} P(11,0) { addition( Y, X ) ==> Y, !
% 5.62/6.03 leq( X, Y ) }.
% 5.62/6.03 parent0: (20745) {G1,W8,D3,L2,V2,M2} { addition( X, Y ) ==> X, ! leq( Y, X
% 5.62/6.03 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := Y
% 5.62/6.03 Y := X
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 1 ==> 1
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20746) {G0,W8,D3,L2,V2,M2} { ! Y ==> addition( X, Y ), leq( X, Y
% 5.62/6.03 ) }.
% 5.62/6.03 parent0[0]: (12) {G0,W8,D3,L2,V2,M2} I { ! addition( X, Y ) ==> Y, leq( X,
% 5.62/6.03 Y ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20747) {G0,W5,D3,L1,V1,M1} { X ==> addition( X, X ) }.
% 5.62/6.03 parent0[0]: (3) {G0,W5,D3,L1,V1,M1} I { addition( X, X ) ==> X }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 resolution: (20748) {G1,W3,D2,L1,V1,M1} { leq( X, X ) }.
% 5.62/6.03 parent0[0]: (20746) {G0,W8,D3,L2,V2,M2} { ! Y ==> addition( X, Y ), leq( X
% 5.62/6.03 , Y ) }.
% 5.62/6.03 parent1[0]: (20747) {G0,W5,D3,L1,V1,M1} { X ==> addition( X, X ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := X
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 X := X
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (149) {G1,W3,D2,L1,V1,M1} R(12,3) { leq( X, X ) }.
% 5.62/6.03 parent0: (20748) {G1,W3,D2,L1,V1,M1} { leq( X, X ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20750) {G0,W8,D3,L2,V2,M2} { ! Y ==> addition( X, Y ), leq( X, Y
% 5.62/6.03 ) }.
% 5.62/6.03 parent0[0]: (12) {G0,W8,D3,L2,V2,M2} I { ! addition( X, Y ) ==> Y, leq( X,
% 5.62/6.03 Y ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20751) {G1,W14,D4,L2,V3,M2} { ! addition( X, Y ) ==> addition(
% 5.62/6.03 addition( Z, X ), Y ), leq( Z, addition( X, Y ) ) }.
% 5.62/6.03 parent0[0]: (1) {G0,W11,D4,L1,V3,M1} I { addition( Z, addition( Y, X ) )
% 5.62/6.03 ==> addition( addition( Z, Y ), X ) }.
% 5.62/6.03 parent1[0; 5]: (20750) {G0,W8,D3,L2,V2,M2} { ! Y ==> addition( X, Y ), leq
% 5.62/6.03 ( X, Y ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := Y
% 5.62/6.03 Y := X
% 5.62/6.03 Z := Z
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 X := Z
% 5.62/6.03 Y := addition( X, Y )
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20752) {G1,W14,D4,L2,V3,M2} { ! addition( addition( Z, X ), Y )
% 5.62/6.03 ==> addition( X, Y ), leq( Z, addition( X, Y ) ) }.
% 5.62/6.03 parent0[0]: (20751) {G1,W14,D4,L2,V3,M2} { ! addition( X, Y ) ==> addition
% 5.62/6.03 ( addition( Z, X ), Y ), leq( Z, addition( X, Y ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 Z := Z
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (154) {G1,W14,D4,L2,V3,M2} P(1,12) { ! addition( addition( X,
% 5.62/6.03 Y ), Z ) ==> addition( Y, Z ), leq( X, addition( Y, Z ) ) }.
% 5.62/6.03 parent0: (20752) {G1,W14,D4,L2,V3,M2} { ! addition( addition( Z, X ), Y )
% 5.62/6.03 ==> addition( X, Y ), leq( Z, addition( X, Y ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := Y
% 5.62/6.03 Y := Z
% 5.62/6.03 Z := X
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 1 ==> 1
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 resolution: (20753) {G1,W4,D3,L1,V0,M1} { complement( skol1( skol3 ),
% 5.62/6.03 skol3 ) }.
% 5.62/6.03 parent0[0]: (13) {G0,W6,D3,L2,V1,M2} I { ! test( X ), complement( skol1( X
% 5.62/6.03 ), X ) }.
% 5.62/6.03 parent1[0]: (26) {G0,W2,D2,L1,V0,M1} I { test( skol3 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := skol3
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (183) {G1,W4,D3,L1,V0,M1} R(13,26) { complement( skol1( skol3
% 5.62/6.03 ), skol3 ) }.
% 5.62/6.03 parent0: (20753) {G1,W4,D3,L1,V0,M1} { complement( skol1( skol3 ), skol3 )
% 5.62/6.03 }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 resolution: (20754) {G1,W4,D3,L1,V0,M1} { complement( skol1( skol2 ),
% 5.62/6.03 skol2 ) }.
% 5.62/6.03 parent0[0]: (13) {G0,W6,D3,L2,V1,M2} I { ! test( X ), complement( skol1( X
% 5.62/6.03 ), X ) }.
% 5.62/6.03 parent1[0]: (27) {G0,W2,D2,L1,V0,M1} I { test( skol2 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := skol2
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (184) {G1,W4,D3,L1,V0,M1} R(13,27) { complement( skol1( skol2
% 5.62/6.03 ), skol2 ) }.
% 5.62/6.03 parent0: (20754) {G1,W4,D3,L1,V0,M1} { complement( skol1( skol2 ), skol2 )
% 5.62/6.03 }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 resolution: (20755) {G1,W4,D3,L1,V0,M1} { alpha1( skol3, skol1( skol3 ) )
% 5.62/6.03 }.
% 5.62/6.03 parent0[0]: (16) {G0,W6,D2,L2,V2,M2} I { ! complement( Y, X ), alpha1( X, Y
% 5.62/6.03 ) }.
% 5.62/6.03 parent1[0]: (183) {G1,W4,D3,L1,V0,M1} R(13,26) { complement( skol1( skol3 )
% 5.62/6.03 , skol3 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := skol3
% 5.62/6.03 Y := skol1( skol3 )
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (187) {G2,W4,D3,L1,V0,M1} R(183,16) { alpha1( skol3, skol1(
% 5.62/6.03 skol3 ) ) }.
% 5.62/6.03 parent0: (20755) {G1,W4,D3,L1,V0,M1} { alpha1( skol3, skol1( skol3 ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 resolution: (20756) {G1,W4,D3,L1,V0,M1} { alpha1( skol2, skol1( skol2 ) )
% 5.62/6.03 }.
% 5.62/6.03 parent0[0]: (16) {G0,W6,D2,L2,V2,M2} I { ! complement( Y, X ), alpha1( X, Y
% 5.62/6.03 ) }.
% 5.62/6.03 parent1[0]: (184) {G1,W4,D3,L1,V0,M1} R(13,27) { complement( skol1( skol2 )
% 5.62/6.03 , skol2 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := skol2
% 5.62/6.03 Y := skol1( skol2 )
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (191) {G2,W4,D3,L1,V0,M1} R(184,16) { alpha1( skol2, skol1(
% 5.62/6.03 skol2 ) ) }.
% 5.62/6.03 parent0: (20756) {G1,W4,D3,L1,V0,M1} { alpha1( skol2, skol1( skol2 ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20757) {G0,W8,D3,L2,V2,M2} { zero ==> multiplication( X, Y ), !
% 5.62/6.03 complement( Y, X ) }.
% 5.62/6.03 parent0[1]: (15) {G0,W8,D3,L2,V2,M2} I { ! complement( Y, X ),
% 5.62/6.03 multiplication( X, Y ) ==> zero }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 resolution: (20758) {G1,W6,D4,L1,V0,M1} { zero ==> multiplication( skol2,
% 5.62/6.03 skol1( skol2 ) ) }.
% 5.62/6.03 parent0[1]: (20757) {G0,W8,D3,L2,V2,M2} { zero ==> multiplication( X, Y )
% 5.62/6.03 , ! complement( Y, X ) }.
% 5.62/6.03 parent1[0]: (184) {G1,W4,D3,L1,V0,M1} R(13,27) { complement( skol1( skol2 )
% 5.62/6.03 , skol2 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := skol2
% 5.62/6.03 Y := skol1( skol2 )
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20759) {G1,W6,D4,L1,V0,M1} { multiplication( skol2, skol1( skol2
% 5.62/6.03 ) ) ==> zero }.
% 5.62/6.03 parent0[0]: (20758) {G1,W6,D4,L1,V0,M1} { zero ==> multiplication( skol2,
% 5.62/6.03 skol1( skol2 ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (194) {G2,W6,D4,L1,V0,M1} R(15,184) { multiplication( skol2,
% 5.62/6.03 skol1( skol2 ) ) ==> zero }.
% 5.62/6.03 parent0: (20759) {G1,W6,D4,L1,V0,M1} { multiplication( skol2, skol1( skol2
% 5.62/6.03 ) ) ==> zero }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20760) {G0,W8,D3,L2,V2,M2} { zero ==> multiplication( X, Y ), !
% 5.62/6.03 complement( Y, X ) }.
% 5.62/6.03 parent0[1]: (15) {G0,W8,D3,L2,V2,M2} I { ! complement( Y, X ),
% 5.62/6.03 multiplication( X, Y ) ==> zero }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 resolution: (20761) {G1,W6,D4,L1,V0,M1} { zero ==> multiplication( skol3,
% 5.62/6.03 skol1( skol3 ) ) }.
% 5.62/6.03 parent0[1]: (20760) {G0,W8,D3,L2,V2,M2} { zero ==> multiplication( X, Y )
% 5.62/6.03 , ! complement( Y, X ) }.
% 5.62/6.03 parent1[0]: (183) {G1,W4,D3,L1,V0,M1} R(13,26) { complement( skol1( skol3 )
% 5.62/6.03 , skol3 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := skol3
% 5.62/6.03 Y := skol1( skol3 )
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20762) {G1,W6,D4,L1,V0,M1} { multiplication( skol3, skol1( skol3
% 5.62/6.03 ) ) ==> zero }.
% 5.62/6.03 parent0[0]: (20761) {G1,W6,D4,L1,V0,M1} { zero ==> multiplication( skol3,
% 5.62/6.03 skol1( skol3 ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (195) {G2,W6,D4,L1,V0,M1} R(15,183) { multiplication( skol3,
% 5.62/6.03 skol1( skol3 ) ) ==> zero }.
% 5.62/6.03 parent0: (20762) {G1,W6,D4,L1,V0,M1} { multiplication( skol3, skol1( skol3
% 5.62/6.03 ) ) ==> zero }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20763) {G0,W8,D3,L2,V2,M2} { zero ==> multiplication( X, Y ), !
% 5.62/6.03 alpha1( Y, X ) }.
% 5.62/6.03 parent0[1]: (18) {G0,W8,D3,L2,V2,M2} I { ! alpha1( X, Y ), multiplication(
% 5.62/6.03 Y, X ) ==> zero }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := Y
% 5.62/6.03 Y := X
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 resolution: (20764) {G1,W6,D4,L1,V0,M1} { zero ==> multiplication( skol1(
% 5.62/6.03 skol2 ), skol2 ) }.
% 5.62/6.03 parent0[1]: (20763) {G0,W8,D3,L2,V2,M2} { zero ==> multiplication( X, Y )
% 5.62/6.03 , ! alpha1( Y, X ) }.
% 5.62/6.03 parent1[0]: (191) {G2,W4,D3,L1,V0,M1} R(184,16) { alpha1( skol2, skol1(
% 5.62/6.03 skol2 ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := skol1( skol2 )
% 5.62/6.03 Y := skol2
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20765) {G1,W6,D4,L1,V0,M1} { multiplication( skol1( skol2 ),
% 5.62/6.03 skol2 ) ==> zero }.
% 5.62/6.03 parent0[0]: (20764) {G1,W6,D4,L1,V0,M1} { zero ==> multiplication( skol1(
% 5.62/6.03 skol2 ), skol2 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (236) {G3,W6,D4,L1,V0,M1} R(18,191) { multiplication( skol1(
% 5.62/6.03 skol2 ), skol2 ) ==> zero }.
% 5.62/6.03 parent0: (20765) {G1,W6,D4,L1,V0,M1} { multiplication( skol1( skol2 ),
% 5.62/6.03 skol2 ) ==> zero }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20766) {G0,W8,D3,L2,V2,M2} { zero ==> multiplication( X, Y ), !
% 5.62/6.03 alpha1( Y, X ) }.
% 5.62/6.03 parent0[1]: (18) {G0,W8,D3,L2,V2,M2} I { ! alpha1( X, Y ), multiplication(
% 5.62/6.03 Y, X ) ==> zero }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := Y
% 5.62/6.03 Y := X
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 resolution: (20767) {G1,W6,D4,L1,V0,M1} { zero ==> multiplication( skol1(
% 5.62/6.03 skol3 ), skol3 ) }.
% 5.62/6.03 parent0[1]: (20766) {G0,W8,D3,L2,V2,M2} { zero ==> multiplication( X, Y )
% 5.62/6.03 , ! alpha1( Y, X ) }.
% 5.62/6.03 parent1[0]: (187) {G2,W4,D3,L1,V0,M1} R(183,16) { alpha1( skol3, skol1(
% 5.62/6.03 skol3 ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := skol1( skol3 )
% 5.62/6.03 Y := skol3
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20768) {G1,W6,D4,L1,V0,M1} { multiplication( skol1( skol3 ),
% 5.62/6.03 skol3 ) ==> zero }.
% 5.62/6.03 parent0[0]: (20767) {G1,W6,D4,L1,V0,M1} { zero ==> multiplication( skol1(
% 5.62/6.03 skol3 ), skol3 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (237) {G3,W6,D4,L1,V0,M1} R(18,187) { multiplication( skol1(
% 5.62/6.03 skol3 ), skol3 ) ==> zero }.
% 5.62/6.03 parent0: (20768) {G1,W6,D4,L1,V0,M1} { multiplication( skol1( skol3 ),
% 5.62/6.03 skol3 ) ==> zero }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20769) {G0,W8,D3,L2,V2,M2} { one ==> addition( X, Y ), ! alpha1(
% 5.62/6.03 X, Y ) }.
% 5.62/6.03 parent0[1]: (19) {G0,W8,D3,L2,V2,M2} I { ! alpha1( X, Y ), addition( X, Y )
% 5.62/6.03 ==> one }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 resolution: (20770) {G1,W6,D4,L1,V0,M1} { one ==> addition( skol2, skol1(
% 5.62/6.03 skol2 ) ) }.
% 5.62/6.03 parent0[1]: (20769) {G0,W8,D3,L2,V2,M2} { one ==> addition( X, Y ), !
% 5.62/6.03 alpha1( X, Y ) }.
% 5.62/6.03 parent1[0]: (191) {G2,W4,D3,L1,V0,M1} R(184,16) { alpha1( skol2, skol1(
% 5.62/6.03 skol2 ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := skol2
% 5.62/6.03 Y := skol1( skol2 )
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20771) {G1,W6,D4,L1,V0,M1} { addition( skol2, skol1( skol2 ) )
% 5.62/6.03 ==> one }.
% 5.62/6.03 parent0[0]: (20770) {G1,W6,D4,L1,V0,M1} { one ==> addition( skol2, skol1(
% 5.62/6.03 skol2 ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (262) {G3,W6,D4,L1,V0,M1} R(19,191) { addition( skol2, skol1(
% 5.62/6.03 skol2 ) ) ==> one }.
% 5.62/6.03 parent0: (20771) {G1,W6,D4,L1,V0,M1} { addition( skol2, skol1( skol2 ) )
% 5.62/6.03 ==> one }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20772) {G0,W8,D3,L2,V2,M2} { one ==> addition( X, Y ), ! alpha1(
% 5.62/6.03 X, Y ) }.
% 5.62/6.03 parent0[1]: (19) {G0,W8,D3,L2,V2,M2} I { ! alpha1( X, Y ), addition( X, Y )
% 5.62/6.03 ==> one }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 resolution: (20773) {G1,W6,D4,L1,V0,M1} { one ==> addition( skol3, skol1(
% 5.62/6.03 skol3 ) ) }.
% 5.62/6.03 parent0[1]: (20772) {G0,W8,D3,L2,V2,M2} { one ==> addition( X, Y ), !
% 5.62/6.03 alpha1( X, Y ) }.
% 5.62/6.03 parent1[0]: (187) {G2,W4,D3,L1,V0,M1} R(183,16) { alpha1( skol3, skol1(
% 5.62/6.03 skol3 ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := skol3
% 5.62/6.03 Y := skol1( skol3 )
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20774) {G1,W6,D4,L1,V0,M1} { addition( skol3, skol1( skol3 ) )
% 5.62/6.03 ==> one }.
% 5.62/6.03 parent0[0]: (20773) {G1,W6,D4,L1,V0,M1} { one ==> addition( skol3, skol1(
% 5.62/6.03 skol3 ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (263) {G3,W6,D4,L1,V0,M1} R(19,187) { addition( skol3, skol1(
% 5.62/6.03 skol3 ) ) ==> one }.
% 5.62/6.03 parent0: (20774) {G1,W6,D4,L1,V0,M1} { addition( skol3, skol1( skol3 ) )
% 5.62/6.03 ==> one }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20775) {G0,W8,D3,L2,V2,M2} { ! Y ==> addition( X, Y ), leq( X, Y
% 5.62/6.03 ) }.
% 5.62/6.03 parent0[0]: (12) {G0,W8,D3,L2,V2,M2} I { ! addition( X, Y ) ==> Y, leq( X,
% 5.62/6.03 Y ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 resolution: (20778) {G1,W62,D8,L2,V0,M2} { ! leq( addition( addition(
% 5.62/6.03 multiplication( addition( skol3, c( skol3 ) ), skol2 ), multiplication(
% 5.62/6.03 addition( skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), c(
% 5.62/6.03 skol3 ) ) ), one ), ! addition( addition( multiplication( addition( skol3
% 5.62/6.03 , c( skol3 ) ), skol2 ), multiplication( addition( skol2, c( skol2 ) ),
% 5.62/6.03 skol3 ) ), multiplication( c( skol2 ), c( skol3 ) ) ) ==> addition( one,
% 5.62/6.03 addition( addition( multiplication( addition( skol3, c( skol3 ) ), skol2
% 5.62/6.03 ), multiplication( addition( skol2, c( skol2 ) ), skol3 ) ),
% 5.62/6.03 multiplication( c( skol2 ), c( skol3 ) ) ) ) }.
% 5.62/6.03 parent0[0]: (28) {G0,W42,D7,L2,V0,M2} I { ! leq( one, addition( addition(
% 5.62/6.03 multiplication( addition( skol3, c( skol3 ) ), skol2 ), multiplication(
% 5.62/6.03 addition( skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), c(
% 5.62/6.03 skol3 ) ) ) ), ! leq( addition( addition( multiplication( addition( skol3
% 5.62/6.03 , c( skol3 ) ), skol2 ), multiplication( addition( skol2, c( skol2 ) ),
% 5.62/6.03 skol3 ) ), multiplication( c( skol2 ), c( skol3 ) ) ), one ) }.
% 5.62/6.03 parent1[1]: (20775) {G0,W8,D3,L2,V2,M2} { ! Y ==> addition( X, Y ), leq( X
% 5.62/6.03 , Y ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 X := one
% 5.62/6.03 Y := addition( addition( multiplication( addition( skol3, c( skol3 ) ),
% 5.62/6.03 skol2 ), multiplication( addition( skol2, c( skol2 ) ), skol3 ) ),
% 5.62/6.03 multiplication( c( skol2 ), c( skol3 ) ) )
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20780) {G1,W62,D8,L2,V0,M2} { ! addition( addition(
% 5.62/6.03 multiplication( addition( skol3, c( skol3 ) ), skol2 ), multiplication(
% 5.62/6.03 addition( skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), c(
% 5.62/6.03 skol3 ) ) ) ==> addition( addition( one, addition( multiplication(
% 5.62/6.03 addition( skol3, c( skol3 ) ), skol2 ), multiplication( addition( skol2,
% 5.62/6.03 c( skol2 ) ), skol3 ) ) ), multiplication( c( skol2 ), c( skol3 ) ) ), !
% 5.62/6.03 leq( addition( addition( multiplication( addition( skol3, c( skol3 ) ),
% 5.62/6.03 skol2 ), multiplication( addition( skol2, c( skol2 ) ), skol3 ) ),
% 5.62/6.03 multiplication( c( skol2 ), c( skol3 ) ) ), one ) }.
% 5.62/6.03 parent0[0]: (1) {G0,W11,D4,L1,V3,M1} I { addition( Z, addition( Y, X ) )
% 5.62/6.03 ==> addition( addition( Z, Y ), X ) }.
% 5.62/6.03 parent1[1; 21]: (20778) {G1,W62,D8,L2,V0,M2} { ! leq( addition( addition(
% 5.62/6.03 multiplication( addition( skol3, c( skol3 ) ), skol2 ), multiplication(
% 5.62/6.03 addition( skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), c(
% 5.62/6.03 skol3 ) ) ), one ), ! addition( addition( multiplication( addition( skol3
% 5.62/6.03 , c( skol3 ) ), skol2 ), multiplication( addition( skol2, c( skol2 ) ),
% 5.62/6.03 skol3 ) ), multiplication( c( skol2 ), c( skol3 ) ) ) ==> addition( one,
% 5.62/6.03 addition( addition( multiplication( addition( skol3, c( skol3 ) ), skol2
% 5.62/6.03 ), multiplication( addition( skol2, c( skol2 ) ), skol3 ) ),
% 5.62/6.03 multiplication( c( skol2 ), c( skol3 ) ) ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := multiplication( c( skol2 ), c( skol3 ) )
% 5.62/6.03 Y := addition( multiplication( addition( skol3, c( skol3 ) ), skol2 ),
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) )
% 5.62/6.03 Z := one
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20782) {G1,W62,D8,L2,V0,M2} { ! addition( addition(
% 5.62/6.03 multiplication( addition( skol3, c( skol3 ) ), skol2 ), multiplication(
% 5.62/6.03 addition( skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), c(
% 5.62/6.03 skol3 ) ) ) ==> addition( addition( addition( one, multiplication(
% 5.62/6.03 addition( skol3, c( skol3 ) ), skol2 ) ), multiplication( addition( skol2
% 5.62/6.03 , c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), c( skol3 ) ) ), !
% 5.62/6.03 leq( addition( addition( multiplication( addition( skol3, c( skol3 ) ),
% 5.62/6.03 skol2 ), multiplication( addition( skol2, c( skol2 ) ), skol3 ) ),
% 5.62/6.03 multiplication( c( skol2 ), c( skol3 ) ) ), one ) }.
% 5.62/6.03 parent0[0]: (1) {G0,W11,D4,L1,V3,M1} I { addition( Z, addition( Y, X ) )
% 5.62/6.03 ==> addition( addition( Z, Y ), X ) }.
% 5.62/6.03 parent1[0; 22]: (20780) {G1,W62,D8,L2,V0,M2} { ! addition( addition(
% 5.62/6.03 multiplication( addition( skol3, c( skol3 ) ), skol2 ), multiplication(
% 5.62/6.03 addition( skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), c(
% 5.62/6.03 skol3 ) ) ) ==> addition( addition( one, addition( multiplication(
% 5.62/6.03 addition( skol3, c( skol3 ) ), skol2 ), multiplication( addition( skol2,
% 5.62/6.03 c( skol2 ) ), skol3 ) ) ), multiplication( c( skol2 ), c( skol3 ) ) ), !
% 5.62/6.03 leq( addition( addition( multiplication( addition( skol3, c( skol3 ) ),
% 5.62/6.03 skol2 ), multiplication( addition( skol2, c( skol2 ) ), skol3 ) ),
% 5.62/6.03 multiplication( c( skol2 ), c( skol3 ) ) ), one ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := multiplication( addition( skol2, c( skol2 ) ), skol3 )
% 5.62/6.03 Y := multiplication( addition( skol3, c( skol3 ) ), skol2 )
% 5.62/6.03 Z := one
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20783) {G1,W62,D8,L2,V0,M2} { ! addition( addition( addition( one
% 5.62/6.03 , multiplication( addition( skol3, c( skol3 ) ), skol2 ) ),
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), c( skol3 ) ) ) ==> addition( addition( multiplication(
% 5.62/6.03 addition( skol3, c( skol3 ) ), skol2 ), multiplication( addition( skol2,
% 5.62/6.03 c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), c( skol3 ) ) ), !
% 5.62/6.03 leq( addition( addition( multiplication( addition( skol3, c( skol3 ) ),
% 5.62/6.03 skol2 ), multiplication( addition( skol2, c( skol2 ) ), skol3 ) ),
% 5.62/6.03 multiplication( c( skol2 ), c( skol3 ) ) ), one ) }.
% 5.62/6.03 parent0[0]: (20782) {G1,W62,D8,L2,V0,M2} { ! addition( addition(
% 5.62/6.03 multiplication( addition( skol3, c( skol3 ) ), skol2 ), multiplication(
% 5.62/6.03 addition( skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), c(
% 5.62/6.03 skol3 ) ) ) ==> addition( addition( addition( one, multiplication(
% 5.62/6.03 addition( skol3, c( skol3 ) ), skol2 ) ), multiplication( addition( skol2
% 5.62/6.03 , c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), c( skol3 ) ) ), !
% 5.62/6.03 leq( addition( addition( multiplication( addition( skol3, c( skol3 ) ),
% 5.62/6.03 skol2 ), multiplication( addition( skol2, c( skol2 ) ), skol3 ) ),
% 5.62/6.03 multiplication( c( skol2 ), c( skol3 ) ) ), one ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (515) {G1,W62,D8,L2,V0,M2} R(28,12);d(1);d(1) { ! leq(
% 5.62/6.03 addition( addition( multiplication( addition( skol3, c( skol3 ) ), skol2
% 5.62/6.03 ), multiplication( addition( skol2, c( skol2 ) ), skol3 ) ),
% 5.62/6.03 multiplication( c( skol2 ), c( skol3 ) ) ), one ), ! addition( addition(
% 5.62/6.03 addition( one, multiplication( addition( skol3, c( skol3 ) ), skol2 ) ),
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), c( skol3 ) ) ) ==> addition( addition( multiplication(
% 5.62/6.03 addition( skol3, c( skol3 ) ), skol2 ), multiplication( addition( skol2,
% 5.62/6.03 c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), c( skol3 ) ) ) }.
% 5.62/6.03 parent0: (20783) {G1,W62,D8,L2,V0,M2} { ! addition( addition( addition(
% 5.62/6.03 one, multiplication( addition( skol3, c( skol3 ) ), skol2 ) ),
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), c( skol3 ) ) ) ==> addition( addition( multiplication(
% 5.62/6.03 addition( skol3, c( skol3 ) ), skol2 ), multiplication( addition( skol2,
% 5.62/6.03 c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), c( skol3 ) ) ), !
% 5.62/6.03 leq( addition( addition( multiplication( addition( skol3, c( skol3 ) ),
% 5.62/6.03 skol2 ), multiplication( addition( skol2, c( skol2 ) ), skol3 ) ),
% 5.62/6.03 multiplication( c( skol2 ), c( skol3 ) ) ), one ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 1
% 5.62/6.03 1 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20785) {G1,W9,D4,L1,V2,M1} { addition( X, Y ) ==> addition(
% 5.62/6.03 addition( X, Y ), Y ) }.
% 5.62/6.03 parent0[0]: (34) {G1,W9,D4,L1,V2,M1} P(3,1) { addition( addition( Y, X ), X
% 5.62/6.03 ) ==> addition( Y, X ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := Y
% 5.62/6.03 Y := X
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20787) {G2,W9,D4,L1,V0,M1} { addition( skol2, skol1( skol2 ) )
% 5.62/6.03 ==> addition( one, skol1( skol2 ) ) }.
% 5.62/6.03 parent0[0]: (262) {G3,W6,D4,L1,V0,M1} R(19,191) { addition( skol2, skol1(
% 5.62/6.03 skol2 ) ) ==> one }.
% 5.62/6.03 parent1[0; 6]: (20785) {G1,W9,D4,L1,V2,M1} { addition( X, Y ) ==> addition
% 5.62/6.03 ( addition( X, Y ), Y ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 X := skol2
% 5.62/6.03 Y := skol1( skol2 )
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20788) {G3,W6,D4,L1,V0,M1} { one ==> addition( one, skol1( skol2
% 5.62/6.03 ) ) }.
% 5.62/6.03 parent0[0]: (262) {G3,W6,D4,L1,V0,M1} R(19,191) { addition( skol2, skol1(
% 5.62/6.03 skol2 ) ) ==> one }.
% 5.62/6.03 parent1[0; 1]: (20787) {G2,W9,D4,L1,V0,M1} { addition( skol2, skol1( skol2
% 5.62/6.03 ) ) ==> addition( one, skol1( skol2 ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20790) {G3,W6,D4,L1,V0,M1} { addition( one, skol1( skol2 ) ) ==>
% 5.62/6.03 one }.
% 5.62/6.03 parent0[0]: (20788) {G3,W6,D4,L1,V0,M1} { one ==> addition( one, skol1(
% 5.62/6.03 skol2 ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (2384) {G4,W6,D4,L1,V0,M1} P(262,34) { addition( one, skol1(
% 5.62/6.03 skol2 ) ) ==> one }.
% 5.62/6.03 parent0: (20790) {G3,W6,D4,L1,V0,M1} { addition( one, skol1( skol2 ) ) ==>
% 5.62/6.03 one }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20792) {G3,W6,D4,L1,V0,M1} { one ==> addition( skol2, skol1(
% 5.62/6.03 skol2 ) ) }.
% 5.62/6.03 parent0[0]: (262) {G3,W6,D4,L1,V0,M1} R(19,191) { addition( skol2, skol1(
% 5.62/6.03 skol2 ) ) ==> one }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20793) {G1,W6,D4,L1,V0,M1} { one ==> addition( skol1( skol2 ),
% 5.62/6.03 skol2 ) }.
% 5.62/6.03 parent0[0]: (0) {G0,W7,D3,L1,V2,M1} I { addition( X, Y ) = addition( Y, X )
% 5.62/6.03 }.
% 5.62/6.03 parent1[0; 2]: (20792) {G3,W6,D4,L1,V0,M1} { one ==> addition( skol2,
% 5.62/6.03 skol1( skol2 ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := skol2
% 5.62/6.03 Y := skol1( skol2 )
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20796) {G1,W6,D4,L1,V0,M1} { addition( skol1( skol2 ), skol2 )
% 5.62/6.03 ==> one }.
% 5.62/6.03 parent0[0]: (20793) {G1,W6,D4,L1,V0,M1} { one ==> addition( skol1( skol2 )
% 5.62/6.03 , skol2 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (2391) {G4,W6,D4,L1,V0,M1} P(262,0) { addition( skol1( skol2 )
% 5.62/6.03 , skol2 ) ==> one }.
% 5.62/6.03 parent0: (20796) {G1,W6,D4,L1,V0,M1} { addition( skol1( skol2 ), skol2 )
% 5.62/6.03 ==> one }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20798) {G1,W11,D4,L1,V2,M1} { multiplication( addition( one, Y )
% 5.62/6.03 , X ) = addition( X, multiplication( Y, X ) ) }.
% 5.62/6.03 parent0[0]: (64) {G1,W11,D4,L1,V2,M1} P(6,8) { addition( X, multiplication
% 5.62/6.03 ( Y, X ) ) = multiplication( addition( one, Y ), X ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20800) {G2,W10,D5,L1,V1,M1} { multiplication( one, X ) =
% 5.62/6.03 addition( X, multiplication( skol1( skol2 ), X ) ) }.
% 5.62/6.03 parent0[0]: (2384) {G4,W6,D4,L1,V0,M1} P(262,34) { addition( one, skol1(
% 5.62/6.03 skol2 ) ) ==> one }.
% 5.62/6.03 parent1[0; 2]: (20798) {G1,W11,D4,L1,V2,M1} { multiplication( addition(
% 5.62/6.03 one, Y ), X ) = addition( X, multiplication( Y, X ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 X := X
% 5.62/6.03 Y := skol1( skol2 )
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20801) {G1,W8,D5,L1,V1,M1} { X = addition( X, multiplication(
% 5.62/6.03 skol1( skol2 ), X ) ) }.
% 5.62/6.03 parent0[0]: (6) {G0,W5,D3,L1,V1,M1} I { multiplication( one, X ) ==> X }.
% 5.62/6.03 parent1[0; 1]: (20800) {G2,W10,D5,L1,V1,M1} { multiplication( one, X ) =
% 5.62/6.03 addition( X, multiplication( skol1( skol2 ), X ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 X := X
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20802) {G1,W8,D5,L1,V1,M1} { addition( X, multiplication( skol1(
% 5.62/6.03 skol2 ), X ) ) = X }.
% 5.62/6.03 parent0[0]: (20801) {G1,W8,D5,L1,V1,M1} { X = addition( X, multiplication
% 5.62/6.03 ( skol1( skol2 ), X ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (2396) {G5,W8,D5,L1,V1,M1} P(2384,64);d(6) { addition( X,
% 5.62/6.03 multiplication( skol1( skol2 ), X ) ) ==> X }.
% 5.62/6.03 parent0: (20802) {G1,W8,D5,L1,V1,M1} { addition( X, multiplication( skol1
% 5.62/6.03 ( skol2 ), X ) ) = X }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20803) {G4,W6,D4,L1,V0,M1} { one ==> addition( skol1( skol2 ),
% 5.62/6.03 skol2 ) }.
% 5.62/6.03 parent0[0]: (2391) {G4,W6,D4,L1,V0,M1} P(262,0) { addition( skol1( skol2 )
% 5.62/6.03 , skol2 ) ==> one }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20805) {G0,W13,D3,L3,V2,M3} { ! one ==> addition( X, Y ), !
% 5.62/6.03 multiplication( Y, X ) ==> zero, alpha1( X, Y ) }.
% 5.62/6.03 parent0[1]: (20) {G0,W13,D3,L3,V2,M3} I { ! multiplication( Y, X ) ==> zero
% 5.62/6.03 , ! addition( X, Y ) ==> one, alpha1( X, Y ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20806) {G0,W13,D3,L3,V2,M3} { ! zero ==> multiplication( X, Y ),
% 5.62/6.03 ! one ==> addition( Y, X ), alpha1( Y, X ) }.
% 5.62/6.03 parent0[1]: (20805) {G0,W13,D3,L3,V2,M3} { ! one ==> addition( X, Y ), !
% 5.62/6.03 multiplication( Y, X ) ==> zero, alpha1( X, Y ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := Y
% 5.62/6.03 Y := X
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 resolution: (20808) {G1,W10,D4,L2,V0,M2} { ! zero ==> multiplication(
% 5.62/6.03 skol2, skol1( skol2 ) ), alpha1( skol1( skol2 ), skol2 ) }.
% 5.62/6.03 parent0[1]: (20806) {G0,W13,D3,L3,V2,M3} { ! zero ==> multiplication( X, Y
% 5.62/6.03 ), ! one ==> addition( Y, X ), alpha1( Y, X ) }.
% 5.62/6.03 parent1[0]: (20803) {G4,W6,D4,L1,V0,M1} { one ==> addition( skol1( skol2 )
% 5.62/6.03 , skol2 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := skol2
% 5.62/6.03 Y := skol1( skol2 )
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20809) {G2,W7,D3,L2,V0,M2} { ! zero ==> zero, alpha1( skol1(
% 5.62/6.03 skol2 ), skol2 ) }.
% 5.62/6.03 parent0[0]: (194) {G2,W6,D4,L1,V0,M1} R(15,184) { multiplication( skol2,
% 5.62/6.03 skol1( skol2 ) ) ==> zero }.
% 5.62/6.03 parent1[0; 3]: (20808) {G1,W10,D4,L2,V0,M2} { ! zero ==> multiplication(
% 5.62/6.03 skol2, skol1( skol2 ) ), alpha1( skol1( skol2 ), skol2 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqrefl: (20810) {G0,W4,D3,L1,V0,M1} { alpha1( skol1( skol2 ), skol2 ) }.
% 5.62/6.03 parent0[0]: (20809) {G2,W7,D3,L2,V0,M2} { ! zero ==> zero, alpha1( skol1(
% 5.62/6.03 skol2 ), skol2 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (2426) {G5,W4,D3,L1,V0,M1} R(2391,20);d(194);q { alpha1( skol1
% 5.62/6.03 ( skol2 ), skol2 ) }.
% 5.62/6.03 parent0: (20810) {G0,W4,D3,L1,V0,M1} { alpha1( skol1( skol2 ), skol2 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20812) {G1,W9,D4,L1,V2,M1} { addition( X, Y ) ==> addition(
% 5.62/6.03 addition( X, Y ), Y ) }.
% 5.62/6.03 parent0[0]: (34) {G1,W9,D4,L1,V2,M1} P(3,1) { addition( addition( Y, X ), X
% 5.62/6.03 ) ==> addition( Y, X ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := Y
% 5.62/6.03 Y := X
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20814) {G2,W8,D4,L1,V0,M1} { addition( skol1( skol2 ), skol2 )
% 5.62/6.03 ==> addition( one, skol2 ) }.
% 5.62/6.03 parent0[0]: (2391) {G4,W6,D4,L1,V0,M1} P(262,0) { addition( skol1( skol2 )
% 5.62/6.03 , skol2 ) ==> one }.
% 5.62/6.03 parent1[0; 6]: (20812) {G1,W9,D4,L1,V2,M1} { addition( X, Y ) ==> addition
% 5.62/6.03 ( addition( X, Y ), Y ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 X := skol1( skol2 )
% 5.62/6.03 Y := skol2
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20815) {G3,W5,D3,L1,V0,M1} { one ==> addition( one, skol2 ) }.
% 5.62/6.03 parent0[0]: (2391) {G4,W6,D4,L1,V0,M1} P(262,0) { addition( skol1( skol2 )
% 5.62/6.03 , skol2 ) ==> one }.
% 5.62/6.03 parent1[0; 1]: (20814) {G2,W8,D4,L1,V0,M1} { addition( skol1( skol2 ),
% 5.62/6.03 skol2 ) ==> addition( one, skol2 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20817) {G3,W5,D3,L1,V0,M1} { addition( one, skol2 ) ==> one }.
% 5.62/6.03 parent0[0]: (20815) {G3,W5,D3,L1,V0,M1} { one ==> addition( one, skol2 )
% 5.62/6.03 }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (2438) {G5,W5,D3,L1,V0,M1} P(2391,34) { addition( one, skol2 )
% 5.62/6.03 ==> one }.
% 5.62/6.03 parent0: (20817) {G3,W5,D3,L1,V0,M1} { addition( one, skol2 ) ==> one }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20819) {G0,W11,D3,L3,V2,M3} { ! zero ==> multiplication( X, Y ),
% 5.62/6.03 ! alpha1( X, Y ), complement( Y, X ) }.
% 5.62/6.03 parent0[0]: (17) {G0,W11,D3,L3,V2,M3} I { ! multiplication( X, Y ) ==> zero
% 5.62/6.03 , ! alpha1( X, Y ), complement( Y, X ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 resolution: (20821) {G1,W10,D4,L2,V0,M2} { ! zero ==> multiplication(
% 5.62/6.03 skol1( skol2 ), skol2 ), complement( skol2, skol1( skol2 ) ) }.
% 5.62/6.03 parent0[1]: (20819) {G0,W11,D3,L3,V2,M3} { ! zero ==> multiplication( X, Y
% 5.62/6.03 ), ! alpha1( X, Y ), complement( Y, X ) }.
% 5.62/6.03 parent1[0]: (2426) {G5,W4,D3,L1,V0,M1} R(2391,20);d(194);q { alpha1( skol1
% 5.62/6.03 ( skol2 ), skol2 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := skol1( skol2 )
% 5.62/6.03 Y := skol2
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20822) {G2,W7,D3,L2,V0,M2} { ! zero ==> zero, complement( skol2
% 5.62/6.03 , skol1( skol2 ) ) }.
% 5.62/6.03 parent0[0]: (236) {G3,W6,D4,L1,V0,M1} R(18,191) { multiplication( skol1(
% 5.62/6.03 skol2 ), skol2 ) ==> zero }.
% 5.62/6.03 parent1[0; 3]: (20821) {G1,W10,D4,L2,V0,M2} { ! zero ==> multiplication(
% 5.62/6.03 skol1( skol2 ), skol2 ), complement( skol2, skol1( skol2 ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqrefl: (20823) {G0,W4,D3,L1,V0,M1} { complement( skol2, skol1( skol2 ) )
% 5.62/6.03 }.
% 5.62/6.03 parent0[0]: (20822) {G2,W7,D3,L2,V0,M2} { ! zero ==> zero, complement(
% 5.62/6.03 skol2, skol1( skol2 ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (2441) {G6,W4,D3,L1,V0,M1} R(2426,17);d(236);q { complement(
% 5.62/6.03 skol2, skol1( skol2 ) ) }.
% 5.62/6.03 parent0: (20823) {G0,W4,D3,L1,V0,M1} { complement( skol2, skol1( skol2 ) )
% 5.62/6.03 }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20824) {G0,W9,D3,L3,V2,M3} { Y = c( X ), ! test( X ), !
% 5.62/6.03 complement( X, Y ) }.
% 5.62/6.03 parent0[2]: (22) {G0,W9,D3,L3,V2,M3} I { ! test( X ), ! complement( X, Y )
% 5.62/6.03 , c( X ) = Y }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 resolution: (20825) {G1,W7,D3,L2,V0,M2} { skol1( skol2 ) = c( skol2 ), !
% 5.62/6.03 test( skol2 ) }.
% 5.62/6.03 parent0[2]: (20824) {G0,W9,D3,L3,V2,M3} { Y = c( X ), ! test( X ), !
% 5.62/6.03 complement( X, Y ) }.
% 5.62/6.03 parent1[0]: (2441) {G6,W4,D3,L1,V0,M1} R(2426,17);d(236);q { complement(
% 5.62/6.03 skol2, skol1( skol2 ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := skol2
% 5.62/6.03 Y := skol1( skol2 )
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 resolution: (20826) {G1,W5,D3,L1,V0,M1} { skol1( skol2 ) = c( skol2 ) }.
% 5.62/6.03 parent0[1]: (20825) {G1,W7,D3,L2,V0,M2} { skol1( skol2 ) = c( skol2 ), !
% 5.62/6.03 test( skol2 ) }.
% 5.62/6.03 parent1[0]: (27) {G0,W2,D2,L1,V0,M1} I { test( skol2 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20827) {G1,W5,D3,L1,V0,M1} { c( skol2 ) = skol1( skol2 ) }.
% 5.62/6.03 parent0[0]: (20826) {G1,W5,D3,L1,V0,M1} { skol1( skol2 ) = c( skol2 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (2446) {G7,W5,D3,L1,V0,M1} R(2441,22);r(27) { c( skol2 ) ==>
% 5.62/6.03 skol1( skol2 ) }.
% 5.62/6.03 parent0: (20827) {G1,W5,D3,L1,V0,M1} { c( skol2 ) = skol1( skol2 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20829) {G1,W11,D4,L1,V2,M1} { multiplication( X, addition( one, Y
% 5.62/6.03 ) ) = addition( X, multiplication( X, Y ) ) }.
% 5.62/6.03 parent0[0]: (51) {G1,W11,D4,L1,V2,M1} P(5,7) { addition( X, multiplication
% 5.62/6.03 ( X, Y ) ) = multiplication( X, addition( one, Y ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20831) {G2,W9,D4,L1,V1,M1} { multiplication( X, one ) = addition
% 5.62/6.03 ( X, multiplication( X, skol2 ) ) }.
% 5.62/6.03 parent0[0]: (2438) {G5,W5,D3,L1,V0,M1} P(2391,34) { addition( one, skol2 )
% 5.62/6.03 ==> one }.
% 5.62/6.03 parent1[0; 3]: (20829) {G1,W11,D4,L1,V2,M1} { multiplication( X, addition
% 5.62/6.03 ( one, Y ) ) = addition( X, multiplication( X, Y ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 X := X
% 5.62/6.03 Y := skol2
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20832) {G1,W7,D4,L1,V1,M1} { X = addition( X, multiplication( X
% 5.62/6.03 , skol2 ) ) }.
% 5.62/6.03 parent0[0]: (5) {G0,W5,D3,L1,V1,M1} I { multiplication( X, one ) ==> X }.
% 5.62/6.03 parent1[0; 1]: (20831) {G2,W9,D4,L1,V1,M1} { multiplication( X, one ) =
% 5.62/6.03 addition( X, multiplication( X, skol2 ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 X := X
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20833) {G1,W7,D4,L1,V1,M1} { addition( X, multiplication( X,
% 5.62/6.03 skol2 ) ) = X }.
% 5.62/6.03 parent0[0]: (20832) {G1,W7,D4,L1,V1,M1} { X = addition( X, multiplication
% 5.62/6.03 ( X, skol2 ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (2503) {G6,W7,D4,L1,V1,M1} P(2438,51);d(5) { addition( X,
% 5.62/6.03 multiplication( X, skol2 ) ) ==> X }.
% 5.62/6.03 parent0: (20833) {G1,W7,D4,L1,V1,M1} { addition( X, multiplication( X,
% 5.62/6.03 skol2 ) ) = X }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20834) {G5,W5,D3,L1,V0,M1} { one ==> addition( one, skol2 ) }.
% 5.62/6.03 parent0[0]: (2438) {G5,W5,D3,L1,V0,M1} P(2391,34) { addition( one, skol2 )
% 5.62/6.03 ==> one }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20835) {G1,W5,D3,L1,V0,M1} { one ==> addition( skol2, one ) }.
% 5.62/6.03 parent0[0]: (0) {G0,W7,D3,L1,V2,M1} I { addition( X, Y ) = addition( Y, X )
% 5.62/6.03 }.
% 5.62/6.03 parent1[0; 2]: (20834) {G5,W5,D3,L1,V0,M1} { one ==> addition( one, skol2
% 5.62/6.03 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := one
% 5.62/6.03 Y := skol2
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20838) {G1,W5,D3,L1,V0,M1} { addition( skol2, one ) ==> one }.
% 5.62/6.03 parent0[0]: (20835) {G1,W5,D3,L1,V0,M1} { one ==> addition( skol2, one )
% 5.62/6.03 }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (2514) {G6,W5,D3,L1,V0,M1} P(2438,0) { addition( skol2, one )
% 5.62/6.03 ==> one }.
% 5.62/6.03 parent0: (20838) {G1,W5,D3,L1,V0,M1} { addition( skol2, one ) ==> one }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20839) {G3,W6,D4,L1,V0,M1} { one ==> addition( skol3, skol1(
% 5.62/6.03 skol3 ) ) }.
% 5.62/6.03 parent0[0]: (263) {G3,W6,D4,L1,V0,M1} R(19,187) { addition( skol3, skol1(
% 5.62/6.03 skol3 ) ) ==> one }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20840) {G1,W6,D4,L1,V0,M1} { one ==> addition( skol1( skol3 ),
% 5.62/6.03 skol3 ) }.
% 5.62/6.03 parent0[0]: (0) {G0,W7,D3,L1,V2,M1} I { addition( X, Y ) = addition( Y, X )
% 5.62/6.03 }.
% 5.62/6.03 parent1[0; 2]: (20839) {G3,W6,D4,L1,V0,M1} { one ==> addition( skol3,
% 5.62/6.03 skol1( skol3 ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := skol3
% 5.62/6.03 Y := skol1( skol3 )
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20843) {G1,W6,D4,L1,V0,M1} { addition( skol1( skol3 ), skol3 )
% 5.62/6.03 ==> one }.
% 5.62/6.03 parent0[0]: (20840) {G1,W6,D4,L1,V0,M1} { one ==> addition( skol1( skol3 )
% 5.62/6.03 , skol3 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (2747) {G4,W6,D4,L1,V0,M1} P(263,0) { addition( skol1( skol3 )
% 5.62/6.03 , skol3 ) ==> one }.
% 5.62/6.03 parent0: (20843) {G1,W6,D4,L1,V0,M1} { addition( skol1( skol3 ), skol3 )
% 5.62/6.03 ==> one }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20844) {G4,W6,D4,L1,V0,M1} { one ==> addition( skol1( skol3 ),
% 5.62/6.03 skol3 ) }.
% 5.62/6.03 parent0[0]: (2747) {G4,W6,D4,L1,V0,M1} P(263,0) { addition( skol1( skol3 )
% 5.62/6.03 , skol3 ) ==> one }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20846) {G0,W13,D3,L3,V2,M3} { ! one ==> addition( X, Y ), !
% 5.62/6.03 multiplication( Y, X ) ==> zero, alpha1( X, Y ) }.
% 5.62/6.03 parent0[1]: (20) {G0,W13,D3,L3,V2,M3} I { ! multiplication( Y, X ) ==> zero
% 5.62/6.03 , ! addition( X, Y ) ==> one, alpha1( X, Y ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20847) {G0,W13,D3,L3,V2,M3} { ! zero ==> multiplication( X, Y ),
% 5.62/6.03 ! one ==> addition( Y, X ), alpha1( Y, X ) }.
% 5.62/6.03 parent0[1]: (20846) {G0,W13,D3,L3,V2,M3} { ! one ==> addition( X, Y ), !
% 5.62/6.03 multiplication( Y, X ) ==> zero, alpha1( X, Y ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := Y
% 5.62/6.03 Y := X
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 resolution: (20849) {G1,W10,D4,L2,V0,M2} { ! zero ==> multiplication(
% 5.62/6.03 skol3, skol1( skol3 ) ), alpha1( skol1( skol3 ), skol3 ) }.
% 5.62/6.03 parent0[1]: (20847) {G0,W13,D3,L3,V2,M3} { ! zero ==> multiplication( X, Y
% 5.62/6.03 ), ! one ==> addition( Y, X ), alpha1( Y, X ) }.
% 5.62/6.03 parent1[0]: (20844) {G4,W6,D4,L1,V0,M1} { one ==> addition( skol1( skol3 )
% 5.62/6.03 , skol3 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := skol3
% 5.62/6.03 Y := skol1( skol3 )
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20850) {G2,W7,D3,L2,V0,M2} { ! zero ==> zero, alpha1( skol1(
% 5.62/6.03 skol3 ), skol3 ) }.
% 5.62/6.03 parent0[0]: (195) {G2,W6,D4,L1,V0,M1} R(15,183) { multiplication( skol3,
% 5.62/6.03 skol1( skol3 ) ) ==> zero }.
% 5.62/6.03 parent1[0; 3]: (20849) {G1,W10,D4,L2,V0,M2} { ! zero ==> multiplication(
% 5.62/6.03 skol3, skol1( skol3 ) ), alpha1( skol1( skol3 ), skol3 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqrefl: (20851) {G0,W4,D3,L1,V0,M1} { alpha1( skol1( skol3 ), skol3 ) }.
% 5.62/6.03 parent0[0]: (20850) {G2,W7,D3,L2,V0,M2} { ! zero ==> zero, alpha1( skol1(
% 5.62/6.03 skol3 ), skol3 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (2782) {G5,W4,D3,L1,V0,M1} R(2747,20);d(195);q { alpha1( skol1
% 5.62/6.03 ( skol3 ), skol3 ) }.
% 5.62/6.03 parent0: (20851) {G0,W4,D3,L1,V0,M1} { alpha1( skol1( skol3 ), skol3 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20853) {G1,W9,D4,L1,V2,M1} { addition( X, Y ) ==> addition(
% 5.62/6.03 addition( X, Y ), Y ) }.
% 5.62/6.03 parent0[0]: (34) {G1,W9,D4,L1,V2,M1} P(3,1) { addition( addition( Y, X ), X
% 5.62/6.03 ) ==> addition( Y, X ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := Y
% 5.62/6.03 Y := X
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20855) {G2,W8,D4,L1,V0,M1} { addition( skol1( skol3 ), skol3 )
% 5.62/6.03 ==> addition( one, skol3 ) }.
% 5.62/6.03 parent0[0]: (2747) {G4,W6,D4,L1,V0,M1} P(263,0) { addition( skol1( skol3 )
% 5.62/6.03 , skol3 ) ==> one }.
% 5.62/6.03 parent1[0; 6]: (20853) {G1,W9,D4,L1,V2,M1} { addition( X, Y ) ==> addition
% 5.62/6.03 ( addition( X, Y ), Y ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 X := skol1( skol3 )
% 5.62/6.03 Y := skol3
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20856) {G3,W5,D3,L1,V0,M1} { one ==> addition( one, skol3 ) }.
% 5.62/6.03 parent0[0]: (2747) {G4,W6,D4,L1,V0,M1} P(263,0) { addition( skol1( skol3 )
% 5.62/6.03 , skol3 ) ==> one }.
% 5.62/6.03 parent1[0; 1]: (20855) {G2,W8,D4,L1,V0,M1} { addition( skol1( skol3 ),
% 5.62/6.03 skol3 ) ==> addition( one, skol3 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20858) {G3,W5,D3,L1,V0,M1} { addition( one, skol3 ) ==> one }.
% 5.62/6.03 parent0[0]: (20856) {G3,W5,D3,L1,V0,M1} { one ==> addition( one, skol3 )
% 5.62/6.03 }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (2794) {G5,W5,D3,L1,V0,M1} P(2747,34) { addition( one, skol3 )
% 5.62/6.03 ==> one }.
% 5.62/6.03 parent0: (20858) {G3,W5,D3,L1,V0,M1} { addition( one, skol3 ) ==> one }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20860) {G0,W11,D3,L3,V2,M3} { ! zero ==> multiplication( X, Y ),
% 5.62/6.03 ! alpha1( X, Y ), complement( Y, X ) }.
% 5.62/6.03 parent0[0]: (17) {G0,W11,D3,L3,V2,M3} I { ! multiplication( X, Y ) ==> zero
% 5.62/6.03 , ! alpha1( X, Y ), complement( Y, X ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 resolution: (20862) {G1,W10,D4,L2,V0,M2} { ! zero ==> multiplication(
% 5.62/6.03 skol1( skol3 ), skol3 ), complement( skol3, skol1( skol3 ) ) }.
% 5.62/6.03 parent0[1]: (20860) {G0,W11,D3,L3,V2,M3} { ! zero ==> multiplication( X, Y
% 5.62/6.03 ), ! alpha1( X, Y ), complement( Y, X ) }.
% 5.62/6.03 parent1[0]: (2782) {G5,W4,D3,L1,V0,M1} R(2747,20);d(195);q { alpha1( skol1
% 5.62/6.03 ( skol3 ), skol3 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := skol1( skol3 )
% 5.62/6.03 Y := skol3
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20863) {G2,W7,D3,L2,V0,M2} { ! zero ==> zero, complement( skol3
% 5.62/6.03 , skol1( skol3 ) ) }.
% 5.62/6.03 parent0[0]: (237) {G3,W6,D4,L1,V0,M1} R(18,187) { multiplication( skol1(
% 5.62/6.03 skol3 ), skol3 ) ==> zero }.
% 5.62/6.03 parent1[0; 3]: (20862) {G1,W10,D4,L2,V0,M2} { ! zero ==> multiplication(
% 5.62/6.03 skol1( skol3 ), skol3 ), complement( skol3, skol1( skol3 ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqrefl: (20864) {G0,W4,D3,L1,V0,M1} { complement( skol3, skol1( skol3 ) )
% 5.62/6.03 }.
% 5.62/6.03 parent0[0]: (20863) {G2,W7,D3,L2,V0,M2} { ! zero ==> zero, complement(
% 5.62/6.03 skol3, skol1( skol3 ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (2797) {G6,W4,D3,L1,V0,M1} R(2782,17);d(237);q { complement(
% 5.62/6.03 skol3, skol1( skol3 ) ) }.
% 5.62/6.03 parent0: (20864) {G0,W4,D3,L1,V0,M1} { complement( skol3, skol1( skol3 ) )
% 5.62/6.03 }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20865) {G0,W9,D3,L3,V2,M3} { Y = c( X ), ! test( X ), !
% 5.62/6.03 complement( X, Y ) }.
% 5.62/6.03 parent0[2]: (22) {G0,W9,D3,L3,V2,M3} I { ! test( X ), ! complement( X, Y )
% 5.62/6.03 , c( X ) = Y }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 resolution: (20866) {G1,W7,D3,L2,V0,M2} { skol1( skol3 ) = c( skol3 ), !
% 5.62/6.03 test( skol3 ) }.
% 5.62/6.03 parent0[2]: (20865) {G0,W9,D3,L3,V2,M3} { Y = c( X ), ! test( X ), !
% 5.62/6.03 complement( X, Y ) }.
% 5.62/6.03 parent1[0]: (2797) {G6,W4,D3,L1,V0,M1} R(2782,17);d(237);q { complement(
% 5.62/6.03 skol3, skol1( skol3 ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := skol3
% 5.62/6.03 Y := skol1( skol3 )
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 resolution: (20867) {G1,W5,D3,L1,V0,M1} { skol1( skol3 ) = c( skol3 ) }.
% 5.62/6.03 parent0[1]: (20866) {G1,W7,D3,L2,V0,M2} { skol1( skol3 ) = c( skol3 ), !
% 5.62/6.03 test( skol3 ) }.
% 5.62/6.03 parent1[0]: (26) {G0,W2,D2,L1,V0,M1} I { test( skol3 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20868) {G1,W5,D3,L1,V0,M1} { c( skol3 ) = skol1( skol3 ) }.
% 5.62/6.03 parent0[0]: (20867) {G1,W5,D3,L1,V0,M1} { skol1( skol3 ) = c( skol3 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (2802) {G7,W5,D3,L1,V0,M1} R(2797,22);r(26) { c( skol3 ) ==>
% 5.62/6.03 skol1( skol3 ) }.
% 5.62/6.03 parent0: (20868) {G1,W5,D3,L1,V0,M1} { c( skol3 ) = skol1( skol3 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20870) {G1,W11,D4,L1,V2,M1} { multiplication( X, addition( one, Y
% 5.62/6.03 ) ) = addition( X, multiplication( X, Y ) ) }.
% 5.62/6.03 parent0[0]: (51) {G1,W11,D4,L1,V2,M1} P(5,7) { addition( X, multiplication
% 5.62/6.03 ( X, Y ) ) = multiplication( X, addition( one, Y ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20872) {G2,W9,D4,L1,V1,M1} { multiplication( X, one ) = addition
% 5.62/6.03 ( X, multiplication( X, skol3 ) ) }.
% 5.62/6.03 parent0[0]: (2794) {G5,W5,D3,L1,V0,M1} P(2747,34) { addition( one, skol3 )
% 5.62/6.03 ==> one }.
% 5.62/6.03 parent1[0; 3]: (20870) {G1,W11,D4,L1,V2,M1} { multiplication( X, addition
% 5.62/6.03 ( one, Y ) ) = addition( X, multiplication( X, Y ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 X := X
% 5.62/6.03 Y := skol3
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20873) {G1,W7,D4,L1,V1,M1} { X = addition( X, multiplication( X
% 5.62/6.03 , skol3 ) ) }.
% 5.62/6.03 parent0[0]: (5) {G0,W5,D3,L1,V1,M1} I { multiplication( X, one ) ==> X }.
% 5.62/6.03 parent1[0; 1]: (20872) {G2,W9,D4,L1,V1,M1} { multiplication( X, one ) =
% 5.62/6.03 addition( X, multiplication( X, skol3 ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 X := X
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20874) {G1,W7,D4,L1,V1,M1} { addition( X, multiplication( X,
% 5.62/6.03 skol3 ) ) = X }.
% 5.62/6.03 parent0[0]: (20873) {G1,W7,D4,L1,V1,M1} { X = addition( X, multiplication
% 5.62/6.03 ( X, skol3 ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (2859) {G6,W7,D4,L1,V1,M1} P(2794,51);d(5) { addition( X,
% 5.62/6.03 multiplication( X, skol3 ) ) ==> X }.
% 5.62/6.03 parent0: (20874) {G1,W7,D4,L1,V1,M1} { addition( X, multiplication( X,
% 5.62/6.03 skol3 ) ) = X }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20875) {G5,W5,D3,L1,V0,M1} { one ==> addition( one, skol3 ) }.
% 5.62/6.03 parent0[0]: (2794) {G5,W5,D3,L1,V0,M1} P(2747,34) { addition( one, skol3 )
% 5.62/6.03 ==> one }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20876) {G1,W5,D3,L1,V0,M1} { one ==> addition( skol3, one ) }.
% 5.62/6.03 parent0[0]: (0) {G0,W7,D3,L1,V2,M1} I { addition( X, Y ) = addition( Y, X )
% 5.62/6.03 }.
% 5.62/6.03 parent1[0; 2]: (20875) {G5,W5,D3,L1,V0,M1} { one ==> addition( one, skol3
% 5.62/6.03 ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := one
% 5.62/6.03 Y := skol3
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20879) {G1,W5,D3,L1,V0,M1} { addition( skol3, one ) ==> one }.
% 5.62/6.03 parent0[0]: (20876) {G1,W5,D3,L1,V0,M1} { one ==> addition( skol3, one )
% 5.62/6.03 }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (2870) {G6,W5,D3,L1,V0,M1} P(2794,0) { addition( skol3, one )
% 5.62/6.03 ==> one }.
% 5.62/6.03 parent0: (20879) {G1,W5,D3,L1,V0,M1} { addition( skol3, one ) ==> one }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20881) {G1,W11,D4,L1,V2,M1} { multiplication( X, addition( Y, one
% 5.62/6.03 ) ) = addition( multiplication( X, Y ), X ) }.
% 5.62/6.03 parent0[0]: (52) {G1,W11,D4,L1,V2,M1} P(5,7) { addition( multiplication( X
% 5.62/6.03 , Y ), X ) = multiplication( X, addition( Y, one ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20883) {G2,W9,D4,L1,V1,M1} { multiplication( X, one ) = addition
% 5.62/6.03 ( multiplication( X, skol3 ), X ) }.
% 5.62/6.03 parent0[0]: (2870) {G6,W5,D3,L1,V0,M1} P(2794,0) { addition( skol3, one )
% 5.62/6.03 ==> one }.
% 5.62/6.03 parent1[0; 3]: (20881) {G1,W11,D4,L1,V2,M1} { multiplication( X, addition
% 5.62/6.03 ( Y, one ) ) = addition( multiplication( X, Y ), X ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 X := X
% 5.62/6.03 Y := skol3
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20884) {G1,W7,D4,L1,V1,M1} { X = addition( multiplication( X,
% 5.62/6.03 skol3 ), X ) }.
% 5.62/6.03 parent0[0]: (5) {G0,W5,D3,L1,V1,M1} I { multiplication( X, one ) ==> X }.
% 5.62/6.03 parent1[0; 1]: (20883) {G2,W9,D4,L1,V1,M1} { multiplication( X, one ) =
% 5.62/6.03 addition( multiplication( X, skol3 ), X ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 X := X
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20885) {G1,W7,D4,L1,V1,M1} { addition( multiplication( X, skol3 )
% 5.62/6.03 , X ) = X }.
% 5.62/6.03 parent0[0]: (20884) {G1,W7,D4,L1,V1,M1} { X = addition( multiplication( X
% 5.62/6.03 , skol3 ), X ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (2875) {G7,W7,D4,L1,V1,M1} P(2870,52);d(5) { addition(
% 5.62/6.03 multiplication( X, skol3 ), X ) ==> X }.
% 5.62/6.03 parent0: (20885) {G1,W7,D4,L1,V1,M1} { addition( multiplication( X, skol3
% 5.62/6.03 ), X ) = X }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20887) {G1,W14,D4,L2,V3,M2} { ! addition( Y, Z ) ==> addition(
% 5.62/6.03 addition( X, Y ), Z ), leq( X, addition( Y, Z ) ) }.
% 5.62/6.03 parent0[0]: (154) {G1,W14,D4,L2,V3,M2} P(1,12) { ! addition( addition( X, Y
% 5.62/6.03 ), Z ) ==> addition( Y, Z ), leq( X, addition( Y, Z ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 Z := Z
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20890) {G1,W12,D3,L2,V2,M2} { ! addition( X, Y ) ==> addition( X
% 5.62/6.03 , Y ), leq( X, addition( X, Y ) ) }.
% 5.62/6.03 parent0[0]: (3) {G0,W5,D3,L1,V1,M1} I { addition( X, X ) ==> X }.
% 5.62/6.03 parent1[0; 6]: (20887) {G1,W14,D4,L2,V3,M2} { ! addition( Y, Z ) ==>
% 5.62/6.03 addition( addition( X, Y ), Z ), leq( X, addition( Y, Z ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 X := X
% 5.62/6.03 Y := X
% 5.62/6.03 Z := Y
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqrefl: (20893) {G0,W5,D3,L1,V2,M1} { leq( X, addition( X, Y ) ) }.
% 5.62/6.03 parent0[0]: (20890) {G1,W12,D3,L2,V2,M2} { ! addition( X, Y ) ==> addition
% 5.62/6.03 ( X, Y ), leq( X, addition( X, Y ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (4122) {G2,W5,D3,L1,V2,M1} P(3,154);q { leq( X, addition( X, Y
% 5.62/6.03 ) ) }.
% 5.62/6.03 parent0: (20893) {G0,W5,D3,L1,V2,M1} { leq( X, addition( X, Y ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20895) {G1,W7,D4,L1,V3,M1} { leq( X, addition( addition( X, Y )
% 5.62/6.03 , Z ) ) }.
% 5.62/6.03 parent0[0]: (1) {G0,W11,D4,L1,V3,M1} I { addition( Z, addition( Y, X ) )
% 5.62/6.03 ==> addition( addition( Z, Y ), X ) }.
% 5.62/6.03 parent1[0; 2]: (4122) {G2,W5,D3,L1,V2,M1} P(3,154);q { leq( X, addition( X
% 5.62/6.03 , Y ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := Z
% 5.62/6.03 Y := Y
% 5.62/6.03 Z := X
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 X := X
% 5.62/6.03 Y := addition( Y, Z )
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (4179) {G3,W7,D4,L1,V3,M1} P(1,4122) { leq( X, addition(
% 5.62/6.03 addition( X, Y ), Z ) ) }.
% 5.62/6.03 parent0: (20895) {G1,W7,D4,L1,V3,M1} { leq( X, addition( addition( X, Y )
% 5.62/6.03 , Z ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 Z := Z
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20897) {G4,W7,D3,L1,V2,M1} { leq( multiplication( X, skol3 ),
% 5.62/6.03 addition( X, Y ) ) }.
% 5.62/6.03 parent0[0]: (2875) {G7,W7,D4,L1,V1,M1} P(2870,52);d(5) { addition(
% 5.62/6.03 multiplication( X, skol3 ), X ) ==> X }.
% 5.62/6.03 parent1[0; 5]: (4179) {G3,W7,D4,L1,V3,M1} P(1,4122) { leq( X, addition(
% 5.62/6.03 addition( X, Y ), Z ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 X := multiplication( X, skol3 )
% 5.62/6.03 Y := X
% 5.62/6.03 Z := Y
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (18502) {G8,W7,D3,L1,V2,M1} P(2875,4179) { leq( multiplication
% 5.62/6.03 ( X, skol3 ), addition( X, Y ) ) }.
% 5.62/6.03 parent0: (20897) {G4,W7,D3,L1,V2,M1} { leq( multiplication( X, skol3 ),
% 5.62/6.03 addition( X, Y ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20899) {G7,W5,D3,L1,V0,M1} { leq( multiplication( skol2, skol3 )
% 5.62/6.03 , one ) }.
% 5.62/6.03 parent0[0]: (2514) {G6,W5,D3,L1,V0,M1} P(2438,0) { addition( skol2, one )
% 5.62/6.03 ==> one }.
% 5.62/6.03 parent1[0; 4]: (18502) {G8,W7,D3,L1,V2,M1} P(2875,4179) { leq(
% 5.62/6.03 multiplication( X, skol3 ), addition( X, Y ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 X := skol2
% 5.62/6.03 Y := one
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (18564) {G9,W5,D3,L1,V0,M1} P(2514,18502) { leq(
% 5.62/6.03 multiplication( skol2, skol3 ), one ) }.
% 5.62/6.03 parent0: (20899) {G7,W5,D3,L1,V0,M1} { leq( multiplication( skol2, skol3 )
% 5.62/6.03 , one ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20900) {G1,W8,D3,L2,V2,M2} { X ==> addition( X, Y ), ! leq( Y, X
% 5.62/6.03 ) }.
% 5.62/6.03 parent0[0]: (80) {G1,W8,D3,L2,V2,M2} P(11,0) { addition( Y, X ) ==> Y, !
% 5.62/6.03 leq( X, Y ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := Y
% 5.62/6.03 Y := X
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 resolution: (20901) {G2,W7,D4,L1,V0,M1} { one ==> addition( one,
% 5.62/6.03 multiplication( skol2, skol3 ) ) }.
% 5.62/6.03 parent0[1]: (20900) {G1,W8,D3,L2,V2,M2} { X ==> addition( X, Y ), ! leq( Y
% 5.62/6.03 , X ) }.
% 5.62/6.03 parent1[0]: (18564) {G9,W5,D3,L1,V0,M1} P(2514,18502) { leq( multiplication
% 5.62/6.03 ( skol2, skol3 ), one ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := one
% 5.62/6.03 Y := multiplication( skol2, skol3 )
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20902) {G2,W7,D4,L1,V0,M1} { addition( one, multiplication( skol2
% 5.62/6.03 , skol3 ) ) ==> one }.
% 5.62/6.03 parent0[0]: (20901) {G2,W7,D4,L1,V0,M1} { one ==> addition( one,
% 5.62/6.03 multiplication( skol2, skol3 ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (18605) {G10,W7,D4,L1,V0,M1} R(18564,80) { addition( one,
% 5.62/6.03 multiplication( skol2, skol3 ) ) ==> one }.
% 5.62/6.03 parent0: (20902) {G2,W7,D4,L1,V0,M1} { addition( one, multiplication(
% 5.62/6.03 skol2, skol3 ) ) ==> one }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20904) {G1,W17,D5,L1,V4,M1} { addition( X, multiplication(
% 5.62/6.03 addition( Y, T ), Z ) ) ==> addition( addition( X, multiplication( Y, Z )
% 5.62/6.03 ), multiplication( T, Z ) ) }.
% 5.62/6.03 parent0[0]: (63) {G1,W17,D5,L1,V4,M1} P(8,1) { addition( addition( T,
% 5.62/6.03 multiplication( X, Y ) ), multiplication( Z, Y ) ) ==> addition( T,
% 5.62/6.03 multiplication( addition( X, Z ), Y ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := Y
% 5.62/6.03 Y := Z
% 5.62/6.03 Z := T
% 5.62/6.03 T := X
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20910) {G2,W13,D5,L1,V2,M1} { addition( X, multiplication(
% 5.62/6.03 addition( X, Y ), skol3 ) ) ==> addition( X, multiplication( Y, skol3 ) )
% 5.62/6.03 }.
% 5.62/6.03 parent0[0]: (2859) {G6,W7,D4,L1,V1,M1} P(2794,51);d(5) { addition( X,
% 5.62/6.03 multiplication( X, skol3 ) ) ==> X }.
% 5.62/6.03 parent1[0; 9]: (20904) {G1,W17,D5,L1,V4,M1} { addition( X, multiplication
% 5.62/6.03 ( addition( Y, T ), Z ) ) ==> addition( addition( X, multiplication( Y, Z
% 5.62/6.03 ) ), multiplication( T, Z ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 X := X
% 5.62/6.03 Y := X
% 5.62/6.03 Z := skol3
% 5.62/6.03 T := Y
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (18875) {G7,W13,D5,L1,V2,M1} P(2859,63) { addition( X,
% 5.62/6.03 multiplication( addition( X, Y ), skol3 ) ) ==> addition( X,
% 5.62/6.03 multiplication( Y, skol3 ) ) }.
% 5.62/6.03 parent0: (20910) {G2,W13,D5,L1,V2,M1} { addition( X, multiplication(
% 5.62/6.03 addition( X, Y ), skol3 ) ) ==> addition( X, multiplication( Y, skol3 ) )
% 5.62/6.03 }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 Y := Y
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqswap: (20916) {G1,W17,D5,L1,V4,M1} { addition( X, multiplication(
% 5.62/6.03 addition( Y, T ), Z ) ) ==> addition( addition( X, multiplication( Y, Z )
% 5.62/6.03 ), multiplication( T, Z ) ) }.
% 5.62/6.03 parent0[0]: (63) {G1,W17,D5,L1,V4,M1} P(8,1) { addition( addition( T,
% 5.62/6.03 multiplication( X, Y ) ), multiplication( Z, Y ) ) ==> addition( T,
% 5.62/6.03 multiplication( addition( X, Z ), Y ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := Y
% 5.62/6.03 Y := Z
% 5.62/6.03 Z := T
% 5.62/6.03 T := X
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20918) {G2,W13,D5,L1,V1,M1} { addition( one, multiplication(
% 5.62/6.03 addition( skol2, X ), skol3 ) ) ==> addition( one, multiplication( X,
% 5.62/6.03 skol3 ) ) }.
% 5.62/6.03 parent0[0]: (18605) {G10,W7,D4,L1,V0,M1} R(18564,80) { addition( one,
% 5.62/6.03 multiplication( skol2, skol3 ) ) ==> one }.
% 5.62/6.03 parent1[0; 9]: (20916) {G1,W17,D5,L1,V4,M1} { addition( X, multiplication
% 5.62/6.03 ( addition( Y, T ), Z ) ) ==> addition( addition( X, multiplication( Y, Z
% 5.62/6.03 ) ), multiplication( T, Z ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 X := one
% 5.62/6.03 Y := skol2
% 5.62/6.03 Z := skol3
% 5.62/6.03 T := X
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (19903) {G11,W13,D5,L1,V1,M1} P(18605,63) { addition( one,
% 5.62/6.03 multiplication( addition( skol2, X ), skol3 ) ) ==> addition( one,
% 5.62/6.03 multiplication( X, skol3 ) ) }.
% 5.62/6.03 parent0: (20918) {G2,W13,D5,L1,V1,M1} { addition( one, multiplication(
% 5.62/6.03 addition( skol2, X ), skol3 ) ) ==> addition( one, multiplication( X,
% 5.62/6.03 skol3 ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := X
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 0 ==> 0
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 *** allocated 384427 integers for termspace/termends
% 5.62/6.03 paramod: (20950) {G2,W62,D8,L2,V0,M2} { ! addition( addition( addition(
% 5.62/6.03 one, multiplication( addition( skol3, c( skol3 ) ), skol2 ) ),
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), c( skol3 ) ) ) ==> addition( addition( multiplication(
% 5.62/6.03 addition( skol3, c( skol3 ) ), skol2 ), multiplication( addition( skol2,
% 5.62/6.03 c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), skol1( skol3 ) ) ),
% 5.62/6.03 ! leq( addition( addition( multiplication( addition( skol3, c( skol3 ) )
% 5.62/6.03 , skol2 ), multiplication( addition( skol2, c( skol2 ) ), skol3 ) ),
% 5.62/6.03 multiplication( c( skol2 ), c( skol3 ) ) ), one ) }.
% 5.62/6.03 parent0[0]: (2802) {G7,W5,D3,L1,V0,M1} R(2797,22);r(26) { c( skol3 ) ==>
% 5.62/6.03 skol1( skol3 ) }.
% 5.62/6.03 parent1[1; 40]: (515) {G1,W62,D8,L2,V0,M2} R(28,12);d(1);d(1) { ! leq(
% 5.62/6.03 addition( addition( multiplication( addition( skol3, c( skol3 ) ), skol2
% 5.62/6.03 ), multiplication( addition( skol2, c( skol2 ) ), skol3 ) ),
% 5.62/6.03 multiplication( c( skol2 ), c( skol3 ) ) ), one ), ! addition( addition(
% 5.62/6.03 addition( one, multiplication( addition( skol3, c( skol3 ) ), skol2 ) ),
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), c( skol3 ) ) ) ==> addition( addition( multiplication(
% 5.62/6.03 addition( skol3, c( skol3 ) ), skol2 ), multiplication( addition( skol2,
% 5.62/6.03 c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), c( skol3 ) ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20971) {G3,W62,D8,L2,V0,M2} { ! leq( addition( addition(
% 5.62/6.03 multiplication( addition( skol3, c( skol3 ) ), skol2 ), multiplication(
% 5.62/6.03 addition( skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ),
% 5.62/6.03 skol1( skol3 ) ) ), one ), ! addition( addition( addition( one,
% 5.62/6.03 multiplication( addition( skol3, c( skol3 ) ), skol2 ) ), multiplication
% 5.62/6.03 ( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), c
% 5.62/6.03 ( skol3 ) ) ) ==> addition( addition( multiplication( addition( skol3, c
% 5.62/6.03 ( skol3 ) ), skol2 ), multiplication( addition( skol2, c( skol2 ) ),
% 5.62/6.03 skol3 ) ), multiplication( c( skol2 ), skol1( skol3 ) ) ) }.
% 5.62/6.03 parent0[0]: (2802) {G7,W5,D3,L1,V0,M1} R(2797,22);r(26) { c( skol3 ) ==>
% 5.62/6.03 skol1( skol3 ) }.
% 5.62/6.03 parent1[1; 19]: (20950) {G2,W62,D8,L2,V0,M2} { ! addition( addition(
% 5.62/6.03 addition( one, multiplication( addition( skol3, c( skol3 ) ), skol2 ) ),
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), c( skol3 ) ) ) ==> addition( addition( multiplication(
% 5.62/6.03 addition( skol3, c( skol3 ) ), skol2 ), multiplication( addition( skol2,
% 5.62/6.03 c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), skol1( skol3 ) ) ),
% 5.62/6.03 ! leq( addition( addition( multiplication( addition( skol3, c( skol3 ) )
% 5.62/6.03 , skol2 ), multiplication( addition( skol2, c( skol2 ) ), skol3 ) ),
% 5.62/6.03 multiplication( c( skol2 ), c( skol3 ) ) ), one ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20975) {G4,W62,D8,L2,V0,M2} { ! addition( addition( addition(
% 5.62/6.03 one, multiplication( addition( skol3, c( skol3 ) ), skol2 ) ),
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), c( skol3 ) ) ) ==> addition( addition( multiplication(
% 5.62/6.03 addition( skol3, skol1( skol3 ) ), skol2 ), multiplication( addition(
% 5.62/6.03 skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), skol1( skol3
% 5.62/6.03 ) ) ), ! leq( addition( addition( multiplication( addition( skol3, c(
% 5.62/6.03 skol3 ) ), skol2 ), multiplication( addition( skol2, c( skol2 ) ), skol3
% 5.62/6.03 ) ), multiplication( c( skol2 ), skol1( skol3 ) ) ), one ) }.
% 5.62/6.03 parent0[0]: (2802) {G7,W5,D3,L1,V0,M1} R(2797,22);r(26) { c( skol3 ) ==>
% 5.62/6.03 skol1( skol3 ) }.
% 5.62/6.03 parent1[1; 28]: (20971) {G3,W62,D8,L2,V0,M2} { ! leq( addition( addition(
% 5.62/6.03 multiplication( addition( skol3, c( skol3 ) ), skol2 ), multiplication(
% 5.62/6.03 addition( skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ),
% 5.62/6.03 skol1( skol3 ) ) ), one ), ! addition( addition( addition( one,
% 5.62/6.03 multiplication( addition( skol3, c( skol3 ) ), skol2 ) ), multiplication
% 5.62/6.03 ( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), c
% 5.62/6.03 ( skol3 ) ) ) ==> addition( addition( multiplication( addition( skol3, c
% 5.62/6.03 ( skol3 ) ), skol2 ), multiplication( addition( skol2, c( skol2 ) ),
% 5.62/6.03 skol3 ) ), multiplication( c( skol2 ), skol1( skol3 ) ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20978) {G5,W62,D8,L2,V0,M2} { ! leq( addition( addition(
% 5.62/6.03 multiplication( addition( skol3, skol1( skol3 ) ), skol2 ),
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), skol1( skol3 ) ) ), one ), ! addition( addition( addition(
% 5.62/6.03 one, multiplication( addition( skol3, c( skol3 ) ), skol2 ) ),
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), c( skol3 ) ) ) ==> addition( addition( multiplication(
% 5.62/6.03 addition( skol3, skol1( skol3 ) ), skol2 ), multiplication( addition(
% 5.62/6.03 skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), skol1( skol3
% 5.62/6.03 ) ) ) }.
% 5.62/6.03 parent0[0]: (2802) {G7,W5,D3,L1,V0,M1} R(2797,22);r(26) { c( skol3 ) ==>
% 5.62/6.03 skol1( skol3 ) }.
% 5.62/6.03 parent1[1; 7]: (20975) {G4,W62,D8,L2,V0,M2} { ! addition( addition(
% 5.62/6.03 addition( one, multiplication( addition( skol3, c( skol3 ) ), skol2 ) ),
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), c( skol3 ) ) ) ==> addition( addition( multiplication(
% 5.62/6.03 addition( skol3, skol1( skol3 ) ), skol2 ), multiplication( addition(
% 5.62/6.03 skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), skol1( skol3
% 5.62/6.03 ) ) ), ! leq( addition( addition( multiplication( addition( skol3, c(
% 5.62/6.03 skol3 ) ), skol2 ), multiplication( addition( skol2, c( skol2 ) ), skol3
% 5.62/6.03 ) ), multiplication( c( skol2 ), skol1( skol3 ) ) ), one ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20980) {G6,W62,D8,L2,V0,M2} { ! addition( addition( addition(
% 5.62/6.03 one, multiplication( addition( skol3, c( skol3 ) ), skol2 ) ),
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), skol1( skol3 ) ) ) ==> addition( addition( multiplication(
% 5.62/6.03 addition( skol3, skol1( skol3 ) ), skol2 ), multiplication( addition(
% 5.62/6.03 skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), skol1( skol3
% 5.62/6.03 ) ) ), ! leq( addition( addition( multiplication( addition( skol3, skol1
% 5.62/6.03 ( skol3 ) ), skol2 ), multiplication( addition( skol2, c( skol2 ) ),
% 5.62/6.03 skol3 ) ), multiplication( c( skol2 ), skol1( skol3 ) ) ), one ) }.
% 5.62/6.03 parent0[0]: (2802) {G7,W5,D3,L1,V0,M1} R(2797,22);r(26) { c( skol3 ) ==>
% 5.62/6.03 skol1( skol3 ) }.
% 5.62/6.03 parent1[1; 21]: (20978) {G5,W62,D8,L2,V0,M2} { ! leq( addition( addition(
% 5.62/6.03 multiplication( addition( skol3, skol1( skol3 ) ), skol2 ),
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), skol1( skol3 ) ) ), one ), ! addition( addition( addition(
% 5.62/6.03 one, multiplication( addition( skol3, c( skol3 ) ), skol2 ) ),
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), c( skol3 ) ) ) ==> addition( addition( multiplication(
% 5.62/6.03 addition( skol3, skol1( skol3 ) ), skol2 ), multiplication( addition(
% 5.62/6.03 skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), skol1( skol3
% 5.62/6.03 ) ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (20981) {G7,W62,D8,L2,V0,M2} { ! addition( addition( addition(
% 5.62/6.03 one, multiplication( addition( skol3, skol1( skol3 ) ), skol2 ) ),
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), skol1( skol3 ) ) ) ==> addition( addition( multiplication(
% 5.62/6.03 addition( skol3, skol1( skol3 ) ), skol2 ), multiplication( addition(
% 5.62/6.03 skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), skol1( skol3
% 5.62/6.03 ) ) ), ! leq( addition( addition( multiplication( addition( skol3, skol1
% 5.62/6.03 ( skol3 ) ), skol2 ), multiplication( addition( skol2, c( skol2 ) ),
% 5.62/6.03 skol3 ) ), multiplication( c( skol2 ), skol1( skol3 ) ) ), one ) }.
% 5.62/6.03 parent0[0]: (2802) {G7,W5,D3,L1,V0,M1} R(2797,22);r(26) { c( skol3 ) ==>
% 5.62/6.03 skol1( skol3 ) }.
% 5.62/6.03 parent1[0; 9]: (20980) {G6,W62,D8,L2,V0,M2} { ! addition( addition(
% 5.62/6.03 addition( one, multiplication( addition( skol3, c( skol3 ) ), skol2 ) ),
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), skol1( skol3 ) ) ) ==> addition( addition( multiplication(
% 5.62/6.03 addition( skol3, skol1( skol3 ) ), skol2 ), multiplication( addition(
% 5.62/6.03 skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), skol1( skol3
% 5.62/6.03 ) ) ), ! leq( addition( addition( multiplication( addition( skol3, skol1
% 5.62/6.03 ( skol3 ) ), skol2 ), multiplication( addition( skol2, c( skol2 ) ),
% 5.62/6.03 skol3 ) ), multiplication( c( skol2 ), skol1( skol3 ) ) ), one ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (21010) {G4,W59,D8,L2,V0,M2} { ! leq( addition( addition(
% 5.62/6.03 multiplication( one, skol2 ), multiplication( addition( skol2, c( skol2 )
% 5.62/6.03 ), skol3 ) ), multiplication( c( skol2 ), skol1( skol3 ) ) ), one ), !
% 5.62/6.03 addition( addition( addition( one, multiplication( addition( skol3, skol1
% 5.62/6.03 ( skol3 ) ), skol2 ) ), multiplication( addition( skol2, c( skol2 ) ),
% 5.62/6.03 skol3 ) ), multiplication( c( skol2 ), skol1( skol3 ) ) ) ==> addition(
% 5.62/6.03 addition( multiplication( addition( skol3, skol1( skol3 ) ), skol2 ),
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), skol1( skol3 ) ) ) }.
% 5.62/6.03 parent0[0]: (263) {G3,W6,D4,L1,V0,M1} R(19,187) { addition( skol3, skol1(
% 5.62/6.03 skol3 ) ) ==> one }.
% 5.62/6.03 parent1[1; 5]: (20981) {G7,W62,D8,L2,V0,M2} { ! addition( addition(
% 5.62/6.03 addition( one, multiplication( addition( skol3, skol1( skol3 ) ), skol2 )
% 5.62/6.03 ), multiplication( addition( skol2, c( skol2 ) ), skol3 ) ),
% 5.62/6.03 multiplication( c( skol2 ), skol1( skol3 ) ) ) ==> addition( addition(
% 5.62/6.03 multiplication( addition( skol3, skol1( skol3 ) ), skol2 ),
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), skol1( skol3 ) ) ), ! leq( addition( addition(
% 5.62/6.03 multiplication( addition( skol3, skol1( skol3 ) ), skol2 ),
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), skol1( skol3 ) ) ), one ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (21016) {G4,W56,D8,L2,V0,M2} { ! addition( addition( addition(
% 5.62/6.03 one, multiplication( addition( skol3, skol1( skol3 ) ), skol2 ) ),
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), skol1( skol3 ) ) ) ==> addition( addition( multiplication(
% 5.62/6.03 one, skol2 ), multiplication( addition( skol2, c( skol2 ) ), skol3 ) ),
% 5.62/6.03 multiplication( c( skol2 ), skol1( skol3 ) ) ), ! leq( addition( addition
% 5.62/6.03 ( multiplication( one, skol2 ), multiplication( addition( skol2, c( skol2
% 5.62/6.03 ) ), skol3 ) ), multiplication( c( skol2 ), skol1( skol3 ) ) ), one )
% 5.62/6.03 }.
% 5.62/6.03 parent0[0]: (263) {G3,W6,D4,L1,V0,M1} R(19,187) { addition( skol3, skol1(
% 5.62/6.03 skol3 ) ) ==> one }.
% 5.62/6.03 parent1[1; 26]: (21010) {G4,W59,D8,L2,V0,M2} { ! leq( addition( addition(
% 5.62/6.03 multiplication( one, skol2 ), multiplication( addition( skol2, c( skol2 )
% 5.62/6.03 ), skol3 ) ), multiplication( c( skol2 ), skol1( skol3 ) ) ), one ), !
% 5.62/6.03 addition( addition( addition( one, multiplication( addition( skol3, skol1
% 5.62/6.03 ( skol3 ) ), skol2 ) ), multiplication( addition( skol2, c( skol2 ) ),
% 5.62/6.03 skol3 ) ), multiplication( c( skol2 ), skol1( skol3 ) ) ) ==> addition(
% 5.62/6.03 addition( multiplication( addition( skol3, skol1( skol3 ) ), skol2 ),
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), skol1( skol3 ) ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (21017) {G4,W53,D7,L2,V0,M2} { ! addition( addition( addition(
% 5.62/6.03 one, multiplication( one, skol2 ) ), multiplication( addition( skol2, c(
% 5.62/6.03 skol2 ) ), skol3 ) ), multiplication( c( skol2 ), skol1( skol3 ) ) ) ==>
% 5.62/6.03 addition( addition( multiplication( one, skol2 ), multiplication(
% 5.62/6.03 addition( skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ),
% 5.62/6.03 skol1( skol3 ) ) ), ! leq( addition( addition( multiplication( one, skol2
% 5.62/6.03 ), multiplication( addition( skol2, c( skol2 ) ), skol3 ) ),
% 5.62/6.03 multiplication( c( skol2 ), skol1( skol3 ) ) ), one ) }.
% 5.62/6.03 parent0[0]: (263) {G3,W6,D4,L1,V0,M1} R(19,187) { addition( skol3, skol1(
% 5.62/6.03 skol3 ) ) ==> one }.
% 5.62/6.03 parent1[0; 7]: (21016) {G4,W56,D8,L2,V0,M2} { ! addition( addition(
% 5.62/6.03 addition( one, multiplication( addition( skol3, skol1( skol3 ) ), skol2 )
% 5.62/6.03 ), multiplication( addition( skol2, c( skol2 ) ), skol3 ) ),
% 5.62/6.03 multiplication( c( skol2 ), skol1( skol3 ) ) ) ==> addition( addition(
% 5.62/6.03 multiplication( one, skol2 ), multiplication( addition( skol2, c( skol2 )
% 5.62/6.03 ), skol3 ) ), multiplication( c( skol2 ), skol1( skol3 ) ) ), ! leq(
% 5.62/6.03 addition( addition( multiplication( one, skol2 ), multiplication(
% 5.62/6.03 addition( skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ),
% 5.62/6.03 skol1( skol3 ) ) ), one ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (21023) {G1,W51,D7,L2,V0,M2} { ! leq( addition( addition( skol2,
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), skol1( skol3 ) ) ), one ), ! addition( addition( addition(
% 5.62/6.03 one, multiplication( one, skol2 ) ), multiplication( addition( skol2, c(
% 5.62/6.03 skol2 ) ), skol3 ) ), multiplication( c( skol2 ), skol1( skol3 ) ) ) ==>
% 5.62/6.03 addition( addition( multiplication( one, skol2 ), multiplication(
% 5.62/6.03 addition( skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ),
% 5.62/6.03 skol1( skol3 ) ) ) }.
% 5.62/6.03 parent0[0]: (6) {G0,W5,D3,L1,V1,M1} I { multiplication( one, X ) ==> X }.
% 5.62/6.03 parent1[1; 4]: (21017) {G4,W53,D7,L2,V0,M2} { ! addition( addition(
% 5.62/6.03 addition( one, multiplication( one, skol2 ) ), multiplication( addition(
% 5.62/6.03 skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), skol1( skol3
% 5.62/6.03 ) ) ) ==> addition( addition( multiplication( one, skol2 ),
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), skol1( skol3 ) ) ), ! leq( addition( addition(
% 5.62/6.03 multiplication( one, skol2 ), multiplication( addition( skol2, c( skol2 )
% 5.62/6.03 ), skol3 ) ), multiplication( c( skol2 ), skol1( skol3 ) ) ), one ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := skol2
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (21028) {G2,W47,D7,L2,V0,M2} { ! addition( addition( one,
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), skol1( skol3 ) ) ) ==> addition( addition( multiplication(
% 5.62/6.03 one, skol2 ), multiplication( addition( skol2, c( skol2 ) ), skol3 ) ),
% 5.62/6.03 multiplication( c( skol2 ), skol1( skol3 ) ) ), ! leq( addition( addition
% 5.62/6.03 ( skol2, multiplication( addition( skol2, c( skol2 ) ), skol3 ) ),
% 5.62/6.03 multiplication( c( skol2 ), skol1( skol3 ) ) ), one ) }.
% 5.62/6.03 parent0[0]: (2503) {G6,W7,D4,L1,V1,M1} P(2438,51);d(5) { addition( X,
% 5.62/6.03 multiplication( X, skol2 ) ) ==> X }.
% 5.62/6.03 parent1[1; 4]: (21023) {G1,W51,D7,L2,V0,M2} { ! leq( addition( addition(
% 5.62/6.03 skol2, multiplication( addition( skol2, c( skol2 ) ), skol3 ) ),
% 5.62/6.03 multiplication( c( skol2 ), skol1( skol3 ) ) ), one ), ! addition(
% 5.62/6.03 addition( addition( one, multiplication( one, skol2 ) ), multiplication(
% 5.62/6.03 addition( skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ),
% 5.62/6.03 skol1( skol3 ) ) ) ==> addition( addition( multiplication( one, skol2 ),
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), skol1( skol3 ) ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := one
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (21029) {G3,W45,D7,L2,V0,M2} { ! leq( addition( addition( skol2,
% 5.62/6.03 multiplication( c( skol2 ), skol3 ) ), multiplication( c( skol2 ), skol1
% 5.62/6.03 ( skol3 ) ) ), one ), ! addition( addition( one, multiplication( addition
% 5.62/6.03 ( skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ), skol1(
% 5.62/6.03 skol3 ) ) ) ==> addition( addition( multiplication( one, skol2 ),
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), skol1( skol3 ) ) ) }.
% 5.62/6.03 parent0[0]: (18875) {G7,W13,D5,L1,V2,M1} P(2859,63) { addition( X,
% 5.62/6.03 multiplication( addition( X, Y ), skol3 ) ) ==> addition( X,
% 5.62/6.03 multiplication( Y, skol3 ) ) }.
% 5.62/6.03 parent1[1; 3]: (21028) {G2,W47,D7,L2,V0,M2} { ! addition( addition( one,
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), skol1( skol3 ) ) ) ==> addition( addition( multiplication(
% 5.62/6.03 one, skol2 ), multiplication( addition( skol2, c( skol2 ) ), skol3 ) ),
% 5.62/6.03 multiplication( c( skol2 ), skol1( skol3 ) ) ), ! leq( addition( addition
% 5.62/6.03 ( skol2, multiplication( addition( skol2, c( skol2 ) ), skol3 ) ),
% 5.62/6.03 multiplication( c( skol2 ), skol1( skol3 ) ) ), one ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := skol2
% 5.62/6.03 Y := c( skol2 )
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (21030) {G4,W43,D7,L2,V0,M2} { ! addition( addition( one,
% 5.62/6.03 multiplication( c( skol2 ), skol3 ) ), multiplication( c( skol2 ), skol1
% 5.62/6.03 ( skol3 ) ) ) ==> addition( addition( multiplication( one, skol2 ),
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), skol1( skol3 ) ) ), ! leq( addition( addition( skol2,
% 5.62/6.03 multiplication( c( skol2 ), skol3 ) ), multiplication( c( skol2 ), skol1
% 5.62/6.03 ( skol3 ) ) ), one ) }.
% 5.62/6.03 parent0[0]: (19903) {G11,W13,D5,L1,V1,M1} P(18605,63) { addition( one,
% 5.62/6.03 multiplication( addition( skol2, X ), skol3 ) ) ==> addition( one,
% 5.62/6.03 multiplication( X, skol3 ) ) }.
% 5.62/6.03 parent1[1; 3]: (21029) {G3,W45,D7,L2,V0,M2} { ! leq( addition( addition(
% 5.62/6.03 skol2, multiplication( c( skol2 ), skol3 ) ), multiplication( c( skol2 )
% 5.62/6.03 , skol1( skol3 ) ) ), one ), ! addition( addition( one, multiplication(
% 5.62/6.03 addition( skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ),
% 5.62/6.03 skol1( skol3 ) ) ) ==> addition( addition( multiplication( one, skol2 ),
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), skol1( skol3 ) ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := c( skol2 )
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (21032) {G2,W40,D7,L2,V0,M2} { ! leq( addition( skol2,
% 5.62/6.03 multiplication( c( skol2 ), addition( skol3, skol1( skol3 ) ) ) ), one )
% 5.62/6.03 , ! addition( addition( one, multiplication( c( skol2 ), skol3 ) ),
% 5.62/6.03 multiplication( c( skol2 ), skol1( skol3 ) ) ) ==> addition( addition(
% 5.62/6.03 multiplication( one, skol2 ), multiplication( addition( skol2, c( skol2 )
% 5.62/6.03 ), skol3 ) ), multiplication( c( skol2 ), skol1( skol3 ) ) ) }.
% 5.62/6.03 parent0[0]: (50) {G1,W17,D5,L1,V4,M1} P(7,1) { addition( addition( T,
% 5.62/6.03 multiplication( X, Y ) ), multiplication( X, Z ) ) ==> addition( T,
% 5.62/6.03 multiplication( X, addition( Y, Z ) ) ) }.
% 5.62/6.03 parent1[1; 2]: (21030) {G4,W43,D7,L2,V0,M2} { ! addition( addition( one,
% 5.62/6.03 multiplication( c( skol2 ), skol3 ) ), multiplication( c( skol2 ), skol1
% 5.62/6.03 ( skol3 ) ) ) ==> addition( addition( multiplication( one, skol2 ),
% 5.62/6.03 multiplication( addition( skol2, c( skol2 ) ), skol3 ) ), multiplication
% 5.62/6.03 ( c( skol2 ), skol1( skol3 ) ) ), ! leq( addition( addition( skol2,
% 5.62/6.03 multiplication( c( skol2 ), skol3 ) ), multiplication( c( skol2 ), skol1
% 5.62/6.03 ( skol3 ) ) ), one ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := c( skol2 )
% 5.62/6.03 Y := skol3
% 5.62/6.03 Z := skol1( skol3 )
% 5.62/6.03 T := skol2
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (21034) {G2,W37,D7,L2,V0,M2} { ! addition( one, multiplication( c
% 5.62/6.03 ( skol2 ), addition( skol3, skol1( skol3 ) ) ) ) ==> addition( addition(
% 5.62/6.03 multiplication( one, skol2 ), multiplication( addition( skol2, c( skol2 )
% 5.62/6.03 ), skol3 ) ), multiplication( c( skol2 ), skol1( skol3 ) ) ), ! leq(
% 5.62/6.03 addition( skol2, multiplication( c( skol2 ), addition( skol3, skol1(
% 5.62/6.03 skol3 ) ) ) ), one ) }.
% 5.62/6.03 parent0[0]: (50) {G1,W17,D5,L1,V4,M1} P(7,1) { addition( addition( T,
% 5.62/6.03 multiplication( X, Y ) ), multiplication( X, Z ) ) ==> addition( T,
% 5.62/6.03 multiplication( X, addition( Y, Z ) ) ) }.
% 5.62/6.03 parent1[1; 2]: (21032) {G2,W40,D7,L2,V0,M2} { ! leq( addition( skol2,
% 5.62/6.03 multiplication( c( skol2 ), addition( skol3, skol1( skol3 ) ) ) ), one )
% 5.62/6.03 , ! addition( addition( one, multiplication( c( skol2 ), skol3 ) ),
% 5.62/6.03 multiplication( c( skol2 ), skol1( skol3 ) ) ) ==> addition( addition(
% 5.62/6.03 multiplication( one, skol2 ), multiplication( addition( skol2, c( skol2 )
% 5.62/6.03 ), skol3 ) ), multiplication( c( skol2 ), skol1( skol3 ) ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := c( skol2 )
% 5.62/6.03 Y := skol3
% 5.62/6.03 Z := skol1( skol3 )
% 5.62/6.03 T := one
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (21038) {G3,W37,D7,L2,V0,M2} { ! leq( addition( skol2,
% 5.62/6.03 multiplication( skol1( skol2 ), addition( skol3, skol1( skol3 ) ) ) ),
% 5.62/6.03 one ), ! addition( one, multiplication( c( skol2 ), addition( skol3,
% 5.62/6.03 skol1( skol3 ) ) ) ) ==> addition( addition( multiplication( one, skol2 )
% 5.62/6.03 , multiplication( addition( skol2, c( skol2 ) ), skol3 ) ),
% 5.62/6.03 multiplication( c( skol2 ), skol1( skol3 ) ) ) }.
% 5.62/6.03 parent0[0]: (2446) {G7,W5,D3,L1,V0,M1} R(2441,22);r(27) { c( skol2 ) ==>
% 5.62/6.03 skol1( skol2 ) }.
% 5.62/6.03 parent1[1; 5]: (21034) {G2,W37,D7,L2,V0,M2} { ! addition( one,
% 5.62/6.03 multiplication( c( skol2 ), addition( skol3, skol1( skol3 ) ) ) ) ==>
% 5.62/6.03 addition( addition( multiplication( one, skol2 ), multiplication(
% 5.62/6.03 addition( skol2, c( skol2 ) ), skol3 ) ), multiplication( c( skol2 ),
% 5.62/6.03 skol1( skol3 ) ) ), ! leq( addition( skol2, multiplication( c( skol2 ),
% 5.62/6.03 addition( skol3, skol1( skol3 ) ) ) ), one ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (21051) {G4,W37,D7,L2,V0,M2} { ! addition( one, multiplication( c
% 5.62/6.03 ( skol2 ), addition( skol3, skol1( skol3 ) ) ) ) ==> addition( addition(
% 5.62/6.03 multiplication( one, skol2 ), multiplication( addition( skol2, c( skol2 )
% 5.62/6.03 ), skol3 ) ), multiplication( skol1( skol2 ), skol1( skol3 ) ) ), ! leq
% 5.62/6.03 ( addition( skol2, multiplication( skol1( skol2 ), addition( skol3, skol1
% 5.62/6.03 ( skol3 ) ) ) ), one ) }.
% 5.62/6.03 parent0[0]: (2446) {G7,W5,D3,L1,V0,M1} R(2441,22);r(27) { c( skol2 ) ==>
% 5.62/6.03 skol1( skol2 ) }.
% 5.62/6.03 parent1[1; 23]: (21038) {G3,W37,D7,L2,V0,M2} { ! leq( addition( skol2,
% 5.62/6.03 multiplication( skol1( skol2 ), addition( skol3, skol1( skol3 ) ) ) ),
% 5.62/6.03 one ), ! addition( one, multiplication( c( skol2 ), addition( skol3,
% 5.62/6.03 skol1( skol3 ) ) ) ) ==> addition( addition( multiplication( one, skol2 )
% 5.62/6.03 , multiplication( addition( skol2, c( skol2 ) ), skol3 ) ),
% 5.62/6.03 multiplication( c( skol2 ), skol1( skol3 ) ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (21053) {G5,W37,D7,L2,V0,M2} { ! addition( one, multiplication( c
% 5.62/6.03 ( skol2 ), addition( skol3, skol1( skol3 ) ) ) ) ==> addition( addition(
% 5.62/6.03 multiplication( one, skol2 ), multiplication( addition( skol2, skol1(
% 5.62/6.03 skol2 ) ), skol3 ) ), multiplication( skol1( skol2 ), skol1( skol3 ) ) )
% 5.62/6.03 , ! leq( addition( skol2, multiplication( skol1( skol2 ), addition( skol3
% 5.62/6.03 , skol1( skol3 ) ) ) ), one ) }.
% 5.62/6.03 parent0[0]: (2446) {G7,W5,D3,L1,V0,M1} R(2441,22);r(27) { c( skol2 ) ==>
% 5.62/6.03 skol1( skol2 ) }.
% 5.62/6.03 parent1[0; 19]: (21051) {G4,W37,D7,L2,V0,M2} { ! addition( one,
% 5.62/6.03 multiplication( c( skol2 ), addition( skol3, skol1( skol3 ) ) ) ) ==>
% 5.62/6.03 addition( addition( multiplication( one, skol2 ), multiplication(
% 5.62/6.03 addition( skol2, c( skol2 ) ), skol3 ) ), multiplication( skol1( skol2 )
% 5.62/6.03 , skol1( skol3 ) ) ), ! leq( addition( skol2, multiplication( skol1(
% 5.62/6.03 skol2 ), addition( skol3, skol1( skol3 ) ) ) ), one ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (21054) {G6,W37,D7,L2,V0,M2} { ! addition( one, multiplication(
% 5.62/6.03 skol1( skol2 ), addition( skol3, skol1( skol3 ) ) ) ) ==> addition(
% 5.62/6.03 addition( multiplication( one, skol2 ), multiplication( addition( skol2,
% 5.62/6.03 skol1( skol2 ) ), skol3 ) ), multiplication( skol1( skol2 ), skol1( skol3
% 5.62/6.03 ) ) ), ! leq( addition( skol2, multiplication( skol1( skol2 ), addition
% 5.62/6.03 ( skol3, skol1( skol3 ) ) ) ), one ) }.
% 5.62/6.03 parent0[0]: (2446) {G7,W5,D3,L1,V0,M1} R(2441,22);r(27) { c( skol2 ) ==>
% 5.62/6.03 skol1( skol2 ) }.
% 5.62/6.03 parent1[0; 5]: (21053) {G5,W37,D7,L2,V0,M2} { ! addition( one,
% 5.62/6.03 multiplication( c( skol2 ), addition( skol3, skol1( skol3 ) ) ) ) ==>
% 5.62/6.03 addition( addition( multiplication( one, skol2 ), multiplication(
% 5.62/6.03 addition( skol2, skol1( skol2 ) ), skol3 ) ), multiplication( skol1(
% 5.62/6.03 skol2 ), skol1( skol3 ) ) ), ! leq( addition( skol2, multiplication(
% 5.62/6.03 skol1( skol2 ), addition( skol3, skol1( skol3 ) ) ) ), one ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (21079) {G4,W34,D7,L2,V0,M2} { ! leq( addition( skol2,
% 5.62/6.03 multiplication( skol1( skol2 ), one ) ), one ), ! addition( one,
% 5.62/6.03 multiplication( skol1( skol2 ), addition( skol3, skol1( skol3 ) ) ) ) ==>
% 5.62/6.03 addition( addition( multiplication( one, skol2 ), multiplication(
% 5.62/6.03 addition( skol2, skol1( skol2 ) ), skol3 ) ), multiplication( skol1(
% 5.62/6.03 skol2 ), skol1( skol3 ) ) ) }.
% 5.62/6.03 parent0[0]: (263) {G3,W6,D4,L1,V0,M1} R(19,187) { addition( skol3, skol1(
% 5.62/6.03 skol3 ) ) ==> one }.
% 5.62/6.03 parent1[1; 7]: (21054) {G6,W37,D7,L2,V0,M2} { ! addition( one,
% 5.62/6.03 multiplication( skol1( skol2 ), addition( skol3, skol1( skol3 ) ) ) ) ==>
% 5.62/6.03 addition( addition( multiplication( one, skol2 ), multiplication(
% 5.62/6.03 addition( skol2, skol1( skol2 ) ), skol3 ) ), multiplication( skol1(
% 5.62/6.03 skol2 ), skol1( skol3 ) ) ), ! leq( addition( skol2, multiplication(
% 5.62/6.03 skol1( skol2 ), addition( skol3, skol1( skol3 ) ) ) ), one ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (21081) {G4,W31,D7,L2,V0,M2} { ! addition( one, multiplication(
% 5.62/6.03 skol1( skol2 ), one ) ) ==> addition( addition( multiplication( one,
% 5.62/6.03 skol2 ), multiplication( addition( skol2, skol1( skol2 ) ), skol3 ) ),
% 5.62/6.03 multiplication( skol1( skol2 ), skol1( skol3 ) ) ), ! leq( addition(
% 5.62/6.03 skol2, multiplication( skol1( skol2 ), one ) ), one ) }.
% 5.62/6.03 parent0[0]: (263) {G3,W6,D4,L1,V0,M1} R(19,187) { addition( skol3, skol1(
% 5.62/6.03 skol3 ) ) ==> one }.
% 5.62/6.03 parent1[1; 7]: (21079) {G4,W34,D7,L2,V0,M2} { ! leq( addition( skol2,
% 5.62/6.03 multiplication( skol1( skol2 ), one ) ), one ), ! addition( one,
% 5.62/6.03 multiplication( skol1( skol2 ), addition( skol3, skol1( skol3 ) ) ) ) ==>
% 5.62/6.03 addition( addition( multiplication( one, skol2 ), multiplication(
% 5.62/6.03 addition( skol2, skol1( skol2 ) ), skol3 ) ), multiplication( skol1(
% 5.62/6.03 skol2 ), skol1( skol3 ) ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (21083) {G1,W29,D7,L2,V0,M2} { ! leq( addition( skol2, skol1(
% 5.62/6.03 skol2 ) ), one ), ! addition( one, multiplication( skol1( skol2 ), one )
% 5.62/6.03 ) ==> addition( addition( multiplication( one, skol2 ), multiplication(
% 5.62/6.03 addition( skol2, skol1( skol2 ) ), skol3 ) ), multiplication( skol1(
% 5.62/6.03 skol2 ), skol1( skol3 ) ) ) }.
% 5.62/6.03 parent0[0]: (5) {G0,W5,D3,L1,V1,M1} I { multiplication( X, one ) ==> X }.
% 5.62/6.03 parent1[1; 4]: (21081) {G4,W31,D7,L2,V0,M2} { ! addition( one,
% 5.62/6.03 multiplication( skol1( skol2 ), one ) ) ==> addition( addition(
% 5.62/6.03 multiplication( one, skol2 ), multiplication( addition( skol2, skol1(
% 5.62/6.03 skol2 ) ), skol3 ) ), multiplication( skol1( skol2 ), skol1( skol3 ) ) )
% 5.62/6.03 , ! leq( addition( skol2, multiplication( skol1( skol2 ), one ) ), one )
% 5.62/6.03 }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := skol1( skol2 )
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (21085) {G2,W24,D7,L2,V0,M2} { ! one ==> addition( addition(
% 5.62/6.03 multiplication( one, skol2 ), multiplication( addition( skol2, skol1(
% 5.62/6.03 skol2 ) ), skol3 ) ), multiplication( skol1( skol2 ), skol1( skol3 ) ) )
% 5.62/6.03 , ! leq( addition( skol2, skol1( skol2 ) ), one ) }.
% 5.62/6.03 parent0[0]: (2396) {G5,W8,D5,L1,V1,M1} P(2384,64);d(6) { addition( X,
% 5.62/6.03 multiplication( skol1( skol2 ), X ) ) ==> X }.
% 5.62/6.03 parent1[1; 2]: (21083) {G1,W29,D7,L2,V0,M2} { ! leq( addition( skol2,
% 5.62/6.03 skol1( skol2 ) ), one ), ! addition( one, multiplication( skol1( skol2 )
% 5.62/6.03 , one ) ) ==> addition( addition( multiplication( one, skol2 ),
% 5.62/6.03 multiplication( addition( skol2, skol1( skol2 ) ), skol3 ) ),
% 5.62/6.03 multiplication( skol1( skol2 ), skol1( skol3 ) ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := one
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (21087) {G3,W21,D7,L2,V0,M2} { ! leq( one, one ), ! one ==>
% 5.62/6.03 addition( addition( multiplication( one, skol2 ), multiplication(
% 5.62/6.03 addition( skol2, skol1( skol2 ) ), skol3 ) ), multiplication( skol1(
% 5.62/6.03 skol2 ), skol1( skol3 ) ) ) }.
% 5.62/6.03 parent0[0]: (262) {G3,W6,D4,L1,V0,M1} R(19,191) { addition( skol2, skol1(
% 5.62/6.03 skol2 ) ) ==> one }.
% 5.62/6.03 parent1[1; 2]: (21085) {G2,W24,D7,L2,V0,M2} { ! one ==> addition( addition
% 5.62/6.03 ( multiplication( one, skol2 ), multiplication( addition( skol2, skol1(
% 5.62/6.03 skol2 ) ), skol3 ) ), multiplication( skol1( skol2 ), skol1( skol3 ) ) )
% 5.62/6.03 , ! leq( addition( skol2, skol1( skol2 ) ), one ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (21089) {G1,W19,D7,L2,V0,M2} { ! one ==> addition( addition(
% 5.62/6.03 skol2, multiplication( addition( skol2, skol1( skol2 ) ), skol3 ) ),
% 5.62/6.03 multiplication( skol1( skol2 ), skol1( skol3 ) ) ), ! leq( one, one ) }.
% 5.62/6.03 parent0[0]: (6) {G0,W5,D3,L1,V1,M1} I { multiplication( one, X ) ==> X }.
% 5.62/6.03 parent1[1; 5]: (21087) {G3,W21,D7,L2,V0,M2} { ! leq( one, one ), ! one ==>
% 5.62/6.03 addition( addition( multiplication( one, skol2 ), multiplication(
% 5.62/6.03 addition( skol2, skol1( skol2 ) ), skol3 ) ), multiplication( skol1(
% 5.62/6.03 skol2 ), skol1( skol3 ) ) ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := skol2
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (21090) {G2,W17,D6,L2,V0,M2} { ! one ==> addition( addition(
% 5.62/6.03 skol2, multiplication( skol1( skol2 ), skol3 ) ), multiplication( skol1(
% 5.62/6.03 skol2 ), skol1( skol3 ) ) ), ! leq( one, one ) }.
% 5.62/6.03 parent0[0]: (18875) {G7,W13,D5,L1,V2,M1} P(2859,63) { addition( X,
% 5.62/6.03 multiplication( addition( X, Y ), skol3 ) ) ==> addition( X,
% 5.62/6.03 multiplication( Y, skol3 ) ) }.
% 5.62/6.03 parent1[0; 4]: (21089) {G1,W19,D7,L2,V0,M2} { ! one ==> addition( addition
% 5.62/6.03 ( skol2, multiplication( addition( skol2, skol1( skol2 ) ), skol3 ) ),
% 5.62/6.03 multiplication( skol1( skol2 ), skol1( skol3 ) ) ), ! leq( one, one ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := skol2
% 5.62/6.03 Y := skol1( skol2 )
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (21091) {G2,W14,D6,L2,V0,M2} { ! one ==> addition( skol2,
% 5.62/6.03 multiplication( skol1( skol2 ), addition( skol3, skol1( skol3 ) ) ) ), !
% 5.62/6.03 leq( one, one ) }.
% 5.62/6.03 parent0[0]: (50) {G1,W17,D5,L1,V4,M1} P(7,1) { addition( addition( T,
% 5.62/6.03 multiplication( X, Y ) ), multiplication( X, Z ) ) ==> addition( T,
% 5.62/6.03 multiplication( X, addition( Y, Z ) ) ) }.
% 5.62/6.03 parent1[0; 3]: (21090) {G2,W17,D6,L2,V0,M2} { ! one ==> addition( addition
% 5.62/6.03 ( skol2, multiplication( skol1( skol2 ), skol3 ) ), multiplication( skol1
% 5.62/6.03 ( skol2 ), skol1( skol3 ) ) ), ! leq( one, one ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := skol1( skol2 )
% 5.62/6.03 Y := skol3
% 5.62/6.03 Z := skol1( skol3 )
% 5.62/6.03 T := skol2
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (21092) {G3,W11,D5,L2,V0,M2} { ! one ==> addition( skol2,
% 5.62/6.03 multiplication( skol1( skol2 ), one ) ), ! leq( one, one ) }.
% 5.62/6.03 parent0[0]: (263) {G3,W6,D4,L1,V0,M1} R(19,187) { addition( skol3, skol1(
% 5.62/6.03 skol3 ) ) ==> one }.
% 5.62/6.03 parent1[0; 8]: (21091) {G2,W14,D6,L2,V0,M2} { ! one ==> addition( skol2,
% 5.62/6.03 multiplication( skol1( skol2 ), addition( skol3, skol1( skol3 ) ) ) ), !
% 5.62/6.03 leq( one, one ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (21093) {G1,W9,D4,L2,V0,M2} { ! one ==> addition( skol2, skol1(
% 5.62/6.03 skol2 ) ), ! leq( one, one ) }.
% 5.62/6.03 parent0[0]: (5) {G0,W5,D3,L1,V1,M1} I { multiplication( X, one ) ==> X }.
% 5.62/6.03 parent1[0; 5]: (21092) {G3,W11,D5,L2,V0,M2} { ! one ==> addition( skol2,
% 5.62/6.03 multiplication( skol1( skol2 ), one ) ), ! leq( one, one ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 X := skol1( skol2 )
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 paramod: (21094) {G2,W6,D2,L2,V0,M2} { ! one ==> one, ! leq( one, one )
% 5.62/6.03 }.
% 5.62/6.03 parent0[0]: (262) {G3,W6,D4,L1,V0,M1} R(19,191) { addition( skol2, skol1(
% 5.62/6.03 skol2 ) ) ==> one }.
% 5.62/6.03 parent1[0; 3]: (21093) {G1,W9,D4,L2,V0,M2} { ! one ==> addition( skol2,
% 5.62/6.03 skol1( skol2 ) ), ! leq( one, one ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 eqrefl: (21095) {G0,W3,D2,L1,V0,M1} { ! leq( one, one ) }.
% 5.62/6.03 parent0[0]: (21094) {G2,W6,D2,L2,V0,M2} { ! one ==> one, ! leq( one, one )
% 5.62/6.03 }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 resolution: (21096) {G1,W0,D0,L0,V0,M0} { }.
% 5.62/6.03 parent0[0]: (21095) {G0,W3,D2,L1,V0,M1} { ! leq( one, one ) }.
% 5.62/6.03 parent1[0]: (149) {G1,W3,D2,L1,V1,M1} R(12,3) { leq( X, X ) }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 substitution1:
% 5.62/6.03 X := one
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 subsumption: (20404) {G12,W0,D0,L0,V0,M0} S(515);d(2802);d(2802);d(263);d(
% 5.62/6.03 263);d(6);d(2503);d(18875);d(19903);d(50);d(50);d(2446);d(2446);d(263);d(
% 5.62/6.03 263);d(5);d(2396);d(262);d(6);d(18875);d(50);d(263);d(5);d(262);q;r(149)
% 5.62/6.03 { }.
% 5.62/6.03 parent0: (21096) {G1,W0,D0,L0,V0,M0} { }.
% 5.62/6.03 substitution0:
% 5.62/6.03 end
% 5.62/6.03 permutation0:
% 5.62/6.03 end
% 5.62/6.03
% 5.62/6.03 Proof check complete!
% 5.62/6.03
% 5.62/6.03 Memory use:
% 5.62/6.03
% 5.62/6.03 space for terms: 251133
% 5.62/6.03 space for clauses: 968572
% 5.62/6.03
% 5.62/6.03
% 5.62/6.03 clauses generated: 155282
% 5.62/6.03 clauses kept: 20405
% 5.62/6.03 clauses selected: 1311
% 5.62/6.03 clauses deleted: 5486
% 5.62/6.03 clauses inuse deleted: 315
% 5.62/6.03
% 5.62/6.03 subsentry: 939080
% 5.62/6.03 literals s-matched: 525683
% 5.62/6.03 literals matched: 517570
% 5.62/6.03 full subsumption: 192807
% 5.62/6.03
% 5.62/6.03 checksum: 1379686
% 5.62/6.03
% 5.62/6.03
% 5.62/6.03 Bliksem ended
%------------------------------------------------------------------------------