%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS255+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n004.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 7.67s 7.85s
% Output : Refutation 7.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : KRS255+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n004.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:05:53 EDT 2024
% 0.14/0.34 % CPUTime :
% 7.67/7.85 % Version: 1.5
% 7.67/7.85 % SZS status Theorem
% 7.67/7.85 % SZS output start CNFRefutation
% 7.67/7.85 fof(contradiction,axiom,(?[F]:(![I]:(~model(I,F)))),file('/export/starexec/sandbox/benchmark/Axioms/KRS001+1.ax', contradiction)).
% 7.67/7.85 fof(c26,plain,(?[F]:(![I]:~model(I,F))),inference(fof_simplification,[status(thm)],[contradiction])).
% 7.67/7.85 fof(c27,plain,(?[X17]:(![X18]:~model(X18,X17))),inference(variable_rename,[status(thm)],[c26])).
% 7.67/7.85 fof(c28,plain,(![X18]:~model(X18,skolem0015)),inference(skolemize,[status(esa)],[c27])).
% 7.67/7.85 cnf(c29,plain,~model(X236,skolem0015),inference(split_conjunct,[status(thm)],[c28])).
% 7.67/7.85 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)).
% 7.67/7.85 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])).
% 7.67/7.85 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])).
% 7.67/7.85 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])).
% 7.67/7.85 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])).])).
% 7.67/7.85 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])).
% 7.67/7.85 cnf(c252,plain,model(skolem0062(X574,X573),X574)|status(X574,X573,thm),inference(split_conjunct,[status(thm)],[c251])).
% 7.67/7.85 cnf(c1150,plain,status(skolem0015,X584,thm),inference(resolution,[status(thm)],[c252, c29])).
% 7.67/7.85 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/sandbox/benchmark/Axioms/KRS001+1.ax', mixed_pair)).
% 7.67/7.85 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])).
% 7.67/7.85 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])).
% 7.67/7.85 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])).
% 7.67/7.85 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])).])).
% 7.67/7.85 cnf(c14,plain,model(skolem0007,skolem0005),inference(split_conjunct,[status(thm)],[c13])).
% 7.67/7.85 fof(sap,axiom,(![Ax]:(![C]:(((?[I1]:model(I1,Ax))=>(?[I2]:model(I2,C)))<=>status(Ax,C,sap)))),file('/export/starexec/sandbox/benchmark/Axioms/KRS001+0.ax', sap)).
% 7.67/7.85 fof(c274,plain,(![Ax]:(![C]:((((?[I1]:model(I1,Ax))&(![I2]:~model(I2,C)))|status(Ax,C,sap))&(~status(Ax,C,sap)|((![I1]:~model(I1,Ax))|(?[I2]:model(I2,C))))))),inference(fof_nnf,[status(thm)],[sap])).
% 7.67/7.85 fof(c275,plain,((![Ax]:(![C]:(((?[I1]:model(I1,Ax))&(![I2]:~model(I2,C)))|status(Ax,C,sap))))&(![Ax]:(![C]:(~status(Ax,C,sap)|((![I1]:~model(I1,Ax))|(?[I2]:model(I2,C))))))),inference(shift_quantors,[status(thm)],[c274])).
% 7.67/7.85 fof(c276,plain,((![X220]:(![X221]:(((?[X222]:model(X222,X220))&(![X223]:~model(X223,X221)))|status(X220,X221,sap))))&(![X224]:(![X225]:(~status(X224,X225,sap)|((![X226]:~model(X226,X224))|(?[X227]:model(X227,X225))))))),inference(variable_rename,[status(thm)],[c275])).
% 7.67/7.85 fof(c278,plain,(![X220]:(![X221]:(![X223]:(![X224]:(![X225]:(![X226]:(((model(skolem0068(X220,X221),X220)&~model(X223,X221))|status(X220,X221,sap))&(~status(X224,X225,sap)|(~model(X226,X224)|model(skolem0069(X224,X225),X225)))))))))),inference(shift_quantors,[status(thm)],[fof(c277,plain,((![X220]:(![X221]:((model(skolem0068(X220,X221),X220)&(![X223]:~model(X223,X221)))|status(X220,X221,sap))))&(![X224]:(![X225]:(~status(X224,X225,sap)|((![X226]:~model(X226,X224))|model(skolem0069(X224,X225),X225)))))),inference(skolemize,[status(esa)],[c276])).])).
% 7.67/7.85 fof(c279,plain,(![X220]:(![X221]:(![X223]:(![X224]:(![X225]:(![X226]:(((model(skolem0068(X220,X221),X220)|status(X220,X221,sap))&(~model(X223,X221)|status(X220,X221,sap)))&(~status(X224,X225,sap)|(~model(X226,X224)|model(skolem0069(X224,X225),X225)))))))))),inference(distribute,[status(thm)],[c278])).
% 7.67/7.85 cnf(c281,plain,~model(X286,X287)|status(X285,X287,sap),inference(split_conjunct,[status(thm)],[c279])).
% 7.67/7.85 cnf(c320,plain,status(X303,skolem0005,sap),inference(resolution,[status(thm)],[c281, c14])).
% 7.67/7.85 fof(nevera,axiom,(![S1]:(![S2]:((![Ax]:(![C]:(status(Ax,C,S1)=>(~status(Ax,C,S2)))))<=>nevera(S1,S2)))),file('/export/starexec/sandbox/benchmark/Axioms/KRS001+1.ax', nevera)).
% 7.67/7.85 fof(c63,plain,(![S1]:(![S2]:((![Ax]:(![C]:(status(Ax,C,S1)=>~status(Ax,C,S2))))<=>nevera(S1,S2)))),inference(fof_simplification,[status(thm)],[nevera])).
% 7.67/7.85 fof(c64,plain,(![S1]:(![S2]:(((?[Ax]:(?[C]:(status(Ax,C,S1)&status(Ax,C,S2))))|nevera(S1,S2))&(~nevera(S1,S2)|(![Ax]:(![C]:(~status(Ax,C,S1)|~status(Ax,C,S2)))))))),inference(fof_nnf,[status(thm)],[c63])).
% 7.67/7.85 fof(c65,plain,((![S1]:(![S2]:((?[Ax]:(?[C]:(status(Ax,C,S1)&status(Ax,C,S2))))|nevera(S1,S2))))&(![S1]:(![S2]:(~nevera(S1,S2)|(![Ax]:(![C]:(~status(Ax,C,S1)|~status(Ax,C,S2)))))))),inference(shift_quantors,[status(thm)],[c64])).
% 7.67/7.85 fof(c66,plain,((![X42]:(![X43]:((?[X44]:(?[X45]:(status(X44,X45,X42)&status(X44,X45,X43))))|nevera(X42,X43))))&(![X46]:(![X47]:(~nevera(X46,X47)|(![X48]:(![X49]:(~status(X48,X49,X46)|~status(X48,X49,X47)))))))),inference(variable_rename,[status(thm)],[c65])).
% 7.67/7.85 fof(c68,plain,(![X42]:(![X43]:(![X46]:(![X47]:(![X48]:(![X49]:(((status(skolem0022(X42,X43),skolem0023(X42,X43),X42)&status(skolem0022(X42,X43),skolem0023(X42,X43),X43))|nevera(X42,X43))&(~nevera(X46,X47)|(~status(X48,X49,X46)|~status(X48,X49,X47)))))))))),inference(shift_quantors,[status(thm)],[fof(c67,plain,((![X42]:(![X43]:((status(skolem0022(X42,X43),skolem0023(X42,X43),X42)&status(skolem0022(X42,X43),skolem0023(X42,X43),X43))|nevera(X42,X43))))&(![X46]:(![X47]:(~nevera(X46,X47)|(![X48]:(![X49]:(~status(X48,X49,X46)|~status(X48,X49,X47)))))))),inference(skolemize,[status(esa)],[c66])).])).
% 7.67/7.85 fof(c69,plain,(![X42]:(![X43]:(![X46]:(![X47]:(![X48]:(![X49]:(((status(skolem0022(X42,X43),skolem0023(X42,X43),X42)|nevera(X42,X43))&(status(skolem0022(X42,X43),skolem0023(X42,X43),X43)|nevera(X42,X43)))&(~nevera(X46,X47)|(~status(X48,X49,X46)|~status(X48,X49,X47)))))))))),inference(distribute,[status(thm)],[c68])).
% 7.67/7.85 cnf(c72,plain,~nevera(X317,X319)|~status(X318,X320,X317)|~status(X318,X320,X319),inference(split_conjunct,[status(thm)],[c69])).
% 7.67/7.85 cnf(c375,plain,~nevera(X705,sap)|~status(X706,skolem0005,X705),inference(resolution,[status(thm)],[c72, c320])).
% 7.67/7.85 cnf(c2486,plain,~nevera(thm,sap),inference(resolution,[status(thm)],[c375, c1150])).
% 7.67/7.85 cnf(c71,plain,status(skolem0022(X316,X315),skolem0023(X316,X315),X315)|nevera(X316,X315),inference(split_conjunct,[status(thm)],[c69])).
% 7.67/7.85 cnf(c70,plain,status(skolem0022(X309,X308),skolem0023(X309,X308),X309)|nevera(X309,X308),inference(split_conjunct,[status(thm)],[c69])).
% 7.67/7.85 cnf(c388,plain,~nevera(X732,X734)|~status(skolem0022(X734,X733),skolem0023(X734,X733),X732)|nevera(X734,X733),inference(resolution,[status(thm)],[c72, c70])).
% 7.67/7.85 cnf(c2835,plain,~nevera(X1363,X1364)|nevera(X1364,X1363),inference(resolution,[status(thm)],[c388, c71])).
% 7.67/7.85 fof(mighta_sap_thm,conjecture,mighta(sap,thm),file('/export/starexec/sandbox/benchmark/theBenchmark.p', mighta_sap_thm)).
% 7.67/7.85 fof(c0,negated_conjecture,(~mighta(sap,thm)),inference(assume_negation,[status(cth)],[mighta_sap_thm])).
% 7.67/7.85 fof(c1,negated_conjecture,~mighta(sap,thm),inference(fof_simplification,[status(thm)],[c0])).
% 7.67/7.85 cnf(c2,negated_conjecture,~mighta(sap,thm),inference(split_conjunct,[status(thm)],[c1])).
% 7.67/7.85 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)).
% 7.67/7.85 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])).
% 7.67/7.85 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])).
% 7.67/7.85 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])).
% 7.67/7.85 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])).])).
% 7.67/7.85 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])).
% 7.67/7.85 cnf(c98,plain,~status(X362,X361,X360)|~status(X362,X361,X359)|mighta(X360,X359),inference(split_conjunct,[status(thm)],[c97])).
% 7.67/7.85 cnf(c500,plain,~status(skolem0022(X883,X882),skolem0023(X883,X882),X881)|mighta(X881,X882)|nevera(X883,X882),inference(resolution,[status(thm)],[c98, c71])).
% 7.67/7.85 cnf(c5146,plain,mighta(X1412,X1411)|nevera(X1412,X1411),inference(resolution,[status(thm)],[c500, c70])).
% 7.67/7.85 cnf(c19680,plain,nevera(sap,thm),inference(resolution,[status(thm)],[c5146, c2])).
% 7.67/7.85 cnf(c19698,plain,nevera(thm,sap),inference(resolution,[status(thm)],[c19680, c2835])).
% 7.67/7.85 cnf(c19897,plain,$false,inference(resolution,[status(thm)],[c19698, c2486])).
% 7.67/7.85 % SZS output end CNFRefutation
% 7.67/7.85
% 7.67/7.85 % Initial clauses : 109
% 7.67/7.85 % Processed clauses : 627
% 7.67/7.85 % Factors computed : 55
% 7.67/7.85 % Resolvents computed: 19552
% 7.67/7.85 % Tautologies deleted: 5
% 7.67/7.85 % Forward subsumed : 2058
% 7.67/7.85 % Backward subsumed : 0
% 7.67/7.85 % -------- CPU Time ---------
% 7.67/7.85 % User time : 7.458 s
% 7.67/7.85 % System time : 0.053 s
% 7.67/7.85 % Total time : 7.511 s
%------------------------------------------------------------------------------