↑ Up

Drodi-SAT---4.1.1.UNS-Ass.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : Drodi-SAT---4.1.1
% Problem  : COM003-1 : TPTP v9.3.1. Bugfixed v1.0.1.
% Transfm  : none
% Format   : tptp:raw
% Command  : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p

% Computer : n013.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Thu Sep 24 12:10:40 PM UTC 2026

% Result   : Unsatisfiable 0.14s 0.44s
% 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. Bugfixed v1.0.1.
% 0.00/0.03  % Command  : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35  % Computer : n013.cluster.edu
% 0.09/0.35  % Model    : x86_64 x86_64
% 0.09/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35  % Memory   : 8046.5625MB
% 0.09/0.35  % OS       : Linux 6.8.0-71-generic
% 0.09/0.35  % CPULimit : 300
% 0.09/0.35  % WCLimit  : 300
% 0.09/0.35  % DateTime : Mon Sep 21 14:13:05 UTC 2026
% 0.09/0.35  % CPUTime  : 
% 0.14/0.36  % Drodi V4.1.1
% 0.14/0.44  % Refutation found
% 0.14/0.44  % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/0.44  % SZS output start CNFRefutation for theBenchmark
% 0.14/0.44  fof(f1,hypothesis,(
% 0.14/0.44    (![X]: (( ~ algorithm(X)| program(f2(X))| program(c1) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f2,hypothesis,(
% 0.14/0.44    (![X,Y,Z]: (( ~ algorithm(X)| program(f2(X))| ~ program(Y)| decides(c1,Y,Z) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f3,hypothesis,(
% 0.14/0.44    (![X]: (( ~ algorithm(X)| ~ decides(X,f2(X),f1(X))| program(c1) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f4,hypothesis,(
% 0.14/0.44    (![X,Y,Z]: (( ~ algorithm(X)| ~ decides(X,f2(X),f1(X))| ~ program(Y)| decides(c1,Y,Z) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f5,hypothesis,(
% 0.14/0.44    (![W,Y,Z]: (( ~ program(W)| program(f4(W))| ~ program(Y)| ~ halts2(Y,Z)| halts3(W,Y,Z) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f6,hypothesis,(
% 0.14/0.44    (![W,Y,Z]: (( ~ program(W)| program(f4(W))| ~ program(Y)| ~ halts2(Y,Z)| outputs(W,good) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f7,hypothesis,(
% 0.14/0.44    (![W,Y,Z]: (( ~ program(W)| program(f4(W))| ~ program(Y)| halts2(Y,Z)| halts3(W,Y,Z) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f8,hypothesis,(
% 0.14/0.44    (![W,Y,Z]: (( ~ program(W)| program(f4(W))| ~ program(Y)| halts2(Y,Z)| outputs(W,bad) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f9,hypothesis,(
% 0.14/0.44    (![W,Y,Z]: (( ~ program(W)| ~ decides(W,f4(W),f3(W))| ~ program(Y)| ~ halts2(Y,Z)| halts3(W,Y,Z) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f10,hypothesis,(
% 0.14/0.44    (![W,Y,Z]: (( ~ program(W)| ~ decides(W,f4(W),f3(W))| ~ program(Y)| ~ halts2(Y,Z)| outputs(W,good) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f11,hypothesis,(
% 0.14/0.44    (![W,Y,Z]: (( ~ program(W)| ~ decides(W,f4(W),f3(W))| ~ program(Y)| halts2(Y,Z)| halts3(W,Y,Z) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f12,hypothesis,(
% 0.14/0.44    (![W,Y,Z]: (( ~ program(W)| ~ decides(W,f4(W),f3(W))| ~ program(Y)| halts2(Y,Z)| outputs(W,bad) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f13,hypothesis,(
% 0.14/0.44    (![W]: (( ~ program(W)| program(f5(W))| program(c2) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f14,hypothesis,(
% 0.14/0.44    (![W,Y]: (( ~ program(W)| program(f5(W))| ~ program(Y)| ~ halts2(Y,Y)| halts2(c2,Y) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f15,hypothesis,(
% 0.14/0.44    (![W,Y]: (( ~ program(W)| program(f5(W))| ~ program(Y)| ~ halts2(Y,Y)| outputs(c2,good) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f16,hypothesis,(
% 0.14/0.44    (![W,Y]: (( ~ program(W)| program(f5(W))| ~ program(Y)| halts2(Y,Y)| halts2(c2,Y) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f17,hypothesis,(
% 0.14/0.44    (![W,Y]: (( ~ program(W)| program(f5(W))| ~ program(Y)| halts2(Y,Y)| outputs(c2,bad) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f18,hypothesis,(
% 0.14/0.44    (![W]: (( ~ program(W)| halts2(f5(W),f5(W))| ~ halts3(W,f5(W),f5(W))| ~ outputs(W,bad)| program(c2) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f19,hypothesis,(
% 0.14/0.44    (![W,Y]: (( ~ program(W)| halts2(f5(W),f5(W))| ~ halts3(W,f5(W),f5(W))| ~ outputs(W,bad)| ~ program(Y)| ~ halts2(Y,Y)| halts2(c2,Y) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f20,hypothesis,(
% 0.14/0.44    (![W,Y]: (( ~ program(W)| halts2(f5(W),f5(W))| ~ halts3(W,f5(W),f5(W))| ~ outputs(W,bad)| ~ program(Y)| ~ halts2(Y,Y)| outputs(c2,good) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f21,hypothesis,(
% 0.14/0.44    (![W,Y]: (( ~ program(W)| halts2(f5(W),f5(W))| ~ halts3(W,f5(W),f5(W))| ~ outputs(W,bad)| ~ program(Y)| halts2(Y,Y)| halts2(c2,Y) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f22,hypothesis,(
% 0.14/0.44    (![W,Y]: (( ~ program(W)| halts2(f5(W),f5(W))| ~ halts3(W,f5(W),f5(W))| ~ outputs(W,bad)| ~ program(Y)| halts2(Y,Y)| outputs(c2,bad) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f23,hypothesis,(
% 0.14/0.44    (![W]: (( ~ program(W)| ~ halts3(W,f5(W),f5(W))| ~ outputs(W,good)| ~ halts2(f5(W),f5(W))| program(c2) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f24,hypothesis,(
% 0.14/0.44    (![W,Y]: (( ~ program(W)| ~ halts3(W,f5(W),f5(W))| ~ outputs(W,good)| ~ halts2(f5(W),f5(W))| ~ program(Y)| ~ halts2(Y,Y)| halts2(c2,Y) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f25,hypothesis,(
% 0.14/0.44    (![W,Y]: (( ~ program(W)| ~ halts3(W,f5(W),f5(W))| ~ outputs(W,good)| ~ halts2(f5(W),f5(W))| ~ program(Y)| ~ halts2(Y,Y)| outputs(c2,good) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f26,hypothesis,(
% 0.14/0.44    (![W,Y]: (( ~ program(W)| ~ halts3(W,f5(W),f5(W))| ~ outputs(W,good)| ~ halts2(f5(W),f5(W))| ~ program(Y)| halts2(Y,Y)| halts2(c2,Y) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f27,hypothesis,(
% 0.14/0.44    (![W,Y]: (( ~ program(W)| ~ halts3(W,f5(W),f5(W))| ~ outputs(W,good)| ~ halts2(f5(W),f5(W))| ~ program(Y)| halts2(Y,Y)| outputs(c2,bad) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f28,hypothesis,(
% 0.14/0.44    (![W]: (( ~ program(W)| ~ halts3(W,f5(W),f5(W))| ~ outputs(W,good)| ~ outputs(W,bad)| program(c2) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f29,hypothesis,(
% 0.14/0.44    (![W,Y]: (( ~ program(W)| ~ halts3(W,f5(W),f5(W))| ~ outputs(W,good)| ~ outputs(W,bad)| ~ program(Y)| ~ halts2(Y,Y)| halts2(c2,Y) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f30,hypothesis,(
% 0.14/0.44    (![W,Y]: (( ~ program(W)| ~ halts3(W,f5(W),f5(W))| ~ outputs(W,good)| ~ outputs(W,bad)| ~ program(Y)| ~ halts2(Y,Y)| outputs(c2,good) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f31,hypothesis,(
% 0.14/0.44    (![W,Y]: (( ~ program(W)| ~ halts3(W,f5(W),f5(W))| ~ outputs(W,good)| ~ outputs(W,bad)| ~ program(Y)| halts2(Y,Y)| halts2(c2,Y) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f32,hypothesis,(
% 0.14/0.44    (![W,Y]: (( ~ program(W)| ~ halts3(W,f5(W),f5(W))| ~ outputs(W,good)| ~ outputs(W,bad)| ~ program(Y)| halts2(Y,Y)| outputs(c2,bad) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f33,hypothesis,(
% 0.14/0.44    (![V]: (( ~ program(V)| program(f6(V))| program(c3) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f34,hypothesis,(
% 0.14/0.44    (![V,Y]: (( ~ program(V)| program(f6(V))| ~ program(Y)| ~ halts2(Y,Y)| ~ halts2(c3,Y) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f35,hypothesis,(
% 0.14/0.44    (![V,Y]: (( ~ program(V)| program(f6(V))| ~ program(Y)| halts2(Y,Y)| halts2(c3,Y) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f36,hypothesis,(
% 0.14/0.44    (![V,Y]: (( ~ program(V)| program(f6(V))| ~ program(Y)| halts2(Y,Y)| outputs(c3,bad) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f37,hypothesis,(
% 0.14/0.44    (![V]: (( ~ program(V)| halts2(f6(V),f6(V))| ~ halts2(V,f6(V))| ~ outputs(V,bad)| program(c3) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f38,hypothesis,(
% 0.14/0.44    (![V,Y]: (( ~ program(V)| halts2(f6(V),f6(V))| ~ halts2(V,f6(V))| ~ outputs(V,bad)| ~ program(Y)| ~ halts2(Y,Y)| ~ halts2(c3,Y) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f39,hypothesis,(
% 0.14/0.44    (![V,Y]: (( ~ program(V)| halts2(f6(V),f6(V))| ~ halts2(V,f6(V))| ~ outputs(V,bad)| ~ program(Y)| halts2(Y,Y)| halts2(c3,Y) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f40,hypothesis,(
% 0.14/0.44    (![V,Y]: (( ~ program(V)| halts2(f6(V),f6(V))| ~ halts2(V,f6(V))| ~ outputs(V,bad)| ~ program(Y)| halts2(Y,Y)| outputs(c3,bad) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f41,hypothesis,(
% 0.14/0.44    (![V]: (( ~ program(V)| ~ halts2(V,f6(V))| ~ outputs(V,good)| ~ halts2(f6(V),f6(V))| program(c3) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f42,hypothesis,(
% 0.14/0.44    (![V,Y]: (( ~ program(V)| ~ halts2(V,f6(V))| ~ outputs(V,good)| ~ halts2(f6(V),f6(V))| ~ program(Y)| ~ halts2(Y,Y)| ~ halts2(c3,Y) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f43,hypothesis,(
% 0.14/0.44    (![V,Y]: (( ~ program(V)| ~ halts2(V,f6(V))| ~ outputs(V,good)| ~ halts2(f6(V),f6(V))| ~ program(Y)| halts2(Y,Y)| halts2(c3,Y) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f44,hypothesis,(
% 0.14/0.44    (![V,Y]: (( ~ program(V)| ~ halts2(V,f6(V))| ~ outputs(V,good)| ~ halts2(f6(V),f6(V))| ~ program(Y)| halts2(Y,Y)| outputs(c3,bad) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f45,hypothesis,(
% 0.14/0.44    (![V]: (( ~ program(V)| ~ halts2(V,f6(V))| ~ outputs(V,good)| ~ outputs(V,bad)| program(c3) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f46,hypothesis,(
% 0.14/0.44    (![V,Y]: (( ~ program(V)| ~ halts2(V,f6(V))| ~ outputs(V,good)| ~ outputs(V,bad)| ~ program(Y)| ~ halts2(Y,Y)| ~ halts2(c3,Y) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f47,hypothesis,(
% 0.14/0.44    (![V,Y]: (( ~ program(V)| ~ halts2(V,f6(V))| ~ outputs(V,good)| ~ outputs(V,bad)| ~ program(Y)| halts2(Y,Y)| halts2(c3,Y) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f48,hypothesis,(
% 0.14/0.44    (![V,Y]: (( ~ program(V)| ~ halts2(V,f6(V))| ~ outputs(V,good)| ~ outputs(V,bad)| ~ program(Y)| halts2(Y,Y)| outputs(c3,bad) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f49,negated_conjecture,(
% 0.14/0.44    algorithm(c4) ),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f50,negated_conjecture,(
% 0.14/0.44    (![Y1,Z1]: (( ~ program(Y1)| decides(c4,Y1,Z1) ) ))),
% 0.14/0.44    file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.44  fof(f51,plain,(
% 0.14/0.44    (![X]: (~algorithm(X)|program(f2(X))))|program(c1)),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f1])).
% 0.14/0.44  fof(f52,plain,(
% 0.14/0.44    ![X0]: (~algorithm(X0)|program(f2(X0))|program(c1))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f51])).
% 0.14/0.44  fof(f53,plain,(
% 0.14/0.44    ![Y]: (((![X]: (~algorithm(X)|program(f2(X))))|~program(Y))|(![Z]: decides(c1,Y,Z)))),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f2])).
% 0.14/0.44  fof(f54,plain,(
% 0.14/0.44    ![X0,X1,X2]: (~algorithm(X0)|program(f2(X0))|~program(X1)|decides(c1,X1,X2))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f53])).
% 0.14/0.44  fof(f55,plain,(
% 0.14/0.44    (![X]: (~algorithm(X)|~decides(X,f2(X),f1(X))))|program(c1)),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f3])).
% 0.14/0.44  fof(f56,plain,(
% 0.14/0.44    ![X0]: (~algorithm(X0)|~decides(X0,f2(X0),f1(X0))|program(c1))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f55])).
% 0.14/0.44  fof(f57,plain,(
% 0.14/0.44    ![Y]: (((![X]: (~algorithm(X)|~decides(X,f2(X),f1(X))))|~program(Y))|(![Z]: decides(c1,Y,Z)))),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f4])).
% 0.14/0.44  fof(f58,plain,(
% 0.14/0.44    ![X0,X1,X2]: (~algorithm(X0)|~decides(X0,f2(X0),f1(X0))|~program(X1)|decides(c1,X1,X2))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f57])).
% 0.14/0.44  fof(f59,plain,(
% 0.14/0.44    ![X0,X1,X2]: (~program(X0)|program(f4(X0))|~program(X1)|~halts2(X1,X2)|halts3(X0,X1,X2))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f5])).
% 0.14/0.44  fof(f60,plain,(
% 0.14/0.44    ![W]: ((![Y]: (((~program(W)|program(f4(W)))|~program(Y))|(![Z]: ~halts2(Y,Z))))|outputs(W,good))),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f6])).
% 0.14/0.44  fof(f61,plain,(
% 0.14/0.44    ![X0,X1,X2]: (~program(X0)|program(f4(X0))|~program(X1)|~halts2(X1,X2)|outputs(X0,good))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f60])).
% 0.14/0.44  fof(f62,plain,(
% 0.14/0.44    ![X0,X1,X2]: (~program(X0)|program(f4(X0))|~program(X1)|halts2(X1,X2)|halts3(X0,X1,X2))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f7])).
% 0.14/0.44  fof(f63,plain,(
% 0.14/0.44    ![W]: ((![Y]: (((~program(W)|program(f4(W)))|~program(Y))|(![Z]: halts2(Y,Z))))|outputs(W,bad))),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f8])).
% 0.14/0.44  fof(f64,plain,(
% 0.14/0.44    ![X0,X1,X2]: (~program(X0)|program(f4(X0))|~program(X1)|halts2(X1,X2)|outputs(X0,bad))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f63])).
% 0.14/0.44  fof(f65,plain,(
% 0.14/0.44    ![X0,X1,X2]: (~program(X0)|~decides(X0,f4(X0),f3(X0))|~program(X1)|~halts2(X1,X2)|halts3(X0,X1,X2))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f9])).
% 0.14/0.44  fof(f66,plain,(
% 0.14/0.44    ![W]: ((![Y]: (((~program(W)|~decides(W,f4(W),f3(W)))|~program(Y))|(![Z]: ~halts2(Y,Z))))|outputs(W,good))),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f10])).
% 0.14/0.44  fof(f67,plain,(
% 0.14/0.44    ![X0,X1,X2]: (~program(X0)|~decides(X0,f4(X0),f3(X0))|~program(X1)|~halts2(X1,X2)|outputs(X0,good))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f66])).
% 0.14/0.44  fof(f68,plain,(
% 0.14/0.44    ![X0,X1,X2]: (~program(X0)|~decides(X0,f4(X0),f3(X0))|~program(X1)|halts2(X1,X2)|halts3(X0,X1,X2))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f11])).
% 0.14/0.44  fof(f69,plain,(
% 0.14/0.44    ![W]: ((![Y]: (((~program(W)|~decides(W,f4(W),f3(W)))|~program(Y))|(![Z]: halts2(Y,Z))))|outputs(W,bad))),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f12])).
% 0.14/0.44  fof(f70,plain,(
% 0.14/0.44    ![X0,X1,X2]: (~program(X0)|~decides(X0,f4(X0),f3(X0))|~program(X1)|halts2(X1,X2)|outputs(X0,bad))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f69])).
% 0.14/0.44  fof(f71,plain,(
% 0.14/0.44    (![W]: (~program(W)|program(f5(W))))|program(c2)),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f13])).
% 0.14/0.44  fof(f72,plain,(
% 0.14/0.44    ![X0]: (~program(X0)|program(f5(X0))|program(c2))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f71])).
% 0.14/0.44  fof(f73,plain,(
% 0.14/0.44    ![Y]: ((((![W]: (~program(W)|program(f5(W))))|~program(Y))|~halts2(Y,Y))|halts2(c2,Y))),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f14])).
% 0.14/0.44  fof(f74,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|program(f5(X0))|~program(X1)|~halts2(X1,X1)|halts2(c2,X1))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f73])).
% 0.14/0.44  fof(f75,plain,(
% 0.14/0.44    (![Y]: (((![W]: (~program(W)|program(f5(W))))|~program(Y))|~halts2(Y,Y)))|outputs(c2,good)),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f15])).
% 0.14/0.44  fof(f76,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|program(f5(X0))|~program(X1)|~halts2(X1,X1)|outputs(c2,good))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f75])).
% 0.14/0.44  fof(f77,plain,(
% 0.14/0.44    ![Y]: ((((![W]: (~program(W)|program(f5(W))))|~program(Y))|halts2(Y,Y))|halts2(c2,Y))),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f16])).
% 0.14/0.44  fof(f78,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|program(f5(X0))|~program(X1)|halts2(X1,X1)|halts2(c2,X1))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f77])).
% 0.14/0.44  fof(f79,plain,(
% 0.14/0.44    (![Y]: (((![W]: (~program(W)|program(f5(W))))|~program(Y))|halts2(Y,Y)))|outputs(c2,bad)),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f17])).
% 0.14/0.44  fof(f80,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|program(f5(X0))|~program(X1)|halts2(X1,X1)|outputs(c2,bad))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f79])).
% 0.14/0.44  fof(f81,plain,(
% 0.14/0.44    (![W]: (((~program(W)|halts2(f5(W),f5(W)))|~halts3(W,f5(W),f5(W)))|~outputs(W,bad)))|program(c2)),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f18])).
% 0.14/0.44  fof(f82,plain,(
% 0.14/0.44    ![X0]: (~program(X0)|halts2(f5(X0),f5(X0))|~halts3(X0,f5(X0),f5(X0))|~outputs(X0,bad)|program(c2))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f81])).
% 0.14/0.44  fof(f83,plain,(
% 0.14/0.44    ![Y]: ((((![W]: (((~program(W)|halts2(f5(W),f5(W)))|~halts3(W,f5(W),f5(W)))|~outputs(W,bad)))|~program(Y))|~halts2(Y,Y))|halts2(c2,Y))),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f19])).
% 0.14/0.44  fof(f84,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|halts2(f5(X0),f5(X0))|~halts3(X0,f5(X0),f5(X0))|~outputs(X0,bad)|~program(X1)|~halts2(X1,X1)|halts2(c2,X1))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f83])).
% 0.14/0.44  fof(f85,plain,(
% 0.14/0.44    (![Y]: (((![W]: (((~program(W)|halts2(f5(W),f5(W)))|~halts3(W,f5(W),f5(W)))|~outputs(W,bad)))|~program(Y))|~halts2(Y,Y)))|outputs(c2,good)),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f20])).
% 0.14/0.44  fof(f86,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|halts2(f5(X0),f5(X0))|~halts3(X0,f5(X0),f5(X0))|~outputs(X0,bad)|~program(X1)|~halts2(X1,X1)|outputs(c2,good))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f85])).
% 0.14/0.44  fof(f87,plain,(
% 0.14/0.44    ![Y]: ((((![W]: (((~program(W)|halts2(f5(W),f5(W)))|~halts3(W,f5(W),f5(W)))|~outputs(W,bad)))|~program(Y))|halts2(Y,Y))|halts2(c2,Y))),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f21])).
% 0.14/0.44  fof(f88,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|halts2(f5(X0),f5(X0))|~halts3(X0,f5(X0),f5(X0))|~outputs(X0,bad)|~program(X1)|halts2(X1,X1)|halts2(c2,X1))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f87])).
% 0.14/0.44  fof(f89,plain,(
% 0.14/0.44    (![Y]: (((![W]: (((~program(W)|halts2(f5(W),f5(W)))|~halts3(W,f5(W),f5(W)))|~outputs(W,bad)))|~program(Y))|halts2(Y,Y)))|outputs(c2,bad)),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f22])).
% 0.14/0.44  fof(f90,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|halts2(f5(X0),f5(X0))|~halts3(X0,f5(X0),f5(X0))|~outputs(X0,bad)|~program(X1)|halts2(X1,X1)|outputs(c2,bad))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f89])).
% 0.14/0.44  fof(f91,plain,(
% 0.14/0.44    (![W]: (((~program(W)|~halts3(W,f5(W),f5(W)))|~outputs(W,good))|~halts2(f5(W),f5(W))))|program(c2)),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f23])).
% 0.14/0.44  fof(f92,plain,(
% 0.14/0.44    ![X0]: (~program(X0)|~halts3(X0,f5(X0),f5(X0))|~outputs(X0,good)|~halts2(f5(X0),f5(X0))|program(c2))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f91])).
% 0.14/0.44  fof(f93,plain,(
% 0.14/0.44    ![Y]: ((((![W]: (((~program(W)|~halts3(W,f5(W),f5(W)))|~outputs(W,good))|~halts2(f5(W),f5(W))))|~program(Y))|~halts2(Y,Y))|halts2(c2,Y))),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f24])).
% 0.14/0.44  fof(f94,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|~halts3(X0,f5(X0),f5(X0))|~outputs(X0,good)|~halts2(f5(X0),f5(X0))|~program(X1)|~halts2(X1,X1)|halts2(c2,X1))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f93])).
% 0.14/0.44  fof(f95,plain,(
% 0.14/0.44    (![Y]: (((![W]: (((~program(W)|~halts3(W,f5(W),f5(W)))|~outputs(W,good))|~halts2(f5(W),f5(W))))|~program(Y))|~halts2(Y,Y)))|outputs(c2,good)),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f25])).
% 0.14/0.44  fof(f96,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|~halts3(X0,f5(X0),f5(X0))|~outputs(X0,good)|~halts2(f5(X0),f5(X0))|~program(X1)|~halts2(X1,X1)|outputs(c2,good))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f95])).
% 0.14/0.44  fof(f97,plain,(
% 0.14/0.44    ![Y]: ((((![W]: (((~program(W)|~halts3(W,f5(W),f5(W)))|~outputs(W,good))|~halts2(f5(W),f5(W))))|~program(Y))|halts2(Y,Y))|halts2(c2,Y))),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f26])).
% 0.14/0.44  fof(f98,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|~halts3(X0,f5(X0),f5(X0))|~outputs(X0,good)|~halts2(f5(X0),f5(X0))|~program(X1)|halts2(X1,X1)|halts2(c2,X1))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f97])).
% 0.14/0.44  fof(f99,plain,(
% 0.14/0.44    (![Y]: (((![W]: (((~program(W)|~halts3(W,f5(W),f5(W)))|~outputs(W,good))|~halts2(f5(W),f5(W))))|~program(Y))|halts2(Y,Y)))|outputs(c2,bad)),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f27])).
% 0.14/0.44  fof(f100,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|~halts3(X0,f5(X0),f5(X0))|~outputs(X0,good)|~halts2(f5(X0),f5(X0))|~program(X1)|halts2(X1,X1)|outputs(c2,bad))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f99])).
% 0.14/0.44  fof(f101,plain,(
% 0.14/0.44    (![W]: (((~program(W)|~halts3(W,f5(W),f5(W)))|~outputs(W,good))|~outputs(W,bad)))|program(c2)),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f28])).
% 0.14/0.44  fof(f102,plain,(
% 0.14/0.44    ![X0]: (~program(X0)|~halts3(X0,f5(X0),f5(X0))|~outputs(X0,good)|~outputs(X0,bad)|program(c2))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f101])).
% 0.14/0.44  fof(f103,plain,(
% 0.14/0.44    ![Y]: ((((![W]: (((~program(W)|~halts3(W,f5(W),f5(W)))|~outputs(W,good))|~outputs(W,bad)))|~program(Y))|~halts2(Y,Y))|halts2(c2,Y))),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f29])).
% 0.14/0.44  fof(f104,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|~halts3(X0,f5(X0),f5(X0))|~outputs(X0,good)|~outputs(X0,bad)|~program(X1)|~halts2(X1,X1)|halts2(c2,X1))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f103])).
% 0.14/0.44  fof(f105,plain,(
% 0.14/0.44    (![Y]: (((![W]: (((~program(W)|~halts3(W,f5(W),f5(W)))|~outputs(W,good))|~outputs(W,bad)))|~program(Y))|~halts2(Y,Y)))|outputs(c2,good)),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f30])).
% 0.14/0.44  fof(f106,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|~halts3(X0,f5(X0),f5(X0))|~outputs(X0,good)|~outputs(X0,bad)|~program(X1)|~halts2(X1,X1)|outputs(c2,good))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f105])).
% 0.14/0.44  fof(f107,plain,(
% 0.14/0.44    ![Y]: ((((![W]: (((~program(W)|~halts3(W,f5(W),f5(W)))|~outputs(W,good))|~outputs(W,bad)))|~program(Y))|halts2(Y,Y))|halts2(c2,Y))),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f31])).
% 0.14/0.44  fof(f108,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|~halts3(X0,f5(X0),f5(X0))|~outputs(X0,good)|~outputs(X0,bad)|~program(X1)|halts2(X1,X1)|halts2(c2,X1))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f107])).
% 0.14/0.44  fof(f109,plain,(
% 0.14/0.44    (![Y]: (((![W]: (((~program(W)|~halts3(W,f5(W),f5(W)))|~outputs(W,good))|~outputs(W,bad)))|~program(Y))|halts2(Y,Y)))|outputs(c2,bad)),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f32])).
% 0.14/0.44  fof(f110,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|~halts3(X0,f5(X0),f5(X0))|~outputs(X0,good)|~outputs(X0,bad)|~program(X1)|halts2(X1,X1)|outputs(c2,bad))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f109])).
% 0.14/0.44  fof(f111,plain,(
% 0.14/0.44    (![V]: (~program(V)|program(f6(V))))|program(c3)),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f33])).
% 0.14/0.44  fof(f112,plain,(
% 0.14/0.44    ![X0]: (~program(X0)|program(f6(X0))|program(c3))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f111])).
% 0.14/0.44  fof(f113,plain,(
% 0.14/0.44    ![Y]: ((((![V]: (~program(V)|program(f6(V))))|~program(Y))|~halts2(Y,Y))|~halts2(c3,Y))),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f34])).
% 0.14/0.44  fof(f114,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|program(f6(X0))|~program(X1)|~halts2(X1,X1)|~halts2(c3,X1))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f113])).
% 0.14/0.44  fof(f115,plain,(
% 0.14/0.44    ![Y]: ((((![V]: (~program(V)|program(f6(V))))|~program(Y))|halts2(Y,Y))|halts2(c3,Y))),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f35])).
% 0.14/0.44  fof(f116,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|program(f6(X0))|~program(X1)|halts2(X1,X1)|halts2(c3,X1))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f115])).
% 0.14/0.44  fof(f117,plain,(
% 0.14/0.44    (![Y]: (((![V]: (~program(V)|program(f6(V))))|~program(Y))|halts2(Y,Y)))|outputs(c3,bad)),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f36])).
% 0.14/0.44  fof(f118,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|program(f6(X0))|~program(X1)|halts2(X1,X1)|outputs(c3,bad))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f117])).
% 0.14/0.44  fof(f119,plain,(
% 0.14/0.44    (![V]: (((~program(V)|halts2(f6(V),f6(V)))|~halts2(V,f6(V)))|~outputs(V,bad)))|program(c3)),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f37])).
% 0.14/0.44  fof(f120,plain,(
% 0.14/0.44    ![X0]: (~program(X0)|halts2(f6(X0),f6(X0))|~halts2(X0,f6(X0))|~outputs(X0,bad)|program(c3))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f119])).
% 0.14/0.44  fof(f121,plain,(
% 0.14/0.44    ![Y]: ((((![V]: (((~program(V)|halts2(f6(V),f6(V)))|~halts2(V,f6(V)))|~outputs(V,bad)))|~program(Y))|~halts2(Y,Y))|~halts2(c3,Y))),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f38])).
% 0.14/0.44  fof(f122,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|halts2(f6(X0),f6(X0))|~halts2(X0,f6(X0))|~outputs(X0,bad)|~program(X1)|~halts2(X1,X1)|~halts2(c3,X1))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f121])).
% 0.14/0.44  fof(f123,plain,(
% 0.14/0.44    ![Y]: ((((![V]: (((~program(V)|halts2(f6(V),f6(V)))|~halts2(V,f6(V)))|~outputs(V,bad)))|~program(Y))|halts2(Y,Y))|halts2(c3,Y))),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f39])).
% 0.14/0.44  fof(f124,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|halts2(f6(X0),f6(X0))|~halts2(X0,f6(X0))|~outputs(X0,bad)|~program(X1)|halts2(X1,X1)|halts2(c3,X1))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f123])).
% 0.14/0.44  fof(f125,plain,(
% 0.14/0.44    (![Y]: (((![V]: (((~program(V)|halts2(f6(V),f6(V)))|~halts2(V,f6(V)))|~outputs(V,bad)))|~program(Y))|halts2(Y,Y)))|outputs(c3,bad)),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f40])).
% 0.14/0.44  fof(f126,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|halts2(f6(X0),f6(X0))|~halts2(X0,f6(X0))|~outputs(X0,bad)|~program(X1)|halts2(X1,X1)|outputs(c3,bad))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f125])).
% 0.14/0.44  fof(f127,plain,(
% 0.14/0.44    (![V]: (((~program(V)|~halts2(V,f6(V)))|~outputs(V,good))|~halts2(f6(V),f6(V))))|program(c3)),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f41])).
% 0.14/0.44  fof(f128,plain,(
% 0.14/0.44    ![X0]: (~program(X0)|~halts2(X0,f6(X0))|~outputs(X0,good)|~halts2(f6(X0),f6(X0))|program(c3))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f127])).
% 0.14/0.44  fof(f129,plain,(
% 0.14/0.44    ![Y]: ((((![V]: (((~program(V)|~halts2(V,f6(V)))|~outputs(V,good))|~halts2(f6(V),f6(V))))|~program(Y))|~halts2(Y,Y))|~halts2(c3,Y))),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f42])).
% 0.14/0.44  fof(f130,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|~halts2(X0,f6(X0))|~outputs(X0,good)|~halts2(f6(X0),f6(X0))|~program(X1)|~halts2(X1,X1)|~halts2(c3,X1))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f129])).
% 0.14/0.44  fof(f131,plain,(
% 0.14/0.44    ![Y]: ((((![V]: (((~program(V)|~halts2(V,f6(V)))|~outputs(V,good))|~halts2(f6(V),f6(V))))|~program(Y))|halts2(Y,Y))|halts2(c3,Y))),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f43])).
% 0.14/0.44  fof(f132,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|~halts2(X0,f6(X0))|~outputs(X0,good)|~halts2(f6(X0),f6(X0))|~program(X1)|halts2(X1,X1)|halts2(c3,X1))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f131])).
% 0.14/0.44  fof(f133,plain,(
% 0.14/0.44    (![Y]: (((![V]: (((~program(V)|~halts2(V,f6(V)))|~outputs(V,good))|~halts2(f6(V),f6(V))))|~program(Y))|halts2(Y,Y)))|outputs(c3,bad)),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f44])).
% 0.14/0.44  fof(f134,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|~halts2(X0,f6(X0))|~outputs(X0,good)|~halts2(f6(X0),f6(X0))|~program(X1)|halts2(X1,X1)|outputs(c3,bad))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f133])).
% 0.14/0.44  fof(f135,plain,(
% 0.14/0.44    (![V]: (((~program(V)|~halts2(V,f6(V)))|~outputs(V,good))|~outputs(V,bad)))|program(c3)),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f45])).
% 0.14/0.44  fof(f136,plain,(
% 0.14/0.44    ![X0]: (~program(X0)|~halts2(X0,f6(X0))|~outputs(X0,good)|~outputs(X0,bad)|program(c3))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f135])).
% 0.14/0.44  fof(f137,plain,(
% 0.14/0.44    ![Y]: ((((![V]: (((~program(V)|~halts2(V,f6(V)))|~outputs(V,good))|~outputs(V,bad)))|~program(Y))|~halts2(Y,Y))|~halts2(c3,Y))),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f46])).
% 0.14/0.44  fof(f138,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|~halts2(X0,f6(X0))|~outputs(X0,good)|~outputs(X0,bad)|~program(X1)|~halts2(X1,X1)|~halts2(c3,X1))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f137])).
% 0.14/0.44  fof(f139,plain,(
% 0.14/0.44    ![Y]: ((((![V]: (((~program(V)|~halts2(V,f6(V)))|~outputs(V,good))|~outputs(V,bad)))|~program(Y))|halts2(Y,Y))|halts2(c3,Y))),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f47])).
% 0.14/0.44  fof(f140,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|~halts2(X0,f6(X0))|~outputs(X0,good)|~outputs(X0,bad)|~program(X1)|halts2(X1,X1)|halts2(c3,X1))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f139])).
% 0.14/0.44  fof(f141,plain,(
% 0.14/0.44    (![Y]: (((![V]: (((~program(V)|~halts2(V,f6(V)))|~outputs(V,good))|~outputs(V,bad)))|~program(Y))|halts2(Y,Y)))|outputs(c3,bad)),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f48])).
% 0.14/0.44  fof(f142,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|~halts2(X0,f6(X0))|~outputs(X0,good)|~outputs(X0,bad)|~program(X1)|halts2(X1,X1)|outputs(c3,bad))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f141])).
% 0.14/0.44  fof(f143,plain,(
% 0.14/0.44    algorithm(c4)),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f49])).
% 0.14/0.44  fof(f144,plain,(
% 0.14/0.44    ![Y1]: (~program(Y1)|(![Z1]: decides(c4,Y1,Z1)))),
% 0.14/0.44    inference(miniscoping,[status(thm)],[f50])).
% 0.14/0.44  fof(f145,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|decides(c4,X0,X1))),
% 0.14/0.44    inference(cnf_transformation,[status(thm)],[f144])).
% 0.14/0.44  fof(f146,definition,(
% 0.14/0.44    ![X0]: (sQ0_spl <=> (~algorithm(X0)|program(f2(X0))))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f147,plain,(
% 0.14/0.44    ![X0]: (~algorithm(X0)|program(f2(X0))|~sQ0_spl)),
% 0.14/0.44    inference(component_clause,[status(thm)],[f146])).
% 0.14/0.44  fof(f149,definition,(
% 0.14/0.44    sQ1_spl <=> (program(c1))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f150,plain,(
% 0.14/0.44    program(c1)|~sQ1_spl),
% 0.14/0.44    inference(component_clause,[status(thm)],[f149])).
% 0.14/0.44  fof(f152,plain,(
% 0.14/0.44    sQ0_spl|sQ1_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f52,f146,f149])).
% 0.14/0.44  fof(f153,definition,(
% 0.14/0.44    ![X1,X2]: (sQ2_spl <=> (~program(X1)|decides(c1,X1,X2)))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f154,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|decides(c1,X0,X1)|~sQ2_spl)),
% 0.14/0.44    inference(component_clause,[status(thm)],[f153])).
% 0.14/0.44  fof(f156,plain,(
% 0.14/0.44    sQ0_spl|sQ2_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f54,f146,f153])).
% 0.14/0.44  fof(f157,definition,(
% 0.14/0.44    ![X0]: (sQ3_spl <=> (~algorithm(X0)|~decides(X0,f2(X0),f1(X0))))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f158,plain,(
% 0.14/0.44    ![X0]: (~algorithm(X0)|~decides(X0,f2(X0),f1(X0))|~sQ3_spl)),
% 0.14/0.44    inference(component_clause,[status(thm)],[f157])).
% 0.14/0.44  fof(f160,plain,(
% 0.14/0.44    sQ3_spl|sQ1_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f56,f157,f149])).
% 0.14/0.44  fof(f161,plain,(
% 0.14/0.44    sQ3_spl|sQ2_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f58,f157,f153])).
% 0.14/0.44  fof(f162,definition,(
% 0.14/0.44    ![X0]: (sQ4_spl <=> (~program(X0)|program(f4(X0))|outputs(X0,good)))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f163,plain,(
% 0.14/0.44    ![X0]: (~program(X0)|program(f4(X0))|outputs(X0,good)|~sQ4_spl)),
% 0.14/0.44    inference(component_clause,[status(thm)],[f162])).
% 0.14/0.44  fof(f165,definition,(
% 0.14/0.44    ![X1,X2]: (sQ5_spl <=> (~program(X1)|~halts2(X1,X2)))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f166,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|~halts2(X0,X1)|~sQ5_spl)),
% 0.14/0.44    inference(component_clause,[status(thm)],[f165])).
% 0.14/0.44  fof(f168,plain,(
% 0.14/0.44    sQ4_spl|sQ5_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f61,f162,f165])).
% 0.14/0.44  fof(f169,definition,(
% 0.14/0.44    ![X0]: (sQ6_spl <=> (~program(X0)|program(f4(X0))|outputs(X0,bad)))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f170,plain,(
% 0.14/0.44    ![X0]: (~program(X0)|program(f4(X0))|outputs(X0,bad)|~sQ6_spl)),
% 0.14/0.44    inference(component_clause,[status(thm)],[f169])).
% 0.14/0.44  fof(f172,definition,(
% 0.14/0.44    ![X1,X2]: (sQ7_spl <=> (~program(X1)|halts2(X1,X2)))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f173,plain,(
% 0.14/0.44    ![X0,X1]: (~program(X0)|halts2(X0,X1)|~sQ7_spl)),
% 0.14/0.44    inference(component_clause,[status(thm)],[f172])).
% 0.14/0.44  fof(f175,plain,(
% 0.14/0.44    sQ6_spl|sQ7_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f64,f169,f172])).
% 0.14/0.44  fof(f176,definition,(
% 0.14/0.44    ![X0]: (sQ8_spl <=> (~program(X0)|~decides(X0,f4(X0),f3(X0))|outputs(X0,good)))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f177,plain,(
% 0.14/0.44    ![X0]: (~program(X0)|~decides(X0,f4(X0),f3(X0))|outputs(X0,good)|~sQ8_spl)),
% 0.14/0.44    inference(component_clause,[status(thm)],[f176])).
% 0.14/0.44  fof(f179,plain,(
% 0.14/0.44    sQ8_spl|sQ5_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f67,f176,f165])).
% 0.14/0.44  fof(f180,definition,(
% 0.14/0.44    ![X0]: (sQ9_spl <=> (~program(X0)|~decides(X0,f4(X0),f3(X0))|outputs(X0,bad)))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f181,plain,(
% 0.14/0.44    ![X0]: (~program(X0)|~decides(X0,f4(X0),f3(X0))|outputs(X0,bad)|~sQ9_spl)),
% 0.14/0.44    inference(component_clause,[status(thm)],[f180])).
% 0.14/0.44  fof(f183,plain,(
% 0.14/0.44    sQ9_spl|sQ7_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f70,f180,f172])).
% 0.14/0.44  fof(f184,definition,(
% 0.14/0.44    ![X0]: (sQ10_spl <=> (~program(X0)|program(f5(X0))))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f185,plain,(
% 0.14/0.44    ![X0]: (~program(X0)|program(f5(X0))|~sQ10_spl)),
% 0.14/0.44    inference(component_clause,[status(thm)],[f184])).
% 0.14/0.44  fof(f187,definition,(
% 0.14/0.44    sQ11_spl <=> (program(c2))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f188,plain,(
% 0.14/0.44    program(c2)|~sQ11_spl),
% 0.14/0.44    inference(component_clause,[status(thm)],[f187])).
% 0.14/0.44  fof(f190,plain,(
% 0.14/0.44    sQ10_spl|sQ11_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f72,f184,f187])).
% 0.14/0.44  fof(f191,definition,(
% 0.14/0.44    ![X1]: (sQ12_spl <=> (~program(X1)|~halts2(X1,X1)|halts2(c2,X1)))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f192,plain,(
% 0.14/0.44    ![X0]: (~program(X0)|~halts2(X0,X0)|halts2(c2,X0)|~sQ12_spl)),
% 0.14/0.44    inference(component_clause,[status(thm)],[f191])).
% 0.14/0.44  fof(f194,plain,(
% 0.14/0.44    sQ10_spl|sQ12_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f74,f184,f191])).
% 0.14/0.44  fof(f195,definition,(
% 0.14/0.44    ![X1]: (sQ13_spl <=> (~program(X1)|~halts2(X1,X1)))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f196,plain,(
% 0.14/0.44    ![X0]: (~program(X0)|~halts2(X0,X0)|~sQ13_spl)),
% 0.14/0.44    inference(component_clause,[status(thm)],[f195])).
% 0.14/0.44  fof(f198,definition,(
% 0.14/0.44    sQ14_spl <=> (outputs(c2,good))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f199,plain,(
% 0.14/0.44    outputs(c2,good)|~sQ14_spl),
% 0.14/0.44    inference(component_clause,[status(thm)],[f198])).
% 0.14/0.44  fof(f200,plain,(
% 0.14/0.44    ~outputs(c2,good)|sQ14_spl),
% 0.14/0.44    inference(component_clause,[status(thm)],[f198])).
% 0.14/0.44  fof(f201,plain,(
% 0.14/0.44    sQ10_spl|sQ13_spl|sQ14_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f76,f184,f195,f198])).
% 0.14/0.44  fof(f202,definition,(
% 0.14/0.44    ![X1]: (sQ15_spl <=> (~program(X1)|halts2(X1,X1)|halts2(c2,X1)))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f203,plain,(
% 0.14/0.44    ![X0]: (~program(X0)|halts2(X0,X0)|halts2(c2,X0)|~sQ15_spl)),
% 0.14/0.44    inference(component_clause,[status(thm)],[f202])).
% 0.14/0.44  fof(f205,plain,(
% 0.14/0.44    sQ10_spl|sQ15_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f78,f184,f202])).
% 0.14/0.44  fof(f206,definition,(
% 0.14/0.44    ![X1]: (sQ16_spl <=> (~program(X1)|halts2(X1,X1)))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f207,plain,(
% 0.14/0.44    ![X0]: (~program(X0)|halts2(X0,X0)|~sQ16_spl)),
% 0.14/0.44    inference(component_clause,[status(thm)],[f206])).
% 0.14/0.44  fof(f209,definition,(
% 0.14/0.44    sQ17_spl <=> (outputs(c2,bad))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f210,plain,(
% 0.14/0.44    outputs(c2,bad)|~sQ17_spl),
% 0.14/0.44    inference(component_clause,[status(thm)],[f209])).
% 0.14/0.44  fof(f211,plain,(
% 0.14/0.44    ~outputs(c2,bad)|sQ17_spl),
% 0.14/0.44    inference(component_clause,[status(thm)],[f209])).
% 0.14/0.44  fof(f212,plain,(
% 0.14/0.44    sQ10_spl|sQ16_spl|sQ17_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f80,f184,f206,f209])).
% 0.14/0.44  fof(f213,definition,(
% 0.14/0.44    ![X0]: (sQ18_spl <=> (~program(X0)|halts2(f5(X0),f5(X0))|~halts3(X0,f5(X0),f5(X0))|~outputs(X0,bad)))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f214,plain,(
% 0.14/0.44    ![X0]: (~program(X0)|halts2(f5(X0),f5(X0))|~halts3(X0,f5(X0),f5(X0))|~outputs(X0,bad)|~sQ18_spl)),
% 0.14/0.44    inference(component_clause,[status(thm)],[f213])).
% 0.14/0.44  fof(f216,plain,(
% 0.14/0.44    sQ18_spl|sQ11_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f82,f213,f187])).
% 0.14/0.44  fof(f217,plain,(
% 0.14/0.44    sQ18_spl|sQ12_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f84,f213,f191])).
% 0.14/0.44  fof(f218,plain,(
% 0.14/0.44    sQ18_spl|sQ13_spl|sQ14_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f86,f213,f195,f198])).
% 0.14/0.44  fof(f219,plain,(
% 0.14/0.44    sQ18_spl|sQ15_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f88,f213,f202])).
% 0.14/0.44  fof(f220,plain,(
% 0.14/0.44    sQ18_spl|sQ16_spl|sQ17_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f90,f213,f206,f209])).
% 0.14/0.44  fof(f221,definition,(
% 0.14/0.44    ![X0]: (sQ19_spl <=> (~program(X0)|~halts3(X0,f5(X0),f5(X0))|~outputs(X0,good)|~halts2(f5(X0),f5(X0))))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f224,plain,(
% 0.14/0.44    sQ19_spl|sQ11_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f92,f221,f187])).
% 0.14/0.44  fof(f225,plain,(
% 0.14/0.44    sQ19_spl|sQ12_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f94,f221,f191])).
% 0.14/0.44  fof(f226,plain,(
% 0.14/0.44    sQ19_spl|sQ13_spl|sQ14_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f96,f221,f195,f198])).
% 0.14/0.44  fof(f227,plain,(
% 0.14/0.44    sQ19_spl|sQ15_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f98,f221,f202])).
% 0.14/0.44  fof(f228,plain,(
% 0.14/0.44    sQ19_spl|sQ16_spl|sQ17_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f100,f221,f206,f209])).
% 0.14/0.44  fof(f229,definition,(
% 0.14/0.44    ![X0]: (sQ20_spl <=> (~program(X0)|~halts3(X0,f5(X0),f5(X0))|~outputs(X0,good)|~outputs(X0,bad)))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f230,plain,(
% 0.14/0.44    ![X0]: (~program(X0)|~halts3(X0,f5(X0),f5(X0))|~outputs(X0,good)|~outputs(X0,bad)|~sQ20_spl)),
% 0.14/0.44    inference(component_clause,[status(thm)],[f229])).
% 0.14/0.44  fof(f232,plain,(
% 0.14/0.44    sQ20_spl|sQ11_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f102,f229,f187])).
% 0.14/0.44  fof(f233,plain,(
% 0.14/0.44    sQ20_spl|sQ12_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f104,f229,f191])).
% 0.14/0.44  fof(f234,plain,(
% 0.14/0.44    sQ20_spl|sQ13_spl|sQ14_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f106,f229,f195,f198])).
% 0.14/0.44  fof(f235,plain,(
% 0.14/0.44    sQ20_spl|sQ15_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f108,f229,f202])).
% 0.14/0.44  fof(f236,plain,(
% 0.14/0.44    sQ20_spl|sQ16_spl|sQ17_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f110,f229,f206,f209])).
% 0.14/0.44  fof(f237,definition,(
% 0.14/0.44    ![X0]: (sQ21_spl <=> (~program(X0)|program(f6(X0))))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f238,plain,(
% 0.14/0.44    ![X0]: (~program(X0)|program(f6(X0))|~sQ21_spl)),
% 0.14/0.44    inference(component_clause,[status(thm)],[f237])).
% 0.14/0.44  fof(f240,definition,(
% 0.14/0.44    sQ22_spl <=> (program(c3))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f241,plain,(
% 0.14/0.44    program(c3)|~sQ22_spl),
% 0.14/0.44    inference(component_clause,[status(thm)],[f240])).
% 0.14/0.44  fof(f243,plain,(
% 0.14/0.44    sQ21_spl|sQ22_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f112,f237,f240])).
% 0.14/0.44  fof(f244,definition,(
% 0.14/0.44    ![X1]: (sQ23_spl <=> (~program(X1)|~halts2(X1,X1)|~halts2(c3,X1)))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f245,plain,(
% 0.14/0.44    ![X0]: (~program(X0)|~halts2(X0,X0)|~halts2(c3,X0)|~sQ23_spl)),
% 0.14/0.44    inference(component_clause,[status(thm)],[f244])).
% 0.14/0.44  fof(f247,plain,(
% 0.14/0.44    sQ21_spl|sQ23_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f114,f237,f244])).
% 0.14/0.44  fof(f248,definition,(
% 0.14/0.44    ![X1]: (sQ24_spl <=> (~program(X1)|halts2(X1,X1)|halts2(c3,X1)))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f249,plain,(
% 0.14/0.44    ![X0]: (~program(X0)|halts2(X0,X0)|halts2(c3,X0)|~sQ24_spl)),
% 0.14/0.44    inference(component_clause,[status(thm)],[f248])).
% 0.14/0.44  fof(f251,plain,(
% 0.14/0.44    sQ21_spl|sQ24_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f116,f237,f248])).
% 0.14/0.44  fof(f252,definition,(
% 0.14/0.44    sQ25_spl <=> (outputs(c3,bad))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f253,plain,(
% 0.14/0.44    outputs(c3,bad)|~sQ25_spl),
% 0.14/0.44    inference(component_clause,[status(thm)],[f252])).
% 0.14/0.44  fof(f255,plain,(
% 0.14/0.44    sQ21_spl|sQ16_spl|sQ25_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f118,f237,f206,f252])).
% 0.14/0.44  fof(f256,definition,(
% 0.14/0.44    ![X0]: (sQ26_spl <=> (~program(X0)|halts2(f6(X0),f6(X0))|~halts2(X0,f6(X0))|~outputs(X0,bad)))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f257,plain,(
% 0.14/0.44    ![X0]: (~program(X0)|halts2(f6(X0),f6(X0))|~halts2(X0,f6(X0))|~outputs(X0,bad)|~sQ26_spl)),
% 0.14/0.44    inference(component_clause,[status(thm)],[f256])).
% 0.14/0.44  fof(f259,plain,(
% 0.14/0.44    sQ26_spl|sQ22_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f120,f256,f240])).
% 0.14/0.44  fof(f260,plain,(
% 0.14/0.44    sQ26_spl|sQ23_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f122,f256,f244])).
% 0.14/0.44  fof(f261,plain,(
% 0.14/0.44    sQ26_spl|sQ24_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f124,f256,f248])).
% 0.14/0.44  fof(f262,plain,(
% 0.14/0.44    sQ26_spl|sQ16_spl|sQ25_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f126,f256,f206,f252])).
% 0.14/0.44  fof(f263,definition,(
% 0.14/0.44    ![X0]: (sQ27_spl <=> (~program(X0)|~halts2(X0,f6(X0))|~outputs(X0,good)|~halts2(f6(X0),f6(X0))))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f264,plain,(
% 0.14/0.44    ![X0]: (~program(X0)|~halts2(X0,f6(X0))|~outputs(X0,good)|~halts2(f6(X0),f6(X0))|~sQ27_spl)),
% 0.14/0.44    inference(component_clause,[status(thm)],[f263])).
% 0.14/0.44  fof(f266,plain,(
% 0.14/0.44    sQ27_spl|sQ22_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f128,f263,f240])).
% 0.14/0.44  fof(f267,plain,(
% 0.14/0.44    sQ27_spl|sQ23_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f130,f263,f244])).
% 0.14/0.44  fof(f268,plain,(
% 0.14/0.44    sQ27_spl|sQ24_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f132,f263,f248])).
% 0.14/0.44  fof(f269,plain,(
% 0.14/0.44    sQ27_spl|sQ16_spl|sQ25_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f134,f263,f206,f252])).
% 0.14/0.44  fof(f270,definition,(
% 0.14/0.44    ![X0]: (sQ28_spl <=> (~program(X0)|~halts2(X0,f6(X0))|~outputs(X0,good)|~outputs(X0,bad)))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.14/0.44  fof(f271,plain,(
% 0.14/0.44    ![X0]: (~program(X0)|~halts2(X0,f6(X0))|~outputs(X0,good)|~outputs(X0,bad)|~sQ28_spl)),
% 0.14/0.44    inference(component_clause,[status(thm)],[f270])).
% 0.14/0.44  fof(f273,plain,(
% 0.14/0.44    sQ28_spl|sQ22_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f136,f270,f240])).
% 0.14/0.44  fof(f274,plain,(
% 0.14/0.44    sQ28_spl|sQ23_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f138,f270,f244])).
% 0.14/0.44  fof(f275,plain,(
% 0.14/0.44    sQ28_spl|sQ24_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f140,f270,f248])).
% 0.14/0.44  fof(f276,plain,(
% 0.14/0.44    sQ28_spl|sQ16_spl|sQ25_spl),
% 0.14/0.44    inference(split_clause,[status(thm)],[f142,f270,f206,f252])).
% 0.14/0.44  fof(f279,plain,(
% 0.14/0.44    program(f2(c4))|~sQ0_spl),
% 0.14/0.44    inference(resolution,[status(thm)],[f147,f143])).
% 0.14/0.44  fof(f285,plain,(
% 0.14/0.44    ![X0]: (decides(c4,f2(c4),X0)|~sQ0_spl)),
% 0.14/0.44    inference(resolution,[status(thm)],[f279,f145])).
% 0.14/0.44  fof(f290,plain,(
% 0.14/0.44    ~decides(c4,f2(c4),f1(c4))|~sQ3_spl),
% 0.14/0.44    inference(resolution,[status(thm)],[f158,f143])).
% 0.14/0.44  fof(f291,plain,(
% 0.14/0.44    $false|~sQ0_spl|~sQ3_spl),
% 0.14/0.44    inference(forward_subsumption_resolution,[status(thm)],[f290,f285])).
% 0.14/0.44  fof(f292,plain,(
% 0.14/0.44    ~sQ0_spl|~sQ3_spl),
% 0.14/0.44    inference(contradiction_clause,[status(thm)],[f291])).
% 0.14/0.44  fof(f293,plain,(
% 0.14/0.44    ![X0]: (~program(X0)|~sQ16_spl|~sQ13_spl)),
% 0.14/0.44    inference(forward_subsumption_resolution,[status(thm)],[f196,f207])).
% 0.14/0.44  fof(f294,plain,(
% 0.14/0.44    $false|~sQ16_spl|~sQ13_spl|~sQ22_spl),
% 0.14/0.44    inference(forward_subsumption_resolution,[status(thm)],[f241,f293])).
% 0.14/0.44  fof(f295,plain,(
% 0.14/0.44    ~sQ16_spl|~sQ13_spl|~sQ22_spl),
% 0.14/0.44    inference(contradiction_clause,[status(thm)],[f294])).
% 0.14/0.44  fof(f296,plain,(
% 0.14/0.44    ![X0]: (~program(X0)|halts2(c2,X0)|~sQ15_spl|~sQ12_spl)),
% 0.14/0.44    inference(forward_subsumption_resolution,[status(thm)],[f192,f203])).
% 0.14/0.44  fof(f298,plain,(
% 0.14/0.44    ![X0]: (~halts2(c2,X0)|~sQ5_spl|~sQ11_spl)),
% 0.14/0.44    inference(resolution,[status(thm)],[f166,f188])).
% 0.14/0.44  fof(f300,plain,(
% 0.14/0.44    program(f5(c1))|~sQ1_spl|~sQ10_spl),
% 0.14/0.44    inference(resolution,[status(thm)],[f150,f185])).
% 0.14/0.44  fof(f301,plain,(
% 0.14/0.44    ![X0]: (~halts2(c1,X0)|~sQ1_spl|~sQ5_spl)),
% 0.14/0.44    inference(resolution,[status(thm)],[f150,f166])).
% 0.14/0.44  fof(f304,plain,(
% 0.14/0.44    program(f6(c2))|~sQ21_spl|~sQ11_spl),
% 0.14/0.44    inference(resolution,[status(thm)],[f238,f188])).
% 0.14/0.44  fof(f306,plain,(
% 0.14/0.44    program(f5(c3))|~sQ22_spl|~sQ10_spl),
% 0.14/0.44    inference(resolution,[status(thm)],[f241,f185])).
% 0.14/0.44  fof(f309,plain,(
% 0.14/0.44    ![X0]: (~program(X0)|~sQ5_spl|~sQ11_spl|~sQ15_spl|~sQ12_spl)),
% 0.14/0.44    inference(backward_subsumption_resolution,[status(thm)],[f296,f298])).
% 0.14/0.44  fof(f310,plain,(
% 0.14/0.44    ~program(c1)|outputs(c1,bad)|~program(f4(c1))|~sQ9_spl|~sQ2_spl),
% 0.14/0.44    inference(resolution,[status(thm)],[f181,f154])).
% 0.14/0.44  fof(f311,definition,(
% 0.14/0.44    sQ29_spl <=> (outputs(c1,bad))),
% 0.14/0.44    introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f312,plain,(
% 0.14/0.45    outputs(c1,bad)|~sQ29_spl),
% 0.14/0.45    inference(component_clause,[status(thm)],[f311])).
% 0.14/0.45  fof(f314,definition,(
% 0.14/0.45    sQ30_spl <=> (program(f4(c1)))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f316,plain,(
% 0.14/0.45    ~program(f4(c1))|sQ30_spl),
% 0.14/0.45    inference(component_clause,[status(thm)],[f314])).
% 0.14/0.45  fof(f317,plain,(
% 0.14/0.45    ~sQ1_spl|sQ29_spl|~sQ30_spl|~sQ9_spl|~sQ2_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f310,f149,f311,f314,f180,f153])).
% 0.14/0.45  fof(f318,plain,(
% 0.14/0.45    ~program(c1)|outputs(c1,good)|~program(f4(c1))|~sQ8_spl|~sQ2_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f177,f154])).
% 0.14/0.45  fof(f319,definition,(
% 0.14/0.45    sQ31_spl <=> (outputs(c1,good))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f320,plain,(
% 0.14/0.45    outputs(c1,good)|~sQ31_spl),
% 0.14/0.45    inference(component_clause,[status(thm)],[f319])).
% 0.14/0.45  fof(f322,plain,(
% 0.14/0.45    ~sQ1_spl|sQ31_spl|~sQ30_spl|~sQ8_spl|~sQ2_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f318,f149,f319,f314,f176,f153])).
% 0.14/0.45  fof(f345,plain,(
% 0.14/0.45    ![X0,X1]: (~program(c1)|~program(X0)|halts2(X0,X1)|halts3(c1,X0,X1)|~program(f4(c1))|~sQ2_spl)),
% 0.14/0.45    inference(resolution,[status(thm)],[f68,f154])).
% 0.14/0.45  fof(f346,definition,(
% 0.14/0.45    ![X0,X1]: (sQ32_spl <=> (~program(X0)|halts2(X0,X1)|halts3(c1,X0,X1)))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f349,plain,(
% 0.14/0.45    ~sQ1_spl|sQ32_spl|~sQ30_spl|~sQ2_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f345,f149,f346,f314,f153])).
% 0.14/0.45  fof(f350,plain,(
% 0.14/0.45    ![X0,X1,X2]: (~program(X0)|~decides(X0,f4(X0),f3(X0))|~program(X1)|halts3(X0,X1,X2))),
% 0.14/0.45    inference(forward_subsumption_resolution,[status(thm)],[f65,f68])).
% 0.14/0.45  fof(f351,plain,(
% 0.14/0.45    ![X0,X1]: (~program(c1)|~program(X0)|halts3(c1,X0,X1)|~program(f4(c1))|~sQ2_spl)),
% 0.14/0.45    inference(resolution,[status(thm)],[f350,f154])).
% 0.14/0.45  fof(f352,definition,(
% 0.14/0.45    ![X0,X1]: (sQ33_spl <=> (~program(X0)|halts3(c1,X0,X1)))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f353,plain,(
% 0.14/0.45    ![X0,X1]: (~program(X0)|halts3(c1,X0,X1)|~sQ33_spl)),
% 0.14/0.45    inference(component_clause,[status(thm)],[f352])).
% 0.14/0.45  fof(f355,plain,(
% 0.14/0.45    ~sQ1_spl|sQ33_spl|~sQ30_spl|~sQ2_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f351,f149,f352,f314,f153])).
% 0.14/0.45  fof(f358,plain,(
% 0.14/0.45    $false|~sQ5_spl|~sQ11_spl|~sQ15_spl|~sQ12_spl|~sQ1_spl),
% 0.14/0.45    inference(backward_subsumption_resolution,[status(thm)],[f150,f309])).
% 0.14/0.45  fof(f360,plain,(
% 0.14/0.45    ~sQ5_spl|~sQ11_spl|~sQ15_spl|~sQ12_spl|~sQ1_spl),
% 0.14/0.45    inference(contradiction_clause,[status(thm)],[f358])).
% 0.14/0.45  fof(f362,plain,(
% 0.14/0.45    ![X0,X1,X2]: (~program(X0)|program(f4(X0))|~program(X1)|halts3(X0,X1,X2))),
% 0.14/0.45    inference(forward_subsumption_resolution,[status(thm)],[f62,f59])).
% 0.14/0.45  fof(f365,plain,(
% 0.14/0.45    halts2(c1,c1)|~sQ1_spl|~sQ16_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f150,f207])).
% 0.14/0.45  fof(f366,plain,(
% 0.14/0.45    program(f5(c1))|~sQ1_spl|~sQ10_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f150,f185])).
% 0.14/0.45  fof(f383,plain,(
% 0.14/0.45    ![X0]: (~program(X0)|~outputs(X0,good)|~halts2(f6(X0),f6(X0))|~sQ7_spl|~sQ27_spl)),
% 0.14/0.45    inference(backward_subsumption_resolution,[status(thm)],[f264,f173])).
% 0.14/0.45  fof(f385,plain,(
% 0.14/0.45    ![X0]: (~program(X0)|~outputs(X0,good)|~outputs(X0,bad)|~sQ7_spl|~sQ28_spl)),
% 0.14/0.45    inference(backward_subsumption_resolution,[status(thm)],[f271,f173])).
% 0.14/0.45  fof(f388,plain,(
% 0.14/0.45    ![X0]: (halts2(c1,X0)|~sQ7_spl|~sQ1_spl)),
% 0.14/0.45    inference(resolution,[status(thm)],[f173,f150])).
% 0.14/0.45  fof(f393,plain,(
% 0.14/0.45    ~program(c1)|~outputs(c1,bad)|~sQ7_spl|~sQ28_spl|~sQ31_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f385,f320])).
% 0.14/0.45  fof(f394,plain,(
% 0.14/0.45    ~program(c2)|~outputs(c2,bad)|~sQ7_spl|~sQ28_spl|~sQ14_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f385,f199])).
% 0.14/0.45  fof(f396,plain,(
% 0.14/0.45    ~sQ1_spl|~sQ29_spl|~sQ7_spl|~sQ28_spl|~sQ31_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f393,f149,f311,f172,f270,f319])).
% 0.14/0.45  fof(f397,plain,(
% 0.14/0.45    ~sQ11_spl|~sQ17_spl|~sQ7_spl|~sQ28_spl|~sQ14_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f394,f187,f209,f172,f270,f198])).
% 0.14/0.45  fof(f400,plain,(
% 0.14/0.45    ![X0]: (~program(X0)|~halts2(c3,X0)|~sQ7_spl|~sQ23_spl)),
% 0.14/0.45    inference(forward_subsumption_resolution,[status(thm)],[f245,f173])).
% 0.14/0.45  fof(f401,plain,(
% 0.14/0.45    ![X0]: (~program(X0)|~sQ7_spl|~sQ13_spl)),
% 0.14/0.45    inference(forward_subsumption_resolution,[status(thm)],[f196,f173])).
% 0.14/0.45  fof(f404,plain,(
% 0.14/0.45    $false|~sQ7_spl|~sQ13_spl|~sQ1_spl|~sQ10_spl),
% 0.14/0.45    inference(backward_subsumption_resolution,[status(thm)],[f300,f401])).
% 0.14/0.45  fof(f407,plain,(
% 0.14/0.45    ~sQ7_spl|~sQ13_spl|~sQ1_spl|~sQ10_spl),
% 0.14/0.45    inference(contradiction_clause,[status(thm)],[f404])).
% 0.14/0.45  fof(f417,definition,(
% 0.14/0.45    sQ34_spl <=> (program(c4))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f420,definition,(
% 0.14/0.45    sQ35_spl <=> (outputs(c4,good))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f429,definition,(
% 0.14/0.45    sQ36_spl <=> (outputs(c4,bad))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f431,plain,(
% 0.14/0.45    ~outputs(c4,bad)|sQ36_spl),
% 0.14/0.45    inference(component_clause,[status(thm)],[f429])).
% 0.14/0.45  fof(f437,plain,(
% 0.14/0.45    ![X0]: (~program(X0)|program(f4(X0))|~program(f5(X0))|~program(X0)|halts2(f5(X0),f5(X0))|~outputs(X0,bad)|~sQ18_spl)),
% 0.14/0.45    inference(resolution,[status(thm)],[f362,f214])).
% 0.14/0.45  fof(f438,plain,(
% 0.14/0.45    ![X0]: (~program(X0)|program(f4(X0))|~program(f5(X0))|halts2(f5(X0),f5(X0))|~outputs(X0,bad)|~sQ18_spl)),
% 0.14/0.45    inference(duplicate_literals_removal,[status(thm)],[f437])).
% 0.14/0.45  fof(f439,plain,(
% 0.14/0.45    ![X0]: (~program(X0)|program(f4(X0))|halts2(f5(X0),f5(X0))|~outputs(X0,bad)|~sQ10_spl|~sQ18_spl)),
% 0.14/0.45    inference(forward_subsumption_resolution,[status(thm)],[f438,f185])).
% 0.14/0.45  fof(f441,plain,(
% 0.14/0.45    ![X0]: (~program(f6(X0))|~program(X0)|~outputs(X0,good)|~sQ7_spl|~sQ27_spl)),
% 0.14/0.45    inference(resolution,[status(thm)],[f173,f383])).
% 0.14/0.45  fof(f442,plain,(
% 0.14/0.45    ![X0]: (~program(c3)|~program(X0)|~sQ7_spl|~sQ23_spl)),
% 0.14/0.45    inference(resolution,[status(thm)],[f173,f400])).
% 0.14/0.45  fof(f444,definition,(
% 0.14/0.45    ![X0]: (sQ37_spl <=> (~program(X0)))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f445,plain,(
% 0.14/0.45    ![X0]: (~program(X0)|~sQ37_spl)),
% 0.14/0.45    inference(component_clause,[status(thm)],[f444])).
% 0.14/0.45  fof(f447,plain,(
% 0.14/0.45    ~sQ22_spl|sQ37_spl|~sQ7_spl|~sQ23_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f442,f240,f444,f172,f244])).
% 0.14/0.45  fof(f448,plain,(
% 0.14/0.45    ~program(f5(c1))|~program(c1)|halts2(f5(c1),f5(c1))|~outputs(c1,bad)|~sQ33_spl|~sQ18_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f353,f214])).
% 0.14/0.45  fof(f449,definition,(
% 0.14/0.45    sQ38_spl <=> (program(f5(c1)))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f451,plain,(
% 0.14/0.45    ~program(f5(c1))|sQ38_spl),
% 0.14/0.45    inference(component_clause,[status(thm)],[f449])).
% 0.14/0.45  fof(f452,definition,(
% 0.14/0.45    sQ39_spl <=> (halts2(f5(c1),f5(c1)))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f453,plain,(
% 0.14/0.45    halts2(f5(c1),f5(c1))|~sQ39_spl),
% 0.14/0.45    inference(component_clause,[status(thm)],[f452])).
% 0.14/0.45  fof(f455,plain,(
% 0.14/0.45    ~sQ38_spl|~sQ1_spl|sQ39_spl|~sQ29_spl|~sQ33_spl|~sQ18_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f448,f449,f149,f452,f311,f352,f213])).
% 0.14/0.45  fof(f456,plain,(
% 0.14/0.45    $false|~sQ1_spl|~sQ10_spl|sQ38_spl),
% 0.14/0.45    inference(forward_subsumption_resolution,[status(thm)],[f451,f366])).
% 0.14/0.45  fof(f457,plain,(
% 0.14/0.45    ~sQ1_spl|~sQ10_spl|sQ38_spl),
% 0.14/0.45    inference(contradiction_clause,[status(thm)],[f456])).
% 0.14/0.45  fof(f459,plain,(
% 0.14/0.45    ~program(c3)|~halts3(c3,f5(c3),f5(c3))|~outputs(c3,good)|~sQ20_spl|~sQ25_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f230,f253])).
% 0.14/0.45  fof(f462,definition,(
% 0.14/0.45    sQ40_spl <=> (halts3(c3,f5(c3),f5(c3)))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f464,plain,(
% 0.14/0.45    ~halts3(c3,f5(c3),f5(c3))|sQ40_spl),
% 0.14/0.45    inference(component_clause,[status(thm)],[f462])).
% 0.14/0.45  fof(f465,definition,(
% 0.14/0.45    sQ41_spl <=> (outputs(c3,good))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f467,plain,(
% 0.14/0.45    ~outputs(c3,good)|sQ41_spl),
% 0.14/0.45    inference(component_clause,[status(thm)],[f465])).
% 0.14/0.45  fof(f468,plain,(
% 0.14/0.45    ~sQ22_spl|~sQ40_spl|~sQ41_spl|~sQ20_spl|~sQ25_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f459,f240,f462,f465,f229,f252])).
% 0.14/0.45  fof(f470,definition,(
% 0.14/0.45    sQ42_spl <=> (halts2(c1,c1))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f471,plain,(
% 0.14/0.45    halts2(c1,c1)|~sQ42_spl),
% 0.14/0.45    inference(component_clause,[status(thm)],[f470])).
% 0.14/0.45  fof(f473,definition,(
% 0.14/0.45    sQ43_spl <=> (halts2(c3,c1))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f474,plain,(
% 0.14/0.45    halts2(c3,c1)|~sQ43_spl),
% 0.14/0.45    inference(component_clause,[status(thm)],[f473])).
% 0.14/0.45  fof(f477,plain,(
% 0.14/0.45    $false|~sQ37_spl|~sQ1_spl),
% 0.14/0.45    inference(backward_subsumption_resolution,[status(thm)],[f150,f445])).
% 0.14/0.45  fof(f478,plain,(
% 0.14/0.45    ~sQ37_spl|~sQ1_spl),
% 0.14/0.45    inference(contradiction_clause,[status(thm)],[f477])).
% 0.14/0.45  fof(f500,plain,(
% 0.14/0.45    ~program(f6(c2))|~program(c2)|halts2(f6(c2),f6(c2))|~outputs(c2,bad)|~sQ15_spl|~sQ12_spl|~sQ26_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f296,f257])).
% 0.14/0.45  fof(f501,definition,(
% 0.14/0.45    sQ44_spl <=> (program(f6(c2)))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f503,plain,(
% 0.14/0.45    ~program(f6(c2))|sQ44_spl),
% 0.14/0.45    inference(component_clause,[status(thm)],[f501])).
% 0.14/0.45  fof(f504,definition,(
% 0.14/0.45    sQ45_spl <=> (halts2(f6(c2),f6(c2)))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f505,plain,(
% 0.14/0.45    halts2(f6(c2),f6(c2))|~sQ45_spl),
% 0.14/0.45    inference(component_clause,[status(thm)],[f504])).
% 0.14/0.45  fof(f507,plain,(
% 0.14/0.45    ~sQ44_spl|~sQ11_spl|sQ45_spl|~sQ17_spl|~sQ15_spl|~sQ12_spl|~sQ26_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f500,f501,f187,f504,f209,f202,f191,f256])).
% 0.14/0.45  fof(f511,plain,(
% 0.14/0.45    ~program(c3)|program(f4(c3))|sQ41_spl|~sQ4_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f467,f163])).
% 0.14/0.45  fof(f512,definition,(
% 0.14/0.45    sQ46_spl <=> (program(f4(c3)))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f515,plain,(
% 0.14/0.45    ~sQ22_spl|sQ46_spl|sQ41_spl|~sQ4_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f511,f240,f512,f465,f162])).
% 0.14/0.45  fof(f519,plain,(
% 0.14/0.45    ~program(c3)|program(f4(c3))|~program(f5(c3))|sQ40_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f464,f362])).
% 0.14/0.45  fof(f520,definition,(
% 0.14/0.45    sQ47_spl <=> (program(f5(c3)))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f522,plain,(
% 0.14/0.45    ~program(f5(c3))|sQ47_spl),
% 0.14/0.45    inference(component_clause,[status(thm)],[f520])).
% 0.14/0.45  fof(f523,plain,(
% 0.14/0.45    ~sQ22_spl|sQ46_spl|~sQ47_spl|sQ40_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f519,f240,f512,f520,f462])).
% 0.14/0.45  fof(f525,plain,(
% 0.14/0.45    ~program(c4)|program(f4(c4))|sQ36_spl|~sQ6_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f431,f170])).
% 0.14/0.45  fof(f526,definition,(
% 0.14/0.45    sQ48_spl <=> (program(f4(c4)))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f527,plain,(
% 0.14/0.45    program(f4(c4))|~sQ48_spl),
% 0.14/0.45    inference(component_clause,[status(thm)],[f526])).
% 0.14/0.45  fof(f529,plain,(
% 0.14/0.45    ~sQ34_spl|sQ48_spl|sQ36_spl|~sQ6_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f525,f417,f526,f429,f169])).
% 0.14/0.45  fof(f532,plain,(
% 0.14/0.45    ![X0]: (decides(c4,f4(c4),X0)|~sQ48_spl)),
% 0.14/0.45    inference(resolution,[status(thm)],[f527,f145])).
% 0.14/0.45  fof(f536,plain,(
% 0.14/0.45    ~program(c4)|outputs(c4,good)|~sQ48_spl|~sQ8_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f532,f177])).
% 0.14/0.45  fof(f537,plain,(
% 0.14/0.45    ![X0,X1]: (~program(c4)|~program(X0)|halts3(c4,X0,X1)|~sQ48_spl)),
% 0.14/0.45    inference(resolution,[status(thm)],[f532,f350])).
% 0.14/0.45  fof(f538,plain,(
% 0.14/0.45    ~program(c4)|outputs(c4,bad)|~sQ48_spl|~sQ9_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f532,f181])).
% 0.14/0.45  fof(f539,plain,(
% 0.14/0.45    ~sQ34_spl|sQ35_spl|~sQ48_spl|~sQ8_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f536,f417,f420,f526,f176])).
% 0.14/0.45  fof(f540,definition,(
% 0.14/0.45    ![X0,X1]: (sQ49_spl <=> (~program(X0)|halts3(c4,X0,X1)))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f541,plain,(
% 0.14/0.45    ![X0,X1]: (~program(X0)|halts3(c4,X0,X1)|~sQ49_spl)),
% 0.14/0.45    inference(component_clause,[status(thm)],[f540])).
% 0.14/0.45  fof(f543,plain,(
% 0.14/0.45    ~sQ34_spl|sQ49_spl|~sQ48_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f537,f417,f540,f526])).
% 0.14/0.45  fof(f544,plain,(
% 0.14/0.45    ~sQ34_spl|sQ36_spl|~sQ48_spl|~sQ9_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f538,f417,f429,f526,f180])).
% 0.14/0.45  fof(f545,plain,(
% 0.14/0.45    ![X0]: (~program(X0)|~halts3(X0,f5(X0),f5(X0))|~outputs(X0,good)|~program(X0)|program(f4(X0))|~sQ20_spl|~sQ6_spl)),
% 0.14/0.45    inference(resolution,[status(thm)],[f230,f170])).
% 0.14/0.45  fof(f546,plain,(
% 0.14/0.45    ![X0]: (~program(X0)|~halts3(X0,f5(X0),f5(X0))|~outputs(X0,good)|program(f4(X0))|~sQ20_spl|~sQ6_spl)),
% 0.14/0.45    inference(duplicate_literals_removal,[status(thm)],[f545])).
% 0.14/0.45  fof(f547,plain,(
% 0.14/0.45    ![X0]: (~program(X0)|~halts3(X0,f5(X0),f5(X0))|program(f4(X0))|~sQ4_spl|~sQ20_spl|~sQ6_spl)),
% 0.14/0.45    inference(forward_subsumption_resolution,[status(thm)],[f546,f163])).
% 0.14/0.45  fof(f550,definition,(
% 0.14/0.45    sQ50_spl <=> (program(f5(c4)))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f561,plain,(
% 0.14/0.45    ~program(c3)|halts2(f6(c3),f6(c3))|~halts2(c3,f6(c3))|~sQ25_spl|~sQ26_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f253,f257])).
% 0.14/0.45  fof(f563,definition,(
% 0.14/0.45    sQ51_spl <=> (halts2(f6(c3),f6(c3)))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f566,definition,(
% 0.14/0.45    sQ52_spl <=> (halts2(c3,f6(c3)))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f569,plain,(
% 0.14/0.45    ~sQ22_spl|sQ51_spl|~sQ52_spl|~sQ25_spl|~sQ26_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f561,f240,f563,f566,f252,f256])).
% 0.14/0.45  fof(f576,plain,(
% 0.14/0.45    ~program(c2)|~halts2(c2,f6(c2))|~outputs(c2,good)|~sQ45_spl|~sQ27_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f505,f264])).
% 0.14/0.45  fof(f577,definition,(
% 0.14/0.45    sQ53_spl <=> (halts2(c2,f6(c2)))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f579,plain,(
% 0.14/0.45    ~halts2(c2,f6(c2))|sQ53_spl),
% 0.14/0.45    inference(component_clause,[status(thm)],[f577])).
% 0.14/0.45  fof(f580,plain,(
% 0.14/0.45    ~sQ11_spl|~sQ53_spl|~sQ14_spl|~sQ45_spl|~sQ27_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f576,f187,f577,f198,f504,f263])).
% 0.14/0.45  fof(f581,plain,(
% 0.14/0.45    $false|~sQ21_spl|~sQ11_spl|sQ44_spl),
% 0.14/0.45    inference(forward_subsumption_resolution,[status(thm)],[f503,f304])).
% 0.14/0.45  fof(f582,plain,(
% 0.14/0.45    ~sQ21_spl|~sQ11_spl|sQ44_spl),
% 0.14/0.45    inference(contradiction_clause,[status(thm)],[f581])).
% 0.14/0.45  fof(f590,plain,(
% 0.14/0.45    halts2(c3,c3)|halts2(c3,c3)|~sQ24_spl|~sQ22_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f249,f241])).
% 0.14/0.45  fof(f592,plain,(
% 0.14/0.45    halts2(c2,c2)|halts2(c3,c2)|~sQ24_spl|~sQ11_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f249,f188])).
% 0.14/0.45  fof(f600,definition,(
% 0.14/0.45    sQ56_spl <=> (halts2(c3,c3))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f601,plain,(
% 0.14/0.45    halts2(c3,c3)|~sQ56_spl),
% 0.14/0.45    inference(component_clause,[status(thm)],[f600])).
% 0.14/0.45  fof(f603,plain,(
% 0.14/0.45    sQ56_spl|~sQ24_spl|~sQ22_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f590,f600,f248,f240])).
% 0.14/0.45  fof(f605,definition,(
% 0.14/0.45    sQ57_spl <=> (halts2(c2,c2))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f606,plain,(
% 0.14/0.45    halts2(c2,c2)|~sQ57_spl),
% 0.14/0.45    inference(component_clause,[status(thm)],[f605])).
% 0.14/0.45  fof(f608,definition,(
% 0.14/0.45    sQ58_spl <=> (halts2(c3,c2))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f609,plain,(
% 0.14/0.45    halts2(c3,c2)|~sQ58_spl),
% 0.14/0.45    inference(component_clause,[status(thm)],[f608])).
% 0.14/0.45  fof(f611,plain,(
% 0.14/0.45    sQ57_spl|sQ58_spl|~sQ24_spl|~sQ11_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f592,f605,f608,f248,f187])).
% 0.14/0.45  fof(f612,plain,(
% 0.14/0.45    ~program(c1)|~halts2(c1,c1)|~sQ23_spl|~sQ43_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f245,f474])).
% 0.14/0.45  fof(f613,plain,(
% 0.14/0.45    ~sQ1_spl|~sQ42_spl|~sQ23_spl|~sQ43_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f612,f149,f470,f244,f473])).
% 0.14/0.45  fof(f620,plain,(
% 0.14/0.45    ~program(c2)|halts2(f6(c2),f6(c2))|~halts2(c2,f6(c2))|~sQ17_spl|~sQ26_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f210,f257])).
% 0.14/0.45  fof(f621,plain,(
% 0.14/0.45    ~sQ11_spl|sQ45_spl|~sQ53_spl|~sQ17_spl|~sQ26_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f620,f187,f504,f577,f209,f256])).
% 0.14/0.45  fof(f632,plain,(
% 0.14/0.45    ~program(c3)|~halts2(c3,c3)|~sQ56_spl|~sQ23_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f601,f245])).
% 0.14/0.45  fof(f633,plain,(
% 0.14/0.45    ~sQ22_spl|~sQ56_spl|~sQ23_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f632,f240,f600,f244])).
% 0.14/0.45  fof(f637,plain,(
% 0.14/0.45    ~halts2(c3,c3)|~sQ13_spl|~sQ22_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f196,f241])).
% 0.14/0.45  fof(f640,plain,(
% 0.14/0.45    $false|~sQ56_spl|~sQ13_spl|~sQ22_spl),
% 0.14/0.45    inference(forward_subsumption_resolution,[status(thm)],[f637,f601])).
% 0.14/0.45  fof(f641,plain,(
% 0.14/0.45    ~sQ56_spl|~sQ13_spl|~sQ22_spl),
% 0.14/0.45    inference(contradiction_clause,[status(thm)],[f640])).
% 0.14/0.45  fof(f643,plain,(
% 0.14/0.45    ~program(c2)|~outputs(c2,good)|~outputs(c2,bad)|~program(f6(c2))|~sQ28_spl|~sQ15_spl|~sQ12_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f271,f296])).
% 0.14/0.45  fof(f644,plain,(
% 0.14/0.45    ~sQ11_spl|~sQ14_spl|~sQ17_spl|~sQ44_spl|~sQ28_spl|~sQ15_spl|~sQ12_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f643,f187,f198,f209,f501,f270,f202,f191])).
% 0.14/0.45  fof(f645,plain,(
% 0.14/0.45    ~program(c2)|program(f4(c2))|sQ14_spl|~sQ4_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f200,f163])).
% 0.14/0.45  fof(f646,definition,(
% 0.14/0.45    sQ59_spl <=> (program(f4(c2)))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f649,plain,(
% 0.14/0.45    ~sQ11_spl|sQ59_spl|sQ14_spl|~sQ4_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f645,f187,f646,f198,f162])).
% 0.14/0.45  fof(f650,plain,(
% 0.14/0.45    sQ42_spl|~sQ1_spl|~sQ16_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f365,f470,f149,f206])).
% 0.14/0.45  fof(f651,plain,(
% 0.14/0.45    ![X0]: (~program(X0)|~outputs(X0,good)|~sQ21_spl|~sQ7_spl|~sQ27_spl)),
% 0.14/0.45    inference(forward_subsumption_resolution,[status(thm)],[f441,f238])).
% 0.14/0.45  fof(f653,plain,(
% 0.14/0.45    ![X0]: (~program(f6(X0))|~program(X0)|~halts2(X0,f6(X0))|~outputs(X0,good)|~sQ16_spl|~sQ27_spl)),
% 0.14/0.45    inference(resolution,[status(thm)],[f207,f264])).
% 0.14/0.45  fof(f654,plain,(
% 0.14/0.45    ![X0]: (~program(X0)|~halts2(X0,f6(X0))|~outputs(X0,good)|~sQ21_spl|~sQ16_spl|~sQ27_spl)),
% 0.14/0.45    inference(forward_subsumption_resolution,[status(thm)],[f653,f238])).
% 0.14/0.45  fof(f669,plain,(
% 0.14/0.45    ![X0]: (~program(X0)|~decides(X0,f4(X0),f3(X0))|~sQ21_spl|~sQ7_spl|~sQ27_spl|~sQ8_spl)),
% 0.14/0.45    inference(backward_subsumption_resolution,[status(thm)],[f177,f651])).
% 0.14/0.45  fof(f670,plain,(
% 0.14/0.45    ![X0]: (~program(X0)|program(f4(X0))|~sQ21_spl|~sQ7_spl|~sQ27_spl|~sQ4_spl)),
% 0.14/0.45    inference(backward_subsumption_resolution,[status(thm)],[f163,f651])).
% 0.14/0.45  fof(f675,plain,(
% 0.14/0.45    ~program(c2)|~program(c2)|~sQ13_spl|~sQ15_spl|~sQ12_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f196,f296])).
% 0.14/0.45  fof(f676,plain,(
% 0.14/0.45    ~sQ11_spl|~sQ13_spl|~sQ15_spl|~sQ12_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f675,f187,f195,f202,f191])).
% 0.14/0.45  fof(f687,plain,(
% 0.14/0.45    ~program(c2)|program(f4(c2))|sQ17_spl|~sQ6_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f211,f170])).
% 0.14/0.45  fof(f688,plain,(
% 0.14/0.45    ~sQ11_spl|sQ59_spl|sQ17_spl|~sQ6_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f687,f187,f646,f209,f169])).
% 0.14/0.45  fof(f689,plain,(
% 0.14/0.45    ~program(c1)|halts2(f6(c1),f6(c1))|~halts2(c1,f6(c1))|~sQ29_spl|~sQ26_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f312,f257])).
% 0.14/0.45  fof(f690,plain,(
% 0.14/0.45    ~program(c1)|~halts2(c1,f6(c1))|~outputs(c1,good)|~sQ29_spl|~sQ28_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f312,f271])).
% 0.14/0.45  fof(f691,definition,(
% 0.14/0.45    sQ60_spl <=> (halts2(f6(c1),f6(c1)))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f694,definition,(
% 0.14/0.45    sQ61_spl <=> (halts2(c1,f6(c1)))),
% 0.14/0.45    introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.14/0.45  fof(f697,plain,(
% 0.14/0.45    ~sQ1_spl|sQ60_spl|~sQ61_spl|~sQ29_spl|~sQ26_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f689,f149,f691,f694,f311,f256])).
% 0.14/0.45  fof(f698,plain,(
% 0.14/0.45    ~sQ1_spl|~sQ61_spl|~sQ31_spl|~sQ29_spl|~sQ28_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f690,f149,f694,f319,f311,f270])).
% 0.14/0.45  fof(f704,plain,(
% 0.14/0.45    ~program(f6(c2))|sQ53_spl|~sQ15_spl|~sQ12_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f579,f296])).
% 0.14/0.45  fof(f705,plain,(
% 0.14/0.45    ~sQ44_spl|sQ53_spl|~sQ15_spl|~sQ12_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f704,f501,f577,f202,f191])).
% 0.14/0.45  fof(f706,plain,(
% 0.14/0.45    ~program(c2)|~outputs(c2,good)|~program(f6(c2))|~sQ21_spl|~sQ16_spl|~sQ27_spl|~sQ15_spl|~sQ12_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f654,f296])).
% 0.14/0.45  fof(f707,plain,(
% 0.14/0.45    ~sQ11_spl|~sQ14_spl|~sQ44_spl|~sQ21_spl|~sQ16_spl|~sQ27_spl|~sQ15_spl|~sQ12_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f706,f187,f198,f501,f237,f206,f263,f202,f191])).
% 0.14/0.45  fof(f708,plain,(
% 0.14/0.45    $false|sQ47_spl|~sQ22_spl|~sQ10_spl),
% 0.14/0.45    inference(forward_subsumption_resolution,[status(thm)],[f306,f522])).
% 0.14/0.45  fof(f709,plain,(
% 0.14/0.45    sQ47_spl|~sQ22_spl|~sQ10_spl),
% 0.14/0.45    inference(contradiction_clause,[status(thm)],[f708])).
% 0.14/0.45  fof(f710,plain,(
% 0.14/0.45    ![X0]: (~program(X0)|program(f4(X0))|halts2(f5(X0),f5(X0))|~sQ6_spl|~sQ10_spl|~sQ18_spl)),
% 0.14/0.45    inference(forward_subsumption_resolution,[status(thm)],[f439,f170])).
% 0.14/0.45  fof(f721,plain,(
% 0.14/0.45    ![X0]: (~program(X0)|program(f4(X0))|~program(X0)|program(f4(X0))|~program(f5(X0))|~sQ4_spl|~sQ20_spl|~sQ6_spl)),
% 0.14/0.45    inference(resolution,[status(thm)],[f547,f362])).
% 0.14/0.45  fof(f722,plain,(
% 0.14/0.45    ![X0]: (~program(X0)|program(f4(X0))|~program(f5(X0))|~sQ4_spl|~sQ20_spl|~sQ6_spl)),
% 0.14/0.45    inference(duplicate_literals_removal,[status(thm)],[f721])).
% 0.14/0.45  fof(f723,plain,(
% 0.14/0.45    ![X0]: (~program(X0)|program(f4(X0))|~sQ10_spl|~sQ4_spl|~sQ20_spl|~sQ6_spl)),
% 0.14/0.45    inference(forward_subsumption_resolution,[status(thm)],[f722,f185])).
% 0.14/0.45  fof(f729,plain,(
% 0.14/0.45    ~program(c1)|~sQ10_spl|~sQ4_spl|~sQ20_spl|~sQ6_spl|sQ30_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f723,f316])).
% 0.14/0.45  fof(f731,plain,(
% 0.14/0.45    $false|~sQ1_spl|~sQ10_spl|~sQ4_spl|~sQ20_spl|~sQ6_spl|sQ30_spl),
% 0.14/0.45    inference(forward_subsumption_resolution,[status(thm)],[f729,f150])).
% 0.14/0.45  fof(f732,plain,(
% 0.14/0.45    ~sQ1_spl|~sQ10_spl|~sQ4_spl|~sQ20_spl|~sQ6_spl|sQ30_spl),
% 0.14/0.45    inference(contradiction_clause,[status(thm)],[f731])).
% 0.14/0.45  fof(f736,plain,(
% 0.14/0.45    ~program(c3)|~sQ5_spl|~sQ58_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f166,f609])).
% 0.14/0.45  fof(f737,plain,(
% 0.14/0.45    ~program(c2)|~sQ5_spl|~sQ57_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f166,f606])).
% 0.14/0.45  fof(f746,plain,(
% 0.14/0.45    ![X0]: (~program(X0)|program(f4(X0))|~program(f5(X0))|~sQ6_spl|~sQ10_spl|~sQ18_spl|~sQ5_spl)),
% 0.14/0.45    inference(resolution,[status(thm)],[f710,f166])).
% 0.14/0.45  fof(f748,plain,(
% 0.14/0.45    ![X0]: (~program(X0)|program(f4(X0))|~sQ6_spl|~sQ10_spl|~sQ18_spl|~sQ5_spl)),
% 0.14/0.45    inference(forward_subsumption_resolution,[status(thm)],[f746,f185])).
% 0.14/0.45  fof(f749,plain,(
% 0.14/0.45    ~program(c1)|~sQ6_spl|~sQ10_spl|~sQ18_spl|~sQ5_spl|sQ30_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f748,f316])).
% 0.14/0.45  fof(f751,plain,(
% 0.14/0.45    $false|~sQ1_spl|~sQ6_spl|~sQ10_spl|~sQ18_spl|~sQ5_spl|sQ30_spl),
% 0.14/0.45    inference(forward_subsumption_resolution,[status(thm)],[f749,f150])).
% 0.14/0.45  fof(f752,plain,(
% 0.14/0.45    ~sQ1_spl|~sQ6_spl|~sQ10_spl|~sQ18_spl|~sQ5_spl|sQ30_spl),
% 0.14/0.45    inference(contradiction_clause,[status(thm)],[f751])).
% 0.14/0.45  fof(f753,plain,(
% 0.14/0.45    ~sQ11_spl|~sQ5_spl|~sQ57_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f737,f187,f165,f605])).
% 0.14/0.45  fof(f754,plain,(
% 0.14/0.45    ~sQ22_spl|~sQ5_spl|~sQ58_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f736,f240,f165,f608])).
% 0.14/0.45  fof(f755,plain,(
% 0.14/0.45    $false|~sQ1_spl|~sQ5_spl|~sQ42_spl),
% 0.14/0.45    inference(forward_subsumption_resolution,[status(thm)],[f471,f301])).
% 0.14/0.45  fof(f756,plain,(
% 0.14/0.45    ~sQ1_spl|~sQ5_spl|~sQ42_spl),
% 0.14/0.45    inference(contradiction_clause,[status(thm)],[f755])).
% 0.14/0.45  fof(f766,plain,(
% 0.14/0.45    ![X0,X1]: (~program(X0)|decides(c4,f4(X0),X1)|~sQ21_spl|~sQ7_spl|~sQ27_spl|~sQ4_spl)),
% 0.14/0.45    inference(resolution,[status(thm)],[f670,f145])).
% 0.14/0.45  fof(f769,plain,(
% 0.14/0.45    ~program(c1)|~program(f4(c1))|~sQ21_spl|~sQ7_spl|~sQ27_spl|~sQ8_spl|~sQ2_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f669,f154])).
% 0.14/0.45  fof(f770,plain,(
% 0.14/0.45    ~program(c4)|~program(c4)|~sQ8_spl|~sQ21_spl|~sQ7_spl|~sQ27_spl|~sQ4_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f669,f766])).
% 0.14/0.45  fof(f771,plain,(
% 0.14/0.45    ~sQ1_spl|~sQ30_spl|~sQ21_spl|~sQ7_spl|~sQ27_spl|~sQ8_spl|~sQ2_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f769,f149,f314,f237,f172,f263,f176,f153])).
% 0.14/0.45  fof(f772,plain,(
% 0.14/0.45    ~sQ34_spl|~sQ8_spl|~sQ21_spl|~sQ7_spl|~sQ27_spl|~sQ4_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f770,f417,f176,f237,f172,f263,f162])).
% 0.14/0.45  fof(f802,plain,(
% 0.14/0.45    ~program(f5(c1))|~program(c1)|~outputs(c1,good)|~outputs(c1,bad)|~sQ33_spl|~sQ20_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f353,f230])).
% 0.14/0.45  fof(f804,plain,(
% 0.14/0.45    ~sQ38_spl|~sQ1_spl|~sQ31_spl|~sQ29_spl|~sQ33_spl|~sQ20_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f802,f449,f149,f319,f311,f352,f229])).
% 0.14/0.45  fof(f807,plain,(
% 0.14/0.45    ~program(f5(c1))|~sQ39_spl|~sQ5_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f453,f166])).
% 0.14/0.45  fof(f812,plain,(
% 0.14/0.45    ~sQ38_spl|~sQ39_spl|~sQ5_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f807,f449,f452,f165])).
% 0.14/0.45  fof(f815,plain,(
% 0.14/0.45    ~program(f5(c4))|~program(c4)|~outputs(c4,good)|~outputs(c4,bad)|~sQ49_spl|~sQ20_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f541,f230])).
% 0.14/0.45  fof(f817,plain,(
% 0.14/0.45    ~sQ50_spl|~sQ34_spl|~sQ35_spl|~sQ36_spl|~sQ49_spl|~sQ20_spl),
% 0.14/0.45    inference(split_clause,[status(thm)],[f815,f550,f417,f420,f429,f540,f229])).
% 0.14/0.45  fof(f842,plain,(
% 0.14/0.45    ~program(c1)|sQ30_spl|~sQ21_spl|~sQ7_spl|~sQ27_spl|~sQ4_spl),
% 0.14/0.45    inference(resolution,[status(thm)],[f316,f670])).
% 0.14/0.45  fof(f843,plain,(
% 0.14/0.45    $false|~sQ1_spl|sQ30_spl|~sQ21_spl|~sQ7_spl|~sQ27_spl|~sQ4_spl),
% 0.14/0.45    inference(forward_subsumption_resolution,[status(thm)],[f842,f150])).
% 0.14/0.45  fof(f844,plain,(
% 0.14/0.45    ~sQ1_spl|sQ30_spl|~sQ21_spl|~sQ7_spl|~sQ27_spl|~sQ4_spl),
% 0.14/0.45    inference(contradiction_clause,[status(thm)],[f843])).
% 0.14/0.45  fof(f846,plain,(
% 0.14/0.45    $false|~sQ7_spl|~sQ1_spl|~sQ5_spl),
% 0.14/0.45    inference(forward_subsumption_resolution,[status(thm)],[f301,f388])).
% 0.14/0.45  fof(f847,plain,(
% 0.14/0.45    ~sQ7_spl|~sQ1_spl|~sQ5_spl),
% 0.14/0.45    inference(contradiction_clause,[status(thm)],[f846])).
% 0.14/0.45  fof(f848,plain,(
% 0.14/0.45    $false),
% 0.14/0.45    inference(sat_refutation,[status(thm)],[f152,f156,f160,f161,f168,f175,f179,f183,f190,f194,f201,f205,f212,f216,f217,f218,f219,f220,f224,f225,f226,f227,f228,f232,f233,f234,f235,f236,f243,f247,f251,f255,f259,f260,f261,f262,f266,f267,f268,f269,f273,f274,f275,f276,f292,f295,f317,f322,f349,f355,f360,f396,f397,f407,f447,f455,f457,f468,f478,f507,f515,f523,f529,f539,f543,f544,f569,f580,f582,f603,f611,f613,f621,f633,f641,f644,f649,f650,f676,f688,f697,f698,f705,f707,f709,f732,f752,f753,f754,f756,f771,f772,f804,f812,f817,f844,f847])).
% 0.14/0.45  % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.47  % Elapsed time: 0.101680 seconds
% 0.14/0.47  % CPU time: 0.558500 seconds
% 0.14/0.47  % Total memory used: 28.750 MB
% 0.14/0.47  % Net memory used: 28.340 MB
%------------------------------------------------------------------------------