%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : GRP711+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n005.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 : Sat Jul 16 07:39:12 EDT 2022
% Result : Theorem 36.15s 36.59s
% Output : Refutation 36.15s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : GRP711+1 : TPTP v8.1.0. Released v4.0.0.
% 0.13/0.14 % Command : bliksem %s
% 0.13/0.35 % Computer : n005.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % DateTime : Mon Jun 13 09:13:54 EDT 2022
% 0.13/0.35 % CPUTime :
% 36.15/36.59 *** allocated 10000 integers for termspace/termends
% 36.15/36.59 *** allocated 10000 integers for clauses
% 36.15/36.59 *** allocated 10000 integers for justifications
% 36.15/36.59 Bliksem 1.12
% 36.15/36.59
% 36.15/36.59
% 36.15/36.59 Automatic Strategy Selection
% 36.15/36.59
% 36.15/36.59
% 36.15/36.59 Clauses:
% 36.15/36.59
% 36.15/36.59 { mult( X, unit ) = X }.
% 36.15/36.59 { mult( unit, X ) = X }.
% 36.15/36.59 { mult( Z, mult( Y, mult( Y, X ) ) ) = mult( mult( mult( Z, Y ), Y ), X ) }
% 36.15/36.59 .
% 36.15/36.59 { mult( X, i( X ) ) = unit }.
% 36.15/36.59 { mult( i( X ), X ) = unit }.
% 36.15/36.59 { alpha1( skol1, skol2, skol3 ), mult( skol2, skol1 ) = mult( skol3, skol1
% 36.15/36.59 ) }.
% 36.15/36.59 { alpha1( skol1, skol2, skol3 ), ! skol2 = skol3 }.
% 36.15/36.59 { ! alpha1( X, Y, Z ), mult( X, Y ) = mult( X, Z ) }.
% 36.15/36.59 { ! alpha1( X, Y, Z ), ! Y = Z }.
% 36.15/36.59 { ! mult( X, Y ) = mult( X, Z ), Y = Z, alpha1( X, Y, Z ) }.
% 36.15/36.59
% 36.15/36.59 percentage equality = 0.687500, percentage horn = 0.800000
% 36.15/36.59 This is a problem with some equality
% 36.15/36.59
% 36.15/36.59
% 36.15/36.59
% 36.15/36.59 Options Used:
% 36.15/36.59
% 36.15/36.59 useres = 1
% 36.15/36.59 useparamod = 1
% 36.15/36.59 useeqrefl = 1
% 36.15/36.59 useeqfact = 1
% 36.15/36.59 usefactor = 1
% 36.15/36.59 usesimpsplitting = 0
% 36.15/36.59 usesimpdemod = 5
% 36.15/36.59 usesimpres = 3
% 36.15/36.59
% 36.15/36.59 resimpinuse = 1000
% 36.15/36.59 resimpclauses = 20000
% 36.15/36.59 substype = eqrewr
% 36.15/36.59 backwardsubs = 1
% 36.15/36.59 selectoldest = 5
% 36.15/36.59
% 36.15/36.59 litorderings [0] = split
% 36.15/36.59 litorderings [1] = extend the termordering, first sorting on arguments
% 36.15/36.59
% 36.15/36.59 termordering = kbo
% 36.15/36.59
% 36.15/36.59 litapriori = 0
% 36.15/36.59 termapriori = 1
% 36.15/36.59 litaposteriori = 0
% 36.15/36.59 termaposteriori = 0
% 36.15/36.59 demodaposteriori = 0
% 36.15/36.59 ordereqreflfact = 0
% 36.15/36.59
% 36.15/36.59 litselect = negord
% 36.15/36.59
% 36.15/36.59 maxweight = 15
% 36.15/36.59 maxdepth = 30000
% 36.15/36.59 maxlength = 115
% 36.15/36.59 maxnrvars = 195
% 36.15/36.59 excuselevel = 1
% 36.15/36.59 increasemaxweight = 1
% 36.15/36.59
% 36.15/36.59 maxselected = 10000000
% 36.15/36.59 maxnrclauses = 10000000
% 36.15/36.59
% 36.15/36.59 showgenerated = 0
% 36.15/36.59 showkept = 0
% 36.15/36.59 showselected = 0
% 36.15/36.59 showdeleted = 0
% 36.15/36.59 showresimp = 1
% 36.15/36.59 showstatus = 2000
% 36.15/36.59
% 36.15/36.59 prologoutput = 0
% 36.15/36.59 nrgoals = 5000000
% 36.15/36.59 totalproof = 1
% 36.15/36.59
% 36.15/36.59 Symbols occurring in the translation:
% 36.15/36.59
% 36.15/36.59 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 36.15/36.59 . [1, 2] (w:1, o:22, a:1, s:1, b:0),
% 36.15/36.59 ! [4, 1] (w:0, o:16, a:1, s:1, b:0),
% 36.15/36.59 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 36.15/36.59 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 36.15/36.59 unit [36, 0] (w:1, o:7, a:1, s:1, b:0),
% 36.15/36.59 mult [37, 2] (w:1, o:46, a:1, s:1, b:0),
% 36.15/36.59 i [40, 1] (w:1, o:21, a:1, s:1, b:0),
% 36.15/36.59 alpha1 [44, 3] (w:1, o:47, a:1, s:1, b:1),
% 36.15/36.59 skol1 [45, 0] (w:1, o:13, a:1, s:1, b:1),
% 36.15/36.59 skol2 [46, 0] (w:1, o:14, a:1, s:1, b:1),
% 36.15/36.59 skol3 [47, 0] (w:1, o:15, a:1, s:1, b:1).
% 36.15/36.59
% 36.15/36.59
% 36.15/36.59 Starting Search:
% 36.15/36.59
% 36.15/36.59 *** allocated 15000 integers for clauses
% 36.15/36.59 *** allocated 22500 integers for clauses
% 36.15/36.59 *** allocated 33750 integers for clauses
% 36.15/36.59 *** allocated 50625 integers for clauses
% 36.15/36.59 *** allocated 15000 integers for termspace/termends
% 36.15/36.59 *** allocated 75937 integers for clauses
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59 *** allocated 22500 integers for termspace/termends
% 36.15/36.59 *** allocated 113905 integers for clauses
% 36.15/36.59 *** allocated 33750 integers for termspace/termends
% 36.15/36.59
% 36.15/36.59 Intermediate Status:
% 36.15/36.59 Generated: 17264
% 36.15/36.59 Kept: 2043
% 36.15/36.59 Inuse: 193
% 36.15/36.59 Deleted: 31
% 36.15/36.59 Deletedinuse: 9
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59 *** allocated 50625 integers for termspace/termends
% 36.15/36.59 *** allocated 170857 integers for clauses
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59 *** allocated 75937 integers for termspace/termends
% 36.15/36.59 *** allocated 256285 integers for clauses
% 36.15/36.59
% 36.15/36.59 Intermediate Status:
% 36.15/36.59 Generated: 60830
% 36.15/36.59 Kept: 4070
% 36.15/36.59 Inuse: 349
% 36.15/36.59 Deleted: 96
% 36.15/36.59 Deletedinuse: 68
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59 *** allocated 113905 integers for termspace/termends
% 36.15/36.59 *** allocated 384427 integers for clauses
% 36.15/36.59
% 36.15/36.59 Intermediate Status:
% 36.15/36.59 Generated: 80537
% 36.15/36.59 Kept: 6112
% 36.15/36.59 Inuse: 433
% 36.15/36.59 Deleted: 119
% 36.15/36.59 Deletedinuse: 89
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59 *** allocated 170857 integers for termspace/termends
% 36.15/36.59
% 36.15/36.59 Intermediate Status:
% 36.15/36.59 Generated: 92061
% 36.15/36.59 Kept: 8128
% 36.15/36.59 Inuse: 551
% 36.15/36.59 Deleted: 439
% 36.15/36.59 Deletedinuse: 322
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59 *** allocated 576640 integers for clauses
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59
% 36.15/36.59 Intermediate Status:
% 36.15/36.59 Generated: 104485
% 36.15/36.59 Kept: 10132
% 36.15/36.59 Inuse: 619
% 36.15/36.59 Deleted: 599
% 36.15/36.59 Deletedinuse: 358
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59 *** allocated 256285 integers for termspace/termends
% 36.15/36.59
% 36.15/36.59 Intermediate Status:
% 36.15/36.59 Generated: 118094
% 36.15/36.59 Kept: 12698
% 36.15/36.59 Inuse: 693
% 36.15/36.59 Deleted: 1368
% 36.15/36.59 Deletedinuse: 496
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59 *** allocated 864960 integers for clauses
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59
% 36.15/36.59 Intermediate Status:
% 36.15/36.59 Generated: 129336
% 36.15/36.59 Kept: 14707
% 36.15/36.59 Inuse: 765
% 36.15/36.59 Deleted: 1660
% 36.15/36.59 Deletedinuse: 496
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59
% 36.15/36.59 Intermediate Status:
% 36.15/36.59 Generated: 144284
% 36.15/36.59 Kept: 16716
% 36.15/36.59 Inuse: 830
% 36.15/36.59 Deleted: 2055
% 36.15/36.59 Deletedinuse: 496
% 36.15/36.59
% 36.15/36.59 *** allocated 384427 integers for termspace/termends
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59
% 36.15/36.59 Intermediate Status:
% 36.15/36.59 Generated: 163539
% 36.15/36.59 Kept: 18725
% 36.15/36.59 Inuse: 900
% 36.15/36.59 Deleted: 2267
% 36.15/36.59 Deletedinuse: 496
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59 *** allocated 1297440 integers for clauses
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59 Resimplifying clauses:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59
% 36.15/36.59 Intermediate Status:
% 36.15/36.59 Generated: 196717
% 36.15/36.59 Kept: 21075
% 36.15/36.59 Inuse: 973
% 36.15/36.59 Deleted: 9186
% 36.15/36.59 Deletedinuse: 496
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59
% 36.15/36.59 Intermediate Status:
% 36.15/36.59 Generated: 257937
% 36.15/36.59 Kept: 23075
% 36.15/36.59 Inuse: 1091
% 36.15/36.59 Deleted: 9186
% 36.15/36.59 Deletedinuse: 496
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59 *** allocated 576640 integers for termspace/termends
% 36.15/36.59
% 36.15/36.59 Intermediate Status:
% 36.15/36.59 Generated: 323384
% 36.15/36.59 Kept: 25188
% 36.15/36.59 Inuse: 1165
% 36.15/36.59 Deleted: 9187
% 36.15/36.59 Deletedinuse: 497
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59
% 36.15/36.59 Intermediate Status:
% 36.15/36.59 Generated: 355723
% 36.15/36.59 Kept: 27352
% 36.15/36.59 Inuse: 1260
% 36.15/36.59 Deleted: 9199
% 36.15/36.59 Deletedinuse: 509
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59
% 36.15/36.59 Intermediate Status:
% 36.15/36.59 Generated: 388787
% 36.15/36.59 Kept: 29368
% 36.15/36.59 Inuse: 1331
% 36.15/36.59 Deleted: 9209
% 36.15/36.59 Deletedinuse: 515
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59 *** allocated 1946160 integers for clauses
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59
% 36.15/36.59 Intermediate Status:
% 36.15/36.59 Generated: 426337
% 36.15/36.59 Kept: 31588
% 36.15/36.59 Inuse: 1382
% 36.15/36.59 Deleted: 9210
% 36.15/36.59 Deletedinuse: 515
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59
% 36.15/36.59 Intermediate Status:
% 36.15/36.59 Generated: 471471
% 36.15/36.59 Kept: 33610
% 36.15/36.59 Inuse: 1439
% 36.15/36.59 Deleted: 9211
% 36.15/36.59 Deletedinuse: 515
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59
% 36.15/36.59 Intermediate Status:
% 36.15/36.59 Generated: 527780
% 36.15/36.59 Kept: 35683
% 36.15/36.59 Inuse: 1496
% 36.15/36.59 Deleted: 9211
% 36.15/36.59 Deletedinuse: 515
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59 *** allocated 864960 integers for termspace/termends
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59
% 36.15/36.59 Intermediate Status:
% 36.15/36.59 Generated: 575625
% 36.15/36.59 Kept: 37692
% 36.15/36.59 Inuse: 1594
% 36.15/36.59 Deleted: 9214
% 36.15/36.59 Deletedinuse: 515
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59
% 36.15/36.59 Intermediate Status:
% 36.15/36.59 Generated: 636025
% 36.15/36.59 Kept: 40195
% 36.15/36.59 Inuse: 1681
% 36.15/36.59 Deleted: 9220
% 36.15/36.59 Deletedinuse: 518
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59 Resimplifying clauses:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59
% 36.15/36.59 Intermediate Status:
% 36.15/36.59 Generated: 686593
% 36.15/36.59 Kept: 42251
% 36.15/36.59 Inuse: 1769
% 36.15/36.59 Deleted: 10482
% 36.15/36.59 Deletedinuse: 527
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59
% 36.15/36.59 Intermediate Status:
% 36.15/36.59 Generated: 764996
% 36.15/36.59 Kept: 44257
% 36.15/36.59 Inuse: 1963
% 36.15/36.59 Deleted: 10488
% 36.15/36.59 Deletedinuse: 527
% 36.15/36.59
% 36.15/36.59 Resimplifying inuse:
% 36.15/36.59 Done
% 36.15/36.59
% 36.15/36.59
% 36.15/36.59 Bliksems!, er is een bewijs:
% 36.15/36.59 % SZS status Theorem
% 36.15/36.59 % SZS output start Refutation
% 36.15/36.59
% 36.15/36.59 (0) {G0,W5,D3,L1,V1,M1} I { mult( X, unit ) ==> X }.
% 36.15/36.59 (1) {G0,W5,D3,L1,V1,M1} I { mult( unit, X ) ==> X }.
% 36.15/36.59 (2) {G0,W15,D5,L1,V3,M1} I { mult( Z, mult( Y, mult( Y, X ) ) ) ==> mult(
% 36.15/36.59 mult( mult( Z, Y ), Y ), X ) }.
% 36.15/36.59 (3) {G0,W6,D4,L1,V1,M1} I { mult( X, i( X ) ) ==> unit }.
% 36.15/36.59 (5) {G0,W11,D3,L2,V0,M2} I { alpha1( skol1, skol2, skol3 ), mult( skol3,
% 36.15/36.59 skol1 ) ==> mult( skol2, skol1 ) }.
% 36.15/36.59 (6) {G0,W7,D2,L2,V0,M2} I { alpha1( skol1, skol2, skol3 ), ! skol3 ==>
% 36.15/36.59 skol2 }.
% 36.15/36.59 (7) {G0,W11,D3,L2,V3,M2} I { ! alpha1( X, Y, Z ), mult( X, Y ) = mult( X, Z
% 36.15/36.59 ) }.
% 36.15/36.59 (8) {G0,W7,D2,L2,V3,M2} I { ! alpha1( X, Y, Z ), ! Y = Z }.
% 36.15/36.59 (9) {G0,W14,D3,L3,V3,M3} I { ! mult( X, Y ) = mult( X, Z ), Y = Z, alpha1(
% 36.15/36.59 X, Y, Z ) }.
% 36.15/36.59 (13) {G1,W23,D7,L1,V4,M1} P(2,2);d(2) { mult( T, mult( X, mult( mult( mult
% 36.15/36.59 ( X, Y ), Y ), Z ) ) ) ==> mult( mult( mult( mult( mult( T, X ), X ), Y )
% 36.15/36.59 , Y ), Z ) }.
% 36.15/36.59 (17) {G1,W11,D4,L1,V2,M1} P(2,1);d(1) { mult( X, mult( X, Y ) ) ==> mult(
% 36.15/36.59 mult( X, X ), Y ) }.
% 36.15/36.59 (18) {G1,W12,D5,L1,V2,M1} P(3,2);d(0) { mult( mult( mult( Y, X ), X ), i( X
% 36.15/36.59 ) ) ==> mult( Y, X ) }.
% 36.15/36.59 (19) {G1,W3,D2,L1,V0,M1} S(6);r(8) { ! skol3 ==> skol2 }.
% 36.15/36.59 (21) {G1,W14,D3,L2,V0,M2} R(7,5) { mult( skol1, skol3 ) ==> mult( skol1,
% 36.15/36.59 skol2 ), mult( skol3, skol1 ) ==> mult( skol2, skol1 ) }.
% 36.15/36.59 (32) {G1,W19,D5,L2,V4,M2} P(7,2);d(2) { ! alpha1( X, Y, Z ), mult( mult(
% 36.15/36.59 mult( T, X ), X ), Z ) = mult( mult( mult( T, X ), X ), Y ) }.
% 36.15/36.59 (37) {G1,W7,D2,L2,V2,M2} P(7,1);d(1) { ! alpha1( unit, X, Y ), Y = X }.
% 36.15/36.59 (50) {G2,W10,D3,L2,V2,M2} P(37,3) { mult( X, Y ) ==> unit, ! alpha1( unit,
% 36.15/36.59 i( X ), Y ) }.
% 36.15/36.59 (82) {G2,W14,D3,L3,V2,M3} P(9,19) { ! X = skol2, ! mult( Y, skol3 ) = mult
% 36.15/36.59 ( Y, X ), alpha1( Y, skol3, X ) }.
% 36.15/36.59 (85) {G1,W14,D3,L3,V2,M3} P(3,9) { ! mult( X, Y ) ==> unit, Y = i( X ),
% 36.15/36.59 alpha1( X, Y, i( X ) ) }.
% 36.15/36.59 (88) {G1,W18,D4,L3,V3,M3} P(9,3) { mult( X, Y ) ==> unit, ! mult( Z, i( X )
% 36.15/36.59 ) = mult( Z, Y ), alpha1( Z, i( X ), Y ) }.
% 36.15/36.59 (117) {G2,W15,D5,L1,V3,M1} P(1,13);d(1);d(0);d(0) { mult( Z, mult( mult( X
% 36.15/36.59 , X ), Y ) ) ==> mult( mult( mult( Z, X ), X ), Y ) }.
% 36.15/36.59 (198) {G2,W8,D4,L1,V1,M1} P(3,17);d(0) { mult( mult( X, X ), i( X ) ) ==> X
% 36.15/36.59 }.
% 36.15/36.59 (216) {G3,W5,D4,L1,V1,M1} P(198,18);d(3);d(1) { i( i( X ) ) ==> X }.
% 36.15/36.59 (838) {G3,W8,D3,L2,V3,M2} P(198,32);d(3);d(1);d(1) { ! alpha1( i( X ), Y, Z
% 36.15/36.59 ), Z = Y }.
% 36.15/36.59 (927) {G4,W8,D3,L2,V2,M2} P(838,19) { ! X = skol2, ! alpha1( i( Y ), skol3
% 36.15/36.59 , X ) }.
% 36.15/36.59 (938) {G5,W5,D3,L1,V1,M1} Q(927) { ! alpha1( i( X ), skol3, skol2 ) }.
% 36.15/36.59 (2821) {G6,W9,D4,L1,V1,M1} R(82,938);q { ! mult( i( X ), skol3 ) ==> mult(
% 36.15/36.59 i( X ), skol2 ) }.
% 36.15/36.59 (3358) {G3,W9,D3,L2,V2,M2} R(88,50);f;d(1);d(1) { mult( X, Y ) ==> unit, !
% 36.15/36.59 i( X ) = Y }.
% 36.15/36.59 (3582) {G4,W8,D3,L2,V2,M2} R(3358,85);r(8) { ! i( X ) = Y, Y = i( X ) }.
% 36.15/36.59 (3713) {G5,W8,D3,L2,V2,M2} P(3582,216) { i( Y ) = X, ! i( X ) = Y }.
% 36.15/36.59 (4146) {G7,W13,D4,L2,V1,M2} P(3713,21);r(2821) { mult( skol3, i( X ) ) ==>
% 36.15/36.59 mult( skol2, i( X ) ), ! i( skol1 ) = X }.
% 36.15/36.59 (4164) {G8,W7,D3,L1,V0,M1} Q(4146);d(216) { mult( skol3, skol1 ) ==> mult(
% 36.15/36.59 skol2, skol1 ) }.
% 36.15/36.59 (5941) {G4,W15,D5,L2,V3,M2} P(3358,117);d(0) { ! i( mult( X, X ) ) = Y,
% 36.15/36.59 mult( mult( mult( Z, X ), X ), Y ) ==> Z }.
% 36.15/36.59 (44390) {G9,W9,D4,L2,V1,M2} P(4164,5941);d(5941) { ! i( mult( skol1, skol1
% 36.15/36.59 ) ) = X, skol3 ==> skol2 }.
% 36.15/36.59 (44404) {G10,W0,D0,L0,V0,M0} Q(44390);r(19) { }.
% 36.15/36.59
% 36.15/36.59
% 36.15/36.59 % SZS output end Refutation
% 36.15/36.59 found a proof!
% 36.15/36.59
% 36.15/36.59
% 36.15/36.59 Unprocessed initial clauses:
% 36.15/36.59
% 36.15/36.59 (44406) {G0,W5,D3,L1,V1,M1} { mult( X, unit ) = X }.
% 36.15/36.59 (44407) {G0,W5,D3,L1,V1,M1} { mult( unit, X ) = X }.
% 36.15/36.59 (44408) {G0,W15,D5,L1,V3,M1} { mult( Z, mult( Y, mult( Y, X ) ) ) = mult(
% 36.15/36.59 mult( mult( Z, Y ), Y ), X ) }.
% 36.15/36.59 (44409) {G0,W6,D4,L1,V1,M1} { mult( X, i( X ) ) = unit }.
% 36.15/36.59 (44410) {G0,W6,D4,L1,V1,M1} { mult( i( X ), X ) = unit }.
% 36.15/36.59 (44411) {G0,W11,D3,L2,V0,M2} { alpha1( skol1, skol2, skol3 ), mult( skol2
% 36.15/36.59 , skol1 ) = mult( skol3, skol1 ) }.
% 36.15/36.59 (44412) {G0,W7,D2,L2,V0,M2} { alpha1( skol1, skol2, skol3 ), ! skol2 =
% 36.15/36.59 skol3 }.
% 36.15/36.59 (44413) {G0,W11,D3,L2,V3,M2} { ! alpha1( X, Y, Z ), mult( X, Y ) = mult( X
% 36.15/36.59 , Z ) }.
% 36.15/36.59 (44414) {G0,W7,D2,L2,V3,M2} { ! alpha1( X, Y, Z ), ! Y = Z }.
% 36.15/36.59 (44415) {G0,W14,D3,L3,V3,M3} { ! mult( X, Y ) = mult( X, Z ), Y = Z,
% 36.15/36.59 alpha1( X, Y, Z ) }.
% 36.15/36.59
% 36.15/36.59
% 36.15/36.59 Total Proof:
% 36.15/36.59
% 36.15/36.59 subsumption: (0) {G0,W5,D3,L1,V1,M1} I { mult( X, unit ) ==> X }.
% 36.15/36.59 parent0: (44406) {G0,W5,D3,L1,V1,M1} { mult( X, unit ) = X }.
% 36.15/36.59 substitution0:
% 36.15/36.59 X := X
% 36.15/36.59 end
% 36.15/36.59 permutation0:
% 36.15/36.59 0 ==> 0
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 subsumption: (1) {G0,W5,D3,L1,V1,M1} I { mult( unit, X ) ==> X }.
% 36.15/36.59 parent0: (44407) {G0,W5,D3,L1,V1,M1} { mult( unit, X ) = X }.
% 36.15/36.59 substitution0:
% 36.15/36.59 X := X
% 36.15/36.59 end
% 36.15/36.59 permutation0:
% 36.15/36.59 0 ==> 0
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 subsumption: (2) {G0,W15,D5,L1,V3,M1} I { mult( Z, mult( Y, mult( Y, X ) )
% 36.15/36.59 ) ==> mult( mult( mult( Z, Y ), Y ), X ) }.
% 36.15/36.59 parent0: (44408) {G0,W15,D5,L1,V3,M1} { mult( Z, mult( Y, mult( Y, X ) ) )
% 36.15/36.59 = mult( mult( mult( Z, Y ), Y ), X ) }.
% 36.15/36.59 substitution0:
% 36.15/36.59 X := X
% 36.15/36.59 Y := Y
% 36.15/36.59 Z := Z
% 36.15/36.59 end
% 36.15/36.59 permutation0:
% 36.15/36.59 0 ==> 0
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 subsumption: (3) {G0,W6,D4,L1,V1,M1} I { mult( X, i( X ) ) ==> unit }.
% 36.15/36.59 parent0: (44409) {G0,W6,D4,L1,V1,M1} { mult( X, i( X ) ) = unit }.
% 36.15/36.59 substitution0:
% 36.15/36.59 X := X
% 36.15/36.59 end
% 36.15/36.59 permutation0:
% 36.15/36.59 0 ==> 0
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 eqswap: (44431) {G0,W11,D3,L2,V0,M2} { mult( skol3, skol1 ) = mult( skol2
% 36.15/36.59 , skol1 ), alpha1( skol1, skol2, skol3 ) }.
% 36.15/36.59 parent0[1]: (44411) {G0,W11,D3,L2,V0,M2} { alpha1( skol1, skol2, skol3 ),
% 36.15/36.59 mult( skol2, skol1 ) = mult( skol3, skol1 ) }.
% 36.15/36.59 substitution0:
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 subsumption: (5) {G0,W11,D3,L2,V0,M2} I { alpha1( skol1, skol2, skol3 ),
% 36.15/36.59 mult( skol3, skol1 ) ==> mult( skol2, skol1 ) }.
% 36.15/36.59 parent0: (44431) {G0,W11,D3,L2,V0,M2} { mult( skol3, skol1 ) = mult( skol2
% 36.15/36.59 , skol1 ), alpha1( skol1, skol2, skol3 ) }.
% 36.15/36.59 substitution0:
% 36.15/36.59 end
% 36.15/36.59 permutation0:
% 36.15/36.59 0 ==> 1
% 36.15/36.59 1 ==> 0
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 eqswap: (44438) {G0,W7,D2,L2,V0,M2} { ! skol3 = skol2, alpha1( skol1,
% 36.15/36.59 skol2, skol3 ) }.
% 36.15/36.59 parent0[1]: (44412) {G0,W7,D2,L2,V0,M2} { alpha1( skol1, skol2, skol3 ), !
% 36.15/36.59 skol2 = skol3 }.
% 36.15/36.59 substitution0:
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 subsumption: (6) {G0,W7,D2,L2,V0,M2} I { alpha1( skol1, skol2, skol3 ), !
% 36.15/36.59 skol3 ==> skol2 }.
% 36.15/36.59 parent0: (44438) {G0,W7,D2,L2,V0,M2} { ! skol3 = skol2, alpha1( skol1,
% 36.15/36.59 skol2, skol3 ) }.
% 36.15/36.59 substitution0:
% 36.15/36.59 end
% 36.15/36.59 permutation0:
% 36.15/36.59 0 ==> 1
% 36.15/36.59 1 ==> 0
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 subsumption: (7) {G0,W11,D3,L2,V3,M2} I { ! alpha1( X, Y, Z ), mult( X, Y )
% 36.15/36.59 = mult( X, Z ) }.
% 36.15/36.59 parent0: (44413) {G0,W11,D3,L2,V3,M2} { ! alpha1( X, Y, Z ), mult( X, Y )
% 36.15/36.59 = mult( X, Z ) }.
% 36.15/36.59 substitution0:
% 36.15/36.59 X := X
% 36.15/36.59 Y := Y
% 36.15/36.59 Z := Z
% 36.15/36.59 end
% 36.15/36.59 permutation0:
% 36.15/36.59 0 ==> 0
% 36.15/36.59 1 ==> 1
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 subsumption: (8) {G0,W7,D2,L2,V3,M2} I { ! alpha1( X, Y, Z ), ! Y = Z }.
% 36.15/36.59 parent0: (44414) {G0,W7,D2,L2,V3,M2} { ! alpha1( X, Y, Z ), ! Y = Z }.
% 36.15/36.59 substitution0:
% 36.15/36.59 X := X
% 36.15/36.59 Y := Y
% 36.15/36.59 Z := Z
% 36.15/36.59 end
% 36.15/36.59 permutation0:
% 36.15/36.59 0 ==> 0
% 36.15/36.59 1 ==> 1
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 subsumption: (9) {G0,W14,D3,L3,V3,M3} I { ! mult( X, Y ) = mult( X, Z ), Y
% 36.15/36.59 = Z, alpha1( X, Y, Z ) }.
% 36.15/36.59 parent0: (44415) {G0,W14,D3,L3,V3,M3} { ! mult( X, Y ) = mult( X, Z ), Y =
% 36.15/36.59 Z, alpha1( X, Y, Z ) }.
% 36.15/36.59 substitution0:
% 36.15/36.59 X := X
% 36.15/36.59 Y := Y
% 36.15/36.59 Z := Z
% 36.15/36.59 end
% 36.15/36.59 permutation0:
% 36.15/36.59 0 ==> 0
% 36.15/36.59 1 ==> 1
% 36.15/36.59 2 ==> 2
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 eqswap: (44468) {G0,W15,D5,L1,V3,M1} { mult( mult( mult( X, Y ), Y ), Z )
% 36.15/36.59 ==> mult( X, mult( Y, mult( Y, Z ) ) ) }.
% 36.15/36.59 parent0[0]: (2) {G0,W15,D5,L1,V3,M1} I { mult( Z, mult( Y, mult( Y, X ) ) )
% 36.15/36.59 ==> mult( mult( mult( Z, Y ), Y ), X ) }.
% 36.15/36.59 substitution0:
% 36.15/36.59 X := Z
% 36.15/36.59 Y := Y
% 36.15/36.59 Z := X
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 paramod: (44476) {G1,W23,D7,L1,V4,M1} { mult( mult( mult( X, Y ), Y ),
% 36.15/36.59 mult( Z, mult( Z, T ) ) ) ==> mult( X, mult( Y, mult( mult( mult( Y, Z )
% 36.15/36.59 , Z ), T ) ) ) }.
% 36.15/36.59 parent0[0]: (2) {G0,W15,D5,L1,V3,M1} I { mult( Z, mult( Y, mult( Y, X ) ) )
% 36.15/36.59 ==> mult( mult( mult( Z, Y ), Y ), X ) }.
% 36.15/36.59 parent1[0; 16]: (44468) {G0,W15,D5,L1,V3,M1} { mult( mult( mult( X, Y ), Y
% 36.15/36.59 ), Z ) ==> mult( X, mult( Y, mult( Y, Z ) ) ) }.
% 36.15/36.59 substitution0:
% 36.15/36.59 X := T
% 36.15/36.59 Y := Z
% 36.15/36.59 Z := Y
% 36.15/36.59 end
% 36.15/36.59 substitution1:
% 36.15/36.59 X := X
% 36.15/36.59 Y := Y
% 36.15/36.59 Z := mult( Z, mult( Z, T ) )
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 paramod: (44486) {G1,W23,D7,L1,V4,M1} { mult( mult( mult( mult( mult( X, Y
% 36.15/36.59 ), Y ), Z ), Z ), T ) ==> mult( X, mult( Y, mult( mult( mult( Y, Z ), Z
% 36.15/36.59 ), T ) ) ) }.
% 36.15/36.59 parent0[0]: (2) {G0,W15,D5,L1,V3,M1} I { mult( Z, mult( Y, mult( Y, X ) ) )
% 36.15/36.59 ==> mult( mult( mult( Z, Y ), Y ), X ) }.
% 36.15/36.59 parent1[0; 1]: (44476) {G1,W23,D7,L1,V4,M1} { mult( mult( mult( X, Y ), Y
% 36.15/36.59 ), mult( Z, mult( Z, T ) ) ) ==> mult( X, mult( Y, mult( mult( mult( Y,
% 36.15/36.59 Z ), Z ), T ) ) ) }.
% 36.15/36.59 substitution0:
% 36.15/36.59 X := T
% 36.15/36.59 Y := Z
% 36.15/36.59 Z := mult( mult( X, Y ), Y )
% 36.15/36.59 end
% 36.15/36.59 substitution1:
% 36.15/36.59 X := X
% 36.15/36.59 Y := Y
% 36.15/36.59 Z := Z
% 36.15/36.59 T := T
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 eqswap: (44487) {G1,W23,D7,L1,V4,M1} { mult( X, mult( Y, mult( mult( mult
% 36.15/36.59 ( Y, Z ), Z ), T ) ) ) ==> mult( mult( mult( mult( mult( X, Y ), Y ), Z )
% 36.15/36.59 , Z ), T ) }.
% 36.15/36.59 parent0[0]: (44486) {G1,W23,D7,L1,V4,M1} { mult( mult( mult( mult( mult( X
% 36.15/36.59 , Y ), Y ), Z ), Z ), T ) ==> mult( X, mult( Y, mult( mult( mult( Y, Z )
% 36.15/36.59 , Z ), T ) ) ) }.
% 36.15/36.59 substitution0:
% 36.15/36.59 X := X
% 36.15/36.59 Y := Y
% 36.15/36.59 Z := Z
% 36.15/36.59 T := T
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 subsumption: (13) {G1,W23,D7,L1,V4,M1} P(2,2);d(2) { mult( T, mult( X, mult
% 36.15/36.59 ( mult( mult( X, Y ), Y ), Z ) ) ) ==> mult( mult( mult( mult( mult( T, X
% 36.15/36.59 ), X ), Y ), Y ), Z ) }.
% 36.15/36.59 parent0: (44487) {G1,W23,D7,L1,V4,M1} { mult( X, mult( Y, mult( mult( mult
% 36.15/36.59 ( Y, Z ), Z ), T ) ) ) ==> mult( mult( mult( mult( mult( X, Y ), Y ), Z )
% 36.15/36.59 , Z ), T ) }.
% 36.15/36.59 substitution0:
% 36.15/36.59 X := T
% 36.15/36.59 Y := X
% 36.15/36.59 Z := Y
% 36.15/36.59 T := Z
% 36.15/36.59 end
% 36.15/36.59 permutation0:
% 36.15/36.59 0 ==> 0
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 eqswap: (44488) {G0,W15,D5,L1,V3,M1} { mult( mult( mult( X, Y ), Y ), Z )
% 36.15/36.59 ==> mult( X, mult( Y, mult( Y, Z ) ) ) }.
% 36.15/36.59 parent0[0]: (2) {G0,W15,D5,L1,V3,M1} I { mult( Z, mult( Y, mult( Y, X ) ) )
% 36.15/36.59 ==> mult( mult( mult( Z, Y ), Y ), X ) }.
% 36.15/36.59 substitution0:
% 36.15/36.59 X := Z
% 36.15/36.59 Y := Y
% 36.15/36.59 Z := X
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 paramod: (44492) {G1,W13,D5,L1,V2,M1} { mult( mult( mult( unit, X ), X ),
% 36.15/36.59 Y ) ==> mult( X, mult( X, Y ) ) }.
% 36.15/36.59 parent0[0]: (1) {G0,W5,D3,L1,V1,M1} I { mult( unit, X ) ==> X }.
% 36.15/36.59 parent1[0; 8]: (44488) {G0,W15,D5,L1,V3,M1} { mult( mult( mult( X, Y ), Y
% 36.15/36.59 ), Z ) ==> mult( X, mult( Y, mult( Y, Z ) ) ) }.
% 36.15/36.59 substitution0:
% 36.15/36.59 X := mult( X, mult( X, Y ) )
% 36.15/36.59 end
% 36.15/36.59 substitution1:
% 36.15/36.59 X := unit
% 36.15/36.59 Y := X
% 36.15/36.59 Z := Y
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 paramod: (44498) {G1,W11,D4,L1,V2,M1} { mult( mult( X, X ), Y ) ==> mult(
% 36.15/36.59 X, mult( X, Y ) ) }.
% 36.15/36.59 parent0[0]: (1) {G0,W5,D3,L1,V1,M1} I { mult( unit, X ) ==> X }.
% 36.15/36.59 parent1[0; 3]: (44492) {G1,W13,D5,L1,V2,M1} { mult( mult( mult( unit, X )
% 36.15/36.59 , X ), Y ) ==> mult( X, mult( X, Y ) ) }.
% 36.15/36.59 substitution0:
% 36.15/36.59 X := X
% 36.15/36.59 end
% 36.15/36.59 substitution1:
% 36.15/36.59 X := X
% 36.15/36.59 Y := Y
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 eqswap: (44499) {G1,W11,D4,L1,V2,M1} { mult( X, mult( X, Y ) ) ==> mult(
% 36.15/36.59 mult( X, X ), Y ) }.
% 36.15/36.59 parent0[0]: (44498) {G1,W11,D4,L1,V2,M1} { mult( mult( X, X ), Y ) ==>
% 36.15/36.59 mult( X, mult( X, Y ) ) }.
% 36.15/36.59 substitution0:
% 36.15/36.59 X := X
% 36.15/36.59 Y := Y
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 subsumption: (17) {G1,W11,D4,L1,V2,M1} P(2,1);d(1) { mult( X, mult( X, Y )
% 36.15/36.59 ) ==> mult( mult( X, X ), Y ) }.
% 36.15/36.59 parent0: (44499) {G1,W11,D4,L1,V2,M1} { mult( X, mult( X, Y ) ) ==> mult(
% 36.15/36.59 mult( X, X ), Y ) }.
% 36.15/36.59 substitution0:
% 36.15/36.59 X := X
% 36.15/36.59 Y := Y
% 36.15/36.59 end
% 36.15/36.59 permutation0:
% 36.15/36.59 0 ==> 0
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 eqswap: (44501) {G0,W15,D5,L1,V3,M1} { mult( mult( mult( X, Y ), Y ), Z )
% 36.15/36.59 ==> mult( X, mult( Y, mult( Y, Z ) ) ) }.
% 36.15/36.59 parent0[0]: (2) {G0,W15,D5,L1,V3,M1} I { mult( Z, mult( Y, mult( Y, X ) ) )
% 36.15/36.59 ==> mult( mult( mult( Z, Y ), Y ), X ) }.
% 36.15/36.59 substitution0:
% 36.15/36.59 X := Z
% 36.15/36.59 Y := Y
% 36.15/36.59 Z := X
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 paramod: (44505) {G1,W14,D5,L1,V2,M1} { mult( mult( mult( X, Y ), Y ), i(
% 36.15/36.59 Y ) ) ==> mult( X, mult( Y, unit ) ) }.
% 36.15/36.59 parent0[0]: (3) {G0,W6,D4,L1,V1,M1} I { mult( X, i( X ) ) ==> unit }.
% 36.15/36.59 parent1[0; 13]: (44501) {G0,W15,D5,L1,V3,M1} { mult( mult( mult( X, Y ), Y
% 36.15/36.59 ), Z ) ==> mult( X, mult( Y, mult( Y, Z ) ) ) }.
% 36.15/36.59 substitution0:
% 36.15/36.59 X := Y
% 36.15/36.59 end
% 36.15/36.59 substitution1:
% 36.15/36.59 X := X
% 36.15/36.59 Y := Y
% 36.15/36.59 Z := i( Y )
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 paramod: (44506) {G1,W12,D5,L1,V2,M1} { mult( mult( mult( X, Y ), Y ), i(
% 36.15/36.59 Y ) ) ==> mult( X, Y ) }.
% 36.15/36.59 parent0[0]: (0) {G0,W5,D3,L1,V1,M1} I { mult( X, unit ) ==> X }.
% 36.15/36.59 parent1[0; 11]: (44505) {G1,W14,D5,L1,V2,M1} { mult( mult( mult( X, Y ), Y
% 36.15/36.59 ), i( Y ) ) ==> mult( X, mult( Y, unit ) ) }.
% 36.15/36.59 substitution0:
% 36.15/36.59 X := Y
% 36.15/36.59 end
% 36.15/36.59 substitution1:
% 36.15/36.59 X := X
% 36.15/36.59 Y := Y
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 subsumption: (18) {G1,W12,D5,L1,V2,M1} P(3,2);d(0) { mult( mult( mult( Y, X
% 36.15/36.59 ), X ), i( X ) ) ==> mult( Y, X ) }.
% 36.15/36.59 parent0: (44506) {G1,W12,D5,L1,V2,M1} { mult( mult( mult( X, Y ), Y ), i(
% 36.15/36.59 Y ) ) ==> mult( X, Y ) }.
% 36.15/36.59 substitution0:
% 36.15/36.59 X := Y
% 36.15/36.59 Y := X
% 36.15/36.59 end
% 36.15/36.59 permutation0:
% 36.15/36.59 0 ==> 0
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 eqswap: (44509) {G0,W7,D2,L2,V3,M2} { ! Y = X, ! alpha1( Z, X, Y ) }.
% 36.15/36.59 parent0[1]: (8) {G0,W7,D2,L2,V3,M2} I { ! alpha1( X, Y, Z ), ! Y = Z }.
% 36.15/36.59 substitution0:
% 36.15/36.59 X := Z
% 36.15/36.59 Y := X
% 36.15/36.59 Z := Y
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 resolution: (44510) {G1,W6,D2,L2,V0,M2} { ! skol3 = skol2, ! skol3 ==>
% 36.15/36.59 skol2 }.
% 36.15/36.59 parent0[1]: (44509) {G0,W7,D2,L2,V3,M2} { ! Y = X, ! alpha1( Z, X, Y ) }.
% 36.15/36.59 parent1[0]: (6) {G0,W7,D2,L2,V0,M2} I { alpha1( skol1, skol2, skol3 ), !
% 36.15/36.59 skol3 ==> skol2 }.
% 36.15/36.59 substitution0:
% 36.15/36.59 X := skol2
% 36.15/36.59 Y := skol3
% 36.15/36.59 Z := skol1
% 36.15/36.59 end
% 36.15/36.59 substitution1:
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 factor: (44515) {G1,W3,D2,L1,V0,M1} { ! skol3 = skol2 }.
% 36.15/36.59 parent0[0, 1]: (44510) {G1,W6,D2,L2,V0,M2} { ! skol3 = skol2, ! skol3 ==>
% 36.15/36.59 skol2 }.
% 36.15/36.59 substitution0:
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 subsumption: (19) {G1,W3,D2,L1,V0,M1} S(6);r(8) { ! skol3 ==> skol2 }.
% 36.15/36.59 parent0: (44515) {G1,W3,D2,L1,V0,M1} { ! skol3 = skol2 }.
% 36.15/36.59 substitution0:
% 36.15/36.59 end
% 36.15/36.59 permutation0:
% 36.15/36.59 0 ==> 0
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 eqswap: (44516) {G0,W11,D3,L2,V3,M2} { mult( X, Z ) = mult( X, Y ), !
% 36.15/36.59 alpha1( X, Y, Z ) }.
% 36.15/36.59 parent0[1]: (7) {G0,W11,D3,L2,V3,M2} I { ! alpha1( X, Y, Z ), mult( X, Y )
% 36.15/36.59 = mult( X, Z ) }.
% 36.15/36.59 substitution0:
% 36.15/36.59 X := X
% 36.15/36.59 Y := Y
% 36.15/36.59 Z := Z
% 36.15/36.59 end
% 36.15/36.59
% 36.15/36.59 eqswap: (44517) {G0,W11,D3,L2,V0,M2} { mult( skol2, skol1 ) ==> mult(
% 70.59/71.07 skol3, skol1 ), alpha1( skol1, skol2, skol3 ) }.
% 70.59/71.07 parent0[1]: (5) {G0,W11,D3,L2,V0,M2} I { alpha1( skol1, skol2, skol3 ),
% 70.59/71.07 mult( skol3, skol1 ) ==> mult( skol2, skol1 ) }.
% 70.59/71.07 substitution0:
% 70.59/71.07 end
% 70.59/71.07
% 70.59/71.07 resolution: (44518) {G1,W14,D3,L2,V0,M2} { mult( skol1, skol3 ) = mult(
% 70.59/71.07 skol1, skol2 ), mult( skol2, skol1 ) ==> mult( skol3, skol1 ) }.
% 70.59/71.07 parent0[1]: (44516) {G0,W11,D3,L2,V3,M2} { mult( X, Z ) = mult( X, Y ), !
% 70.59/71.07 alpha1( X, Y, Z ) }.
% 70.59/71.07 parent1[1]: (44517) {G0,W11,D3,L2,V0,M2} { mult( skol2, skol1 ) ==> mult(
% 70.59/71.07 skol3, skol1 ), alpha1( skol1, skol2, skol3 ) }.
% 70.59/71.07 substitution0:
% 70.59/71.07 X := skol1
% 70.59/71.07 Y := skol2
% 70.59/71.07 Z := skol3
% 70.59/71.07 end
% 70.59/71.07 substitution1:
% 70.59/71.07 end
% 70.59/71.07
% 70.59/71.07 eqswap: (44520) {G1,W14,D3,L2,V0,M2} { mult( skol3, skol1 ) ==> mult(
% 70.59/71.07 skol2, skol1 ), mult( skol1, skol3 ) = mult( skol1, skol2 ) }.
% 70.59/71.07 parent0[1]: (44518) {G1,W14,D3,L2,V0,M2} { mult( skol1, skol3 ) = mult(
% 70.59/71.07 skol1, skol2 ), mult( skol2, skol1 ) ==> mult( skol3, skol1 ) }.
% 70.59/71.07 substitution0:
% 70.59/71.07 end
% 70.59/71.07
% 70.59/71.07 subsumption: (21) {G1,W14,D3,L2,V0,M2} R(7,5) { mult( skol1, skol3 ) ==>
% 70.59/71.07 mult( skol1, skol2 ), mult( skol3, skol1 ) ==> mult( skol2, skol1 ) }.
% 70.59/71.07 parent0: (44520) {G1,W14,D3,L2,V0,M2} { mult( skol3, skol1 ) ==> mult(
% 70.59/71.07 skol2, skol1 ), mult( skol1, skol3 ) = mult( skol1, skol2 ) }.
% 70.59/71.07 substitution0:
% 70.59/71.07 end
% 70.59/71.07 permutation0:
% 70.59/71.07 0 ==> 1
% 70.59/71.07 1 ==> 0
% 70.59/71.07 end
% 70.59/71.07
% 70.59/71.07 *** allocated 15000 integers for justifications
% 70.59/71.07 *** allocated 22500 integers for justifications
% 70.59/71.07 *** allocated 33750 integers for justifications
% 70.59/71.07 *** allocated 50625 integers for justifications
% 70.59/71.07 *** allocated 75937 integers for justifications
% 70.59/71.07 *** allocated 2919240 integers for clauses
% 70.59/71.07 *** allocated 113905 integers for justifications
% 70.59/71.07 *** allocated 170857 integers for justifications
% 70.59/71.07 *** allocated 1297440 integers for termspace/termends
% 70.59/71.07 *** allocated 256285 integers for justifications
% 70.59/71.07 *** allocated 384427 integers for justifications
% 70.59/71.07 eqswap: (44522) {G0,W11,D3,L2,V3,M2} { mult( X, Z ) = mult( X, Y ), !
% 70.59/71.07 alpha1( X, Y, Z ) }.
% 70.59/71.07 parent0[1]: (7) {G0,W11,D3,L2,V3,M2} I { ! alpha1( X, Y, Z ), mult( X, Y )
% 70.59/71.07 = mult( X, Z ) }.
% 70.59/71.07 substitution0:
% 70.59/71.07 X := X
% 70.59/71.07 Y := Y
% 70.59/71.07 Z := Z
% 70.59/71.07 end
% 70.59/71.07
% 70.59/71.07 eqswap: (44523) {G0,W15,D5,L1,V3,M1} { mult( mult( mult( X, Y ), Y ), Z )
% 70.59/71.07 ==> mult( X, mult( Y, mult( Y, Z ) ) ) }.
% 70.59/71.07 parent0[0]: (2) {G0,W15,D5,L1,V3,M1} I { mult( Z, mult( Y, mult( Y, X ) ) )
% 70.59/71.07 ==> mult( mult( mult( Z, Y ), Y ), X ) }.
% 70.59/71.07 substitution0:
% 70.59/71.07 X := Z
% 70.59/71.07 Y := Y
% 70.59/71.07 Z := X
% 70.59/71.07 end
% 70.59/71.07
% 70.59/71.07 paramod: (44530) {G1,W19,D5,L2,V4,M2} { mult( mult( mult( X, Y ), Y ), Z )
% 70.59/71.07 ==> mult( X, mult( Y, mult( Y, T ) ) ), ! alpha1( Y, T, Z ) }.
% 70.59/71.07 parent0[0]: (44522) {G0,W11,D3,L2,V3,M2} { mult( X, Z ) = mult( X, Y ), !
% 70.59/71.07 alpha1( X, Y, Z ) }.
% 70.59/71.07 parent1[0; 12]: (44523) {G0,W15,D5,L1,V3,M1} { mult( mult( mult( X, Y ), Y
% 70.59/71.07 ), Z ) ==> mult( X, mult( Y, mult( Y, Z ) ) ) }.
% 70.59/71.07 substitution0:
% 70.59/71.07 X := Y
% 70.59/71.07 Y := T
% 70.59/71.07 Z := Z
% 70.59/71.07 end
% 70.59/71.07 substitution1:
% 70.59/71.07 X := X
% 70.59/71.07 Y := Y
% 70.59/71.07 Z := Z
% 70.59/71.07 end
% 70.59/71.07
% 70.59/71.07 paramod: (49869) {G1,W19,D5,L2,V4,M2} { mult( mult( mult( X, Y ), Y ), Z )
% 70.59/71.07 ==> mult( mult( mult( X, Y ), Y ), T ), ! alpha1( Y, T, Z ) }.
% 70.59/71.07 parent0[0]: (2) {G0,W15,D5,L1,V3,M1} I { mult( Z, mult( Y, mult( Y, X ) ) )
% 70.59/71.07 ==> mult( mult( mult( Z, Y ), Y ), X ) }.
% 70.59/71.07 parent1[0; 8]: (44530) {G1,W19,D5,L2,V4,M2} { mult( mult( mult( X, Y ), Y
% 70.59/71.07 ), Z ) ==> mult( X, mult( Y, mult( Y, T ) ) ), ! alpha1( Y, T, Z ) }.
% 70.59/71.07 substitution0:
% 70.59/71.07 X := T
% 70.59/71.07 Y := Y
% 70.59/71.07 Z := X
% 70.59/71.07 end
% 70.59/71.07 substitution1:
% 70.59/71.07 X := X
% 70.59/71.07 Y := Y
% 70.59/71.07 Z := Z
% 70.59/71.07 T := T
% 70.59/71.07 end
% 70.59/71.07
% 70.59/71.07 subsumption: (32) {G1,W19,D5,L2,V4,M2} P(7,2);d(2) { ! alpha1( X, Y, Z ),
% 70.59/71.07 mult( mult( mult( T, X ), X ), Z ) = mult( mult( mult( T, X ), X ), Y )
% 70.59/71.07 }.
% 70.59/71.07 parent0: (49869) {G1,W19,D5,L2,V4,M2} { mult( mult( mult( X, Y ), Y ), Z )
% 70.59/71.07 ==> mult( mult( mult( X, Y ), Y ), T ), ! alpha1( Y, T, Z ) }.
% 70.59/71.07 substitution0:
% 70.59/71.07 X := T
% 70.59/71.07 Y := X
% 70.59/71.07 Z := Z
% 70.59/71.07 T := Y
% 70.59/71.07 end
% 70.59/71.07 permutation0:
% 70.59/71.07 0 ==> 1
% 70.59/71.07 1 ==> 0
% 70.59/71.07 end
% 70.59/71.07
% 70.59/71.07 eqswap: (49871) {G0,W11,D3,L2,V3,M2} { mult( X, Z ) = mult( X, Y ), !
% 70.59/71.07 alpha1( X, Y, Z ) }.
% 70.59/71.07 parent0[1]: (7) {G0,W11,D3,L2,V3,M2} I { ! alpha1( X, Y, Z ), mult( X, Y )
% 70.59/71.07 = mult( X, Z ) }.
% 70.59/71.07 substitution0:
% 70.59/71.07 X := X
% 70.59/71.07 Y := Y
% 70.59/71.07 Z := Z
% 70.59/71.07 end
% 70.59/71.07
% 70.59/71.07 eqswap: (49872) {G0,W5,D3,L1,V1,M1} { X ==> mult( unit, X ) }.
% 70.59/71.07 parent0[0]: (1) {G0,W5,D3,L1,V1,M1} I { mult( unit,Cputime limit exceeded (core dumped)
%------------------------------------------------------------------------------