%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : KRS102+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 : n013.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.15s 1.21s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS102+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/1.17 % Computer : n013.cluster.edu
% 0.11/1.17 % Model : x86_64 x86_64
% 0.11/1.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/1.17 % Memory : 8046.5625MB
% 0.11/1.17 % OS : Linux 6.8.0-71-generic
% 0.11/1.17 % CPULimit : 300
% 0.11/1.17 % WCLimit : 300
% 0.11/1.17 % DateTime : Sun Sep 20 22:53:09 UTC 2026
% 0.11/1.17 % CPUTime :
% 0.11/1.18 % Drodi V4.1.1
% 0.15/1.21 % Refutation found
% 0.15/1.21 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.15/1.21 % SZS output start CNFRefutation for theBenchmark
% 0.15/1.21 fof(f9,axiom,(
% 0.15/1.21 (! [X] :( cTorF(X)<=> ( X = iminus4| X = iplus4 ) ) )),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f10,axiom,(
% 0.15/1.21 (! [X] :( cTorF(X)<=> ( X = iplus2| X = iminus2 ) ) )),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f11,axiom,(
% 0.15/1.21 (! [X] :( cTorF(X)<=> ( X = iplus7| X = iminus7 ) ) )),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f12,axiom,(
% 0.15/1.21 (! [X] :( cTorF(X)<=> ( X = iplus5| X = iminus5 ) ) )),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f13,axiom,(
% 0.15/1.21 (! [X] :( cTorF(X)<=> ( X = iplus3| X = iminus3 ) ) )),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f14,axiom,(
% 0.15/1.21 (! [X] :( cTorF(X)<=> ( X = iT| X = iF ) ) )),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f15,axiom,(
% 0.15/1.21 (! [X] :( cTorF(X)<=> ( X = iplus8| X = iminus8 ) ) )),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f16,axiom,(
% 0.15/1.21 (! [X] :( cTorF(X)<=> ( X = iminus6| X = iplus6 ) ) )),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f17,axiom,(
% 0.15/1.21 (! [X] :( cTorF(X)<=> ( X = iminus9| X = iplus9 ) ) )),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f20,axiom,(
% 0.15/1.21 ( iT = iminus6| iT = iplus9| iT = iminus7 ) ),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f21,axiom,(
% 0.15/1.21 ( iT = iplus8| iT = iminus3| iT = iplus7 ) ),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f24,axiom,(
% 0.15/1.21 ( iT = iplus3| iT = iminus9| iT = iplus4 ) ),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f27,axiom,(
% 0.15/1.21 ( iT = iminus8| iT = iminus4| iT = iplus9 ) ),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f28,axiom,(
% 0.15/1.21 ( iT = iplus3| iT = iplus6| iT = iplus4 ) ),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f31,axiom,(
% 0.15/1.21 ( iT = iminus8| iT = iplus6| iT = iplus4 ) ),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f32,axiom,(
% 0.15/1.21 ( iT = iplus3| iT = iminus9| iT = iminus2 ) ),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f33,axiom,(
% 0.15/1.21 ( iT = iplus6| iT = iminus2| iT = iminus7 ) ),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f34,axiom,(
% 0.15/1.21 ( iT = iplus6| iT = iminus4| iT = iminus3 ) ),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f37,axiom,(
% 0.15/1.21 ( iT = iplus8| iT = iplus2| iT = iminus4 ) ),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f42,axiom,(
% 0.15/1.21 ( iT = iminus4| iT = iminus3| iT = iminus7 ) ),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f45,axiom,(
% 0.15/1.21 ( iT = iplus3| iT = iplus6| iT = iminus4 ) ),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f46,axiom,(
% 0.15/1.21 ( iT = iminus8| iT = iminus9| iT = iminus4 ) ),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f48,axiom,(
% 0.15/1.21 ( iT = iplus8| iT = iplus2| iT = iminus3 ) ),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f51,axiom,(
% 0.15/1.21 ( iT = iminus5| iT = iminus8| iT = iminus3 ) ),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f52,axiom,(
% 0.15/1.21 ( iT = iplus3| iT = iplus9| iT = iplus4 ) ),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f55,axiom,(
% 0.15/1.21 ( iT = iplus5| iT = iminus8| iT = iminus3 ) ),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f61,axiom,(
% 0.15/1.21 ( iT = iplus5| iT = iplus2| iT = iplus9 ) ),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f62,axiom,(
% 0.15/1.21 ( iT = iminus6| iT = iminus2| iT = iplus4 ) ),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f64,axiom,(
% 0.15/1.21 ( iT = iminus4| iT = iplus7| iT = iplus9 ) ),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f83,axiom,(
% 0.15/1.21 iT != iF ),
% 0.15/1.21 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/1.21 fof(f111,plain,(
% 0.15/1.21 ![X]: ((~cTorF(X)|(X=iminus4|X=iplus4))&(cTorF(X)|(~X=iminus4&~X=iplus4)))),
% 0.15/1.21 inference(NNF_transformation,[status(thm)],[f9])).
% 0.15/1.21 fof(f112,plain,(
% 0.15/1.21 (![X]: (~cTorF(X)|(X=iminus4|X=iplus4)))&(![X]: (cTorF(X)|(~X=iminus4&~X=iplus4)))),
% 0.15/1.21 inference(miniscoping,[status(thm)],[f111])).
% 0.15/1.21 fof(f113,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iminus4|X0=iplus4)),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f112])).
% 0.15/1.21 fof(f114,plain,(
% 0.15/1.21 ![X0]: (cTorF(X0)|~X0=iminus4)),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f112])).
% 0.15/1.21 fof(f115,plain,(
% 0.15/1.21 ![X0]: (cTorF(X0)|~X0=iplus4)),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f112])).
% 0.15/1.21 fof(f116,plain,(
% 0.15/1.21 ![X]: ((~cTorF(X)|(X=iplus2|X=iminus2))&(cTorF(X)|(~X=iplus2&~X=iminus2)))),
% 0.15/1.21 inference(NNF_transformation,[status(thm)],[f10])).
% 0.15/1.21 fof(f117,plain,(
% 0.15/1.21 (![X]: (~cTorF(X)|(X=iplus2|X=iminus2)))&(![X]: (cTorF(X)|(~X=iplus2&~X=iminus2)))),
% 0.15/1.21 inference(miniscoping,[status(thm)],[f116])).
% 0.15/1.21 fof(f118,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iplus2|X0=iminus2)),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f117])).
% 0.15/1.21 fof(f121,plain,(
% 0.15/1.21 ![X]: ((~cTorF(X)|(X=iplus7|X=iminus7))&(cTorF(X)|(~X=iplus7&~X=iminus7)))),
% 0.15/1.21 inference(NNF_transformation,[status(thm)],[f11])).
% 0.15/1.21 fof(f122,plain,(
% 0.15/1.21 (![X]: (~cTorF(X)|(X=iplus7|X=iminus7)))&(![X]: (cTorF(X)|(~X=iplus7&~X=iminus7)))),
% 0.15/1.21 inference(miniscoping,[status(thm)],[f121])).
% 0.15/1.21 fof(f123,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iplus7|X0=iminus7)),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f122])).
% 0.15/1.21 fof(f126,plain,(
% 0.15/1.21 ![X]: ((~cTorF(X)|(X=iplus5|X=iminus5))&(cTorF(X)|(~X=iplus5&~X=iminus5)))),
% 0.15/1.21 inference(NNF_transformation,[status(thm)],[f12])).
% 0.15/1.21 fof(f127,plain,(
% 0.15/1.21 (![X]: (~cTorF(X)|(X=iplus5|X=iminus5)))&(![X]: (cTorF(X)|(~X=iplus5&~X=iminus5)))),
% 0.15/1.21 inference(miniscoping,[status(thm)],[f126])).
% 0.15/1.21 fof(f128,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iplus5|X0=iminus5)),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f127])).
% 0.15/1.21 fof(f131,plain,(
% 0.15/1.21 ![X]: ((~cTorF(X)|(X=iplus3|X=iminus3))&(cTorF(X)|(~X=iplus3&~X=iminus3)))),
% 0.15/1.21 inference(NNF_transformation,[status(thm)],[f13])).
% 0.15/1.21 fof(f132,plain,(
% 0.15/1.21 (![X]: (~cTorF(X)|(X=iplus3|X=iminus3)))&(![X]: (cTorF(X)|(~X=iplus3&~X=iminus3)))),
% 0.15/1.21 inference(miniscoping,[status(thm)],[f131])).
% 0.15/1.21 fof(f133,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iplus3|X0=iminus3)),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f132])).
% 0.15/1.21 fof(f135,plain,(
% 0.15/1.21 ![X0]: (cTorF(X0)|~X0=iminus3)),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f132])).
% 0.15/1.21 fof(f136,plain,(
% 0.15/1.21 ![X]: ((~cTorF(X)|(X=iT|X=iF))&(cTorF(X)|(~X=iT&~X=iF)))),
% 0.15/1.21 inference(NNF_transformation,[status(thm)],[f14])).
% 0.15/1.21 fof(f137,plain,(
% 0.15/1.21 (![X]: (~cTorF(X)|(X=iT|X=iF)))&(![X]: (cTorF(X)|(~X=iT&~X=iF)))),
% 0.15/1.21 inference(miniscoping,[status(thm)],[f136])).
% 0.15/1.21 fof(f139,plain,(
% 0.15/1.21 ![X0]: (cTorF(X0)|~X0=iT)),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f137])).
% 0.15/1.21 fof(f140,plain,(
% 0.15/1.21 ![X0]: (cTorF(X0)|~X0=iF)),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f137])).
% 0.15/1.21 fof(f141,plain,(
% 0.15/1.21 ![X]: ((~cTorF(X)|(X=iplus8|X=iminus8))&(cTorF(X)|(~X=iplus8&~X=iminus8)))),
% 0.15/1.21 inference(NNF_transformation,[status(thm)],[f15])).
% 0.15/1.21 fof(f142,plain,(
% 0.15/1.21 (![X]: (~cTorF(X)|(X=iplus8|X=iminus8)))&(![X]: (cTorF(X)|(~X=iplus8&~X=iminus8)))),
% 0.15/1.21 inference(miniscoping,[status(thm)],[f141])).
% 0.15/1.21 fof(f143,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iplus8|X0=iminus8)),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f142])).
% 0.15/1.21 fof(f144,plain,(
% 0.15/1.21 ![X0]: (cTorF(X0)|~X0=iplus8)),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f142])).
% 0.15/1.21 fof(f145,plain,(
% 0.15/1.21 ![X0]: (cTorF(X0)|~X0=iminus8)),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f142])).
% 0.15/1.21 fof(f146,plain,(
% 0.15/1.21 ![X]: ((~cTorF(X)|(X=iminus6|X=iplus6))&(cTorF(X)|(~X=iminus6&~X=iplus6)))),
% 0.15/1.21 inference(NNF_transformation,[status(thm)],[f16])).
% 0.15/1.21 fof(f147,plain,(
% 0.15/1.21 (![X]: (~cTorF(X)|(X=iminus6|X=iplus6)))&(![X]: (cTorF(X)|(~X=iminus6&~X=iplus6)))),
% 0.15/1.21 inference(miniscoping,[status(thm)],[f146])).
% 0.15/1.21 fof(f148,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iminus6|X0=iplus6)),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f147])).
% 0.15/1.21 fof(f149,plain,(
% 0.15/1.21 ![X0]: (cTorF(X0)|~X0=iminus6)),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f147])).
% 0.15/1.21 fof(f151,plain,(
% 0.15/1.21 ![X]: ((~cTorF(X)|(X=iminus9|X=iplus9))&(cTorF(X)|(~X=iminus9&~X=iplus9)))),
% 0.15/1.21 inference(NNF_transformation,[status(thm)],[f17])).
% 0.15/1.21 fof(f152,plain,(
% 0.15/1.21 (![X]: (~cTorF(X)|(X=iminus9|X=iplus9)))&(![X]: (cTorF(X)|(~X=iminus9&~X=iplus9)))),
% 0.15/1.21 inference(miniscoping,[status(thm)],[f151])).
% 0.15/1.21 fof(f153,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iminus9|X0=iplus9)),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f152])).
% 0.15/1.21 fof(f155,plain,(
% 0.15/1.21 ![X0]: (cTorF(X0)|~X0=iplus9)),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f152])).
% 0.15/1.21 fof(f158,plain,(
% 0.15/1.21 iT=iminus6|iT=iplus9|iT=iminus7),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f20])).
% 0.15/1.21 fof(f159,plain,(
% 0.15/1.21 iT=iplus8|iT=iminus3|iT=iplus7),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f21])).
% 0.15/1.21 fof(f162,plain,(
% 0.15/1.21 iT=iplus3|iT=iminus9|iT=iplus4),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f24])).
% 0.15/1.21 fof(f165,plain,(
% 0.15/1.21 iT=iminus8|iT=iminus4|iT=iplus9),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f27])).
% 0.15/1.21 fof(f166,plain,(
% 0.15/1.21 iT=iplus3|iT=iplus6|iT=iplus4),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f28])).
% 0.15/1.21 fof(f169,plain,(
% 0.15/1.21 iT=iminus8|iT=iplus6|iT=iplus4),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f31])).
% 0.15/1.21 fof(f170,plain,(
% 0.15/1.21 iT=iplus3|iT=iminus9|iT=iminus2),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f32])).
% 0.15/1.21 fof(f171,plain,(
% 0.15/1.21 iT=iplus6|iT=iminus2|iT=iminus7),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f33])).
% 0.15/1.21 fof(f172,plain,(
% 0.15/1.21 iT=iplus6|iT=iminus4|iT=iminus3),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f34])).
% 0.15/1.21 fof(f175,plain,(
% 0.15/1.21 iT=iplus8|iT=iplus2|iT=iminus4),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f37])).
% 0.15/1.21 fof(f180,plain,(
% 0.15/1.21 iT=iminus4|iT=iminus3|iT=iminus7),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f42])).
% 0.15/1.21 fof(f183,plain,(
% 0.15/1.21 iT=iplus3|iT=iplus6|iT=iminus4),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f45])).
% 0.15/1.21 fof(f184,plain,(
% 0.15/1.21 iT=iminus8|iT=iminus9|iT=iminus4),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f46])).
% 0.15/1.21 fof(f186,plain,(
% 0.15/1.21 iT=iplus8|iT=iplus2|iT=iminus3),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f48])).
% 0.15/1.21 fof(f189,plain,(
% 0.15/1.21 iT=iminus5|iT=iminus8|iT=iminus3),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f51])).
% 0.15/1.21 fof(f190,plain,(
% 0.15/1.21 iT=iplus3|iT=iplus9|iT=iplus4),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f52])).
% 0.15/1.21 fof(f193,plain,(
% 0.15/1.21 iT=iplus5|iT=iminus8|iT=iminus3),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f55])).
% 0.15/1.21 fof(f199,plain,(
% 0.15/1.21 iT=iplus5|iT=iplus2|iT=iplus9),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f61])).
% 0.15/1.21 fof(f200,plain,(
% 0.15/1.21 iT=iminus6|iT=iminus2|iT=iplus4),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f62])).
% 0.15/1.21 fof(f202,plain,(
% 0.15/1.21 iT=iminus4|iT=iplus7|iT=iplus9),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f64])).
% 0.15/1.21 fof(f221,plain,(
% 0.15/1.21 ~iT=iF),
% 0.15/1.21 inference(cnf_transformation,[status(thm)],[f83])).
% 0.15/1.21 fof(f222,definition,(
% 0.15/1.21 sQ0_spl <=> (iT=iminus6)),
% 0.15/1.21 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.15/1.21 fof(f223,plain,(
% 0.15/1.21 iT=iminus6|~sQ0_spl),
% 0.15/1.21 inference(component_clause,[status(thm)],[f222])).
% 0.15/1.21 fof(f225,definition,(
% 0.15/1.21 sQ1_spl <=> (iT=iplus2)),
% 0.15/1.21 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.15/1.21 fof(f226,plain,(
% 0.15/1.21 iT=iplus2|~sQ1_spl),
% 0.15/1.21 inference(component_clause,[status(thm)],[f225])).
% 0.15/1.21 fof(f232,definition,(
% 0.15/1.21 sQ3_spl <=> (iT=iplus9)),
% 0.15/1.21 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.15/1.21 fof(f233,plain,(
% 0.15/1.21 iT=iplus9|~sQ3_spl),
% 0.15/1.21 inference(component_clause,[status(thm)],[f232])).
% 0.15/1.21 fof(f235,definition,(
% 0.15/1.21 sQ4_spl <=> (iT=iminus7)),
% 0.15/1.21 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.15/1.21 fof(f236,plain,(
% 0.15/1.21 iT=iminus7|~sQ4_spl),
% 0.15/1.21 inference(component_clause,[status(thm)],[f235])).
% 0.15/1.21 fof(f238,plain,(
% 0.15/1.21 sQ0_spl|sQ3_spl|sQ4_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f158,f222,f232,f235])).
% 0.15/1.21 fof(f239,definition,(
% 0.15/1.21 sQ5_spl <=> (iT=iplus8)),
% 0.15/1.21 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.15/1.21 fof(f240,plain,(
% 0.15/1.21 iT=iplus8|~sQ5_spl),
% 0.15/1.21 inference(component_clause,[status(thm)],[f239])).
% 0.15/1.21 fof(f242,definition,(
% 0.15/1.21 sQ6_spl <=> (iT=iminus3)),
% 0.15/1.21 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.15/1.21 fof(f243,plain,(
% 0.15/1.21 iT=iminus3|~sQ6_spl),
% 0.15/1.21 inference(component_clause,[status(thm)],[f242])).
% 0.15/1.21 fof(f245,definition,(
% 0.15/1.21 sQ7_spl <=> (iT=iplus7)),
% 0.15/1.21 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.15/1.21 fof(f246,plain,(
% 0.15/1.21 iT=iplus7|~sQ7_spl),
% 0.15/1.21 inference(component_clause,[status(thm)],[f245])).
% 0.15/1.21 fof(f248,plain,(
% 0.15/1.21 sQ5_spl|sQ6_spl|sQ7_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f159,f239,f242,f245])).
% 0.15/1.21 fof(f249,definition,(
% 0.15/1.21 sQ8_spl <=> (iT=iplus5)),
% 0.15/1.21 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.15/1.21 fof(f250,plain,(
% 0.15/1.21 iT=iplus5|~sQ8_spl),
% 0.15/1.21 inference(component_clause,[status(thm)],[f249])).
% 0.15/1.21 fof(f254,definition,(
% 0.15/1.21 sQ9_spl <=> (iT=iplus3)),
% 0.15/1.21 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.15/1.21 fof(f255,plain,(
% 0.15/1.21 iT=iplus3|~sQ9_spl),
% 0.15/1.21 inference(component_clause,[status(thm)],[f254])).
% 0.15/1.21 fof(f257,definition,(
% 0.15/1.21 sQ10_spl <=> (iT=iminus9)),
% 0.15/1.21 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.15/1.21 fof(f258,plain,(
% 0.15/1.21 iT=iminus9|~sQ10_spl),
% 0.15/1.21 inference(component_clause,[status(thm)],[f257])).
% 0.15/1.21 fof(f260,definition,(
% 0.15/1.21 sQ11_spl <=> (iT=iplus4)),
% 0.15/1.21 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.15/1.21 fof(f261,plain,(
% 0.15/1.21 iT=iplus4|~sQ11_spl),
% 0.15/1.21 inference(component_clause,[status(thm)],[f260])).
% 0.15/1.21 fof(f263,plain,(
% 0.15/1.21 sQ9_spl|sQ10_spl|sQ11_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f162,f254,f257,f260])).
% 0.15/1.21 fof(f265,definition,(
% 0.15/1.21 sQ12_spl <=> (iT=iminus8)),
% 0.15/1.21 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.15/1.21 fof(f266,plain,(
% 0.15/1.21 iT=iminus8|~sQ12_spl),
% 0.15/1.21 inference(component_clause,[status(thm)],[f265])).
% 0.15/1.21 fof(f268,definition,(
% 0.15/1.21 sQ13_spl <=> (iT=iminus4)),
% 0.15/1.21 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.15/1.21 fof(f269,plain,(
% 0.15/1.21 iT=iminus4|~sQ13_spl),
% 0.15/1.21 inference(component_clause,[status(thm)],[f268])).
% 0.15/1.21 fof(f271,plain,(
% 0.15/1.21 sQ12_spl|sQ13_spl|sQ3_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f165,f265,f268,f232])).
% 0.15/1.21 fof(f272,definition,(
% 0.15/1.21 sQ14_spl <=> (iT=iplus6)),
% 0.15/1.21 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.15/1.21 fof(f273,plain,(
% 0.15/1.21 iT=iplus6|~sQ14_spl),
% 0.15/1.21 inference(component_clause,[status(thm)],[f272])).
% 0.15/1.21 fof(f275,plain,(
% 0.15/1.21 sQ9_spl|sQ14_spl|sQ11_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f166,f254,f272,f260])).
% 0.15/1.21 fof(f277,definition,(
% 0.15/1.21 sQ15_spl <=> (iT=iminus2)),
% 0.15/1.21 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.15/1.21 fof(f278,plain,(
% 0.15/1.21 iT=iminus2|~sQ15_spl),
% 0.15/1.21 inference(component_clause,[status(thm)],[f277])).
% 0.15/1.21 fof(f281,plain,(
% 0.15/1.21 sQ12_spl|sQ14_spl|sQ11_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f169,f265,f272,f260])).
% 0.15/1.21 fof(f282,plain,(
% 0.15/1.21 sQ9_spl|sQ10_spl|sQ15_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f170,f254,f257,f277])).
% 0.15/1.21 fof(f283,plain,(
% 0.15/1.21 sQ14_spl|sQ15_spl|sQ4_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f171,f272,f277,f235])).
% 0.15/1.21 fof(f284,plain,(
% 0.15/1.21 sQ14_spl|sQ13_spl|sQ6_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f172,f272,f268,f242])).
% 0.15/1.21 fof(f287,plain,(
% 0.15/1.21 sQ5_spl|sQ1_spl|sQ13_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f175,f239,f225,f268])).
% 0.15/1.21 fof(f289,definition,(
% 0.15/1.21 sQ16_spl <=> (iT=iminus5)),
% 0.15/1.21 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.15/1.21 fof(f290,plain,(
% 0.15/1.21 iT=iminus5|~sQ16_spl),
% 0.15/1.21 inference(component_clause,[status(thm)],[f289])).
% 0.15/1.21 fof(f295,plain,(
% 0.15/1.21 sQ13_spl|sQ6_spl|sQ4_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f180,f268,f242,f235])).
% 0.15/1.21 fof(f301,plain,(
% 0.15/1.21 sQ9_spl|sQ14_spl|sQ13_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f183,f254,f272,f268])).
% 0.15/1.21 fof(f302,plain,(
% 0.15/1.21 sQ12_spl|sQ10_spl|sQ13_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f184,f265,f257,f268])).
% 0.15/1.21 fof(f304,plain,(
% 0.15/1.21 sQ5_spl|sQ1_spl|sQ6_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f186,f239,f225,f242])).
% 0.15/1.21 fof(f307,plain,(
% 0.15/1.21 sQ16_spl|sQ12_spl|sQ6_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f189,f289,f265,f242])).
% 0.15/1.21 fof(f308,plain,(
% 0.15/1.21 sQ9_spl|sQ3_spl|sQ11_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f190,f254,f232,f260])).
% 0.15/1.21 fof(f311,plain,(
% 0.15/1.21 sQ8_spl|sQ12_spl|sQ6_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f193,f249,f265,f242])).
% 0.15/1.21 fof(f317,plain,(
% 0.15/1.21 sQ8_spl|sQ1_spl|sQ3_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f199,f249,f225,f232])).
% 0.15/1.21 fof(f318,plain,(
% 0.15/1.21 sQ0_spl|sQ15_spl|sQ11_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f200,f222,f277,f260])).
% 0.15/1.21 fof(f320,plain,(
% 0.15/1.21 sQ13_spl|sQ7_spl|sQ3_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f202,f268,f245,f232])).
% 0.15/1.21 fof(f323,plain,(
% 0.15/1.21 cTorF(iminus4)),
% 0.15/1.21 inference(destructive_equality_resolution,[status(thm)],[f114])).
% 0.15/1.21 fof(f324,plain,(
% 0.15/1.21 cTorF(iplus4)),
% 0.15/1.21 inference(destructive_equality_resolution,[status(thm)],[f115])).
% 0.15/1.21 fof(f332,plain,(
% 0.15/1.21 cTorF(iminus3)),
% 0.15/1.21 inference(destructive_equality_resolution,[status(thm)],[f135])).
% 0.15/1.21 fof(f333,plain,(
% 0.15/1.21 cTorF(iT)),
% 0.15/1.21 inference(destructive_equality_resolution,[status(thm)],[f139])).
% 0.15/1.21 fof(f334,plain,(
% 0.15/1.21 cTorF(iF)),
% 0.15/1.21 inference(destructive_equality_resolution,[status(thm)],[f140])).
% 0.15/1.21 fof(f335,plain,(
% 0.15/1.21 cTorF(iplus8)),
% 0.15/1.21 inference(destructive_equality_resolution,[status(thm)],[f144])).
% 0.15/1.21 fof(f336,plain,(
% 0.15/1.21 cTorF(iminus8)),
% 0.15/1.21 inference(destructive_equality_resolution,[status(thm)],[f145])).
% 0.15/1.21 fof(f337,plain,(
% 0.15/1.21 cTorF(iminus6)),
% 0.15/1.21 inference(destructive_equality_resolution,[status(thm)],[f149])).
% 0.15/1.21 fof(f340,plain,(
% 0.15/1.21 cTorF(iplus9)),
% 0.15/1.21 inference(destructive_equality_resolution,[status(thm)],[f155])).
% 0.15/1.21 fof(f342,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iT|X0=iplus4|~sQ13_spl)),
% 0.15/1.21 inference(backward_demodulation,[status(thm)],[f269,f113])).
% 0.15/1.21 fof(f344,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iminus9|X0=iT|~sQ3_spl)),
% 0.15/1.21 inference(backward_demodulation,[status(thm)],[f233,f153])).
% 0.15/1.21 fof(f346,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iminus6|X0=iT|~sQ14_spl)),
% 0.15/1.21 inference(backward_demodulation,[status(thm)],[f273,f148])).
% 0.15/1.21 fof(f348,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iT|X0=iminus3|~sQ9_spl)),
% 0.15/1.21 inference(backward_demodulation,[status(thm)],[f255,f133])).
% 0.15/1.21 fof(f353,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iplus2|X0=iT|~sQ15_spl)),
% 0.15/1.21 inference(backward_demodulation,[status(thm)],[f278,f118])).
% 0.15/1.21 fof(f355,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iplus8|X0=iT|~sQ12_spl)),
% 0.15/1.21 inference(backward_demodulation,[status(thm)],[f266,f143])).
% 0.15/1.21 fof(f362,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iT|X0=iT|~sQ11_spl|~sQ13_spl)),
% 0.15/1.21 inference(forward_demodulation,[status(thm)],[f261,f342])).
% 0.15/1.21 fof(f363,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iT|~sQ11_spl|~sQ13_spl)),
% 0.15/1.21 inference(duplicate_literals_removal,[status(thm)],[f362])).
% 0.15/1.21 fof(f366,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iT|X0=iT|~sQ6_spl|~sQ9_spl)),
% 0.15/1.21 inference(forward_demodulation,[status(thm)],[f243,f348])).
% 0.15/1.21 fof(f367,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iT|~sQ6_spl|~sQ9_spl)),
% 0.15/1.21 inference(duplicate_literals_removal,[status(thm)],[f366])).
% 0.15/1.21 fof(f368,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iT|X0=iT|~sQ1_spl|~sQ15_spl)),
% 0.15/1.21 inference(forward_demodulation,[status(thm)],[f226,f353])).
% 0.15/1.21 fof(f369,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iT|~sQ1_spl|~sQ15_spl)),
% 0.15/1.21 inference(duplicate_literals_removal,[status(thm)],[f368])).
% 0.15/1.21 fof(f370,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iT|X0=iT|~sQ5_spl|~sQ12_spl)),
% 0.15/1.21 inference(forward_demodulation,[status(thm)],[f240,f355])).
% 0.15/1.21 fof(f371,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iT|~sQ5_spl|~sQ12_spl)),
% 0.15/1.21 inference(duplicate_literals_removal,[status(thm)],[f370])).
% 0.15/1.21 fof(f400,definition,(
% 0.15/1.21 sQ23_spl <=> (iminus5=iplus5)),
% 0.15/1.21 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.15/1.21 fof(f401,plain,(
% 0.15/1.21 iminus5=iplus5|~sQ23_spl),
% 0.15/1.21 inference(component_clause,[status(thm)],[f400])).
% 0.15/1.21 fof(f402,plain,(
% 0.15/1.21 ~iminus5=iplus5|sQ23_spl),
% 0.15/1.21 inference(component_clause,[status(thm)],[f400])).
% 0.15/1.21 fof(f407,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iminus5|X0=iminus5|~sQ23_spl)),
% 0.15/1.21 inference(backward_demodulation,[status(thm)],[f401,f128])).
% 0.15/1.21 fof(f410,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iminus5|~sQ23_spl)),
% 0.15/1.21 inference(duplicate_literals_removal,[status(thm)],[f407])).
% 0.15/1.21 fof(f412,plain,(
% 0.15/1.21 iF=iT|~sQ11_spl|~sQ13_spl),
% 0.15/1.21 inference(resolution,[status(thm)],[f363,f334])).
% 0.15/1.21 fof(f416,plain,(
% 0.15/1.21 $false|~sQ11_spl|~sQ13_spl),
% 0.15/1.21 inference(forward_subsumption_resolution,[status(thm)],[f412,f221])).
% 0.15/1.21 fof(f417,plain,(
% 0.15/1.21 ~sQ11_spl|~sQ13_spl),
% 0.15/1.21 inference(contradiction_clause,[status(thm)],[f416])).
% 0.15/1.21 fof(f420,plain,(
% 0.15/1.21 iF=iminus4|iF=iplus4),
% 0.15/1.21 inference(resolution,[status(thm)],[f113,f334])).
% 0.15/1.21 fof(f421,plain,(
% 0.15/1.21 iT=iminus4|iT=iplus4),
% 0.15/1.21 inference(resolution,[status(thm)],[f113,f333])).
% 0.15/1.21 fof(f423,definition,(
% 0.15/1.21 sQ25_spl <=> (iF=iminus4)),
% 0.15/1.21 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.15/1.21 fof(f424,plain,(
% 0.15/1.21 iF=iminus4|~sQ25_spl),
% 0.15/1.21 inference(component_clause,[status(thm)],[f423])).
% 0.15/1.21 fof(f426,definition,(
% 0.15/1.21 sQ26_spl <=> (iF=iplus4)),
% 0.15/1.21 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.15/1.21 fof(f427,plain,(
% 0.15/1.21 iF=iplus4|~sQ26_spl),
% 0.15/1.21 inference(component_clause,[status(thm)],[f426])).
% 0.15/1.21 fof(f428,plain,(
% 0.15/1.21 ~iF=iplus4|sQ26_spl),
% 0.15/1.21 inference(component_clause,[status(thm)],[f426])).
% 0.15/1.21 fof(f429,plain,(
% 0.15/1.21 sQ25_spl|sQ26_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f420,f423,f426])).
% 0.15/1.21 fof(f430,plain,(
% 0.15/1.21 sQ13_spl|sQ11_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f421,f268,f260])).
% 0.15/1.21 fof(f431,definition,(
% 0.15/1.21 sQ27_spl <=> (iminus5=iminus4)),
% 0.15/1.21 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.15/1.21 fof(f432,plain,(
% 0.15/1.21 iminus5=iminus4|~sQ27_spl),
% 0.15/1.21 inference(component_clause,[status(thm)],[f431])).
% 0.15/1.21 fof(f433,plain,(
% 0.15/1.21 ~iminus5=iminus4|sQ27_spl),
% 0.15/1.21 inference(component_clause,[status(thm)],[f431])).
% 0.15/1.21 fof(f440,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iminus4|~sQ27_spl|~sQ23_spl)),
% 0.15/1.21 inference(backward_demodulation,[status(thm)],[f432,f410])).
% 0.15/1.21 fof(f443,plain,(
% 0.15/1.21 ~iT=iminus4|~sQ25_spl),
% 0.15/1.21 inference(backward_demodulation,[status(thm)],[f424,f221])).
% 0.15/1.21 fof(f444,plain,(
% 0.15/1.21 cTorF(iminus4)|~sQ25_spl),
% 0.15/1.21 inference(backward_demodulation,[status(thm)],[f424,f334])).
% 0.15/1.21 fof(f454,plain,(
% 0.15/1.21 ~sQ13_spl|~sQ25_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f443,f268,f423])).
% 0.15/1.21 fof(f460,plain,(
% 0.15/1.21 ~iT=iplus4|~sQ26_spl),
% 0.15/1.21 inference(forward_demodulation,[status(thm)],[f427,f221])).
% 0.15/1.21 fof(f461,plain,(
% 0.15/1.21 ~iT=iT|~sQ11_spl|~sQ26_spl),
% 0.15/1.21 inference(forward_demodulation,[status(thm)],[f261,f460])).
% 0.15/1.21 fof(f462,plain,(
% 0.15/1.21 $false|~sQ11_spl|~sQ26_spl),
% 0.15/1.21 inference(trivial_equality_resolution,[status(thm)],[f461])).
% 0.15/1.21 fof(f463,plain,(
% 0.15/1.21 ~sQ11_spl|~sQ26_spl),
% 0.15/1.21 inference(contradiction_clause,[status(thm)],[f462])).
% 0.15/1.21 fof(f473,plain,(
% 0.15/1.21 iminus6=iT|~sQ5_spl|~sQ12_spl),
% 0.15/1.21 inference(resolution,[status(thm)],[f371,f337])).
% 0.15/1.21 fof(f476,plain,(
% 0.15/1.21 iplus4=iT|~sQ5_spl|~sQ12_spl),
% 0.15/1.21 inference(resolution,[status(thm)],[f324,f371])).
% 0.15/1.21 fof(f477,plain,(
% 0.15/1.21 sQ11_spl|~sQ5_spl|~sQ12_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f476,f260,f239,f265])).
% 0.15/1.21 fof(f478,plain,(
% 0.15/1.21 iT=iminus4|~sQ16_spl|~sQ27_spl),
% 0.15/1.21 inference(forward_demodulation,[status(thm)],[f290,f432])).
% 0.15/1.21 fof(f480,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iT|~sQ16_spl|~sQ27_spl|~sQ23_spl)),
% 0.15/1.21 inference(forward_demodulation,[status(thm)],[f478,f440])).
% 0.15/1.21 fof(f508,plain,(
% 0.15/1.21 iminus4=iT|~sQ25_spl|~sQ6_spl|~sQ9_spl),
% 0.15/1.21 inference(resolution,[status(thm)],[f444,f367])).
% 0.15/1.21 fof(f509,plain,(
% 0.15/1.21 sQ13_spl|~sQ25_spl|~sQ6_spl|~sQ9_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f508,f268,f423,f242,f254])).
% 0.15/1.21 fof(f544,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iT|X0=iT|~sQ0_spl|~sQ14_spl)),
% 0.15/1.21 inference(forward_demodulation,[status(thm)],[f223,f346])).
% 0.15/1.21 fof(f545,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iT|~sQ0_spl|~sQ14_spl)),
% 0.15/1.21 inference(duplicate_literals_removal,[status(thm)],[f544])).
% 0.15/1.21 fof(f548,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iT|X0=iT|~sQ10_spl|~sQ3_spl)),
% 0.15/1.21 inference(forward_demodulation,[status(thm)],[f258,f344])).
% 0.15/1.21 fof(f549,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iT|~sQ10_spl|~sQ3_spl)),
% 0.15/1.21 inference(duplicate_literals_removal,[status(thm)],[f548])).
% 0.15/1.21 fof(f575,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iT|X0=iminus3|~sQ9_spl)),
% 0.15/1.21 inference(forward_demodulation,[status(thm)],[f255,f133])).
% 0.15/1.21 fof(f576,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iT|X0=iT|~sQ6_spl|~sQ9_spl)),
% 0.15/1.21 inference(forward_demodulation,[status(thm)],[f243,f575])).
% 0.15/1.21 fof(f577,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iT|~sQ6_spl|~sQ9_spl)),
% 0.15/1.21 inference(duplicate_literals_removal,[status(thm)],[f576])).
% 0.15/1.21 fof(f580,plain,(
% 0.15/1.21 iplus4=iT|~sQ1_spl|~sQ15_spl),
% 0.15/1.21 inference(resolution,[status(thm)],[f324,f369])).
% 0.15/1.21 fof(f581,plain,(
% 0.15/1.21 sQ11_spl|~sQ1_spl|~sQ15_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f580,f260,f225,f277])).
% 0.15/1.21 fof(f586,plain,(
% 0.15/1.21 iminus8=iT|~sQ6_spl|~sQ9_spl),
% 0.15/1.21 inference(resolution,[status(thm)],[f577,f336])).
% 0.15/1.21 fof(f587,plain,(
% 0.15/1.21 iplus4=iT|~sQ6_spl|~sQ9_spl),
% 0.15/1.21 inference(resolution,[status(thm)],[f577,f324])).
% 0.15/1.21 fof(f589,plain,(
% 0.15/1.21 sQ12_spl|~sQ6_spl|~sQ9_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f586,f265,f242,f254])).
% 0.15/1.21 fof(f590,plain,(
% 0.15/1.21 sQ11_spl|~sQ6_spl|~sQ9_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f587,f260,f242,f254])).
% 0.15/1.21 fof(f594,plain,(
% 0.15/1.21 iminus3=iT|~sQ16_spl|~sQ27_spl|~sQ23_spl),
% 0.15/1.21 inference(resolution,[status(thm)],[f480,f332])).
% 0.15/1.21 fof(f601,plain,(
% 0.15/1.21 sQ6_spl|~sQ16_spl|~sQ27_spl|~sQ23_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f594,f242,f289,f431,f400])).
% 0.15/1.21 fof(f615,plain,(
% 0.15/1.21 ~iT=iminus4|~sQ16_spl|sQ27_spl),
% 0.15/1.21 inference(forward_demodulation,[status(thm)],[f290,f433])).
% 0.15/1.21 fof(f616,plain,(
% 0.15/1.21 ~iT=iT|~sQ13_spl|~sQ16_spl|sQ27_spl),
% 0.15/1.21 inference(forward_demodulation,[status(thm)],[f269,f615])).
% 0.15/1.21 fof(f617,plain,(
% 0.15/1.21 $false|~sQ13_spl|~sQ16_spl|sQ27_spl),
% 0.15/1.21 inference(trivial_equality_resolution,[status(thm)],[f616])).
% 0.15/1.21 fof(f618,plain,(
% 0.15/1.21 ~sQ13_spl|~sQ16_spl|sQ27_spl),
% 0.15/1.21 inference(contradiction_clause,[status(thm)],[f617])).
% 0.15/1.21 fof(f624,plain,(
% 0.15/1.21 ~iT=iplus5|~sQ16_spl|sQ23_spl),
% 0.15/1.21 inference(forward_demodulation,[status(thm)],[f290,f402])).
% 0.15/1.21 fof(f625,plain,(
% 0.15/1.21 ~iT=iT|~sQ8_spl|~sQ16_spl|sQ23_spl),
% 0.15/1.21 inference(forward_demodulation,[status(thm)],[f250,f624])).
% 0.15/1.21 fof(f626,plain,(
% 0.15/1.21 $false|~sQ8_spl|~sQ16_spl|sQ23_spl),
% 0.15/1.21 inference(trivial_equality_resolution,[status(thm)],[f625])).
% 0.15/1.21 fof(f627,plain,(
% 0.15/1.21 ~sQ8_spl|~sQ16_spl|sQ23_spl),
% 0.15/1.21 inference(contradiction_clause,[status(thm)],[f626])).
% 0.15/1.21 fof(f633,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iT|X0=iminus7|~sQ7_spl)),
% 0.15/1.21 inference(forward_demodulation,[status(thm)],[f246,f123])).
% 0.15/1.21 fof(f637,plain,(
% 0.15/1.21 iminus3=iT|~sQ0_spl|~sQ14_spl),
% 0.15/1.21 inference(resolution,[status(thm)],[f545,f332])).
% 0.15/1.21 fof(f639,plain,(
% 0.15/1.21 iplus4=iT|~sQ0_spl|~sQ14_spl),
% 0.15/1.21 inference(resolution,[status(thm)],[f545,f324])).
% 0.15/1.21 fof(f642,plain,(
% 0.15/1.21 sQ6_spl|~sQ0_spl|~sQ14_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f637,f242,f222,f272])).
% 0.15/1.21 fof(f644,plain,(
% 0.15/1.21 sQ11_spl|~sQ0_spl|~sQ14_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f639,f260,f222,f272])).
% 0.15/1.21 fof(f649,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iT|X0=iT|~sQ4_spl|~sQ7_spl)),
% 0.15/1.21 inference(forward_demodulation,[status(thm)],[f236,f633])).
% 0.15/1.21 fof(f650,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iT|~sQ4_spl|~sQ7_spl)),
% 0.15/1.21 inference(duplicate_literals_removal,[status(thm)],[f649])).
% 0.15/1.21 fof(f708,plain,(
% 0.15/1.21 ~iminus4=iplus4|~sQ25_spl|sQ26_spl),
% 0.15/1.21 inference(forward_demodulation,[status(thm)],[f424,f428])).
% 0.15/1.21 fof(f709,plain,(
% 0.15/1.21 ~iminus4=iT|~sQ11_spl|~sQ25_spl|sQ26_spl),
% 0.15/1.21 inference(forward_demodulation,[status(thm)],[f261,f708])).
% 0.15/1.21 fof(f718,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iT|X0=iminus2|~sQ1_spl)),
% 0.15/1.21 inference(backward_demodulation,[status(thm)],[f226,f118])).
% 0.15/1.21 fof(f720,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iT|X0=iplus6|~sQ0_spl)),
% 0.15/1.21 inference(backward_demodulation,[status(thm)],[f223,f148])).
% 0.15/1.21 fof(f741,plain,(
% 0.15/1.21 sQ0_spl|~sQ5_spl|~sQ12_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f473,f222,f239,f265])).
% 0.15/1.21 fof(f811,plain,(
% 0.15/1.21 iminus8=iT|~sQ10_spl|~sQ3_spl),
% 0.15/1.21 inference(resolution,[status(thm)],[f549,f336])).
% 0.15/1.21 fof(f812,plain,(
% 0.15/1.21 iminus6=iT|~sQ10_spl|~sQ3_spl),
% 0.15/1.21 inference(resolution,[status(thm)],[f549,f337])).
% 0.15/1.21 fof(f814,plain,(
% 0.15/1.21 iminus4=iT|~sQ10_spl|~sQ3_spl),
% 0.15/1.21 inference(resolution,[status(thm)],[f549,f323])).
% 0.15/1.21 fof(f816,plain,(
% 0.15/1.21 sQ12_spl|~sQ10_spl|~sQ3_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f811,f265,f257,f232])).
% 0.15/1.21 fof(f817,plain,(
% 0.15/1.21 sQ0_spl|~sQ10_spl|~sQ3_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f812,f222,f257,f232])).
% 0.15/1.21 fof(f819,plain,(
% 0.15/1.21 sQ13_spl|~sQ10_spl|~sQ3_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f814,f268,f257,f232])).
% 0.15/1.21 fof(f821,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iT|X0=iT|~sQ15_spl|~sQ1_spl)),
% 0.15/1.21 inference(forward_demodulation,[status(thm)],[f278,f718])).
% 0.15/1.21 fof(f822,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iT|~sQ15_spl|~sQ1_spl)),
% 0.15/1.21 inference(duplicate_literals_removal,[status(thm)],[f821])).
% 0.15/1.21 fof(f842,plain,(
% 0.15/1.21 iminus4=iT|~sQ15_spl|~sQ1_spl),
% 0.15/1.21 inference(resolution,[status(thm)],[f822,f323])).
% 0.15/1.21 fof(f845,plain,(
% 0.15/1.21 sQ13_spl|~sQ15_spl|~sQ1_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f842,f268,f277,f225])).
% 0.15/1.21 fof(f847,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iT|X0=iT|~sQ14_spl|~sQ0_spl)),
% 0.15/1.21 inference(forward_demodulation,[status(thm)],[f273,f720])).
% 0.15/1.21 fof(f848,plain,(
% 0.15/1.21 ![X0]: (~cTorF(X0)|X0=iT|~sQ14_spl|~sQ0_spl)),
% 0.15/1.21 inference(duplicate_literals_removal,[status(thm)],[f847])).
% 0.15/1.21 fof(f883,plain,(
% 0.15/1.21 iplus9=iT|~sQ14_spl|~sQ0_spl),
% 0.15/1.21 inference(resolution,[status(thm)],[f848,f340])).
% 0.15/1.21 fof(f884,plain,(
% 0.15/1.21 iminus4=iT|~sQ14_spl|~sQ0_spl),
% 0.15/1.21 inference(resolution,[status(thm)],[f848,f323])).
% 0.15/1.21 fof(f886,plain,(
% 0.15/1.21 sQ3_spl|~sQ14_spl|~sQ0_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f883,f232,f272,f222])).
% 0.15/1.21 fof(f887,plain,(
% 0.15/1.21 sQ13_spl|~sQ14_spl|~sQ0_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f884,f268,f272,f222])).
% 0.15/1.21 fof(f896,plain,(
% 0.15/1.21 iplus9=iminus9|iplus9=iplus9),
% 0.15/1.21 inference(resolution,[status(thm)],[f153,f340])).
% 0.15/1.21 fof(f897,plain,(
% 0.15/1.21 iminus4=iminus9|iminus4=iplus9),
% 0.15/1.21 inference(resolution,[status(thm)],[f153,f323])).
% 0.15/1.21 fof(f898,plain,(
% 0.15/1.21 iT=iminus9|iT=iplus9),
% 0.15/1.21 inference(resolution,[status(thm)],[f153,f333])).
% 0.15/1.21 fof(f899,definition,(
% 0.15/1.21 sQ31_spl <=> (iplus9=iminus9)),
% 0.15/1.21 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.15/1.21 fof(f900,plain,(
% 0.15/1.21 iplus9=iminus9|~sQ31_spl),
% 0.15/1.21 inference(component_clause,[status(thm)],[f899])).
% 0.15/1.21 fof(f902,definition,(
% 0.15/1.21 sQ32_spl <=> (iplus9=iplus9)),
% 0.15/1.21 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.15/1.21 fof(f905,plain,(
% 0.15/1.21 sQ31_spl|sQ32_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f896,f899,f902])).
% 0.15/1.21 fof(f906,definition,(
% 0.15/1.21 sQ33_spl <=> (iminus4=iminus9)),
% 0.15/1.21 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.15/1.21 fof(f907,plain,(
% 0.15/1.21 iminus4=iminus9|~sQ33_spl),
% 0.15/1.21 inference(component_clause,[status(thm)],[f906])).
% 0.15/1.21 fof(f909,definition,(
% 0.15/1.21 sQ34_spl <=> (iminus4=iplus9)),
% 0.15/1.21 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.15/1.21 fof(f910,plain,(
% 0.15/1.21 iminus4=iplus9|~sQ34_spl),
% 0.15/1.21 inference(component_clause,[status(thm)],[f909])).
% 0.15/1.21 fof(f912,plain,(
% 0.15/1.21 sQ33_spl|sQ34_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f897,f906,f909])).
% 0.15/1.21 fof(f913,plain,(
% 0.15/1.21 sQ10_spl|sQ3_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f898,f257,f232])).
% 0.15/1.21 fof(f917,plain,(
% 0.15/1.21 iplus9=iminus4|~sQ33_spl|~sQ31_spl),
% 0.15/1.21 inference(forward_demodulation,[status(thm)],[f907,f900])).
% 0.15/1.21 fof(f918,plain,(
% 0.15/1.21 iT=iminus4|~sQ3_spl|~sQ33_spl|~sQ31_spl),
% 0.15/1.21 inference(backward_demodulation,[status(thm)],[f233,f917])).
% 0.15/1.21 fof(f922,plain,(
% 0.15/1.21 sQ13_spl|~sQ3_spl|~sQ33_spl|~sQ31_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f918,f268,f232,f906,f899])).
% 0.15/1.21 fof(f923,plain,(
% 0.15/1.21 iminus4=iT|~sQ3_spl|~sQ34_spl),
% 0.15/1.21 inference(forward_demodulation,[status(thm)],[f233,f910])).
% 0.15/1.21 fof(f924,plain,(
% 0.15/1.21 $false|~sQ11_spl|~sQ25_spl|sQ26_spl|~sQ3_spl|~sQ34_spl),
% 0.15/1.21 inference(forward_subsumption_resolution,[status(thm)],[f923,f709])).
% 0.15/1.21 fof(f925,plain,(
% 0.15/1.21 ~sQ11_spl|~sQ25_spl|sQ26_spl|~sQ3_spl|~sQ34_spl),
% 0.15/1.21 inference(contradiction_clause,[status(thm)],[f924])).
% 0.15/1.21 fof(f1010,plain,(
% 0.15/1.21 iminus6=iT|~sQ4_spl|~sQ7_spl),
% 0.15/1.21 inference(resolution,[status(thm)],[f650,f337])).
% 0.15/1.21 fof(f1011,plain,(
% 0.15/1.21 iplus8=iT|~sQ4_spl|~sQ7_spl),
% 0.15/1.21 inference(resolution,[status(thm)],[f650,f335])).
% 0.15/1.21 fof(f1013,plain,(
% 0.15/1.21 iminus4=iT|~sQ4_spl|~sQ7_spl),
% 0.15/1.21 inference(resolution,[status(thm)],[f650,f323])).
% 0.15/1.21 fof(f1015,plain,(
% 0.15/1.21 sQ0_spl|~sQ4_spl|~sQ7_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f1010,f222,f235,f245])).
% 0.15/1.21 fof(f1016,plain,(
% 0.15/1.21 sQ5_spl|~sQ4_spl|~sQ7_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f1011,f239,f235,f245])).
% 0.15/1.21 fof(f1018,plain,(
% 0.15/1.21 sQ13_spl|~sQ4_spl|~sQ7_spl),
% 0.15/1.21 inference(split_clause,[status(thm)],[f1013,f268,f235,f245])).
% 0.15/1.21 fof(f1019,plain,(
% 0.15/1.21 $false),
% 0.15/1.21 inference(sat_refutation,[status(thm)],[f238,f248,f263,f271,f275,f281,f282,f283,f284,f287,f295,f301,f302,f304,f307,f308,f311,f317,f318,f320,f417,f429,f430,f454,f463,f477,f509,f581,f589,f590,f601,f618,f627,f642,f644,f741,f816,f817,f819,f845,f886,f887,f905,f912,f913,f922,f925,f1015,f1016,f1018])).
% 0.15/1.21 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/1.22 % Elapsed time: 0.043085 seconds
% 0.15/1.22 % CPU time: 0.177892 seconds
% 0.15/1.22 % Total memory used: 8.367 MB
% 0.15/1.22 % Net memory used: 8.231 MB
%------------------------------------------------------------------------------