%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ALG036+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 : 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 : Fri Sep 25 12:51:16 PM UTC 2026
% Result : Theorem 3.94s 0.95s
% Output : Proof 3.94s
% 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(f3,axiom,
unit = e0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax4) ).
fof(f3_nnf,plain,
unit = e0,
inference(nnf_transformation,[status(thm)],[f3]) ).
cnf(c57,plain,
unit = e0,
inference(cnf_transformation,[status(esa)],[f3_nnf]) ).
fof(f1,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',ax2) ).
fof(f1_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)],[f1]) ).
fof(f1_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)],[f1_nnf]) ).
cnf(c16,plain,
op(unit,e0) = e0,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p378,plain,
op(e0,e0) = e0,
inference(superposition,[status(thm)],[c57,c16]) ).
fof(f6,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(f6_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)],[f6]) ).
fof(f6_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)],[f6_neg]) ).
fof(f6_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)],[f6_nnf]) ).
cnf(c191,plain,
( op(e3,e3) = e3
| op(e2,e2) = e2
| op(e0,e0) = e1
| op(e1,e1) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p403,plain,
( op(e3,e3) = e3
| op(e2,e2) = e2
| e0 = e1
| op(e1,e1) = e0 ),
inference(demodulation,[status(thm)],[p378,c191]) ).
cnf(c22,plain,
op(unit,e3) = e3,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p558,plain,
op(e0,e3) = e3,
inference(superposition,[status(thm)],[c57,c22]) ).
fof(f4,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',ax5) ).
fof(f4_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)],[f4]) ).
fof(f4_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)],[f4_nnf]) ).
cnf(c78,plain,
op(e0,e3) != op(e3,e3),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p564,plain,
e3 != op(e3,e3),
inference(demodulation,[status(thm)],[p558,c78]) ).
cnf(p1534,plain,
( e3 != e3
| op(e2,e2) = e2
| e0 = e1
| op(e1,e1) = e0 ),
inference(superposition,[status(thm)],[p403,p564]) ).
cnf(p1551,plain,
( op(e2,e2) = e2
| e0 = e1
| op(e1,e1) = e0 ),
inference(equality_resolution,[status(thm)],[p1534]) ).
cnf(c20,plain,
op(unit,e2) = e2,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p535,plain,
op(e0,e2) = e2,
inference(superposition,[status(thm)],[c57,c20]) ).
cnf(c71,plain,
op(e0,e2) != op(e2,e2),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p540,plain,
e2 != op(e2,e2),
inference(demodulation,[status(thm)],[p535,c71]) ).
cnf(p1552,plain,
( e2 != e2
| e0 = e1
| op(e1,e1) = e0 ),
inference(superposition,[status(thm)],[p1551,p540]) ).
cnf(p1555,plain,
( e0 = e1
| op(e1,e1) = e0 ),
inference(equality_resolution,[status(thm)],[p1552]) ).
cnf(c112,plain,
( op(e3,e3) != e0
| op(e2,e2) != e0
| op(e1,e1) != e0
| op(e0,e0) != e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p391,plain,
( op(e3,e3) != e0
| op(e2,e2) != e0
| op(e1,e1) != e0
| e0 != e0 ),
inference(demodulation,[status(thm)],[p378,c112]) ).
cnf(p1473,plain,
( op(e3,e3) != e0
| op(e2,e2) != e0
| op(e1,e1) != e0 ),
inference(equality_resolution,[status(thm)],[p391]) ).
cnf(p1567,plain,
( op(e3,e3) != e0
| op(e2,e2) != e0
| e0 = e1 ),
inference(resolution,[status(thm)],[p1555,p1473]) ).
cnf(c247,plain,
( op(e3,e3) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e2,e2) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p432,plain,
( op(e3,e3) = e3
| e0 = e2
| e0 = e1
| op(e2,e2) = e0 ),
inference(demodulation,[status(thm)],[p378,c247]) ).
cnf(p1083,plain,
( e3 != e3
| e0 = e2
| e0 = e1
| op(e2,e2) = e0 ),
inference(superposition,[status(thm)],[p432,p564]) ).
cnf(p1095,plain,
( e0 = e2
| e0 = e1
| op(e2,e2) = e0 ),
inference(equality_resolution,[status(thm)],[p1083]) ).
cnf(p1578,plain,
( e0 = e2
| e0 = e1
| op(e3,e3) != e0
| e0 = e1 ),
inference(resolution,[status(thm)],[p1567,p1095]) ).
cnf(p1581,plain,
( e0 = e2
| op(e3,e3) != e0
| e0 = e1 ),
inference(factoring,[status(thm)],[p1578]) ).
cnf(c311,plain,
( op(e3,e3) = e3
| op(e0,e0) = e2
| op(e0,e0) = e1
| op(e3,e3) = e0 ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p469,plain,
( op(e3,e3) = e3
| e0 = e2
| e0 = e1
| op(e3,e3) = e0 ),
inference(demodulation,[status(thm)],[p378,c311]) ).
cnf(p1221,plain,
( e3 != e3
| e0 = e2
| e0 = e1
| op(e3,e3) = e0 ),
inference(superposition,[status(thm)],[p469,p564]) ).
cnf(p1227,plain,
( e0 = e2
| e0 = e1
| op(e3,e3) = e0 ),
inference(equality_resolution,[status(thm)],[p1221]) ).
cnf(p1589,plain,
( e0 = e2
| e0 = e1
| e0 = e2
| e0 = e1 ),
inference(resolution,[status(thm)],[p1581,p1227]) ).
cnf(p1615,plain,
( e0 = e2
| e0 = e2
| e0 = e1 ),
inference(factoring,[status(thm)],[p1589]) ).
cnf(p1617,plain,
( e0 = e2
| e0 = e1 ),
inference(factoring,[status(thm)],[p1615]) ).
fof(f5,axiom,
( e2 != e3
& e1 != e3
& e1 != e2
& e0 != e3
& e0 != e2
& e0 != e1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
fof(f5_nnf,plain,
( e2 != e3
& e1 != e3
& e1 != e2
& e0 != e3
& e0 != e2
& e0 != e1 ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
( e2 != e3
& e1 != e3
& e1 != e2
& e0 != e3
& e0 != e2
& e0 != e1 ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c107,plain,
e0 != e2,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1625,plain,
e0 = e1,
inference(resolution,[status(thm)],[p1617,c107]) ).
cnf(c106,plain,
e0 != e1,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p1626,plain,
$false,
inference(resolution,[status(thm)],[p1625,c106]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : ALG036+1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.02 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 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 04:35:20 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 3.94/0.95 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.94/0.95 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------