%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRA002+4 : 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 : n014.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 0.17s 0.50s
% Output : CNFRefutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 6
% Syntax : Number of formulae : 28 ( 14 unt; 0 def)
% Number of atoms : 51 ( 13 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 37 ( 14 ~; 7 |; 6 &)
% ( 1 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 2 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 8 con; 0-2 aty)
% Number of variables : 41 ( 9 sgn 21 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
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(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(triangles_and_sequential_pairs,axiom,
( complete
=> ! [P,V1,V2] :
( shortest_path(V1,V2,P)
=> number_of_in(sequential_pairs,P) = number_of_in(triangles,P) ) ),
file('theBenchmark.p',triangles_and_sequential_pairs) ).
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]) ).
cnf(c_25,plain,
( number_of_in(triangles,C) = number_of_in(sequential_pairs,C)
| ~ shortest_path(A,B,C)
| ~ complete ),
inference(clausify,[status(thm)],[triangles_and_sequential_pairs]) ).
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(sK2),n1),number_of_in(triangles,graph))
& shortest_path(sK0,sK1,sK2)
& complete ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(P,sK2),skolemize(V1,sK0),skolemize(V2,sK1)],[nnf_19]) ).
cnf(c_26,negated_conjecture,
shortest_path(sK0,sK1,sK2),
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(sK0,sK1,sK2),
inference(resolve,[status(thm)],[c_33,c_26]) ).
cnf(c_47,negated_conjecture,
( number_of_in(triangles,sK2) = number_of_in(sequential_pairs,sK2)
| ~ complete ),
inference(resolve,[status(thm)],[c_25,c_26]) ).
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]) ).
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(sK2),n1),number_of_in(triangles,graph)),
inference(split_conjunct,[status(thm)],[sk_maximal_path_length_neg]) ).
cnf(c_128,negated_conjecture,
number_of_in(triangles,sK2) = number_of_in(sequential_pairs,sK2),
inference(resolve,[status(thm)],[c_96,c_47]) ).
cnf(c_152,plain,
length_of(sK2) = number_of_in(edges,sK2),
inference(resolve,[status(thm)],[c_89,c_34]) ).
cnf(c_156,negated_conjecture,
~ less_or_equal(minus(number_of_in(edges,sK2),n1),number_of_in(triangles,graph)),
inference(paramod,[status(thm)],[c_152,c_97]) ).
cnf(c_161,negated_conjecture,
minus(length_of(sK2),n1) = number_of_in(sequential_pairs,sK2),
inference(resolve,[status(thm)],[c_90,c_34]) ).
cnf(c_158,negated_conjecture,
minus(number_of_in(edges,sK2),n1) = number_of_in(sequential_pairs,sK2),
inference(paramod,[status(thm)],[c_152,c_161]) ).
cnf(c_159,negated_conjecture,
~ less_or_equal(number_of_in(sequential_pairs,sK2),number_of_in(triangles,graph)),
inference(paramod,[status(thm)],[c_158,c_156]) ).
cnf(c_162,plain,
less_or_equal(number_of_in(sequential_pairs,sK2),number_of_in(triangles,graph)),
inference(paramod,[status(thm)],[c_128,c_95]) ).
cnf(c_160,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_159,c_162]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRA002+4 : TPTP v9.3.1. Bugfixed v3.2.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n014.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Fri Sep 25 13:47:17 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.45 % Process 363746 was started by sandbox on n014,
% 0.17/0.45 % Fri Sep 25 13:47:17 2026
% 0.17/0.45 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.17/0.46
% 0.17/0.46 % From the command line: assign(max_seconds, 300).
% 0.17/0.50
% 0.17/0.50 % SZS status Theorem for theBenchmark
% 0.17/0.50
% 0.17/0.50 % Proof 1 at 0.02 (+ 0.01) seconds.
% 0.17/0.50 % Length of proof is 23.
% 0.17/0.50 % Level of proof is 6.
% 0.17/0.50 % Maximum clause weight is 12.000.
% 0.17/0.50 % Given clauses 72.
% 0.17/0.50
% 0.17/0.50 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------