%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : NUN065+2 : TPTP v8.1.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n032.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 : Mon Jul 18 16:19:11 EDT 2022
% Result : Theorem 0.51s 0.94s
% Output : Refutation 0.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.10 % Problem : NUN065+2 : TPTP v8.1.0. Released v7.3.0.
% 0.03/0.10 % Command : bliksem %s
% 0.10/0.30 % Computer : n032.cluster.edu
% 0.10/0.30 % Model : x86_64 x86_64
% 0.10/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.30 % Memory : 8042.1875MB
% 0.10/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.30 % CPULimit : 300
% 0.10/0.30 % DateTime : Thu Jun 2 09:11:30 EDT 2022
% 0.10/0.30 % CPUTime :
% 0.51/0.94 *** allocated 10000 integers for termspace/termends
% 0.51/0.94 *** allocated 10000 integers for clauses
% 0.51/0.94 *** allocated 10000 integers for justifications
% 0.51/0.94 Bliksem 1.12
% 0.51/0.94
% 0.51/0.94
% 0.51/0.94 Automatic Strategy Selection
% 0.51/0.94
% 0.51/0.94
% 0.51/0.94 Clauses:
% 0.51/0.94
% 0.51/0.94 { alpha1( skol1, X ), r1( X ) }.
% 0.51/0.94 { alpha1( skol1, X ), X = skol1 }.
% 0.51/0.94 { ! alpha1( X, Y ), ! r1( Y ) }.
% 0.51/0.94 { ! alpha1( X, Y ), ! Y = X }.
% 0.51/0.94 { r1( Y ), Y = X, alpha1( X, Y ) }.
% 0.51/0.94 { alpha2( X, skol2( X ), Y ), r2( X, Y ) }.
% 0.51/0.94 { alpha2( X, skol2( X ), Y ), Y = skol2( X ) }.
% 0.51/0.94 { ! alpha2( X, Y, Z ), ! r2( X, Z ) }.
% 0.51/0.94 { ! alpha2( X, Y, Z ), ! Z = Y }.
% 0.51/0.94 { r2( X, Z ), Z = Y, alpha2( X, Y, Z ) }.
% 0.51/0.94 { alpha3( X, Y, skol3( X, Y ), Z ), r3( X, Y, Z ) }.
% 0.51/0.94 { alpha3( X, Y, skol3( X, Y ), Z ), Z = skol3( X, Y ) }.
% 0.51/0.94 { ! alpha3( X, Y, Z, T ), ! r3( X, Y, T ) }.
% 0.51/0.94 { ! alpha3( X, Y, Z, T ), ! T = Z }.
% 0.51/0.94 { r3( X, Y, T ), T = Z, alpha3( X, Y, Z, T ) }.
% 0.51/0.94 { alpha4( X, Y, skol4( X, Y ), Z ), r4( X, Y, Z ) }.
% 0.51/0.94 { alpha4( X, Y, skol4( X, Y ), Z ), Z = skol4( X, Y ) }.
% 0.51/0.94 { ! alpha4( X, Y, Z, T ), ! r4( X, Y, T ) }.
% 0.51/0.94 { ! alpha4( X, Y, Z, T ), ! T = Z }.
% 0.51/0.94 { r4( X, Y, T ), T = Z, alpha4( X, Y, Z, T ) }.
% 0.51/0.94 { r2( Y, skol19( Z, Y ) ) }.
% 0.51/0.94 { r3( X, skol19( X, Y ), skol13( X, Y ) ) }.
% 0.51/0.94 { skol13( X, Y ) = skol5( X, Y ) }.
% 0.51/0.94 { r2( skol22( X, Y ), skol5( X, Y ) ) }.
% 0.51/0.94 { r3( X, Y, skol22( X, Y ) ) }.
% 0.51/0.94 { r2( Y, skol20( Z, Y ) ) }.
% 0.51/0.94 { r4( X, skol20( X, Y ), skol14( X, Y ) ) }.
% 0.51/0.94 { skol14( X, Y ) = skol6( X, Y ) }.
% 0.51/0.94 { r3( skol23( X, Y ), X, skol6( X, Y ) ) }.
% 0.51/0.94 { r4( X, Y, skol23( X, Y ) ) }.
% 0.51/0.94 { ! r2( X, T ), ! T = Z, ! r2( Y, Z ), X = Y }.
% 0.51/0.94 { r1( skol15( Y ) ) }.
% 0.51/0.94 { r3( X, skol15( X ), skol7( X ) ) }.
% 0.51/0.94 { skol7( X ) = X }.
% 0.51/0.94 { r1( skol16( Z ) ) }.
% 0.51/0.94 { skol8( Y ) = skol16( Y ) }.
% 0.51/0.94 { r1( skol21( Y ) ) }.
% 0.51/0.94 { r4( X, skol21( X ), skol8( X ) ) }.
% 0.51/0.94 { alpha5( X ), r2( skol17( Y ), skol9( Y ) ) }.
% 0.51/0.94 { alpha5( X ), X = skol9( X ) }.
% 0.51/0.94 { ! alpha5( X ), r1( skol10( Y ) ) }.
% 0.51/0.94 { ! alpha5( X ), X = skol10( X ) }.
% 0.51/0.94 { ! r1( Y ), ! X = Y, alpha5( X ) }.
% 0.51/0.94 { ! r1( Y ), ! Y = X, ! r2( Z, X ) }.
% 0.51/0.94 { alpha6( X ), r1( skol11( Y ) ) }.
% 0.51/0.94 { alpha6( X ), X = skol11( X ) }.
% 0.51/0.94 { ! alpha6( X ), r1( skol18( Z ) ) }.
% 0.51/0.94 { ! alpha6( X ), r2( skol18( Y ), skol12( Y ) ) }.
% 0.51/0.94 { ! alpha6( X ), X = skol12( X ) }.
% 0.51/0.94 { ! r1( Z ), ! r2( Z, Y ), ! X = Y, alpha6( X ) }.
% 0.51/0.94
% 0.51/0.94 percentage equality = 0.268817, percentage horn = 0.680000
% 0.51/0.94 This is a problem with some equality
% 0.51/0.94
% 0.51/0.94
% 0.51/0.94
% 0.51/0.94 Options Used:
% 0.51/0.94
% 0.51/0.94 useres = 1
% 0.51/0.94 useparamod = 1
% 0.51/0.94 useeqrefl = 1
% 0.51/0.94 useeqfact = 1
% 0.51/0.94 usefactor = 1
% 0.51/0.94 usesimpsplitting = 0
% 0.51/0.94 usesimpdemod = 5
% 0.51/0.94 usesimpres = 3
% 0.51/0.94
% 0.51/0.94 resimpinuse = 1000
% 0.51/0.94 resimpclauses = 20000
% 0.51/0.94 substype = eqrewr
% 0.51/0.94 backwardsubs = 1
% 0.51/0.94 selectoldest = 5
% 0.51/0.94
% 0.51/0.94 litorderings [0] = split
% 0.51/0.94 litorderings [1] = extend the termordering, first sorting on arguments
% 0.51/0.94
% 0.51/0.94 termordering = kbo
% 0.51/0.94
% 0.51/0.94 litapriori = 0
% 0.51/0.94 termapriori = 1
% 0.51/0.94 litaposteriori = 0
% 0.51/0.94 termaposteriori = 0
% 0.51/0.94 demodaposteriori = 0
% 0.51/0.94 ordereqreflfact = 0
% 0.51/0.94
% 0.51/0.94 litselect = negord
% 0.51/0.94
% 0.51/0.94 maxweight = 15
% 0.51/0.94 maxdepth = 30000
% 0.51/0.94 maxlength = 115
% 0.51/0.94 maxnrvars = 195
% 0.51/0.94 excuselevel = 1
% 0.51/0.94 increasemaxweight = 1
% 0.51/0.94
% 0.51/0.94 maxselected = 10000000
% 0.51/0.94 maxnrclauses = 10000000
% 0.51/0.94
% 0.51/0.94 showgenerated = 0
% 0.51/0.94 showkept = 0
% 0.51/0.94 showselected = 0
% 0.51/0.94 showdeleted = 0
% 0.51/0.94 showresimp = 1
% 0.51/0.94 showstatus = 2000
% 0.51/0.94
% 0.51/0.94 prologoutput = 0
% 0.51/0.94 nrgoals = 5000000
% 0.51/0.94 totalproof = 1
% 0.51/0.94
% 0.51/0.94 Symbols occurring in the translation:
% 0.51/0.94
% 0.51/0.94 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.51/0.94 . [1, 2] (w:1, o:70, a:1, s:1, b:0),
% 0.51/0.94 ! [4, 1] (w:0, o:50, a:1, s:1, b:0),
% 0.51/0.94 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.51/0.94 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.51/0.94 r1 [37, 1] (w:1, o:55, a:1, s:1, b:0),
% 0.51/0.94 r2 [41, 2] (w:1, o:94, a:1, s:1, b:0),
% 0.51/0.94 r3 [46, 3] (w:1, o:106, a:1, s:1, b:0),
% 0.51/0.94 r4 [51, 3] (w:1, o:107, a:1, s:1, b:0),
% 0.51/0.94 alpha1 [82, 2] (w:1, o:95, a:1, s:1, b:1),
% 0.51/0.94 alpha2 [83, 3] (w:1, o:108, a:1, s:1, b:1),
% 0.51/0.94 alpha3 [84, 4] (w:1, o:109, a:1, s:1, b:1),
% 0.51/0.94 alpha4 [85, 4] (w:1, o:110, a:1, s:1, b:1),
% 0.51/0.94 alpha5 [86, 1] (w:1, o:56, a:1, s:1, b:1),
% 0.51/0.94 alpha6 [87, 1] (w:1, o:57, a:1, s:1, b:1),
% 0.51/0.94 skol1 [88, 0] (w:1, o:49, a:1, s:1, b:1),
% 0.51/0.94 skol2 [89, 1] (w:1, o:65, a:1, s:1, b:1),
% 0.51/0.94 skol3 [90, 2] (w:1, o:99, a:1, s:1, b:1),
% 0.51/0.94 skol4 [91, 2] (w:1, o:100, a:1, s:1, b:1),
% 0.51/0.94 skol5 [92, 2] (w:1, o:101, a:1, s:1, b:1),
% 0.51/0.94 skol6 [93, 2] (w:1, o:102, a:1, s:1, b:1),
% 0.51/0.94 skol7 [94, 1] (w:1, o:66, a:1, s:1, b:1),
% 0.51/0.94 skol8 [95, 1] (w:1, o:67, a:1, s:1, b:1),
% 0.51/0.94 skol9 [96, 1] (w:1, o:68, a:1, s:1, b:1),
% 0.51/0.94 skol10 [97, 1] (w:1, o:58, a:1, s:1, b:1),
% 0.51/0.94 skol11 [98, 1] (w:1, o:59, a:1, s:1, b:1),
% 0.51/0.94 skol12 [99, 1] (w:1, o:60, a:1, s:1, b:1),
% 0.51/0.94 skol13 [100, 2] (w:1, o:103, a:1, s:1, b:1),
% 0.51/0.94 skol14 [101, 2] (w:1, o:104, a:1, s:1, b:1),
% 0.51/0.94 skol15 [102, 1] (w:1, o:61, a:1, s:1, b:1),
% 0.51/0.94 skol16 [103, 1] (w:1, o:62, a:1, s:1, b:1),
% 0.51/0.94 skol17 [104, 1] (w:1, o:63, a:1, s:1, b:1),
% 0.51/0.94 skol18 [105, 1] (w:1, o:64, a:1, s:1, b:1),
% 0.51/0.94 skol19 [106, 2] (w:1, o:105, a:1, s:1, b:1),
% 0.51/0.94 skol20 [107, 2] (w:1, o:96, a:1, s:1, b:1),
% 0.51/0.94 skol21 [108, 1] (w:1, o:69, a:1, s:1, b:1),
% 0.51/0.94 skol22 [109, 2] (w:1, o:97, a:1, s:1, b:1),
% 0.51/0.94 skol23 [110, 2] (w:1, o:98, a:1, s:1, b:1).
% 0.51/0.94
% 0.51/0.94
% 0.51/0.94 Starting Search:
% 0.51/0.94
% 0.51/0.94 *** allocated 15000 integers for clauses
% 0.51/0.94 *** allocated 22500 integers for clauses
% 0.51/0.94 *** allocated 33750 integers for clauses
% 0.51/0.94 *** allocated 50625 integers for clauses
% 0.51/0.94 *** allocated 15000 integers for termspace/termends
% 0.51/0.94 Resimplifying inuse:
% 0.51/0.94 Done
% 0.51/0.94
% 0.51/0.94 *** allocated 75937 integers for clauses
% 0.51/0.94 *** allocated 22500 integers for termspace/termends
% 0.51/0.94 *** allocated 113905 integers for clauses
% 0.51/0.94 *** allocated 33750 integers for termspace/termends
% 0.51/0.94
% 0.51/0.94 Intermediate Status:
% 0.51/0.94 Generated: 6124
% 0.51/0.94 Kept: 2033
% 0.51/0.94 Inuse: 206
% 0.51/0.94 Deleted: 66
% 0.51/0.94 Deletedinuse: 34
% 0.51/0.94
% 0.51/0.94 Resimplifying inuse:
% 0.51/0.94 Done
% 0.51/0.94
% 0.51/0.94
% 0.51/0.94 Bliksems!, er is een bewijs:
% 0.51/0.94 % SZS status Theorem
% 0.51/0.94 % SZS output start Refutation
% 0.51/0.94
% 0.51/0.94 (0) {G0,W5,D2,L2,V1,M2} I { alpha1( skol1, X ), r1( X ) }.
% 0.51/0.94 (1) {G0,W6,D2,L2,V1,M2} I { alpha1( skol1, X ), X = skol1 }.
% 0.51/0.94 (2) {G0,W5,D2,L2,V2,M2} I { ! alpha1( X, Y ), ! r1( Y ) }.
% 0.51/0.94 (3) {G0,W6,D2,L2,V2,M2} I { ! alpha1( X, Y ), ! Y = X }.
% 0.51/0.94 (4) {G0,W8,D2,L3,V2,M3} I { r1( Y ), Y = X, alpha1( X, Y ) }.
% 0.51/0.94 (5) {G0,W8,D3,L2,V2,M2} I { alpha2( X, skol2( X ), Y ), r2( X, Y ) }.
% 0.51/0.94 (6) {G0,W9,D3,L2,V2,M2} I { alpha2( X, skol2( X ), Y ), Y = skol2( X ) }.
% 0.51/0.94 (7) {G0,W7,D2,L2,V3,M2} I { ! alpha2( X, Y, Z ), ! r2( X, Z ) }.
% 0.51/0.94 (8) {G0,W7,D2,L2,V3,M2} I { ! alpha2( X, Y, Z ), ! Z = Y }.
% 0.51/0.94 (20) {G0,W5,D3,L1,V2,M1} I { r2( Y, skol19( Z, Y ) ) }.
% 0.51/0.94 (30) {G0,W12,D2,L4,V4,M4} I { ! r2( X, T ), ! T = Z, ! r2( Y, Z ), X = Y
% 0.51/0.94 }.
% 0.51/0.94 (36) {G0,W3,D3,L1,V1,M1} I { r1( skol21( Y ) ) }.
% 0.51/0.94 (38) {G0,W7,D3,L2,V2,M2} I { alpha5( X ), r2( skol17( Y ), skol9( Y ) ) }.
% 0.51/0.94 (40) {G0,W5,D3,L2,V2,M2} I { ! alpha5( X ), r1( skol10( Y ) ) }.
% 0.51/0.94 (41) {G0,W6,D3,L2,V1,M2} I { ! alpha5( X ), skol10( X ) ==> X }.
% 0.51/0.94 (42) {G0,W7,D2,L3,V2,M3} I { ! r1( Y ), ! X = Y, alpha5( X ) }.
% 0.51/0.94 (43) {G0,W8,D2,L3,V3,M3} I { ! r1( Y ), ! Y = X, ! r2( Z, X ) }.
% 0.51/0.94 (44) {G0,W5,D3,L2,V2,M2} I { alpha6( X ), r1( skol11( Y ) ) }.
% 0.51/0.94 (45) {G0,W6,D3,L2,V1,M2} I { alpha6( X ), skol11( X ) ==> X }.
% 0.51/0.94 (46) {G0,W5,D3,L2,V2,M2} I { ! alpha6( X ), r1( skol18( Z ) ) }.
% 0.51/0.94 (47) {G0,W7,D3,L2,V2,M2} I { ! alpha6( X ), r2( skol18( Y ), skol12( Y ) )
% 0.51/0.94 }.
% 0.51/0.94 (48) {G0,W6,D3,L2,V1,M2} I { ! alpha6( X ), skol12( X ) ==> X }.
% 0.51/0.94 (51) {G1,W4,D2,L1,V2,M1} Q(8) { ! alpha2( X, Y, Y ) }.
% 0.51/0.94 (55) {G1,W4,D2,L2,V1,M2} Q(42) { ! r1( X ), alpha5( X ) }.
% 0.51/0.94 (56) {G1,W5,D2,L2,V2,M2} Q(43) { ! r1( X ), ! r2( Y, X ) }.
% 0.51/0.94 (63) {G2,W3,D3,L1,V1,M1} R(55,36) { alpha5( skol21( X ) ) }.
% 0.51/0.94 (65) {G1,W5,D2,L2,V1,M2} R(2,1) { ! r1( X ), X = skol1 }.
% 0.51/0.94 (74) {G1,W5,D2,L2,V1,M2} R(3,0) { ! X = skol1, r1( X ) }.
% 0.51/0.94 (87) {G2,W4,D3,L1,V1,M1} R(5,51) { r2( X, skol2( X ) ) }.
% 0.51/0.94 (88) {G3,W3,D3,L1,V1,M1} R(87,56) { ! r1( skol2( X ) ) }.
% 0.51/0.94 (89) {G4,W7,D3,L2,V2,M2} P(4,87);r(88) { r2( X, Y ), alpha1( Y, skol2( X )
% 0.51/0.94 ) }.
% 0.51/0.94 (96) {G1,W9,D3,L2,V2,M2} R(6,3) { alpha2( X, skol2( X ), Y ), ! alpha1(
% 0.51/0.94 skol2( X ), Y ) }.
% 0.51/0.94 (123) {G1,W6,D3,L1,V3,M1} R(20,7) { ! alpha2( X, Y, skol19( Z, X ) ) }.
% 0.51/0.94 (124) {G2,W4,D3,L1,V2,M1} R(20,56) { ! r1( skol19( X, Y ) ) }.
% 0.51/0.94 (134) {G3,W5,D3,L1,V2,M1} R(124,74) { ! skol19( X, Y ) ==> skol1 }.
% 0.51/0.94 (198) {G2,W6,D3,L2,V3,M2} R(44,56) { alpha6( X ), ! r2( Y, skol11( Z ) )
% 0.51/0.94 }.
% 0.51/0.94 (214) {G3,W3,D3,L1,V1,M1} R(40,63) { r1( skol10( X ) ) }.
% 0.51/0.94 (251) {G4,W4,D3,L1,V1,M1} R(214,65) { skol10( X ) ==> skol1 }.
% 0.51/0.94 (332) {G2,W6,D3,L1,V2,M1} R(123,6) { skol19( X, Y ) ==> skol2( Y ) }.
% 0.51/0.94 (713) {G3,W7,D2,L3,V3,M3} P(45,198) { alpha6( Y ), ! r2( Z, X ), alpha6( X
% 0.51/0.94 ) }.
% 0.51/0.94 (714) {G1,W6,D2,L3,V2,M3} P(45,44) { alpha6( Y ), r1( X ), alpha6( X ) }.
% 0.51/0.94 (715) {G2,W4,D2,L2,V1,M2} F(714) { alpha6( X ), r1( X ) }.
% 0.51/0.94 (716) {G4,W5,D2,L2,V2,M2} F(713) { alpha6( X ), ! r2( Y, X ) }.
% 0.51/0.94 (729) {G3,W5,D3,L2,V2,M2} R(715,46) { r1( X ), r1( skol18( Y ) ) }.
% 0.51/0.94 (730) {G3,W3,D3,L1,V1,M1} R(715,124);d(332) { alpha6( skol2( Y ) ) }.
% 0.51/0.94 (733) {G4,W3,D3,L1,V1,M1} F(729) { r1( skol18( X ) ) }.
% 0.51/0.94 (767) {G5,W4,D3,L1,V1,M1} R(733,65) { skol18( X ) ==> skol1 }.
% 0.51/0.94 (922) {G5,W5,D3,L2,V2,M2} R(38,716) { alpha5( X ), alpha6( skol9( Y ) ) }.
% 0.51/0.94 (976) {G5,W5,D2,L2,V1,M2} S(41);d(251) { ! alpha5( X ), skol1 = X }.
% 0.51/0.94 (1013) {G6,W3,D3,L1,V1,M1} P(976,134);q;d(332) { ! alpha5( skol2( Y ) ) }.
% 0.51/0.94 (1024) {G7,W3,D3,L1,V1,M1} R(1013,922) { alpha6( skol9( X ) ) }.
% 0.51/0.94 (1100) {G6,W6,D3,L2,V2,M2} S(47);d(767) { ! alpha6( X ), r2( skol1, skol12
% 0.51/0.94 ( Y ) ) }.
% 0.51/0.94 (1254) {G8,W4,D3,L1,V1,M1} R(1100,1024) { r2( skol1, skol12( X ) ) }.
% 0.51/0.94 (1270) {G7,W7,D2,L3,V2,M3} P(48,1100) { ! alpha6( Y ), r2( skol1, X ), !
% 0.51/0.94 alpha6( X ) }.
% 0.51/0.94 (1291) {G8,W5,D2,L2,V1,M2} F(1270) { ! alpha6( X ), r2( skol1, X ) }.
% 0.51/0.94 (1335) {G9,W3,D3,L1,V1,M1} R(1254,56) { ! r1( skol12( X ) ) }.
% 0.51/0.94 (1376) {G10,W4,D2,L2,V1,M2} P(48,1335) { ! r1( X ), ! alpha6( X ) }.
% 0.51/0.94 (1425) {G11,W5,D2,L2,V1,M2} R(1376,74) { ! alpha6( X ), ! X = skol1 }.
% 0.51/0.94 (1493) {G12,W14,D2,L5,V4,M5} P(30,1425) { ! alpha6( Y ), ! Y = X, ! r2(
% 0.51/0.94 skol1, Z ), ! Z = T, ! r2( X, T ) }.
% 0.51/0.94 (1506) {G13,W8,D2,L3,V2,M3} F(1493);r(1291) { ! alpha6( X ), ! X = Y, ! r2
% 0.51/0.94 ( Y, Y ) }.
% 0.51/0.94 (1507) {G14,W5,D2,L2,V1,M2} Q(1506) { ! alpha6( X ), ! r2( X, X ) }.
% 0.51/0.94 (1538) {G15,W6,D2,L2,V2,M2} R(1507,716) { ! r2( X, X ), ! r2( Y, X ) }.
% 0.51/0.94 (1545) {G16,W3,D2,L1,V1,M1} F(1538) { ! r2( X, X ) }.
% 0.51/0.94 (1567) {G9,W4,D3,L1,V1,M1} R(1291,730) { r2( skol1, skol2( X ) ) }.
% 0.51/0.94 (1619) {G10,W5,D3,L1,V2,M1} R(1567,7) { ! alpha2( skol1, X, skol2( Y ) )
% 0.51/0.94 }.
% 0.51/0.94 (1691) {G17,W4,D3,L1,V1,M1} R(89,1545) { alpha1( X, skol2( X ) ) }.
% 0.51/0.94 (2076) {G11,W5,D3,L1,V1,M1} R(96,1619) { ! alpha1( skol2( skol1 ), skol2( X
% 0.51/0.94 ) ) }.
% 0.51/0.94 (2078) {G18,W0,D0,L0,V0,M0} R(2076,1691) { }.
% 0.51/0.94
% 0.51/0.94
% 0.51/0.94 % SZS output end Refutation
% 0.51/0.94 found a proof!
% 0.51/0.94
% 0.51/0.94
% 0.51/0.94 Unprocessed initial clauses:
% 0.51/0.94
% 0.51/0.94 (2080) {G0,W5,D2,L2,V1,M2} { alpha1( skol1, X ), r1( X ) }.
% 0.51/0.94 (2081) {G0,W6,D2,L2,V1,M2} { alpha1( skol1, X ), X = skol1 }.
% 0.51/0.94 (2082) {G0,W5,D2,L2,V2,M2} { ! alpha1( X, Y ), ! r1( Y ) }.
% 0.51/0.94 (2083) {G0,W6,D2,L2,V2,M2} { ! alpha1( X, Y ), ! Y = X }.
% 0.51/0.94 (2084) {G0,W8,D2,L3,V2,M3} { r1( Y ), Y = X, alpha1( X, Y ) }.
% 0.51/0.94 (2085) {G0,W8,D3,L2,V2,M2} { alpha2( X, skol2( X ), Y ), r2( X, Y ) }.
% 0.51/0.94 (2086) {G0,W9,D3,L2,V2,M2} { alpha2( X, skol2( X ), Y ), Y = skol2( X )
% 0.51/0.94 }.
% 0.51/0.94 (2087) {G0,W7,D2,L2,V3,M2} { ! alpha2( X, Y, Z ), ! r2( X, Z ) }.
% 0.51/0.94 (2088) {G0,W7,D2,L2,V3,M2} { ! alpha2( X, Y, Z ), ! Z = Y }.
% 0.51/0.94 (2089) {G0,W10,D2,L3,V3,M3} { r2( X, Z ), Z = Y, alpha2( X, Y, Z ) }.
% 0.51/0.94 (2090) {G0,W11,D3,L2,V3,M2} { alpha3( X, Y, skol3( X, Y ), Z ), r3( X, Y,
% 0.51/0.94 Z ) }.
% 0.51/0.94 (2091) {G0,W12,D3,L2,V3,M2} { alpha3( X, Y, skol3( X, Y ), Z ), Z = skol3
% 0.51/0.94 ( X, Y ) }.
% 0.51/0.94 (2092) {G0,W9,D2,L2,V4,M2} { ! alpha3( X, Y, Z, T ), ! r3( X, Y, T ) }.
% 0.51/0.94 (2093) {G0,W8,D2,L2,V4,M2} { ! alpha3( X, Y, Z, T ), ! T = Z }.
% 0.51/0.94 (2094) {G0,W12,D2,L3,V4,M3} { r3( X, Y, T ), T = Z, alpha3( X, Y, Z, T )
% 0.51/0.94 }.
% 0.51/0.94 (2095) {G0,W11,D3,L2,V3,M2} { alpha4( X, Y, skol4( X, Y ), Z ), r4( X, Y,
% 0.51/0.94 Z ) }.
% 0.51/0.94 (2096) {G0,W12,D3,L2,V3,M2} { alpha4( X, Y, skol4( X, Y ), Z ), Z = skol4
% 0.51/0.94 ( X, Y ) }.
% 0.51/0.94 (2097) {G0,W9,D2,L2,V4,M2} { ! alpha4( X, Y, Z, T ), ! r4( X, Y, T ) }.
% 0.51/0.94 (2098) {G0,W8,D2,L2,V4,M2} { ! alpha4( X, Y, Z, T ), ! T = Z }.
% 0.51/0.94 (2099) {G0,W12,D2,L3,V4,M3} { r4( X, Y, T ), T = Z, alpha4( X, Y, Z, T )
% 0.51/0.94 }.
% 0.51/0.94 (2100) {G0,W5,D3,L1,V2,M1} { r2( Y, skol19( Z, Y ) ) }.
% 0.51/0.94 (2101) {G0,W8,D3,L1,V2,M1} { r3( X, skol19( X, Y ), skol13( X, Y ) ) }.
% 0.51/0.94 (2102) {G0,W7,D3,L1,V2,M1} { skol13( X, Y ) = skol5( X, Y ) }.
% 0.51/0.94 (2103) {G0,W7,D3,L1,V2,M1} { r2( skol22( X, Y ), skol5( X, Y ) ) }.
% 0.51/0.94 (2104) {G0,W6,D3,L1,V2,M1} { r3( X, Y, skol22( X, Y ) ) }.
% 0.51/0.94 (2105) {G0,W5,D3,L1,V2,M1} { r2( Y, skol20( Z, Y ) ) }.
% 0.51/0.94 (2106) {G0,W8,D3,L1,V2,M1} { r4( X, skol20( X, Y ), skol14( X, Y ) ) }.
% 0.51/0.94 (2107) {G0,W7,D3,L1,V2,M1} { skol14( X, Y ) = skol6( X, Y ) }.
% 0.51/0.94 (2108) {G0,W8,D3,L1,V2,M1} { r3( skol23( X, Y ), X, skol6( X, Y ) ) }.
% 0.51/0.94 (2109) {G0,W6,D3,L1,V2,M1} { r4( X, Y, skol23( X, Y ) ) }.
% 0.51/0.94 (2110) {G0,W12,D2,L4,V4,M4} { ! r2( X, T ), ! T = Z, ! r2( Y, Z ), X = Y
% 0.51/0.94 }.
% 0.51/0.94 (2111) {G0,W3,D3,L1,V1,M1} { r1( skol15( Y ) ) }.
% 0.51/0.94 (2112) {G0,W6,D3,L1,V1,M1} { r3( X, skol15( X ), skol7( X ) ) }.
% 0.51/0.94 (2113) {G0,W4,D3,L1,V1,M1} { skol7( X ) = X }.
% 0.51/0.94 (2114) {G0,W3,D3,L1,V1,M1} { r1( skol16( Z ) ) }.
% 0.51/0.94 (2115) {G0,W5,D3,L1,V1,M1} { skol8( Y ) = skol16( Y ) }.
% 0.51/0.94 (2116) {G0,W3,D3,L1,V1,M1} { r1( skol21( Y ) ) }.
% 0.51/0.94 (2117) {G0,W6,D3,L1,V1,M1} { r4( X, skol21( X ), skol8( X ) ) }.
% 0.51/0.94 (2118) {G0,W7,D3,L2,V2,M2} { alpha5( X ), r2( skol17( Y ), skol9( Y ) )
% 0.51/0.94 }.
% 0.51/0.94 (2119) {G0,W6,D3,L2,V1,M2} { alpha5( X ), X = skol9( X ) }.
% 0.51/0.94 (2120) {G0,W5,D3,L2,V2,M2} { ! alpha5( X ), r1( skol10( Y ) ) }.
% 0.51/0.94 (2121) {G0,W6,D3,L2,V1,M2} { ! alpha5( X ), X = skol10( X ) }.
% 0.51/0.94 (2122) {G0,W7,D2,L3,V2,M3} { ! r1( Y ), ! X = Y, alpha5( X ) }.
% 0.51/0.94 (2123) {G0,W8,D2,L3,V3,M3} { ! r1( Y ), ! Y = X, ! r2( Z, X ) }.
% 0.51/0.94 (2124) {G0,W5,D3,L2,V2,M2} { alpha6( X ), r1( skol11( Y ) ) }.
% 0.51/0.94 (2125) {G0,W6,D3,L2,V1,M2} { alpha6( X ), X = skol11( X ) }.
% 0.51/0.94 (2126) {G0,W5,D3,L2,V2,M2} { ! alpha6( X ), r1( skol18( Z ) ) }.
% 0.51/0.94 (2127) {G0,W7,D3,L2,V2,M2} { ! alpha6( X ), r2( skol18( Y ), skol12( Y ) )
% 0.51/0.94 }.
% 0.51/0.94 (2128) {G0,W6,D3,L2,V1,M2} { ! alpha6( X ), X = skol12( X ) }.
% 0.51/0.94 (2129) {G0,W10,D2,L4,V3,M4} { ! r1( Z ), ! r2( Z, Y ), ! X = Y, alpha6( X
% 0.51/0.94 ) }.
% 0.51/0.94
% 0.51/0.94
% 0.51/0.94 Total Proof:
% 0.51/0.94
% 0.51/0.94 subsumption: (0) {G0,W5,D2,L2,V1,M2} I { alpha1( skol1, X ), r1( X ) }.
% 0.51/0.94 parent0: (2080) {G0,W5,D2,L2,V1,M2} { alpha1( skol1, X ), r1( X ) }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := X
% 0.51/0.94 end
% 0.51/0.94 permutation0:
% 0.51/0.94 0 ==> 0
% 0.51/0.94 1 ==> 1
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 subsumption: (1) {G0,W6,D2,L2,V1,M2} I { alpha1( skol1, X ), X = skol1 }.
% 0.51/0.94 parent0: (2081) {G0,W6,D2,L2,V1,M2} { alpha1( skol1, X ), X = skol1 }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := X
% 0.51/0.94 end
% 0.51/0.94 permutation0:
% 0.51/0.94 0 ==> 0
% 0.51/0.94 1 ==> 1
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 subsumption: (2) {G0,W5,D2,L2,V2,M2} I { ! alpha1( X, Y ), ! r1( Y ) }.
% 0.51/0.94 parent0: (2082) {G0,W5,D2,L2,V2,M2} { ! alpha1( X, Y ), ! r1( Y ) }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := X
% 0.51/0.94 Y := Y
% 0.51/0.94 end
% 0.51/0.94 permutation0:
% 0.51/0.94 0 ==> 0
% 0.51/0.94 1 ==> 1
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 subsumption: (3) {G0,W6,D2,L2,V2,M2} I { ! alpha1( X, Y ), ! Y = X }.
% 0.51/0.94 parent0: (2083) {G0,W6,D2,L2,V2,M2} { ! alpha1( X, Y ), ! Y = X }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := X
% 0.51/0.94 Y := Y
% 0.51/0.94 end
% 0.51/0.94 permutation0:
% 0.51/0.94 0 ==> 0
% 0.51/0.94 1 ==> 1
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 subsumption: (4) {G0,W8,D2,L3,V2,M3} I { r1( Y ), Y = X, alpha1( X, Y ) }.
% 0.51/0.94 parent0: (2084) {G0,W8,D2,L3,V2,M3} { r1( Y ), Y = X, alpha1( X, Y ) }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := X
% 0.51/0.94 Y := Y
% 0.51/0.94 end
% 0.51/0.94 permutation0:
% 0.51/0.94 0 ==> 0
% 0.51/0.94 1 ==> 1
% 0.51/0.94 2 ==> 2
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 subsumption: (5) {G0,W8,D3,L2,V2,M2} I { alpha2( X, skol2( X ), Y ), r2( X
% 0.51/0.94 , Y ) }.
% 0.51/0.94 parent0: (2085) {G0,W8,D3,L2,V2,M2} { alpha2( X, skol2( X ), Y ), r2( X, Y
% 0.51/0.94 ) }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := X
% 0.51/0.94 Y := Y
% 0.51/0.94 end
% 0.51/0.94 permutation0:
% 0.51/0.94 0 ==> 0
% 0.51/0.94 1 ==> 1
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 subsumption: (6) {G0,W9,D3,L2,V2,M2} I { alpha2( X, skol2( X ), Y ), Y =
% 0.51/0.94 skol2( X ) }.
% 0.51/0.94 parent0: (2086) {G0,W9,D3,L2,V2,M2} { alpha2( X, skol2( X ), Y ), Y =
% 0.51/0.94 skol2( X ) }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := X
% 0.51/0.94 Y := Y
% 0.51/0.94 end
% 0.51/0.94 permutation0:
% 0.51/0.94 0 ==> 0
% 0.51/0.94 1 ==> 1
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 subsumption: (7) {G0,W7,D2,L2,V3,M2} I { ! alpha2( X, Y, Z ), ! r2( X, Z )
% 0.51/0.94 }.
% 0.51/0.94 parent0: (2087) {G0,W7,D2,L2,V3,M2} { ! alpha2( X, Y, Z ), ! r2( X, Z )
% 0.51/0.94 }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := X
% 0.51/0.94 Y := Y
% 0.51/0.94 Z := Z
% 0.51/0.94 end
% 0.51/0.94 permutation0:
% 0.51/0.94 0 ==> 0
% 0.51/0.94 1 ==> 1
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 subsumption: (8) {G0,W7,D2,L2,V3,M2} I { ! alpha2( X, Y, Z ), ! Z = Y }.
% 0.51/0.94 parent0: (2088) {G0,W7,D2,L2,V3,M2} { ! alpha2( X, Y, Z ), ! Z = Y }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := X
% 0.51/0.94 Y := Y
% 0.51/0.94 Z := Z
% 0.51/0.94 end
% 0.51/0.94 permutation0:
% 0.51/0.94 0 ==> 0
% 0.51/0.94 1 ==> 1
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 subsumption: (20) {G0,W5,D3,L1,V2,M1} I { r2( Y, skol19( Z, Y ) ) }.
% 0.51/0.94 parent0: (2100) {G0,W5,D3,L1,V2,M1} { r2( Y, skol19( Z, Y ) ) }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := T
% 0.51/0.94 Y := Y
% 0.51/0.94 Z := Z
% 0.51/0.94 end
% 0.51/0.94 permutation0:
% 0.51/0.94 0 ==> 0
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 subsumption: (30) {G0,W12,D2,L4,V4,M4} I { ! r2( X, T ), ! T = Z, ! r2( Y,
% 0.51/0.94 Z ), X = Y }.
% 0.51/0.94 parent0: (2110) {G0,W12,D2,L4,V4,M4} { ! r2( X, T ), ! T = Z, ! r2( Y, Z )
% 0.51/0.94 , X = Y }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := X
% 0.51/0.94 Y := Y
% 0.51/0.94 Z := Z
% 0.51/0.94 T := T
% 0.51/0.94 end
% 0.51/0.94 permutation0:
% 0.51/0.94 0 ==> 0
% 0.51/0.94 1 ==> 1
% 0.51/0.94 2 ==> 2
% 0.51/0.94 3 ==> 3
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 subsumption: (36) {G0,W3,D3,L1,V1,M1} I { r1( skol21( Y ) ) }.
% 0.51/0.94 parent0: (2116) {G0,W3,D3,L1,V1,M1} { r1( skol21( Y ) ) }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := Z
% 0.51/0.94 Y := Y
% 0.51/0.94 end
% 0.51/0.94 permutation0:
% 0.51/0.94 0 ==> 0
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 subsumption: (38) {G0,W7,D3,L2,V2,M2} I { alpha5( X ), r2( skol17( Y ),
% 0.51/0.94 skol9( Y ) ) }.
% 0.51/0.94 parent0: (2118) {G0,W7,D3,L2,V2,M2} { alpha5( X ), r2( skol17( Y ), skol9
% 0.51/0.94 ( Y ) ) }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := X
% 0.51/0.94 Y := Y
% 0.51/0.94 end
% 0.51/0.94 permutation0:
% 0.51/0.94 0 ==> 0
% 0.51/0.94 1 ==> 1
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 subsumption: (40) {G0,W5,D3,L2,V2,M2} I { ! alpha5( X ), r1( skol10( Y ) )
% 0.51/0.94 }.
% 0.51/0.94 parent0: (2120) {G0,W5,D3,L2,V2,M2} { ! alpha5( X ), r1( skol10( Y ) ) }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := X
% 0.51/0.94 Y := Y
% 0.51/0.94 end
% 0.51/0.94 permutation0:
% 0.51/0.94 0 ==> 0
% 0.51/0.94 1 ==> 1
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 eqswap: (2255) {G0,W6,D3,L2,V1,M2} { skol10( X ) = X, ! alpha5( X ) }.
% 0.51/0.94 parent0[1]: (2121) {G0,W6,D3,L2,V1,M2} { ! alpha5( X ), X = skol10( X )
% 0.51/0.94 }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := X
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 subsumption: (41) {G0,W6,D3,L2,V1,M2} I { ! alpha5( X ), skol10( X ) ==> X
% 0.51/0.94 }.
% 0.51/0.94 parent0: (2255) {G0,W6,D3,L2,V1,M2} { skol10( X ) = X, ! alpha5( X ) }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := X
% 0.51/0.94 end
% 0.51/0.94 permutation0:
% 0.51/0.94 0 ==> 1
% 0.51/0.94 1 ==> 0
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 subsumption: (42) {G0,W7,D2,L3,V2,M3} I { ! r1( Y ), ! X = Y, alpha5( X )
% 0.51/0.94 }.
% 0.51/0.94 parent0: (2122) {G0,W7,D2,L3,V2,M3} { ! r1( Y ), ! X = Y, alpha5( X ) }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := X
% 0.51/0.94 Y := Y
% 0.51/0.94 end
% 0.51/0.94 permutation0:
% 0.51/0.94 0 ==> 0
% 0.51/0.94 1 ==> 1
% 0.51/0.94 2 ==> 2
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 subsumption: (43) {G0,W8,D2,L3,V3,M3} I { ! r1( Y ), ! Y = X, ! r2( Z, X )
% 0.51/0.94 }.
% 0.51/0.94 parent0: (2123) {G0,W8,D2,L3,V3,M3} { ! r1( Y ), ! Y = X, ! r2( Z, X ) }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := X
% 0.51/0.94 Y := Y
% 0.51/0.94 Z := Z
% 0.51/0.94 end
% 0.51/0.94 permutation0:
% 0.51/0.94 0 ==> 0
% 0.51/0.94 1 ==> 1
% 0.51/0.94 2 ==> 2
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 subsumption: (44) {G0,W5,D3,L2,V2,M2} I { alpha6( X ), r1( skol11( Y ) )
% 0.51/0.94 }.
% 0.51/0.94 parent0: (2124) {G0,W5,D3,L2,V2,M2} { alpha6( X ), r1( skol11( Y ) ) }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := X
% 0.51/0.94 Y := Y
% 0.51/0.94 end
% 0.51/0.94 permutation0:
% 0.51/0.94 0 ==> 0
% 0.51/0.94 1 ==> 1
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 eqswap: (2343) {G0,W6,D3,L2,V1,M2} { skol11( X ) = X, alpha6( X ) }.
% 0.51/0.94 parent0[1]: (2125) {G0,W6,D3,L2,V1,M2} { alpha6( X ), X = skol11( X ) }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := X
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 subsumption: (45) {G0,W6,D3,L2,V1,M2} I { alpha6( X ), skol11( X ) ==> X
% 0.51/0.94 }.
% 0.51/0.94 parent0: (2343) {G0,W6,D3,L2,V1,M2} { skol11( X ) = X, alpha6( X ) }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := X
% 0.51/0.94 end
% 0.51/0.94 permutation0:
% 0.51/0.94 0 ==> 1
% 0.51/0.94 1 ==> 0
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 subsumption: (46) {G0,W5,D3,L2,V2,M2} I { ! alpha6( X ), r1( skol18( Z ) )
% 0.51/0.94 }.
% 0.51/0.94 parent0: (2126) {G0,W5,D3,L2,V2,M2} { ! alpha6( X ), r1( skol18( Z ) ) }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := X
% 0.51/0.94 Y := T
% 0.51/0.94 Z := Z
% 0.51/0.94 end
% 0.51/0.94 permutation0:
% 0.51/0.94 0 ==> 0
% 0.51/0.94 1 ==> 1
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 subsumption: (47) {G0,W7,D3,L2,V2,M2} I { ! alpha6( X ), r2( skol18( Y ),
% 0.51/0.94 skol12( Y ) ) }.
% 0.51/0.94 parent0: (2127) {G0,W7,D3,L2,V2,M2} { ! alpha6( X ), r2( skol18( Y ),
% 0.51/0.94 skol12( Y ) ) }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := X
% 0.51/0.94 Y := Y
% 0.51/0.94 end
% 0.51/0.94 permutation0:
% 0.51/0.94 0 ==> 0
% 0.51/0.94 1 ==> 1
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 eqswap: (2413) {G0,W6,D3,L2,V1,M2} { skol12( X ) = X, ! alpha6( X ) }.
% 0.51/0.94 parent0[1]: (2128) {G0,W6,D3,L2,V1,M2} { ! alpha6( X ), X = skol12( X )
% 0.51/0.94 }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := X
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 subsumption: (48) {G0,W6,D3,L2,V1,M2} I { ! alpha6( X ), skol12( X ) ==> X
% 0.51/0.94 }.
% 0.51/0.94 parent0: (2413) {G0,W6,D3,L2,V1,M2} { skol12( X ) = X, ! alpha6( X ) }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := X
% 0.51/0.94 end
% 0.51/0.94 permutation0:
% 0.51/0.94 0 ==> 1
% 0.51/0.94 1 ==> 0
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 eqswap: (2414) {G0,W7,D2,L2,V3,M2} { ! Y = X, ! alpha2( Z, Y, X ) }.
% 0.51/0.94 parent0[1]: (8) {G0,W7,D2,L2,V3,M2} I { ! alpha2( X, Y, Z ), ! Z = Y }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := Z
% 0.51/0.94 Y := Y
% 0.51/0.94 Z := X
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 eqrefl: (2415) {G0,W4,D2,L1,V2,M1} { ! alpha2( Y, X, X ) }.
% 0.51/0.94 parent0[0]: (2414) {G0,W7,D2,L2,V3,M2} { ! Y = X, ! alpha2( Z, Y, X ) }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := X
% 0.51/0.94 Y := X
% 0.51/0.94 Z := Y
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 subsumption: (51) {G1,W4,D2,L1,V2,M1} Q(8) { ! alpha2( X, Y, Y ) }.
% 0.51/0.94 parent0: (2415) {G0,W4,D2,L1,V2,M1} { ! alpha2( Y, X, X ) }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := Y
% 0.51/0.94 Y := X
% 0.51/0.94 end
% 0.51/0.94 permutation0:
% 0.51/0.94 0 ==> 0
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 eqswap: (2416) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! r1( Y ), alpha5( X ) }.
% 0.51/0.94 parent0[1]: (42) {G0,W7,D2,L3,V2,M3} I { ! r1( Y ), ! X = Y, alpha5( X )
% 0.51/0.94 }.
% 0.51/0.94 substitution0:
% 0.51/0.94 X := X
% 0.51/0.94 Y := Y
% 0.51/0.94 end
% 0.51/0.94
% 0.51/0.94 eqrefl: (2417) {G0,W4,D2,L2,V1,M2} { ! r1( X ), alpha5( X ) }.
% 0.51/1.02 parent0[0]: (2416) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! r1( Y ), alpha5( X )
% 0.51/1.02 }.
% 0.51/1.02 substitution0:
% 0.51/1.02 X := X
% 0.51/1.02 Y := X
% 0.51/1.02 end
% 0.51/1.02
% 0.51/1.02 subsumption: (55) {G1,W4,D2,L2,V1,M2} Q(42) { ! r1( X ), alpha5( X ) }.
% 0.51/1.02 parent0: (2417) {G0,W4,D2,L2,V1,M2} { ! r1( X ), alpha5( X ) }.
% 0.51/1.02 substitution0:
% 0.51/1.02 X := X
% 0.51/1.02 end
% 0.51/1.02 permutation0:
% 0.51/1.02 0 ==> 0
% 0.51/1.02 1 ==> 1
% 0.51/1.02 end
% 0.51/1.02
% 0.51/1.02 eqswap: (2418) {G0,W8,D2,L3,V3,M3} { ! Y = X, ! r1( X ), ! r2( Z, Y ) }.
% 0.51/1.02 parent0[1]: (43) {G0,W8,D2,L3,V3,M3} I { ! r1( Y ), ! Y = X, ! r2( Z, X )
% 0.51/1.02 }.
% 0.51/1.02 substitution0:
% 0.51/1.02 X := Y
% 0.51/1.02 Y := X
% 0.51/1.02 Z := Z
% 0.51/1.02 end
% 0.51/1.02
% 0.51/1.02 eqrefl: (2419) {G0,W5,D2,L2,V2,M2} { ! r1( X ), ! r2( Y, X ) }.
% 0.51/1.02 parent0[0]: (2418) {G0,W8,D2,L3,V3,M3} { ! Y = X, ! r1( X ), ! r2( Z, Y )
% 0.51/1.02 }.
% 0.51/1.02 substitution0:
% 0.51/1.02 X := X
% 0.51/1.02 Y := X
% 0.51/1.02 Z := Y
% 0.51/1.02 end
% 0.51/1.02
% 0.51/1.02 subsumption: (56) {G1,W5,D2,L2,V2,M2} Q(43) { ! r1( X ), ! r2( Y, X ) }.
% 0.51/1.02 parent0: (2419) {G0,W5,D2,L2,V2,M2} { ! r1( X ), ! r2( Y, X ) }.
% 0.51/1.02 substitution0:
% 0.51/1.02 X := X
% 0.51/1.02 Y := Y
% 0.51/1.02 end
% 0.51/1.02 permutation0:
% 0.51/1.02 0 ==> 0
% 0.51/1.02 1 ==> 1
% 0.51/1.02 end
% 0.51/1.02
% 0.51/1.02 resolution: (2420) {G1,W3,D3,L1,V1,M1} { alpha5( skol21( X ) ) }.
% 0.51/1.02 parent0[0]: (55) {G1,W4,D2,L2,V1,M2} Q(42) { ! r1( X ), alpha5( X ) }.
% 0.51/1.02 parent1[0]: (36) {G0,W3,D3,L1,V1,M1} I { r1( skol21( Y ) ) }.
% 0.51/1.02 substitution0:
% 0.51/1.02 X := skol21( X )
% 0.51/1.02 end
% 0.51/1.02 substitution1:
% 0.51/1.02 X := Y
% 0.51/1.02 Y := X
% 0.51/1.02 end
% 0.51/1.02
% 0.51/1.02 subsumption: (63) {G2,W3,D3,L1,V1,M1} R(55,36) { alpha5( skol21( X ) ) }.
% 0.51/1.02 parent0: (2420) {G1,W3,D3,L1,V1,M1} { alpha5( skol21( X ) ) }.
% 0.51/1.02 substitution0:
% 0.51/1.02 X := X
% 0.51/1.02 end
% 0.51/1.02 permutation0:
% 0.51/1.02 0 ==> 0
% 0.51/1.02 end
% 0.51/1.02
% 0.51/1.02 eqswap: (2421) {G0,W6,D2,L2,V1,M2} { skol1 = X, alpha1( skol1, X ) }.
% 0.51/1.02 parent0[1]: (1) {G0,W6,D2,L2,V1,M2} I { alpha1( skol1, X ), X = skol1 }.
% 0.51/1.02 substitution0:
% 0.51/1.02 X := X
% 0.51/1.02 end
% 0.51/1.02
% 0.51/1.02 resolution: (2422) {G1,W5,D2,L2,V1,M2} { ! r1( X ), skol1 = X }.
% 0.51/1.02 parent0[0]: (2) {G0,W5,D2,L2,V2,M2} I { ! alpha1( X, Y ), ! r1( Y ) }.
% 0.51/1.02 parent1[1]: (2421) {G0,W6,D2,L2,V1,M2} { skol1 = X, alpha1( skol1, X ) }.
% 0.51/1.02 substitution0:
% 0.51/1.02 X := skol1
% 0.51/1.02 Y := X
% 0.51/1.02 end
% 0.51/1.02 substitution1:
% 0.51/1.02 X := X
% 0.51/1.02 end
% 0.51/1.02
% 0.51/1.02 eqswap: (2423) {G1,W5,D2,L2,V1,M2} { X = skol1, ! r1( X ) }.
% 0.51/1.02 parent0[1]: (2422) {G1,W5,D2,L2,V1,M2} { ! r1( X ), skol1 = X }.
% 0.51/1.02 substitution0:
% 0.51/1.02 X := X
% 0.51/1.02 end
% 0.51/1.02
% 0.51/1.02 subsumption: (65) {G1,W5,D2,L2,V1,M2} R(2,1) { ! r1( X ), X = skol1 }.
% 0.51/1.02 parent0: (2423) {G1,W5,D2,L2,V1,M2} { X = skol1, ! r1( X ) }.
% 0.51/1.02 substitution0:
% 0.51/1.02 X := X
% 0.51/1.02 end
% 0.51/1.02 permutation0:
% 0.51/1.02 0 ==> 1
% 0.51/1.02 1 ==> 0
% 0.51/1.02 end
% 0.51/1.02
% 0.51/1.02 eqswap: (2424) {G0,W6,D2,L2,V2,M2} { ! Y = X, ! alpha1( Y, X ) }.
% 0.51/1.02 parent0[1]: (3) {G0,W6,D2,L2,V2,M2} I { ! alpha1( X, Y ), ! Y = X }.
% 0.51/1.02 substitution0:
% 0.51/1.02 X := Y
% 0.51/1.02 Y := X
% 0.51/1.02 end
% 0.51/1.02
% 0.51/1.02 resolution: (2425) {G1,W5,D2,L2,V1,M2} { ! skol1 = X, r1( X ) }.
% 0.51/1.02 parent0[1]: (2424) {G0,W6,D2,L2,V2,M2} { ! Y = X, ! alpha1( Y, X ) }.
% 0.51/1.02 parent1[0]: (0) {G0,W5,D2,L2,V1,M2} I { alpha1( skol1, X ), r1( X ) }.
% 0.51/1.02 substitution0:
% 0.51/1.02 X := X
% 0.51/1.02 Y := skol1
% 0.51/1.02 end
% 0.51/1.02 substitution1:
% 0.51/1.02 X := X
% 0.51/1.02 end
% 0.51/1.02
% 0.51/1.02 eqswap: (2426) {G1,W5,D2,L2,V1,M2} { ! X = skol1, r1( X ) }.
% 0.51/1.02 parent0[0]: (2425) {G1,W5,D2,L2,V1,M2} { ! skol1 = X, r1( X ) }.
% 0.51/1.02 substitution0:
% 0.51/1.02 X := X
% 0.51/1.02 end
% 0.51/1.02
% 0.51/1.02 subsumption: (74) {G1,W5,D2,L2,V1,M2} R(3,0) { ! X = skol1, r1( X ) }.
% 0.51/1.02 parent0: (2426) {G1,W5,D2,L2,V1,M2} { ! X = skol1, r1( X ) }.
% 0.51/1.02 substitution0:
% 0.51/1.02 X := X
% 0.51/1.02 end
% 0.51/1.02 permutation0:
% 0.51/1.02 0 ==> 0
% 0.51/1.02 1 ==> 1
% 0.51/1.02 end
% 0.51/1.02
% 0.51/1.02 resolution: (2427) {G1,W4,D3,L1,V1,M1} { r2( X, skol2( X ) ) }.
% 0.51/1.02 parent0[0]: (51) {G1,W4,D2,L1,V2,M1} Q(8) { ! alpha2( X, Y, Y ) }.
% 0.51/1.02 parent1[0]: (5) {G0,W8,D3,L2,V2,M2} I { alpha2( X, skol2( X ), Y ), r2( X,
% 0.51/1.02 Y ) }.
% 0.51/1.02 substitution0:
% 0.51/1.02 X := X
% 0.51/1.02 Y := skol2( X )
% 0.51/1.02 end
% 0.51/1.02 substitution1:
% 0.51/1.02 X := X
% 0.51/1.02 Y := skol2( X )
% 0.51/1.02 end
% 0.51/1.02
% 0.51/1.02 subsumption: (87) {G2,W4,D3,L1,V1,M1} R(5,51) { r2( X, skol2( X ) ) }.
% 0.51/1.02 parent0: (2427) {G1,W4,D3,L1,V1,M1} { r2( X, skol2( X ) ) }.
% 0.51/1.02 substitution0:
% 0.51/1.02 X := X
% 0.51/1.02 end
% 0.51/1.02 permutation0:
% 0.51/1.02 0 ==> 0
% 0.51/1.02 end
% 0.51/1.02
% 0.51/1.02 resolution: (2428) {G2,W3,D3,L1,V1,M1} { ! r1( skol2( X ) ) }.
% 0.51/1.02 parent0[1]: (56) {G1,W5,D2,L2,V2,M2} Q(43) { ! r1( X ), ! r2( Y, X ) }.
% 0.51/1.02 parent1[0]: (87) {G2,W4,D3,L1,V1,M1} R(5,51) { r2( X, skol2( X ) ) }.
% 0.51/1.02 substitution0:
% 0.51/1.02 X := skol2( X )
% 0.51/1.02 Y := X
% 0.51/1.02 end
% 0.51/1.02 substitution1:
% 0.51/1.02 X := X
% 0.51/1.02 end
% 0.51/1.02
% 0.51/1.02 subsumption: (88) {G3,W3,D3,L1,V1,M1} R(87,56) { ! r1( skol2( X ) ) }.
% 0.51/1.02 parent0: (2428) {G2,W3,D3,L1,V1,M1} { ! r1( skol2( X ) ) }.
% 0.51/1.02 substitution0:
% 0.51/1.02 X := X
% 0.51/1.02 end
% 0.51/1.02 permutation0:
% 0.51/1.02 0 ==> 0
% 0.51/1.02 end
% 0.51/1.02
% 0.51/1.02 *** allocated 50625 inteCputime limit exceeded (core dumped)
%------------------------------------------------------------------------------