%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS083+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n012.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:39 EDT 2024
% Result : Unsatisfiable 0.75s 0.93s
% Output : Refutation 0.75s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : KRS083+1 : TPTP v8.1.2. Released v3.1.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n012.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 9 00:13:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.75/0.93 % Version: 1.5
% 0.75/0.93 % SZS status Unsatisfiable
% 0.75/0.93 % SZS output start CNFRefutation
% 0.75/0.93 fof(axiom_8,axiom,cUnsatisfiable(i2003_11_14_17_19_32337),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_8)).
% 0.75/0.93 cnf(c14,plain,cUnsatisfiable(i2003_11_14_17_19_32337),inference(split_conjunct,[status(thm)],[axiom_8])).
% 0.75/0.93 fof(axiom_6,axiom,(![X]:(![Y]:(rinvR(X,Y)<=>rr(Y,X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_6)).
% 0.75/0.93 fof(c18,plain,(![X]:(![Y]:((~rinvR(X,Y)|rr(Y,X))&(~rr(Y,X)|rinvR(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 0.75/0.93 fof(c19,plain,((![X]:(![Y]:(~rinvR(X,Y)|rr(Y,X))))&(![X]:(![Y]:(~rr(Y,X)|rinvR(X,Y))))),inference(shift_quantors,[status(thm)],[c18])).
% 0.75/0.93 fof(c21,plain,(![X7]:(![X8]:(![X9]:(![X10]:((~rinvR(X7,X8)|rr(X8,X7))&(~rr(X10,X9)|rinvR(X9,X10))))))),inference(shift_quantors,[status(thm)],[fof(c20,plain,((![X7]:(![X8]:(~rinvR(X7,X8)|rr(X8,X7))))&(![X9]:(![X10]:(~rr(X10,X9)|rinvR(X9,X10))))),inference(variable_rename,[status(thm)],[c19])).])).
% 0.75/0.93 cnf(c23,plain,~rr(X91,X90)|rinvR(X90,X91),inference(split_conjunct,[status(thm)],[c21])).
% 0.75/0.93 fof(axiom_9,axiom,(![X]:(![Y]:(rf(X,Y)=>rr(X,Y)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_9)).
% 0.75/0.93 fof(c11,plain,(![X]:(![Y]:(~rf(X,Y)|rr(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_9])).
% 0.75/0.93 fof(c12,plain,(![X2]:(![X3]:(~rf(X2,X3)|rr(X2,X3)))),inference(variable_rename,[status(thm)],[c11])).
% 0.75/0.93 cnf(c13,plain,~rf(X87,X86)|rr(X87,X86),inference(split_conjunct,[status(thm)],[c12])).
% 0.75/0.93 fof(axiom_5,axiom,(![X]:(![Y]:(rinvF(X,Y)<=>rf(Y,X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_5)).
% 0.75/0.93 fof(c24,plain,(![X]:(![Y]:((~rinvF(X,Y)|rf(Y,X))&(~rf(Y,X)|rinvF(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.75/0.93 fof(c25,plain,((![X]:(![Y]:(~rinvF(X,Y)|rf(Y,X))))&(![X]:(![Y]:(~rf(Y,X)|rinvF(X,Y))))),inference(shift_quantors,[status(thm)],[c24])).
% 0.75/0.93 fof(c27,plain,(![X11]:(![X12]:(![X13]:(![X14]:((~rinvF(X11,X12)|rf(X12,X11))&(~rf(X14,X13)|rinvF(X13,X14))))))),inference(shift_quantors,[status(thm)],[fof(c26,plain,((![X11]:(![X12]:(~rinvF(X11,X12)|rf(X12,X11))))&(![X13]:(![X14]:(~rf(X14,X13)|rinvF(X13,X14))))),inference(variable_rename,[status(thm)],[c25])).])).
% 0.75/0.93 cnf(c28,plain,~rinvF(X92,X93)|rf(X93,X92),inference(split_conjunct,[status(thm)],[c27])).
% 0.75/0.93 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)<=>(((![Y]:(rinvR(X,Y)=>(?[Z]:(rinvF(Y,Z)&cd(Z)))))&(~cc(X)))&(?[Y]:(rinvF(X,Y)&cd(Y)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 0.75/0.93 fof(c45,plain,(![X]:(cUnsatisfiable(X)<=>(((![Y]:(rinvR(X,Y)=>(?[Z]:(rinvF(Y,Z)&cd(Z)))))&~cc(X))&(?[Y]:(rinvF(X,Y)&cd(Y)))))),inference(fof_simplification,[status(thm)],[axiom_2])).
% 0.75/0.93 fof(c46,plain,(![X]:((~cUnsatisfiable(X)|(((![Y]:(~rinvR(X,Y)|(?[Z]:(rinvF(Y,Z)&cd(Z)))))&~cc(X))&(?[Y]:(rinvF(X,Y)&cd(Y)))))&((((?[Y]:(rinvR(X,Y)&(![Z]:(~rinvF(Y,Z)|~cd(Z)))))|cc(X))|(![Y]:(~rinvF(X,Y)|~cd(Y))))|cUnsatisfiable(X)))),inference(fof_nnf,[status(thm)],[c45])).
% 0.75/0.93 fof(c47,plain,((![X]:(~cUnsatisfiable(X)|(((![Y]:(~rinvR(X,Y)|(?[Z]:(rinvF(Y,Z)&cd(Z)))))&~cc(X))&(?[Y]:(rinvF(X,Y)&cd(Y))))))&(![X]:((((?[Y]:(rinvR(X,Y)&(![Z]:(~rinvF(Y,Z)|~cd(Z)))))|cc(X))|(![Y]:(~rinvF(X,Y)|~cd(Y))))|cUnsatisfiable(X)))),inference(shift_quantors,[status(thm)],[c46])).
% 0.75/0.93 fof(c48,plain,((![X22]:(~cUnsatisfiable(X22)|(((![X23]:(~rinvR(X22,X23)|(?[X24]:(rinvF(X23,X24)&cd(X24)))))&~cc(X22))&(?[X25]:(rinvF(X22,X25)&cd(X25))))))&(![X26]:((((?[X27]:(rinvR(X26,X27)&(![X28]:(~rinvF(X27,X28)|~cd(X28)))))|cc(X26))|(![X29]:(~rinvF(X26,X29)|~cd(X29))))|cUnsatisfiable(X26)))),inference(variable_rename,[status(thm)],[c47])).
% 0.75/0.93 fof(c50,plain,(![X22]:(![X23]:(![X26]:(![X28]:(![X29]:((~cUnsatisfiable(X22)|(((~rinvR(X22,X23)|(rinvF(X23,skolem0002(X22,X23))&cd(skolem0002(X22,X23))))&~cc(X22))&(rinvF(X22,skolem0003(X22))&cd(skolem0003(X22)))))&((((rinvR(X26,skolem0004(X26))&(~rinvF(skolem0004(X26),X28)|~cd(X28)))|cc(X26))|(~rinvF(X26,X29)|~cd(X29)))|cUnsatisfiable(X26)))))))),inference(shift_quantors,[status(thm)],[fof(c49,plain,((![X22]:(~cUnsatisfiable(X22)|(((![X23]:(~rinvR(X22,X23)|(rinvF(X23,skolem0002(X22,X23))&cd(skolem0002(X22,X23)))))&~cc(X22))&(rinvF(X22,skolem0003(X22))&cd(skolem0003(X22))))))&(![X26]:((((rinvR(X26,skolem0004(X26))&(![X28]:(~rinvF(skolem0004(X26),X28)|~cd(X28))))|cc(X26))|(![X29]:(~rinvF(X26,X29)|~cd(X29))))|cUnsatisfiable(X26)))),inference(skolemize,[status(esa)],[c48])).])).
% 0.75/0.93 fof(c51,plain,(![X22]:(![X23]:(![X26]:(![X28]:(![X29]:(((((~cUnsatisfiable(X22)|(~rinvR(X22,X23)|rinvF(X23,skolem0002(X22,X23))))&(~cUnsatisfiable(X22)|(~rinvR(X22,X23)|cd(skolem0002(X22,X23)))))&(~cUnsatisfiable(X22)|~cc(X22)))&((~cUnsatisfiable(X22)|rinvF(X22,skolem0003(X22)))&(~cUnsatisfiable(X22)|cd(skolem0003(X22)))))&((((rinvR(X26,skolem0004(X26))|cc(X26))|(~rinvF(X26,X29)|~cd(X29)))|cUnsatisfiable(X26))&((((~rinvF(skolem0004(X26),X28)|~cd(X28))|cc(X26))|(~rinvF(X26,X29)|~cd(X29)))|cUnsatisfiable(X26))))))))),inference(distribute,[status(thm)],[c50])).
% 0.75/0.93 cnf(c55,plain,~cUnsatisfiable(X111)|rinvF(X111,skolem0003(X111)),inference(split_conjunct,[status(thm)],[c51])).
% 0.75/0.93 cnf(c128,plain,rinvF(i2003_11_14_17_19_32337,skolem0003(i2003_11_14_17_19_32337)),inference(resolution,[status(thm)],[c55, c14])).
% 0.75/0.93 cnf(c129,plain,rf(skolem0003(i2003_11_14_17_19_32337),i2003_11_14_17_19_32337),inference(resolution,[status(thm)],[c128, c28])).
% 0.75/0.93 cnf(c131,plain,rr(skolem0003(i2003_11_14_17_19_32337),i2003_11_14_17_19_32337),inference(resolution,[status(thm)],[c129, c13])).
% 0.75/0.93 cnf(c132,plain,rinvR(i2003_11_14_17_19_32337,skolem0003(i2003_11_14_17_19_32337)),inference(resolution,[status(thm)],[c131, c23])).
% 0.75/0.93 cnf(c53,plain,~cUnsatisfiable(X196)|~rinvR(X196,X197)|cd(skolem0002(X196,X197)),inference(split_conjunct,[status(thm)],[c51])).
% 0.75/0.93 cnf(c167,plain,~cUnsatisfiable(i2003_11_14_17_19_32337)|cd(skolem0002(i2003_11_14_17_19_32337,skolem0003(i2003_11_14_17_19_32337))),inference(resolution,[status(thm)],[c53, c132])).
% 0.75/0.93 cnf(c187,plain,cd(skolem0002(i2003_11_14_17_19_32337,skolem0003(i2003_11_14_17_19_32337))),inference(resolution,[status(thm)],[c167, c14])).
% 0.75/0.93 fof(axiom_3,axiom,(![X]:(cd(X)<=>((?[Y]:(rf(X,Y)&(~cc(Y))))&cc(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_3)).
% 0.75/0.93 fof(c34,plain,(![X]:(cd(X)<=>((?[Y]:(rf(X,Y)&~cc(Y)))&cc(X)))),inference(fof_simplification,[status(thm)],[axiom_3])).
% 0.75/0.93 fof(c35,plain,(![X]:((~cd(X)|((?[Y]:(rf(X,Y)&~cc(Y)))&cc(X)))&(((![Y]:(~rf(X,Y)|cc(Y)))|~cc(X))|cd(X)))),inference(fof_nnf,[status(thm)],[c34])).
% 0.75/0.93 fof(c36,plain,((![X]:(~cd(X)|((?[Y]:(rf(X,Y)&~cc(Y)))&cc(X))))&(![X]:(((![Y]:(~rf(X,Y)|cc(Y)))|~cc(X))|cd(X)))),inference(shift_quantors,[status(thm)],[c35])).
% 0.75/0.93 fof(c37,plain,((![X18]:(~cd(X18)|((?[X19]:(rf(X18,X19)&~cc(X19)))&cc(X18))))&(![X20]:(((![X21]:(~rf(X20,X21)|cc(X21)))|~cc(X20))|cd(X20)))),inference(variable_rename,[status(thm)],[c36])).
% 0.75/0.93 fof(c39,plain,(![X18]:(![X20]:(![X21]:((~cd(X18)|((rf(X18,skolem0001(X18))&~cc(skolem0001(X18)))&cc(X18)))&(((~rf(X20,X21)|cc(X21))|~cc(X20))|cd(X20)))))),inference(shift_quantors,[status(thm)],[fof(c38,plain,((![X18]:(~cd(X18)|((rf(X18,skolem0001(X18))&~cc(skolem0001(X18)))&cc(X18))))&(![X20]:(((![X21]:(~rf(X20,X21)|cc(X21)))|~cc(X20))|cd(X20)))),inference(skolemize,[status(esa)],[c37])).])).
% 0.75/0.93 fof(c40,plain,(![X18]:(![X20]:(![X21]:((((~cd(X18)|rf(X18,skolem0001(X18)))&(~cd(X18)|~cc(skolem0001(X18))))&(~cd(X18)|cc(X18)))&(((~rf(X20,X21)|cc(X21))|~cc(X20))|cd(X20)))))),inference(distribute,[status(thm)],[c39])).
% 0.75/0.93 cnf(c42,plain,~cd(X99)|~cc(skolem0001(X99)),inference(split_conjunct,[status(thm)],[c40])).
% 0.75/0.93 cnf(c43,plain,~cd(X75)|cc(X75),inference(split_conjunct,[status(thm)],[c40])).
% 0.75/0.93 cnf(c56,plain,~cUnsatisfiable(X100)|cd(skolem0003(X100)),inference(split_conjunct,[status(thm)],[c51])).
% 0.75/0.93 cnf(c122,plain,cd(skolem0003(i2003_11_14_17_19_32337)),inference(resolution,[status(thm)],[c56, c14])).
% 0.75/0.93 cnf(c123,plain,cc(skolem0003(i2003_11_14_17_19_32337)),inference(resolution,[status(thm)],[c122, c43])).
% 0.75/0.93 cnf(c1,axiom,X102!=X101|~cc(X102)|cc(X101),theory(equality)).
% 0.75/0.93 fof(axiom_0,axiom,(![X]:(cowlThing(X)&(~cowlNothing(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_0)).
% 0.75/0.93 fof(c66,plain,(![X]:(cowlThing(X)&~cowlNothing(X))),inference(fof_simplification,[status(thm)],[axiom_0])).
% 0.75/0.93 fof(c67,plain,((![X]:cowlThing(X))&(![X]:~cowlNothing(X))),inference(shift_quantors,[status(thm)],[c66])).
% 0.75/0.93 fof(c69,plain,(![X32]:(![X33]:(cowlThing(X32)&~cowlNothing(X33)))),inference(shift_quantors,[status(thm)],[fof(c68,plain,((![X32]:cowlThing(X32))&(![X33]:~cowlNothing(X33))),inference(variable_rename,[status(thm)],[c67])).])).
% 0.75/0.93 cnf(c70,plain,cowlThing(X72),inference(split_conjunct,[status(thm)],[c69])).
% 0.75/0.93 cnf(c52,plain,~cUnsatisfiable(X192)|~rinvR(X192,X193)|rinvF(X193,skolem0002(X192,X193)),inference(split_conjunct,[status(thm)],[c51])).
% 0.75/0.93 cnf(c164,plain,~cUnsatisfiable(i2003_11_14_17_19_32337)|rinvF(skolem0003(i2003_11_14_17_19_32337),skolem0002(i2003_11_14_17_19_32337,skolem0003(i2003_11_14_17_19_32337))),inference(resolution,[status(thm)],[c52, c132])).
% 0.75/0.93 cnf(c209,plain,rinvF(skolem0003(i2003_11_14_17_19_32337),skolem0002(i2003_11_14_17_19_32337,skolem0003(i2003_11_14_17_19_32337))),inference(resolution,[status(thm)],[c164, c14])).
% 0.75/0.93 cnf(c259,plain,rf(skolem0002(i2003_11_14_17_19_32337,skolem0003(i2003_11_14_17_19_32337)),skolem0003(i2003_11_14_17_19_32337)),inference(resolution,[status(thm)],[c209, c28])).
% 0.75/0.93 fof(axiom_4,axiom,(![X]:(cowlThing(X)=>(![Y0]:(![Y1]:((rf(X,Y0)&rf(X,Y1))=>Y0=Y1))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_4)).
% 0.75/0.93 fof(c30,plain,(![X]:(~cowlThing(X)|(![Y0]:(![Y1]:((~rf(X,Y0)|~rf(X,Y1))|Y0=Y1))))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.75/0.93 fof(c32,plain,(![X15]:(![X16]:(![X17]:(~cowlThing(X15)|((~rf(X15,X16)|~rf(X15,X17))|X16=X17))))),inference(shift_quantors,[status(thm)],[fof(c31,plain,(![X15]:(~cowlThing(X15)|(![X16]:(![X17]:((~rf(X15,X16)|~rf(X15,X17))|X16=X17))))),inference(variable_rename,[status(thm)],[c30])).])).
% 0.75/0.93 cnf(c33,plain,~cowlThing(X180)|~rf(X180,X181)|~rf(X180,X182)|X181=X182,inference(split_conjunct,[status(thm)],[c32])).
% 0.75/0.93 cnf(c41,plain,~cd(X107)|rf(X107,skolem0001(X107)),inference(split_conjunct,[status(thm)],[c40])).
% 0.75/0.93 cnf(c188,plain,rf(skolem0002(i2003_11_14_17_19_32337,skolem0003(i2003_11_14_17_19_32337)),skolem0001(skolem0002(i2003_11_14_17_19_32337,skolem0003(i2003_11_14_17_19_32337)))),inference(resolution,[status(thm)],[c187, c41])).
% 0.75/0.93 cnf(c265,plain,~cowlThing(skolem0002(i2003_11_14_17_19_32337,skolem0003(i2003_11_14_17_19_32337)))|~rf(skolem0002(i2003_11_14_17_19_32337,skolem0003(i2003_11_14_17_19_32337)),X259)|X259=skolem0001(skolem0002(i2003_11_14_17_19_32337,skolem0003(i2003_11_14_17_19_32337))),inference(resolution,[status(thm)],[c188, c33])).
% 0.75/0.93 cnf(c367,plain,~cowlThing(skolem0002(i2003_11_14_17_19_32337,skolem0003(i2003_11_14_17_19_32337)))|skolem0003(i2003_11_14_17_19_32337)=skolem0001(skolem0002(i2003_11_14_17_19_32337,skolem0003(i2003_11_14_17_19_32337))),inference(resolution,[status(thm)],[c265, c259])).
% 0.75/0.93 cnf(c633,plain,skolem0003(i2003_11_14_17_19_32337)=skolem0001(skolem0002(i2003_11_14_17_19_32337,skolem0003(i2003_11_14_17_19_32337))),inference(resolution,[status(thm)],[c367, c70])).
% 0.75/0.93 cnf(c641,plain,~cc(skolem0003(i2003_11_14_17_19_32337))|cc(skolem0001(skolem0002(i2003_11_14_17_19_32337,skolem0003(i2003_11_14_17_19_32337)))),inference(resolution,[status(thm)],[c633, c1])).
% 0.75/0.93 cnf(c709,plain,cc(skolem0001(skolem0002(i2003_11_14_17_19_32337,skolem0003(i2003_11_14_17_19_32337)))),inference(resolution,[status(thm)],[c641, c123])).
% 0.75/0.93 cnf(c711,plain,~cd(skolem0002(i2003_11_14_17_19_32337,skolem0003(i2003_11_14_17_19_32337))),inference(resolution,[status(thm)],[c709, c42])).
% 0.75/0.93 cnf(c712,plain,$false,inference(resolution,[status(thm)],[c711, c187])).
% 0.75/0.93 % SZS output end CNFRefutation
% 0.75/0.93
% 0.75/0.93 % Initial clauses : 52
% 0.75/0.93 % Processed clauses : 277
% 0.75/0.93 % Factors computed : 3
% 0.75/0.93 % Resolvents computed: 593
% 0.75/0.93 % Tautologies deleted: 9
% 0.75/0.93 % Forward subsumed : 198
% 0.75/0.93 % Backward subsumed : 15
% 0.75/0.93 % -------- CPU Time ---------
% 0.75/0.93 % User time : 0.561 s
% 0.75/0.93 % System time : 0.018 s
% 0.75/0.93 % Total time : 0.579 s
%------------------------------------------------------------------------------