%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWV399+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n020.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 : Wed Jul 20 16:24:44 EDT 2022
% Result : Theorem 0.81s 1.29s
% Output : Refutation 0.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SWV399+1 : TPTP v8.1.0. Released v3.3.0.
% 0.07/0.14 % Command : bliksem %s
% 0.15/0.35 % Computer : n020.cluster.edu
% 0.15/0.35 % Model : x86_64 x86_64
% 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.35 % Memory : 8042.1875MB
% 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.35 % CPULimit : 300
% 0.15/0.36 % DateTime : Wed Jun 15 18:16:49 EDT 2022
% 0.15/0.36 % CPUTime :
% 0.81/1.29 *** allocated 10000 integers for termspace/termends
% 0.81/1.29 *** allocated 10000 integers for clauses
% 0.81/1.29 *** allocated 10000 integers for justifications
% 0.81/1.29 Bliksem 1.12
% 0.81/1.29
% 0.81/1.29
% 0.81/1.29 Automatic Strategy Selection
% 0.81/1.29
% 0.81/1.29
% 0.81/1.29 Clauses:
% 0.81/1.29
% 0.81/1.29 { ! less_than( X, Z ), ! less_than( Z, Y ), less_than( X, Y ) }.
% 0.81/1.29 { less_than( X, Y ), less_than( Y, X ) }.
% 0.81/1.29 { less_than( X, X ) }.
% 0.81/1.29 { ! strictly_less_than( X, Y ), less_than( X, Y ) }.
% 0.81/1.29 { ! strictly_less_than( X, Y ), ! less_than( Y, X ) }.
% 0.81/1.29 { ! less_than( X, Y ), less_than( Y, X ), strictly_less_than( X, Y ) }.
% 0.81/1.29 { less_than( bottom, X ) }.
% 0.81/1.29 { ! isnonempty_slb( create_slb ) }.
% 0.81/1.29 { isnonempty_slb( insert_slb( X, pair( Y, Z ) ) ) }.
% 0.81/1.29 { ! contains_slb( create_slb, X ) }.
% 0.81/1.29 { ! contains_slb( insert_slb( X, pair( Y, T ) ), Z ), contains_slb( X, Z )
% 0.81/1.29 , Y = Z }.
% 0.81/1.29 { ! contains_slb( X, Z ), contains_slb( insert_slb( X, pair( Y, T ) ), Z )
% 0.81/1.29 }.
% 0.81/1.29 { ! Y = Z, contains_slb( insert_slb( X, pair( Y, T ) ), Z ) }.
% 0.81/1.29 { ! pair_in_list( create_slb, X, Y ) }.
% 0.81/1.29 { ! pair_in_list( insert_slb( X, pair( Y, T ) ), Z, U ), pair_in_list( X, Z
% 0.81/1.29 , U ), alpha1( Y, Z, T, U ) }.
% 0.81/1.29 { ! pair_in_list( X, Z, U ), pair_in_list( insert_slb( X, pair( Y, T ) ), Z
% 0.81/1.29 , U ) }.
% 0.81/1.29 { ! alpha1( Y, Z, T, U ), pair_in_list( insert_slb( X, pair( Y, T ) ), Z, U
% 0.81/1.29 ) }.
% 0.81/1.29 { ! alpha1( X, Y, Z, T ), X = Y }.
% 0.81/1.29 { ! alpha1( X, Y, Z, T ), Z = T }.
% 0.81/1.29 { ! X = Y, ! Z = T, alpha1( X, Y, Z, T ) }.
% 0.81/1.29 { remove_slb( insert_slb( X, pair( Y, Z ) ), Y ) = X }.
% 0.81/1.29 { Y = Z, ! contains_slb( X, Z ), remove_slb( insert_slb( X, pair( Y, T ) )
% 0.81/1.29 , Z ) = insert_slb( remove_slb( X, Z ), pair( Y, T ) ) }.
% 0.81/1.29 { lookup_slb( insert_slb( X, pair( Y, Z ) ), Y ) = Z }.
% 0.81/1.29 { Y = Z, ! contains_slb( X, Z ), lookup_slb( insert_slb( X, pair( Y, T ) )
% 0.81/1.29 , Z ) = lookup_slb( X, Z ) }.
% 0.81/1.29 { update_slb( create_slb, X ) = create_slb }.
% 0.81/1.29 { ! strictly_less_than( Y, X ), update_slb( insert_slb( Z, pair( T, Y ) ),
% 0.81/1.29 X ) = insert_slb( update_slb( Z, X ), pair( T, X ) ) }.
% 0.81/1.29 { ! less_than( X, Y ), update_slb( insert_slb( Z, pair( T, Y ) ), X ) =
% 0.81/1.29 insert_slb( update_slb( Z, X ), pair( T, Y ) ) }.
% 0.81/1.29 { ! pair_in_list( X, Y, Z ), ! less_than( T, Z ), pair_in_list( update_slb
% 0.81/1.29 ( X, T ), Y, Z ) }.
% 0.81/1.29 { ! pair_in_list( X, Y, T ), ! strictly_less_than( T, Z ), pair_in_list(
% 0.81/1.29 update_slb( X, Z ), Y, Z ) }.
% 0.81/1.29 { pair_in_list( skol1, skol2, skol3 ) }.
% 0.81/1.29 { strictly_less_than( skol2, skol3 ) }.
% 0.81/1.29 { ! pair_in_list( update_slb( skol1, skol4 ), X, Y ), ! strictly_less_than
% 0.81/1.29 ( X, Y ) }.
% 0.81/1.29
% 0.81/1.29 percentage equality = 0.241935, percentage horn = 0.812500
% 0.81/1.29 This is a problem with some equality
% 0.81/1.29
% 0.81/1.29
% 0.81/1.29
% 0.81/1.29 Options Used:
% 0.81/1.29
% 0.81/1.29 useres = 1
% 0.81/1.29 useparamod = 1
% 0.81/1.29 useeqrefl = 1
% 0.81/1.29 useeqfact = 1
% 0.81/1.29 usefactor = 1
% 0.81/1.29 usesimpsplitting = 0
% 0.81/1.29 usesimpdemod = 5
% 0.81/1.29 usesimpres = 3
% 0.81/1.29
% 0.81/1.29 resimpinuse = 1000
% 0.81/1.29 resimpclauses = 20000
% 0.81/1.29 substype = eqrewr
% 0.81/1.29 backwardsubs = 1
% 0.81/1.29 selectoldest = 5
% 0.81/1.29
% 0.81/1.29 litorderings [0] = split
% 0.81/1.29 litorderings [1] = extend the termordering, first sorting on arguments
% 0.81/1.29
% 0.81/1.29 termordering = kbo
% 0.81/1.29
% 0.81/1.29 litapriori = 0
% 0.81/1.29 termapriori = 1
% 0.81/1.29 litaposteriori = 0
% 0.81/1.29 termaposteriori = 0
% 0.81/1.29 demodaposteriori = 0
% 0.81/1.29 ordereqreflfact = 0
% 0.81/1.29
% 0.81/1.29 litselect = negord
% 0.81/1.29
% 0.81/1.29 maxweight = 15
% 0.81/1.29 maxdepth = 30000
% 0.81/1.29 maxlength = 115
% 0.81/1.29 maxnrvars = 195
% 0.81/1.29 excuselevel = 1
% 0.81/1.29 increasemaxweight = 1
% 0.81/1.29
% 0.81/1.29 maxselected = 10000000
% 0.81/1.29 maxnrclauses = 10000000
% 0.81/1.29
% 0.81/1.29 showgenerated = 0
% 0.81/1.29 showkept = 0
% 0.81/1.29 showselected = 0
% 0.81/1.29 showdeleted = 0
% 0.81/1.29 showresimp = 1
% 0.81/1.29 showstatus = 2000
% 0.81/1.29
% 0.81/1.29 prologoutput = 0
% 0.81/1.29 nrgoals = 5000000
% 0.81/1.29 totalproof = 1
% 0.81/1.29
% 0.81/1.29 Symbols occurring in the translation:
% 0.81/1.29
% 0.81/1.29 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.81/1.29 . [1, 2] (w:1, o:24, a:1, s:1, b:0),
% 0.81/1.29 ! [4, 1] (w:0, o:18, a:1, s:1, b:0),
% 0.81/1.29 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.81/1.29 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.81/1.29 less_than [38, 2] (w:1, o:48, a:1, s:1, b:0),
% 0.81/1.29 strictly_less_than [39, 2] (w:1, o:50, a:1, s:1, b:0),
% 0.81/1.29 bottom [40, 0] (w:1, o:9, a:1, s:1, b:0),
% 0.81/1.29 create_slb [41, 0] (w:1, o:10, a:1, s:1, b:0),
% 0.81/1.29 isnonempty_slb [42, 1] (w:1, o:23, a:1, s:1, b:0),
% 0.81/1.29 pair [43, 2] (w:1, o:51, a:1, s:1, b:0),
% 0.81/1.29 insert_slb [44, 2] (w:1, o:52, a:1, s:1, b:0),
% 0.81/1.29 contains_slb [45, 2] (w:1, o:53, a:1, s:1, b:0),
% 0.81/1.29 pair_in_list [47, 3] (w:1, o:56, a:1, s:1, b:0),
% 0.81/1.29 remove_slb [49, 2] (w:1, o:49, a:1, s:1, b:0),
% 0.81/1.29 lookup_slb [50, 2] (w:1, o:54, a:1, s:1, b:0),
% 0.81/1.29 update_slb [51, 2] (w:1, o:55, a:1, s:1, b:0),
% 0.81/1.29 alpha1 [53, 4] (w:1, o:57, a:1, s:1, b:1),
% 0.81/1.29 skol1 [54, 0] (w:1, o:14, a:1, s:1, b:1),
% 0.81/1.29 skol2 [55, 0] (w:1, o:15, a:1, s:1, b:1),
% 0.81/1.29 skol3 [56, 0] (w:1, o:16, a:1, s:1, b:1),
% 0.81/1.29 skol4 [57, 0] (w:1, o:17, a:1, s:1, b:1).
% 0.81/1.29
% 0.81/1.29
% 0.81/1.29 Starting Search:
% 0.81/1.29
% 0.81/1.29 *** allocated 15000 integers for clauses
% 0.81/1.29 *** allocated 22500 integers for clauses
% 0.81/1.29 *** allocated 33750 integers for clauses
% 0.81/1.29 *** allocated 15000 integers for termspace/termends
% 0.81/1.29 *** allocated 50625 integers for clauses
% 0.81/1.29 *** allocated 22500 integers for termspace/termends
% 0.81/1.29 Resimplifying inuse:
% 0.81/1.29 Done
% 0.81/1.29
% 0.81/1.29 *** allocated 75937 integers for clauses
% 0.81/1.29 *** allocated 33750 integers for termspace/termends
% 0.81/1.29 *** allocated 113905 integers for clauses
% 0.81/1.29 *** allocated 50625 integers for termspace/termends
% 0.81/1.29
% 0.81/1.29 Intermediate Status:
% 0.81/1.29 Generated: 8367
% 0.81/1.29 Kept: 2375
% 0.81/1.29 Inuse: 173
% 0.81/1.29 Deleted: 3
% 0.81/1.29 Deletedinuse: 0
% 0.81/1.29
% 0.81/1.29 Resimplifying inuse:
% 0.81/1.29 Done
% 0.81/1.29
% 0.81/1.29
% 0.81/1.29 Bliksems!, er is een bewijs:
% 0.81/1.29 % SZS status Theorem
% 0.81/1.29 % SZS output start Refutation
% 0.81/1.29
% 0.81/1.29 (0) {G0,W9,D2,L3,V3,M3} I { ! less_than( X, Z ), ! less_than( Z, Y ),
% 0.81/1.29 less_than( X, Y ) }.
% 0.81/1.29 (1) {G0,W6,D2,L2,V2,M2} I { less_than( X, Y ), less_than( Y, X ) }.
% 0.81/1.29 (3) {G0,W6,D2,L2,V2,M2} I { ! strictly_less_than( X, Y ), less_than( X, Y )
% 0.81/1.29 }.
% 0.81/1.29 (4) {G0,W6,D2,L2,V2,M2} I { ! strictly_less_than( X, Y ), ! less_than( Y, X
% 0.81/1.29 ) }.
% 0.81/1.29 (5) {G1,W6,D2,L2,V2,M2} I;r(1) { less_than( Y, X ), strictly_less_than( X,
% 0.81/1.29 Y ) }.
% 0.81/1.29 (27) {G0,W13,D3,L3,V4,M3} I { ! pair_in_list( X, Y, Z ), ! less_than( T, Z
% 0.81/1.29 ), pair_in_list( update_slb( X, T ), Y, Z ) }.
% 0.81/1.29 (28) {G0,W13,D3,L3,V4,M3} I { ! pair_in_list( X, Y, T ), !
% 0.81/1.29 strictly_less_than( T, Z ), pair_in_list( update_slb( X, Z ), Y, Z ) }.
% 0.81/1.29 (29) {G0,W4,D2,L1,V0,M1} I { pair_in_list( skol1, skol2, skol3 ) }.
% 0.81/1.29 (30) {G0,W3,D2,L1,V0,M1} I { strictly_less_than( skol2, skol3 ) }.
% 0.81/1.29 (31) {G0,W9,D3,L2,V2,M2} I { ! pair_in_list( update_slb( skol1, skol4 ), X
% 0.81/1.29 , Y ), ! strictly_less_than( X, Y ) }.
% 0.81/1.29 (48) {G1,W3,D2,L1,V0,M1} R(4,30) { ! less_than( skol3, skol2 ) }.
% 0.81/1.29 (60) {G2,W6,D2,L2,V1,M2} R(48,0) { ! less_than( skol3, X ), ! less_than( X
% 0.81/1.29 , skol2 ) }.
% 0.81/1.29 (128) {G3,W6,D2,L2,V1,M2} R(60,3) { ! less_than( X, skol2 ), !
% 0.81/1.29 strictly_less_than( skol3, X ) }.
% 0.81/1.29 (134) {G4,W6,D2,L2,V1,M2} R(128,5) { ! strictly_less_than( skol3, X ),
% 0.81/1.29 strictly_less_than( skol2, X ) }.
% 0.81/1.29 (151) {G5,W6,D2,L2,V1,M2} R(134,5) { strictly_less_than( skol2, X ),
% 0.81/1.29 less_than( X, skol3 ) }.
% 0.81/1.29 (1099) {G1,W6,D3,L1,V0,M1} R(31,30) { ! pair_in_list( update_slb( skol1,
% 0.81/1.29 skol4 ), skol2, skol3 ) }.
% 0.81/1.29 (1153) {G2,W3,D2,L1,V0,M1} R(1099,27);r(29) { ! less_than( skol4, skol3 )
% 0.81/1.29 }.
% 0.81/1.29 (1181) {G6,W3,D2,L1,V0,M1} R(1153,151) { strictly_less_than( skol2, skol4 )
% 0.81/1.29 }.
% 0.81/1.29 (1186) {G3,W3,D2,L1,V0,M1} R(1153,5) { strictly_less_than( skol3, skol4 )
% 0.81/1.29 }.
% 0.81/1.29 (1226) {G7,W6,D3,L1,V0,M1} R(1181,31) { ! pair_in_list( update_slb( skol1,
% 0.81/1.29 skol4 ), skol2, skol4 ) }.
% 0.81/1.29 (2627) {G8,W7,D2,L2,V1,M2} R(1226,28) { ! pair_in_list( skol1, skol2, X ),
% 0.81/1.29 ! strictly_less_than( X, skol4 ) }.
% 0.81/1.29 (2696) {G9,W0,D0,L0,V0,M0} R(2627,1186);r(29) { }.
% 0.81/1.29
% 0.81/1.29
% 0.81/1.29 % SZS output end Refutation
% 0.81/1.29 found a proof!
% 0.81/1.29
% 0.81/1.29
% 0.81/1.29 Unprocessed initial clauses:
% 0.81/1.29
% 0.81/1.29 (2698) {G0,W9,D2,L3,V3,M3} { ! less_than( X, Z ), ! less_than( Z, Y ),
% 0.81/1.29 less_than( X, Y ) }.
% 0.81/1.29 (2699) {G0,W6,D2,L2,V2,M2} { less_than( X, Y ), less_than( Y, X ) }.
% 0.81/1.29 (2700) {G0,W3,D2,L1,V1,M1} { less_than( X, X ) }.
% 0.81/1.29 (2701) {G0,W6,D2,L2,V2,M2} { ! strictly_less_than( X, Y ), less_than( X, Y
% 0.81/1.29 ) }.
% 0.81/1.29 (2702) {G0,W6,D2,L2,V2,M2} { ! strictly_less_than( X, Y ), ! less_than( Y
% 0.81/1.29 , X ) }.
% 0.81/1.29 (2703) {G0,W9,D2,L3,V2,M3} { ! less_than( X, Y ), less_than( Y, X ),
% 0.81/1.29 strictly_less_than( X, Y ) }.
% 0.81/1.29 (2704) {G0,W3,D2,L1,V1,M1} { less_than( bottom, X ) }.
% 0.81/1.29 (2705) {G0,W2,D2,L1,V0,M1} { ! isnonempty_slb( create_slb ) }.
% 0.81/1.29 (2706) {G0,W6,D4,L1,V3,M1} { isnonempty_slb( insert_slb( X, pair( Y, Z ) )
% 0.81/1.29 ) }.
% 0.81/1.29 (2707) {G0,W3,D2,L1,V1,M1} { ! contains_slb( create_slb, X ) }.
% 0.81/1.29 (2708) {G0,W13,D4,L3,V4,M3} { ! contains_slb( insert_slb( X, pair( Y, T )
% 0.81/1.29 ), Z ), contains_slb( X, Z ), Y = Z }.
% 0.81/1.29 (2709) {G0,W10,D4,L2,V4,M2} { ! contains_slb( X, Z ), contains_slb(
% 0.81/1.29 insert_slb( X, pair( Y, T ) ), Z ) }.
% 0.81/1.29 (2710) {G0,W10,D4,L2,V4,M2} { ! Y = Z, contains_slb( insert_slb( X, pair(
% 0.81/1.29 Y, T ) ), Z ) }.
% 0.81/1.29 (2711) {G0,W4,D2,L1,V2,M1} { ! pair_in_list( create_slb, X, Y ) }.
% 0.81/1.29 (2712) {G0,W17,D4,L3,V5,M3} { ! pair_in_list( insert_slb( X, pair( Y, T )
% 0.81/1.29 ), Z, U ), pair_in_list( X, Z, U ), alpha1( Y, Z, T, U ) }.
% 0.81/1.29 (2713) {G0,W12,D4,L2,V5,M2} { ! pair_in_list( X, Z, U ), pair_in_list(
% 0.81/1.29 insert_slb( X, pair( Y, T ) ), Z, U ) }.
% 0.81/1.29 (2714) {G0,W13,D4,L2,V5,M2} { ! alpha1( Y, Z, T, U ), pair_in_list(
% 0.81/1.29 insert_slb( X, pair( Y, T ) ), Z, U ) }.
% 0.81/1.29 (2715) {G0,W8,D2,L2,V4,M2} { ! alpha1( X, Y, Z, T ), X = Y }.
% 0.81/1.29 (2716) {G0,W8,D2,L2,V4,M2} { ! alpha1( X, Y, Z, T ), Z = T }.
% 0.81/1.29 (2717) {G0,W11,D2,L3,V4,M3} { ! X = Y, ! Z = T, alpha1( X, Y, Z, T ) }.
% 0.81/1.29 (2718) {G0,W9,D5,L1,V3,M1} { remove_slb( insert_slb( X, pair( Y, Z ) ), Y
% 0.81/1.29 ) = X }.
% 0.81/1.29 (2719) {G0,W21,D5,L3,V4,M3} { Y = Z, ! contains_slb( X, Z ), remove_slb(
% 0.81/1.29 insert_slb( X, pair( Y, T ) ), Z ) = insert_slb( remove_slb( X, Z ), pair
% 0.81/1.29 ( Y, T ) ) }.
% 0.81/1.29 (2720) {G0,W9,D5,L1,V3,M1} { lookup_slb( insert_slb( X, pair( Y, Z ) ), Y
% 0.81/1.29 ) = Z }.
% 0.81/1.29 (2721) {G0,W17,D5,L3,V4,M3} { Y = Z, ! contains_slb( X, Z ), lookup_slb(
% 0.81/1.29 insert_slb( X, pair( Y, T ) ), Z ) = lookup_slb( X, Z ) }.
% 0.81/1.29 (2722) {G0,W5,D3,L1,V1,M1} { update_slb( create_slb, X ) = create_slb }.
% 0.81/1.29 (2723) {G0,W18,D5,L2,V4,M2} { ! strictly_less_than( Y, X ), update_slb(
% 0.81/1.29 insert_slb( Z, pair( T, Y ) ), X ) = insert_slb( update_slb( Z, X ), pair
% 0.81/1.29 ( T, X ) ) }.
% 0.81/1.29 (2724) {G0,W18,D5,L2,V4,M2} { ! less_than( X, Y ), update_slb( insert_slb
% 0.81/1.29 ( Z, pair( T, Y ) ), X ) = insert_slb( update_slb( Z, X ), pair( T, Y ) )
% 0.81/1.29 }.
% 0.81/1.29 (2725) {G0,W13,D3,L3,V4,M3} { ! pair_in_list( X, Y, Z ), ! less_than( T, Z
% 0.81/1.29 ), pair_in_list( update_slb( X, T ), Y, Z ) }.
% 0.81/1.29 (2726) {G0,W13,D3,L3,V4,M3} { ! pair_in_list( X, Y, T ), !
% 0.81/1.29 strictly_less_than( T, Z ), pair_in_list( update_slb( X, Z ), Y, Z ) }.
% 0.81/1.29 (2727) {G0,W4,D2,L1,V0,M1} { pair_in_list( skol1, skol2, skol3 ) }.
% 0.81/1.29 (2728) {G0,W3,D2,L1,V0,M1} { strictly_less_than( skol2, skol3 ) }.
% 0.81/1.29 (2729) {G0,W9,D3,L2,V2,M2} { ! pair_in_list( update_slb( skol1, skol4 ), X
% 0.81/1.29 , Y ), ! strictly_less_than( X, Y ) }.
% 0.81/1.29
% 0.81/1.29
% 0.81/1.29 Total Proof:
% 0.81/1.29
% 0.81/1.29 subsumption: (0) {G0,W9,D2,L3,V3,M3} I { ! less_than( X, Z ), ! less_than(
% 0.81/1.29 Z, Y ), less_than( X, Y ) }.
% 0.81/1.29 parent0: (2698) {G0,W9,D2,L3,V3,M3} { ! less_than( X, Z ), ! less_than( Z
% 0.81/1.29 , Y ), less_than( X, Y ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 X := X
% 0.81/1.29 Y := Y
% 0.81/1.29 Z := Z
% 0.81/1.29 end
% 0.81/1.29 permutation0:
% 0.81/1.29 0 ==> 0
% 0.81/1.29 1 ==> 1
% 0.81/1.29 2 ==> 2
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 subsumption: (1) {G0,W6,D2,L2,V2,M2} I { less_than( X, Y ), less_than( Y, X
% 0.81/1.29 ) }.
% 0.81/1.29 parent0: (2699) {G0,W6,D2,L2,V2,M2} { less_than( X, Y ), less_than( Y, X )
% 0.81/1.29 }.
% 0.81/1.29 substitution0:
% 0.81/1.29 X := X
% 0.81/1.29 Y := Y
% 0.81/1.29 end
% 0.81/1.29 permutation0:
% 0.81/1.29 0 ==> 0
% 0.81/1.29 1 ==> 1
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 subsumption: (3) {G0,W6,D2,L2,V2,M2} I { ! strictly_less_than( X, Y ),
% 0.81/1.29 less_than( X, Y ) }.
% 0.81/1.29 parent0: (2701) {G0,W6,D2,L2,V2,M2} { ! strictly_less_than( X, Y ),
% 0.81/1.29 less_than( X, Y ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 X := X
% 0.81/1.29 Y := Y
% 0.81/1.29 end
% 0.81/1.29 permutation0:
% 0.81/1.29 0 ==> 0
% 0.81/1.29 1 ==> 1
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 subsumption: (4) {G0,W6,D2,L2,V2,M2} I { ! strictly_less_than( X, Y ), !
% 0.81/1.29 less_than( Y, X ) }.
% 0.81/1.29 parent0: (2702) {G0,W6,D2,L2,V2,M2} { ! strictly_less_than( X, Y ), !
% 0.81/1.29 less_than( Y, X ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 X := X
% 0.81/1.29 Y := Y
% 0.81/1.29 end
% 0.81/1.29 permutation0:
% 0.81/1.29 0 ==> 0
% 0.81/1.29 1 ==> 1
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 resolution: (2744) {G1,W9,D2,L3,V2,M3} { less_than( Y, X ),
% 0.81/1.29 strictly_less_than( X, Y ), less_than( Y, X ) }.
% 0.81/1.29 parent0[0]: (2703) {G0,W9,D2,L3,V2,M3} { ! less_than( X, Y ), less_than( Y
% 0.81/1.29 , X ), strictly_less_than( X, Y ) }.
% 0.81/1.29 parent1[0]: (1) {G0,W6,D2,L2,V2,M2} I { less_than( X, Y ), less_than( Y, X
% 0.81/1.29 ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 X := X
% 0.81/1.29 Y := Y
% 0.81/1.29 end
% 0.81/1.29 substitution1:
% 0.81/1.29 X := X
% 0.81/1.29 Y := Y
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 factor: (2745) {G1,W6,D2,L2,V2,M2} { less_than( X, Y ), strictly_less_than
% 0.81/1.29 ( Y, X ) }.
% 0.81/1.29 parent0[0, 2]: (2744) {G1,W9,D2,L3,V2,M3} { less_than( Y, X ),
% 0.81/1.29 strictly_less_than( X, Y ), less_than( Y, X ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 X := Y
% 0.81/1.29 Y := X
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 subsumption: (5) {G1,W6,D2,L2,V2,M2} I;r(1) { less_than( Y, X ),
% 0.81/1.29 strictly_less_than( X, Y ) }.
% 0.81/1.29 parent0: (2745) {G1,W6,D2,L2,V2,M2} { less_than( X, Y ),
% 0.81/1.29 strictly_less_than( Y, X ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 X := Y
% 0.81/1.29 Y := X
% 0.81/1.29 end
% 0.81/1.29 permutation0:
% 0.81/1.29 0 ==> 0
% 0.81/1.29 1 ==> 1
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 *** allocated 170857 integers for clauses
% 0.81/1.29 subsumption: (27) {G0,W13,D3,L3,V4,M3} I { ! pair_in_list( X, Y, Z ), !
% 0.81/1.29 less_than( T, Z ), pair_in_list( update_slb( X, T ), Y, Z ) }.
% 0.81/1.29 parent0: (2725) {G0,W13,D3,L3,V4,M3} { ! pair_in_list( X, Y, Z ), !
% 0.81/1.29 less_than( T, Z ), pair_in_list( update_slb( X, T ), Y, Z ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 X := X
% 0.81/1.29 Y := Y
% 0.81/1.29 Z := Z
% 0.81/1.29 T := T
% 0.81/1.29 end
% 0.81/1.29 permutation0:
% 0.81/1.29 0 ==> 0
% 0.81/1.29 1 ==> 1
% 0.81/1.29 2 ==> 2
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 subsumption: (28) {G0,W13,D3,L3,V4,M3} I { ! pair_in_list( X, Y, T ), !
% 0.81/1.29 strictly_less_than( T, Z ), pair_in_list( update_slb( X, Z ), Y, Z ) }.
% 0.81/1.29 parent0: (2726) {G0,W13,D3,L3,V4,M3} { ! pair_in_list( X, Y, T ), !
% 0.81/1.29 strictly_less_than( T, Z ), pair_in_list( update_slb( X, Z ), Y, Z ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 X := X
% 0.81/1.29 Y := Y
% 0.81/1.29 Z := Z
% 0.81/1.29 T := T
% 0.81/1.29 end
% 0.81/1.29 permutation0:
% 0.81/1.29 0 ==> 0
% 0.81/1.29 1 ==> 1
% 0.81/1.29 2 ==> 2
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 subsumption: (29) {G0,W4,D2,L1,V0,M1} I { pair_in_list( skol1, skol2, skol3
% 0.81/1.29 ) }.
% 0.81/1.29 parent0: (2727) {G0,W4,D2,L1,V0,M1} { pair_in_list( skol1, skol2, skol3 )
% 0.81/1.29 }.
% 0.81/1.29 substitution0:
% 0.81/1.29 end
% 0.81/1.29 permutation0:
% 0.81/1.29 0 ==> 0
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 subsumption: (30) {G0,W3,D2,L1,V0,M1} I { strictly_less_than( skol2, skol3
% 0.81/1.29 ) }.
% 0.81/1.29 parent0: (2728) {G0,W3,D2,L1,V0,M1} { strictly_less_than( skol2, skol3 )
% 0.81/1.29 }.
% 0.81/1.29 substitution0:
% 0.81/1.29 end
% 0.81/1.29 permutation0:
% 0.81/1.29 0 ==> 0
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 subsumption: (31) {G0,W9,D3,L2,V2,M2} I { ! pair_in_list( update_slb( skol1
% 0.81/1.29 , skol4 ), X, Y ), ! strictly_less_than( X, Y ) }.
% 0.81/1.29 parent0: (2729) {G0,W9,D3,L2,V2,M2} { ! pair_in_list( update_slb( skol1,
% 0.81/1.29 skol4 ), X, Y ), ! strictly_less_than( X, Y ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 X := X
% 0.81/1.29 Y := Y
% 0.81/1.29 end
% 0.81/1.29 permutation0:
% 0.81/1.29 0 ==> 0
% 0.81/1.29 1 ==> 1
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 resolution: (2866) {G1,W3,D2,L1,V0,M1} { ! less_than( skol3, skol2 ) }.
% 0.81/1.29 parent0[0]: (4) {G0,W6,D2,L2,V2,M2} I { ! strictly_less_than( X, Y ), !
% 0.81/1.29 less_than( Y, X ) }.
% 0.81/1.29 parent1[0]: (30) {G0,W3,D2,L1,V0,M1} I { strictly_less_than( skol2, skol3 )
% 0.81/1.29 }.
% 0.81/1.29 substitution0:
% 0.81/1.29 X := skol2
% 0.81/1.29 Y := skol3
% 0.81/1.29 end
% 0.81/1.29 substitution1:
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 subsumption: (48) {G1,W3,D2,L1,V0,M1} R(4,30) { ! less_than( skol3, skol2 )
% 0.81/1.29 }.
% 0.81/1.29 parent0: (2866) {G1,W3,D2,L1,V0,M1} { ! less_than( skol3, skol2 ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 end
% 0.81/1.29 permutation0:
% 0.81/1.29 0 ==> 0
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 resolution: (2867) {G1,W6,D2,L2,V1,M2} { ! less_than( skol3, X ), !
% 0.81/1.29 less_than( X, skol2 ) }.
% 0.81/1.29 parent0[0]: (48) {G1,W3,D2,L1,V0,M1} R(4,30) { ! less_than( skol3, skol2 )
% 0.81/1.29 }.
% 0.81/1.29 parent1[2]: (0) {G0,W9,D2,L3,V3,M3} I { ! less_than( X, Z ), ! less_than( Z
% 0.81/1.29 , Y ), less_than( X, Y ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 end
% 0.81/1.29 substitution1:
% 0.81/1.29 X := skol3
% 0.81/1.29 Y := skol2
% 0.81/1.29 Z := X
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 subsumption: (60) {G2,W6,D2,L2,V1,M2} R(48,0) { ! less_than( skol3, X ), !
% 0.81/1.29 less_than( X, skol2 ) }.
% 0.81/1.29 parent0: (2867) {G1,W6,D2,L2,V1,M2} { ! less_than( skol3, X ), ! less_than
% 0.81/1.29 ( X, skol2 ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 X := X
% 0.81/1.29 end
% 0.81/1.29 permutation0:
% 0.81/1.29 0 ==> 0
% 0.81/1.29 1 ==> 1
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 resolution: (2868) {G1,W6,D2,L2,V1,M2} { ! less_than( X, skol2 ), !
% 0.81/1.29 strictly_less_than( skol3, X ) }.
% 0.81/1.29 parent0[0]: (60) {G2,W6,D2,L2,V1,M2} R(48,0) { ! less_than( skol3, X ), !
% 0.81/1.29 less_than( X, skol2 ) }.
% 0.81/1.29 parent1[1]: (3) {G0,W6,D2,L2,V2,M2} I { ! strictly_less_than( X, Y ),
% 0.81/1.29 less_than( X, Y ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 X := X
% 0.81/1.29 end
% 0.81/1.29 substitution1:
% 0.81/1.29 X := skol3
% 0.81/1.29 Y := X
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 subsumption: (128) {G3,W6,D2,L2,V1,M2} R(60,3) { ! less_than( X, skol2 ), !
% 0.81/1.29 strictly_less_than( skol3, X ) }.
% 0.81/1.29 parent0: (2868) {G1,W6,D2,L2,V1,M2} { ! less_than( X, skol2 ), !
% 0.81/1.29 strictly_less_than( skol3, X ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 X := X
% 0.81/1.29 end
% 0.81/1.29 permutation0:
% 0.81/1.29 0 ==> 0
% 0.81/1.29 1 ==> 1
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 resolution: (2870) {G2,W6,D2,L2,V1,M2} { ! strictly_less_than( skol3, X )
% 0.81/1.29 , strictly_less_than( skol2, X ) }.
% 0.81/1.29 parent0[0]: (128) {G3,W6,D2,L2,V1,M2} R(60,3) { ! less_than( X, skol2 ), !
% 0.81/1.29 strictly_less_than( skol3, X ) }.
% 0.81/1.29 parent1[0]: (5) {G1,W6,D2,L2,V2,M2} I;r(1) { less_than( Y, X ),
% 0.81/1.29 strictly_less_than( X, Y ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 X := X
% 0.81/1.29 end
% 0.81/1.29 substitution1:
% 0.81/1.29 X := skol2
% 0.81/1.29 Y := X
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 subsumption: (134) {G4,W6,D2,L2,V1,M2} R(128,5) { ! strictly_less_than(
% 0.81/1.29 skol3, X ), strictly_less_than( skol2, X ) }.
% 0.81/1.29 parent0: (2870) {G2,W6,D2,L2,V1,M2} { ! strictly_less_than( skol3, X ),
% 0.81/1.29 strictly_less_than( skol2, X ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 X := X
% 0.81/1.29 end
% 0.81/1.29 permutation0:
% 0.81/1.29 0 ==> 0
% 0.81/1.29 1 ==> 1
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 resolution: (2872) {G2,W6,D2,L2,V1,M2} { strictly_less_than( skol2, X ),
% 0.81/1.29 less_than( X, skol3 ) }.
% 0.81/1.29 parent0[0]: (134) {G4,W6,D2,L2,V1,M2} R(128,5) { ! strictly_less_than(
% 0.81/1.29 skol3, X ), strictly_less_than( skol2, X ) }.
% 0.81/1.29 parent1[1]: (5) {G1,W6,D2,L2,V2,M2} I;r(1) { less_than( Y, X ),
% 0.81/1.29 strictly_less_than( X, Y ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 X := X
% 0.81/1.29 end
% 0.81/1.29 substitution1:
% 0.81/1.29 X := skol3
% 0.81/1.29 Y := X
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 subsumption: (151) {G5,W6,D2,L2,V1,M2} R(134,5) { strictly_less_than( skol2
% 0.81/1.29 , X ), less_than( X, skol3 ) }.
% 0.81/1.29 parent0: (2872) {G2,W6,D2,L2,V1,M2} { strictly_less_than( skol2, X ),
% 0.81/1.29 less_than( X, skol3 ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 X := X
% 0.81/1.29 end
% 0.81/1.29 permutation0:
% 0.81/1.29 0 ==> 0
% 0.81/1.29 1 ==> 1
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 resolution: (2873) {G1,W6,D3,L1,V0,M1} { ! pair_in_list( update_slb( skol1
% 0.81/1.29 , skol4 ), skol2, skol3 ) }.
% 0.81/1.29 parent0[1]: (31) {G0,W9,D3,L2,V2,M2} I { ! pair_in_list( update_slb( skol1
% 0.81/1.29 , skol4 ), X, Y ), ! strictly_less_than( X, Y ) }.
% 0.81/1.29 parent1[0]: (30) {G0,W3,D2,L1,V0,M1} I { strictly_less_than( skol2, skol3 )
% 0.81/1.29 }.
% 0.81/1.29 substitution0:
% 0.81/1.29 X := skol2
% 0.81/1.29 Y := skol3
% 0.81/1.29 end
% 0.81/1.29 substitution1:
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 subsumption: (1099) {G1,W6,D3,L1,V0,M1} R(31,30) { ! pair_in_list(
% 0.81/1.29 update_slb( skol1, skol4 ), skol2, skol3 ) }.
% 0.81/1.29 parent0: (2873) {G1,W6,D3,L1,V0,M1} { ! pair_in_list( update_slb( skol1,
% 0.81/1.29 skol4 ), skol2, skol3 ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 end
% 0.81/1.29 permutation0:
% 0.81/1.29 0 ==> 0
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 resolution: (2874) {G1,W7,D2,L2,V0,M2} { ! pair_in_list( skol1, skol2,
% 0.81/1.29 skol3 ), ! less_than( skol4, skol3 ) }.
% 0.81/1.29 parent0[0]: (1099) {G1,W6,D3,L1,V0,M1} R(31,30) { ! pair_in_list(
% 0.81/1.29 update_slb( skol1, skol4 ), skol2, skol3 ) }.
% 0.81/1.29 parent1[2]: (27) {G0,W13,D3,L3,V4,M3} I { ! pair_in_list( X, Y, Z ), !
% 0.81/1.29 less_than( T, Z ), pair_in_list( update_slb( X, T ), Y, Z ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 end
% 0.81/1.29 substitution1:
% 0.81/1.29 X := skol1
% 0.81/1.29 Y := skol2
% 0.81/1.29 Z := skol3
% 0.81/1.29 T := skol4
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 resolution: (2875) {G1,W3,D2,L1,V0,M1} { ! less_than( skol4, skol3 ) }.
% 0.81/1.29 parent0[0]: (2874) {G1,W7,D2,L2,V0,M2} { ! pair_in_list( skol1, skol2,
% 0.81/1.29 skol3 ), ! less_than( skol4, skol3 ) }.
% 0.81/1.29 parent1[0]: (29) {G0,W4,D2,L1,V0,M1} I { pair_in_list( skol1, skol2, skol3
% 0.81/1.29 ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 end
% 0.81/1.29 substitution1:
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 subsumption: (1153) {G2,W3,D2,L1,V0,M1} R(1099,27);r(29) { ! less_than(
% 0.81/1.29 skol4, skol3 ) }.
% 0.81/1.29 parent0: (2875) {G1,W3,D2,L1,V0,M1} { ! less_than( skol4, skol3 ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 end
% 0.81/1.29 permutation0:
% 0.81/1.29 0 ==> 0
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 resolution: (2876) {G3,W3,D2,L1,V0,M1} { strictly_less_than( skol2, skol4
% 0.81/1.29 ) }.
% 0.81/1.29 parent0[0]: (1153) {G2,W3,D2,L1,V0,M1} R(1099,27);r(29) { ! less_than(
% 0.81/1.29 skol4, skol3 ) }.
% 0.81/1.29 parent1[1]: (151) {G5,W6,D2,L2,V1,M2} R(134,5) { strictly_less_than( skol2
% 0.81/1.29 , X ), less_than( X, skol3 ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 end
% 0.81/1.29 substitution1:
% 0.81/1.29 X := skol4
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 subsumption: (1181) {G6,W3,D2,L1,V0,M1} R(1153,151) { strictly_less_than(
% 0.81/1.29 skol2, skol4 ) }.
% 0.81/1.29 parent0: (2876) {G3,W3,D2,L1,V0,M1} { strictly_less_than( skol2, skol4 )
% 0.81/1.29 }.
% 0.81/1.29 substitution0:
% 0.81/1.29 end
% 0.81/1.29 permutation0:
% 0.81/1.29 0 ==> 0
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 resolution: (2877) {G2,W3,D2,L1,V0,M1} { strictly_less_than( skol3, skol4
% 0.81/1.29 ) }.
% 0.81/1.29 parent0[0]: (1153) {G2,W3,D2,L1,V0,M1} R(1099,27);r(29) { ! less_than(
% 0.81/1.29 skol4, skol3 ) }.
% 0.81/1.29 parent1[0]: (5) {G1,W6,D2,L2,V2,M2} I;r(1) { less_than( Y, X ),
% 0.81/1.29 strictly_less_than( X, Y ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 end
% 0.81/1.29 substitution1:
% 0.81/1.29 X := skol3
% 0.81/1.29 Y := skol4
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 subsumption: (1186) {G3,W3,D2,L1,V0,M1} R(1153,5) { strictly_less_than(
% 0.81/1.29 skol3, skol4 ) }.
% 0.81/1.29 parent0: (2877) {G2,W3,D2,L1,V0,M1} { strictly_less_than( skol3, skol4 )
% 0.81/1.29 }.
% 0.81/1.29 substitution0:
% 0.81/1.29 end
% 0.81/1.29 permutation0:
% 0.81/1.29 0 ==> 0
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 resolution: (2878) {G1,W6,D3,L1,V0,M1} { ! pair_in_list( update_slb( skol1
% 0.81/1.29 , skol4 ), skol2, skol4 ) }.
% 0.81/1.29 parent0[1]: (31) {G0,W9,D3,L2,V2,M2} I { ! pair_in_list( update_slb( skol1
% 0.81/1.29 , skol4 ), X, Y ), ! strictly_less_than( X, Y ) }.
% 0.81/1.29 parent1[0]: (1181) {G6,W3,D2,L1,V0,M1} R(1153,151) { strictly_less_than(
% 0.81/1.29 skol2, skol4 ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 X := skol2
% 0.81/1.29 Y := skol4
% 0.81/1.29 end
% 0.81/1.29 substitution1:
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 subsumption: (1226) {G7,W6,D3,L1,V0,M1} R(1181,31) { ! pair_in_list(
% 0.81/1.29 update_slb( skol1, skol4 ), skol2, skol4 ) }.
% 0.81/1.29 parent0: (2878) {G1,W6,D3,L1,V0,M1} { ! pair_in_list( update_slb( skol1,
% 0.81/1.29 skol4 ), skol2, skol4 ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 end
% 0.81/1.29 permutation0:
% 0.81/1.29 0 ==> 0
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 resolution: (2879) {G1,W7,D2,L2,V1,M2} { ! pair_in_list( skol1, skol2, X )
% 0.81/1.29 , ! strictly_less_than( X, skol4 ) }.
% 0.81/1.29 parent0[0]: (1226) {G7,W6,D3,L1,V0,M1} R(1181,31) { ! pair_in_list(
% 0.81/1.29 update_slb( skol1, skol4 ), skol2, skol4 ) }.
% 0.81/1.29 parent1[2]: (28) {G0,W13,D3,L3,V4,M3} I { ! pair_in_list( X, Y, T ), !
% 0.81/1.29 strictly_less_than( T, Z ), pair_in_list( update_slb( X, Z ), Y, Z ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 end
% 0.81/1.29 substitution1:
% 0.81/1.29 X := skol1
% 0.81/1.29 Y := skol2
% 0.81/1.29 Z := skol4
% 0.81/1.29 T := X
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 subsumption: (2627) {G8,W7,D2,L2,V1,M2} R(1226,28) { ! pair_in_list( skol1
% 0.81/1.29 , skol2, X ), ! strictly_less_than( X, skol4 ) }.
% 0.81/1.29 parent0: (2879) {G1,W7,D2,L2,V1,M2} { ! pair_in_list( skol1, skol2, X ), !
% 0.81/1.29 strictly_less_than( X, skol4 ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 X := X
% 0.81/1.29 end
% 0.81/1.29 permutation0:
% 0.81/1.29 0 ==> 0
% 0.81/1.29 1 ==> 1
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 resolution: (2880) {G4,W4,D2,L1,V0,M1} { ! pair_in_list( skol1, skol2,
% 0.81/1.29 skol3 ) }.
% 0.81/1.29 parent0[1]: (2627) {G8,W7,D2,L2,V1,M2} R(1226,28) { ! pair_in_list( skol1,
% 0.81/1.29 skol2, X ), ! strictly_less_than( X, skol4 ) }.
% 0.81/1.29 parent1[0]: (1186) {G3,W3,D2,L1,V0,M1} R(1153,5) { strictly_less_than(
% 0.81/1.29 skol3, skol4 ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 X := skol3
% 0.81/1.29 end
% 0.81/1.29 substitution1:
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 resolution: (2881) {G1,W0,D0,L0,V0,M0} { }.
% 0.81/1.29 parent0[0]: (2880) {G4,W4,D2,L1,V0,M1} { ! pair_in_list( skol1, skol2,
% 0.81/1.29 skol3 ) }.
% 0.81/1.29 parent1[0]: (29) {G0,W4,D2,L1,V0,M1} I { pair_in_list( skol1, skol2, skol3
% 0.81/1.29 ) }.
% 0.81/1.29 substitution0:
% 0.81/1.29 end
% 0.81/1.29 substitution1:
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 subsumption: (2696) {G9,W0,D0,L0,V0,M0} R(2627,1186);r(29) { }.
% 0.81/1.29 parent0: (2881) {G1,W0,D0,L0,V0,M0} { }.
% 0.81/1.29 substitution0:
% 0.81/1.29 end
% 0.81/1.29 permutation0:
% 0.81/1.29 end
% 0.81/1.29
% 0.81/1.29 Proof check complete!
% 0.81/1.29
% 0.81/1.29 Memory use:
% 0.81/1.29
% 0.81/1.29 space for terms: 40826
% 0.81/1.29 space for clauses: 112778
% 0.81/1.29
% 0.81/1.29
% 0.81/1.29 clauses generated: 11942
% 0.81/1.29 clauses kept: 2697
% 0.81/1.29 clauses selected: 192
% 0.81/1.29 clauses deleted: 3
% 0.81/1.29 clauses inuse deleted: 0
% 0.81/1.29
% 0.81/1.29 subsentry: 34342
% 0.81/1.29 literals s-matched: 21262
% 0.81/1.29 literals matched: 21184
% 0.81/1.29 full subsumption: 7412
% 0.81/1.29
% 0.81/1.29 checksum: -1732582077
% 0.81/1.29
% 0.81/1.29
% 0.81/1.29 Bliksem ended
%------------------------------------------------------------------------------