%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SYN393+1.003 : TPTP v9.0.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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 : Fri Jul 25 09:27:37 PM UTC 2025
% Result : Theorem 3.59s 0.81s
% Output : CNFRefutation 3.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 1
% Syntax : Number of formulae : 213 ( 1 unt; 0 def)
% Number of atoms : 656 ( 0 equ)
% Maximal formula atoms : 6 ( 3 avg)
% Number of connectives : 793 ( 350 ~; 433 |; 0 &)
% ( 10 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 4 avg)
% Maximal term depth : 0 ( 0 avg)
% Number of predicates : 12 ( 11 usr; 12 prp; 0-0 aty)
% Number of functors : 0 ( 0 usr; 0 con; --- aty)
% Number of variables : 0 ( 0 sgn 0 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(pel12,plain,
( ( ( p1
<=> p2 )
<=> p3 )
<=> ( p1
<=> ( p2
<=> p3 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',pel12) ).
fof(pel12_negated,plain,
~ ( ( ( p1
<=> p2 )
<=> p3 )
<=> ( p1
<=> ( p2
<=> p3 ) ) ),
inference(negate_conjecture,[status(cth)],[pel12]) ).
cnf(0,plain,
( p1
| p2
| sP1
| sP3 ),
inference(cnf,[status(esa)],[pel12_negated]) ).
cnf(l0,plain,
( p1
| p2
| sP1
| sP3 ),
inference(instantiation,[status(thm)],[0]) ).
cnf(6,plain,
( ~ p3
| ~ p1
| ~ p2
| ~ sP7 ),
inference(cnf,[status(esa)],[pel12_negated]) ).
cnf(l1,plain,
( ~ p3
| ~ p1
| ~ p2
| ~ sP7 ),
inference(instantiation,[status(thm)],[6]) ).
cnf(20,plain,
( ~ p1
| ~ p2
| p3
| ~ sP3 ),
inference(cnf,[status(esa)],[pel12_negated]) ).
cnf(l6,plain,
( ~ p1
| ~ p2
| p3
| ~ sP3 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(5,plain,
( ~ p3
| sP5
| sP7
| sP4 ),
inference(cnf,[status(esa)],[pel12_negated]) ).
cnf(l13,plain,
( ~ p3
| sP5
| sP7
| sP4 ),
inference(instantiation,[status(thm)],[5]) ).
cnf(24,plain,
( ~ p1
| sP0
| ~ sP1 ),
inference(cnf,[status(esa)],[pel12_negated]) ).
cnf(l2,plain,
( ~ p1
| sP0
| ~ sP1 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(3,plain,
( p1
| sP5
| sP7 ),
inference(cnf,[status(esa)],[pel12_negated]) ).
cnf(l4,plain,
( p1
| sP5
| sP7 ),
inference(instantiation,[status(thm)],[3]) ).
cnf(12,plain,
( ~ p1
| ~ sP5 ),
inference(cnf,[status(esa)],[pel12_negated]) ).
cnf(l298,plain,
( ~ p1
| ~ sP5 ),
inference(instantiation,[status(thm)],[12]) ).
cnf(26,plain,
( p1
| ~ sP0 ),
inference(cnf,[status(esa)],[pel12_negated]) ).
cnf(l910,plain,
( p1
| ~ sP0 ),
inference(instantiation,[status(thm)],[26]) ).
cnf(10,plain,
( p1
| ~ sP6 ),
inference(cnf,[status(esa)],[pel12_negated]) ).
cnf(l41,plain,
( p1
| ~ sP6 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(17,plain,
( ~ p3
| p1
| sP2
| ~ sP3 ),
inference(cnf,[status(esa)],[pel12_negated]) ).
cnf(l293,plain,
( ~ p3
| p1
| sP2
| ~ sP3 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(2,plain,
( ~ p3
| sP1
| sP3 ),
inference(cnf,[status(esa)],[pel12_negated]) ).
cnf(l8,plain,
( ~ p3
| sP1
| sP3 ),
inference(instantiation,[status(thm)],[2]) ).
cnf(8,plain,
( ~ p2
| p3
| sP6
| ~ sP7 ),
inference(cnf,[status(esa)],[pel12_negated]) ).
cnf(l234,plain,
( ~ p2
| p3
| sP6
| ~ sP7 ),
inference(instantiation,[status(thm)],[8]) ).
cnf(23,plain,
( ~ p2
| sP0
| ~ sP1 ),
inference(cnf,[status(esa)],[pel12_negated]) ).
cnf(l913,plain,
( ~ p2
| sP0
| ~ sP1 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l14,plain,
( ~ p1
| ~ p2
| p3
| ~ sP3 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l3,plain,
( ~ p2
| sP0
| ~ sP1 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l7,plain,
( ~ p2
| p3
| sP6
| ~ sP7 ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l20,plain,
( p1
| ~ sP6 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(9,plain,
( ~ p1
| p3
| sP6
| ~ sP7 ),
inference(cnf,[status(esa)],[pel12_negated]) ).
cnf(l308,plain,
( ~ p1
| p3
| sP6
| ~ sP7 ),
inference(instantiation,[status(thm)],[9]) ).
cnf(19,plain,
( ~ p3
| ~ p1
| p2
| ~ sP3 ),
inference(cnf,[status(esa)],[pel12_negated]) ).
cnf(l16,plain,
( ~ p3
| ~ p1
| p2
| ~ sP3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(13,plain,
( ~ p3
| p2
| ~ sP5 ),
inference(cnf,[status(esa)],[pel12_negated]) ).
cnf(l241,plain,
( ~ p3
| p2
| ~ sP5 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l5,plain,
( ~ p3
| p2
| ~ sP5 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(14,plain,
( ~ p2
| p3
| ~ sP5 ),
inference(cnf,[status(esa)],[pel12_negated]) ).
cnf(l542,plain,
( ~ p2
| p3
| ~ sP5 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(21,plain,
( ~ p2
| ~ sP2 ),
inference(cnf,[status(esa)],[pel12_negated]) ).
cnf(l841,plain,
( ~ p2
| ~ sP2 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l96,plain,
( ~ p2
| p3
| ~ sP5 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l236,plain,
( ~ p3
| p1
| sP2
| ~ sP3 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(4,plain,
( p2
| sP5
| sP7
| sP4 ),
inference(cnf,[status(esa)],[pel12_negated]) ).
cnf(l9,plain,
( p2
| sP5
| sP7
| sP4 ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l30,plain,
( p1
| sP5
| sP7 ),
inference(instantiation,[status(thm)],[3]) ).
cnf(1,plain,
( ~ p1
| ~ p2
| sP1
| sP3 ),
inference(cnf,[status(esa)],[pel12_negated]) ).
cnf(l898,plain,
( ~ p1
| ~ p2
| sP1
| sP3 ),
inference(instantiation,[status(thm)],[1]) ).
cnf(7,plain,
( ~ p3
| p1
| p2
| ~ sP7 ),
inference(cnf,[status(esa)],[pel12_negated]) ).
cnf(l42,plain,
( ~ p3
| p1
| p2
| ~ sP7 ),
inference(instantiation,[status(thm)],[7]) ).
cnf(11,plain,
( p2
| ~ sP6 ),
inference(cnf,[status(esa)],[pel12_negated]) ).
cnf(l959,plain,
( p2
| ~ sP6 ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l318,plain,
( ~ p3
| sP1
| sP3 ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l938,plain,
( ~ p3
| sP1
| sP3 ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l922,plain,
( ~ p1
| ~ p2
| p3
| ~ sP3 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l305,plain,
( ~ p3
| sP5
| sP7
| sP4 ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l310,plain,
( ~ p1
| ~ sP5 ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l958,plain,
( p2
| sP5
| sP7
| sP4 ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l604,plain,
( ~ p3
| ~ p1
| p2
| ~ sP3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(15,plain,
( ~ p2
| ~ sP4 ),
inference(cnf,[status(esa)],[pel12_negated]) ).
cnf(l320,plain,
( ~ p2
| ~ sP4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(18,plain,
( p1
| p2
| sP2
| ~ sP3 ),
inference(cnf,[status(esa)],[pel12_negated]) ).
cnf(l46,plain,
( p1
| p2
| sP2
| ~ sP3 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l71,plain,
( ~ p3
| p1
| p2
| ~ sP7 ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l642,plain,
( ~ p2
| ~ sP2 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l593,plain,
( ~ p2
| ~ sP4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l951,plain,
( ~ p3
| p1
| sP2
| ~ sP3 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l986,plain,
( ~ p2
| p3
| sP6
| ~ sP7 ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l242,plain,
( ~ p3
| sP5
| sP7
| sP4 ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1006,plain,
( p2
| ~ sP6 ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l948,plain,
( ~ p2
| p3
| ~ sP5 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l954,plain,
( ~ p2
| ~ sP4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l530,plain,
( ~ p3
| sP1
| sP3 ),
inference(instantiation,[status(thm)],[2]) ).
cnf(l965,plain,
( ~ p1
| p3
| sP6
| ~ sP7 ),
inference(instantiation,[status(thm)],[9]) ).
cnf(16,plain,
( p3
| ~ sP4 ),
inference(cnf,[status(esa)],[pel12_negated]) ).
cnf(l23,plain,
( p3
| ~ sP4 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l531,plain,
( ~ p2
| p3
| ~ sP5 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(25,plain,
( p3
| ~ sP1 ),
inference(cnf,[status(esa)],[pel12_negated]) ).
cnf(l349,plain,
( p3
| ~ sP1 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l850,plain,
( p2
| ~ sP6 ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l896,plain,
( ~ p3
| ~ p1
| ~ p2
| ~ sP7 ),
inference(instantiation,[status(thm)],[6]) ).
cnf(22,plain,
( p3
| ~ sP2 ),
inference(cnf,[status(esa)],[pel12_negated]) ).
cnf(l763,plain,
( p3
| ~ sP2 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l668,plain,
( p1
| sP5
| sP7 ),
inference(instantiation,[status(thm)],[3]) ).
cnf(27,plain,
( p2
| ~ sP0 ),
inference(cnf,[status(esa)],[pel12_negated]) ).
cnf(l384,plain,
( p2
| ~ sP0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l72,plain,
( ~ p1
| sP0
| ~ sP1 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l985,plain,
( ~ p2
| ~ sP2 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l978,plain,
( ~ p2
| p3
| ~ sP5 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l110,plain,
( ~ p2
| p3
| ~ sP5 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l546,plain,
( p1
| sP5
| sP7 ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l979,plain,
( p2
| sP5
| sP7
| sP4 ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l984,plain,
( p3
| ~ sP4 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l962,plain,
( ~ p3
| ~ p1
| ~ p2
| ~ sP7 ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l927,plain,
( ~ p3
| sP5
| sP7
| sP4 ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1011,plain,
( p2
| ~ sP6 ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l1055,plain,
( p3
| ~ sP4 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l302,plain,
( p2
| ~ sP0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l957,plain,
( p3
| ~ sP1 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l612,plain,
( ~ p3
| ~ p1
| ~ p2
| ~ sP7 ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l911,plain,
( ~ p2
| ~ sP4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l344,plain,
( p3
| ~ sP1 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l932,plain,
( ~ p1
| ~ p2
| sP1
| sP3 ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l323,plain,
( ~ p3
| ~ p1
| p2
| ~ sP3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l964,plain,
( ~ p1
| ~ p2
| p3
| ~ sP3 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1167,plain,
( ~ p3
| sP5
| sP7
| sP4 ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l389,plain,
( ~ p2
| p3
| ~ sP5 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1062,plain,
( ~ p2
| ~ sP4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l945,plain,
( ~ p3
| sP5
| sP7
| sP4 ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l969,plain,
( ~ p3
| p1
| p2
| ~ sP7 ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l585,plain,
( ~ p3
| p2
| ~ sP5 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l995,plain,
( ~ p2
| ~ sP4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1064,plain,
( ~ p1
| p3
| sP6
| ~ sP7 ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l838,plain,
( ~ p3
| p1
| p2
| ~ sP7 ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l929,plain,
( ~ p1
| ~ sP5 ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l431,plain,
( p3
| ~ sP1 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1072,plain,
( ~ p1
| ~ sP5 ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l973,plain,
( ~ p2
| p3
| ~ sP5 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1000,plain,
( p1
| sP5
| sP7 ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l1024,plain,
( ~ p3
| ~ p1
| ~ p2
| ~ sP7 ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1019,plain,
( p3
| ~ sP2 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l1116,plain,
( p1
| p2
| sP2
| ~ sP3 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l1087,plain,
( p1
| p2
| sP2
| ~ sP3 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l1020,plain,
( ~ p3
| sP5
| sP7
| sP4 ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1168,plain,
( ~ p1
| ~ sP5 ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l1097,plain,
( ~ p3
| ~ p1
| ~ p2
| ~ sP7 ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l47,plain,
( ~ p2
| p3
| ~ sP5 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1197,plain,
( p3
| ~ sP2 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l963,plain,
( ~ p2
| p3
| sP6
| ~ sP7 ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1111,plain,
( p1
| ~ sP6 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l545,plain,
( ~ p2
| sP0
| ~ sP1 ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l1198,plain,
( p3
| ~ sP1 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l968,plain,
( ~ p1
| ~ p2
| p3
| ~ sP3 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l324,plain,
( ~ p1
| p3
| sP6
| ~ sP7 ),
inference(instantiation,[status(thm)],[9]) ).
cnf(l59,plain,
( ~ p1
| ~ p2
| p3
| ~ sP3 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l915,plain,
( p3
| ~ sP1 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1041,plain,
( ~ p1
| ~ p2
| p3
| ~ sP3 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l411,plain,
( ~ p3
| ~ p1
| ~ p2
| ~ sP7 ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l991,plain,
( ~ p1
| ~ p2
| p3
| ~ sP3 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l522,plain,
( ~ p3
| sP5
| sP7
| sP4 ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1199,plain,
( ~ p3
| p2
| ~ sP5 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l624,plain,
( p1
| sP5
| sP7 ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l953,plain,
( p3
| ~ sP2 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l191,plain,
( p3
| ~ sP2 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l196,plain,
( p2
| ~ sP0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1174,plain,
( ~ p2
| ~ sP4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l567,plain,
( p2
| sP5
| sP7
| sP4 ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l1032,plain,
( p1
| p2
| sP2
| ~ sP3 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l1088,plain,
( ~ p1
| sP0
| ~ sP1 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l804,plain,
( p1
| p2
| sP2
| ~ sP3 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l1239,plain,
( p2
| ~ sP0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l974,plain,
( ~ p3
| p1
| sP2
| ~ sP3 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l977,plain,
( ~ p2
| ~ sP2 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1040,plain,
( ~ p1
| ~ p2
| sP1
| sP3 ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1226,plain,
( ~ p3
| p2
| ~ sP5 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l190,plain,
( ~ p1
| ~ p2
| sP1
| sP3 ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1042,plain,
( p2
| ~ sP6 ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l999,plain,
( ~ p1
| sP0
| ~ sP1 ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l1120,plain,
( p3
| ~ sP1 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l690,plain,
( ~ p3
| p1
| p2
| ~ sP7 ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1153,plain,
( ~ p1
| ~ sP5 ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l1026,plain,
( ~ p1
| ~ p2
| p3
| ~ sP3 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l697,plain,
( p1
| ~ sP0 ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l1173,plain,
( p1
| ~ sP0 ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l1005,plain,
( ~ p1
| ~ p2
| p3
| ~ sP3 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1181,plain,
( ~ p2
| ~ sP4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1207,plain,
( ~ p1
| ~ p2
| sP1
| sP3 ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l1068,plain,
( ~ p2
| p3
| sP6
| ~ sP7 ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1218,plain,
( ~ p1
| ~ p2
| p3
| ~ sP3 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1171,plain,
( ~ p1
| ~ p2
| p3
| ~ sP3 ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l666,plain,
( ~ p2
| ~ sP2 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1177,plain,
( ~ p1
| ~ p2
| sP1
| sP3 ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l955,plain,
( p1
| p2
| sP2
| ~ sP3 ),
inference(instantiation,[status(thm)],[18]) ).
cnf(l1091,plain,
( p3
| ~ sP2 ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l966,plain,
( p3
| ~ sP4 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l1203,plain,
( p2
| ~ sP0 ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1030,plain,
( ~ p1
| ~ p2
| sP1
| sP3 ),
inference(instantiation,[status(thm)],[1]) ).
cnf(l920,plain,
( p1
| sP5
| sP7 ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l982,plain,
( ~ p3
| p2
| ~ sP5 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l407,plain,
( ~ p3
| sP5
| sP7
| sP4 ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1105,plain,
( ~ p2
| p3
| ~ sP5 ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1184,plain,
( ~ p1
| ~ sP5 ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l983,plain,
( ~ p1
| ~ sP5 ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l1187,plain,
( ~ p3
| ~ p1
| ~ p2
| ~ sP7 ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1279,plain,
( p1
| ~ sP0 ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l1191,plain,
( p2
| sP5
| sP7
| sP4 ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l989,plain,
( p1
| sP5
| sP7 ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l797,plain,
( ~ p3
| ~ p1
| p2
| ~ sP3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1250,plain,
( p3
| ~ sP4 ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l1255,plain,
( p1
| sP5
| sP7 ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l912,plain,
( ~ p3
| p1
| sP2
| ~ sP3 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l356,plain,
( ~ p3
| ~ p1
| p2
| ~ sP3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1092,plain,
( ~ p3
| p2
| ~ sP5 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1145,plain,
( p1
| ~ sP6 ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1130,plain,
( p1
| sP5
| sP7 ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l1182,plain,
( p3
| ~ sP1 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1139,plain,
( ~ p3
| ~ p1
| p2
| ~ sP3 ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1137,plain,
( ~ p2
| ~ sP2 ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1083,plain,
( ~ p3
| p1
| p2
| ~ sP7 ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l921,plain,
( ~ p3
| p2
| ~ sP5 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1224,plain,
( p3
| ~ sP1 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1190,plain,
( p3
| ~ sP1 ),
inference(instantiation,[status(thm)],[25]) ).
cnf(l1169,plain,
( ~ p2
| ~ sP4 ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1192,plain,
( ~ p1
| ~ sP5 ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l1014,plain,
( ~ p3
| p1
| sP2
| ~ sP3 ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l358,plain,
( ~ p3
| p1
| p2
| ~ sP7 ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l1018,plain,
( ~ p1
| ~ sP5 ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l1189,plain,
( p1
| ~ sP0 ),
inference(instantiation,[status(thm)],[26]) ).
cnf(l1151,plain,
( p1
| sP5
| sP7 ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l1314,plain,
( ~ p3
| p2
| ~ sP5 ),
inference(instantiation,[status(thm)],[13]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l6,l13,l2,l4,l298,l910,l41,l293,l8,l234,l913,l14,l3,l7,l20,l308,l16,l241,l5,l542,l841,l96,l236,l9,l30,l898,l42,l959,l318,l938,l922,l305,l310,l958,l604,l320,l46,l71,l642,l593,l951,l986,l242,l1006,l948,l954,l530,l965,l23,l531,l349,l850,l896,l763,l668,l384,l72,l985,l978,l110,l546,l979,l984,l962,l927,l1011,l1055,l302,l957,l612,l911,l344,l932,l323,l964,l1167,l389,l1062,l945,l969,l585,l995,l1064,l838,l929,l431,l1072,l973,l1000,l1024,l1019,l1116,l1087,l1020,l1168,l1097,l47,l1197,l963,l1111,l545,l1198,l968,l324,l59,l915,l1041,l411,l991,l522,l1199,l624,l953,l191,l196,l1174,l567,l1032,l1088,l804,l1239,l974,l977,l1040,l1226,l190,l1042,l999,l1120,l690,l1153,l1026,l697,l1173,l1005,l1181,l1207,l1068,l1218,l1171,l666,l1177,l955,l1091,l966,l1203,l1030,l920,l982,l407,l1105,l1184,l983,l1187,l1279,l1191,l989,l797,l1250,l1255,l912,l356,l1092,l1145,l1130,l1182,l1139,l1137,l1083,l921,l1224,l1190,l1169,l1192,l1014,l358,l1018,l1189,l1151,l1314]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SYN393+1.003 : TPTP v9.0.0. Released v2.0.0.
% 0.11/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.33 % Computer : n026.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Tue Jul 22 16:00:04 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.13/0.34 % launching worker at depth: 4
% 0.13/0.34 % launching worker at depth: 7
% 0.13/0.34 % launching worker at depth: 2
% 0.13/0.34 % launching worker at depth: 1
% 0.13/0.34 % launching worker at depth: 3
% 0.13/0.34 % launching worker at depth: 6
% 0.13/0.34 % launching worker at depth: 5
% 0.13/0.34 % launching worker at depth: 8
% 3.59/0.81 % SZS status Theorem for theBenchmark
% 3.59/0.81 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------