%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : COM003+3 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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.15s 0.53s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : COM003+3 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n004.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Mon Sep 21 14:13:49 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.44 % Drodi V4.1.1
% 0.15/0.53 % Refutation found
% 0.15/0.53 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/0.53 % SZS output start CNFRefutation for theBenchmark
% 0.15/0.53 fof(f1,axiom,(
% 0.15/0.53 ( (? [X] :( algorithm(X)& (! [Y] :( program(Y)=> (! [Z] : decides(X,Y,Z) )) )))=> (? [W] :( program(W)& (! [Y] :( program(Y)=> (! [Z] : decides(W,Y,Z) )) )) )) ),
% 0.15/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.53 fof(f2,axiom,(
% 0.15/0.53 (! [W] :( ( program(W)& (! [Y] :( program(Y)=> (! [Z] : decides(W,Y,Z) )) ))=> (! [Y,Z] :( ( ( program(Y)& halts2(Y,Z) )=> ( halts3(W,Y,Z)& outputs(W,good) ) )& ( ( program(Y)& ~ halts2(Y,Z) )=> ( halts3(W,Y,Z)& outputs(W,bad) ) ) ) )) )),
% 0.15/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.53 fof(f3,axiom,(
% 0.15/0.53 (! [W] :( ( program(W)& (! [Y,Z] :( ( ( program(Y)& halts2(Y,Z) )=> ( halts3(W,Y,Z)& outputs(W,good) ) )& ( ( program(Y)& ~ halts2(Y,Z) )=> ( halts3(W,Y,Z)& outputs(W,bad) ) ) ) ))=> (? [V] :( program(V)& (! [Y] :( ( ( program(Y)& halts3(W,Y,Y)& outputs(W,good) )=> ~ halts2(V,Y) )& ( ( program(Y)& halts3(W,Y,Y)& outputs(W,bad) )=> ( halts2(V,Y)& outputs(V,bad) ) ) ) )) )) )),
% 0.15/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.53 fof(f4,conjecture,(
% 0.15/0.53 ~ (? [X1] :( algorithm(X1)& (! [Y1] :( program(Y1)=> (! [Z1] : decides(X1,Y1,Z1) )) )) )),
% 0.15/0.53 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/0.53 fof(f5,negated_conjecture,(
% 0.15/0.53 ~(~ (? [X1] :( algorithm(X1)& (! [Y1] :( program(Y1)=> (! [Z1] : decides(X1,Y1,Z1) )) )) ))),
% 0.15/0.53 inference(negated_conjecture,[status(cth)],[f4])).
% 0.15/0.53 fof(f6,plain,(
% 0.15/0.53 (![X]: (~algorithm(X)|(?[Y]: (program(Y)&(?[Z]: ~decides(X,Y,Z))))))|(?[W]: (program(W)&(![Y]: (~program(Y)|(![Z]: decides(W,Y,Z))))))),
% 0.15/0.53 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.15/0.53 fof(f7,definition,(
% 0.15/0.53 ![X,Y]: (sP0_prd(Y,X)<=>(program(Y)&(?[Z]: ~decides(X,Y,Z))))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.15/0.53 fof(f8,plain,(
% 0.15/0.53 (![X]: (~algorithm(X)|(?[Y]: sP0_prd(Y,X))))|(?[W]: (program(W)&(![Y]: (~program(Y)|(![Z]: decides(W,Y,Z))))))),
% 0.15/0.53 inference(formula_renaming,[status(thm)],[f6,f7])).
% 0.15/0.53 fof(f9,plain,(
% 0.15/0.53 (![X]: (~algorithm(X)|sP0_prd(sK0_skl(X),X)))|(program(sK1_skl)&(![Y]: (~program(Y)|(![Z]: decides(sK1_skl,Y,Z)))))),
% 0.15/0.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(Y,sK0_skl(X)),skolemize(W,sK1_skl)],[f8])).
% 0.15/0.53 fof(f10,plain,(
% 0.15/0.53 ![X0]: (~algorithm(X0)|sP0_prd(sK0_skl(X0),X0)|program(sK1_skl))),
% 0.15/0.53 inference(cnf_transformation,[status(thm)],[f9])).
% 0.15/0.53 fof(f11,plain,(
% 0.15/0.53 ![X0,X1,X2]: (~algorithm(X0)|sP0_prd(sK0_skl(X0),X0)|~program(X1)|decides(sK1_skl,X1,X2))),
% 0.15/0.53 inference(cnf_transformation,[status(thm)],[f9])).
% 0.15/0.53 fof(f12,plain,(
% 0.15/0.53 ![W]: ((~program(W)|(?[Y]: (program(Y)&(?[Z]: ~decides(W,Y,Z)))))|(![Y,Z]: (((~program(Y)|~halts2(Y,Z))|(halts3(W,Y,Z)&outputs(W,good)))&((~program(Y)|halts2(Y,Z))|(halts3(W,Y,Z)&outputs(W,bad))))))),
% 0.15/0.53 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.15/0.53 fof(f13,definition,(
% 0.15/0.53 ![W,Y]: (sP1_prd(Y,W)<=>(program(Y)&(?[Z]: ~decides(W,Y,Z))))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.15/0.53 fof(f14,plain,(
% 0.15/0.53 ![W]: ((~program(W)|(?[Y]: sP1_prd(Y,W)))|(![Y,Z]: (((~program(Y)|~halts2(Y,Z))|(halts3(W,Y,Z)&outputs(W,good)))&((~program(Y)|halts2(Y,Z))|(halts3(W,Y,Z)&outputs(W,bad))))))),
% 0.15/0.53 inference(formula_renaming,[status(thm)],[f12,f13])).
% 0.15/0.53 fof(f15,plain,(
% 0.15/0.53 ![W]: ((~program(W)|(?[Y]: sP1_prd(Y,W)))|((![Y,Z]: ((~program(Y)|~halts2(Y,Z))|(halts3(W,Y,Z)&outputs(W,good))))&(![Y,Z]: ((~program(Y)|halts2(Y,Z))|(halts3(W,Y,Z)&outputs(W,bad))))))),
% 0.15/0.53 inference(miniscoping,[status(thm)],[f14])).
% 0.15/0.53 fof(f16,plain,(
% 0.15/0.53 ![W]: ((~program(W)|sP1_prd(sK2_skl(W),W))|((![Y,Z]: ((~program(Y)|~halts2(Y,Z))|(halts3(W,Y,Z)&outputs(W,good))))&(![Y,Z]: ((~program(Y)|halts2(Y,Z))|(halts3(W,Y,Z)&outputs(W,bad))))))),
% 0.15/0.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(Y,sK2_skl(W))],[f15])).
% 0.15/0.53 fof(f17,plain,(
% 0.15/0.53 ![X0,X1,X2]: (~program(X0)|sP1_prd(sK2_skl(X0),X0)|~program(X1)|~halts2(X1,X2)|halts3(X0,X1,X2))),
% 0.15/0.53 inference(cnf_transformation,[status(thm)],[f16])).
% 0.15/0.53 fof(f18,plain,(
% 0.15/0.53 ![X0,X1,X2]: (~program(X0)|sP1_prd(sK2_skl(X0),X0)|~program(X1)|~halts2(X1,X2)|outputs(X0,good))),
% 0.15/0.53 inference(cnf_transformation,[status(thm)],[f16])).
% 0.15/0.53 fof(f19,plain,(
% 0.15/0.53 ![X0,X1,X2]: (~program(X0)|sP1_prd(sK2_skl(X0),X0)|~program(X1)|halts2(X1,X2)|halts3(X0,X1,X2))),
% 0.15/0.53 inference(cnf_transformation,[status(thm)],[f16])).
% 0.15/0.53 fof(f20,plain,(
% 0.15/0.53 ![X0,X1,X2]: (~program(X0)|sP1_prd(sK2_skl(X0),X0)|~program(X1)|halts2(X1,X2)|outputs(X0,bad))),
% 0.15/0.53 inference(cnf_transformation,[status(thm)],[f16])).
% 0.15/0.53 fof(f21,plain,(
% 0.15/0.53 ![W]: ((~program(W)|(?[Y,Z]: (((program(Y)&halts2(Y,Z))&(~halts3(W,Y,Z)|~outputs(W,good)))|((program(Y)&~halts2(Y,Z))&(~halts3(W,Y,Z)|~outputs(W,bad))))))|(?[V]: (program(V)&(![Y]: ((((~program(Y)|~halts3(W,Y,Y))|~outputs(W,good))|~halts2(V,Y))&(((~program(Y)|~halts3(W,Y,Y))|~outputs(W,bad))|(halts2(V,Y)&outputs(V,bad))))))))),
% 0.15/0.53 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.15/0.53 fof(f22,definition,(
% 0.15/0.53 ![W,Y,Z]: (sP2_prd(Z,Y,W)<=>(((program(Y)&halts2(Y,Z))&(~halts3(W,Y,Z)|~outputs(W,good)))|((program(Y)&~halts2(Y,Z))&(~halts3(W,Y,Z)|~outputs(W,bad)))))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.15/0.53 fof(f23,plain,(
% 0.15/0.53 ![W]: ((~program(W)|(?[Y,Z]: sP2_prd(Z,Y,W)))|(?[V]: (program(V)&(![Y]: ((((~program(Y)|~halts3(W,Y,Y))|~outputs(W,good))|~halts2(V,Y))&(((~program(Y)|~halts3(W,Y,Y))|~outputs(W,bad))|(halts2(V,Y)&outputs(V,bad))))))))),
% 0.15/0.53 inference(formula_renaming,[status(thm)],[f21,f22])).
% 0.15/0.53 fof(f24,plain,(
% 0.15/0.53 ![W]: ((~program(W)|(?[Y,Z]: sP2_prd(Z,Y,W)))|(?[V]: (program(V)&((![Y]: (((~program(Y)|~halts3(W,Y,Y))|~outputs(W,good))|~halts2(V,Y)))&(![Y]: (((~program(Y)|~halts3(W,Y,Y))|~outputs(W,bad))|(halts2(V,Y)&outputs(V,bad))))))))),
% 0.15/0.53 inference(miniscoping,[status(thm)],[f23])).
% 0.15/0.53 fof(f25,plain,(
% 0.15/0.53 ![W]: ((~program(W)|sP2_prd(sK4_skl(W),sK3_skl(W),W))|(program(sK5_skl(W))&((![Y]: (((~program(Y)|~halts3(W,Y,Y))|~outputs(W,good))|~halts2(sK5_skl(W),Y)))&(![Y]: (((~program(Y)|~halts3(W,Y,Y))|~outputs(W,bad))|(halts2(sK5_skl(W),Y)&outputs(sK5_skl(W),bad)))))))),
% 0.15/0.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl,sK5_skl]),skolemize(Y,sK3_skl(W)),skolemize(Z,sK4_skl(W)),skolemize(V,sK5_skl(W))],[f24])).
% 0.15/0.53 fof(f26,plain,(
% 0.15/0.53 ![X0]: (~program(X0)|sP2_prd(sK4_skl(X0),sK3_skl(X0),X0)|program(sK5_skl(X0)))),
% 0.15/0.53 inference(cnf_transformation,[status(thm)],[f25])).
% 0.15/0.53 fof(f27,plain,(
% 0.15/0.53 ![X0,X1]: (~program(X0)|sP2_prd(sK4_skl(X0),sK3_skl(X0),X0)|~program(X1)|~halts3(X0,X1,X1)|~outputs(X0,good)|~halts2(sK5_skl(X0),X1))),
% 0.15/0.53 inference(cnf_transformation,[status(thm)],[f25])).
% 0.15/0.53 fof(f28,plain,(
% 0.15/0.53 ![X0,X1]: (~program(X0)|sP2_prd(sK4_skl(X0),sK3_skl(X0),X0)|~program(X1)|~halts3(X0,X1,X1)|~outputs(X0,bad)|halts2(sK5_skl(X0),X1))),
% 0.15/0.53 inference(cnf_transformation,[status(thm)],[f25])).
% 0.15/0.53 fof(f29,plain,(
% 0.15/0.53 ![X0,X1]: (~program(X0)|sP2_prd(sK4_skl(X0),sK3_skl(X0),X0)|~program(X1)|~halts3(X0,X1,X1)|~outputs(X0,bad)|outputs(sK5_skl(X0),bad))),
% 0.15/0.53 inference(cnf_transformation,[status(thm)],[f25])).
% 0.15/0.53 fof(f30,plain,(
% 0.15/0.53 ?[X1]: (algorithm(X1)&(![Y1]: (~program(Y1)|(![Z1]: decides(X1,Y1,Z1)))))),
% 0.15/0.53 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 0.15/0.53 fof(f31,plain,(
% 0.15/0.53 (algorithm(sK6_skl)&(![Y1]: (~program(Y1)|(![Z1]: decides(sK6_skl,Y1,Z1)))))),
% 0.15/0.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(X1,sK6_skl)],[f30])).
% 0.15/0.53 fof(f32,plain,(
% 0.15/0.53 algorithm(sK6_skl)),
% 0.15/0.53 inference(cnf_transformation,[status(thm)],[f31])).
% 0.15/0.53 fof(f33,plain,(
% 0.15/0.53 ![X0,X1]: (~program(X0)|decides(sK6_skl,X0,X1))),
% 0.15/0.53 inference(cnf_transformation,[status(thm)],[f31])).
% 0.15/0.53 fof(f34,plain,(
% 0.15/0.53 ![X,Y]: ((~sP0_prd(Y,X)|(program(Y)&(?[Z]: ~decides(X,Y,Z))))&(sP0_prd(Y,X)|(~program(Y)|(![Z]: decides(X,Y,Z)))))),
% 0.15/0.53 inference(NNF_transformation,[status(thm)],[f7])).
% 0.15/0.53 fof(f35,plain,(
% 0.15/0.53 (![X,Y]: (~sP0_prd(Y,X)|(program(Y)&(?[Z]: ~decides(X,Y,Z)))))&(![X,Y]: (sP0_prd(Y,X)|(~program(Y)|(![Z]: decides(X,Y,Z)))))),
% 0.15/0.53 inference(miniscoping,[status(thm)],[f34])).
% 0.15/0.53 fof(f36,plain,(
% 0.15/0.53 (![X,Y]: (~sP0_prd(Y,X)|(program(Y)&~decides(X,Y,sK7_skl(Y,X)))))&(![X,Y]: (sP0_prd(Y,X)|(~program(Y)|(![Z]: decides(X,Y,Z)))))),
% 0.15/0.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(Z,sK7_skl(Y,X))],[f35])).
% 0.15/0.53 fof(f37,plain,(
% 0.15/0.53 ![X0,X1]: (~sP0_prd(X0,X1)|program(X0))),
% 0.15/0.53 inference(cnf_transformation,[status(thm)],[f36])).
% 0.15/0.53 fof(f38,plain,(
% 0.15/0.53 ![X0,X1]: (~sP0_prd(X0,X1)|~decides(X1,X0,sK7_skl(X0,X1)))),
% 0.15/0.53 inference(cnf_transformation,[status(thm)],[f36])).
% 0.15/0.53 fof(f40,plain,(
% 0.15/0.53 ![W,Y]: ((~sP1_prd(Y,W)|(program(Y)&(?[Z]: ~decides(W,Y,Z))))&(sP1_prd(Y,W)|(~program(Y)|(![Z]: decides(W,Y,Z)))))),
% 0.15/0.53 inference(NNF_transformation,[status(thm)],[f13])).
% 0.15/0.53 fof(f41,plain,(
% 0.15/0.53 (![W,Y]: (~sP1_prd(Y,W)|(program(Y)&(?[Z]: ~decides(W,Y,Z)))))&(![W,Y]: (sP1_prd(Y,W)|(~program(Y)|(![Z]: decides(W,Y,Z)))))),
% 0.15/0.53 inference(miniscoping,[status(thm)],[f40])).
% 0.15/0.53 fof(f42,plain,(
% 0.15/0.53 (![W,Y]: (~sP1_prd(Y,W)|(program(Y)&~decides(W,Y,sK8_skl(Y,W)))))&(![W,Y]: (sP1_prd(Y,W)|(~program(Y)|(![Z]: decides(W,Y,Z)))))),
% 0.15/0.53 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(Z,sK8_skl(Y,W))],[f41])).
% 0.15/0.53 fof(f43,plain,(
% 0.15/0.53 ![X0,X1]: (~sP1_prd(X0,X1)|program(X0))),
% 0.15/0.53 inference(cnf_transformation,[status(thm)],[f42])).
% 0.15/0.53 fof(f44,plain,(
% 0.15/0.53 ![X0,X1]: (~sP1_prd(X0,X1)|~decides(X1,X0,sK8_skl(X0,X1)))),
% 0.15/0.53 inference(cnf_transformation,[status(thm)],[f42])).
% 0.15/0.53 fof(f46,definition,(
% 0.15/0.53 ![W,Y,Z]: (sP3_prd(Z,Y,W)<=>((program(Y)&halts2(Y,Z))&(~halts3(W,Y,Z)|~outputs(W,good))))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 0.15/0.53 fof(f47,plain,(
% 0.15/0.53 ![W,Y,Z]: (sP2_prd(Z,Y,W)<=>(sP3_prd(Z,Y,W)|((program(Y)&~halts2(Y,Z))&(~halts3(W,Y,Z)|~outputs(W,bad)))))),
% 0.15/0.53 inference(formula_renaming,[status(thm)],[f22,f46])).
% 0.15/0.53 fof(f48,plain,(
% 0.15/0.53 ![W,Y,Z]: ((~sP2_prd(Z,Y,W)|(sP3_prd(Z,Y,W)|((program(Y)&~halts2(Y,Z))&(~halts3(W,Y,Z)|~outputs(W,bad)))))&(sP2_prd(Z,Y,W)|(~sP3_prd(Z,Y,W)&((~program(Y)|halts2(Y,Z))|(halts3(W,Y,Z)&outputs(W,bad))))))),
% 0.15/0.53 inference(NNF_transformation,[status(thm)],[f47])).
% 0.15/0.53 fof(f49,plain,(
% 0.15/0.53 (![W,Y,Z]: (~sP2_prd(Z,Y,W)|(sP3_prd(Z,Y,W)|((program(Y)&~halts2(Y,Z))&(~halts3(W,Y,Z)|~outputs(W,bad))))))&(![W,Y,Z]: (sP2_prd(Z,Y,W)|(~sP3_prd(Z,Y,W)&((~program(Y)|halts2(Y,Z))|(halts3(W,Y,Z)&outputs(W,bad))))))),
% 0.15/0.53 inference(miniscoping,[status(thm)],[f48])).
% 0.15/0.53 fof(f50,plain,(
% 0.15/0.53 ![X0,X1,X2]: (~sP2_prd(X0,X1,X2)|sP3_prd(X0,X1,X2)|program(X1))),
% 0.15/0.53 inference(cnf_transformation,[status(thm)],[f49])).
% 0.15/0.53 fof(f51,plain,(
% 0.15/0.53 ![X0,X1,X2]: (~sP2_prd(X0,X1,X2)|sP3_prd(X0,X1,X2)|~halts2(X1,X0))),
% 0.15/0.53 inference(cnf_transformation,[status(thm)],[f49])).
% 0.15/0.53 fof(f52,plain,(
% 0.15/0.53 ![X0,X1,X2]: (~sP2_prd(X0,X1,X2)|sP3_prd(X0,X1,X2)|~halts3(X2,X1,X0)|~outputs(X2,bad))),
% 0.15/0.53 inference(cnf_transformation,[status(thm)],[f49])).
% 0.15/0.53 fof(f56,plain,(
% 0.15/0.53 ![W,Y,Z]: ((~sP3_prd(Z,Y,W)|((program(Y)&halts2(Y,Z))&(~halts3(W,Y,Z)|~outputs(W,good))))&(sP3_prd(Z,Y,W)|((~program(Y)|~halts2(Y,Z))|(halts3(W,Y,Z)&outputs(W,good)))))),
% 0.15/0.53 inference(NNF_transformation,[status(thm)],[f46])).
% 0.15/0.53 fof(f57,plain,(
% 0.15/0.53 (![W,Y,Z]: (~sP3_prd(Z,Y,W)|((program(Y)&halts2(Y,Z))&(~halts3(W,Y,Z)|~outputs(W,good)))))&(![W,Y,Z]: (sP3_prd(Z,Y,W)|((~program(Y)|~halts2(Y,Z))|(halts3(W,Y,Z)&outputs(W,good)))))),
% 0.15/0.53 inference(miniscoping,[status(thm)],[f56])).
% 0.15/0.53 fof(f58,plain,(
% 0.15/0.53 ![X0,X1,X2]: (~sP3_prd(X0,X1,X2)|program(X1))),
% 0.15/0.53 inference(cnf_transformation,[status(thm)],[f57])).
% 0.15/0.53 fof(f59,plain,(
% 0.15/0.53 ![X0,X1,X2]: (~sP3_prd(X0,X1,X2)|halts2(X1,X0))),
% 0.15/0.53 inference(cnf_transformation,[status(thm)],[f57])).
% 0.15/0.53 fof(f60,plain,(
% 0.15/0.53 ![X0,X1,X2]: (~sP3_prd(X0,X1,X2)|~halts3(X2,X1,X0)|~outputs(X2,good))),
% 0.15/0.53 inference(cnf_transformation,[status(thm)],[f57])).
% 0.15/0.53 fof(f62,plain,(
% 0.15/0.53 ![X0,X1,X2]: (sP3_prd(X0,X1,X2)|~program(X1)|~halts2(X1,X0)|outputs(X2,good))),
% 0.15/0.53 inference(cnf_transformation,[status(thm)],[f57])).
% 0.15/0.53 fof(f63,definition,(
% 0.15/0.53 ![X0]: (sQ0_spl <=> (~algorithm(X0)|sP0_prd(sK0_skl(X0),X0)))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f64,plain,(
% 0.15/0.53 ![X0]: (~algorithm(X0)|sP0_prd(sK0_skl(X0),X0)|~sQ0_spl)),
% 0.15/0.53 inference(component_clause,[status(thm)],[f63])).
% 0.15/0.53 fof(f66,definition,(
% 0.15/0.53 sQ1_spl <=> (program(sK1_skl))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f67,plain,(
% 0.15/0.53 program(sK1_skl)|~sQ1_spl),
% 0.15/0.53 inference(component_clause,[status(thm)],[f66])).
% 0.15/0.53 fof(f69,plain,(
% 0.15/0.53 sQ0_spl|sQ1_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f10,f63,f66])).
% 0.15/0.53 fof(f70,definition,(
% 0.15/0.53 ![X1,X2]: (sQ2_spl <=> (~program(X1)|decides(sK1_skl,X1,X2)))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f71,plain,(
% 0.15/0.53 ![X0,X1]: (~program(X0)|decides(sK1_skl,X0,X1)|~sQ2_spl)),
% 0.15/0.53 inference(component_clause,[status(thm)],[f70])).
% 0.15/0.53 fof(f73,plain,(
% 0.15/0.53 sQ0_spl|sQ2_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f11,f63,f70])).
% 0.15/0.53 fof(f74,definition,(
% 0.15/0.53 ![X0]: (sQ3_spl <=> (~program(X0)|sP1_prd(sK2_skl(X0),X0)|outputs(X0,good)))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f75,plain,(
% 0.15/0.53 ![X0]: (~program(X0)|sP1_prd(sK2_skl(X0),X0)|outputs(X0,good)|~sQ3_spl)),
% 0.15/0.53 inference(component_clause,[status(thm)],[f74])).
% 0.15/0.53 fof(f77,definition,(
% 0.15/0.53 ![X1,X2]: (sQ4_spl <=> (~program(X1)|~halts2(X1,X2)))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f78,plain,(
% 0.15/0.53 ![X0,X1]: (~program(X0)|~halts2(X0,X1)|~sQ4_spl)),
% 0.15/0.53 inference(component_clause,[status(thm)],[f77])).
% 0.15/0.53 fof(f80,plain,(
% 0.15/0.53 sQ3_spl|sQ4_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f18,f74,f77])).
% 0.15/0.53 fof(f81,definition,(
% 0.15/0.53 ![X0]: (sQ5_spl <=> (~program(X0)|sP1_prd(sK2_skl(X0),X0)|outputs(X0,bad)))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f82,plain,(
% 0.15/0.53 ![X0]: (~program(X0)|sP1_prd(sK2_skl(X0),X0)|outputs(X0,bad)|~sQ5_spl)),
% 0.15/0.53 inference(component_clause,[status(thm)],[f81])).
% 0.15/0.53 fof(f84,definition,(
% 0.15/0.53 ![X1,X2]: (sQ6_spl <=> (~program(X1)|halts2(X1,X2)))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f85,plain,(
% 0.15/0.53 ![X0,X1]: (~program(X0)|halts2(X0,X1)|~sQ6_spl)),
% 0.15/0.53 inference(component_clause,[status(thm)],[f84])).
% 0.15/0.53 fof(f87,plain,(
% 0.15/0.53 sQ5_spl|sQ6_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f20,f81,f84])).
% 0.15/0.53 fof(f88,plain,(
% 0.15/0.53 sP0_prd(sK0_skl(sK6_skl),sK6_skl)|~sQ0_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f64,f32])).
% 0.15/0.53 fof(f89,plain,(
% 0.15/0.53 program(sK0_skl(sK6_skl))|~sQ0_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f88,f37])).
% 0.15/0.53 fof(f90,plain,(
% 0.15/0.53 ![X0]: (decides(sK6_skl,sK0_skl(sK6_skl),X0)|~sQ0_spl)),
% 0.15/0.53 inference(resolution,[status(thm)],[f89,f33])).
% 0.15/0.53 fof(f92,plain,(
% 0.15/0.53 ~sP0_prd(sK0_skl(sK6_skl),sK6_skl)|~sQ0_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f90,f38])).
% 0.15/0.53 fof(f93,plain,(
% 0.15/0.53 $false|~sQ0_spl),
% 0.15/0.53 inference(forward_subsumption_resolution,[status(thm)],[f92,f88])).
% 0.15/0.53 fof(f94,plain,(
% 0.15/0.53 ~sQ0_spl),
% 0.15/0.53 inference(contradiction_clause,[status(thm)],[f93])).
% 0.15/0.53 fof(f102,plain,(
% 0.15/0.53 ![X0,X1]: (sP1_prd(sK2_skl(sK1_skl),sK1_skl)|~program(X0)|~halts2(X0,X1)|halts3(sK1_skl,X0,X1)|~sQ1_spl)),
% 0.15/0.53 inference(resolution,[status(thm)],[f17,f67])).
% 0.15/0.53 fof(f103,definition,(
% 0.15/0.53 sQ7_spl <=> (sP1_prd(sK2_skl(sK1_skl),sK1_skl))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f104,plain,(
% 0.15/0.53 sP1_prd(sK2_skl(sK1_skl),sK1_skl)|~sQ7_spl),
% 0.15/0.53 inference(component_clause,[status(thm)],[f103])).
% 0.15/0.53 fof(f106,definition,(
% 0.15/0.53 ![X0,X1]: (sQ8_spl <=> (~program(X0)|~halts2(X0,X1)|halts3(sK1_skl,X0,X1)))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f107,plain,(
% 0.15/0.53 ![X0,X1]: (~program(X0)|~halts2(X0,X1)|halts3(sK1_skl,X0,X1)|~sQ8_spl)),
% 0.15/0.53 inference(component_clause,[status(thm)],[f106])).
% 0.15/0.53 fof(f109,plain,(
% 0.15/0.53 sQ7_spl|sQ8_spl|~sQ1_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f102,f103,f106,f66])).
% 0.15/0.53 fof(f110,plain,(
% 0.15/0.53 ![X0,X1,X2]: (~program(X0)|sP1_prd(sK2_skl(X0),X0)|~program(X1)|halts3(X0,X1,X2))),
% 0.15/0.53 inference(forward_subsumption_resolution,[status(thm)],[f19,f17])).
% 0.15/0.53 fof(f111,plain,(
% 0.15/0.53 ![X0,X1]: (sP1_prd(sK2_skl(sK1_skl),sK1_skl)|~program(X0)|halts3(sK1_skl,X0,X1)|~sQ1_spl)),
% 0.15/0.53 inference(resolution,[status(thm)],[f110,f67])).
% 0.15/0.53 fof(f112,definition,(
% 0.15/0.53 ![X0,X1]: (sQ9_spl <=> (~program(X0)|halts3(sK1_skl,X0,X1)))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f113,plain,(
% 0.15/0.53 ![X0,X1]: (~program(X0)|halts3(sK1_skl,X0,X1)|~sQ9_spl)),
% 0.15/0.53 inference(component_clause,[status(thm)],[f112])).
% 0.15/0.53 fof(f115,plain,(
% 0.15/0.53 sQ7_spl|sQ9_spl|~sQ1_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f111,f103,f112,f66])).
% 0.15/0.53 fof(f116,plain,(
% 0.15/0.53 sP2_prd(sK4_skl(sK1_skl),sK3_skl(sK1_skl),sK1_skl)|program(sK5_skl(sK1_skl))|~sQ1_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f26,f67])).
% 0.15/0.53 fof(f117,definition,(
% 0.15/0.53 sQ10_spl <=> (sP2_prd(sK4_skl(sK1_skl),sK3_skl(sK1_skl),sK1_skl))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f118,plain,(
% 0.15/0.53 sP2_prd(sK4_skl(sK1_skl),sK3_skl(sK1_skl),sK1_skl)|~sQ10_spl),
% 0.15/0.53 inference(component_clause,[status(thm)],[f117])).
% 0.15/0.53 fof(f120,definition,(
% 0.15/0.53 sQ11_spl <=> (program(sK5_skl(sK1_skl)))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f121,plain,(
% 0.15/0.53 program(sK5_skl(sK1_skl))|~sQ11_spl),
% 0.15/0.53 inference(component_clause,[status(thm)],[f120])).
% 0.15/0.53 fof(f123,plain,(
% 0.15/0.53 sQ10_spl|sQ11_spl|~sQ1_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f116,f117,f120,f66])).
% 0.15/0.53 fof(f124,plain,(
% 0.15/0.53 ![X0,X1,X2]: (~sP2_prd(X0,X1,X2)|program(X1))),
% 0.15/0.53 inference(forward_subsumption_resolution,[status(thm)],[f50,f58])).
% 0.15/0.53 fof(f127,plain,(
% 0.15/0.53 sP1_prd(sK2_skl(sK1_skl),sK1_skl)|outputs(sK1_skl,bad)|~sQ5_spl|~sQ1_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f82,f67])).
% 0.15/0.53 fof(f128,definition,(
% 0.15/0.53 sQ12_spl <=> (outputs(sK1_skl,bad))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f131,plain,(
% 0.15/0.53 sQ7_spl|sQ12_spl|~sQ5_spl|~sQ1_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f127,f103,f128,f81,f66])).
% 0.15/0.53 fof(f132,plain,(
% 0.15/0.53 sP1_prd(sK2_skl(sK1_skl),sK1_skl)|outputs(sK1_skl,good)|~sQ3_spl|~sQ1_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f75,f67])).
% 0.15/0.53 fof(f133,definition,(
% 0.15/0.53 sQ13_spl <=> (outputs(sK1_skl,good))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f136,plain,(
% 0.15/0.53 sQ7_spl|sQ13_spl|~sQ3_spl|~sQ1_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f132,f103,f133,f74,f66])).
% 0.15/0.53 fof(f140,definition,(
% 0.15/0.53 ![X0]: (sQ14_spl <=> (halts2(sK1_skl,X0)))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f141,plain,(
% 0.15/0.53 ![X0]: (halts2(sK1_skl,X0)|~sQ14_spl)),
% 0.15/0.53 inference(component_clause,[status(thm)],[f140])).
% 0.15/0.53 fof(f159,plain,(
% 0.15/0.53 ![X0]: (halts2(sK1_skl,X0)|~sQ6_spl|~sQ1_spl)),
% 0.15/0.53 inference(resolution,[status(thm)],[f85,f67])).
% 0.15/0.53 fof(f166,definition,(
% 0.15/0.53 ![X0]: (sQ17_spl <=> (outputs(X0,good)))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f167,plain,(
% 0.15/0.53 ![X0]: (outputs(X0,good)|~sQ17_spl)),
% 0.15/0.53 inference(component_clause,[status(thm)],[f166])).
% 0.15/0.53 fof(f192,plain,(
% 0.15/0.53 ~program(sK1_skl)|~sQ14_spl|~sQ4_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f141,f78])).
% 0.15/0.53 fof(f193,plain,(
% 0.15/0.53 $false|~sQ1_spl|~sQ14_spl|~sQ4_spl),
% 0.15/0.53 inference(forward_subsumption_resolution,[status(thm)],[f192,f67])).
% 0.15/0.53 fof(f194,plain,(
% 0.15/0.53 ~sQ1_spl|~sQ14_spl|~sQ4_spl),
% 0.15/0.53 inference(contradiction_clause,[status(thm)],[f193])).
% 0.15/0.53 fof(f207,plain,(
% 0.15/0.53 ![X0,X1,X2]: (~sP3_prd(X0,X1,X2)|~halts3(X2,X1,X0)|~sQ17_spl)),
% 0.15/0.53 inference(backward_subsumption_resolution,[status(thm)],[f60,f167])).
% 0.15/0.53 fof(f209,plain,(
% 0.15/0.53 ![X0,X1,X2]: (~sP2_prd(X0,X1,X2)|~halts3(X2,X1,X0)|~outputs(X2,bad)|~sQ17_spl)),
% 0.15/0.53 inference(backward_subsumption_resolution,[status(thm)],[f52,f207])).
% 0.15/0.53 fof(f213,plain,(
% 0.15/0.53 program(sK2_skl(sK1_skl))|~sQ7_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f104,f43])).
% 0.15/0.53 fof(f214,plain,(
% 0.15/0.53 ~halts3(sK1_skl,sK3_skl(sK1_skl),sK4_skl(sK1_skl))|~outputs(sK1_skl,bad)|~sQ10_spl|~sQ17_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f118,f209])).
% 0.15/0.53 fof(f215,plain,(
% 0.15/0.53 program(sK3_skl(sK1_skl))|~sQ10_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f118,f124])).
% 0.15/0.53 fof(f216,plain,(
% 0.15/0.53 sP3_prd(sK4_skl(sK1_skl),sK3_skl(sK1_skl),sK1_skl)|~halts2(sK3_skl(sK1_skl),sK4_skl(sK1_skl))|~sQ10_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f118,f51])).
% 0.15/0.53 fof(f217,definition,(
% 0.15/0.53 sQ19_spl <=> (halts3(sK1_skl,sK3_skl(sK1_skl),sK4_skl(sK1_skl)))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f219,plain,(
% 0.15/0.53 ~halts3(sK1_skl,sK3_skl(sK1_skl),sK4_skl(sK1_skl))|sQ19_spl),
% 0.15/0.53 inference(component_clause,[status(thm)],[f217])).
% 0.15/0.53 fof(f220,plain,(
% 0.15/0.53 ~sQ19_spl|~sQ12_spl|~sQ10_spl|~sQ17_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f214,f217,f128,f117,f166])).
% 0.15/0.53 fof(f221,definition,(
% 0.15/0.53 sQ20_spl <=> (sP3_prd(sK4_skl(sK1_skl),sK3_skl(sK1_skl),sK1_skl))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f222,plain,(
% 0.15/0.53 sP3_prd(sK4_skl(sK1_skl),sK3_skl(sK1_skl),sK1_skl)|~sQ20_spl),
% 0.15/0.53 inference(component_clause,[status(thm)],[f221])).
% 0.15/0.53 fof(f224,definition,(
% 0.15/0.53 sQ21_spl <=> (halts2(sK3_skl(sK1_skl),sK4_skl(sK1_skl)))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f225,plain,(
% 0.15/0.53 halts2(sK3_skl(sK1_skl),sK4_skl(sK1_skl))|~sQ21_spl),
% 0.15/0.53 inference(component_clause,[status(thm)],[f224])).
% 0.15/0.53 fof(f226,plain,(
% 0.15/0.53 ~halts2(sK3_skl(sK1_skl),sK4_skl(sK1_skl))|sQ21_spl),
% 0.15/0.53 inference(component_clause,[status(thm)],[f224])).
% 0.15/0.53 fof(f227,plain,(
% 0.15/0.53 sQ20_spl|~sQ21_spl|~sQ10_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f216,f221,f224,f117])).
% 0.15/0.53 fof(f233,plain,(
% 0.15/0.53 ![X0]: (decides(sK1_skl,sK2_skl(sK1_skl),X0)|~sQ7_spl|~sQ2_spl)),
% 0.15/0.53 inference(resolution,[status(thm)],[f213,f71])).
% 0.15/0.53 fof(f310,definition,(
% 0.15/0.53 ![X0]: (sQ35_spl <=> (halts2(sK3_skl(sK1_skl),X0)))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f311,plain,(
% 0.15/0.53 ![X0]: (halts2(sK3_skl(sK1_skl),X0)|~sQ35_spl)),
% 0.15/0.53 inference(component_clause,[status(thm)],[f310])).
% 0.15/0.53 fof(f313,definition,(
% 0.15/0.53 sQ36_spl <=> (program(sK3_skl(sK1_skl)))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f314,plain,(
% 0.15/0.53 program(sK3_skl(sK1_skl))|~sQ36_spl),
% 0.15/0.53 inference(component_clause,[status(thm)],[f313])).
% 0.15/0.53 fof(f315,plain,(
% 0.15/0.53 ~program(sK3_skl(sK1_skl))|sQ36_spl),
% 0.15/0.53 inference(component_clause,[status(thm)],[f313])).
% 0.15/0.53 fof(f332,plain,(
% 0.15/0.53 halts2(sK3_skl(sK1_skl),sK4_skl(sK1_skl))|~sQ20_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f222,f59])).
% 0.15/0.53 fof(f334,plain,(
% 0.15/0.53 ~sP1_prd(sK2_skl(sK1_skl),sK1_skl)|~sQ7_spl|~sQ2_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f233,f44])).
% 0.15/0.53 fof(f336,plain,(
% 0.15/0.53 $false|~sQ7_spl|~sQ2_spl),
% 0.15/0.53 inference(forward_subsumption_resolution,[status(thm)],[f334,f104])).
% 0.15/0.53 fof(f337,plain,(
% 0.15/0.53 ~sQ7_spl|~sQ2_spl),
% 0.15/0.53 inference(contradiction_clause,[status(thm)],[f336])).
% 0.15/0.53 fof(f338,plain,(
% 0.15/0.53 sQ14_spl|~sQ6_spl|~sQ1_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f159,f140,f84,f66])).
% 0.15/0.53 fof(f342,plain,(
% 0.15/0.53 sP3_prd(sK4_skl(sK1_skl),sK3_skl(sK1_skl),sK1_skl)|~halts3(sK1_skl,sK3_skl(sK1_skl),sK4_skl(sK1_skl))|~outputs(sK1_skl,bad)|~sQ10_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f52,f118])).
% 0.15/0.53 fof(f347,plain,(
% 0.15/0.53 sQ20_spl|~sQ19_spl|~sQ12_spl|~sQ10_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f342,f221,f217,f128,f117])).
% 0.15/0.53 fof(f348,plain,(
% 0.15/0.53 ~halts3(sK1_skl,sK3_skl(sK1_skl),sK4_skl(sK1_skl))|~outputs(sK1_skl,good)|~sQ20_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f60,f222])).
% 0.15/0.53 fof(f349,plain,(
% 0.15/0.53 ~sQ19_spl|~sQ13_spl|~sQ20_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f348,f217,f133,f221])).
% 0.15/0.53 fof(f350,plain,(
% 0.15/0.53 ![X0,X1]: (~program(X0)|halts3(sK1_skl,X0,X1)|~sQ6_spl|~sQ8_spl)),
% 0.15/0.53 inference(forward_subsumption_resolution,[status(thm)],[f107,f85])).
% 0.15/0.53 fof(f352,plain,(
% 0.15/0.53 ![X0]: (halts3(sK1_skl,sK1_skl,X0)|~sQ6_spl|~sQ8_spl|~sQ1_spl)),
% 0.15/0.53 inference(resolution,[status(thm)],[f350,f67])).
% 0.15/0.53 fof(f353,plain,(
% 0.15/0.53 ~program(sK1_skl)|sP2_prd(sK4_skl(sK1_skl),sK3_skl(sK1_skl),sK1_skl)|~program(sK1_skl)|~outputs(sK1_skl,good)|~halts2(sK5_skl(sK1_skl),sK1_skl)|~sQ6_spl|~sQ8_spl|~sQ1_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f352,f27])).
% 0.15/0.53 fof(f354,definition,(
% 0.15/0.53 sQ38_spl <=> (halts2(sK5_skl(sK1_skl),sK1_skl))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f355,plain,(
% 0.15/0.53 halts2(sK5_skl(sK1_skl),sK1_skl)|~sQ38_spl),
% 0.15/0.53 inference(component_clause,[status(thm)],[f354])).
% 0.15/0.53 fof(f356,plain,(
% 0.15/0.53 ~halts2(sK5_skl(sK1_skl),sK1_skl)|sQ38_spl),
% 0.15/0.53 inference(component_clause,[status(thm)],[f354])).
% 0.15/0.53 fof(f357,plain,(
% 0.15/0.53 ~sQ1_spl|sQ10_spl|~sQ13_spl|~sQ38_spl|~sQ6_spl|~sQ8_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f353,f66,f117,f133,f354,f84,f106])).
% 0.15/0.53 fof(f379,definition,(
% 0.15/0.53 sQ39_spl <=> (outputs(sK5_skl(sK1_skl),bad))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f380,plain,(
% 0.15/0.53 outputs(sK5_skl(sK1_skl),bad)|~sQ39_spl),
% 0.15/0.53 inference(component_clause,[status(thm)],[f379])).
% 0.15/0.53 fof(f408,plain,(
% 0.15/0.53 ![X0]: (halts3(sK1_skl,sK3_skl(sK1_skl),X0)|~sQ9_spl|~sQ10_spl)),
% 0.15/0.53 inference(resolution,[status(thm)],[f113,f215])).
% 0.15/0.53 fof(f409,plain,(
% 0.15/0.53 ![X0]: (halts3(sK1_skl,sK1_skl,X0)|~sQ9_spl|~sQ1_spl)),
% 0.15/0.53 inference(resolution,[status(thm)],[f113,f67])).
% 0.15/0.53 fof(f410,plain,(
% 0.15/0.53 ~program(sK1_skl)|sP2_prd(sK4_skl(sK1_skl),sK3_skl(sK1_skl),sK1_skl)|~program(sK1_skl)|~outputs(sK1_skl,bad)|halts2(sK5_skl(sK1_skl),sK1_skl)|~sQ9_spl|~sQ1_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f409,f28])).
% 0.15/0.53 fof(f411,plain,(
% 0.15/0.53 ~program(sK1_skl)|sP2_prd(sK4_skl(sK1_skl),sK3_skl(sK1_skl),sK1_skl)|~program(sK1_skl)|~outputs(sK1_skl,bad)|outputs(sK5_skl(sK1_skl),bad)|~sQ9_spl|~sQ1_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f409,f29])).
% 0.15/0.53 fof(f412,plain,(
% 0.15/0.53 ~program(sK1_skl)|sP2_prd(sK4_skl(sK1_skl),sK3_skl(sK1_skl),sK1_skl)|~program(sK1_skl)|~outputs(sK1_skl,good)|~halts2(sK5_skl(sK1_skl),sK1_skl)|~sQ9_spl|~sQ1_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f409,f27])).
% 0.15/0.53 fof(f413,plain,(
% 0.15/0.53 ~sQ1_spl|sQ10_spl|~sQ12_spl|sQ38_spl|~sQ9_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f410,f66,f117,f128,f354,f112])).
% 0.15/0.53 fof(f414,plain,(
% 0.15/0.53 ~sQ1_spl|sQ10_spl|~sQ12_spl|sQ39_spl|~sQ9_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f411,f66,f117,f128,f379,f112])).
% 0.15/0.53 fof(f415,plain,(
% 0.15/0.53 ~sQ1_spl|sQ10_spl|~sQ13_spl|~sQ38_spl|~sQ9_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f412,f66,f117,f133,f354,f112])).
% 0.15/0.53 fof(f432,plain,(
% 0.15/0.53 ![X0]: (sP3_prd(sK4_skl(sK1_skl),sK3_skl(sK1_skl),X0)|~program(sK3_skl(sK1_skl))|outputs(X0,good)|~sQ20_spl)),
% 0.15/0.53 inference(resolution,[status(thm)],[f332,f62])).
% 0.15/0.53 fof(f437,definition,(
% 0.15/0.53 ![X0]: (sQ45_spl <=> (sP3_prd(sK4_skl(sK1_skl),sK3_skl(sK1_skl),X0)|outputs(X0,good)))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f438,plain,(
% 0.15/0.53 ![X0]: (sP3_prd(sK4_skl(sK1_skl),sK3_skl(sK1_skl),X0)|outputs(X0,good)|~sQ45_spl)),
% 0.15/0.53 inference(component_clause,[status(thm)],[f437])).
% 0.15/0.53 fof(f440,plain,(
% 0.15/0.53 sQ45_spl|~sQ36_spl|~sQ20_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f432,f437,f313,f221])).
% 0.15/0.53 fof(f452,plain,(
% 0.15/0.53 ![X0]: (outputs(X0,good)|halts2(sK3_skl(sK1_skl),sK4_skl(sK1_skl))|~sQ45_spl)),
% 0.15/0.53 inference(resolution,[status(thm)],[f438,f59])).
% 0.15/0.53 fof(f454,plain,(
% 0.15/0.53 sQ17_spl|sQ21_spl|~sQ45_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f452,f166,f224,f437])).
% 0.15/0.53 fof(f456,plain,(
% 0.15/0.53 $false|~sQ10_spl|sQ36_spl),
% 0.15/0.53 inference(forward_subsumption_resolution,[status(thm)],[f315,f215])).
% 0.15/0.53 fof(f457,plain,(
% 0.15/0.53 ~sQ10_spl|sQ36_spl),
% 0.15/0.53 inference(contradiction_clause,[status(thm)],[f456])).
% 0.15/0.53 fof(f679,plain,(
% 0.15/0.53 $false|~sQ9_spl|~sQ10_spl|sQ19_spl),
% 0.15/0.53 inference(backward_subsumption_resolution,[status(thm)],[f219,f408])).
% 0.15/0.53 fof(f683,plain,(
% 0.15/0.53 ~sQ9_spl|~sQ10_spl|sQ19_spl),
% 0.15/0.53 inference(contradiction_clause,[status(thm)],[f679])).
% 0.15/0.53 fof(f686,plain,(
% 0.15/0.53 ![X0]: (halts3(sK1_skl,sK5_skl(sK1_skl),X0)|~sQ11_spl|~sQ9_spl)),
% 0.15/0.53 inference(resolution,[status(thm)],[f121,f113])).
% 0.15/0.53 fof(f688,plain,(
% 0.15/0.53 sP2_prd(sK4_skl(sK5_skl(sK1_skl)),sK3_skl(sK5_skl(sK1_skl)),sK5_skl(sK1_skl))|program(sK5_skl(sK5_skl(sK1_skl)))|~sQ11_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f121,f26])).
% 0.15/0.53 fof(f689,plain,(
% 0.15/0.53 ![X0,X1]: (sP1_prd(sK2_skl(sK5_skl(sK1_skl)),sK5_skl(sK1_skl))|~program(X0)|halts3(sK5_skl(sK1_skl),X0,X1)|~sQ11_spl)),
% 0.15/0.53 inference(resolution,[status(thm)],[f121,f110])).
% 0.15/0.53 fof(f693,definition,(
% 0.15/0.53 sQ64_spl <=> (sP2_prd(sK4_skl(sK5_skl(sK1_skl)),sK3_skl(sK5_skl(sK1_skl)),sK5_skl(sK1_skl)))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f694,plain,(
% 0.15/0.53 sP2_prd(sK4_skl(sK5_skl(sK1_skl)),sK3_skl(sK5_skl(sK1_skl)),sK5_skl(sK1_skl))|~sQ64_spl),
% 0.15/0.53 inference(component_clause,[status(thm)],[f693])).
% 0.15/0.53 fof(f696,definition,(
% 0.15/0.53 sQ65_spl <=> (program(sK5_skl(sK5_skl(sK1_skl))))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f697,plain,(
% 0.15/0.53 program(sK5_skl(sK5_skl(sK1_skl)))|~sQ65_spl),
% 0.15/0.53 inference(component_clause,[status(thm)],[f696])).
% 0.15/0.53 fof(f699,plain,(
% 0.15/0.53 sQ64_spl|sQ65_spl|~sQ11_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f688,f693,f696,f120])).
% 0.15/0.53 fof(f700,definition,(
% 0.15/0.53 sQ66_spl <=> (sP1_prd(sK2_skl(sK5_skl(sK1_skl)),sK5_skl(sK1_skl)))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f701,plain,(
% 0.15/0.53 sP1_prd(sK2_skl(sK5_skl(sK1_skl)),sK5_skl(sK1_skl))|~sQ66_spl),
% 0.15/0.53 inference(component_clause,[status(thm)],[f700])).
% 0.15/0.53 fof(f703,definition,(
% 0.15/0.53 ![X0,X1]: (sQ67_spl <=> (~program(X0)|halts3(sK5_skl(sK1_skl),X0,X1)))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f706,plain,(
% 0.15/0.53 sQ66_spl|sQ67_spl|~sQ11_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f689,f700,f703,f120])).
% 0.15/0.53 fof(f728,definition,(
% 0.15/0.53 sQ68_spl <=> (outputs(sK5_skl(sK1_skl),good))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f752,definition,(
% 0.15/0.53 ![X1]: (sQ69_spl <=> (halts2(sK5_skl(sK1_skl),X1)))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f753,plain,(
% 0.15/0.53 ![X0]: (halts2(sK5_skl(sK1_skl),X0)|~sQ69_spl)),
% 0.15/0.53 inference(component_clause,[status(thm)],[f752])).
% 0.15/0.53 fof(f783,definition,(
% 0.15/0.53 sQ71_spl <=> (halts2(sK5_skl(sK1_skl),sK5_skl(sK1_skl)))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f794,definition,(
% 0.15/0.53 ![X0]: (sQ74_spl <=> (~program(X0)|sP2_prd(sK4_skl(X0),sK3_skl(X0),X0)|~outputs(X0,bad)|outputs(sK5_skl(X0),bad)))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f795,plain,(
% 0.15/0.53 ![X0]: (~program(X0)|sP2_prd(sK4_skl(X0),sK3_skl(X0),X0)|~outputs(X0,bad)|outputs(sK5_skl(X0),bad)|~sQ74_spl)),
% 0.15/0.53 inference(component_clause,[status(thm)],[f794])).
% 0.15/0.53 fof(f864,plain,(
% 0.15/0.53 ~program(sK5_skl(sK1_skl))|sP2_prd(sK4_skl(sK5_skl(sK1_skl)),sK3_skl(sK5_skl(sK1_skl)),sK5_skl(sK1_skl))|outputs(sK5_skl(sK5_skl(sK1_skl)),bad)|~sQ39_spl|~sQ74_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f380,f795])).
% 0.15/0.53 fof(f881,definition,(
% 0.15/0.53 sQ89_spl <=> (outputs(sK5_skl(sK5_skl(sK1_skl)),bad))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f884,plain,(
% 0.15/0.53 ~sQ11_spl|sQ64_spl|sQ89_spl|~sQ39_spl|~sQ74_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f864,f120,f693,f881,f379,f794])).
% 0.15/0.53 fof(f927,plain,(
% 0.15/0.53 ~program(sK1_skl)|sP2_prd(sK4_skl(sK1_skl),sK3_skl(sK1_skl),sK1_skl)|~program(sK5_skl(sK1_skl))|~outputs(sK1_skl,bad)|halts2(sK5_skl(sK1_skl),sK5_skl(sK1_skl))|~sQ11_spl|~sQ9_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f28,f686])).
% 0.15/0.53 fof(f930,plain,(
% 0.15/0.53 ~sQ1_spl|sQ10_spl|~sQ11_spl|~sQ12_spl|sQ71_spl|~sQ9_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f927,f66,f117,f120,f128,f783,f112])).
% 0.15/0.53 fof(f979,plain,(
% 0.15/0.53 ![X0]: (halts2(sK3_skl(sK1_skl),X0)|~sQ6_spl|~sQ36_spl)),
% 0.15/0.53 inference(resolution,[status(thm)],[f85,f314])).
% 0.15/0.53 fof(f1035,plain,(
% 0.15/0.53 ![X0]: (halts2(sK5_skl(sK1_skl),X0)|~sQ11_spl|~sQ6_spl)),
% 0.15/0.53 inference(resolution,[status(thm)],[f121,f85])).
% 0.15/0.53 fof(f1049,plain,(
% 0.15/0.53 sP3_prd(sK4_skl(sK5_skl(sK1_skl)),sK3_skl(sK5_skl(sK1_skl)),sK5_skl(sK1_skl))|~halts3(sK5_skl(sK1_skl),sK3_skl(sK5_skl(sK1_skl)),sK4_skl(sK5_skl(sK1_skl)))|~outputs(sK5_skl(sK1_skl),bad)|~sQ64_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f694,f52])).
% 0.15/0.53 fof(f1050,plain,(
% 0.15/0.53 program(sK3_skl(sK5_skl(sK1_skl)))|~sQ64_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f694,f124])).
% 0.15/0.53 fof(f1051,plain,(
% 0.15/0.53 sP3_prd(sK4_skl(sK5_skl(sK1_skl)),sK3_skl(sK5_skl(sK1_skl)),sK5_skl(sK1_skl))|~halts2(sK3_skl(sK5_skl(sK1_skl)),sK4_skl(sK5_skl(sK1_skl)))|~sQ64_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f694,f51])).
% 0.15/0.53 fof(f1052,definition,(
% 0.15/0.53 sQ94_spl <=> (sP3_prd(sK4_skl(sK5_skl(sK1_skl)),sK3_skl(sK5_skl(sK1_skl)),sK5_skl(sK1_skl)))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f1053,plain,(
% 0.15/0.53 sP3_prd(sK4_skl(sK5_skl(sK1_skl)),sK3_skl(sK5_skl(sK1_skl)),sK5_skl(sK1_skl))|~sQ94_spl),
% 0.15/0.53 inference(component_clause,[status(thm)],[f1052])).
% 0.15/0.53 fof(f1055,definition,(
% 0.15/0.53 sQ95_spl <=> (halts3(sK5_skl(sK1_skl),sK3_skl(sK5_skl(sK1_skl)),sK4_skl(sK5_skl(sK1_skl))))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f1058,plain,(
% 0.15/0.53 sQ94_spl|~sQ95_spl|~sQ39_spl|~sQ64_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f1049,f1052,f1055,f379,f693])).
% 0.15/0.53 fof(f1059,definition,(
% 0.15/0.53 sQ96_spl <=> (halts2(sK3_skl(sK5_skl(sK1_skl)),sK4_skl(sK5_skl(sK1_skl))))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f1062,plain,(
% 0.15/0.53 sQ94_spl|~sQ96_spl|~sQ64_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f1051,f1052,f1059,f693])).
% 0.15/0.53 fof(f1073,plain,(
% 0.15/0.53 sP2_prd(sK4_skl(sK5_skl(sK5_skl(sK1_skl))),sK3_skl(sK5_skl(sK5_skl(sK1_skl))),sK5_skl(sK5_skl(sK1_skl)))|program(sK5_skl(sK5_skl(sK5_skl(sK1_skl))))|~sQ65_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f697,f26])).
% 0.15/0.53 fof(f1074,plain,(
% 0.15/0.53 ![X0,X1]: (sP1_prd(sK2_skl(sK5_skl(sK5_skl(sK1_skl))),sK5_skl(sK5_skl(sK1_skl)))|~program(X0)|halts3(sK5_skl(sK5_skl(sK1_skl)),X0,X1)|~sQ65_spl)),
% 0.15/0.53 inference(resolution,[status(thm)],[f697,f110])).
% 0.15/0.53 fof(f1078,definition,(
% 0.15/0.53 sQ97_spl <=> (sP1_prd(sK2_skl(sK5_skl(sK5_skl(sK1_skl))),sK5_skl(sK5_skl(sK1_skl))))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f1085,definition,(
% 0.15/0.53 sQ99_spl <=> (sP2_prd(sK4_skl(sK5_skl(sK5_skl(sK1_skl))),sK3_skl(sK5_skl(sK5_skl(sK1_skl))),sK5_skl(sK5_skl(sK1_skl))))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f1086,plain,(
% 0.15/0.53 sP2_prd(sK4_skl(sK5_skl(sK5_skl(sK1_skl))),sK3_skl(sK5_skl(sK5_skl(sK1_skl))),sK5_skl(sK5_skl(sK1_skl)))|~sQ99_spl),
% 0.15/0.53 inference(component_clause,[status(thm)],[f1085])).
% 0.15/0.53 fof(f1088,definition,(
% 0.15/0.53 sQ100_spl <=> (program(sK5_skl(sK5_skl(sK5_skl(sK1_skl)))))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f1089,plain,(
% 0.15/0.53 program(sK5_skl(sK5_skl(sK5_skl(sK1_skl))))|~sQ100_spl),
% 0.15/0.53 inference(component_clause,[status(thm)],[f1088])).
% 0.15/0.53 fof(f1091,plain,(
% 0.15/0.53 sQ99_spl|sQ100_spl|~sQ65_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f1073,f1085,f1088,f696])).
% 0.15/0.53 fof(f1092,definition,(
% 0.15/0.53 ![X0,X1]: (sQ101_spl <=> (~program(X0)|halts3(sK5_skl(sK5_skl(sK1_skl)),X0,X1)))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f1095,plain,(
% 0.15/0.53 sQ97_spl|sQ101_spl|~sQ65_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f1074,f1078,f1092,f696])).
% 0.15/0.53 fof(f1125,plain,(
% 0.15/0.53 program(sK2_skl(sK5_skl(sK1_skl)))|~sQ66_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f701,f43])).
% 0.15/0.53 fof(f1130,plain,(
% 0.15/0.53 ~program(sK1_skl)|sP2_prd(sK4_skl(sK1_skl),sK3_skl(sK1_skl),sK1_skl)|~program(sK5_skl(sK1_skl))|~outputs(sK1_skl,good)|~halts2(sK5_skl(sK1_skl),sK5_skl(sK1_skl))|~sQ11_spl|~sQ9_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f686,f27])).
% 0.15/0.53 fof(f1132,plain,(
% 0.15/0.53 ~sQ1_spl|sQ10_spl|~sQ11_spl|~sQ13_spl|~sQ71_spl|~sQ9_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f1130,f66,f117,f120,f133,f783,f112])).
% 0.15/0.53 fof(f1144,plain,(
% 0.15/0.53 sQ35_spl|~sQ6_spl|~sQ36_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f979,f310,f84,f313])).
% 0.15/0.53 fof(f1221,plain,(
% 0.15/0.53 $false|~sQ69_spl|sQ38_spl),
% 0.15/0.53 inference(forward_subsumption_resolution,[status(thm)],[f356,f753])).
% 0.15/0.53 fof(f1222,plain,(
% 0.15/0.53 ~sQ69_spl|sQ38_spl),
% 0.15/0.53 inference(contradiction_clause,[status(thm)],[f1221])).
% 0.15/0.53 fof(f1223,plain,(
% 0.15/0.53 sQ69_spl|~sQ11_spl|~sQ6_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f1035,f752,f120,f84])).
% 0.15/0.53 fof(f1230,plain,(
% 0.15/0.53 ~program(sK3_skl(sK1_skl))|~sQ4_spl|~sQ21_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f78,f225])).
% 0.15/0.53 fof(f1240,plain,(
% 0.15/0.53 sP2_prd(sK4_skl(sK3_skl(sK5_skl(sK1_skl))),sK3_skl(sK3_skl(sK5_skl(sK1_skl))),sK3_skl(sK5_skl(sK1_skl)))|program(sK5_skl(sK3_skl(sK5_skl(sK1_skl))))|~sQ64_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f1050,f26])).
% 0.15/0.53 fof(f1241,plain,(
% 0.15/0.53 ![X0,X1]: (sP1_prd(sK2_skl(sK3_skl(sK5_skl(sK1_skl))),sK3_skl(sK5_skl(sK1_skl)))|~program(X0)|halts3(sK3_skl(sK5_skl(sK1_skl)),X0,X1)|~sQ64_spl)),
% 0.15/0.53 inference(resolution,[status(thm)],[f1050,f110])).
% 0.15/0.53 fof(f1245,definition,(
% 0.15/0.53 sQ115_spl <=> (sP2_prd(sK4_skl(sK3_skl(sK5_skl(sK1_skl))),sK3_skl(sK3_skl(sK5_skl(sK1_skl))),sK3_skl(sK5_skl(sK1_skl))))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f1248,definition,(
% 0.15/0.53 sQ116_spl <=> (program(sK5_skl(sK3_skl(sK5_skl(sK1_skl)))))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f1251,plain,(
% 0.15/0.53 sQ115_spl|sQ116_spl|~sQ64_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f1240,f1245,f1248,f693])).
% 0.15/0.53 fof(f1252,definition,(
% 0.15/0.53 sQ117_spl <=> (sP1_prd(sK2_skl(sK3_skl(sK5_skl(sK1_skl))),sK3_skl(sK5_skl(sK1_skl))))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f1255,definition,(
% 0.15/0.53 ![X0,X1]: (sQ118_spl <=> (~program(X0)|halts3(sK3_skl(sK5_skl(sK1_skl)),X0,X1)))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f1258,plain,(
% 0.15/0.53 sQ117_spl|sQ118_spl|~sQ64_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f1241,f1252,f1255,f693])).
% 0.15/0.53 fof(f1271,plain,(
% 0.15/0.53 ~halts3(sK5_skl(sK1_skl),sK3_skl(sK5_skl(sK1_skl)),sK4_skl(sK5_skl(sK1_skl)))|~outputs(sK5_skl(sK1_skl),good)|~sQ94_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f1053,f60])).
% 0.15/0.53 fof(f1275,plain,(
% 0.15/0.53 ~sQ95_spl|~sQ68_spl|~sQ94_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f1271,f1055,f728,f1052])).
% 0.15/0.53 fof(f1343,plain,(
% 0.15/0.53 sP2_prd(sK4_skl(sK2_skl(sK5_skl(sK1_skl))),sK3_skl(sK2_skl(sK5_skl(sK1_skl))),sK2_skl(sK5_skl(sK1_skl)))|program(sK5_skl(sK2_skl(sK5_skl(sK1_skl))))|~sQ66_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f1125,f26])).
% 0.15/0.53 fof(f1344,plain,(
% 0.15/0.53 ![X0,X1]: (sP1_prd(sK2_skl(sK2_skl(sK5_skl(sK1_skl))),sK2_skl(sK5_skl(sK1_skl)))|~program(X0)|halts3(sK2_skl(sK5_skl(sK1_skl)),X0,X1)|~sQ66_spl)),
% 0.15/0.53 inference(resolution,[status(thm)],[f1125,f110])).
% 0.15/0.53 fof(f1348,definition,(
% 0.15/0.53 sQ120_spl <=> (sP1_prd(sK2_skl(sK2_skl(sK5_skl(sK1_skl))),sK2_skl(sK5_skl(sK1_skl))))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f1355,definition,(
% 0.15/0.53 sQ122_spl <=> (sP2_prd(sK4_skl(sK2_skl(sK5_skl(sK1_skl))),sK3_skl(sK2_skl(sK5_skl(sK1_skl))),sK2_skl(sK5_skl(sK1_skl))))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f1358,definition,(
% 0.15/0.53 sQ123_spl <=> (program(sK5_skl(sK2_skl(sK5_skl(sK1_skl)))))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f1361,plain,(
% 0.15/0.53 sQ122_spl|sQ123_spl|~sQ66_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f1343,f1355,f1358,f700])).
% 0.15/0.53 fof(f1362,definition,(
% 0.15/0.53 ![X0,X1]: (sQ124_spl <=> (~program(X0)|halts3(sK2_skl(sK5_skl(sK1_skl)),X0,X1)))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f1365,plain,(
% 0.15/0.53 sQ120_spl|sQ124_spl|~sQ66_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f1344,f1348,f1362,f700])).
% 0.15/0.53 fof(f1379,plain,(
% 0.15/0.53 sP2_prd(sK4_skl(sK5_skl(sK5_skl(sK5_skl(sK1_skl)))),sK3_skl(sK5_skl(sK5_skl(sK5_skl(sK1_skl)))),sK5_skl(sK5_skl(sK5_skl(sK1_skl))))|program(sK5_skl(sK5_skl(sK5_skl(sK5_skl(sK1_skl)))))|~sQ100_spl),
% 0.15/0.53 inference(resolution,[status(thm)],[f1089,f26])).
% 0.15/0.53 fof(f1380,plain,(
% 0.15/0.53 ![X0,X1]: (sP1_prd(sK2_skl(sK5_skl(sK5_skl(sK5_skl(sK1_skl)))),sK5_skl(sK5_skl(sK5_skl(sK1_skl))))|~program(X0)|halts3(sK5_skl(sK5_skl(sK5_skl(sK1_skl))),X0,X1)|~sQ100_spl)),
% 0.15/0.53 inference(resolution,[status(thm)],[f1089,f110])).
% 0.15/0.53 fof(f1384,definition,(
% 0.15/0.53 sQ125_spl <=> (sP1_prd(sK2_skl(sK5_skl(sK5_skl(sK5_skl(sK1_skl)))),sK5_skl(sK5_skl(sK5_skl(sK1_skl)))))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f1391,definition,(
% 0.15/0.53 sQ127_spl <=> (sP2_prd(sK4_skl(sK5_skl(sK5_skl(sK5_skl(sK1_skl)))),sK3_skl(sK5_skl(sK5_skl(sK5_skl(sK1_skl)))),sK5_skl(sK5_skl(sK5_skl(sK1_skl)))))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f1394,definition,(
% 0.15/0.53 sQ128_spl <=> (program(sK5_skl(sK5_skl(sK5_skl(sK5_skl(sK1_skl))))))),
% 0.15/0.53 introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition])).
% 0.15/0.53 fof(f1397,plain,(
% 0.15/0.53 sQ127_spl|sQ128_spl|~sQ100_spl),
% 0.15/0.53 inference(split_clause,[status(thm)],[f1379,f1391,f1394,f1088])).
% 0.15/0.53 fof(f1398,definition,(
% 0.15/0.53 ![X0,X1]: (sQ129_spl <=> (~program(X0)|halts3(sK5_skl(sK5_skl(sK5_skl(sK1_skl))),X0,X1)))),
% 0.15/0.54 introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition])).
% 0.15/0.54 fof(f1401,plain,(
% 0.15/0.54 sQ125_spl|sQ129_spl|~sQ100_spl),
% 0.15/0.54 inference(split_clause,[status(thm)],[f1380,f1384,f1398,f1088])).
% 0.15/0.54 fof(f1419,plain,(
% 0.15/0.54 sP3_prd(sK4_skl(sK5_skl(sK5_skl(sK1_skl))),sK3_skl(sK5_skl(sK5_skl(sK1_skl))),sK5_skl(sK5_skl(sK1_skl)))|~halts3(sK5_skl(sK5_skl(sK1_skl)),sK3_skl(sK5_skl(sK5_skl(sK1_skl))),sK4_skl(sK5_skl(sK5_skl(sK1_skl))))|~outputs(sK5_skl(sK5_skl(sK1_skl)),bad)|~sQ99_spl),
% 0.15/0.54 inference(resolution,[status(thm)],[f1086,f52])).
% 0.15/0.54 fof(f1421,plain,(
% 0.15/0.54 sP3_prd(sK4_skl(sK5_skl(sK5_skl(sK1_skl))),sK3_skl(sK5_skl(sK5_skl(sK1_skl))),sK5_skl(sK5_skl(sK1_skl)))|~halts2(sK3_skl(sK5_skl(sK5_skl(sK1_skl))),sK4_skl(sK5_skl(sK5_skl(sK1_skl))))|~sQ99_spl),
% 0.15/0.54 inference(resolution,[status(thm)],[f1086,f51])).
% 0.15/0.54 fof(f1422,definition,(
% 0.15/0.54 sQ131_spl <=> (sP3_prd(sK4_skl(sK5_skl(sK5_skl(sK1_skl))),sK3_skl(sK5_skl(sK5_skl(sK1_skl))),sK5_skl(sK5_skl(sK1_skl))))),
% 0.15/0.54 introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition])).
% 0.15/0.54 fof(f1425,definition,(
% 0.15/0.54 sQ132_spl <=> (halts3(sK5_skl(sK5_skl(sK1_skl)),sK3_skl(sK5_skl(sK5_skl(sK1_skl))),sK4_skl(sK5_skl(sK5_skl(sK1_skl)))))),
% 0.15/0.54 introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition])).
% 0.15/0.54 fof(f1428,plain,(
% 0.15/0.54 sQ131_spl|~sQ132_spl|~sQ89_spl|~sQ99_spl),
% 0.15/0.54 inference(split_clause,[status(thm)],[f1419,f1422,f1425,f881,f1085])).
% 0.15/0.54 fof(f1429,definition,(
% 0.15/0.54 sQ133_spl <=> (halts2(sK3_skl(sK5_skl(sK5_skl(sK1_skl))),sK4_skl(sK5_skl(sK5_skl(sK1_skl)))))),
% 0.15/0.54 introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition])).
% 0.15/0.54 fof(f1432,plain,(
% 0.15/0.54 sQ131_spl|~sQ133_spl|~sQ99_spl),
% 0.15/0.54 inference(split_clause,[status(thm)],[f1421,f1422,f1429,f1085])).
% 0.15/0.54 fof(f1495,plain,(
% 0.15/0.54 ~program(sK5_skl(sK1_skl))|~sQ38_spl|~sQ4_spl),
% 0.15/0.54 inference(resolution,[status(thm)],[f355,f78])).
% 0.15/0.54 fof(f1496,plain,(
% 0.15/0.54 ~sQ11_spl|~sQ38_spl|~sQ4_spl),
% 0.15/0.54 inference(split_clause,[status(thm)],[f1495,f120,f354,f77])).
% 0.15/0.54 fof(f1497,plain,(
% 0.15/0.54 $false|~sQ35_spl|sQ21_spl),
% 0.15/0.54 inference(forward_subsumption_resolution,[status(thm)],[f226,f311])).
% 0.15/0.54 fof(f1498,plain,(
% 0.15/0.54 ~sQ35_spl|sQ21_spl),
% 0.15/0.54 inference(contradiction_clause,[status(thm)],[f1497])).
% 0.15/0.54 fof(f1500,plain,(
% 0.15/0.54 ~sQ36_spl|~sQ4_spl|~sQ21_spl),
% 0.15/0.54 inference(split_clause,[status(thm)],[f1230,f313,f77,f224])).
% 0.15/0.54 fof(f1501,plain,(
% 0.15/0.54 $false),
% 0.15/0.54 inference(sat_refutation,[status(thm)],[f69,f73,f80,f87,f94,f109,f115,f123,f131,f136,f194,f220,f227,f337,f338,f347,f349,f357,f413,f414,f415,f440,f454,f457,f683,f699,f706,f884,f930,f1058,f1062,f1091,f1095,f1132,f1144,f1222,f1223,f1251,f1258,f1275,f1361,f1365,f1397,f1401,f1428,f1432,f1496,f1498,f1500])).
% 0.15/0.54 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/0.57 % Elapsed time: 0.127267 seconds
% 0.15/0.57 % CPU time: 0.606480 seconds
% 0.15/0.57 % Total memory used: 19.765 MB
% 0.15/0.57 % Net memory used: 19.418 MB
%------------------------------------------------------------------------------