%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYN393+1.003 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n009.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 03:34:35 PM UTC 2026
% Result : Theorem 4.19s 1.07s
% Output : Proof 4.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 1
% Syntax : Number of formulae : 54 ( 5 unt; 0 def)
% Number of atoms : 272 ( 0 equ)
% Maximal formula atoms : 40 ( 5 avg)
% Number of connectives : 340 ( 122 ~; 168 |; 40 &)
% ( 10 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 0 ( 0 avg)
% Number of predicates : 4 ( 3 usr; 4 prp; 0-0 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f0,conjecture,
( ( ( p1
<=> p2 )
<=> p3 )
<=> ( p1
<=> ( p2
<=> p3 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',pel12) ).
fof(f0_neg,negated_conjecture,
~ ( ( ( p1
<=> p2 )
<=> p3 )
<=> ( p1
<=> ( p2
<=> p3 ) ) ),
inference(negated_conjecture,[status(cth)],[f0]) ).
fof(f0_nnf,plain,
( ( ( ( p3
& ~ p2 )
| ( ~ p3
& p2 )
| p1 )
& ( ( ( ~ p3
| p2 )
& ( p3
| ~ p2 ) )
| ~ p1 )
& ( ( p3
& ( ( p2
& ~ p1 )
| ( ~ p2
& p1 ) ) )
| ( ~ p3
& ( ~ p2
| p1 )
& ( p2
| ~ p1 ) ) ) )
| ( ( ( ( ~ p3
| p2 )
& ( p3
| ~ p2 )
& ~ p1 )
| ( ( ( p3
& ~ p2 )
| ( ~ p3
& p2 ) )
& p1 ) )
& ( ~ p3
| ( ( ~ p2
| p1 )
& ( p2
| ~ p1 ) ) )
& ( p3
| ( p2
& ~ p1 )
| ( ~ p2
& p1 ) ) ) ),
inference(nnf_transformation,[status(thm)],[f0_neg]) ).
fof(f0_sk,plain,
( ( ( ( p3
& ~ p2 )
| ( ~ p3
& p2 )
| p1 )
& ( ( ( ~ p3
| p2 )
& ( p3
| ~ p2 ) )
| ~ p1 )
& ( ( p3
& ( ( p2
& ~ p1 )
| ( ~ p2
& p1 ) ) )
| ( ~ p3
& ( ~ p2
| p1 )
& ( p2
| ~ p1 ) ) ) )
| ( ( ( ( ~ p3
| p2 )
& ( p3
| ~ p2 )
& ~ p1 )
| ( ( ( p3
& ~ p2 )
| ( ~ p3
& p2 ) )
& p1 ) )
& ( ~ p3
| ( ( ~ p2
| p1 )
& ( p2
| ~ p1 ) ) )
& ( p3
| ( p2
& ~ p1 )
| ( ~ p2
& p1 ) ) ) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c327,plain,
( ~ p1
| ~ p2
| ~ p3
| ~ p1
| ~ p2
| ~ p3 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p495,plain,
( ~ p1
| ~ p2
| ~ p1
| ~ p2
| ~ p3 ),
inference(factoring,[status(thm)],[c327]) ).
cnf(p502,plain,
( ~ p1
| ~ p1
| ~ p2
| ~ p3 ),
inference(factoring,[status(thm)],[p495]) ).
cnf(p504,plain,
( ~ p1
| ~ p2
| ~ p3 ),
inference(factoring,[status(thm)],[p502]) ).
cnf(c256,plain,
( p3
| p2
| ~ p1
| ~ p1
| p3
| p2 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p488,plain,
( p3
| ~ p1
| ~ p1
| p3
| p2 ),
inference(factoring,[status(thm)],[c256]) ).
cnf(p491,plain,
( ~ p1
| ~ p1
| p3
| p2 ),
inference(factoring,[status(thm)],[p488]) ).
cnf(p493,plain,
( ~ p1
| p3
| p2 ),
inference(factoring,[status(thm)],[p491]) ).
cnf(c179,plain,
( p2
| p1
| ~ p3
| ~ p3
| p2
| p1 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p471,plain,
( p2
| ~ p3
| ~ p3
| p2
| p1 ),
inference(factoring,[status(thm)],[c179]) ).
cnf(p474,plain,
( ~ p3
| ~ p3
| p2
| p1 ),
inference(factoring,[status(thm)],[p471]) ).
cnf(p476,plain,
( ~ p3
| p2
| p1 ),
inference(factoring,[status(thm)],[p474]) ).
cnf(c39,plain,
( p3
| p2
| p1
| p3
| p2
| p1 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p441,plain,
( p3
| p2
| p3
| p2
| p1 ),
inference(factoring,[status(thm)],[c39]) ).
cnf(p444,plain,
( p3
| p3
| p2
| p1 ),
inference(factoring,[status(thm)],[p441]) ).
cnf(p446,plain,
( p3
| p2
| p1 ),
inference(factoring,[status(thm)],[p444]) ).
cnf(p477,plain,
( p2
| p1
| p2
| p1 ),
inference(resolution,[status(thm)],[p476,p446]) ).
cnf(p478,plain,
( p2
| p2
| p1 ),
inference(factoring,[status(thm)],[p477]) ).
cnf(p480,plain,
( p2
| p1 ),
inference(factoring,[status(thm)],[p478]) ).
cnf(c156,plain,
( p3
| ~ p2
| p1
| p3
| ~ p2
| p1 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p465,plain,
( p3
| ~ p2
| p3
| ~ p2
| p1 ),
inference(factoring,[status(thm)],[c156]) ).
cnf(p468,plain,
( p3
| p3
| ~ p2
| p1 ),
inference(factoring,[status(thm)],[p465]) ).
cnf(p470,plain,
( p3
| ~ p2
| p1 ),
inference(factoring,[status(thm)],[p468]) ).
cnf(p482,plain,
( p3
| p1
| p1 ),
inference(resolution,[status(thm)],[p480,p470]) ).
cnf(p484,plain,
( p3
| p1 ),
inference(factoring,[status(thm)],[p482]) ).
cnf(c124,plain,
( ~ p2
| ~ p3
| p1
| ~ p3
| ~ p2
| p1 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p459,plain,
( ~ p2
| ~ p3
| ~ p3
| ~ p2
| p1 ),
inference(factoring,[status(thm)],[c124]) ).
cnf(p462,plain,
( ~ p3
| ~ p3
| ~ p2
| p1 ),
inference(factoring,[status(thm)],[p459]) ).
cnf(p464,plain,
( ~ p3
| ~ p2
| p1 ),
inference(factoring,[status(thm)],[p462]) ).
cnf(p481,plain,
( ~ p3
| p1
| p1 ),
inference(resolution,[status(thm)],[p480,p464]) ).
cnf(p483,plain,
( ~ p3
| p1 ),
inference(factoring,[status(thm)],[p481]) ).
cnf(p485,plain,
( p1
| p1 ),
inference(resolution,[status(thm)],[p484,p483]) ).
cnf(p486,plain,
p1,
inference(factoring,[status(thm)],[p485]) ).
cnf(p494,plain,
( p3
| p2 ),
inference(resolution,[status(thm)],[p493,p486]) ).
cnf(c100,plain,
( ~ p3
| p2
| ~ p1
| ~ p3
| p2
| ~ p1 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p453,plain,
( ~ p3
| p2
| ~ p3
| p2
| ~ p1 ),
inference(factoring,[status(thm)],[c100]) ).
cnf(p456,plain,
( ~ p3
| ~ p3
| p2
| ~ p1 ),
inference(factoring,[status(thm)],[p453]) ).
cnf(p458,plain,
( ~ p3
| p2
| ~ p1 ),
inference(factoring,[status(thm)],[p456]) ).
cnf(p487,plain,
( ~ p3
| p2 ),
inference(resolution,[status(thm)],[p486,p458]) ).
cnf(p498,plain,
( p2
| p2 ),
inference(resolution,[status(thm)],[p494,p487]) ).
cnf(p499,plain,
p2,
inference(factoring,[status(thm)],[p498]) ).
cnf(c57,plain,
( p3
| ~ p2
| ~ p1
| p3
| ~ p1
| ~ p2 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p447,plain,
( p3
| ~ p1
| p3
| ~ p1
| ~ p2 ),
inference(factoring,[status(thm)],[c57]) ).
cnf(p450,plain,
( p3
| p3
| ~ p1
| ~ p2 ),
inference(factoring,[status(thm)],[p447]) ).
cnf(p452,plain,
( p3
| ~ p1
| ~ p2 ),
inference(factoring,[status(thm)],[p450]) ).
cnf(p500,plain,
( p3
| ~ p1 ),
inference(resolution,[status(thm)],[p499,p452]) ).
cnf(p501,plain,
p3,
inference(resolution,[status(thm)],[p500,p486]) ).
cnf(p505,plain,
( ~ p1
| ~ p2 ),
inference(resolution,[status(thm)],[p504,p501]) ).
cnf(p506,plain,
~ p1,
inference(resolution,[status(thm)],[p505,p499]) ).
cnf(p507,plain,
$false,
inference(resolution,[status(thm)],[p506,p486]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN393+1.003 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n009.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 01:04:29 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 4.19/1.07 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.19/1.07 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------