%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : KRS103+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.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 : Thu Sep 24 01:00:15 PM UTC 2026
% Result : Unsatisfiable 0.07s 5.58s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS103+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/5.57 % Computer : n015.cluster.edu
% 0.07/5.57 % Model : x86_64 x86_64
% 0.07/5.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/5.57 % Memory : 8046.5625MB
% 0.07/5.57 % OS : Linux 6.8.0-71-generic
% 0.07/5.57 % CPULimit : 300
% 0.07/5.57 % WCLimit : 300
% 0.07/5.57 % DateTime : Sun Sep 20 22:56:41 UTC 2026
% 0.07/5.57 % CPUTime :
% 0.07/5.58 % Drodi V4.1.1
% 0.07/5.58 % Refutation found
% 0.07/5.58 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.07/5.58 % SZS output start CNFRefutation for theBenchmark
% 0.07/5.58 fof(f3,axiom,(
% 0.07/5.58 (! [X] :( cTest(X)=> ( cplus1(X)| cplus9(X)| cminus6(X) ) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f5,axiom,(
% 0.07/5.58 (! [X] :( cTest(X)=> ( cminus3(X)| cplus7(X)| cplus8(X) ) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f7,axiom,(
% 0.07/5.58 (! [X] :( cTest(X)=> ( cplus3(X)| cminus7(X)| cplus8(X) ) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f8,axiom,(
% 0.07/5.58 (! [X] :( cTest(X)=> ( cminus4(X)| cplus5(X)| cplus9(X) ) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f9,axiom,(
% 0.07/5.58 (! [X] :( cTest(X)=> ( cminus7(X)| cplus9(X)| cminus6(X) ) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f10,axiom,(
% 0.07/5.58 (! [X] :( cTest(X)=> ( cminus9(X)| cminus4(X)| cminus8(X) ) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f11,axiom,(
% 0.07/5.58 (! [X] :( cTest(X)=> ( cplus3(X)| cminus4(X)| cplus6(X) ) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f12,axiom,(
% 0.07/5.58 (! [X] :( cTest(X)=> ( cplus4(X)| cplus6(X)| cminus8(X) ) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f15,axiom,(
% 0.07/5.58 (! [X] :( cTest(X)=> ( cminus4(X)| cplus2(X)| cplus1(X) ) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f21,axiom,(
% 0.07/5.58 (! [X] :( cTest(X)=> ( cminus3(X)| cplus2(X)| cplus8(X) ) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f22,axiom,(
% 0.07/5.58 (! [X] :( cTest(X)=> ( cminus2(X)| cplus4(X)| cminus6(X) ) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f23,axiom,(
% 0.07/5.58 (! [X] :( cTest(X)=> ( cminus2(X)| cplus6(X)| cminus7(X) ) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f26,axiom,(
% 0.07/5.58 (! [X] :( cTest(X)=> ( cplus3(X)| cplus4(X)| cplus9(X) ) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f29,axiom,(
% 0.07/5.58 (! [X] :( cTest(X)=> ( cminus9(X)| cplus3(X)| cplus4(X) ) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f30,axiom,(
% 0.07/5.58 (! [X] :( cTest(X)=> ( cminus4(X)| cminus3(X)| cminus7(X) ) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f32,axiom,(
% 0.07/5.58 (! [X] :( cTest(X)=> ( cminus4(X)| cminus8(X)| cplus9(X) ) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f34,axiom,(
% 0.07/5.58 (! [X] :( cTest(X)=> ( cminus9(X)| cminus2(X)| cplus7(X) ) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f37,axiom,(
% 0.07/5.58 (! [X] :( cTest(X)=> ( cminus1(X)| cplus4(X)| cplus2(X) ) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f39,axiom,(
% 0.07/5.58 (! [X] :( cTest(X)=> ( cplus3(X)| cplus4(X)| cplus6(X) ) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f44,axiom,(
% 0.07/5.58 (! [X] :( cTest(X)=> ( cminus9(X)| cplus1(X)| cminus6(X) ) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f46,axiom,(
% 0.07/5.58 (! [X] :( cTest(X)=> ( cminus4(X)| cplus2(X)| cplus8(X) ) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f47,axiom,(
% 0.07/5.58 (! [X] :( cTest(X)=> ( cminus5(X)| cplus7(X)| cplus8(X) ) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f48,axiom,(
% 0.07/5.58 cTest(i2003_11_14_17_20_46476) ),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f49,axiom,(
% 0.07/5.58 (! [X] :~ ( cminus8(X)& cplus8(X) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f50,axiom,(
% 0.07/5.58 (! [X] :~ ( cminus9(X)& cplus9(X) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f51,axiom,(
% 0.07/5.58 (! [X] :~ ( cplus4(X)& cminus4(X) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f52,axiom,(
% 0.07/5.58 (! [X] :~ ( cminus7(X)& cplus7(X) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f53,axiom,(
% 0.07/5.58 (! [X] :~ ( cplus3(X)& cminus3(X) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f54,axiom,(
% 0.07/5.58 (! [X] :~ ( cplus5(X)& cminus5(X) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f55,axiom,(
% 0.07/5.58 (! [X] :~ ( cminus2(X)& cplus2(X) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f56,axiom,(
% 0.07/5.58 (! [X] :~ ( cminus1(X)& cplus1(X) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f57,axiom,(
% 0.07/5.58 (! [X] :~ ( cplus6(X)& cminus6(X) ) )),
% 0.07/5.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.07/5.58 fof(f65,plain,(
% 0.07/5.58 ![X]: (~cTest(X)|((cplus1(X)|cplus9(X))|cminus6(X)))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.07/5.58 fof(f66,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cplus1(X0)|cplus9(X0)|cminus6(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f65])).
% 0.07/5.58 fof(f69,plain,(
% 0.07/5.58 ![X]: (~cTest(X)|((cminus3(X)|cplus7(X))|cplus8(X)))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.07/5.58 fof(f70,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cminus3(X0)|cplus7(X0)|cplus8(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f69])).
% 0.07/5.58 fof(f73,plain,(
% 0.07/5.58 ![X]: (~cTest(X)|((cplus3(X)|cminus7(X))|cplus8(X)))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.07/5.58 fof(f74,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cplus3(X0)|cminus7(X0)|cplus8(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f73])).
% 0.07/5.58 fof(f75,plain,(
% 0.07/5.58 ![X]: (~cTest(X)|((cminus4(X)|cplus5(X))|cplus9(X)))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.07/5.58 fof(f76,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cminus4(X0)|cplus5(X0)|cplus9(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f75])).
% 0.07/5.58 fof(f77,plain,(
% 0.07/5.58 ![X]: (~cTest(X)|((cminus7(X)|cplus9(X))|cminus6(X)))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.07/5.58 fof(f78,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cminus7(X0)|cplus9(X0)|cminus6(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f77])).
% 0.07/5.58 fof(f79,plain,(
% 0.07/5.58 ![X]: (~cTest(X)|((cminus9(X)|cminus4(X))|cminus8(X)))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.07/5.58 fof(f80,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cminus9(X0)|cminus4(X0)|cminus8(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f79])).
% 0.07/5.58 fof(f81,plain,(
% 0.07/5.58 ![X]: (~cTest(X)|((cplus3(X)|cminus4(X))|cplus6(X)))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 0.07/5.58 fof(f82,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cplus3(X0)|cminus4(X0)|cplus6(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f81])).
% 0.07/5.58 fof(f83,plain,(
% 0.07/5.58 ![X]: (~cTest(X)|((cplus4(X)|cplus6(X))|cminus8(X)))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.07/5.58 fof(f84,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cplus4(X0)|cplus6(X0)|cminus8(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f83])).
% 0.07/5.58 fof(f89,plain,(
% 0.07/5.58 ![X]: (~cTest(X)|((cminus4(X)|cplus2(X))|cplus1(X)))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.07/5.58 fof(f90,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cminus4(X0)|cplus2(X0)|cplus1(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f89])).
% 0.07/5.58 fof(f101,plain,(
% 0.07/5.58 ![X]: (~cTest(X)|((cminus3(X)|cplus2(X))|cplus8(X)))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 0.07/5.58 fof(f102,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cminus3(X0)|cplus2(X0)|cplus8(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f101])).
% 0.07/5.58 fof(f103,plain,(
% 0.07/5.58 ![X]: (~cTest(X)|((cminus2(X)|cplus4(X))|cminus6(X)))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f22])).
% 0.07/5.58 fof(f104,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cminus2(X0)|cplus4(X0)|cminus6(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f103])).
% 0.07/5.58 fof(f105,plain,(
% 0.07/5.58 ![X]: (~cTest(X)|((cminus2(X)|cplus6(X))|cminus7(X)))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 0.07/5.58 fof(f106,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cminus2(X0)|cplus6(X0)|cminus7(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f105])).
% 0.07/5.58 fof(f111,plain,(
% 0.07/5.58 ![X]: (~cTest(X)|((cplus3(X)|cplus4(X))|cplus9(X)))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 0.07/5.58 fof(f112,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cplus3(X0)|cplus4(X0)|cplus9(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f111])).
% 0.07/5.58 fof(f117,plain,(
% 0.07/5.58 ![X]: (~cTest(X)|((cminus9(X)|cplus3(X))|cplus4(X)))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 0.07/5.58 fof(f118,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cminus9(X0)|cplus3(X0)|cplus4(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f117])).
% 0.07/5.58 fof(f119,plain,(
% 0.07/5.58 ![X]: (~cTest(X)|((cminus4(X)|cminus3(X))|cminus7(X)))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 0.07/5.58 fof(f120,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cminus4(X0)|cminus3(X0)|cminus7(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f119])).
% 0.07/5.58 fof(f123,plain,(
% 0.07/5.58 ![X]: (~cTest(X)|((cminus4(X)|cminus8(X))|cplus9(X)))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 0.07/5.58 fof(f124,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cminus4(X0)|cminus8(X0)|cplus9(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f123])).
% 0.07/5.58 fof(f127,plain,(
% 0.07/5.58 ![X]: (~cTest(X)|((cminus9(X)|cminus2(X))|cplus7(X)))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 0.07/5.58 fof(f128,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cminus9(X0)|cminus2(X0)|cplus7(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f127])).
% 0.07/5.58 fof(f133,plain,(
% 0.07/5.58 ![X]: (~cTest(X)|((cminus1(X)|cplus4(X))|cplus2(X)))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 0.07/5.58 fof(f134,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cminus1(X0)|cplus4(X0)|cplus2(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f133])).
% 0.07/5.58 fof(f137,plain,(
% 0.07/5.58 ![X]: (~cTest(X)|((cplus3(X)|cplus4(X))|cplus6(X)))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 0.07/5.58 fof(f138,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cplus3(X0)|cplus4(X0)|cplus6(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f137])).
% 0.07/5.58 fof(f147,plain,(
% 0.07/5.58 ![X]: (~cTest(X)|((cminus9(X)|cplus1(X))|cminus6(X)))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f44])).
% 0.07/5.58 fof(f148,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cminus9(X0)|cplus1(X0)|cminus6(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f147])).
% 0.07/5.58 fof(f151,plain,(
% 0.07/5.58 ![X]: (~cTest(X)|((cminus4(X)|cplus2(X))|cplus8(X)))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f46])).
% 0.07/5.58 fof(f152,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cminus4(X0)|cplus2(X0)|cplus8(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f151])).
% 0.07/5.58 fof(f153,plain,(
% 0.07/5.58 ![X]: (~cTest(X)|((cminus5(X)|cplus7(X))|cplus8(X)))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 0.07/5.58 fof(f154,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cminus5(X0)|cplus7(X0)|cplus8(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f153])).
% 0.07/5.58 fof(f155,plain,(
% 0.07/5.58 cTest(i2003_11_14_17_20_46476)),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f48])).
% 0.07/5.58 fof(f156,plain,(
% 0.07/5.58 ![X]: (~cminus8(X)|~cplus8(X))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 0.07/5.58 fof(f157,plain,(
% 0.07/5.58 ![X0]: (~cminus8(X0)|~cplus8(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f156])).
% 0.07/5.58 fof(f158,plain,(
% 0.07/5.58 ![X]: (~cminus9(X)|~cplus9(X))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 0.07/5.58 fof(f159,plain,(
% 0.07/5.58 ![X0]: (~cminus9(X0)|~cplus9(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f158])).
% 0.07/5.58 fof(f160,plain,(
% 0.07/5.58 ![X]: (~cplus4(X)|~cminus4(X))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f51])).
% 0.07/5.58 fof(f161,plain,(
% 0.07/5.58 ![X0]: (~cplus4(X0)|~cminus4(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f160])).
% 0.07/5.58 fof(f162,plain,(
% 0.07/5.58 ![X]: (~cminus7(X)|~cplus7(X))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f52])).
% 0.07/5.58 fof(f163,plain,(
% 0.07/5.58 ![X0]: (~cminus7(X0)|~cplus7(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f162])).
% 0.07/5.58 fof(f164,plain,(
% 0.07/5.58 ![X]: (~cplus3(X)|~cminus3(X))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f53])).
% 0.07/5.58 fof(f165,plain,(
% 0.07/5.58 ![X0]: (~cplus3(X0)|~cminus3(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f164])).
% 0.07/5.58 fof(f166,plain,(
% 0.07/5.58 ![X]: (~cplus5(X)|~cminus5(X))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f54])).
% 0.07/5.58 fof(f167,plain,(
% 0.07/5.58 ![X0]: (~cplus5(X0)|~cminus5(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f166])).
% 0.07/5.58 fof(f168,plain,(
% 0.07/5.58 ![X]: (~cminus2(X)|~cplus2(X))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f55])).
% 0.07/5.58 fof(f169,plain,(
% 0.07/5.58 ![X0]: (~cminus2(X0)|~cplus2(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f168])).
% 0.07/5.58 fof(f170,plain,(
% 0.07/5.58 ![X]: (~cminus1(X)|~cplus1(X))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f56])).
% 0.07/5.58 fof(f171,plain,(
% 0.07/5.58 ![X0]: (~cminus1(X0)|~cplus1(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f170])).
% 0.07/5.58 fof(f172,plain,(
% 0.07/5.58 ![X]: (~cplus6(X)|~cminus6(X))),
% 0.07/5.58 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 0.07/5.58 fof(f173,plain,(
% 0.07/5.58 ![X0]: (~cplus6(X0)|~cminus6(X0))),
% 0.07/5.58 inference(cnf_transformation,[status(thm)],[f172])).
% 0.07/5.58 fof(f175,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cminus3(X0)|cplus7(X0)|~cminus8(X0))),
% 0.07/5.58 inference(resolution,[status(thm)],[f70,f157])).
% 0.07/5.58 fof(f176,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cminus4(X0)|cminus8(X0)|~cplus9(X0))),
% 0.07/5.58 inference(resolution,[status(thm)],[f80,f159])).
% 0.07/5.58 fof(f177,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cplus6(X0)|cminus8(X0)|~cminus4(X0))),
% 0.07/5.58 inference(resolution,[status(thm)],[f84,f161])).
% 0.07/5.58 fof(f181,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cplus4(X0)|cminus6(X0)|~cplus2(X0))),
% 0.07/5.58 inference(resolution,[status(thm)],[f104,f169])).
% 0.07/5.58 fof(f182,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cplus6(X0)|cminus7(X0)|~cplus2(X0))),
% 0.07/5.58 inference(resolution,[status(thm)],[f106,f169])).
% 0.07/5.58 fof(f184,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cplus3(X0)|cplus9(X0)|~cminus4(X0))),
% 0.07/5.58 inference(resolution,[status(thm)],[f112,f161])).
% 0.07/5.58 fof(f186,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cminus9(X0)|cplus3(X0)|~cminus4(X0))),
% 0.07/5.58 inference(resolution,[status(thm)],[f118,f161])).
% 0.07/5.58 fof(f187,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cminus9(X0)|cplus7(X0)|~cplus2(X0))),
% 0.07/5.58 inference(resolution,[status(thm)],[f128,f169])).
% 0.07/5.58 fof(f190,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cplus3(X0)|cplus6(X0)|~cminus4(X0))),
% 0.07/5.58 inference(resolution,[status(thm)],[f138,f161])).
% 0.07/5.58 fof(f191,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cplus3(X0)|cplus6(X0))),
% 0.07/5.58 inference(forward_subsumption_resolution,[status(thm)],[f190,f82])).
% 0.07/5.58 fof(f196,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cplus1(X0)|cminus6(X0)|~cplus9(X0))),
% 0.07/5.58 inference(resolution,[status(thm)],[f148,f159])).
% 0.07/5.58 fof(f197,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cplus1(X0)|cminus6(X0))),
% 0.07/5.58 inference(forward_subsumption_resolution,[status(thm)],[f196,f66])).
% 0.07/5.58 fof(f198,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cminus5(X0)|cplus7(X0)|~cminus8(X0))),
% 0.07/5.58 inference(resolution,[status(thm)],[f154,f157])).
% 0.07/5.58 fof(f199,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cminus3(X0)|~cminus8(X0)|~cminus7(X0))),
% 0.07/5.58 inference(resolution,[status(thm)],[f175,f163])).
% 0.07/5.58 fof(f202,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cminus4(X0)|cminus8(X0))),
% 0.07/5.58 inference(forward_subsumption_resolution,[status(thm)],[f176,f124])).
% 0.07/5.58 fof(f203,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cplus6(X0)|cminus8(X0))),
% 0.07/5.58 inference(forward_subsumption_resolution,[status(thm)],[f177,f202])).
% 0.07/5.58 fof(f204,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cminus8(X0)|~cminus6(X0))),
% 0.07/5.58 inference(resolution,[status(thm)],[f203,f173])).
% 0.07/5.58 fof(f206,definition,(
% 0.07/5.58 sQ0_spl <=> (cplus6(i2003_11_14_17_20_46476))),
% 0.07/5.58 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.07/5.58 fof(f207,plain,(
% 0.07/5.58 cplus6(i2003_11_14_17_20_46476)|~sQ0_spl),
% 0.07/5.58 inference(component_clause,[status(thm)],[f206])).
% 0.07/5.58 fof(f209,definition,(
% 0.07/5.58 sQ1_spl <=> (cplus9(i2003_11_14_17_20_46476))),
% 0.07/5.58 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.07/5.58 fof(f210,plain,(
% 0.07/5.58 cplus9(i2003_11_14_17_20_46476)|~sQ1_spl),
% 0.07/5.58 inference(component_clause,[status(thm)],[f209])).
% 0.07/5.58 fof(f212,definition,(
% 0.07/5.58 sQ2_spl <=> (cplus2(i2003_11_14_17_20_46476))),
% 0.07/5.58 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.07/5.58 fof(f214,plain,(
% 0.07/5.58 ~cplus2(i2003_11_14_17_20_46476)|sQ2_spl),
% 0.07/5.58 inference(component_clause,[status(thm)],[f212])).
% 0.07/5.58 fof(f216,plain,(
% 0.07/5.58 ~cTest(i2003_11_14_17_20_46476)|cminus4(i2003_11_14_17_20_46476)|cplus8(i2003_11_14_17_20_46476)|sQ2_spl),
% 0.07/5.58 inference(resolution,[status(thm)],[f214,f152])).
% 0.07/5.58 fof(f217,plain,(
% 0.07/5.58 ~cTest(i2003_11_14_17_20_46476)|cminus1(i2003_11_14_17_20_46476)|cplus4(i2003_11_14_17_20_46476)|sQ2_spl),
% 0.07/5.58 inference(resolution,[status(thm)],[f214,f134])).
% 0.07/5.58 fof(f219,plain,(
% 0.07/5.58 ~cTest(i2003_11_14_17_20_46476)|cminus3(i2003_11_14_17_20_46476)|cplus8(i2003_11_14_17_20_46476)|sQ2_spl),
% 0.07/5.58 inference(resolution,[status(thm)],[f214,f102])).
% 0.07/5.58 fof(f220,plain,(
% 0.07/5.58 ~cTest(i2003_11_14_17_20_46476)|cminus4(i2003_11_14_17_20_46476)|cplus1(i2003_11_14_17_20_46476)|sQ2_spl),
% 0.07/5.58 inference(resolution,[status(thm)],[f214,f90])).
% 0.07/5.58 fof(f222,definition,(
% 0.07/5.58 sQ3_spl <=> (cTest(i2003_11_14_17_20_46476))),
% 0.07/5.58 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.07/5.58 fof(f224,plain,(
% 0.07/5.58 ~cTest(i2003_11_14_17_20_46476)|sQ3_spl),
% 0.07/5.58 inference(component_clause,[status(thm)],[f222])).
% 0.07/5.58 fof(f225,definition,(
% 0.07/5.58 sQ4_spl <=> (cminus4(i2003_11_14_17_20_46476))),
% 0.07/5.58 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.07/5.58 fof(f226,plain,(
% 0.07/5.58 cminus4(i2003_11_14_17_20_46476)|~sQ4_spl),
% 0.07/5.58 inference(component_clause,[status(thm)],[f225])).
% 0.07/5.58 fof(f228,definition,(
% 0.07/5.58 sQ5_spl <=> (cplus8(i2003_11_14_17_20_46476))),
% 0.07/5.58 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.07/5.58 fof(f229,plain,(
% 0.07/5.58 cplus8(i2003_11_14_17_20_46476)|~sQ5_spl),
% 0.07/5.58 inference(component_clause,[status(thm)],[f228])).
% 0.07/5.58 fof(f231,plain,(
% 0.07/5.58 ~sQ3_spl|sQ4_spl|sQ5_spl|sQ2_spl),
% 0.07/5.58 inference(split_clause,[status(thm)],[f216,f222,f225,f228,f212])).
% 0.07/5.58 fof(f232,definition,(
% 0.07/5.58 sQ6_spl <=> (cminus1(i2003_11_14_17_20_46476))),
% 0.07/5.58 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.07/5.58 fof(f233,plain,(
% 0.07/5.58 cminus1(i2003_11_14_17_20_46476)|~sQ6_spl),
% 0.07/5.58 inference(component_clause,[status(thm)],[f232])).
% 0.07/5.58 fof(f235,definition,(
% 0.07/5.58 sQ7_spl <=> (cplus4(i2003_11_14_17_20_46476))),
% 0.07/5.58 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.07/5.58 fof(f236,plain,(
% 0.07/5.58 cplus4(i2003_11_14_17_20_46476)|~sQ7_spl),
% 0.07/5.58 inference(component_clause,[status(thm)],[f235])).
% 0.07/5.58 fof(f238,plain,(
% 0.07/5.58 ~sQ3_spl|sQ6_spl|sQ7_spl|sQ2_spl),
% 0.07/5.58 inference(split_clause,[status(thm)],[f217,f222,f232,f235,f212])).
% 0.07/5.58 fof(f239,definition,(
% 0.07/5.58 sQ8_spl <=> (cminus5(i2003_11_14_17_20_46476))),
% 0.07/5.58 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.07/5.58 fof(f240,plain,(
% 0.07/5.58 cminus5(i2003_11_14_17_20_46476)|~sQ8_spl),
% 0.07/5.58 inference(component_clause,[status(thm)],[f239])).
% 0.07/5.58 fof(f242,definition,(
% 0.07/5.58 sQ9_spl <=> (cminus7(i2003_11_14_17_20_46476))),
% 0.07/5.58 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.07/5.58 fof(f246,definition,(
% 0.07/5.58 sQ10_spl <=> (cminus3(i2003_11_14_17_20_46476))),
% 0.07/5.58 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.07/5.58 fof(f247,plain,(
% 0.07/5.58 cminus3(i2003_11_14_17_20_46476)|~sQ10_spl),
% 0.07/5.58 inference(component_clause,[status(thm)],[f246])).
% 0.07/5.58 fof(f249,plain,(
% 0.07/5.58 ~sQ3_spl|sQ10_spl|sQ5_spl|sQ2_spl),
% 0.07/5.58 inference(split_clause,[status(thm)],[f219,f222,f246,f228,f212])).
% 0.07/5.58 fof(f250,definition,(
% 0.07/5.58 sQ11_spl <=> (cplus1(i2003_11_14_17_20_46476))),
% 0.07/5.58 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.07/5.58 fof(f251,plain,(
% 0.07/5.58 cplus1(i2003_11_14_17_20_46476)|~sQ11_spl),
% 0.07/5.58 inference(component_clause,[status(thm)],[f250])).
% 0.07/5.58 fof(f253,plain,(
% 0.07/5.58 ~sQ3_spl|sQ4_spl|sQ11_spl|sQ2_spl),
% 0.07/5.58 inference(split_clause,[status(thm)],[f220,f222,f225,f250,f212])).
% 0.07/5.58 fof(f258,plain,(
% 0.07/5.58 $false|sQ3_spl),
% 0.07/5.58 inference(forward_subsumption_resolution,[status(thm)],[f224,f155])).
% 0.07/5.58 fof(f259,plain,(
% 0.07/5.58 sQ3_spl),
% 0.07/5.58 inference(contradiction_clause,[status(thm)],[f258])).
% 0.07/5.58 fof(f260,plain,(
% 0.07/5.58 cplus4(i2003_11_14_17_20_46476)|cminus6(i2003_11_14_17_20_46476)|~cplus2(i2003_11_14_17_20_46476)),
% 0.07/5.58 inference(resolution,[status(thm)],[f181,f155])).
% 0.07/5.58 fof(f261,definition,(
% 0.07/5.58 sQ13_spl <=> (cminus6(i2003_11_14_17_20_46476))),
% 0.07/5.58 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.07/5.58 fof(f262,plain,(
% 0.07/5.58 cminus6(i2003_11_14_17_20_46476)|~sQ13_spl),
% 0.07/5.58 inference(component_clause,[status(thm)],[f261])).
% 0.07/5.58 fof(f264,plain,(
% 0.07/5.58 sQ7_spl|sQ13_spl|~sQ2_spl),
% 0.07/5.58 inference(split_clause,[status(thm)],[f260,f235,f261,f212])).
% 0.07/5.58 fof(f265,plain,(
% 0.07/5.58 cplus6(i2003_11_14_17_20_46476)|cminus7(i2003_11_14_17_20_46476)|~cplus2(i2003_11_14_17_20_46476)),
% 0.07/5.58 inference(resolution,[status(thm)],[f182,f155])).
% 0.07/5.58 fof(f266,plain,(
% 0.07/5.58 sQ0_spl|sQ9_spl|~sQ2_spl),
% 0.07/5.58 inference(split_clause,[status(thm)],[f265,f206,f242,f212])).
% 0.07/5.58 fof(f268,definition,(
% 0.07/5.58 sQ14_spl <=> (cminus9(i2003_11_14_17_20_46476))),
% 0.07/5.58 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.07/5.58 fof(f269,plain,(
% 0.07/5.58 cminus9(i2003_11_14_17_20_46476)|~sQ14_spl),
% 0.07/5.58 inference(component_clause,[status(thm)],[f268])).
% 0.07/5.58 fof(f273,plain,(
% 0.07/5.58 ~cminus8(i2003_11_14_17_20_46476)|~sQ5_spl),
% 0.07/5.58 inference(resolution,[status(thm)],[f229,f157])).
% 0.07/5.58 fof(f274,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cplus3(X0)|~cminus4(X0)|~cplus9(X0))),
% 0.07/5.58 inference(resolution,[status(thm)],[f186,f159])).
% 0.07/5.58 fof(f275,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cplus3(X0)|~cminus4(X0))),
% 0.07/5.58 inference(forward_subsumption_resolution,[status(thm)],[f274,f184])).
% 0.07/5.58 fof(f276,plain,(
% 0.07/5.58 cminus9(i2003_11_14_17_20_46476)|cplus7(i2003_11_14_17_20_46476)|~cplus2(i2003_11_14_17_20_46476)),
% 0.07/5.58 inference(resolution,[status(thm)],[f187,f155])).
% 0.07/5.58 fof(f277,definition,(
% 0.07/5.58 sQ15_spl <=> (cplus7(i2003_11_14_17_20_46476))),
% 0.07/5.58 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.07/5.58 fof(f278,plain,(
% 0.07/5.58 cplus7(i2003_11_14_17_20_46476)|~sQ15_spl),
% 0.07/5.58 inference(component_clause,[status(thm)],[f277])).
% 0.07/5.58 fof(f280,plain,(
% 0.07/5.58 sQ14_spl|sQ15_spl|~sQ2_spl),
% 0.07/5.58 inference(split_clause,[status(thm)],[f276,f268,f277,f212])).
% 0.07/5.58 fof(f282,definition,(
% 0.07/5.58 sQ16_spl <=> (cplus3(i2003_11_14_17_20_46476))),
% 0.07/5.58 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.07/5.58 fof(f283,plain,(
% 0.07/5.58 cplus3(i2003_11_14_17_20_46476)|~sQ16_spl),
% 0.07/5.58 inference(component_clause,[status(thm)],[f282])).
% 0.07/5.58 fof(f284,plain,(
% 0.07/5.58 ~cplus3(i2003_11_14_17_20_46476)|sQ16_spl),
% 0.07/5.58 inference(component_clause,[status(thm)],[f282])).
% 0.07/5.58 fof(f288,plain,(
% 0.07/5.58 ~cminus4(i2003_11_14_17_20_46476)|~sQ7_spl),
% 0.07/5.58 inference(resolution,[status(thm)],[f236,f161])).
% 0.07/5.58 fof(f289,plain,(
% 0.07/5.58 $false|~sQ4_spl|~sQ7_spl),
% 0.07/5.58 inference(forward_subsumption_resolution,[status(thm)],[f288,f226])).
% 0.07/5.58 fof(f290,plain,(
% 0.07/5.58 ~sQ4_spl|~sQ7_spl),
% 0.07/5.58 inference(contradiction_clause,[status(thm)],[f289])).
% 0.07/5.58 fof(f292,definition,(
% 0.07/5.58 sQ17_spl <=> (cminus8(i2003_11_14_17_20_46476))),
% 0.07/5.58 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.07/5.58 fof(f293,plain,(
% 0.07/5.58 cminus8(i2003_11_14_17_20_46476)|~sQ17_spl),
% 0.07/5.58 inference(component_clause,[status(thm)],[f292])).
% 0.07/5.58 fof(f296,plain,(
% 0.07/5.58 ~cminus6(i2003_11_14_17_20_46476)|~sQ0_spl),
% 0.07/5.58 inference(resolution,[status(thm)],[f207,f173])).
% 0.07/5.58 fof(f299,plain,(
% 0.07/5.58 ~cplus9(i2003_11_14_17_20_46476)|~sQ14_spl),
% 0.07/5.58 inference(resolution,[status(thm)],[f269,f159])).
% 0.07/5.58 fof(f305,plain,(
% 0.07/5.58 ~cminus1(i2003_11_14_17_20_46476)|~sQ11_spl),
% 0.07/5.58 inference(resolution,[status(thm)],[f251,f171])).
% 0.07/5.58 fof(f307,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cminus8(X0)|~cTest(X0)|cplus1(X0))),
% 0.07/5.58 inference(resolution,[status(thm)],[f204,f197])).
% 0.07/5.58 fof(f308,plain,(
% 0.07/5.58 ![X0]: (~cTest(X0)|cminus8(X0)|cplus1(X0))),
% 0.07/5.58 inference(duplicate_literals_removal,[status(thm)],[f307])).
% 0.07/5.58 fof(f312,plain,(
% 0.07/5.58 ~cTest(i2003_11_14_17_20_46476)|cminus8(i2003_11_14_17_20_46476)|~sQ13_spl),
% 0.07/5.58 inference(resolution,[status(thm)],[f262,f204])).
% 0.07/5.58 fof(f314,plain,(
% 0.07/5.58 ~sQ3_spl|sQ17_spl|~sQ13_spl),
% 0.07/5.58 inference(split_clause,[status(thm)],[f312,f222,f292,f261])).
% 0.07/5.58 fof(f320,plain,(
% 0.07/5.58 ~cTest(i2003_11_14_17_20_46476)|cminus3(i2003_11_14_17_20_46476)|~cminus7(i2003_11_14_17_20_46476)|~sQ17_spl),
% 0.07/5.58 inference(resolution,[status(thm)],[f293,f199])).
% 0.07/5.58 fof(f321,plain,(
% 0.07/5.58 ~cTest(i2003_11_14_17_20_46476)|cminus5(i2003_11_14_17_20_46476)|cplus7(i2003_11_14_17_20_46476)|~sQ17_spl),
% 0.07/5.58 inference(resolution,[status(thm)],[f293,f198])).
% 0.07/5.58 fof(f324,plain,(
% 0.07/5.58 ~sQ3_spl|sQ10_spl|~sQ9_spl|~sQ17_spl),
% 0.07/5.58 inference(split_clause,[status(thm)],[f320,f222,f246,f242,f292])).
% 0.07/5.58 fof(f325,plain,(
% 0.07/5.58 ~sQ3_spl|sQ8_spl|sQ15_spl|~sQ17_spl),
% 0.07/5.58 inference(split_clause,[status(thm)],[f321,f222,f239,f277,f292])).
% 0.07/5.58 fof(f327,plain,(
% 0.07/5.58 ~cminus7(i2003_11_14_17_20_46476)|~sQ15_spl),
% 0.07/5.58 inference(resolution,[status(thm)],[f278,f163])).
% 0.07/5.58 fof(f328,plain,(
% 0.07/5.58 $false|~sQ14_spl|~sQ1_spl),
% 0.07/5.58 inference(forward_subsumption_resolution,[status(thm)],[f210,f299])).
% 0.07/5.58 fof(f329,plain,(
% 0.07/5.58 ~sQ14_spl|~sQ1_spl),
% 0.07/5.58 inference(contradiction_clause,[status(thm)],[f328])).
% 0.07/5.58 fof(f347,plain,(
% 0.07/5.58 ~cplus5(i2003_11_14_17_20_46476)|~sQ8_spl),
% 0.07/5.58 inference(resolution,[status(thm)],[f240,f167])).
% 0.07/5.58 fof(f352,plain,(
% 0.07/5.58 ~cplus3(i2003_11_14_17_20_46476)|~sQ10_spl),
% 0.07/5.58 inference(resolution,[status(thm)],[f247,f165])).
% 0.07/5.58 fof(f353,plain,(
% 0.07/5.58 $false|~sQ16_spl|~sQ10_spl),
% 0.07/5.58 inference(forward_subsumption_resolution,[status(thm)],[f352,f283])).
% 0.07/5.58 fof(f354,plain,(
% 0.07/5.58 ~sQ16_spl|~sQ10_spl),
% 0.07/5.58 inference(contradiction_clause,[status(thm)],[f353])).
% 0.07/5.58 fof(f356,plain,(
% 0.07/5.58 ~cTest(i2003_11_14_17_20_46476)|~cminus4(i2003_11_14_17_20_46476)|sQ16_spl),
% 0.07/5.59 inference(resolution,[status(thm)],[f284,f275])).
% 0.07/5.59 fof(f358,plain,(
% 0.07/5.59 ~cTest(i2003_11_14_17_20_46476)|cplus6(i2003_11_14_17_20_46476)|sQ16_spl),
% 0.07/5.59 inference(resolution,[status(thm)],[f284,f191])).
% 0.07/5.59 fof(f360,plain,(
% 0.07/5.59 ~sQ3_spl|~sQ4_spl|sQ16_spl),
% 0.07/5.59 inference(split_clause,[status(thm)],[f356,f222,f225,f282])).
% 0.07/5.59 fof(f362,plain,(
% 0.07/5.59 ~sQ3_spl|sQ0_spl|sQ16_spl),
% 0.07/5.59 inference(split_clause,[status(thm)],[f358,f222,f206,f282])).
% 0.07/5.59 fof(f364,plain,(
% 0.07/5.59 $false|~sQ17_spl|~sQ5_spl),
% 0.07/5.59 inference(forward_subsumption_resolution,[status(thm)],[f273,f293])).
% 0.07/5.59 fof(f365,plain,(
% 0.07/5.59 ~sQ17_spl|~sQ5_spl),
% 0.07/5.59 inference(contradiction_clause,[status(thm)],[f364])).
% 0.07/5.59 fof(f375,plain,(
% 0.07/5.59 ~cTest(i2003_11_14_17_20_46476)|cminus4(i2003_11_14_17_20_46476)|cplus9(i2003_11_14_17_20_46476)|~sQ8_spl),
% 0.07/5.59 inference(resolution,[status(thm)],[f347,f76])).
% 0.07/5.59 fof(f378,plain,(
% 0.07/5.59 ~sQ3_spl|sQ4_spl|sQ1_spl|~sQ8_spl),
% 0.07/5.59 inference(split_clause,[status(thm)],[f375,f222,f225,f209,f239])).
% 0.07/5.59 fof(f391,plain,(
% 0.07/5.59 ~cTest(i2003_11_14_17_20_46476)|cminus8(i2003_11_14_17_20_46476)|~sQ7_spl),
% 0.07/5.59 inference(resolution,[status(thm)],[f288,f202])).
% 0.07/5.59 fof(f396,plain,(
% 0.07/5.59 ~sQ3_spl|sQ17_spl|~sQ7_spl),
% 0.07/5.59 inference(split_clause,[status(thm)],[f391,f222,f292,f235])).
% 0.07/5.59 fof(f401,plain,(
% 0.07/5.59 cminus8(i2003_11_14_17_20_46476)|cplus1(i2003_11_14_17_20_46476)),
% 0.07/5.59 inference(resolution,[status(thm)],[f308,f155])).
% 0.07/5.59 fof(f402,plain,(
% 0.07/5.59 sQ17_spl|sQ11_spl),
% 0.07/5.59 inference(split_clause,[status(thm)],[f401,f292,f250])).
% 0.07/5.59 fof(f403,plain,(
% 0.07/5.59 ~cTest(i2003_11_14_17_20_46476)|cminus4(i2003_11_14_17_20_46476)|cminus3(i2003_11_14_17_20_46476)|~sQ15_spl),
% 0.07/5.59 inference(resolution,[status(thm)],[f327,f120])).
% 0.07/5.59 fof(f404,plain,(
% 0.07/5.59 ~cTest(i2003_11_14_17_20_46476)|cplus9(i2003_11_14_17_20_46476)|cminus6(i2003_11_14_17_20_46476)|~sQ15_spl),
% 0.07/5.59 inference(resolution,[status(thm)],[f327,f78])).
% 0.07/5.59 fof(f405,plain,(
% 0.07/5.59 ~cTest(i2003_11_14_17_20_46476)|cplus3(i2003_11_14_17_20_46476)|cplus8(i2003_11_14_17_20_46476)|~sQ15_spl),
% 0.07/5.59 inference(resolution,[status(thm)],[f327,f74])).
% 0.07/5.59 fof(f406,plain,(
% 0.07/5.59 ~sQ3_spl|sQ4_spl|sQ10_spl|~sQ15_spl),
% 0.07/5.59 inference(split_clause,[status(thm)],[f403,f222,f225,f246,f277])).
% 0.07/5.59 fof(f407,plain,(
% 0.07/5.59 ~sQ3_spl|sQ1_spl|sQ13_spl|~sQ15_spl),
% 0.07/5.59 inference(split_clause,[status(thm)],[f404,f222,f209,f261,f277])).
% 0.07/5.59 fof(f408,plain,(
% 0.07/5.59 ~sQ3_spl|sQ16_spl|sQ5_spl|~sQ15_spl),
% 0.07/5.59 inference(split_clause,[status(thm)],[f405,f222,f282,f228,f277])).
% 0.07/5.59 fof(f409,plain,(
% 0.07/5.59 $false|~sQ11_spl|~sQ6_spl),
% 0.07/5.59 inference(forward_subsumption_resolution,[status(thm)],[f233,f305])).
% 0.07/5.59 fof(f410,plain,(
% 0.07/5.59 ~sQ11_spl|~sQ6_spl),
% 0.07/5.59 inference(contradiction_clause,[status(thm)],[f409])).
% 0.07/5.59 fof(f411,plain,(
% 0.07/5.59 $false|~sQ0_spl|~sQ13_spl),
% 0.07/5.59 inference(forward_subsumption_resolution,[status(thm)],[f262,f296])).
% 0.07/5.59 fof(f412,plain,(
% 0.07/5.59 ~sQ0_spl|~sQ13_spl),
% 0.07/5.59 inference(contradiction_clause,[status(thm)],[f411])).
% 0.07/5.59 fof(f413,plain,(
% 0.07/5.59 $false),
% 0.07/5.59 inference(sat_refutation,[status(thm)],[f231,f238,f249,f253,f259,f264,f266,f280,f290,f314,f324,f325,f329,f354,f360,f362,f365,f378,f396,f402,f406,f407,f408,f410,f412])).
% 0.07/5.59 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/5.61 % Elapsed time: 0.031945 seconds
% 0.13/5.61 % CPU time: 0.035248 seconds
% 0.13/5.61 % Total memory used: 1.190 MB
% 0.13/5.61 % Net memory used: 1.176 MB
%------------------------------------------------------------------------------