%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS256+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n027.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:29:00 EDT 2024
% Result : Theorem 45.03s 45.23s
% Output : Refutation 45.03s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS256+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n027.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Thu May 9 00:17:08 EDT 2024
% 0.14/0.34 % CPUTime :
% 45.03/45.23 % Version: 1.5
% 45.03/45.23 % SZS status Theorem
% 45.03/45.23 % SZS output start CNFRefutation
% 45.03/45.23 fof(mighta_esa_thm,conjecture,mighta(esa,thm),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mighta_esa_thm)).
% 45.03/45.23 fof(c0,negated_conjecture,(~mighta(esa,thm)),inference(assume_negation,[status(cth)],[mighta_esa_thm])).
% 45.03/45.23 fof(c1,negated_conjecture,~mighta(esa,thm),inference(fof_simplification,[status(thm)],[c0])).
% 45.03/45.23 cnf(c2,negated_conjecture,~mighta(esa,thm),inference(split_conjunct,[status(thm)],[c1])).
% 45.03/45.23 fof(mighta,axiom,(![S1]:(![S2]:((?[Ax]:(?[C]:(status(Ax,C,S1)&status(Ax,C,S2))))<=>mighta(S1,S2)))),file('/export/starexec/sandbox2/benchmark/Axioms/KRS001+1.ax', mighta)).
% 45.03/45.23 fof(c92,plain,(![S1]:(![S2]:(((![Ax]:(![C]:(~status(Ax,C,S1)|~status(Ax,C,S2))))|mighta(S1,S2))&(~mighta(S1,S2)|(?[Ax]:(?[C]:(status(Ax,C,S1)&status(Ax,C,S2)))))))),inference(fof_nnf,[status(thm)],[mighta])).
% 45.03/45.23 fof(c93,plain,((![S1]:(![S2]:((![Ax]:(![C]:(~status(Ax,C,S1)|~status(Ax,C,S2))))|mighta(S1,S2))))&(![S1]:(![S2]:(~mighta(S1,S2)|(?[Ax]:(?[C]:(status(Ax,C,S1)&status(Ax,C,S2)))))))),inference(shift_quantors,[status(thm)],[c92])).
% 45.03/45.23 fof(c94,plain,((![X66]:(![X67]:((![X68]:(![X69]:(~status(X68,X69,X66)|~status(X68,X69,X67))))|mighta(X66,X67))))&(![X70]:(![X71]:(~mighta(X70,X71)|(?[X72]:(?[X73]:(status(X72,X73,X70)&status(X72,X73,X71)))))))),inference(variable_rename,[status(thm)],[c93])).
% 45.03/45.23 fof(c96,plain,(![X66]:(![X67]:(![X68]:(![X69]:(![X70]:(![X71]:(((~status(X68,X69,X66)|~status(X68,X69,X67))|mighta(X66,X67))&(~mighta(X70,X71)|(status(skolem0028(X70,X71),skolem0029(X70,X71),X70)&status(skolem0028(X70,X71),skolem0029(X70,X71),X71)))))))))),inference(shift_quantors,[status(thm)],[fof(c95,plain,((![X66]:(![X67]:((![X68]:(![X69]:(~status(X68,X69,X66)|~status(X68,X69,X67))))|mighta(X66,X67))))&(![X70]:(![X71]:(~mighta(X70,X71)|(status(skolem0028(X70,X71),skolem0029(X70,X71),X70)&status(skolem0028(X70,X71),skolem0029(X70,X71),X71)))))),inference(skolemize,[status(esa)],[c94])).])).
% 45.03/45.23 fof(c97,plain,(![X66]:(![X67]:(![X68]:(![X69]:(![X70]:(![X71]:(((~status(X68,X69,X66)|~status(X68,X69,X67))|mighta(X66,X67))&((~mighta(X70,X71)|status(skolem0028(X70,X71),skolem0029(X70,X71),X70))&(~mighta(X70,X71)|status(skolem0028(X70,X71),skolem0029(X70,X71),X71)))))))))),inference(distribute,[status(thm)],[c96])).
% 45.03/45.23 cnf(c98,plain,~status(X360,X362,X359)|~status(X360,X362,X361)|mighta(X359,X361),inference(split_conjunct,[status(thm)],[c97])).
% 45.03/45.23 fof(thm,axiom,(![Ax]:(![C]:((![I1]:(model(I1,Ax)=>model(I1,C)))<=>status(Ax,C,thm)))),file('/export/starexec/sandbox2/benchmark/Axioms/KRS001+0.ax', thm)).
% 45.03/45.23 fof(c246,plain,(![Ax]:(![C]:(((?[I1]:(model(I1,Ax)&~model(I1,C)))|status(Ax,C,thm))&(~status(Ax,C,thm)|(![I1]:(~model(I1,Ax)|model(I1,C))))))),inference(fof_nnf,[status(thm)],[thm])).
% 45.03/45.23 fof(c247,plain,((![Ax]:(![C]:((?[I1]:(model(I1,Ax)&~model(I1,C)))|status(Ax,C,thm))))&(![Ax]:(![C]:(~status(Ax,C,thm)|(![I1]:(~model(I1,Ax)|model(I1,C))))))),inference(shift_quantors,[status(thm)],[c246])).
% 45.03/45.23 fof(c248,plain,((![X196]:(![X197]:((?[X198]:(model(X198,X196)&~model(X198,X197)))|status(X196,X197,thm))))&(![X199]:(![X200]:(~status(X199,X200,thm)|(![X201]:(~model(X201,X199)|model(X201,X200))))))),inference(variable_rename,[status(thm)],[c247])).
% 45.03/45.23 fof(c250,plain,(![X196]:(![X197]:(![X199]:(![X200]:(![X201]:(((model(skolem0062(X196,X197),X196)&~model(skolem0062(X196,X197),X197))|status(X196,X197,thm))&(~status(X199,X200,thm)|(~model(X201,X199)|model(X201,X200))))))))),inference(shift_quantors,[status(thm)],[fof(c249,plain,((![X196]:(![X197]:((model(skolem0062(X196,X197),X196)&~model(skolem0062(X196,X197),X197))|status(X196,X197,thm))))&(![X199]:(![X200]:(~status(X199,X200,thm)|(![X201]:(~model(X201,X199)|model(X201,X200))))))),inference(skolemize,[status(esa)],[c248])).])).
% 45.03/45.23 fof(c251,plain,(![X196]:(![X197]:(![X199]:(![X200]:(![X201]:(((model(skolem0062(X196,X197),X196)|status(X196,X197,thm))&(~model(skolem0062(X196,X197),X197)|status(X196,X197,thm)))&(~status(X199,X200,thm)|(~model(X201,X199)|model(X201,X200))))))))),inference(distribute,[status(thm)],[c250])).
% 45.03/45.23 cnf(c252,plain,model(skolem0062(X574,X573),X574)|status(X574,X573,thm),inference(split_conjunct,[status(thm)],[c251])).
% 45.03/45.23 cnf(c253,plain,~model(skolem0062(X576,X575),X575)|status(X576,X575,thm),inference(split_conjunct,[status(thm)],[c251])).
% 45.03/45.23 cnf(c1185,plain,status(X577,X577,thm),inference(resolution,[status(thm)],[c253, c252])).
% 45.03/45.23 cnf(c1200,plain,~status(X1963,X1963,X1962)|mighta(X1962,thm),inference(resolution,[status(thm)],[c1185, c98])).
% 45.03/45.23 fof(mixed_pair,axiom,(?[Ax]:(?[C]:((((?[I1]:model(I1,Ax))&(![I2]:(model(I2,Ax)=>model(I2,C))))&(?[I3]:((~model(I3,Ax))&model(I3,C))))&(?[I4]:(~model(I4,C)))))),file('/export/starexec/sandbox2/benchmark/Axioms/KRS001+1.ax', mixed_pair)).
% 45.03/45.23 fof(c9,plain,(?[Ax]:(?[C]:((((?[I1]:model(I1,Ax))&(![I2]:(model(I2,Ax)=>model(I2,C))))&(?[I3]:(~model(I3,Ax)&model(I3,C))))&(?[I4]:~model(I4,C))))),inference(fof_simplification,[status(thm)],[mixed_pair])).
% 45.03/45.23 fof(c10,plain,(?[Ax]:(?[C]:((((?[I1]:model(I1,Ax))&(![I2]:(~model(I2,Ax)|model(I2,C))))&(?[I3]:(~model(I3,Ax)&model(I3,C))))&(?[I4]:~model(I4,C))))),inference(fof_nnf,[status(thm)],[c9])).
% 45.03/45.23 fof(c11,plain,(?[X6]:(?[X7]:((((?[X8]:model(X8,X6))&(![X9]:(~model(X9,X6)|model(X9,X7))))&(?[X10]:(~model(X10,X6)&model(X10,X7))))&(?[X11]:~model(X11,X7))))),inference(variable_rename,[status(thm)],[c10])).
% 45.03/45.23 fof(c13,plain,(![X9]:(((model(skolem0007,skolem0005)&(~model(X9,skolem0005)|model(X9,skolem0006)))&(~model(skolem0008,skolem0005)&model(skolem0008,skolem0006)))&~model(skolem0009,skolem0006))),inference(shift_quantors,[status(thm)],[fof(c12,plain,(((model(skolem0007,skolem0005)&(![X9]:(~model(X9,skolem0005)|model(X9,skolem0006))))&(~model(skolem0008,skolem0005)&model(skolem0008,skolem0006)))&~model(skolem0009,skolem0006)),inference(skolemize,[status(esa)],[c11])).])).
% 45.03/45.23 cnf(c15,plain,~model(X238,skolem0005)|model(X238,skolem0006),inference(split_conjunct,[status(thm)],[c13])).
% 45.03/45.23 cnf(c14,plain,model(skolem0007,skolem0005),inference(split_conjunct,[status(thm)],[c13])).
% 45.03/45.23 fof(cax,axiom,(![Ax]:(![C]:((~(?[I1]:model(I1,Ax)))<=>status(Ax,C,cax)))),file('/export/starexec/sandbox2/benchmark/Axioms/KRS001+0.ax', cax)).
% 45.03/45.23 fof(c159,plain,(![Ax]:(![C]:(((?[I1]:model(I1,Ax))|status(Ax,C,cax))&(~status(Ax,C,cax)|(![I1]:~model(I1,Ax)))))),inference(fof_nnf,[status(thm)],[cax])).
% 45.03/45.23 fof(c160,plain,((![Ax]:((?[I1]:model(I1,Ax))|(![C]:status(Ax,C,cax))))&(![Ax]:((![C]:~status(Ax,C,cax))|(![I1]:~model(I1,Ax))))),inference(shift_quantors,[status(thm)],[c159])).
% 45.03/45.23 fof(c161,plain,((![X122]:((?[X123]:model(X123,X122))|(![X124]:status(X122,X124,cax))))&(![X125]:((![X126]:~status(X125,X126,cax))|(![X127]:~model(X127,X125))))),inference(variable_rename,[status(thm)],[c160])).
% 45.03/45.23 fof(c163,plain,(![X122]:(![X124]:(![X125]:(![X126]:(![X127]:((model(skolem0042(X122),X122)|status(X122,X124,cax))&(~status(X125,X126,cax)|~model(X127,X125)))))))),inference(shift_quantors,[status(thm)],[fof(c162,plain,((![X122]:(model(skolem0042(X122),X122)|(![X124]:status(X122,X124,cax))))&(![X125]:((![X126]:~status(X125,X126,cax))|(![X127]:~model(X127,X125))))),inference(skolemize,[status(esa)],[c161])).])).
% 45.03/45.23 cnf(c165,plain,~status(X268,X269,cax)|~model(X270,X268),inference(split_conjunct,[status(thm)],[c163])).
% 45.03/45.23 cnf(c164,plain,model(skolem0042(X445),X445)|status(X445,X444,cax),inference(split_conjunct,[status(thm)],[c163])).
% 45.03/45.23 cnf(c772,plain,model(skolem0042(X461),X461)|~model(X460,X461),inference(resolution,[status(thm)],[c164, c165])).
% 45.03/45.23 cnf(c824,plain,model(skolem0042(skolem0005),skolem0005),inference(resolution,[status(thm)],[c772, c14])).
% 45.03/45.23 cnf(c855,plain,model(skolem0042(skolem0005),skolem0006),inference(resolution,[status(thm)],[c824, c15])).
% 45.03/45.23 fof(esa,axiom,(![Ax]:(![C]:(((?[I1]:model(I1,Ax))<=>(?[I2]:model(I2,C)))<=>status(Ax,C,esa)))),file('/export/starexec/sandbox2/benchmark/Axioms/KRS001+0.ax', esa)).
% 45.03/45.23 fof(c264,plain,(![Ax]:(![C]:(((((![I1]:~model(I1,Ax))|(![I2]:~model(I2,C)))&((?[I1]:model(I1,Ax))|(?[I2]:model(I2,C))))|status(Ax,C,esa))&(~status(Ax,C,esa)|(((![I1]:~model(I1,Ax))|(?[I2]:model(I2,C)))&((![I2]:~model(I2,C))|(?[I1]:model(I1,Ax)))))))),inference(fof_nnf,[status(thm)],[esa])).
% 45.03/45.23 fof(c265,plain,((![Ax]:(![C]:((((![I1]:~model(I1,Ax))|(![I2]:~model(I2,C)))&((?[I1]:model(I1,Ax))|(?[I2]:model(I2,C))))|status(Ax,C,esa))))&(![Ax]:(![C]:(~status(Ax,C,esa)|(((![I1]:~model(I1,Ax))|(?[I2]:model(I2,C)))&((![I2]:~model(I2,C))|(?[I1]:model(I1,Ax)))))))),inference(shift_quantors,[status(thm)],[c264])).
% 45.03/45.23 fof(c266,plain,((![X208]:(![X209]:((((![X210]:~model(X210,X208))|(![X211]:~model(X211,X209)))&((?[X212]:model(X212,X208))|(?[X213]:model(X213,X209))))|status(X208,X209,esa))))&(![X214]:(![X215]:(~status(X214,X215,esa)|(((![X216]:~model(X216,X214))|(?[X217]:model(X217,X215)))&((![X218]:~model(X218,X215))|(?[X219]:model(X219,X214)))))))),inference(variable_rename,[status(thm)],[c265])).
% 45.03/45.23 fof(c268,plain,(![X208]:(![X209]:(![X210]:(![X211]:(![X214]:(![X215]:(![X216]:(![X218]:((((~model(X210,X208)|~model(X211,X209))&(model(skolem0064(X208,X209),X208)|model(skolem0065(X208,X209),X209)))|status(X208,X209,esa))&(~status(X214,X215,esa)|((~model(X216,X214)|model(skolem0066(X214,X215),X215))&(~model(X218,X215)|model(skolem0067(X214,X215),X214))))))))))))),inference(shift_quantors,[status(thm)],[fof(c267,plain,((![X208]:(![X209]:((((![X210]:~model(X210,X208))|(![X211]:~model(X211,X209)))&(model(skolem0064(X208,X209),X208)|model(skolem0065(X208,X209),X209)))|status(X208,X209,esa))))&(![X214]:(![X215]:(~status(X214,X215,esa)|(((![X216]:~model(X216,X214))|model(skolem0066(X214,X215),X215))&((![X218]:~model(X218,X215))|model(skolem0067(X214,X215),X214))))))),inference(skolemize,[status(esa)],[c266])).])).
% 45.03/45.23 fof(c269,plain,(![X208]:(![X209]:(![X210]:(![X211]:(![X214]:(![X215]:(![X216]:(![X218]:((((~model(X210,X208)|~model(X211,X209))|status(X208,X209,esa))&((model(skolem0064(X208,X209),X208)|model(skolem0065(X208,X209),X209))|status(X208,X209,esa)))&((~status(X214,X215,esa)|(~model(X216,X214)|model(skolem0066(X214,X215),X215)))&(~status(X214,X215,esa)|(~model(X218,X215)|model(skolem0067(X214,X215),X214))))))))))))),inference(distribute,[status(thm)],[c268])).
% 45.03/45.23 cnf(c270,plain,~model(X590,X589)|~model(X592,X591)|status(X589,X591,esa),inference(split_conjunct,[status(thm)],[c269])).
% 45.03/45.23 cnf(c1263,plain,~model(X2118,X2119)|status(X2119,X2119,esa),inference(factor,[status(thm)],[c270])).
% 45.03/45.23 cnf(c55031,plain,status(skolem0006,skolem0006,esa),inference(resolution,[status(thm)],[c1263, c855])).
% 45.03/45.23 cnf(c71211,plain,mighta(esa,thm),inference(resolution,[status(thm)],[c55031, c1200])).
% 45.03/45.23 cnf(c71795,plain,$false,inference(resolution,[status(thm)],[c71211, c2])).
% 45.03/45.23 % SZS output end CNFRefutation
% 45.03/45.23
% 45.03/45.23 % Initial clauses : 109
% 45.03/45.23 % Processed clauses : 1149
% 45.03/45.23 % Factors computed : 153
% 45.03/45.23 % Resolvents computed: 71352
% 45.03/45.23 % Tautologies deleted: 7
% 45.03/45.23 % Forward subsumed : 3376
% 45.03/45.23 % Backward subsumed : 0
% 45.03/45.23 % -------- CPU Time ---------
% 45.03/45.23 % User time : 44.738 s
% 45.03/45.23 % System time : 0.154 s
% 45.03/45.23 % Total time : 44.892 s
%------------------------------------------------------------------------------