%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : KRS041+1 : TPTP v9.2.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n003.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 : Tue May 5 04:36:13 PM UTC 2026
% Result : Satisfiable 1.29s 1.72s
% Output : Saturation 1.29s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_32,axiom,
! [X1] :
( cTest(X1)
=> ( cplus3(X1)
| cplus8(X1)
| cminus6(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_32) ).
fof(axiom_56,axiom,
! [X1] :
~ ( cplus6(X1)
& cminus6(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_56) ).
fof(axiom_47,axiom,
cTest(i2003_11_14_17_16_07145),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_47) ).
fof(axiom_3,axiom,
! [X1] :
( cTest(X1)
=> ( cplus3(X1)
| cplus6(X1)
| cplus7(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_3) ).
fof(axiom_33,axiom,
! [X1] :
( cTest(X1)
=> ( cplus2(X1)
| cminus8(X1)
| cminus9(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_33) ).
fof(axiom_35,axiom,
! [X1] :
( cTest(X1)
=> ( cplus3(X1)
| cminus7(X1)
| cplus8(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_35) ).
fof(axiom_43,axiom,
! [X1] :
( cTest(X1)
=> ( cplus1(X1)
| cplus2(X1)
| cminus8(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_43) ).
fof(axiom_54,axiom,
! [X1] :
~ ( cplus2(X1)
& cminus2(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_54) ).
fof(axiom_28,axiom,
! [X1] :
( cTest(X1)
=> ( cminus3(X1)
| cplus2(X1)
| cminus6(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_28) ).
fof(axiom_9,axiom,
! [X1] :
( cTest(X1)
=> ( cminus3(X1)
| cplus6(X1)
| cplus8(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_9) ).
fof(axiom_51,axiom,
! [X1] :
~ ( cminus7(X1)
& cplus7(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_51) ).
fof(axiom_55,axiom,
! [X1] :
~ ( cplus1(X1)
& cminus1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_55) ).
fof(axiom_34,axiom,
! [X1] :
( cTest(X1)
=> ( cplus3(X1)
| cplus2(X1)
| cminus1(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_34) ).
fof(axiom_12,axiom,
! [X1] :
( cTest(X1)
=> ( cminus8(X1)
| cplus9(X1)
| cminus1(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_12) ).
fof(axiom_23,axiom,
! [X1] :
( cTest(X1)
=> ( cminus8(X1)
| cminus2(X1)
| cminus9(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_23) ).
fof(axiom_52,axiom,
! [X1] :
~ ( cplus3(X1)
& cminus3(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_52) ).
fof(axiom_49,axiom,
! [X1] :
~ ( cplus9(X1)
& cminus9(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_49) ).
fof(axiom_19,axiom,
! [X1] :
( cTest(X1)
=> ( cplus3(X1)
| cminus2(X1)
| cplus7(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_19) ).
fof(axiom_24,axiom,
! [X1] :
( cTest(X1)
=> ( cplus1(X1)
| cplus7(X1)
| cminus6(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_24) ).
fof(axiom_39,axiom,
! [X1] :
( cTest(X1)
=> ( cminus9(X1)
| cminus1(X1)
| cplus7(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_39) ).
fof(axiom_41,axiom,
! [X1] :
( cTest(X1)
=> ( cminus3(X1)
| cminus8(X1)
| cplus7(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_41) ).
fof(axiom_48,axiom,
! [X1] :
~ ( cminus8(X1)
& cplus8(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_48) ).
fof(axiom_16,axiom,
! [X1] :
( cTest(X1)
=> ( cminus2(X1)
| cplus9(X1)
| cminus1(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_16) ).
fof(axiom_20,axiom,
! [X1] :
( cTest(X1)
=> ( cminus3(X1)
| cminus7(X1)
| cminus2(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_20) ).
fof(axiom_25,axiom,
! [X1] :
( cTest(X1)
=> ( cplus3(X1)
| cminus7(X1)
| cminus9(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_25) ).
fof(axiom_38,axiom,
! [X1] :
( cTest(X1)
=> ( cplus3(X1)
| cminus5(X1)
| cminus2(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_38) ).
fof(axiom_10,axiom,
! [X1] :
( cTest(X1)
=> ( cminus3(X1)
| cplus1(X1)
| cplus9(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_10) ).
fof(axiom_53,axiom,
! [X1] :
~ ( cminus5(X1)
& cplus5(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_53) ).
fof(axiom_37,axiom,
! [X1] :
( cTest(X1)
=> ( cminus7(X1)
| cplus2(X1)
| cplus5(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_37) ).
fof(axiom_31,axiom,
! [X1] :
( cTest(X1)
=> ( cplus3(X1)
| cminus2(X1)
| cminus1(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_31) ).
fof(axiom_11,axiom,
! [X1] :
( cTest(X1)
=> ( cminus2(X1)
| cplus6(X1)
| cplus5(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_11) ).
fof(axiom_36,axiom,
! [X1] :
( cTest(X1)
=> ( cminus5(X1)
| cminus8(X1)
| cminus6(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_36) ).
fof(axiom_1,axiom,
! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1) ).
fof(axiom_0,axiom,
! [X1] :
( cowlThing(X1)
& ~ cowlNothing(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_0) ).
fof(axiom_13,axiom,
! [X1] :
( cTest(X1)
=> ( cplus8(X1)
| cminus1(X1)
| cplus5(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_13) ).
fof(axiom_18,axiom,
! [X1] :
( cTest(X1)
=> ( cminus2(X1)
| cminus4(X1)
| cminus9(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_18) ).
fof(axiom_26,axiom,
! [X1] :
( cTest(X1)
=> ( cplus1(X1)
| cminus2(X1)
| cminus9(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_26) ).
fof(axiom_7,axiom,
! [X1] :
( cTest(X1)
=> ( cplus1(X1)
| cminus7(X1)
| cminus5(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_7) ).
fof(axiom_6,axiom,
! [X1] :
( cTest(X1)
=> ( cminus7(X1)
| cminus9(X1)
| cplus5(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_6) ).
fof(axiom_44,axiom,
! [X1] :
( cTest(X1)
=> ( cminus4(X1)
| cplus8(X1)
| cminus6(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_44) ).
fof(axiom_5,axiom,
! [X1] :
( cTest(X1)
=> ( cminus3(X1)
| cminus8(X1)
| cminus6(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_5) ).
fof(axiom_21,axiom,
! [X1] :
( cTest(X1)
=> ( cplus4(X1)
| cplus8(X1)
| cplus5(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_21) ).
fof(axiom_46,axiom,
! [X1] :
( cTest(X1)
=> ( cminus7(X1)
| cplus4(X1)
| cplus8(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_46) ).
fof(axiom_14,axiom,
! [X1] :
( cTest(X1)
=> ( cminus3(X1)
| cminus5(X1)
| cplus4(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_14) ).
fof(axiom_42,axiom,
! [X1] :
( cTest(X1)
=> ( cminus4(X1)
| cminus1(X1)
| cplus7(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_42) ).
fof(axiom_17,axiom,
! [X1] :
( cTest(X1)
=> ( cminus8(X1)
| cminus9(X1)
| cplus7(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_17) ).
fof(axiom_8,axiom,
! [X1] :
( cTest(X1)
=> ( cplus4(X1)
| cminus5(X1)
| cplus7(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_8) ).
fof(axiom_4,axiom,
! [X1] :
( cTest(X1)
=> ( cplus4(X1)
| cminus8(X1)
| cplus7(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_4) ).
fof(axiom_27,axiom,
! [X1] :
( cTest(X1)
=> ( cminus7(X1)
| cplus6(X1)
| cplus5(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_27) ).
fof(axiom_45,axiom,
! [X1] :
( cTest(X1)
=> ( cplus1(X1)
| cplus4(X1)
| cplus6(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_45) ).
fof(axiom_30,axiom,
! [X1] :
( cTest(X1)
=> ( cplus6(X1)
| cminus1(X1)
| cplus7(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_30) ).
fof(axiom_22,axiom,
! [X1] :
( cTest(X1)
=> ( cplus2(X1)
| cplus8(X1)
| cplus5(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_22) ).
fof(axiom_29,axiom,
! [X1] :
( cTest(X1)
=> ( cminus3(X1)
| cplus2(X1)
| cplus7(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_29) ).
fof(axiom_15,axiom,
! [X1] :
( cTest(X1)
=> ( cplus3(X1)
| cminus5(X1)
| cplus8(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_15) ).
fof(axiom_40,axiom,
! [X1] :
( cTest(X1)
=> ( cplus3(X1)
| cplus6(X1)
| cminus9(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_40) ).
fof(axiom_2,axiom,
! [X1] :
( cTest(X1)
=> ( cplus3(X1)
| cplus2(X1)
| cplus6(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2) ).
fof(axiom_50,axiom,
! [X1] :
~ ( cplus4(X1)
& cminus4(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_50) ).
fof(c_0_57,plain,
! [X90] :
( ~ cTest(X90)
| cplus3(X90)
| cplus8(X90)
| cminus6(X90) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_32])]) ).
fof(c_0_58,plain,
! [X113] :
( ~ cplus6(X113)
| ~ cminus6(X113) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_56])]) ).
cnf(c_0_59,plain,
( cplus3(X1)
| cplus8(X1)
| cminus6(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_57]),
[final] ).
cnf(c_0_60,plain,
cTest(i2003_11_14_17_16_07145),
inference(split_conjunct,[status(thm)],[axiom_47]),
[final] ).
fof(c_0_61,plain,
! [X61] :
( ~ cTest(X61)
| cplus3(X61)
| cplus6(X61)
| cplus7(X61) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_3])]) ).
fof(c_0_62,plain,
! [X91] :
( ~ cTest(X91)
| cplus2(X91)
| cminus8(X91)
| cminus9(X91) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_33])]) ).
fof(c_0_63,plain,
! [X93] :
( ~ cTest(X93)
| cplus3(X93)
| cminus7(X93)
| cplus8(X93) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_35])]) ).
cnf(c_0_64,plain,
( ~ cplus6(X1)
| ~ cminus6(X1) ),
inference(split_conjunct,[status(thm)],[c_0_58]),
[final] ).
cnf(c_0_65,plain,
( cplus8(i2003_11_14_17_16_07145)
| cminus6(i2003_11_14_17_16_07145)
| cplus3(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_59,c_0_60]) ).
cnf(c_0_66,plain,
( cplus3(X1)
| cplus6(X1)
| cplus7(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_61]),
[final] ).
fof(c_0_67,plain,
! [X101] :
( ~ cTest(X101)
| cplus1(X101)
| cplus2(X101)
| cminus8(X101) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_43])]) ).
fof(c_0_68,plain,
! [X111] :
( ~ cplus2(X111)
| ~ cminus2(X111) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_54])]) ).
cnf(c_0_69,plain,
( cplus2(X1)
| cminus8(X1)
| cminus9(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_62]),
[final] ).
fof(c_0_70,plain,
! [X86] :
( ~ cTest(X86)
| cminus3(X86)
| cplus2(X86)
| cminus6(X86) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_28])]) ).
fof(c_0_71,plain,
! [X67] :
( ~ cTest(X67)
| cminus3(X67)
| cplus6(X67)
| cplus8(X67) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_9])]) ).
fof(c_0_72,plain,
! [X108] :
( ~ cminus7(X108)
| ~ cplus7(X108) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_51])]) ).
cnf(c_0_73,plain,
( cplus3(X1)
| cminus7(X1)
| cplus8(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_63]),
[final] ).
cnf(c_0_74,plain,
( cplus8(i2003_11_14_17_16_07145)
| cplus3(i2003_11_14_17_16_07145)
| ~ cplus6(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_64,c_0_65]) ).
cnf(c_0_75,plain,
( cplus7(i2003_11_14_17_16_07145)
| cplus6(i2003_11_14_17_16_07145)
| cplus3(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_66,c_0_60]) ).
fof(c_0_76,plain,
! [X112] :
( ~ cplus1(X112)
| ~ cminus1(X112) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_55])]) ).
cnf(c_0_77,plain,
( cplus1(X1)
| cplus2(X1)
| cminus8(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_67]),
[final] ).
fof(c_0_78,plain,
! [X92] :
( ~ cTest(X92)
| cplus3(X92)
| cplus2(X92)
| cminus1(X92) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_34])]) ).
fof(c_0_79,plain,
! [X70] :
( ~ cTest(X70)
| cminus8(X70)
| cplus9(X70)
| cminus1(X70) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_12])]) ).
fof(c_0_80,plain,
! [X81] :
( ~ cTest(X81)
| cminus8(X81)
| cminus2(X81)
| cminus9(X81) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_23])]) ).
cnf(c_0_81,plain,
( ~ cplus2(X1)
| ~ cminus2(X1) ),
inference(split_conjunct,[status(thm)],[c_0_68]),
[final] ).
cnf(c_0_82,plain,
( cminus9(i2003_11_14_17_16_07145)
| cminus8(i2003_11_14_17_16_07145)
| cplus2(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_69,c_0_60]) ).
cnf(c_0_83,plain,
( cminus3(X1)
| cplus2(X1)
| cminus6(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_70]),
[final] ).
fof(c_0_84,plain,
! [X109] :
( ~ cplus3(X109)
| ~ cminus3(X109) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_52])]) ).
cnf(c_0_85,plain,
( cminus3(X1)
| cplus6(X1)
| cplus8(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_71]),
[final] ).
cnf(c_0_86,plain,
( ~ cminus7(X1)
| ~ cplus7(X1) ),
inference(split_conjunct,[status(thm)],[c_0_72]),
[final] ).
cnf(c_0_87,plain,
( cplus8(i2003_11_14_17_16_07145)
| cminus7(i2003_11_14_17_16_07145)
| cplus3(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_73,c_0_60]) ).
cnf(c_0_88,plain,
( cplus8(i2003_11_14_17_16_07145)
| cplus7(i2003_11_14_17_16_07145)
| cplus3(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_74,c_0_75]) ).
cnf(c_0_89,plain,
( ~ cplus1(X1)
| ~ cminus1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_76]),
[final] ).
cnf(c_0_90,plain,
( cplus1(i2003_11_14_17_16_07145)
| cminus8(i2003_11_14_17_16_07145)
| cplus2(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_77,c_0_60]) ).
cnf(c_0_91,plain,
( cplus3(X1)
| cplus2(X1)
| cminus1(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_78]),
[final] ).
fof(c_0_92,plain,
! [X106] :
( ~ cplus9(X106)
| ~ cminus9(X106) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_49])]) ).
cnf(c_0_93,plain,
( cminus8(X1)
| cplus9(X1)
| cminus1(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_79]),
[final] ).
cnf(c_0_94,plain,
( cminus8(X1)
| cminus2(X1)
| cminus9(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_80]),
[final] ).
cnf(c_0_95,plain,
( cminus9(i2003_11_14_17_16_07145)
| cminus8(i2003_11_14_17_16_07145)
| ~ cminus2(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_81,c_0_82]) ).
cnf(c_0_96,plain,
( cminus6(i2003_11_14_17_16_07145)
| cminus3(i2003_11_14_17_16_07145)
| cplus2(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_83,c_0_60]) ).
cnf(c_0_97,plain,
( ~ cplus3(X1)
| ~ cminus3(X1) ),
inference(split_conjunct,[status(thm)],[c_0_84]),
[final] ).
cnf(c_0_98,plain,
( cplus8(i2003_11_14_17_16_07145)
| cminus3(i2003_11_14_17_16_07145)
| cplus6(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_85,c_0_60]) ).
cnf(c_0_99,plain,
( cplus8(i2003_11_14_17_16_07145)
| cplus3(i2003_11_14_17_16_07145) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_86,c_0_87]),c_0_88]) ).
cnf(c_0_100,plain,
( cminus8(i2003_11_14_17_16_07145)
| cplus2(i2003_11_14_17_16_07145)
| ~ cminus1(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_89,c_0_90]) ).
cnf(c_0_101,plain,
( cminus1(i2003_11_14_17_16_07145)
| cplus2(i2003_11_14_17_16_07145)
| cplus3(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_91,c_0_60]) ).
fof(c_0_102,plain,
! [X77] :
( ~ cTest(X77)
| cplus3(X77)
| cminus2(X77)
| cplus7(X77) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_19])]) ).
cnf(c_0_103,plain,
( ~ cplus9(X1)
| ~ cminus9(X1) ),
inference(split_conjunct,[status(thm)],[c_0_92]),
[final] ).
cnf(c_0_104,plain,
( cminus1(i2003_11_14_17_16_07145)
| cplus9(i2003_11_14_17_16_07145)
| cminus8(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_93,c_0_60]) ).
cnf(c_0_105,plain,
( cminus9(i2003_11_14_17_16_07145)
| cminus8(i2003_11_14_17_16_07145) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_94,c_0_60]),c_0_95]) ).
cnf(c_0_106,plain,
( cminus3(i2003_11_14_17_16_07145)
| cplus2(i2003_11_14_17_16_07145)
| ~ cplus6(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_64,c_0_96]) ).
cnf(c_0_107,plain,
( cplus8(i2003_11_14_17_16_07145)
| cplus6(i2003_11_14_17_16_07145) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_97,c_0_98]),c_0_99]) ).
fof(c_0_108,plain,
! [X82] :
( ~ cTest(X82)
| cplus1(X82)
| cplus7(X82)
| cminus6(X82) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_24])]) ).
cnf(c_0_109,plain,
( cminus8(i2003_11_14_17_16_07145)
| cplus2(i2003_11_14_17_16_07145)
| cplus3(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_100,c_0_101]) ).
cnf(c_0_110,plain,
( cplus3(X1)
| cminus2(X1)
| cplus7(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_102]),
[final] ).
cnf(c_0_111,plain,
( cminus1(i2003_11_14_17_16_07145)
| cminus8(i2003_11_14_17_16_07145) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_103,c_0_104]),c_0_105]) ).
cnf(c_0_112,plain,
( cplus8(i2003_11_14_17_16_07145)
| cminus3(i2003_11_14_17_16_07145)
| cplus2(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_106,c_0_107]) ).
cnf(c_0_113,plain,
( cplus1(X1)
| cplus7(X1)
| cminus6(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_108]),
[final] ).
fof(c_0_114,plain,
! [X97] :
( ~ cTest(X97)
| cminus9(X97)
| cminus1(X97)
| cplus7(X97) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_39])]) ).
fof(c_0_115,plain,
! [X99] :
( ~ cTest(X99)
| cminus3(X99)
| cminus8(X99)
| cplus7(X99) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_41])]) ).
fof(c_0_116,plain,
! [X105] :
( ~ cminus8(X105)
| ~ cplus8(X105) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_48])]) ).
cnf(c_0_117,plain,
( cminus8(i2003_11_14_17_16_07145)
| cplus3(i2003_11_14_17_16_07145)
| ~ cminus2(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_81,c_0_109]) ).
cnf(c_0_118,plain,
( cminus2(i2003_11_14_17_16_07145)
| cplus7(i2003_11_14_17_16_07145)
| cplus3(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_110,c_0_60]) ).
cnf(c_0_119,plain,
( cminus8(i2003_11_14_17_16_07145)
| cplus2(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_100,c_0_111]) ).
cnf(c_0_120,plain,
( cplus8(i2003_11_14_17_16_07145)
| cplus2(i2003_11_14_17_16_07145) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_97,c_0_112]),c_0_99]) ).
cnf(c_0_121,plain,
( cplus1(i2003_11_14_17_16_07145)
| cminus6(i2003_11_14_17_16_07145)
| cplus7(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_113,c_0_60]) ).
cnf(c_0_122,plain,
( cminus9(X1)
| cminus1(X1)
| cplus7(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_114]),
[final] ).
cnf(c_0_123,plain,
( cminus3(X1)
| cminus8(X1)
| cplus7(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_115]),
[final] ).
cnf(c_0_124,plain,
( ~ cminus8(X1)
| ~ cplus8(X1) ),
inference(split_conjunct,[status(thm)],[c_0_116]),
[final] ).
cnf(c_0_125,plain,
( cminus8(i2003_11_14_17_16_07145)
| cplus7(i2003_11_14_17_16_07145)
| cplus3(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_117,c_0_118]) ).
fof(c_0_126,plain,
! [X74] :
( ~ cTest(X74)
| cminus2(X74)
| cplus9(X74)
| cminus1(X74) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_16])]) ).
cnf(c_0_127,plain,
( cminus8(i2003_11_14_17_16_07145)
| ~ cminus2(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_81,c_0_119]),
[final] ).
cnf(c_0_128,plain,
( cplus8(i2003_11_14_17_16_07145)
| ~ cminus2(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_81,c_0_120]) ).
cnf(c_0_129,plain,
( cminus6(i2003_11_14_17_16_07145)
| cplus7(i2003_11_14_17_16_07145)
| ~ cminus1(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_89,c_0_121]) ).
cnf(c_0_130,plain,
( cminus1(i2003_11_14_17_16_07145)
| cminus9(i2003_11_14_17_16_07145)
| cplus7(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_122,c_0_60]) ).
cnf(c_0_131,plain,
( cminus3(i2003_11_14_17_16_07145)
| cminus8(i2003_11_14_17_16_07145)
| cplus7(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_123,c_0_60]) ).
cnf(c_0_132,plain,
( cplus7(i2003_11_14_17_16_07145)
| cplus3(i2003_11_14_17_16_07145) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_124,c_0_125]),c_0_99]) ).
cnf(c_0_133,plain,
( cminus2(X1)
| cplus9(X1)
| cminus1(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_126]),
[final] ).
cnf(c_0_134,plain,
~ cminus2(i2003_11_14_17_16_07145),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_124,c_0_127]),c_0_128]),
[final] ).
cnf(c_0_135,plain,
( cminus9(i2003_11_14_17_16_07145)
| cminus6(i2003_11_14_17_16_07145)
| cplus7(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_129,c_0_130]) ).
cnf(c_0_136,plain,
( cminus8(i2003_11_14_17_16_07145)
| cplus7(i2003_11_14_17_16_07145) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_97,c_0_131]),c_0_132]) ).
fof(c_0_137,plain,
! [X78] :
( ~ cTest(X78)
| cminus3(X78)
| cminus7(X78)
| cminus2(X78) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_20])]) ).
cnf(c_0_138,plain,
( cminus1(i2003_11_14_17_16_07145)
| cplus9(i2003_11_14_17_16_07145) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_133,c_0_60]),c_0_134]) ).
cnf(c_0_139,plain,
( cminus9(i2003_11_14_17_16_07145)
| cplus7(i2003_11_14_17_16_07145)
| ~ cplus6(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_64,c_0_135]) ).
cnf(c_0_140,plain,
( cplus7(i2003_11_14_17_16_07145)
| ~ cplus8(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_124,c_0_136]) ).
fof(c_0_141,plain,
! [X83] :
( ~ cTest(X83)
| cplus3(X83)
| cminus7(X83)
| cminus9(X83) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_25])]) ).
fof(c_0_142,plain,
! [X96] :
( ~ cTest(X96)
| cplus3(X96)
| cminus5(X96)
| cminus2(X96) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_38])]) ).
cnf(c_0_143,plain,
( cminus3(X1)
| cminus7(X1)
| cminus2(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_137]),
[final] ).
cnf(c_0_144,plain,
( cminus1(i2003_11_14_17_16_07145)
| ~ cminus9(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_103,c_0_138]) ).
cnf(c_0_145,plain,
( cminus9(i2003_11_14_17_16_07145)
| cplus7(i2003_11_14_17_16_07145) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_139,c_0_107]),c_0_140]) ).
fof(c_0_146,plain,
! [X68] :
( ~ cTest(X68)
| cminus3(X68)
| cplus1(X68)
| cplus9(X68) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_10])]) ).
cnf(c_0_147,plain,
( cplus3(X1)
| cminus7(X1)
| cminus9(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_141]),
[final] ).
fof(c_0_148,plain,
! [X110] :
( ~ cminus5(X110)
| ~ cplus5(X110) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_53])]) ).
cnf(c_0_149,plain,
( cplus3(X1)
| cminus5(X1)
| cminus2(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_142]),
[final] ).
fof(c_0_150,plain,
! [X95] :
( ~ cTest(X95)
| cminus7(X95)
| cplus2(X95)
| cplus5(X95) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_37])]) ).
cnf(c_0_151,plain,
( cminus7(i2003_11_14_17_16_07145)
| cminus3(i2003_11_14_17_16_07145) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_143,c_0_60]),c_0_134]) ).
cnf(c_0_152,plain,
( cminus6(i2003_11_14_17_16_07145)
| cplus7(i2003_11_14_17_16_07145) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_129,c_0_144]),c_0_145]) ).
cnf(c_0_153,plain,
( cminus3(X1)
| cplus1(X1)
| cplus9(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_146]),
[final] ).
cnf(c_0_154,plain,
( cminus9(i2003_11_14_17_16_07145)
| cminus7(i2003_11_14_17_16_07145)
| cplus3(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_147,c_0_60]) ).
fof(c_0_155,plain,
! [X89] :
( ~ cTest(X89)
| cplus3(X89)
| cminus2(X89)
| cminus1(X89) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_31])]) ).
fof(c_0_156,plain,
! [X69] :
( ~ cTest(X69)
| cminus2(X69)
| cplus6(X69)
| cplus5(X69) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_11])]) ).
cnf(c_0_157,plain,
( ~ cminus5(X1)
| ~ cplus5(X1) ),
inference(split_conjunct,[status(thm)],[c_0_148]),
[final] ).
cnf(c_0_158,plain,
( cminus2(i2003_11_14_17_16_07145)
| cminus5(i2003_11_14_17_16_07145)
| cplus3(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_149,c_0_60]) ).
cnf(c_0_159,plain,
( cminus7(X1)
| cplus2(X1)
| cplus5(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_150]),
[final] ).
cnf(c_0_160,plain,
( cminus7(i2003_11_14_17_16_07145)
| ~ cplus3(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_97,c_0_151]),
[final] ).
cnf(c_0_161,plain,
( cplus7(i2003_11_14_17_16_07145)
| ~ cplus6(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_64,c_0_152]) ).
cnf(c_0_162,plain,
( cplus9(i2003_11_14_17_16_07145)
| cplus1(i2003_11_14_17_16_07145)
| cminus3(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_153,c_0_60]) ).
cnf(c_0_163,plain,
( cminus9(i2003_11_14_17_16_07145)
| cplus3(i2003_11_14_17_16_07145)
| ~ cplus7(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_86,c_0_154]) ).
cnf(c_0_164,plain,
( cplus3(X1)
| cminus2(X1)
| cminus1(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_155]),
[final] ).
cnf(c_0_165,plain,
( cminus2(X1)
| cplus6(X1)
| cplus5(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_156]),
[final] ).
cnf(c_0_166,plain,
( cminus2(i2003_11_14_17_16_07145)
| cplus3(i2003_11_14_17_16_07145)
| ~ cplus5(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_157,c_0_158]) ).
cnf(c_0_167,plain,
( cplus5(i2003_11_14_17_16_07145)
| cminus7(i2003_11_14_17_16_07145)
| cplus2(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_159,c_0_60]) ).
fof(c_0_168,plain,
! [X94] :
( ~ cTest(X94)
| cminus5(X94)
| cminus8(X94)
| cminus6(X94) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_36])]) ).
cnf(c_0_169,plain,
( ~ cplus7(i2003_11_14_17_16_07145)
| ~ cplus3(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_86,c_0_160]) ).
cnf(c_0_170,plain,
cplus7(i2003_11_14_17_16_07145),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_161,c_0_107]),c_0_140]),
[final] ).
cnf(c_0_171,plain,
( cplus1(i2003_11_14_17_16_07145)
| cminus3(i2003_11_14_17_16_07145)
| ~ cminus9(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_103,c_0_162]) ).
cnf(c_0_172,plain,
( cminus9(i2003_11_14_17_16_07145)
| cplus3(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_163,c_0_132]) ).
cnf(c_0_173,plain,
( cminus1(i2003_11_14_17_16_07145)
| cminus2(i2003_11_14_17_16_07145)
| cplus3(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_164,c_0_60]) ).
cnf(c_0_174,plain,
( cminus2(i2003_11_14_17_16_07145)
| cplus5(i2003_11_14_17_16_07145)
| cplus6(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_165,c_0_60]) ).
cnf(c_0_175,plain,
( cminus2(i2003_11_14_17_16_07145)
| cminus7(i2003_11_14_17_16_07145)
| cplus2(i2003_11_14_17_16_07145)
| cplus3(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_166,c_0_167]) ).
cnf(c_0_176,plain,
( cminus5(X1)
| cminus8(X1)
| cminus6(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_168]),
[final] ).
fof(c_0_177,plain,
! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) ),
inference(fof_simplification,[status(thm)],[axiom_1]) ).
cnf(c_0_178,plain,
( cminus5(i2003_11_14_17_16_07145)
| cplus3(i2003_11_14_17_16_07145) ),
inference(sr,[status(thm)],[c_0_158,c_0_134]) ).
cnf(c_0_179,plain,
~ cplus3(i2003_11_14_17_16_07145),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_169,c_0_170])]),
[final] ).
fof(c_0_180,plain,
! [X1] :
( cowlThing(X1)
& ~ cowlNothing(X1) ),
inference(fof_simplification,[status(thm)],[axiom_0]) ).
cnf(c_0_181,plain,
( cplus1(i2003_11_14_17_16_07145)
| cminus3(i2003_11_14_17_16_07145)
| cplus3(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_171,c_0_172]) ).
cnf(c_0_182,plain,
( cminus1(i2003_11_14_17_16_07145)
| cplus3(i2003_11_14_17_16_07145) ),
inference(sr,[status(thm)],[c_0_173,c_0_134]) ).
cnf(c_0_183,plain,
( cminus2(i2003_11_14_17_16_07145)
| cplus6(i2003_11_14_17_16_07145)
| cplus3(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_166,c_0_174]) ).
cnf(c_0_184,plain,
( cminus7(i2003_11_14_17_16_07145)
| cplus2(i2003_11_14_17_16_07145) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[c_0_175,c_0_134]),c_0_160]) ).
cnf(c_0_185,plain,
( cminus5(i2003_11_14_17_16_07145)
| cminus6(i2003_11_14_17_16_07145)
| cminus8(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_176,c_0_60]) ).
fof(c_0_186,plain,
! [X71] :
( ~ cTest(X71)
| cplus8(X71)
| cminus1(X71)
| cplus5(X71) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_13])]) ).
fof(c_0_187,plain,
! [X76] :
( ~ cTest(X76)
| cminus2(X76)
| cminus4(X76)
| cminus9(X76) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_18])]) ).
fof(c_0_188,plain,
! [X84] :
( ~ cTest(X84)
| cplus1(X84)
| cminus2(X84)
| cminus9(X84) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_26])]) ).
fof(c_0_189,plain,
! [X65] :
( ~ cTest(X65)
| cplus1(X65)
| cminus7(X65)
| cminus5(X65) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_7])]) ).
fof(c_0_190,plain,
! [X64] :
( ~ cTest(X64)
| cminus7(X64)
| cminus9(X64)
| cplus5(X64) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_6])]) ).
fof(c_0_191,plain,
! [X102] :
( ~ cTest(X102)
| cminus4(X102)
| cplus8(X102)
| cminus6(X102) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_44])]) ).
fof(c_0_192,plain,
! [X63] :
( ~ cTest(X63)
| cminus3(X63)
| cminus8(X63)
| cminus6(X63) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_5])]) ).
fof(c_0_193,plain,
! [X79] :
( ~ cTest(X79)
| cplus4(X79)
| cplus8(X79)
| cplus5(X79) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_21])]) ).
fof(c_0_194,plain,
! [X104] :
( ~ cTest(X104)
| cminus7(X104)
| cplus4(X104)
| cplus8(X104) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_46])]) ).
fof(c_0_195,plain,
! [X72] :
( ~ cTest(X72)
| cminus3(X72)
| cminus5(X72)
| cplus4(X72) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_14])]) ).
fof(c_0_196,plain,
! [X100] :
( ~ cTest(X100)
| cminus4(X100)
| cminus1(X100)
| cplus7(X100) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_42])]) ).
fof(c_0_197,plain,
! [X75] :
( ~ cTest(X75)
| cminus8(X75)
| cminus9(X75)
| cplus7(X75) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_17])]) ).
fof(c_0_198,plain,
! [X66] :
( ~ cTest(X66)
| cplus4(X66)
| cminus5(X66)
| cplus7(X66) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_8])]) ).
fof(c_0_199,plain,
! [X62] :
( ~ cTest(X62)
| cplus4(X62)
| cminus8(X62)
| cplus7(X62) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_4])]) ).
fof(c_0_200,plain,
! [X85] :
( ~ cTest(X85)
| cminus7(X85)
| cplus6(X85)
| cplus5(X85) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_27])]) ).
fof(c_0_201,plain,
! [X103] :
( ~ cTest(X103)
| cplus1(X103)
| cplus4(X103)
| cplus6(X103) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_45])]) ).
fof(c_0_202,plain,
! [X88] :
( ~ cTest(X88)
| cplus6(X88)
| cminus1(X88)
| cplus7(X88) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_30])]) ).
fof(c_0_203,plain,
! [X80] :
( ~ cTest(X80)
| cplus2(X80)
| cplus8(X80)
| cplus5(X80) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_22])]) ).
fof(c_0_204,plain,
! [X87] :
( ~ cTest(X87)
| cminus3(X87)
| cplus2(X87)
| cplus7(X87) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_29])]) ).
fof(c_0_205,plain,
! [X73] :
( ~ cTest(X73)
| cplus3(X73)
| cminus5(X73)
| cplus8(X73) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_15])]) ).
fof(c_0_206,plain,
! [X98] :
( ~ cTest(X98)
| cplus3(X98)
| cplus6(X98)
| cminus9(X98) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_40])]) ).
fof(c_0_207,plain,
! [X60] :
( ~ cTest(X60)
| cplus3(X60)
| cplus2(X60)
| cplus6(X60) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_2])]) ).
fof(c_0_208,plain,
! [X107] :
( ~ cplus4(X107)
| ~ cminus4(X107) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_50])]) ).
fof(c_0_209,plain,
! [X59] :
( ( ~ xsd_string(X59)
| ~ xsd_integer(X59) )
& ( xsd_integer(X59)
| xsd_string(X59) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_177])]) ).
cnf(c_0_210,plain,
cminus5(i2003_11_14_17_16_07145),
inference(sr,[status(thm)],[c_0_178,c_0_179]),
[final] ).
fof(c_0_211,plain,
! [X58] :
( cowlThing(X58)
& ~ cowlNothing(X58) ),
inference(variable_rename,[status(thm)],[c_0_180]) ).
cnf(c_0_212,plain,
( cminus3(i2003_11_14_17_16_07145)
| cplus3(i2003_11_14_17_16_07145) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_89,c_0_181]),c_0_182]) ).
cnf(c_0_213,plain,
( cplus6(i2003_11_14_17_16_07145)
| cplus3(i2003_11_14_17_16_07145) ),
inference(sr,[status(thm)],[c_0_183,c_0_134]) ).
cnf(c_0_214,plain,
( cplus2(i2003_11_14_17_16_07145)
| ~ cplus7(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_86,c_0_184]) ).
cnf(c_0_215,plain,
( cplus3(i2003_11_14_17_16_07145)
| ~ cplus5(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_157,c_0_178]),
[final] ).
cnf(c_0_216,plain,
( cminus6(i2003_11_14_17_16_07145)
| cminus8(i2003_11_14_17_16_07145)
| ~ cplus5(i2003_11_14_17_16_07145) ),
inference(spm,[status(thm)],[c_0_157,c_0_185]),
[final] ).
cnf(c_0_217,plain,
( cplus8(X1)
| cminus1(X1)
| cplus5(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_186]),
[final] ).
cnf(c_0_218,plain,
( cminus2(X1)
| cminus4(X1)
| cminus9(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_187]),
[final] ).
cnf(c_0_219,plain,
( cplus1(X1)
| cminus2(X1)
| cminus9(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_188]),
[final] ).
cnf(c_0_220,plain,
( cplus1(X1)
| cminus7(X1)
| cminus5(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_189]),
[final] ).
cnf(c_0_221,plain,
( cminus7(X1)
| cminus9(X1)
| cplus5(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_190]),
[final] ).
cnf(c_0_222,plain,
( cminus4(X1)
| cplus8(X1)
| cminus6(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_191]),
[final] ).
cnf(c_0_223,plain,
( cminus3(X1)
| cminus8(X1)
| cminus6(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_192]),
[final] ).
cnf(c_0_224,plain,
( cplus4(X1)
| cplus8(X1)
| cplus5(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_193]),
[final] ).
cnf(c_0_225,plain,
( cminus7(X1)
| cplus4(X1)
| cplus8(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_194]),
[final] ).
cnf(c_0_226,plain,
( cminus3(X1)
| cminus5(X1)
| cplus4(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_195]),
[final] ).
cnf(c_0_227,plain,
( cminus4(X1)
| cminus1(X1)
| cplus7(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_196]),
[final] ).
cnf(c_0_228,plain,
( cminus8(X1)
| cminus9(X1)
| cplus7(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_197]),
[final] ).
cnf(c_0_229,plain,
( cplus4(X1)
| cminus5(X1)
| cplus7(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_198]),
[final] ).
cnf(c_0_230,plain,
( cplus4(X1)
| cminus8(X1)
| cplus7(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_199]),
[final] ).
cnf(c_0_231,plain,
( cminus7(X1)
| cplus6(X1)
| cplus5(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_200]),
[final] ).
cnf(c_0_232,plain,
( cplus1(X1)
| cplus4(X1)
| cplus6(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_201]),
[final] ).
cnf(c_0_233,plain,
( cplus6(X1)
| cminus1(X1)
| cplus7(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_202]),
[final] ).
cnf(c_0_234,plain,
( cplus2(X1)
| cplus8(X1)
| cplus5(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_203]),
[final] ).
cnf(c_0_235,plain,
( cminus3(X1)
| cplus2(X1)
| cplus7(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_204]),
[final] ).
cnf(c_0_236,plain,
( cplus3(X1)
| cminus5(X1)
| cplus8(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_205]),
[final] ).
cnf(c_0_237,plain,
( cplus3(X1)
| cplus6(X1)
| cminus9(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_206]),
[final] ).
cnf(c_0_238,plain,
( cplus3(X1)
| cplus2(X1)
| cplus6(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[c_0_207]),
[final] ).
cnf(c_0_239,plain,
( ~ cplus4(X1)
| ~ cminus4(X1) ),
inference(split_conjunct,[status(thm)],[c_0_208]),
[final] ).
cnf(c_0_240,plain,
( xsd_integer(X1)
| xsd_string(X1) ),
inference(split_conjunct,[status(thm)],[c_0_209]),
[final] ).
cnf(c_0_241,plain,
( ~ xsd_string(X1)
| ~ xsd_integer(X1) ),
inference(split_conjunct,[status(thm)],[c_0_209]),
[final] ).
cnf(c_0_242,plain,
~ cplus5(i2003_11_14_17_16_07145),
inference(spm,[status(thm)],[c_0_157,c_0_210]),
[final] ).
cnf(c_0_243,plain,
~ cowlNothing(X1),
inference(split_conjunct,[status(thm)],[c_0_211]),
[final] ).
cnf(c_0_244,plain,
cminus3(i2003_11_14_17_16_07145),
inference(sr,[status(thm)],[c_0_212,c_0_179]),
[final] ).
cnf(c_0_245,plain,
cplus6(i2003_11_14_17_16_07145),
inference(sr,[status(thm)],[c_0_213,c_0_179]),
[final] ).
cnf(c_0_246,plain,
cminus1(i2003_11_14_17_16_07145),
inference(sr,[status(thm)],[c_0_182,c_0_179]),
[final] ).
cnf(c_0_247,plain,
cminus9(i2003_11_14_17_16_07145),
inference(sr,[status(thm)],[c_0_172,c_0_179]),
[final] ).
cnf(c_0_248,plain,
cplus8(i2003_11_14_17_16_07145),
inference(sr,[status(thm)],[c_0_99,c_0_179]),
[final] ).
cnf(c_0_249,plain,
cplus2(i2003_11_14_17_16_07145),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_214,c_0_170])]),
[final] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : KRS041+1 : TPTP v9.2.1. Released v3.1.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n003.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Mon May 4 20:35:56 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 1.29/1.72 % Version : CSE_E---1.7
% 1.29/1.72 % Problem : theBenchmark.p
% 1.29/1.72 % SZS status Satisfiable for theBenchmark.p
% 1.29/1.72 % SZS output start Saturation
% See solution above
% 1.29/1.72 % Total time : 1.367s
%------------------------------------------------------------------------------