%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : PUZ001+1 : TPTP v8.1.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n024.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 17:58:06 EDT 2022
% Result : Theorem 0.77s 1.14s
% Output : Refutation 0.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : PUZ001+1 : TPTP v8.1.0. Released v2.0.0.
% 0.03/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n024.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % DateTime : Sat May 28 22:21:21 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.77/1.14 *** allocated 10000 integers for termspace/termends
% 0.77/1.14 *** allocated 10000 integers for clauses
% 0.77/1.14 *** allocated 10000 integers for justifications
% 0.77/1.14 Bliksem 1.12
% 0.77/1.14
% 0.77/1.14
% 0.77/1.14 Automatic Strategy Selection
% 0.77/1.14
% 0.77/1.14
% 0.77/1.14 Clauses:
% 0.77/1.14
% 0.77/1.14 { lives( skol1 ) }.
% 0.77/1.14 { killed( skol1, agatha ) }.
% 0.77/1.14 { lives( agatha ) }.
% 0.77/1.14 { lives( butler ) }.
% 0.77/1.14 { lives( charles ) }.
% 0.77/1.14 { ! lives( X ), X = agatha, X = butler, X = charles }.
% 0.77/1.14 { ! killed( X, Y ), hates( X, Y ) }.
% 0.77/1.14 { ! killed( X, Y ), ! richer( X, Y ) }.
% 0.77/1.14 { ! hates( agatha, X ), ! hates( charles, X ) }.
% 0.77/1.14 { X = butler, hates( agatha, X ) }.
% 0.77/1.14 { richer( X, agatha ), hates( butler, X ) }.
% 0.77/1.14 { ! hates( agatha, X ), hates( butler, X ) }.
% 0.77/1.14 { ! hates( X, skol2( X ) ) }.
% 0.77/1.14 { ! agatha = butler }.
% 0.77/1.14 { ! killed( agatha, agatha ) }.
% 0.77/1.14
% 0.77/1.14 percentage equality = 0.208333, percentage horn = 0.800000
% 0.77/1.14 This is a problem with some equality
% 0.77/1.14
% 0.77/1.14
% 0.77/1.14
% 0.77/1.14 Options Used:
% 0.77/1.14
% 0.77/1.14 useres = 1
% 0.77/1.14 useparamod = 1
% 0.77/1.14 useeqrefl = 1
% 0.77/1.14 useeqfact = 1
% 0.77/1.14 usefactor = 1
% 0.77/1.14 usesimpsplitting = 0
% 0.77/1.14 usesimpdemod = 5
% 0.77/1.14 usesimpres = 3
% 0.77/1.14
% 0.77/1.14 resimpinuse = 1000
% 0.77/1.14 resimpclauses = 20000
% 0.77/1.14 substype = eqrewr
% 0.77/1.14 backwardsubs = 1
% 0.77/1.14 selectoldest = 5
% 0.77/1.14
% 0.77/1.14 litorderings [0] = split
% 0.77/1.14 litorderings [1] = extend the termordering, first sorting on arguments
% 0.77/1.14
% 0.77/1.14 termordering = kbo
% 0.77/1.14
% 0.77/1.14 litapriori = 0
% 0.77/1.14 termapriori = 1
% 0.77/1.14 litaposteriori = 0
% 0.77/1.14 termaposteriori = 0
% 0.77/1.14 demodaposteriori = 0
% 0.77/1.14 ordereqreflfact = 0
% 0.77/1.14
% 0.77/1.14 litselect = negord
% 0.77/1.14
% 0.77/1.14 maxweight = 15
% 0.77/1.14 maxdepth = 30000
% 0.77/1.14 maxlength = 115
% 0.77/1.14 maxnrvars = 195
% 0.77/1.14 excuselevel = 1
% 0.77/1.14 increasemaxweight = 1
% 0.77/1.14
% 0.77/1.14 maxselected = 10000000
% 0.77/1.14 maxnrclauses = 10000000
% 0.77/1.14
% 0.77/1.14 showgenerated = 0
% 0.77/1.14 showkept = 0
% 0.77/1.14 showselected = 0
% 0.77/1.14 showdeleted = 0
% 0.77/1.14 showresimp = 1
% 0.77/1.14 showstatus = 2000
% 0.77/1.14
% 0.77/1.14 prologoutput = 0
% 0.77/1.14 nrgoals = 5000000
% 0.77/1.14 totalproof = 1
% 0.77/1.14
% 0.77/1.14 Symbols occurring in the translation:
% 0.77/1.14
% 0.77/1.14 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.77/1.14 . [1, 2] (w:1, o:19, a:1, s:1, b:0),
% 0.77/1.14 ! [4, 1] (w:0, o:12, a:1, s:1, b:0),
% 0.77/1.14 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.77/1.14 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.77/1.14 lives [36, 1] (w:1, o:17, a:1, s:1, b:0),
% 0.77/1.14 agatha [37, 0] (w:1, o:7, a:1, s:1, b:0),
% 0.77/1.14 killed [38, 2] (w:1, o:43, a:1, s:1, b:0),
% 0.77/1.14 butler [39, 0] (w:1, o:8, a:1, s:1, b:0),
% 0.77/1.14 charles [40, 0] (w:1, o:9, a:1, s:1, b:0),
% 0.77/1.14 hates [42, 2] (w:1, o:44, a:1, s:1, b:0),
% 0.77/1.14 richer [43, 2] (w:1, o:45, a:1, s:1, b:0),
% 0.77/1.14 skol1 [44, 0] (w:1, o:11, a:1, s:1, b:1),
% 0.77/1.14 skol2 [45, 1] (w:1, o:18, a:1, s:1, b:1).
% 0.77/1.14
% 0.77/1.14
% 0.77/1.14 Starting Search:
% 0.77/1.14
% 0.77/1.14 *** allocated 15000 integers for clauses
% 0.77/1.14 *** allocated 22500 integers for clauses
% 0.77/1.14 *** allocated 33750 integers for clauses
% 0.77/1.14
% 0.77/1.14 Bliksems!, er is een bewijs:
% 0.77/1.14 % SZS status Theorem
% 0.77/1.14 % SZS output start Refutation
% 0.77/1.14
% 0.77/1.14 (0) {G0,W2,D2,L1,V0,M1} I { lives( skol1 ) }.
% 0.77/1.14 (1) {G0,W3,D2,L1,V0,M1} I { killed( skol1, agatha ) }.
% 0.77/1.14 (5) {G0,W11,D2,L4,V1,M4} I { ! lives( X ), X = agatha, X = butler, X =
% 0.77/1.14 charles }.
% 0.77/1.14 (6) {G0,W6,D2,L2,V2,M2} I { ! killed( X, Y ), hates( X, Y ) }.
% 0.77/1.14 (7) {G0,W6,D2,L2,V2,M2} I { ! killed( X, Y ), ! richer( X, Y ) }.
% 0.77/1.14 (8) {G0,W6,D2,L2,V1,M2} I { ! hates( agatha, X ), ! hates( charles, X ) }.
% 0.77/1.14 (9) {G0,W6,D2,L2,V1,M2} I { X = butler, hates( agatha, X ) }.
% 0.77/1.14 (10) {G0,W6,D2,L2,V1,M2} I { richer( X, agatha ), hates( butler, X ) }.
% 0.77/1.14 (11) {G0,W6,D2,L2,V1,M2} I { ! hates( agatha, X ), hates( butler, X ) }.
% 0.77/1.14 (12) {G0,W4,D3,L1,V1,M1} I { ! hates( X, skol2( X ) ) }.
% 0.77/1.14 (13) {G0,W3,D2,L1,V0,M1} I { ! butler ==> agatha }.
% 0.77/1.14 (14) {G0,W3,D2,L1,V0,M1} I { ! killed( agatha, agatha ) }.
% 0.77/1.14 (23) {G1,W9,D2,L3,V0,M3} R(5,0) { skol1 ==> agatha, skol1 ==> butler, skol1
% 0.77/1.14 ==> charles }.
% 0.77/1.14 (66) {G1,W3,D2,L1,V0,M1} R(6,1) { hates( skol1, agatha ) }.
% 0.77/1.14 (78) {G1,W4,D3,L1,V0,M1} R(11,12) { ! hates( agatha, skol2( butler ) ) }.
% 0.77/1.14 (108) {G2,W4,D3,L1,V0,M1} R(9,78) { skol2( butler ) ==> butler }.
% 0.77/1.14 (132) {G1,W6,D2,L2,V1,M2} P(9,13) { ! X = agatha, hates( agatha, X ) }.
% 0.77/1.14 (136) {G2,W3,D2,L1,V0,M1} Q(132) { hates( agatha, agatha ) }.
% 0.77/1.14 (150) {G3,W3,D2,L1,V0,M1} R(136,8) { ! hates( charles, agatha ) }.
% 0.77/1.14 (164) {G3,W3,D2,L1,V0,M1} R(10,12);d(108) { richer( butler, agatha ) }.
% 0.77/1.14 (176) {G4,W3,D2,L1,V0,M1} R(164,7) { ! killed( butler, agatha ) }.
% 0.77/1.14 (182) {G5,W6,D2,L2,V1,M2} P(9,176) { ! killed( X, agatha ), hates( agatha,
% 0.77/1.14 X ) }.
% 0.77/1.14 (195) {G3,W3,D2,L1,V0,M1} P(108,78) { ! hates( agatha, butler ) }.
% 0.77/1.14 (301) {G2,W6,D2,L2,V0,M2} P(23,1);r(14) { skol1 ==> butler, skol1 ==>
% 0.77/1.14 charles }.
% 0.77/1.14 (306) {G6,W3,D2,L1,V0,M1} R(182,1) { hates( agatha, skol1 ) }.
% 0.77/1.14 (309) {G7,W6,D2,L2,V0,M2} P(23,306);d(301);r(195) { skol1 ==> charles,
% 0.77/1.14 butler ==> agatha }.
% 0.77/1.14 (591) {G8,W3,D2,L1,V0,M1} S(309);r(13) { skol1 ==> charles }.
% 0.77/1.14 (593) {G9,W0,D0,L0,V0,M0} P(591,66);r(150) { }.
% 0.77/1.14
% 0.77/1.14
% 0.77/1.14 % SZS output end Refutation
% 0.77/1.14 found a proof!
% 0.77/1.14
% 0.77/1.14
% 0.77/1.14 Unprocessed initial clauses:
% 0.77/1.14
% 0.77/1.14 (595) {G0,W2,D2,L1,V0,M1} { lives( skol1 ) }.
% 0.77/1.14 (596) {G0,W3,D2,L1,V0,M1} { killed( skol1, agatha ) }.
% 0.77/1.14 (597) {G0,W2,D2,L1,V0,M1} { lives( agatha ) }.
% 0.77/1.14 (598) {G0,W2,D2,L1,V0,M1} { lives( butler ) }.
% 0.77/1.14 (599) {G0,W2,D2,L1,V0,M1} { lives( charles ) }.
% 0.77/1.14 (600) {G0,W11,D2,L4,V1,M4} { ! lives( X ), X = agatha, X = butler, X =
% 0.77/1.14 charles }.
% 0.77/1.14 (601) {G0,W6,D2,L2,V2,M2} { ! killed( X, Y ), hates( X, Y ) }.
% 0.77/1.14 (602) {G0,W6,D2,L2,V2,M2} { ! killed( X, Y ), ! richer( X, Y ) }.
% 0.77/1.14 (603) {G0,W6,D2,L2,V1,M2} { ! hates( agatha, X ), ! hates( charles, X )
% 0.77/1.14 }.
% 0.77/1.14 (604) {G0,W6,D2,L2,V1,M2} { X = butler, hates( agatha, X ) }.
% 0.77/1.14 (605) {G0,W6,D2,L2,V1,M2} { richer( X, agatha ), hates( butler, X ) }.
% 0.77/1.14 (606) {G0,W6,D2,L2,V1,M2} { ! hates( agatha, X ), hates( butler, X ) }.
% 0.77/1.14 (607) {G0,W4,D3,L1,V1,M1} { ! hates( X, skol2( X ) ) }.
% 0.77/1.14 (608) {G0,W3,D2,L1,V0,M1} { ! agatha = butler }.
% 0.77/1.14 (609) {G0,W3,D2,L1,V0,M1} { ! killed( agatha, agatha ) }.
% 0.77/1.14
% 0.77/1.14
% 0.77/1.14 Total Proof:
% 0.77/1.14
% 0.77/1.14 subsumption: (0) {G0,W2,D2,L1,V0,M1} I { lives( skol1 ) }.
% 0.77/1.14 parent0: (595) {G0,W2,D2,L1,V0,M1} { lives( skol1 ) }.
% 0.77/1.14 substitution0:
% 0.77/1.14 end
% 0.77/1.14 permutation0:
% 0.77/1.14 0 ==> 0
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 subsumption: (1) {G0,W3,D2,L1,V0,M1} I { killed( skol1, agatha ) }.
% 0.77/1.14 parent0: (596) {G0,W3,D2,L1,V0,M1} { killed( skol1, agatha ) }.
% 0.77/1.14 substitution0:
% 0.77/1.14 end
% 0.77/1.14 permutation0:
% 0.77/1.14 0 ==> 0
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 subsumption: (5) {G0,W11,D2,L4,V1,M4} I { ! lives( X ), X = agatha, X =
% 0.77/1.14 butler, X = charles }.
% 0.77/1.14 parent0: (600) {G0,W11,D2,L4,V1,M4} { ! lives( X ), X = agatha, X = butler
% 0.77/1.14 , X = charles }.
% 0.77/1.14 substitution0:
% 0.77/1.14 X := X
% 0.77/1.14 end
% 0.77/1.14 permutation0:
% 0.77/1.14 0 ==> 0
% 0.77/1.14 1 ==> 1
% 0.77/1.14 2 ==> 2
% 0.77/1.14 3 ==> 3
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 subsumption: (6) {G0,W6,D2,L2,V2,M2} I { ! killed( X, Y ), hates( X, Y )
% 0.77/1.14 }.
% 0.77/1.14 parent0: (601) {G0,W6,D2,L2,V2,M2} { ! killed( X, Y ), hates( X, Y ) }.
% 0.77/1.14 substitution0:
% 0.77/1.14 X := X
% 0.77/1.14 Y := Y
% 0.77/1.14 end
% 0.77/1.14 permutation0:
% 0.77/1.14 0 ==> 0
% 0.77/1.14 1 ==> 1
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 subsumption: (7) {G0,W6,D2,L2,V2,M2} I { ! killed( X, Y ), ! richer( X, Y )
% 0.77/1.14 }.
% 0.77/1.14 parent0: (602) {G0,W6,D2,L2,V2,M2} { ! killed( X, Y ), ! richer( X, Y )
% 0.77/1.14 }.
% 0.77/1.14 substitution0:
% 0.77/1.14 X := X
% 0.77/1.14 Y := Y
% 0.77/1.14 end
% 0.77/1.14 permutation0:
% 0.77/1.14 0 ==> 0
% 0.77/1.14 1 ==> 1
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 subsumption: (8) {G0,W6,D2,L2,V1,M2} I { ! hates( agatha, X ), ! hates(
% 0.77/1.14 charles, X ) }.
% 0.77/1.14 parent0: (603) {G0,W6,D2,L2,V1,M2} { ! hates( agatha, X ), ! hates(
% 0.77/1.14 charles, X ) }.
% 0.77/1.14 substitution0:
% 0.77/1.14 X := X
% 0.77/1.14 end
% 0.77/1.14 permutation0:
% 0.77/1.14 0 ==> 0
% 0.77/1.14 1 ==> 1
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 subsumption: (9) {G0,W6,D2,L2,V1,M2} I { X = butler, hates( agatha, X ) }.
% 0.77/1.14 parent0: (604) {G0,W6,D2,L2,V1,M2} { X = butler, hates( agatha, X ) }.
% 0.77/1.14 substitution0:
% 0.77/1.14 X := X
% 0.77/1.14 end
% 0.77/1.14 permutation0:
% 0.77/1.14 0 ==> 0
% 0.77/1.14 1 ==> 1
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 subsumption: (10) {G0,W6,D2,L2,V1,M2} I { richer( X, agatha ), hates(
% 0.77/1.14 butler, X ) }.
% 0.77/1.14 parent0: (605) {G0,W6,D2,L2,V1,M2} { richer( X, agatha ), hates( butler, X
% 0.77/1.14 ) }.
% 0.77/1.14 substitution0:
% 0.77/1.14 X := X
% 0.77/1.14 end
% 0.77/1.14 permutation0:
% 0.77/1.14 0 ==> 0
% 0.77/1.14 1 ==> 1
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 subsumption: (11) {G0,W6,D2,L2,V1,M2} I { ! hates( agatha, X ), hates(
% 0.77/1.14 butler, X ) }.
% 0.77/1.14 parent0: (606) {G0,W6,D2,L2,V1,M2} { ! hates( agatha, X ), hates( butler,
% 0.77/1.14 X ) }.
% 0.77/1.14 substitution0:
% 0.77/1.14 X := X
% 0.77/1.14 end
% 0.77/1.14 permutation0:
% 0.77/1.14 0 ==> 0
% 0.77/1.14 1 ==> 1
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 subsumption: (12) {G0,W4,D3,L1,V1,M1} I { ! hates( X, skol2( X ) ) }.
% 0.77/1.14 parent0: (607) {G0,W4,D3,L1,V1,M1} { ! hates( X, skol2( X ) ) }.
% 0.77/1.14 substitution0:
% 0.77/1.14 X := X
% 0.77/1.14 end
% 0.77/1.14 permutation0:
% 0.77/1.14 0 ==> 0
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 eqswap: (678) {G0,W3,D2,L1,V0,M1} { ! butler = agatha }.
% 0.77/1.14 parent0[0]: (608) {G0,W3,D2,L1,V0,M1} { ! agatha = butler }.
% 0.77/1.14 substitution0:
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 subsumption: (13) {G0,W3,D2,L1,V0,M1} I { ! butler ==> agatha }.
% 0.77/1.14 parent0: (678) {G0,W3,D2,L1,V0,M1} { ! butler = agatha }.
% 0.77/1.14 substitution0:
% 0.77/1.14 end
% 0.77/1.14 permutation0:
% 0.77/1.14 0 ==> 0
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 subsumption: (14) {G0,W3,D2,L1,V0,M1} I { ! killed( agatha, agatha ) }.
% 0.77/1.14 parent0: (609) {G0,W3,D2,L1,V0,M1} { ! killed( agatha, agatha ) }.
% 0.77/1.14 substitution0:
% 0.77/1.14 end
% 0.77/1.14 permutation0:
% 0.77/1.14 0 ==> 0
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 eqswap: (688) {G0,W11,D2,L4,V1,M4} { agatha = X, ! lives( X ), X = butler
% 0.77/1.14 , X = charles }.
% 0.77/1.14 parent0[1]: (5) {G0,W11,D2,L4,V1,M4} I { ! lives( X ), X = agatha, X =
% 0.77/1.14 butler, X = charles }.
% 0.77/1.14 substitution0:
% 0.77/1.14 X := X
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 resolution: (695) {G1,W9,D2,L3,V0,M3} { agatha = skol1, skol1 = butler,
% 0.77/1.14 skol1 = charles }.
% 0.77/1.14 parent0[1]: (688) {G0,W11,D2,L4,V1,M4} { agatha = X, ! lives( X ), X =
% 0.77/1.14 butler, X = charles }.
% 0.77/1.14 parent1[0]: (0) {G0,W2,D2,L1,V0,M1} I { lives( skol1 ) }.
% 0.77/1.14 substitution0:
% 0.77/1.14 X := skol1
% 0.77/1.14 end
% 0.77/1.14 substitution1:
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 eqswap: (696) {G1,W9,D2,L3,V0,M3} { skol1 = agatha, skol1 = butler, skol1
% 0.77/1.14 = charles }.
% 0.77/1.14 parent0[0]: (695) {G1,W9,D2,L3,V0,M3} { agatha = skol1, skol1 = butler,
% 0.77/1.14 skol1 = charles }.
% 0.77/1.14 substitution0:
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 subsumption: (23) {G1,W9,D2,L3,V0,M3} R(5,0) { skol1 ==> agatha, skol1 ==>
% 0.77/1.14 butler, skol1 ==> charles }.
% 0.77/1.14 parent0: (696) {G1,W9,D2,L3,V0,M3} { skol1 = agatha, skol1 = butler, skol1
% 0.77/1.14 = charles }.
% 0.77/1.14 substitution0:
% 0.77/1.14 end
% 0.77/1.14 permutation0:
% 0.77/1.14 0 ==> 0
% 0.77/1.14 1 ==> 1
% 0.77/1.14 2 ==> 2
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 resolution: (703) {G1,W3,D2,L1,V0,M1} { hates( skol1, agatha ) }.
% 0.77/1.14 parent0[0]: (6) {G0,W6,D2,L2,V2,M2} I { ! killed( X, Y ), hates( X, Y ) }.
% 0.77/1.14 parent1[0]: (1) {G0,W3,D2,L1,V0,M1} I { killed( skol1, agatha ) }.
% 0.77/1.14 substitution0:
% 0.77/1.14 X := skol1
% 0.77/1.14 Y := agatha
% 0.77/1.14 end
% 0.77/1.14 substitution1:
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 subsumption: (66) {G1,W3,D2,L1,V0,M1} R(6,1) { hates( skol1, agatha ) }.
% 0.77/1.14 parent0: (703) {G1,W3,D2,L1,V0,M1} { hates( skol1, agatha ) }.
% 0.77/1.14 substitution0:
% 0.77/1.14 end
% 0.77/1.14 permutation0:
% 0.77/1.14 0 ==> 0
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 resolution: (704) {G1,W4,D3,L1,V0,M1} { ! hates( agatha, skol2( butler ) )
% 0.77/1.14 }.
% 0.77/1.14 parent0[0]: (12) {G0,W4,D3,L1,V1,M1} I { ! hates( X, skol2( X ) ) }.
% 0.77/1.14 parent1[1]: (11) {G0,W6,D2,L2,V1,M2} I { ! hates( agatha, X ), hates(
% 0.77/1.14 butler, X ) }.
% 0.77/1.14 substitution0:
% 0.77/1.14 X := butler
% 0.77/1.14 end
% 0.77/1.14 substitution1:
% 0.77/1.14 X := skol2( butler )
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 subsumption: (78) {G1,W4,D3,L1,V0,M1} R(11,12) { ! hates( agatha, skol2(
% 0.77/1.14 butler ) ) }.
% 0.77/1.14 parent0: (704) {G1,W4,D3,L1,V0,M1} { ! hates( agatha, skol2( butler ) )
% 0.77/1.14 }.
% 0.77/1.14 substitution0:
% 0.77/1.14 end
% 0.77/1.14 permutation0:
% 0.77/1.14 0 ==> 0
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 eqswap: (705) {G0,W6,D2,L2,V1,M2} { butler = X, hates( agatha, X ) }.
% 0.77/1.14 parent0[0]: (9) {G0,W6,D2,L2,V1,M2} I { X = butler, hates( agatha, X ) }.
% 0.77/1.14 substitution0:
% 0.77/1.14 X := X
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 resolution: (706) {G1,W4,D3,L1,V0,M1} { butler = skol2( butler ) }.
% 0.77/1.14 parent0[0]: (78) {G1,W4,D3,L1,V0,M1} R(11,12) { ! hates( agatha, skol2(
% 0.77/1.14 butler ) ) }.
% 0.77/1.14 parent1[1]: (705) {G0,W6,D2,L2,V1,M2} { butler = X, hates( agatha, X ) }.
% 0.77/1.14 substitution0:
% 0.77/1.14 end
% 0.77/1.14 substitution1:
% 0.77/1.14 X := skol2( butler )
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 eqswap: (707) {G1,W4,D3,L1,V0,M1} { skol2( butler ) = butler }.
% 0.77/1.14 parent0[0]: (706) {G1,W4,D3,L1,V0,M1} { butler = skol2( butler ) }.
% 0.77/1.14 substitution0:
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 subsumption: (108) {G2,W4,D3,L1,V0,M1} R(9,78) { skol2( butler ) ==> butler
% 0.77/1.14 }.
% 0.77/1.14 parent0: (707) {G1,W4,D3,L1,V0,M1} { skol2( butler ) = butler }.
% 0.77/1.14 substitution0:
% 0.77/1.14 end
% 0.77/1.14 permutation0:
% 0.77/1.14 0 ==> 0
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 eqswap: (708) {G0,W6,D2,L2,V1,M2} { butler = X, hates( agatha, X ) }.
% 0.77/1.14 parent0[0]: (9) {G0,W6,D2,L2,V1,M2} I { X = butler, hates( agatha, X ) }.
% 0.77/1.14 substitution0:
% 0.77/1.14 X := X
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 eqswap: (709) {G0,W3,D2,L1,V0,M1} { ! agatha ==> butler }.
% 0.77/1.14 parent0[0]: (13) {G0,W3,D2,L1,V0,M1} I { ! butler ==> agatha }.
% 0.77/1.14 substitution0:
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 paramod: (710) {G1,W6,D2,L2,V1,M2} { ! agatha ==> X, hates( agatha, X )
% 0.77/1.14 }.
% 0.77/1.14 parent0[0]: (708) {G0,W6,D2,L2,V1,M2} { butler = X, hates( agatha, X ) }.
% 0.77/1.14 parent1[0; 3]: (709) {G0,W3,D2,L1,V0,M1} { ! agatha ==> butler }.
% 0.77/1.14 substitution0:
% 0.77/1.14 X := X
% 0.77/1.14 end
% 0.77/1.14 substitution1:
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 eqswap: (711) {G1,W6,D2,L2,V1,M2} { ! X ==> agatha, hates( agatha, X ) }.
% 0.77/1.14 parent0[0]: (710) {G1,W6,D2,L2,V1,M2} { ! agatha ==> X, hates( agatha, X )
% 0.77/1.14 }.
% 0.77/1.14 substitution0:
% 0.77/1.14 X := X
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 subsumption: (132) {G1,W6,D2,L2,V1,M2} P(9,13) { ! X = agatha, hates(
% 0.77/1.14 agatha, X ) }.
% 0.77/1.14 parent0: (711) {G1,W6,D2,L2,V1,M2} { ! X ==> agatha, hates( agatha, X )
% 0.77/1.14 }.
% 0.77/1.14 substitution0:
% 0.77/1.14 X := X
% 0.77/1.14 end
% 0.77/1.14 permutation0:
% 0.77/1.14 0 ==> 0
% 0.77/1.14 1 ==> 1
% 0.77/1.14 end
% 0.77/1.14
% 0.77/1.14 eqswap: (712) {G1,W6,D2,L2,V1,M2} { ! agatha = X, hates( agatha, X ) }.
% 0.77/1.16 parent0[0]: (132) {G1,W6,D2,L2,V1,M2} P(9,13) { ! X = agatha, hates( agatha
% 0.77/1.16 , X ) }.
% 0.77/1.16 substitution0:
% 0.77/1.16 X := X
% 0.77/1.16 end
% 0.77/1.16
% 0.77/1.16 eqrefl: (713) {G0,W3,D2,L1,V0,M1} { hates( agatha, agatha ) }.
% 0.77/1.16 parent0[0]: (712) {G1,W6,D2,L2,V1,M2} { ! agatha = X, hates( agatha, X )
% 0.77/1.16 }.
% 0.77/1.16 substitution0:
% 0.77/1.16 X := agatha
% 0.77/1.16 end
% 0.77/1.16
% 0.77/1.16 subsumption: (136) {G2,W3,D2,L1,V0,M1} Q(132) { hates( agatha, agatha ) }.
% 0.77/1.16 parent0: (713) {G0,W3,D2,L1,V0,M1} { hates( agatha, agatha ) }.
% 0.77/1.16 substitution0:
% 0.77/1.16 end
% 0.77/1.16 permutation0:
% 0.77/1.16 0 ==> 0
% 0.77/1.16 end
% 0.77/1.16
% 0.77/1.16 resolution: (714) {G1,W3,D2,L1,V0,M1} { ! hates( charles, agatha ) }.
% 0.77/1.16 parent0[0]: (8) {G0,W6,D2,L2,V1,M2} I { ! hates( agatha, X ), ! hates(
% 0.77/1.16 charles, X ) }.
% 0.77/1.16 parent1[0]: (136) {G2,W3,D2,L1,V0,M1} Q(132) { hates( agatha, agatha ) }.
% 0.77/1.16 substitution0:
% 0.77/1.16 X := agatha
% 0.77/1.16 end
% 0.77/1.16 substitution1:
% 0.77/1.16 end
% 0.77/1.16
% 0.77/1.16 subsumption: (150) {G3,W3,D2,L1,V0,M1} R(136,8) { ! hates( charles, agatha
% 0.77/1.16 ) }.
% 0.77/1.16 parent0: (714) {G1,W3,D2,L1,V0,M1} { ! hates( charles, agatha ) }.
% 0.77/1.16 substitution0:
% 0.77/1.16 end
% 0.77/1.16 permutation0:
% 0.77/1.16 0 ==> 0
% 0.77/1.16 end
% 0.77/1.16
% 0.77/1.16 resolution: (716) {G1,W4,D3,L1,V0,M1} { richer( skol2( butler ), agatha )
% 0.77/1.16 }.
% 0.77/1.16 parent0[0]: (12) {G0,W4,D3,L1,V1,M1} I { ! hates( X, skol2( X ) ) }.
% 0.77/1.16 parent1[1]: (10) {G0,W6,D2,L2,V1,M2} I { richer( X, agatha ), hates( butler
% 0.77/1.16 , X ) }.
% 0.77/1.16 substitution0:
% 0.77/1.16 X := butler
% 0.77/1.16 end
% 0.77/1.16 substitution1:
% 0.77/1.16 X := skol2( butler )
% 0.77/1.16 end
% 0.77/1.16
% 0.77/1.16 paramod: (717) {G2,W3,D2,L1,V0,M1} { richer( butler, agatha ) }.
% 0.77/1.16 parent0[0]: (108) {G2,W4,D3,L1,V0,M1} R(9,78) { skol2( butler ) ==> butler
% 0.77/1.16 }.
% 0.77/1.16 parent1[0; 1]: (716) {G1,W4,D3,L1,V0,M1} { richer( skol2( butler ), agatha
% 0.77/1.16 ) }.
% 0.77/1.16 substitution0:
% 0.77/1.16 end
% 0.77/1.16 substitution1:
% 0.77/1.16 end
% 0.77/1.16
% 0.77/1.16 subsumption: (164) {G3,W3,D2,L1,V0,M1} R(10,12);d(108) { richer( butler,
% 0.77/1.16 agatha ) }.
% 0.77/1.16 parent0: (717) {G2,W3,D2,L1,V0,M1} { richer( butler, agatha ) }.
% 0.77/1.16 substitution0:
% 0.77/1.16 end
% 0.77/1.16 permutation0:
% 0.77/1.16 0 ==> 0
% 0.77/1.16 end
% 0.77/1.16
% 0.77/1.16 resolution: (718) {G1,W3,D2,L1,V0,M1} { ! killed( butler, agatha ) }.
% 0.77/1.16 parent0[1]: (7) {G0,W6,D2,L2,V2,M2} I { ! killed( X, Y ), ! richer( X, Y )
% 0.77/1.16 }.
% 0.77/1.16 parent1[0]: (164) {G3,W3,D2,L1,V0,M1} R(10,12);d(108) { richer( butler,
% 0.77/1.16 agatha ) }.
% 0.77/1.16 substitution0:
% 0.77/1.16 X := butler
% 0.77/1.16 Y := agatha
% 0.77/1.16 end
% 0.77/1.16 substitution1:
% 0.77/1.16 end
% 0.77/1.16
% 0.77/1.16 subsumption: (176) {G4,W3,D2,L1,V0,M1} R(164,7) { ! killed( butler, agatha
% 0.77/1.16 ) }.
% 0.77/1.16 parent0: (718) {G1,W3,D2,L1,V0,M1} { ! killed( butler, agatha ) }.
% 0.77/1.16 substitution0:
% 0.77/1.16 end
% 0.77/1.16 permutation0:
% 0.77/1.16 0 ==> 0
% 0.77/1.16 end
% 0.77/1.16
% 0.77/1.16 eqswap: (719) {G0,W6,D2,L2,V1,M2} { butler = X, hates( agatha, X ) }.
% 0.77/1.16 parent0[0]: (9) {G0,W6,D2,L2,V1,M2} I { X = butler, hates( agatha, X ) }.
% 0.77/1.16 substitution0:
% 0.77/1.16 X := X
% 0.77/1.16 end
% 0.77/1.16
% 0.77/1.16 paramod: (720) {G1,W6,D2,L2,V1,M2} { ! killed( X, agatha ), hates( agatha
% 0.77/1.16 , X ) }.
% 0.77/1.16 parent0[0]: (719) {G0,W6,D2,L2,V1,M2} { butler = X, hates( agatha, X ) }.
% 0.77/1.16 parent1[0; 2]: (176) {G4,W3,D2,L1,V0,M1} R(164,7) { ! killed( butler,
% 0.77/1.16 agatha ) }.
% 0.77/1.16 substitution0:
% 0.77/1.16 X := X
% 0.77/1.16 end
% 0.77/1.16 substitution1:
% 0.77/1.16 end
% 0.77/1.16
% 0.77/1.16 subsumption: (182) {G5,W6,D2,L2,V1,M2} P(9,176) { ! killed( X, agatha ),
% 0.77/1.16 hates( agatha, X ) }.
% 0.77/1.16 parent0: (720) {G1,W6,D2,L2,V1,M2} { ! killed( X, agatha ), hates( agatha
% 0.77/1.16 , X ) }.
% 0.77/1.16 substitution0:
% 0.77/1.16 X := X
% 0.77/1.16 end
% 0.77/1.16 permutation0:
% 0.77/1.16 0 ==> 0
% 0.77/1.16 1 ==> 1
% 0.77/1.16 end
% 0.77/1.16
% 0.77/1.16 paramod: (722) {G2,W3,D2,L1,V0,M1} { ! hates( agatha, butler ) }.
% 0.77/1.16 parent0[0]: (108) {G2,W4,D3,L1,V0,M1} R(9,78) { skol2( butler ) ==> butler
% 0.77/1.16 }.
% 0.77/1.16 parent1[0; 3]: (78) {G1,W4,D3,L1,V0,M1} R(11,12) { ! hates( agatha, skol2(
% 0.77/1.16 butler ) ) }.
% 0.77/1.16 substitution0:
% 0.77/1.16 end
% 0.77/1.16 substitution1:
% 0.77/1.16 end
% 0.77/1.16
% 0.77/1.16 subsumption: (195) {G3,W3,D2,L1,V0,M1} P(108,78) { ! hates( agatha, butler
% 0.77/1.16 ) }.
% 0.77/1.16 parent0: (722) {G2,W3,D2,L1,V0,M1} { ! hates( agatha, butler ) }.
% 0.77/1.16 substitution0:
% 0.77/1.16 end
% 0.77/1.16 permutation0:
% 0.77/1.16 0 ==> 0
% 0.77/1.16 end
% 0.77/1.16
% 0.77/1.16 *** allocated 15000 integers for termspace/termends
% 0.77/1.16 eqswap: (724) {G1,W9,D2,L3,V0,M3} { butler ==> skol1, skol1 ==> agatha,
% 0.77/1.16 skol1 ==> charles }.
% 0.77/1.16 parent0[1]: (23) {G1,W9,D2,L3,V0,M3} R(5,0) { skol1 ==> agatha, skol1 ==>
% 0.77/1.16 butler, skol1 ==> charles }.
% 0.77/1.16 substitution0:
% 0.77/1.16 end
% 0.77/1.16
% 0.77/1.16 paramod: (811) {G1,W9,D2,L3,V0,M3} { killed( agatha, agatha ), butler ==>
% 0.77/1.16 skol1, skol1 ==> charles }.
% 0.77/1.16 parent0[1]: (724) {G1,W9,D2,L3,V0,M3} { butler ==> skol1, skol1 ==> agatha
% 0.77/1.16 , skol1 ==> charles }.
% 0.77/1.16 parent1[0; 1]: (1) {G0,W3,D2,L1,V0,M1} I { killed( skol1, agatha ) }.
% 0.77/1.16 substitution0:
% 0.77/1.16 end
% 0.77/1.16 substitution1:
% 0.77/1.16 end
% 0.77/1.16
% 0.77/1.16 resolution: (892) {G1,W6,D2,L2,V0,M2} { butler ==> skol1, skol1 ==>
% 1.93/2.34 charles }.
% 1.93/2.34 parent0[0]: (14) {G0,W3,D2,L1,V0,M1} I { ! killed( agatha, agatha ) }.
% 1.93/2.34 parent1[0]: (811) {G1,W9,D2,L3,V0,M3} { killed( agatha, agatha ), butler
% 1.93/2.34 ==> skol1, skol1 ==> charles }.
% 1.93/2.34 substitution0:
% 1.93/2.34 end
% 1.93/2.34 substitution1:
% 1.93/2.34 end
% 1.93/2.34
% 1.93/2.34 eqswap: (893) {G1,W6,D2,L2,V0,M2} { skol1 ==> butler, skol1 ==> charles
% 1.93/2.34 }.
% 1.93/2.34 parent0[0]: (892) {G1,W6,D2,L2,V0,M2} { butler ==> skol1, skol1 ==>
% 1.93/2.34 charles }.
% 1.93/2.34 substitution0:
% 1.93/2.34 end
% 1.93/2.34
% 1.93/2.34 subsumption: (301) {G2,W6,D2,L2,V0,M2} P(23,1);r(14) { skol1 ==> butler,
% 1.93/2.34 skol1 ==> charles }.
% 1.93/2.34 parent0: (893) {G1,W6,D2,L2,V0,M2} { skol1 ==> butler, skol1 ==> charles
% 1.93/2.34 }.
% 1.93/2.34 substitution0:
% 1.93/2.34 end
% 1.93/2.34 permutation0:
% 1.93/2.34 0 ==> 0
% 1.93/2.34 1 ==> 1
% 1.93/2.34 end
% 1.93/2.34
% 1.93/2.34 resolution: (896) {G1,W3,D2,L1,V0,M1} { hates( agatha, skol1 ) }.
% 1.93/2.34 parent0[0]: (182) {G5,W6,D2,L2,V1,M2} P(9,176) { ! killed( X, agatha ),
% 1.93/2.34 hates( agatha, X ) }.
% 1.93/2.34 parent1[0]: (1) {G0,W3,D2,L1,V0,M1} I { killed( skol1, agatha ) }.
% 1.93/2.34 substitution0:
% 1.93/2.34 X := skol1
% 1.93/2.34 end
% 1.93/2.34 substitution1:
% 1.93/2.34 end
% 1.93/2.34
% 1.93/2.34 subsumption: (306) {G6,W3,D2,L1,V0,M1} R(182,1) { hates( agatha, skol1 )
% 1.93/2.34 }.
% 1.93/2.34 parent0: (896) {G1,W3,D2,L1,V0,M1} { hates( agatha, skol1 ) }.
% 1.93/2.34 substitution0:
% 1.93/2.34 end
% 1.93/2.34 permutation0:
% 1.93/2.34 0 ==> 0
% 1.93/2.34 end
% 1.93/2.34
% 1.93/2.34 *** allocated 22500 integers for termspace/termends
% 1.93/2.34 *** allocated 50625 integers for clauses
% 1.93/2.34 eqswap: (897) {G1,W9,D2,L3,V0,M3} { agatha ==> skol1, skol1 ==> butler,
% 1.93/2.34 skol1 ==> charles }.
% 1.93/2.34 parent0[0]: (23) {G1,W9,D2,L3,V0,M3} R(5,0) { skol1 ==> agatha, skol1 ==>
% 1.93/2.34 butler, skol1 ==> charles }.
% 1.93/2.34 substitution0:
% 1.93/2.34 end
% 1.93/2.34
% 1.93/2.34 eqswap: (905) {G2,W6,D2,L2,V0,M2} { charles ==> skol1, skol1 ==> butler
% 1.93/2.34 }.
% 1.93/2.34 parent0[1]: (301) {G2,W6,D2,L2,V0,M2} P(23,1);r(14) { skol1 ==> butler,
% 1.93/2.34 skol1 ==> charles }.
% 1.93/2.34 substitution0:
% 1.93/2.34 end
% 1.93/2.34
% 1.93/2.34 paramod: (907) {G2,W9,D2,L3,V0,M3} { hates( agatha, butler ), agatha ==>
% 1.93/2.34 skol1, skol1 ==> charles }.
% 1.93/2.34 parent0[1]: (897) {G1,W9,D2,L3,V0,M3} { agatha ==> skol1, skol1 ==> butler
% 1.93/2.34 , skol1 ==> charles }.
% 1.93/2.34 parent1[0; 2]: (306) {G6,W3,D2,L1,V0,M1} R(182,1) { hates( agatha, skol1 )
% 1.93/2.34 }.
% 1.93/2.34 substitution0:
% 1.93/2.34 end
% 1.93/2.34 substitution1:
% 1.93/2.34 end
% 1.93/2.34
% 1.93/2.34 paramod: (12860) {G3,W12,D2,L4,V0,M4} { agatha ==> butler, charles ==>
% 1.93/2.34 skol1, hates( agatha, butler ), skol1 ==> charles }.
% 1.93/2.34 parent0[1]: (905) {G2,W6,D2,L2,V0,M2} { charles ==> skol1, skol1 ==>
% 1.93/2.34 butler }.
% 1.93/2.34 parent1[1; 2]: (907) {G2,W9,D2,L3,V0,M3} { hates( agatha, butler ), agatha
% 1.93/2.34 ==> skol1, skol1 ==> charles }.
% 1.93/2.34 substitution0:
% 1.93/2.34 end
% 1.93/2.34 substitution1:
% 1.93/2.34 end
% 1.93/2.34
% 1.93/2.34 resolution: (13112) {G4,W9,D2,L3,V0,M3} { agatha ==> butler, charles ==>
% 1.93/2.34 skol1, skol1 ==> charles }.
% 1.93/2.34 parent0[0]: (195) {G3,W3,D2,L1,V0,M1} P(108,78) { ! hates( agatha, butler )
% 1.93/2.34 }.
% 1.93/2.34 parent1[2]: (12860) {G3,W12,D2,L4,V0,M4} { agatha ==> butler, charles ==>
% 1.93/2.34 skol1, hates( agatha, butler ), skol1 ==> charles }.
% 1.93/2.34 substitution0:
% 1.93/2.34 end
% 1.93/2.34 substitution1:
% 1.93/2.34 end
% 1.93/2.34
% 1.93/2.34 eqswap: (13114) {G4,W9,D2,L3,V0,M3} { skol1 ==> charles, agatha ==> butler
% 1.93/2.34 , skol1 ==> charles }.
% 1.93/2.34 parent0[1]: (13112) {G4,W9,D2,L3,V0,M3} { agatha ==> butler, charles ==>
% 1.93/2.34 skol1, skol1 ==> charles }.
% 1.93/2.34 substitution0:
% 1.93/2.34 end
% 1.93/2.34
% 1.93/2.34 eqswap: (13117) {G4,W9,D2,L3,V0,M3} { butler ==> agatha, skol1 ==> charles
% 1.93/2.34 , skol1 ==> charles }.
% 1.93/2.34 parent0[1]: (13114) {G4,W9,D2,L3,V0,M3} { skol1 ==> charles, agatha ==>
% 1.93/2.34 butler, skol1 ==> charles }.
% 1.93/2.34 substitution0:
% 1.93/2.34 end
% 1.93/2.34
% 1.93/2.34 factor: (13118) {G4,W6,D2,L2,V0,M2} { butler ==> agatha, skol1 ==> charles
% 1.93/2.34 }.
% 1.93/2.34 parent0[1, 2]: (13117) {G4,W9,D2,L3,V0,M3} { butler ==> agatha, skol1 ==>
% 1.93/2.34 charles, skol1 ==> charles }.
% 1.93/2.34 substitution0:
% 1.93/2.34 end
% 1.93/2.34
% 1.93/2.34 subsumption: (309) {G7,W6,D2,L2,V0,M2} P(23,306);d(301);r(195) { skol1 ==>
% 1.93/2.34 charles, butler ==> agatha }.
% 1.93/2.34 parent0: (13118) {G4,W6,D2,L2,V0,M2} { butler ==> agatha, skol1 ==>
% 1.93/2.34 charles }.
% 1.93/2.34 substitution0:
% 1.93/2.34 end
% 1.93/2.34 permutation0:
% 1.93/2.34 0 ==> 1
% 1.93/2.34 1 ==> 0
% 1.93/2.34 end
% 1.93/2.34
% 1.93/2.34 resolution: (13126) {G1,W3,D2,L1,V0,M1} { skol1 ==> charles }.
% 1.93/2.34 parent0[0]: (13) {G0,W3,D2,L1,V0,M1} I { ! butler ==> agatha }.
% 1.93/2.34 parent1[1]: (309) {G7,W6,D2,L2,V0,M2} P(23,306);d(301);r(195) { skol1 ==>
% 1.93/2.34 charles, butler ==> agatha }.
% 1.93/2.34 substitution0:
% 1.93/2.34 end
% 1.93/2.34 substitution1:
% 1.93/2.34 end
% 1.93/2.34
% 1.93/2.34 subsumption: (591) {G8,W3,D2,L1,V0,M1} S(309);r(13) { skol1 ==> charles }.
% 1.93/2.34 parent0: (13126) {G1,W3,D2,L1,V0,M1} { skol1 ==> charles }.
% 1.93/2.34 substitution0:
% 1.93/2.34 end
% 1.93/2.34 permutation0:
% 1.93/2.34 0 ==> 0
% 1.93/2.34 end
% 1.93/2.34
% 1.93/2.34 paramod: (13129) {G2,W3,D2,L1,V0,M1} { hates( charles, agatha ) }.
% 1.93/2.34 parent0[0]: (591) {G8,W3,D2,L1,V0,M1} S(309);r(13) { skol1 ==> charles }.
% 1.93/2.34 parent1[0; 1]: (66) {G1,W3,D2,L1,V0,M1} R(6,1) { hates( skol1, agatha ) }.
% 1.93/2.34 substitution0:
% 1.93/2.34 end
% 1.93/2.34 substitution1:
% 1.93/2.34 end
% 1.93/2.34
% 1.93/2.34 resolution: (13130) {G3,W0,D0,L0,V0,M0} { }.
% 1.93/2.34 parent0[0]: (150) {G3,W3,D2,L1,V0,M1} R(136,8) { ! hates( charles, agatha )
% 1.93/2.34 }.
% 1.93/2.34 parent1[0]: (13129) {G2,W3,D2,L1,V0,M1} { hates( charles, agatha ) }.
% 1.93/2.34 substitution0:
% 1.93/2.34 end
% 1.93/2.34 substitution1:
% 1.93/2.34 end
% 1.93/2.34
% 1.93/2.34 subsumption: (593) {G9,W0,D0,L0,V0,M0} P(591,66);r(150) { }.
% 1.93/2.34 parent0: (13130) {G3,W0,D0,L0,V0,M0} { }.
% 1.93/2.34 substitution0:
% 1.93/2.34 end
% 1.93/2.34 permutation0:
% 1.93/2.34 end
% 1.93/2.34
% 1.93/2.34 Proof check complete!
% 1.93/2.34
% 1.93/2.34 Memory use:
% 1.93/2.34
% 1.93/2.34 space for terms: 7636
% 1.93/2.34 space for clauses: 23188
% 1.93/2.34
% 1.93/2.34
% 1.93/2.34 clauses generated: 9516
% 1.93/2.34 clauses kept: 594
% 1.93/2.34 clauses selected: 95
% 1.93/2.34 clauses deleted: 18
% 1.93/2.34 clauses inuse deleted: 0
% 1.93/2.34
% 1.93/2.34 subsentry: 514590
% 1.93/2.34 literals s-matched: 450742
% 1.93/2.34 literals matched: 450519
% 1.93/2.34 full subsumption: 699
% 1.93/2.34
% 1.93/2.34 checksum: -1501394341
% 1.93/2.34
% 1.93/2.34
% 1.93/2.34 Bliksem ended
%------------------------------------------------------------------------------