%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : GRA003+1 : TPTP v9.0.0. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n025.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 : 300s
% DateTime : Thu Jul 24 01:41:51 PM UTC 2025
% Result : Theorem 13.34s 2.08s
% Output : CNFRefutation 13.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 6
% Syntax : Number of formulae : 53 ( 16 unt; 0 def)
% Number of atoms : 150 ( 24 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 159 ( 62 ~; 55 |; 31 &)
% ( 1 <=>; 8 =>; 0 <=; 2 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-3 aty)
% Number of variables : 70 ( 15 sgn 31 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(vertices_and_edges,plain,
! [V1,V2,E1,E2,P] :
( ( shortest_path(V1,V2,P)
& precedes(E1,E2,P) )
=> ( vertex(V1)
& vertex(V2)
& V1 != V2
& edge(E1)
& edge(E2)
& E1 != E2
& path(V1,V2,P) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',vertices_and_edges) ).
fof(vertices_and_edges_negated,plain,
~ ! [V1,V2,E1,E2,P] :
( ( shortest_path(V1,V2,P)
& precedes(E1,E2,P) )
=> ( vertex(V1)
& vertex(V2)
& V1 != V2
& edge(E1)
& edge(E2)
& E1 != E2
& path(V1,V2,P) ) ),
inference(negate_conjecture,[status(cth)],[vertices_and_edges]) ).
cnf(61,plain,
( ~ vertex(sK11)
| ~ vertex(sK12)
| ~ edge(sK13)
| ~ edge(sK14)
| ~ path(sK11,sK12,sK15)
| sK11 = sK12
| sK13 = sK14 ),
inference(cnf,[status(esa)],[vertices_and_edges_negated]) ).
cnf(l0,plain,
( ~ vertex(sK11)
| ~ vertex(sK12)
| ~ edge(sK13)
| ~ edge(sK14)
| ~ path(sK11,sK12,sK15)
| sK11 = sK12
| sK13 = sK14 ),
inference(instantiation,[status(thm)],[61]) ).
fof(on_path_properties,plain,
! [V1,V2,P,E] :
( ( path(V1,V2,P)
& on_path(E,P) )
=> ( edge(E)
& in_path(head_of(E),P)
& in_path(tail_of(E),P) ) ),
file('Axioms/GRA001+0.ax',on_path_properties) ).
cnf(20,plain,
( ~ path(X0,X1,X2)
| ~ on_path(X3,X2)
| edge(X3) ),
inference(cnf,[status(esa)],[on_path_properties]) ).
cnf(l675,plain,
( ~ path(sK11,sK12,sK15)
| ~ on_path(sK14,sK15)
| edge(sK14) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l692,plain,
( ~ path(sK11,sK12,sK15)
| ~ on_path(sK13,sK15)
| edge(sK13) ),
inference(instantiation,[status(thm)],[20]) ).
fof(path_properties,plain,
! [V1,V2,P] :
( path(V1,V2,P)
=> ( vertex(V1)
& vertex(V2)
& ? [E] :
( edge(E)
& V1 = tail_of(E)
& ( ( V2 = head_of(E)
& P = path_cons(E,empty) )
<~> ? [TP] :
( path(head_of(E),V2,TP)
& P = path_cons(E,TP) ) ) ) ) ),
file('Axioms/GRA001+0.ax',path_properties) ).
cnf(11,plain,
( ~ path(X0,X1,X2)
| vertex(X0) ),
inference(cnf,[status(esa)],[path_properties]) ).
cnf(l1,plain,
( ~ path(sK11,sK12,sK15)
| vertex(sK11) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(12,plain,
( ~ path(X0,X1,X2)
| vertex(X1) ),
inference(cnf,[status(esa)],[path_properties]) ).
cnf(l680,plain,
( ~ path(sK11,sK12,sK8(sK11,sK12,sK15))
| vertex(sK12) ),
inference(instantiation,[status(thm)],[12]) ).
fof(shortest_path_defn,plain,
! [V1,V2,SP] :
( shortest_path(V1,V2,SP)
<=> ( path(V1,V2,SP)
& V1 != V2
& ! [P] :
( path(V1,V2,P)
=> less_or_equal(length_of(SP),length_of(P)) ) ) ),
file('Axioms/GRA001+0.ax',shortest_path_defn) ).
cnf(38,plain,
( ~ shortest_path(X0,X1,X2)
| path(X0,X1,X2) ),
inference(cnf,[status(esa)],[shortest_path_defn]) ).
cnf(l697,plain,
( ~ shortest_path(sK11,sK12,sK15)
| path(sK11,sK12,sK15) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l695,plain,
( ~ shortest_path(sK11,sK12,sK15)
| path(sK11,sK12,sK15) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l674,plain,
( ~ shortest_path(sK11,sK12,sK15)
| path(sK11,sK12,sK15) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(41,plain,
( ~ path(X0,X1,X2)
| X0 = X1
| path(X0,X1,sK8(X0,X1,X2))
| shortest_path(X0,X1,X2) ),
inference(cnf,[status(esa)],[shortest_path_defn]) ).
cnf(l708,plain,
( ~ path(sK11,sK12,sK15)
| sK11 = sK12
| path(sK11,sK12,sK8(sK11,sK12,sK15))
| shortest_path(sK11,sK12,sK15) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l116,plain,
( ~ shortest_path(sK11,sK12,sK15)
| path(sK11,sK12,sK15) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(59,plain,
shortest_path(sK11,sK12,sK15),
inference(cnf,[status(esa)],[vertices_and_edges_negated]) ).
cnf(l122,plain,
shortest_path(sK11,sK12,sK15),
inference(instantiation,[status(thm)],[59]) ).
cnf(l693,plain,
shortest_path(sK11,sK12,sK15),
inference(instantiation,[status(thm)],[59]) ).
fof(precedes_properties,plain,
! [P,V1,V2] :
( path(V1,V2,P)
=> ! [E1,E2] :
( precedes(E1,E2,P)
=> ( on_path(E1,P)
& on_path(E2,P)
& ( sequential(E1,E2)
<~> ? [E3] :
( sequential(E1,E3)
& precedes(E3,E2,P) ) ) ) ) ),
file('Axioms/GRA001+0.ax',precedes_properties) ).
cnf(34,plain,
( ~ path(X0,X1,X2)
| ~ precedes(X3,X4,X2)
| on_path(X4,X2) ),
inference(cnf,[status(esa)],[precedes_properties]) ).
cnf(l1018,plain,
( ~ path(sK11,sK12,sK15)
| ~ precedes(sK13,sK14,sK15)
| on_path(sK14,sK15) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l817,plain,
( ~ shortest_path(sK11,sK12,sK15)
| path(sK11,sK12,sK15) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(60,plain,
precedes(sK13,sK14,sK15),
inference(cnf,[status(esa)],[vertices_and_edges_negated]) ).
cnf(l1019,plain,
precedes(sK13,sK14,sK15),
inference(instantiation,[status(thm)],[60]) ).
cnf(l755,plain,
( ~ shortest_path(sK11,sK12,sK15)
| path(sK11,sK12,sK15) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l795,plain,
shortest_path(sK11,sK12,sK15),
inference(instantiation,[status(thm)],[59]) ).
cnf(l1021,plain,
( ~ shortest_path(sK11,sK12,sK15)
| path(sK11,sK12,sK15) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l792,plain,
shortest_path(sK11,sK12,sK15),
inference(instantiation,[status(thm)],[59]) ).
cnf(l741,plain,
shortest_path(sK11,sK12,sK15),
inference(instantiation,[status(thm)],[59]) ).
cnf(l1196,plain,
shortest_path(sK11,sK12,sK15),
inference(instantiation,[status(thm)],[59]) ).
cnf(33,plain,
( ~ path(X0,X1,X2)
| ~ precedes(X3,X4,X2)
| on_path(X3,X2) ),
inference(cnf,[status(esa)],[precedes_properties]) ).
cnf(l911,plain,
( ~ path(sK11,sK12,sK15)
| ~ precedes(sK13,sK14,sK15)
| on_path(sK13,sK15) ),
inference(instantiation,[status(thm)],[33]) ).
cnf(l1203,plain,
( ~ path(sK11,sK12,sK15)
| vertex(sK12) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l1084,plain,
precedes(sK13,sK14,sK15),
inference(instantiation,[status(thm)],[60]) ).
cnf(l913,plain,
( ~ shortest_path(sK11,sK12,sK15)
| path(sK11,sK12,sK15) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l915,plain,
shortest_path(sK11,sK12,sK15),
inference(instantiation,[status(thm)],[59]) ).
cnf(39,plain,
( X0 != X1
| ~ shortest_path(X0,X1,X2) ),
inference(cnf,[status(esa)],[shortest_path_defn]) ).
cnf(l728,plain,
( sK11 != sK12
| ~ shortest_path(sK11,sK12,sK15) ),
inference(instantiation,[status(thm)],[39]) ).
cnf(l922,plain,
shortest_path(sK11,sK12,sK15),
inference(instantiation,[status(thm)],[59]) ).
cnf(l1238,plain,
( sK11 != sK11
| ~ shortest_path(sK11,sK11,sK15) ),
inference(instantiation,[status(thm)],[39]) ).
fof(shortest_path_properties,plain,
! [V1,V2,E1,E2,P] :
( ( shortest_path(V1,V2,P)
& precedes(E1,E2,P) )
=> ( ~ ? [E3] :
( tail_of(E3) = tail_of(E1)
& head_of(E3) = head_of(E2) )
& ~ precedes(E2,E1,P) ) ),
file('Axioms/GRA001+0.ax',shortest_path_properties) ).
cnf(43,plain,
( tail_of(X0) != tail_of(X1)
| head_of(X0) != head_of(X2)
| ~ shortest_path(X3,X4,X5)
| ~ precedes(X1,X2,X5) ),
inference(cnf,[status(esa)],[shortest_path_properties]) ).
cnf(l805,plain,
( tail_of(sK13) != tail_of(sK14)
| head_of(sK13) != head_of(sK14)
| ~ shortest_path(sK11,sK12,sK15)
| ~ precedes(sK14,sK14,sK15) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(l1469,plain,
shortest_path(sK11,sK12,sK15),
inference(instantiation,[status(thm)],[59]) ).
cnf(l921,plain,
shortest_path(sK11,sK12,sK15),
inference(instantiation,[status(thm)],[59]) ).
cnf(l959,plain,
precedes(sK13,sK14,sK15),
inference(instantiation,[status(thm)],[60]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l675,l692,l1,l680,l697,l695,l674,l708,l116,l122,l693,l1018,l817,l1019,l755,l795,l1021,l792,l741,l1196,l911,l1203,l1084,l913,l915,l728,l922,l1238,l805,l1469,l921,l959]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GRA003+1 : TPTP v9.0.0. Bugfixed v3.2.0.
% 0.11/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n025.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 % WCLimit : 300
% 0.12/0.33 % DateTime : Sun Jul 20 13:07:34 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.34 % launching worker at depth: 4
% 0.12/0.34 % launching worker at depth: 7
% 0.12/0.34 % launching worker at depth: 1
% 0.12/0.34 % launching worker at depth: 2
% 0.12/0.34 % launching worker at depth: 5
% 0.12/0.34 % launching worker at depth: 3
% 0.12/0.34 % launching worker at depth: 6
% 0.12/0.34 % launching worker at depth: 8
% 0.12/0.34 % launching worker at depth: 9
% 0.12/0.35 % launching worker at depth: 10
% 0.19/0.48 % launching worker at depth: 11
% 13.34/2.08 % SZS status Theorem for theBenchmark
% 13.34/2.08 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------