%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : GRA010+2 : TPTP v9.3.1. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 08:40:47 AM UTC 2026
% Result : Theorem 30.44s 35.74s
% Output : Proof 30.44s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(no_loops,axiom,
! [E] :
( edge(E)
=> head_of(E) != tail_of(E) ),
file('GRA001+0.ax',no_loops) ).
fof(edge_ends_are_vertices,axiom,
! [E] :
( edge(E)
=> ( vertex(tail_of(E))
& vertex(head_of(E)) ) ),
file('GRA001+0.ax',edge_ends_are_vertices) ).
fof(complete_properties,axiom,
( complete
=> ! [V1,V2] :
( ( V1 != V2
& vertex(V2)
& vertex(V1) )
=> ? [E] :
( ( ( V1 = tail_of(E)
& V2 = head_of(E)
& ~ ( V2 = tail_of(E)
& V1 = head_of(E) ) )
| ( ~ ( V1 = tail_of(E)
& V2 = head_of(E) )
& V2 = tail_of(E)
& V1 = head_of(E) ) )
& edge(E) ) ) ),
file('GRA001+0.ax',complete_properties) ).
fof(path_defn,axiom,
! [V1,V2,P] :
( ( ? [E] :
( ( ? [TP] :
( P = path_cons(E,TP)
& path(head_of(E),V2,TP) )
| ( P = path_cons(E,empty)
& V2 = head_of(E) ) )
& V1 = tail_of(E)
& edge(E) )
& vertex(V2)
& vertex(V1) )
=> path(V1,V2,P) ),
file('GRA001+0.ax',path_defn) ).
fof(path_properties,axiom,
! [V1,V2,P] :
( path(V1,V2,P)
=> ( ? [E] :
( ( ( ? [TP] :
( P = path_cons(E,TP)
& path(head_of(E),V2,TP) )
& ~ ( P = path_cons(E,empty)
& V2 = head_of(E) ) )
| ( ~ ? [TP] :
( P = path_cons(E,TP)
& path(head_of(E),V2,TP) )
& P = path_cons(E,empty)
& V2 = head_of(E) ) )
& V1 = tail_of(E)
& edge(E) )
& vertex(V2)
& vertex(V1) ) ),
file('GRA001+0.ax',path_properties) ).
fof(on_path_properties,axiom,
! [V1,V2,P,E] :
( ( on_path(E,P)
& path(V1,V2,P) )
=> ( in_path(tail_of(E),P)
& in_path(head_of(E),P)
& edge(E) ) ),
file('GRA001+0.ax',on_path_properties) ).
fof(in_path_properties,axiom,
! [V1,V2,P,V] :
( ( in_path(V,P)
& path(V1,V2,P) )
=> ( ? [E] :
( ( V = tail_of(E)
| V = head_of(E) )
& on_path(E,P) )
& vertex(V) ) ),
file('GRA001+0.ax',in_path_properties) ).
fof(sequential_defn,axiom,
! [E1,E2] :
( sequential(E1,E2)
<=> ( head_of(E1) = tail_of(E2)
& E1 != E2
& edge(E2)
& edge(E1) ) ),
file('GRA001+0.ax',sequential_defn) ).
fof(precedes_defn,axiom,
! [P,V1,V2] :
( path(V1,V2,P)
=> ! [E1,E2] :
( ( ( ? [E3] :
( precedes(E3,E2,P)
& sequential(E1,E3) )
| sequential(E1,E2) )
& on_path(E2,P)
& on_path(E1,P) )
=> precedes(E1,E2,P) ) ),
file('GRA001+0.ax',precedes_defn) ).
fof(precedes_properties,axiom,
! [P,V1,V2] :
( path(V1,V2,P)
=> ! [E1,E2] :
( precedes(E1,E2,P)
=> ( ( ( ? [E3] :
( precedes(E3,E2,P)
& sequential(E1,E3) )
& ~ sequential(E1,E2) )
| ( ~ ? [E3] :
( precedes(E3,E2,P)
& sequential(E1,E3) )
& sequential(E1,E2) ) )
& on_path(E2,P)
& on_path(E1,P) ) ) ),
file('GRA001+0.ax',precedes_properties) ).
fof(shortest_path_defn,axiom,
! [V1,V2,SP] :
( shortest_path(V1,V2,SP)
<=> ( ! [P] :
( path(V1,V2,P)
=> less_or_equal(length_of(SP),length_of(P)) )
& V1 != V2
& path(V1,V2,SP) ) ),
file('GRA001+0.ax',shortest_path_defn) ).
fof(shortest_path_properties,axiom,
! [V1,V2,E1,E2,P] :
( ( precedes(E1,E2,P)
& shortest_path(V1,V2,P) )
=> ( ~ precedes(E2,E1,P)
& ~ ? [E3] :
( head_of(E3) = head_of(E2)
& tail_of(E3) = tail_of(E1) ) ) ),
file('GRA001+0.ax',shortest_path_properties) ).
fof(triangle_defn,axiom,
! [E1,E2,E3] :
( triangle(E1,E2,E3)
<=> ( sequential(E3,E1)
& sequential(E2,E3)
& sequential(E1,E2)
& edge(E3)
& edge(E2)
& edge(E1) ) ),
file('theBenchmark.p',triangle_defn) ).
fof(length_defn,axiom,
! [V1,V2,P] :
( path(V1,V2,P)
=> length_of(P) = number_of_in(edges,P) ),
file('theBenchmark.p',length_defn) ).
fof(path_length_sequential_pairs,axiom,
! [V1,V2,P] :
( path(V1,V2,P)
=> number_of_in(sequential_pairs,P) = minus(length_of(P),n1) ),
file('theBenchmark.p',path_length_sequential_pairs) ).
fof(sequential_pairs_and_triangles,axiom,
! [P,V1,V2] :
( ( ! [E1,E2] :
( ( sequential(E1,E2)
& on_path(E2,P)
& on_path(E1,P) )
=> ? [E3] : triangle(E1,E2,E3) )
& path(V1,V2,P) )
=> number_of_in(sequential_pairs,P) = number_of_in(triangles,P) ),
file('theBenchmark.p',sequential_pairs_and_triangles) ).
fof(graph_has_them_all,axiom,
! [Things,InThese] : less_or_equal(number_of_in(Things,InThese),number_of_in(Things,graph)),
file('theBenchmark.p',graph_has_them_all) ).
fof(sequential_is_triangle,lemma,
( complete
=> ! [V1,V2,E1,E2,P] :
( ( sequential(E1,E2)
& precedes(E1,E2,P)
& shortest_path(V1,V2,P) )
=> ? [E3] : triangle(E1,E2,E3) ) ),
file('theBenchmark.p',sequential_is_triangle) ).
fof(complete_means_sequential_pairs_and_triangles,conjecture,
( complete
=> ! [P,V1,V2] :
( ( ! [E1,E2] :
( ( sequential(E1,E2)
& on_path(E2,P)
& on_path(E1,P) )
=> ? [E3] : triangle(E1,E2,E3) )
& path(V1,V2,P) )
=> number_of_in(sequential_pairs,P) = number_of_in(triangles,P) ) ),
file('theBenchmark.p',complete_means_sequential_pairs_and_triangles) ).
fof(f_1_1,plain,
! [E] :
( head_of(E) != tail_of(E)
| ~ edge(E) ),
inference(fof_nnf,[status(thm)],[no_loops]) ).
fof(f_1_2,plain,
! [U_0] :
( head_of(U_0) != tail_of(U_0)
| ~ edge(U_0) ),
inference(variable_rename,[status(thm)],[f_1_1]) ).
fof(f_1_3,plain,
! [U_0] :
( head_of(U_0) != tail_of(U_0)
| ~ edge(U_0) ),
inference(definitional_conversion,[status(esa)],[f_1_2]) ).
cnf(f_1_4,plain,
( head_of(U_0) != tail_of(U_0)
| ~ edge(U_0) ),
inference(clausify,[status(thm)],[f_1_3]) ).
fof(f_2_1,plain,
! [E] :
( ( vertex(tail_of(E))
& vertex(head_of(E)) )
| ~ edge(E) ),
inference(fof_nnf,[status(thm)],[edge_ends_are_vertices]) ).
fof(f_2_2,plain,
! [U_1] :
( ( vertex(tail_of(U_1))
& vertex(head_of(U_1)) )
| ~ edge(U_1) ),
inference(variable_rename,[status(thm)],[f_2_1]) ).
fof(f_2_3,plain,
( ! [U_1] :
( vertex(tail_of(U_1))
| ~ sP0(U_1) )
& ! [U_1] :
( vertex(head_of(U_1))
| ~ sP0(U_1) )
& ! [U_1] :
( sP0(U_1)
| ~ edge(U_1) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0])],[f_2_2]) ).
cnf(f_2_4,plain,
( sP0(U_1)
| ~ edge(U_1) ),
inference(clausify,[status(thm)],[f_2_3]) ).
cnf(f_2_5,plain,
( vertex(head_of(U_1))
| ~ sP0(U_1) ),
inference(clausify,[status(thm)],[f_2_3]) ).
cnf(f_2_6,plain,
( vertex(tail_of(U_1))
| ~ sP0(U_1) ),
inference(clausify,[status(thm)],[f_2_3]) ).
fof(f_3_1,plain,
( ! [V1,V2] :
( ? [E] :
( ( ( V1 = tail_of(E)
& V2 = head_of(E)
& ( V2 != tail_of(E)
| V1 != head_of(E) ) )
| ( ( V1 != tail_of(E)
| V2 != head_of(E) )
& V2 = tail_of(E)
& V1 = head_of(E) ) )
& edge(E) )
| V1 = V2
| ~ vertex(V2)
| ~ vertex(V1) )
| ~ complete ),
inference(fof_nnf,[status(thm)],[complete_properties]) ).
fof(f_3_2,plain,
( ! [U_4,U_3] :
( ? [U_2] :
( ( ( U_4 = tail_of(U_2)
& U_3 = head_of(U_2)
& ( U_3 != tail_of(U_2)
| U_4 != head_of(U_2) ) )
| ( ( U_4 != tail_of(U_2)
| U_3 != head_of(U_2) )
& U_3 = tail_of(U_2)
& U_4 = head_of(U_2) ) )
& edge(U_2) )
| U_4 = U_3
| ~ vertex(U_3)
| ~ vertex(U_4) )
| ~ complete ),
inference(variable_rename,[status(thm)],[f_3_1]) ).
fof(f_3_3,plain,
( ! [U_4,U_3] :
( ( ( ( U_4 = tail_of(sK1(U_4,U_3))
& U_3 = head_of(sK1(U_4,U_3))
& ( U_3 != tail_of(sK1(U_4,U_3))
| U_4 != head_of(sK1(U_4,U_3)) ) )
| ( ( U_4 != tail_of(sK1(U_4,U_3))
| U_3 != head_of(sK1(U_4,U_3)) )
& U_3 = tail_of(sK1(U_4,U_3))
& U_4 = head_of(sK1(U_4,U_3)) ) )
& edge(sK1(U_4,U_3)) )
| U_4 = U_3
| ~ vertex(U_3)
| ~ vertex(U_4) )
| ~ complete ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_2,sK1(U_4,U_3))],[f_3_2]) ).
fof(f_3_4,plain,
( ! [U_3,U_4] :
( U_4 = tail_of(sK1(U_4,U_3))
| ~ sP2(U_3,U_4) )
& ! [U_3,U_4] :
( U_3 = head_of(sK1(U_4,U_3))
| ~ sP2(U_3,U_4) )
& ! [U_3,U_4] :
( U_3 != tail_of(sK1(U_4,U_3))
| U_4 != head_of(sK1(U_4,U_3))
| ~ sP2(U_3,U_4) )
& ! [U_3,U_4] :
( U_4 != tail_of(sK1(U_4,U_3))
| U_3 != head_of(sK1(U_4,U_3))
| ~ sP1(U_3,U_4) )
& ! [U_3,U_4] :
( U_3 = tail_of(sK1(U_4,U_3))
| ~ sP1(U_3,U_4) )
& ! [U_3,U_4] :
( U_4 = head_of(sK1(U_4,U_3))
| ~ sP1(U_3,U_4) )
& ! [U_3,U_4] :
( sP2(U_3,U_4)
| sP1(U_3,U_4)
| ~ sP3(U_3,U_4) )
& ! [U_3,U_4] :
( edge(sK1(U_4,U_3))
| ~ sP3(U_3,U_4) )
& ! [U_3,U_4] :
( sP3(U_3,U_4)
| U_4 = U_3
| ~ vertex(U_3)
| ~ vertex(U_4)
| ~ complete ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP1,sP2,sP3])],[f_3_3]) ).
cnf(f_3_5,plain,
( sP3(U_3,U_4)
| U_4 = U_3
| ~ vertex(U_3)
| ~ vertex(U_4)
| ~ complete ),
inference(clausify,[status(thm)],[f_3_4]) ).
cnf(f_3_6,plain,
( edge(sK1(U_4,U_3))
| ~ sP3(U_3,U_4) ),
inference(clausify,[status(thm)],[f_3_4]) ).
cnf(f_3_7,plain,
( sP2(U_3,U_4)
| sP1(U_3,U_4)
| ~ sP3(U_3,U_4) ),
inference(clausify,[status(thm)],[f_3_4]) ).
cnf(f_3_8,plain,
( U_4 = head_of(sK1(U_4,U_3))
| ~ sP1(U_3,U_4) ),
inference(clausify,[status(thm)],[f_3_4]) ).
cnf(f_3_9,plain,
( U_3 = tail_of(sK1(U_4,U_3))
| ~ sP1(U_3,U_4) ),
inference(clausify,[status(thm)],[f_3_4]) ).
cnf(f_3_10,plain,
( U_4 != tail_of(sK1(U_4,U_3))
| U_3 != head_of(sK1(U_4,U_3))
| ~ sP1(U_3,U_4) ),
inference(clausify,[status(thm)],[f_3_4]) ).
cnf(f_3_11,plain,
( U_3 != tail_of(sK1(U_4,U_3))
| U_4 != head_of(sK1(U_4,U_3))
| ~ sP2(U_3,U_4) ),
inference(clausify,[status(thm)],[f_3_4]) ).
cnf(f_3_12,plain,
( U_3 = head_of(sK1(U_4,U_3))
| ~ sP2(U_3,U_4) ),
inference(clausify,[status(thm)],[f_3_4]) ).
cnf(f_3_13,plain,
( U_4 = tail_of(sK1(U_4,U_3))
| ~ sP2(U_3,U_4) ),
inference(clausify,[status(thm)],[f_3_4]) ).
fof(f_4_1,plain,
! [V1,V2,P] :
( path(V1,V2,P)
| ! [E] :
( ( ! [TP] :
( P != path_cons(E,TP)
| ~ path(head_of(E),V2,TP) )
& ( P != path_cons(E,empty)
| V2 != head_of(E) ) )
| V1 != tail_of(E)
| ~ edge(E) )
| ~ vertex(V2)
| ~ vertex(V1) ),
inference(fof_nnf,[status(thm)],[path_defn]) ).
fof(f_4_2,plain,
! [U_9,U_8,U_7] :
( path(U_9,U_8,U_7)
| ! [U_6] :
( ( ! [U_5] :
( U_7 != path_cons(U_6,U_5)
| ~ path(head_of(U_6),U_8,U_5) )
& ( U_7 != path_cons(U_6,empty)
| U_8 != head_of(U_6) ) )
| U_9 != tail_of(U_6)
| ~ edge(U_6) )
| ~ vertex(U_8)
| ~ vertex(U_9) ),
inference(variable_rename,[status(thm)],[f_4_1]) ).
fof(f_4_3,plain,
( ! [U_8,U_5,U_7,U_6] :
( U_7 != path_cons(U_6,U_5)
| ~ path(head_of(U_6),U_8,U_5)
| ~ sP4(U_8,U_5,U_7,U_6) )
& ! [U_8,U_5,U_7,U_6] :
( U_7 != path_cons(U_6,empty)
| U_8 != head_of(U_6)
| ~ sP4(U_8,U_5,U_7,U_6) )
& ! [U_8,U_5,U_9,U_7,U_6] :
( path(U_9,U_8,U_7)
| sP4(U_8,U_5,U_7,U_6)
| U_9 != tail_of(U_6)
| ~ edge(U_6)
| ~ vertex(U_8)
| ~ vertex(U_9) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP4])],[f_4_2]) ).
cnf(f_4_4,plain,
( path(U_9,U_8,U_7)
| sP4(U_8,U_5,U_7,U_6)
| U_9 != tail_of(U_6)
| ~ edge(U_6)
| ~ vertex(U_8)
| ~ vertex(U_9) ),
inference(clausify,[status(thm)],[f_4_3]) ).
cnf(f_4_5,plain,
( U_7 != path_cons(U_6,empty)
| U_8 != head_of(U_6)
| ~ sP4(U_8,U_5,U_7,U_6) ),
inference(clausify,[status(thm)],[f_4_3]) ).
cnf(f_4_6,plain,
( U_7 != path_cons(U_6,U_5)
| ~ path(head_of(U_6),U_8,U_5)
| ~ sP4(U_8,U_5,U_7,U_6) ),
inference(clausify,[status(thm)],[f_4_3]) ).
fof(f_5_1,plain,
! [V1,V2,P] :
( ( ? [E] :
( ( ( ? [TP] :
( P = path_cons(E,TP)
& path(head_of(E),V2,TP) )
& ( P != path_cons(E,empty)
| V2 != head_of(E) ) )
| ( ! [TP] :
( P != path_cons(E,TP)
| ~ path(head_of(E),V2,TP) )
& P = path_cons(E,empty)
& V2 = head_of(E) ) )
& V1 = tail_of(E)
& edge(E) )
& vertex(V2)
& vertex(V1) )
| ~ path(V1,V2,P) ),
inference(fof_nnf,[status(thm)],[path_properties]) ).
fof(f_5_2,plain,
! [U_15,U_14,U_13] :
( ( ? [U_12] :
( ( ( ? [U_11] :
( U_13 = path_cons(U_12,U_11)
& path(head_of(U_12),U_14,U_11) )
& ( U_13 != path_cons(U_12,empty)
| U_14 != head_of(U_12) ) )
| ( ! [U_10] :
( U_13 != path_cons(U_12,U_10)
| ~ path(head_of(U_12),U_14,U_10) )
& U_13 = path_cons(U_12,empty)
& U_14 = head_of(U_12) ) )
& U_15 = tail_of(U_12)
& edge(U_12) )
& vertex(U_14)
& vertex(U_15) )
| ~ path(U_15,U_14,U_13) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
fof(f_5_3,plain,
! [U_15,U_14,U_13] :
( ( ( ( ? [U_11] :
( U_13 = path_cons(sK2(U_15,U_14,U_13),U_11)
& path(head_of(sK2(U_15,U_14,U_13)),U_14,U_11) )
& ( U_13 != path_cons(sK2(U_15,U_14,U_13),empty)
| U_14 != head_of(sK2(U_15,U_14,U_13)) ) )
| ( ! [U_10] :
( U_13 != path_cons(sK2(U_15,U_14,U_13),U_10)
| ~ path(head_of(sK2(U_15,U_14,U_13)),U_14,U_10) )
& U_13 = path_cons(sK2(U_15,U_14,U_13),empty)
& U_14 = head_of(sK2(U_15,U_14,U_13)) ) )
& U_15 = tail_of(sK2(U_15,U_14,U_13))
& edge(sK2(U_15,U_14,U_13))
& vertex(U_14)
& vertex(U_15) )
| ~ path(U_15,U_14,U_13) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_12,sK2(U_15,U_14,U_13))],[f_5_2]) ).
fof(f_5_4,plain,
! [U_15,U_14,U_13] :
( ( ( ( U_13 = path_cons(sK2(U_15,U_14,U_13),sK3(U_15,U_14,U_13))
& path(head_of(sK2(U_15,U_14,U_13)),U_14,sK3(U_15,U_14,U_13))
& ( U_13 != path_cons(sK2(U_15,U_14,U_13),empty)
| U_14 != head_of(sK2(U_15,U_14,U_13)) ) )
| ( ! [U_10] :
( U_13 != path_cons(sK2(U_15,U_14,U_13),U_10)
| ~ path(head_of(sK2(U_15,U_14,U_13)),U_14,U_10) )
& U_13 = path_cons(sK2(U_15,U_14,U_13),empty)
& U_14 = head_of(sK2(U_15,U_14,U_13)) ) )
& U_15 = tail_of(sK2(U_15,U_14,U_13))
& edge(sK2(U_15,U_14,U_13))
& vertex(U_14)
& vertex(U_15) )
| ~ path(U_15,U_14,U_13) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_11,sK3(U_15,U_14,U_13))],[f_5_3]) ).
fof(f_5_5,plain,
( ! [U_13,U_14,U_15] :
( U_13 = path_cons(sK2(U_15,U_14,U_13),sK3(U_15,U_14,U_13))
| ~ sP6(U_13,U_14,U_15) )
& ! [U_13,U_14,U_15] :
( path(head_of(sK2(U_15,U_14,U_13)),U_14,sK3(U_15,U_14,U_13))
| ~ sP6(U_13,U_14,U_15) )
& ! [U_13,U_14,U_15] :
( U_13 != path_cons(sK2(U_15,U_14,U_13),empty)
| U_14 != head_of(sK2(U_15,U_14,U_13))
| ~ sP6(U_13,U_14,U_15) )
& ! [U_13,U_14,U_15,U_10] :
( U_13 != path_cons(sK2(U_15,U_14,U_13),U_10)
| ~ path(head_of(sK2(U_15,U_14,U_13)),U_14,U_10)
| ~ sP5(U_13,U_14,U_15,U_10) )
& ! [U_13,U_14,U_15,U_10] :
( U_13 = path_cons(sK2(U_15,U_14,U_13),empty)
| ~ sP5(U_13,U_14,U_15,U_10) )
& ! [U_13,U_14,U_15,U_10] :
( U_14 = head_of(sK2(U_15,U_14,U_13))
| ~ sP5(U_13,U_14,U_15,U_10) )
& ! [U_13,U_14,U_15,U_10] :
( sP6(U_13,U_14,U_15)
| sP5(U_13,U_14,U_15,U_10)
| ~ sP7(U_13,U_14,U_15,U_10) )
& ! [U_13,U_14,U_15,U_10] :
( U_15 = tail_of(sK2(U_15,U_14,U_13))
| ~ sP7(U_13,U_14,U_15,U_10) )
& ! [U_13,U_14,U_15,U_10] :
( edge(sK2(U_15,U_14,U_13))
| ~ sP7(U_13,U_14,U_15,U_10) )
& ! [U_13,U_14,U_15,U_10] :
( vertex(U_14)
| ~ sP7(U_13,U_14,U_15,U_10) )
& ! [U_13,U_14,U_15,U_10] :
( vertex(U_15)
| ~ sP7(U_13,U_14,U_15,U_10) )
& ! [U_13,U_14,U_15,U_10] :
( sP7(U_13,U_14,U_15,U_10)
| ~ path(U_15,U_14,U_13) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP5,sP6,sP7])],[f_5_4]) ).
cnf(f_5_6,plain,
( sP7(U_13,U_14,U_15,U_10)
| ~ path(U_15,U_14,U_13) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_7,plain,
( vertex(U_15)
| ~ sP7(U_13,U_14,U_15,U_10) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_8,plain,
( vertex(U_14)
| ~ sP7(U_13,U_14,U_15,U_10) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_9,plain,
( edge(sK2(U_15,U_14,U_13))
| ~ sP7(U_13,U_14,U_15,U_10) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_10,plain,
( U_15 = tail_of(sK2(U_15,U_14,U_13))
| ~ sP7(U_13,U_14,U_15,U_10) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_11,plain,
( sP6(U_13,U_14,U_15)
| sP5(U_13,U_14,U_15,U_10)
| ~ sP7(U_13,U_14,U_15,U_10) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_12,plain,
( U_14 = head_of(sK2(U_15,U_14,U_13))
| ~ sP5(U_13,U_14,U_15,U_10) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_13,plain,
( U_13 = path_cons(sK2(U_15,U_14,U_13),empty)
| ~ sP5(U_13,U_14,U_15,U_10) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_14,plain,
( U_13 != path_cons(sK2(U_15,U_14,U_13),U_10)
| ~ path(head_of(sK2(U_15,U_14,U_13)),U_14,U_10)
| ~ sP5(U_13,U_14,U_15,U_10) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_15,plain,
( U_13 != path_cons(sK2(U_15,U_14,U_13),empty)
| U_14 != head_of(sK2(U_15,U_14,U_13))
| ~ sP6(U_13,U_14,U_15) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_16,plain,
( path(head_of(sK2(U_15,U_14,U_13)),U_14,sK3(U_15,U_14,U_13))
| ~ sP6(U_13,U_14,U_15) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_17,plain,
( U_13 = path_cons(sK2(U_15,U_14,U_13),sK3(U_15,U_14,U_13))
| ~ sP6(U_13,U_14,U_15) ),
inference(clausify,[status(thm)],[f_5_5]) ).
fof(f_6_1,plain,
! [V1,V2,P,E] :
( ( in_path(tail_of(E),P)
& in_path(head_of(E),P)
& edge(E) )
| ~ on_path(E,P)
| ~ path(V1,V2,P) ),
inference(fof_nnf,[status(thm)],[on_path_properties]) ).
fof(f_6_2,plain,
! [U_19,U_18,U_17,U_16] :
( ( in_path(tail_of(U_16),U_17)
& in_path(head_of(U_16),U_17)
& edge(U_16) )
| ~ on_path(U_16,U_17)
| ~ path(U_19,U_18,U_17) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
fof(f_6_3,plain,
( ! [U_16,U_17] :
( in_path(tail_of(U_16),U_17)
| ~ sP8(U_16,U_17) )
& ! [U_16,U_17] :
( in_path(head_of(U_16),U_17)
| ~ sP8(U_16,U_17) )
& ! [U_16,U_17] :
( edge(U_16)
| ~ sP8(U_16,U_17) )
& ! [U_16,U_19,U_17,U_18] :
( sP8(U_16,U_17)
| ~ on_path(U_16,U_17)
| ~ path(U_19,U_18,U_17) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP8])],[f_6_2]) ).
cnf(f_6_4,plain,
( sP8(U_16,U_17)
| ~ on_path(U_16,U_17)
| ~ path(U_19,U_18,U_17) ),
inference(clausify,[status(thm)],[f_6_3]) ).
cnf(f_6_5,plain,
( edge(U_16)
| ~ sP8(U_16,U_17) ),
inference(clausify,[status(thm)],[f_6_3]) ).
cnf(f_6_6,plain,
( in_path(head_of(U_16),U_17)
| ~ sP8(U_16,U_17) ),
inference(clausify,[status(thm)],[f_6_3]) ).
cnf(f_6_7,plain,
( in_path(tail_of(U_16),U_17)
| ~ sP8(U_16,U_17) ),
inference(clausify,[status(thm)],[f_6_3]) ).
fof(f_7_1,plain,
! [V1,V2,P,V] :
( ( ? [E] :
( ( V = tail_of(E)
| V = head_of(E) )
& on_path(E,P) )
& vertex(V) )
| ~ in_path(V,P)
| ~ path(V1,V2,P) ),
inference(fof_nnf,[status(thm)],[in_path_properties]) ).
fof(f_7_2,plain,
! [U_24,U_23,U_22,U_21] :
( ( ? [U_20] :
( ( U_21 = tail_of(U_20)
| U_21 = head_of(U_20) )
& on_path(U_20,U_22) )
& vertex(U_21) )
| ~ in_path(U_21,U_22)
| ~ path(U_24,U_23,U_22) ),
inference(variable_rename,[status(thm)],[f_7_1]) ).
fof(f_7_3,plain,
! [U_24,U_23,U_22,U_21] :
( ( ( U_21 = tail_of(sK4(U_24,U_23,U_22,U_21))
| U_21 = head_of(sK4(U_24,U_23,U_22,U_21)) )
& on_path(sK4(U_24,U_23,U_22,U_21),U_22)
& vertex(U_21) )
| ~ in_path(U_21,U_22)
| ~ path(U_24,U_23,U_22) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_20,sK4(U_24,U_23,U_22,U_21))],[f_7_2]) ).
fof(f_7_4,plain,
( ! [U_24,U_21,U_22,U_23] :
( U_21 = tail_of(sK4(U_24,U_23,U_22,U_21))
| U_21 = head_of(sK4(U_24,U_23,U_22,U_21))
| ~ sP9(U_24,U_21,U_22,U_23) )
& ! [U_24,U_21,U_22,U_23] :
( on_path(sK4(U_24,U_23,U_22,U_21),U_22)
| ~ sP9(U_24,U_21,U_22,U_23) )
& ! [U_24,U_21,U_22,U_23] :
( vertex(U_21)
| ~ sP9(U_24,U_21,U_22,U_23) )
& ! [U_24,U_21,U_22,U_23] :
( sP9(U_24,U_21,U_22,U_23)
| ~ in_path(U_21,U_22)
| ~ path(U_24,U_23,U_22) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP9])],[f_7_3]) ).
cnf(f_7_5,plain,
( sP9(U_24,U_21,U_22,U_23)
| ~ in_path(U_21,U_22)
| ~ path(U_24,U_23,U_22) ),
inference(clausify,[status(thm)],[f_7_4]) ).
cnf(f_7_6,plain,
( vertex(U_21)
| ~ sP9(U_24,U_21,U_22,U_23) ),
inference(clausify,[status(thm)],[f_7_4]) ).
cnf(f_7_7,plain,
( on_path(sK4(U_24,U_23,U_22,U_21),U_22)
| ~ sP9(U_24,U_21,U_22,U_23) ),
inference(clausify,[status(thm)],[f_7_4]) ).
cnf(f_7_8,plain,
( U_21 = tail_of(sK4(U_24,U_23,U_22,U_21))
| U_21 = head_of(sK4(U_24,U_23,U_22,U_21))
| ~ sP9(U_24,U_21,U_22,U_23) ),
inference(clausify,[status(thm)],[f_7_4]) ).
fof(f_8_1,plain,
! [E1,E2] :
( ( sequential(E1,E2)
| head_of(E1) != tail_of(E2)
| E1 = E2
| ~ edge(E2)
| ~ edge(E1) )
& ( ( head_of(E1) = tail_of(E2)
& E1 != E2
& edge(E2)
& edge(E1) )
| ~ sequential(E1,E2) ) ),
inference(fof_nnf,[status(thm)],[sequential_defn]) ).
fof(f_8_2,plain,
! [U_26,U_25] :
( ( sequential(U_26,U_25)
| head_of(U_26) != tail_of(U_25)
| U_26 = U_25
| ~ edge(U_25)
| ~ edge(U_26) )
& ( ( head_of(U_26) = tail_of(U_25)
& U_26 != U_25
& edge(U_25)
& edge(U_26) )
| ~ sequential(U_26,U_25) ) ),
inference(variable_rename,[status(thm)],[f_8_1]) ).
fof(f_8_3,plain,
( ! [U_30,U_28] :
( sequential(U_30,U_28)
| head_of(U_30) != tail_of(U_28)
| U_30 = U_28
| ~ edge(U_28)
| ~ edge(U_30) )
& ! [U_29,U_27] :
( ( head_of(U_29) = tail_of(U_27)
& U_29 != U_27
& edge(U_27)
& edge(U_29) )
| ~ sequential(U_29,U_27) ) ),
inference(miniscope,[status(thm)],[f_8_2]) ).
fof(f_8_4,plain,
( ! [U_27,U_29] :
( head_of(U_29) = tail_of(U_27)
| ~ sP10(U_27,U_29) )
& ! [U_27,U_29] :
( U_29 != U_27
| ~ sP10(U_27,U_29) )
& ! [U_27,U_29] :
( edge(U_27)
| ~ sP10(U_27,U_29) )
& ! [U_27,U_29] :
( edge(U_29)
| ~ sP10(U_27,U_29) )
& ! [U_30,U_28] :
( sequential(U_30,U_28)
| head_of(U_30) != tail_of(U_28)
| U_30 = U_28
| ~ edge(U_28)
| ~ edge(U_30) )
& ! [U_27,U_29] :
( sP10(U_27,U_29)
| ~ sequential(U_29,U_27) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP10])],[f_8_3]) ).
cnf(f_8_5,plain,
( sP10(U_27,U_29)
| ~ sequential(U_29,U_27) ),
inference(clausify,[status(thm)],[f_8_4]) ).
cnf(f_8_6,plain,
( sequential(U_30,U_28)
| head_of(U_30) != tail_of(U_28)
| U_30 = U_28
| ~ edge(U_28)
| ~ edge(U_30) ),
inference(clausify,[status(thm)],[f_8_4]) ).
cnf(f_8_7,plain,
( edge(U_29)
| ~ sP10(U_27,U_29) ),
inference(clausify,[status(thm)],[f_8_4]) ).
cnf(f_8_8,plain,
( edge(U_27)
| ~ sP10(U_27,U_29) ),
inference(clausify,[status(thm)],[f_8_4]) ).
cnf(f_8_9,plain,
( U_29 != U_27
| ~ sP10(U_27,U_29) ),
inference(clausify,[status(thm)],[f_8_4]) ).
cnf(f_8_10,plain,
( head_of(U_29) = tail_of(U_27)
| ~ sP10(U_27,U_29) ),
inference(clausify,[status(thm)],[f_8_4]) ).
fof(f_9_1,plain,
! [P,V1,V2] :
( ! [E1,E2] :
( precedes(E1,E2,P)
| ( ! [E3] :
( ~ precedes(E3,E2,P)
| ~ sequential(E1,E3) )
& ~ sequential(E1,E2) )
| ~ on_path(E2,P)
| ~ on_path(E1,P) )
| ~ path(V1,V2,P) ),
inference(fof_nnf,[status(thm)],[precedes_defn]) ).
fof(f_9_2,plain,
! [U_36,U_35,U_34] :
( ! [U_33,U_32] :
( precedes(U_33,U_32,U_36)
| ( ! [U_31] :
( ~ precedes(U_31,U_32,U_36)
| ~ sequential(U_33,U_31) )
& ~ sequential(U_33,U_32) )
| ~ on_path(U_32,U_36)
| ~ on_path(U_33,U_36) )
| ~ path(U_35,U_34,U_36) ),
inference(variable_rename,[status(thm)],[f_9_1]) ).
fof(f_9_3,plain,
! [U_36] :
( ! [U_35,U_34] : ~ path(U_35,U_34,U_36)
| ! [U_33,U_32] :
( precedes(U_33,U_32,U_36)
| ( ! [U_31] :
( ~ precedes(U_31,U_32,U_36)
| ~ sequential(U_33,U_31) )
& ~ sequential(U_33,U_32) )
| ~ on_path(U_32,U_36)
| ~ on_path(U_33,U_36) ) ),
inference(miniscope,[status(thm)],[f_9_2]) ).
fof(f_9_4,plain,
( ! [U_32,U_36,U_33,U_31] :
( ~ precedes(U_31,U_32,U_36)
| ~ sequential(U_33,U_31)
| ~ sP11(U_32,U_36,U_33,U_31) )
& ! [U_32,U_36,U_33,U_31] :
( ~ sequential(U_33,U_32)
| ~ sP11(U_32,U_36,U_33,U_31) )
& ! [U_32,U_34,U_35,U_36,U_33,U_31] :
( ~ path(U_35,U_34,U_36)
| precedes(U_33,U_32,U_36)
| sP11(U_32,U_36,U_33,U_31)
| ~ on_path(U_32,U_36)
| ~ on_path(U_33,U_36) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP11])],[f_9_3]) ).
cnf(f_9_5,plain,
( ~ path(U_35,U_34,U_36)
| precedes(U_33,U_32,U_36)
| sP11(U_32,U_36,U_33,U_31)
| ~ on_path(U_32,U_36)
| ~ on_path(U_33,U_36) ),
inference(clausify,[status(thm)],[f_9_4]) ).
cnf(f_9_6,plain,
( ~ sequential(U_33,U_32)
| ~ sP11(U_32,U_36,U_33,U_31) ),
inference(clausify,[status(thm)],[f_9_4]) ).
cnf(f_9_7,plain,
( ~ precedes(U_31,U_32,U_36)
| ~ sequential(U_33,U_31)
| ~ sP11(U_32,U_36,U_33,U_31) ),
inference(clausify,[status(thm)],[f_9_4]) ).
fof(f_10_1,plain,
! [P,V1,V2] :
( ! [E1,E2] :
( ( ( ( ? [E3] :
( precedes(E3,E2,P)
& sequential(E1,E3) )
& ~ sequential(E1,E2) )
| ( ! [E3] :
( ~ precedes(E3,E2,P)
| ~ sequential(E1,E3) )
& sequential(E1,E2) ) )
& on_path(E2,P)
& on_path(E1,P) )
| ~ precedes(E1,E2,P) )
| ~ path(V1,V2,P) ),
inference(fof_nnf,[status(thm)],[precedes_properties]) ).
fof(f_10_2,plain,
! [U_43,U_42,U_41] :
( ! [U_40,U_39] :
( ( ( ( ? [U_38] :
( precedes(U_38,U_39,U_43)
& sequential(U_40,U_38) )
& ~ sequential(U_40,U_39) )
| ( ! [U_37] :
( ~ precedes(U_37,U_39,U_43)
| ~ sequential(U_40,U_37) )
& sequential(U_40,U_39) ) )
& on_path(U_39,U_43)
& on_path(U_40,U_43) )
| ~ precedes(U_40,U_39,U_43) )
| ~ path(U_42,U_41,U_43) ),
inference(variable_rename,[status(thm)],[f_10_1]) ).
fof(f_10_3,plain,
! [U_43] :
( ! [U_42,U_41] : ~ path(U_42,U_41,U_43)
| ! [U_40,U_39] :
( ( ( ( ? [U_38] :
( precedes(U_38,U_39,U_43)
& sequential(U_40,U_38) )
& ~ sequential(U_40,U_39) )
| ( ! [U_37] :
( ~ precedes(U_37,U_39,U_43)
| ~ sequential(U_40,U_37) )
& sequential(U_40,U_39) ) )
& on_path(U_39,U_43)
& on_path(U_40,U_43) )
| ~ precedes(U_40,U_39,U_43) ) ),
inference(miniscope,[status(thm)],[f_10_2]) ).
fof(f_10_4,plain,
! [U_43] :
( ! [U_42,U_41] : ~ path(U_42,U_41,U_43)
| ! [U_40,U_39] :
( ( ( ( precedes(sK5(U_43,U_40,U_39),U_39,U_43)
& sequential(U_40,sK5(U_43,U_40,U_39))
& ~ sequential(U_40,U_39) )
| ( ! [U_37] :
( ~ precedes(U_37,U_39,U_43)
| ~ sequential(U_40,U_37) )
& sequential(U_40,U_39) ) )
& on_path(U_39,U_43)
& on_path(U_40,U_43) )
| ~ precedes(U_40,U_39,U_43) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_38,sK5(U_43,U_40,U_39))],[f_10_3]) ).
fof(f_10_5,plain,
( ! [U_40,U_39,U_43] :
( precedes(sK5(U_43,U_40,U_39),U_39,U_43)
| ~ sP13(U_40,U_39,U_43) )
& ! [U_40,U_39,U_43] :
( sequential(U_40,sK5(U_43,U_40,U_39))
| ~ sP13(U_40,U_39,U_43) )
& ! [U_40,U_39,U_43] :
( ~ sequential(U_40,U_39)
| ~ sP13(U_40,U_39,U_43) )
& ! [U_40,U_39,U_43,U_37] :
( ~ precedes(U_37,U_39,U_43)
| ~ sequential(U_40,U_37)
| ~ sP12(U_40,U_39,U_43,U_37) )
& ! [U_40,U_39,U_43,U_37] :
( sequential(U_40,U_39)
| ~ sP12(U_40,U_39,U_43,U_37) )
& ! [U_40,U_39,U_43,U_37] :
( sP13(U_40,U_39,U_43)
| sP12(U_40,U_39,U_43,U_37)
| ~ sP14(U_40,U_39,U_43,U_37) )
& ! [U_40,U_39,U_43,U_37] :
( on_path(U_39,U_43)
| ~ sP14(U_40,U_39,U_43,U_37) )
& ! [U_40,U_39,U_43,U_37] :
( on_path(U_40,U_43)
| ~ sP14(U_40,U_39,U_43,U_37) )
& ! [U_40,U_41,U_42,U_39,U_43,U_37] :
( ~ path(U_42,U_41,U_43)
| sP14(U_40,U_39,U_43,U_37)
| ~ precedes(U_40,U_39,U_43) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP12,sP13,sP14])],[f_10_4]) ).
cnf(f_10_6,plain,
( ~ path(U_42,U_41,U_43)
| sP14(U_40,U_39,U_43,U_37)
| ~ precedes(U_40,U_39,U_43) ),
inference(clausify,[status(thm)],[f_10_5]) ).
cnf(f_10_7,plain,
( on_path(U_40,U_43)
| ~ sP14(U_40,U_39,U_43,U_37) ),
inference(clausify,[status(thm)],[f_10_5]) ).
cnf(f_10_8,plain,
( on_path(U_39,U_43)
| ~ sP14(U_40,U_39,U_43,U_37) ),
inference(clausify,[status(thm)],[f_10_5]) ).
cnf(f_10_9,plain,
( sP13(U_40,U_39,U_43)
| sP12(U_40,U_39,U_43,U_37)
| ~ sP14(U_40,U_39,U_43,U_37) ),
inference(clausify,[status(thm)],[f_10_5]) ).
cnf(f_10_10,plain,
( sequential(U_40,U_39)
| ~ sP12(U_40,U_39,U_43,U_37) ),
inference(clausify,[status(thm)],[f_10_5]) ).
cnf(f_10_11,plain,
( ~ precedes(U_37,U_39,U_43)
| ~ sequential(U_40,U_37)
| ~ sP12(U_40,U_39,U_43,U_37) ),
inference(clausify,[status(thm)],[f_10_5]) ).
cnf(f_10_12,plain,
( ~ sequential(U_40,U_39)
| ~ sP13(U_40,U_39,U_43) ),
inference(clausify,[status(thm)],[f_10_5]) ).
cnf(f_10_13,plain,
( sequential(U_40,sK5(U_43,U_40,U_39))
| ~ sP13(U_40,U_39,U_43) ),
inference(clausify,[status(thm)],[f_10_5]) ).
cnf(f_10_14,plain,
( precedes(sK5(U_43,U_40,U_39),U_39,U_43)
| ~ sP13(U_40,U_39,U_43) ),
inference(clausify,[status(thm)],[f_10_5]) ).
fof(f_11_1,plain,
! [V1,V2,SP] :
( ( shortest_path(V1,V2,SP)
| ? [P] :
( ~ less_or_equal(length_of(SP),length_of(P))
& path(V1,V2,P) )
| V1 = V2
| ~ path(V1,V2,SP) )
& ( ( ! [P] :
( less_or_equal(length_of(SP),length_of(P))
| ~ path(V1,V2,P) )
& V1 != V2
& path(V1,V2,SP) )
| ~ shortest_path(V1,V2,SP) ) ),
inference(fof_nnf,[status(thm)],[shortest_path_defn]) ).
fof(f_11_2,plain,
! [U_48,U_47,U_46] :
( ( shortest_path(U_48,U_47,U_46)
| ? [U_45] :
( ~ less_or_equal(length_of(U_46),length_of(U_45))
& path(U_48,U_47,U_45) )
| U_48 = U_47
| ~ path(U_48,U_47,U_46) )
& ( ( ! [U_44] :
( less_or_equal(length_of(U_46),length_of(U_44))
| ~ path(U_48,U_47,U_44) )
& U_48 != U_47
& path(U_48,U_47,U_46) )
| ~ shortest_path(U_48,U_47,U_46) ) ),
inference(variable_rename,[status(thm)],[f_11_1]) ).
fof(f_11_3,plain,
( ! [U_54,U_52,U_50] :
( shortest_path(U_54,U_52,U_50)
| ? [U_45] :
( ~ less_or_equal(length_of(U_50),length_of(U_45))
& path(U_54,U_52,U_45) )
| U_54 = U_52
| ~ path(U_54,U_52,U_50) )
& ! [U_53,U_51,U_49] :
( ( ! [U_44] :
( less_or_equal(length_of(U_49),length_of(U_44))
| ~ path(U_53,U_51,U_44) )
& U_53 != U_51
& path(U_53,U_51,U_49) )
| ~ shortest_path(U_53,U_51,U_49) ) ),
inference(miniscope,[status(thm)],[f_11_2]) ).
fof(f_11_4,plain,
( ! [U_54,U_52,U_50] :
( shortest_path(U_54,U_52,U_50)
| ( ~ less_or_equal(length_of(U_50),length_of(sK6(U_54,U_52,U_50)))
& path(U_54,U_52,sK6(U_54,U_52,U_50)) )
| U_54 = U_52
| ~ path(U_54,U_52,U_50) )
& ! [U_53,U_51,U_49] :
( ( ! [U_44] :
( less_or_equal(length_of(U_49),length_of(U_44))
| ~ path(U_53,U_51,U_44) )
& U_53 != U_51
& path(U_53,U_51,U_49) )
| ~ shortest_path(U_53,U_51,U_49) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_45,sK6(U_54,U_52,U_50))],[f_11_3]) ).
fof(f_11_5,plain,
( ! [U_52,U_54,U_50] :
( ~ less_or_equal(length_of(U_50),length_of(sK6(U_54,U_52,U_50)))
| ~ sP16(U_52,U_54,U_50) )
& ! [U_52,U_54,U_50] :
( path(U_54,U_52,sK6(U_54,U_52,U_50))
| ~ sP16(U_52,U_54,U_50) )
& ! [U_51,U_49,U_44,U_53] :
( less_or_equal(length_of(U_49),length_of(U_44))
| ~ path(U_53,U_51,U_44)
| ~ sP15(U_51,U_49,U_44,U_53) )
& ! [U_51,U_49,U_44,U_53] :
( U_53 != U_51
| ~ sP15(U_51,U_49,U_44,U_53) )
& ! [U_51,U_49,U_44,U_53] :
( path(U_53,U_51,U_49)
| ~ sP15(U_51,U_49,U_44,U_53) )
& ! [U_52,U_54,U_50] :
( shortest_path(U_54,U_52,U_50)
| sP16(U_52,U_54,U_50)
| U_54 = U_52
| ~ path(U_54,U_52,U_50) )
& ! [U_51,U_49,U_44,U_53] :
( sP15(U_51,U_49,U_44,U_53)
| ~ shortest_path(U_53,U_51,U_49) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP15,sP16])],[f_11_4]) ).
cnf(f_11_6,plain,
( sP15(U_51,U_49,U_44,U_53)
| ~ shortest_path(U_53,U_51,U_49) ),
inference(clausify,[status(thm)],[f_11_5]) ).
cnf(f_11_7,plain,
( shortest_path(U_54,U_52,U_50)
| sP16(U_52,U_54,U_50)
| U_54 = U_52
| ~ path(U_54,U_52,U_50) ),
inference(clausify,[status(thm)],[f_11_5]) ).
cnf(f_11_8,plain,
( path(U_53,U_51,U_49)
| ~ sP15(U_51,U_49,U_44,U_53) ),
inference(clausify,[status(thm)],[f_11_5]) ).
cnf(f_11_9,plain,
( U_53 != U_51
| ~ sP15(U_51,U_49,U_44,U_53) ),
inference(clausify,[status(thm)],[f_11_5]) ).
cnf(f_11_10,plain,
( less_or_equal(length_of(U_49),length_of(U_44))
| ~ path(U_53,U_51,U_44)
| ~ sP15(U_51,U_49,U_44,U_53) ),
inference(clausify,[status(thm)],[f_11_5]) ).
cnf(f_11_11,plain,
( path(U_54,U_52,sK6(U_54,U_52,U_50))
| ~ sP16(U_52,U_54,U_50) ),
inference(clausify,[status(thm)],[f_11_5]) ).
cnf(f_11_12,plain,
( ~ less_or_equal(length_of(U_50),length_of(sK6(U_54,U_52,U_50)))
| ~ sP16(U_52,U_54,U_50) ),
inference(clausify,[status(thm)],[f_11_5]) ).
fof(f_12_1,plain,
! [V1,V2,E1,E2,P] :
( ( ~ precedes(E2,E1,P)
& ! [E3] :
( head_of(E3) != head_of(E2)
| tail_of(E3) != tail_of(E1) ) )
| ~ precedes(E1,E2,P)
| ~ shortest_path(V1,V2,P) ),
inference(fof_nnf,[status(thm)],[shortest_path_properties]) ).
fof(f_12_2,plain,
! [U_60,U_59,U_58,U_57,U_56] :
( ( ~ precedes(U_57,U_58,U_56)
& ! [U_55] :
( head_of(U_55) != head_of(U_57)
| tail_of(U_55) != tail_of(U_58) ) )
| ~ precedes(U_58,U_57,U_56)
| ~ shortest_path(U_60,U_59,U_56) ),
inference(variable_rename,[status(thm)],[f_12_1]) ).
fof(f_12_3,plain,
( ! [U_58,U_56,U_55,U_57] :
( ~ precedes(U_57,U_58,U_56)
| ~ sP17(U_58,U_56,U_55,U_57) )
& ! [U_58,U_56,U_55,U_57] :
( head_of(U_55) != head_of(U_57)
| tail_of(U_55) != tail_of(U_58)
| ~ sP17(U_58,U_56,U_55,U_57) )
& ! [U_58,U_59,U_56,U_60,U_55,U_57] :
( sP17(U_58,U_56,U_55,U_57)
| ~ precedes(U_58,U_57,U_56)
| ~ shortest_path(U_60,U_59,U_56) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP17])],[f_12_2]) ).
cnf(f_12_4,plain,
( sP17(U_58,U_56,U_55,U_57)
| ~ precedes(U_58,U_57,U_56)
| ~ shortest_path(U_60,U_59,U_56) ),
inference(clausify,[status(thm)],[f_12_3]) ).
cnf(f_12_5,plain,
( head_of(U_55) != head_of(U_57)
| tail_of(U_55) != tail_of(U_58)
| ~ sP17(U_58,U_56,U_55,U_57) ),
inference(clausify,[status(thm)],[f_12_3]) ).
cnf(f_12_6,plain,
( ~ precedes(U_57,U_58,U_56)
| ~ sP17(U_58,U_56,U_55,U_57) ),
inference(clausify,[status(thm)],[f_12_3]) ).
fof(f_13_1,plain,
! [E1,E2,E3] :
( ( triangle(E1,E2,E3)
| ~ sequential(E3,E1)
| ~ sequential(E2,E3)
| ~ sequential(E1,E2)
| ~ edge(E3)
| ~ edge(E2)
| ~ edge(E1) )
& ( ( sequential(E3,E1)
& sequential(E2,E3)
& sequential(E1,E2)
& edge(E3)
& edge(E2)
& edge(E1) )
| ~ triangle(E1,E2,E3) ) ),
inference(fof_nnf,[status(thm)],[triangle_defn]) ).
fof(f_13_2,plain,
! [U_63,U_62,U_61] :
( ( triangle(U_63,U_62,U_61)
| ~ sequential(U_61,U_63)
| ~ sequential(U_62,U_61)
| ~ sequential(U_63,U_62)
| ~ edge(U_61)
| ~ edge(U_62)
| ~ edge(U_63) )
& ( ( sequential(U_61,U_63)
& sequential(U_62,U_61)
& sequential(U_63,U_62)
& edge(U_61)
& edge(U_62)
& edge(U_63) )
| ~ triangle(U_63,U_62,U_61) ) ),
inference(variable_rename,[status(thm)],[f_13_1]) ).
fof(f_13_3,plain,
( ! [U_69,U_67,U_65] :
( triangle(U_69,U_67,U_65)
| ~ sequential(U_65,U_69)
| ~ sequential(U_67,U_65)
| ~ sequential(U_69,U_67)
| ~ edge(U_65)
| ~ edge(U_67)
| ~ edge(U_69) )
& ! [U_68,U_66,U_64] :
( ( sequential(U_64,U_68)
& sequential(U_66,U_64)
& sequential(U_68,U_66)
& edge(U_64)
& edge(U_66)
& edge(U_68) )
| ~ triangle(U_68,U_66,U_64) ) ),
inference(miniscope,[status(thm)],[f_13_2]) ).
fof(f_13_4,plain,
( ! [U_66,U_68,U_64] :
( sequential(U_64,U_68)
| ~ sP18(U_66,U_68,U_64) )
& ! [U_66,U_68,U_64] :
( sequential(U_66,U_64)
| ~ sP18(U_66,U_68,U_64) )
& ! [U_66,U_68,U_64] :
( sequential(U_68,U_66)
| ~ sP18(U_66,U_68,U_64) )
& ! [U_66,U_68,U_64] :
( edge(U_64)
| ~ sP18(U_66,U_68,U_64) )
& ! [U_66,U_68,U_64] :
( edge(U_66)
| ~ sP18(U_66,U_68,U_64) )
& ! [U_66,U_68,U_64] :
( edge(U_68)
| ~ sP18(U_66,U_68,U_64) )
& ! [U_67,U_69,U_65] :
( triangle(U_69,U_67,U_65)
| ~ sequential(U_65,U_69)
| ~ sequential(U_67,U_65)
| ~ sequential(U_69,U_67)
| ~ edge(U_65)
| ~ edge(U_67)
| ~ edge(U_69) )
& ! [U_66,U_68,U_64] :
( sP18(U_66,U_68,U_64)
| ~ triangle(U_68,U_66,U_64) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP18])],[f_13_3]) ).
cnf(f_13_5,plain,
( sP18(U_66,U_68,U_64)
| ~ triangle(U_68,U_66,U_64) ),
inference(clausify,[status(thm)],[f_13_4]) ).
cnf(f_13_6,plain,
( triangle(U_69,U_67,U_65)
| ~ sequential(U_65,U_69)
| ~ sequential(U_67,U_65)
| ~ sequential(U_69,U_67)
| ~ edge(U_65)
| ~ edge(U_67)
| ~ edge(U_69) ),
inference(clausify,[status(thm)],[f_13_4]) ).
cnf(f_13_7,plain,
( edge(U_68)
| ~ sP18(U_66,U_68,U_64) ),
inference(clausify,[status(thm)],[f_13_4]) ).
cnf(f_13_8,plain,
( edge(U_66)
| ~ sP18(U_66,U_68,U_64) ),
inference(clausify,[status(thm)],[f_13_4]) ).
cnf(f_13_9,plain,
( edge(U_64)
| ~ sP18(U_66,U_68,U_64) ),
inference(clausify,[status(thm)],[f_13_4]) ).
cnf(f_13_10,plain,
( sequential(U_68,U_66)
| ~ sP18(U_66,U_68,U_64) ),
inference(clausify,[status(thm)],[f_13_4]) ).
cnf(f_13_11,plain,
( sequential(U_66,U_64)
| ~ sP18(U_66,U_68,U_64) ),
inference(clausify,[status(thm)],[f_13_4]) ).
cnf(f_13_12,plain,
( sequential(U_64,U_68)
| ~ sP18(U_66,U_68,U_64) ),
inference(clausify,[status(thm)],[f_13_4]) ).
fof(f_14_1,plain,
! [V1,V2,P] :
( length_of(P) = number_of_in(edges,P)
| ~ path(V1,V2,P) ),
inference(fof_nnf,[status(thm)],[length_defn]) ).
fof(f_14_2,plain,
! [U_72,U_71,U_70] :
( length_of(U_70) = number_of_in(edges,U_70)
| ~ path(U_72,U_71,U_70) ),
inference(variable_rename,[status(thm)],[f_14_1]) ).
fof(f_14_3,plain,
! [U_71,U_72,U_70] :
( length_of(U_70) = number_of_in(edges,U_70)
| ~ path(U_72,U_71,U_70) ),
inference(definitional_conversion,[status(esa)],[f_14_2]) ).
cnf(f_14_4,plain,
( length_of(U_70) = number_of_in(edges,U_70)
| ~ path(U_72,U_71,U_70) ),
inference(clausify,[status(thm)],[f_14_3]) ).
fof(f_15_1,plain,
! [V1,V2,P] :
( number_of_in(sequential_pairs,P) = minus(length_of(P),n1)
| ~ path(V1,V2,P) ),
inference(fof_nnf,[status(thm)],[path_length_sequential_pairs]) ).
fof(f_15_2,plain,
! [U_75,U_74,U_73] :
( number_of_in(sequential_pairs,U_73) = minus(length_of(U_73),n1)
| ~ path(U_75,U_74,U_73) ),
inference(variable_rename,[status(thm)],[f_15_1]) ).
fof(f_15_3,plain,
! [U_73,U_75,U_74] :
( number_of_in(sequential_pairs,U_73) = minus(length_of(U_73),n1)
| ~ path(U_75,U_74,U_73) ),
inference(definitional_conversion,[status(esa)],[f_15_2]) ).
cnf(f_15_4,plain,
( number_of_in(sequential_pairs,U_73) = minus(length_of(U_73),n1)
| ~ path(U_75,U_74,U_73) ),
inference(clausify,[status(thm)],[f_15_3]) ).
fof(f_16_1,plain,
! [P,V1,V2] :
( number_of_in(sequential_pairs,P) = number_of_in(triangles,P)
| ? [E1,E2] :
( ! [E3] : ~ triangle(E1,E2,E3)
& sequential(E1,E2)
& on_path(E2,P)
& on_path(E1,P) )
| ~ path(V1,V2,P) ),
inference(fof_nnf,[status(thm)],[sequential_pairs_and_triangles]) ).
fof(f_16_2,plain,
! [U_81,U_80,U_79] :
( number_of_in(sequential_pairs,U_81) = number_of_in(triangles,U_81)
| ? [U_78,U_77] :
( ! [U_76] : ~ triangle(U_78,U_77,U_76)
& sequential(U_78,U_77)
& on_path(U_77,U_81)
& on_path(U_78,U_81) )
| ~ path(U_80,U_79,U_81) ),
inference(variable_rename,[status(thm)],[f_16_1]) ).
fof(f_16_3,plain,
! [U_81] :
( ! [U_80,U_79] : ~ path(U_80,U_79,U_81)
| ? [U_78,U_77] :
( ! [U_76] : ~ triangle(U_78,U_77,U_76)
& sequential(U_78,U_77)
& on_path(U_77,U_81)
& on_path(U_78,U_81) )
| number_of_in(sequential_pairs,U_81) = number_of_in(triangles,U_81) ),
inference(miniscope,[status(thm)],[f_16_2]) ).
fof(f_16_4,plain,
! [U_81] :
( ! [U_80,U_79] : ~ path(U_80,U_79,U_81)
| ? [U_77] :
( ! [U_76] : ~ triangle(sK7(U_81),U_77,U_76)
& sequential(sK7(U_81),U_77)
& on_path(U_77,U_81)
& on_path(sK7(U_81),U_81) )
| number_of_in(sequential_pairs,U_81) = number_of_in(triangles,U_81) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_78,sK7(U_81))],[f_16_3]) ).
fof(f_16_5,plain,
! [U_81] :
( ! [U_80,U_79] : ~ path(U_80,U_79,U_81)
| ( ! [U_76] : ~ triangle(sK7(U_81),sK8(U_81),U_76)
& sequential(sK7(U_81),sK8(U_81))
& on_path(sK8(U_81),U_81)
& on_path(sK7(U_81),U_81) )
| number_of_in(sequential_pairs,U_81) = number_of_in(triangles,U_81) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_77,sK8(U_81))],[f_16_4]) ).
fof(f_16_6,plain,
( ! [U_76,U_81] :
( ~ triangle(sK7(U_81),sK8(U_81),U_76)
| ~ sP19(U_76,U_81) )
& ! [U_76,U_81] :
( sequential(sK7(U_81),sK8(U_81))
| ~ sP19(U_76,U_81) )
& ! [U_76,U_81] :
( on_path(sK8(U_81),U_81)
| ~ sP19(U_76,U_81) )
& ! [U_76,U_81] :
( on_path(sK7(U_81),U_81)
| ~ sP19(U_76,U_81) )
& ! [U_79,U_76,U_80,U_81] :
( ~ path(U_80,U_79,U_81)
| sP19(U_76,U_81)
| number_of_in(sequential_pairs,U_81) = number_of_in(triangles,U_81) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP19])],[f_16_5]) ).
cnf(f_16_7,plain,
( ~ path(U_80,U_79,U_81)
| sP19(U_76,U_81)
| number_of_in(sequential_pairs,U_81) = number_of_in(triangles,U_81) ),
inference(clausify,[status(thm)],[f_16_6]) ).
cnf(f_16_8,plain,
( on_path(sK7(U_81),U_81)
| ~ sP19(U_76,U_81) ),
inference(clausify,[status(thm)],[f_16_6]) ).
cnf(f_16_9,plain,
( on_path(sK8(U_81),U_81)
| ~ sP19(U_76,U_81) ),
inference(clausify,[status(thm)],[f_16_6]) ).
cnf(f_16_10,plain,
( sequential(sK7(U_81),sK8(U_81))
| ~ sP19(U_76,U_81) ),
inference(clausify,[status(thm)],[f_16_6]) ).
cnf(f_16_11,plain,
( ~ triangle(sK7(U_81),sK8(U_81),U_76)
| ~ sP19(U_76,U_81) ),
inference(clausify,[status(thm)],[f_16_6]) ).
fof(f_17_1,plain,
! [Things,InThese] : less_or_equal(number_of_in(Things,InThese),number_of_in(Things,graph)),
inference(fof_nnf,[status(thm)],[graph_has_them_all]) ).
fof(f_17_2,plain,
! [U_83,U_82] : less_or_equal(number_of_in(U_83,U_82),number_of_in(U_83,graph)),
inference(variable_rename,[status(thm)],[f_17_1]) ).
fof(f_17_3,plain,
! [U_83,U_82] : less_or_equal(number_of_in(U_83,U_82),number_of_in(U_83,graph)),
inference(definitional_conversion,[status(esa)],[f_17_2]) ).
cnf(f_17_4,plain,
less_or_equal(number_of_in(U_83,U_82),number_of_in(U_83,graph)),
inference(clausify,[status(thm)],[f_17_3]) ).
fof(f_18_1,plain,
( ! [V1,V2,E1,E2,P] :
( ? [E3] : triangle(E1,E2,E3)
| ~ sequential(E1,E2)
| ~ precedes(E1,E2,P)
| ~ shortest_path(V1,V2,P) )
| ~ complete ),
inference(fof_nnf,[status(thm)],[sequential_is_triangle]) ).
fof(f_18_2,plain,
( ! [U_89,U_88,U_87,U_86,U_85] :
( ? [U_84] : triangle(U_87,U_86,U_84)
| ~ sequential(U_87,U_86)
| ~ precedes(U_87,U_86,U_85)
| ~ shortest_path(U_89,U_88,U_85) )
| ~ complete ),
inference(variable_rename,[status(thm)],[f_18_1]) ).
fof(f_18_3,plain,
( ! [U_89,U_88,U_87,U_86] :
( ! [U_85] :
( ~ precedes(U_87,U_86,U_85)
| ~ shortest_path(U_89,U_88,U_85) )
| ~ sequential(U_87,U_86)
| ? [U_84] : triangle(U_87,U_86,U_84) )
| ~ complete ),
inference(miniscope,[status(thm)],[f_18_2]) ).
fof(f_18_4,plain,
( ! [U_89,U_88,U_87,U_86] :
( ! [U_85] :
( ~ precedes(U_87,U_86,U_85)
| ~ shortest_path(U_89,U_88,U_85) )
| ~ sequential(U_87,U_86)
| triangle(U_87,U_86,sK9(U_89,U_88,U_87,U_86)) )
| ~ complete ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_84,sK9(U_89,U_88,U_87,U_86))],[f_18_3]) ).
fof(f_18_5,plain,
! [U_85,U_86,U_87,U_88,U_89] :
( ~ precedes(U_87,U_86,U_85)
| ~ shortest_path(U_89,U_88,U_85)
| ~ sequential(U_87,U_86)
| triangle(U_87,U_86,sK9(U_89,U_88,U_87,U_86))
| ~ complete ),
inference(definitional_conversion,[status(esa)],[f_18_4]) ).
cnf(f_18_6,plain,
( ~ precedes(U_87,U_86,U_85)
| ~ shortest_path(U_89,U_88,U_85)
| ~ sequential(U_87,U_86)
| triangle(U_87,U_86,sK9(U_89,U_88,U_87,U_86))
| ~ complete ),
inference(clausify,[status(thm)],[f_18_5]) ).
fof(f_19_1,negated_conjecture,
( ~ ! [P,V1,V2] :
( ( ! [E1,E2] :
( ( sequential(E1,E2)
& on_path(E2,P)
& on_path(E1,P) )
=> ? [E3] : triangle(E1,E2,E3) )
& path(V1,V2,P) )
=> number_of_in(sequential_pairs,P) = number_of_in(triangles,P) )
& complete ),
inference(negate,[status(cth)],[complete_means_sequential_pairs_and_triangles]) ).
fof(f_19_2,negated_conjecture,
( ? [P,V1,V2] :
( number_of_in(sequential_pairs,P) != number_of_in(triangles,P)
& ! [E1,E2] :
( ? [E3] : triangle(E1,E2,E3)
| ~ sequential(E1,E2)
| ~ on_path(E2,P)
| ~ on_path(E1,P) )
& path(V1,V2,P) )
& complete ),
inference(fof_nnf,[status(thm)],[f_19_1]) ).
fof(f_19_3,negated_conjecture,
( ? [U_95,U_94,U_93] :
( number_of_in(sequential_pairs,U_95) != number_of_in(triangles,U_95)
& ! [U_92,U_91] :
( ? [U_90] : triangle(U_92,U_91,U_90)
| ~ sequential(U_92,U_91)
| ~ on_path(U_91,U_95)
| ~ on_path(U_92,U_95) )
& path(U_94,U_93,U_95) )
& complete ),
inference(variable_rename,[status(thm)],[f_19_2]) ).
fof(f_19_4,negated_conjecture,
( ? [U_95] :
( ? [U_94,U_93] : path(U_94,U_93,U_95)
& ! [U_92,U_91] :
( ? [U_90] : triangle(U_92,U_91,U_90)
| ~ sequential(U_92,U_91)
| ~ on_path(U_91,U_95)
| ~ on_path(U_92,U_95) )
& number_of_in(sequential_pairs,U_95) != number_of_in(triangles,U_95) )
& complete ),
inference(miniscope,[status(thm)],[f_19_3]) ).
fof(f_19_5,negated_conjecture,
( ? [U_94,U_93] : path(U_94,U_93,sK10)
& ! [U_92,U_91] :
( ? [U_90] : triangle(U_92,U_91,U_90)
| ~ sequential(U_92,U_91)
| ~ on_path(U_91,sK10)
| ~ on_path(U_92,sK10) )
& number_of_in(sequential_pairs,sK10) != number_of_in(triangles,sK10)
& complete ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(U_95,sK10)],[f_19_4]) ).
fof(f_19_6,negated_conjecture,
( ? [U_94,U_93] : path(U_94,U_93,sK10)
& ! [U_92,U_91] :
( triangle(U_92,U_91,sK11(U_92,U_91))
| ~ sequential(U_92,U_91)
| ~ on_path(U_91,sK10)
| ~ on_path(U_92,sK10) )
& number_of_in(sequential_pairs,sK10) != number_of_in(triangles,sK10)
& complete ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(U_90,sK11(U_92,U_91))],[f_19_5]) ).
fof(f_19_7,negated_conjecture,
( ? [U_93] : path(sK12,U_93,sK10)
& ! [U_92,U_91] :
( triangle(U_92,U_91,sK11(U_92,U_91))
| ~ sequential(U_92,U_91)
| ~ on_path(U_91,sK10)
| ~ on_path(U_92,sK10) )
& number_of_in(sequential_pairs,sK10) != number_of_in(triangles,sK10)
& complete ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(U_94,sK12)],[f_19_6]) ).
fof(f_19_8,negated_conjecture,
( path(sK12,sK13,sK10)
& ! [U_92,U_91] :
( triangle(U_92,U_91,sK11(U_92,U_91))
| ~ sequential(U_92,U_91)
| ~ on_path(U_91,sK10)
| ~ on_path(U_92,sK10) )
& number_of_in(sequential_pairs,sK10) != number_of_in(triangles,sK10)
& complete ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(U_93,sK13)],[f_19_7]) ).
fof(f_19_9,negated_conjecture,
( path(sK12,sK13,sK10)
& ! [U_92,U_91] :
( triangle(U_92,U_91,sK11(U_92,U_91))
| ~ sequential(U_92,U_91)
| ~ on_path(U_91,sK10)
| ~ on_path(U_92,sK10) )
& number_of_in(sequential_pairs,sK10) != number_of_in(triangles,sK10)
& complete ),
inference(definitional_conversion,[status(esa)],[f_19_8]) ).
cnf(f_19_10,negated_conjecture,
complete,
inference(clausify,[status(thm)],[f_19_9]) ).
cnf(f_19_11,negated_conjecture,
number_of_in(sequential_pairs,sK10) != number_of_in(triangles,sK10),
inference(clausify,[status(thm)],[f_19_9]) ).
cnf(f_19_12,negated_conjecture,
( triangle(U_92,U_91,sK11(U_92,U_91))
| ~ sequential(U_92,U_91)
| ~ on_path(U_91,sK10)
| ~ on_path(U_92,sK10) ),
inference(clausify,[status(thm)],[f_19_9]) ).
cnf(f_19_13,negated_conjecture,
path(sK12,sK13,sK10),
inference(clausify,[status(thm)],[f_19_9]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( head_of(Eq_x_0) = head_of(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( tail_of(Eq_x_0) = tail_of(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( path_cons(Eq_x_0,Eq_x_1) = path_cons(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( length_of(Eq_x_0) = length_of(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( number_of_in(Eq_x_0,Eq_x_1) = number_of_in(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_9,axiom,
( minus(Eq_x_0,Eq_x_1) = minus(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_10,axiom,
( sK1(Eq_x_0,Eq_x_1) = sK1(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_11,axiom,
( sK2(Eq_x_0,Eq_x_1,Eq_x_2) = sK2(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_12,axiom,
( sK3(Eq_x_0,Eq_x_1,Eq_x_2) = sK3(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_13,axiom,
( sK4(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = sK4(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_14,axiom,
( sK5(Eq_x_0,Eq_x_1,Eq_x_2) = sK5(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_15,axiom,
( sK6(Eq_x_0,Eq_x_1,Eq_x_2) = sK6(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_16,axiom,
( sK7(Eq_x_0) = sK7(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_17,axiom,
( sK8(Eq_x_0) = sK8(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_18,axiom,
( sK9(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3) = sK9(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_19,axiom,
( sK11(Eq_x_0,Eq_x_1) = sK11(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_20,axiom,
( edge(Eq_y_0)
| ~ edge(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_21,axiom,
( vertex(Eq_y_0)
| ~ vertex(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_22,axiom,
( path(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ path(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_23,axiom,
( on_path(Eq_y_0,Eq_y_1)
| ~ on_path(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_24,axiom,
( in_path(Eq_y_0,Eq_y_1)
| ~ in_path(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_25,axiom,
( sequential(Eq_y_0,Eq_y_1)
| ~ sequential(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_26,axiom,
( precedes(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ precedes(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_27,axiom,
( shortest_path(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ shortest_path(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_28,axiom,
( less_or_equal(Eq_y_0,Eq_y_1)
| ~ less_or_equal(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_29,axiom,
( triangle(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ triangle(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_30,axiom,
( sP0(Eq_y_0)
| ~ sP0(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_31,axiom,
( sP1(Eq_y_0,Eq_y_1)
| ~ sP1(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_32,axiom,
( sP2(Eq_y_0,Eq_y_1)
| ~ sP2(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_33,axiom,
( sP3(Eq_y_0,Eq_y_1)
| ~ sP3(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_34,axiom,
( sP4(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ sP4(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_35,axiom,
( sP5(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ sP5(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_36,axiom,
( sP6(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ sP6(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_37,axiom,
( sP7(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ sP7(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_38,axiom,
( sP8(Eq_y_0,Eq_y_1)
| ~ sP8(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_39,axiom,
( sP9(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ sP9(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_40,axiom,
( sP10(Eq_y_0,Eq_y_1)
| ~ sP10(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_41,axiom,
( sP11(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ sP11(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_42,axiom,
( sP12(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ sP12(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_43,axiom,
( sP13(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ sP13(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_44,axiom,
( sP14(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ sP14(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_45,axiom,
( sP15(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ sP15(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_46,axiom,
( sP16(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ sP16(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_47,axiom,
( sP17(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3)
| ~ sP17(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3)
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_48,axiom,
( sP18(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ sP18(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_49,axiom,
( sP19(Eq_y_0,Eq_y_1)
| ~ sP19(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRA010+2 : TPTP v9.3.1. Bugfixed v3.2.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/5.37 % Computer : n011.cluster.edu
% 0.08/5.37 % Model : x86_64 x86_64
% 0.08/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.37 % Memory : 8046.5625MB
% 0.08/5.37 % OS : Linux 6.8.0-71-generic
% 0.08/5.37 % CPULimit : 300
% 0.08/5.37 % WCLimit : 300
% 0.08/5.37 % DateTime : Sat Sep 19 08:19:30 UTC 2026
% 0.08/5.38 % CPUTime :
% 30.44/35.74 % SZS status Theorem for theBenchmark
% 30.44/35.74 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------