%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SYN550+1 : TPTP v8.1.0. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n016.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 : Thu Jul 21 02:52:53 EDT 2022
% Result : Theorem 0.89s 1.28s
% Output : Refutation 0.89s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SYN550+1 : TPTP v8.1.0. Released v2.2.0.
% 0.07/0.13 % Command : bliksem %s
% 0.14/0.33 % Computer : n016.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % DateTime : Tue Jul 12 04:16:28 EDT 2022
% 0.14/0.33 % CPUTime :
% 0.89/1.27 *** allocated 10000 integers for termspace/termends
% 0.89/1.27 *** allocated 10000 integers for clauses
% 0.89/1.27 *** allocated 10000 integers for justifications
% 0.89/1.27 Bliksem 1.12
% 0.89/1.27
% 0.89/1.27
% 0.89/1.27 Automatic Strategy Selection
% 0.89/1.27
% 0.89/1.27
% 0.89/1.27 Clauses:
% 0.89/1.27
% 0.89/1.27 { reachable( X, X ) }.
% 0.89/1.27 { ! reachable( X, Z ), ! reachable( Z, Y ), reachable( X, Y ) }.
% 0.89/1.27 { alpha6, reachable( initial_world, skol1 ) }.
% 0.89/1.27 { alpha6, alpha2( skol1 ) }.
% 0.89/1.27 { alpha6, ! alpha1 }.
% 0.89/1.27 { ! alpha6, alpha1 }.
% 0.89/1.27 { ! alpha6, ! reachable( initial_world, X ), ! alpha2( X ) }.
% 0.89/1.27 { ! alpha1, reachable( initial_world, skol2 ), alpha6 }.
% 0.89/1.27 { ! alpha1, alpha2( skol2 ), alpha6 }.
% 0.89/1.27 { ! alpha2( X ), ! reachable( X, Y ), alpha4( Y ) }.
% 0.89/1.27 { ! alpha4( skol3( Y ) ), alpha2( X ) }.
% 0.89/1.27 { reachable( X, skol3( X ) ), alpha2( X ) }.
% 0.89/1.27 { ! alpha4( X ), alpha5( skol4( Y ) ) }.
% 0.89/1.27 { ! alpha4( X ), reachable( X, skol4( X ) ) }.
% 0.89/1.27 { ! reachable( X, Y ), ! alpha5( Y ), alpha4( X ) }.
% 0.89/1.27 { ! alpha5( X ), ! reachable( X, Y ), p( Y ) }.
% 0.89/1.27 { ! p( skol5( Y ) ), alpha5( X ) }.
% 0.89/1.27 { reachable( X, skol5( X ) ), alpha5( X ) }.
% 0.89/1.27 { ! alpha1, reachable( initial_world, skol6 ) }.
% 0.89/1.27 { ! alpha1, alpha3( skol6 ) }.
% 0.89/1.27 { ! reachable( initial_world, X ), ! alpha3( X ), alpha1 }.
% 0.89/1.27 { ! alpha3( X ), ! reachable( X, Y ), p( Y ) }.
% 0.89/1.27 { ! p( skol7( Y ) ), alpha3( X ) }.
% 0.89/1.27 { reachable( X, skol7( X ) ), alpha3( X ) }.
% 0.89/1.27
% 0.89/1.27 percentage equality = 0.000000, percentage horn = 0.772727
% 0.89/1.27 This a non-horn, non-equality problem
% 0.89/1.27
% 0.89/1.27
% 0.89/1.27 Options Used:
% 0.89/1.27
% 0.89/1.27 useres = 1
% 0.89/1.27 useparamod = 0
% 0.89/1.27 useeqrefl = 0
% 0.89/1.27 useeqfact = 0
% 0.89/1.27 usefactor = 1
% 0.89/1.27 usesimpsplitting = 0
% 0.89/1.27 usesimpdemod = 0
% 0.89/1.27 usesimpres = 3
% 0.89/1.27
% 0.89/1.27 resimpinuse = 1000
% 0.89/1.27 resimpclauses = 20000
% 0.89/1.27 substype = standard
% 0.89/1.27 backwardsubs = 1
% 0.89/1.27 selectoldest = 5
% 0.89/1.27
% 0.89/1.27 litorderings [0] = split
% 0.89/1.27 litorderings [1] = liftord
% 0.89/1.27
% 0.89/1.27 termordering = none
% 0.89/1.27
% 0.89/1.27 litapriori = 1
% 0.89/1.27 termapriori = 0
% 0.89/1.27 litaposteriori = 0
% 0.89/1.27 termaposteriori = 0
% 0.89/1.27 demodaposteriori = 0
% 0.89/1.27 ordereqreflfact = 0
% 0.89/1.27
% 0.89/1.27 litselect = none
% 0.89/1.27
% 0.89/1.27 maxweight = 15
% 0.89/1.27 maxdepth = 30000
% 0.89/1.27 maxlength = 115
% 0.89/1.27 maxnrvars = 195
% 0.89/1.27 excuselevel = 1
% 0.89/1.27 increasemaxweight = 1
% 0.89/1.27
% 0.89/1.27 maxselected = 10000000
% 0.89/1.27 maxnrclauses = 10000000
% 0.89/1.27
% 0.89/1.27 showgenerated = 0
% 0.89/1.27 showkept = 0
% 0.89/1.27 showselected = 0
% 0.89/1.27 showdeleted = 0
% 0.89/1.27 showresimp = 1
% 0.89/1.27 showstatus = 2000
% 0.89/1.27
% 0.89/1.27 prologoutput = 0
% 0.89/1.27 nrgoals = 5000000
% 0.89/1.27 totalproof = 1
% 0.89/1.27
% 0.89/1.27 Symbols occurring in the translation:
% 0.89/1.27
% 0.89/1.27 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.89/1.27 . [1, 2] (w:1, o:30, a:1, s:1, b:0),
% 0.89/1.27 ! [4, 1] (w:0, o:16, a:1, s:1, b:0),
% 0.89/1.27 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.89/1.27 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.89/1.27 reachable [36, 2] (w:1, o:54, a:1, s:1, b:0),
% 0.89/1.27 initial_world [39, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.89/1.27 p [40, 1] (w:1, o:21, a:1, s:1, b:0),
% 0.89/1.27 alpha1 [42, 0] (w:1, o:11, a:1, s:1, b:0),
% 0.89/1.27 alpha2 [43, 1] (w:1, o:22, a:1, s:1, b:0),
% 0.89/1.27 alpha3 [44, 1] (w:1, o:23, a:1, s:1, b:0),
% 0.89/1.27 alpha4 [45, 1] (w:1, o:24, a:1, s:1, b:0),
% 0.89/1.27 alpha5 [46, 1] (w:1, o:25, a:1, s:1, b:0),
% 0.89/1.27 alpha6 [47, 0] (w:1, o:12, a:1, s:1, b:0),
% 0.89/1.27 skol1 [48, 0] (w:1, o:13, a:1, s:1, b:0),
% 0.89/1.27 skol2 [49, 0] (w:1, o:14, a:1, s:1, b:0),
% 0.89/1.28 skol3 [50, 1] (w:1, o:26, a:1, s:1, b:0),
% 0.89/1.28 skol4 [51, 1] (w:1, o:27, a:1, s:1, b:0),
% 0.89/1.28 skol5 [52, 1] (w:1, o:28, a:1, s:1, b:0),
% 0.89/1.28 skol6 [53, 0] (w:1, o:15, a:1, s:1, b:0),
% 0.89/1.28 skol7 [54, 1] (w:1, o:29, a:1, s:1, b:0).
% 0.89/1.28
% 0.89/1.28
% 0.89/1.28 Starting Search:
% 0.89/1.28
% 0.89/1.28 *** allocated 15000 integers for clauses
% 0.89/1.28 *** allocated 22500 integers for clauses
% 0.89/1.28 *** allocated 33750 integers for clauses
% 0.89/1.28 *** allocated 15000 integers for termspace/termends
% 0.89/1.28 *** allocated 50625 integers for clauses
% 0.89/1.28 Resimplifying inuse:
% 0.89/1.28 Done
% 0.89/1.28
% 0.89/1.28 *** allocated 22500 integers for termspace/termends
% 0.89/1.28 *** allocated 75937 integers for clauses
% 0.89/1.28 *** allocated 33750 integers for termspace/termends
% 0.89/1.28
% 0.89/1.28 Intermediate Status:
% 0.89/1.28 Generated: 7956
% 0.89/1.28 Kept: 2009
% 0.89/1.28 Inuse: 256
% 0.89/1.28 Deleted: 63
% 0.89/1.28 Deletedinuse: 18
% 0.89/1.28
% 0.89/1.28 *** allocated 113905 integers for clauses
% 0.89/1.28 Resimplifying inuse:
% 0.89/1.28 Done
% 0.89/1.28
% 0.89/1.28 *** allocated 50625 integers for termspace/termends
% 0.89/1.28 Resimplifying inuse:
% 0.89/1.28 Done
% 0.89/1.28
% 0.89/1.28 *** allocated 170857 integers for clauses
% 0.89/1.28 *** allocated 75937 integers for termspace/termends
% 0.89/1.28
% 0.89/1.28 Intermediate Status:
% 0.89/1.28 Generated: 17838
% 0.89/1.28 Kept: 4015
% 0.89/1.28 Inuse: 439
% 0.89/1.28 Deleted: 149
% 0.89/1.28 Deletedinuse: 48
% 0.89/1.28
% 0.89/1.28 Resimplifying inuse:
% 0.89/1.28 Done
% 0.89/1.28
% 0.89/1.28
% 0.89/1.28 Bliksems!, er is een bewijs:
% 0.89/1.28 % SZS status Theorem
% 0.89/1.28 % SZS output start Refutation
% 0.89/1.28
% 0.89/1.28 (0) {G0,W3,D2,L1,V1,M1} I { reachable( X, X ) }.
% 0.89/1.28 (1) {G0,W9,D2,L3,V3,M3} I { ! reachable( Z, Y ), reachable( X, Y ), !
% 0.89/1.28 reachable( X, Z ) }.
% 0.89/1.28 (2) {G0,W4,D2,L2,V0,M1} I { alpha6, reachable( initial_world, skol1 ) }.
% 0.89/1.28 (3) {G0,W3,D2,L2,V0,M1} I { alpha6, alpha2( skol1 ) }.
% 0.89/1.28 (4) {G0,W2,D1,L2,V0,M1} I { alpha6, ! alpha1 }.
% 0.89/1.28 (5) {G0,W2,D1,L2,V0,M1} I { alpha1, ! alpha6 }.
% 0.89/1.28 (6) {G0,W6,D2,L3,V1,M1} I { ! reachable( initial_world, X ), ! alpha2( X )
% 0.89/1.28 , ! alpha6 }.
% 0.89/1.28 (7) {G0,W7,D2,L3,V2,M1} I { ! alpha2( X ), alpha4( Y ), ! reachable( X, Y )
% 0.89/1.28 }.
% 0.89/1.28 (8) {G0,W5,D3,L2,V2,M1} I { alpha2( X ), ! alpha4( skol3( Y ) ) }.
% 0.89/1.28 (9) {G0,W6,D3,L2,V1,M1} I { alpha2( X ), reachable( X, skol3( X ) ) }.
% 0.89/1.28 (10) {G0,W5,D3,L2,V2,M1} I { ! alpha4( X ), alpha5( skol4( Y ) ) }.
% 0.89/1.28 (11) {G0,W6,D3,L2,V1,M1} I { ! alpha4( X ), reachable( X, skol4( X ) ) }.
% 0.89/1.28 (12) {G0,W7,D2,L3,V2,M1} I { ! alpha5( Y ), alpha4( X ), ! reachable( X, Y
% 0.89/1.28 ) }.
% 0.89/1.28 (13) {G0,W7,D2,L3,V2,M1} I { ! alpha5( X ), p( Y ), ! reachable( X, Y ) }.
% 0.89/1.28 (14) {G0,W5,D3,L2,V2,M1} I { ! p( skol5( Y ) ), alpha5( X ) }.
% 0.89/1.28 (15) {G0,W6,D3,L2,V1,M1} I { alpha5( X ), reachable( X, skol5( X ) ) }.
% 0.89/1.28 (16) {G0,W4,D2,L2,V0,M1} I { reachable( initial_world, skol6 ), ! alpha1
% 0.89/1.28 }.
% 0.89/1.28 (17) {G0,W3,D2,L2,V0,M1} I { alpha3( skol6 ), ! alpha1 }.
% 0.89/1.28 (18) {G0,W6,D2,L3,V1,M1} I { ! alpha3( X ), alpha1, ! reachable(
% 0.89/1.28 initial_world, X ) }.
% 0.89/1.28 (19) {G0,W7,D2,L3,V2,M1} I { ! alpha3( X ), p( Y ), ! reachable( X, Y ) }.
% 0.89/1.28 (20) {G0,W5,D3,L2,V2,M1} I { ! p( skol7( Y ) ), alpha3( X ) }.
% 0.89/1.28 (21) {G0,W6,D3,L2,V1,M1} I { alpha3( X ), reachable( X, skol7( X ) ) }.
% 0.89/1.28 (24) {G1,W7,D2,L3,V1,M1} R(2,1) { alpha6, reachable( initial_world, X ), !
% 0.89/1.28 reachable( skol1, X ) }.
% 0.89/1.28 (25) {G1,W3,D2,L2,V0,M1} R(18,2);r(4) { alpha6, ! alpha3( skol1 ) }.
% 0.89/1.28 (26) {G1,W9,D2,L4,V2,M2} R(18,1) { alpha1, ! alpha3( X ), ! reachable(
% 0.89/1.28 initial_world, Y ), ! reachable( Y, X ) }.
% 0.89/1.28 (28) {G2,W4,D3,L2,V1,M1} R(25,20) { alpha6, ! p( skol7( X ) ) }.
% 0.89/1.28 (31) {G1,W4,D2,L2,V1,M1} R(7,0) { ! alpha2( X ), alpha4( X ) }.
% 0.89/1.28 (36) {G1,W9,D3,L3,V2,M2} R(9,1) { alpha2( X ), reachable( X, Y ), !
% 0.89/1.28 reachable( skol3( X ), Y ) }.
% 0.89/1.28 (42) {G1,W6,D3,L3,V0,M1} R(11,18) { ! alpha3( skol4( initial_world ) ),
% 0.89/1.28 alpha1, ! alpha4( initial_world ) }.
% 0.89/1.28 (44) {G1,W9,D3,L3,V2,M2} R(11,1) { ! alpha4( X ), reachable( X, Y ), !
% 0.89/1.28 reachable( skol4( X ), Y ) }.
% 0.89/1.28 (55) {G1,W4,D2,L2,V1,M1} R(12,0) { alpha4( X ), ! alpha5( X ) }.
% 0.89/1.28 (57) {G2,W5,D3,L2,V2,M2} R(55,10) { ! alpha4( Y ), alpha4( skol4( X ) ) }.
% 0.89/1.28 (58) {G2,W5,D3,L2,V2,M1} R(55,14) { ! p( skol5( Y ) ), alpha4( X ) }.
% 0.89/1.28 (61) {G1,W7,D3,L3,V1,M1} R(13,21) { p( skol7( X ) ), alpha3( X ), ! alpha5
% 0.89/1.28 ( X ) }.
% 0.89/1.28 (72) {G1,W7,D3,L3,V1,M1} R(19,15) { p( skol5( X ) ), ! alpha3( X ), alpha5
% 0.89/1.28 ( X ) }.
% 0.89/1.28 (101) {G3,W5,D3,L2,V2,M1} R(58,8) { ! p( skol5( X ) ), alpha2( Y ) }.
% 0.89/1.28 (114) {G2,W7,D3,L3,V0,M1} R(24,11) { alpha6, ! alpha4( skol1 ), reachable(
% 0.89/1.28 initial_world, skol4( skol1 ) ) }.
% 0.89/1.28 (139) {G2,W6,D2,L3,V1,M1} R(26,2);r(4) { ! alpha3( X ), alpha6, ! reachable
% 0.89/1.28 ( skol1, X ) }.
% 0.89/1.28 (191) {G2,W10,D3,L4,V2,M1} R(36,13) { alpha2( X ), ! alpha5( X ), p( Y ), !
% 0.89/1.28 reachable( skol3( X ), Y ) }.
% 0.89/1.28 (283) {G2,W9,D4,L3,V2,M1} R(61,10) { p( skol7( skol4( X ) ) ), alpha3(
% 0.89/1.28 skol4( X ) ), ! alpha4( Y ) }.
% 0.89/1.28 (324) {G3,W9,D3,L4,V1,M1} R(44,139) { ! alpha4( skol1 ), ! alpha3( X ),
% 0.89/1.28 alpha6, ! reachable( skol4( skol1 ), X ) }.
% 0.89/1.28 (502) {G3,W8,D3,L4,V0,M1} R(114,12) { alpha6, ! alpha4( skol1 ), alpha4(
% 0.89/1.28 initial_world ), ! alpha5( skol4( skol1 ) ) }.
% 0.89/1.28 (1681) {G4,W7,D2,L4,V1,M2} R(502,10) { alpha6, alpha4( initial_world ), !
% 0.89/1.28 alpha4( X ), ! alpha4( skol1 ) }.
% 0.89/1.28 (1682) {G5,W5,D2,L3,V0,M1} F(1681) { alpha6, alpha4( initial_world ), !
% 0.89/1.28 alpha4( skol1 ) }.
% 0.89/1.28 (1683) {G6,W3,D2,L2,V0,M1} R(1682,31);r(3) { alpha6, alpha4( initial_world
% 0.89/1.28 ) }.
% 0.89/1.28 (1685) {G7,W4,D3,L2,V1,M1} R(1683,57) { alpha6, alpha4( skol4( X ) ) }.
% 0.89/1.28 (1686) {G7,W4,D3,L2,V0,M1} R(1683,42);r(5) { alpha1, ! alpha3( skol4(
% 0.89/1.28 initial_world ) ) }.
% 0.89/1.28 (3098) {G8,W7,D4,L3,V0,M1} R(324,11);r(1685) { ! alpha3( skol4( skol4(
% 0.89/1.28 skol1 ) ) ), alpha6, ! alpha4( skol1 ) }.
% 0.89/1.28 (3102) {G9,W5,D4,L2,V0,M1} R(3098,31);r(3) { alpha6, ! alpha3( skol4( skol4
% 0.89/1.28 ( skol1 ) ) ) }.
% 0.89/1.28 (3325) {G8,W4,D3,L2,V1,M1} R(283,1685);r(28) { alpha6, alpha3( skol4( X ) )
% 0.89/1.28 }.
% 0.89/1.28 (3330) {G10,W1,D1,L1,V0,M1} R(3325,3102);f { alpha6 }.
% 0.89/1.28 (3335) {G9,W1,D1,L1,V0,M1} R(3325,1686);r(5) { alpha1 }.
% 0.89/1.28 (3336) {G11,W5,D2,L2,V1,M1} R(3330,6) { ! alpha2( X ), ! reachable(
% 0.89/1.28 initial_world, X ) }.
% 0.89/1.28 (3351) {G10,W3,D2,L1,V0,M1} R(3335,16) { reachable( initial_world, skol6 )
% 0.89/1.28 }.
% 0.89/1.28 (3352) {G10,W2,D2,L1,V0,M1} R(3335,17) { alpha3( skol6 ) }.
% 0.89/1.28 (3434) {G12,W2,D2,L1,V0,M1} R(3336,3351) { ! alpha2( skol6 ) }.
% 0.89/1.28 (3464) {G13,W3,D3,L1,V1,M1} R(3434,101) { ! p( skol5( X ) ) }.
% 0.89/1.28 (3713) {G14,W7,D3,L3,V1,M2} R(191,15);r(3464) { alpha2( X ), alpha5( skol3
% 0.89/1.28 ( X ) ), ! alpha5( X ) }.
% 0.89/1.28 (4053) {G14,W4,D2,L2,V1,M1} S(72);r(3464) { ! alpha3( X ), alpha5( X ) }.
% 0.89/1.28 (4355) {G15,W7,D3,L3,V1,M1} R(3713,55) { alpha2( X ), alpha4( skol3( X ) )
% 0.89/1.28 , ! alpha5( X ) }.
% 0.89/1.28 (4451) {G16,W7,D3,L3,V1,M1} R(4355,4053) { alpha2( X ), ! alpha3( X ),
% 0.89/1.28 alpha4( skol3( X ) ) }.
% 0.89/1.28 (4453) {G17,W6,D2,L3,V2,M1} R(4451,8) { alpha2( X ), alpha2( Y ), ! alpha3
% 0.89/1.28 ( X ) }.
% 0.89/1.28 (4454) {G18,W4,D2,L2,V1,M1} F(4453) { alpha2( X ), ! alpha3( X ) }.
% 0.89/1.28 (4457) {G19,W0,D0,L0,V0,M0} R(4454,3352);r(3434) { }.
% 0.89/1.28
% 0.89/1.28
% 0.89/1.28 % SZS output end Refutation
% 0.89/1.28 found a proof!
% 0.89/1.28
% 0.89/1.28
% 0.89/1.28 Unprocessed initial clauses:
% 0.89/1.28
% 0.89/1.28 (4459) {G0,W3,D2,L1,V1,M1} { reachable( X, X ) }.
% 0.89/1.28 (4460) {G0,W9,D2,L3,V3,M3} { ! reachable( X, Z ), ! reachable( Z, Y ),
% 0.89/1.28 reachable( X, Y ) }.
% 0.89/1.28 (4461) {G0,W4,D2,L2,V0,M2} { alpha6, reachable( initial_world, skol1 ) }.
% 0.89/1.28 (4462) {G0,W3,D2,L2,V0,M2} { alpha6, alpha2( skol1 ) }.
% 0.89/1.28 (4463) {G0,W2,D1,L2,V0,M2} { alpha6, ! alpha1 }.
% 0.89/1.28 (4464) {G0,W2,D1,L2,V0,M2} { ! alpha6, alpha1 }.
% 0.89/1.28 (4465) {G0,W6,D2,L3,V1,M3} { ! alpha6, ! reachable( initial_world, X ), !
% 0.89/1.28 alpha2( X ) }.
% 0.89/1.28 (4466) {G0,W5,D2,L3,V0,M3} { ! alpha1, reachable( initial_world, skol2 ),
% 0.89/1.28 alpha6 }.
% 0.89/1.28 (4467) {G0,W4,D2,L3,V0,M3} { ! alpha1, alpha2( skol2 ), alpha6 }.
% 0.89/1.28 (4468) {G0,W7,D2,L3,V2,M3} { ! alpha2( X ), ! reachable( X, Y ), alpha4( Y
% 0.89/1.28 ) }.
% 0.89/1.28 (4469) {G0,W5,D3,L2,V2,M2} { ! alpha4( skol3( Y ) ), alpha2( X ) }.
% 0.89/1.28 (4470) {G0,W6,D3,L2,V1,M2} { reachable( X, skol3( X ) ), alpha2( X ) }.
% 0.89/1.28 (4471) {G0,W5,D3,L2,V2,M2} { ! alpha4( X ), alpha5( skol4( Y ) ) }.
% 0.89/1.28 (4472) {G0,W6,D3,L2,V1,M2} { ! alpha4( X ), reachable( X, skol4( X ) ) }.
% 0.89/1.28 (4473) {G0,W7,D2,L3,V2,M3} { ! reachable( X, Y ), ! alpha5( Y ), alpha4( X
% 0.89/1.28 ) }.
% 0.89/1.28 (4474) {G0,W7,D2,L3,V2,M3} { ! alpha5( X ), ! reachable( X, Y ), p( Y )
% 0.89/1.28 }.
% 0.89/1.28 (4475) {G0,W5,D3,L2,V2,M2} { ! p( skol5( Y ) ), alpha5( X ) }.
% 0.89/1.28 (4476) {G0,W6,D3,L2,V1,M2} { reachable( X, skol5( X ) ), alpha5( X ) }.
% 0.89/1.28 (4477) {G0,W4,D2,L2,V0,M2} { ! alpha1, reachable( initial_world, skol6 )
% 0.89/1.28 }.
% 0.89/1.28 (4478) {G0,W3,D2,L2,V0,M2} { ! alpha1, alpha3( skol6 ) }.
% 0.89/1.28 (4479) {G0,W6,D2,L3,V1,M3} { ! reachable( initial_world, X ), ! alpha3( X
% 0.89/1.28 ), alpha1 }.
% 0.89/1.28 (4480) {G0,W7,D2,L3,V2,M3} { ! alpha3( X ), ! reachable( X, Y ), p( Y )
% 0.89/1.28 }.
% 0.89/1.28 (4481) {G0,W5,D3,L2,V2,M2} { ! p( skol7( Y ) ), alpha3( X ) }.
% 0.89/1.28 (4482) {G0,W6,D3,L2,V1,M2} { reachable( X, skol7( X ) ), alpha3( X ) }.
% 0.89/1.28
% 0.89/1.28
% 0.89/1.28 Total Proof:
% 0.89/1.28
% 0.89/1.28 subsumption: (0) {G0,W3,D2,L1,V1,M1} I { reachable( X, X ) }.
% 0.89/1.28 parent0: (4459) {G0,W3,D2,L1,V1,M1} { reachable( X, X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (1) {G0,W9,D2,L3,V3,M3} I { ! reachable( Z, Y ), reachable( X
% 0.89/1.28 , Y ), ! reachable( X, Z ) }.
% 0.89/1.28 parent0: (4460) {G0,W9,D2,L3,V3,M3} { ! reachable( X, Z ), ! reachable( Z
% 0.89/1.28 , Y ), reachable( X, Y ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := Y
% 0.89/1.28 Z := Z
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 2
% 0.89/1.28 1 ==> 0
% 0.89/1.28 2 ==> 1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (2) {G0,W4,D2,L2,V0,M1} I { alpha6, reachable( initial_world,
% 0.89/1.28 skol1 ) }.
% 0.89/1.28 parent0: (4461) {G0,W4,D2,L2,V0,M2} { alpha6, reachable( initial_world,
% 0.89/1.28 skol1 ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 1 ==> 1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (3) {G0,W3,D2,L2,V0,M1} I { alpha6, alpha2( skol1 ) }.
% 0.89/1.28 parent0: (4462) {G0,W3,D2,L2,V0,M2} { alpha6, alpha2( skol1 ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 1 ==> 1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (4) {G0,W2,D1,L2,V0,M1} I { alpha6, ! alpha1 }.
% 0.89/1.28 parent0: (4463) {G0,W2,D1,L2,V0,M2} { alpha6, ! alpha1 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 1 ==> 1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (5) {G0,W2,D1,L2,V0,M1} I { alpha1, ! alpha6 }.
% 0.89/1.28 parent0: (4464) {G0,W2,D1,L2,V0,M2} { ! alpha6, alpha1 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 1
% 0.89/1.28 1 ==> 0
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (6) {G0,W6,D2,L3,V1,M1} I { ! reachable( initial_world, X ), !
% 0.89/1.28 alpha2( X ), ! alpha6 }.
% 0.89/1.28 parent0: (4465) {G0,W6,D2,L3,V1,M3} { ! alpha6, ! reachable( initial_world
% 0.89/1.28 , X ), ! alpha2( X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 2
% 0.89/1.28 1 ==> 0
% 0.89/1.28 2 ==> 1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (7) {G0,W7,D2,L3,V2,M1} I { ! alpha2( X ), alpha4( Y ), !
% 0.89/1.28 reachable( X, Y ) }.
% 0.89/1.28 parent0: (4468) {G0,W7,D2,L3,V2,M3} { ! alpha2( X ), ! reachable( X, Y ),
% 0.89/1.28 alpha4( Y ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := Y
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 1 ==> 2
% 0.89/1.28 2 ==> 1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (8) {G0,W5,D3,L2,V2,M1} I { alpha2( X ), ! alpha4( skol3( Y )
% 0.89/1.28 ) }.
% 0.89/1.28 parent0: (4469) {G0,W5,D3,L2,V2,M2} { ! alpha4( skol3( Y ) ), alpha2( X )
% 0.89/1.28 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := Y
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 1
% 0.89/1.28 1 ==> 0
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (9) {G0,W6,D3,L2,V1,M1} I { alpha2( X ), reachable( X, skol3(
% 0.89/1.28 X ) ) }.
% 0.89/1.28 parent0: (4470) {G0,W6,D3,L2,V1,M2} { reachable( X, skol3( X ) ), alpha2(
% 0.89/1.28 X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 1
% 0.89/1.28 1 ==> 0
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (10) {G0,W5,D3,L2,V2,M1} I { ! alpha4( X ), alpha5( skol4( Y )
% 0.89/1.28 ) }.
% 0.89/1.28 parent0: (4471) {G0,W5,D3,L2,V2,M2} { ! alpha4( X ), alpha5( skol4( Y ) )
% 0.89/1.28 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := Y
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 1 ==> 1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (11) {G0,W6,D3,L2,V1,M1} I { ! alpha4( X ), reachable( X,
% 0.89/1.28 skol4( X ) ) }.
% 0.89/1.28 parent0: (4472) {G0,W6,D3,L2,V1,M2} { ! alpha4( X ), reachable( X, skol4(
% 0.89/1.28 X ) ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 1 ==> 1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (12) {G0,W7,D2,L3,V2,M1} I { ! alpha5( Y ), alpha4( X ), !
% 0.89/1.28 reachable( X, Y ) }.
% 0.89/1.28 parent0: (4473) {G0,W7,D2,L3,V2,M3} { ! reachable( X, Y ), ! alpha5( Y ),
% 0.89/1.28 alpha4( X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := Y
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 2
% 0.89/1.28 1 ==> 0
% 0.89/1.28 2 ==> 1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (13) {G0,W7,D2,L3,V2,M1} I { ! alpha5( X ), p( Y ), !
% 0.89/1.28 reachable( X, Y ) }.
% 0.89/1.28 parent0: (4474) {G0,W7,D2,L3,V2,M3} { ! alpha5( X ), ! reachable( X, Y ),
% 0.89/1.28 p( Y ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := Y
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 1 ==> 2
% 0.89/1.28 2 ==> 1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (14) {G0,W5,D3,L2,V2,M1} I { ! p( skol5( Y ) ), alpha5( X )
% 0.89/1.28 }.
% 0.89/1.28 parent0: (4475) {G0,W5,D3,L2,V2,M2} { ! p( skol5( Y ) ), alpha5( X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := Y
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 1 ==> 1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (15) {G0,W6,D3,L2,V1,M1} I { alpha5( X ), reachable( X, skol5
% 0.89/1.28 ( X ) ) }.
% 0.89/1.28 parent0: (4476) {G0,W6,D3,L2,V1,M2} { reachable( X, skol5( X ) ), alpha5(
% 0.89/1.28 X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 1
% 0.89/1.28 1 ==> 0
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (16) {G0,W4,D2,L2,V0,M1} I { reachable( initial_world, skol6 )
% 0.89/1.28 , ! alpha1 }.
% 0.89/1.28 parent0: (4477) {G0,W4,D2,L2,V0,M2} { ! alpha1, reachable( initial_world,
% 0.89/1.28 skol6 ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 1
% 0.89/1.28 1 ==> 0
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (17) {G0,W3,D2,L2,V0,M1} I { alpha3( skol6 ), ! alpha1 }.
% 0.89/1.28 parent0: (4478) {G0,W3,D2,L2,V0,M2} { ! alpha1, alpha3( skol6 ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 1
% 0.89/1.28 1 ==> 0
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (18) {G0,W6,D2,L3,V1,M1} I { ! alpha3( X ), alpha1, !
% 0.89/1.28 reachable( initial_world, X ) }.
% 0.89/1.28 parent0: (4479) {G0,W6,D2,L3,V1,M3} { ! reachable( initial_world, X ), !
% 0.89/1.28 alpha3( X ), alpha1 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 2
% 0.89/1.28 1 ==> 0
% 0.89/1.28 2 ==> 1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (19) {G0,W7,D2,L3,V2,M1} I { ! alpha3( X ), p( Y ), !
% 0.89/1.28 reachable( X, Y ) }.
% 0.89/1.28 parent0: (4480) {G0,W7,D2,L3,V2,M3} { ! alpha3( X ), ! reachable( X, Y ),
% 0.89/1.28 p( Y ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := Y
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 1 ==> 2
% 0.89/1.28 2 ==> 1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (20) {G0,W5,D3,L2,V2,M1} I { ! p( skol7( Y ) ), alpha3( X )
% 0.89/1.28 }.
% 0.89/1.28 parent0: (4481) {G0,W5,D3,L2,V2,M2} { ! p( skol7( Y ) ), alpha3( X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := Y
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 1 ==> 1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (21) {G0,W6,D3,L2,V1,M1} I { alpha3( X ), reachable( X, skol7
% 0.89/1.28 ( X ) ) }.
% 0.89/1.28 parent0: (4482) {G0,W6,D3,L2,V1,M2} { reachable( X, skol7( X ) ), alpha3(
% 0.89/1.28 X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 1
% 0.89/1.28 1 ==> 0
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4505) {G1,W7,D2,L3,V1,M3} { ! reachable( skol1, X ),
% 0.89/1.28 reachable( initial_world, X ), alpha6 }.
% 0.89/1.28 parent0[2]: (1) {G0,W9,D2,L3,V3,M3} I { ! reachable( Z, Y ), reachable( X,
% 0.89/1.28 Y ), ! reachable( X, Z ) }.
% 0.89/1.28 parent1[1]: (2) {G0,W4,D2,L2,V0,M1} I { alpha6, reachable( initial_world,
% 0.89/1.28 skol1 ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := initial_world
% 0.89/1.28 Y := X
% 0.89/1.28 Z := skol1
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (24) {G1,W7,D2,L3,V1,M1} R(2,1) { alpha6, reachable(
% 0.89/1.28 initial_world, X ), ! reachable( skol1, X ) }.
% 0.89/1.28 parent0: (4505) {G1,W7,D2,L3,V1,M3} { ! reachable( skol1, X ), reachable(
% 0.89/1.28 initial_world, X ), alpha6 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 2
% 0.89/1.28 1 ==> 1
% 0.89/1.28 2 ==> 0
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4506) {G1,W4,D2,L3,V0,M3} { ! alpha3( skol1 ), alpha1, alpha6
% 0.89/1.28 }.
% 0.89/1.28 parent0[2]: (18) {G0,W6,D2,L3,V1,M1} I { ! alpha3( X ), alpha1, ! reachable
% 0.89/1.28 ( initial_world, X ) }.
% 0.89/1.28 parent1[1]: (2) {G0,W4,D2,L2,V0,M1} I { alpha6, reachable( initial_world,
% 0.89/1.28 skol1 ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := skol1
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4507) {G1,W4,D2,L3,V0,M3} { alpha6, ! alpha3( skol1 ), alpha6
% 0.89/1.28 }.
% 0.89/1.28 parent0[1]: (4) {G0,W2,D1,L2,V0,M1} I { alpha6, ! alpha1 }.
% 0.89/1.28 parent1[1]: (4506) {G1,W4,D2,L3,V0,M3} { ! alpha3( skol1 ), alpha1, alpha6
% 0.89/1.28 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 factor: (4508) {G1,W3,D2,L2,V0,M2} { alpha6, ! alpha3( skol1 ) }.
% 0.89/1.28 parent0[0, 2]: (4507) {G1,W4,D2,L3,V0,M3} { alpha6, ! alpha3( skol1 ),
% 0.89/1.28 alpha6 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (25) {G1,W3,D2,L2,V0,M1} R(18,2);r(4) { alpha6, ! alpha3(
% 0.89/1.28 skol1 ) }.
% 0.89/1.28 parent0: (4508) {G1,W3,D2,L2,V0,M2} { alpha6, ! alpha3( skol1 ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 1 ==> 1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4509) {G1,W9,D2,L4,V2,M4} { ! alpha3( X ), alpha1, !
% 0.89/1.28 reachable( Y, X ), ! reachable( initial_world, Y ) }.
% 0.89/1.28 parent0[2]: (18) {G0,W6,D2,L3,V1,M1} I { ! alpha3( X ), alpha1, ! reachable
% 0.89/1.28 ( initial_world, X ) }.
% 0.89/1.28 parent1[1]: (1) {G0,W9,D2,L3,V3,M3} I { ! reachable( Z, Y ), reachable( X,
% 0.89/1.28 Y ), ! reachable( X, Z ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := initial_world
% 0.89/1.28 Y := X
% 0.89/1.28 Z := Y
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (26) {G1,W9,D2,L4,V2,M2} R(18,1) { alpha1, ! alpha3( X ), !
% 0.89/1.28 reachable( initial_world, Y ), ! reachable( Y, X ) }.
% 0.89/1.28 parent0: (4509) {G1,W9,D2,L4,V2,M4} { ! alpha3( X ), alpha1, ! reachable(
% 0.89/1.28 Y, X ), ! reachable( initial_world, Y ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := Y
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 1
% 0.89/1.28 1 ==> 0
% 0.89/1.28 2 ==> 3
% 0.89/1.28 3 ==> 2
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4511) {G1,W4,D3,L2,V1,M2} { alpha6, ! p( skol7( X ) ) }.
% 0.89/1.28 parent0[1]: (25) {G1,W3,D2,L2,V0,M1} R(18,2);r(4) { alpha6, ! alpha3( skol1
% 0.89/1.28 ) }.
% 0.89/1.28 parent1[1]: (20) {G0,W5,D3,L2,V2,M1} I { ! p( skol7( Y ) ), alpha3( X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := skol1
% 0.89/1.28 Y := X
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (28) {G2,W4,D3,L2,V1,M1} R(25,20) { alpha6, ! p( skol7( X ) )
% 0.89/1.28 }.
% 0.89/1.28 parent0: (4511) {G1,W4,D3,L2,V1,M2} { alpha6, ! p( skol7( X ) ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 1 ==> 1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4512) {G1,W4,D2,L2,V1,M2} { ! alpha2( X ), alpha4( X ) }.
% 0.89/1.28 parent0[2]: (7) {G0,W7,D2,L3,V2,M1} I { ! alpha2( X ), alpha4( Y ), !
% 0.89/1.28 reachable( X, Y ) }.
% 0.89/1.28 parent1[0]: (0) {G0,W3,D2,L1,V1,M1} I { reachable( X, X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := X
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (31) {G1,W4,D2,L2,V1,M1} R(7,0) { ! alpha2( X ), alpha4( X )
% 0.89/1.28 }.
% 0.89/1.28 parent0: (4512) {G1,W4,D2,L2,V1,M2} { ! alpha2( X ), alpha4( X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 1 ==> 1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4514) {G1,W9,D3,L3,V2,M3} { ! reachable( skol3( X ), Y ),
% 0.89/1.28 reachable( X, Y ), alpha2( X ) }.
% 0.89/1.28 parent0[2]: (1) {G0,W9,D2,L3,V3,M3} I { ! reachable( Z, Y ), reachable( X,
% 0.89/1.28 Y ), ! reachable( X, Z ) }.
% 0.89/1.28 parent1[1]: (9) {G0,W6,D3,L2,V1,M1} I { alpha2( X ), reachable( X, skol3( X
% 0.89/1.28 ) ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := Y
% 0.89/1.28 Z := skol3( X )
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (36) {G1,W9,D3,L3,V2,M2} R(9,1) { alpha2( X ), reachable( X, Y
% 0.89/1.28 ), ! reachable( skol3( X ), Y ) }.
% 0.89/1.28 parent0: (4514) {G1,W9,D3,L3,V2,M3} { ! reachable( skol3( X ), Y ),
% 0.89/1.28 reachable( X, Y ), alpha2( X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := Y
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 2
% 0.89/1.28 1 ==> 1
% 0.89/1.28 2 ==> 0
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4515) {G1,W6,D3,L3,V0,M3} { ! alpha3( skol4( initial_world )
% 0.89/1.28 ), alpha1, ! alpha4( initial_world ) }.
% 0.89/1.28 parent0[2]: (18) {G0,W6,D2,L3,V1,M1} I { ! alpha3( X ), alpha1, ! reachable
% 0.89/1.28 ( initial_world, X ) }.
% 0.89/1.28 parent1[1]: (11) {G0,W6,D3,L2,V1,M1} I { ! alpha4( X ), reachable( X, skol4
% 0.89/1.28 ( X ) ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := skol4( initial_world )
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := initial_world
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (42) {G1,W6,D3,L3,V0,M1} R(11,18) { ! alpha3( skol4(
% 0.89/1.28 initial_world ) ), alpha1, ! alpha4( initial_world ) }.
% 0.89/1.28 parent0: (4515) {G1,W6,D3,L3,V0,M3} { ! alpha3( skol4( initial_world ) ),
% 0.89/1.28 alpha1, ! alpha4( initial_world ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 1 ==> 1
% 0.89/1.28 2 ==> 2
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4517) {G1,W9,D3,L3,V2,M3} { ! reachable( skol4( X ), Y ),
% 0.89/1.28 reachable( X, Y ), ! alpha4( X ) }.
% 0.89/1.28 parent0[2]: (1) {G0,W9,D2,L3,V3,M3} I { ! reachable( Z, Y ), reachable( X,
% 0.89/1.28 Y ), ! reachable( X, Z ) }.
% 0.89/1.28 parent1[1]: (11) {G0,W6,D3,L2,V1,M1} I { ! alpha4( X ), reachable( X, skol4
% 0.89/1.28 ( X ) ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := Y
% 0.89/1.28 Z := skol4( X )
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (44) {G1,W9,D3,L3,V2,M2} R(11,1) { ! alpha4( X ), reachable( X
% 0.89/1.28 , Y ), ! reachable( skol4( X ), Y ) }.
% 0.89/1.28 parent0: (4517) {G1,W9,D3,L3,V2,M3} { ! reachable( skol4( X ), Y ),
% 0.89/1.28 reachable( X, Y ), ! alpha4( X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := Y
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 2
% 0.89/1.28 1 ==> 1
% 0.89/1.28 2 ==> 0
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4518) {G1,W4,D2,L2,V1,M2} { ! alpha5( X ), alpha4( X ) }.
% 0.89/1.28 parent0[2]: (12) {G0,W7,D2,L3,V2,M1} I { ! alpha5( Y ), alpha4( X ), !
% 0.89/1.28 reachable( X, Y ) }.
% 0.89/1.28 parent1[0]: (0) {G0,W3,D2,L1,V1,M1} I { reachable( X, X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := X
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (55) {G1,W4,D2,L2,V1,M1} R(12,0) { alpha4( X ), ! alpha5( X )
% 0.89/1.28 }.
% 0.89/1.28 parent0: (4518) {G1,W4,D2,L2,V1,M2} { ! alpha5( X ), alpha4( X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 1
% 0.89/1.28 1 ==> 0
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4519) {G1,W5,D3,L2,V2,M2} { alpha4( skol4( X ) ), ! alpha4( Y
% 0.89/1.28 ) }.
% 0.89/1.28 parent0[1]: (55) {G1,W4,D2,L2,V1,M1} R(12,0) { alpha4( X ), ! alpha5( X )
% 0.89/1.28 }.
% 0.89/1.28 parent1[1]: (10) {G0,W5,D3,L2,V2,M1} I { ! alpha4( X ), alpha5( skol4( Y )
% 0.89/1.28 ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := skol4( X )
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := Y
% 0.89/1.28 Y := X
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (57) {G2,W5,D3,L2,V2,M2} R(55,10) { ! alpha4( Y ), alpha4(
% 0.89/1.28 skol4( X ) ) }.
% 0.89/1.28 parent0: (4519) {G1,W5,D3,L2,V2,M2} { alpha4( skol4( X ) ), ! alpha4( Y )
% 0.89/1.28 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := Y
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 1
% 0.89/1.28 1 ==> 0
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4520) {G1,W5,D3,L2,V2,M2} { alpha4( X ), ! p( skol5( Y ) )
% 0.89/1.28 }.
% 0.89/1.28 parent0[1]: (55) {G1,W4,D2,L2,V1,M1} R(12,0) { alpha4( X ), ! alpha5( X )
% 0.89/1.28 }.
% 0.89/1.28 parent1[1]: (14) {G0,W5,D3,L2,V2,M1} I { ! p( skol5( Y ) ), alpha5( X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := X
% 0.89/1.28 Y := Y
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (58) {G2,W5,D3,L2,V2,M1} R(55,14) { ! p( skol5( Y ) ), alpha4
% 0.89/1.28 ( X ) }.
% 0.89/1.28 parent0: (4520) {G1,W5,D3,L2,V2,M2} { alpha4( X ), ! p( skol5( Y ) ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := Y
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 1
% 0.89/1.28 1 ==> 0
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4521) {G1,W7,D3,L3,V1,M3} { ! alpha5( X ), p( skol7( X ) ),
% 0.89/1.28 alpha3( X ) }.
% 0.89/1.28 parent0[2]: (13) {G0,W7,D2,L3,V2,M1} I { ! alpha5( X ), p( Y ), ! reachable
% 0.89/1.28 ( X, Y ) }.
% 0.89/1.28 parent1[1]: (21) {G0,W6,D3,L2,V1,M1} I { alpha3( X ), reachable( X, skol7(
% 0.89/1.28 X ) ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := skol7( X )
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (61) {G1,W7,D3,L3,V1,M1} R(13,21) { p( skol7( X ) ), alpha3( X
% 0.89/1.28 ), ! alpha5( X ) }.
% 0.89/1.28 parent0: (4521) {G1,W7,D3,L3,V1,M3} { ! alpha5( X ), p( skol7( X ) ),
% 0.89/1.28 alpha3( X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 2
% 0.89/1.28 1 ==> 0
% 0.89/1.28 2 ==> 1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4522) {G1,W7,D3,L3,V1,M3} { ! alpha3( X ), p( skol5( X ) ),
% 0.89/1.28 alpha5( X ) }.
% 0.89/1.28 parent0[2]: (19) {G0,W7,D2,L3,V2,M1} I { ! alpha3( X ), p( Y ), ! reachable
% 0.89/1.28 ( X, Y ) }.
% 0.89/1.28 parent1[1]: (15) {G0,W6,D3,L2,V1,M1} I { alpha5( X ), reachable( X, skol5(
% 0.89/1.28 X ) ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := skol5( X )
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (72) {G1,W7,D3,L3,V1,M1} R(19,15) { p( skol5( X ) ), ! alpha3
% 0.89/1.28 ( X ), alpha5( X ) }.
% 0.89/1.28 parent0: (4522) {G1,W7,D3,L3,V1,M3} { ! alpha3( X ), p( skol5( X ) ),
% 0.89/1.28 alpha5( X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 1
% 0.89/1.28 1 ==> 0
% 0.89/1.28 2 ==> 2
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4523) {G1,W5,D3,L2,V2,M2} { alpha2( X ), ! p( skol5( Z ) )
% 0.89/1.28 }.
% 0.89/1.28 parent0[1]: (8) {G0,W5,D3,L2,V2,M1} I { alpha2( X ), ! alpha4( skol3( Y ) )
% 0.89/1.28 }.
% 0.89/1.28 parent1[1]: (58) {G2,W5,D3,L2,V2,M1} R(55,14) { ! p( skol5( Y ) ), alpha4(
% 0.89/1.28 X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := Y
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := skol3( Y )
% 0.89/1.28 Y := Z
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (101) {G3,W5,D3,L2,V2,M1} R(58,8) { ! p( skol5( X ) ), alpha2
% 0.89/1.28 ( Y ) }.
% 0.89/1.28 parent0: (4523) {G1,W5,D3,L2,V2,M2} { alpha2( X ), ! p( skol5( Z ) ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := Y
% 0.89/1.28 Y := Z
% 0.89/1.28 Z := X
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 1
% 0.89/1.28 1 ==> 0
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4524) {G1,W7,D3,L3,V0,M3} { alpha6, reachable( initial_world
% 0.89/1.28 , skol4( skol1 ) ), ! alpha4( skol1 ) }.
% 0.89/1.28 parent0[2]: (24) {G1,W7,D2,L3,V1,M1} R(2,1) { alpha6, reachable(
% 0.89/1.28 initial_world, X ), ! reachable( skol1, X ) }.
% 0.89/1.28 parent1[1]: (11) {G0,W6,D3,L2,V1,M1} I { ! alpha4( X ), reachable( X, skol4
% 0.89/1.28 ( X ) ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := skol4( skol1 )
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := skol1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (114) {G2,W7,D3,L3,V0,M1} R(24,11) { alpha6, ! alpha4( skol1 )
% 0.89/1.28 , reachable( initial_world, skol4( skol1 ) ) }.
% 0.89/1.28 parent0: (4524) {G1,W7,D3,L3,V0,M3} { alpha6, reachable( initial_world,
% 0.89/1.28 skol4( skol1 ) ), ! alpha4( skol1 ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 1 ==> 2
% 0.89/1.28 2 ==> 1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4525) {G1,W7,D2,L4,V1,M4} { alpha1, ! alpha3( X ), !
% 0.89/1.28 reachable( skol1, X ), alpha6 }.
% 0.89/1.28 parent0[2]: (26) {G1,W9,D2,L4,V2,M2} R(18,1) { alpha1, ! alpha3( X ), !
% 0.89/1.28 reachable( initial_world, Y ), ! reachable( Y, X ) }.
% 0.89/1.28 parent1[1]: (2) {G0,W4,D2,L2,V0,M1} I { alpha6, reachable( initial_world,
% 0.89/1.28 skol1 ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := skol1
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4527) {G1,W7,D2,L4,V1,M4} { alpha6, ! alpha3( X ), !
% 0.89/1.28 reachable( skol1, X ), alpha6 }.
% 0.89/1.28 parent0[1]: (4) {G0,W2,D1,L2,V0,M1} I { alpha6, ! alpha1 }.
% 0.89/1.28 parent1[0]: (4525) {G1,W7,D2,L4,V1,M4} { alpha1, ! alpha3( X ), !
% 0.89/1.28 reachable( skol1, X ), alpha6 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 factor: (4528) {G1,W6,D2,L3,V1,M3} { alpha6, ! alpha3( X ), ! reachable(
% 0.89/1.28 skol1, X ) }.
% 0.89/1.28 parent0[0, 3]: (4527) {G1,W7,D2,L4,V1,M4} { alpha6, ! alpha3( X ), !
% 0.89/1.28 reachable( skol1, X ), alpha6 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (139) {G2,W6,D2,L3,V1,M1} R(26,2);r(4) { ! alpha3( X ), alpha6
% 0.89/1.28 , ! reachable( skol1, X ) }.
% 0.89/1.28 parent0: (4528) {G1,W6,D2,L3,V1,M3} { alpha6, ! alpha3( X ), ! reachable(
% 0.89/1.28 skol1, X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 1
% 0.89/1.28 1 ==> 0
% 0.89/1.28 2 ==> 2
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4529) {G1,W10,D3,L4,V2,M4} { ! alpha5( X ), p( Y ), alpha2( X
% 0.89/1.28 ), ! reachable( skol3( X ), Y ) }.
% 0.89/1.28 parent0[2]: (13) {G0,W7,D2,L3,V2,M1} I { ! alpha5( X ), p( Y ), ! reachable
% 0.89/1.28 ( X, Y ) }.
% 0.89/1.28 parent1[1]: (36) {G1,W9,D3,L3,V2,M2} R(9,1) { alpha2( X ), reachable( X, Y
% 0.89/1.28 ), ! reachable( skol3( X ), Y ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := Y
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := X
% 0.89/1.28 Y := Y
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (191) {G2,W10,D3,L4,V2,M1} R(36,13) { alpha2( X ), ! alpha5( X
% 0.89/1.28 ), p( Y ), ! reachable( skol3( X ), Y ) }.
% 0.89/1.28 parent0: (4529) {G1,W10,D3,L4,V2,M4} { ! alpha5( X ), p( Y ), alpha2( X )
% 0.89/1.28 , ! reachable( skol3( X ), Y ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := Y
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 1
% 0.89/1.28 1 ==> 2
% 0.89/1.28 2 ==> 0
% 0.89/1.28 3 ==> 3
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4530) {G1,W9,D4,L3,V2,M3} { p( skol7( skol4( X ) ) ), alpha3
% 0.89/1.28 ( skol4( X ) ), ! alpha4( Y ) }.
% 0.89/1.28 parent0[2]: (61) {G1,W7,D3,L3,V1,M1} R(13,21) { p( skol7( X ) ), alpha3( X
% 0.89/1.28 ), ! alpha5( X ) }.
% 0.89/1.28 parent1[1]: (10) {G0,W5,D3,L2,V2,M1} I { ! alpha4( X ), alpha5( skol4( Y )
% 0.89/1.28 ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := skol4( X )
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := Y
% 0.89/1.28 Y := X
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (283) {G2,W9,D4,L3,V2,M1} R(61,10) { p( skol7( skol4( X ) ) )
% 0.89/1.28 , alpha3( skol4( X ) ), ! alpha4( Y ) }.
% 0.89/1.28 parent0: (4530) {G1,W9,D4,L3,V2,M3} { p( skol7( skol4( X ) ) ), alpha3(
% 0.89/1.28 skol4( X ) ), ! alpha4( Y ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := Y
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 1 ==> 1
% 0.89/1.28 2 ==> 2
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4531) {G2,W9,D3,L4,V1,M4} { ! alpha3( X ), alpha6, ! alpha4(
% 0.89/1.28 skol1 ), ! reachable( skol4( skol1 ), X ) }.
% 0.89/1.28 parent0[2]: (139) {G2,W6,D2,L3,V1,M1} R(26,2);r(4) { ! alpha3( X ), alpha6
% 0.89/1.28 , ! reachable( skol1, X ) }.
% 0.89/1.28 parent1[1]: (44) {G1,W9,D3,L3,V2,M2} R(11,1) { ! alpha4( X ), reachable( X
% 0.89/1.28 , Y ), ! reachable( skol4( X ), Y ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := skol1
% 0.89/1.28 Y := X
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (324) {G3,W9,D3,L4,V1,M1} R(44,139) { ! alpha4( skol1 ), !
% 0.89/1.28 alpha3( X ), alpha6, ! reachable( skol4( skol1 ), X ) }.
% 0.89/1.28 parent0: (4531) {G2,W9,D3,L4,V1,M4} { ! alpha3( X ), alpha6, ! alpha4(
% 0.89/1.28 skol1 ), ! reachable( skol4( skol1 ), X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 1
% 0.89/1.28 1 ==> 2
% 0.89/1.28 2 ==> 0
% 0.89/1.28 3 ==> 3
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4533) {G1,W8,D3,L4,V0,M4} { ! alpha5( skol4( skol1 ) ),
% 0.89/1.28 alpha4( initial_world ), alpha6, ! alpha4( skol1 ) }.
% 0.89/1.28 parent0[2]: (12) {G0,W7,D2,L3,V2,M1} I { ! alpha5( Y ), alpha4( X ), !
% 0.89/1.28 reachable( X, Y ) }.
% 0.89/1.28 parent1[2]: (114) {G2,W7,D3,L3,V0,M1} R(24,11) { alpha6, ! alpha4( skol1 )
% 0.89/1.28 , reachable( initial_world, skol4( skol1 ) ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := initial_world
% 0.89/1.28 Y := skol4( skol1 )
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (502) {G3,W8,D3,L4,V0,M1} R(114,12) { alpha6, ! alpha4( skol1
% 0.89/1.28 ), alpha4( initial_world ), ! alpha5( skol4( skol1 ) ) }.
% 0.89/1.28 parent0: (4533) {G1,W8,D3,L4,V0,M4} { ! alpha5( skol4( skol1 ) ), alpha4(
% 0.89/1.28 initial_world ), alpha6, ! alpha4( skol1 ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 3
% 0.89/1.28 1 ==> 2
% 0.89/1.28 2 ==> 0
% 0.89/1.28 3 ==> 1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4534) {G1,W7,D2,L4,V1,M4} { alpha6, ! alpha4( skol1 ), alpha4
% 0.89/1.28 ( initial_world ), ! alpha4( X ) }.
% 0.89/1.28 parent0[3]: (502) {G3,W8,D3,L4,V0,M1} R(114,12) { alpha6, ! alpha4( skol1 )
% 0.89/1.28 , alpha4( initial_world ), ! alpha5( skol4( skol1 ) ) }.
% 0.89/1.28 parent1[1]: (10) {G0,W5,D3,L2,V2,M1} I { ! alpha4( X ), alpha5( skol4( Y )
% 0.89/1.28 ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := X
% 0.89/1.28 Y := skol1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (1681) {G4,W7,D2,L4,V1,M2} R(502,10) { alpha6, alpha4(
% 0.89/1.28 initial_world ), ! alpha4( X ), ! alpha4( skol1 ) }.
% 0.89/1.28 parent0: (4534) {G1,W7,D2,L4,V1,M4} { alpha6, ! alpha4( skol1 ), alpha4(
% 0.89/1.28 initial_world ), ! alpha4( X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 1 ==> 3
% 0.89/1.28 2 ==> 1
% 0.89/1.28 3 ==> 2
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 factor: (4536) {G4,W5,D2,L3,V0,M3} { alpha6, alpha4( initial_world ), !
% 0.89/1.28 alpha4( skol1 ) }.
% 0.89/1.28 parent0[2, 3]: (1681) {G4,W7,D2,L4,V1,M2} R(502,10) { alpha6, alpha4(
% 0.89/1.28 initial_world ), ! alpha4( X ), ! alpha4( skol1 ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := skol1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (1682) {G5,W5,D2,L3,V0,M1} F(1681) { alpha6, alpha4(
% 0.89/1.28 initial_world ), ! alpha4( skol1 ) }.
% 0.89/1.28 parent0: (4536) {G4,W5,D2,L3,V0,M3} { alpha6, alpha4( initial_world ), !
% 0.89/1.28 alpha4( skol1 ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 1 ==> 1
% 0.89/1.28 2 ==> 2
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4537) {G2,W5,D2,L3,V0,M3} { alpha6, alpha4( initial_world ),
% 0.89/1.28 ! alpha2( skol1 ) }.
% 0.89/1.28 parent0[2]: (1682) {G5,W5,D2,L3,V0,M1} F(1681) { alpha6, alpha4(
% 0.89/1.28 initial_world ), ! alpha4( skol1 ) }.
% 0.89/1.28 parent1[1]: (31) {G1,W4,D2,L2,V1,M1} R(7,0) { ! alpha2( X ), alpha4( X )
% 0.89/1.28 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := skol1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4538) {G1,W4,D2,L3,V0,M3} { alpha6, alpha4( initial_world ),
% 0.89/1.28 alpha6 }.
% 0.89/1.28 parent0[2]: (4537) {G2,W5,D2,L3,V0,M3} { alpha6, alpha4( initial_world ),
% 0.89/1.28 ! alpha2( skol1 ) }.
% 0.89/1.28 parent1[1]: (3) {G0,W3,D2,L2,V0,M1} I { alpha6, alpha2( skol1 ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 factor: (4539) {G1,W3,D2,L2,V0,M2} { alpha6, alpha4( initial_world ) }.
% 0.89/1.28 parent0[0, 2]: (4538) {G1,W4,D2,L3,V0,M3} { alpha6, alpha4( initial_world
% 0.89/1.28 ), alpha6 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (1683) {G6,W3,D2,L2,V0,M1} R(1682,31);r(3) { alpha6, alpha4(
% 0.89/1.28 initial_world ) }.
% 0.89/1.28 parent0: (4539) {G1,W3,D2,L2,V0,M2} { alpha6, alpha4( initial_world ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 1 ==> 1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4540) {G3,W4,D3,L2,V1,M2} { alpha4( skol4( X ) ), alpha6 }.
% 0.89/1.28 parent0[0]: (57) {G2,W5,D3,L2,V2,M2} R(55,10) { ! alpha4( Y ), alpha4(
% 0.89/1.28 skol4( X ) ) }.
% 0.89/1.28 parent1[1]: (1683) {G6,W3,D2,L2,V0,M1} R(1682,31);r(3) { alpha6, alpha4(
% 0.89/1.28 initial_world ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := initial_world
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (1685) {G7,W4,D3,L2,V1,M1} R(1683,57) { alpha6, alpha4( skol4
% 0.89/1.28 ( X ) ) }.
% 0.89/1.28 parent0: (4540) {G3,W4,D3,L2,V1,M2} { alpha4( skol4( X ) ), alpha6 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 1
% 0.89/1.28 1 ==> 0
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4541) {G2,W5,D3,L3,V0,M3} { ! alpha3( skol4( initial_world )
% 0.89/1.28 ), alpha1, alpha6 }.
% 0.89/1.28 parent0[2]: (42) {G1,W6,D3,L3,V0,M1} R(11,18) { ! alpha3( skol4(
% 0.89/1.28 initial_world ) ), alpha1, ! alpha4( initial_world ) }.
% 0.89/1.28 parent1[1]: (1683) {G6,W3,D2,L2,V0,M1} R(1682,31);r(3) { alpha6, alpha4(
% 0.89/1.28 initial_world ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4542) {G1,W5,D3,L3,V0,M3} { alpha1, ! alpha3( skol4(
% 0.89/1.28 initial_world ) ), alpha1 }.
% 0.89/1.28 parent0[1]: (5) {G0,W2,D1,L2,V0,M1} I { alpha1, ! alpha6 }.
% 0.89/1.28 parent1[2]: (4541) {G2,W5,D3,L3,V0,M3} { ! alpha3( skol4( initial_world )
% 0.89/1.28 ), alpha1, alpha6 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 factor: (4543) {G1,W4,D3,L2,V0,M2} { alpha1, ! alpha3( skol4(
% 0.89/1.28 initial_world ) ) }.
% 0.89/1.28 parent0[0, 2]: (4542) {G1,W5,D3,L3,V0,M3} { alpha1, ! alpha3( skol4(
% 0.89/1.28 initial_world ) ), alpha1 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (1686) {G7,W4,D3,L2,V0,M1} R(1683,42);r(5) { alpha1, ! alpha3
% 0.89/1.28 ( skol4( initial_world ) ) }.
% 0.89/1.28 parent0: (4543) {G1,W4,D3,L2,V0,M2} { alpha1, ! alpha3( skol4(
% 0.89/1.28 initial_world ) ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 1 ==> 1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4544) {G1,W10,D4,L4,V0,M4} { ! alpha4( skol1 ), ! alpha3(
% 0.89/1.28 skol4( skol4( skol1 ) ) ), alpha6, ! alpha4( skol4( skol1 ) ) }.
% 0.89/1.28 parent0[3]: (324) {G3,W9,D3,L4,V1,M1} R(44,139) { ! alpha4( skol1 ), !
% 0.89/1.28 alpha3( X ), alpha6, ! reachable( skol4( skol1 ), X ) }.
% 0.89/1.28 parent1[1]: (11) {G0,W6,D3,L2,V1,M1} I { ! alpha4( X ), reachable( X, skol4
% 0.89/1.28 ( X ) ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := skol4( skol4( skol1 ) )
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := skol4( skol1 )
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4545) {G2,W8,D4,L4,V0,M4} { ! alpha4( skol1 ), ! alpha3(
% 0.89/1.28 skol4( skol4( skol1 ) ) ), alpha6, alpha6 }.
% 0.89/1.28 parent0[3]: (4544) {G1,W10,D4,L4,V0,M4} { ! alpha4( skol1 ), ! alpha3(
% 0.89/1.28 skol4( skol4( skol1 ) ) ), alpha6, ! alpha4( skol4( skol1 ) ) }.
% 0.89/1.28 parent1[1]: (1685) {G7,W4,D3,L2,V1,M1} R(1683,57) { alpha6, alpha4( skol4(
% 0.89/1.28 X ) ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := skol1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 factor: (4546) {G2,W7,D4,L3,V0,M3} { ! alpha4( skol1 ), ! alpha3( skol4(
% 0.89/1.28 skol4( skol1 ) ) ), alpha6 }.
% 0.89/1.28 parent0[2, 3]: (4545) {G2,W8,D4,L4,V0,M4} { ! alpha4( skol1 ), ! alpha3(
% 0.89/1.28 skol4( skol4( skol1 ) ) ), alpha6, alpha6 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (3098) {G8,W7,D4,L3,V0,M1} R(324,11);r(1685) { ! alpha3( skol4
% 0.89/1.28 ( skol4( skol1 ) ) ), alpha6, ! alpha4( skol1 ) }.
% 0.89/1.28 parent0: (4546) {G2,W7,D4,L3,V0,M3} { ! alpha4( skol1 ), ! alpha3( skol4(
% 0.89/1.28 skol4( skol1 ) ) ), alpha6 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 2
% 0.89/1.28 1 ==> 0
% 0.89/1.28 2 ==> 1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4547) {G2,W7,D4,L3,V0,M3} { ! alpha3( skol4( skol4( skol1 ) )
% 0.89/1.28 ), alpha6, ! alpha2( skol1 ) }.
% 0.89/1.28 parent0[2]: (3098) {G8,W7,D4,L3,V0,M1} R(324,11);r(1685) { ! alpha3( skol4
% 0.89/1.28 ( skol4( skol1 ) ) ), alpha6, ! alpha4( skol1 ) }.
% 0.89/1.28 parent1[1]: (31) {G1,W4,D2,L2,V1,M1} R(7,0) { ! alpha2( X ), alpha4( X )
% 0.89/1.28 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := skol1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4548) {G1,W6,D4,L3,V0,M3} { ! alpha3( skol4( skol4( skol1 ) )
% 0.89/1.28 ), alpha6, alpha6 }.
% 0.89/1.28 parent0[2]: (4547) {G2,W7,D4,L3,V0,M3} { ! alpha3( skol4( skol4( skol1 ) )
% 0.89/1.28 ), alpha6, ! alpha2( skol1 ) }.
% 0.89/1.28 parent1[1]: (3) {G0,W3,D2,L2,V0,M1} I { alpha6, alpha2( skol1 ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 factor: (4549) {G1,W5,D4,L2,V0,M2} { ! alpha3( skol4( skol4( skol1 ) ) ),
% 0.89/1.28 alpha6 }.
% 0.89/1.28 parent0[1, 2]: (4548) {G1,W6,D4,L3,V0,M3} { ! alpha3( skol4( skol4( skol1
% 0.89/1.28 ) ) ), alpha6, alpha6 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (3102) {G9,W5,D4,L2,V0,M1} R(3098,31);r(3) { alpha6, ! alpha3
% 0.89/1.28 ( skol4( skol4( skol1 ) ) ) }.
% 0.89/1.28 parent0: (4549) {G1,W5,D4,L2,V0,M2} { ! alpha3( skol4( skol4( skol1 ) ) )
% 0.89/1.28 , alpha6 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 1
% 0.89/1.28 1 ==> 0
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4550) {G3,W8,D4,L3,V1,M3} { p( skol7( skol4( X ) ) ), alpha3
% 0.89/1.28 ( skol4( X ) ), alpha6 }.
% 0.89/1.28 parent0[2]: (283) {G2,W9,D4,L3,V2,M1} R(61,10) { p( skol7( skol4( X ) ) ),
% 0.89/1.28 alpha3( skol4( X ) ), ! alpha4( Y ) }.
% 0.89/1.28 parent1[1]: (1685) {G7,W4,D3,L2,V1,M1} R(1683,57) { alpha6, alpha4( skol4(
% 0.89/1.28 X ) ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := skol4( Y )
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := Y
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4551) {G3,W5,D3,L3,V1,M3} { alpha6, alpha3( skol4( X ) ),
% 0.89/1.28 alpha6 }.
% 0.89/1.28 parent0[1]: (28) {G2,W4,D3,L2,V1,M1} R(25,20) { alpha6, ! p( skol7( X ) )
% 0.89/1.28 }.
% 0.89/1.28 parent1[0]: (4550) {G3,W8,D4,L3,V1,M3} { p( skol7( skol4( X ) ) ), alpha3
% 0.89/1.28 ( skol4( X ) ), alpha6 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := skol4( X )
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 factor: (4552) {G3,W4,D3,L2,V1,M2} { alpha6, alpha3( skol4( X ) ) }.
% 0.89/1.28 parent0[0, 2]: (4551) {G3,W5,D3,L3,V1,M3} { alpha6, alpha3( skol4( X ) ),
% 0.89/1.28 alpha6 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (3325) {G8,W4,D3,L2,V1,M1} R(283,1685);r(28) { alpha6, alpha3
% 0.89/1.28 ( skol4( X ) ) }.
% 0.89/1.28 parent0: (4552) {G3,W4,D3,L2,V1,M2} { alpha6, alpha3( skol4( X ) ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 1 ==> 1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4553) {G9,W2,D1,L2,V0,M2} { alpha6, alpha6 }.
% 0.89/1.28 parent0[1]: (3102) {G9,W5,D4,L2,V0,M1} R(3098,31);r(3) { alpha6, ! alpha3(
% 0.89/1.28 skol4( skol4( skol1 ) ) ) }.
% 0.89/1.28 parent1[1]: (3325) {G8,W4,D3,L2,V1,M1} R(283,1685);r(28) { alpha6, alpha3(
% 0.89/1.28 skol4( X ) ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := skol4( skol1 )
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 factor: (4554) {G9,W1,D1,L1,V0,M1} { alpha6 }.
% 0.89/1.28 parent0[0, 1]: (4553) {G9,W2,D1,L2,V0,M2} { alpha6, alpha6 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (3330) {G10,W1,D1,L1,V0,M1} R(3325,3102);f { alpha6 }.
% 0.89/1.28 parent0: (4554) {G9,W1,D1,L1,V0,M1} { alpha6 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4555) {G8,W2,D1,L2,V0,M2} { alpha1, alpha6 }.
% 0.89/1.28 parent0[1]: (1686) {G7,W4,D3,L2,V0,M1} R(1683,42);r(5) { alpha1, ! alpha3(
% 0.89/1.28 skol4( initial_world ) ) }.
% 0.89/1.28 parent1[1]: (3325) {G8,W4,D3,L2,V1,M1} R(283,1685);r(28) { alpha6, alpha3(
% 0.89/1.28 skol4( X ) ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := initial_world
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4556) {G1,W2,D1,L2,V0,M2} { alpha1, alpha1 }.
% 0.89/1.28 parent0[1]: (5) {G0,W2,D1,L2,V0,M1} I { alpha1, ! alpha6 }.
% 0.89/1.28 parent1[1]: (4555) {G8,W2,D1,L2,V0,M2} { alpha1, alpha6 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 factor: (4557) {G1,W1,D1,L1,V0,M1} { alpha1 }.
% 0.89/1.28 parent0[0, 1]: (4556) {G1,W2,D1,L2,V0,M2} { alpha1, alpha1 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (3335) {G9,W1,D1,L1,V0,M1} R(3325,1686);r(5) { alpha1 }.
% 0.89/1.28 parent0: (4557) {G1,W1,D1,L1,V0,M1} { alpha1 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4558) {G1,W5,D2,L2,V1,M2} { ! reachable( initial_world, X ),
% 0.89/1.28 ! alpha2( X ) }.
% 0.89/1.28 parent0[2]: (6) {G0,W6,D2,L3,V1,M1} I { ! reachable( initial_world, X ), !
% 0.89/1.28 alpha2( X ), ! alpha6 }.
% 0.89/1.28 parent1[0]: (3330) {G10,W1,D1,L1,V0,M1} R(3325,3102);f { alpha6 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (3336) {G11,W5,D2,L2,V1,M1} R(3330,6) { ! alpha2( X ), !
% 0.89/1.28 reachable( initial_world, X ) }.
% 0.89/1.28 parent0: (4558) {G1,W5,D2,L2,V1,M2} { ! reachable( initial_world, X ), !
% 0.89/1.28 alpha2( X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 1
% 0.89/1.28 1 ==> 0
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4559) {G1,W3,D2,L1,V0,M1} { reachable( initial_world, skol6 )
% 0.89/1.28 }.
% 0.89/1.28 parent0[1]: (16) {G0,W4,D2,L2,V0,M1} I { reachable( initial_world, skol6 )
% 0.89/1.28 , ! alpha1 }.
% 0.89/1.28 parent1[0]: (3335) {G9,W1,D1,L1,V0,M1} R(3325,1686);r(5) { alpha1 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (3351) {G10,W3,D2,L1,V0,M1} R(3335,16) { reachable(
% 0.89/1.28 initial_world, skol6 ) }.
% 0.89/1.28 parent0: (4559) {G1,W3,D2,L1,V0,M1} { reachable( initial_world, skol6 )
% 0.89/1.28 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4560) {G1,W2,D2,L1,V0,M1} { alpha3( skol6 ) }.
% 0.89/1.28 parent0[1]: (17) {G0,W3,D2,L2,V0,M1} I { alpha3( skol6 ), ! alpha1 }.
% 0.89/1.28 parent1[0]: (3335) {G9,W1,D1,L1,V0,M1} R(3325,1686);r(5) { alpha1 }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (3352) {G10,W2,D2,L1,V0,M1} R(3335,17) { alpha3( skol6 ) }.
% 0.89/1.28 parent0: (4560) {G1,W2,D2,L1,V0,M1} { alpha3( skol6 ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4561) {G11,W2,D2,L1,V0,M1} { ! alpha2( skol6 ) }.
% 0.89/1.28 parent0[1]: (3336) {G11,W5,D2,L2,V1,M1} R(3330,6) { ! alpha2( X ), !
% 0.89/1.28 reachable( initial_world, X ) }.
% 0.89/1.28 parent1[0]: (3351) {G10,W3,D2,L1,V0,M1} R(3335,16) { reachable(
% 0.89/1.28 initial_world, skol6 ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := skol6
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (3434) {G12,W2,D2,L1,V0,M1} R(3336,3351) { ! alpha2( skol6 )
% 0.89/1.28 }.
% 0.89/1.28 parent0: (4561) {G11,W2,D2,L1,V0,M1} { ! alpha2( skol6 ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4562) {G4,W3,D3,L1,V1,M1} { ! p( skol5( X ) ) }.
% 0.89/1.28 parent0[0]: (3434) {G12,W2,D2,L1,V0,M1} R(3336,3351) { ! alpha2( skol6 )
% 0.89/1.28 }.
% 0.89/1.28 parent1[1]: (101) {G3,W5,D3,L2,V2,M1} R(58,8) { ! p( skol5( X ) ), alpha2(
% 0.89/1.28 Y ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := X
% 0.89/1.28 Y := skol6
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (3464) {G13,W3,D3,L1,V1,M1} R(3434,101) { ! p( skol5( X ) )
% 0.89/1.28 }.
% 0.89/1.28 parent0: (4562) {G4,W3,D3,L1,V1,M1} { ! p( skol5( X ) ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4564) {G1,W11,D4,L4,V1,M4} { alpha2( X ), ! alpha5( X ), p(
% 0.89/1.28 skol5( skol3( X ) ) ), alpha5( skol3( X ) ) }.
% 0.89/1.28 parent0[3]: (191) {G2,W10,D3,L4,V2,M1} R(36,13) { alpha2( X ), ! alpha5( X
% 0.89/1.28 ), p( Y ), ! reachable( skol3( X ), Y ) }.
% 0.89/1.28 parent1[1]: (15) {G0,W6,D3,L2,V1,M1} I { alpha5( X ), reachable( X, skol5(
% 0.89/1.28 X ) ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := skol5( skol3( X ) )
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := skol3( X )
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4565) {G2,W7,D3,L3,V1,M3} { alpha2( X ), ! alpha5( X ),
% 0.89/1.28 alpha5( skol3( X ) ) }.
% 0.89/1.28 parent0[0]: (3464) {G13,W3,D3,L1,V1,M1} R(3434,101) { ! p( skol5( X ) ) }.
% 0.89/1.28 parent1[2]: (4564) {G1,W11,D4,L4,V1,M4} { alpha2( X ), ! alpha5( X ), p(
% 0.89/1.28 skol5( skol3( X ) ) ), alpha5( skol3( X ) ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := skol3( X )
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (3713) {G14,W7,D3,L3,V1,M2} R(191,15);r(3464) { alpha2( X ),
% 0.89/1.28 alpha5( skol3( X ) ), ! alpha5( X ) }.
% 0.89/1.28 parent0: (4565) {G2,W7,D3,L3,V1,M3} { alpha2( X ), ! alpha5( X ), alpha5(
% 0.89/1.28 skol3( X ) ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 1 ==> 2
% 0.89/1.28 2 ==> 1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4566) {G2,W4,D2,L2,V1,M2} { ! alpha3( X ), alpha5( X ) }.
% 0.89/1.28 parent0[0]: (3464) {G13,W3,D3,L1,V1,M1} R(3434,101) { ! p( skol5( X ) ) }.
% 0.89/1.28 parent1[0]: (72) {G1,W7,D3,L3,V1,M1} R(19,15) { p( skol5( X ) ), ! alpha3(
% 0.89/1.28 X ), alpha5( X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (4053) {G14,W4,D2,L2,V1,M1} S(72);r(3464) { ! alpha3( X ),
% 0.89/1.28 alpha5( X ) }.
% 0.89/1.28 parent0: (4566) {G2,W4,D2,L2,V1,M2} { ! alpha3( X ), alpha5( X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 1 ==> 1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4567) {G2,W7,D3,L3,V1,M3} { alpha4( skol3( X ) ), alpha2( X )
% 0.89/1.28 , ! alpha5( X ) }.
% 0.89/1.28 parent0[1]: (55) {G1,W4,D2,L2,V1,M1} R(12,0) { alpha4( X ), ! alpha5( X )
% 0.89/1.28 }.
% 0.89/1.28 parent1[1]: (3713) {G14,W7,D3,L3,V1,M2} R(191,15);r(3464) { alpha2( X ),
% 0.89/1.28 alpha5( skol3( X ) ), ! alpha5( X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := skol3( X )
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (4355) {G15,W7,D3,L3,V1,M1} R(3713,55) { alpha2( X ), alpha4(
% 0.89/1.28 skol3( X ) ), ! alpha5( X ) }.
% 0.89/1.28 parent0: (4567) {G2,W7,D3,L3,V1,M3} { alpha4( skol3( X ) ), alpha2( X ), !
% 0.89/1.28 alpha5( X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 1
% 0.89/1.28 1 ==> 0
% 0.89/1.28 2 ==> 2
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4568) {G15,W7,D3,L3,V1,M3} { alpha2( X ), alpha4( skol3( X )
% 0.89/1.28 ), ! alpha3( X ) }.
% 0.89/1.28 parent0[2]: (4355) {G15,W7,D3,L3,V1,M1} R(3713,55) { alpha2( X ), alpha4(
% 0.89/1.28 skol3( X ) ), ! alpha5( X ) }.
% 0.89/1.28 parent1[1]: (4053) {G14,W4,D2,L2,V1,M1} S(72);r(3464) { ! alpha3( X ),
% 0.89/1.28 alpha5( X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (4451) {G16,W7,D3,L3,V1,M1} R(4355,4053) { alpha2( X ), !
% 0.89/1.28 alpha3( X ), alpha4( skol3( X ) ) }.
% 0.89/1.28 parent0: (4568) {G15,W7,D3,L3,V1,M3} { alpha2( X ), alpha4( skol3( X ) ),
% 0.89/1.28 ! alpha3( X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 1 ==> 2
% 0.89/1.28 2 ==> 1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4569) {G1,W6,D2,L3,V2,M3} { alpha2( X ), alpha2( Y ), !
% 0.89/1.28 alpha3( Y ) }.
% 0.89/1.28 parent0[1]: (8) {G0,W5,D3,L2,V2,M1} I { alpha2( X ), ! alpha4( skol3( Y ) )
% 0.89/1.28 }.
% 0.89/1.28 parent1[2]: (4451) {G16,W7,D3,L3,V1,M1} R(4355,4053) { alpha2( X ), !
% 0.89/1.28 alpha3( X ), alpha4( skol3( X ) ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := Y
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 X := Y
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (4453) {G17,W6,D2,L3,V2,M1} R(4451,8) { alpha2( X ), alpha2( Y
% 0.89/1.28 ), ! alpha3( X ) }.
% 0.89/1.28 parent0: (4569) {G1,W6,D2,L3,V2,M3} { alpha2( X ), alpha2( Y ), ! alpha3(
% 0.89/1.28 Y ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := X
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 1 ==> 0
% 0.89/1.28 2 ==> 2
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 factor: (4571) {G17,W4,D2,L2,V1,M2} { alpha2( X ), ! alpha3( X ) }.
% 0.89/1.28 parent0[0, 1]: (4453) {G17,W6,D2,L3,V2,M1} R(4451,8) { alpha2( X ), alpha2
% 0.89/1.28 ( Y ), ! alpha3( X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 Y := X
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (4454) {G18,W4,D2,L2,V1,M1} F(4453) { alpha2( X ), ! alpha3( X
% 0.89/1.28 ) }.
% 0.89/1.28 parent0: (4571) {G17,W4,D2,L2,V1,M2} { alpha2( X ), ! alpha3( X ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := X
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 0 ==> 0
% 0.89/1.28 1 ==> 1
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4572) {G11,W2,D2,L1,V0,M1} { alpha2( skol6 ) }.
% 0.89/1.28 parent0[1]: (4454) {G18,W4,D2,L2,V1,M1} F(4453) { alpha2( X ), ! alpha3( X
% 0.89/1.28 ) }.
% 0.89/1.28 parent1[0]: (3352) {G10,W2,D2,L1,V0,M1} R(3335,17) { alpha3( skol6 ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 X := skol6
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 resolution: (4573) {G12,W0,D0,L0,V0,M0} { }.
% 0.89/1.28 parent0[0]: (3434) {G12,W2,D2,L1,V0,M1} R(3336,3351) { ! alpha2( skol6 )
% 0.89/1.28 }.
% 0.89/1.28 parent1[0]: (4572) {G11,W2,D2,L1,V0,M1} { alpha2( skol6 ) }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 substitution1:
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 subsumption: (4457) {G19,W0,D0,L0,V0,M0} R(4454,3352);r(3434) { }.
% 0.89/1.28 parent0: (4573) {G12,W0,D0,L0,V0,M0} { }.
% 0.89/1.28 substitution0:
% 0.89/1.28 end
% 0.89/1.28 permutation0:
% 0.89/1.28 end
% 0.89/1.28
% 0.89/1.28 Proof check complete!
% 0.89/1.28
% 0.89/1.28 Memory use:
% 0.89/1.28
% 0.89/1.28 space for terms: 63563
% 0.89/1.28 space for clauses: 167212
% 0.89/1.28
% 0.89/1.28
% 0.89/1.28 clauses generated: 20724
% 0.89/1.28 clauses kept: 4458
% 0.89/1.28 clauses selected: 510
% 0.89/1.28 clauses deleted: 415
% 0.89/1.28 clauses inuse deleted: 303
% 0.89/1.28
% 0.89/1.28 subsentry: 84340
% 0.89/1.28 literals s-matched: 60187
% 0.89/1.28 literals matched: 60187
% 0.89/1.28 full subsumption: 31628
% 0.89/1.28
% 0.89/1.28 checksum: -1150486311
% 0.89/1.28
% 0.89/1.28
% 0.89/1.28 Bliksem ended
%------------------------------------------------------------------------------