%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS195+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n029.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 23.68s 23.95s
% Output : Refutation 23.68s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : KRS195+1 : TPTP v8.1.2. Bugfixed v5.4.0.
% 0.04/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n029.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 9 00:07:53 EDT 2024
% 0.14/0.35 % CPUTime :
% 23.68/23.95 % Version: 1.5
% 23.68/23.95 % SZS status Theorem
% 23.68/23.95 % SZS output start CNFRefutation
% 23.68/23.95 fof(isa_tca_thm,conjecture,isa(tca,thm),file('/export/starexec/sandbox/benchmark/theBenchmark.p', isa_tca_thm)).
% 23.68/23.95 fof(c0,negated_conjecture,(~isa(tca,thm)),inference(assume_negation,[status(cth)],[isa_tca_thm])).
% 23.68/23.95 fof(c1,negated_conjecture,~isa(tca,thm),inference(fof_simplification,[status(thm)],[c0])).
% 23.68/23.95 cnf(c2,negated_conjecture,~isa(tca,thm),inference(split_conjunct,[status(thm)],[c1])).
% 23.68/23.95 fof(tca,axiom,(![Ax]:(![C]:(((~(?[I1]:model(I1,Ax)))&(![I2]:model(I2,C)))<=>status(Ax,C,tca)))),file('/export/starexec/sandbox/benchmark/Axioms/KRS001+0.ax', tca)).
% 23.68/23.95 fof(c141,plain,(![Ax]:(![C]:((((?[I1]:model(I1,Ax))|(?[I2]:~model(I2,C)))|status(Ax,C,tca))&(~status(Ax,C,tca)|((![I1]:~model(I1,Ax))&(![I2]:model(I2,C))))))),inference(fof_nnf,[status(thm)],[tca])).
% 23.68/23.95 fof(c142,plain,((![Ax]:(![C]:(((?[I1]:model(I1,Ax))|(?[I2]:~model(I2,C)))|status(Ax,C,tca))))&(![Ax]:(![C]:(~status(Ax,C,tca)|((![I1]:~model(I1,Ax))&(![I2]:model(I2,C))))))),inference(shift_quantors,[status(thm)],[c141])).
% 23.68/23.95 fof(c143,plain,((![X106]:(![X107]:(((?[X108]:model(X108,X106))|(?[X109]:~model(X109,X107)))|status(X106,X107,tca))))&(![X110]:(![X111]:(~status(X110,X111,tca)|((![X112]:~model(X112,X110))&(![X113]:model(X113,X111))))))),inference(variable_rename,[status(thm)],[c142])).
% 23.68/23.95 fof(c145,plain,(![X106]:(![X107]:(![X110]:(![X111]:(![X112]:(![X113]:(((model(skolem0038(X106,X107),X106)|~model(skolem0039(X106,X107),X107))|status(X106,X107,tca))&(~status(X110,X111,tca)|(~model(X112,X110)&model(X113,X111)))))))))),inference(shift_quantors,[status(thm)],[fof(c144,plain,((![X106]:(![X107]:((model(skolem0038(X106,X107),X106)|~model(skolem0039(X106,X107),X107))|status(X106,X107,tca))))&(![X110]:(![X111]:(~status(X110,X111,tca)|((![X112]:~model(X112,X110))&(![X113]:model(X113,X111))))))),inference(skolemize,[status(esa)],[c143])).])).
% 23.68/23.95 fof(c146,plain,(![X106]:(![X107]:(![X110]:(![X111]:(![X112]:(![X113]:(((model(skolem0038(X106,X107),X106)|~model(skolem0039(X106,X107),X107))|status(X106,X107,tca))&((~status(X110,X111,tca)|~model(X112,X110))&(~status(X110,X111,tca)|model(X113,X111)))))))))),inference(distribute,[status(thm)],[c145])).
% 23.68/23.95 cnf(c148,plain,~status(X258,X259,tca)|~model(X257,X258),inference(split_conjunct,[status(thm)],[c146])).
% 23.68/23.95 fof(isa,axiom,(![S1]:(![S2]:((![Ax]:(![C]:(status(Ax,C,S1)=>status(Ax,C,S2))))<=>isa(S1,S2)))),file('/export/starexec/sandbox/benchmark/Axioms/KRS001+1.ax', isa)).
% 23.68/23.95 fof(c83,plain,(![S1]:(![S2]:(((?[Ax]:(?[C]:(status(Ax,C,S1)&~status(Ax,C,S2))))|isa(S1,S2))&(~isa(S1,S2)|(![Ax]:(![C]:(~status(Ax,C,S1)|status(Ax,C,S2)))))))),inference(fof_nnf,[status(thm)],[isa])).
% 23.68/23.95 fof(c84,plain,((![S1]:(![S2]:((?[Ax]:(?[C]:(status(Ax,C,S1)&~status(Ax,C,S2))))|isa(S1,S2))))&(![S1]:(![S2]:(~isa(S1,S2)|(![Ax]:(![C]:(~status(Ax,C,S1)|status(Ax,C,S2)))))))),inference(shift_quantors,[status(thm)],[c83])).
% 23.68/23.95 fof(c85,plain,((![X58]:(![X59]:((?[X60]:(?[X61]:(status(X60,X61,X58)&~status(X60,X61,X59))))|isa(X58,X59))))&(![X62]:(![X63]:(~isa(X62,X63)|(![X64]:(![X65]:(~status(X64,X65,X62)|status(X64,X65,X63)))))))),inference(variable_rename,[status(thm)],[c84])).
% 23.68/23.95 fof(c87,plain,(![X58]:(![X59]:(![X62]:(![X63]:(![X64]:(![X65]:(((status(skolem0026(X58,X59),skolem0027(X58,X59),X58)&~status(skolem0026(X58,X59),skolem0027(X58,X59),X59))|isa(X58,X59))&(~isa(X62,X63)|(~status(X64,X65,X62)|status(X64,X65,X63)))))))))),inference(shift_quantors,[status(thm)],[fof(c86,plain,((![X58]:(![X59]:((status(skolem0026(X58,X59),skolem0027(X58,X59),X58)&~status(skolem0026(X58,X59),skolem0027(X58,X59),X59))|isa(X58,X59))))&(![X62]:(![X63]:(~isa(X62,X63)|(![X64]:(![X65]:(~status(X64,X65,X62)|status(X64,X65,X63)))))))),inference(skolemize,[status(esa)],[c85])).])).
% 23.68/23.95 fof(c88,plain,(![X58]:(![X59]:(![X62]:(![X63]:(![X64]:(![X65]:(((status(skolem0026(X58,X59),skolem0027(X58,X59),X58)|isa(X58,X59))&(~status(skolem0026(X58,X59),skolem0027(X58,X59),X59)|isa(X58,X59)))&(~isa(X62,X63)|(~status(X64,X65,X62)|status(X64,X65,X63)))))))))),inference(distribute,[status(thm)],[c87])).
% 23.68/23.95 cnf(c89,plain,status(skolem0026(X336,X337),skolem0027(X336,X337),X336)|isa(X336,X337),inference(split_conjunct,[status(thm)],[c88])).
% 23.68/23.95 cnf(c437,plain,status(skolem0026(tca,thm),skolem0027(tca,thm),tca),inference(resolution,[status(thm)],[c89, c2])).
% 23.68/23.95 cnf(c4049,plain,~model(X1722,skolem0026(tca,thm)),inference(resolution,[status(thm)],[c437, c148])).
% 23.68/23.95 cnf(c90,plain,~status(skolem0026(X344,X345),skolem0027(X344,X345),X345)|isa(X344,X345),inference(split_conjunct,[status(thm)],[c88])).
% 23.68/23.95 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)).
% 23.68/23.95 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])).
% 23.68/23.95 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])).
% 23.68/23.95 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])).
% 23.68/23.95 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])).])).
% 23.68/23.95 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])).
% 23.68/23.95 cnf(c252,plain,model(skolem0062(X573,X574),X573)|status(X573,X574,thm),inference(split_conjunct,[status(thm)],[c251])).
% 23.68/23.95 cnf(c1175,plain,model(skolem0062(skolem0026(X2043,thm),skolem0027(X2043,thm)),skolem0026(X2043,thm))|isa(X2043,thm),inference(resolution,[status(thm)],[c252, c90])).
% 23.68/23.95 cnf(c49363,plain,isa(tca,thm),inference(resolution,[status(thm)],[c1175, c4049])).
% 23.68/23.95 cnf(c49485,plain,$false,inference(resolution,[status(thm)],[c49363, c2])).
% 23.68/23.95 % SZS output end CNFRefutation
% 23.68/23.95
% 23.68/23.95 % Initial clauses : 109
% 23.68/23.95 % Processed clauses : 1003
% 23.68/23.95 % Factors computed : 135
% 23.68/23.95 % Resolvents computed: 49060
% 23.68/23.95 % Tautologies deleted: 7
% 23.68/23.95 % Forward subsumed : 2851
% 23.68/23.95 % Backward subsumed : 0
% 23.68/23.95 % -------- CPU Time ---------
% 23.68/23.95 % User time : 23.457 s
% 23.68/23.95 % System time : 0.117 s
% 23.68/23.95 % Total time : 23.574 s
%------------------------------------------------------------------------------