%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : GRA002+4 : TPTP v9.3.1. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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:18:42 AM UTC 2026
% Result : Theorem 12.52s 2.05s
% Output : CNFRefutation 12.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GRA002+4 : TPTP v9.3.1. Bugfixed v3.2.0.
% 0.00/0.02 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Fri Sep 25 13:47:08 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.52/2.05 % SZS status Theorem for theBenchmark.p
% 12.52/2.05 % SZS output start CNFRefutation for theBenchmark.p
% 12.52/2.05 fof(path_length_sequential_pairs, axiom, ! [X0] : ! [X1] : ! [X2] : ((path(X0,X1,X2) => 'number$uof$uin'('sequential$upairs',X2) = minus('length$uof'(X2),n1)))).
% 12.52/2.05 fof(graph_has_them_all, axiom, ! [X0] : ! [X1] : 'less$uor$uequal'('number$uof$uin'(X0,X1),'number$uof$uin'(X0,graph))).
% 12.52/2.05 fof(triangles_and_sequential_pairs, lemma, (complete => ! [X0] : ! [X1] : ! [X2] : (('shortest$upath'(X1,X2,X0) => 'number$uof$uin'('sequential$upairs',X0) = 'number$uof$uin'(triangles,X0))))).
% 12.52/2.05 fof(shortest_path_defn, axiom, ! [X0] : ! [X1] : ! [X2] : (('shortest$upath'(X0,X1,X2) <=> (path(X0,X1,X2) & (X0 != X1 & ! [X3] : ((path(X0,X1,X3) => 'less$uor$uequal'('length$uof'(X2),'length$uof'(X3))))))))).
% 12.52/2.05 fof(maximal_path_length, conjecture, (complete => ! [X0] : ! [X1] : ! [X2] : (('shortest$upath'(X1,X2,X0) => 'less$uor$uequal'(minus('length$uof'(X0),n1),'number$uof$uin'(triangles,graph)))))).
% 12.52/2.05 fof(negated_conjecture, negated_conjecture, ~((complete => ! [X0] : ! [X1] : ! [X2] : (('shortest$upath'(X1,X2,X0) => 'less$uor$uequal'(minus('length$uof'(X0),n1),'number$uof$uin'(triangles,graph)))))), inference(negate_conjecture, [status(cth)], [maximal_path_length])).
% 12.52/2.05 cnf(c10, plain, ~path(X0,X1,X2) | 'number$uof$uin'('sequential$upairs',X2) = minus('length$uof'(X2),n1), inference(clausification, [status(esa)], [path_length_sequential_pairs])).
% 12.52/2.05 cnf(c15, plain, 'less$uor$uequal'('number$uof$uin'(X0,X1),'number$uof$uin'(X0,graph)), inference(clausification, [status(esa)], [graph_has_them_all])).
% 12.52/2.05 cnf(c16, plain, ~complete | ~'shortest$upath'(X0,X1,X2) | 'number$uof$uin'('sequential$upairs',X2) = 'number$uof$uin'(triangles,X2), inference(clausification, [status(esa)], [triangles_and_sequential_pairs])).
% 12.52/2.05 cnf(c70, plain, ~'shortest$upath'(X0,X1,X2) | X3(X2,X0,X1), inference(clausification, [status(esa)], [shortest_path_defn])).
% 12.52/2.05 cnf(c72, plain, ~X0(X1,X2,X3) | path(X2,X3,X1), inference(clausification, [status(esa)], [shortest_path_defn])).
% 12.52/2.05 cnf(c79, plain, complete, inference(clausification, [status(esa)], [negated_conjecture])).
% 12.52/2.05 cnf(c80, plain, 'shortest$upath'(sK79,sK80,sK78), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.52/2.05 cnf(c81, plain, ~'less$uor$uequal'(minus('length$uof'(sK78),n1),'number$uof$uin'(triangles,graph)), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.52/2.05 cnf(d0, plain, 'Ts66'(sK78,sK79,sK80), inference(resolution, [status(thm)], [c70,c80])).
% 12.52/2.05 cnf(d1, plain, path(sK79,sK80,sK78), inference(resolution, [status(thm)], [c72,d0])).
% 12.52/2.05 cnf(d2, plain, ~'less$uor$uequal'('number$uof$uin'('sequential$upairs',sK78),'number$uof$uin'(triangles,graph)) | ~path(X0,X1,sK78), inference(superposition, [status(thm)], [c10,c81])).
% 12.52/2.05 cnf(d3, plain, 'number$uof$uin'('sequential$upairs',X0) = 'number$uof$uin'(triangles,X0) | ~'shortest$upath'(X1,X2,X0), inference(resolution, [status(thm)], [c79,c16])).
% 12.52/2.05 cnf(d4, plain, 'less$uor$uequal'('number$uof$uin'('sequential$upairs',X0),'number$uof$uin'(triangles,graph)) | ~'shortest$upath'(X1,X2,X0), inference(superposition, [status(thm)], [d3,c15])).
% 12.52/2.05 cnf(d5, plain, ~'shortest$upath'(X0,X1,sK78) | ~path(X2,X3,sK78), inference(resolution, [status(thm)], [d4,d2])).
% 12.52/2.05 cnf(d6, plain, ~path(X0,X1,sK78), inference(resolution, [status(thm)], [d5,c80])).
% 12.52/2.05 cnf(d7, plain, $false, inference(resolution, [status(thm)], [d6,d1])).
% 12.52/2.05 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------