%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : KRS103+1 : TPTP v9.0.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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 08:46:40 PM UTC 2025
% Result : Unsatisfiable 9.15s 1.49s
% Output : CNFRefutation 9.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 44
% Syntax : Number of formulae : 319 ( 4 unt; 0 def)
% Number of atoms : 1000 ( 0 equ)
% Maximal formula atoms : 4 ( 3 avg)
% Number of connectives : 1085 ( 404 ~; 638 |; 9 &)
% ( 0 <=>; 34 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 20 ( 19 usr; 1 prp; 0-1 aty)
% Number of functors : 1 ( 1 usr; 1 con; 0-0 aty)
% Number of variables : 86 ( 0 sgn 43 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_47,plain,
cTest(i2003_11_14_17_20_46476),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_47) ).
cnf(49,plain,
cTest(i2003_11_14_17_20_46476),
inference(cnf,[status(esa)],[axiom_47]) ).
cnf(l0,plain,
cTest(i2003_11_14_17_20_46476),
inference(instantiation,[status(thm)],[49]) ).
fof(axiom_42,plain,
! [X] :
( cTest(X)
=> ( cminus4(X)
| cminus3(X)
| cplus6(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_42) ).
cnf(44,plain,
( ~ cTest(X0)
| cminus4(X0)
| cplus6(X0)
| cminus3(X0) ),
inference(cnf,[status(esa)],[axiom_42]) ).
cnf(l1,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cplus6(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[44]) ).
fof(axiom_56,plain,
! [X] :
~ ( cplus6(X)
& cminus6(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_56) ).
cnf(58,plain,
( ~ cplus6(X0)
| ~ cminus6(X0) ),
inference(cnf,[status(esa)],[axiom_56]) ).
cnf(l4,plain,
( ~ cplus6(i2003_11_14_17_20_46476)
| ~ cminus6(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[58]) ).
fof(axiom_21,plain,
! [X] :
( cTest(X)
=> ( cminus2(X)
| cplus4(X)
| cminus6(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_21) ).
cnf(23,plain,
( ~ cTest(X0)
| cminus6(X0)
| cminus2(X0)
| cplus4(X0) ),
inference(cnf,[status(esa)],[axiom_21]) ).
cnf(l5,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus6(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[23]) ).
fof(axiom_54,plain,
! [X] :
~ ( cminus2(X)
& cplus2(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_54) ).
cnf(56,plain,
( ~ cminus2(X0)
| ~ cplus2(X0) ),
inference(cnf,[status(esa)],[axiom_54]) ).
cnf(l388,plain,
( ~ cminus2(i2003_11_14_17_20_46476)
| ~ cplus2(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[56]) ).
fof(axiom_13,plain,
! [X] :
( cTest(X)
=> ( cplus2(X)
| cplus5(X)
| cplus9(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_13) ).
cnf(15,plain,
( ~ cTest(X0)
| cplus9(X0)
| cplus5(X0)
| cplus2(X0) ),
inference(cnf,[status(esa)],[axiom_13]) ).
cnf(l1306,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus9(i2003_11_14_17_20_46476)
| cplus5(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[15]) ).
fof(axiom_49,plain,
! [X] :
~ ( cminus9(X)
& cplus9(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_49) ).
cnf(51,plain,
( ~ cplus9(X0)
| ~ cminus9(X0) ),
inference(cnf,[status(esa)],[axiom_49]) ).
cnf(l1307,plain,
( ~ cplus9(i2003_11_14_17_20_46476)
| ~ cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[51]) ).
fof(axiom_53,plain,
! [X] :
~ ( cplus5(X)
& cminus5(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_53) ).
cnf(55,plain,
( ~ cminus5(X0)
| ~ cplus5(X0) ),
inference(cnf,[status(esa)],[axiom_53]) ).
cnf(l1308,plain,
( ~ cminus5(i2003_11_14_17_20_46476)
| ~ cplus5(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[55]) ).
fof(axiom_52,plain,
! [X] :
~ ( cplus3(X)
& cminus3(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_52) ).
cnf(54,plain,
( ~ cminus3(X0)
| ~ cplus3(X0) ),
inference(cnf,[status(esa)],[axiom_52]) ).
cnf(l6,plain,
( ~ cminus3(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[54]) ).
fof(axiom_6,plain,
! [X] :
( cTest(X)
=> ( cplus3(X)
| cminus7(X)
| cplus8(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_6) ).
cnf(8,plain,
( ~ cTest(X0)
| cplus3(X0)
| cminus7(X0)
| cplus8(X0) ),
inference(cnf,[status(esa)],[axiom_6]) ).
cnf(l9,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus7(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[8]) ).
fof(axiom_51,plain,
! [X] :
~ ( cminus7(X)
& cplus7(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_51) ).
cnf(53,plain,
( ~ cplus7(X0)
| ~ cminus7(X0) ),
inference(cnf,[status(esa)],[axiom_51]) ).
cnf(l1309,plain,
( ~ cplus7(i2003_11_14_17_20_46476)
| ~ cminus7(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[53]) ).
fof(axiom_50,plain,
! [X] :
~ ( cplus4(X)
& cminus4(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_50) ).
cnf(52,plain,
( ~ cminus4(X0)
| ~ cplus4(X0) ),
inference(cnf,[status(esa)],[axiom_50]) ).
cnf(l7,plain,
( ~ cminus4(i2003_11_14_17_20_46476)
| ~ cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[52]) ).
fof(axiom_48,plain,
! [X] :
~ ( cminus8(X)
& cplus8(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_48) ).
cnf(50,plain,
( ~ cminus8(X0)
| ~ cplus8(X0) ),
inference(cnf,[status(esa)],[axiom_48]) ).
cnf(l16,plain,
( ~ cminus8(i2003_11_14_17_20_46476)
| ~ cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[50]) ).
fof(axiom_40,plain,
! [X] :
( cTest(X)
=> ( cminus9(X)
| cplus3(X)
| cminus5(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_40) ).
cnf(42,plain,
( ~ cTest(X0)
| cminus5(X0)
| cplus3(X0)
| cminus9(X0) ),
inference(cnf,[status(esa)],[axiom_40]) ).
cnf(l1310,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus5(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[42]) ).
fof(axiom_46,plain,
! [X] :
( cTest(X)
=> ( cminus5(X)
| cplus7(X)
| cplus8(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_46) ).
cnf(48,plain,
( ~ cTest(X0)
| cminus5(X0)
| cplus7(X0)
| cplus8(X0) ),
inference(cnf,[status(esa)],[axiom_46]) ).
cnf(l1311,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus5(i2003_11_14_17_20_46476)
| cplus7(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l2,plain,
( ~ cminus4(i2003_11_14_17_20_46476)
| ~ cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l1312,plain,
( ~ cminus3(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[54]) ).
fof(axiom_34,plain,
! [X] :
( cTest(X)
=> ( cminus4(X)
| cplus9(X)
| cplus7(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_34) ).
cnf(36,plain,
( ~ cTest(X0)
| cminus4(X0)
| cplus9(X0)
| cplus7(X0) ),
inference(cnf,[status(esa)],[axiom_34]) ).
cnf(l12,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cplus9(i2003_11_14_17_20_46476)
| cplus7(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l1315,plain,
( ~ cplus9(i2003_11_14_17_20_46476)
| ~ cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[51]) ).
fof(axiom_29,plain,
! [X] :
( cTest(X)
=> ( cminus4(X)
| cminus3(X)
| cminus7(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_29) ).
cnf(31,plain,
( ~ cTest(X0)
| cminus4(X0)
| cminus3(X0)
| cminus7(X0) ),
inference(cnf,[status(esa)],[axiom_29]) ).
cnf(l1316,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476)
| cminus7(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l1313,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus5(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[42]) ).
cnf(l1317,plain,
( ~ cplus7(i2003_11_14_17_20_46476)
| ~ cminus7(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l1318,plain,
( ~ cminus4(i2003_11_14_17_20_46476)
| ~ cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l851,plain,
( ~ cplus7(i2003_11_14_17_20_46476)
| ~ cminus7(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[53]) ).
fof(axiom_32,plain,
! [X] :
( cTest(X)
=> ( cplus3(X)
| cminus8(X)
| cplus9(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_32) ).
cnf(34,plain,
( ~ cTest(X0)
| cplus9(X0)
| cplus3(X0)
| cminus8(X0) ),
inference(cnf,[status(esa)],[axiom_32]) ).
cnf(l17,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus9(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l1314,plain,
( ~ cminus5(i2003_11_14_17_20_46476)
| ~ cplus5(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l1322,plain,
( ~ cminus5(i2003_11_14_17_20_46476)
| ~ cplus5(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l15,plain,
( ~ cplus9(i2003_11_14_17_20_46476)
| ~ cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[51]) ).
fof(axiom_15,plain,
! [X] :
( cTest(X)
=> ( cminus3(X)
| cplus5(X)
| cminus8(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_15) ).
cnf(17,plain,
( ~ cTest(X0)
| cminus3(X0)
| cplus5(X0)
| cminus8(X0) ),
inference(cnf,[status(esa)],[axiom_15]) ).
cnf(l1319,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476)
| cplus5(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1334,plain,
( ~ cminus3(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[54]) ).
fof(axiom_41,plain,
! [X] :
( cTest(X)
=> ( cplus4(X)
| cplus1(X)
| cplus7(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_41) ).
cnf(43,plain,
( ~ cTest(X0)
| cplus1(X0)
| cplus7(X0)
| cplus4(X0) ),
inference(cnf,[status(esa)],[axiom_41]) ).
cnf(l1338,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus1(i2003_11_14_17_20_46476)
| cplus7(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(l1321,plain,
( ~ cminus8(i2003_11_14_17_20_46476)
| ~ cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l8,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus6(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l1328,plain,
( ~ cplus9(i2003_11_14_17_20_46476)
| ~ cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[51]) ).
fof(axiom_9,plain,
! [X] :
( cTest(X)
=> ( cminus9(X)
| cminus4(X)
| cminus8(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_9) ).
cnf(11,plain,
( ~ cTest(X0)
| cminus4(X0)
| cminus8(X0)
| cminus9(X0) ),
inference(cnf,[status(esa)],[axiom_9]) ).
cnf(l1325,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[11]) ).
fof(axiom_55,plain,
! [X] :
~ ( cminus1(X)
& cplus1(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_55) ).
cnf(57,plain,
( ~ cplus1(X0)
| ~ cminus1(X0) ),
inference(cnf,[status(esa)],[axiom_55]) ).
cnf(l1366,plain,
( ~ cplus1(i2003_11_14_17_20_46476)
| ~ cminus1(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l1348,plain,
( ~ cminus8(i2003_11_14_17_20_46476)
| ~ cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l10,plain,
( ~ cplus6(i2003_11_14_17_20_46476)
| ~ cminus6(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l11,plain,
( ~ cminus2(i2003_11_14_17_20_46476)
| ~ cplus2(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l1323,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus9(i2003_11_14_17_20_46476)
| cplus5(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[15]) ).
fof(axiom_8,plain,
! [X] :
( cTest(X)
=> ( cminus7(X)
| cplus9(X)
| cminus6(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_8) ).
cnf(10,plain,
( ~ cTest(X0)
| cplus9(X0)
| cminus6(X0)
| cminus7(X0) ),
inference(cnf,[status(esa)],[axiom_8]) ).
cnf(l880,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus9(i2003_11_14_17_20_46476)
| cminus6(i2003_11_14_17_20_46476)
| cminus7(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l1361,plain,
( ~ cplus9(i2003_11_14_17_20_46476)
| ~ cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l1320,plain,
( ~ cminus3(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l1331,plain,
( ~ cminus2(i2003_11_14_17_20_46476)
| ~ cplus2(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[56]) ).
fof(axiom_20,plain,
! [X] :
( cTest(X)
=> ( cminus3(X)
| cplus2(X)
| cplus8(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_20) ).
cnf(22,plain,
( ~ cTest(X0)
| cminus3(X0)
| cplus2(X0)
| cplus8(X0) ),
inference(cnf,[status(esa)],[axiom_20]) ).
cnf(l26,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l28,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[11]) ).
fof(axiom_35,plain,
! [X] :
( cTest(X)
=> ( cminus9(X)
| cminus2(X)
| cplus3(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_35) ).
cnf(37,plain,
( ~ cTest(X0)
| cminus2(X0)
| cplus3(X0)
| cminus9(X0) ),
inference(cnf,[status(esa)],[axiom_35]) ).
cnf(l1371,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l1339,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus5(i2003_11_14_17_20_46476)
| cplus7(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l891,plain,
( ~ cplus9(i2003_11_14_17_20_46476)
| ~ cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[51]) ).
fof(axiom_33,plain,
! [X] :
( cTest(X)
=> ( cminus9(X)
| cminus2(X)
| cplus7(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_33) ).
cnf(35,plain,
( ~ cTest(X0)
| cminus2(X0)
| cplus7(X0)
| cminus9(X0) ),
inference(cnf,[status(esa)],[axiom_33]) ).
cnf(l1330,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476)
| cplus7(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l1389,plain,
( ~ cplus7(i2003_11_14_17_20_46476)
| ~ cminus7(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l1343,plain,
( ~ cminus2(i2003_11_14_17_20_46476)
| ~ cplus2(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l1375,plain,
( ~ cminus2(i2003_11_14_17_20_46476)
| ~ cplus2(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[56]) ).
fof(axiom_19,plain,
! [X] :
( cTest(X)
=> ( cplus2(X)
| cplus1(X)
| cminus6(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_19) ).
cnf(21,plain,
( ~ cTest(X0)
| cplus1(X0)
| cminus6(X0)
| cplus2(X0) ),
inference(cnf,[status(esa)],[axiom_19]) ).
cnf(l1360,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus1(i2003_11_14_17_20_46476)
| cminus6(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l74,plain,
( ~ cminus3(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l1347,plain,
( ~ cminus8(i2003_11_14_17_20_46476)
| ~ cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l1386,plain,
( ~ cplus9(i2003_11_14_17_20_46476)
| ~ cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l1358,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476)
| cplus5(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l894,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l1364,plain,
( ~ cplus1(i2003_11_14_17_20_46476)
| ~ cminus1(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l1528,plain,
( ~ cminus8(i2003_11_14_17_20_46476)
| ~ cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l1368,plain,
( ~ cplus6(i2003_11_14_17_20_46476)
| ~ cminus6(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[58]) ).
fof(axiom_36,plain,
! [X] :
( cTest(X)
=> ( cminus1(X)
| cplus4(X)
| cplus2(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_36) ).
cnf(38,plain,
( ~ cTest(X0)
| cminus1(X0)
| cplus2(X0)
| cplus4(X0) ),
inference(cnf,[status(esa)],[axiom_36]) ).
cnf(l1529,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus1(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[38]) ).
fof(axiom_3,plain,
! [X] :
( cTest(X)
=> ( cminus3(X)
| cminus5(X)
| cminus8(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_3) ).
cnf(5,plain,
( ~ cTest(X0)
| cminus5(X0)
| cminus3(X0)
| cminus8(X0) ),
inference(cnf,[status(esa)],[axiom_3]) ).
cnf(l1353,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus5(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[5]) ).
fof(axiom_27,plain,
! [X] :
( cTest(X)
=> ( cplus4(X)
| cminus5(X)
| cplus6(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_27) ).
cnf(29,plain,
( ~ cTest(X0)
| cminus5(X0)
| cplus6(X0)
| cplus4(X0) ),
inference(cnf,[status(esa)],[axiom_27]) ).
cnf(l1523,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus5(i2003_11_14_17_20_46476)
| cplus6(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l1533,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476)
| cplus5(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1548,plain,
( ~ cminus5(i2003_11_14_17_20_46476)
| ~ cplus5(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[55]) ).
fof(axiom_22,plain,
! [X] :
( cTest(X)
=> ( cminus2(X)
| cplus6(X)
| cminus7(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_22) ).
cnf(24,plain,
( ~ cTest(X0)
| cplus6(X0)
| cminus2(X0)
| cminus7(X0) ),
inference(cnf,[status(esa)],[axiom_22]) ).
cnf(l1391,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus6(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476)
| cminus7(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l1400,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus9(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l1543,plain,
( ~ cminus5(i2003_11_14_17_20_46476)
| ~ cplus5(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l1526,plain,
( ~ cminus5(i2003_11_14_17_20_46476)
| ~ cplus5(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l33,plain,
( ~ cminus8(i2003_11_14_17_20_46476)
| ~ cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[50]) ).
fof(axiom_28,plain,
! [X] :
( cTest(X)
=> ( cminus9(X)
| cplus3(X)
| cplus4(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_28) ).
cnf(30,plain,
( ~ cTest(X0)
| cplus3(X0)
| cminus9(X0)
| cplus4(X0) ),
inference(cnf,[status(esa)],[axiom_28]) ).
cnf(l1373,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[30]) ).
fof(axiom_45,plain,
! [X] :
( cTest(X)
=> ( cminus4(X)
| cplus2(X)
| cplus8(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_45) ).
cnf(47,plain,
( ~ cTest(X0)
| cminus4(X0)
| cplus2(X0)
| cplus8(X0) ),
inference(cnf,[status(esa)],[axiom_45]) ).
cnf(l34,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l1376,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l1440,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476)
| cplus7(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l1344,plain,
( ~ cplus7(i2003_11_14_17_20_46476)
| ~ cminus7(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l1562,plain,
( ~ cminus8(i2003_11_14_17_20_46476)
| ~ cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l37,plain,
( ~ cminus2(i2003_11_14_17_20_46476)
| ~ cplus2(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l1012,plain,
( ~ cminus8(i2003_11_14_17_20_46476)
| ~ cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l1419,plain,
( ~ cminus2(i2003_11_14_17_20_46476)
| ~ cplus2(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l1630,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[11]) ).
fof(axiom_26,plain,
! [X] :
( cTest(X)
=> ( cplus2(X)
| cminus5(X)
| cminus7(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_26) ).
cnf(28,plain,
( ~ cTest(X0)
| cminus5(X0)
| cplus2(X0)
| cminus7(X0) ),
inference(cnf,[status(esa)],[axiom_26]) ).
cnf(l1345,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus5(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cminus7(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[28]) ).
fof(axiom_11,plain,
! [X] :
( cTest(X)
=> ( cplus4(X)
| cplus6(X)
| cminus8(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_11) ).
cnf(13,plain,
( ~ cTest(X0)
| cplus6(X0)
| cminus8(X0)
| cplus4(X0) ),
inference(cnf,[status(esa)],[axiom_11]) ).
cnf(l1369,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus6(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1412,plain,
( ~ cplus6(i2003_11_14_17_20_46476)
| ~ cminus6(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l1740,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus5(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l1324,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cplus9(i2003_11_14_17_20_46476)
| cplus7(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l1720,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus5(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cminus7(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[28]) ).
cnf(l1752,plain,
( ~ cminus8(i2003_11_14_17_20_46476)
| ~ cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l1596,plain,
( ~ cminus4(i2003_11_14_17_20_46476)
| ~ cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l1365,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus1(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l1759,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l1417,plain,
( ~ cminus8(i2003_11_14_17_20_46476)
| ~ cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l1381,plain,
( ~ cminus4(i2003_11_14_17_20_46476)
| ~ cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l1271,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l1544,plain,
( ~ cplus9(i2003_11_14_17_20_46476)
| ~ cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l1742,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cplus9(i2003_11_14_17_20_46476)
| cplus7(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[36]) ).
cnf(l89,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus7(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[8]) ).
fof(axiom_14,plain,
! [X] :
( cTest(X)
=> ( cminus4(X)
| cplus2(X)
| cplus1(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_14) ).
cnf(16,plain,
( ~ cTest(X0)
| cminus4(X0)
| cplus1(X0)
| cplus2(X0) ),
inference(cnf,[status(esa)],[axiom_14]) ).
cnf(l1600,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cplus1(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l1771,plain,
( ~ cminus4(i2003_11_14_17_20_46476)
| ~ cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l1793,plain,
( ~ cminus4(i2003_11_14_17_20_46476)
| ~ cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l1549,plain,
( ~ cminus3(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l1797,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l1384,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l1649,plain,
( ~ cminus2(i2003_11_14_17_20_46476)
| ~ cplus2(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l90,plain,
( ~ cminus8(i2003_11_14_17_20_46476)
| ~ cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l1741,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l1674,plain,
( ~ cplus1(i2003_11_14_17_20_46476)
| ~ cminus1(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l1329,plain,
( ~ cminus4(i2003_11_14_17_20_46476)
| ~ cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l1401,plain,
( ~ cminus8(i2003_11_14_17_20_46476)
| ~ cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l1571,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476)
| cplus5(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[17]) ).
cnf(l1764,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus1(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l1547,plain,
( ~ cminus4(i2003_11_14_17_20_46476)
| ~ cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l1595,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus9(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l1768,plain,
( ~ cplus7(i2003_11_14_17_20_46476)
| ~ cminus7(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[53]) ).
fof(axiom_4,plain,
! [X] :
( cTest(X)
=> ( cminus3(X)
| cplus7(X)
| cplus8(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_4) ).
cnf(6,plain,
( ~ cTest(X0)
| cminus3(X0)
| cplus7(X0)
| cplus8(X0) ),
inference(cnf,[status(esa)],[axiom_4]) ).
cnf(l1349,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476)
| cplus7(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1862,plain,
( ~ cminus4(i2003_11_14_17_20_46476)
| ~ cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[52]) ).
fof(axiom_25,plain,
! [X] :
( cTest(X)
=> ( cplus3(X)
| cplus4(X)
| cplus9(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_25) ).
cnf(27,plain,
( ~ cTest(X0)
| cplus9(X0)
| cplus3(X0)
| cplus4(X0) ),
inference(cnf,[status(esa)],[axiom_25]) ).
cnf(l1332,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus9(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1560,plain,
( ~ cminus4(i2003_11_14_17_20_46476)
| ~ cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l152,plain,
( ~ cplus7(i2003_11_14_17_20_46476)
| ~ cminus7(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l1765,plain,
( ~ cplus1(i2003_11_14_17_20_46476)
| ~ cminus1(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l1749,plain,
( ~ cminus4(i2003_11_14_17_20_46476)
| ~ cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l1575,plain,
( ~ cminus3(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l1561,plain,
( ~ cminus3(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[54]) ).
fof(axiom_12,plain,
! [X] :
( cTest(X)
=> ( cminus1(X)
| cminus4(X)
| cplus6(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_12) ).
cnf(14,plain,
( ~ cTest(X0)
| cminus4(X0)
| cplus6(X0)
| cminus1(X0) ),
inference(cnf,[status(esa)],[axiom_12]) ).
cnf(l1805,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cplus6(i2003_11_14_17_20_46476)
| cminus1(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l1751,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus1(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l1736,plain,
( ~ cplus9(i2003_11_14_17_20_46476)
| ~ cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l1770,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus1(i2003_11_14_17_20_46476)
| cplus7(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(l47,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476)
| cplus7(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l1654,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l1788,plain,
( ~ cplus1(i2003_11_14_17_20_46476)
| ~ cminus1(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l1569,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l1572,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus5(i2003_11_14_17_20_46476)
| cplus7(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l1574,plain,
( ~ cminus8(i2003_11_14_17_20_46476)
| ~ cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l1655,plain,
( ~ cminus2(i2003_11_14_17_20_46476)
| ~ cplus2(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l1553,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus1(i2003_11_14_17_20_46476)
| cplus7(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[43]) ).
cnf(l1337,plain,
( ~ cplus9(i2003_11_14_17_20_46476)
| ~ cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[51]) ).
fof(axiom_43,plain,
! [X] :
( cTest(X)
=> ( cminus9(X)
| cplus1(X)
| cminus6(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_43) ).
cnf(45,plain,
( ~ cTest(X0)
| cplus1(X0)
| cminus6(X0)
| cminus9(X0) ),
inference(cnf,[status(esa)],[axiom_43]) ).
cnf(l1738,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus1(i2003_11_14_17_20_46476)
| cminus6(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[45]) ).
fof(axiom_17,plain,
! [X] :
( cTest(X)
=> ( cplus3(X)
| cplus4(X)
| cplus1(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_17) ).
cnf(19,plain,
( ~ cTest(X0)
| cplus1(X0)
| cplus3(X0)
| cplus4(X0) ),
inference(cnf,[status(esa)],[axiom_17]) ).
cnf(l1865,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus1(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[19]) ).
cnf(l1651,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l1888,plain,
( ~ cminus4(i2003_11_14_17_20_46476)
| ~ cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l1500,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l1606,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus9(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l1645,plain,
( ~ cminus5(i2003_11_14_17_20_46476)
| ~ cplus5(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[55]) ).
cnf(l1811,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l1659,plain,
( ~ cminus3(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l1804,plain,
( ~ cminus8(i2003_11_14_17_20_46476)
| ~ cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l1646,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus9(i2003_11_14_17_20_46476)
| cplus5(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1351,plain,
( ~ cplus7(i2003_11_14_17_20_46476)
| ~ cminus7(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l1355,plain,
( ~ cminus3(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l1626,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[37]) ).
cnf(l293,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus9(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l1413,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus1(i2003_11_14_17_20_46476)
| cminus6(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[21]) ).
cnf(l1843,plain,
( ~ cplus9(i2003_11_14_17_20_46476)
| ~ cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l1591,plain,
( ~ cplus1(i2003_11_14_17_20_46476)
| ~ cminus1(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l1356,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l1573,plain,
( ~ cminus2(i2003_11_14_17_20_46476)
| ~ cplus2(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l1554,plain,
( ~ cplus1(i2003_11_14_17_20_46476)
| ~ cminus1(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l1558,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus1(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l1597,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus1(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l129,plain,
( ~ cplus7(i2003_11_14_17_20_46476)
| ~ cminus7(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l1616,plain,
( ~ cminus2(i2003_11_14_17_20_46476)
| ~ cplus2(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l1866,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l1416,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l1791,plain,
( ~ cplus6(i2003_11_14_17_20_46476)
| ~ cminus6(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l1900,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus6(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[13]) ).
fof(axiom_39,plain,
! [X] :
( cTest(X)
=> ( cminus2(X)
| cplus3(X)
| cminus8(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_39) ).
cnf(41,plain,
( ~ cTest(X0)
| cminus2(X0)
| cplus3(X0)
| cminus8(X0) ),
inference(cnf,[status(esa)],[axiom_39]) ).
cnf(l1719,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l1352,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus7(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1806,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus7(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1816,plain,
( ~ cminus3(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l1844,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l1790,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus1(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l1628,plain,
( ~ cminus2(i2003_11_14_17_20_46476)
| ~ cplus2(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l1346,plain,
( ~ cminus4(i2003_11_14_17_20_46476)
| ~ cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l1615,plain,
( ~ cminus4(i2003_11_14_17_20_46476)
| ~ cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l1737,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476)
| cminus7(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l1812,plain,
( ~ cplus7(i2003_11_14_17_20_46476)
| ~ cminus7(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l1362,plain,
( ~ cminus4(i2003_11_14_17_20_46476)
| ~ cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l1385,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus9(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1652,plain,
( ~ cplus9(i2003_11_14_17_20_46476)
| ~ cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l1726,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[41]) ).
cnf(l1666,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus9(i2003_11_14_17_20_46476)
| cplus5(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1946,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476)
| cplus7(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1949,plain,
( ~ cplus7(i2003_11_14_17_20_46476)
| ~ cminus7(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l1363,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[47]) ).
cnf(l1975,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus6(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476)
| cminus7(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[24]) ).
cnf(l1672,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus9(i2003_11_14_17_20_46476)
| cplus5(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[15]) ).
cnf(l1814,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476)
| cplus7(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[6]) ).
cnf(l1372,plain,
( ~ cminus3(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l1327,plain,
( ~ cplus7(i2003_11_14_17_20_46476)
| ~ cminus7(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[53]) ).
cnf(l1510,plain,
( ~ cminus3(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l1772,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus9(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[27]) ).
cnf(l1892,plain,
( ~ cplus9(i2003_11_14_17_20_46476)
| ~ cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l1374,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l348,plain,
( ~ cplus9(i2003_11_14_17_20_46476)
| ~ cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l1884,plain,
( ~ cplus1(i2003_11_14_17_20_46476)
| ~ cminus1(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l1893,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l1976,plain,
( ~ cminus2(i2003_11_14_17_20_46476)
| ~ cplus2(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l1886,plain,
( ~ cminus2(i2003_11_14_17_20_46476)
| ~ cplus2(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l1885,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus1(i2003_11_14_17_20_46476)
| cminus6(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l1820,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l1821,plain,
( ~ cminus8(i2003_11_14_17_20_46476)
| ~ cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l1978,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[22]) ).
cnf(l131,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476)
| cminus7(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l1758,plain,
( ~ cplus1(i2003_11_14_17_20_46476)
| ~ cminus1(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l1611,plain,
( ~ cplus9(i2003_11_14_17_20_46476)
| ~ cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l1883,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus1(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l1890,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cplus1(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[16]) ).
cnf(l1823,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus5(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l351,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus1(i2003_11_14_17_20_46476)
| cminus6(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l1841,plain,
( ~ cplus6(i2003_11_14_17_20_46476)
| ~ cminus6(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[58]) ).
cnf(l1582,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476)
| cminus7(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l1845,plain,
( ~ cplus1(i2003_11_14_17_20_46476)
| ~ cminus1(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l1870,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus1(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[38]) ).
fof(axiom_18,plain,
! [X] :
( cTest(X)
=> ( cminus2(X)
| cplus6(X)
| cplus9(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_18) ).
cnf(20,plain,
( ~ cTest(X0)
| cplus9(X0)
| cplus6(X0)
| cminus2(X0) ),
inference(cnf,[status(esa)],[axiom_18]) ).
cnf(l1904,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus9(i2003_11_14_17_20_46476)
| cplus6(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[20]) ).
cnf(l1789,plain,
( ~ cminus3(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l1948,plain,
( ~ cminus3(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l1918,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus7(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1618,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l1911,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[30]) ).
cnf(l1673,plain,
( ~ cminus3(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[54]) ).
cnf(l1694,plain,
( ~ cminus4(i2003_11_14_17_20_46476)
| ~ cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[52]) ).
cnf(l1787,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cminus1(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[38]) ).
cnf(l1868,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus9(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l1891,plain,
( ~ cminus8(i2003_11_14_17_20_46476)
| ~ cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l1853,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus6(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[13]) ).
cnf(l1899,plain,
( ~ cplus1(i2003_11_14_17_20_46476)
| ~ cminus1(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[57]) ).
cnf(l1988,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus7(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1901,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus1(i2003_11_14_17_20_46476)
| cminus6(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[21]) ).
fof(axiom_38,plain,
! [X] :
( cTest(X)
=> ( cplus3(X)
| cplus4(X)
| cplus6(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_38) ).
cnf(40,plain,
( ~ cTest(X0)
| cplus6(X0)
| cplus3(X0)
| cplus4(X0) ),
inference(cnf,[status(esa)],[axiom_38]) ).
cnf(l1951,plain,
( ~ cTest(i2003_11_14_17_20_46476)
| cplus6(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476) ),
inference(instantiation,[status(thm)],[40]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l4,l5,l388,l1306,l1307,l1308,l6,l9,l1309,l7,l16,l1310,l1311,l2,l1312,l12,l1315,l1316,l1313,l1317,l1318,l851,l17,l1314,l1322,l15,l1319,l1334,l1338,l1321,l8,l1328,l1325,l1366,l1348,l10,l11,l1323,l880,l1361,l1320,l1331,l26,l28,l1371,l1339,l891,l1330,l1389,l1343,l1375,l1360,l74,l1347,l1386,l1358,l894,l1364,l1528,l1368,l1529,l1353,l1523,l1533,l1548,l1391,l1400,l1543,l1526,l33,l1373,l34,l1376,l1440,l1344,l1562,l37,l1012,l1419,l1630,l1345,l1369,l1412,l1740,l1324,l1720,l1752,l1596,l1365,l1759,l1417,l1381,l1271,l1544,l1742,l89,l1600,l1771,l1793,l1549,l1797,l1384,l1649,l90,l1741,l1674,l1329,l1401,l1571,l1764,l1547,l1595,l1768,l1349,l1862,l1332,l1560,l152,l1765,l1749,l1575,l1561,l1805,l1751,l1736,l1770,l47,l1654,l1788,l1569,l1572,l1574,l1655,l1553,l1337,l1738,l1865,l1651,l1888,l1500,l1606,l1645,l1811,l1659,l1804,l1646,l1351,l1355,l1626,l293,l1413,l1843,l1591,l1356,l1573,l1554,l1558,l1597,l129,l1616,l1866,l1416,l1791,l1900,l1719,l1352,l1806,l1816,l1844,l1790,l1628,l1346,l1615,l1737,l1812,l1362,l1385,l1652,l1726,l1666,l1946,l1949,l1363,l1975,l1672,l1814,l1372,l1327,l1510,l1772,l1892,l1374,l348,l1884,l1893,l1976,l1886,l1885,l1820,l1821,l1978,l131,l1758,l1611,l1883,l1890,l1823,l351,l1841,l1582,l1845,l1870,l1904,l1789,l1948,l1918,l1618,l1911,l1673,l1694,l1787,l1868,l1891,l1853,l1899,l1988,l1901,l1951]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : KRS103+1 : TPTP v9.0.0. Released v3.1.0.
% 0.11/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.34 % Computer : n017.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % 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 : Sun Jul 20 22:12:19 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.13/0.34 % launching worker at depth: 4
% 0.13/0.34 % launching worker at depth: 3
% 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: 5
% 0.13/0.34 % launching worker at depth: 6
% 0.13/0.34 % launching worker at depth: 7
% 0.13/0.34 % launching worker at depth: 8
% 0.13/0.35 % launching worker at depth: 9
% 0.13/0.35 % launching worker at depth: 10
% 0.13/0.35 % launching worker at depth: 11
% 0.13/0.35 % launching worker at depth: 12
% 0.13/0.38 % launching worker at depth: 13
% 0.13/0.40 % launching worker at depth: 14
% 0.20/0.51 % launching worker at depth: 15
% 1.96/0.58 % launching worker at depth: 16
% 7.17/1.23 % launching worker at depth: 17
% 9.15/1.49 % SZS status Theorem for theBenchmark
% 9.15/1.49 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------