%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRA002+3 : TPTP v9.3.1. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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 : Sun Sep 27 07:19:21 AM UTC 2026
% Result : Theorem 31.65s 5.16s
% Output : CNFRefutation 31.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 8
% Syntax : Number of formulae : 58 ( 19 unt; 0 def)
% Number of atoms : 159 ( 25 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 159 ( 58 ~; 64 |; 23 &)
% ( 1 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 2 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-5 aty)
% Number of variables : 122 ( 11 sgn 69 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
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('theBenchmark.p',precedes_defn) ).
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('theBenchmark.p',shortest_path_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,axiom,
( 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(maximal_path_length,conjecture,
( complete
=> ! [P,V1,V2] :
( shortest_path(V1,V2,P)
=> less_or_equal(minus(length_of(P),n1),number_of_in(triangles,graph)) ) ),
file('theBenchmark.p',maximal_path_length) ).
fof(maximal_path_length_neg,negated_conjecture,
~ ( complete
=> ! [P,V1,V2] :
( shortest_path(V1,V2,P)
=> less_or_equal(minus(length_of(P),n1),number_of_in(triangles,graph)) ) ),
inference(assume_negation,[status(cth)],[maximal_path_length]) ).
fof(nnf_18,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(sk_sequential_is_triangle_sk,plain,
( ! [V1,V2,E1,E2,P] :
( triangle(E1,E2,sK0(V1,V2,E1,E2,P))
| ~ sequential(E1,E2)
| ~ precedes(E1,E2,P)
| ~ shortest_path(V1,V2,P) )
| ~ complete ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(E3,sK0(V1,V2,E1,E2,P))],[nnf_18]) ).
fof(sk_sequential_is_triangle,plain,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( triangle(VAR_3,VAR_4,sK0(VAR_0,VAR_1,VAR_3,VAR_4,VAR_2))
| ~ sequential(VAR_3,VAR_4)
| ~ precedes(VAR_3,VAR_4,VAR_2)
| ~ shortest_path(VAR_0,VAR_1,VAR_2)
| ~ complete ),
inference(cnf_transformation,[status(thm)],[sk_sequential_is_triangle_sk]) ).
cnf(c_25,plain,
( triangle(D,E,sK0(A,B,D,E,C))
| ~ sequential(D,E)
| ~ precedes(D,E,C)
| ~ shortest_path(A,B,C)
| ~ complete ),
inference(split_conjunct,[status(thm)],[sk_sequential_is_triangle]) ).
fof(nnf_19,plain,
( ? [P,V1,V2] :
( ~ less_or_equal(minus(length_of(P),n1),number_of_in(triangles,graph))
& shortest_path(V1,V2,P) )
& complete ),
inference(fof_nnf,[status(thm)],[maximal_path_length_neg]) ).
fof(sk_maximal_path_length_neg,plain,
( ~ less_or_equal(minus(length_of(sK3),n1),number_of_in(triangles,graph))
& shortest_path(sK1,sK2,sK3)
& complete ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3]),skolemize(P,sK3),skolemize(V1,sK1),skolemize(V2,sK2)],[nnf_19]) ).
cnf(c_26,negated_conjecture,
shortest_path(sK1,sK2,sK3),
inference(split_conjunct,[status(thm)],[sk_maximal_path_length_neg]) ).
cnf(c_33,plain,
( path(A,B,C)
| ~ shortest_path(A,B,C) ),
inference(clausify,[status(thm)],[shortest_path_defn]) ).
cnf(c_34,negated_conjecture,
path(sK1,sK2,sK3),
inference(resolve,[status(thm)],[c_33,c_26]) ).
cnf(c_47,negated_conjecture,
( triangle(A,B,sK0(sK1,sK2,A,B,sK3))
| ~ sequential(A,B)
| ~ precedes(A,B,sK3)
| ~ complete ),
inference(resolve,[status(thm)],[c_25,c_26]) ).
cnf(c_74,plain,
( ~ sequential(D,E)
| ~ on_path(E,C)
| ~ on_path(D,C)
| precedes(D,E,C)
| ~ path(A,B,C) ),
inference(clausify,[status(thm)],[precedes_defn]) ).
cnf(c_88,plain,
( number_of_in(edges,C) = length_of(C)
| ~ path(A,B,C) ),
inference(clausify,[status(thm)],[length_defn]) ).
cnf(c_89,plain,
( length_of(C) = number_of_in(edges,C)
| ~ path(A,B,C) ),
inference(copy,[status(thm)],[c_88]) ).
cnf(c_90,plain,
( minus(length_of(C),n1) = number_of_in(sequential_pairs,C)
| ~ path(A,B,C) ),
inference(clausify,[status(thm)],[path_length_sequential_pairs]) ).
fof(nnf_16,plain,
! [P,V1,V2] :
( number_of_in(triangles,P) = number_of_in(sequential_pairs,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(sk_sequential_pairs_and_triangles_sk,plain,
! [P,V1,V2] :
( number_of_in(triangles,P) = number_of_in(sequential_pairs,P)
| ( ! [E3] : ~ triangle(sK4(P,V1,V2),sK5(P,V1,V2),E3)
& sequential(sK4(P,V1,V2),sK5(P,V1,V2))
& on_path(sK5(P,V1,V2),P)
& on_path(sK4(P,V1,V2),P) )
| ~ path(V1,V2,P) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5]),skolemize(E1,sK4(P,V1,V2)),skolemize(E2,sK5(P,V1,V2))],[nnf_16]) ).
fof(sk_sequential_pairs_and_triangles,plain,
( ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( number_of_in(triangles,VAR_2) = number_of_in(sequential_pairs,VAR_2)
| ~ triangle(sK4(VAR_2,VAR_0,VAR_1),sK5(VAR_2,VAR_0,VAR_1),VAR_3)
| ~ path(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( number_of_in(triangles,VAR_2) = number_of_in(sequential_pairs,VAR_2)
| sequential(sK4(VAR_2,VAR_0,VAR_1),sK5(VAR_2,VAR_0,VAR_1))
| ~ path(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( number_of_in(triangles,VAR_2) = number_of_in(sequential_pairs,VAR_2)
| on_path(sK5(VAR_2,VAR_0,VAR_1),VAR_2)
| ~ path(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2] :
( number_of_in(triangles,VAR_2) = number_of_in(sequential_pairs,VAR_2)
| on_path(sK4(VAR_2,VAR_0,VAR_1),VAR_2)
| ~ path(VAR_0,VAR_1,VAR_2) ) ),
inference(cnf_transformation,[status(thm)],[sk_sequential_pairs_and_triangles_sk]) ).
cnf(c_91,plain,
( number_of_in(triangles,C) = number_of_in(sequential_pairs,C)
| on_path(sK4(C,A,B),C)
| ~ path(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sequential_pairs_and_triangles]) ).
cnf(c_92,plain,
( number_of_in(triangles,C) = number_of_in(sequential_pairs,C)
| on_path(sK5(C,A,B),C)
| ~ path(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sequential_pairs_and_triangles]) ).
cnf(c_93,plain,
( number_of_in(triangles,C) = number_of_in(sequential_pairs,C)
| sequential(sK4(C,A,B),sK5(C,A,B))
| ~ path(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sequential_pairs_and_triangles]) ).
cnf(c_94,plain,
( number_of_in(triangles,C) = number_of_in(sequential_pairs,C)
| ~ triangle(sK4(C,A,B),sK5(C,A,B),D)
| ~ path(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_sequential_pairs_and_triangles]) ).
cnf(c_95,plain,
less_or_equal(number_of_in(A,B),number_of_in(A,graph)),
inference(clausify,[status(thm)],[graph_has_them_all]) ).
cnf(c_96,negated_conjecture,
complete,
inference(split_conjunct,[status(thm)],[sk_maximal_path_length_neg]) ).
cnf(c_97,negated_conjecture,
~ less_or_equal(minus(length_of(sK3),n1),number_of_in(triangles,graph)),
inference(split_conjunct,[status(thm)],[sk_maximal_path_length_neg]) ).
cnf(c_126,negated_conjecture,
( triangle(A,B,sK0(sK1,sK2,A,B,sK3))
| ~ sequential(A,B)
| ~ precedes(A,B,sK3) ),
inference(resolve,[status(thm)],[c_96,c_47]) ).
cnf(c_163,plain,
( ~ sequential(A,B)
| ~ on_path(B,sK3)
| ~ on_path(A,sK3)
| precedes(A,B,sK3) ),
inference(resolve,[status(thm)],[c_74,c_34]) ).
cnf(c_171,plain,
length_of(sK3) = number_of_in(edges,sK3),
inference(resolve,[status(thm)],[c_89,c_34]) ).
cnf(c_175,negated_conjecture,
~ less_or_equal(minus(number_of_in(edges,sK3),n1),number_of_in(triangles,graph)),
inference(paramod,[status(thm)],[c_171,c_97]) ).
cnf(c_3067,negated_conjecture,
minus(length_of(sK3),n1) = number_of_in(sequential_pairs,sK3),
inference(resolve,[status(thm)],[c_90,c_34]) ).
cnf(c_177,negated_conjecture,
minus(number_of_in(edges,sK3),n1) = number_of_in(sequential_pairs,sK3),
inference(paramod,[status(thm)],[c_171,c_3067]) ).
cnf(c_178,negated_conjecture,
~ less_or_equal(number_of_in(sequential_pairs,sK3),number_of_in(triangles,graph)),
inference(paramod,[status(thm)],[c_177,c_175]) ).
cnf(c_179,plain,
( number_of_in(triangles,sK3) = number_of_in(sequential_pairs,sK3)
| on_path(sK4(sK3,sK1,sK2),sK3) ),
inference(resolve,[status(thm)],[c_91,c_34]) ).
cnf(c_180,plain,
( number_of_in(triangles,sK3) = number_of_in(sequential_pairs,sK3)
| on_path(sK5(sK3,sK1,sK2),sK3) ),
inference(resolve,[status(thm)],[c_92,c_34]) ).
cnf(c_181,plain,
( number_of_in(triangles,sK3) = number_of_in(sequential_pairs,sK3)
| sequential(sK4(sK3,sK1,sK2),sK5(sK3,sK1,sK2)) ),
inference(resolve,[status(thm)],[c_93,c_34]) ).
cnf(c_182,plain,
( number_of_in(triangles,sK3) = number_of_in(sequential_pairs,sK3)
| ~ triangle(sK4(sK3,sK1,sK2),sK5(sK3,sK1,sK2),A) ),
inference(resolve,[status(thm)],[c_94,c_34]) ).
cnf(c_3068,plain,
( less_or_equal(number_of_in(sequential_pairs,sK3),number_of_in(triangles,graph))
| on_path(sK4(sK3,sK1,sK2),sK3) ),
inference(paramod,[status(thm)],[c_179,c_95]) ).
cnf(c_356,negated_conjecture,
on_path(sK4(sK3,sK1,sK2),sK3),
inference(resolve,[status(thm)],[c_178,c_3068]) ).
cnf(c_3069,plain,
( less_or_equal(number_of_in(sequential_pairs,sK3),number_of_in(triangles,graph))
| on_path(sK5(sK3,sK1,sK2),sK3) ),
inference(paramod,[status(thm)],[c_180,c_95]) ).
cnf(c_422,negated_conjecture,
on_path(sK5(sK3,sK1,sK2),sK3),
inference(resolve,[status(thm)],[c_178,c_3069]) ).
cnf(c_3070,plain,
( less_or_equal(number_of_in(sequential_pairs,sK3),number_of_in(triangles,graph))
| sequential(sK4(sK3,sK1,sK2),sK5(sK3,sK1,sK2)) ),
inference(paramod,[status(thm)],[c_181,c_95]) ).
cnf(c_503,negated_conjecture,
sequential(sK4(sK3,sK1,sK2),sK5(sK3,sK1,sK2)),
inference(resolve,[status(thm)],[c_178,c_3070]) ).
cnf(c_3071,plain,
( ~ on_path(sK5(sK3,sK1,sK2),sK3)
| ~ on_path(sK4(sK3,sK1,sK2),sK3)
| precedes(sK4(sK3,sK1,sK2),sK5(sK3,sK1,sK2),sK3) ),
inference(resolve,[status(thm)],[c_503,c_163]) ).
cnf(c_3072,plain,
( ~ on_path(sK5(sK3,sK1,sK2),sK3)
| precedes(sK4(sK3,sK1,sK2),sK5(sK3,sK1,sK2),sK3) ),
inference(resolve,[status(thm)],[c_356,c_3071]) ).
cnf(c_508,plain,
precedes(sK4(sK3,sK1,sK2),sK5(sK3,sK1,sK2),sK3),
inference(resolve,[status(thm)],[c_422,c_3072]) ).
cnf(c_3073,negated_conjecture,
( triangle(sK4(sK3,sK1,sK2),sK5(sK3,sK1,sK2),sK0(sK1,sK2,sK4(sK3,sK1,sK2),sK5(sK3,sK1,sK2),sK3))
| ~ precedes(sK4(sK3,sK1,sK2),sK5(sK3,sK1,sK2),sK3) ),
inference(resolve,[status(thm)],[c_503,c_126]) ).
cnf(c_509,negated_conjecture,
triangle(sK4(sK3,sK1,sK2),sK5(sK3,sK1,sK2),sK0(sK1,sK2,sK4(sK3,sK1,sK2),sK5(sK3,sK1,sK2),sK3)),
inference(resolve,[status(thm)],[c_508,c_3073]) ).
cnf(c_3062,plain,
number_of_in(triangles,sK3) = number_of_in(sequential_pairs,sK3),
inference(resolve,[status(thm)],[c_509,c_182]) ).
cnf(c_3074,plain,
less_or_equal(number_of_in(sequential_pairs,sK3),number_of_in(triangles,graph)),
inference(paramod,[status(thm)],[c_3062,c_95]) ).
cnf(c_3066,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_178,c_3074]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRA002+3 : TPTP v9.3.1. Bugfixed v3.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.51 % Computer : n020.cluster.edu
% 0.09/0.51 % Model : x86_64 x86_64
% 0.09/0.51 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.51 % Memory : 8046.5625MB
% 0.09/0.51 % OS : Linux 6.8.0-71-generic
% 0.09/0.51 % CPULimit : 300
% 0.09/0.51 % WCLimit : 300
% 0.09/0.51 % DateTime : Fri Sep 25 13:48:19 UTC 2026
% 0.09/0.52 % CPUTime :
% 0.09/0.52 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.52 % Process 3066173 was started by sandbox on n020,
% 0.09/0.52 % Fri Sep 25 13:48:19 2026
% 0.09/0.52 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.53
% 0.09/0.53 % From the command line: assign(max_seconds, 300).
% 31.65/5.16
% 31.65/5.16 % given #500 (A,wt=23): 303 -vertex(A) | tail_of(f1(c2,c3)) = A | edge(f1(A,tail_of(f1(c2,c3)))). [resolve(295,a,125,b)].
% 31.65/5.16
% 31.65/5.16 % SZS status Theorem for theBenchmark
% 31.65/5.16
% 31.65/5.16 % Proof 1 at 3.55 (+ 0.94) seconds.
% 31.65/5.16 % Length of proof is 41.
% 31.65/5.16 % Level of proof is 10.
% 31.65/5.16 % Maximum clause weight is 27.000.
% 31.65/5.16 % Given clauses 840.
% 31.65/5.16
% 31.65/5.16 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------