%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS200+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n024.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:28:55 EDT 2024
% Result : Theorem 158.48s 158.78s
% Output : Refutation 158.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.12 % Problem : KRS200+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.05/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n024.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:11:53 EDT 2024
% 0.14/0.34 % CPUTime :
% 158.48/158.78 % Version: 1.5
% 158.48/158.78 % SZS status Theorem
% 158.48/158.78 % SZS output start CNFRefutation
% 158.48/158.78 fof(cax,axiom,(![Ax]:(![C]:((~(?[I1]:model(I1,Ax)))<=>status(Ax,C,cax)))),file('/export/starexec/sandbox/benchmark/Axioms/KRS001+0.ax', cax)).
% 158.48/158.78 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])).
% 158.48/158.78 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])).
% 158.48/158.78 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])).
% 158.48/158.78 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])).])).
% 158.48/158.78 cnf(c165,plain,~status(X270,X269,cax)|~model(X268,X270),inference(split_conjunct,[status(thm)],[c163])).
% 158.48/158.78 fof(mighta,axiom,(![S1]:(![S2]:((?[Ax]:(?[C]:(status(Ax,C,S1)&status(Ax,C,S2))))<=>mighta(S1,S2)))),file('/export/starexec/sandbox/benchmark/Axioms/KRS001+1.ax', mighta)).
% 158.48/158.78 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])).
% 158.48/158.78 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])).
% 158.48/158.78 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])).
% 158.48/158.78 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])).])).
% 158.48/158.78 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])).
% 158.48/158.78 cnf(c99,plain,~mighta(X365,X364)|status(skolem0028(X365,X364),skolem0029(X365,X364),X365),inference(split_conjunct,[status(thm)],[c97])).
% 158.48/158.78 cnf(c98,plain,~status(X362,X359,X361)|~status(X362,X359,X360)|mighta(X361,X360),inference(split_conjunct,[status(thm)],[c97])).
% 158.48/158.78 cnf(c496,plain,~status(X390,X388,X389)|mighta(X389,X389),inference(factor,[status(thm)],[c98])).
% 158.48/158.78 fof(contradiction,axiom,(?[F]:(![I]:(~model(I,F)))),file('/export/starexec/sandbox/benchmark/Axioms/KRS001+1.ax', contradiction)).
% 158.48/158.78 fof(c26,plain,(?[F]:(![I]:~model(I,F))),inference(fof_simplification,[status(thm)],[contradiction])).
% 158.48/158.78 fof(c27,plain,(?[X17]:(![X18]:~model(X18,X17))),inference(variable_rename,[status(thm)],[c26])).
% 158.48/158.78 fof(c28,plain,(![X18]:~model(X18,skolem0015)),inference(skolemize,[status(esa)],[c27])).
% 158.48/158.78 cnf(c29,plain,~model(X236,skolem0015),inference(split_conjunct,[status(thm)],[c28])).
% 158.48/158.78 cnf(c164,plain,model(skolem0042(X444),X444)|status(X444,X445,cax),inference(split_conjunct,[status(thm)],[c163])).
% 158.48/158.78 cnf(c757,plain,status(skolem0015,X456,cax),inference(resolution,[status(thm)],[c164, c29])).
% 158.48/158.78 cnf(c799,plain,mighta(cax,cax),inference(resolution,[status(thm)],[c757, c496])).
% 158.48/158.78 cnf(c809,plain,status(skolem0028(cax,cax),skolem0029(cax,cax),cax),inference(resolution,[status(thm)],[c799, c99])).
% 158.48/158.78 cnf(c18176,plain,~model(X3313,skolem0028(cax,cax)),inference(resolution,[status(thm)],[c809, c165])).
% 158.48/158.78 fof(satisfiable,axiom,(?[F]:((?[I1]:model(I1,F))&(?[I2]:(~model(I2,F))))),file('/export/starexec/sandbox/benchmark/Axioms/KRS001+1.ax', satisfiable)).
% 158.48/158.78 fof(c30,plain,(?[F]:((?[I1]:model(I1,F))&(?[I2]:~model(I2,F)))),inference(fof_simplification,[status(thm)],[satisfiable])).
% 158.48/158.78 fof(c31,plain,(?[X19]:((?[X20]:model(X20,X19))&(?[X21]:~model(X21,X19)))),inference(variable_rename,[status(thm)],[c30])).
% 158.48/158.78 fof(c32,plain,(model(skolem0017,skolem0016)&~model(skolem0018,skolem0016)),inference(skolemize,[status(esa)],[c31])).
% 158.48/158.78 cnf(c33,plain,model(skolem0017,skolem0016),inference(split_conjunct,[status(thm)],[c32])).
% 158.48/158.78 fof(thm,axiom,(![Ax]:(![C]:((![I1]:(model(I1,Ax)=>model(I1,C)))<=>status(Ax,C,thm)))),file('/export/starexec/sandbox/benchmark/Axioms/KRS001+0.ax', thm)).
% 158.48/158.78 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])).
% 158.48/158.78 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])).
% 158.48/158.78 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])).
% 158.48/158.78 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])).])).
% 158.48/158.78 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])).
% 158.48/158.78 cnf(c254,plain,~status(X578,X580,thm)|~model(X579,X578)|model(X579,X580),inference(split_conjunct,[status(thm)],[c251])).
% 158.48/158.78 fof(nota_unp_thm,conjecture,nota(unp,thm),file('/export/starexec/sandbox/benchmark/theBenchmark.p', nota_unp_thm)).
% 158.48/158.78 fof(c0,negated_conjecture,(~nota(unp,thm)),inference(assume_negation,[status(cth)],[nota_unp_thm])).
% 158.48/158.78 fof(c1,negated_conjecture,~nota(unp,thm),inference(fof_simplification,[status(thm)],[c0])).
% 158.48/158.78 cnf(c2,negated_conjecture,~nota(unp,thm),inference(split_conjunct,[status(thm)],[c1])).
% 158.48/158.78 fof(nota,axiom,(![S1]:(![S2]:((?[Ax]:(?[C]:(status(Ax,C,S1)&(~status(Ax,C,S2)))))<=>nota(S1,S2)))),file('/export/starexec/sandbox/benchmark/Axioms/KRS001+1.ax', nota)).
% 158.48/158.78 fof(c73,plain,(![S1]:(![S2]:((?[Ax]:(?[C]:(status(Ax,C,S1)&~status(Ax,C,S2))))<=>nota(S1,S2)))),inference(fof_simplification,[status(thm)],[nota])).
% 158.48/158.78 fof(c74,plain,(![S1]:(![S2]:(((![Ax]:(![C]:(~status(Ax,C,S1)|status(Ax,C,S2))))|nota(S1,S2))&(~nota(S1,S2)|(?[Ax]:(?[C]:(status(Ax,C,S1)&~status(Ax,C,S2)))))))),inference(fof_nnf,[status(thm)],[c73])).
% 158.48/158.78 fof(c75,plain,((![S1]:(![S2]:((![Ax]:(![C]:(~status(Ax,C,S1)|status(Ax,C,S2))))|nota(S1,S2))))&(![S1]:(![S2]:(~nota(S1,S2)|(?[Ax]:(?[C]:(status(Ax,C,S1)&~status(Ax,C,S2)))))))),inference(shift_quantors,[status(thm)],[c74])).
% 158.48/158.78 fof(c76,plain,((![X50]:(![X51]:((![X52]:(![X53]:(~status(X52,X53,X50)|status(X52,X53,X51))))|nota(X50,X51))))&(![X54]:(![X55]:(~nota(X54,X55)|(?[X56]:(?[X57]:(status(X56,X57,X54)&~status(X56,X57,X55)))))))),inference(variable_rename,[status(thm)],[c75])).
% 158.48/158.78 fof(c78,plain,(![X50]:(![X51]:(![X52]:(![X53]:(![X54]:(![X55]:(((~status(X52,X53,X50)|status(X52,X53,X51))|nota(X50,X51))&(~nota(X54,X55)|(status(skolem0024(X54,X55),skolem0025(X54,X55),X54)&~status(skolem0024(X54,X55),skolem0025(X54,X55),X55)))))))))),inference(shift_quantors,[status(thm)],[fof(c77,plain,((![X50]:(![X51]:((![X52]:(![X53]:(~status(X52,X53,X50)|status(X52,X53,X51))))|nota(X50,X51))))&(![X54]:(![X55]:(~nota(X54,X55)|(status(skolem0024(X54,X55),skolem0025(X54,X55),X54)&~status(skolem0024(X54,X55),skolem0025(X54,X55),X55)))))),inference(skolemize,[status(esa)],[c76])).])).
% 158.48/158.78 fof(c79,plain,(![X50]:(![X51]:(![X52]:(![X53]:(![X54]:(![X55]:(((~status(X52,X53,X50)|status(X52,X53,X51))|nota(X50,X51))&((~nota(X54,X55)|status(skolem0024(X54,X55),skolem0025(X54,X55),X54))&(~nota(X54,X55)|~status(skolem0024(X54,X55),skolem0025(X54,X55),X55)))))))))),inference(distribute,[status(thm)],[c78])).
% 158.48/158.78 cnf(c80,plain,~status(X324,X323,X322)|status(X324,X323,X321)|nota(X322,X321),inference(split_conjunct,[status(thm)],[c79])).
% 158.48/158.78 fof(unp,axiom,(![Ax]:(![C]:(((~(?[I1]:model(I1,Ax)))=>(~(?[I2]:model(I2,C))))<=>status(Ax,C,unp)))),file('/export/starexec/sandbox/benchmark/Axioms/KRS001+0.ax', unp)).
% 158.48/158.78 fof(c283,plain,(![Ax]:(![C]:((((![I1]:~model(I1,Ax))&(?[I2]:model(I2,C)))|status(Ax,C,unp))&(~status(Ax,C,unp)|((?[I1]:model(I1,Ax))|(![I2]:~model(I2,C))))))),inference(fof_nnf,[status(thm)],[unp])).
% 158.48/158.78 fof(c284,plain,((![Ax]:(![C]:(((![I1]:~model(I1,Ax))&(?[I2]:model(I2,C)))|status(Ax,C,unp))))&(![Ax]:(![C]:(~status(Ax,C,unp)|((?[I1]:model(I1,Ax))|(![I2]:~model(I2,C))))))),inference(shift_quantors,[status(thm)],[c283])).
% 158.48/158.78 fof(c285,plain,((![X228]:(![X229]:(((![X230]:~model(X230,X228))&(?[X231]:model(X231,X229)))|status(X228,X229,unp))))&(![X232]:(![X233]:(~status(X232,X233,unp)|((?[X234]:model(X234,X232))|(![X235]:~model(X235,X233))))))),inference(variable_rename,[status(thm)],[c284])).
% 158.48/158.78 fof(c287,plain,(![X228]:(![X229]:(![X230]:(![X232]:(![X233]:(![X235]:(((~model(X230,X228)&model(skolem0070(X228,X229),X229))|status(X228,X229,unp))&(~status(X232,X233,unp)|(model(skolem0071(X232,X233),X232)|~model(X235,X233)))))))))),inference(shift_quantors,[status(thm)],[fof(c286,plain,((![X228]:(![X229]:(((![X230]:~model(X230,X228))&model(skolem0070(X228,X229),X229))|status(X228,X229,unp))))&(![X232]:(![X233]:(~status(X232,X233,unp)|(model(skolem0071(X232,X233),X232)|(![X235]:~model(X235,X233))))))),inference(skolemize,[status(esa)],[c285])).])).
% 158.48/158.78 fof(c288,plain,(![X228]:(![X229]:(![X230]:(![X232]:(![X233]:(![X235]:(((~model(X230,X228)|status(X228,X229,unp))&(model(skolem0070(X228,X229),X229)|status(X228,X229,unp)))&(~status(X232,X233,unp)|(model(skolem0071(X232,X233),X232)|~model(X235,X233)))))))))),inference(distribute,[status(thm)],[c287])).
% 158.48/158.78 cnf(c289,plain,~model(X350,X349)|status(X349,X351,unp),inference(split_conjunct,[status(thm)],[c288])).
% 158.48/158.78 cnf(c445,plain,status(skolem0016,X352,unp),inference(resolution,[status(thm)],[c289, c33])).
% 158.48/158.78 cnf(c460,plain,status(skolem0016,X817,X816)|nota(unp,X816),inference(resolution,[status(thm)],[c445, c80])).
% 158.48/158.78 cnf(c4465,plain,status(skolem0016,X1329,thm),inference(resolution,[status(thm)],[c460, c2])).
% 158.48/158.78 cnf(c18981,plain,~model(X3333,skolem0016)|model(X3333,X3332),inference(resolution,[status(thm)],[c4465, c254])).
% 158.48/158.78 cnf(c150428,plain,model(skolem0017,X3334),inference(resolution,[status(thm)],[c18981, c33])).
% 158.48/158.78 cnf(c150562,plain,$false,inference(resolution,[status(thm)],[c150428, c18176])).
% 158.48/158.78 % SZS output end CNFRefutation
% 158.48/158.78
% 158.48/158.78 % Initial clauses : 109
% 158.48/158.78 % Processed clauses : 1592
% 158.48/158.78 % Factors computed : 196
% 158.48/158.78 % Resolvents computed: 150222
% 158.48/158.78 % Tautologies deleted: 14
% 158.48/158.78 % Forward subsumed : 5982
% 158.48/158.78 % Backward subsumed : 26
% 158.48/158.78 % -------- CPU Time ---------
% 158.48/158.78 % User time : 157.983 s
% 158.48/158.78 % System time : 0.354 s
% 158.48/158.78 % Total time : 158.337 s
%------------------------------------------------------------------------------