%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : GRA005+1 : TPTP v8.1.0. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n022.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Sat Jul 16 07:11:31 EDT 2022
% Result : Theorem 2.11s 2.50s
% Output : Refutation 2.11s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : GRA005+1 : TPTP v8.1.0. Bugfixed v3.2.0.
% 0.08/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n022.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 : Tue May 31 00:51:07 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.44/1.07 *** allocated 10000 integers for termspace/termends
% 0.44/1.07 *** allocated 10000 integers for clauses
% 0.44/1.07 *** allocated 10000 integers for justifications
% 0.44/1.07 Bliksem 1.12
% 0.44/1.07
% 0.44/1.07
% 0.44/1.07 Automatic Strategy Selection
% 0.44/1.07
% 0.44/1.07
% 0.44/1.07 Clauses:
% 0.44/1.07
% 0.44/1.07 { ! edge( X ), ! head_of( X ) = tail_of( X ) }.
% 0.44/1.07 { ! edge( X ), vertex( head_of( X ) ) }.
% 0.44/1.07 { ! edge( X ), vertex( tail_of( X ) ) }.
% 0.44/1.07 { ! complete, ! vertex( X ), ! vertex( Y ), X = Y, edge( skol1( Z, T ) ) }
% 0.44/1.07 .
% 0.44/1.07 { ! complete, ! vertex( X ), ! vertex( Y ), X = Y, alpha11( X, Y, skol1( X
% 0.44/1.07 , Y ) ), alpha15( X, Y, skol1( X, Y ) ) }.
% 0.44/1.07 { ! alpha15( X, Y, Z ), Y = head_of( Z ) }.
% 0.44/1.07 { ! alpha15( X, Y, Z ), X = tail_of( Z ) }.
% 0.44/1.07 { ! alpha15( X, Y, Z ), ! alpha1( X, Y, Z ) }.
% 0.44/1.07 { ! Y = head_of( Z ), ! X = tail_of( Z ), alpha1( X, Y, Z ), alpha15( X, Y
% 0.44/1.07 , Z ) }.
% 0.44/1.07 { ! alpha11( X, Y, Z ), alpha1( X, Y, Z ) }.
% 0.44/1.07 { ! alpha11( X, Y, Z ), ! Y = head_of( Z ), ! X = tail_of( Z ) }.
% 0.44/1.07 { ! alpha1( X, Y, Z ), Y = head_of( Z ), alpha11( X, Y, Z ) }.
% 0.44/1.07 { ! alpha1( X, Y, Z ), X = tail_of( Z ), alpha11( X, Y, Z ) }.
% 0.44/1.07 { ! alpha1( X, Y, Z ), X = head_of( Z ) }.
% 0.44/1.07 { ! alpha1( X, Y, Z ), Y = tail_of( Z ) }.
% 0.44/1.07 { ! X = head_of( Z ), ! Y = tail_of( Z ), alpha1( X, Y, Z ) }.
% 0.44/1.07 { ! vertex( X ), ! vertex( Y ), ! edge( T ), ! X = tail_of( T ), ! Y =
% 0.44/1.07 head_of( T ), ! Z = path_cons( T, empty ), path( X, Y, Z ) }.
% 0.44/1.07 { ! vertex( X ), ! vertex( Y ), ! edge( T ), ! X = tail_of( T ), ! path(
% 0.44/1.07 head_of( T ), Y, U ), ! Z = path_cons( T, U ), path( X, Y, Z ) }.
% 0.44/1.07 { ! path( X, Y, Z ), alpha12( X, Y ) }.
% 0.44/1.07 { ! path( X, Y, Z ), alpha16( X, skol2( X, T, U ) ) }.
% 0.44/1.07 { ! path( X, Y, Z ), alpha20( Y, Z, skol2( X, Y, Z ) ) }.
% 0.44/1.07 { ! alpha20( X, Y, Z ), alpha18( X, Y, Z ), alpha21( X, Y, Z ) }.
% 0.44/1.07 { ! alpha18( X, Y, Z ), alpha20( X, Y, Z ) }.
% 0.44/1.07 { ! alpha21( X, Y, Z ), alpha20( X, Y, Z ) }.
% 0.44/1.07 { ! alpha21( X, Y, Z ), Y = path_cons( Z, skol3( T, Y, Z ) ) }.
% 0.44/1.07 { ! alpha21( X, Y, Z ), path( head_of( Z ), X, skol3( X, Y, Z ) ) }.
% 0.44/1.07 { ! alpha21( X, Y, Z ), ! alpha2( X, Y, Z ) }.
% 0.44/1.07 { ! path( head_of( Z ), X, T ), ! Y = path_cons( Z, T ), alpha2( X, Y, Z )
% 0.44/1.07 , alpha21( X, Y, Z ) }.
% 0.44/1.07 { ! alpha18( X, Y, Z ), alpha2( X, Y, Z ) }.
% 0.44/1.08 { ! alpha18( X, Y, Z ), ! path( head_of( Z ), X, T ), ! Y = path_cons( Z, T
% 0.44/1.08 ) }.
% 0.44/1.08 { ! alpha2( X, Y, Z ), Y = path_cons( Z, skol4( T, Y, Z ) ), alpha18( X, Y
% 0.44/1.08 , Z ) }.
% 0.44/1.08 { ! alpha2( X, Y, Z ), path( head_of( Z ), X, skol4( X, Y, Z ) ), alpha18(
% 0.44/1.08 X, Y, Z ) }.
% 0.44/1.08 { ! alpha16( X, Y ), edge( Y ) }.
% 0.44/1.08 { ! alpha16( X, Y ), X = tail_of( Y ) }.
% 0.44/1.08 { ! edge( Y ), ! X = tail_of( Y ), alpha16( X, Y ) }.
% 0.44/1.08 { ! alpha12( X, Y ), vertex( X ) }.
% 0.44/1.08 { ! alpha12( X, Y ), vertex( Y ) }.
% 0.44/1.08 { ! vertex( X ), ! vertex( Y ), alpha12( X, Y ) }.
% 0.44/1.08 { ! alpha2( X, Y, Z ), X = head_of( Z ) }.
% 0.44/1.08 { ! alpha2( X, Y, Z ), Y = path_cons( Z, empty ) }.
% 0.44/1.08 { ! X = head_of( Z ), ! Y = path_cons( Z, empty ), alpha2( X, Y, Z ) }.
% 0.44/1.08 { ! path( Z, T, X ), ! on_path( Y, X ), edge( Y ) }.
% 0.44/1.08 { ! path( Z, T, X ), ! on_path( Y, X ), in_path( head_of( Y ), X ) }.
% 0.44/1.08 { ! path( Z, T, X ), ! on_path( Y, X ), in_path( tail_of( Y ), X ) }.
% 0.44/1.08 { ! path( Z, T, X ), ! in_path( Y, X ), vertex( Y ) }.
% 0.44/1.08 { ! path( Z, T, X ), ! in_path( Y, X ), Y = head_of( skol5( U, Y ) ), Y =
% 0.44/1.08 tail_of( skol5( U, Y ) ) }.
% 0.44/1.08 { ! path( Z, T, X ), ! in_path( Y, X ), on_path( skol5( X, Y ), X ) }.
% 0.44/1.08 { ! sequential( X, Y ), edge( X ) }.
% 0.44/1.08 { ! sequential( X, Y ), alpha3( X, Y ) }.
% 0.44/1.08 { ! edge( X ), ! alpha3( X, Y ), sequential( X, Y ) }.
% 0.44/1.08 { ! alpha3( X, Y ), edge( Y ) }.
% 0.44/1.08 { ! alpha3( X, Y ), alpha6( X, Y ) }.
% 0.44/1.08 { ! edge( Y ), ! alpha6( X, Y ), alpha3( X, Y ) }.
% 0.44/1.08 { ! alpha6( X, Y ), ! X = Y }.
% 0.44/1.08 { ! alpha6( X, Y ), head_of( X ) = tail_of( Y ) }.
% 0.44/1.08 { X = Y, ! head_of( X ) = tail_of( Y ), alpha6( X, Y ) }.
% 0.44/1.08 { ! path( Y, Z, X ), ! on_path( T, X ), ! on_path( U, X ), ! sequential( T
% 0.44/1.08 , U ), precedes( T, U, X ) }.
% 0.44/1.08 { ! path( Y, Z, X ), ! on_path( T, X ), ! on_path( U, X ), ! sequential( T
% 0.44/1.08 , W ), ! precedes( W, U, X ), precedes( T, U, X ) }.
% 0.44/1.08 { ! path( Y, Z, X ), ! precedes( T, U, X ), alpha13( X, T, U ) }.
% 0.44/1.08 { ! path( Y, Z, X ), ! precedes( T, U, X ), alpha17( X, T, U ), alpha19( X
% 0.44/1.08 , T, U ) }.
% 0.44/1.08 { ! alpha19( X, Y, Z ), sequential( Y, skol6( T, Y, U ) ) }.
% 0.44/1.08 { ! alpha19( X, Y, Z ), precedes( skol6( X, Y, Z ), Z, X ) }.
% 0.44/1.08 { ! alpha19( X, Y, Z ), ! sequential( Y, Z ) }.
% 0.80/1.20 { ! sequential( Y, T ), ! precedes( T, Z, X ), sequential( Y, Z ), alpha19
% 0.80/1.20 ( X, Y, Z ) }.
% 0.80/1.20 { ! alpha17( X, Y, Z ), sequential( Y, Z ) }.
% 0.80/1.20 { ! alpha17( X, Y, Z ), ! sequential( Y, T ), ! precedes( T, Z, X ) }.
% 0.80/1.20 { ! sequential( Y, Z ), sequential( Y, skol7( T, Y, U ) ), alpha17( X, Y, Z
% 0.80/1.20 ) }.
% 0.80/1.20 { ! sequential( Y, Z ), precedes( skol7( X, Y, Z ), Z, X ), alpha17( X, Y,
% 0.80/1.20 Z ) }.
% 0.80/1.20 { ! alpha13( X, Y, Z ), on_path( Y, X ) }.
% 0.80/1.20 { ! alpha13( X, Y, Z ), on_path( Z, X ) }.
% 0.80/1.20 { ! on_path( Y, X ), ! on_path( Z, X ), alpha13( X, Y, Z ) }.
% 0.80/1.20 { ! shortest_path( X, Y, Z ), path( X, Y, Z ) }.
% 0.80/1.20 { ! shortest_path( X, Y, Z ), alpha4( X, Y, Z ) }.
% 0.80/1.20 { ! path( X, Y, Z ), ! alpha4( X, Y, Z ), shortest_path( X, Y, Z ) }.
% 0.80/1.20 { ! alpha4( X, Y, Z ), ! X = Y }.
% 0.80/1.20 { ! alpha4( X, Y, Z ), alpha7( X, Y, Z ) }.
% 0.80/1.20 { X = Y, ! alpha7( X, Y, Z ), alpha4( X, Y, Z ) }.
% 0.80/1.20 { ! alpha7( X, Y, Z ), ! path( X, Y, T ), less_or_equal( length_of( Z ),
% 0.80/1.20 length_of( T ) ) }.
% 0.80/1.20 { ! less_or_equal( length_of( Z ), length_of( skol8( T, U, Z ) ) ), alpha7
% 0.80/1.20 ( X, Y, Z ) }.
% 0.80/1.20 { path( X, Y, skol8( X, Y, Z ) ), alpha7( X, Y, Z ) }.
% 0.80/1.20 { ! shortest_path( T, U, Z ), ! precedes( X, Y, Z ), ! tail_of( W ) =
% 0.80/1.20 tail_of( X ), ! head_of( W ) = head_of( Y ) }.
% 0.80/1.20 { ! shortest_path( T, U, Z ), ! precedes( X, Y, Z ), ! precedes( Y, X, Z )
% 0.80/1.20 }.
% 0.80/1.20 { ! triangle( X, Y, Z ), edge( X ) }.
% 0.80/1.20 { ! triangle( X, Y, Z ), alpha5( X, Y, Z ) }.
% 0.80/1.20 { ! edge( X ), ! alpha5( X, Y, Z ), triangle( X, Y, Z ) }.
% 0.80/1.20 { ! alpha5( X, Y, Z ), edge( Y ) }.
% 0.80/1.20 { ! alpha5( X, Y, Z ), alpha8( X, Y, Z ) }.
% 0.80/1.20 { ! edge( Y ), ! alpha8( X, Y, Z ), alpha5( X, Y, Z ) }.
% 0.80/1.20 { ! alpha8( X, Y, Z ), edge( Z ) }.
% 0.80/1.20 { ! alpha8( X, Y, Z ), alpha9( X, Y, Z ) }.
% 0.80/1.20 { ! edge( Z ), ! alpha9( X, Y, Z ), alpha8( X, Y, Z ) }.
% 0.80/1.20 { ! alpha9( X, Y, Z ), sequential( X, Y ) }.
% 0.80/1.20 { ! alpha9( X, Y, Z ), alpha10( X, Y, Z ) }.
% 0.80/1.20 { ! sequential( X, Y ), ! alpha10( X, Y, Z ), alpha9( X, Y, Z ) }.
% 0.80/1.20 { ! alpha10( X, Y, Z ), sequential( Y, Z ) }.
% 0.80/1.20 { ! alpha10( X, Y, Z ), sequential( Z, X ) }.
% 0.80/1.20 { ! sequential( Y, Z ), ! sequential( Z, X ), alpha10( X, Y, Z ) }.
% 0.80/1.20 { ! path( Y, Z, X ), length_of( X ) = number_of_in( edges, X ) }.
% 0.80/1.20 { ! path( Y, Z, X ), number_of_in( sequential_pairs, X ) = minus( length_of
% 0.80/1.20 ( X ), n1 ) }.
% 0.80/1.20 { ! path( Y, Z, X ), alpha14( X, skol9( X ), skol11( X ) ), number_of_in(
% 0.80/1.20 sequential_pairs, X ) = number_of_in( triangles, X ) }.
% 0.80/1.20 { ! path( Y, Z, X ), ! triangle( skol9( X ), skol11( X ), T ), number_of_in
% 0.80/1.20 ( sequential_pairs, X ) = number_of_in( triangles, X ) }.
% 0.80/1.20 { ! alpha14( X, Y, Z ), on_path( Y, X ) }.
% 0.80/1.20 { ! alpha14( X, Y, Z ), on_path( Z, X ) }.
% 0.80/1.20 { ! alpha14( X, Y, Z ), sequential( Y, Z ) }.
% 0.80/1.20 { ! on_path( Y, X ), ! on_path( Z, X ), ! sequential( Y, Z ), alpha14( X, Y
% 0.80/1.20 , Z ) }.
% 0.80/1.20 { less_or_equal( number_of_in( X, Y ), number_of_in( X, graph ) ) }.
% 0.80/1.20 { shortest_path( skol14, skol15, skol13 ) }.
% 0.80/1.20 { precedes( skol10, skol12, skol13 ) }.
% 0.80/1.20 { edge( skol16 ) }.
% 0.80/1.20 { tail_of( skol16 ) = tail_of( skol10 ) }.
% 0.80/1.20 { head_of( skol16 ) = head_of( skol12 ) }.
% 0.80/1.20
% 0.80/1.20 percentage equality = 0.159170, percentage horn = 0.837838
% 0.80/1.20 This is a problem with some equality
% 0.80/1.20
% 0.80/1.20
% 0.80/1.20
% 0.80/1.20 Options Used:
% 0.80/1.20
% 0.80/1.20 useres = 1
% 0.80/1.20 useparamod = 1
% 0.80/1.20 useeqrefl = 1
% 0.80/1.20 useeqfact = 1
% 0.80/1.20 usefactor = 1
% 0.80/1.20 usesimpsplitting = 0
% 0.80/1.20 usesimpdemod = 5
% 0.80/1.20 usesimpres = 3
% 0.80/1.20
% 0.80/1.20 resimpinuse = 1000
% 0.80/1.20 resimpclauses = 20000
% 0.80/1.20 substype = eqrewr
% 0.80/1.20 backwardsubs = 1
% 0.80/1.20 selectoldest = 5
% 0.80/1.20
% 0.80/1.20 litorderings [0] = split
% 0.80/1.20 litorderings [1] = extend the termordering, first sorting on arguments
% 0.80/1.20
% 0.80/1.20 termordering = kbo
% 0.80/1.20
% 0.80/1.20 litapriori = 0
% 0.80/1.20 termapriori = 1
% 0.80/1.20 litaposteriori = 0
% 0.80/1.20 termaposteriori = 0
% 0.80/1.20 demodaposteriori = 0
% 0.80/1.20 ordereqreflfact = 0
% 0.80/1.20
% 0.80/1.20 litselect = negord
% 0.80/1.20
% 0.80/1.20 maxweight = 15
% 0.80/1.20 maxdepth = 30000
% 0.80/1.20 maxlength = 115
% 0.80/1.20 maxnrvars = 195
% 0.80/1.20 excuselevel = 1
% 0.80/1.20 increasemaxweight = 1
% 0.80/1.20
% 0.80/1.20 maxselected = 10000000
% 0.80/1.20 maxnrclauses = 10000000
% 0.80/1.20
% 0.80/1.20 showgenerated = 0
% 0.80/1.20 showkept = 0
% 0.80/1.20 showselected = 0
% 0.80/1.20 showdeleted = 0
% 0.80/1.20 showresimp = 1
% 0.80/1.20 showstatus = 2000
% 0.80/1.20
% 0.80/1.20 prologoutput = 0
% 0.80/1.20 nrgoals = 5000000
% 0.80/1.20 totalproof = 1
% 0.80/1.20
% 0.80/1.20 Symbols occurring in the translation:
% 0.80/1.20
% 0.80/1.20 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 2.11/2.50 . [1, 2] (w:1, o:43, a:1, s:1, b:0),
% 2.11/2.50 ! [4, 1] (w:0, o:31, a:1, s:1, b:0),
% 2.11/2.50 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 2.11/2.50 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 2.11/2.50 edge [36, 1] (w:1, o:36, a:1, s:1, b:0),
% 2.11/2.50 head_of [37, 1] (w:1, o:37, a:1, s:1, b:0),
% 2.11/2.50 tail_of [38, 1] (w:1, o:40, a:1, s:1, b:0),
% 2.11/2.50 vertex [39, 1] (w:1, o:41, a:1, s:1, b:0),
% 2.11/2.50 complete [40, 0] (w:1, o:7, a:1, s:1, b:0),
% 2.11/2.50 empty [44, 0] (w:1, o:11, a:1, s:1, b:0),
% 2.11/2.50 path_cons [45, 2] (w:1, o:70, a:1, s:1, b:0),
% 2.11/2.50 path [47, 3] (w:1, o:80, a:1, s:1, b:0),
% 2.11/2.50 on_path [48, 2] (w:1, o:69, a:1, s:1, b:0),
% 2.11/2.50 in_path [49, 2] (w:1, o:71, a:1, s:1, b:0),
% 2.11/2.50 sequential [53, 2] (w:1, o:72, a:1, s:1, b:0),
% 2.11/2.50 precedes [55, 3] (w:1, o:81, a:1, s:1, b:0),
% 2.11/2.50 shortest_path [57, 3] (w:1, o:82, a:1, s:1, b:0),
% 2.11/2.50 length_of [58, 1] (w:1, o:42, a:1, s:1, b:0),
% 2.11/2.50 less_or_equal [59, 2] (w:1, o:73, a:1, s:1, b:0),
% 2.11/2.50 triangle [60, 3] (w:1, o:89, a:1, s:1, b:0),
% 2.11/2.50 edges [61, 0] (w:1, o:18, a:1, s:1, b:0),
% 2.11/2.50 number_of_in [62, 2] (w:1, o:68, a:1, s:1, b:0),
% 2.11/2.50 sequential_pairs [63, 0] (w:1, o:19, a:1, s:1, b:0),
% 2.11/2.50 n1 [64, 0] (w:1, o:20, a:1, s:1, b:0),
% 2.11/2.50 minus [65, 2] (w:1, o:67, a:1, s:1, b:0),
% 2.11/2.50 triangles [66, 0] (w:1, o:27, a:1, s:1, b:0),
% 2.11/2.50 graph [69, 0] (w:1, o:30, a:1, s:1, b:0),
% 2.11/2.50 alpha1 [70, 3] (w:1, o:90, a:1, s:1, b:1),
% 2.11/2.50 alpha2 [71, 3] (w:1, o:99, a:1, s:1, b:1),
% 2.11/2.50 alpha3 [72, 2] (w:1, o:74, a:1, s:1, b:1),
% 2.11/2.50 alpha4 [73, 3] (w:1, o:100, a:1, s:1, b:1),
% 2.11/2.50 alpha5 [74, 3] (w:1, o:101, a:1, s:1, b:1),
% 2.11/2.50 alpha6 [75, 2] (w:1, o:75, a:1, s:1, b:1),
% 2.11/2.50 alpha7 [76, 3] (w:1, o:102, a:1, s:1, b:1),
% 2.11/2.50 alpha8 [77, 3] (w:1, o:103, a:1, s:1, b:1),
% 2.11/2.50 alpha9 [78, 3] (w:1, o:104, a:1, s:1, b:1),
% 2.11/2.50 alpha10 [79, 3] (w:1, o:91, a:1, s:1, b:1),
% 2.11/2.50 alpha11 [80, 3] (w:1, o:92, a:1, s:1, b:1),
% 2.11/2.50 alpha12 [81, 2] (w:1, o:76, a:1, s:1, b:1),
% 2.11/2.50 alpha13 [82, 3] (w:1, o:93, a:1, s:1, b:1),
% 2.11/2.50 alpha14 [83, 3] (w:1, o:94, a:1, s:1, b:1),
% 2.11/2.50 alpha15 [84, 3] (w:1, o:95, a:1, s:1, b:1),
% 2.11/2.50 alpha16 [85, 2] (w:1, o:77, a:1, s:1, b:1),
% 2.11/2.50 alpha17 [86, 3] (w:1, o:96, a:1, s:1, b:1),
% 2.11/2.50 alpha18 [87, 3] (w:1, o:97, a:1, s:1, b:1),
% 2.11/2.50 alpha19 [88, 3] (w:1, o:98, a:1, s:1, b:1),
% 2.11/2.50 alpha20 [89, 3] (w:1, o:105, a:1, s:1, b:1),
% 2.11/2.50 alpha21 [90, 3] (w:1, o:106, a:1, s:1, b:1),
% 2.11/2.50 skol1 [91, 2] (w:1, o:78, a:1, s:1, b:1),
% 2.11/2.50 skol2 [92, 3] (w:1, o:83, a:1, s:1, b:1),
% 2.11/2.50 skol3 [93, 3] (w:1, o:84, a:1, s:1, b:1),
% 2.11/2.50 skol4 [94, 3] (w:1, o:85, a:1, s:1, b:1),
% 2.11/2.50 skol5 [95, 2] (w:1, o:79, a:1, s:1, b:1),
% 2.11/2.50 skol6 [96, 3] (w:1, o:86, a:1, s:1, b:1),
% 2.11/2.50 skol7 [97, 3] (w:1, o:87, a:1, s:1, b:1),
% 2.11/2.50 skol8 [98, 3] (w:1, o:88, a:1, s:1, b:1),
% 2.11/2.50 skol9 [99, 1] (w:1, o:38, a:1, s:1, b:1),
% 2.11/2.50 skol10 [100, 0] (w:1, o:21, a:1, s:1, b:1),
% 2.11/2.50 skol11 [101, 1] (w:1, o:39, a:1, s:1, b:1),
% 2.11/2.50 skol12 [102, 0] (w:1, o:22, a:1, s:1, b:1),
% 2.11/2.50 skol13 [103, 0] (w:1, o:23, a:1, s:1, b:1),
% 2.11/2.50 skol14 [104, 0] (w:1, o:24, a:1, s:1, b:1),
% 2.11/2.50 skol15 [105, 0] (w:1, o:25, a:1, s:1, b:1),
% 2.11/2.50 skol16 [106, 0] (w:1, o:26, a:1, s:1, b:1).
% 2.11/2.50
% 2.11/2.50
% 2.11/2.50 Starting Search:
% 2.11/2.50
% 2.11/2.50 *** allocated 15000 integers for clauses
% 2.11/2.50 *** allocated 22500 integers for clauses
% 2.11/2.50 *** allocated 33750 integers for clauses
% 2.11/2.50 *** allocated 15000 integers for termspace/termends
% 2.11/2.50 *** allocated 50625 integers for clauses
% 2.11/2.50 *** allocated 22500 integers for termspace/termends
% 2.11/2.50 Resimplifying inuse:
% 2.11/2.50 Done
% 2.11/2.50
% 2.11/2.50 *** allocated 75937 integers for clauses
% 2.11/2.50 *** allocated 33750 integers for termspace/termends
% 2.11/2.50 *** allocated 113905 integers for clauses
% 2.11/2.50 *** allocated 50625 integers for termspace/termends
% 2.11/2.50
% 2.11/2.50 Intermediate Status:
% 2.11/2.50 Generated: 4151
% 2.11/2.50 Kept: 2009
% 2.11/2.50 Inuse: 181
% 2.11/2.50 Deleted: 4
% 2.11/2.50 Deletedinuse: 2
% 2.11/2.50
% 2.11/2.50 Resimplifying inuse:
% 2.11/2.50 Done
% 2.11/2.50
% 2.11/2.50 *** allocated 170857 integers for clauses
% 2.11/2.50 *** allocated 75937 integers for termspace/termends
% 2.11/2.50 Resimplifying inuse:
% 2.11/2.50 Done
% 2.11/2.50
% 2.11/2.50 *** allocated 256285 integers for clauses
% 2.11/2.50
% 2.11/2.50 Intermediate Status:
% 2.11/2.50 Generated: 8814
% 2.11/2.50 Kept: 4206
% 2.11/2.50 Inuse: 310
% 2.11/2.50 Deleted: 9
% 2.11/2.50 Deletedinuse: 3
% 2.11/2.50
% 2.11/2.50 Resimplifying inuse:
% 2.11/2.50 Done
% 2.11/2.50
% 2.11/2.50 *** allocated 113905 integers for termspace/termends
% 2.11/2.50 Resimplifying inuse:
% 2.11/2.50 Done
% 2.11/2.50
% 2.11/2.50 *** allocated 384427 integers for clauses
% 2.11/2.50
% 2.11/2.50 Intermediate Status:
% 2.11/2.50 Generated: 14674
% 2.11/2.50 Kept: 6213
% 2.11/2.50 Inuse: 464
% 2.11/2.50 Deleted: 12
% 2.11/2.50 Deletedinuse: 5
% 2.11/2.50
% 2.11/2.50 Resimplifying inuse:
% 2.11/2.50 Done
% 2.11/2.50
% 2.11/2.50 *** allocated 170857 integers for termspace/termends
% 2.11/2.50 Resimplifying inuse:
% 2.11/2.50 Done
% 2.11/2.50
% 2.11/2.50
% 2.11/2.50 Intermediate Status:
% 2.11/2.50 Generated: 31488
% 2.11/2.50 Kept: 8239
% 2.11/2.50 Inuse: 722
% 2.11/2.50 Deleted: 52
% 2.11/2.50 Deletedinuse: 10
% 2.11/2.50
% 2.11/2.50 Resimplifying inuse:
% 2.11/2.50 Done
% 2.11/2.50
% 2.11/2.50 Resimplifying inuse:
% 2.11/2.50 Done
% 2.11/2.50
% 2.11/2.50 *** allocated 576640 integers for clauses
% 2.11/2.50
% 2.11/2.50 Intermediate Status:
% 2.11/2.50 Generated: 52260
% 2.11/2.50 Kept: 10258
% 2.11/2.50 Inuse: 873
% 2.11/2.50 Deleted: 99
% 2.11/2.50 Deletedinuse: 11
% 2.11/2.50
% 2.11/2.50 Resimplifying inuse:
% 2.11/2.50 Done
% 2.11/2.50
% 2.11/2.50 *** allocated 256285 integers for termspace/termends
% 2.11/2.50 Resimplifying inuse:
% 2.11/2.50 Done
% 2.11/2.50
% 2.11/2.50
% 2.11/2.50 Intermediate Status:
% 2.11/2.50 Generated: 66847
% 2.11/2.50 Kept: 12301
% 2.11/2.50 Inuse: 951
% 2.11/2.50 Deleted: 103
% 2.11/2.50 Deletedinuse: 11
% 2.11/2.50
% 2.11/2.50 Resimplifying inuse:
% 2.11/2.50 Done
% 2.11/2.50
% 2.11/2.50 Resimplifying inuse:
% 2.11/2.50 Done
% 2.11/2.50
% 2.11/2.50
% 2.11/2.50 Intermediate Status:
% 2.11/2.50 Generated: 75201
% 2.11/2.50 Kept: 14371
% 2.11/2.50 Inuse: 1013
% 2.11/2.50 Deleted: 103
% 2.11/2.50 Deletedinuse: 11
% 2.11/2.50
% 2.11/2.50 Resimplifying inuse:
% 2.11/2.50 Done
% 2.11/2.50
% 2.11/2.50 *** allocated 864960 integers for clauses
% 2.11/2.50 Resimplifying inuse:
% 2.11/2.50 Done
% 2.11/2.50
% 2.11/2.50
% 2.11/2.50 Intermediate Status:
% 2.11/2.50 Generated: 83919
% 2.11/2.50 Kept: 16407
% 2.11/2.50 Inuse: 1102
% 2.11/2.50 Deleted: 108
% 2.11/2.50 Deletedinuse: 11
% 2.11/2.50
% 2.11/2.50 Resimplifying inuse:
% 2.11/2.50 Done
% 2.11/2.50
% 2.11/2.50 *** allocated 384427 integers for termspace/termends
% 2.11/2.50
% 2.11/2.50 Bliksems!, er is een bewijs:
% 2.11/2.50 % SZS status Theorem
% 2.11/2.50 % SZS output start Refutation
% 2.11/2.50
% 2.11/2.50 (80) {G0,W18,D3,L4,V6,M4} I { ! shortest_path( T, U, Z ), ! precedes( X, Y
% 2.11/2.50 , Z ), ! tail_of( W ) = tail_of( X ), ! head_of( W ) = head_of( Y ) }.
% 2.11/2.50 (106) {G0,W4,D2,L1,V0,M1} I { shortest_path( skol14, skol15, skol13 ) }.
% 2.11/2.50 (107) {G0,W4,D2,L1,V0,M1} I { precedes( skol10, skol12, skol13 ) }.
% 2.11/2.50 (109) {G0,W5,D3,L1,V0,M1} I { tail_of( skol16 ) ==> tail_of( skol10 ) }.
% 2.11/2.50 (110) {G0,W5,D3,L1,V0,M1} I { head_of( skol16 ) ==> head_of( skol12 ) }.
% 2.11/2.50 (4800) {G1,W18,D3,L4,V5,M4} P(109,80);d(110) { ! shortest_path( X, Y, Z ),
% 2.11/2.50 ! precedes( T, U, Z ), ! tail_of( skol10 ) = tail_of( T ), ! head_of(
% 2.11/2.50 skol12 ) = head_of( U ) }.
% 2.11/2.50 (4810) {G2,W13,D3,L3,V4,M3} Q(4800) { ! shortest_path( X, Y, Z ), !
% 2.11/2.50 precedes( T, skol12, Z ), ! tail_of( skol10 ) = tail_of( T ) }.
% 2.11/2.50 (4811) {G3,W8,D2,L2,V3,M2} Q(4810) { ! shortest_path( X, Y, Z ), ! precedes
% 2.11/2.50 ( skol10, skol12, Z ) }.
% 2.11/2.50 (18024) {G4,W0,D0,L0,V0,M0} R(4811,106);r(107) { }.
% 2.11/2.50
% 2.11/2.50
% 2.11/2.50 % SZS output end Refutation
% 2.11/2.50 found a proof!
% 2.11/2.50
% 2.11/2.50
% 2.11/2.50 Unprocessed initial clauses:
% 2.11/2.50
% 2.11/2.50 (18026) {G0,W7,D3,L2,V1,M2} { ! edge( X ), ! head_of( X ) = tail_of( X )
% 2.11/2.50 }.
% 2.11/2.50 (18027) {G0,W5,D3,L2,V1,M2} { ! edge( X ), vertex( head_of( X ) ) }.
% 2.11/2.50 (18028) {G0,W5,D3,L2,V1,M2} { ! edge( X ), vertex( tail_of( X ) ) }.
% 2.11/2.50 (18029) {G0,W12,D3,L5,V4,M5} { ! complete, ! vertex( X ), ! vertex( Y ), X
% 2.11/2.50 = Y, edge( skol1( Z, T ) ) }.
% 2.11/2.50 (18030) {G0,W20,D3,L6,V2,M6} { ! complete, ! vertex( X ), ! vertex( Y ), X
% 2.11/2.50 = Y, alpha11( X, Y, skol1( X, Y ) ), alpha15( X, Y, skol1( X, Y ) ) }.
% 2.11/2.50 (18031) {G0,W8,D3,L2,V3,M2} { ! alpha15( X, Y, Z ), Y = head_of( Z ) }.
% 2.11/2.50 (18032) {G0,W8,D3,L2,V3,M2} { ! alpha15( X, Y, Z ), X = tail_of( Z ) }.
% 2.11/2.50 (18033) {G0,W8,D2,L2,V3,M2} { ! alpha15( X, Y, Z ), ! alpha1( X, Y, Z )
% 2.11/2.50 }.
% 2.11/2.50 (18034) {G0,W16,D3,L4,V3,M4} { ! Y = head_of( Z ), ! X = tail_of( Z ),
% 2.11/2.50 alpha1( X, Y, Z ), alpha15( X, Y, Z ) }.
% 2.11/2.50 (18035) {G0,W8,D2,L2,V3,M2} { ! alpha11( X, Y, Z ), alpha1( X, Y, Z ) }.
% 2.11/2.50 (18036) {G0,W12,D3,L3,V3,M3} { ! alpha11( X, Y, Z ), ! Y = head_of( Z ), !
% 2.11/2.50 X = tail_of( Z ) }.
% 2.11/2.50 (18037) {G0,W12,D3,L3,V3,M3} { ! alpha1( X, Y, Z ), Y = head_of( Z ),
% 2.11/2.50 alpha11( X, Y, Z ) }.
% 2.11/2.50 (18038) {G0,W12,D3,L3,V3,M3} { ! alpha1( X, Y, Z ), X = tail_of( Z ),
% 2.11/2.50 alpha11( X, Y, Z ) }.
% 2.11/2.50 (18039) {G0,W8,D3,L2,V3,M2} { ! alpha1( X, Y, Z ), X = head_of( Z ) }.
% 2.11/2.50 (18040) {G0,W8,D3,L2,V3,M2} { ! alpha1( X, Y, Z ), Y = tail_of( Z ) }.
% 2.11/2.50 (18041) {G0,W12,D3,L3,V3,M3} { ! X = head_of( Z ), ! Y = tail_of( Z ),
% 2.11/2.50 alpha1( X, Y, Z ) }.
% 2.11/2.50 (18042) {G0,W23,D3,L7,V4,M7} { ! vertex( X ), ! vertex( Y ), ! edge( T ),
% 2.11/2.50 ! X = tail_of( T ), ! Y = head_of( T ), ! Z = path_cons( T, empty ), path
% 2.11/2.50 ( X, Y, Z ) }.
% 2.11/2.50 (18043) {G0,W24,D3,L7,V5,M7} { ! vertex( X ), ! vertex( Y ), ! edge( T ),
% 2.11/2.50 ! X = tail_of( T ), ! path( head_of( T ), Y, U ), ! Z = path_cons( T, U )
% 2.11/2.50 , path( X, Y, Z ) }.
% 2.11/2.50 (18044) {G0,W7,D2,L2,V3,M2} { ! path( X, Y, Z ), alpha12( X, Y ) }.
% 2.11/2.50 (18045) {G0,W10,D3,L2,V5,M2} { ! path( X, Y, Z ), alpha16( X, skol2( X, T
% 2.11/2.50 , U ) ) }.
% 2.11/2.50 (18046) {G0,W11,D3,L2,V3,M2} { ! path( X, Y, Z ), alpha20( Y, Z, skol2( X
% 2.11/2.50 , Y, Z ) ) }.
% 2.11/2.50 (18047) {G0,W12,D2,L3,V3,M3} { ! alpha20( X, Y, Z ), alpha18( X, Y, Z ),
% 2.11/2.50 alpha21( X, Y, Z ) }.
% 2.11/2.50 (18048) {G0,W8,D2,L2,V3,M2} { ! alpha18( X, Y, Z ), alpha20( X, Y, Z ) }.
% 2.11/2.50 (18049) {G0,W8,D2,L2,V3,M2} { ! alpha21( X, Y, Z ), alpha20( X, Y, Z ) }.
% 2.11/2.50 (18050) {G0,W12,D4,L2,V4,M2} { ! alpha21( X, Y, Z ), Y = path_cons( Z,
% 2.11/2.50 skol3( T, Y, Z ) ) }.
% 2.11/2.50 (18051) {G0,W12,D3,L2,V3,M2} { ! alpha21( X, Y, Z ), path( head_of( Z ), X
% 2.11/2.50 , skol3( X, Y, Z ) ) }.
% 2.11/2.50 (18052) {G0,W8,D2,L2,V3,M2} { ! alpha21( X, Y, Z ), ! alpha2( X, Y, Z )
% 2.11/2.50 }.
% 2.11/2.50 (18053) {G0,W18,D3,L4,V4,M4} { ! path( head_of( Z ), X, T ), ! Y =
% 2.11/2.50 path_cons( Z, T ), alpha2( X, Y, Z ), alpha21( X, Y, Z ) }.
% 2.11/2.50 (18054) {G0,W8,D2,L2,V3,M2} { ! alpha18( X, Y, Z ), alpha2( X, Y, Z ) }.
% 2.11/2.50 (18055) {G0,W14,D3,L3,V4,M3} { ! alpha18( X, Y, Z ), ! path( head_of( Z )
% 2.11/2.50 , X, T ), ! Y = path_cons( Z, T ) }.
% 2.11/2.50 (18056) {G0,W16,D4,L3,V4,M3} { ! alpha2( X, Y, Z ), Y = path_cons( Z,
% 2.11/2.50 skol4( T, Y, Z ) ), alpha18( X, Y, Z ) }.
% 2.11/2.50 (18057) {G0,W16,D3,L3,V3,M3} { ! alpha2( X, Y, Z ), path( head_of( Z ), X
% 2.11/2.50 , skol4( X, Y, Z ) ), alpha18( X, Y, Z ) }.
% 2.11/2.50 (18058) {G0,W5,D2,L2,V2,M2} { ! alpha16( X, Y ), edge( Y ) }.
% 2.11/2.50 (18059) {G0,W7,D3,L2,V2,M2} { ! alpha16( X, Y ), X = tail_of( Y ) }.
% 2.11/2.50 (18060) {G0,W9,D3,L3,V2,M3} { ! edge( Y ), ! X = tail_of( Y ), alpha16( X
% 2.11/2.50 , Y ) }.
% 2.11/2.50 (18061) {G0,W5,D2,L2,V2,M2} { ! alpha12( X, Y ), vertex( X ) }.
% 2.11/2.50 (18062) {G0,W5,D2,L2,V2,M2} { ! alpha12( X, Y ), vertex( Y ) }.
% 2.11/2.50 (18063) {G0,W7,D2,L3,V2,M3} { ! vertex( X ), ! vertex( Y ), alpha12( X, Y
% 2.11/2.50 ) }.
% 2.11/2.50 (18064) {G0,W8,D3,L2,V3,M2} { ! alpha2( X, Y, Z ), X = head_of( Z ) }.
% 2.11/2.50 (18065) {G0,W9,D3,L2,V3,M2} { ! alpha2( X, Y, Z ), Y = path_cons( Z, empty
% 2.11/2.50 ) }.
% 2.11/2.50 (18066) {G0,W13,D3,L3,V3,M3} { ! X = head_of( Z ), ! Y = path_cons( Z,
% 2.11/2.50 empty ), alpha2( X, Y, Z ) }.
% 2.11/2.50 (18067) {G0,W9,D2,L3,V4,M3} { ! path( Z, T, X ), ! on_path( Y, X ), edge(
% 2.11/2.50 Y ) }.
% 2.11/2.50 (18068) {G0,W11,D3,L3,V4,M3} { ! path( Z, T, X ), ! on_path( Y, X ),
% 2.11/2.50 in_path( head_of( Y ), X ) }.
% 2.11/2.50 (18069) {G0,W11,D3,L3,V4,M3} { ! path( Z, T, X ), ! on_path( Y, X ),
% 2.11/2.50 in_path( tail_of( Y ), X ) }.
% 2.11/2.50 (18070) {G0,W9,D2,L3,V4,M3} { ! path( Z, T, X ), ! in_path( Y, X ), vertex
% 2.11/2.50 ( Y ) }.
% 2.11/2.50 (18071) {G0,W19,D4,L4,V5,M4} { ! path( Z, T, X ), ! in_path( Y, X ), Y =
% 2.11/2.50 head_of( skol5( U, Y ) ), Y = tail_of( skol5( U, Y ) ) }.
% 2.11/2.50 (18072) {G0,W12,D3,L3,V4,M3} { ! path( Z, T, X ), ! in_path( Y, X ),
% 2.11/2.50 on_path( skol5( X, Y ), X ) }.
% 2.11/2.50 (18073) {G0,W5,D2,L2,V2,M2} { ! sequential( X, Y ), edge( X ) }.
% 2.11/2.50 (18074) {G0,W6,D2,L2,V2,M2} { ! sequential( X, Y ), alpha3( X, Y ) }.
% 2.11/2.50 (18075) {G0,W8,D2,L3,V2,M3} { ! edge( X ), ! alpha3( X, Y ), sequential( X
% 2.11/2.50 , Y ) }.
% 2.11/2.50 (18076) {G0,W5,D2,L2,V2,M2} { ! alpha3( X, Y ), edge( Y ) }.
% 2.11/2.50 (18077) {G0,W6,D2,L2,V2,M2} { ! alpha3( X, Y ), alpha6( X, Y ) }.
% 2.11/2.50 (18078) {G0,W8,D2,L3,V2,M3} { ! edge( Y ), ! alpha6( X, Y ), alpha3( X, Y
% 2.11/2.50 ) }.
% 2.11/2.50 (18079) {G0,W6,D2,L2,V2,M2} { ! alpha6( X, Y ), ! X = Y }.
% 2.11/2.50 (18080) {G0,W8,D3,L2,V2,M2} { ! alpha6( X, Y ), head_of( X ) = tail_of( Y
% 2.11/2.50 ) }.
% 2.11/2.50 (18081) {G0,W11,D3,L3,V2,M3} { X = Y, ! head_of( X ) = tail_of( Y ),
% 2.11/2.50 alpha6( X, Y ) }.
% 2.11/2.50 (18082) {G0,W17,D2,L5,V5,M5} { ! path( Y, Z, X ), ! on_path( T, X ), !
% 2.11/2.50 on_path( U, X ), ! sequential( T, U ), precedes( T, U, X ) }.
% 2.11/2.50 (18083) {G0,W21,D2,L6,V6,M6} { ! path( Y, Z, X ), ! on_path( T, X ), !
% 2.11/2.50 on_path( U, X ), ! sequential( T, W ), ! precedes( W, U, X ), precedes( T
% 2.11/2.50 , U, X ) }.
% 2.11/2.50 (18084) {G0,W12,D2,L3,V5,M3} { ! path( Y, Z, X ), ! precedes( T, U, X ),
% 2.11/2.50 alpha13( X, T, U ) }.
% 2.11/2.50 (18085) {G0,W16,D2,L4,V5,M4} { ! path( Y, Z, X ), ! precedes( T, U, X ),
% 2.11/2.50 alpha17( X, T, U ), alpha19( X, T, U ) }.
% 2.11/2.50 (18086) {G0,W10,D3,L2,V5,M2} { ! alpha19( X, Y, Z ), sequential( Y, skol6
% 2.11/2.50 ( T, Y, U ) ) }.
% 2.11/2.50 (18087) {G0,W11,D3,L2,V3,M2} { ! alpha19( X, Y, Z ), precedes( skol6( X, Y
% 2.11/2.50 , Z ), Z, X ) }.
% 2.11/2.50 (18088) {G0,W7,D2,L2,V3,M2} { ! alpha19( X, Y, Z ), ! sequential( Y, Z )
% 2.11/2.50 }.
% 2.11/2.50 (18089) {G0,W14,D2,L4,V4,M4} { ! sequential( Y, T ), ! precedes( T, Z, X )
% 2.11/2.50 , sequential( Y, Z ), alpha19( X, Y, Z ) }.
% 2.11/2.50 (18090) {G0,W7,D2,L2,V3,M2} { ! alpha17( X, Y, Z ), sequential( Y, Z ) }.
% 2.11/2.50 (18091) {G0,W11,D2,L3,V4,M3} { ! alpha17( X, Y, Z ), ! sequential( Y, T )
% 2.11/2.50 , ! precedes( T, Z, X ) }.
% 2.11/2.50 (18092) {G0,W13,D3,L3,V5,M3} { ! sequential( Y, Z ), sequential( Y, skol7
% 2.11/2.50 ( T, Y, U ) ), alpha17( X, Y, Z ) }.
% 2.11/2.50 (18093) {G0,W14,D3,L3,V3,M3} { ! sequential( Y, Z ), precedes( skol7( X, Y
% 2.11/2.50 , Z ), Z, X ), alpha17( X, Y, Z ) }.
% 2.11/2.50 (18094) {G0,W7,D2,L2,V3,M2} { ! alpha13( X, Y, Z ), on_path( Y, X ) }.
% 2.11/2.50 (18095) {G0,W7,D2,L2,V3,M2} { ! alpha13( X, Y, Z ), on_path( Z, X ) }.
% 2.11/2.50 (18096) {G0,W10,D2,L3,V3,M3} { ! on_path( Y, X ), ! on_path( Z, X ),
% 2.11/2.50 alpha13( X, Y, Z ) }.
% 2.11/2.50 (18097) {G0,W8,D2,L2,V3,M2} { ! shortest_path( X, Y, Z ), path( X, Y, Z )
% 2.11/2.50 }.
% 2.11/2.50 (18098) {G0,W8,D2,L2,V3,M2} { ! shortest_path( X, Y, Z ), alpha4( X, Y, Z
% 2.11/2.50 ) }.
% 2.11/2.50 (18099) {G0,W12,D2,L3,V3,M3} { ! path( X, Y, Z ), ! alpha4( X, Y, Z ),
% 2.11/2.50 shortest_path( X, Y, Z ) }.
% 2.11/2.50 (18100) {G0,W7,D2,L2,V3,M2} { ! alpha4( X, Y, Z ), ! X = Y }.
% 2.11/2.50 (18101) {G0,W8,D2,L2,V3,M2} { ! alpha4( X, Y, Z ), alpha7( X, Y, Z ) }.
% 2.11/2.50 (18102) {G0,W11,D2,L3,V3,M3} { X = Y, ! alpha7( X, Y, Z ), alpha4( X, Y, Z
% 2.11/2.50 ) }.
% 2.11/2.50 (18103) {G0,W13,D3,L3,V4,M3} { ! alpha7( X, Y, Z ), ! path( X, Y, T ),
% 2.11/2.50 less_or_equal( length_of( Z ), length_of( T ) ) }.
% 2.11/2.50 (18104) {G0,W12,D4,L2,V5,M2} { ! less_or_equal( length_of( Z ), length_of
% 2.11/2.50 ( skol8( T, U, Z ) ) ), alpha7( X, Y, Z ) }.
% 2.11/2.50 (18105) {G0,W11,D3,L2,V3,M2} { path( X, Y, skol8( X, Y, Z ) ), alpha7( X,
% 2.11/2.50 Y, Z ) }.
% 2.11/2.50 (18106) {G0,W18,D3,L4,V6,M4} { ! shortest_path( T, U, Z ), ! precedes( X,
% 2.11/2.50 Y, Z ), ! tail_of( W ) = tail_of( X ), ! head_of( W ) = head_of( Y ) }.
% 2.11/2.50 (18107) {G0,W12,D2,L3,V5,M3} { ! shortest_path( T, U, Z ), ! precedes( X,
% 2.11/2.50 Y, Z ), ! precedes( Y, X, Z ) }.
% 2.11/2.50 (18108) {G0,W6,D2,L2,V3,M2} { ! triangle( X, Y, Z ), edge( X ) }.
% 2.11/2.50 (18109) {G0,W8,D2,L2,V3,M2} { ! triangle( X, Y, Z ), alpha5( X, Y, Z ) }.
% 2.11/2.50 (18110) {G0,W10,D2,L3,V3,M3} { ! edge( X ), ! alpha5( X, Y, Z ), triangle
% 2.11/2.50 ( X, Y, Z ) }.
% 2.11/2.50 (18111) {G0,W6,D2,L2,V3,M2} { ! alpha5( X, Y, Z ), edge( Y ) }.
% 2.11/2.50 (18112) {G0,W8,D2,L2,V3,M2} { ! alpha5( X, Y, Z ), alpha8( X, Y, Z ) }.
% 2.11/2.50 (18113) {G0,W10,D2,L3,V3,M3} { ! edge( Y ), ! alpha8( X, Y, Z ), alpha5( X
% 2.11/2.50 , Y, Z ) }.
% 2.11/2.50 (18114) {G0,W6,D2,L2,V3,M2} { ! alpha8( X, Y, Z ), edge( Z ) }.
% 2.11/2.50 (18115) {G0,W8,D2,L2,V3,M2} { ! alpha8( X, Y, Z ), alpha9( X, Y, Z ) }.
% 2.11/2.50 (18116) {G0,W10,D2,L3,V3,M3} { ! edge( Z ), ! alpha9( X, Y, Z ), alpha8( X
% 2.11/2.50 , Y, Z ) }.
% 2.11/2.50 (18117) {G0,W7,D2,L2,V3,M2} { ! alpha9( X, Y, Z ), sequential( X, Y ) }.
% 2.11/2.50 (18118) {G0,W8,D2,L2,V3,M2} { ! alpha9( X, Y, Z ), alpha10( X, Y, Z ) }.
% 2.11/2.50 (18119) {G0,W11,D2,L3,V3,M3} { ! sequential( X, Y ), ! alpha10( X, Y, Z )
% 2.11/2.50 , alpha9( X, Y, Z ) }.
% 2.11/2.50 (18120) {G0,W7,D2,L2,V3,M2} { ! alpha10( X, Y, Z ), sequential( Y, Z ) }.
% 2.11/2.50 (18121) {G0,W7,D2,L2,V3,M2} { ! alpha10( X, Y, Z ), sequential( Z, X ) }.
% 2.11/2.50 (18122) {G0,W10,D2,L3,V3,M3} { ! sequential( Y, Z ), ! sequential( Z, X )
% 2.11/2.50 , alpha10( X, Y, Z ) }.
% 2.11/2.50 (18123) {G0,W10,D3,L2,V3,M2} { ! path( Y, Z, X ), length_of( X ) =
% 2.11/2.50 number_of_in( edges, X ) }.
% 2.11/2.50 (18124) {G0,W12,D4,L2,V3,M2} { ! path( Y, Z, X ), number_of_in(
% 2.11/2.50 sequential_pairs, X ) = minus( length_of( X ), n1 ) }.
% 2.11/2.50 (18125) {G0,W17,D3,L3,V3,M3} { ! path( Y, Z, X ), alpha14( X, skol9( X ),
% 2.11/2.50 skol11( X ) ), number_of_in( sequential_pairs, X ) = number_of_in(
% 2.11/2.50 triangles, X ) }.
% 2.11/2.50 (18126) {G0,W17,D3,L3,V4,M3} { ! path( Y, Z, X ), ! triangle( skol9( X ),
% 2.11/2.50 skol11( X ), T ), number_of_in( sequential_pairs, X ) = number_of_in(
% 2.11/2.50 triangles, X ) }.
% 2.11/2.50 (18127) {G0,W7,D2,L2,V3,M2} { ! alpha14( X, Y, Z ), on_path( Y, X ) }.
% 2.11/2.50 (18128) {G0,W7,D2,L2,V3,M2} { ! alpha14( X, Y, Z ), on_path( Z, X ) }.
% 2.11/2.50 (18129) {G0,W7,D2,L2,V3,M2} { ! alpha14( X, Y, Z ), sequential( Y, Z ) }.
% 2.11/2.50 (18130) {G0,W13,D2,L4,V3,M4} { ! on_path( Y, X ), ! on_path( Z, X ), !
% 2.11/2.50 sequential( Y, Z ), alpha14( X, Y, Z ) }.
% 2.11/2.50 (18131) {G0,W7,D3,L1,V2,M1} { less_or_equal( number_of_in( X, Y ),
% 2.11/2.50 number_of_in( X, graph ) ) }.
% 2.11/2.50 (18132) {G0,W4,D2,L1,V0,M1} { shortest_path( skol14, skol15, skol13 ) }.
% 2.11/2.50 (18133) {G0,W4,D2,L1,V0,M1} { precedes( skol10, skol12, skol13 ) }.
% 2.11/2.50 (18134) {G0,W2,D2,L1,V0,M1} { edge( skol16 ) }.
% 2.11/2.50 (18135) {G0,W5,D3,L1,V0,M1} { tail_of( skol16 ) = tail_of( skol10 ) }.
% 2.11/2.50 (18136) {G0,W5,D3,L1,V0,M1} { head_of( skol16 ) = head_of( skol12 ) }.
% 2.11/2.50
% 2.11/2.50
% 2.11/2.50 Total Proof:
% 2.11/2.50
% 2.11/2.50 subsumption: (80) {G0,W18,D3,L4,V6,M4} I { ! shortest_path( T, U, Z ), !
% 2.11/2.50 precedes( X, Y, Z ), ! tail_of( W ) = tail_of( X ), ! head_of( W ) =
% 2.11/2.50 head_of( Y ) }.
% 2.11/2.50 parent0: (18106) {G0,W18,D3,L4,V6,M4} { ! shortest_path( T, U, Z ), !
% 2.11/2.50 precedes( X, Y, Z ), ! tail_of( W ) = tail_of( X ), ! head_of( W ) =
% 2.11/2.50 head_of( Y ) }.
% 2.11/2.50 substitution0:
% 2.11/2.50 X := X
% 2.11/2.50 Y := Y
% 2.11/2.50 Z := Z
% 2.11/2.50 T := T
% 2.11/2.50 U := U
% 2.11/2.50 W := W
% 2.11/2.50 end
% 2.11/2.50 permutation0:
% 2.11/2.50 0 ==> 0
% 2.11/2.50 1 ==> 1
% 2.11/2.50 2 ==> 2
% 2.11/2.50 3 ==> 3
% 2.11/2.50 end
% 2.11/2.50
% 2.11/2.50 subsumption: (106) {G0,W4,D2,L1,V0,M1} I { shortest_path( skol14, skol15,
% 2.11/2.50 skol13 ) }.
% 2.11/2.50 parent0: (18132) {G0,W4,D2,L1,V0,M1} { shortest_path( skol14, skol15,
% 2.11/2.50 skol13 ) }.
% 2.11/2.50 substitution0:
% 2.11/2.50 end
% 2.11/2.50 permutation0:
% 2.11/2.50 0 ==> 0
% 2.11/2.50 end
% 2.11/2.50
% 2.11/2.50 subsumption: (107) {G0,W4,D2,L1,V0,M1} I { precedes( skol10, skol12, skol13
% 2.11/2.50 ) }.
% 2.11/2.50 parent0: (18133) {G0,W4,D2,L1,V0,M1} { precedes( skol10, skol12, skol13 )
% 2.11/2.50 }.
% 2.11/2.50 substitution0:
% 2.11/2.50 end
% 2.11/2.50 permutation0:
% 2.11/2.50 0 ==> 0
% 2.11/2.50 end
% 2.11/2.50
% 2.11/2.50 subsumption: (109) {G0,W5,D3,L1,V0,M1} I { tail_of( skol16 ) ==> tail_of(
% 2.11/2.50 skol10 ) }.
% 2.11/2.50 parent0: (18135) {G0,W5,D3,L1,V0,M1} { tail_of( skol16 ) = tail_of( skol10
% 2.11/2.50 ) }.
% 2.11/2.50 substitution0:
% 2.11/2.50 end
% 2.11/2.50 permutation0:
% 2.11/2.50 0 ==> 0
% 2.11/2.50 end
% 2.11/2.50
% 2.11/2.50 subsumption: (110) {G0,W5,D3,L1,V0,M1} I { head_of( skol16 ) ==> head_of(
% 2.11/2.50 skol12 ) }.
% 2.11/2.50 parent0: (18136) {G0,W5,D3,L1,V0,M1} { head_of( skol16 ) = head_of( skol12
% 2.11/2.50 ) }.
% 2.11/2.50 substitution0:
% 2.11/2.50 end
% 2.11/2.50 permutation0:
% 2.11/2.50 0 ==> 0
% 2.11/2.50 end
% 2.11/2.50
% 2.11/2.50 eqswap: (18674) {G0,W18,D3,L4,V6,M4} { ! tail_of( Y ) = tail_of( X ), !
% 2.11/2.50 shortest_path( Z, T, U ), ! precedes( Y, W, U ), ! head_of( X ) = head_of
% 2.11/2.50 ( W ) }.
% 2.11/2.50 parent0[2]: (80) {G0,W18,D3,L4,V6,M4} I { ! shortest_path( T, U, Z ), !
% 2.11/2.50 precedes( X, Y, Z ), ! tail_of( W ) = tail_of( X ), ! head_of( W ) =
% 2.11/2.50 head_of( Y ) }.
% 2.11/2.50 substitution0:
% 2.11/2.50 X := Y
% 2.11/2.50 Y := W
% 2.11/2.50 Z := U
% 2.11/2.50 T := Z
% 2.11/2.50 U := T
% 2.11/2.50 W := X
% 2.11/2.50 end
% 2.11/2.50
% 2.11/2.50 paramod: (18679) {G1,W18,D3,L4,V5,M4} { ! tail_of( X ) = tail_of( skol10 )
% 2.11/2.50 , ! shortest_path( Y, Z, T ), ! precedes( X, U, T ), ! head_of( skol16 )
% 2.11/2.50 = head_of( U ) }.
% 2.11/2.50 parent0[0]: (109) {G0,W5,D3,L1,V0,M1} I { tail_of( skol16 ) ==> tail_of(
% 2.11/2.50 skol10 ) }.
% 2.11/2.50 parent1[0; 4]: (18674) {G0,W18,D3,L4,V6,M4} { ! tail_of( Y ) = tail_of( X
% 2.11/2.50 ), ! shortest_path( Z, T, U ), ! precedes( Y, W, U ), ! head_of( X ) =
% 2.11/2.50 head_of( W ) }.
% 2.11/2.50 substitution0:
% 2.11/2.50 end
% 2.11/2.50 substitution1:
% 2.11/2.50 X := skol16
% 2.11/2.50 Y := X
% 2.11/2.50 Z := Y
% 2.11/2.50 T := Z
% 2.11/2.50 U := T
% 2.11/2.50 W := U
% 2.11/2.50 end
% 2.11/2.50
% 2.11/2.50 paramod: (18680) {G1,W18,D3,L4,V5,M4} { ! head_of( skol12 ) = head_of( X )
% 2.11/2.50 , ! tail_of( Y ) = tail_of( skol10 ), ! shortest_path( Z, T, U ), !
% 2.11/2.50 precedes( Y, X, U ) }.
% 2.11/2.50 parent0[0]: (110) {G0,W5,D3,L1,V0,M1} I { head_of( skol16 ) ==> head_of(
% 2.11/2.50 skol12 ) }.
% 2.11/2.50 parent1[3; 2]: (18679) {G1,W18,D3,L4,V5,M4} { ! tail_of( X ) = tail_of(
% 2.11/2.50 skol10 ), ! shortest_path( Y, Z, T ), ! precedes( X, U, T ), ! head_of(
% 2.11/2.50 skol16 ) = head_of( U ) }.
% 2.11/2.50 substitution0:
% 2.11/2.50 end
% 2.11/2.50 substitution1:
% 2.11/2.50 X := Y
% 2.11/2.50 Y := Z
% 2.11/2.50 Z := T
% 2.11/2.50 T := U
% 2.11/2.50 U := X
% 2.11/2.50 end
% 2.11/2.50
% 2.11/2.50 eqswap: (18682) {G1,W18,D3,L4,V5,M4} { ! tail_of( skol10 ) = tail_of( X )
% 2.11/2.50 , ! head_of( skol12 ) = head_of( Y ), ! shortest_path( Z, T, U ), !
% 2.11/2.50 precedes( X, Y, U ) }.
% 2.11/2.50 parent0[1]: (18680) {G1,W18,D3,L4,V5,M4} { ! head_of( skol12 ) = head_of(
% 2.11/2.50 X ), ! tail_of( Y ) = tail_of( skol10 ), ! shortest_path( Z, T, U ), !
% 2.11/2.50 precedes( Y, X, U ) }.
% 2.11/2.50 substitution0:
% 2.11/2.50 X := Y
% 2.11/2.50 Y := X
% 2.11/2.50 Z := Z
% 2.11/2.50 T := T
% 2.11/2.50 U := U
% 2.11/2.50 end
% 2.11/2.50
% 2.11/2.50 subsumption: (4800) {G1,W18,D3,L4,V5,M4} P(109,80);d(110) { ! shortest_path
% 2.11/2.50 ( X, Y, Z ), ! precedes( T, U, Z ), ! tail_of( skol10 ) = tail_of( T ), !
% 2.11/2.50 head_of( skol12 ) = head_of( U ) }.
% 2.11/2.50 parent0: (18682) {G1,W18,D3,L4,V5,M4} { ! tail_of( skol10 ) = tail_of( X )
% 2.11/2.50 , ! head_of( skol12 ) = head_of( Y ), ! shortest_path( Z, T, U ), !
% 2.11/2.50 precedes( X, Y, U ) }.
% 2.11/2.50 substitution0:
% 2.11/2.50 X := T
% 2.11/2.50 Y := U
% 2.11/2.50 Z := X
% 2.11/2.50 T := Y
% 2.11/2.50 U := Z
% 2.11/2.50 end
% 2.11/2.50 permutation0:
% 2.11/2.50 0 ==> 2
% 2.11/2.50 1 ==> 3
% 2.11/2.50 2 ==> 0
% 2.11/2.50 3 ==> 1
% 2.11/2.50 end
% 2.11/2.50
% 2.11/2.50 eqswap: (18684) {G1,W18,D3,L4,V5,M4} { ! tail_of( X ) = tail_of( skol10 )
% 2.11/2.50 , ! shortest_path( Y, Z, T ), ! precedes( X, U, T ), ! head_of( skol12 )
% 2.11/2.50 = head_of( U ) }.
% 2.11/2.50 parent0[2]: (4800) {G1,W18,D3,L4,V5,M4} P(109,80);d(110) { ! shortest_path
% 2.11/2.50 ( X, Y, Z ), ! precedes( T, U, Z ), ! tail_of( skol10 ) = tail_of( T ), !
% 2.11/2.50 head_of( skol12 ) = head_of( U ) }.
% 2.11/2.50 substitution0:
% 2.11/2.50 X := Y
% 2.11/2.50 Y := Z
% 2.11/2.50 Z := T
% 2.11/2.50 T := X
% 2.11/2.50 U := U
% 2.11/2.50 end
% 2.11/2.50
% 2.11/2.50 eqrefl: (18688) {G0,W13,D3,L3,V4,M3} { ! tail_of( X ) = tail_of( skol10 )
% 2.11/2.50 , ! shortest_path( Y, Z, T ), ! precedes( X, skol12, T ) }.
% 2.11/2.50 parent0[3]: (18684) {G1,W18,D3,L4,V5,M4} { ! tail_of( X ) = tail_of(
% 2.11/2.50 skol10 ), ! shortest_path( Y, Z, T ), ! precedes( X, U, T ), ! head_of(
% 2.11/2.50 skol12 ) = head_of( U ) }.
% 2.11/2.50 substitution0:
% 2.11/2.50 X := X
% 2.11/2.50 Y := Y
% 2.11/2.50 Z := Z
% 2.11/2.50 T := T
% 2.11/2.50 U := skol12
% 2.11/2.50 end
% 2.11/2.50
% 2.11/2.50 eqswap: (18689) {G0,W13,D3,L3,V4,M3} { ! tail_of( skol10 ) = tail_of( X )
% 2.11/2.50 , ! shortest_path( Y, Z, T ), ! precedes( X, skol12, T ) }.
% 2.11/2.50 parent0[0]: (18688) {G0,W13,D3,L3,V4,M3} { ! tail_of( X ) = tail_of(
% 2.11/2.50 skol10 ), ! shortest_path( Y, Z, T ), ! precedes( X, skol12, T ) }.
% 2.11/2.50 substitution0:
% 2.11/2.50 X := X
% 2.11/2.50 Y := Y
% 2.11/2.50 Z := Z
% 2.11/2.50 T := T
% 2.11/2.50 end
% 2.11/2.50
% 2.11/2.50 subsumption: (4810) {G2,W13,D3,L3,V4,M3} Q(4800) { ! shortest_path( X, Y, Z
% 2.11/2.50 ), ! precedes( T, skol12, Z ), ! tail_of( skol10 ) = tail_of( T ) }.
% 2.11/2.50 parent0: (18689) {G0,W13,D3,L3,V4,M3} { ! tail_of( skol10 ) = tail_of( X )
% 2.11/2.50 , ! shortest_path( Y, Z, T ), ! precedes( X, skol12, T ) }.
% 2.11/2.50 substitution0:
% 2.11/2.50 X := T
% 2.11/2.50 Y := X
% 2.11/2.50 Z := Y
% 2.11/2.50 T := Z
% 2.11/2.50 end
% 2.11/2.50 permutation0:
% 2.11/2.50 0 ==> 2
% 2.11/2.50 1 ==> 0
% 2.11/2.50 2 ==> 1
% 2.11/2.50 end
% 2.11/2.50
% 2.11/2.50 eqswap: (18691) {G2,W13,D3,L3,V4,M3} { ! tail_of( X ) = tail_of( skol10 )
% 2.11/2.50 , ! shortest_path( Y, Z, T ), ! precedes( X, skol12, T ) }.
% 2.11/2.50 parent0[2]: (4810) {G2,W13,D3,L3,V4,M3} Q(4800) { ! shortest_path( X, Y, Z
% 2.11/2.50 ), ! precedes( T, skol12, Z ), ! tail_of( skol10 ) = tail_of( T ) }.
% 2.11/2.50 substitution0:
% 2.11/2.50 X := Y
% 2.11/2.50 Y := Z
% 2.11/2.50 Z := T
% 2.11/2.50 T := X
% 2.11/2.50 end
% 2.11/2.50
% 2.11/2.50 eqrefl: (18692) {G0,W8,D2,L2,V3,M2} { ! shortest_path( X, Y, Z ), !
% 2.11/2.50 precedes( skol10, skol12, Z ) }.
% 2.11/2.50 parent0[0]: (18691) {G2,W13,D3,L3,V4,M3} { ! tail_of( X ) = tail_of(
% 2.11/2.50 skol10 ), ! shortest_path( Y, Z, T ), ! precedes( X, skol12, T ) }.
% 2.11/2.50 substitution0:
% 2.11/2.50 X := skol10
% 2.11/2.50 Y := X
% 2.11/2.50 Z := Y
% 2.11/2.50 T := Z
% 2.11/2.50 end
% 2.11/2.50
% 2.11/2.50 subsumption: (4811) {G3,W8,D2,L2,V3,M2} Q(4810) { ! shortest_path( X, Y, Z
% 2.11/2.50 ), ! precedes( skol10, skol12, Z ) }.
% 2.11/2.50 parent0: (18692) {G0,W8,D2,L2,V3,M2} { ! shortest_path( X, Y, Z ), !
% 2.11/2.50 precedes( skol10, skol12, Z ) }.
% 2.11/2.50 substitution0:
% 2.11/2.50 X := X
% 2.11/2.50 Y := Y
% 2.11/2.50 Z := Z
% 2.11/2.50 end
% 2.11/2.50 permutation0:
% 2.11/2.50 0 ==> 0
% 2.11/2.50 1 ==> 1
% 2.11/2.50 end
% 2.11/2.50
% 2.11/2.50 resolution: (18693) {G1,W4,D2,L1,V0,M1} { ! precedes( skol10, skol12,
% 2.11/2.50 skol13 ) }.
% 2.11/2.50 parent0[0]: (4811) {G3,W8,D2,L2,V3,M2} Q(4810) { ! shortest_path( X, Y, Z )
% 2.11/2.50 , ! precedes( skol10, skol12, Z ) }.
% 2.11/2.50 parent1[0]: (106) {G0,W4,D2,L1,V0,M1} I { shortest_path( skol14, skol15,
% 2.11/2.50 skol13 ) }.
% 2.11/2.50 substitution0:
% 2.11/2.50 X := skol14
% 2.11/2.50 Y := skol15
% 2.11/2.50 Z := skol13
% 2.11/2.50 end
% 2.11/2.50 substitution1:
% 2.11/2.50 end
% 2.11/2.50
% 2.11/2.50 resolution: (18694) {G1,W0,D0,L0,V0,M0} { }.
% 2.11/2.50 parent0[0]: (18693) {G1,W4,D2,L1,V0,M1} { ! precedes( skol10, skol12,
% 2.11/2.50 skol13 ) }.
% 2.11/2.50 parent1[0]: (107) {G0,W4,D2,L1,V0,M1} I { precedes( skol10, skol12, skol13
% 2.11/2.50 ) }.
% 2.11/2.50 substitution0:
% 2.11/2.50 end
% 2.11/2.50 substitution1:
% 2.11/2.50 end
% 2.11/2.50
% 2.11/2.50 subsumption: (18024) {G4,W0,D0,L0,V0,M0} R(4811,106);r(107) { }.
% 2.11/2.50 parent0: (18694) {G1,W0,D0,L0,V0,M0} { }.
% 2.11/2.50 substitution0:
% 2.11/2.50 end
% 2.11/2.50 permutation0:
% 2.11/2.50 end
% 2.11/2.50
% 2.11/2.50 Proof check complete!
% 2.11/2.50
% 2.11/2.50 Memory use:
% 2.11/2.50
% 2.11/2.50 space for terms: 266346
% 2.11/2.50 space for clauses: 692390
% 2.11/2.50
% 2.11/2.50
% 2.11/2.50 clauses generated: 104598
% 2.11/2.50 clauses kept: 18025
% 2.11/2.50 clauses selected: 1272
% 2.11/2.50 clauses deleted: 133
% 2.11/2.50 clauses inuse deleted: 11
% 2.11/2.50
% 2.11/2.50 subsentry: 151398
% 2.11/2.50 literals s-matched: 108650
% 2.11/2.50 literals matched: 101436
% 2.11/2.50 full subsumption: 28204
% 2.11/2.50
% 2.11/2.50 checksum: 823123480
% 2.11/2.50
% 2.11/2.50
% 2.11/2.50 Bliksem ended
%------------------------------------------------------------------------------