%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL674+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n001.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 : Fri Sep 25 02:02:36 PM UTC 2026
% Result : Theorem 5.12s 1.10s
% Output : Proof 5.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 3
% Syntax : Number of formulae : 42 ( 8 unt; 0 def)
% Number of atoms : 589 ( 0 equ)
% Maximal formula atoms : 121 ( 14 avg)
% Number of connectives : 943 ( 396 ~; 317 |; 229 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 28 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 15 ( 14 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 1 con; 0-1 aty)
% Number of variables : 100 ( 0 sgn 76 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y,Z] :
( ( r1(Y,Z)
& r1(X,Y) )
=> r1(X,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',transitivity) ).
fof(f1_nnf,plain,
! [X,Y,Z] :
( r1(X,Z)
| ~ r1(Y,Z)
| ~ r1(X,Y) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Y,Z] :
( r1(X,Z)
| ~ r1(Y,Z)
| ~ r1(X,Y) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( r1(X0,X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
fof(f0,axiom,
! [X] : r1(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity) ).
fof(f0_nnf,plain,
! [X] : r1(X,X),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X] : r1(X,X),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
r1(X0,X0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
fof(f2,conjecture,
~ ? [X] :
~ ( ~ ( p100(X)
& ~ p101(X)
& ! [Y] :
( ( ( ~ p101(Y)
| p100(Y) )
& ( ~ p102(Y)
| p101(Y) )
& ( ~ p103(Y)
| p102(Y) )
& ( ~ p104(Y)
| p103(Y) )
& ( ~ p105(Y)
| p104(Y) )
& ( ~ p106(Y)
| p105(Y) )
& ( ~ p100(Y)
| ( ( ~ p1(Y)
| ! [X] :
( ~ p100(X)
| p1(X)
| ~ r1(Y,X) ) )
& ( p1(Y)
| ! [X] :
( ~ p100(X)
| ~ p1(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p101(Y)
| ( ( ~ p2(Y)
| ! [X] :
( ~ p101(X)
| p2(X)
| ~ r1(Y,X) ) )
& ( p2(Y)
| ! [X] :
( ~ p101(X)
| ~ p2(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p102(Y)
| ( ( ~ p3(Y)
| ! [X] :
( ~ p102(X)
| p3(X)
| ~ r1(Y,X) ) )
& ( p3(Y)
| ! [X] :
( ~ p102(X)
| ~ p3(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p103(Y)
| ( ( ~ p4(Y)
| ! [X] :
( ~ p103(X)
| p4(X)
| ~ r1(Y,X) ) )
& ( p4(Y)
| ! [X] :
( ~ p103(X)
| ~ p4(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p104(Y)
| ( ( ~ p5(Y)
| ! [X] :
( ~ p104(X)
| p5(X)
| ~ r1(Y,X) ) )
& ( p5(Y)
| ! [X] :
( ~ p104(X)
| ~ p5(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p105(Y)
| ( ( ~ p6(Y)
| ! [X] :
( ~ p105(X)
| p6(X)
| ~ r1(Y,X) ) )
& ( p6(Y)
| ! [X] :
( ~ p105(X)
| ~ p6(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ ( p100(Y)
& ~ p101(Y) )
| ( ~ ! [X] :
( ~ ( p101(X)
& ~ p102(X)
& p2(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p101(X)
& ~ p102(X)
& ~ p2(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p101(Y)
& ~ p102(Y) )
| ( ~ ! [X] :
( ~ ( p102(X)
& ~ p103(X)
& p3(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p102(X)
& ~ p103(X)
& ~ p3(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p102(Y)
& ~ p103(Y) )
| ( ~ ! [X] :
( ~ ( p103(X)
& ~ p104(X)
& p4(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p103(X)
& ~ p104(X)
& ~ p4(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p103(Y)
& ~ p104(Y) )
| ( ~ ! [X] :
( ~ ( p104(X)
& ~ p105(X)
& p5(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p104(X)
& ~ p105(X)
& ~ p5(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p104(Y)
& ~ p105(Y) )
| ( ~ ! [X] :
( ~ ( p105(X)
& ~ p106(X)
& p6(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p105(X)
& ~ p106(X)
& ~ p6(X) )
| ~ r1(Y,X) ) ) ) )
| ~ r1(X,Y) ) )
| ~ ! [Y] :
( p3(Y)
| ~ r1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',main) ).
fof(f2_neg,negated_conjecture,
~ ~ ? [X] :
~ ( ~ ( p100(X)
& ~ p101(X)
& ! [Y] :
( ( ( ~ p101(Y)
| p100(Y) )
& ( ~ p102(Y)
| p101(Y) )
& ( ~ p103(Y)
| p102(Y) )
& ( ~ p104(Y)
| p103(Y) )
& ( ~ p105(Y)
| p104(Y) )
& ( ~ p106(Y)
| p105(Y) )
& ( ~ p100(Y)
| ( ( ~ p1(Y)
| ! [X] :
( ~ p100(X)
| p1(X)
| ~ r1(Y,X) ) )
& ( p1(Y)
| ! [X] :
( ~ p100(X)
| ~ p1(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p101(Y)
| ( ( ~ p2(Y)
| ! [X] :
( ~ p101(X)
| p2(X)
| ~ r1(Y,X) ) )
& ( p2(Y)
| ! [X] :
( ~ p101(X)
| ~ p2(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p102(Y)
| ( ( ~ p3(Y)
| ! [X] :
( ~ p102(X)
| p3(X)
| ~ r1(Y,X) ) )
& ( p3(Y)
| ! [X] :
( ~ p102(X)
| ~ p3(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p103(Y)
| ( ( ~ p4(Y)
| ! [X] :
( ~ p103(X)
| p4(X)
| ~ r1(Y,X) ) )
& ( p4(Y)
| ! [X] :
( ~ p103(X)
| ~ p4(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p104(Y)
| ( ( ~ p5(Y)
| ! [X] :
( ~ p104(X)
| p5(X)
| ~ r1(Y,X) ) )
& ( p5(Y)
| ! [X] :
( ~ p104(X)
| ~ p5(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p105(Y)
| ( ( ~ p6(Y)
| ! [X] :
( ~ p105(X)
| p6(X)
| ~ r1(Y,X) ) )
& ( p6(Y)
| ! [X] :
( ~ p105(X)
| ~ p6(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ ( p100(Y)
& ~ p101(Y) )
| ( ~ ! [X] :
( ~ ( p101(X)
& ~ p102(X)
& p2(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p101(X)
& ~ p102(X)
& ~ p2(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p101(Y)
& ~ p102(Y) )
| ( ~ ! [X] :
( ~ ( p102(X)
& ~ p103(X)
& p3(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p102(X)
& ~ p103(X)
& ~ p3(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p102(Y)
& ~ p103(Y) )
| ( ~ ! [X] :
( ~ ( p103(X)
& ~ p104(X)
& p4(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p103(X)
& ~ p104(X)
& ~ p4(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p103(Y)
& ~ p104(Y) )
| ( ~ ! [X] :
( ~ ( p104(X)
& ~ p105(X)
& p5(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p104(X)
& ~ p105(X)
& ~ p5(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p104(Y)
& ~ p105(Y) )
| ( ~ ! [X] :
( ~ ( p105(X)
& ~ p106(X)
& p6(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p105(X)
& ~ p106(X)
& ~ p6(X) )
| ~ r1(Y,X) ) ) ) )
| ~ r1(X,Y) ) )
| ~ ! [Y] :
( p3(Y)
| ~ r1(X,Y) ) ),
inference(negated_conjecture,[status(cth)],[f2]) ).
fof(f2_nnf,plain,
? [X] :
( p100(X)
& ~ p101(X)
& ! [Y] :
( ( ( ~ p101(Y)
| p100(Y) )
& ( ~ p102(Y)
| p101(Y) )
& ( ~ p103(Y)
| p102(Y) )
& ( ~ p104(Y)
| p103(Y) )
& ( ~ p105(Y)
| p104(Y) )
& ( ~ p106(Y)
| p105(Y) )
& ( ~ p100(Y)
| ( ( ~ p1(Y)
| ! [X] :
( ~ p100(X)
| p1(X)
| ~ r1(Y,X) ) )
& ( p1(Y)
| ! [X] :
( ~ p100(X)
| ~ p1(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p101(Y)
| ( ( ~ p2(Y)
| ! [X] :
( ~ p101(X)
| p2(X)
| ~ r1(Y,X) ) )
& ( p2(Y)
| ! [X] :
( ~ p101(X)
| ~ p2(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p102(Y)
| ( ( ~ p3(Y)
| ! [X] :
( ~ p102(X)
| p3(X)
| ~ r1(Y,X) ) )
& ( p3(Y)
| ! [X] :
( ~ p102(X)
| ~ p3(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p103(Y)
| ( ( ~ p4(Y)
| ! [X] :
( ~ p103(X)
| p4(X)
| ~ r1(Y,X) ) )
& ( p4(Y)
| ! [X] :
( ~ p103(X)
| ~ p4(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p104(Y)
| ( ( ~ p5(Y)
| ! [X] :
( ~ p104(X)
| p5(X)
| ~ r1(Y,X) ) )
& ( p5(Y)
| ! [X] :
( ~ p104(X)
| ~ p5(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p105(Y)
| ( ( ~ p6(Y)
| ! [X] :
( ~ p105(X)
| p6(X)
| ~ r1(Y,X) ) )
& ( p6(Y)
| ! [X] :
( ~ p105(X)
| ~ p6(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p100(Y)
| p101(Y)
| ( ? [X] :
( p101(X)
& ~ p102(X)
& p2(X)
& r1(Y,X) )
& ? [X] :
( p101(X)
& ~ p102(X)
& ~ p2(X)
& r1(Y,X) ) ) )
& ( ~ p101(Y)
| p102(Y)
| ( ? [X] :
( p102(X)
& ~ p103(X)
& p3(X)
& r1(Y,X) )
& ? [X] :
( p102(X)
& ~ p103(X)
& ~ p3(X)
& r1(Y,X) ) ) )
& ( ~ p102(Y)
| p103(Y)
| ( ? [X] :
( p103(X)
& ~ p104(X)
& p4(X)
& r1(Y,X) )
& ? [X] :
( p103(X)
& ~ p104(X)
& ~ p4(X)
& r1(Y,X) ) ) )
& ( ~ p103(Y)
| p104(Y)
| ( ? [X] :
( p104(X)
& ~ p105(X)
& p5(X)
& r1(Y,X) )
& ? [X] :
( p104(X)
& ~ p105(X)
& ~ p5(X)
& r1(Y,X) ) ) )
& ( ~ p104(Y)
| p105(Y)
| ( ? [X] :
( p105(X)
& ~ p106(X)
& p6(X)
& r1(Y,X) )
& ? [X] :
( p105(X)
& ~ p106(X)
& ~ p6(X)
& r1(Y,X) ) ) ) )
| ~ r1(X,Y) )
& ! [Y] :
( p3(Y)
| ~ r1(X,Y) ) ),
inference(nnf_transformation,[status(thm)],[f2_neg]) ).
fof(f2_sk,plain,
! [Y,X] :
( p100(sk0)
& ~ p101(sk0)
& ( ( ( ~ p101(Y)
| p100(Y) )
& ( ~ p102(Y)
| p101(Y) )
& ( ~ p103(Y)
| p102(Y) )
& ( ~ p104(Y)
| p103(Y) )
& ( ~ p105(Y)
| p104(Y) )
& ( ~ p106(Y)
| p105(Y) )
& ( ~ p100(Y)
| ( ( ~ p1(Y)
| ~ p100(X)
| p1(X)
| ~ r1(Y,X) )
& ( p1(Y)
| ~ p100(X)
| ~ p1(X)
| ~ r1(Y,X) ) ) )
& ( ~ p101(Y)
| ( ( ~ p2(Y)
| ~ p101(X)
| p2(X)
| ~ r1(Y,X) )
& ( p2(Y)
| ~ p101(X)
| ~ p2(X)
| ~ r1(Y,X) ) ) )
& ( ~ p102(Y)
| ( ( ~ p3(Y)
| ~ p102(X)
| p3(X)
| ~ r1(Y,X) )
& ( p3(Y)
| ~ p102(X)
| ~ p3(X)
| ~ r1(Y,X) ) ) )
& ( ~ p103(Y)
| ( ( ~ p4(Y)
| ~ p103(X)
| p4(X)
| ~ r1(Y,X) )
& ( p4(Y)
| ~ p103(X)
| ~ p4(X)
| ~ r1(Y,X) ) ) )
& ( ~ p104(Y)
| ( ( ~ p5(Y)
| ~ p104(X)
| p5(X)
| ~ r1(Y,X) )
& ( p5(Y)
| ~ p104(X)
| ~ p5(X)
| ~ r1(Y,X) ) ) )
& ( ~ p105(Y)
| ( ( ~ p6(Y)
| ~ p105(X)
| p6(X)
| ~ r1(Y,X) )
& ( p6(Y)
| ~ p105(X)
| ~ p6(X)
| ~ r1(Y,X) ) ) )
& ( ~ p100(Y)
| p101(Y)
| ( p101(sk10(Y))
& ~ p102(sk10(Y))
& p2(sk10(Y))
& r1(Y,sk10(Y))
& p101(sk9(Y))
& ~ p102(sk9(Y))
& ~ p2(sk9(Y))
& r1(Y,sk9(Y)) ) )
& ( ~ p101(Y)
| p102(Y)
| ( p102(sk8(Y))
& ~ p103(sk8(Y))
& p3(sk8(Y))
& r1(Y,sk8(Y))
& p102(sk7(Y))
& ~ p103(sk7(Y))
& ~ p3(sk7(Y))
& r1(Y,sk7(Y)) ) )
& ( ~ p102(Y)
| p103(Y)
| ( p103(sk6(Y))
& ~ p104(sk6(Y))
& p4(sk6(Y))
& r1(Y,sk6(Y))
& p103(sk5(Y))
& ~ p104(sk5(Y))
& ~ p4(sk5(Y))
& r1(Y,sk5(Y)) ) )
& ( ~ p103(Y)
| p104(Y)
| ( p104(sk4(Y))
& ~ p105(sk4(Y))
& p5(sk4(Y))
& r1(Y,sk4(Y))
& p104(sk3(Y))
& ~ p105(sk3(Y))
& ~ p5(sk3(Y))
& r1(Y,sk3(Y)) ) )
& ( ~ p104(Y)
| p105(Y)
| ( p105(sk2(Y))
& ~ p106(sk2(Y))
& p6(sk2(Y))
& r1(Y,sk2(Y))
& p105(sk1(Y))
& ~ p106(sk1(Y))
& ~ p6(sk1(Y))
& r1(Y,sk1(Y)) ) ) )
| ~ r1(sk0,Y) )
& ( p3(Y)
| ~ r1(sk0,Y) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2,sk3,sk4,sk5,sk6,sk7,sk8,sk9,sk10])],[f2_nnf]) ).
cnf(c35,plain,
( ~ p100(X1)
| p101(X1)
| r1(X1,sk9(X1))
| ~ r1(sk0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p99,plain,
( ~ p100(sk0)
| p101(sk0)
| r1(sk0,sk9(sk0)) ),
inference(resolution,[status(thm)],[c0,c35]) ).
cnf(c62,plain,
p100(sk0),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p112,plain,
( p101(sk0)
| r1(sk0,sk9(sk0)) ),
inference(resolution,[status(thm)],[p99,c62]) ).
cnf(p315,plain,
( p101(sk0)
| r1(sk0,X0)
| ~ r1(sk9(sk0),X0) ),
inference(resolution,[status(thm)],[c1,p112]) ).
cnf(c27,plain,
( ~ p101(X1)
| p102(X1)
| r1(X1,sk7(X1))
| ~ r1(sk0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p149,plain,
( ~ p101(sk9(sk0))
| p102(sk9(sk0))
| r1(sk9(sk0),sk7(sk9(sk0)))
| p101(sk0) ),
inference(resolution,[status(thm)],[p112,c27]) ).
cnf(c38,plain,
( ~ p100(X1)
| p101(X1)
| p101(sk9(X1))
| ~ r1(sk0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p89,plain,
( ~ p100(sk0)
| p101(sk0)
| p101(sk9(sk0)) ),
inference(resolution,[status(thm)],[c0,c38]) ).
cnf(p109,plain,
( p101(sk0)
| p101(sk9(sk0)) ),
inference(resolution,[status(thm)],[p89,c62]) ).
cnf(p247,plain,
( p101(sk0)
| p102(sk9(sk0))
| r1(sk9(sk0),sk7(sk9(sk0)))
| p101(sk0) ),
inference(resolution,[status(thm)],[p149,p109]) ).
cnf(p248,plain,
( p102(sk9(sk0))
| r1(sk9(sk0),sk7(sk9(sk0)))
| p101(sk0) ),
inference(factoring,[status(thm)],[p247]) ).
cnf(p321,plain,
( p102(sk9(sk0))
| p101(sk0)
| p101(sk0)
| r1(sk0,sk7(sk9(sk0))) ),
inference(resolution,[status(thm)],[p315,p248]) ).
cnf(p325,plain,
( p102(sk9(sk0))
| p101(sk0)
| r1(sk0,sk7(sk9(sk0))) ),
inference(factoring,[status(thm)],[p321]) ).
cnf(c2,plain,
( p3(X1)
| ~ r1(sk0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p326,plain,
( p3(sk7(sk9(sk0)))
| p102(sk9(sk0))
| p101(sk0) ),
inference(resolution,[status(thm)],[p325,c2]) ).
cnf(c28,plain,
( ~ p101(X1)
| p102(X1)
| ~ p3(sk7(X1))
| ~ r1(sk0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p137,plain,
( ~ p101(sk9(sk0))
| p102(sk9(sk0))
| ~ p3(sk7(sk9(sk0)))
| p101(sk0) ),
inference(resolution,[status(thm)],[p112,c28]) ).
cnf(p384,plain,
( ~ p101(sk9(sk0))
| p102(sk9(sk0))
| p101(sk0)
| p102(sk9(sk0))
| p101(sk0) ),
inference(resolution,[status(thm)],[p326,p137]) ).
cnf(p566,plain,
( ~ p101(sk9(sk0))
| p101(sk0)
| p102(sk9(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p384]) ).
cnf(p567,plain,
( ~ p101(sk9(sk0))
| p102(sk9(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p566]) ).
cnf(p568,plain,
( p101(sk0)
| p102(sk9(sk0))
| p101(sk0) ),
inference(resolution,[status(thm)],[p567,p109]) ).
cnf(p569,plain,
( p102(sk9(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p568]) ).
cnf(c37,plain,
( ~ p100(X1)
| p101(X1)
| ~ p102(sk9(X1))
| ~ r1(sk0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p88,plain,
( ~ p100(sk0)
| p101(sk0)
| ~ p102(sk9(sk0)) ),
inference(resolution,[status(thm)],[c0,c37]) ).
cnf(p570,plain,
( ~ p100(sk0)
| p101(sk0)
| p101(sk0) ),
inference(resolution,[status(thm)],[p569,p88]) ).
cnf(p576,plain,
( ~ p100(sk0)
| p101(sk0) ),
inference(factoring,[status(thm)],[p570]) ).
cnf(p577,plain,
p101(sk0),
inference(resolution,[status(thm)],[p576,c62]) ).
cnf(c61,plain,
~ p101(sk0),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p578,plain,
$false,
inference(resolution,[status(thm)],[p577,c61]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL674+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n001.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 00:18:05 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 5.12/1.10 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.12/1.10 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------