%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : KRS103+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:46:02 AM UTC 2026
% Result : Unsatisfiable 0.10s 0.39s
% Output : CNFRefutation 0.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 24
% Syntax : Number of formulae : 128 ( 9 unt; 0 def)
% Number of atoms : 391 ( 0 equ)
% Maximal formula atoms : 6 ( 3 avg)
% Number of connectives : 391 ( 128 ~; 240 |; 8 &)
% ( 0 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 18 ( 17 usr; 1 prp; 0-1 aty)
% Number of functors : 1 ( 1 usr; 1 con; 0-0 aty)
% Number of variables : 46 ( 0 sgn 23 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_3,axiom,
! [X] :
( cTest(X)
=> ( cminus8(X)
| cminus5(X)
| cminus3(X) ) ),
file('theBenchmark.p',axiom_3) ).
fof(axiom_4,axiom,
! [X] :
( cTest(X)
=> ( cplus8(X)
| cplus7(X)
| cminus3(X) ) ),
file('theBenchmark.p',axiom_4) ).
fof(axiom_6,axiom,
! [X] :
( cTest(X)
=> ( cplus8(X)
| cminus7(X)
| cplus3(X) ) ),
file('theBenchmark.p',axiom_6) ).
fof(axiom_9,axiom,
! [X] :
( cTest(X)
=> ( cminus8(X)
| cminus4(X)
| cminus9(X) ) ),
file('theBenchmark.p',axiom_9) ).
fof(axiom_15,axiom,
! [X] :
( cTest(X)
=> ( cminus8(X)
| cplus5(X)
| cminus3(X) ) ),
file('theBenchmark.p',axiom_15) ).
fof(axiom_20,axiom,
! [X] :
( cTest(X)
=> ( cplus8(X)
| cplus2(X)
| cminus3(X) ) ),
file('theBenchmark.p',axiom_20) ).
fof(axiom_21,axiom,
! [X] :
( cTest(X)
=> ( cminus6(X)
| cplus4(X)
| cminus2(X) ) ),
file('theBenchmark.p',axiom_21) ).
fof(axiom_22,axiom,
! [X] :
( cTest(X)
=> ( cminus7(X)
| cplus6(X)
| cminus2(X) ) ),
file('theBenchmark.p',axiom_22) ).
fof(axiom_25,axiom,
! [X] :
( cTest(X)
=> ( cplus9(X)
| cplus4(X)
| cplus3(X) ) ),
file('theBenchmark.p',axiom_25) ).
fof(axiom_28,axiom,
! [X] :
( cTest(X)
=> ( cplus4(X)
| cplus3(X)
| cminus9(X) ) ),
file('theBenchmark.p',axiom_28) ).
fof(axiom_29,axiom,
! [X] :
( cTest(X)
=> ( cminus7(X)
| cminus3(X)
| cminus4(X) ) ),
file('theBenchmark.p',axiom_29) ).
fof(axiom_32,axiom,
! [X] :
( cTest(X)
=> ( cplus9(X)
| cminus8(X)
| cplus3(X) ) ),
file('theBenchmark.p',axiom_32) ).
fof(axiom_34,axiom,
! [X] :
( cTest(X)
=> ( cplus7(X)
| cplus9(X)
| cminus4(X) ) ),
file('theBenchmark.p',axiom_34) ).
fof(axiom_35,axiom,
! [X] :
( cTest(X)
=> ( cplus3(X)
| cminus2(X)
| cminus9(X) ) ),
file('theBenchmark.p',axiom_35) ).
fof(axiom_45,axiom,
! [X] :
( cTest(X)
=> ( cplus8(X)
| cplus2(X)
| cminus4(X) ) ),
file('theBenchmark.p',axiom_45) ).
fof(axiom_48,axiom,
! [X] :
~ ( cplus8(X)
& cminus8(X) ),
file('theBenchmark.p',axiom_48) ).
fof(axiom_49,axiom,
! [X] :
~ ( cplus9(X)
& cminus9(X) ),
file('theBenchmark.p',axiom_49) ).
fof(axiom_50,axiom,
! [X] :
~ ( cminus4(X)
& cplus4(X) ),
file('theBenchmark.p',axiom_50) ).
fof(axiom_51,axiom,
! [X] :
~ ( cplus7(X)
& cminus7(X) ),
file('theBenchmark.p',axiom_51) ).
fof(axiom_52,axiom,
! [X] :
~ ( cminus3(X)
& cplus3(X) ),
file('theBenchmark.p',axiom_52) ).
fof(axiom_53,axiom,
! [X] :
~ ( cminus5(X)
& cplus5(X) ),
file('theBenchmark.p',axiom_53) ).
fof(axiom_54,axiom,
! [X] :
~ ( cplus2(X)
& cminus2(X) ),
file('theBenchmark.p',axiom_54) ).
fof(axiom_56,axiom,
! [X] :
~ ( cminus6(X)
& cplus6(X) ),
file('theBenchmark.p',axiom_56) ).
fof(axiom_47,axiom,
cTest(i2003_11_14_17_20_46476),
file('theBenchmark.p',axiom_47) ).
cnf(c_60,plain,
cTest(i2003_11_14_17_20_46476),
inference(clausify,[status(thm)],[axiom_47]) ).
cnf(c_61,plain,
( cplus8(A)
| cplus2(A)
| cminus4(A)
| ~ cTest(A) ),
inference(clausify,[status(thm)],[axiom_45]) ).
cnf(c_71,plain,
( cplus3(A)
| cminus2(A)
| cminus9(A)
| ~ cTest(A) ),
inference(clausify,[status(thm)],[axiom_35]) ).
cnf(c_72,plain,
( cplus7(A)
| cplus9(A)
| cminus4(A)
| ~ cTest(A) ),
inference(clausify,[status(thm)],[axiom_34]) ).
cnf(c_74,plain,
( cplus9(A)
| cminus8(A)
| cplus3(A)
| ~ cTest(A) ),
inference(clausify,[status(thm)],[axiom_32]) ).
cnf(c_77,plain,
( cminus7(A)
| cminus3(A)
| cminus4(A)
| ~ cTest(A) ),
inference(clausify,[status(thm)],[axiom_29]) ).
cnf(c_78,plain,
( cplus4(A)
| cplus3(A)
| cminus9(A)
| ~ cTest(A) ),
inference(clausify,[status(thm)],[axiom_28]) ).
cnf(c_81,plain,
( cplus9(A)
| cplus4(A)
| cplus3(A)
| ~ cTest(A) ),
inference(clausify,[status(thm)],[axiom_25]) ).
cnf(c_84,plain,
( cminus7(A)
| cplus6(A)
| cminus2(A)
| ~ cTest(A) ),
inference(clausify,[status(thm)],[axiom_22]) ).
cnf(c_85,plain,
( cminus6(A)
| cplus4(A)
| cminus2(A)
| ~ cTest(A) ),
inference(clausify,[status(thm)],[axiom_21]) ).
cnf(c_86,plain,
( cplus8(A)
| cplus2(A)
| cminus3(A)
| ~ cTest(A) ),
inference(clausify,[status(thm)],[axiom_20]) ).
cnf(c_91,plain,
( cminus8(A)
| cplus5(A)
| cminus3(A)
| ~ cTest(A) ),
inference(clausify,[status(thm)],[axiom_15]) ).
cnf(c_97,plain,
( cminus8(A)
| cminus4(A)
| cminus9(A)
| ~ cTest(A) ),
inference(clausify,[status(thm)],[axiom_9]) ).
cnf(c_100,plain,
( cplus8(A)
| cminus7(A)
| cplus3(A)
| ~ cTest(A) ),
inference(clausify,[status(thm)],[axiom_6]) ).
cnf(c_102,plain,
( cplus8(A)
| cplus7(A)
| cminus3(A)
| ~ cTest(A) ),
inference(clausify,[status(thm)],[axiom_4]) ).
cnf(c_103,plain,
( cminus8(A)
| cminus5(A)
| cminus3(A)
| ~ cTest(A) ),
inference(clausify,[status(thm)],[axiom_3]) ).
cnf(c_115,plain,
( ~ cplus9(A)
| ~ cminus9(A) ),
inference(clausify,[status(thm)],[axiom_49]) ).
cnf(c_118,plain,
( cplus7(i2003_11_14_17_20_46476)
| cplus9(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_72,c_60]) ).
cnf(c_119,plain,
( cplus9(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_74,c_60]) ).
cnf(c_121,plain,
( cplus9(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_81,c_60]) ).
cnf(c_127,plain,
( ~ cminus6(A)
| ~ cplus6(A) ),
inference(clausify,[status(thm)],[axiom_56]) ).
cnf(c_128,plain,
( cminus6(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_85,c_60]) ).
cnf(c_134,plain,
( ~ cminus3(A)
| ~ cplus3(A) ),
inference(clausify,[status(thm)],[axiom_52]) ).
cnf(c_137,plain,
( cminus7(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_77,c_60]) ).
cnf(c_138,plain,
( cplus8(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_86,c_60]) ).
cnf(c_139,plain,
( cminus8(i2003_11_14_17_20_46476)
| cplus5(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_91,c_60]) ).
cnf(c_140,plain,
( cplus8(i2003_11_14_17_20_46476)
| cplus7(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_102,c_60]) ).
cnf(c_141,plain,
( cminus8(i2003_11_14_17_20_46476)
| cminus5(i2003_11_14_17_20_46476)
| cminus3(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_103,c_60]) ).
cnf(c_142,plain,
( ~ cminus5(A)
| ~ cplus5(A) ),
inference(clausify,[status(thm)],[axiom_53]) ).
cnf(c_148,plain,
( ~ cplus3(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476)
| cminus5(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_141,c_134]) ).
cnf(c_149,plain,
( ~ cplus8(A)
| ~ cminus8(A) ),
inference(clausify,[status(thm)],[axiom_48]) ).
cnf(c_150,plain,
( ~ cplus3(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476)
| ~ cplus5(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_142,c_148]) ).
cnf(c_154,plain,
( cminus8(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_97,c_60]) ).
cnf(c_155,plain,
( ~ cminus9(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_119,c_115]) ).
cnf(c_157,plain,
( ~ cplus3(i2003_11_14_17_20_46476)
| cminus8(i2003_11_14_17_20_46476)
| cplus5(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_139,c_134]) ).
cnf(c_158,plain,
( ~ cplus7(A)
| ~ cminus7(A) ),
inference(clausify,[status(thm)],[axiom_51]) ).
cnf(c_160,plain,
( ~ cminus9(i2003_11_14_17_20_46476)
| cplus7(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_118,c_115]) ).
cnf(c_161,plain,
( ~ cplus3(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476)
| cplus7(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_140,c_134]) ).
cnf(c_164,plain,
( ~ cplus3(i2003_11_14_17_20_46476)
| ~ cplus5(i2003_11_14_17_20_46476)
| ~ cplus8(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_149,c_150]) ).
cnf(c_165,plain,
( ~ cplus3(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_138,c_134]) ).
cnf(c_167,plain,
( cplus8(i2003_11_14_17_20_46476)
| cminus7(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_100,c_60]) ).
cnf(c_168,plain,
( cplus8(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_61,c_60]) ).
cnf(c_169,plain,
( ~ cplus3(i2003_11_14_17_20_46476)
| cplus8(i2003_11_14_17_20_46476)
| ~ cminus7(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_158,c_161]) ).
cnf(c_174,plain,
( ~ cplus8(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_154,c_149]) ).
cnf(c_175,plain,
( ~ cplus8(i2003_11_14_17_20_46476)
| ~ cminus9(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_155,c_149]) ).
cnf(c_177,plain,
( ~ cplus8(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476)
| cplus5(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_157,c_149]) ).
cnf(c_179,plain,
( ~ cplus3(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476)
| cplus5(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_177,c_165]) ).
cnf(c_181,plain,
( ~ cplus3(i2003_11_14_17_20_46476)
| ~ cminus7(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476)
| cplus5(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_177,c_169]) ).
cnf(c_186,plain,
( ~ cplus3(i2003_11_14_17_20_46476)
| ~ cminus7(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476)
| ~ cplus5(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_164,c_169]) ).
cnf(c_188,plain,
( ~ cplus3(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476)
| ~ cplus5(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_164,c_165]) ).
cnf(c_196,plain,
( ~ cminus4(A)
| ~ cplus4(A) ),
inference(clausify,[status(thm)],[axiom_50]) ).
cnf(c_198,plain,
( cplus4(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476)
| ~ cplus6(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_127,c_128]) ).
cnf(c_207,plain,
( cplus4(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_78,c_60]) ).
cnf(c_208,plain,
( ~ cminus9(i2003_11_14_17_20_46476)
| cplus4(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_121,c_115]) ).
cnf(c_223,plain,
( ~ cplus2(A)
| ~ cminus2(A) ),
inference(clausify,[status(thm)],[axiom_54]) ).
cnf(c_228,plain,
( cplus3(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_71,c_60]) ).
cnf(c_229,plain,
( cminus7(i2003_11_14_17_20_46476)
| cplus6(i2003_11_14_17_20_46476)
| cminus2(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_84,c_60]) ).
cnf(c_234,plain,
( cminus2(i2003_11_14_17_20_46476)
| ~ cplus6(i2003_11_14_17_20_46476)
| ~ cminus4(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_196,c_198]) ).
cnf(c_235,plain,
( ~ cplus2(i2003_11_14_17_20_46476)
| ~ cplus6(i2003_11_14_17_20_46476)
| ~ cminus4(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_234,c_223]) ).
cnf(c_240,plain,
( ~ cplus2(i2003_11_14_17_20_46476)
| cminus7(i2003_11_14_17_20_46476)
| cplus6(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_229,c_223]) ).
cnf(c_241,plain,
( ~ cplus2(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_228,c_223]) ).
cnf(c_245,plain,
( ~ cminus4(i2003_11_14_17_20_46476)
| ~ cminus9(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_208,c_196]) ).
cnf(c_246,plain,
( ~ cminus4(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_207,c_196]) ).
cnf(c_255,plain,
( cminus7(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| ~ cminus9(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_175,c_167]) ).
cnf(c_256,plain,
( cminus7(i2003_11_14_17_20_46476)
| ~ cminus9(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476) ),
inference(copy,[status(thm)],[c_255]) ).
cnf(c_258,plain,
( cplus2(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_174,c_168]) ).
cnf(c_259,plain,
( cplus2(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(copy,[status(thm)],[c_258]) ).
cnf(c_268,plain,
( ~ cplus3(i2003_11_14_17_20_46476)
| cminus7(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_137,c_134]) ).
cnf(c_272,plain,
( ~ cminus9(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| ~ cminus7(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_158,c_160]) ).
cnf(c_275,plain,
( ~ cplus3(i2003_11_14_17_20_46476)
| ~ cminus7(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476)
| ~ cminus7(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_186,c_181]) ).
cnf(c_325,plain,
( ~ cplus3(i2003_11_14_17_20_46476)
| ~ cminus7(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476)
| ~ cminus7(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476) ),
inference(copy,[status(thm)],[c_275]) ).
cnf(c_326,plain,
( ~ cplus3(i2003_11_14_17_20_46476)
| ~ cminus7(i2003_11_14_17_20_46476)
| ~ cminus7(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476) ),
inference(copy,[status(thm)],[c_325]) ).
cnf(c_327,plain,
( ~ cplus3(i2003_11_14_17_20_46476)
| ~ cminus7(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476) ),
inference(copy,[status(thm)],[c_326]) ).
cnf(c_276,plain,
( ~ cminus7(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476) ),
inference(copy,[status(thm)],[c_327]) ).
cnf(c_277,plain,
( ~ cplus3(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_188,c_179]) ).
cnf(c_328,plain,
( ~ cplus3(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476) ),
inference(copy,[status(thm)],[c_277]) ).
cnf(c_329,plain,
( ~ cplus3(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476) ),
inference(copy,[status(thm)],[c_328]) ).
cnf(c_330,plain,
( ~ cplus3(i2003_11_14_17_20_46476)
| cplus2(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476) ),
inference(copy,[status(thm)],[c_329]) ).
cnf(c_278,plain,
( cplus2(i2003_11_14_17_20_46476)
| ~ cplus3(i2003_11_14_17_20_46476) ),
inference(copy,[status(thm)],[c_330]) ).
cnf(c_331,plain,
( cplus3(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_259,c_241]) ).
cnf(c_295,plain,
( cplus3(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(copy,[status(thm)],[c_331]) ).
cnf(c_332,plain,
( cminus7(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_295,c_256]) ).
cnf(c_298,plain,
( cminus7(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476) ),
inference(copy,[status(thm)],[c_332]) ).
cnf(c_333,plain,
( ~ cminus9(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_298,c_272]) ).
cnf(c_300,plain,
( ~ cminus9(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476) ),
inference(copy,[status(thm)],[c_333]) ).
cnf(c_334,plain,
( cplus3(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_300,c_295]) ).
cnf(c_335,plain,
( cplus3(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476) ),
inference(copy,[status(thm)],[c_334]) ).
cnf(c_301,plain,
( cplus3(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476) ),
inference(copy,[status(thm)],[c_335]) ).
cnf(c_336,plain,
( cminus7(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_301,c_268]) ).
cnf(c_304,plain,
( cminus7(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476) ),
inference(copy,[status(thm)],[c_336]) ).
cnf(c_305,plain,
( ~ cplus3(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_304,c_276]) ).
cnf(c_337,plain,
( cminus4(i2003_11_14_17_20_46476)
| cminus4(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_305,c_301]) ).
cnf(c_308,plain,
cminus4(i2003_11_14_17_20_46476),
inference(copy,[status(thm)],[c_337]) ).
cnf(c_315,plain,
( cplus3(i2003_11_14_17_20_46476)
| cminus9(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_308,c_246]) ).
cnf(c_316,plain,
( ~ cminus9(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_308,c_245]) ).
cnf(c_317,plain,
( ~ cplus2(i2003_11_14_17_20_46476)
| ~ cplus6(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_308,c_235]) ).
cnf(c_338,plain,
( cplus3(i2003_11_14_17_20_46476)
| cplus3(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_316,c_315]) ).
cnf(c_320,plain,
cplus3(i2003_11_14_17_20_46476),
inference(copy,[status(thm)],[c_338]) ).
cnf(c_321,plain,
cplus2(i2003_11_14_17_20_46476),
inference(resolve,[status(thm)],[c_320,c_278]) ).
cnf(c_322,plain,
~ cminus7(i2003_11_14_17_20_46476),
inference(resolve,[status(thm)],[c_320,c_276]) ).
cnf(c_323,plain,
~ cplus6(i2003_11_14_17_20_46476),
inference(resolve,[status(thm)],[c_321,c_317]) ).
cnf(c_339,plain,
( ~ cplus2(i2003_11_14_17_20_46476)
| cminus7(i2003_11_14_17_20_46476) ),
inference(resolve,[status(thm)],[c_323,c_240]) ).
cnf(c_340,plain,
~ cplus2(i2003_11_14_17_20_46476),
inference(resolve,[status(thm)],[c_322,c_339]) ).
cnf(c_324,plain,
$false,
inference(resolve,[status(thm)],[c_321,c_340]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS103+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n009.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 19:39:29 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.36 % Process 2368410 was started by sandbox on n009,
% 0.10/0.36 % Fri Sep 25 19:39:29 2026
% 0.10/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.37
% 0.10/0.37 % From the command line: assign(max_seconds, 300).
% 0.10/0.39
% 0.10/0.39 % SZS status Unsatisfiable for theBenchmark
% 0.10/0.39
% 0.10/0.39 % Proof 1 at 0.01 (+ 0.00) seconds.
% 0.10/0.39 % Length of proof is 111.
% 0.10/0.39 % Level of proof is 17.
% 0.10/0.39 % Maximum clause weight is 6.000.
% 0.10/0.39 % Given clauses 50.
% 0.10/0.39
% 0.10/0.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------