%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : COM003+2 : TPTP v8.1.2. Bugfixed v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:17:41 EDT 2024
% Result : Theorem 1.59s 1.81s
% Output : Refutation 1.59s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : COM003+2 : TPTP v8.1.2. Bugfixed v2.2.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n012.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 9 07:12:38 EDT 2024
% 0.13/0.34 % CPUTime :
% 1.59/1.81 % Version: 1.5
% 1.59/1.81 % SZS status Theorem
% 1.59/1.81 % SZS output start CNFRefutation
% 1.59/1.81 fof(program_program_decides_def,axiom,(![X]:(program_program_decides(X)<=>(program(X)&program_decides(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', program_program_decides_def)).
% 1.59/1.81 fof(c109,plain,(![X]:((~program_program_decides(X)|(program(X)&program_decides(X)))&((~program(X)|~program_decides(X))|program_program_decides(X)))),inference(fof_nnf,[status(thm)],[program_program_decides_def])).
% 1.59/1.81 fof(c110,plain,((![X]:(~program_program_decides(X)|(program(X)&program_decides(X))))&(![X]:((~program(X)|~program_decides(X))|program_program_decides(X)))),inference(shift_quantors,[status(thm)],[c109])).
% 1.59/1.81 fof(c112,plain,(![X74]:(![X75]:((~program_program_decides(X74)|(program(X74)&program_decides(X74)))&((~program(X75)|~program_decides(X75))|program_program_decides(X75))))),inference(shift_quantors,[status(thm)],[fof(c111,plain,((![X74]:(~program_program_decides(X74)|(program(X74)&program_decides(X74))))&(![X75]:((~program(X75)|~program_decides(X75))|program_program_decides(X75)))),inference(variable_rename,[status(thm)],[c110])).])).
% 1.59/1.81 fof(c113,plain,(![X74]:(![X75]:(((~program_program_decides(X74)|program(X74))&(~program_program_decides(X74)|program_decides(X74)))&((~program(X75)|~program_decides(X75))|program_program_decides(X75))))),inference(distribute,[status(thm)],[c112])).
% 1.59/1.81 cnf(c114,plain,~program_program_decides(X85)|program(X85),inference(split_conjunct,[status(thm)],[c113])).
% 1.59/1.81 fof(prove_this,conjecture,(~(?[X]:algorithm_program_decides(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', prove_this)).
% 1.59/1.81 fof(c0,negated_conjecture,(~(~(?[X]:algorithm_program_decides(X)))),inference(assume_negation,[status(cth)],[prove_this])).
% 1.59/1.81 fof(c1,negated_conjecture,(?[X]:algorithm_program_decides(X)),inference(fof_nnf,[status(thm)],[c0])).
% 1.59/1.81 fof(c2,negated_conjecture,(?[X2]:algorithm_program_decides(X2)),inference(variable_rename,[status(thm)],[c1])).
% 1.59/1.81 fof(c3,negated_conjecture,algorithm_program_decides(skolem0001),inference(skolemize,[status(esa)],[c2])).
% 1.59/1.81 cnf(c4,negated_conjecture,algorithm_program_decides(skolem0001),inference(split_conjunct,[status(thm)],[c3])).
% 1.59/1.81 fof(p1,axiom,((?[X]:algorithm_program_decides(X))=>(?[W]:program_program_decides(W))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', p1)).
% 1.59/1.81 fof(c31,plain,((![X]:~algorithm_program_decides(X))|(?[W]:program_program_decides(W))),inference(fof_nnf,[status(thm)],[p1])).
% 1.59/1.81 fof(c32,plain,((![X20]:~algorithm_program_decides(X20))|(?[X21]:program_program_decides(X21))),inference(variable_rename,[status(thm)],[c31])).
% 1.59/1.81 fof(c34,plain,(![X20]:(~algorithm_program_decides(X20)|program_program_decides(skolem0008))),inference(shift_quantors,[status(thm)],[fof(c33,plain,((![X20]:~algorithm_program_decides(X20))|program_program_decides(skolem0008)),inference(skolemize,[status(esa)],[c32])).])).
% 1.59/1.81 cnf(c35,plain,~algorithm_program_decides(X87)|program_program_decides(skolem0008),inference(split_conjunct,[status(thm)],[c34])).
% 1.59/1.81 cnf(c128,plain,program_program_decides(skolem0008),inference(resolution,[status(thm)],[c35, c4])).
% 1.59/1.81 cnf(c129,plain,program(skolem0008),inference(resolution,[status(thm)],[c128, c114])).
% 1.59/1.81 fof(p2,axiom,(![W]:(program_program_decides(W)=>(![Y]:(![Z]:(program_halts2_halts3_outputs(W,Y,Z,good)&program_not_halts2_halts3_outputs(W,Y,Z,bad)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', p2)).
% 1.59/1.81 fof(c24,plain,(![W]:(~program_program_decides(W)|(![Y]:(![Z]:(program_halts2_halts3_outputs(W,Y,Z,good)&program_not_halts2_halts3_outputs(W,Y,Z,bad)))))),inference(fof_nnf,[status(thm)],[p2])).
% 1.59/1.81 fof(c25,plain,(![W]:(~program_program_decides(W)|((![Y]:(![Z]:program_halts2_halts3_outputs(W,Y,Z,good)))&(![Y]:(![Z]:program_not_halts2_halts3_outputs(W,Y,Z,bad)))))),inference(shift_quantors,[status(thm)],[c24])).
% 1.59/1.81 fof(c27,plain,(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(~program_program_decides(X15)|(program_halts2_halts3_outputs(X15,X16,X17,good)&program_not_halts2_halts3_outputs(X15,X18,X19,bad)))))))),inference(shift_quantors,[status(thm)],[fof(c26,plain,(![X15]:(~program_program_decides(X15)|((![X16]:(![X17]:program_halts2_halts3_outputs(X15,X16,X17,good)))&(![X18]:(![X19]:program_not_halts2_halts3_outputs(X15,X18,X19,bad)))))),inference(variable_rename,[status(thm)],[c25])).])).
% 1.59/1.81 fof(c28,plain,(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:((~program_program_decides(X15)|program_halts2_halts3_outputs(X15,X16,X17,good))&(~program_program_decides(X15)|program_not_halts2_halts3_outputs(X15,X18,X19,bad)))))))),inference(distribute,[status(thm)],[c27])).
% 1.59/1.81 cnf(c29,plain,~program_program_decides(X132)|program_halts2_halts3_outputs(X132,X134,X133,good),inference(split_conjunct,[status(thm)],[c28])).
% 1.59/1.81 cnf(c150,plain,program_halts2_halts3_outputs(skolem0008,X136,X135,good),inference(resolution,[status(thm)],[c29, c128])).
% 1.59/1.81 fof(p3,axiom,((?[W]:(program(W)&(![Y]:(program_halts2_halts3_outputs(W,Y,Y,good)&program_not_halts2_halts3_outputs(W,Y,Y,bad)))))=>(?[V]:(program(V)&(![Y]:(program_halts2_halts2_outputs(V,Y,good)&program_not_halts2_halts2_outputs(V,Y,bad)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', p3)).
% 1.59/1.81 fof(c15,plain,((![W]:(~program(W)|(?[Y]:(~program_halts2_halts3_outputs(W,Y,Y,good)|~program_not_halts2_halts3_outputs(W,Y,Y,bad)))))|(?[V]:(program(V)&(![Y]:(program_halts2_halts2_outputs(V,Y,good)&program_not_halts2_halts2_outputs(V,Y,bad)))))),inference(fof_nnf,[status(thm)],[p3])).
% 1.59/1.81 fof(c16,plain,((![W]:(~program(W)|((?[Y]:~program_halts2_halts3_outputs(W,Y,Y,good))|(?[Y]:~program_not_halts2_halts3_outputs(W,Y,Y,bad)))))|(?[V]:(program(V)&((![Y]:program_halts2_halts2_outputs(V,Y,good))&(![Y]:program_not_halts2_halts2_outputs(V,Y,bad)))))),inference(shift_quantors,[status(thm)],[c15])).
% 1.59/1.81 fof(c17,plain,((![X9]:(~program(X9)|((?[X10]:~program_halts2_halts3_outputs(X9,X10,X10,good))|(?[X11]:~program_not_halts2_halts3_outputs(X9,X11,X11,bad)))))|(?[X12]:(program(X12)&((![X13]:program_halts2_halts2_outputs(X12,X13,good))&(![X14]:program_not_halts2_halts2_outputs(X12,X14,bad)))))),inference(variable_rename,[status(thm)],[c16])).
% 1.59/1.81 fof(c19,plain,(![X9]:(![X13]:(![X14]:((~program(X9)|(~program_halts2_halts3_outputs(X9,skolem0005(X9),skolem0005(X9),good)|~program_not_halts2_halts3_outputs(X9,skolem0006(X9),skolem0006(X9),bad)))|(program(skolem0007)&(program_halts2_halts2_outputs(skolem0007,X13,good)&program_not_halts2_halts2_outputs(skolem0007,X14,bad))))))),inference(shift_quantors,[status(thm)],[fof(c18,plain,((![X9]:(~program(X9)|(~program_halts2_halts3_outputs(X9,skolem0005(X9),skolem0005(X9),good)|~program_not_halts2_halts3_outputs(X9,skolem0006(X9),skolem0006(X9),bad))))|(program(skolem0007)&((![X13]:program_halts2_halts2_outputs(skolem0007,X13,good))&(![X14]:program_not_halts2_halts2_outputs(skolem0007,X14,bad))))),inference(skolemize,[status(esa)],[c17])).])).
% 1.59/1.81 fof(c20,plain,(![X9]:(![X13]:(![X14]:(((~program(X9)|(~program_halts2_halts3_outputs(X9,skolem0005(X9),skolem0005(X9),good)|~program_not_halts2_halts3_outputs(X9,skolem0006(X9),skolem0006(X9),bad)))|program(skolem0007))&(((~program(X9)|(~program_halts2_halts3_outputs(X9,skolem0005(X9),skolem0005(X9),good)|~program_not_halts2_halts3_outputs(X9,skolem0006(X9),skolem0006(X9),bad)))|program_halts2_halts2_outputs(skolem0007,X13,good))&((~program(X9)|(~program_halts2_halts3_outputs(X9,skolem0005(X9),skolem0005(X9),good)|~program_not_halts2_halts3_outputs(X9,skolem0006(X9),skolem0006(X9),bad)))|program_not_halts2_halts2_outputs(skolem0007,X14,bad))))))),inference(distribute,[status(thm)],[c19])).
% 1.59/1.81 cnf(c21,plain,~program(X113)|~program_halts2_halts3_outputs(X113,skolem0005(X113),skolem0005(X113),good)|~program_not_halts2_halts3_outputs(X113,skolem0006(X113),skolem0006(X113),bad)|program(skolem0007),inference(split_conjunct,[status(thm)],[c20])).
% 1.59/1.81 cnf(c30,plain,~program_program_decides(X138)|program_not_halts2_halts3_outputs(X138,X139,X137,bad),inference(split_conjunct,[status(thm)],[c28])).
% 1.59/1.81 cnf(c151,plain,program_not_halts2_halts3_outputs(skolem0008,X140,X141,bad),inference(resolution,[status(thm)],[c30, c128])).
% 1.59/1.81 cnf(c154,plain,~program(skolem0008)|~program_halts2_halts3_outputs(skolem0008,skolem0005(skolem0008),skolem0005(skolem0008),good)|program(skolem0007),inference(resolution,[status(thm)],[c151, c21])).
% 1.59/1.81 cnf(c421,plain,~program(skolem0008)|program(skolem0007),inference(resolution,[status(thm)],[c154, c150])).
% 1.59/1.81 cnf(c430,plain,program(skolem0007),inference(resolution,[status(thm)],[c421, c129])).
% 1.59/1.81 cnf(c22,plain,~program(X121)|~program_halts2_halts3_outputs(X121,skolem0005(X121),skolem0005(X121),good)|~program_not_halts2_halts3_outputs(X121,skolem0006(X121),skolem0006(X121),bad)|program_halts2_halts2_outputs(skolem0007,X122,good),inference(split_conjunct,[status(thm)],[c20])).
% 1.59/1.81 cnf(c152,plain,~program(skolem0008)|~program_halts2_halts3_outputs(skolem0008,skolem0005(skolem0008),skolem0005(skolem0008),good)|program_halts2_halts2_outputs(skolem0007,X381,good),inference(resolution,[status(thm)],[c151, c22])).
% 1.59/1.81 cnf(c361,plain,~program(skolem0008)|program_halts2_halts2_outputs(skolem0007,X382,good),inference(resolution,[status(thm)],[c152, c150])).
% 1.59/1.81 cnf(c370,plain,program_halts2_halts2_outputs(skolem0007,X383,good),inference(resolution,[status(thm)],[c361, c129])).
% 1.59/1.81 fof(p4,axiom,((?[V]:(program(V)&(![Y]:(program_halts2_halts2_outputs(V,Y,good)&program_not_halts2_halts2_outputs(V,Y,bad)))))=>(?[U]:(program(U)&(![Y]:((program_halts2(Y,Y)=>(~halts2(U,Y)))&program_not_halts2_halts2_outputs(U,Y,good)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', p4)).
% 1.59/1.81 fof(c5,plain,((?[V]:(program(V)&(![Y]:(program_halts2_halts2_outputs(V,Y,good)&program_not_halts2_halts2_outputs(V,Y,bad)))))=>(?[U]:(program(U)&(![Y]:((program_halts2(Y,Y)=>~halts2(U,Y))&program_not_halts2_halts2_outputs(U,Y,good)))))),inference(fof_simplification,[status(thm)],[p4])).
% 1.59/1.81 fof(c6,plain,((![V]:(~program(V)|(?[Y]:(~program_halts2_halts2_outputs(V,Y,good)|~program_not_halts2_halts2_outputs(V,Y,bad)))))|(?[U]:(program(U)&(![Y]:((~program_halts2(Y,Y)|~halts2(U,Y))&program_not_halts2_halts2_outputs(U,Y,good)))))),inference(fof_nnf,[status(thm)],[c5])).
% 1.59/1.81 fof(c7,plain,((![V]:(~program(V)|((?[Y]:~program_halts2_halts2_outputs(V,Y,good))|(?[Y]:~program_not_halts2_halts2_outputs(V,Y,bad)))))|(?[U]:(program(U)&((![Y]:(~program_halts2(Y,Y)|~halts2(U,Y)))&(![Y]:program_not_halts2_halts2_outputs(U,Y,good)))))),inference(shift_quantors,[status(thm)],[c6])).
% 1.59/1.81 fof(c8,plain,((![X3]:(~program(X3)|((?[X4]:~program_halts2_halts2_outputs(X3,X4,good))|(?[X5]:~program_not_halts2_halts2_outputs(X3,X5,bad)))))|(?[X6]:(program(X6)&((![X7]:(~program_halts2(X7,X7)|~halts2(X6,X7)))&(![X8]:program_not_halts2_halts2_outputs(X6,X8,good)))))),inference(variable_rename,[status(thm)],[c7])).
% 1.59/1.81 fof(c10,plain,(![X3]:(![X7]:(![X8]:((~program(X3)|(~program_halts2_halts2_outputs(X3,skolem0002(X3),good)|~program_not_halts2_halts2_outputs(X3,skolem0003(X3),bad)))|(program(skolem0004)&((~program_halts2(X7,X7)|~halts2(skolem0004,X7))&program_not_halts2_halts2_outputs(skolem0004,X8,good))))))),inference(shift_quantors,[status(thm)],[fof(c9,plain,((![X3]:(~program(X3)|(~program_halts2_halts2_outputs(X3,skolem0002(X3),good)|~program_not_halts2_halts2_outputs(X3,skolem0003(X3),bad))))|(program(skolem0004)&((![X7]:(~program_halts2(X7,X7)|~halts2(skolem0004,X7)))&(![X8]:program_not_halts2_halts2_outputs(skolem0004,X8,good))))),inference(skolemize,[status(esa)],[c8])).])).
% 1.59/1.81 fof(c11,plain,(![X3]:(![X7]:(![X8]:(((~program(X3)|(~program_halts2_halts2_outputs(X3,skolem0002(X3),good)|~program_not_halts2_halts2_outputs(X3,skolem0003(X3),bad)))|program(skolem0004))&(((~program(X3)|(~program_halts2_halts2_outputs(X3,skolem0002(X3),good)|~program_not_halts2_halts2_outputs(X3,skolem0003(X3),bad)))|(~program_halts2(X7,X7)|~halts2(skolem0004,X7)))&((~program(X3)|(~program_halts2_halts2_outputs(X3,skolem0002(X3),good)|~program_not_halts2_halts2_outputs(X3,skolem0003(X3),bad)))|program_not_halts2_halts2_outputs(skolem0004,X8,good))))))),inference(distribute,[status(thm)],[c10])).
% 1.59/1.81 cnf(c12,plain,~program(X84)|~program_halts2_halts2_outputs(X84,skolem0002(X84),good)|~program_not_halts2_halts2_outputs(X84,skolem0003(X84),bad)|program(skolem0004),inference(split_conjunct,[status(thm)],[c11])).
% 1.59/1.81 cnf(c23,plain,~program(X130)|~program_halts2_halts3_outputs(X130,skolem0005(X130),skolem0005(X130),good)|~program_not_halts2_halts3_outputs(X130,skolem0006(X130),skolem0006(X130),bad)|program_not_halts2_halts2_outputs(skolem0007,X131,bad),inference(split_conjunct,[status(thm)],[c20])).
% 1.59/1.81 cnf(c153,plain,~program(skolem0008)|~program_halts2_halts3_outputs(skolem0008,skolem0005(skolem0008),skolem0005(skolem0008),good)|program_not_halts2_halts2_outputs(skolem0007,X389,bad),inference(resolution,[status(thm)],[c151, c23])).
% 1.59/1.81 cnf(c381,plain,~program(skolem0008)|program_not_halts2_halts2_outputs(skolem0007,X390,bad),inference(resolution,[status(thm)],[c153, c150])).
% 1.59/1.81 cnf(c390,plain,program_not_halts2_halts2_outputs(skolem0007,X391,bad),inference(resolution,[status(thm)],[c381, c129])).
% 1.59/1.81 cnf(c395,plain,~program(skolem0007)|~program_halts2_halts2_outputs(skolem0007,skolem0002(skolem0007),good)|program(skolem0004),inference(resolution,[status(thm)],[c390, c12])).
% 1.59/1.81 cnf(c4425,plain,~program(skolem0007)|program(skolem0004),inference(resolution,[status(thm)],[c395, c370])).
% 1.59/1.81 cnf(c4427,plain,program(skolem0004),inference(resolution,[status(thm)],[c4425, c430])).
% 1.59/1.81 fof(program_halts2_def,axiom,(![X]:(![Y]:(program_halts2(X,Y)<=>(program(X)&halts2(X,Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', program_halts2_def)).
% 1.59/1.81 fof(c93,plain,(![X]:(![Y]:((~program_halts2(X,Y)|(program(X)&halts2(X,Y)))&((~program(X)|~halts2(X,Y))|program_halts2(X,Y))))),inference(fof_nnf,[status(thm)],[program_halts2_def])).
% 1.59/1.81 fof(c94,plain,((![X]:(![Y]:(~program_halts2(X,Y)|(program(X)&halts2(X,Y)))))&(![X]:(![Y]:((~program(X)|~halts2(X,Y))|program_halts2(X,Y))))),inference(shift_quantors,[status(thm)],[c93])).
% 1.59/1.81 fof(c96,plain,(![X68]:(![X69]:(![X70]:(![X71]:((~program_halts2(X68,X69)|(program(X68)&halts2(X68,X69)))&((~program(X70)|~halts2(X70,X71))|program_halts2(X70,X71))))))),inference(shift_quantors,[status(thm)],[fof(c95,plain,((![X68]:(![X69]:(~program_halts2(X68,X69)|(program(X68)&halts2(X68,X69)))))&(![X70]:(![X71]:((~program(X70)|~halts2(X70,X71))|program_halts2(X70,X71))))),inference(variable_rename,[status(thm)],[c94])).])).
% 1.59/1.81 fof(c97,plain,(![X68]:(![X69]:(![X70]:(![X71]:(((~program_halts2(X68,X69)|program(X68))&(~program_halts2(X68,X69)|halts2(X68,X69)))&((~program(X70)|~halts2(X70,X71))|program_halts2(X70,X71))))))),inference(distribute,[status(thm)],[c96])).
% 1.59/1.81 cnf(c100,plain,~program(X221)|~halts2(X221,X220)|program_halts2(X221,X220),inference(split_conjunct,[status(thm)],[c97])).
% 1.59/1.81 fof(halts2_outputs_def,axiom,(![X]:(![Y]:(![W]:(halts2_outputs(X,Y,W)<=>(halts2(X,Y)&outputs(X,W)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', halts2_outputs_def)).
% 1.59/1.81 fof(c68,plain,(![X]:(![Y]:(![W]:((~halts2_outputs(X,Y,W)|(halts2(X,Y)&outputs(X,W)))&((~halts2(X,Y)|~outputs(X,W))|halts2_outputs(X,Y,W)))))),inference(fof_nnf,[status(thm)],[halts2_outputs_def])).
% 1.59/1.81 fof(c69,plain,((![X]:(![Y]:(![W]:(~halts2_outputs(X,Y,W)|(halts2(X,Y)&outputs(X,W))))))&(![X]:(![Y]:(![W]:((~halts2(X,Y)|~outputs(X,W))|halts2_outputs(X,Y,W)))))),inference(shift_quantors,[status(thm)],[c68])).
% 1.59/1.81 fof(c71,plain,(![X50]:(![X51]:(![X52]:(![X53]:(![X54]:(![X55]:((~halts2_outputs(X50,X51,X52)|(halts2(X50,X51)&outputs(X50,X52)))&((~halts2(X53,X54)|~outputs(X53,X55))|halts2_outputs(X53,X54,X55))))))))),inference(shift_quantors,[status(thm)],[fof(c70,plain,((![X50]:(![X51]:(![X52]:(~halts2_outputs(X50,X51,X52)|(halts2(X50,X51)&outputs(X50,X52))))))&(![X53]:(![X54]:(![X55]:((~halts2(X53,X54)|~outputs(X53,X55))|halts2_outputs(X53,X54,X55)))))),inference(variable_rename,[status(thm)],[c69])).])).
% 1.59/1.81 fof(c72,plain,(![X50]:(![X51]:(![X52]:(![X53]:(![X54]:(![X55]:(((~halts2_outputs(X50,X51,X52)|halts2(X50,X51))&(~halts2_outputs(X50,X51,X52)|outputs(X50,X52)))&((~halts2(X53,X54)|~outputs(X53,X55))|halts2_outputs(X53,X54,X55))))))))),inference(distribute,[status(thm)],[c71])).
% 1.59/1.81 cnf(c73,plain,~halts2_outputs(X114,X116,X115)|halts2(X114,X116),inference(split_conjunct,[status(thm)],[c72])).
% 1.59/1.81 fof(program_not_halts2_def,axiom,(![X]:(![Y]:(program_not_halts2(X,Y)<=>(program(X)&(~halts2(X,Y)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', program_not_halts2_def)).
% 1.59/1.81 fof(c76,plain,(![X]:(![Y]:(program_not_halts2(X,Y)<=>(program(X)&~halts2(X,Y))))),inference(fof_simplification,[status(thm)],[program_not_halts2_def])).
% 1.59/1.81 fof(c77,plain,(![X]:(![Y]:((~program_not_halts2(X,Y)|(program(X)&~halts2(X,Y)))&((~program(X)|halts2(X,Y))|program_not_halts2(X,Y))))),inference(fof_nnf,[status(thm)],[c76])).
% 1.59/1.81 fof(c78,plain,((![X]:(![Y]:(~program_not_halts2(X,Y)|(program(X)&~halts2(X,Y)))))&(![X]:(![Y]:((~program(X)|halts2(X,Y))|program_not_halts2(X,Y))))),inference(shift_quantors,[status(thm)],[c77])).
% 1.59/1.81 fof(c80,plain,(![X56]:(![X57]:(![X58]:(![X59]:((~program_not_halts2(X56,X57)|(program(X56)&~halts2(X56,X57)))&((~program(X58)|halts2(X58,X59))|program_not_halts2(X58,X59))))))),inference(shift_quantors,[status(thm)],[fof(c79,plain,((![X56]:(![X57]:(~program_not_halts2(X56,X57)|(program(X56)&~halts2(X56,X57)))))&(![X58]:(![X59]:((~program(X58)|halts2(X58,X59))|program_not_halts2(X58,X59))))),inference(variable_rename,[status(thm)],[c78])).])).
% 1.59/1.81 fof(c81,plain,(![X56]:(![X57]:(![X58]:(![X59]:(((~program_not_halts2(X56,X57)|program(X56))&(~program_not_halts2(X56,X57)|~halts2(X56,X57)))&((~program(X58)|halts2(X58,X59))|program_not_halts2(X58,X59))))))),inference(distribute,[status(thm)],[c80])).
% 1.59/1.81 cnf(c84,plain,~program(X208)|halts2(X208,X207)|program_not_halts2(X208,X207),inference(split_conjunct,[status(thm)],[c81])).
% 1.59/1.81 cnf(c4434,plain,halts2(skolem0004,X2201)|program_not_halts2(skolem0004,X2201),inference(resolution,[status(thm)],[c4427, c84])).
% 1.59/1.81 fof(program_not_halts2_halts2_outputs_def,axiom,(![X]:(![Y]:(![W]:(program_not_halts2_halts2_outputs(X,Y,W)<=>(program_not_halts2(Y,Y)=>halts2_outputs(X,Y,W)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', program_not_halts2_halts2_outputs_def)).
% 1.59/1.81 fof(c36,plain,(![X]:(![Y]:(![W]:((~program_not_halts2_halts2_outputs(X,Y,W)|(~program_not_halts2(Y,Y)|halts2_outputs(X,Y,W)))&((program_not_halts2(Y,Y)&~halts2_outputs(X,Y,W))|program_not_halts2_halts2_outputs(X,Y,W)))))),inference(fof_nnf,[status(thm)],[program_not_halts2_halts2_outputs_def])).
% 1.59/1.81 fof(c37,plain,((![X]:(![Y]:(![W]:(~program_not_halts2_halts2_outputs(X,Y,W)|(~program_not_halts2(Y,Y)|halts2_outputs(X,Y,W))))))&(![X]:(![Y]:(![W]:((program_not_halts2(Y,Y)&~halts2_outputs(X,Y,W))|program_not_halts2_halts2_outputs(X,Y,W)))))),inference(shift_quantors,[status(thm)],[c36])).
% 1.59/1.81 fof(c39,plain,(![X22]:(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:((~program_not_halts2_halts2_outputs(X22,X23,X24)|(~program_not_halts2(X23,X23)|halts2_outputs(X22,X23,X24)))&((program_not_halts2(X26,X26)&~halts2_outputs(X25,X26,X27))|program_not_halts2_halts2_outputs(X25,X26,X27))))))))),inference(shift_quantors,[status(thm)],[fof(c38,plain,((![X22]:(![X23]:(![X24]:(~program_not_halts2_halts2_outputs(X22,X23,X24)|(~program_not_halts2(X23,X23)|halts2_outputs(X22,X23,X24))))))&(![X25]:(![X26]:(![X27]:((program_not_halts2(X26,X26)&~halts2_outputs(X25,X26,X27))|program_not_halts2_halts2_outputs(X25,X26,X27)))))),inference(variable_rename,[status(thm)],[c37])).])).
% 1.59/1.81 fof(c40,plain,(![X22]:(![X23]:(![X24]:(![X25]:(![X26]:(![X27]:((~program_not_halts2_halts2_outputs(X22,X23,X24)|(~program_not_halts2(X23,X23)|halts2_outputs(X22,X23,X24)))&((program_not_halts2(X26,X26)|program_not_halts2_halts2_outputs(X25,X26,X27))&(~halts2_outputs(X25,X26,X27)|program_not_halts2_halts2_outputs(X25,X26,X27)))))))))),inference(distribute,[status(thm)],[c39])).
% 1.59/1.81 cnf(c41,plain,~program_not_halts2_halts2_outputs(X145,X147,X146)|~program_not_halts2(X147,X147)|halts2_outputs(X145,X147,X146),inference(split_conjunct,[status(thm)],[c40])).
% 1.59/1.81 cnf(c42,plain,program_not_halts2(X102,X102)|program_not_halts2_halts2_outputs(X101,X102,X103),inference(split_conjunct,[status(thm)],[c40])).
% 1.59/1.81 cnf(c83,plain,~program_not_halts2(X94,X95)|~halts2(X94,X95),inference(split_conjunct,[status(thm)],[c81])).
% 1.59/1.81 cnf(c14,plain,~program(X98)|~program_halts2_halts2_outputs(X98,skolem0002(X98),good)|~program_not_halts2_halts2_outputs(X98,skolem0003(X98),bad)|program_not_halts2_halts2_outputs(skolem0004,X99,good),inference(split_conjunct,[status(thm)],[c11])).
% 1.59/1.81 cnf(c393,plain,~program(skolem0007)|~program_halts2_halts2_outputs(skolem0007,skolem0002(skolem0007),good)|program_not_halts2_halts2_outputs(skolem0004,X2177,good),inference(resolution,[status(thm)],[c390, c14])).
% 1.59/1.81 cnf(c4351,plain,~program(skolem0007)|program_not_halts2_halts2_outputs(skolem0004,X2178,good),inference(resolution,[status(thm)],[c393, c370])).
% 1.59/1.81 cnf(c4353,plain,program_not_halts2_halts2_outputs(skolem0004,X2179,good),inference(resolution,[status(thm)],[c4351, c430])).
% 1.59/1.81 cnf(c4357,plain,~program_not_halts2(X2180,X2180)|halts2_outputs(skolem0004,X2180,good),inference(resolution,[status(thm)],[c4353, c41])).
% 1.59/1.81 cnf(c4363,plain,halts2_outputs(skolem0004,X2181,good)|program_not_halts2_halts2_outputs(X2182,X2181,X2183),inference(resolution,[status(thm)],[c4357, c42])).
% 1.59/1.81 cnf(c4377,plain,program_not_halts2_halts2_outputs(X2185,X2184,X2186)|halts2(skolem0004,X2184),inference(resolution,[status(thm)],[c4363, c73])).
% 1.59/1.81 cnf(c4391,plain,program_not_halts2_halts2_outputs(X2196,X2195,X2194)|~program_not_halts2(skolem0004,X2195),inference(resolution,[status(thm)],[c4377, c83])).
% 1.59/1.81 cnf(c4448,plain,program_not_halts2_halts2_outputs(X2232,skolem0004,X2233)|program_not_halts2_halts2_outputs(X2231,skolem0004,X2234),inference(resolution,[status(thm)],[c4391, c42])).
% 1.59/1.81 cnf(c4525,plain,program_not_halts2_halts2_outputs(X2236,skolem0004,X2235),inference(factor,[status(thm)],[c4448])).
% 1.59/1.81 cnf(c4528,plain,~program_not_halts2(skolem0004,skolem0004)|halts2_outputs(X2250,skolem0004,X2251),inference(resolution,[status(thm)],[c4525, c41])).
% 1.59/1.81 cnf(c4532,plain,halts2_outputs(X2253,skolem0004,X2252)|halts2(skolem0004,skolem0004),inference(resolution,[status(thm)],[c4528, c4434])).
% 1.59/1.81 cnf(c4541,plain,halts2(skolem0004,skolem0004)|halts2(X2265,skolem0004),inference(resolution,[status(thm)],[c4532, c73])).
% 1.59/1.81 cnf(c4593,plain,halts2(skolem0004,skolem0004),inference(factor,[status(thm)],[c4541])).
% 1.59/1.81 cnf(c4649,plain,~program(skolem0004)|program_halts2(skolem0004,skolem0004),inference(resolution,[status(thm)],[c4593, c100])).
% 1.59/1.81 cnf(c4668,plain,program_halts2(skolem0004,skolem0004),inference(resolution,[status(thm)],[c4649, c4427])).
% 1.59/1.81 cnf(c13,plain,~program(X89)|~program_halts2_halts2_outputs(X89,skolem0002(X89),good)|~program_not_halts2_halts2_outputs(X89,skolem0003(X89),bad)|~program_halts2(X88,X88)|~halts2(skolem0004,X88),inference(split_conjunct,[status(thm)],[c11])).
% 1.59/1.81 cnf(c392,plain,~program(skolem0007)|~program_halts2_halts2_outputs(skolem0007,skolem0002(skolem0007),good)|~program_halts2(X2161,X2161)|~halts2(skolem0004,X2161),inference(resolution,[status(thm)],[c390, c13])).
% 1.59/1.81 cnf(c4313,plain,~program(skolem0007)|~program_halts2(X2162,X2162)|~halts2(skolem0004,X2162),inference(resolution,[status(thm)],[c392, c370])).
% 1.59/1.81 cnf(c4650,plain,~program(skolem0007)|~program_halts2(skolem0004,skolem0004),inference(resolution,[status(thm)],[c4593, c4313])).
% 1.59/1.81 cnf(c4733,plain,~program(skolem0007),inference(resolution,[status(thm)],[c4650, c4668])).
% 1.59/1.81 cnf(c4737,plain,$false,inference(resolution,[status(thm)],[c4733, c430])).
% 1.59/1.81 % SZS output end CNFRefutation
% 1.59/1.81
% 1.59/1.81 % Initial clauses : 43
% 1.59/1.81 % Processed clauses : 486
% 1.59/1.81 % Factors computed : 16
% 1.59/1.81 % Resolvents computed: 4599
% 1.59/1.81 % Tautologies deleted: 12
% 1.59/1.81 % Forward subsumed : 596
% 1.59/1.81 % Backward subsumed : 141
% 1.59/1.81 % -------- CPU Time ---------
% 1.59/1.81 % User time : 1.434 s
% 1.59/1.81 % System time : 0.032 s
% 1.59/1.81 % Total time : 1.466 s
%------------------------------------------------------------------------------