%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS201+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n010.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 179.12s 179.33s
% Output : Refutation 179.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS201+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n010.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 9 00:09:38 EDT 2024
% 0.12/0.34 % CPUTime :
% 179.12/179.33 % Version: 1.5
% 179.12/179.33 % SZS status Theorem
% 179.12/179.33 % SZS output start CNFRefutation
% 179.12/179.33 fof(sat_non_taut_pair,axiom,(?[Ax]:(?[C]:((?[I1]:(model(I1,Ax)&model(I1,C)))&(?[I2]:((~model(I2,Ax))|(~model(I2,C))))))),file('/export/starexec/sandbox2/benchmark/Axioms/KRS001+1.ax', sat_non_taut_pair)).
% 179.12/179.33 fof(c19,plain,(?[Ax]:(?[C]:((?[I1]:(model(I1,Ax)&model(I1,C)))&(?[I2]:(~model(I2,Ax)|~model(I2,C)))))),inference(fof_simplification,[status(thm)],[sat_non_taut_pair])).
% 179.12/179.33 fof(c20,plain,(?[Ax]:(?[C]:((?[I1]:(model(I1,Ax)&model(I1,C)))&((?[I2]:~model(I2,Ax))|(?[I2]:~model(I2,C)))))),inference(shift_quantors,[status(thm)],[c19])).
% 179.12/179.33 fof(c21,plain,(?[X12]:(?[X13]:((?[X14]:(model(X14,X12)&model(X14,X13)))&((?[X15]:~model(X15,X12))|(?[X16]:~model(X16,X13)))))),inference(variable_rename,[status(thm)],[c20])).
% 179.12/179.33 fof(c22,plain,((model(skolem0012,skolem0010)&model(skolem0012,skolem0011))&(~model(skolem0013,skolem0010)|~model(skolem0014,skolem0011))),inference(skolemize,[status(esa)],[c21])).
% 179.12/179.33 cnf(c25,plain,~model(skolem0013,skolem0010)|~model(skolem0014,skolem0011),inference(split_conjunct,[status(thm)],[c22])).
% 179.12/179.33 fof(contradiction,axiom,(?[F]:(![I]:(~model(I,F)))),file('/export/starexec/sandbox2/benchmark/Axioms/KRS001+1.ax', contradiction)).
% 179.12/179.33 fof(c26,plain,(?[F]:(![I]:~model(I,F))),inference(fof_simplification,[status(thm)],[contradiction])).
% 179.12/179.33 fof(c27,plain,(?[X17]:(![X18]:~model(X18,X17))),inference(variable_rename,[status(thm)],[c26])).
% 179.12/179.33 fof(c28,plain,(![X18]:~model(X18,skolem0015)),inference(skolemize,[status(esa)],[c27])).
% 179.12/179.33 cnf(c29,plain,~model(X236,skolem0015),inference(split_conjunct,[status(thm)],[c28])).
% 179.12/179.33 fof(not,axiom,(![I]:(![F]:(model(I,F)<=>(~model(I,not(F)))))),file('/export/starexec/sandbox2/benchmark/Axioms/KRS001+1.ax', not)).
% 179.12/179.33 fof(c38,plain,(![I]:(![F]:(model(I,F)<=>~model(I,not(F))))),inference(fof_simplification,[status(thm)],[not])).
% 179.12/179.33 fof(c39,plain,(![I]:(![F]:((~model(I,F)|~model(I,not(F)))&(model(I,not(F))|model(I,F))))),inference(fof_nnf,[status(thm)],[c38])).
% 179.12/179.33 fof(c40,plain,((![I]:(![F]:(~model(I,F)|~model(I,not(F)))))&(![I]:(![F]:(model(I,not(F))|model(I,F))))),inference(shift_quantors,[status(thm)],[c39])).
% 179.12/179.33 fof(c42,plain,(![X24]:(![X25]:(![X26]:(![X27]:((~model(X24,X25)|~model(X24,not(X25)))&(model(X26,not(X27))|model(X26,X27))))))),inference(shift_quantors,[status(thm)],[fof(c41,plain,((![X24]:(![X25]:(~model(X24,X25)|~model(X24,not(X25)))))&(![X26]:(![X27]:(model(X26,not(X27))|model(X26,X27))))),inference(variable_rename,[status(thm)],[c40])).])).
% 179.12/179.33 cnf(c44,plain,model(X242,not(X241))|model(X242,X241),inference(split_conjunct,[status(thm)],[c42])).
% 179.12/179.33 cnf(c300,plain,model(X243,not(skolem0015)),inference(resolution,[status(thm)],[c44, c29])).
% 179.12/179.33 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)).
% 179.12/179.33 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])).
% 179.12/179.33 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])).
% 179.12/179.33 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])).
% 179.12/179.33 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])).])).
% 179.12/179.33 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])).
% 179.12/179.33 cnf(c254,plain,~status(X580,X578,thm)|~model(X579,X580)|model(X579,X578),inference(split_conjunct,[status(thm)],[c251])).
% 179.12/179.33 fof(nota_sap_thm,conjecture,nota(sap,thm),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', nota_sap_thm)).
% 179.12/179.33 fof(c0,negated_conjecture,(~nota(sap,thm)),inference(assume_negation,[status(cth)],[nota_sap_thm])).
% 179.12/179.33 fof(c1,negated_conjecture,~nota(sap,thm),inference(fof_simplification,[status(thm)],[c0])).
% 179.12/179.33 cnf(c2,negated_conjecture,~nota(sap,thm),inference(split_conjunct,[status(thm)],[c1])).
% 179.12/179.33 cnf(c24,plain,model(skolem0012,skolem0011),inference(split_conjunct,[status(thm)],[c22])).
% 179.12/179.33 fof(sap,axiom,(![Ax]:(![C]:(((?[I1]:model(I1,Ax))=>(?[I2]:model(I2,C)))<=>status(Ax,C,sap)))),file('/export/starexec/sandbox2/benchmark/Axioms/KRS001+0.ax', sap)).
% 179.12/179.33 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])).
% 179.12/179.33 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])).
% 179.12/179.33 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])).
% 179.12/179.33 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])).])).
% 179.12/179.33 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])).
% 179.12/179.33 cnf(c281,plain,~model(X285,X287)|status(X286,X287,sap),inference(split_conjunct,[status(thm)],[c279])).
% 179.12/179.33 cnf(c307,plain,status(X288,skolem0011,sap),inference(resolution,[status(thm)],[c281, c24])).
% 179.12/179.33 fof(nota,axiom,(![S1]:(![S2]:((?[Ax]:(?[C]:(status(Ax,C,S1)&(~status(Ax,C,S2)))))<=>nota(S1,S2)))),file('/export/starexec/sandbox2/benchmark/Axioms/KRS001+1.ax', nota)).
% 179.12/179.33 fof(c73,plain,(![S1]:(![S2]:((?[Ax]:(?[C]:(status(Ax,C,S1)&~status(Ax,C,S2))))<=>nota(S1,S2)))),inference(fof_simplification,[status(thm)],[nota])).
% 179.12/179.33 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])).
% 179.12/179.33 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])).
% 179.12/179.33 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])).
% 179.12/179.33 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])).])).
% 179.12/179.33 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])).
% 179.12/179.33 cnf(c80,plain,~status(X323,X321,X322)|status(X323,X321,X324)|nota(X322,X324),inference(split_conjunct,[status(thm)],[c79])).
% 179.12/179.33 cnf(c393,plain,status(X745,skolem0011,X746)|nota(sap,X746),inference(resolution,[status(thm)],[c80, c307])).
% 179.12/179.33 cnf(c3109,plain,status(X1331,skolem0011,thm),inference(resolution,[status(thm)],[c393, c2])).
% 179.12/179.33 cnf(c18969,plain,~model(X3263,X3262)|model(X3263,skolem0011),inference(resolution,[status(thm)],[c3109, c254])).
% 179.12/179.33 cnf(c145075,plain,model(X3264,skolem0011),inference(resolution,[status(thm)],[c18969, c300])).
% 179.12/179.33 cnf(c145512,plain,~model(skolem0013,skolem0010),inference(resolution,[status(thm)],[c145075, c25])).
% 179.12/179.33 cnf(c23,plain,model(skolem0012,skolem0010),inference(split_conjunct,[status(thm)],[c22])).
% 179.12/179.33 cnf(c314,plain,status(X297,skolem0010,sap),inference(resolution,[status(thm)],[c281, c23])).
% 179.12/179.33 cnf(c395,plain,status(X750,skolem0010,X751)|nota(sap,X751),inference(resolution,[status(thm)],[c80, c314])).
% 179.12/179.33 cnf(c3234,plain,status(X1350,skolem0010,thm),inference(resolution,[status(thm)],[c395, c2])).
% 179.12/179.33 cnf(c19601,plain,~model(X3462,X3461)|model(X3462,skolem0010),inference(resolution,[status(thm)],[c3234, c254])).
% 179.12/179.33 cnf(c158273,plain,model(X3463,skolem0010),inference(resolution,[status(thm)],[c19601, c300])).
% 179.12/179.33 cnf(c158744,plain,$false,inference(resolution,[status(thm)],[c158273, c145512])).
% 179.12/179.33 % SZS output end CNFRefutation
% 179.12/179.33
% 179.12/179.33 % Initial clauses : 109
% 179.12/179.33 % Processed clauses : 1654
% 179.12/179.33 % Factors computed : 197
% 179.12/179.33 % Resolvents computed: 158789
% 179.12/179.33 % Tautologies deleted: 14
% 179.12/179.33 % Forward subsumed : 6186
% 179.12/179.33 % Backward subsumed : 45
% 179.12/179.33 % -------- CPU Time ---------
% 179.12/179.33 % User time : 178.540 s
% 179.12/179.33 % System time : 0.446 s
% 179.12/179.33 % Total time : 178.986 s
%------------------------------------------------------------------------------