%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ALG014+1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n005.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 12:51:11 PM UTC 2026
% Result : Theorem 35.12s 4.84s
% Output : Proof 35.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 5
% Syntax : Number of formulae : 53 ( 17 unt; 0 def)
% Number of atoms : 423 ( 422 equ)
% Maximal formula atoms : 48 ( 7 avg)
% Number of connectives : 592 ( 222 ~; 110 |; 260 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 7 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 5 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
unit = e0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
fof(f4_nnf,plain,
unit = e0,
inference(nnf_transformation,[status(thm)],[f4]) ).
cnf(c101,plain,
unit = e0,
inference(cnf_transformation,[status(esa)],[f4_nnf]) ).
fof(f2,axiom,
( ( unit = e3
| unit = e2
| unit = e1
| unit = e0 )
& op(e3,unit) = e3
& op(unit,e3) = e3
& op(e2,unit) = e2
& op(unit,e2) = e2
& op(e1,unit) = e1
& op(unit,e1) = e1
& op(e0,unit) = e0
& op(unit,e0) = e0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3) ).
fof(f2_nnf,plain,
( ( unit = e3
| unit = e2
| unit = e1
| unit = e0 )
& op(e3,unit) = e3
& op(unit,e3) = e3
& op(e2,unit) = e2
& op(unit,e2) = e2
& op(e1,unit) = e1
& op(unit,e1) = e1
& op(e0,unit) = e0
& op(unit,e0) = e0 ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
( ( unit = e3
| unit = e2
| unit = e1
| unit = e0 )
& op(e3,unit) = e3
& op(unit,e3) = e3
& op(e2,unit) = e2
& op(unit,e2) = e2
& op(e1,unit) = e1
& op(unit,e1) = e1
& op(e0,unit) = e0
& op(unit,e0) = e0 ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c80,plain,
op(unit,e0) = e0,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p469,plain,
op(e0,e0) = e0,
inference(superposition,[status(thm)],[c101,c80]) ).
fof(f11,conjecture,
( ~ ( ( op(e3,e3) = e3
& op(e2,e2) = e3
& op(e1,e1) = e3
& op(e0,e0) = e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e2
& op(e1,e1) = e2
& op(e0,e0) = e2 )
| ( op(e3,e3) = e1
& op(e2,e2) = e1
& op(e1,e1) = e1
& op(e0,e0) = e1 )
| ( op(e3,e3) = e0
& op(e2,e2) = e0
& op(e1,e1) = e0
& op(e0,e0) = e0 ) )
| ( op(e3,e3) = e3
& op(e2,e2) = e3
& op(e1,e1) = e3
& op(e0,e0) = e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e2
& op(e1,e1) = e2
& op(e0,e0) = e2 )
| ( op(e3,e3) = e1
& op(e2,e2) = e1
& op(e1,e1) = e1
& op(e0,e0) = e1 )
| ( op(e3,e3) = e0
& op(e2,e2) = e0
& op(e1,e1) = e0
& op(e0,e0) = e0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(f11_neg,negated_conjecture,
~ ( ~ ( ( op(e3,e3) = e3
& op(e2,e2) = e3
& op(e1,e1) = e3
& op(e0,e0) = e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e2
& op(e1,e1) = e2
& op(e0,e0) = e2 )
| ( op(e3,e3) = e1
& op(e2,e2) = e1
& op(e1,e1) = e1
& op(e0,e0) = e1 )
| ( op(e3,e3) = e0
& op(e2,e2) = e0
& op(e1,e1) = e0
& op(e0,e0) = e0 ) )
| ( op(e3,e3) = e3
& op(e2,e2) = e3
& op(e1,e1) = e3
& op(e0,e0) = e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e2
& op(e1,e1) = e2
& op(e0,e0) = e2 )
| ( op(e3,e3) = e1
& op(e2,e2) = e1
& op(e1,e1) = e1
& op(e0,e0) = e1 )
| ( op(e3,e3) = e0
& op(e2,e2) = e0
& op(e1,e1) = e0
& op(e0,e0) = e0 ) ),
inference(negated_conjecture,[status(cth)],[f11]) ).
fof(f11_nnf,plain,
( ( ( op(e3,e3) = e3
& op(e2,e2) = e3
& op(e1,e1) = e3
& op(e0,e0) = e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e2
& op(e1,e1) = e2
& op(e0,e0) = e2 )
| ( op(e3,e3) = e1
& op(e2,e2) = e1
& op(e1,e1) = e1
& op(e0,e0) = e1 )
| ( op(e3,e3) = e0
& op(e2,e2) = e0
& op(e1,e1) = e0
& op(e0,e0) = e0 ) )
& ( op(e3,e3) != e3
| op(e2,e2) != e3
| op(e1,e1) != e3
| op(e0,e0) != e3 )
& ( op(e3,e3) != e2
| op(e2,e2) != e2
| op(e1,e1) != e2
| op(e0,e0) != e2 )
& ( op(e3,e3) != e1
| op(e2,e2) != e1
| op(e1,e1) != e1
| op(e0,e0) != e1 )
& ( op(e3,e3) != e0
| op(e2,e2) != e0
| op(e1,e1) != e0
| op(e0,e0) != e0 ) ),
inference(nnf_transformation,[status(thm)],[f11_neg]) ).
fof(f11_sk,plain,
( ( ( op(e3,e3) = e3
& op(e2,e2) = e3
& op(e1,e1) = e3
& op(e0,e0) = e3 )
| ( op(e3,e3) = e2
& op(e2,e2) = e2
& op(e1,e1) = e2
& op(e0,e0) = e2 )
| ( op(e3,e3) = e1
& op(e2,e2) = e1
& op(e1,e1) = e1
& op(e0,e0) = e1 )
| ( op(e3,e3) = e0
& op(e2,e2) = e0
& op(e1,e1) = e0
& op(e0,e0) = e0 ) )
& ( op(e3,e3) != e3
| op(e2,e2) != e3
| op(e1,e1) != e3
| op(e0,e0) != e3 )
& ( op(e3,e3) != e2
| op(e2,e2) != e2
| op(e1,e1) != e2
| op(e0,e0) != e2 )
& ( op(e3,e3) != e1
| op(e2,e2) != e1
| op(e1,e1) != e1
| op(e0,e0) != e1 )
& ( op(e3,e3) != e0
| op(e2,e2) != e0
| op(e1,e1) != e0
| op(e0,e0) != e0 ) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c262,plain,
( op(e3,e3) = e3
| op(e2,e2) = e2
| op(e0,e0) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p494,plain,
( op(e3,e3) = e3
| op(e2,e2) = e2
| e0 = e1
| op(e1,e1) = e0 ),
inference(demodulation,[status(thm)],[p469,c262]) ).
cnf(c86,plain,
op(unit,e3) = e3,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p651,plain,
op(e0,e3) = e3,
inference(superposition,[status(thm)],[c101,c86]) ).
fof(f9,axiom,
( op(e3,e2) != op(e3,e3)
& op(e3,e1) != op(e3,e3)
& op(e3,e1) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e1)
& op(e2,e2) != op(e2,e3)
& op(e2,e1) != op(e2,e3)
& op(e2,e1) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e1)
& op(e1,e2) != op(e1,e3)
& op(e1,e1) != op(e1,e3)
& op(e1,e1) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e1)
& op(e0,e2) != op(e0,e3)
& op(e0,e1) != op(e0,e3)
& op(e0,e1) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e1)
& op(e2,e3) != op(e3,e3)
& op(e1,e3) != op(e3,e3)
& op(e1,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e1,e3)
& op(e2,e2) != op(e3,e2)
& op(e1,e2) != op(e3,e2)
& op(e1,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e1,e2)
& op(e2,e1) != op(e3,e1)
& op(e1,e1) != op(e3,e1)
& op(e1,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e1,e1)
& op(e2,e0) != op(e3,e0)
& op(e1,e0) != op(e3,e0)
& op(e1,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e1,e0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax10) ).
fof(f9_nnf,plain,
( op(e3,e2) != op(e3,e3)
& op(e3,e1) != op(e3,e3)
& op(e3,e1) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e1)
& op(e2,e2) != op(e2,e3)
& op(e2,e1) != op(e2,e3)
& op(e2,e1) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e1)
& op(e1,e2) != op(e1,e3)
& op(e1,e1) != op(e1,e3)
& op(e1,e1) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e1)
& op(e0,e2) != op(e0,e3)
& op(e0,e1) != op(e0,e3)
& op(e0,e1) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e1)
& op(e2,e3) != op(e3,e3)
& op(e1,e3) != op(e3,e3)
& op(e1,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e1,e3)
& op(e2,e2) != op(e3,e2)
& op(e1,e2) != op(e3,e2)
& op(e1,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e1,e2)
& op(e2,e1) != op(e3,e1)
& op(e1,e1) != op(e3,e1)
& op(e1,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e1,e1)
& op(e2,e0) != op(e3,e0)
& op(e1,e0) != op(e3,e0)
& op(e1,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e1,e0) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
( op(e3,e2) != op(e3,e3)
& op(e3,e1) != op(e3,e3)
& op(e3,e1) != op(e3,e2)
& op(e3,e0) != op(e3,e3)
& op(e3,e0) != op(e3,e2)
& op(e3,e0) != op(e3,e1)
& op(e2,e2) != op(e2,e3)
& op(e2,e1) != op(e2,e3)
& op(e2,e1) != op(e2,e2)
& op(e2,e0) != op(e2,e3)
& op(e2,e0) != op(e2,e2)
& op(e2,e0) != op(e2,e1)
& op(e1,e2) != op(e1,e3)
& op(e1,e1) != op(e1,e3)
& op(e1,e1) != op(e1,e2)
& op(e1,e0) != op(e1,e3)
& op(e1,e0) != op(e1,e2)
& op(e1,e0) != op(e1,e1)
& op(e0,e2) != op(e0,e3)
& op(e0,e1) != op(e0,e3)
& op(e0,e1) != op(e0,e2)
& op(e0,e0) != op(e0,e3)
& op(e0,e0) != op(e0,e2)
& op(e0,e0) != op(e0,e1)
& op(e2,e3) != op(e3,e3)
& op(e1,e3) != op(e3,e3)
& op(e1,e3) != op(e2,e3)
& op(e0,e3) != op(e3,e3)
& op(e0,e3) != op(e2,e3)
& op(e0,e3) != op(e1,e3)
& op(e2,e2) != op(e3,e2)
& op(e1,e2) != op(e3,e2)
& op(e1,e2) != op(e2,e2)
& op(e0,e2) != op(e3,e2)
& op(e0,e2) != op(e2,e2)
& op(e0,e2) != op(e1,e2)
& op(e2,e1) != op(e3,e1)
& op(e1,e1) != op(e3,e1)
& op(e1,e1) != op(e2,e1)
& op(e0,e1) != op(e3,e1)
& op(e0,e1) != op(e2,e1)
& op(e0,e1) != op(e1,e1)
& op(e2,e0) != op(e3,e0)
& op(e1,e0) != op(e3,e0)
& op(e1,e0) != op(e2,e0)
& op(e0,e0) != op(e3,e0)
& op(e0,e0) != op(e2,e0)
& op(e0,e0) != op(e1,e0) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c149,plain,
op(e0,e3) != op(e3,e3),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p659,plain,
e3 != op(e3,e3),
inference(demodulation,[status(thm)],[p651,c149]) ).
cnf(p2501,plain,
( e3 != e3
| op(e2,e2) = e2
| e0 = e1
| op(e1,e1) = e0 ),
inference(superposition,[status(thm)],[p494,p659]) ).
cnf(p4632,plain,
( op(e2,e2) = e2
| e0 = e1
| op(e1,e1) = e0 ),
inference(equality_resolution,[status(thm)],[p2501]) ).
cnf(c84,plain,
op(unit,e2) = e2,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p630,plain,
op(e0,e2) = e2,
inference(superposition,[status(thm)],[c101,c84]) ).
cnf(c142,plain,
op(e0,e2) != op(e2,e2),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p638,plain,
e2 != op(e2,e2),
inference(demodulation,[status(thm)],[p630,c142]) ).
cnf(p4635,plain,
( e2 != e2
| e0 = e1
| op(e1,e1) = e0 ),
inference(superposition,[status(thm)],[p4632,p638]) ).
cnf(p4648,plain,
( e0 = e1
| op(e1,e1) = e0 ),
inference(equality_resolution,[status(thm)],[p4635]) ).
cnf(c183,plain,
( op(e3,e3) != e0
| op(e2,e2) != e0
| op(e1,e1) != e0
| op(e0,e0) != e0 ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p482,plain,
( op(e3,e3) != e0
| op(e2,e2) != e0
| op(e1,e1) != e0
| e0 != e0 ),
inference(demodulation,[status(thm)],[p469,c183]) ).
cnf(p2388,plain,
( op(e3,e3) != e0
| op(e2,e2) != e0
| op(e1,e1) != e0 ),
inference(equality_resolution,[status(thm)],[p482]) ).
cnf(p4662,plain,
( op(e3,e3) != e0
| op(e2,e2) != e0
| e0 = e1 ),
inference(resolution,[status(thm)],[p4648,p2388]) ).
cnf(c318,plain,
( op(e3,e3) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p523,plain,
( op(e3,e3) = e3
| e0 = e2
| e0 = e1
| op(e2,e2) = e0 ),
inference(demodulation,[status(thm)],[p469,c318]) ).
cnf(p2715,plain,
( e3 != e3
| e0 = e2
| e0 = e1
| op(e2,e2) = e0 ),
inference(superposition,[status(thm)],[p523,p659]) ).
cnf(p2728,plain,
( e0 = e2
| e0 = e1
| op(e2,e2) = e0 ),
inference(equality_resolution,[status(thm)],[p2715]) ).
cnf(p4689,plain,
( e0 = e2
| e0 = e1
| op(e3,e3) != e0
| e0 = e1 ),
inference(resolution,[status(thm)],[p4662,p2728]) ).
cnf(p4702,plain,
( e0 = e2
| op(e3,e3) != e0
| e0 = e1 ),
inference(factoring,[status(thm)],[p4689]) ).
cnf(c382,plain,
( op(e3,e3) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p560,plain,
( op(e3,e3) = e3
| e0 = e2
| e0 = e1
| op(e3,e3) = e0 ),
inference(demodulation,[status(thm)],[p469,c382]) ).
cnf(p3356,plain,
( e3 != e3
| e0 = e2
| e0 = e1
| op(e3,e3) = e0 ),
inference(superposition,[status(thm)],[p560,p659]) ).
cnf(p3370,plain,
( e0 = e2
| e0 = e1
| op(e3,e3) = e0 ),
inference(equality_resolution,[status(thm)],[p3356]) ).
cnf(p4714,plain,
( e0 = e2
| e0 = e1
| e0 = e2
| e0 = e1 ),
inference(resolution,[status(thm)],[p4702,p3370]) ).
cnf(p4756,plain,
( e0 = e2
| e0 = e2
| e0 = e1 ),
inference(factoring,[status(thm)],[p4714]) ).
cnf(p4758,plain,
( e0 = e2
| e0 = e1 ),
inference(factoring,[status(thm)],[p4756]) ).
fof(f10,axiom,
( e2 != e3
& e1 != e3
& e1 != e2
& e0 != e3
& e0 != e2
& e0 != e1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax11) ).
fof(f10_nnf,plain,
( e2 != e3
& e1 != e3
& e1 != e2
& e0 != e3
& e0 != e2
& e0 != e1 ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
( e2 != e3
& e1 != e3
& e1 != e2
& e0 != e3
& e0 != e2
& e0 != e1 ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c178,plain,
e0 != e2,
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p4762,plain,
e0 = e1,
inference(resolution,[status(thm)],[p4758,c178]) ).
cnf(c177,plain,
e0 != e1,
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p4763,plain,
$false,
inference(resolution,[status(thm)],[p4762,c177]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG014+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.06/0.35 % Computer : n005.cluster.edu
% 0.06/0.35 % Model : x86_64 x86_64
% 0.06/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.35 % Memory : 8046.5625MB
% 0.06/0.35 % OS : Linux 6.8.0-71-generic
% 0.06/0.35 % CPULimit : 300
% 0.06/0.35 % WCLimit : 300
% 0.06/0.35 % DateTime : Fri Sep 25 04:31:34 UTC 2026
% 0.06/0.35 % CPUTime :
% 0.06/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 35.12/4.84 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 35.12/4.84 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------