%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS115+1 : TPTP v8.1.2. Released v3.1.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:44 EDT 2024
% Result : Unsatisfiable 0.48s 0.66s
% Output : Refutation 0.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.13 % Problem : KRS115+1 : TPTP v8.1.2. Released v3.1.0.
% 0.05/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n029.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Thu May 9 00:13:23 EDT 2024
% 0.15/0.36 % CPUTime :
% 0.48/0.66 % Version: 1.5
% 0.48/0.66 % SZS status Unsatisfiable
% 0.48/0.66 % SZS output start CNFRefutation
% 0.48/0.66 fof(axiom_4,axiom,(![X]:(cp2(X)<=>(~(?[Y]:ra_Px1(X,Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_4)).
% 0.48/0.66 fof(c34,plain,(![X]:((~cp2(X)|(![Y]:~ra_Px1(X,Y)))&((?[Y]:ra_Px1(X,Y))|cp2(X)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.48/0.66 fof(c35,plain,((![X]:(~cp2(X)|(![Y]:~ra_Px1(X,Y))))&(![X]:((?[Y]:ra_Px1(X,Y))|cp2(X)))),inference(shift_quantors,[status(thm)],[c34])).
% 0.48/0.66 fof(c36,plain,((![X16]:(~cp2(X16)|(![X17]:~ra_Px1(X16,X17))))&(![X18]:((?[X19]:ra_Px1(X18,X19))|cp2(X18)))),inference(variable_rename,[status(thm)],[c35])).
% 0.48/0.66 fof(c38,plain,(![X16]:(![X17]:(![X18]:((~cp2(X16)|~ra_Px1(X16,X17))&(ra_Px1(X18,skolem0002(X18))|cp2(X18)))))),inference(shift_quantors,[status(thm)],[fof(c37,plain,((![X16]:(~cp2(X16)|(![X17]:~ra_Px1(X16,X17))))&(![X18]:(ra_Px1(X18,skolem0002(X18))|cp2(X18)))),inference(skolemize,[status(esa)],[c36])).])).
% 0.48/0.66 cnf(c39,plain,~cp2(X89)|~ra_Px1(X89,X88),inference(split_conjunct,[status(thm)],[c38])).
% 0.48/0.66 fof(axiom_3,axiom,(![X]:(cp1(X)=>cp2xcomp(X))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_3)).
% 0.48/0.66 fof(c41,plain,(![X]:(~cp1(X)|cp2xcomp(X))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.48/0.66 fof(c42,plain,(![X20]:(~cp1(X20)|cp2xcomp(X20))),inference(variable_rename,[status(thm)],[c41])).
% 0.48/0.66 cnf(c43,plain,~cp1(X76)|cp2xcomp(X76),inference(split_conjunct,[status(thm)],[c42])).
% 0.48/0.66 fof(axiom_8,axiom,cUnsatisfiable(i2003_11_14_17_21_30578),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_8)).
% 0.48/0.66 cnf(c18,plain,cUnsatisfiable(i2003_11_14_17_21_30578),inference(split_conjunct,[status(thm)],[axiom_8])).
% 0.48/0.66 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)<=>(((?[Y]:(rf2(X,Y)&cp2(Y)))&(?[Y]:(rf1(X,Y)&cp1(Y))))&(?[Y]:(rr(X,Y)&cowlThing(Y)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 0.48/0.66 fof(c44,plain,(![X]:((~cUnsatisfiable(X)|(((?[Y]:(rf2(X,Y)&cp2(Y)))&(?[Y]:(rf1(X,Y)&cp1(Y))))&(?[Y]:(rr(X,Y)&cowlThing(Y)))))&((((![Y]:(~rf2(X,Y)|~cp2(Y)))|(![Y]:(~rf1(X,Y)|~cp1(Y))))|(![Y]:(~rr(X,Y)|~cowlThing(Y))))|cUnsatisfiable(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.48/0.66 fof(c45,plain,((![X]:(~cUnsatisfiable(X)|(((?[Y]:(rf2(X,Y)&cp2(Y)))&(?[Y]:(rf1(X,Y)&cp1(Y))))&(?[Y]:(rr(X,Y)&cowlThing(Y))))))&(![X]:((((![Y]:(~rf2(X,Y)|~cp2(Y)))|(![Y]:(~rf1(X,Y)|~cp1(Y))))|(![Y]:(~rr(X,Y)|~cowlThing(Y))))|cUnsatisfiable(X)))),inference(shift_quantors,[status(thm)],[c44])).
% 0.48/0.66 fof(c46,plain,((![X21]:(~cUnsatisfiable(X21)|(((?[X22]:(rf2(X21,X22)&cp2(X22)))&(?[X23]:(rf1(X21,X23)&cp1(X23))))&(?[X24]:(rr(X21,X24)&cowlThing(X24))))))&(![X25]:((((![X26]:(~rf2(X25,X26)|~cp2(X26)))|(![X27]:(~rf1(X25,X27)|~cp1(X27))))|(![X28]:(~rr(X25,X28)|~cowlThing(X28))))|cUnsatisfiable(X25)))),inference(variable_rename,[status(thm)],[c45])).
% 0.48/0.66 fof(c48,plain,(![X21]:(![X25]:(![X26]:(![X27]:(![X28]:((~cUnsatisfiable(X21)|(((rf2(X21,skolem0003(X21))&cp2(skolem0003(X21)))&(rf1(X21,skolem0004(X21))&cp1(skolem0004(X21))))&(rr(X21,skolem0005(X21))&cowlThing(skolem0005(X21)))))&((((~rf2(X25,X26)|~cp2(X26))|(~rf1(X25,X27)|~cp1(X27)))|(~rr(X25,X28)|~cowlThing(X28)))|cUnsatisfiable(X25)))))))),inference(shift_quantors,[status(thm)],[fof(c47,plain,((![X21]:(~cUnsatisfiable(X21)|(((rf2(X21,skolem0003(X21))&cp2(skolem0003(X21)))&(rf1(X21,skolem0004(X21))&cp1(skolem0004(X21))))&(rr(X21,skolem0005(X21))&cowlThing(skolem0005(X21))))))&(![X25]:((((![X26]:(~rf2(X25,X26)|~cp2(X26)))|(![X27]:(~rf1(X25,X27)|~cp1(X27))))|(![X28]:(~rr(X25,X28)|~cowlThing(X28))))|cUnsatisfiable(X25)))),inference(skolemize,[status(esa)],[c46])).])).
% 0.48/0.66 fof(c49,plain,(![X21]:(![X25]:(![X26]:(![X27]:(![X28]:(((((~cUnsatisfiable(X21)|rf2(X21,skolem0003(X21)))&(~cUnsatisfiable(X21)|cp2(skolem0003(X21))))&((~cUnsatisfiable(X21)|rf1(X21,skolem0004(X21)))&(~cUnsatisfiable(X21)|cp1(skolem0004(X21)))))&((~cUnsatisfiable(X21)|rr(X21,skolem0005(X21)))&(~cUnsatisfiable(X21)|cowlThing(skolem0005(X21)))))&((((~rf2(X25,X26)|~cp2(X26))|(~rf1(X25,X27)|~cp1(X27)))|(~rr(X25,X28)|~cowlThing(X28)))|cUnsatisfiable(X25)))))))),inference(distribute,[status(thm)],[c48])).
% 0.48/0.66 cnf(c53,plain,~cUnsatisfiable(X98)|cp1(skolem0004(X98)),inference(split_conjunct,[status(thm)],[c49])).
% 0.48/0.66 cnf(c124,plain,cp1(skolem0004(i2003_11_14_17_21_30578)),inference(resolution,[status(thm)],[c53, c18])).
% 0.48/0.66 cnf(c125,plain,cp2xcomp(skolem0004(i2003_11_14_17_21_30578)),inference(resolution,[status(thm)],[c124, c43])).
% 0.48/0.66 fof(axiom_5,axiom,(![X]:(cp2xcomp(X)<=>(?[Y0]:ra_Px1(X,Y0)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_5)).
% 0.48/0.66 fof(c27,plain,(![X]:((~cp2xcomp(X)|(?[Y0]:ra_Px1(X,Y0)))&((![Y0]:~ra_Px1(X,Y0))|cp2xcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.48/0.66 fof(c28,plain,((![X]:(~cp2xcomp(X)|(?[Y0]:ra_Px1(X,Y0))))&(![X]:((![Y0]:~ra_Px1(X,Y0))|cp2xcomp(X)))),inference(shift_quantors,[status(thm)],[c27])).
% 0.48/0.66 fof(c29,plain,((![X12]:(~cp2xcomp(X12)|(?[X13]:ra_Px1(X12,X13))))&(![X14]:((![X15]:~ra_Px1(X14,X15))|cp2xcomp(X14)))),inference(variable_rename,[status(thm)],[c28])).
% 0.48/0.66 fof(c31,plain,(![X12]:(![X14]:(![X15]:((~cp2xcomp(X12)|ra_Px1(X12,skolem0001(X12)))&(~ra_Px1(X14,X15)|cp2xcomp(X14)))))),inference(shift_quantors,[status(thm)],[fof(c30,plain,((![X12]:(~cp2xcomp(X12)|ra_Px1(X12,skolem0001(X12))))&(![X14]:((![X15]:~ra_Px1(X14,X15))|cp2xcomp(X14)))),inference(skolemize,[status(esa)],[c29])).])).
% 0.48/0.66 cnf(c32,plain,~cp2xcomp(X105)|ra_Px1(X105,skolem0001(X105)),inference(split_conjunct,[status(thm)],[c31])).
% 0.48/0.66 cnf(c126,plain,ra_Px1(skolem0004(i2003_11_14_17_21_30578),skolem0001(skolem0004(i2003_11_14_17_21_30578))),inference(resolution,[status(thm)],[c32, c125])).
% 0.48/0.66 cnf(c169,plain,~cp2(skolem0004(i2003_11_14_17_21_30578)),inference(resolution,[status(thm)],[c126, c39])).
% 0.48/0.66 cnf(c51,plain,~cUnsatisfiable(X94)|cp2(skolem0003(X94)),inference(split_conjunct,[status(thm)],[c49])).
% 0.48/0.66 cnf(c122,plain,cp2(skolem0003(i2003_11_14_17_21_30578)),inference(resolution,[status(thm)],[c51, c18])).
% 0.48/0.66 cnf(c4,axiom,X118!=X117|~cp2(X118)|cp2(X117),theory(equality)).
% 0.48/0.66 fof(axiom_0,axiom,(![X]:(cowlThing(X)&(~cowlNothing(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_0)).
% 0.48/0.66 fof(c64,plain,(![X]:(cowlThing(X)&~cowlNothing(X))),inference(fof_simplification,[status(thm)],[axiom_0])).
% 0.48/0.66 fof(c65,plain,((![X]:cowlThing(X))&(![X]:~cowlNothing(X))),inference(shift_quantors,[status(thm)],[c64])).
% 0.48/0.66 fof(c67,plain,(![X31]:(![X32]:(cowlThing(X31)&~cowlNothing(X32)))),inference(shift_quantors,[status(thm)],[fof(c66,plain,((![X31]:cowlThing(X31))&(![X32]:~cowlNothing(X32))),inference(variable_rename,[status(thm)],[c65])).])).
% 0.48/0.66 cnf(c68,plain,cowlThing(X73),inference(split_conjunct,[status(thm)],[c67])).
% 0.48/0.66 fof(axiom_10,axiom,(![X]:(![Y]:(rr(X,Y)=>rf1(X,Y)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_10)).
% 0.48/0.66 fof(c12,plain,(![X]:(![Y]:(~rr(X,Y)|rf1(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_10])).
% 0.48/0.66 fof(c13,plain,(![X2]:(![X3]:(~rr(X2,X3)|rf1(X2,X3)))),inference(variable_rename,[status(thm)],[c12])).
% 0.48/0.66 cnf(c14,plain,~rr(X91,X90)|rf1(X91,X90),inference(split_conjunct,[status(thm)],[c13])).
% 0.48/0.66 cnf(c54,plain,~cUnsatisfiable(X116)|rr(X116,skolem0005(X116)),inference(split_conjunct,[status(thm)],[c49])).
% 0.48/0.66 cnf(c133,plain,rr(i2003_11_14_17_21_30578,skolem0005(i2003_11_14_17_21_30578)),inference(resolution,[status(thm)],[c54, c18])).
% 0.48/0.66 cnf(c135,plain,rf1(i2003_11_14_17_21_30578,skolem0005(i2003_11_14_17_21_30578)),inference(resolution,[status(thm)],[c133, c14])).
% 0.48/0.66 fof(rf1_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rf1(C,A))=>rf1(C,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rf1_substitution_2)).
% 0.48/0.66 fof(c88,plain,(![A]:(![B]:(![C]:((A!=B|~rf1(C,A))|rf1(C,B))))),inference(fof_nnf,[status(thm)],[rf1_substitution_2])).
% 0.48/0.66 fof(c89,plain,(![X49]:(![X50]:(![X51]:((X49!=X50|~rf1(X51,X49))|rf1(X51,X50))))),inference(variable_rename,[status(thm)],[c88])).
% 0.48/0.66 cnf(c90,plain,X178!=X177|~rf1(X176,X178)|rf1(X176,X177),inference(split_conjunct,[status(thm)],[c89])).
% 0.48/0.66 cnf(c156,plain,skolem0005(i2003_11_14_17_21_30578)!=X215|rf1(i2003_11_14_17_21_30578,X215),inference(resolution,[status(thm)],[c90, c135])).
% 0.48/0.66 fof(axiom_9,axiom,(![X]:(![Y]:(rr(X,Y)=>rf2(X,Y)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_9)).
% 0.48/0.66 fof(c15,plain,(![X]:(![Y]:(~rr(X,Y)|rf2(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_9])).
% 0.48/0.66 fof(c16,plain,(![X4]:(![X5]:(~rr(X4,X5)|rf2(X4,X5)))),inference(variable_rename,[status(thm)],[c15])).
% 0.48/0.66 cnf(c17,plain,~rr(X93,X92)|rf2(X93,X92),inference(split_conjunct,[status(thm)],[c16])).
% 0.48/0.66 cnf(c134,plain,rf2(i2003_11_14_17_21_30578,skolem0005(i2003_11_14_17_21_30578)),inference(resolution,[status(thm)],[c133, c17])).
% 0.48/0.66 cnf(c50,plain,~cUnsatisfiable(X111)|rf2(X111,skolem0003(X111)),inference(split_conjunct,[status(thm)],[c49])).
% 0.48/0.66 cnf(c130,plain,rf2(i2003_11_14_17_21_30578,skolem0003(i2003_11_14_17_21_30578)),inference(resolution,[status(thm)],[c50, c18])).
% 0.48/0.66 fof(axiom_7,axiom,(![X]:(cowlThing(X)=>(![Y0]:(![Y1]:((rf2(X,Y0)&rf2(X,Y1))=>Y0=Y1))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_7)).
% 0.48/0.66 fof(c19,plain,(![X]:(~cowlThing(X)|(![Y0]:(![Y1]:((~rf2(X,Y0)|~rf2(X,Y1))|Y0=Y1))))),inference(fof_nnf,[status(thm)],[axiom_7])).
% 0.48/0.66 fof(c21,plain,(![X6]:(![X7]:(![X8]:(~cowlThing(X6)|((~rf2(X6,X7)|~rf2(X6,X8))|X7=X8))))),inference(shift_quantors,[status(thm)],[fof(c20,plain,(![X6]:(~cowlThing(X6)|(![X7]:(![X8]:((~rf2(X6,X7)|~rf2(X6,X8))|X7=X8))))),inference(variable_rename,[status(thm)],[c19])).])).
% 0.48/0.66 cnf(c22,plain,~cowlThing(X186)|~rf2(X186,X185)|~rf2(X186,X187)|X185=X187,inference(split_conjunct,[status(thm)],[c21])).
% 0.48/0.66 cnf(c162,plain,~cowlThing(i2003_11_14_17_21_30578)|~rf2(i2003_11_14_17_21_30578,X249)|X249=skolem0003(i2003_11_14_17_21_30578),inference(resolution,[status(thm)],[c22, c130])).
% 0.48/0.66 cnf(c205,plain,~cowlThing(i2003_11_14_17_21_30578)|skolem0005(i2003_11_14_17_21_30578)=skolem0003(i2003_11_14_17_21_30578),inference(resolution,[status(thm)],[c162, c134])).
% 0.48/0.66 cnf(c206,plain,skolem0005(i2003_11_14_17_21_30578)=skolem0003(i2003_11_14_17_21_30578),inference(resolution,[status(thm)],[c205, c68])).
% 0.48/0.66 cnf(c214,plain,rf1(i2003_11_14_17_21_30578,skolem0003(i2003_11_14_17_21_30578)),inference(resolution,[status(thm)],[c206, c156])).
% 0.48/0.66 cnf(c52,plain,~cUnsatisfiable(X112)|rf1(X112,skolem0004(X112)),inference(split_conjunct,[status(thm)],[c49])).
% 0.48/0.66 cnf(c131,plain,rf1(i2003_11_14_17_21_30578,skolem0004(i2003_11_14_17_21_30578)),inference(resolution,[status(thm)],[c52, c18])).
% 0.48/0.66 fof(axiom_6,axiom,(![X]:(cowlThing(X)=>(![Y0]:(![Y1]:((rf1(X,Y0)&rf1(X,Y1))=>Y0=Y1))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_6)).
% 0.48/0.66 fof(c23,plain,(![X]:(~cowlThing(X)|(![Y0]:(![Y1]:((~rf1(X,Y0)|~rf1(X,Y1))|Y0=Y1))))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 0.48/0.66 fof(c25,plain,(![X9]:(![X10]:(![X11]:(~cowlThing(X9)|((~rf1(X9,X10)|~rf1(X9,X11))|X10=X11))))),inference(shift_quantors,[status(thm)],[fof(c24,plain,(![X9]:(~cowlThing(X9)|(![X10]:(![X11]:((~rf1(X9,X10)|~rf1(X9,X11))|X10=X11))))),inference(variable_rename,[status(thm)],[c23])).])).
% 0.48/0.66 cnf(c26,plain,~cowlThing(X195)|~rf1(X195,X193)|~rf1(X195,X194)|X193=X194,inference(split_conjunct,[status(thm)],[c25])).
% 0.48/0.66 cnf(c175,plain,~cowlThing(i2003_11_14_17_21_30578)|~rf1(i2003_11_14_17_21_30578,X259)|X259=skolem0004(i2003_11_14_17_21_30578),inference(resolution,[status(thm)],[c26, c131])).
% 0.48/0.66 cnf(c255,plain,~cowlThing(i2003_11_14_17_21_30578)|skolem0003(i2003_11_14_17_21_30578)=skolem0004(i2003_11_14_17_21_30578),inference(resolution,[status(thm)],[c175, c214])).
% 0.48/0.66 cnf(c285,plain,skolem0003(i2003_11_14_17_21_30578)=skolem0004(i2003_11_14_17_21_30578),inference(resolution,[status(thm)],[c255, c68])).
% 0.48/0.66 cnf(c295,plain,~cp2(skolem0003(i2003_11_14_17_21_30578))|cp2(skolem0004(i2003_11_14_17_21_30578)),inference(resolution,[status(thm)],[c285, c4])).
% 0.48/0.66 cnf(c371,plain,cp2(skolem0004(i2003_11_14_17_21_30578)),inference(resolution,[status(thm)],[c295, c122])).
% 0.48/0.66 cnf(c375,plain,$false,inference(resolution,[status(thm)],[c371, c169])).
% 0.48/0.66 % SZS output end CNFRefutation
% 0.48/0.66
% 0.48/0.66 % Initial clauses : 52
% 0.48/0.66 % Processed clauses : 125
% 0.48/0.66 % Factors computed : 3
% 0.48/0.66 % Resolvents computed: 255
% 0.48/0.66 % Tautologies deleted: 11
% 0.48/0.66 % Forward subsumed : 95
% 0.48/0.66 % Backward subsumed : 4
% 0.48/0.66 % -------- CPU Time ---------
% 0.48/0.66 % User time : 0.284 s
% 0.48/0.66 % System time : 0.015 s
% 0.48/0.66 % Total time : 0.299 s
%------------------------------------------------------------------------------