%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : COM003+1 : 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 : n026.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:40 PM UTC 2026
% Result : Theorem 15.16s 2.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COM003+1 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n026.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 21 14:16:22 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.13/0.36 % Drodi V4.1.1
% 15.16/2.41 % Refutation found
% 15.16/2.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 15.16/2.41 % SZS output start CNFRefutation for theBenchmark
% 15.16/2.41 fof(f1,axiom,(
% 15.16/2.41 ( (? [X] :( algorithm(X)& (! [Y] :( program(Y)=> (! [Z] : decides(X,Y,Z) )) )))=> (? [W] :( program(W)& (! [Y] :( program(Y)=> (! [Z] : decides(W,Y,Z) )) )) )) ),
% 15.16/2.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.16/2.41 fof(f2,axiom,(
% 15.16/2.41 (! [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) ) ) ) )) )),
% 15.16/2.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.16/2.41 fof(f3,axiom,(
% 15.16/2.41 ( (? [W] :( program(W)& (! [Y] :( ( ( program(Y)& halts2(Y,Y) )=> ( halts3(W,Y,Y)& outputs(W,good) ) )& ( ( program(Y)& ~ halts2(Y,Y) )=> ( halts3(W,Y,Y)& outputs(W,bad) ) ) ) )))=> (? [V] :( program(V)& (! [Y] :( ( ( program(Y)& halts2(Y,Y) )=> ( halts2(V,Y)& outputs(V,good) ) )& ( ( program(Y)& ~ halts2(Y,Y) )=> ( halts2(V,Y)& outputs(V,bad) ) ) ) )) )) ),
% 15.16/2.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.16/2.41 fof(f4,axiom,(
% 15.16/2.41 ( (? [V] :( program(V)& (! [Y] :( ( ( program(Y)& halts2(Y,Y) )=> ( halts2(V,Y)& outputs(V,good) ) )& ( ( program(Y)& ~ halts2(Y,Y) )=> ( halts2(V,Y)& outputs(V,bad) ) ) ) )))=> (? [U] :( program(U)& (! [Y] :( ( ( program(Y)& halts2(Y,Y) )=> ~ halts2(U,Y) )& ( ( program(Y)& ~ halts2(Y,Y) )=> ( halts2(U,Y)& outputs(U,bad) ) ) ) )) )) ),
% 15.16/2.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.16/2.41 fof(f5,conjecture,(
% 15.16/2.41 ~ (? [X1] :( algorithm(X1)& (! [Y1] :( program(Y1)=> (! [Z1] : decides(X1,Y1,Z1) )) )) )),
% 15.16/2.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.16/2.41 fof(f6,negated_conjecture,(
% 15.16/2.41 ~(~ (? [X1] :( algorithm(X1)& (! [Y1] :( program(Y1)=> (! [Z1] : decides(X1,Y1,Z1) )) )) ))),
% 15.16/2.41 inference(negated_conjecture,[status(cth)],[f5])).
% 15.16/2.41 fof(f7,plain,(
% 15.16/2.41 (![X]: (~algorithm(X)|(?[Y]: (program(Y)&(?[Z]: ~decides(X,Y,Z))))))|(?[W]: (program(W)&(![Y]: (~program(Y)|(![Z]: decides(W,Y,Z))))))),
% 15.16/2.41 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 15.16/2.41 fof(f8,definition,(
% 15.16/2.41 ![X,Y]: (sP0_prd(Y,X)<=>(program(Y)&(?[Z]: ~decides(X,Y,Z))))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 15.16/2.41 fof(f9,plain,(
% 15.16/2.41 (![X]: (~algorithm(X)|(?[Y]: sP0_prd(Y,X))))|(?[W]: (program(W)&(![Y]: (~program(Y)|(![Z]: decides(W,Y,Z))))))),
% 15.16/2.41 inference(formula_renaming,[status(thm)],[f7,f8])).
% 15.16/2.41 fof(f10,plain,(
% 15.16/2.41 (![X]: (~algorithm(X)|sP0_prd(sK0_skl(X),X)))|(program(sK1_skl)&(![Y]: (~program(Y)|(![Z]: decides(sK1_skl,Y,Z)))))),
% 15.16/2.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(Y,sK0_skl(X)),skolemize(W,sK1_skl)],[f9])).
% 15.16/2.41 fof(f11,plain,(
% 15.16/2.41 ![X0]: (~algorithm(X0)|sP0_prd(sK0_skl(X0),X0)|program(sK1_skl))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f10])).
% 15.16/2.41 fof(f12,plain,(
% 15.16/2.41 ![X0,X1,X2]: (~algorithm(X0)|sP0_prd(sK0_skl(X0),X0)|~program(X1)|decides(sK1_skl,X1,X2))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f10])).
% 15.16/2.41 fof(f13,plain,(
% 15.16/2.41 ![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))))))),
% 15.16/2.41 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 15.16/2.41 fof(f14,definition,(
% 15.16/2.41 ![W,Y]: (sP1_prd(Y,W)<=>(program(Y)&(?[Z]: ~decides(W,Y,Z))))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 15.16/2.41 fof(f15,plain,(
% 15.16/2.41 ![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))))))),
% 15.16/2.41 inference(formula_renaming,[status(thm)],[f13,f14])).
% 15.16/2.41 fof(f16,plain,(
% 15.16/2.41 ![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))))))),
% 15.16/2.41 inference(miniscoping,[status(thm)],[f15])).
% 15.16/2.41 fof(f17,plain,(
% 15.16/2.41 ![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))))))),
% 15.16/2.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(Y,sK2_skl(W))],[f16])).
% 15.16/2.41 fof(f18,plain,(
% 15.16/2.41 ![X0,X1,X2]: (~program(X0)|sP1_prd(sK2_skl(X0),X0)|~program(X1)|~halts2(X1,X2)|halts3(X0,X1,X2))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f17])).
% 15.16/2.41 fof(f19,plain,(
% 15.16/2.41 ![X0,X1,X2]: (~program(X0)|sP1_prd(sK2_skl(X0),X0)|~program(X1)|~halts2(X1,X2)|outputs(X0,good))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f17])).
% 15.16/2.41 fof(f20,plain,(
% 15.16/2.41 ![X0,X1,X2]: (~program(X0)|sP1_prd(sK2_skl(X0),X0)|~program(X1)|halts2(X1,X2)|halts3(X0,X1,X2))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f17])).
% 15.16/2.41 fof(f21,plain,(
% 15.16/2.41 ![X0,X1,X2]: (~program(X0)|sP1_prd(sK2_skl(X0),X0)|~program(X1)|halts2(X1,X2)|outputs(X0,bad))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f17])).
% 15.16/2.41 fof(f22,plain,(
% 15.16/2.41 (![W]: (~program(W)|(?[Y]: (((program(Y)&halts2(Y,Y))&(~halts3(W,Y,Y)|~outputs(W,good)))|((program(Y)&~halts2(Y,Y))&(~halts3(W,Y,Y)|~outputs(W,bad)))))))|(?[V]: (program(V)&(![Y]: (((~program(Y)|~halts2(Y,Y))|(halts2(V,Y)&outputs(V,good)))&((~program(Y)|halts2(Y,Y))|(halts2(V,Y)&outputs(V,bad)))))))),
% 15.16/2.41 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 15.16/2.41 fof(f23,definition,(
% 15.16/2.41 ![W,Y]: (sP2_prd(Y,W)<=>(((program(Y)&halts2(Y,Y))&(~halts3(W,Y,Y)|~outputs(W,good)))|((program(Y)&~halts2(Y,Y))&(~halts3(W,Y,Y)|~outputs(W,bad)))))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 15.16/2.41 fof(f24,plain,(
% 15.16/2.41 (![W]: (~program(W)|(?[Y]: sP2_prd(Y,W))))|(?[V]: (program(V)&(![Y]: (((~program(Y)|~halts2(Y,Y))|(halts2(V,Y)&outputs(V,good)))&((~program(Y)|halts2(Y,Y))|(halts2(V,Y)&outputs(V,bad)))))))),
% 15.16/2.41 inference(formula_renaming,[status(thm)],[f22,f23])).
% 15.16/2.41 fof(f25,plain,(
% 15.16/2.41 (![W]: (~program(W)|(?[Y]: sP2_prd(Y,W))))|(?[V]: (program(V)&((![Y]: ((~program(Y)|~halts2(Y,Y))|(halts2(V,Y)&outputs(V,good))))&(![Y]: ((~program(Y)|halts2(Y,Y))|(halts2(V,Y)&outputs(V,bad)))))))),
% 15.16/2.41 inference(miniscoping,[status(thm)],[f24])).
% 15.16/2.41 fof(f26,plain,(
% 15.16/2.41 (![W]: (~program(W)|sP2_prd(sK3_skl(W),W)))|(program(sK4_skl)&((![Y]: ((~program(Y)|~halts2(Y,Y))|(halts2(sK4_skl,Y)&outputs(sK4_skl,good))))&(![Y]: ((~program(Y)|halts2(Y,Y))|(halts2(sK4_skl,Y)&outputs(sK4_skl,bad))))))),
% 15.16/2.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl]),skolemize(Y,sK3_skl(W)),skolemize(V,sK4_skl)],[f25])).
% 15.16/2.41 fof(f27,plain,(
% 15.16/2.41 ![X0]: (~program(X0)|sP2_prd(sK3_skl(X0),X0)|program(sK4_skl))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f26])).
% 15.16/2.41 fof(f28,plain,(
% 15.16/2.41 ![X0,X1]: (~program(X0)|sP2_prd(sK3_skl(X0),X0)|~program(X1)|~halts2(X1,X1)|halts2(sK4_skl,X1))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f26])).
% 15.16/2.41 fof(f29,plain,(
% 15.16/2.41 ![X0,X1]: (~program(X0)|sP2_prd(sK3_skl(X0),X0)|~program(X1)|~halts2(X1,X1)|outputs(sK4_skl,good))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f26])).
% 15.16/2.41 fof(f30,plain,(
% 15.16/2.41 ![X0,X1]: (~program(X0)|sP2_prd(sK3_skl(X0),X0)|~program(X1)|halts2(X1,X1)|halts2(sK4_skl,X1))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f26])).
% 15.16/2.41 fof(f31,plain,(
% 15.16/2.41 ![X0,X1]: (~program(X0)|sP2_prd(sK3_skl(X0),X0)|~program(X1)|halts2(X1,X1)|outputs(sK4_skl,bad))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f26])).
% 15.16/2.41 fof(f32,plain,(
% 15.16/2.41 (![V]: (~program(V)|(?[Y]: (((program(Y)&halts2(Y,Y))&(~halts2(V,Y)|~outputs(V,good)))|((program(Y)&~halts2(Y,Y))&(~halts2(V,Y)|~outputs(V,bad)))))))|(?[U]: (program(U)&(![Y]: (((~program(Y)|~halts2(Y,Y))|~halts2(U,Y))&((~program(Y)|halts2(Y,Y))|(halts2(U,Y)&outputs(U,bad)))))))),
% 15.16/2.41 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 15.16/2.41 fof(f33,definition,(
% 15.16/2.41 ![V,Y]: (sP3_prd(Y,V)<=>(((program(Y)&halts2(Y,Y))&(~halts2(V,Y)|~outputs(V,good)))|((program(Y)&~halts2(Y,Y))&(~halts2(V,Y)|~outputs(V,bad)))))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 15.16/2.41 fof(f34,plain,(
% 15.16/2.41 (![V]: (~program(V)|(?[Y]: sP3_prd(Y,V))))|(?[U]: (program(U)&(![Y]: (((~program(Y)|~halts2(Y,Y))|~halts2(U,Y))&((~program(Y)|halts2(Y,Y))|(halts2(U,Y)&outputs(U,bad)))))))),
% 15.16/2.41 inference(formula_renaming,[status(thm)],[f32,f33])).
% 15.16/2.41 fof(f35,plain,(
% 15.16/2.41 (![V]: (~program(V)|(?[Y]: sP3_prd(Y,V))))|(?[U]: (program(U)&((![Y]: ((~program(Y)|~halts2(Y,Y))|~halts2(U,Y)))&(![Y]: ((~program(Y)|halts2(Y,Y))|(halts2(U,Y)&outputs(U,bad)))))))),
% 15.16/2.41 inference(miniscoping,[status(thm)],[f34])).
% 15.16/2.41 fof(f36,plain,(
% 15.16/2.41 (![V]: (~program(V)|sP3_prd(sK5_skl(V),V)))|(program(sK6_skl)&((![Y]: ((~program(Y)|~halts2(Y,Y))|~halts2(sK6_skl,Y)))&(![Y]: ((~program(Y)|halts2(Y,Y))|(halts2(sK6_skl,Y)&outputs(sK6_skl,bad))))))),
% 15.16/2.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl,sK6_skl]),skolemize(Y,sK5_skl(V)),skolemize(U,sK6_skl)],[f35])).
% 15.16/2.41 fof(f37,plain,(
% 15.16/2.41 ![X0]: (~program(X0)|sP3_prd(sK5_skl(X0),X0)|program(sK6_skl))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f36])).
% 15.16/2.41 fof(f38,plain,(
% 15.16/2.41 ![X0,X1]: (~program(X0)|sP3_prd(sK5_skl(X0),X0)|~program(X1)|~halts2(X1,X1)|~halts2(sK6_skl,X1))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f36])).
% 15.16/2.41 fof(f39,plain,(
% 15.16/2.41 ![X0,X1]: (~program(X0)|sP3_prd(sK5_skl(X0),X0)|~program(X1)|halts2(X1,X1)|halts2(sK6_skl,X1))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f36])).
% 15.16/2.41 fof(f41,plain,(
% 15.16/2.41 ?[X1]: (algorithm(X1)&(![Y1]: (~program(Y1)|(![Z1]: decides(X1,Y1,Z1)))))),
% 15.16/2.41 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 15.16/2.41 fof(f42,plain,(
% 15.16/2.41 (algorithm(sK7_skl)&(![Y1]: (~program(Y1)|(![Z1]: decides(sK7_skl,Y1,Z1)))))),
% 15.16/2.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(X1,sK7_skl)],[f41])).
% 15.16/2.41 fof(f43,plain,(
% 15.16/2.41 algorithm(sK7_skl)),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f42])).
% 15.16/2.41 fof(f44,plain,(
% 15.16/2.41 ![X0,X1]: (~program(X0)|decides(sK7_skl,X0,X1))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f42])).
% 15.16/2.41 fof(f45,plain,(
% 15.16/2.41 ![X,Y]: ((~sP0_prd(Y,X)|(program(Y)&(?[Z]: ~decides(X,Y,Z))))&(sP0_prd(Y,X)|(~program(Y)|(![Z]: decides(X,Y,Z)))))),
% 15.16/2.41 inference(NNF_transformation,[status(thm)],[f8])).
% 15.16/2.41 fof(f46,plain,(
% 15.16/2.41 (![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)))))),
% 15.16/2.41 inference(miniscoping,[status(thm)],[f45])).
% 15.16/2.41 fof(f47,plain,(
% 15.16/2.41 (![X,Y]: (~sP0_prd(Y,X)|(program(Y)&~decides(X,Y,sK8_skl(Y,X)))))&(![X,Y]: (sP0_prd(Y,X)|(~program(Y)|(![Z]: decides(X,Y,Z)))))),
% 15.16/2.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl]),skolemize(Z,sK8_skl(Y,X))],[f46])).
% 15.16/2.41 fof(f48,plain,(
% 15.16/2.41 ![X0,X1]: (~sP0_prd(X0,X1)|program(X0))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f47])).
% 15.16/2.41 fof(f49,plain,(
% 15.16/2.41 ![X0,X1]: (~sP0_prd(X0,X1)|~decides(X1,X0,sK8_skl(X0,X1)))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f47])).
% 15.16/2.41 fof(f51,plain,(
% 15.16/2.41 ![W,Y]: ((~sP1_prd(Y,W)|(program(Y)&(?[Z]: ~decides(W,Y,Z))))&(sP1_prd(Y,W)|(~program(Y)|(![Z]: decides(W,Y,Z)))))),
% 15.16/2.41 inference(NNF_transformation,[status(thm)],[f14])).
% 15.16/2.41 fof(f52,plain,(
% 15.16/2.41 (![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)))))),
% 15.16/2.41 inference(miniscoping,[status(thm)],[f51])).
% 15.16/2.41 fof(f53,plain,(
% 15.16/2.41 (![W,Y]: (~sP1_prd(Y,W)|(program(Y)&~decides(W,Y,sK9_skl(Y,W)))))&(![W,Y]: (sP1_prd(Y,W)|(~program(Y)|(![Z]: decides(W,Y,Z)))))),
% 15.16/2.41 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl]),skolemize(Z,sK9_skl(Y,W))],[f52])).
% 15.16/2.41 fof(f54,plain,(
% 15.16/2.41 ![X0,X1]: (~sP1_prd(X0,X1)|program(X0))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f53])).
% 15.16/2.41 fof(f55,plain,(
% 15.16/2.41 ![X0,X1]: (~sP1_prd(X0,X1)|~decides(X1,X0,sK9_skl(X0,X1)))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f53])).
% 15.16/2.41 fof(f57,definition,(
% 15.16/2.41 ![W,Y]: (sP4_prd(Y,W)<=>((program(Y)&halts2(Y,Y))&(~halts3(W,Y,Y)|~outputs(W,good))))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 15.16/2.41 fof(f58,plain,(
% 15.16/2.41 ![W,Y]: (sP2_prd(Y,W)<=>(sP4_prd(Y,W)|((program(Y)&~halts2(Y,Y))&(~halts3(W,Y,Y)|~outputs(W,bad)))))),
% 15.16/2.41 inference(formula_renaming,[status(thm)],[f23,f57])).
% 15.16/2.41 fof(f59,plain,(
% 15.16/2.41 ![W,Y]: ((~sP2_prd(Y,W)|(sP4_prd(Y,W)|((program(Y)&~halts2(Y,Y))&(~halts3(W,Y,Y)|~outputs(W,bad)))))&(sP2_prd(Y,W)|(~sP4_prd(Y,W)&((~program(Y)|halts2(Y,Y))|(halts3(W,Y,Y)&outputs(W,bad))))))),
% 15.16/2.41 inference(NNF_transformation,[status(thm)],[f58])).
% 15.16/2.41 fof(f60,plain,(
% 15.16/2.41 (![W,Y]: (~sP2_prd(Y,W)|(sP4_prd(Y,W)|((program(Y)&~halts2(Y,Y))&(~halts3(W,Y,Y)|~outputs(W,bad))))))&(![W,Y]: (sP2_prd(Y,W)|(~sP4_prd(Y,W)&((~program(Y)|halts2(Y,Y))|(halts3(W,Y,Y)&outputs(W,bad))))))),
% 15.16/2.41 inference(miniscoping,[status(thm)],[f59])).
% 15.16/2.41 fof(f61,plain,(
% 15.16/2.41 ![X0,X1]: (~sP2_prd(X0,X1)|sP4_prd(X0,X1)|program(X0))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f60])).
% 15.16/2.41 fof(f62,plain,(
% 15.16/2.41 ![X0,X1]: (~sP2_prd(X0,X1)|sP4_prd(X0,X1)|~halts2(X0,X0))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f60])).
% 15.16/2.41 fof(f63,plain,(
% 15.16/2.41 ![X0,X1]: (~sP2_prd(X0,X1)|sP4_prd(X0,X1)|~halts3(X1,X0,X0)|~outputs(X1,bad))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f60])).
% 15.16/2.41 fof(f66,plain,(
% 15.16/2.41 ![X0,X1]: (sP2_prd(X0,X1)|~program(X0)|halts2(X0,X0)|outputs(X1,bad))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f60])).
% 15.16/2.41 fof(f67,definition,(
% 15.16/2.41 ![V,Y]: (sP5_prd(Y,V)<=>((program(Y)&halts2(Y,Y))&(~halts2(V,Y)|~outputs(V,good))))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 15.16/2.41 fof(f68,plain,(
% 15.16/2.41 ![V,Y]: (sP3_prd(Y,V)<=>(sP5_prd(Y,V)|((program(Y)&~halts2(Y,Y))&(~halts2(V,Y)|~outputs(V,bad)))))),
% 15.16/2.41 inference(formula_renaming,[status(thm)],[f33,f67])).
% 15.16/2.41 fof(f69,plain,(
% 15.16/2.41 ![V,Y]: ((~sP3_prd(Y,V)|(sP5_prd(Y,V)|((program(Y)&~halts2(Y,Y))&(~halts2(V,Y)|~outputs(V,bad)))))&(sP3_prd(Y,V)|(~sP5_prd(Y,V)&((~program(Y)|halts2(Y,Y))|(halts2(V,Y)&outputs(V,bad))))))),
% 15.16/2.41 inference(NNF_transformation,[status(thm)],[f68])).
% 15.16/2.41 fof(f70,plain,(
% 15.16/2.41 (![V,Y]: (~sP3_prd(Y,V)|(sP5_prd(Y,V)|((program(Y)&~halts2(Y,Y))&(~halts2(V,Y)|~outputs(V,bad))))))&(![V,Y]: (sP3_prd(Y,V)|(~sP5_prd(Y,V)&((~program(Y)|halts2(Y,Y))|(halts2(V,Y)&outputs(V,bad))))))),
% 15.16/2.41 inference(miniscoping,[status(thm)],[f69])).
% 15.16/2.41 fof(f71,plain,(
% 15.16/2.41 ![X0,X1]: (~sP3_prd(X0,X1)|sP5_prd(X0,X1)|program(X0))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f70])).
% 15.16/2.41 fof(f72,plain,(
% 15.16/2.41 ![X0,X1]: (~sP3_prd(X0,X1)|sP5_prd(X0,X1)|~halts2(X0,X0))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f70])).
% 15.16/2.41 fof(f73,plain,(
% 15.16/2.41 ![X0,X1]: (~sP3_prd(X0,X1)|sP5_prd(X0,X1)|~halts2(X1,X0)|~outputs(X1,bad))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f70])).
% 15.16/2.41 fof(f74,plain,(
% 15.16/2.41 ![X0,X1]: (sP3_prd(X0,X1)|~sP5_prd(X0,X1))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f70])).
% 15.16/2.41 fof(f75,plain,(
% 15.16/2.41 ![X0,X1]: (sP3_prd(X0,X1)|~program(X0)|halts2(X0,X0)|halts2(X1,X0))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f70])).
% 15.16/2.41 fof(f76,plain,(
% 15.16/2.41 ![X0,X1]: (sP3_prd(X0,X1)|~program(X0)|halts2(X0,X0)|outputs(X1,bad))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f70])).
% 15.16/2.41 fof(f77,plain,(
% 15.16/2.41 ![W,Y]: ((~sP4_prd(Y,W)|((program(Y)&halts2(Y,Y))&(~halts3(W,Y,Y)|~outputs(W,good))))&(sP4_prd(Y,W)|((~program(Y)|~halts2(Y,Y))|(halts3(W,Y,Y)&outputs(W,good)))))),
% 15.16/2.41 inference(NNF_transformation,[status(thm)],[f57])).
% 15.16/2.41 fof(f78,plain,(
% 15.16/2.41 (![W,Y]: (~sP4_prd(Y,W)|((program(Y)&halts2(Y,Y))&(~halts3(W,Y,Y)|~outputs(W,good)))))&(![W,Y]: (sP4_prd(Y,W)|((~program(Y)|~halts2(Y,Y))|(halts3(W,Y,Y)&outputs(W,good)))))),
% 15.16/2.41 inference(miniscoping,[status(thm)],[f77])).
% 15.16/2.41 fof(f79,plain,(
% 15.16/2.41 ![X0,X1]: (~sP4_prd(X0,X1)|program(X0))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f78])).
% 15.16/2.41 fof(f80,plain,(
% 15.16/2.41 ![X0,X1]: (~sP4_prd(X0,X1)|halts2(X0,X0))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f78])).
% 15.16/2.41 fof(f81,plain,(
% 15.16/2.41 ![X0,X1]: (~sP4_prd(X0,X1)|~halts3(X1,X0,X0)|~outputs(X1,good))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f78])).
% 15.16/2.41 fof(f83,plain,(
% 15.16/2.41 ![X0,X1]: (sP4_prd(X0,X1)|~program(X0)|~halts2(X0,X0)|outputs(X1,good))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f78])).
% 15.16/2.41 fof(f84,plain,(
% 15.16/2.41 ![V,Y]: ((~sP5_prd(Y,V)|((program(Y)&halts2(Y,Y))&(~halts2(V,Y)|~outputs(V,good))))&(sP5_prd(Y,V)|((~program(Y)|~halts2(Y,Y))|(halts2(V,Y)&outputs(V,good)))))),
% 15.16/2.41 inference(NNF_transformation,[status(thm)],[f67])).
% 15.16/2.41 fof(f85,plain,(
% 15.16/2.41 (![V,Y]: (~sP5_prd(Y,V)|((program(Y)&halts2(Y,Y))&(~halts2(V,Y)|~outputs(V,good)))))&(![V,Y]: (sP5_prd(Y,V)|((~program(Y)|~halts2(Y,Y))|(halts2(V,Y)&outputs(V,good)))))),
% 15.16/2.41 inference(miniscoping,[status(thm)],[f84])).
% 15.16/2.41 fof(f86,plain,(
% 15.16/2.41 ![X0,X1]: (~sP5_prd(X0,X1)|program(X0))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f85])).
% 15.16/2.41 fof(f87,plain,(
% 15.16/2.41 ![X0,X1]: (~sP5_prd(X0,X1)|halts2(X0,X0))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f85])).
% 15.16/2.41 fof(f88,plain,(
% 15.16/2.41 ![X0,X1]: (~sP5_prd(X0,X1)|~halts2(X1,X0)|~outputs(X1,good))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f85])).
% 15.16/2.41 fof(f89,plain,(
% 15.16/2.41 ![X0,X1]: (sP5_prd(X0,X1)|~program(X0)|~halts2(X0,X0)|halts2(X1,X0))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f85])).
% 15.16/2.41 fof(f90,plain,(
% 15.16/2.41 ![X0,X1]: (sP5_prd(X0,X1)|~program(X0)|~halts2(X0,X0)|outputs(X1,good))),
% 15.16/2.41 inference(cnf_transformation,[status(thm)],[f85])).
% 15.16/2.41 fof(f91,definition,(
% 15.16/2.41 ![X0]: (sQ0_spl <=> (~algorithm(X0)|sP0_prd(sK0_skl(X0),X0)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f92,plain,(
% 15.16/2.41 ![X0]: (~algorithm(X0)|sP0_prd(sK0_skl(X0),X0)|~sQ0_spl)),
% 15.16/2.41 inference(component_clause,[status(thm)],[f91])).
% 15.16/2.41 fof(f94,definition,(
% 15.16/2.41 sQ1_spl <=> (program(sK1_skl))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f95,plain,(
% 15.16/2.41 program(sK1_skl)|~sQ1_spl),
% 15.16/2.41 inference(component_clause,[status(thm)],[f94])).
% 15.16/2.41 fof(f97,plain,(
% 15.16/2.41 sQ0_spl|sQ1_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f11,f91,f94])).
% 15.16/2.41 fof(f98,definition,(
% 15.16/2.41 ![X1,X2]: (sQ2_spl <=> (~program(X1)|decides(sK1_skl,X1,X2)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f99,plain,(
% 15.16/2.41 ![X0,X1]: (~program(X0)|decides(sK1_skl,X0,X1)|~sQ2_spl)),
% 15.16/2.41 inference(component_clause,[status(thm)],[f98])).
% 15.16/2.41 fof(f101,plain,(
% 15.16/2.41 sQ0_spl|sQ2_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f12,f91,f98])).
% 15.16/2.41 fof(f102,definition,(
% 15.16/2.41 ![X0]: (sQ3_spl <=> (~program(X0)|sP1_prd(sK2_skl(X0),X0)|outputs(X0,good)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f103,plain,(
% 15.16/2.41 ![X0]: (~program(X0)|sP1_prd(sK2_skl(X0),X0)|outputs(X0,good)|~sQ3_spl)),
% 15.16/2.41 inference(component_clause,[status(thm)],[f102])).
% 15.16/2.41 fof(f105,definition,(
% 15.16/2.41 ![X1,X2]: (sQ4_spl <=> (~program(X1)|~halts2(X1,X2)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f106,plain,(
% 15.16/2.41 ![X0,X1]: (~program(X0)|~halts2(X0,X1)|~sQ4_spl)),
% 15.16/2.41 inference(component_clause,[status(thm)],[f105])).
% 15.16/2.41 fof(f108,plain,(
% 15.16/2.41 sQ3_spl|sQ4_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f19,f102,f105])).
% 15.16/2.41 fof(f109,definition,(
% 15.16/2.41 ![X0]: (sQ5_spl <=> (~program(X0)|sP1_prd(sK2_skl(X0),X0)|outputs(X0,bad)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f110,plain,(
% 15.16/2.41 ![X0]: (~program(X0)|sP1_prd(sK2_skl(X0),X0)|outputs(X0,bad)|~sQ5_spl)),
% 15.16/2.41 inference(component_clause,[status(thm)],[f109])).
% 15.16/2.41 fof(f112,definition,(
% 15.16/2.41 ![X1,X2]: (sQ6_spl <=> (~program(X1)|halts2(X1,X2)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f113,plain,(
% 15.16/2.41 ![X0,X1]: (~program(X0)|halts2(X0,X1)|~sQ6_spl)),
% 15.16/2.41 inference(component_clause,[status(thm)],[f112])).
% 15.16/2.41 fof(f115,plain,(
% 15.16/2.41 sQ5_spl|sQ6_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f21,f109,f112])).
% 15.16/2.41 fof(f116,definition,(
% 15.16/2.41 ![X0]: (sQ7_spl <=> (~program(X0)|sP2_prd(sK3_skl(X0),X0)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f117,plain,(
% 15.16/2.41 ![X0]: (~program(X0)|sP2_prd(sK3_skl(X0),X0)|~sQ7_spl)),
% 15.16/2.41 inference(component_clause,[status(thm)],[f116])).
% 15.16/2.41 fof(f119,definition,(
% 15.16/2.41 sQ8_spl <=> (program(sK4_skl))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f120,plain,(
% 15.16/2.41 program(sK4_skl)|~sQ8_spl),
% 15.16/2.41 inference(component_clause,[status(thm)],[f119])).
% 15.16/2.41 fof(f122,plain,(
% 15.16/2.41 sQ7_spl|sQ8_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f27,f116,f119])).
% 15.16/2.41 fof(f123,definition,(
% 15.16/2.41 ![X1]: (sQ9_spl <=> (~program(X1)|~halts2(X1,X1)|halts2(sK4_skl,X1)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f124,plain,(
% 15.16/2.41 ![X0]: (~program(X0)|~halts2(X0,X0)|halts2(sK4_skl,X0)|~sQ9_spl)),
% 15.16/2.41 inference(component_clause,[status(thm)],[f123])).
% 15.16/2.41 fof(f126,plain,(
% 15.16/2.41 sQ7_spl|sQ9_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f28,f116,f123])).
% 15.16/2.41 fof(f127,definition,(
% 15.16/2.41 ![X1]: (sQ10_spl <=> (~program(X1)|~halts2(X1,X1)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f128,plain,(
% 15.16/2.41 ![X0]: (~program(X0)|~halts2(X0,X0)|~sQ10_spl)),
% 15.16/2.41 inference(component_clause,[status(thm)],[f127])).
% 15.16/2.41 fof(f130,definition,(
% 15.16/2.41 sQ11_spl <=> (outputs(sK4_skl,good))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f131,plain,(
% 15.16/2.41 outputs(sK4_skl,good)|~sQ11_spl),
% 15.16/2.41 inference(component_clause,[status(thm)],[f130])).
% 15.16/2.41 fof(f133,plain,(
% 15.16/2.41 sQ7_spl|sQ10_spl|sQ11_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f29,f116,f127,f130])).
% 15.16/2.41 fof(f134,definition,(
% 15.16/2.41 ![X1]: (sQ12_spl <=> (~program(X1)|halts2(X1,X1)|halts2(sK4_skl,X1)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f135,plain,(
% 15.16/2.41 ![X0]: (~program(X0)|halts2(X0,X0)|halts2(sK4_skl,X0)|~sQ12_spl)),
% 15.16/2.41 inference(component_clause,[status(thm)],[f134])).
% 15.16/2.41 fof(f137,plain,(
% 15.16/2.41 sQ7_spl|sQ12_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f30,f116,f134])).
% 15.16/2.41 fof(f138,definition,(
% 15.16/2.41 ![X1]: (sQ13_spl <=> (~program(X1)|halts2(X1,X1)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f139,plain,(
% 15.16/2.41 ![X0]: (~program(X0)|halts2(X0,X0)|~sQ13_spl)),
% 15.16/2.41 inference(component_clause,[status(thm)],[f138])).
% 15.16/2.41 fof(f141,definition,(
% 15.16/2.41 sQ14_spl <=> (outputs(sK4_skl,bad))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f142,plain,(
% 15.16/2.41 outputs(sK4_skl,bad)|~sQ14_spl),
% 15.16/2.41 inference(component_clause,[status(thm)],[f141])).
% 15.16/2.41 fof(f143,plain,(
% 15.16/2.41 ~outputs(sK4_skl,bad)|sQ14_spl),
% 15.16/2.41 inference(component_clause,[status(thm)],[f141])).
% 15.16/2.41 fof(f144,plain,(
% 15.16/2.41 sQ7_spl|sQ13_spl|sQ14_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f31,f116,f138,f141])).
% 15.16/2.41 fof(f145,definition,(
% 15.16/2.41 ![X0]: (sQ15_spl <=> (~program(X0)|sP3_prd(sK5_skl(X0),X0)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f146,plain,(
% 15.16/2.41 ![X0]: (~program(X0)|sP3_prd(sK5_skl(X0),X0)|~sQ15_spl)),
% 15.16/2.41 inference(component_clause,[status(thm)],[f145])).
% 15.16/2.41 fof(f148,definition,(
% 15.16/2.41 sQ16_spl <=> (program(sK6_skl))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f149,plain,(
% 15.16/2.41 program(sK6_skl)|~sQ16_spl),
% 15.16/2.41 inference(component_clause,[status(thm)],[f148])).
% 15.16/2.41 fof(f151,plain,(
% 15.16/2.41 sQ15_spl|sQ16_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f37,f145,f148])).
% 15.16/2.41 fof(f152,definition,(
% 15.16/2.41 ![X1]: (sQ17_spl <=> (~program(X1)|~halts2(X1,X1)|~halts2(sK6_skl,X1)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f153,plain,(
% 15.16/2.41 ![X0]: (~program(X0)|~halts2(X0,X0)|~halts2(sK6_skl,X0)|~sQ17_spl)),
% 15.16/2.41 inference(component_clause,[status(thm)],[f152])).
% 15.16/2.41 fof(f155,plain,(
% 15.16/2.41 sQ15_spl|sQ17_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f38,f145,f152])).
% 15.16/2.41 fof(f156,definition,(
% 15.16/2.41 ![X1]: (sQ18_spl <=> (~program(X1)|halts2(X1,X1)|halts2(sK6_skl,X1)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f157,plain,(
% 15.16/2.41 ![X0]: (~program(X0)|halts2(X0,X0)|halts2(sK6_skl,X0)|~sQ18_spl)),
% 15.16/2.41 inference(component_clause,[status(thm)],[f156])).
% 15.16/2.41 fof(f159,plain,(
% 15.16/2.41 sQ15_spl|sQ18_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f39,f145,f156])).
% 15.16/2.41 fof(f164,plain,(
% 15.16/2.41 ![X0,X1,X2]: (~program(X0)|sP1_prd(sK2_skl(X0),X0)|~program(X1)|halts3(X0,X1,X2))),
% 15.16/2.41 inference(forward_subsumption_resolution,[status(thm)],[f20,f18])).
% 15.16/2.41 fof(f165,plain,(
% 15.16/2.41 ![X0,X1]: (~sP2_prd(X0,X1)|program(X0))),
% 15.16/2.41 inference(backward_subsumption_resolution,[status(thm)],[f61,f79])).
% 15.16/2.41 fof(f166,plain,(
% 15.16/2.41 ![X0,X1]: (~sP3_prd(X0,X1)|program(X0))),
% 15.16/2.41 inference(backward_subsumption_resolution,[status(thm)],[f71,f86])).
% 15.16/2.41 fof(f167,plain,(
% 15.16/2.41 sP0_prd(sK0_skl(sK7_skl),sK7_skl)|~sQ0_spl),
% 15.16/2.41 inference(resolution,[status(thm)],[f92,f43])).
% 15.16/2.41 fof(f168,plain,(
% 15.16/2.41 ~decides(sK7_skl,sK0_skl(sK7_skl),sK8_skl(sK0_skl(sK7_skl),sK7_skl))|~sQ0_spl),
% 15.16/2.41 inference(resolution,[status(thm)],[f167,f49])).
% 15.16/2.41 fof(f169,plain,(
% 15.16/2.41 program(sK0_skl(sK7_skl))|~sQ0_spl),
% 15.16/2.41 inference(resolution,[status(thm)],[f167,f48])).
% 15.16/2.41 fof(f175,plain,(
% 15.16/2.41 ![X0]: (decides(sK7_skl,sK0_skl(sK7_skl),X0)|~sQ0_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f169,f44])).
% 15.16/2.41 fof(f176,plain,(
% 15.16/2.41 $false|~sQ0_spl),
% 15.16/2.41 inference(backward_subsumption_resolution,[status(thm)],[f168,f175])).
% 15.16/2.41 fof(f177,plain,(
% 15.16/2.41 ~sQ0_spl),
% 15.16/2.41 inference(contradiction_clause,[status(thm)],[f176])).
% 15.16/2.41 fof(f179,plain,(
% 15.16/2.41 sP3_prd(sK5_skl(sK1_skl),sK1_skl)|~sQ1_spl|~sQ15_spl),
% 15.16/2.41 inference(resolution,[status(thm)],[f95,f146])).
% 15.16/2.41 fof(f180,plain,(
% 15.16/2.41 sP2_prd(sK3_skl(sK1_skl),sK1_skl)|~sQ1_spl|~sQ7_spl),
% 15.16/2.41 inference(resolution,[status(thm)],[f95,f117])).
% 15.16/2.41 fof(f181,plain,(
% 15.16/2.41 ![X0,X1]: (~program(X0)|sP1_prd(sK2_skl(X0),X0)|halts3(X0,sK1_skl,X1)|~sQ1_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f95,f164])).
% 15.16/2.41 fof(f184,plain,(
% 15.16/2.41 program(sK5_skl(sK1_skl))|~sQ1_spl|~sQ15_spl),
% 15.16/2.41 inference(resolution,[status(thm)],[f179,f166])).
% 15.16/2.41 fof(f191,plain,(
% 15.16/2.41 program(sK3_skl(sK1_skl))|~sQ1_spl|~sQ7_spl),
% 15.16/2.41 inference(resolution,[status(thm)],[f180,f165])).
% 15.16/2.41 fof(f198,plain,(
% 15.16/2.41 sP4_prd(sK3_skl(sK1_skl),sK1_skl)|~halts2(sK3_skl(sK1_skl),sK3_skl(sK1_skl))|~sQ1_spl|~sQ7_spl),
% 15.16/2.41 inference(resolution,[status(thm)],[f62,f180])).
% 15.16/2.41 fof(f199,definition,(
% 15.16/2.41 sQ20_spl <=> (sP4_prd(sK3_skl(sK1_skl),sK1_skl))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f200,plain,(
% 15.16/2.41 sP4_prd(sK3_skl(sK1_skl),sK1_skl)|~sQ20_spl),
% 15.16/2.41 inference(component_clause,[status(thm)],[f199])).
% 15.16/2.41 fof(f202,definition,(
% 15.16/2.41 sQ21_spl <=> (halts2(sK3_skl(sK1_skl),sK3_skl(sK1_skl)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f204,plain,(
% 15.16/2.41 ~halts2(sK3_skl(sK1_skl),sK3_skl(sK1_skl))|sQ21_spl),
% 15.16/2.41 inference(component_clause,[status(thm)],[f202])).
% 15.16/2.41 fof(f205,plain,(
% 15.16/2.41 sQ20_spl|~sQ21_spl|~sQ1_spl|~sQ7_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f198,f199,f202,f94,f116])).
% 15.16/2.41 fof(f208,plain,(
% 15.16/2.41 sP5_prd(sK5_skl(sK1_skl),sK1_skl)|~halts2(sK5_skl(sK1_skl),sK5_skl(sK1_skl))|~sQ1_spl|~sQ15_spl),
% 15.16/2.41 inference(resolution,[status(thm)],[f72,f179])).
% 15.16/2.41 fof(f209,definition,(
% 15.16/2.41 sQ22_spl <=> (sP5_prd(sK5_skl(sK1_skl),sK1_skl))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f210,plain,(
% 15.16/2.41 sP5_prd(sK5_skl(sK1_skl),sK1_skl)|~sQ22_spl),
% 15.16/2.41 inference(component_clause,[status(thm)],[f209])).
% 15.16/2.41 fof(f212,definition,(
% 15.16/2.41 sQ23_spl <=> (halts2(sK5_skl(sK1_skl),sK5_skl(sK1_skl)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f214,plain,(
% 15.16/2.41 ~halts2(sK5_skl(sK1_skl),sK5_skl(sK1_skl))|sQ23_spl),
% 15.16/2.41 inference(component_clause,[status(thm)],[f212])).
% 15.16/2.41 fof(f215,plain,(
% 15.16/2.41 sQ22_spl|~sQ23_spl|~sQ1_spl|~sQ15_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f208,f209,f212,f94,f145])).
% 15.16/2.41 fof(f218,plain,(
% 15.16/2.41 ![X0]: (sP2_prd(sK3_skl(sK1_skl),X0)|halts2(sK3_skl(sK1_skl),sK3_skl(sK1_skl))|outputs(X0,bad)|~sQ1_spl|~sQ7_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f66,f191])).
% 15.16/2.41 fof(f219,plain,(
% 15.16/2.41 ![X0]: (sP2_prd(sK5_skl(sK1_skl),X0)|halts2(sK5_skl(sK1_skl),sK5_skl(sK1_skl))|outputs(X0,bad)|~sQ1_spl|~sQ15_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f66,f184])).
% 15.16/2.41 fof(f220,plain,(
% 15.16/2.41 ![X0]: (sP2_prd(sK1_skl,X0)|halts2(sK1_skl,sK1_skl)|outputs(X0,bad)|~sQ1_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f66,f95])).
% 15.16/2.41 fof(f221,definition,(
% 15.16/2.41 ![X0]: (sQ24_spl <=> (sP2_prd(sK3_skl(sK1_skl),X0)|outputs(X0,bad)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f224,plain,(
% 15.16/2.41 sQ24_spl|sQ21_spl|~sQ1_spl|~sQ7_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f218,f221,f202,f94,f116])).
% 15.16/2.41 fof(f225,definition,(
% 15.16/2.41 ![X0]: (sQ25_spl <=> (sP2_prd(sK5_skl(sK1_skl),X0)|outputs(X0,bad)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f226,plain,(
% 15.16/2.41 ![X0]: (sP2_prd(sK5_skl(sK1_skl),X0)|outputs(X0,bad)|~sQ25_spl)),
% 15.16/2.41 inference(component_clause,[status(thm)],[f225])).
% 15.16/2.41 fof(f228,plain,(
% 15.16/2.41 sQ25_spl|sQ23_spl|~sQ1_spl|~sQ15_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f219,f225,f212,f94,f145])).
% 15.16/2.41 fof(f229,definition,(
% 15.16/2.41 ![X0]: (sQ26_spl <=> (sP2_prd(sK1_skl,X0)|outputs(X0,bad)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f230,plain,(
% 15.16/2.41 ![X0]: (sP2_prd(sK1_skl,X0)|outputs(X0,bad)|~sQ26_spl)),
% 15.16/2.41 inference(component_clause,[status(thm)],[f229])).
% 15.16/2.41 fof(f232,definition,(
% 15.16/2.41 sQ27_spl <=> (halts2(sK1_skl,sK1_skl))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f233,plain,(
% 15.16/2.41 halts2(sK1_skl,sK1_skl)|~sQ27_spl),
% 15.16/2.41 inference(component_clause,[status(thm)],[f232])).
% 15.16/2.41 fof(f234,plain,(
% 15.16/2.41 ~halts2(sK1_skl,sK1_skl)|sQ27_spl),
% 15.16/2.41 inference(component_clause,[status(thm)],[f232])).
% 15.16/2.41 fof(f235,plain,(
% 15.16/2.41 sQ26_spl|sQ27_spl|~sQ1_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f220,f229,f232,f94])).
% 15.16/2.41 fof(f236,plain,(
% 15.16/2.41 ![X0]: (outputs(X0,bad)|sP4_prd(sK1_skl,X0)|~halts2(sK1_skl,sK1_skl)|~sQ26_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f230,f62])).
% 15.16/2.41 fof(f238,definition,(
% 15.16/2.41 ![X0]: (sQ28_spl <=> (outputs(X0,bad)|sP4_prd(sK1_skl,X0)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f241,plain,(
% 15.16/2.41 sQ28_spl|~sQ27_spl|~sQ26_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f236,f238,f232,f229])).
% 15.16/2.41 fof(f242,definition,(
% 15.16/2.41 ![X0]: (sQ29_spl <=> (outputs(X0,bad)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f243,plain,(
% 15.16/2.41 ![X0]: (outputs(X0,bad)|~sQ29_spl)),
% 15.16/2.41 inference(component_clause,[status(thm)],[f242])).
% 15.16/2.41 fof(f251,definition,(
% 15.16/2.41 sQ30_spl <=> (sP5_prd(sK5_skl(sK5_skl(sK1_skl)),sK5_skl(sK1_skl)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f252,plain,(
% 15.16/2.41 sP5_prd(sK5_skl(sK5_skl(sK1_skl)),sK5_skl(sK1_skl))|~sQ30_spl),
% 15.16/2.41 inference(component_clause,[status(thm)],[f251])).
% 15.16/2.41 fof(f269,plain,(
% 15.16/2.41 ![X0,X1]: (~sP2_prd(X0,X1)|sP4_prd(X0,X1)|~halts3(X1,X0,X0)|~sQ29_spl)),
% 15.16/2.41 inference(backward_subsumption_resolution,[status(thm)],[f63,f243])).
% 15.16/2.41 fof(f270,plain,(
% 15.16/2.41 ![X0,X1]: (~sP3_prd(X0,X1)|sP5_prd(X0,X1)|~halts2(X1,X0)|~sQ29_spl)),
% 15.16/2.41 inference(backward_subsumption_resolution,[status(thm)],[f73,f243])).
% 15.16/2.41 fof(f273,plain,(
% 15.16/2.41 ![X0,X1]: (sP4_prd(X0,X1)|~program(X0)|outputs(X1,good)|~sQ13_spl)),
% 15.16/2.41 inference(backward_subsumption_resolution,[status(thm)],[f83,f139])).
% 15.16/2.41 fof(f275,plain,(
% 15.16/2.41 ![X0]: (~program(X0)|~halts2(sK6_skl,X0)|~sQ13_spl|~sQ17_spl)),
% 15.16/2.41 inference(forward_subsumption_resolution,[status(thm)],[f153,f139])).
% 15.16/2.41 fof(f286,plain,(
% 15.16/2.41 ~program(sK6_skl)|~program(sK6_skl)|~sQ17_spl|~sQ13_spl),
% 15.16/2.41 inference(resolution,[status(thm)],[f275,f139])).
% 15.16/2.41 fof(f289,plain,(
% 15.16/2.41 ~sQ16_spl|~sQ17_spl|~sQ13_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f286,f148,f152,f138])).
% 15.16/2.41 fof(f307,plain,(
% 15.16/2.41 ![X0]: (~program(X0)|~sQ13_spl|~sQ10_spl)),
% 15.16/2.41 inference(forward_subsumption_resolution,[status(thm)],[f128,f139])).
% 15.16/2.41 fof(f308,plain,(
% 15.16/2.41 $false|~sQ13_spl|~sQ10_spl|~sQ8_spl),
% 15.16/2.41 inference(forward_subsumption_resolution,[status(thm)],[f120,f307])).
% 15.16/2.41 fof(f309,plain,(
% 15.16/2.41 ~sQ13_spl|~sQ10_spl|~sQ8_spl),
% 15.16/2.41 inference(contradiction_clause,[status(thm)],[f308])).
% 15.16/2.41 fof(f310,plain,(
% 15.16/2.41 ![X0]: (~program(X0)|~sQ6_spl|~sQ4_spl)),
% 15.16/2.41 inference(forward_subsumption_resolution,[status(thm)],[f106,f113])).
% 15.16/2.41 fof(f311,plain,(
% 15.16/2.41 $false|~sQ6_spl|~sQ4_spl|~sQ1_spl|~sQ15_spl),
% 15.16/2.41 inference(forward_subsumption_resolution,[status(thm)],[f184,f310])).
% 15.16/2.41 fof(f312,plain,(
% 15.16/2.41 ~sQ6_spl|~sQ4_spl|~sQ1_spl|~sQ15_spl),
% 15.16/2.41 inference(contradiction_clause,[status(thm)],[f311])).
% 15.16/2.41 fof(f313,plain,(
% 15.16/2.41 ![X0]: (~program(X0)|halts2(sK4_skl,X0)|~sQ9_spl|~sQ12_spl)),
% 15.16/2.41 inference(forward_subsumption_resolution,[status(thm)],[f135,f124])).
% 15.16/2.41 fof(f321,plain,(
% 15.16/2.41 ![X0,X1]: (~program(X0)|~sP5_prd(X0,X1)|~sQ4_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f106,f87])).
% 15.16/2.41 fof(f322,plain,(
% 15.16/2.41 ![X0,X1]: (~program(X0)|~sP4_prd(X0,X1)|~sQ4_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f106,f80])).
% 15.16/2.41 fof(f323,plain,(
% 15.16/2.41 ![X0,X1]: (~sP3_prd(X0,X1)|~halts2(X0,X0)|~sQ4_spl)),
% 15.16/2.41 inference(backward_subsumption_resolution,[status(thm)],[f72,f327])).
% 15.16/2.41 fof(f324,plain,(
% 15.16/2.41 $false|~sQ4_spl|~sQ22_spl),
% 15.16/2.41 inference(backward_subsumption_resolution,[status(thm)],[f210,f327])).
% 15.16/2.41 fof(f327,plain,(
% 15.16/2.41 ![X0,X1]: (~sP5_prd(X0,X1)|~sQ4_spl)),
% 15.16/2.41 inference(forward_subsumption_resolution,[status(thm)],[f321,f86])).
% 15.16/2.41 fof(f329,plain,(
% 15.16/2.41 $false|~sQ4_spl|~sQ20_spl),
% 15.16/2.41 inference(backward_subsumption_resolution,[status(thm)],[f200,f331])).
% 15.16/2.41 fof(f331,plain,(
% 15.16/2.41 ![X0,X1]: (~sP4_prd(X0,X1)|~sQ4_spl)),
% 15.16/2.41 inference(forward_subsumption_resolution,[status(thm)],[f322,f79])).
% 15.16/2.41 fof(f332,plain,(
% 15.16/2.41 ~sQ4_spl|~sQ22_spl),
% 15.16/2.41 inference(contradiction_clause,[status(thm)],[f324])).
% 15.16/2.41 fof(f339,plain,(
% 15.16/2.41 ![X0,X1]: (~program(X0)|sP1_prd(sK2_skl(X0),X0)|halts3(X0,sK4_skl,X1)|~sQ8_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f164,f120])).
% 15.16/2.41 fof(f341,plain,(
% 15.16/2.41 ![X0]: (~program(X0)|program(sK3_skl(X0))|~sQ7_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f117,f165])).
% 15.16/2.41 fof(f350,plain,(
% 15.16/2.41 ![X0]: (~program(X0)|program(sK5_skl(X0))|~sQ15_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f146,f166])).
% 15.16/2.41 fof(f351,plain,(
% 15.16/2.41 ![X0,X1,X2]: (~program(X0)|~program(X1)|sP1_prd(sK2_skl(X1),X1)|halts3(X1,sK3_skl(X0),X2)|~sQ7_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f341,f164])).
% 15.16/2.41 fof(f352,plain,(
% 15.16/2.41 ![X0,X1,X2]: (~program(X0)|~program(X1)|sP1_prd(sK2_skl(X1),X1)|halts3(X1,sK5_skl(X0),X2)|~sQ15_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f350,f164])).
% 15.16/2.41 fof(f369,plain,(
% 15.16/2.41 ![X0]: (~sP5_prd(X0,sK4_skl)|~halts2(sK4_skl,X0)|~sQ11_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f88,f131])).
% 15.16/2.41 fof(f373,plain,(
% 15.16/2.41 ![X0]: (~halts2(sK4_skl,X0)|~sP3_prd(X0,sK4_skl)|~halts2(sK4_skl,X0)|~sQ11_spl|~sQ29_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f369,f270])).
% 15.16/2.41 fof(f376,plain,(
% 15.16/2.41 ![X0]: (~halts2(sK4_skl,X0)|~sP3_prd(X0,sK4_skl)|~sQ11_spl|~sQ29_spl)),
% 15.16/2.41 inference(duplicate_literals_removal,[status(thm)],[f373])).
% 15.16/2.41 fof(f377,plain,(
% 15.16/2.41 ~halts2(sK4_skl,sK5_skl(sK4_skl))|~program(sK4_skl)|~sQ11_spl|~sQ29_spl|~sQ15_spl),
% 15.16/2.41 inference(resolution,[status(thm)],[f376,f146])).
% 15.16/2.41 fof(f379,definition,(
% 15.16/2.41 sQ35_spl <=> (halts2(sK4_skl,sK5_skl(sK4_skl)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f381,plain,(
% 15.16/2.41 ~halts2(sK4_skl,sK5_skl(sK4_skl))|sQ35_spl),
% 15.16/2.41 inference(component_clause,[status(thm)],[f379])).
% 15.16/2.41 fof(f382,plain,(
% 15.16/2.41 ~sQ35_spl|~sQ8_spl|~sQ11_spl|~sQ29_spl|~sQ15_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f377,f379,f119,f130,f242,f145])).
% 15.16/2.41 fof(f383,plain,(
% 15.16/2.41 ~program(sK5_skl(sK4_skl))|sQ35_spl|~sQ9_spl|~sQ12_spl),
% 15.16/2.41 inference(resolution,[status(thm)],[f381,f313])).
% 15.16/2.41 fof(f385,plain,(
% 15.16/2.41 ~program(sK4_skl)|sQ35_spl|~sQ9_spl|~sQ12_spl|~sQ15_spl),
% 15.16/2.41 inference(resolution,[status(thm)],[f383,f350])).
% 15.16/2.41 fof(f393,definition,(
% 15.16/2.41 ![X0]: (sQ37_spl <=> (~program(X0)|program(X0)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f396,definition,(
% 15.16/2.41 ![X1]: (sQ38_spl <=> (outputs(X1,good)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f397,plain,(
% 15.16/2.41 ![X0]: (outputs(X0,good)|~sQ38_spl)),
% 15.16/2.41 inference(component_clause,[status(thm)],[f396])).
% 15.16/2.41 fof(f401,plain,(
% 15.16/2.41 ![X0,X1]: (~sP5_prd(X0,X1)|~halts2(X1,X0)|~sQ38_spl)),
% 15.16/2.41 inference(backward_subsumption_resolution,[status(thm)],[f88,f397])).
% 15.16/2.41 fof(f403,plain,(
% 15.16/2.41 ![X0,X1]: (~sP3_prd(X0,X1)|~halts2(X1,X0)|~sQ38_spl|~sQ29_spl)),
% 15.16/2.41 inference(backward_subsumption_resolution,[status(thm)],[f270,f401])).
% 15.16/2.41 fof(f404,plain,(
% 15.16/2.41 ~halts2(sK5_skl(sK1_skl),sK5_skl(sK5_skl(sK1_skl)))|~sQ38_spl|~sQ30_spl),
% 15.16/2.41 inference(resolution,[status(thm)],[f401,f252])).
% 15.16/2.41 fof(f410,plain,(
% 15.16/2.41 ![X0]: (~halts2(X0,sK5_skl(X0))|~program(X0)|~sQ38_spl|~sQ29_spl|~sQ15_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f403,f146])).
% 15.16/2.41 fof(f411,plain,(
% 15.16/2.41 ~program(sK4_skl)|~program(sK5_skl(sK4_skl))|~sQ38_spl|~sQ29_spl|~sQ15_spl|~sQ9_spl|~sQ12_spl),
% 15.16/2.41 inference(resolution,[status(thm)],[f410,f313])).
% 15.16/2.41 fof(f412,definition,(
% 15.16/2.41 sQ39_spl <=> (program(sK5_skl(sK4_skl)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f414,plain,(
% 15.16/2.41 ~program(sK5_skl(sK4_skl))|sQ39_spl),
% 15.16/2.41 inference(component_clause,[status(thm)],[f412])).
% 15.16/2.41 fof(f415,plain,(
% 15.16/2.41 ~sQ8_spl|~sQ39_spl|~sQ38_spl|~sQ29_spl|~sQ15_spl|~sQ9_spl|~sQ12_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f411,f119,f412,f396,f242,f145,f123,f134])).
% 15.16/2.41 fof(f434,plain,(
% 15.16/2.41 ![X0]: (sP1_prd(sK2_skl(sK1_skl),sK1_skl)|halts3(sK1_skl,sK1_skl,X0)|~sQ1_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f181,f95])).
% 15.16/2.41 fof(f477,definition,(
% 15.16/2.41 sQ52_spl <=> (sP1_prd(sK2_skl(sK1_skl),sK1_skl))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f478,plain,(
% 15.16/2.41 sP1_prd(sK2_skl(sK1_skl),sK1_skl)|~sQ52_spl),
% 15.16/2.41 inference(component_clause,[status(thm)],[f477])).
% 15.16/2.41 fof(f479,plain,(
% 15.16/2.41 ~sP1_prd(sK2_skl(sK1_skl),sK1_skl)|sQ52_spl),
% 15.16/2.41 inference(component_clause,[status(thm)],[f477])).
% 15.16/2.41 fof(f480,definition,(
% 15.16/2.41 ![X0]: (sQ53_spl <=> (halts3(sK1_skl,sK1_skl,X0)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f483,plain,(
% 15.16/2.41 sQ52_spl|sQ53_spl|~sQ1_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f434,f477,f480,f94])).
% 15.16/2.41 fof(f493,plain,(
% 15.16/2.41 program(sK2_skl(sK1_skl))|~sQ52_spl),
% 15.16/2.41 inference(resolution,[status(thm)],[f478,f54])).
% 15.16/2.41 fof(f494,plain,(
% 15.16/2.41 ~decides(sK1_skl,sK2_skl(sK1_skl),sK9_skl(sK2_skl(sK1_skl),sK1_skl))|~sQ52_spl),
% 15.16/2.41 inference(resolution,[status(thm)],[f478,f55])).
% 15.16/2.41 fof(f497,definition,(
% 15.16/2.41 sQ56_spl <=> (sP1_prd(sK2_skl(sK2_skl(sK1_skl)),sK2_skl(sK1_skl)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f498,plain,(
% 15.16/2.41 sP1_prd(sK2_skl(sK2_skl(sK1_skl)),sK2_skl(sK1_skl))|~sQ56_spl),
% 15.16/2.41 inference(component_clause,[status(thm)],[f497])).
% 15.16/2.41 fof(f499,plain,(
% 15.16/2.41 ~sP1_prd(sK2_skl(sK2_skl(sK1_skl)),sK2_skl(sK1_skl))|sQ56_spl),
% 15.16/2.41 inference(component_clause,[status(thm)],[f497])).
% 15.16/2.41 fof(f506,definition,(
% 15.16/2.41 sQ58_spl <=> (halts2(sK6_skl,sK6_skl))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f507,plain,(
% 15.16/2.41 halts2(sK6_skl,sK6_skl)|~sQ58_spl),
% 15.16/2.41 inference(component_clause,[status(thm)],[f506])).
% 15.16/2.41 fof(f511,plain,(
% 15.16/2.41 ![X0,X1,X2]: (~sP2_prd(X0,X1)|sP4_prd(X0,X1)|~sP4_prd(X0,X2))),
% 15.16/2.41 inference(resolution,[status(thm)],[f62,f80])).
% 15.16/2.41 fof(f512,plain,(
% 15.16/2.41 ![X0,X1,X2]: (~sP2_prd(X0,X1)|sP4_prd(X0,X1)|~sP5_prd(X0,X2))),
% 15.16/2.41 inference(resolution,[status(thm)],[f62,f87])).
% 15.16/2.41 fof(f520,plain,(
% 15.16/2.41 ![X0,X1,X2]: (sP5_prd(X0,X1)|~program(X0)|halts2(X1,X0)|~sP4_prd(X0,X2))),
% 15.16/2.41 inference(resolution,[status(thm)],[f89,f80])).
% 15.16/2.41 fof(f521,plain,(
% 15.16/2.41 ![X0,X1,X2]: (sP5_prd(X0,X1)|~program(X0)|halts2(X1,X0)|~sP5_prd(X0,X2))),
% 15.16/2.41 inference(resolution,[status(thm)],[f89,f87])).
% 15.16/2.41 fof(f522,plain,(
% 15.16/2.41 ![X0,X1,X2]: (sP5_prd(X0,X1)|halts2(X1,X0)|~sP4_prd(X0,X2))),
% 15.16/2.41 inference(forward_subsumption_resolution,[status(thm)],[f520,f79])).
% 15.16/2.41 fof(f523,plain,(
% 15.16/2.41 ![X0,X1,X2]: (sP5_prd(X0,X1)|halts2(X1,X0)|~sP5_prd(X0,X2))),
% 15.16/2.41 inference(forward_subsumption_resolution,[status(thm)],[f521,f86])).
% 15.16/2.41 fof(f530,definition,(
% 15.16/2.41 sQ60_spl <=> (sP3_prd(sK5_skl(sK1_skl),sK1_skl))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f532,plain,(
% 15.16/2.41 ~sP3_prd(sK5_skl(sK1_skl),sK1_skl)|sQ60_spl),
% 15.16/2.41 inference(component_clause,[status(thm)],[f530])).
% 15.16/2.41 fof(f534,plain,(
% 15.16/2.41 $false|sQ60_spl|~sQ1_spl|~sQ15_spl),
% 15.16/2.41 inference(forward_subsumption_resolution,[status(thm)],[f179,f532])).
% 15.16/2.41 fof(f535,plain,(
% 15.16/2.41 sQ60_spl|~sQ1_spl|~sQ15_spl),
% 15.16/2.41 inference(contradiction_clause,[status(thm)],[f534])).
% 15.16/2.41 fof(f550,plain,(
% 15.16/2.41 halts2(sK6_skl,sK6_skl)|halts2(sK6_skl,sK6_skl)|~sQ18_spl|~sQ16_spl),
% 15.16/2.41 inference(resolution,[status(thm)],[f157,f149])).
% 15.16/2.41 fof(f554,plain,(
% 15.16/2.41 halts2(sK1_skl,sK1_skl)|halts2(sK6_skl,sK1_skl)|~sQ18_spl|~sQ1_spl),
% 15.16/2.41 inference(resolution,[status(thm)],[f157,f95])).
% 15.16/2.41 fof(f555,plain,(
% 15.16/2.41 sQ58_spl|~sQ18_spl|~sQ16_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f550,f506,f156,f148])).
% 15.16/2.41 fof(f567,definition,(
% 15.16/2.41 sQ66_spl <=> (halts2(sK6_skl,sK1_skl))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f570,plain,(
% 15.16/2.41 sQ27_spl|sQ66_spl|~sQ18_spl|~sQ1_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f554,f232,f567,f156,f94])).
% 15.16/2.41 fof(f574,plain,(
% 15.16/2.41 ![X0]: (~sP4_prd(sK1_skl,X0)|sQ27_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f234,f80])).
% 15.16/2.41 fof(f575,plain,(
% 15.16/2.41 ![X0]: (~sP5_prd(sK1_skl,X0)|sQ27_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f234,f87])).
% 15.16/2.41 fof(f596,plain,(
% 15.16/2.41 ![X0]: (sP3_prd(sK3_skl(sK1_skl),X0)|halts2(sK3_skl(sK1_skl),sK3_skl(sK1_skl))|halts2(X0,sK3_skl(sK1_skl))|~sQ1_spl|~sQ7_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f75,f191])).
% 15.16/2.41 fof(f598,plain,(
% 15.16/2.41 ![X0]: (sP3_prd(sK1_skl,X0)|halts2(sK1_skl,sK1_skl)|halts2(X0,sK1_skl)|~sQ1_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f75,f95])).
% 15.16/2.41 fof(f618,definition,(
% 15.16/2.41 ![X0]: (sQ73_spl <=> (sP3_prd(sK3_skl(sK1_skl),X0)|halts2(X0,sK3_skl(sK1_skl))))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f619,plain,(
% 15.16/2.41 ![X0]: (sP3_prd(sK3_skl(sK1_skl),X0)|halts2(X0,sK3_skl(sK1_skl))|~sQ73_spl)),
% 15.16/2.41 inference(component_clause,[status(thm)],[f618])).
% 15.16/2.41 fof(f621,plain,(
% 15.16/2.41 sQ73_spl|sQ21_spl|~sQ1_spl|~sQ7_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f596,f618,f202,f94,f116])).
% 15.16/2.41 fof(f622,definition,(
% 15.16/2.41 ![X0]: (sQ74_spl <=> (sP3_prd(sK1_skl,X0)|halts2(X0,sK1_skl)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f625,plain,(
% 15.16/2.41 sQ74_spl|sQ27_spl|~sQ1_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f598,f622,f232,f94])).
% 15.16/2.41 fof(f674,definition,(
% 15.16/2.41 ![X0]: (sQ79_spl <=> (sP5_prd(sK1_skl,X0)|halts2(X0,sK1_skl)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f675,plain,(
% 15.16/2.41 ![X0]: (sP5_prd(sK1_skl,X0)|halts2(X0,sK1_skl)|~sQ79_spl)),
% 15.16/2.41 inference(component_clause,[status(thm)],[f674])).
% 15.16/2.41 fof(f678,plain,(
% 15.16/2.41 ![X0]: (halts2(X0,sK1_skl)|sQ27_spl|~sQ79_spl)),
% 15.16/2.41 inference(backward_subsumption_resolution,[status(thm)],[f675,f575])).
% 15.16/2.41 fof(f683,plain,(
% 15.16/2.41 $false|~sQ79_spl|sQ27_spl),
% 15.16/2.41 inference(backward_subsumption_resolution,[status(thm)],[f234,f678])).
% 15.16/2.41 fof(f684,plain,(
% 15.16/2.41 ~sQ79_spl|sQ27_spl),
% 15.16/2.41 inference(contradiction_clause,[status(thm)],[f683])).
% 15.16/2.41 fof(f706,plain,(
% 15.16/2.41 ![X0]: (~sP4_prd(sK3_skl(sK1_skl),X0)|sQ21_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f204,f80])).
% 15.16/2.41 fof(f707,plain,(
% 15.16/2.41 ![X0]: (~sP5_prd(sK3_skl(sK1_skl),X0)|sQ21_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f204,f87])).
% 15.16/2.41 fof(f708,plain,(
% 15.16/2.41 $false|sQ21_spl|~sQ20_spl),
% 15.16/2.41 inference(backward_subsumption_resolution,[status(thm)],[f200,f706])).
% 15.16/2.41 fof(f709,plain,(
% 15.16/2.41 sQ21_spl|~sQ20_spl),
% 15.16/2.41 inference(contradiction_clause,[status(thm)],[f708])).
% 15.16/2.41 fof(f711,definition,(
% 15.16/2.41 ![X0]: (sQ82_spl <=> (~sP3_prd(sK3_skl(sK1_skl),X0)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f712,plain,(
% 15.16/2.41 ![X0]: (~sP3_prd(sK3_skl(sK1_skl),X0)|~sQ82_spl)),
% 15.16/2.41 inference(component_clause,[status(thm)],[f711])).
% 15.16/2.41 fof(f717,definition,(
% 15.16/2.41 ![X0]: (sQ83_spl <=> (halts2(X0,sK1_skl)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f718,plain,(
% 15.16/2.41 ![X0]: (halts2(X0,sK1_skl)|~sQ83_spl)),
% 15.16/2.41 inference(component_clause,[status(thm)],[f717])).
% 15.16/2.41 fof(f747,plain,(
% 15.16/2.41 ~program(sK6_skl)|~halts2(sK6_skl,sK6_skl)|~sQ58_spl|~sQ17_spl),
% 15.16/2.41 inference(resolution,[status(thm)],[f507,f153])).
% 15.16/2.41 fof(f749,plain,(
% 15.16/2.41 ~sQ16_spl|~sQ58_spl|~sQ17_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f747,f148,f506,f152])).
% 15.16/2.41 fof(f776,plain,(
% 15.16/2.41 ~program(sK4_skl)|~sQ15_spl|sQ39_spl),
% 15.16/2.41 inference(resolution,[status(thm)],[f350,f414])).
% 15.16/2.41 fof(f825,plain,(
% 15.16/2.41 ![X0]: (sP5_prd(sK1_skl,X0)|~program(sK1_skl)|outputs(X0,good)|~sQ27_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f90,f233])).
% 15.16/2.41 fof(f828,definition,(
% 15.16/2.41 ![X0]: (sQ90_spl <=> (sP5_prd(sK1_skl,X0)|outputs(X0,good)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f829,plain,(
% 15.16/2.41 ![X0]: (sP5_prd(sK1_skl,X0)|outputs(X0,good)|~sQ90_spl)),
% 15.16/2.41 inference(component_clause,[status(thm)],[f828])).
% 15.16/2.41 fof(f831,plain,(
% 15.16/2.41 sQ90_spl|~sQ1_spl|~sQ27_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f825,f828,f94,f232])).
% 15.16/2.41 fof(f893,plain,(
% 15.16/2.41 program(sK2_skl(sK2_skl(sK1_skl)))|~sQ56_spl),
% 15.16/2.41 inference(resolution,[status(thm)],[f498,f54])).
% 15.16/2.41 fof(f895,plain,(
% 15.16/2.41 ![X0]: (sP3_prd(sK2_skl(sK2_skl(sK1_skl)),X0)|halts2(sK2_skl(sK2_skl(sK1_skl)),sK2_skl(sK2_skl(sK1_skl)))|halts2(X0,sK2_skl(sK2_skl(sK1_skl)))|~sQ56_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f893,f75])).
% 15.16/2.41 fof(f896,plain,(
% 15.16/2.41 ![X0]: (sP1_prd(sK2_skl(sK2_skl(sK2_skl(sK1_skl))),sK2_skl(sK2_skl(sK1_skl)))|halts3(sK2_skl(sK2_skl(sK1_skl)),sK1_skl,X0)|~sQ56_spl|~sQ1_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f893,f181])).
% 15.16/2.41 fof(f898,definition,(
% 15.16/2.41 ![X0]: (sQ99_spl <=> (sP3_prd(sK2_skl(sK2_skl(sK1_skl)),X0)|halts2(X0,sK2_skl(sK2_skl(sK1_skl)))))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f901,definition,(
% 15.16/2.41 sQ100_spl <=> (halts2(sK2_skl(sK2_skl(sK1_skl)),sK2_skl(sK2_skl(sK1_skl))))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f904,plain,(
% 15.16/2.41 sQ99_spl|sQ100_spl|~sQ56_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f895,f898,f901,f497])).
% 15.16/2.41 fof(f905,definition,(
% 15.16/2.41 sQ101_spl <=> (sP1_prd(sK2_skl(sK2_skl(sK2_skl(sK1_skl))),sK2_skl(sK2_skl(sK1_skl))))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f908,definition,(
% 15.16/2.41 ![X0]: (sQ102_spl <=> (halts3(sK2_skl(sK2_skl(sK1_skl)),sK1_skl,X0)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f911,plain,(
% 15.16/2.41 sQ101_spl|sQ102_spl|~sQ56_spl|~sQ1_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f896,f905,f908,f497,f94])).
% 15.16/2.41 fof(f913,plain,(
% 15.16/2.41 ![X0,X1,X2]: (sP5_prd(X0,X1)|halts2(X1,X0)|~sP3_prd(X0,X2)|~halts2(X0,X0))),
% 15.16/2.41 inference(resolution,[status(thm)],[f523,f72])).
% 15.16/2.41 fof(f970,plain,(
% 15.16/2.41 ![X0,X1]: (~program(X0)|sP1_prd(sK2_skl(sK1_skl),sK1_skl)|halts3(sK1_skl,sK3_skl(X0),X1)|~sQ7_spl|~sQ1_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f351,f95])).
% 15.16/2.41 fof(f999,definition,(
% 15.16/2.41 ![X0,X1]: (sQ118_spl <=> (~program(X0)|halts3(sK1_skl,sK3_skl(X0),X1)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f1000,plain,(
% 15.16/2.41 ![X0,X1]: (~program(X0)|halts3(sK1_skl,sK3_skl(X0),X1)|~sQ118_spl)),
% 15.16/2.41 inference(component_clause,[status(thm)],[f999])).
% 15.16/2.41 fof(f1002,plain,(
% 15.16/2.41 sQ118_spl|sQ52_spl|~sQ7_spl|~sQ1_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f970,f999,f477,f116,f94])).
% 15.16/2.41 fof(f1070,definition,(
% 15.16/2.41 sQ133_spl <=> (halts2(sK2_skl(sK1_skl),sK2_skl(sK1_skl)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f1071,plain,(
% 15.16/2.41 halts2(sK2_skl(sK1_skl),sK2_skl(sK1_skl))|~sQ133_spl),
% 15.16/2.41 inference(component_clause,[status(thm)],[f1070])).
% 15.16/2.41 fof(f1072,plain,(
% 15.16/2.41 ~halts2(sK2_skl(sK1_skl),sK2_skl(sK1_skl))|sQ133_spl),
% 15.16/2.41 inference(component_clause,[status(thm)],[f1070])).
% 15.16/2.41 fof(f1077,plain,(
% 15.16/2.41 ![X0]: (sP5_prd(sK2_skl(sK1_skl),X0)|~program(sK2_skl(sK1_skl))|halts2(X0,sK2_skl(sK1_skl))|~sQ133_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f1071,f89])).
% 15.16/2.41 fof(f1079,definition,(
% 15.16/2.41 ![X0]: (sQ134_spl <=> (sP5_prd(sK2_skl(sK1_skl),X0)|halts2(X0,sK2_skl(sK1_skl))))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f1082,definition,(
% 15.16/2.41 sQ135_spl <=> (program(sK2_skl(sK1_skl)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f1084,plain,(
% 15.16/2.41 ~program(sK2_skl(sK1_skl))|sQ135_spl),
% 15.16/2.41 inference(component_clause,[status(thm)],[f1082])).
% 15.16/2.41 fof(f1085,plain,(
% 15.16/2.41 sQ134_spl|~sQ135_spl|~sQ133_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f1077,f1079,f1082,f1070])).
% 15.16/2.41 fof(f1086,plain,(
% 15.16/2.41 $false|~sQ52_spl|sQ135_spl),
% 15.16/2.41 inference(forward_subsumption_resolution,[status(thm)],[f1084,f493])).
% 15.16/2.41 fof(f1087,plain,(
% 15.16/2.41 ~sQ52_spl|sQ135_spl),
% 15.16/2.41 inference(contradiction_clause,[status(thm)],[f1086])).
% 15.16/2.41 fof(f1097,plain,(
% 15.16/2.41 ![X0,X1]: (outputs(X0,good)|sP5_prd(sK1_skl,X1)|halts2(X1,sK1_skl)|~sQ90_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f829,f523])).
% 15.16/2.41 fof(f1101,plain,(
% 15.16/2.41 sQ38_spl|sQ79_spl|~sQ90_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f1097,f396,f674,f828])).
% 15.16/2.41 fof(f1102,definition,(
% 15.16/2.41 ![X1]: (sQ136_spl <=> (~sP2_prd(sK1_skl,X1)|sP4_prd(sK1_skl,X1)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f1103,plain,(
% 15.16/2.41 ![X0]: (~sP2_prd(sK1_skl,X0)|sP4_prd(sK1_skl,X0)|~sQ136_spl)),
% 15.16/2.41 inference(component_clause,[status(thm)],[f1102])).
% 15.16/2.41 fof(f1123,plain,(
% 15.16/2.41 ![X0,X1]: (halts2(X0,sK1_skl)|~sP2_prd(sK1_skl,X1)|sP4_prd(sK1_skl,X1)|~sQ79_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f675,f512])).
% 15.16/2.41 fof(f1127,plain,(
% 15.16/2.41 sQ83_spl|sQ136_spl|~sQ79_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f1123,f717,f1102,f674])).
% 15.16/2.41 fof(f1188,plain,(
% 15.16/2.41 ![X0]: (sP5_prd(sK1_skl,X0)|~program(sK1_skl)|halts2(X0,sK1_skl)|~sQ83_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f718,f89])).
% 15.16/2.41 fof(f1190,plain,(
% 15.16/2.41 sQ79_spl|~sQ1_spl|~sQ83_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f1188,f674,f94,f717])).
% 15.16/2.41 fof(f1207,definition,(
% 15.16/2.41 sQ149_spl <=> (program(sK3_skl(sK1_skl)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ149_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f1209,plain,(
% 15.16/2.41 ~program(sK3_skl(sK1_skl))|sQ149_spl),
% 15.16/2.41 inference(component_clause,[status(thm)],[f1207])).
% 15.16/2.41 fof(f1215,plain,(
% 15.16/2.41 $false|~sQ1_spl|~sQ7_spl|sQ149_spl),
% 15.16/2.41 inference(forward_subsumption_resolution,[status(thm)],[f1209,f191])).
% 15.16/2.41 fof(f1216,plain,(
% 15.16/2.41 ~sQ1_spl|~sQ7_spl|sQ149_spl),
% 15.16/2.41 inference(contradiction_clause,[status(thm)],[f1215])).
% 15.16/2.41 fof(f1217,plain,(
% 15.16/2.41 ~sQ8_spl|~sQ15_spl|sQ39_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f776,f119,f145,f412])).
% 15.16/2.41 fof(f1219,plain,(
% 15.16/2.41 ~sQ8_spl|sQ35_spl|~sQ9_spl|~sQ12_spl|~sQ15_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f385,f119,f379,f123,f134,f145])).
% 15.16/2.41 fof(f1284,definition,(
% 15.16/2.41 sQ151_spl <=> (program(sK5_skl(sK1_skl)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f1286,plain,(
% 15.16/2.41 ~program(sK5_skl(sK1_skl))|sQ151_spl),
% 15.16/2.41 inference(component_clause,[status(thm)],[f1284])).
% 15.16/2.41 fof(f1288,plain,(
% 15.16/2.41 $false|~sQ1_spl|~sQ15_spl|sQ151_spl),
% 15.16/2.41 inference(forward_subsumption_resolution,[status(thm)],[f1286,f184])).
% 15.16/2.41 fof(f1289,plain,(
% 15.16/2.41 ~sQ1_spl|~sQ15_spl|sQ151_spl),
% 15.16/2.41 inference(contradiction_clause,[status(thm)],[f1288])).
% 15.16/2.41 fof(f1323,plain,(
% 15.16/2.41 ![X0]: (sP4_prd(sK1_skl,X0)|~program(sK1_skl)|outputs(X0,good)|~sQ27_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f83,f233])).
% 15.16/2.41 fof(f1326,definition,(
% 15.16/2.41 ![X0]: (sQ152_spl <=> (sP4_prd(sK1_skl,X0)|outputs(X0,good)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ152_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f1327,plain,(
% 15.16/2.41 ![X0]: (sP4_prd(sK1_skl,X0)|outputs(X0,good)|~sQ152_spl)),
% 15.16/2.41 inference(component_clause,[status(thm)],[f1326])).
% 15.16/2.41 fof(f1329,plain,(
% 15.16/2.41 sQ152_spl|~sQ1_spl|~sQ27_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f1323,f1326,f94,f232])).
% 15.16/2.41 fof(f1332,plain,(
% 15.16/2.41 ![X0]: (~sP2_prd(sK1_skl,X0)|sQ27_spl|~sQ136_spl)),
% 15.16/2.41 inference(backward_subsumption_resolution,[status(thm)],[f1103,f574])).
% 15.16/2.41 fof(f1340,plain,(
% 15.16/2.41 ![X0,X1]: (~sP4_prd(X0,X1)|~halts3(X1,X0,X0)|~sQ38_spl)),
% 15.16/2.41 inference(backward_subsumption_resolution,[status(thm)],[f81,f397])).
% 15.16/2.41 fof(f1499,plain,(
% 15.16/2.41 ![X0]: (sP2_prd(sK2_skl(sK2_skl(sK1_skl)),X0)|halts2(sK2_skl(sK2_skl(sK1_skl)),sK2_skl(sK2_skl(sK1_skl)))|outputs(X0,bad)|~sQ56_spl)),
% 15.16/2.41 inference(resolution,[status(thm)],[f66,f893])).
% 15.16/2.41 fof(f1520,definition,(
% 15.16/2.41 ![X0]: (sQ158_spl <=> (sP2_prd(sK2_skl(sK2_skl(sK1_skl)),X0)|outputs(X0,bad)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition])).
% 15.16/2.41 fof(f1523,plain,(
% 15.16/2.41 sQ158_spl|sQ100_spl|~sQ56_spl),
% 15.16/2.41 inference(split_clause,[status(thm)],[f1499,f1520,f901,f497])).
% 15.16/2.41 fof(f1536,definition,(
% 15.16/2.41 ![X0]: (sQ162_spl <=> (sP2_prd(sK2_skl(sK1_skl),X0)|outputs(X0,bad)))),
% 15.16/2.41 introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition])).
% 15.16/2.42 fof(f1537,plain,(
% 15.16/2.42 ![X0]: (sP2_prd(sK2_skl(sK1_skl),X0)|outputs(X0,bad)|~sQ162_spl)),
% 15.16/2.42 inference(component_clause,[status(thm)],[f1536])).
% 15.16/2.42 fof(f1558,plain,(
% 15.16/2.42 ![X0]: (sP3_prd(sK3_skl(sK1_skl),X0)|halts2(sK3_skl(sK1_skl),sK3_skl(sK1_skl))|outputs(X0,bad)|~sQ1_spl|~sQ7_spl)),
% 15.16/2.42 inference(resolution,[status(thm)],[f76,f191])).
% 15.16/2.42 fof(f1560,plain,(
% 15.16/2.42 ![X0]: (sP3_prd(sK2_skl(sK2_skl(sK1_skl)),X0)|halts2(sK2_skl(sK2_skl(sK1_skl)),sK2_skl(sK2_skl(sK1_skl)))|outputs(X0,bad)|~sQ56_spl)),
% 15.16/2.42 inference(resolution,[status(thm)],[f76,f893])).
% 15.16/2.42 fof(f1567,plain,(
% 15.16/2.42 ![X0]: (sP3_prd(sK5_skl(sK1_skl),X0)|halts2(sK5_skl(sK1_skl),sK5_skl(sK1_skl))|outputs(X0,bad)|~sQ1_spl|~sQ15_spl)),
% 15.16/2.42 inference(resolution,[status(thm)],[f76,f184])).
% 15.16/2.42 fof(f1569,plain,(
% 15.16/2.42 ![X0]: (sP3_prd(sK1_skl,X0)|halts2(sK1_skl,sK1_skl)|outputs(X0,bad)|~sQ1_spl)),
% 15.16/2.42 inference(resolution,[status(thm)],[f76,f95])).
% 15.16/2.42 fof(f1586,definition,(
% 15.16/2.42 ![X0]: (sQ168_spl <=> (sP3_prd(sK3_skl(sK1_skl),X0)|outputs(X0,bad)))),
% 15.16/2.42 introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition])).
% 15.16/2.42 fof(f1589,plain,(
% 15.16/2.42 sQ168_spl|sQ21_spl|~sQ1_spl|~sQ7_spl),
% 15.16/2.42 inference(split_clause,[status(thm)],[f1558,f1586,f202,f94,f116])).
% 15.16/2.42 fof(f1590,definition,(
% 15.16/2.42 ![X0]: (sQ169_spl <=> (sP3_prd(sK2_skl(sK2_skl(sK1_skl)),X0)|outputs(X0,bad)))),
% 15.16/2.42 introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition])).
% 15.16/2.42 fof(f1593,plain,(
% 15.16/2.42 sQ169_spl|sQ100_spl|~sQ56_spl),
% 15.16/2.42 inference(split_clause,[status(thm)],[f1560,f1590,f901,f497])).
% 15.16/2.42 fof(f1606,definition,(
% 15.16/2.42 ![X0]: (sQ173_spl <=> (sP3_prd(sK2_skl(sK1_skl),X0)|outputs(X0,bad)))),
% 15.16/2.42 introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition])).
% 15.16/2.42 fof(f1607,plain,(
% 15.16/2.42 ![X0]: (sP3_prd(sK2_skl(sK1_skl),X0)|outputs(X0,bad)|~sQ173_spl)),
% 15.16/2.42 inference(component_clause,[status(thm)],[f1606])).
% 15.16/2.42 fof(f1618,definition,(
% 15.16/2.42 ![X0]: (sQ176_spl <=> (sP3_prd(sK5_skl(sK1_skl),X0)|outputs(X0,bad)))),
% 15.16/2.42 introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition])).
% 15.16/2.42 fof(f1619,plain,(
% 15.16/2.42 ![X0]: (sP3_prd(sK5_skl(sK1_skl),X0)|outputs(X0,bad)|~sQ176_spl)),
% 15.16/2.42 inference(component_clause,[status(thm)],[f1618])).
% 15.16/2.42 fof(f1621,plain,(
% 15.16/2.42 sQ176_spl|sQ23_spl|~sQ1_spl|~sQ15_spl),
% 15.16/2.42 inference(split_clause,[status(thm)],[f1567,f1618,f212,f94,f145])).
% 15.16/2.42 fof(f1622,definition,(
% 15.16/2.42 ![X0]: (sQ177_spl <=> (sP3_prd(sK1_skl,X0)|outputs(X0,bad)))),
% 15.16/2.42 introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition])).
% 15.16/2.42 fof(f1625,plain,(
% 15.16/2.42 sQ177_spl|sQ27_spl|~sQ1_spl),
% 15.16/2.42 inference(split_clause,[status(thm)],[f1569,f1622,f232,f94])).
% 15.16/2.42 fof(f1796,plain,(
% 15.16/2.42 ![X0]: (~program(X0)|outputs(X0,bad)|~decides(X0,sK2_skl(X0),sK9_skl(sK2_skl(X0),X0))|~sQ5_spl)),
% 15.16/2.42 inference(resolution,[status(thm)],[f110,f55])).
% 15.16/2.42 fof(f1797,plain,(
% 15.16/2.42 ![X0]: (~program(X0)|outputs(X0,bad)|program(sK2_skl(X0))|~sQ5_spl)),
% 15.16/2.42 inference(resolution,[status(thm)],[f110,f54])).
% 15.16/2.42 fof(f1802,plain,(
% 15.16/2.42 ![X0]: (outputs(X0,bad)|program(sK5_skl(sK1_skl))|~sQ176_spl)),
% 15.16/2.42 inference(resolution,[status(thm)],[f1619,f166])).
% 15.16/2.42 fof(f1803,plain,(
% 15.16/2.42 sQ29_spl|sQ151_spl|~sQ176_spl),
% 15.16/2.42 inference(split_clause,[status(thm)],[f1802,f242,f1284,f1618])).
% 15.16/2.42 fof(f1812,definition,(
% 15.16/2.42 sQ183_spl <=> (halts3(sK4_skl,sK3_skl(sK4_skl),sK3_skl(sK4_skl)))),
% 15.16/2.42 introduced(definition,[new_symbols(definition,[sQ183_spl])],[split_symbol_definition])).
% 15.16/2.42 fof(f1813,plain,(
% 15.16/2.42 halts3(sK4_skl,sK3_skl(sK4_skl),sK3_skl(sK4_skl))|~sQ183_spl),
% 15.16/2.42 inference(component_clause,[status(thm)],[f1812])).
% 15.16/2.42 fof(f1961,definition,(
% 15.16/2.42 sQ190_spl <=> (halts3(sK1_skl,sK3_skl(sK1_skl),sK3_skl(sK1_skl)))),
% 15.16/2.42 introduced(definition,[new_symbols(definition,[sQ190_spl])],[split_symbol_definition])).
% 15.16/2.42 fof(f1963,plain,(
% 15.16/2.42 ~halts3(sK1_skl,sK3_skl(sK1_skl),sK3_skl(sK1_skl))|sQ190_spl),
% 15.16/2.42 inference(component_clause,[status(thm)],[f1961])).
% 15.16/2.42 fof(f1973,plain,(
% 15.16/2.42 sP4_prd(sK3_skl(sK1_skl),sK1_skl)|~halts3(sK1_skl,sK3_skl(sK1_skl),sK3_skl(sK1_skl))|~sQ1_spl|~sQ7_spl|~sQ29_spl),
% 15.16/2.42 inference(resolution,[status(thm)],[f180,f269])).
% 15.16/2.42 fof(f1975,plain,(
% 15.16/2.42 sQ20_spl|~sQ190_spl|~sQ1_spl|~sQ7_spl|~sQ29_spl),
% 15.16/2.42 inference(split_clause,[status(thm)],[f1973,f199,f1961,f94,f116,f242])).
% 15.16/2.42 fof(f2000,plain,(
% 15.16/2.42 ![X0,X1]: (outputs(X0,good)|sP5_prd(sK1_skl,X1)|halts2(X1,sK1_skl)|~sQ152_spl)),
% 15.16/2.42 inference(resolution,[status(thm)],[f1327,f522])).
% 15.16/2.42 fof(f2001,plain,(
% 15.16/2.42 ![X0,X1]: (outputs(X0,good)|~sP2_prd(sK1_skl,X1)|sP4_prd(sK1_skl,X1)|~sQ152_spl)),
% 15.16/2.42 inference(resolution,[status(thm)],[f1327,f511])).
% 15.16/2.42 fof(f2005,plain,(
% 15.16/2.42 sQ38_spl|sQ79_spl|~sQ152_spl),
% 15.16/2.42 inference(split_clause,[status(thm)],[f2000,f396,f674,f1326])).
% 15.16/2.42 fof(f2006,plain,(
% 15.16/2.42 sQ38_spl|sQ136_spl|~sQ152_spl),
% 15.16/2.42 inference(split_clause,[status(thm)],[f2001,f396,f1102,f1326])).
% 15.16/2.42 fof(f2028,definition,(
% 15.16/2.42 sQ191_spl <=> (sP4_prd(sK3_skl(sK4_skl),sK4_skl))),
% 15.16/2.42 introduced(definition,[new_symbols(definition,[sQ191_spl])],[split_symbol_definition])).
% 15.16/2.42 fof(f2029,plain,(
% 15.16/2.42 sP4_prd(sK3_skl(sK4_skl),sK4_skl)|~sQ191_spl),
% 15.16/2.42 inference(component_clause,[status(thm)],[f2028])).
% 15.16/2.42 fof(f2031,definition,(
% 15.16/2.42 sQ192_spl <=> (program(sK3_skl(sK4_skl)))),
% 15.16/2.42 introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition])).
% 15.16/2.42 fof(f2033,plain,(
% 15.16/2.42 ~program(sK3_skl(sK4_skl))|sQ192_spl),
% 15.16/2.42 inference(component_clause,[status(thm)],[f2031])).
% 15.16/2.42 fof(f2034,definition,(
% 15.16/2.42 sQ193_spl <=> (halts2(sK3_skl(sK4_skl),sK3_skl(sK4_skl)))),
% 15.16/2.42 introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition])).
% 15.16/2.42 fof(f2035,plain,(
% 15.16/2.42 halts2(sK3_skl(sK4_skl),sK3_skl(sK4_skl))|~sQ193_spl),
% 15.16/2.42 inference(component_clause,[status(thm)],[f2034])).
% 15.16/2.42 fof(f2036,plain,(
% 15.16/2.42 ~halts2(sK3_skl(sK4_skl),sK3_skl(sK4_skl))|sQ193_spl),
% 15.16/2.42 inference(component_clause,[status(thm)],[f2034])).
% 15.16/2.42 fof(f2038,definition,(
% 15.16/2.42 sQ194_spl <=> (sP2_prd(sK3_skl(sK4_skl),sK4_skl))),
% 15.16/2.42 introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition])).
% 15.16/2.42 fof(f2039,plain,(
% 15.16/2.42 sP2_prd(sK3_skl(sK4_skl),sK4_skl)|~sQ194_spl),
% 15.16/2.42 inference(component_clause,[status(thm)],[f2038])).
% 15.16/2.42 fof(f2044,plain,(
% 15.16/2.42 program(sK3_skl(sK4_skl))|~sQ194_spl),
% 15.16/2.42 inference(resolution,[status(thm)],[f2039,f165])).
% 15.16/2.42 fof(f2045,plain,(
% 15.16/2.42 $false|sQ192_spl|~sQ194_spl),
% 15.16/2.42 inference(forward_subsumption_resolution,[status(thm)],[f2044,f2033])).
% 15.16/2.42 fof(f2046,plain,(
% 15.16/2.42 sQ192_spl|~sQ194_spl),
% 15.16/2.42 inference(contradiction_clause,[status(thm)],[f2045])).
% 15.16/2.42 fof(f2050,definition,(
% 15.16/2.42 ![X0]: (sQ195_spl <=> (sP3_prd(sK3_skl(sK4_skl),X0)|halts2(X0,sK3_skl(sK4_skl))))),
% 15.16/2.42 introduced(definition,[new_symbols(definition,[sQ195_spl])],[split_symbol_definition])).
% 15.16/2.42 fof(f2051,plain,(
% 15.16/2.42 ![X0]: (sP3_prd(sK3_skl(sK4_skl),X0)|halts2(X0,sK3_skl(sK4_skl))|~sQ195_spl)),
% 15.16/2.42 inference(component_clause,[status(thm)],[f2050])).
% 15.16/2.42 fof(f2054,plain,(
% 15.16/2.42 ~halts3(sK4_skl,sK3_skl(sK4_skl),sK3_skl(sK4_skl))|~sQ191_spl|~sQ38_spl),
% 15.16/2.42 inference(resolution,[status(thm)],[f2029,f1340])).
% 15.16/2.42 fof(f2104,definition,(
% 15.16/2.42 sQ198_spl <=> (halts2(sK5_skl(sK1_skl),sK5_skl(sK5_skl(sK1_skl))))),
% 15.16/2.42 introduced(definition,[new_symbols(definition,[sQ198_spl])],[split_symbol_definition])).
% 15.16/2.42 fof(f2106,plain,(
% 15.16/2.42 ~halts2(sK5_skl(sK1_skl),sK5_skl(sK5_skl(sK1_skl)))|sQ198_spl),
% 15.16/2.42 inference(component_clause,[status(thm)],[f2104])).
% 15.16/2.42 fof(f2108,definition,(
% 15.16/2.42 sQ199_spl <=> (sP5_prd(sK5_skl(sK3_skl(sK1_skl)),sK3_skl(sK1_skl)))),
% 15.16/2.42 introduced(definition,[new_symbols(definition,[sQ199_spl])],[split_symbol_definition])).
% 15.16/2.42 fof(f2109,plain,(
% 15.16/2.42 sP5_prd(sK5_skl(sK3_skl(sK1_skl)),sK3_skl(sK1_skl))|~sQ199_spl),
% 15.16/2.42 inference(component_clause,[status(thm)],[f2108])).
% 15.16/2.42 fof(f2115,definition,(
% 15.16/2.42 sQ201_spl <=> (halts2(sK1_skl,sK5_skl(sK1_skl)))),
% 15.16/2.42 introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition])).
% 15.16/2.42 fof(f2117,plain,(
% 15.16/2.42 ~halts2(sK1_skl,sK5_skl(sK1_skl))|sQ201_spl),
% 15.16/2.42 inference(component_clause,[status(thm)],[f2115])).
% 15.16/2.42 fof(f2161,plain,(
% 15.16/2.42 ~program(sK5_skl(sK1_skl))|~sQ13_spl|sQ23_spl),
% 15.16/2.42 inference(resolution,[status(thm)],[f139,f214])).
% 15.16/2.42 fof(f2162,plain,(
% 15.16/2.42 ~program(sK2_skl(sK1_skl))|~sQ13_spl|sQ133_spl),
% 15.16/2.42 inference(resolution,[status(thm)],[f139,f1072])).
% 15.16/2.42 fof(f2164,plain,(
% 15.16/2.42 ![X0,X1]: (~program(X0)|~sP3_prd(X0,X1)|sP5_prd(X0,X1)|~sQ13_spl)),
% 15.16/2.42 inference(resolution,[status(thm)],[f139,f72])).
% 15.16/2.42 fof(f2165,plain,(
% 15.16/2.42 ~sQ151_spl|~sQ13_spl|sQ23_spl),
% 15.16/2.42 inference(split_clause,[status(thm)],[f2161,f1284,f138,f212])).
% 15.16/2.42 fof(f2166,plain,(
% 15.16/2.42 ~sQ135_spl|~sQ13_spl|sQ133_spl),
% 15.16/2.42 inference(split_clause,[status(thm)],[f2162,f1082,f138,f1070])).
% 15.16/2.42 fof(f2168,plain,(
% 15.16/2.42 ![X0,X1]: (~sP3_prd(X0,X1)|sP5_prd(X0,X1)|~sQ13_spl)),
% 15.16/2.42 inference(forward_subsumption_resolution,[status(thm)],[f2164,f166])).
% 15.16/2.42 fof(f2231,definition,(
% 15.16/2.42 ![X0]: (sQ208_spl <=> (sP5_prd(sK3_skl(sK4_skl),X0)|halts2(X0,sK3_skl(sK4_skl))))),
% 15.16/2.42 introduced(definition,[new_symbols(definition,[sQ208_spl])],[split_symbol_definition])).
% 15.16/2.42 fof(f2236,plain,(
% 15.16/2.42 $false|~sQ191_spl|~sQ38_spl|~sQ183_spl),
% 15.16/2.42 inference(forward_subsumption_resolution,[status(thm)],[f1813,f2054])).
% 15.16/2.42 fof(f2237,plain,(
% 15.16/2.42 ~sQ191_spl|~sQ38_spl|~sQ183_spl),
% 15.16/2.42 inference(contradiction_clause,[status(thm)],[f2236])).
% 15.16/2.42 fof(f2281,definition,(
% 15.16/2.42 ![X0]: (sQ210_spl <=> (sP3_prd(sK3_skl(sK4_skl),X0)|outputs(X0,bad)))),
% 15.16/2.42 introduced(definition,[new_symbols(definition,[sQ210_spl])],[split_symbol_definition])).
% 15.16/2.42 fof(f2282,plain,(
% 15.16/2.42 ![X0]: (sP3_prd(sK3_skl(sK4_skl),X0)|outputs(X0,bad)|~sQ210_spl)),
% 15.16/2.42 inference(component_clause,[status(thm)],[f2281])).
% 15.16/2.42 fof(f2316,definition,(
% 15.16/2.42 ![X0]: (sQ211_spl <=> (sP2_prd(sK3_skl(sK4_skl),X0)|outputs(X0,bad)))),
% 15.16/2.42 introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition])).
% 15.16/2.42 fof(f2317,plain,(
% 15.16/2.42 ![X0]: (sP2_prd(sK3_skl(sK4_skl),X0)|outputs(X0,bad)|~sQ211_spl)),
% 15.16/2.42 inference(component_clause,[status(thm)],[f2316])).
% 15.16/2.42 fof(f2334,plain,(
% 15.16/2.42 halts2(sK3_skl(sK4_skl),sK3_skl(sK4_skl))|~sQ191_spl),
% 15.16/2.42 inference(resolution,[status(thm)],[f2029,f80])).
% 15.16/2.42 fof(f2463,plain,(
% 15.16/2.42 ![X0]: (outputs(X0,bad)|program(sK2_skl(sK1_skl))|~sQ173_spl)),
% 15.16/2.42 inference(resolution,[status(thm)],[f1607,f166])).
% 15.16/2.42 fof(f2464,plain,(
% 15.16/2.42 sQ29_spl|sQ135_spl|~sQ173_spl),
% 15.16/2.42 inference(split_clause,[status(thm)],[f2463,f242,f1082,f1606])).
% 15.16/2.42 fof(f2467,plain,(
% 15.16/2.42 ![X0]: (outputs(X0,bad)|program(sK2_skl(sK1_skl))|~sQ162_spl)),
% 15.16/2.42 inference(resolution,[status(thm)],[f1537,f165])).
% 15.16/2.42 fof(f2468,plain,(
% 15.16/2.42 sQ29_spl|sQ135_spl|~sQ162_spl),
% 15.16/2.42 inference(split_clause,[status(thm)],[f2467,f242,f1082,f1536])).
% 15.16/2.42 fof(f2488,plain,(
% 15.16/2.42 ![X0]: (sP4_prd(sK1_skl,X0)|~program(sK1_skl)|outputs(X0,good)|~sQ83_spl)),
% 15.16/2.42 inference(resolution,[status(thm)],[f83,f718])).
% 15.16/2.42 fof(f2497,plain,(
% 15.16/2.42 sQ152_spl|~sQ1_spl|~sQ83_spl),
% 15.16/2.42 inference(split_clause,[status(thm)],[f2488,f1326,f94,f717])).
% 15.16/2.42 fof(f2867,plain,(
% 15.16/2.42 ~program(sK1_skl)|outputs(sK1_skl,bad)|~program(sK2_skl(sK1_skl))|~sQ5_spl|~sQ2_spl),
% 15.16/2.42 inference(resolution,[status(thm)],[f1796,f99])).
% 15.16/2.42 fof(f2871,definition,(
% 15.16/2.42 sQ258_spl <=> (outputs(sK1_skl,bad))),
% 15.16/2.42 introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition])).
% 15.16/2.42 fof(f2872,plain,(
% 15.16/2.42 outputs(sK1_skl,bad)|~sQ258_spl),
% 15.16/2.42 inference(component_clause,[status(thm)],[f2871])).
% 15.16/2.42 fof(f2874,plain,(
% 15.16/2.42 ~sQ1_spl|sQ258_spl|~sQ135_spl|~sQ5_spl|~sQ2_spl),
% 15.16/2.42 inference(split_clause,[status(thm)],[f2867,f94,f2871,f1082,f109,f98])).
% 15.16/2.42 fof(f3166,plain,(
% 15.16/2.42 ![X0,X1]: (~program(X0)|sP1_prd(sK2_skl(sK1_skl),sK1_skl)|halts3(sK1_skl,sK5_skl(X0),X1)|~sQ15_spl|~sQ1_spl)),
% 15.16/2.42 inference(resolution,[status(thm)],[f352,f95])).
% 15.16/2.42 fof(f3231,definition,(
% 15.16/2.42 ![X0,X1]: (sQ335_spl <=> (~program(X0)|halts3(sK1_skl,sK5_skl(X0),X1)))),
% 15.16/2.42 introduced(definition,[new_symbols(definition,[sQ335_spl])],[split_symbol_definition])).
% 15.16/2.42 fof(f3234,plain,(
% 15.16/2.42 sQ335_spl|sQ52_spl|~sQ15_spl|~sQ1_spl),
% 15.16/2.42 inference(split_clause,[status(thm)],[f3166,f3231,f477,f145,f94])).
% 15.16/2.42 fof(f3690,plain,(
% 15.16/2.42 ![X0]: (outputs(X0,bad)|program(sK5_skl(sK1_skl))|~sQ25_spl)),
% 15.16/2.42 inference(resolution,[status(thm)],[f226,f165])).
% 15.16/2.42 fof(f3695,plain,(
% 15.16/2.42 sQ29_spl|sQ151_spl|~sQ25_spl),
% 15.16/2.42 inference(split_clause,[status(thm)],[f3690,f242,f1284,f225])).
% 15.16/2.42 fof(f3806,plain,(
% 15.16/2.42 ![X0]: (outputs(X0,bad)|program(sK3_skl(sK4_skl))|~sQ210_spl)),
% 15.16/2.42 inference(resolution,[status(thm)],[f2282,f166])).
% 15.16/2.42 fof(f3811,plain,(
% 15.16/2.42 sQ29_spl|sQ192_spl|~sQ210_spl),
% 15.16/2.42 inference(split_clause,[status(thm)],[f3806,f242,f2031,f2281])).
% 15.16/2.42 fof(f3813,plain,(
% 15.16/2.42 ![X0]: (outputs(X0,bad)|program(sK3_skl(sK4_skl))|~sQ211_spl)),
% 15.16/2.42 inference(resolution,[status(thm)],[f2317,f165])).
% 15.16/2.42 fof(f3818,plain,(
% 15.16/2.42 sQ29_spl|sQ192_spl|~sQ211_spl),
% 15.16/2.42 inference(split_clause,[status(thm)],[f3813,f242,f2031,f2316])).
% 15.16/2.42 fof(f4082,plain,(
% 15.16/2.42 ![X0,X1]: (sP5_prd(sK3_skl(sK4_skl),X0)|halts2(X0,sK3_skl(sK4_skl))|~sP3_prd(sK3_skl(sK4_skl),X1)|~sQ191_spl)),
% 15.16/2.42 inference(resolution,[status(thm)],[f2334,f913])).
% 15.16/2.42 fof(f4083,plain,(
% 15.16/2.42 ![X0]: (sP5_prd(sK3_skl(sK4_skl),X0)|~program(sK3_skl(sK4_skl))|halts2(X0,sK3_skl(sK4_skl))|~sQ191_spl)),
% 15.16/2.42 inference(resolution,[status(thm)],[f2334,f89])).
% 15.16/2.42 fof(f4086,definition,(
% 15.16/2.42 ![X1]: (sQ449_spl <=> (~sP3_prd(sK3_skl(sK4_skl),X1)))),
% 15.16/2.42 introduced(definition,[new_symbols(definition,[sQ449_spl])],[split_symbol_definition])).
% 15.16/2.42 fof(f4087,plain,(
% 15.16/2.42 ![X0]: (~sP3_prd(sK3_skl(sK4_skl),X0)|~sQ449_spl)),
% 15.16/2.42 inference(component_clause,[status(thm)],[f4086])).
% 15.16/2.42 fof(f4089,plain,(
% 15.16/2.42 sQ208_spl|sQ449_spl|~sQ191_spl),
% 15.16/2.42 inference(split_clause,[status(thm)],[f4082,f2231,f4086,f2028])).
% 15.16/2.42 fof(f4090,plain,(
% 15.16/2.42 sQ208_spl|~sQ192_spl|~sQ191_spl),
% 15.16/2.42 inference(split_clause,[status(thm)],[f4083,f2231,f2031,f2028])).
% 10.67/2.42 fof(f4091,plain,(
% 10.67/2.42 ![X0]: (outputs(X0,bad)|~sQ449_spl|~sQ210_spl)),
% 10.67/2.42 inference(backward_subsumption_resolution,[status(thm)],[f2282,f4087])).
% 10.67/2.42 fof(f4092,plain,(
% 10.67/2.42 ![X0]: (halts2(X0,sK3_skl(sK4_skl))|~sQ449_spl|~sQ195_spl)),
% 10.67/2.42 inference(backward_subsumption_resolution,[status(thm)],[f2051,f4087])).
% 10.67/2.42 fof(f4093,plain,(
% 10.67/2.42 sQ29_spl|~sQ449_spl|~sQ210_spl),
% 10.67/2.42 inference(split_clause,[status(thm)],[f4091,f242,f4086,f2281])).
% 10.67/2.42 fof(f4094,plain,(
% 10.67/2.42 $false|~sQ449_spl|~sQ195_spl|sQ193_spl),
% 10.67/2.42 inference(backward_subsumption_resolution,[status(thm)],[f2036,f4092])).
% 10.67/2.42 fof(f4095,plain,(
% 10.67/2.42 ~sQ449_spl|~sQ195_spl|sQ193_spl),
% 10.67/2.42 inference(contradiction_clause,[status(thm)],[f4094])).
% 10.67/2.42 fof(f4278,definition,(
% 10.67/2.42 ![X0]: (sQ451_spl <=> (sP5_prd(sK3_skl(sK1_skl),X0)|halts2(X0,sK3_skl(sK1_skl))))),
% 10.67/2.42 introduced(definition,[new_symbols(definition,[sQ451_spl])],[split_symbol_definition])).
% 10.67/2.42 fof(f4279,plain,(
% 10.67/2.42 ![X0]: (sP5_prd(sK3_skl(sK1_skl),X0)|halts2(X0,sK3_skl(sK1_skl))|~sQ451_spl)),
% 10.67/2.42 inference(component_clause,[status(thm)],[f4278])).
% 10.67/2.42 fof(f4283,plain,(
% 10.67/2.42 ![X0]: (halts2(X0,sK3_skl(sK1_skl))|~sQ82_spl|~sQ73_spl)),
% 10.67/2.42 inference(backward_subsumption_resolution,[status(thm)],[f619,f712])).
% 10.67/2.42 fof(f4287,plain,(
% 10.67/2.42 ![X0]: (sP5_prd(sK3_skl(sK1_skl),X0)|~program(sK3_skl(sK1_skl))|halts2(X0,sK3_skl(sK1_skl))|~sQ82_spl|~sQ73_spl)),
% 10.67/2.42 inference(resolution,[status(thm)],[f4283,f89])).
% 10.67/2.42 fof(f4291,plain,(
% 10.67/2.42 sQ451_spl|~sQ149_spl|~sQ82_spl|~sQ73_spl),
% 10.67/2.42 inference(split_clause,[status(thm)],[f4287,f4278,f1207,f711,f618])).
% 10.67/2.42 fof(f4799,definition,(
% 10.67/2.42 sQ537_spl <=> (sP3_prd(sK1_skl,sK1_skl))),
% 10.67/2.42 introduced(definition,[new_symbols(definition,[sQ537_spl])],[split_symbol_definition])).
% 10.67/2.42 fof(f4913,plain,(
% 10.67/2.42 ![X0,X1]: (sP3_prd(X0,X1)|~program(X0)|outputs(X1,bad)|~sQ4_spl)),
% 10.67/2.42 inference(backward_subsumption_resolution,[status(thm)],[f76,f106])).
% 10.67/2.42 fof(f4919,plain,(
% 10.67/2.42 $false|~sQ4_spl|~sQ199_spl),
% 10.67/2.42 inference(backward_subsumption_resolution,[status(thm)],[f2109,f327])).
% 10.67/2.42 fof(f4940,plain,(
% 10.67/2.42 ~sQ4_spl|~sQ20_spl),
% 10.67/2.42 inference(contradiction_clause,[status(thm)],[f329])).
% 10.67/2.42 fof(f4946,plain,(
% 10.67/2.42 ~program(sK1_skl)|~sQ6_spl|sQ201_spl),
% 10.67/2.42 inference(resolution,[status(thm)],[f113,f2117])).
% 10.67/2.42 fof(f4948,plain,(
% 10.67/2.42 ~program(sK5_skl(sK1_skl))|~sQ6_spl|sQ198_spl),
% 10.67/2.42 inference(resolution,[status(thm)],[f113,f2106])).
% 10.67/2.42 fof(f4949,plain,(
% 10.67/2.42 ~program(sK5_skl(sK1_skl))|~sQ6_spl|sQ23_spl),
% 10.67/2.42 inference(resolution,[status(thm)],[f113,f214])).
% 10.67/2.42 fof(f4953,plain,(
% 10.67/2.42 $false|~sQ1_spl|~sQ6_spl|sQ201_spl),
% 10.67/2.42 inference(forward_subsumption_resolution,[status(thm)],[f4946,f95])).
% 10.67/2.42 fof(f4954,plain,(
% 10.67/2.42 ~sQ1_spl|~sQ6_spl|sQ201_spl),
% 10.67/2.42 inference(contradiction_clause,[status(thm)],[f4953])).
% 10.67/2.42 fof(f4986,plain,(
% 10.67/2.42 ![X0]: (~sP2_prd(X0,sK1_skl)|sP4_prd(X0,sK1_skl)|~halts3(sK1_skl,X0,X0)|~sQ258_spl)),
% 10.67/2.42 inference(resolution,[status(thm)],[f63,f2872])).
% 10.67/2.42 fof(f4996,definition,(
% 10.67/2.42 sQ542_spl <=> (outputs(sK1_skl,good))),
% 10.67/2.42 introduced(definition,[new_symbols(definition,[sQ542_spl])],[split_symbol_definition])).
% 10.67/2.42 fof(f4997,plain,(
% 10.67/2.42 outputs(sK1_skl,good)|~sQ542_spl),
% 10.67/2.42 inference(component_clause,[status(thm)],[f4996])).
% 10.67/2.42 fof(f5001,plain,(
% 10.67/2.42 ![X0]: (~sP5_prd(X0,sK1_skl)|~halts2(sK1_skl,X0)|~sQ542_spl)),
% 10.67/2.42 inference(resolution,[status(thm)],[f4997,f88])).
% 10.67/2.42 fof(f5002,plain,(
% 10.67/2.42 ![X0]: (~sP4_prd(X0,sK1_skl)|~halts3(sK1_skl,X0,X0)|~sQ542_spl)),
% 10.67/2.42 inference(resolution,[status(thm)],[f4997,f81])).
% 10.67/2.42 fof(f5003,plain,(
% 10.67/2.42 ![X0]: (~sP2_prd(X0,sK1_skl)|~halts3(sK1_skl,X0,X0)|~sQ542_spl|~sQ258_spl)),
% 10.67/2.42 inference(backward_subsumption_resolution,[status(thm)],[f4986,f5002])).
% 10.67/2.42 fof(f5009,plain,(
% 10.67/2.42 ![X0]: (~sP3_prd(X0,sK1_skl)|sP5_prd(X0,sK1_skl)|~halts2(sK1_skl,X0)|~sQ258_spl)),
% 10.67/2.42 inference(resolution,[status(thm)],[f73,f2872])).
% 10.67/2.42 fof(f5010,plain,(
% 10.67/2.42 ![X0]: (~sP3_prd(X0,sK1_skl)|~halts2(sK1_skl,X0)|~sQ542_spl|~sQ258_spl)),
% 10.67/2.42 inference(forward_subsumption_resolution,[status(thm)],[f5009,f5001])).
% 10.67/2.42 fof(f5393,definition,(
% 10.67/2.42 sQ546_spl <=> (program(sK2_skl(sK4_skl)))),
% 10.67/2.42 introduced(definition,[new_symbols(definition,[sQ546_spl])],[split_symbol_definition])).
% 10.67/2.42 fof(f5394,plain,(
% 10.67/2.42 program(sK2_skl(sK4_skl))|~sQ546_spl),
% 10.67/2.42 inference(component_clause,[status(thm)],[f5393])).
% 10.67/2.42 fof(f5398,plain,(
% 10.67/2.43 ![X0]: (sP3_prd(sK2_skl(sK4_skl),X0)|halts2(sK2_skl(sK4_skl),sK2_skl(sK4_skl))|halts2(X0,sK2_skl(sK4_skl))|~sQ546_spl)),
% 10.67/2.43 inference(resolution,[status(thm)],[f5394,f75])).
% 10.67/2.43 fof(f5399,plain,(
% 10.67/2.43 ![X0]: (sP2_prd(sK2_skl(sK4_skl),X0)|halts2(sK2_skl(sK4_skl),sK2_skl(sK4_skl))|outputs(X0,bad)|~sQ546_spl)),
% 10.67/2.43 inference(resolution,[status(thm)],[f5394,f66])).
% 10.67/2.43 fof(f5400,plain,(
% 10.67/2.43 ![X0]: (sP3_prd(sK2_skl(sK4_skl),X0)|halts2(sK2_skl(sK4_skl),sK2_skl(sK4_skl))|outputs(X0,bad)|~sQ546_spl)),
% 10.67/2.43 inference(resolution,[status(thm)],[f5394,f76])).
% 10.67/2.43 fof(f5417,definition,(
% 10.67/2.43 ![X0]: (sQ548_spl <=> (sP3_prd(sK2_skl(sK4_skl),X0)|halts2(X0,sK2_skl(sK4_skl))))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ548_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f5420,definition,(
% 10.67/2.43 sQ549_spl <=> (halts2(sK2_skl(sK4_skl),sK2_skl(sK4_skl)))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ549_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f5421,plain,(
% 10.67/2.43 halts2(sK2_skl(sK4_skl),sK2_skl(sK4_skl))|~sQ549_spl),
% 10.67/2.43 inference(component_clause,[status(thm)],[f5420])).
% 10.67/2.43 fof(f5423,plain,(
% 10.67/2.43 sQ548_spl|sQ549_spl|~sQ546_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f5398,f5417,f5420,f5393])).
% 10.67/2.43 fof(f5424,definition,(
% 10.67/2.43 ![X0]: (sQ550_spl <=> (sP2_prd(sK2_skl(sK4_skl),X0)|outputs(X0,bad)))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ550_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f5427,plain,(
% 10.67/2.43 sQ550_spl|sQ549_spl|~sQ546_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f5399,f5424,f5420,f5393])).
% 10.67/2.43 fof(f5428,definition,(
% 10.67/2.43 ![X0]: (sQ551_spl <=> (sP3_prd(sK2_skl(sK4_skl),X0)|outputs(X0,bad)))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ551_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f5429,plain,(
% 10.67/2.43 ![X0]: (sP3_prd(sK2_skl(sK4_skl),X0)|outputs(X0,bad)|~sQ551_spl)),
% 10.67/2.43 inference(component_clause,[status(thm)],[f5428])).
% 10.67/2.43 fof(f5431,plain,(
% 10.67/2.43 sQ551_spl|sQ549_spl|~sQ546_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f5400,f5428,f5420,f5393])).
% 10.67/2.43 fof(f5494,plain,(
% 10.67/2.43 ![X0]: (sP5_prd(sK2_skl(sK4_skl),X0)|~program(sK2_skl(sK4_skl))|halts2(X0,sK2_skl(sK4_skl))|~sQ549_spl)),
% 10.67/2.43 inference(resolution,[status(thm)],[f5421,f89])).
% 10.67/2.43 fof(f5498,definition,(
% 10.67/2.43 ![X0]: (sQ566_spl <=> (sP5_prd(sK2_skl(sK4_skl),X0)|halts2(X0,sK2_skl(sK4_skl))))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ566_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f5501,definition,(
% 10.67/2.43 ![X1]: (sQ567_spl <=> (~sP3_prd(sK2_skl(sK4_skl),X1)))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ567_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f5502,plain,(
% 10.67/2.43 ![X0]: (~sP3_prd(sK2_skl(sK4_skl),X0)|~sQ567_spl)),
% 10.67/2.43 inference(component_clause,[status(thm)],[f5501])).
% 10.67/2.43 fof(f5505,plain,(
% 10.67/2.43 sQ566_spl|~sQ546_spl|~sQ549_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f5494,f5498,f5393,f5420])).
% 10.67/2.43 fof(f5507,plain,(
% 10.67/2.43 ![X0]: (outputs(X0,bad)|~sQ567_spl|~sQ551_spl)),
% 10.67/2.43 inference(backward_subsumption_resolution,[status(thm)],[f5429,f5502])).
% 10.67/2.43 fof(f5508,plain,(
% 10.67/2.43 sQ29_spl|~sQ567_spl|~sQ551_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f5507,f242,f5501,f5428])).
% 10.67/2.43 fof(f5610,plain,(
% 10.67/2.43 ~program(sK2_skl(sK1_skl))|~sQ52_spl|~sQ2_spl),
% 10.67/2.43 inference(resolution,[status(thm)],[f494,f99])).
% 10.67/2.43 fof(f5613,plain,(
% 10.67/2.43 ~sQ135_spl|~sQ52_spl|~sQ2_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f5610,f1082,f477,f98])).
% 10.67/2.43 fof(f5614,definition,(
% 10.67/2.43 sQ568_spl <=> (sP0_prd(sK2_skl(sK1_skl),sK1_skl))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ568_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f5615,plain,(
% 10.67/2.43 sP0_prd(sK2_skl(sK1_skl),sK1_skl)|~sQ568_spl),
% 10.67/2.43 inference(component_clause,[status(thm)],[f5614])).
% 10.67/2.43 fof(f5634,plain,(
% 10.67/2.43 ![X0,X1]: (~sP2_prd(X0,X1)|~halts3(X1,X0,X0)|~outputs(X1,bad)|~sQ4_spl)),
% 10.67/2.43 inference(backward_subsumption_resolution,[status(thm)],[f63,f331])).
% 10.67/2.43 fof(f5636,plain,(
% 10.67/2.43 ~sQ4_spl|~sQ199_spl),
% 10.67/2.43 inference(contradiction_clause,[status(thm)],[f4919])).
% 10.67/2.43 fof(f5638,plain,(
% 10.67/2.43 ![X0]: (outputs(X0,bad)|sQ27_spl|~sQ136_spl|~sQ26_spl)),
% 10.67/2.43 inference(forward_subsumption_resolution,[status(thm)],[f230,f1332])).
% 10.67/2.43 fof(f5672,definition,(
% 10.67/2.43 ![X1,X2]: (sQ573_spl <=> (~sP4_prd(X1,X2)))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ573_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f5673,plain,(
% 10.67/2.43 ![X0,X1]: (~sP4_prd(X0,X1)|~sQ573_spl)),
% 10.67/2.43 inference(component_clause,[status(thm)],[f5672])).
% 10.67/2.43 fof(f5736,plain,(
% 10.67/2.43 sQ29_spl|sQ27_spl|~sQ136_spl|~sQ26_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f5638,f242,f232,f1102,f229])).
% 10.67/2.43 fof(f5741,plain,(
% 10.67/2.43 $false|~sQ573_spl|~sQ191_spl),
% 10.67/2.43 inference(backward_subsumption_resolution,[status(thm)],[f2029,f5673])).
% 10.67/2.43 fof(f5798,plain,(
% 10.67/2.43 ~program(sK4_skl)|~program(sK4_skl)|~sQ9_spl|~sQ12_spl|~sQ10_spl),
% 10.67/2.43 inference(resolution,[status(thm)],[f313,f128])).
% 10.67/2.43 fof(f5799,plain,(
% 10.67/2.43 ~sQ8_spl|~sQ9_spl|~sQ12_spl|~sQ10_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f5798,f119,f123,f134,f127])).
% 10.67/2.43 fof(f5836,plain,(
% 10.67/2.43 ~program(sK1_skl)|outputs(sK1_skl,bad)|sQ52_spl|~sQ5_spl),
% 10.67/2.43 inference(resolution,[status(thm)],[f479,f110])).
% 10.67/2.43 fof(f5837,plain,(
% 10.67/2.43 ~sQ1_spl|sQ258_spl|sQ52_spl|~sQ5_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f5836,f94,f2871,f477,f109])).
% 10.67/2.43 fof(f5851,plain,(
% 10.67/2.43 ~program(sK1_skl)|outputs(sK1_skl,good)|~sQ3_spl|sQ52_spl),
% 10.67/2.43 inference(resolution,[status(thm)],[f103,f479])).
% 10.67/2.43 fof(f5854,plain,(
% 10.67/2.43 ~sQ1_spl|sQ542_spl|~sQ3_spl|sQ52_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f5851,f94,f4996,f102,f477])).
% 10.67/2.43 fof(f5933,plain,(
% 10.67/2.43 program(sK2_skl(sK1_skl))|~sQ568_spl),
% 10.67/2.43 inference(resolution,[status(thm)],[f5615,f48])).
% 10.67/2.43 fof(f5971,definition,(
% 10.67/2.43 sQ597_spl <=> (halts2(sK4_skl,sK4_skl))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ597_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f5972,plain,(
% 10.67/2.43 halts2(sK4_skl,sK4_skl)|~sQ597_spl),
% 10.67/2.43 inference(component_clause,[status(thm)],[f5971])).
% 10.67/2.43 fof(f5973,plain,(
% 10.67/2.43 ~halts2(sK4_skl,sK4_skl)|sQ597_spl),
% 10.67/2.43 inference(component_clause,[status(thm)],[f5971])).
% 10.67/2.43 fof(f5995,plain,(
% 10.67/2.43 ![X0]: (halts2(X0,sK3_skl(sK1_skl))|sQ21_spl|~sQ451_spl)),
% 10.67/2.43 inference(backward_subsumption_resolution,[status(thm)],[f4279,f707])).
% 10.67/2.43 fof(f5997,plain,(
% 10.67/2.43 $false|~sQ451_spl|sQ21_spl),
% 10.67/2.43 inference(backward_subsumption_resolution,[status(thm)],[f204,f5995])).
% 10.67/2.43 fof(f6000,plain,(
% 10.67/2.43 ~sQ451_spl|sQ21_spl),
% 10.67/2.43 inference(contradiction_clause,[status(thm)],[f5997])).
% 10.67/2.43 fof(f6151,plain,(
% 10.67/2.43 ![X0]: (sP5_prd(sK4_skl,X0)|~program(sK4_skl)|halts2(X0,sK4_skl)|~program(sK4_skl)|~sQ9_spl|~sQ12_spl)),
% 10.67/2.43 inference(resolution,[status(thm)],[f89,f313])).
% 10.67/2.43 fof(f6155,definition,(
% 10.67/2.43 ![X0]: (sQ604_spl <=> (sP5_prd(sK4_skl,X0)|halts2(X0,sK4_skl)))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ604_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f6156,plain,(
% 10.67/2.43 ![X0]: (sP5_prd(sK4_skl,X0)|halts2(X0,sK4_skl)|~sQ604_spl)),
% 10.67/2.43 inference(component_clause,[status(thm)],[f6155])).
% 10.67/2.43 fof(f6158,plain,(
% 10.67/2.43 sQ604_spl|~sQ8_spl|~sQ9_spl|~sQ12_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f6151,f6155,f119,f123,f134])).
% 10.67/2.43 fof(f6174,plain,(
% 10.67/2.43 ![X0]: (~sP3_prd(sK4_skl,X0)|sP5_prd(sK4_skl,X0)|~program(sK4_skl)|~sQ9_spl|~sQ12_spl)),
% 10.67/2.43 inference(resolution,[status(thm)],[f72,f313])).
% 10.67/2.43 fof(f6175,definition,(
% 10.67/2.43 ![X0]: (sQ605_spl <=> (~sP3_prd(sK4_skl,X0)|sP5_prd(sK4_skl,X0)))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ605_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f6178,plain,(
% 10.67/2.43 sQ605_spl|~sQ8_spl|~sQ9_spl|~sQ12_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f6174,f6175,f119,f123,f134])).
% 10.67/2.43 fof(f6285,plain,(
% 10.67/2.43 ![X0]: (halts2(X0,sK4_skl)|halts2(sK4_skl,sK4_skl)|~sQ604_spl)),
% 10.67/2.43 inference(resolution,[status(thm)],[f6156,f87])).
% 10.67/2.43 fof(f6287,definition,(
% 10.67/2.43 ![X0]: (sQ606_spl <=> (halts2(X0,sK4_skl)))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ606_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f6288,plain,(
% 10.67/2.43 ![X0]: (halts2(X0,sK4_skl)|~sQ606_spl)),
% 10.67/2.43 inference(component_clause,[status(thm)],[f6287])).
% 10.67/2.43 fof(f6291,plain,(
% 10.67/2.43 sQ606_spl|sQ597_spl|~sQ604_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f6285,f6287,f5971,f6155])).
% 10.67/2.43 fof(f6370,plain,(
% 10.67/2.43 ![X0]: (~sP3_prd(X0,sK4_skl)|sP5_prd(X0,sK4_skl)|~halts2(sK4_skl,X0)|~sQ14_spl)),
% 10.67/2.43 inference(resolution,[status(thm)],[f73,f142])).
% 10.67/2.43 fof(f6373,plain,(
% 10.67/2.43 ![X0]: (~sP3_prd(X0,sK4_skl)|~halts2(sK4_skl,X0)|~sQ11_spl|~sQ14_spl)),
% 10.67/2.43 inference(forward_subsumption_resolution,[status(thm)],[f6370,f369])).
% 10.67/2.43 fof(f6380,plain,(
% 10.67/2.43 ![X0]: (~sP3_prd(X0,sK4_skl)|~program(X0)|~sQ11_spl|~sQ14_spl|~sQ9_spl|~sQ12_spl)),
% 10.67/2.43 inference(resolution,[status(thm)],[f6373,f313])).
% 10.67/2.43 fof(f6382,plain,(
% 10.67/2.43 ![X0]: (~sP3_prd(X0,sK4_skl)|~sQ11_spl|~sQ14_spl|~sQ9_spl|~sQ12_spl)),
% 10.67/2.43 inference(forward_subsumption_resolution,[status(thm)],[f6380,f166])).
% 10.67/2.43 fof(f6387,plain,(
% 10.67/2.43 ~program(sK4_skl)|~sQ11_spl|~sQ14_spl|~sQ9_spl|~sQ12_spl|~sQ15_spl),
% 10.67/2.43 inference(resolution,[status(thm)],[f6382,f146])).
% 10.67/2.43 fof(f6388,plain,(
% 10.67/2.43 ~sQ8_spl|~sQ11_spl|~sQ14_spl|~sQ9_spl|~sQ12_spl|~sQ15_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f6387,f119,f130,f141,f123,f134,f145])).
% 10.67/2.43 fof(f6389,plain,(
% 10.67/2.43 sQ135_spl|~sQ568_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f5933,f1082,f5614])).
% 10.67/2.43 fof(f6395,plain,(
% 10.67/2.43 ~program(sK3_skl(sK1_skl))|~sQ13_spl|sQ21_spl),
% 10.67/2.43 inference(resolution,[status(thm)],[f139,f204])).
% 10.67/2.43 fof(f6399,plain,(
% 10.67/2.43 ~program(sK1_skl)|~sP3_prd(sK1_skl,sK1_skl)|~sQ13_spl|~sQ542_spl|~sQ258_spl),
% 10.67/2.43 inference(resolution,[status(thm)],[f139,f5010])).
% 10.67/2.43 fof(f6402,plain,(
% 10.67/2.43 ~sQ149_spl|~sQ13_spl|sQ21_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f6395,f1207,f138,f202])).
% 10.67/2.43 fof(f6406,plain,(
% 10.67/2.43 ~sQ1_spl|~sQ537_spl|~sQ13_spl|~sQ542_spl|~sQ258_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f6399,f94,f4799,f138,f4996,f2871])).
% 10.67/2.43 fof(f6411,plain,(
% 10.67/2.43 ~sQ151_spl|~sQ6_spl|sQ198_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f4948,f1284,f112,f2104])).
% 10.67/2.43 fof(f6423,plain,(
% 10.67/2.43 ![X0,X1]: (~program(X0)|outputs(X1,good)|program(X0)|~sQ13_spl)),
% 10.67/2.43 inference(resolution,[status(thm)],[f273,f79])).
% 10.67/2.43 fof(f6426,plain,(
% 10.67/2.43 sQ37_spl|sQ38_spl|~sQ13_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f6423,f393,f396,f138])).
% 10.67/2.43 fof(f6428,plain,(
% 10.67/2.43 ~halts2(sK1_skl,sK5_skl(sK1_skl))|~sQ22_spl|~sQ542_spl),
% 10.67/2.43 inference(resolution,[status(thm)],[f210,f5001])).
% 10.67/2.43 fof(f6433,plain,(
% 10.67/2.43 ~sQ201_spl|~sQ22_spl|~sQ542_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f6428,f2115,f209,f4996])).
% 10.67/2.43 fof(f6459,plain,(
% 10.67/2.43 ![X0]: (sP5_prd(sK5_skl(X0),X0)|~program(X0)|~sQ13_spl|~sQ15_spl)),
% 10.67/2.43 inference(resolution,[status(thm)],[f2168,f146])).
% 10.67/2.43 fof(f6477,plain,(
% 10.67/2.43 ![X0]: (sP1_prd(sK2_skl(sK1_skl),sK1_skl)|halts3(sK1_skl,sK4_skl,X0)|~sQ8_spl|~sQ1_spl)),
% 10.67/2.43 inference(resolution,[status(thm)],[f339,f95])).
% 10.67/2.43 fof(f6510,definition,(
% 10.67/2.43 ![X0]: (sQ619_spl <=> (halts3(sK1_skl,sK4_skl,X0)))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ619_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f6513,plain,(
% 10.67/2.43 sQ52_spl|sQ619_spl|~sQ8_spl|~sQ1_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f6477,f477,f6510,f119,f94])).
% 10.67/2.43 fof(f6514,plain,(
% 10.67/2.43 ~program(sK4_skl)|~halts2(sK4_skl,sK5_skl(sK4_skl))|~sQ13_spl|~sQ15_spl|~sQ11_spl),
% 10.67/2.43 inference(resolution,[status(thm)],[f6459,f369])).
% 10.67/2.43 fof(f6515,plain,(
% 10.67/2.43 ~program(sK1_skl)|~halts2(sK1_skl,sK5_skl(sK1_skl))|~sQ13_spl|~sQ15_spl|~sQ542_spl),
% 10.67/2.43 inference(resolution,[status(thm)],[f6459,f5001])).
% 10.67/2.43 fof(f6520,plain,(
% 10.67/2.43 ~sQ8_spl|~sQ35_spl|~sQ13_spl|~sQ15_spl|~sQ11_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f6514,f119,f379,f138,f145,f130])).
% 10.67/2.43 fof(f6521,plain,(
% 10.67/2.43 ~sQ1_spl|~sQ201_spl|~sQ13_spl|~sQ15_spl|~sQ542_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f6515,f94,f2115,f138,f145,f4996])).
% 10.67/2.43 fof(f6829,plain,(
% 10.67/2.43 ~halts3(sK1_skl,sK3_skl(sK1_skl),sK3_skl(sK1_skl))|~program(sK1_skl)|~sQ542_spl|~sQ258_spl|~sQ7_spl),
% 10.67/2.43 inference(resolution,[status(thm)],[f5003,f117])).
% 10.67/2.43 fof(f6832,plain,(
% 10.67/2.43 ~sQ190_spl|~sQ1_spl|~sQ542_spl|~sQ258_spl|~sQ7_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f6829,f1961,f94,f4996,f2871,f116])).
% 10.67/2.43 fof(f6942,plain,(
% 10.67/2.43 ![X0]: (sP5_prd(sK2_skl(sK4_skl),X0)|~program(sK2_skl(sK4_skl))|outputs(X0,good)|~sQ549_spl)),
% 10.67/2.43 inference(resolution,[status(thm)],[f90,f5421])).
% 10.67/2.43 fof(f6948,definition,(
% 10.67/2.43 ![X0]: (sQ621_spl <=> (sP5_prd(sK2_skl(sK4_skl),X0)|outputs(X0,good)))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ621_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f6949,plain,(
% 10.67/2.43 ![X0]: (sP5_prd(sK2_skl(sK4_skl),X0)|outputs(X0,good)|~sQ621_spl)),
% 10.67/2.43 inference(component_clause,[status(thm)],[f6948])).
% 10.67/2.43 fof(f6951,plain,(
% 10.67/2.43 sQ621_spl|~sQ546_spl|~sQ549_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f6942,f6948,f5393,f5420])).
% 10.67/2.43 fof(f6957,plain,(
% 10.67/2.43 ~sP3_prd(sK3_skl(sK4_skl),sK3_skl(sK4_skl))|sP5_prd(sK3_skl(sK4_skl),sK3_skl(sK4_skl))|~outputs(sK3_skl(sK4_skl),bad)|~sQ193_spl),
% 10.67/2.43 inference(resolution,[status(thm)],[f73,f2035])).
% 10.67/2.43 fof(f6958,definition,(
% 10.67/2.43 sQ622_spl <=> (sP3_prd(sK3_skl(sK4_skl),sK3_skl(sK4_skl)))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ622_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f6961,definition,(
% 10.67/2.43 sQ623_spl <=> (sP5_prd(sK3_skl(sK4_skl),sK3_skl(sK4_skl)))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ623_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f6962,plain,(
% 10.67/2.43 sP5_prd(sK3_skl(sK4_skl),sK3_skl(sK4_skl))|~sQ623_spl),
% 10.67/2.43 inference(component_clause,[status(thm)],[f6961])).
% 10.67/2.43 fof(f6964,definition,(
% 10.67/2.43 sQ624_spl <=> (outputs(sK3_skl(sK4_skl),bad))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ624_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f6967,plain,(
% 10.67/2.43 ~sQ622_spl|sQ623_spl|~sQ624_spl|~sQ193_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f6957,f6958,f6961,f6964,f2034])).
% 10.67/2.43 fof(f6978,plain,(
% 10.67/2.43 ~sP3_prd(sK4_skl,sK4_skl)|sP5_prd(sK4_skl,sK4_skl)|~outputs(sK4_skl,bad)|~sQ597_spl),
% 10.67/2.43 inference(resolution,[status(thm)],[f5972,f73])).
% 10.67/2.43 fof(f6979,plain,(
% 10.67/2.43 ![X0]: (sP4_prd(sK4_skl,X0)|~program(sK4_skl)|outputs(X0,good)|~sQ597_spl)),
% 10.67/2.43 inference(resolution,[status(thm)],[f5972,f83])).
% 10.67/2.43 fof(f6980,plain,(
% 10.67/2.43 ![X0]: (sP5_prd(sK4_skl,X0)|~program(sK4_skl)|outputs(X0,good)|~sQ597_spl)),
% 10.67/2.43 inference(resolution,[status(thm)],[f5972,f90])).
% 10.67/2.43 fof(f6984,definition,(
% 10.67/2.43 sQ626_spl <=> (sP3_prd(sK4_skl,sK4_skl))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ626_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f6987,definition,(
% 10.67/2.43 sQ627_spl <=> (sP5_prd(sK4_skl,sK4_skl))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ627_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f6988,plain,(
% 10.67/2.43 sP5_prd(sK4_skl,sK4_skl)|~sQ627_spl),
% 10.67/2.43 inference(component_clause,[status(thm)],[f6987])).
% 10.67/2.43 fof(f6990,plain,(
% 10.67/2.43 ~sQ626_spl|sQ627_spl|~sQ14_spl|~sQ597_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f6978,f6984,f6987,f141,f5971])).
% 10.67/2.43 fof(f6991,definition,(
% 10.67/2.43 ![X0]: (sQ628_spl <=> (sP4_prd(sK4_skl,X0)|outputs(X0,good)))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ628_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f6992,plain,(
% 10.67/2.43 ![X0]: (sP4_prd(sK4_skl,X0)|outputs(X0,good)|~sQ628_spl)),
% 10.67/2.43 inference(component_clause,[status(thm)],[f6991])).
% 10.67/2.43 fof(f6994,plain,(
% 10.67/2.43 sQ628_spl|~sQ8_spl|~sQ597_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f6979,f6991,f119,f5971])).
% 10.67/2.43 fof(f6995,definition,(
% 10.67/2.43 ![X0]: (sQ629_spl <=> (sP5_prd(sK4_skl,X0)|outputs(X0,good)))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ629_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f6998,plain,(
% 10.67/2.43 sQ629_spl|~sQ8_spl|~sQ597_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f6980,f6995,f119,f5971])).
% 10.67/2.43 fof(f7000,plain,(
% 10.67/2.43 ~halts2(sK4_skl,sK4_skl)|~outputs(sK4_skl,good)|~sQ627_spl),
% 10.67/2.43 inference(resolution,[status(thm)],[f6988,f88])).
% 10.67/2.43 fof(f7006,plain,(
% 10.67/2.43 ~sQ597_spl|~sQ11_spl|~sQ627_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f7000,f5971,f130,f6987])).
% 10.67/2.43 fof(f7013,plain,(
% 10.67/2.43 ~program(sK4_skl)|program(sK2_skl(sK4_skl))|sQ14_spl|~sQ5_spl),
% 10.67/2.43 inference(resolution,[status(thm)],[f143,f1797])).
% 10.67/2.43 fof(f7014,plain,(
% 10.67/2.43 ~sQ8_spl|sQ546_spl|sQ14_spl|~sQ5_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f7013,f119,f5393,f141,f109])).
% 10.67/2.43 fof(f7015,plain,(
% 10.67/2.43 $false|~sQ606_spl|sQ597_spl),
% 10.67/2.43 inference(forward_subsumption_resolution,[status(thm)],[f5973,f6288])).
% 10.67/2.43 fof(f7016,plain,(
% 10.67/2.43 ~sQ606_spl|sQ597_spl),
% 10.67/2.43 inference(contradiction_clause,[status(thm)],[f7015])).
% 10.67/2.43 fof(f7044,plain,(
% 10.67/2.43 program(sK3_skl(sK4_skl))|~sQ623_spl),
% 10.67/2.43 inference(resolution,[status(thm)],[f6962,f86])).
% 10.67/2.43 fof(f7051,plain,(
% 10.67/2.43 sQ192_spl|~sQ623_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f7044,f2031,f6961])).
% 10.67/2.43 fof(f7058,plain,(
% 10.67/2.43 ![X0,X1]: (outputs(X0,good)|~sP2_prd(sK4_skl,X1)|sP4_prd(sK4_skl,X1)|~sQ628_spl)),
% 10.67/2.43 inference(resolution,[status(thm)],[f6992,f511])).
% 10.67/2.43 fof(f7064,definition,(
% 10.67/2.43 ![X1]: (sQ632_spl <=> (~sP2_prd(sK4_skl,X1)|sP4_prd(sK4_skl,X1)))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ632_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f7067,plain,(
% 10.67/2.43 sQ38_spl|sQ632_spl|~sQ628_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f7058,f396,f7064,f6991])).
% 10.67/2.43 fof(f7369,plain,(
% 10.67/2.43 ~sQ198_spl|~sQ38_spl|~sQ30_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f404,f2104,f396,f251])).
% 10.67/2.43 fof(f7373,plain,(
% 10.67/2.43 ~sQ151_spl|~sQ6_spl|sQ23_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f4949,f1284,f112,f212])).
% 10.67/2.43 fof(f7386,plain,(
% 10.67/2.43 $false|~sQ29_spl|sQ14_spl),
% 10.67/2.43 inference(forward_subsumption_resolution,[status(thm)],[f143,f243])).
% 10.67/2.43 fof(f7387,plain,(
% 10.67/2.43 ~sQ29_spl|sQ14_spl),
% 10.67/2.43 inference(contradiction_clause,[status(thm)],[f7386])).
% 10.67/2.43 fof(f7477,definition,(
% 10.67/2.43 ![X0]: (sQ658_spl <=> (sP5_prd(sK2_skl(sK1_skl),X0)|outputs(X0,good)))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ658_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f7481,definition,(
% 10.67/2.43 ![X0]: (sQ659_spl <=> (sP4_prd(sK2_skl(sK1_skl),X0)|outputs(X0,good)))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ659_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f7499,plain,(
% 10.67/2.43 ~halts3(sK1_skl,sK3_skl(sK1_skl),sK3_skl(sK1_skl))|~outputs(sK1_skl,good)|~sQ20_spl),
% 10.67/2.43 inference(resolution,[status(thm)],[f81,f200])).
% 10.67/2.43 fof(f7500,plain,(
% 10.67/2.43 ~sQ190_spl|~sQ542_spl|~sQ20_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f7499,f1961,f4996,f199])).
% 10.67/2.43 fof(f7588,plain,(
% 10.67/2.43 ![X0]: (sP5_prd(sK2_skl(sK1_skl),X0)|~program(sK2_skl(sK1_skl))|outputs(X0,good)|~sQ133_spl)),
% 10.67/2.43 inference(resolution,[status(thm)],[f1071,f90])).
% 10.67/2.43 fof(f7589,plain,(
% 10.67/2.43 ![X0]: (sP4_prd(sK2_skl(sK1_skl),X0)|~program(sK2_skl(sK1_skl))|outputs(X0,good)|~sQ133_spl)),
% 10.67/2.43 inference(resolution,[status(thm)],[f1071,f83])).
% 10.67/2.43 fof(f7594,definition,(
% 10.67/2.43 sQ668_spl <=> (sP3_prd(sK2_skl(sK1_skl),sK2_skl(sK1_skl)))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ668_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f7596,plain,(
% 10.67/2.43 ~sP3_prd(sK2_skl(sK1_skl),sK2_skl(sK1_skl))|sQ668_spl),
% 10.67/2.43 inference(component_clause,[status(thm)],[f7594])).
% 10.67/2.43 fof(f7597,definition,(
% 10.67/2.43 sQ669_spl <=> (sP5_prd(sK2_skl(sK1_skl),sK2_skl(sK1_skl)))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ669_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f7598,plain,(
% 10.67/2.43 sP5_prd(sK2_skl(sK1_skl),sK2_skl(sK1_skl))|~sQ669_spl),
% 10.67/2.43 inference(component_clause,[status(thm)],[f7597])).
% 10.67/2.43 fof(f7601,plain,(
% 10.67/2.43 sQ658_spl|~sQ135_spl|~sQ133_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f7588,f7477,f1082,f1070])).
% 10.67/2.43 fof(f7602,plain,(
% 10.67/2.43 sQ659_spl|~sQ135_spl|~sQ133_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f7589,f7481,f1082,f1070])).
% 10.67/2.43 fof(f7648,plain,(
% 10.67/2.43 ~halts2(sK2_skl(sK1_skl),sK2_skl(sK1_skl))|~outputs(sK2_skl(sK1_skl),good)|~sQ669_spl),
% 10.67/2.43 inference(resolution,[status(thm)],[f7598,f88])).
% 10.67/2.43 fof(f7651,plain,(
% 10.67/2.43 program(sK2_skl(sK1_skl))|~sQ669_spl),
% 10.67/2.43 inference(resolution,[status(thm)],[f7598,f86])).
% 10.67/2.43 fof(f7653,plain,(
% 10.67/2.43 sP3_prd(sK2_skl(sK1_skl),sK2_skl(sK1_skl))|~sQ669_spl),
% 10.67/2.43 inference(resolution,[status(thm)],[f7598,f74])).
% 10.67/2.43 fof(f7654,definition,(
% 10.67/2.43 sQ674_spl <=> (outputs(sK2_skl(sK1_skl),good))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ674_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f7657,plain,(
% 10.67/2.43 ~sQ133_spl|~sQ674_spl|~sQ669_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f7648,f1070,f7654,f7597])).
% 10.67/2.43 fof(f7658,plain,(
% 10.67/2.43 sQ135_spl|~sQ669_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f7651,f1082,f7597])).
% 10.67/2.43 fof(f7659,plain,(
% 10.67/2.43 $false|sQ668_spl|~sQ669_spl),
% 10.67/2.43 inference(forward_subsumption_resolution,[status(thm)],[f7653,f7596])).
% 10.67/2.43 fof(f7660,plain,(
% 10.67/2.43 sQ668_spl|~sQ669_spl),
% 10.67/2.43 inference(contradiction_clause,[status(thm)],[f7659])).
% 10.67/2.43 fof(f7743,plain,(
% 10.67/2.43 ~program(sK2_skl(sK1_skl))|outputs(sK2_skl(sK1_skl),good)|sQ56_spl|~sQ3_spl),
% 10.67/2.43 inference(resolution,[status(thm)],[f499,f103])).
% 10.67/2.43 fof(f7744,plain,(
% 10.67/2.43 ~sQ135_spl|sQ674_spl|sQ56_spl|~sQ3_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f7743,f1082,f7654,f497,f102])).
% 10.67/2.43 fof(f7803,plain,(
% 10.67/2.43 ![X0,X1]: (outputs(X0,good)|~sP2_prd(sK2_skl(sK4_skl),X1)|sP4_prd(sK2_skl(sK4_skl),X1)|~sQ621_spl)),
% 10.67/2.43 inference(resolution,[status(thm)],[f6949,f512])).
% 10.67/2.43 fof(f7806,plain,(
% 10.67/2.43 ![X0]: (outputs(X0,good)|halts2(sK2_skl(sK4_skl),sK2_skl(sK4_skl))|~sQ621_spl)),
% 10.67/2.43 inference(resolution,[status(thm)],[f6949,f87])).
% 10.67/2.43 fof(f7813,definition,(
% 10.67/2.43 ![X1]: (sQ682_spl <=> (sP4_prd(sK2_skl(sK4_skl),X1)|outputs(X1,good)))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ682_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f7817,definition,(
% 10.67/2.43 ![X1]: (sQ683_spl <=> (~sP2_prd(sK2_skl(sK4_skl),X1)|sP4_prd(sK2_skl(sK4_skl),X1)))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ683_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f7820,plain,(
% 10.67/2.43 sQ38_spl|sQ683_spl|~sQ621_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f7803,f396,f7817,f6948])).
% 10.67/2.43 fof(f7823,plain,(
% 10.67/2.43 sQ38_spl|sQ549_spl|~sQ621_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f7806,f396,f5420,f6948])).
% 10.67/2.43 fof(f7828,plain,(
% 10.67/2.43 ![X0]: (sP4_prd(sK2_skl(sK4_skl),X0)|~program(sK2_skl(sK4_skl))|outputs(X0,good)|~sQ549_spl)),
% 10.67/2.43 inference(resolution,[status(thm)],[f5421,f83])).
% 10.67/2.43 fof(f7836,definition,(
% 10.67/2.43 sQ685_spl <=> (sP5_prd(sK2_skl(sK4_skl),sK2_skl(sK4_skl)))),
% 10.67/2.43 introduced(definition,[new_symbols(definition,[sQ685_spl])],[split_symbol_definition])).
% 10.67/2.43 fof(f7837,plain,(
% 10.67/2.43 sP5_prd(sK2_skl(sK4_skl),sK2_skl(sK4_skl))|~sQ685_spl),
% 10.67/2.43 inference(component_clause,[status(thm)],[f7836])).
% 10.67/2.43 fof(f7841,plain,(
% 10.67/2.43 sQ682_spl|~sQ546_spl|~sQ549_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f7828,f7813,f5393,f5420])).
% 10.67/2.43 fof(f7851,plain,(
% 10.67/2.43 halts2(sK2_skl(sK4_skl),sK2_skl(sK4_skl))|~sQ685_spl),
% 10.67/2.43 inference(resolution,[status(thm)],[f7837,f87])).
% 10.67/2.43 fof(f7859,plain,(
% 10.67/2.43 sQ549_spl|~sQ685_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f7851,f5420,f7836])).
% 10.67/2.43 fof(f8273,plain,(
% 10.67/2.43 ~program(sK1_skl)|sQ190_spl|~sQ118_spl),
% 10.67/2.43 inference(resolution,[status(thm)],[f1963,f1000])).
% 10.67/2.43 fof(f8276,plain,(
% 10.67/2.43 $false|~sQ1_spl|sQ190_spl|~sQ118_spl),
% 10.67/2.43 inference(forward_subsumption_resolution,[status(thm)],[f8273,f95])).
% 10.67/2.43 fof(f8277,plain,(
% 10.67/2.43 ~sQ1_spl|sQ190_spl|~sQ118_spl),
% 10.67/2.43 inference(contradiction_clause,[status(thm)],[f8276])).
% 10.67/2.43 fof(f8289,plain,(
% 10.67/2.43 ![X0,X1]: (~program(X0)|~halts2(X0,X0)|outputs(X1,good)|~sQ4_spl)),
% 10.67/2.43 inference(backward_subsumption_resolution,[status(thm)],[f83,f331])).
% 10.67/2.43 fof(f8325,plain,(
% 10.67/2.43 ~sQ573_spl|~sQ191_spl),
% 10.67/2.43 inference(contradiction_clause,[status(thm)],[f5741])).
% 10.67/2.43 fof(f8327,plain,(
% 10.67/2.43 sQ10_spl|sQ38_spl|~sQ4_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f8289,f127,f396,f105])).
% 10.67/2.43 fof(f8587,plain,(
% 10.67/2.43 ![X0,X1]: (~program(X0)|outputs(X1,bad)|~halts2(X0,X0)|~sQ4_spl)),
% 10.67/2.43 inference(resolution,[status(thm)],[f4913,f323])).
% 10.67/2.43 fof(f8592,plain,(
% 10.67/2.43 sQ10_spl|sQ29_spl|~sQ4_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f8587,f127,f242,f105])).
% 10.67/2.43 fof(f8594,plain,(
% 10.67/2.43 ~halts3(sK1_skl,sK3_skl(sK1_skl),sK3_skl(sK1_skl))|~outputs(sK1_skl,bad)|~sQ1_spl|~sQ7_spl|~sQ4_spl),
% 10.67/2.43 inference(resolution,[status(thm)],[f180,f5634])).
% 10.67/2.43 fof(f8597,plain,(
% 10.67/2.43 ~sQ190_spl|~sQ258_spl|~sQ1_spl|~sQ7_spl|~sQ4_spl),
% 10.67/2.43 inference(split_clause,[status(thm)],[f8594,f1961,f2871,f94,f116,f105])).
% 10.67/2.43 fof(f8598,plain,(
% 10.67/2.43 $false),
% 10.67/2.43 inference(sat_refutation,[status(thm)],[f97,f101,f108,f115,f122,f126,f133,f137,f144,f151,f155,f159,f177,f205,f215,f224,f228,f235,f241,f289,f309,f312,f332,f382,f415,f483,f535,f555,f570,f621,f625,f684,f709,f749,f831,f904,f911,f1002,f1085,f1087,f1101,f1127,f1190,f1216,f1217,f1219,f1289,f1329,f1523,f1589,f1593,f1621,f1625,f1803,f1975,f2005,f2006,f2046,f2165,f2166,f2237,f2464,f2468,f2497,f2874,f3234,f3695,f3811,f3818,f4089,f4090,f4093,f4095,f4291,f4940,f4954,f5423,f5427,f5431,f5505,f5508,f5613,f5636,f5736,f5799,f5837,f5854,f6000,f6158,f6178,f6291,f6388,f6389,f6402,f6406,f6411,f6426,f6433,f6513,f6520,f6521,f6832,f6951,f6967,f6990,f6994,f6998,f7006,f7014,f7016,f7051,f7067,f7369,f7373,f7387,f7500,f7601,f7602,f7657,f7658,f7660,f7744,f7820,f7823,f7841,f7859,f8277,f8325,f8327,f8592,f8597])).
% 10.67/2.43 % SZS output end CNFRefutation for theBenchmark.p
% 10.67/2.45 % Elapsed time: 2.080122 seconds
% 10.67/2.45 % CPU time: 16.148244 seconds
% 10.67/2.45 % Total memory used: 116.549 MB
% 10.67/2.45 % Net memory used: 111.584 MB
%------------------------------------------------------------------------------