%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : ALG017+1 : TPTP v9.0.0. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Jul 24 09:45:43 AM UTC 2025
% Result : Theorem 4.57s 0.90s
% Output : CNFRefutation 4.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 2
% Syntax : Number of formulae : 186 ( 1 unt; 0 def)
% Number of atoms : 599 ( 421 equ)
% Maximal formula atoms : 64 ( 3 avg)
% Number of connectives : 687 ( 274 ~; 348 |; 65 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 4 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(co1,plain,
~ ( ( ( op(e0,e0) = e0
& op(e1,e1) = e0
& op(e2,e2) = e0
& op(e3,e3) = e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e1
& op(e2,e2) = e1
& op(e3,e3) = e1 )
| ( op(e0,e0) = e2
& op(e1,e1) = e2
& op(e2,e2) = e2
& op(e3,e3) = e2 )
| ( op(e0,e0) = e3
& op(e1,e1) = e3
& op(e2,e2) = e3
& op(e3,e3) = e3 ) )
& ~ ( ( op(e0,e0) = e0
& op(e1,e1) = e0
& op(e2,e2) = e0
& op(e3,e3) = e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e1
& op(e2,e2) = e1
& op(e3,e3) = e1 )
| ( op(e0,e0) = e2
& op(e1,e1) = e2
& op(e2,e2) = e2
& op(e3,e3) = e2 )
| ( op(e0,e0) = e3
& op(e1,e1) = e3
& op(e2,e2) = e3
& op(e3,e3) = e3 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',co1) ).
fof(co1_negated,plain,
~ ~ ( ( ( op(e0,e0) = e0
& op(e1,e1) = e0
& op(e2,e2) = e0
& op(e3,e3) = e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e1
& op(e2,e2) = e1
& op(e3,e3) = e1 )
| ( op(e0,e0) = e2
& op(e1,e1) = e2
& op(e2,e2) = e2
& op(e3,e3) = e2 )
| ( op(e0,e0) = e3
& op(e1,e1) = e3
& op(e2,e2) = e3
& op(e3,e3) = e3 ) )
& ~ ( ( op(e0,e0) = e0
& op(e1,e1) = e0
& op(e2,e2) = e0
& op(e3,e3) = e0 )
| ( op(e0,e0) = e1
& op(e1,e1) = e1
& op(e2,e2) = e1
& op(e3,e3) = e1 )
| ( op(e0,e0) = e2
& op(e1,e1) = e2
& op(e2,e2) = e2
& op(e3,e3) = e2 )
| ( op(e0,e0) = e3
& op(e1,e1) = e3
& op(e2,e2) = e3
& op(e3,e3) = e3 ) ) ),
inference(negate_conjecture,[status(cth)],[co1]) ).
cnf(180,plain,
( op(e0,e0) = e0
| sP0
| sP1
| sP2 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l0,plain,
( op(e0,e0) = e0
| sP0
| sP1
| sP2 ),
inference(instantiation,[status(thm)],[180]) ).
cnf(184,plain,
( op(e2,e2) != e0
| op(e3,e3) != e0
| op(e0,e0) != e0
| op(e1,e1) != e0 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l2,plain,
( op(e2,e2) != e0
| op(e3,e3) != e0
| op(e0,e0) != e0
| op(e1,e1) != e0 ),
inference(instantiation,[status(thm)],[184]) ).
cnf(191,plain,
( op(e0,e0) = e3
| ~ sP2 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l5,plain,
( op(e0,e0) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[191]) ).
cnf(182,plain,
( op(e2,e2) = e0
| sP0
| sP1
| sP2 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l11,plain,
( op(e2,e2) = e0
| sP0
| sP1
| sP2 ),
inference(instantiation,[status(thm)],[182]) ).
cnf(183,plain,
( op(e3,e3) = e0
| sP0
| sP1
| sP2 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l7,plain,
( op(e3,e3) = e0
| sP0
| sP1
| sP2 ),
inference(instantiation,[status(thm)],[183]) ).
cnf(199,plain,
( op(e0,e0) = e1
| ~ sP0 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l1,plain,
( op(e0,e0) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[199]) ).
cnf(197,plain,
( op(e2,e2) = e1
| ~ sP0 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l14,plain,
( op(e2,e2) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[197]) ).
cnf(194,plain,
( op(e1,e1) = e2
| ~ sP1 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l9,plain,
( op(e1,e1) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[194]) ).
cnf(195,plain,
( op(e0,e0) = e2
| ~ sP1 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l16,plain,
( op(e0,e0) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[195]) ).
cnf(185,plain,
( op(e2,e2) != e1
| op(e3,e3) != e1
| op(e0,e0) != e1
| op(e1,e1) != e1 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l24,plain,
( op(e2,e2) != e1
| op(e3,e3) != e1
| op(e0,e0) != e1
| op(e1,e1) != e1 ),
inference(instantiation,[status(thm)],[185]) ).
cnf(189,plain,
( op(e2,e2) = e3
| ~ sP2 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l10,plain,
( op(e2,e2) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[189]) ).
cnf(187,plain,
( op(e2,e2) != e3
| op(e3,e3) != e3
| op(e0,e0) != e3
| op(e1,e1) != e3 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l21,plain,
( op(e2,e2) != e3
| op(e3,e3) != e3
| op(e0,e0) != e3
| op(e1,e1) != e3 ),
inference(instantiation,[status(thm)],[187]) ).
cnf(l19,plain,
( op(e0,e0) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[191]) ).
cnf(l3,plain,
( op(e2,e2) != e1
| op(e3,e3) != e1
| op(e0,e0) != e1
| op(e1,e1) != e1 ),
inference(instantiation,[status(thm)],[185]) ).
cnf(186,plain,
( op(e2,e2) != e2
| op(e3,e3) != e2
| op(e0,e0) != e2
| op(e1,e1) != e2 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l20,plain,
( op(e2,e2) != e2
| op(e3,e3) != e2
| op(e0,e0) != e2
| op(e1,e1) != e2 ),
inference(instantiation,[status(thm)],[186]) ).
cnf(l693,plain,
( op(e2,e2) != e3
| op(e3,e3) != e3
| op(e0,e0) != e3
| op(e1,e1) != e3 ),
inference(instantiation,[status(thm)],[187]) ).
cnf(193,plain,
( op(e2,e2) = e2
| ~ sP1 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l680,plain,
( op(e2,e2) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[193]) ).
cnf(190,plain,
( op(e1,e1) = e3
| ~ sP2 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l701,plain,
( op(e1,e1) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[190]) ).
cnf(196,plain,
( op(e3,e3) = e1
| ~ sP0 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l57,plain,
( op(e3,e3) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[196]) ).
cnf(l6,plain,
( op(e2,e2) != e3
| op(e3,e3) != e3
| op(e0,e0) != e3
| op(e1,e1) != e3 ),
inference(instantiation,[status(thm)],[187]) ).
cnf(l694,plain,
( op(e2,e2) != e2
| op(e3,e3) != e2
| op(e0,e0) != e2
| op(e1,e1) != e2 ),
inference(instantiation,[status(thm)],[186]) ).
cnf(198,plain,
( op(e1,e1) = e1
| ~ sP0 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l28,plain,
( op(e1,e1) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[198]) ).
fof(ax1,plain,
( ( op(e0,e0) = e0
| op(e0,e0) = e1
| op(e0,e0) = e2
| op(e0,e0) = e3 )
& ( op(e0,e1) = e0
| op(e0,e1) = e1
| op(e0,e1) = e2
| op(e0,e1) = e3 )
& ( op(e0,e2) = e0
| op(e0,e2) = e1
| op(e0,e2) = e2
| op(e0,e2) = e3 )
& ( op(e0,e3) = e0
| op(e0,e3) = e1
| op(e0,e3) = e2
| op(e0,e3) = e3 )
& ( op(e1,e0) = e0
| op(e1,e0) = e1
| op(e1,e0) = e2
| op(e1,e0) = e3 )
& ( op(e1,e1) = e0
| op(e1,e1) = e1
| op(e1,e1) = e2
| op(e1,e1) = e3 )
& ( op(e1,e2) = e0
| op(e1,e2) = e1
| op(e1,e2) = e2
| op(e1,e2) = e3 )
& ( op(e1,e3) = e0
| op(e1,e3) = e1
| op(e1,e3) = e2
| op(e1,e3) = e3 )
& ( op(e2,e0) = e0
| op(e2,e0) = e1
| op(e2,e0) = e2
| op(e2,e0) = e3 )
& ( op(e2,e1) = e0
| op(e2,e1) = e1
| op(e2,e1) = e2
| op(e2,e1) = e3 )
& ( op(e2,e2) = e0
| op(e2,e2) = e1
| op(e2,e2) = e2
| op(e2,e2) = e3 )
& ( op(e2,e3) = e0
| op(e2,e3) = e1
| op(e2,e3) = e2
| op(e2,e3) = e3 )
& ( op(e3,e0) = e0
| op(e3,e0) = e1
| op(e3,e0) = e2
| op(e3,e0) = e3 )
& ( op(e3,e1) = e0
| op(e3,e1) = e1
| op(e3,e1) = e2
| op(e3,e1) = e3 )
& ( op(e3,e2) = e0
| op(e3,e2) = e1
| op(e3,e2) = e2
| op(e3,e2) = e3 )
& ( op(e3,e3) = e0
| op(e3,e3) = e1
| op(e3,e3) = e2
| op(e3,e3) = e3 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
cnf(5,plain,
( op(e1,e1) = e2
| op(e1,e1) = e3
| op(e1,e1) = e0
| op(e1,e1) = e1 ),
inference(cnf,[status(esa)],[ax1]) ).
cnf(l4,plain,
( op(e1,e1) = e2
| op(e1,e1) = e3
| op(e1,e1) = e0
| op(e1,e1) = e1 ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l31,plain,
( op(e2,e2) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[193]) ).
cnf(l62,plain,
( op(e0,e0) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[199]) ).
cnf(l18,plain,
( op(e2,e2) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[197]) ).
cnf(l17,plain,
( op(e2,e2) != e2
| op(e3,e3) != e2
| op(e0,e0) != e2
| op(e1,e1) != e2 ),
inference(instantiation,[status(thm)],[186]) ).
cnf(l56,plain,
( op(e1,e1) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[198]) ).
cnf(l676,plain,
( op(e2,e2) != e1
| op(e3,e3) != e1
| op(e0,e0) != e1
| op(e1,e1) != e1 ),
inference(instantiation,[status(thm)],[185]) ).
cnf(l61,plain,
( op(e2,e2) != e3
| op(e3,e3) != e3
| op(e0,e0) != e3
| op(e1,e1) != e3 ),
inference(instantiation,[status(thm)],[187]) ).
cnf(l68,plain,
( op(e2,e2) != e2
| op(e3,e3) != e2
| op(e0,e0) != e2
| op(e1,e1) != e2 ),
inference(instantiation,[status(thm)],[186]) ).
cnf(188,plain,
( op(e3,e3) = e3
| ~ sP2 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l45,plain,
( op(e3,e3) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[188]) ).
cnf(192,plain,
( op(e3,e3) = e2
| ~ sP1 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l820,plain,
( op(e3,e3) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[192]) ).
cnf(l38,plain,
( op(e2,e2) != e1
| op(e3,e3) != e1
| op(e0,e0) != e1
| op(e1,e1) != e1 ),
inference(instantiation,[status(thm)],[185]) ).
cnf(l278,plain,
( op(e0,e0) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[195]) ).
cnf(l93,plain,
( op(e1,e1) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[190]) ).
cnf(l757,plain,
( op(e1,e1) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[198]) ).
cnf(l69,plain,
( op(e2,e2) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[193]) ).
cnf(l216,plain,
( op(e2,e2) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[189]) ).
cnf(l60,plain,
( op(e2,e2) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[197]) ).
cnf(l753,plain,
( op(e3,e3) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[196]) ).
cnf(l150,plain,
( op(e2,e2) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[189]) ).
cnf(l55,plain,
( op(e1,e1) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[190]) ).
cnf(l709,plain,
( op(e2,e2) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[189]) ).
cnf(l43,plain,
( op(e1,e1) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[194]) ).
cnf(l279,plain,
( op(e3,e3) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[196]) ).
cnf(l427,plain,
( op(e0,e0) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[195]) ).
cnf(l704,plain,
( op(e3,e3) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[188]) ).
cnf(l15,plain,
( op(e3,e3) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[188]) ).
cnf(l752,plain,
( op(e0,e0) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[199]) ).
cnf(181,plain,
( op(e1,e1) = e0
| sP0
| sP1
| sP2 ),
inference(cnf,[status(esa)],[co1_negated]) ).
cnf(l367,plain,
( op(e1,e1) = e0
| sP0
| sP1
| sP2 ),
inference(instantiation,[status(thm)],[181]) ).
cnf(l368,plain,
( op(e0,e0) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[199]) ).
cnf(l33,plain,
( op(e3,e3) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[192]) ).
cnf(l22,plain,
( op(e3,e3) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[196]) ).
cnf(l324,plain,
( op(e1,e1) = e0
| sP0
| sP1
| sP2 ),
inference(instantiation,[status(thm)],[181]) ).
cnf(l325,plain,
( op(e0,e0) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[191]) ).
cnf(l714,plain,
( op(e1,e1) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[190]) ).
cnf(l312,plain,
( op(e3,e3) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[192]) ).
cnf(l277,plain,
( op(e0,e0) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[199]) ).
cnf(l819,plain,
( op(e0,e0) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[195]) ).
cnf(l426,plain,
( op(e2,e2) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[197]) ).
cnf(l108,plain,
( op(e2,e2) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[193]) ).
cnf(l299,plain,
( op(e0,e0) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[191]) ).
cnf(l327,plain,
( op(e2,e2) != e3
| op(e3,e3) != e3
| op(e0,e0) != e3
| op(e1,e1) != e3 ),
inference(instantiation,[status(thm)],[187]) ).
cnf(l672,plain,
( op(e1,e1) = e0
| sP0
| sP1
| sP2 ),
inference(instantiation,[status(thm)],[181]) ).
cnf(l811,plain,
( op(e1,e1) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[194]) ).
cnf(l1006,plain,
( op(e3,e3) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[188]) ).
cnf(l345,plain,
( op(e1,e1) = e0
| sP0
| sP1
| sP2 ),
inference(instantiation,[status(thm)],[181]) ).
cnf(l756,plain,
( op(e0,e0) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[191]) ).
cnf(l678,plain,
( op(e3,e3) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[188]) ).
cnf(l301,plain,
( op(e1,e1) = e0
| sP0
| sP1
| sP2 ),
inference(instantiation,[status(thm)],[181]) ).
cnf(l333,plain,
( op(e0,e0) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[195]) ).
cnf(l686,plain,
( op(e1,e1) = e0
| sP0
| sP1
| sP2 ),
inference(instantiation,[status(thm)],[181]) ).
cnf(l934,plain,
( op(e2,e2) != e3
| op(e3,e3) != e3
| op(e0,e0) != e3
| op(e1,e1) != e3 ),
inference(instantiation,[status(thm)],[187]) ).
cnf(l369,plain,
( op(e2,e2) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[193]) ).
cnf(l405,plain,
( op(e0,e0) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[195]) ).
cnf(l747,plain,
( op(e2,e2) != e1
| op(e3,e3) != e1
| op(e0,e0) != e1
| op(e1,e1) != e1 ),
inference(instantiation,[status(thm)],[185]) ).
cnf(l323,plain,
( op(e1,e1) = e0
| sP0
| sP1
| sP2 ),
inference(instantiation,[status(thm)],[181]) ).
cnf(l1046,plain,
( op(e0,e0) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[191]) ).
cnf(l677,plain,
( op(e0,e0) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[199]) ).
cnf(l755,plain,
( op(e2,e2) != e3
| op(e3,e3) != e3
| op(e0,e0) != e3
| op(e1,e1) != e3 ),
inference(instantiation,[status(thm)],[187]) ).
cnf(l1018,plain,
( op(e0,e0) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[191]) ).
cnf(l370,plain,
( op(e2,e2) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[189]) ).
cnf(l39,plain,
( op(e3,e3) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[192]) ).
cnf(l1011,plain,
( op(e3,e3) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[196]) ).
cnf(l349,plain,
( op(e1,e1) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[194]) ).
cnf(l1029,plain,
( op(e2,e2) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[189]) ).
cnf(l271,plain,
( op(e3,e3) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[188]) ).
cnf(l342,plain,
( op(e2,e2) != e2
| op(e3,e3) != e2
| op(e0,e0) != e2
| op(e1,e1) != e2 ),
inference(instantiation,[status(thm)],[186]) ).
cnf(l697,plain,
( op(e2,e2) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[189]) ).
cnf(l733,plain,
( op(e2,e2) != e3
| op(e3,e3) != e3
| op(e0,e0) != e3
| op(e1,e1) != e3 ),
inference(instantiation,[status(thm)],[187]) ).
cnf(l1007,plain,
( op(e2,e2) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[189]) ).
cnf(l743,plain,
( op(e2,e2) != e2
| op(e3,e3) != e2
| op(e0,e0) != e2
| op(e1,e1) != e2 ),
inference(instantiation,[status(thm)],[186]) ).
cnf(l411,plain,
( op(e2,e2) != e2
| op(e3,e3) != e2
| op(e0,e0) != e2
| op(e1,e1) != e2 ),
inference(instantiation,[status(thm)],[186]) ).
cnf(l1048,plain,
( op(e1,e1) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[190]) ).
cnf(l354,plain,
( op(e2,e2) != e2
| op(e3,e3) != e2
| op(e0,e0) != e2
| op(e1,e1) != e2 ),
inference(instantiation,[status(thm)],[186]) ).
cnf(l406,plain,
( op(e0,e0) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[199]) ).
cnf(l1008,plain,
( op(e1,e1) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[190]) ).
cnf(l690,plain,
( op(e2,e2) != e1
| op(e3,e3) != e1
| op(e0,e0) != e1
| op(e1,e1) != e1 ),
inference(instantiation,[status(thm)],[185]) ).
cnf(l779,plain,
( op(e0,e0) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[191]) ).
cnf(l957,plain,
( op(e1,e1) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[194]) ).
cnf(l780,plain,
( op(e3,e3) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[192]) ).
cnf(l1001,plain,
( op(e2,e2) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[193]) ).
cnf(l331,plain,
( op(e1,e1) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[190]) ).
cnf(l1100,plain,
( op(e1,e1) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[194]) ).
cnf(l1135,plain,
( op(e3,e3) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[192]) ).
cnf(l999,plain,
( op(e1,e1) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[198]) ).
cnf(l1110,plain,
( op(e1,e1) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[190]) ).
cnf(l788,plain,
( op(e2,e2) != e1
| op(e3,e3) != e1
| op(e0,e0) != e1
| op(e1,e1) != e1 ),
inference(instantiation,[status(thm)],[185]) ).
cnf(l1012,plain,
( op(e2,e2) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[189]) ).
cnf(l1019,plain,
( op(e1,e1) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[194]) ).
cnf(l356,plain,
( op(e2,e2) != e3
| op(e3,e3) != e3
| op(e0,e0) != e3
| op(e1,e1) != e3 ),
inference(instantiation,[status(thm)],[187]) ).
cnf(l1050,plain,
( op(e2,e2) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[189]) ).
cnf(l1016,plain,
( op(e1,e1) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[198]) ).
cnf(l1131,plain,
( op(e0,e0) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[195]) ).
cnf(l960,plain,
( op(e3,e3) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[192]) ).
cnf(l980,plain,
( op(e2,e2) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[193]) ).
cnf(l778,plain,
( op(e0,e0) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[195]) ).
cnf(l1005,plain,
( op(e2,e2) != e3
| op(e3,e3) != e3
| op(e0,e0) != e3
| op(e1,e1) != e3 ),
inference(instantiation,[status(thm)],[187]) ).
cnf(l1074,plain,
( op(e1,e1) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[198]) ).
cnf(l718,plain,
( op(e0,e0) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[199]) ).
cnf(l997,plain,
( op(e2,e2) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[193]) ).
cnf(l1072,plain,
( op(e3,e3) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[196]) ).
cnf(l1087,plain,
( op(e3,e3) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[188]) ).
cnf(l398,plain,
( op(e1,e1) = e0
| sP0
| sP1
| sP2 ),
inference(instantiation,[status(thm)],[181]) ).
cnf(l400,plain,
( op(e2,e2) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[193]) ).
cnf(l1069,plain,
( op(e3,e3) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[196]) ).
cnf(l998,plain,
( op(e2,e2) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[197]) ).
cnf(l1047,plain,
( op(e0,e0) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[191]) ).
cnf(l927,plain,
( op(e2,e2) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[197]) ).
cnf(l1033,plain,
( op(e3,e3) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[192]) ).
cnf(l801,plain,
( op(e1,e1) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[198]) ).
cnf(l307,plain,
( op(e1,e1) = e0
| sP0
| sP1
| sP2 ),
inference(instantiation,[status(thm)],[181]) ).
cnf(l802,plain,
( op(e2,e2) != e1
| op(e3,e3) != e1
| op(e0,e0) != e1
| op(e1,e1) != e1 ),
inference(instantiation,[status(thm)],[185]) ).
cnf(l1004,plain,
( op(e2,e2) != e1
| op(e3,e3) != e1
| op(e0,e0) != e1
| op(e1,e1) != e1 ),
inference(instantiation,[status(thm)],[185]) ).
cnf(l308,plain,
( op(e1,e1) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[198]) ).
cnf(l1039,plain,
( op(e3,e3) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[188]) ).
cnf(l1128,plain,
( op(e3,e3) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[188]) ).
cnf(l1013,plain,
( op(e2,e2) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[197]) ).
cnf(l1053,plain,
( op(e0,e0) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[191]) ).
cnf(l1172,plain,
( op(e0,e0) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[199]) ).
cnf(l1088,plain,
( op(e3,e3) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[196]) ).
cnf(l1038,plain,
( op(e1,e1) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[198]) ).
cnf(l912,plain,
( op(e1,e1) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[194]) ).
cnf(l1080,plain,
( op(e1,e1) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[190]) ).
cnf(l1030,plain,
( op(e3,e3) = e3
| ~ sP2 ),
inference(instantiation,[status(thm)],[188]) ).
cnf(l987,plain,
( op(e2,e2) != e2
| op(e3,e3) != e2
| op(e0,e0) != e2
| op(e1,e1) != e2 ),
inference(instantiation,[status(thm)],[186]) ).
cnf(l1023,plain,
( op(e2,e2) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[197]) ).
cnf(l981,plain,
( op(e2,e2) != e2
| op(e3,e3) != e2
| op(e0,e0) != e2
| op(e1,e1) != e2 ),
inference(instantiation,[status(thm)],[186]) ).
cnf(l1179,plain,
( op(e2,e2) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[193]) ).
cnf(l1117,plain,
( op(e0,e0) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[195]) ).
cnf(l1079,plain,
( op(e3,e3) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[196]) ).
cnf(l1130,plain,
( op(e1,e1) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[194]) ).
cnf(l1061,plain,
( op(e0,e0) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[195]) ).
cnf(l1173,plain,
( op(e2,e2) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[197]) ).
cnf(l964,plain,
( op(e2,e2) != e1
| op(e3,e3) != e1
| op(e0,e0) != e1
| op(e1,e1) != e1 ),
inference(instantiation,[status(thm)],[185]) ).
cnf(l1204,plain,
( op(e0,e0) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[199]) ).
cnf(l1060,plain,
( op(e3,e3) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[192]) ).
cnf(l1113,plain,
( op(e3,e3) = e2
| ~ sP1 ),
inference(instantiation,[status(thm)],[192]) ).
cnf(l1192,plain,
( op(e2,e2) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[197]) ).
cnf(l1209,plain,
( op(e3,e3) = e1
| ~ sP0 ),
inference(instantiation,[status(thm)],[196]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l2,l5,l11,l7,l1,l14,l9,l16,l24,l10,l21,l19,l3,l20,l693,l680,l701,l57,l6,l694,l28,l4,l31,l62,l18,l17,l56,l676,l61,l68,l45,l820,l38,l278,l93,l757,l69,l216,l60,l753,l150,l55,l709,l43,l279,l427,l704,l15,l752,l367,l368,l33,l22,l324,l325,l714,l312,l277,l819,l426,l108,l299,l327,l672,l811,l1006,l345,l756,l678,l301,l333,l686,l934,l369,l405,l747,l323,l1046,l677,l755,l1018,l370,l39,l1011,l349,l1029,l271,l342,l697,l733,l1007,l743,l411,l1048,l354,l406,l1008,l690,l779,l957,l780,l1001,l331,l1100,l1135,l999,l1110,l788,l1012,l1019,l356,l1050,l1016,l1131,l960,l980,l778,l1005,l1074,l718,l997,l1072,l1087,l398,l400,l1069,l998,l1047,l927,l1033,l801,l307,l802,l1004,l308,l1039,l1128,l1013,l1053,l1172,l1088,l1038,l912,l1080,l1030,l987,l1023,l981,l1179,l1117,l1079,l1130,l1061,l1173,l964,l1204,l1060,l1113,l1192,l1209]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : ALG017+1 : TPTP v9.0.0. Released v2.7.0.
% 0.11/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n019.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Sun Jul 20 01:56:49 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.34 % launching worker at depth: 3
% 0.12/0.34 % launching worker at depth: 5
% 0.12/0.34 % launching worker at depth: 6
% 0.12/0.34 % launching worker at depth: 7
% 0.12/0.34 % launching worker at depth: 4
% 0.12/0.34 % launching worker at depth: 8
% 0.12/0.34 % launching worker at depth: 1
% 0.12/0.34 % launching worker at depth: 2
% 4.57/0.90 % SZS status Theorem for theBenchmark
% 4.57/0.90 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------