%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : KLE009+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n010.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:33 EDT 2022
% Result : Theorem 6.66s 7.10s
% Output : Refutation 6.66s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : KLE009+1 : TPTP v8.1.0. Released v4.0.0.
% 0.10/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n010.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % DateTime : Thu Jun 16 08:15:08 EDT 2022
% 0.12/0.34 % CPUTime :
% 6.66/7.10 *** allocated 10000 integers for termspace/termends
% 6.66/7.10 *** allocated 10000 integers for clauses
% 6.66/7.10 *** allocated 10000 integers for justifications
% 6.66/7.10 Bliksem 1.12
% 6.66/7.10
% 6.66/7.10
% 6.66/7.10 Automatic Strategy Selection
% 6.66/7.10
% 6.66/7.10
% 6.66/7.10 Clauses:
% 6.66/7.10
% 6.66/7.10 { addition( X, Y ) = addition( Y, X ) }.
% 6.66/7.10 { addition( Z, addition( Y, X ) ) = addition( addition( Z, Y ), X ) }.
% 6.66/7.10 { addition( X, zero ) = X }.
% 6.66/7.10 { addition( X, X ) = X }.
% 6.66/7.10 { multiplication( X, multiplication( Y, Z ) ) = multiplication(
% 6.66/7.10 multiplication( X, Y ), Z ) }.
% 6.66/7.10 { multiplication( X, one ) = X }.
% 6.66/7.10 { multiplication( one, X ) = X }.
% 6.66/7.10 { multiplication( X, addition( Y, Z ) ) = addition( multiplication( X, Y )
% 6.66/7.10 , multiplication( X, Z ) ) }.
% 6.66/7.10 { multiplication( addition( X, Y ), Z ) = addition( multiplication( X, Z )
% 6.66/7.10 , multiplication( Y, Z ) ) }.
% 6.66/7.10 { multiplication( X, zero ) = zero }.
% 6.66/7.10 { multiplication( zero, X ) = zero }.
% 6.66/7.10 { ! leq( X, Y ), addition( X, Y ) = Y }.
% 6.66/7.10 { ! addition( X, Y ) = Y, leq( X, Y ) }.
% 6.66/7.10 { ! test( X ), complement( skol1( X ), X ) }.
% 6.66/7.10 { ! complement( Y, X ), test( X ) }.
% 6.66/7.10 { ! complement( Y, X ), multiplication( X, Y ) = zero }.
% 6.66/7.10 { ! complement( Y, X ), alpha1( X, Y ) }.
% 6.66/7.10 { ! multiplication( X, Y ) = zero, ! alpha1( X, Y ), complement( Y, X ) }.
% 6.66/7.10 { ! alpha1( X, Y ), multiplication( Y, X ) = zero }.
% 6.66/7.10 { ! alpha1( X, Y ), addition( X, Y ) = one }.
% 6.66/7.10 { ! multiplication( Y, X ) = zero, ! addition( X, Y ) = one, alpha1( X, Y )
% 6.66/7.10 }.
% 6.66/7.10 { ! test( X ), ! c( X ) = Y, complement( X, Y ) }.
% 6.66/7.10 { ! test( X ), ! complement( X, Y ), c( X ) = Y }.
% 6.66/7.10 { test( X ), c( X ) = zero }.
% 6.66/7.10 { test( skol3 ) }.
% 6.66/7.10 { test( skol2 ) }.
% 6.66/7.10 { ! one = addition( addition( addition( multiplication( skol2, skol3 ),
% 6.66/7.10 multiplication( skol2, c( skol3 ) ) ), multiplication( c( skol2 ), skol3
% 6.66/7.10 ) ), multiplication( c( skol2 ), c( skol3 ) ) ) }.
% 6.66/7.10
% 6.66/7.10 percentage equality = 0.522727, percentage horn = 0.962963
% 6.66/7.10 This is a problem with some equality
% 6.66/7.10
% 6.66/7.10
% 6.66/7.10
% 6.66/7.10 Options Used:
% 6.66/7.10
% 6.66/7.10 useres = 1
% 6.66/7.10 useparamod = 1
% 6.66/7.10 useeqrefl = 1
% 6.66/7.10 useeqfact = 1
% 6.66/7.10 usefactor = 1
% 6.66/7.10 usesimpsplitting = 0
% 6.66/7.10 usesimpdemod = 5
% 6.66/7.10 usesimpres = 3
% 6.66/7.10
% 6.66/7.10 resimpinuse = 1000
% 6.66/7.10 resimpclauses = 20000
% 6.66/7.10 substype = eqrewr
% 6.66/7.10 backwardsubs = 1
% 6.66/7.10 selectoldest = 5
% 6.66/7.10
% 6.66/7.10 litorderings [0] = split
% 6.66/7.10 litorderings [1] = extend the termordering, first sorting on arguments
% 6.66/7.10
% 6.66/7.10 termordering = kbo
% 6.66/7.10
% 6.66/7.10 litapriori = 0
% 6.66/7.10 termapriori = 1
% 6.66/7.10 litaposteriori = 0
% 6.66/7.10 termaposteriori = 0
% 6.66/7.10 demodaposteriori = 0
% 6.66/7.10 ordereqreflfact = 0
% 6.66/7.10
% 6.66/7.10 litselect = negord
% 6.66/7.10
% 6.66/7.10 maxweight = 15
% 6.66/7.10 maxdepth = 30000
% 6.66/7.10 maxlength = 115
% 6.66/7.10 maxnrvars = 195
% 6.66/7.10 excuselevel = 1
% 6.66/7.10 increasemaxweight = 1
% 6.66/7.10
% 6.66/7.10 maxselected = 10000000
% 6.66/7.10 maxnrclauses = 10000000
% 6.66/7.10
% 6.66/7.10 showgenerated = 0
% 6.66/7.10 showkept = 0
% 6.66/7.10 showselected = 0
% 6.66/7.10 showdeleted = 0
% 6.66/7.10 showresimp = 1
% 6.66/7.10 showstatus = 2000
% 6.66/7.10
% 6.66/7.10 prologoutput = 0
% 6.66/7.10 nrgoals = 5000000
% 6.66/7.10 totalproof = 1
% 6.66/7.10
% 6.66/7.10 Symbols occurring in the translation:
% 6.66/7.10
% 6.66/7.10 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 6.66/7.10 . [1, 2] (w:1, o:23, a:1, s:1, b:0),
% 6.66/7.10 ! [4, 1] (w:0, o:15, a:1, s:1, b:0),
% 6.66/7.10 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 6.66/7.10 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 6.66/7.10 addition [37, 2] (w:1, o:47, a:1, s:1, b:0),
% 6.66/7.10 zero [39, 0] (w:1, o:9, a:1, s:1, b:0),
% 6.66/7.10 multiplication [40, 2] (w:1, o:49, a:1, s:1, b:0),
% 6.66/7.10 one [41, 0] (w:1, o:10, a:1, s:1, b:0),
% 6.66/7.10 leq [42, 2] (w:1, o:48, a:1, s:1, b:0),
% 6.66/7.10 test [44, 1] (w:1, o:21, a:1, s:1, b:0),
% 6.66/7.10 complement [46, 2] (w:1, o:50, a:1, s:1, b:0),
% 6.66/7.10 c [47, 1] (w:1, o:22, a:1, s:1, b:0),
% 6.66/7.10 alpha1 [48, 2] (w:1, o:51, a:1, s:1, b:1),
% 6.66/7.10 skol1 [49, 1] (w:1, o:20, a:1, s:1, b:1),
% 6.66/7.10 skol2 [50, 0] (w:1, o:13, a:1, s:1, b:1),
% 6.66/7.10 skol3 [51, 0] (w:1, o:14, a:1, s:1, b:1).
% 6.66/7.10
% 6.66/7.10
% 6.66/7.10 Starting Search:
% 6.66/7.10
% 6.66/7.10 *** allocated 15000 integers for clauses
% 6.66/7.10 *** allocated 22500 integers for clauses
% 6.66/7.10 *** allocated 33750 integers for clauses
% 6.66/7.10 *** allocated 50625 integers for clauses
% 6.66/7.10 *** allocated 15000 integers for termspace/termends
% 6.66/7.10 *** allocated 75937 integers for clauses
% 6.66/7.10 Resimplifying inuse:
% 6.66/7.10 Done
% 6.66/7.10
% 6.66/7.10 *** allocated 22500 integers for termspace/termends
% 6.66/7.10 *** allocated 113905 integers for clauses
% 6.66/7.10 *** allocated 33750 integers for termspace/termends
% 6.66/7.10
% 6.66/7.10 Intermediate Status:
% 6.66/7.10 Generated: 16797
% 6.66/7.10 Kept: 2099
% 6.66/7.10 Inuse: 208
% 6.66/7.10 Deleted: 65
% 6.66/7.10 Deletedinuse: 12
% 6.66/7.10
% 6.66/7.10 Resimplifying inuse:
% 6.66/7.10 Done
% 6.66/7.10
% 6.66/7.10 *** allocated 170857 integers for clauses
% 6.66/7.10 *** allocated 50625 integers for termspace/termends
% 6.66/7.10 Resimplifying inuse:
% 6.66/7.10 Done
% 6.66/7.10
% 6.66/7.10 *** allocated 256285 integers for clauses
% 6.66/7.10
% 6.66/7.10 Intermediate Status:
% 6.66/7.10 Generated: 35171
% 6.66/7.10 Kept: 4117
% 6.66/7.10 Inuse: 360
% 6.66/7.10 Deleted: 224
% 6.66/7.10 Deletedinuse: 56
% 6.66/7.10
% 6.66/7.10 Resimplifying inuse:
% 6.66/7.10 Done
% 6.66/7.10
% 6.66/7.10 *** allocated 75937 integers for termspace/termends
% 6.66/7.10 *** allocated 384427 integers for clauses
% 6.66/7.10 Resimplifying inuse:
% 6.66/7.10 Done
% 6.66/7.10
% 6.66/7.10
% 6.66/7.10 Intermediate Status:
% 6.66/7.10 Generated: 50274
% 6.66/7.10 Kept: 6138
% 6.66/7.10 Inuse: 470
% 6.66/7.10 Deleted: 321
% 6.66/7.10 Deletedinuse: 72
% 6.66/7.10
% 6.66/7.10 Resimplifying inuse:
% 6.66/7.10 Done
% 6.66/7.10
% 6.66/7.10 *** allocated 113905 integers for termspace/termends
% 6.66/7.10 Resimplifying inuse:
% 6.66/7.10 Done
% 6.66/7.10
% 6.66/7.10 *** allocated 576640 integers for clauses
% 6.66/7.10
% 6.66/7.10 Intermediate Status:
% 6.66/7.10 Generated: 65628
% 6.66/7.10 Kept: 8141
% 6.66/7.10 Inuse: 545
% 6.66/7.10 Deleted: 328
% 6.66/7.10 Deletedinuse: 72
% 6.66/7.10
% 6.66/7.10 Resimplifying inuse:
% 6.66/7.10 Done
% 6.66/7.10
% 6.66/7.10 Resimplifying inuse:
% 6.66/7.10 Done
% 6.66/7.10
% 6.66/7.10 *** allocated 170857 integers for termspace/termends
% 6.66/7.10
% 6.66/7.10 Intermediate Status:
% 6.66/7.10 Generated: 85773
% 6.66/7.10 Kept: 10149
% 6.66/7.10 Inuse: 629
% 6.66/7.10 Deleted: 335
% 6.66/7.10 Deletedinuse: 72
% 6.66/7.10
% 6.66/7.10 Resimplifying inuse:
% 6.66/7.10 Done
% 6.66/7.10
% 6.66/7.10 Resimplifying inuse:
% 6.66/7.10 Done
% 6.66/7.10
% 6.66/7.10 *** allocated 864960 integers for clauses
% 6.66/7.10
% 6.66/7.10 Intermediate Status:
% 6.66/7.10 Generated: 95918
% 6.66/7.10 Kept: 12331
% 6.66/7.10 Inuse: 686
% 6.66/7.10 Deleted: 378
% 6.66/7.10 Deletedinuse: 106
% 6.66/7.10
% 6.66/7.10 Resimplifying inuse:
% 6.66/7.10 Done
% 6.66/7.10
% 6.66/7.10 Resimplifying inuse:
% 6.66/7.10 Done
% 6.66/7.10
% 6.66/7.10 *** allocated 256285 integers for termspace/termends
% 6.66/7.10
% 6.66/7.10 Intermediate Status:
% 6.66/7.10 Generated: 111607
% 6.66/7.10 Kept: 14507
% 6.66/7.10 Inuse: 754
% 6.66/7.10 Deleted: 516
% 6.66/7.10 Deletedinuse: 215
% 6.66/7.10
% 6.66/7.10 Resimplifying inuse:
% 6.66/7.10 Done
% 6.66/7.10
% 6.66/7.10 Resimplifying inuse:
% 6.66/7.10 Done
% 6.66/7.10
% 6.66/7.10
% 6.66/7.10 Intermediate Status:
% 6.66/7.10 Generated: 124176
% 6.66/7.10 Kept: 16535
% 6.66/7.10 Inuse: 807
% 6.66/7.10 Deleted: 626
% 6.66/7.10 Deletedinuse: 225
% 6.66/7.10
% 6.66/7.10 Resimplifying inuse:
% 6.66/7.10 Done
% 6.66/7.10
% 6.66/7.10 Resimplifying inuse:
% 6.66/7.10 Done
% 6.66/7.10
% 6.66/7.10
% 6.66/7.10 Intermediate Status:
% 6.66/7.10 Generated: 137204
% 6.66/7.10 Kept: 18606
% 6.66/7.10 Inuse: 864
% 6.66/7.10 Deleted: 693
% 6.66/7.10 Deletedinuse: 225
% 6.66/7.10
% 6.66/7.10 Resimplifying inuse:
% 6.66/7.10 Done
% 6.66/7.10
% 6.66/7.10 *** allocated 1297440 integers for clauses
% 6.66/7.10 Resimplifying inuse:
% 6.66/7.10 Done
% 6.66/7.10
% 6.66/7.10 Resimplifying clauses:
% 6.66/7.10
% 6.66/7.10 Bliksems!, er is een bewijs:
% 6.66/7.10 % SZS status Theorem
% 6.66/7.10 % SZS output start Refutation
% 6.66/7.10
% 6.66/7.10 (0) {G0,W7,D3,L1,V2,M1} I { addition( X, Y ) = addition( Y, X ) }.
% 6.66/7.10 (1) {G0,W11,D4,L1,V3,M1} I { addition( Z, addition( Y, X ) ) ==> addition(
% 6.66/7.10 addition( Z, Y ), X ) }.
% 6.66/7.10 (6) {G0,W5,D3,L1,V1,M1} I { multiplication( one, X ) ==> X }.
% 6.66/7.10 (7) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Y ),
% 6.66/7.10 multiplication( X, Z ) ) ==> multiplication( X, addition( Y, Z ) ) }.
% 6.66/7.10 (8) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Z ),
% 6.66/7.10 multiplication( Y, Z ) ) ==> multiplication( addition( X, Y ), Z ) }.
% 6.66/7.10 (13) {G0,W6,D3,L2,V1,M2} I { ! test( X ), complement( skol1( X ), X ) }.
% 6.66/7.10 (15) {G0,W8,D3,L2,V2,M2} I { ! complement( Y, X ), multiplication( X, Y )
% 6.66/7.10 ==> zero }.
% 6.66/7.10 (16) {G0,W6,D2,L2,V2,M2} I { ! complement( Y, X ), alpha1( X, Y ) }.
% 6.66/7.10 (17) {G0,W11,D3,L3,V2,M3} I { ! multiplication( X, Y ) ==> zero, ! alpha1(
% 6.66/7.10 X, Y ), complement( Y, X ) }.
% 6.66/7.10 (18) {G0,W8,D3,L2,V2,M2} I { ! alpha1( X, Y ), multiplication( Y, X ) ==>
% 6.66/7.10 zero }.
% 6.66/7.10 (19) {G0,W8,D3,L2,V2,M2} I { ! alpha1( X, Y ), addition( X, Y ) ==> one }.
% 6.66/7.10 (20) {G0,W13,D3,L3,V2,M3} I { ! multiplication( Y, X ) ==> zero, ! addition
% 6.66/7.10 ( X, Y ) ==> one, alpha1( X, Y ) }.
% 6.66/7.10 (22) {G0,W9,D3,L3,V2,M3} I { ! test( X ), ! complement( X, Y ), c( X ) = Y
% 6.66/7.10 }.
% 6.66/7.10 (24) {G0,W2,D2,L1,V0,M1} I { test( skol3 ) }.
% 6.66/7.10 (25) {G0,W2,D2,L1,V0,M1} I { test( skol2 ) }.
% 6.66/7.10 (26) {G1,W19,D7,L1,V0,M1} I;d(7) { ! addition( addition( multiplication(
% 6.66/7.10 skol2, addition( skol3, c( skol3 ) ) ), multiplication( c( skol2 ), skol3
% 6.66/7.10 ) ), multiplication( c( skol2 ), c( skol3 ) ) ) ==> one }.
% 6.66/7.10 (46) {G1,W17,D5,L1,V4,M1} P(7,1) { addition( addition( T, multiplication( X
% 6.66/7.10 , Y ) ), multiplication( X, Z ) ) ==> addition( T, multiplication( X,
% 6.66/7.10 addition( Y, Z ) ) ) }.
% 6.66/7.10 (179) {G1,W4,D3,L1,V0,M1} R(13,24) { complement( skol1( skol3 ), skol3 )
% 6.66/7.10 }.
% 6.66/7.10 (180) {G1,W4,D3,L1,V0,M1} R(13,25) { complement( skol1( skol2 ), skol2 )
% 6.66/7.10 }.
% 6.66/7.10 (183) {G2,W4,D3,L1,V0,M1} R(179,16) { alpha1( skol3, skol1( skol3 ) ) }.
% 6.66/7.10 (187) {G2,W4,D3,L1,V0,M1} R(180,16) { alpha1( skol2, skol1( skol2 ) ) }.
% 6.66/7.10 (190) {G2,W6,D4,L1,V0,M1} R(15,180) { multiplication( skol2, skol1( skol2 )
% 6.66/7.10 ) ==> zero }.
% 6.66/7.10 (191) {G2,W6,D4,L1,V0,M1} R(15,179) { multiplication( skol3, skol1( skol3 )
% 6.66/7.10 ) ==> zero }.
% 6.66/7.10 (232) {G3,W6,D4,L1,V0,M1} R(18,187) { multiplication( skol1( skol2 ), skol2
% 6.66/7.10 ) ==> zero }.
% 6.66/7.10 (233) {G3,W6,D4,L1,V0,M1} R(18,183) { multiplication( skol1( skol3 ), skol3
% 6.66/7.10 ) ==> zero }.
% 6.66/7.10 (258) {G3,W6,D4,L1,V0,M1} R(19,187) { addition( skol2, skol1( skol2 ) ) ==>
% 6.66/7.10 one }.
% 6.66/7.10 (259) {G3,W6,D4,L1,V0,M1} R(19,183) { addition( skol3, skol1( skol3 ) ) ==>
% 6.66/7.10 one }.
% 6.66/7.10 (432) {G2,W11,D5,L1,V0,M1} S(26);d(46);d(8) { ! multiplication( addition(
% 6.66/7.10 skol2, c( skol2 ) ), addition( skol3, c( skol3 ) ) ) ==> one }.
% 6.66/7.10 (2130) {G4,W6,D4,L1,V0,M1} P(258,0) { addition( skol1( skol2 ), skol2 ) ==>
% 6.66/7.10 one }.
% 6.66/7.10 (2167) {G5,W4,D3,L1,V0,M1} R(2130,20);d(190);q { alpha1( skol1( skol2 ),
% 6.66/7.10 skol2 ) }.
% 6.66/7.10 (2183) {G6,W4,D3,L1,V0,M1} R(2167,17);d(232);q { complement( skol2, skol1(
% 6.66/7.10 skol2 ) ) }.
% 6.66/7.10 (2187) {G7,W5,D3,L1,V0,M1} R(2183,22);r(25) { c( skol2 ) ==> skol1( skol2 )
% 6.66/7.10 }.
% 6.66/7.10 (2445) {G4,W6,D4,L1,V0,M1} P(259,0) { addition( skol1( skol3 ), skol3 ) ==>
% 6.66/7.10 one }.
% 6.66/7.10 (2482) {G5,W4,D3,L1,V0,M1} R(2445,20);d(191);q { alpha1( skol1( skol3 ),
% 6.66/7.10 skol3 ) }.
% 6.66/7.10 (2498) {G6,W4,D3,L1,V0,M1} R(2482,17);d(233);q { complement( skol3, skol1(
% 6.66/7.10 skol3 ) ) }.
% 6.66/7.10 (2502) {G7,W5,D3,L1,V0,M1} R(2498,22);r(24) { c( skol3 ) ==> skol1( skol3 )
% 6.66/7.10 }.
% 6.66/7.10 (20123) {G8,W0,D0,L0,V0,M0} S(432);d(2187);d(258);d(6);d(2502);d(259);q {
% 6.66/7.10 }.
% 6.66/7.10
% 6.66/7.10
% 6.66/7.10 % SZS output end Refutation
% 6.66/7.10 found a proof!
% 6.66/7.10
% 6.66/7.10
% 6.66/7.10 Unprocessed initial clauses:
% 6.66/7.10
% 6.66/7.10 (20125) {G0,W7,D3,L1,V2,M1} { addition( X, Y ) = addition( Y, X ) }.
% 6.66/7.10 (20126) {G0,W11,D4,L1,V3,M1} { addition( Z, addition( Y, X ) ) = addition
% 6.66/7.10 ( addition( Z, Y ), X ) }.
% 6.66/7.10 (20127) {G0,W5,D3,L1,V1,M1} { addition( X, zero ) = X }.
% 6.66/7.10 (20128) {G0,W5,D3,L1,V1,M1} { addition( X, X ) = X }.
% 6.66/7.10 (20129) {G0,W11,D4,L1,V3,M1} { multiplication( X, multiplication( Y, Z ) )
% 6.66/7.10 = multiplication( multiplication( X, Y ), Z ) }.
% 6.66/7.10 (20130) {G0,W5,D3,L1,V1,M1} { multiplication( X, one ) = X }.
% 6.66/7.10 (20131) {G0,W5,D3,L1,V1,M1} { multiplication( one, X ) = X }.
% 6.66/7.10 (20132) {G0,W13,D4,L1,V3,M1} { multiplication( X, addition( Y, Z ) ) =
% 6.66/7.10 addition( multiplication( X, Y ), multiplication( X, Z ) ) }.
% 6.66/7.10 (20133) {G0,W13,D4,L1,V3,M1} { multiplication( addition( X, Y ), Z ) =
% 6.66/7.10 addition( multiplication( X, Z ), multiplication( Y, Z ) ) }.
% 6.66/7.10 (20134) {G0,W5,D3,L1,V1,M1} { multiplication( X, zero ) = zero }.
% 6.66/7.10 (20135) {G0,W5,D3,L1,V1,M1} { multiplication( zero, X ) = zero }.
% 6.66/7.10 (20136) {G0,W8,D3,L2,V2,M2} { ! leq( X, Y ), addition( X, Y ) = Y }.
% 6.66/7.10 (20137) {G0,W8,D3,L2,V2,M2} { ! addition( X, Y ) = Y, leq( X, Y ) }.
% 6.66/7.10 (20138) {G0,W6,D3,L2,V1,M2} { ! test( X ), complement( skol1( X ), X ) }.
% 6.66/7.10 (20139) {G0,W5,D2,L2,V2,M2} { ! complement( Y, X ), test( X ) }.
% 6.66/7.10 (20140) {G0,W8,D3,L2,V2,M2} { ! complement( Y, X ), multiplication( X, Y )
% 6.66/7.10 = zero }.
% 6.66/7.10 (20141) {G0,W6,D2,L2,V2,M2} { ! complement( Y, X ), alpha1( X, Y ) }.
% 6.66/7.10 (20142) {G0,W11,D3,L3,V2,M3} { ! multiplication( X, Y ) = zero, ! alpha1(
% 6.66/7.10 X, Y ), complement( Y, X ) }.
% 6.74/7.10 (20143) {G0,W8,D3,L2,V2,M2} { ! alpha1( X, Y ), multiplication( Y, X ) =
% 6.74/7.10 zero }.
% 6.74/7.10 (20144) {G0,W8,D3,L2,V2,M2} { ! alpha1( X, Y ), addition( X, Y ) = one }.
% 6.74/7.10 (20145) {G0,W13,D3,L3,V2,M3} { ! multiplication( Y, X ) = zero, ! addition
% 6.74/7.10 ( X, Y ) = one, alpha1( X, Y ) }.
% 6.74/7.10 (20146) {G0,W9,D3,L3,V2,M3} { ! test( X ), ! c( X ) = Y, complement( X, Y
% 6.74/7.10 ) }.
% 6.74/7.10 (20147) {G0,W9,D3,L3,V2,M3} { ! test( X ), ! complement( X, Y ), c( X ) =
% 6.74/7.10 Y }.
% 6.74/7.10 (20148) {G0,W6,D3,L2,V1,M2} { test( X ), c( X ) = zero }.
% 6.74/7.10 (20149) {G0,W2,D2,L1,V0,M1} { test( skol3 ) }.
% 6.74/7.10 (20150) {G0,W2,D2,L1,V0,M1} { test( skol2 ) }.
% 6.74/7.10 (20151) {G0,W21,D7,L1,V0,M1} { ! one = addition( addition( addition(
% 6.74/7.10 multiplication( skol2, skol3 ), multiplication( skol2, c( skol3 ) ) ),
% 6.74/7.10 multiplication( c( skol2 ), skol3 ) ), multiplication( c( skol2 ), c(
% 6.74/7.10 skol3 ) ) ) }.
% 6.74/7.10
% 6.74/7.10
% 6.74/7.10 Total Proof:
% 6.74/7.10
% 6.74/7.10 subsumption: (0) {G0,W7,D3,L1,V2,M1} I { addition( X, Y ) = addition( Y, X
% 6.74/7.10 ) }.
% 6.74/7.10 parent0: (20125) {G0,W7,D3,L1,V2,M1} { addition( X, Y ) = addition( Y, X )
% 6.74/7.10 }.
% 6.74/7.10 substitution0:
% 6.74/7.10 X := X
% 6.74/7.10 Y := Y
% 6.74/7.10 end
% 6.74/7.10 permutation0:
% 6.74/7.10 0 ==> 0
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 subsumption: (1) {G0,W11,D4,L1,V3,M1} I { addition( Z, addition( Y, X ) )
% 6.74/7.10 ==> addition( addition( Z, Y ), X ) }.
% 6.74/7.10 parent0: (20126) {G0,W11,D4,L1,V3,M1} { addition( Z, addition( Y, X ) ) =
% 6.74/7.10 addition( addition( Z, Y ), X ) }.
% 6.74/7.10 substitution0:
% 6.74/7.10 X := X
% 6.74/7.10 Y := Y
% 6.74/7.10 Z := Z
% 6.74/7.10 end
% 6.74/7.10 permutation0:
% 6.74/7.10 0 ==> 0
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 subsumption: (6) {G0,W5,D3,L1,V1,M1} I { multiplication( one, X ) ==> X }.
% 6.74/7.10 parent0: (20131) {G0,W5,D3,L1,V1,M1} { multiplication( one, X ) = X }.
% 6.74/7.10 substitution0:
% 6.74/7.10 X := X
% 6.74/7.10 end
% 6.74/7.10 permutation0:
% 6.74/7.10 0 ==> 0
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 eqswap: (20165) {G0,W13,D4,L1,V3,M1} { addition( multiplication( X, Y ),
% 6.74/7.10 multiplication( X, Z ) ) = multiplication( X, addition( Y, Z ) ) }.
% 6.74/7.10 parent0[0]: (20132) {G0,W13,D4,L1,V3,M1} { multiplication( X, addition( Y
% 6.74/7.10 , Z ) ) = addition( multiplication( X, Y ), multiplication( X, Z ) ) }.
% 6.74/7.10 substitution0:
% 6.74/7.10 X := X
% 6.74/7.10 Y := Y
% 6.74/7.10 Z := Z
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 subsumption: (7) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Y )
% 6.74/7.10 , multiplication( X, Z ) ) ==> multiplication( X, addition( Y, Z ) ) }.
% 6.74/7.10 parent0: (20165) {G0,W13,D4,L1,V3,M1} { addition( multiplication( X, Y ),
% 6.74/7.10 multiplication( X, Z ) ) = multiplication( X, addition( Y, Z ) ) }.
% 6.74/7.10 substitution0:
% 6.74/7.10 X := X
% 6.74/7.10 Y := Y
% 6.74/7.10 Z := Z
% 6.74/7.10 end
% 6.74/7.10 permutation0:
% 6.74/7.10 0 ==> 0
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 eqswap: (20173) {G0,W13,D4,L1,V3,M1} { addition( multiplication( X, Z ),
% 6.74/7.10 multiplication( Y, Z ) ) = multiplication( addition( X, Y ), Z ) }.
% 6.74/7.10 parent0[0]: (20133) {G0,W13,D4,L1,V3,M1} { multiplication( addition( X, Y
% 6.74/7.10 ), Z ) = addition( multiplication( X, Z ), multiplication( Y, Z ) ) }.
% 6.74/7.10 substitution0:
% 6.74/7.10 X := X
% 6.74/7.10 Y := Y
% 6.74/7.10 Z := Z
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 subsumption: (8) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Z )
% 6.74/7.10 , multiplication( Y, Z ) ) ==> multiplication( addition( X, Y ), Z ) }.
% 6.74/7.10 parent0: (20173) {G0,W13,D4,L1,V3,M1} { addition( multiplication( X, Z ),
% 6.74/7.10 multiplication( Y, Z ) ) = multiplication( addition( X, Y ), Z ) }.
% 6.74/7.10 substitution0:
% 6.74/7.10 X := X
% 6.74/7.10 Y := Y
% 6.74/7.10 Z := Z
% 6.74/7.10 end
% 6.74/7.10 permutation0:
% 6.74/7.10 0 ==> 0
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 subsumption: (13) {G0,W6,D3,L2,V1,M2} I { ! test( X ), complement( skol1( X
% 6.74/7.10 ), X ) }.
% 6.74/7.10 parent0: (20138) {G0,W6,D3,L2,V1,M2} { ! test( X ), complement( skol1( X )
% 6.74/7.10 , X ) }.
% 6.74/7.10 substitution0:
% 6.74/7.10 X := X
% 6.74/7.10 end
% 6.74/7.10 permutation0:
% 6.74/7.10 0 ==> 0
% 6.74/7.10 1 ==> 1
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 subsumption: (15) {G0,W8,D3,L2,V2,M2} I { ! complement( Y, X ),
% 6.74/7.10 multiplication( X, Y ) ==> zero }.
% 6.74/7.10 parent0: (20140) {G0,W8,D3,L2,V2,M2} { ! complement( Y, X ),
% 6.74/7.10 multiplication( X, Y ) = zero }.
% 6.74/7.10 substitution0:
% 6.74/7.10 X := X
% 6.74/7.10 Y := Y
% 6.74/7.10 end
% 6.74/7.10 permutation0:
% 6.74/7.10 0 ==> 0
% 6.74/7.10 1 ==> 1
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 subsumption: (16) {G0,W6,D2,L2,V2,M2} I { ! complement( Y, X ), alpha1( X,
% 6.74/7.10 Y ) }.
% 6.74/7.10 parent0: (20141) {G0,W6,D2,L2,V2,M2} { ! complement( Y, X ), alpha1( X, Y
% 6.74/7.10 ) }.
% 6.74/7.10 substitution0:
% 6.74/7.10 X := X
% 6.74/7.10 Y := Y
% 6.74/7.10 end
% 6.74/7.10 permutation0:
% 6.74/7.10 0 ==> 0
% 6.74/7.10 1 ==> 1
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 subsumption: (17) {G0,W11,D3,L3,V2,M3} I { ! multiplication( X, Y ) ==>
% 6.74/7.10 zero, ! alpha1( X, Y ), complement( Y, X ) }.
% 6.74/7.10 parent0: (20142) {G0,W11,D3,L3,V2,M3} { ! multiplication( X, Y ) = zero, !
% 6.74/7.10 alpha1( X, Y ), complement( Y, X ) }.
% 6.74/7.10 substitution0:
% 6.74/7.10 X := X
% 6.74/7.10 Y := Y
% 6.74/7.10 end
% 6.74/7.10 permutation0:
% 6.74/7.10 0 ==> 0
% 6.74/7.10 1 ==> 1
% 6.74/7.10 2 ==> 2
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 subsumption: (18) {G0,W8,D3,L2,V2,M2} I { ! alpha1( X, Y ), multiplication
% 6.74/7.10 ( Y, X ) ==> zero }.
% 6.74/7.10 parent0: (20143) {G0,W8,D3,L2,V2,M2} { ! alpha1( X, Y ), multiplication( Y
% 6.74/7.10 , X ) = zero }.
% 6.74/7.10 substitution0:
% 6.74/7.10 X := X
% 6.74/7.10 Y := Y
% 6.74/7.10 end
% 6.74/7.10 permutation0:
% 6.74/7.10 0 ==> 0
% 6.74/7.10 1 ==> 1
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 subsumption: (19) {G0,W8,D3,L2,V2,M2} I { ! alpha1( X, Y ), addition( X, Y
% 6.74/7.10 ) ==> one }.
% 6.74/7.10 parent0: (20144) {G0,W8,D3,L2,V2,M2} { ! alpha1( X, Y ), addition( X, Y )
% 6.74/7.10 = one }.
% 6.74/7.10 substitution0:
% 6.74/7.10 X := X
% 6.74/7.10 Y := Y
% 6.74/7.10 end
% 6.74/7.10 permutation0:
% 6.74/7.10 0 ==> 0
% 6.74/7.10 1 ==> 1
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 subsumption: (20) {G0,W13,D3,L3,V2,M3} I { ! multiplication( Y, X ) ==>
% 6.74/7.10 zero, ! addition( X, Y ) ==> one, alpha1( X, Y ) }.
% 6.74/7.10 parent0: (20145) {G0,W13,D3,L3,V2,M3} { ! multiplication( Y, X ) = zero, !
% 6.74/7.10 addition( X, Y ) = one, alpha1( X, Y ) }.
% 6.74/7.10 substitution0:
% 6.74/7.10 X := X
% 6.74/7.10 Y := Y
% 6.74/7.10 end
% 6.74/7.10 permutation0:
% 6.74/7.10 0 ==> 0
% 6.74/7.10 1 ==> 1
% 6.74/7.10 2 ==> 2
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 subsumption: (22) {G0,W9,D3,L3,V2,M3} I { ! test( X ), ! complement( X, Y )
% 6.74/7.10 , c( X ) = Y }.
% 6.74/7.10 parent0: (20147) {G0,W9,D3,L3,V2,M3} { ! test( X ), ! complement( X, Y ),
% 6.74/7.10 c( X ) = Y }.
% 6.74/7.10 substitution0:
% 6.74/7.10 X := X
% 6.74/7.10 Y := Y
% 6.74/7.10 end
% 6.74/7.10 permutation0:
% 6.74/7.10 0 ==> 0
% 6.74/7.10 1 ==> 1
% 6.74/7.10 2 ==> 2
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 subsumption: (24) {G0,W2,D2,L1,V0,M1} I { test( skol3 ) }.
% 6.74/7.10 parent0: (20149) {G0,W2,D2,L1,V0,M1} { test( skol3 ) }.
% 6.74/7.10 substitution0:
% 6.74/7.10 end
% 6.74/7.10 permutation0:
% 6.74/7.10 0 ==> 0
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 subsumption: (25) {G0,W2,D2,L1,V0,M1} I { test( skol2 ) }.
% 6.74/7.10 parent0: (20150) {G0,W2,D2,L1,V0,M1} { test( skol2 ) }.
% 6.74/7.10 substitution0:
% 6.74/7.10 end
% 6.74/7.10 permutation0:
% 6.74/7.10 0 ==> 0
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 paramod: (20393) {G1,W19,D7,L1,V0,M1} { ! one = addition( addition(
% 6.74/7.10 multiplication( skol2, addition( skol3, c( skol3 ) ) ), multiplication( c
% 6.74/7.10 ( skol2 ), skol3 ) ), multiplication( c( skol2 ), c( skol3 ) ) ) }.
% 6.74/7.10 parent0[0]: (7) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Y ),
% 6.74/7.10 multiplication( X, Z ) ) ==> multiplication( X, addition( Y, Z ) ) }.
% 6.74/7.10 parent1[0; 5]: (20151) {G0,W21,D7,L1,V0,M1} { ! one = addition( addition(
% 6.74/7.10 addition( multiplication( skol2, skol3 ), multiplication( skol2, c( skol3
% 6.74/7.10 ) ) ), multiplication( c( skol2 ), skol3 ) ), multiplication( c( skol2 )
% 6.74/7.10 , c( skol3 ) ) ) }.
% 6.74/7.10 substitution0:
% 6.74/7.10 X := skol2
% 6.74/7.10 Y := skol3
% 6.74/7.10 Z := c( skol3 )
% 6.74/7.10 end
% 6.74/7.10 substitution1:
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 eqswap: (20394) {G1,W19,D7,L1,V0,M1} { ! addition( addition(
% 6.74/7.10 multiplication( skol2, addition( skol3, c( skol3 ) ) ), multiplication( c
% 6.74/7.10 ( skol2 ), skol3 ) ), multiplication( c( skol2 ), c( skol3 ) ) ) = one
% 6.74/7.10 }.
% 6.74/7.10 parent0[0]: (20393) {G1,W19,D7,L1,V0,M1} { ! one = addition( addition(
% 6.74/7.10 multiplication( skol2, addition( skol3, c( skol3 ) ) ), multiplication( c
% 6.74/7.10 ( skol2 ), skol3 ) ), multiplication( c( skol2 ), c( skol3 ) ) ) }.
% 6.74/7.10 substitution0:
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 subsumption: (26) {G1,W19,D7,L1,V0,M1} I;d(7) { ! addition( addition(
% 6.74/7.10 multiplication( skol2, addition( skol3, c( skol3 ) ) ), multiplication( c
% 6.74/7.10 ( skol2 ), skol3 ) ), multiplication( c( skol2 ), c( skol3 ) ) ) ==> one
% 6.74/7.10 }.
% 6.74/7.10 parent0: (20394) {G1,W19,D7,L1,V0,M1} { ! addition( addition(
% 6.74/7.10 multiplication( skol2, addition( skol3, c( skol3 ) ) ), multiplication( c
% 6.74/7.10 ( skol2 ), skol3 ) ), multiplication( c( skol2 ), c( skol3 ) ) ) = one
% 6.74/7.10 }.
% 6.74/7.10 substitution0:
% 6.74/7.10 end
% 6.74/7.10 permutation0:
% 6.74/7.10 0 ==> 0
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 eqswap: (20396) {G0,W11,D4,L1,V3,M1} { addition( addition( X, Y ), Z ) ==>
% 6.74/7.10 addition( X, addition( Y, Z ) ) }.
% 6.74/7.10 parent0[0]: (1) {G0,W11,D4,L1,V3,M1} I { addition( Z, addition( Y, X ) )
% 6.74/7.10 ==> addition( addition( Z, Y ), X ) }.
% 6.74/7.10 substitution0:
% 6.74/7.10 X := Z
% 6.74/7.10 Y := Y
% 6.74/7.10 Z := X
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 paramod: (20400) {G1,W17,D5,L1,V4,M1} { addition( addition( X,
% 6.74/7.10 multiplication( Y, Z ) ), multiplication( Y, T ) ) ==> addition( X,
% 6.74/7.10 multiplication( Y, addition( Z, T ) ) ) }.
% 6.74/7.10 parent0[0]: (7) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Y ),
% 6.74/7.10 multiplication( X, Z ) ) ==> multiplication( X, addition( Y, Z ) ) }.
% 6.74/7.10 parent1[0; 12]: (20396) {G0,W11,D4,L1,V3,M1} { addition( addition( X, Y )
% 6.74/7.10 , Z ) ==> addition( X, addition( Y, Z ) ) }.
% 6.74/7.10 substitution0:
% 6.74/7.10 X := Y
% 6.74/7.10 Y := Z
% 6.74/7.10 Z := T
% 6.74/7.10 end
% 6.74/7.10 substitution1:
% 6.74/7.10 X := X
% 6.74/7.10 Y := multiplication( Y, Z )
% 6.74/7.10 Z := multiplication( Y, T )
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 subsumption: (46) {G1,W17,D5,L1,V4,M1} P(7,1) { addition( addition( T,
% 6.74/7.10 multiplication( X, Y ) ), multiplication( X, Z ) ) ==> addition( T,
% 6.74/7.10 multiplication( X, addition( Y, Z ) ) ) }.
% 6.74/7.10 parent0: (20400) {G1,W17,D5,L1,V4,M1} { addition( addition( X,
% 6.74/7.10 multiplication( Y, Z ) ), multiplication( Y, T ) ) ==> addition( X,
% 6.74/7.10 multiplication( Y, addition( Z, T ) ) ) }.
% 6.74/7.10 substitution0:
% 6.74/7.10 X := T
% 6.74/7.10 Y := X
% 6.74/7.10 Z := Y
% 6.74/7.10 T := Z
% 6.74/7.10 end
% 6.74/7.10 permutation0:
% 6.74/7.10 0 ==> 0
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 resolution: (20403) {G1,W4,D3,L1,V0,M1} { complement( skol1( skol3 ),
% 6.74/7.10 skol3 ) }.
% 6.74/7.10 parent0[0]: (13) {G0,W6,D3,L2,V1,M2} I { ! test( X ), complement( skol1( X
% 6.74/7.10 ), X ) }.
% 6.74/7.10 parent1[0]: (24) {G0,W2,D2,L1,V0,M1} I { test( skol3 ) }.
% 6.74/7.10 substitution0:
% 6.74/7.10 X := skol3
% 6.74/7.10 end
% 6.74/7.10 substitution1:
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 subsumption: (179) {G1,W4,D3,L1,V0,M1} R(13,24) { complement( skol1( skol3
% 6.74/7.10 ), skol3 ) }.
% 6.74/7.10 parent0: (20403) {G1,W4,D3,L1,V0,M1} { complement( skol1( skol3 ), skol3 )
% 6.74/7.10 }.
% 6.74/7.10 substitution0:
% 6.74/7.10 end
% 6.74/7.10 permutation0:
% 6.74/7.10 0 ==> 0
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 resolution: (20404) {G1,W4,D3,L1,V0,M1} { complement( skol1( skol2 ),
% 6.74/7.10 skol2 ) }.
% 6.74/7.10 parent0[0]: (13) {G0,W6,D3,L2,V1,M2} I { ! test( X ), complement( skol1( X
% 6.74/7.10 ), X ) }.
% 6.74/7.10 parent1[0]: (25) {G0,W2,D2,L1,V0,M1} I { test( skol2 ) }.
% 6.74/7.10 substitution0:
% 6.74/7.10 X := skol2
% 6.74/7.10 end
% 6.74/7.10 substitution1:
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 subsumption: (180) {G1,W4,D3,L1,V0,M1} R(13,25) { complement( skol1( skol2
% 6.74/7.10 ), skol2 ) }.
% 6.74/7.10 parent0: (20404) {G1,W4,D3,L1,V0,M1} { complement( skol1( skol2 ), skol2 )
% 6.74/7.10 }.
% 6.74/7.10 substitution0:
% 6.74/7.10 end
% 6.74/7.10 permutation0:
% 6.74/7.10 0 ==> 0
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 resolution: (20405) {G1,W4,D3,L1,V0,M1} { alpha1( skol3, skol1( skol3 ) )
% 6.74/7.10 }.
% 6.74/7.10 parent0[0]: (16) {G0,W6,D2,L2,V2,M2} I { ! complement( Y, X ), alpha1( X, Y
% 6.74/7.10 ) }.
% 6.74/7.10 parent1[0]: (179) {G1,W4,D3,L1,V0,M1} R(13,24) { complement( skol1( skol3 )
% 6.74/7.10 , skol3 ) }.
% 6.74/7.10 substitution0:
% 6.74/7.10 X := skol3
% 6.74/7.10 Y := skol1( skol3 )
% 6.74/7.10 end
% 6.74/7.10 substitution1:
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 subsumption: (183) {G2,W4,D3,L1,V0,M1} R(179,16) { alpha1( skol3, skol1(
% 6.74/7.10 skol3 ) ) }.
% 6.74/7.10 parent0: (20405) {G1,W4,D3,L1,V0,M1} { alpha1( skol3, skol1( skol3 ) ) }.
% 6.74/7.10 substitution0:
% 6.74/7.10 end
% 6.74/7.10 permutation0:
% 6.74/7.10 0 ==> 0
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 resolution: (20406) {G1,W4,D3,L1,V0,M1} { alpha1( skol2, skol1( skol2 ) )
% 6.74/7.10 }.
% 6.74/7.10 parent0[0]: (16) {G0,W6,D2,L2,V2,M2} I { ! complement( Y, X ), alpha1( X, Y
% 6.74/7.10 ) }.
% 6.74/7.10 parent1[0]: (180) {G1,W4,D3,L1,V0,M1} R(13,25) { complement( skol1( skol2 )
% 6.74/7.10 , skol2 ) }.
% 6.74/7.10 substitution0:
% 6.74/7.10 X := skol2
% 6.74/7.10 Y := skol1( skol2 )
% 6.74/7.10 end
% 6.74/7.10 substitution1:
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 subsumption: (187) {G2,W4,D3,L1,V0,M1} R(180,16) { alpha1( skol2, skol1(
% 6.74/7.10 skol2 ) ) }.
% 6.74/7.10 parent0: (20406) {G1,W4,D3,L1,V0,M1} { alpha1( skol2, skol1( skol2 ) ) }.
% 6.74/7.10 substitution0:
% 6.74/7.10 end
% 6.74/7.10 permutation0:
% 6.74/7.10 0 ==> 0
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 eqswap: (20407) {G0,W8,D3,L2,V2,M2} { zero ==> multiplication( X, Y ), !
% 6.74/7.10 complement( Y, X ) }.
% 6.74/7.10 parent0[1]: (15) {G0,W8,D3,L2,V2,M2} I { ! complement( Y, X ),
% 6.74/7.10 multiplication( X, Y ) ==> zero }.
% 6.74/7.10 substitution0:
% 6.74/7.10 X := X
% 6.74/7.10 Y := Y
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 resolution: (20408) {G1,W6,D4,L1,V0,M1} { zero ==> multiplication( skol2,
% 6.74/7.10 skol1( skol2 ) ) }.
% 6.74/7.10 parent0[1]: (20407) {G0,W8,D3,L2,V2,M2} { zero ==> multiplication( X, Y )
% 6.74/7.10 , ! complement( Y, X ) }.
% 6.74/7.10 parent1[0]: (180) {G1,W4,D3,L1,V0,M1} R(13,25) { complement( skol1( skol2 )
% 6.74/7.10 , skol2 ) }.
% 6.74/7.10 substitution0:
% 6.74/7.10 X := skol2
% 6.74/7.10 Y := skol1( skol2 )
% 6.74/7.10 end
% 6.74/7.10 substitution1:
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 eqswap: (20409) {G1,W6,D4,L1,V0,M1} { multiplication( skol2, skol1( skol2
% 6.74/7.10 ) ) ==> zero }.
% 6.74/7.10 parent0[0]: (20408) {G1,W6,D4,L1,V0,M1} { zero ==> multiplication( skol2,
% 6.74/7.10 skol1( skol2 ) ) }.
% 6.74/7.10 substitution0:
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 subsumption: (190) {G2,W6,D4,L1,V0,M1} R(15,180) { multiplication( skol2,
% 6.74/7.10 skol1( skol2 ) ) ==> zero }.
% 6.74/7.10 parent0: (20409) {G1,W6,D4,L1,V0,M1} { multiplication( skol2, skol1( skol2
% 6.74/7.10 ) ) ==> zero }.
% 6.74/7.10 substitution0:
% 6.74/7.10 end
% 6.74/7.10 permutation0:
% 6.74/7.10 0 ==> 0
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 eqswap: (20410) {G0,W8,D3,L2,V2,M2} { zero ==> multiplication( X, Y ), !
% 6.74/7.10 complement( Y, X ) }.
% 6.74/7.10 parent0[1]: (15) {G0,W8,D3,L2,V2,M2} I { ! complement( Y, X ),
% 6.74/7.10 multiplication( X, Y ) ==> zero }.
% 6.74/7.10 substitution0:
% 6.74/7.10 X := X
% 6.74/7.10 Y := Y
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 resolution: (20411) {G1,W6,D4,L1,V0,M1} { zero ==> multiplication( skol3,
% 6.74/7.10 skol1( skol3 ) ) }.
% 6.74/7.10 parent0[1]: (20410) {G0,W8,D3,L2,V2,M2} { zero ==> multiplication( X, Y )
% 6.74/7.10 , ! complement( Y, X ) }.
% 6.74/7.10 parent1[0]: (179) {G1,W4,D3,L1,V0,M1} R(13,24) { complement( skol1( skol3 )
% 6.74/7.10 , skol3 ) }.
% 6.74/7.10 substitution0:
% 6.74/7.10 X := skol3
% 6.74/7.10 Y := skol1( skol3 )
% 6.74/7.10 end
% 6.74/7.10 substitution1:
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 eqswap: (20412) {G1,W6,D4,L1,V0,M1} { multiplication( skol3, skol1( skol3
% 6.74/7.10 ) ) ==> zero }.
% 6.74/7.10 parent0[0]: (20411) {G1,W6,D4,L1,V0,M1} { zero ==> multiplication( skol3,
% 6.74/7.10 skol1( skol3 ) ) }.
% 6.74/7.10 substitution0:
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 subsumption: (191) {G2,W6,D4,L1,V0,M1} R(15,179) { multiplication( skol3,
% 6.74/7.10 skol1( skol3 ) ) ==> zero }.
% 6.74/7.10 parent0: (20412) {G1,W6,D4,L1,V0,M1} { multiplication( skol3, skol1( skol3
% 6.74/7.10 ) ) ==> zero }.
% 6.74/7.10 substitution0:
% 6.74/7.10 end
% 6.74/7.10 permutation0:
% 6.74/7.10 0 ==> 0
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 eqswap: (20413) {G0,W8,D3,L2,V2,M2} { zero ==> multiplication( X, Y ), !
% 6.74/7.10 alpha1( Y, X ) }.
% 6.74/7.10 parent0[1]: (18) {G0,W8,D3,L2,V2,M2} I { ! alpha1( X, Y ), multiplication(
% 6.74/7.10 Y, X ) ==> zero }.
% 6.74/7.10 substitution0:
% 6.74/7.10 X := Y
% 6.74/7.10 Y := X
% 6.74/7.10 end
% 6.74/7.10
% 6.74/7.10 resolution: (20414) {G1,W6,D4,L1,V0,M1} { zero ==> multiplication( skol1(
% 6.74/7.10 skol2 ), skol2 ) }.
% 6.74/7.10 parent0[1]: (20413) {G0,W8,D3,L2,V2,M2} { zero ==> multiplication( X, Y )
% 6.74/7.10 , ! alpha1( Y, X ) }.
% 6.74/7.10 parent1[0]: (187) {G2,W4,D3,L1,V0,M1} R(180,16) { alpha1( skol2, skol1(
% 6.74/7.11 skol2 ) ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 X := skol1( skol2 )
% 6.74/7.11 Y := skol2
% 6.74/7.11 end
% 6.74/7.11 substitution1:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 eqswap: (20415) {G1,W6,D4,L1,V0,M1} { multiplication( skol1( skol2 ),
% 6.74/7.11 skol2 ) ==> zero }.
% 6.74/7.11 parent0[0]: (20414) {G1,W6,D4,L1,V0,M1} { zero ==> multiplication( skol1(
% 6.74/7.11 skol2 ), skol2 ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 subsumption: (232) {G3,W6,D4,L1,V0,M1} R(18,187) { multiplication( skol1(
% 6.74/7.11 skol2 ), skol2 ) ==> zero }.
% 6.74/7.11 parent0: (20415) {G1,W6,D4,L1,V0,M1} { multiplication( skol1( skol2 ),
% 6.74/7.11 skol2 ) ==> zero }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11 permutation0:
% 6.74/7.11 0 ==> 0
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 eqswap: (20416) {G0,W8,D3,L2,V2,M2} { zero ==> multiplication( X, Y ), !
% 6.74/7.11 alpha1( Y, X ) }.
% 6.74/7.11 parent0[1]: (18) {G0,W8,D3,L2,V2,M2} I { ! alpha1( X, Y ), multiplication(
% 6.74/7.11 Y, X ) ==> zero }.
% 6.74/7.11 substitution0:
% 6.74/7.11 X := Y
% 6.74/7.11 Y := X
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 resolution: (20417) {G1,W6,D4,L1,V0,M1} { zero ==> multiplication( skol1(
% 6.74/7.11 skol3 ), skol3 ) }.
% 6.74/7.11 parent0[1]: (20416) {G0,W8,D3,L2,V2,M2} { zero ==> multiplication( X, Y )
% 6.74/7.11 , ! alpha1( Y, X ) }.
% 6.74/7.11 parent1[0]: (183) {G2,W4,D3,L1,V0,M1} R(179,16) { alpha1( skol3, skol1(
% 6.74/7.11 skol3 ) ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 X := skol1( skol3 )
% 6.74/7.11 Y := skol3
% 6.74/7.11 end
% 6.74/7.11 substitution1:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 eqswap: (20418) {G1,W6,D4,L1,V0,M1} { multiplication( skol1( skol3 ),
% 6.74/7.11 skol3 ) ==> zero }.
% 6.74/7.11 parent0[0]: (20417) {G1,W6,D4,L1,V0,M1} { zero ==> multiplication( skol1(
% 6.74/7.11 skol3 ), skol3 ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 subsumption: (233) {G3,W6,D4,L1,V0,M1} R(18,183) { multiplication( skol1(
% 6.74/7.11 skol3 ), skol3 ) ==> zero }.
% 6.74/7.11 parent0: (20418) {G1,W6,D4,L1,V0,M1} { multiplication( skol1( skol3 ),
% 6.74/7.11 skol3 ) ==> zero }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11 permutation0:
% 6.74/7.11 0 ==> 0
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 eqswap: (20419) {G0,W8,D3,L2,V2,M2} { one ==> addition( X, Y ), ! alpha1(
% 6.74/7.11 X, Y ) }.
% 6.74/7.11 parent0[1]: (19) {G0,W8,D3,L2,V2,M2} I { ! alpha1( X, Y ), addition( X, Y )
% 6.74/7.11 ==> one }.
% 6.74/7.11 substitution0:
% 6.74/7.11 X := X
% 6.74/7.11 Y := Y
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 resolution: (20420) {G1,W6,D4,L1,V0,M1} { one ==> addition( skol2, skol1(
% 6.74/7.11 skol2 ) ) }.
% 6.74/7.11 parent0[1]: (20419) {G0,W8,D3,L2,V2,M2} { one ==> addition( X, Y ), !
% 6.74/7.11 alpha1( X, Y ) }.
% 6.74/7.11 parent1[0]: (187) {G2,W4,D3,L1,V0,M1} R(180,16) { alpha1( skol2, skol1(
% 6.74/7.11 skol2 ) ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 X := skol2
% 6.74/7.11 Y := skol1( skol2 )
% 6.74/7.11 end
% 6.74/7.11 substitution1:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 eqswap: (20421) {G1,W6,D4,L1,V0,M1} { addition( skol2, skol1( skol2 ) )
% 6.74/7.11 ==> one }.
% 6.74/7.11 parent0[0]: (20420) {G1,W6,D4,L1,V0,M1} { one ==> addition( skol2, skol1(
% 6.74/7.11 skol2 ) ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 subsumption: (258) {G3,W6,D4,L1,V0,M1} R(19,187) { addition( skol2, skol1(
% 6.74/7.11 skol2 ) ) ==> one }.
% 6.74/7.11 parent0: (20421) {G1,W6,D4,L1,V0,M1} { addition( skol2, skol1( skol2 ) )
% 6.74/7.11 ==> one }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11 permutation0:
% 6.74/7.11 0 ==> 0
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 eqswap: (20422) {G0,W8,D3,L2,V2,M2} { one ==> addition( X, Y ), ! alpha1(
% 6.74/7.11 X, Y ) }.
% 6.74/7.11 parent0[1]: (19) {G0,W8,D3,L2,V2,M2} I { ! alpha1( X, Y ), addition( X, Y )
% 6.74/7.11 ==> one }.
% 6.74/7.11 substitution0:
% 6.74/7.11 X := X
% 6.74/7.11 Y := Y
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 resolution: (20423) {G1,W6,D4,L1,V0,M1} { one ==> addition( skol3, skol1(
% 6.74/7.11 skol3 ) ) }.
% 6.74/7.11 parent0[1]: (20422) {G0,W8,D3,L2,V2,M2} { one ==> addition( X, Y ), !
% 6.74/7.11 alpha1( X, Y ) }.
% 6.74/7.11 parent1[0]: (183) {G2,W4,D3,L1,V0,M1} R(179,16) { alpha1( skol3, skol1(
% 6.74/7.11 skol3 ) ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 X := skol3
% 6.74/7.11 Y := skol1( skol3 )
% 6.74/7.11 end
% 6.74/7.11 substitution1:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 eqswap: (20424) {G1,W6,D4,L1,V0,M1} { addition( skol3, skol1( skol3 ) )
% 6.74/7.11 ==> one }.
% 6.74/7.11 parent0[0]: (20423) {G1,W6,D4,L1,V0,M1} { one ==> addition( skol3, skol1(
% 6.74/7.11 skol3 ) ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 subsumption: (259) {G3,W6,D4,L1,V0,M1} R(19,183) { addition( skol3, skol1(
% 6.74/7.11 skol3 ) ) ==> one }.
% 6.74/7.11 parent0: (20424) {G1,W6,D4,L1,V0,M1} { addition( skol3, skol1( skol3 ) )
% 6.74/7.11 ==> one }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11 permutation0:
% 6.74/7.11 0 ==> 0
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 paramod: (20428) {G2,W16,D6,L1,V0,M1} { ! addition( multiplication( skol2
% 6.74/7.11 , addition( skol3, c( skol3 ) ) ), multiplication( c( skol2 ), addition(
% 6.74/7.11 skol3, c( skol3 ) ) ) ) ==> one }.
% 6.74/7.11 parent0[0]: (46) {G1,W17,D5,L1,V4,M1} P(7,1) { addition( addition( T,
% 6.74/7.11 multiplication( X, Y ) ), multiplication( X, Z ) ) ==> addition( T,
% 6.74/7.11 multiplication( X, addition( Y, Z ) ) ) }.
% 6.74/7.11 parent1[0; 2]: (26) {G1,W19,D7,L1,V0,M1} I;d(7) { ! addition( addition(
% 6.74/7.11 multiplication( skol2, addition( skol3, c( skol3 ) ) ), multiplication( c
% 6.74/7.11 ( skol2 ), skol3 ) ), multiplication( c( skol2 ), c( skol3 ) ) ) ==> one
% 6.74/7.11 }.
% 6.74/7.11 substitution0:
% 6.74/7.11 X := c( skol2 )
% 6.74/7.11 Y := skol3
% 6.74/7.11 Z := c( skol3 )
% 6.74/7.11 T := multiplication( skol2, addition( skol3, c( skol3 ) ) )
% 6.74/7.11 end
% 6.74/7.11 substitution1:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 paramod: (20429) {G1,W11,D5,L1,V0,M1} { ! multiplication( addition( skol2
% 6.74/7.11 , c( skol2 ) ), addition( skol3, c( skol3 ) ) ) ==> one }.
% 6.74/7.11 parent0[0]: (8) {G0,W13,D4,L1,V3,M1} I { addition( multiplication( X, Z ),
% 6.74/7.11 multiplication( Y, Z ) ) ==> multiplication( addition( X, Y ), Z ) }.
% 6.74/7.11 parent1[0; 2]: (20428) {G2,W16,D6,L1,V0,M1} { ! addition( multiplication(
% 6.74/7.11 skol2, addition( skol3, c( skol3 ) ) ), multiplication( c( skol2 ),
% 6.74/7.11 addition( skol3, c( skol3 ) ) ) ) ==> one }.
% 6.74/7.11 substitution0:
% 6.74/7.11 X := skol2
% 6.74/7.11 Y := c( skol2 )
% 6.74/7.11 Z := addition( skol3, c( skol3 ) )
% 6.74/7.11 end
% 6.74/7.11 substitution1:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 subsumption: (432) {G2,W11,D5,L1,V0,M1} S(26);d(46);d(8) { ! multiplication
% 6.74/7.11 ( addition( skol2, c( skol2 ) ), addition( skol3, c( skol3 ) ) ) ==> one
% 6.74/7.11 }.
% 6.74/7.11 parent0: (20429) {G1,W11,D5,L1,V0,M1} { ! multiplication( addition( skol2
% 6.74/7.11 , c( skol2 ) ), addition( skol3, c( skol3 ) ) ) ==> one }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11 permutation0:
% 6.74/7.11 0 ==> 0
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 eqswap: (20431) {G3,W6,D4,L1,V0,M1} { one ==> addition( skol2, skol1(
% 6.74/7.11 skol2 ) ) }.
% 6.74/7.11 parent0[0]: (258) {G3,W6,D4,L1,V0,M1} R(19,187) { addition( skol2, skol1(
% 6.74/7.11 skol2 ) ) ==> one }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 paramod: (20432) {G1,W6,D4,L1,V0,M1} { one ==> addition( skol1( skol2 ),
% 6.74/7.11 skol2 ) }.
% 6.74/7.11 parent0[0]: (0) {G0,W7,D3,L1,V2,M1} I { addition( X, Y ) = addition( Y, X )
% 6.74/7.11 }.
% 6.74/7.11 parent1[0; 2]: (20431) {G3,W6,D4,L1,V0,M1} { one ==> addition( skol2,
% 6.74/7.11 skol1( skol2 ) ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 X := skol2
% 6.74/7.11 Y := skol1( skol2 )
% 6.74/7.11 end
% 6.74/7.11 substitution1:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 eqswap: (20435) {G1,W6,D4,L1,V0,M1} { addition( skol1( skol2 ), skol2 )
% 6.74/7.11 ==> one }.
% 6.74/7.11 parent0[0]: (20432) {G1,W6,D4,L1,V0,M1} { one ==> addition( skol1( skol2 )
% 6.74/7.11 , skol2 ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 subsumption: (2130) {G4,W6,D4,L1,V0,M1} P(258,0) { addition( skol1( skol2 )
% 6.74/7.11 , skol2 ) ==> one }.
% 6.74/7.11 parent0: (20435) {G1,W6,D4,L1,V0,M1} { addition( skol1( skol2 ), skol2 )
% 6.74/7.11 ==> one }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11 permutation0:
% 6.74/7.11 0 ==> 0
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 eqswap: (20436) {G4,W6,D4,L1,V0,M1} { one ==> addition( skol1( skol2 ),
% 6.74/7.11 skol2 ) }.
% 6.74/7.11 parent0[0]: (2130) {G4,W6,D4,L1,V0,M1} P(258,0) { addition( skol1( skol2 )
% 6.74/7.11 , skol2 ) ==> one }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 eqswap: (20438) {G0,W13,D3,L3,V2,M3} { ! one ==> addition( X, Y ), !
% 6.74/7.11 multiplication( Y, X ) ==> zero, alpha1( X, Y ) }.
% 6.74/7.11 parent0[1]: (20) {G0,W13,D3,L3,V2,M3} I { ! multiplication( Y, X ) ==> zero
% 6.74/7.11 , ! addition( X, Y ) ==> one, alpha1( X, Y ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 X := X
% 6.74/7.11 Y := Y
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 eqswap: (20439) {G0,W13,D3,L3,V2,M3} { ! zero ==> multiplication( X, Y ),
% 6.74/7.11 ! one ==> addition( Y, X ), alpha1( Y, X ) }.
% 6.74/7.11 parent0[1]: (20438) {G0,W13,D3,L3,V2,M3} { ! one ==> addition( X, Y ), !
% 6.74/7.11 multiplication( Y, X ) ==> zero, alpha1( X, Y ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 X := Y
% 6.74/7.11 Y := X
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 resolution: (20441) {G1,W10,D4,L2,V0,M2} { ! zero ==> multiplication(
% 6.74/7.11 skol2, skol1( skol2 ) ), alpha1( skol1( skol2 ), skol2 ) }.
% 6.74/7.11 parent0[1]: (20439) {G0,W13,D3,L3,V2,M3} { ! zero ==> multiplication( X, Y
% 6.74/7.11 ), ! one ==> addition( Y, X ), alpha1( Y, X ) }.
% 6.74/7.11 parent1[0]: (20436) {G4,W6,D4,L1,V0,M1} { one ==> addition( skol1( skol2 )
% 6.74/7.11 , skol2 ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 X := skol2
% 6.74/7.11 Y := skol1( skol2 )
% 6.74/7.11 end
% 6.74/7.11 substitution1:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 paramod: (20442) {G2,W7,D3,L2,V0,M2} { ! zero ==> zero, alpha1( skol1(
% 6.74/7.11 skol2 ), skol2 ) }.
% 6.74/7.11 parent0[0]: (190) {G2,W6,D4,L1,V0,M1} R(15,180) { multiplication( skol2,
% 6.74/7.11 skol1( skol2 ) ) ==> zero }.
% 6.74/7.11 parent1[0; 3]: (20441) {G1,W10,D4,L2,V0,M2} { ! zero ==> multiplication(
% 6.74/7.11 skol2, skol1( skol2 ) ), alpha1( skol1( skol2 ), skol2 ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11 substitution1:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 eqrefl: (20443) {G0,W4,D3,L1,V0,M1} { alpha1( skol1( skol2 ), skol2 ) }.
% 6.74/7.11 parent0[0]: (20442) {G2,W7,D3,L2,V0,M2} { ! zero ==> zero, alpha1( skol1(
% 6.74/7.11 skol2 ), skol2 ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 subsumption: (2167) {G5,W4,D3,L1,V0,M1} R(2130,20);d(190);q { alpha1( skol1
% 6.74/7.11 ( skol2 ), skol2 ) }.
% 6.74/7.11 parent0: (20443) {G0,W4,D3,L1,V0,M1} { alpha1( skol1( skol2 ), skol2 ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11 permutation0:
% 6.74/7.11 0 ==> 0
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 eqswap: (20444) {G0,W11,D3,L3,V2,M3} { ! zero ==> multiplication( X, Y ),
% 6.74/7.11 ! alpha1( X, Y ), complement( Y, X ) }.
% 6.74/7.11 parent0[0]: (17) {G0,W11,D3,L3,V2,M3} I { ! multiplication( X, Y ) ==> zero
% 6.74/7.11 , ! alpha1( X, Y ), complement( Y, X ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 X := X
% 6.74/7.11 Y := Y
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 resolution: (20446) {G1,W10,D4,L2,V0,M2} { ! zero ==> multiplication(
% 6.74/7.11 skol1( skol2 ), skol2 ), complement( skol2, skol1( skol2 ) ) }.
% 6.74/7.11 parent0[1]: (20444) {G0,W11,D3,L3,V2,M3} { ! zero ==> multiplication( X, Y
% 6.74/7.11 ), ! alpha1( X, Y ), complement( Y, X ) }.
% 6.74/7.11 parent1[0]: (2167) {G5,W4,D3,L1,V0,M1} R(2130,20);d(190);q { alpha1( skol1
% 6.74/7.11 ( skol2 ), skol2 ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 X := skol1( skol2 )
% 6.74/7.11 Y := skol2
% 6.74/7.11 end
% 6.74/7.11 substitution1:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 paramod: (20447) {G2,W7,D3,L2,V0,M2} { ! zero ==> zero, complement( skol2
% 6.74/7.11 , skol1( skol2 ) ) }.
% 6.74/7.11 parent0[0]: (232) {G3,W6,D4,L1,V0,M1} R(18,187) { multiplication( skol1(
% 6.74/7.11 skol2 ), skol2 ) ==> zero }.
% 6.74/7.11 parent1[0; 3]: (20446) {G1,W10,D4,L2,V0,M2} { ! zero ==> multiplication(
% 6.74/7.11 skol1( skol2 ), skol2 ), complement( skol2, skol1( skol2 ) ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11 substitution1:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 eqrefl: (20448) {G0,W4,D3,L1,V0,M1} { complement( skol2, skol1( skol2 ) )
% 6.74/7.11 }.
% 6.74/7.11 parent0[0]: (20447) {G2,W7,D3,L2,V0,M2} { ! zero ==> zero, complement(
% 6.74/7.11 skol2, skol1( skol2 ) ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 subsumption: (2183) {G6,W4,D3,L1,V0,M1} R(2167,17);d(232);q { complement(
% 6.74/7.11 skol2, skol1( skol2 ) ) }.
% 6.74/7.11 parent0: (20448) {G0,W4,D3,L1,V0,M1} { complement( skol2, skol1( skol2 ) )
% 6.74/7.11 }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11 permutation0:
% 6.74/7.11 0 ==> 0
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 eqswap: (20449) {G0,W9,D3,L3,V2,M3} { Y = c( X ), ! test( X ), !
% 6.74/7.11 complement( X, Y ) }.
% 6.74/7.11 parent0[2]: (22) {G0,W9,D3,L3,V2,M3} I { ! test( X ), ! complement( X, Y )
% 6.74/7.11 , c( X ) = Y }.
% 6.74/7.11 substitution0:
% 6.74/7.11 X := X
% 6.74/7.11 Y := Y
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 resolution: (20450) {G1,W7,D3,L2,V0,M2} { skol1( skol2 ) = c( skol2 ), !
% 6.74/7.11 test( skol2 ) }.
% 6.74/7.11 parent0[2]: (20449) {G0,W9,D3,L3,V2,M3} { Y = c( X ), ! test( X ), !
% 6.74/7.11 complement( X, Y ) }.
% 6.74/7.11 parent1[0]: (2183) {G6,W4,D3,L1,V0,M1} R(2167,17);d(232);q { complement(
% 6.74/7.11 skol2, skol1( skol2 ) ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 X := skol2
% 6.74/7.11 Y := skol1( skol2 )
% 6.74/7.11 end
% 6.74/7.11 substitution1:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 resolution: (20451) {G1,W5,D3,L1,V0,M1} { skol1( skol2 ) = c( skol2 ) }.
% 6.74/7.11 parent0[1]: (20450) {G1,W7,D3,L2,V0,M2} { skol1( skol2 ) = c( skol2 ), !
% 6.74/7.11 test( skol2 ) }.
% 6.74/7.11 parent1[0]: (25) {G0,W2,D2,L1,V0,M1} I { test( skol2 ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11 substitution1:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 eqswap: (20452) {G1,W5,D3,L1,V0,M1} { c( skol2 ) = skol1( skol2 ) }.
% 6.74/7.11 parent0[0]: (20451) {G1,W5,D3,L1,V0,M1} { skol1( skol2 ) = c( skol2 ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 subsumption: (2187) {G7,W5,D3,L1,V0,M1} R(2183,22);r(25) { c( skol2 ) ==>
% 6.74/7.11 skol1( skol2 ) }.
% 6.74/7.11 parent0: (20452) {G1,W5,D3,L1,V0,M1} { c( skol2 ) = skol1( skol2 ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11 permutation0:
% 6.74/7.11 0 ==> 0
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 eqswap: (20453) {G3,W6,D4,L1,V0,M1} { one ==> addition( skol3, skol1(
% 6.74/7.11 skol3 ) ) }.
% 6.74/7.11 parent0[0]: (259) {G3,W6,D4,L1,V0,M1} R(19,183) { addition( skol3, skol1(
% 6.74/7.11 skol3 ) ) ==> one }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 paramod: (20454) {G1,W6,D4,L1,V0,M1} { one ==> addition( skol1( skol3 ),
% 6.74/7.11 skol3 ) }.
% 6.74/7.11 parent0[0]: (0) {G0,W7,D3,L1,V2,M1} I { addition( X, Y ) = addition( Y, X )
% 6.74/7.11 }.
% 6.74/7.11 parent1[0; 2]: (20453) {G3,W6,D4,L1,V0,M1} { one ==> addition( skol3,
% 6.74/7.11 skol1( skol3 ) ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 X := skol3
% 6.74/7.11 Y := skol1( skol3 )
% 6.74/7.11 end
% 6.74/7.11 substitution1:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 eqswap: (20457) {G1,W6,D4,L1,V0,M1} { addition( skol1( skol3 ), skol3 )
% 6.74/7.11 ==> one }.
% 6.74/7.11 parent0[0]: (20454) {G1,W6,D4,L1,V0,M1} { one ==> addition( skol1( skol3 )
% 6.74/7.11 , skol3 ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 subsumption: (2445) {G4,W6,D4,L1,V0,M1} P(259,0) { addition( skol1( skol3 )
% 6.74/7.11 , skol3 ) ==> one }.
% 6.74/7.11 parent0: (20457) {G1,W6,D4,L1,V0,M1} { addition( skol1( skol3 ), skol3 )
% 6.74/7.11 ==> one }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11 permutation0:
% 6.74/7.11 0 ==> 0
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 eqswap: (20458) {G4,W6,D4,L1,V0,M1} { one ==> addition( skol1( skol3 ),
% 6.74/7.11 skol3 ) }.
% 6.74/7.11 parent0[0]: (2445) {G4,W6,D4,L1,V0,M1} P(259,0) { addition( skol1( skol3 )
% 6.74/7.11 , skol3 ) ==> one }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 eqswap: (20460) {G0,W13,D3,L3,V2,M3} { ! one ==> addition( X, Y ), !
% 6.74/7.11 multiplication( Y, X ) ==> zero, alpha1( X, Y ) }.
% 6.74/7.11 parent0[1]: (20) {G0,W13,D3,L3,V2,M3} I { ! multiplication( Y, X ) ==> zero
% 6.74/7.11 , ! addition( X, Y ) ==> one, alpha1( X, Y ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 X := X
% 6.74/7.11 Y := Y
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 eqswap: (20461) {G0,W13,D3,L3,V2,M3} { ! zero ==> multiplication( X, Y ),
% 6.74/7.11 ! one ==> addition( Y, X ), alpha1( Y, X ) }.
% 6.74/7.11 parent0[1]: (20460) {G0,W13,D3,L3,V2,M3} { ! one ==> addition( X, Y ), !
% 6.74/7.11 multiplication( Y, X ) ==> zero, alpha1( X, Y ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 X := Y
% 6.74/7.11 Y := X
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 resolution: (20463) {G1,W10,D4,L2,V0,M2} { ! zero ==> multiplication(
% 6.74/7.11 skol3, skol1( skol3 ) ), alpha1( skol1( skol3 ), skol3 ) }.
% 6.74/7.11 parent0[1]: (20461) {G0,W13,D3,L3,V2,M3} { ! zero ==> multiplication( X, Y
% 6.74/7.11 ), ! one ==> addition( Y, X ), alpha1( Y, X ) }.
% 6.74/7.11 parent1[0]: (20458) {G4,W6,D4,L1,V0,M1} { one ==> addition( skol1( skol3 )
% 6.74/7.11 , skol3 ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 X := skol3
% 6.74/7.11 Y := skol1( skol3 )
% 6.74/7.11 end
% 6.74/7.11 substitution1:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 paramod: (20464) {G2,W7,D3,L2,V0,M2} { ! zero ==> zero, alpha1( skol1(
% 6.74/7.11 skol3 ), skol3 ) }.
% 6.74/7.11 parent0[0]: (191) {G2,W6,D4,L1,V0,M1} R(15,179) { multiplication( skol3,
% 6.74/7.11 skol1( skol3 ) ) ==> zero }.
% 6.74/7.11 parent1[0; 3]: (20463) {G1,W10,D4,L2,V0,M2} { ! zero ==> multiplication(
% 6.74/7.11 skol3, skol1( skol3 ) ), alpha1( skol1( skol3 ), skol3 ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11 substitution1:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 eqrefl: (20465) {G0,W4,D3,L1,V0,M1} { alpha1( skol1( skol3 ), skol3 ) }.
% 6.74/7.11 parent0[0]: (20464) {G2,W7,D3,L2,V0,M2} { ! zero ==> zero, alpha1( skol1(
% 6.74/7.11 skol3 ), skol3 ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 subsumption: (2482) {G5,W4,D3,L1,V0,M1} R(2445,20);d(191);q { alpha1( skol1
% 6.74/7.11 ( skol3 ), skol3 ) }.
% 6.74/7.11 parent0: (20465) {G0,W4,D3,L1,V0,M1} { alpha1( skol1( skol3 ), skol3 ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11 permutation0:
% 6.74/7.11 0 ==> 0
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 eqswap: (20466) {G0,W11,D3,L3,V2,M3} { ! zero ==> multiplication( X, Y ),
% 6.74/7.11 ! alpha1( X, Y ), complement( Y, X ) }.
% 6.74/7.11 parent0[0]: (17) {G0,W11,D3,L3,V2,M3} I { ! multiplication( X, Y ) ==> zero
% 6.74/7.11 , ! alpha1( X, Y ), complement( Y, X ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 X := X
% 6.74/7.11 Y := Y
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 resolution: (20468) {G1,W10,D4,L2,V0,M2} { ! zero ==> multiplication(
% 6.74/7.11 skol1( skol3 ), skol3 ), complement( skol3, skol1( skol3 ) ) }.
% 6.74/7.11 parent0[1]: (20466) {G0,W11,D3,L3,V2,M3} { ! zero ==> multiplication( X, Y
% 6.74/7.11 ), ! alpha1( X, Y ), complement( Y, X ) }.
% 6.74/7.11 parent1[0]: (2482) {G5,W4,D3,L1,V0,M1} R(2445,20);d(191);q { alpha1( skol1
% 6.74/7.11 ( skol3 ), skol3 ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 X := skol1( skol3 )
% 6.74/7.11 Y := skol3
% 6.74/7.11 end
% 6.74/7.11 substitution1:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 paramod: (20469) {G2,W7,D3,L2,V0,M2} { ! zero ==> zero, complement( skol3
% 6.74/7.11 , skol1( skol3 ) ) }.
% 6.74/7.11 parent0[0]: (233) {G3,W6,D4,L1,V0,M1} R(18,183) { multiplication( skol1(
% 6.74/7.11 skol3 ), skol3 ) ==> zero }.
% 6.74/7.11 parent1[0; 3]: (20468) {G1,W10,D4,L2,V0,M2} { ! zero ==> multiplication(
% 6.74/7.11 skol1( skol3 ), skol3 ), complement( skol3, skol1( skol3 ) ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11 substitution1:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 eqrefl: (20470) {G0,W4,D3,L1,V0,M1} { complement( skol3, skol1( skol3 ) )
% 6.74/7.11 }.
% 6.74/7.11 parent0[0]: (20469) {G2,W7,D3,L2,V0,M2} { ! zero ==> zero, complement(
% 6.74/7.11 skol3, skol1( skol3 ) ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 subsumption: (2498) {G6,W4,D3,L1,V0,M1} R(2482,17);d(233);q { complement(
% 6.74/7.11 skol3, skol1( skol3 ) ) }.
% 6.74/7.11 parent0: (20470) {G0,W4,D3,L1,V0,M1} { complement( skol3, skol1( skol3 ) )
% 6.74/7.11 }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11 permutation0:
% 6.74/7.11 0 ==> 0
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 eqswap: (20471) {G0,W9,D3,L3,V2,M3} { Y = c( X ), ! test( X ), !
% 6.74/7.11 complement( X, Y ) }.
% 6.74/7.11 parent0[2]: (22) {G0,W9,D3,L3,V2,M3} I { ! test( X ), ! complement( X, Y )
% 6.74/7.11 , c( X ) = Y }.
% 6.74/7.11 substitution0:
% 6.74/7.11 X := X
% 6.74/7.11 Y := Y
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 resolution: (20472) {G1,W7,D3,L2,V0,M2} { skol1( skol3 ) = c( skol3 ), !
% 6.74/7.11 test( skol3 ) }.
% 6.74/7.11 parent0[2]: (20471) {G0,W9,D3,L3,V2,M3} { Y = c( X ), ! test( X ), !
% 6.74/7.11 complement( X, Y ) }.
% 6.74/7.11 parent1[0]: (2498) {G6,W4,D3,L1,V0,M1} R(2482,17);d(233);q { complement(
% 6.74/7.11 skol3, skol1( skol3 ) ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 X := skol3
% 6.74/7.11 Y := skol1( skol3 )
% 6.74/7.11 end
% 6.74/7.11 substitution1:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 resolution: (20473) {G1,W5,D3,L1,V0,M1} { skol1( skol3 ) = c( skol3 ) }.
% 6.74/7.11 parent0[1]: (20472) {G1,W7,D3,L2,V0,M2} { skol1( skol3 ) = c( skol3 ), !
% 6.74/7.11 test( skol3 ) }.
% 6.74/7.11 parent1[0]: (24) {G0,W2,D2,L1,V0,M1} I { test( skol3 ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11 substitution1:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 eqswap: (20474) {G1,W5,D3,L1,V0,M1} { c( skol3 ) = skol1( skol3 ) }.
% 6.74/7.11 parent0[0]: (20473) {G1,W5,D3,L1,V0,M1} { skol1( skol3 ) = c( skol3 ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 subsumption: (2502) {G7,W5,D3,L1,V0,M1} R(2498,22);r(24) { c( skol3 ) ==>
% 6.74/7.11 skol1( skol3 ) }.
% 6.74/7.11 parent0: (20474) {G1,W5,D3,L1,V0,M1} { c( skol3 ) = skol1( skol3 ) }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11 permutation0:
% 6.74/7.11 0 ==> 0
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 paramod: (20481) {G3,W11,D5,L1,V0,M1} { ! multiplication( addition( skol2
% 6.74/7.11 , skol1( skol2 ) ), addition( skol3, c( skol3 ) ) ) ==> one }.
% 6.74/7.11 parent0[0]: (2187) {G7,W5,D3,L1,V0,M1} R(2183,22);r(25) { c( skol2 ) ==>
% 6.74/7.11 skol1( skol2 ) }.
% 6.74/7.11 parent1[0; 5]: (432) {G2,W11,D5,L1,V0,M1} S(26);d(46);d(8) { !
% 6.74/7.11 multiplication( addition( skol2, c( skol2 ) ), addition( skol3, c( skol3
% 6.74/7.11 ) ) ) ==> one }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11 substitution1:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 paramod: (20482) {G4,W8,D5,L1,V0,M1} { ! multiplication( one, addition(
% 6.74/7.11 skol3, c( skol3 ) ) ) ==> one }.
% 6.74/7.11 parent0[0]: (258) {G3,W6,D4,L1,V0,M1} R(19,187) { addition( skol2, skol1(
% 6.74/7.11 skol2 ) ) ==> one }.
% 6.74/7.11 parent1[0; 3]: (20481) {G3,W11,D5,L1,V0,M1} { ! multiplication( addition(
% 6.74/7.11 skol2, skol1( skol2 ) ), addition( skol3, c( skol3 ) ) ) ==> one }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11 substitution1:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 paramod: (20483) {G1,W6,D4,L1,V0,M1} { ! addition( skol3, c( skol3 ) ) ==>
% 6.74/7.11 one }.
% 6.74/7.11 parent0[0]: (6) {G0,W5,D3,L1,V1,M1} I { multiplication( one, X ) ==> X }.
% 6.74/7.11 parent1[0; 2]: (20482) {G4,W8,D5,L1,V0,M1} { ! multiplication( one,
% 6.74/7.11 addition( skol3, c( skol3 ) ) ) ==> one }.
% 6.74/7.11 substitution0:
% 6.74/7.11 X := addition( skol3, c( skol3 ) )
% 6.74/7.11 end
% 6.74/7.11 substitution1:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 paramod: (20484) {G2,W6,D4,L1,V0,M1} { ! addition( skol3, skol1( skol3 ) )
% 6.74/7.11 ==> one }.
% 6.74/7.11 parent0[0]: (2502) {G7,W5,D3,L1,V0,M1} R(2498,22);r(24) { c( skol3 ) ==>
% 6.74/7.11 skol1( skol3 ) }.
% 6.74/7.11 parent1[0; 4]: (20483) {G1,W6,D4,L1,V0,M1} { ! addition( skol3, c( skol3 )
% 6.74/7.11 ) ==> one }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11 substitution1:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 paramod: (20485) {G3,W3,D2,L1,V0,M1} { ! one ==> one }.
% 6.74/7.11 parent0[0]: (259) {G3,W6,D4,L1,V0,M1} R(19,183) { addition( skol3, skol1(
% 6.74/7.11 skol3 ) ) ==> one }.
% 6.74/7.11 parent1[0; 2]: (20484) {G2,W6,D4,L1,V0,M1} { ! addition( skol3, skol1(
% 6.74/7.11 skol3 ) ) ==> one }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11 substitution1:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 eqrefl: (20486) {G0,W0,D0,L0,V0,M0} { }.
% 6.74/7.11 parent0[0]: (20485) {G3,W3,D2,L1,V0,M1} { ! one ==> one }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 subsumption: (20123) {G8,W0,D0,L0,V0,M0} S(432);d(2187);d(258);d(6);d(2502)
% 6.74/7.11 ;d(259);q { }.
% 6.74/7.11 parent0: (20486) {G0,W0,D0,L0,V0,M0} { }.
% 6.74/7.11 substitution0:
% 6.74/7.11 end
% 6.74/7.11 permutation0:
% 6.74/7.11 end
% 6.74/7.11
% 6.74/7.11 Proof check complete!
% 6.74/7.11
% 6.74/7.11 Memory use:
% 6.74/7.11
% 6.74/7.11 space for terms: 249501
% 6.74/7.11 space for clauses: 913558
% 6.74/7.11
% 6.74/7.11
% 6.74/7.11 clauses generated: 179801
% 6.74/7.11 clauses kept: 20124
% 6.74/7.11 clauses selected: 918
% 6.74/7.11 clauses deleted: 6179
% 6.74/7.11 clauses inuse deleted: 225
% 6.74/7.11
% 6.74/7.11 subsentry: 950076
% 6.74/7.11 literals s-matched: 659876
% 6.74/7.11 literals matched: 624837
% 6.74/7.11 full subsumption: 158763
% 6.74/7.11
% 6.74/7.11 checksum: -545373421
% 6.74/7.11
% 6.74/7.11
% 6.74/7.11 Bliksem ended
%------------------------------------------------------------------------------