%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : COM003+2 : TPTP v9.3.1. Bugfixed v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.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 12:10:41 PM UTC 2026
% Result : Theorem 0.19s 0.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : COM003+2 : TPTP v9.3.1. Bugfixed v2.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.39 % Computer : n001.cluster.edu
% 0.14/0.39 % Model : x86_64 x86_64
% 0.14/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.39 % Memory : 8046.5625MB
% 0.14/0.39 % OS : Linux 6.8.0-71-generic
% 0.14/0.39 % CPULimit : 300
% 0.14/0.39 % WCLimit : 300
% 0.14/0.39 % DateTime : Mon Sep 21 14:19:29 UTC 2026
% 0.14/0.39 % CPUTime :
% 0.14/0.42 % Drodi V4.1.1
% 0.19/0.45 % Refutation found
% 0.19/0.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.19/0.45 % SZS output start CNFRefutation for theBenchmark
% 0.19/0.45 fof(f2,axiom,(
% 0.19/0.45 (! [X] :( program_program_decides(X)<=> ( program(X)& program_decides(X) ) ) )),
% 0.19/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.45 fof(f4,axiom,(
% 0.19/0.45 (! [X,Y] :( program_halts2(X,Y)<=> ( program(X)& halts2(X,Y) ) ) )),
% 0.19/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.45 fof(f6,axiom,(
% 0.19/0.45 (! [X,Y] :( program_not_halts2(X,Y)<=> ( program(X)& ~ halts2(X,Y) ) ) )),
% 0.19/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.45 fof(f7,axiom,(
% 0.19/0.45 (! [X,Y,W] :( halts2_outputs(X,Y,W)<=> ( halts2(X,Y)& outputs(X,W) ) ) )),
% 0.19/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.45 fof(f11,axiom,(
% 0.19/0.45 (! [X,Y,W] :( program_not_halts2_halts2_outputs(X,Y,W)<=> ( program_not_halts2(Y,Y)=> halts2_outputs(X,Y,W) ) ) )),
% 0.19/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.45 fof(f12,axiom,(
% 0.19/0.45 ( (? [X] : algorithm_program_decides(X))=> (? [W] : program_program_decides(W) )) ),
% 0.19/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.45 fof(f13,axiom,(
% 0.19/0.45 (! [W] :( program_program_decides(W)=> (! [Y,Z] :( program_halts2_halts3_outputs(W,Y,Z,good)& program_not_halts2_halts3_outputs(W,Y,Z,bad) ) )) )),
% 0.19/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.45 fof(f14,axiom,(
% 0.19/0.45 ( (? [W] :( program(W)& (! [Y] :( program_halts2_halts3_outputs(W,Y,Y,good)& program_not_halts2_halts3_outputs(W,Y,Y,bad) ) )))=> (? [V] :( program(V)& (! [Y] :( program_halts2_halts2_outputs(V,Y,good)& program_not_halts2_halts2_outputs(V,Y,bad) ) )) )) ),
% 0.19/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.45 fof(f15,axiom,(
% 0.19/0.45 ( (? [V] :( program(V)& (! [Y] :( program_halts2_halts2_outputs(V,Y,good)& program_not_halts2_halts2_outputs(V,Y,bad) ) )))=> (? [U] :( program(U)& (! [Y] :( ( program_halts2(Y,Y)=> ~ halts2(U,Y) )& program_not_halts2_halts2_outputs(U,Y,good) ) )) )) ),
% 0.19/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.45 fof(f16,conjecture,(
% 0.19/0.45 ~ (? [X] : algorithm_program_decides(X) )),
% 0.19/0.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.19/0.45 fof(f17,negated_conjecture,(
% 0.19/0.45 ~(~ (? [X] : algorithm_program_decides(X) ))),
% 0.19/0.45 inference(negated_conjecture,[status(cth)],[f16])).
% 0.19/0.45 fof(f25,plain,(
% 0.19/0.45 ![X]: ((~program_program_decides(X)|(program(X)&program_decides(X)))&(program_program_decides(X)|(~program(X)|~program_decides(X))))),
% 0.19/0.45 inference(NNF_transformation,[status(thm)],[f2])).
% 0.19/0.45 fof(f26,plain,(
% 0.19/0.45 (![X]: (~program_program_decides(X)|(program(X)&program_decides(X))))&(![X]: (program_program_decides(X)|(~program(X)|~program_decides(X))))),
% 0.19/0.45 inference(miniscoping,[status(thm)],[f25])).
% 0.19/0.45 fof(f27,plain,(
% 0.19/0.45 ![X0]: (~program_program_decides(X0)|program(X0))),
% 0.19/0.45 inference(cnf_transformation,[status(thm)],[f26])).
% 0.19/0.45 fof(f35,plain,(
% 0.19/0.45 ![X,Y]: ((~program_halts2(X,Y)|(program(X)&halts2(X,Y)))&(program_halts2(X,Y)|(~program(X)|~halts2(X,Y))))),
% 0.19/0.45 inference(NNF_transformation,[status(thm)],[f4])).
% 0.19/0.45 fof(f36,plain,(
% 0.19/0.45 (![X,Y]: (~program_halts2(X,Y)|(program(X)&halts2(X,Y))))&(![X,Y]: (program_halts2(X,Y)|(~program(X)|~halts2(X,Y))))),
% 0.19/0.45 inference(miniscoping,[status(thm)],[f35])).
% 0.19/0.45 fof(f38,plain,(
% 0.19/0.45 ![X0,X1]: (~program_halts2(X0,X1)|halts2(X0,X1))),
% 0.19/0.45 inference(cnf_transformation,[status(thm)],[f36])).
% 0.19/0.45 fof(f39,plain,(
% 0.19/0.45 ![X0,X1]: (program_halts2(X0,X1)|~program(X0)|~halts2(X0,X1))),
% 0.19/0.45 inference(cnf_transformation,[status(thm)],[f36])).
% 0.19/0.45 fof(f45,plain,(
% 0.19/0.45 ![X,Y]: ((~program_not_halts2(X,Y)|(program(X)&~halts2(X,Y)))&(program_not_halts2(X,Y)|(~program(X)|halts2(X,Y))))),
% 0.19/0.45 inference(NNF_transformation,[status(thm)],[f6])).
% 0.19/0.45 fof(f46,plain,(
% 0.19/0.45 (![X,Y]: (~program_not_halts2(X,Y)|(program(X)&~halts2(X,Y))))&(![X,Y]: (program_not_halts2(X,Y)|(~program(X)|halts2(X,Y))))),
% 0.19/0.45 inference(miniscoping,[status(thm)],[f45])).
% 0.19/0.45 fof(f49,plain,(
% 0.19/0.45 ![X0,X1]: (program_not_halts2(X0,X1)|~program(X0)|halts2(X0,X1))),
% 0.19/0.45 inference(cnf_transformation,[status(thm)],[f46])).
% 0.19/0.45 fof(f50,plain,(
% 0.19/0.45 ![X,Y,W]: ((~halts2_outputs(X,Y,W)|(halts2(X,Y)&outputs(X,W)))&(halts2_outputs(X,Y,W)|(~halts2(X,Y)|~outputs(X,W))))),
% 0.19/0.45 inference(NNF_transformation,[status(thm)],[f7])).
% 0.19/0.45 fof(f51,plain,(
% 0.19/0.45 (![X,Y,W]: (~halts2_outputs(X,Y,W)|(halts2(X,Y)&outputs(X,W))))&(![X,Y,W]: (halts2_outputs(X,Y,W)|(~halts2(X,Y)|~outputs(X,W))))),
% 0.19/0.45 inference(miniscoping,[status(thm)],[f50])).
% 0.19/0.45 fof(f52,plain,(
% 0.19/0.45 ![X0,X1,X2]: (~halts2_outputs(X0,X1,X2)|halts2(X0,X1))),
% 0.19/0.45 inference(cnf_transformation,[status(thm)],[f51])).
% 0.19/0.45 fof(f73,plain,(
% 0.19/0.45 ![X,Y,W]: (program_not_halts2_halts2_outputs(X,Y,W)<=>(~program_not_halts2(Y,Y)|halts2_outputs(X,Y,W)))),
% 0.19/0.45 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 0.19/0.45 fof(f74,plain,(
% 0.19/0.45 ![X,Y,W]: ((~program_not_halts2_halts2_outputs(X,Y,W)|(~program_not_halts2(Y,Y)|halts2_outputs(X,Y,W)))&(program_not_halts2_halts2_outputs(X,Y,W)|(program_not_halts2(Y,Y)&~halts2_outputs(X,Y,W))))),
% 0.19/0.45 inference(NNF_transformation,[status(thm)],[f73])).
% 0.19/0.45 fof(f75,plain,(
% 0.19/0.45 (![X,Y,W]: (~program_not_halts2_halts2_outputs(X,Y,W)|(~program_not_halts2(Y,Y)|halts2_outputs(X,Y,W))))&(![X,Y,W]: (program_not_halts2_halts2_outputs(X,Y,W)|(program_not_halts2(Y,Y)&~halts2_outputs(X,Y,W))))),
% 0.19/0.45 inference(miniscoping,[status(thm)],[f74])).
% 0.19/0.45 fof(f76,plain,(
% 0.19/0.45 ![X0,X1,X2]: (~program_not_halts2_halts2_outputs(X0,X1,X2)|~program_not_halts2(X1,X1)|halts2_outputs(X0,X1,X2))),
% 0.19/0.45 inference(cnf_transformation,[status(thm)],[f75])).
% 0.19/0.45 fof(f79,plain,(
% 0.19/0.45 (![X]: ~algorithm_program_decides(X))|(?[W]: program_program_decides(W))),
% 0.19/0.45 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.19/0.45 fof(f80,plain,(
% 0.19/0.45 (![X]: ~algorithm_program_decides(X))|program_program_decides(sK2_skl)),
% 0.19/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(W,sK2_skl)],[f79])).
% 0.19/0.45 fof(f81,plain,(
% 0.19/0.45 ![X0]: (~algorithm_program_decides(X0)|program_program_decides(sK2_skl))),
% 0.19/0.45 inference(cnf_transformation,[status(thm)],[f80])).
% 0.19/0.45 fof(f82,plain,(
% 0.19/0.45 ![W]: (~program_program_decides(W)|(![Y,Z]: (program_halts2_halts3_outputs(W,Y,Z,good)&program_not_halts2_halts3_outputs(W,Y,Z,bad))))),
% 0.19/0.45 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.19/0.45 fof(f83,plain,(
% 0.19/0.45 ![W]: (~program_program_decides(W)|((![Y,Z]: program_halts2_halts3_outputs(W,Y,Z,good))&(![Y,Z]: program_not_halts2_halts3_outputs(W,Y,Z,bad))))),
% 0.19/0.45 inference(miniscoping,[status(thm)],[f82])).
% 0.19/0.45 fof(f84,plain,(
% 0.19/0.45 ![X0,X1,X2]: (~program_program_decides(X0)|program_halts2_halts3_outputs(X0,X1,X2,good))),
% 0.19/0.45 inference(cnf_transformation,[status(thm)],[f83])).
% 0.19/0.45 fof(f85,plain,(
% 0.19/0.45 ![X0,X1,X2]: (~program_program_decides(X0)|program_not_halts2_halts3_outputs(X0,X1,X2,bad))),
% 0.19/0.45 inference(cnf_transformation,[status(thm)],[f83])).
% 0.19/0.45 fof(f86,plain,(
% 0.19/0.45 (![W]: (~program(W)|(?[Y]: (~program_halts2_halts3_outputs(W,Y,Y,good)|~program_not_halts2_halts3_outputs(W,Y,Y,bad)))))|(?[V]: (program(V)&(![Y]: (program_halts2_halts2_outputs(V,Y,good)&program_not_halts2_halts2_outputs(V,Y,bad)))))),
% 0.19/0.45 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.19/0.45 fof(f87,plain,(
% 0.19/0.45 (![W]: (~program(W)|((?[Y]: ~program_halts2_halts3_outputs(W,Y,Y,good))|(?[Y]: ~program_not_halts2_halts3_outputs(W,Y,Y,bad)))))|(?[V]: (program(V)&((![Y]: program_halts2_halts2_outputs(V,Y,good))&(![Y]: program_not_halts2_halts2_outputs(V,Y,bad)))))),
% 0.19/0.45 inference(miniscoping,[status(thm)],[f86])).
% 0.19/0.45 fof(f88,plain,(
% 0.19/0.45 (![W]: (~program(W)|(~program_halts2_halts3_outputs(W,sK3_skl(W),sK3_skl(W),good)|~program_not_halts2_halts3_outputs(W,sK4_skl(W),sK4_skl(W),bad))))|(program(sK5_skl)&((![Y]: program_halts2_halts2_outputs(sK5_skl,Y,good))&(![Y]: program_not_halts2_halts2_outputs(sK5_skl,Y,bad))))),
% 0.19/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl,sK5_skl]),skolemize(Y,sK3_skl(W)),skolemize(Y,sK4_skl(W)),skolemize(V,sK5_skl)],[f87])).
% 0.19/0.45 fof(f89,plain,(
% 0.19/0.45 ![X0]: (~program(X0)|~program_halts2_halts3_outputs(X0,sK3_skl(X0),sK3_skl(X0),good)|~program_not_halts2_halts3_outputs(X0,sK4_skl(X0),sK4_skl(X0),bad)|program(sK5_skl))),
% 0.19/0.45 inference(cnf_transformation,[status(thm)],[f88])).
% 0.19/0.45 fof(f90,plain,(
% 0.19/0.45 ![X0,X1]: (~program(X0)|~program_halts2_halts3_outputs(X0,sK3_skl(X0),sK3_skl(X0),good)|~program_not_halts2_halts3_outputs(X0,sK4_skl(X0),sK4_skl(X0),bad)|program_halts2_halts2_outputs(sK5_skl,X1,good))),
% 0.19/0.45 inference(cnf_transformation,[status(thm)],[f88])).
% 0.19/0.45 fof(f91,plain,(
% 0.19/0.45 ![X0,X1]: (~program(X0)|~program_halts2_halts3_outputs(X0,sK3_skl(X0),sK3_skl(X0),good)|~program_not_halts2_halts3_outputs(X0,sK4_skl(X0),sK4_skl(X0),bad)|program_not_halts2_halts2_outputs(sK5_skl,X1,bad))),
% 0.19/0.45 inference(cnf_transformation,[status(thm)],[f88])).
% 0.19/0.45 fof(f92,plain,(
% 0.19/0.45 (![V]: (~program(V)|(?[Y]: (~program_halts2_halts2_outputs(V,Y,good)|~program_not_halts2_halts2_outputs(V,Y,bad)))))|(?[U]: (program(U)&(![Y]: ((~program_halts2(Y,Y)|~halts2(U,Y))&program_not_halts2_halts2_outputs(U,Y,good)))))),
% 0.19/0.45 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.19/0.45 fof(f93,plain,(
% 0.19/0.45 (![V]: (~program(V)|((?[Y]: ~program_halts2_halts2_outputs(V,Y,good))|(?[Y]: ~program_not_halts2_halts2_outputs(V,Y,bad)))))|(?[U]: (program(U)&((![Y]: (~program_halts2(Y,Y)|~halts2(U,Y)))&(![Y]: program_not_halts2_halts2_outputs(U,Y,good)))))),
% 0.19/0.45 inference(miniscoping,[status(thm)],[f92])).
% 0.19/0.45 fof(f94,plain,(
% 0.19/0.45 (![V]: (~program(V)|(~program_halts2_halts2_outputs(V,sK6_skl(V),good)|~program_not_halts2_halts2_outputs(V,sK7_skl(V),bad))))|(program(sK8_skl)&((![Y]: (~program_halts2(Y,Y)|~halts2(sK8_skl,Y)))&(![Y]: program_not_halts2_halts2_outputs(sK8_skl,Y,good))))),
% 0.19/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl,sK7_skl,sK8_skl]),skolemize(Y,sK6_skl(V)),skolemize(Y,sK7_skl(V)),skolemize(U,sK8_skl)],[f93])).
% 0.19/0.45 fof(f95,plain,(
% 0.19/0.45 ![X0]: (~program(X0)|~program_halts2_halts2_outputs(X0,sK6_skl(X0),good)|~program_not_halts2_halts2_outputs(X0,sK7_skl(X0),bad)|program(sK8_skl))),
% 0.19/0.45 inference(cnf_transformation,[status(thm)],[f94])).
% 0.19/0.45 fof(f96,plain,(
% 0.19/0.45 ![X0,X1]: (~program(X0)|~program_halts2_halts2_outputs(X0,sK6_skl(X0),good)|~program_not_halts2_halts2_outputs(X0,sK7_skl(X0),bad)|~program_halts2(X1,X1)|~halts2(sK8_skl,X1))),
% 0.19/0.45 inference(cnf_transformation,[status(thm)],[f94])).
% 0.19/0.45 fof(f97,plain,(
% 0.19/0.45 ![X0,X1]: (~program(X0)|~program_halts2_halts2_outputs(X0,sK6_skl(X0),good)|~program_not_halts2_halts2_outputs(X0,sK7_skl(X0),bad)|program_not_halts2_halts2_outputs(sK8_skl,X1,good))),
% 0.19/0.45 inference(cnf_transformation,[status(thm)],[f94])).
% 0.19/0.45 fof(f98,plain,(
% 0.19/0.45 algorithm_program_decides(sK9_skl)),
% 0.19/0.45 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(X,sK9_skl)],[f17])).
% 0.19/0.45 fof(f99,plain,(
% 0.19/0.45 algorithm_program_decides(sK9_skl)),
% 0.19/0.45 inference(cnf_transformation,[status(thm)],[f98])).
% 0.19/0.45 fof(f100,definition,(
% 0.19/0.45 ![X0]: (sQ0_spl <=> (~algorithm_program_decides(X0)))),
% 0.19/0.45 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.19/0.45 fof(f101,plain,(
% 0.19/0.45 ![X0]: (~algorithm_program_decides(X0)|~sQ0_spl)),
% 0.19/0.45 inference(component_clause,[status(thm)],[f100])).
% 0.19/0.45 fof(f103,definition,(
% 0.19/0.45 sQ1_spl <=> (program_program_decides(sK2_skl))),
% 0.19/0.45 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.19/0.45 fof(f104,plain,(
% 0.19/0.45 program_program_decides(sK2_skl)|~sQ1_spl),
% 0.19/0.45 inference(component_clause,[status(thm)],[f103])).
% 0.19/0.45 fof(f106,plain,(
% 0.19/0.45 sQ0_spl|sQ1_spl),
% 0.19/0.45 inference(split_clause,[status(thm)],[f81,f100,f103])).
% 0.19/0.45 fof(f107,definition,(
% 0.19/0.45 ![X0]: (sQ2_spl <=> (~program(X0)|~program_halts2_halts3_outputs(X0,sK3_skl(X0),sK3_skl(X0),good)|~program_not_halts2_halts3_outputs(X0,sK4_skl(X0),sK4_skl(X0),bad)))),
% 0.19/0.45 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.19/0.45 fof(f108,plain,(
% 0.19/0.45 ![X0]: (~program(X0)|~program_halts2_halts3_outputs(X0,sK3_skl(X0),sK3_skl(X0),good)|~program_not_halts2_halts3_outputs(X0,sK4_skl(X0),sK4_skl(X0),bad)|~sQ2_spl)),
% 0.19/0.45 inference(component_clause,[status(thm)],[f107])).
% 0.19/0.45 fof(f110,definition,(
% 0.19/0.45 sQ3_spl <=> (program(sK5_skl))),
% 0.19/0.45 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.19/0.45 fof(f113,plain,(
% 0.19/0.45 sQ2_spl|sQ3_spl),
% 0.19/0.45 inference(split_clause,[status(thm)],[f89,f107,f110])).
% 0.19/0.45 fof(f114,definition,(
% 0.19/0.45 ![X1]: (sQ4_spl <=> (program_halts2_halts2_outputs(sK5_skl,X1,good)))),
% 0.19/0.45 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.19/0.45 fof(f115,plain,(
% 0.19/0.45 ![X0]: (program_halts2_halts2_outputs(sK5_skl,X0,good)|~sQ4_spl)),
% 0.19/0.45 inference(component_clause,[status(thm)],[f114])).
% 0.19/0.45 fof(f117,plain,(
% 0.19/0.45 sQ2_spl|sQ4_spl),
% 0.19/0.45 inference(split_clause,[status(thm)],[f90,f107,f114])).
% 0.19/0.45 fof(f118,definition,(
% 0.19/0.45 ![X1]: (sQ5_spl <=> (program_not_halts2_halts2_outputs(sK5_skl,X1,bad)))),
% 0.19/0.45 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.19/0.45 fof(f119,plain,(
% 0.19/0.45 ![X0]: (program_not_halts2_halts2_outputs(sK5_skl,X0,bad)|~sQ5_spl)),
% 0.19/0.45 inference(component_clause,[status(thm)],[f118])).
% 0.19/0.45 fof(f121,plain,(
% 0.19/0.45 sQ2_spl|sQ5_spl),
% 0.19/0.45 inference(split_clause,[status(thm)],[f91,f107,f118])).
% 0.19/0.45 fof(f122,definition,(
% 0.19/0.45 ![X0]: (sQ6_spl <=> (~program(X0)|~program_halts2_halts2_outputs(X0,sK6_skl(X0),good)|~program_not_halts2_halts2_outputs(X0,sK7_skl(X0),bad)))),
% 0.19/0.45 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.19/0.45 fof(f123,plain,(
% 0.19/0.45 ![X0]: (~program(X0)|~program_halts2_halts2_outputs(X0,sK6_skl(X0),good)|~program_not_halts2_halts2_outputs(X0,sK7_skl(X0),bad)|~sQ6_spl)),
% 0.19/0.45 inference(component_clause,[status(thm)],[f122])).
% 0.19/0.45 fof(f125,definition,(
% 0.19/0.45 sQ7_spl <=> (program(sK8_skl))),
% 0.19/0.45 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.19/0.45 fof(f126,plain,(
% 0.19/0.45 program(sK8_skl)|~sQ7_spl),
% 0.19/0.45 inference(component_clause,[status(thm)],[f125])).
% 0.19/0.45 fof(f128,plain,(
% 0.19/0.45 sQ6_spl|sQ7_spl),
% 0.19/0.45 inference(split_clause,[status(thm)],[f95,f122,f125])).
% 0.19/0.45 fof(f129,definition,(
% 0.19/0.45 ![X1]: (sQ8_spl <=> (~program_halts2(X1,X1)|~halts2(sK8_skl,X1)))),
% 0.19/0.45 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.19/0.45 fof(f130,plain,(
% 0.19/0.45 ![X0]: (~program_halts2(X0,X0)|~halts2(sK8_skl,X0)|~sQ8_spl)),
% 0.19/0.45 inference(component_clause,[status(thm)],[f129])).
% 0.19/0.45 fof(f132,plain,(
% 0.19/0.45 sQ6_spl|sQ8_spl),
% 0.19/0.45 inference(split_clause,[status(thm)],[f96,f122,f129])).
% 0.19/0.45 fof(f133,definition,(
% 0.19/0.45 ![X1]: (sQ9_spl <=> (program_not_halts2_halts2_outputs(sK8_skl,X1,good)))),
% 0.19/0.45 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.19/0.45 fof(f134,plain,(
% 0.19/0.45 ![X0]: (program_not_halts2_halts2_outputs(sK8_skl,X0,good)|~sQ9_spl)),
% 0.19/0.45 inference(component_clause,[status(thm)],[f133])).
% 0.19/0.45 fof(f136,plain,(
% 0.19/0.45 sQ6_spl|sQ9_spl),
% 0.19/0.45 inference(split_clause,[status(thm)],[f97,f122,f133])).
% 0.19/0.45 fof(f138,plain,(
% 0.19/0.45 $false|~sQ0_spl),
% 0.19/0.45 inference(backward_subsumption_resolution,[status(thm)],[f99,f101])).
% 0.19/0.45 fof(f139,plain,(
% 0.19/0.45 ~sQ0_spl),
% 0.19/0.45 inference(contradiction_clause,[status(thm)],[f138])).
% 0.19/0.45 fof(f141,plain,(
% 0.19/0.45 program(sK2_skl)|~sQ1_spl),
% 0.19/0.45 inference(resolution,[status(thm)],[f27,f104])).
% 0.19/0.45 fof(f217,plain,(
% 0.19/0.45 ~program_halts2_halts3_outputs(sK2_skl,sK3_skl(sK2_skl),sK3_skl(sK2_skl),good)|~program_not_halts2_halts3_outputs(sK2_skl,sK4_skl(sK2_skl),sK4_skl(sK2_skl),bad)|~sQ2_spl|~sQ1_spl),
% 0.19/0.45 inference(resolution,[status(thm)],[f108,f141])).
% 0.19/0.45 fof(f218,definition,(
% 0.19/0.45 sQ19_spl <=> (program_halts2_halts3_outputs(sK2_skl,sK3_skl(sK2_skl),sK3_skl(sK2_skl),good))),
% 0.19/0.45 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.19/0.45 fof(f220,plain,(
% 0.19/0.45 ~program_halts2_halts3_outputs(sK2_skl,sK3_skl(sK2_skl),sK3_skl(sK2_skl),good)|sQ19_spl),
% 0.19/0.45 inference(component_clause,[status(thm)],[f218])).
% 0.19/0.45 fof(f221,definition,(
% 0.19/0.45 sQ20_spl <=> (program_not_halts2_halts3_outputs(sK2_skl,sK4_skl(sK2_skl),sK4_skl(sK2_skl),bad))),
% 0.19/0.45 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.19/0.45 fof(f223,plain,(
% 0.19/0.45 ~program_not_halts2_halts3_outputs(sK2_skl,sK4_skl(sK2_skl),sK4_skl(sK2_skl),bad)|sQ20_spl),
% 0.19/0.45 inference(component_clause,[status(thm)],[f221])).
% 0.19/0.45 fof(f224,plain,(
% 0.19/0.45 ~sQ19_spl|~sQ20_spl|~sQ2_spl|~sQ1_spl),
% 0.19/0.45 inference(split_clause,[status(thm)],[f217,f218,f221,f107,f103])).
% 0.19/0.45 fof(f279,plain,(
% 0.19/0.45 ![X0]: (program_not_halts2(sK8_skl,X0)|halts2(sK8_skl,X0)|~sQ7_spl)),
% 0.19/0.45 inference(resolution,[status(thm)],[f126,f49])).
% 0.19/0.45 fof(f282,plain,(
% 0.19/0.45 ![X0]: (~program_halts2(X0,X0)|~program_halts2(sK8_skl,X0)|~sQ8_spl)),
% 0.19/0.45 inference(resolution,[status(thm)],[f130,f38])).
% 0.19/0.45 fof(f302,plain,(
% 0.19/0.45 ~program(sK5_skl)|~program_not_halts2_halts2_outputs(sK5_skl,sK7_skl(sK5_skl),bad)|~sQ6_spl|~sQ4_spl),
% 0.19/0.45 inference(resolution,[status(thm)],[f123,f115])).
% 0.19/0.45 fof(f306,definition,(
% 0.19/0.45 sQ30_spl <=> (program_not_halts2_halts2_outputs(sK5_skl,sK7_skl(sK5_skl),bad))),
% 0.19/0.46 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.19/0.46 fof(f308,plain,(
% 0.19/0.46 ~program_not_halts2_halts2_outputs(sK5_skl,sK7_skl(sK5_skl),bad)|sQ30_spl),
% 0.19/0.46 inference(component_clause,[status(thm)],[f306])).
% 0.19/0.46 fof(f309,plain,(
% 0.19/0.46 ~sQ3_spl|~sQ30_spl|~sQ6_spl|~sQ4_spl),
% 0.19/0.46 inference(split_clause,[status(thm)],[f302,f110,f306,f122,f114])).
% 0.19/0.46 fof(f316,definition,(
% 0.19/0.46 sQ31_spl <=> (program_halts2(sK8_skl,sK8_skl))),
% 0.19/0.46 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.19/0.46 fof(f317,plain,(
% 0.19/0.46 program_halts2(sK8_skl,sK8_skl)|~sQ31_spl),
% 0.19/0.46 inference(component_clause,[status(thm)],[f316])).
% 0.19/0.46 fof(f341,plain,(
% 0.19/0.46 ![X0,X1]: (halts2(sK8_skl,sK8_skl)|~program_not_halts2_halts2_outputs(X0,sK8_skl,X1)|halts2_outputs(X0,sK8_skl,X1)|~sQ7_spl)),
% 0.19/0.46 inference(resolution,[status(thm)],[f279,f76])).
% 0.19/0.46 fof(f345,definition,(
% 0.19/0.46 sQ35_spl <=> (halts2(sK8_skl,sK8_skl))),
% 0.19/0.46 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.19/0.46 fof(f346,plain,(
% 0.19/0.46 halts2(sK8_skl,sK8_skl)|~sQ35_spl),
% 0.19/0.46 inference(component_clause,[status(thm)],[f345])).
% 0.19/0.46 fof(f348,definition,(
% 0.19/0.46 ![X0,X1]: (sQ36_spl <=> (~program_not_halts2_halts2_outputs(X0,sK8_skl,X1)|halts2_outputs(X0,sK8_skl,X1)))),
% 0.19/0.46 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.19/0.46 fof(f349,plain,(
% 0.19/0.46 ![X0,X1]: (~program_not_halts2_halts2_outputs(X0,sK8_skl,X1)|halts2_outputs(X0,sK8_skl,X1)|~sQ36_spl)),
% 0.19/0.46 inference(component_clause,[status(thm)],[f348])).
% 0.19/0.46 fof(f351,plain,(
% 0.19/0.46 sQ35_spl|sQ36_spl|~sQ7_spl),
% 0.19/0.46 inference(split_clause,[status(thm)],[f341,f345,f348,f125])).
% 0.19/0.46 fof(f357,plain,(
% 0.19/0.46 program_halts2(sK8_skl,sK8_skl)|~program(sK8_skl)|~sQ35_spl),
% 0.19/0.46 inference(resolution,[status(thm)],[f346,f39])).
% 0.19/0.46 fof(f358,plain,(
% 0.19/0.46 sQ31_spl|~sQ7_spl|~sQ35_spl),
% 0.19/0.46 inference(split_clause,[status(thm)],[f357,f316,f125,f345])).
% 0.19/0.46 fof(f359,plain,(
% 0.19/0.46 ~program_halts2(sK8_skl,sK8_skl)|~sQ31_spl|~sQ8_spl),
% 0.19/0.46 inference(resolution,[status(thm)],[f317,f282])).
% 0.19/0.46 fof(f363,plain,(
% 0.19/0.46 ~sQ31_spl|~sQ8_spl),
% 0.19/0.46 inference(split_clause,[status(thm)],[f359,f316,f129])).
% 0.19/0.46 fof(f419,plain,(
% 0.19/0.46 $false|~sQ5_spl|sQ30_spl),
% 0.19/0.46 inference(forward_subsumption_resolution,[status(thm)],[f308,f119])).
% 0.19/0.46 fof(f420,plain,(
% 0.19/0.46 ~sQ5_spl|sQ30_spl),
% 0.19/0.46 inference(contradiction_clause,[status(thm)],[f419])).
% 0.19/0.46 fof(f440,plain,(
% 0.19/0.46 halts2_outputs(sK8_skl,sK8_skl,good)|~sQ36_spl|~sQ9_spl),
% 0.19/0.46 inference(resolution,[status(thm)],[f349,f134])).
% 0.19/0.46 fof(f473,plain,(
% 0.19/0.46 halts2(sK8_skl,sK8_skl)|~sQ36_spl|~sQ9_spl),
% 0.19/0.46 inference(resolution,[status(thm)],[f440,f52])).
% 0.19/0.46 fof(f474,plain,(
% 0.19/0.46 sQ35_spl|~sQ36_spl|~sQ9_spl),
% 0.19/0.46 inference(split_clause,[status(thm)],[f473,f345,f348,f133])).
% 0.19/0.46 fof(f655,plain,(
% 0.19/0.46 ~program_program_decides(sK2_skl)|sQ19_spl),
% 0.19/0.46 inference(resolution,[status(thm)],[f220,f84])).
% 0.19/0.46 fof(f658,plain,(
% 0.19/0.46 $false|~sQ1_spl|sQ19_spl),
% 0.19/0.46 inference(forward_subsumption_resolution,[status(thm)],[f655,f104])).
% 0.19/0.46 fof(f659,plain,(
% 0.19/0.46 ~sQ1_spl|sQ19_spl),
% 0.19/0.46 inference(contradiction_clause,[status(thm)],[f658])).
% 0.19/0.46 fof(f745,plain,(
% 0.19/0.46 ~program_program_decides(sK2_skl)|sQ20_spl),
% 0.19/0.46 inference(resolution,[status(thm)],[f223,f85])).
% 0.19/0.46 fof(f748,plain,(
% 0.19/0.46 $false|~sQ1_spl|sQ20_spl),
% 0.19/0.46 inference(forward_subsumption_resolution,[status(thm)],[f745,f104])).
% 0.19/0.46 fof(f749,plain,(
% 0.19/0.46 ~sQ1_spl|sQ20_spl),
% 0.19/0.46 inference(contradiction_clause,[status(thm)],[f748])).
% 0.19/0.46 fof(f750,plain,(
% 0.19/0.46 $false),
% 0.19/0.46 inference(sat_refutation,[status(thm)],[f106,f113,f117,f121,f128,f132,f136,f139,f224,f309,f351,f358,f363,f420,f474,f659,f749])).
% 0.19/0.46 % SZS output end CNFRefutation for theBenchmark.p
% 0.19/0.49 % Elapsed time: 0.080920 seconds
% 0.19/0.49 % CPU time: 0.163538 seconds
% 0.19/0.49 % Total memory used: 7.200 MB
% 0.19/0.49 % Net memory used: 7.139 MB
%------------------------------------------------------------------------------