%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS079+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n014.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.54s 0.71s
% Output : Refutation 0.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : KRS079+1 : TPTP v8.1.2. Released v3.1.0.
% 0.08/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n014.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:16:23 EDT 2024
% 0.15/0.36 % CPUTime :
% 0.54/0.71 % Version: 1.5
% 0.54/0.71 % SZS status Unsatisfiable
% 0.54/0.71 % SZS output start CNFRefutation
% 0.54/0.71 fof(axiom_6,axiom,cUnsatisfiable(i2003_11_14_17_19_17492),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_6)).
% 0.54/0.71 cnf(c16,plain,cUnsatisfiable(i2003_11_14_17_19_17492),inference(split_conjunct,[status(thm)],[axiom_6])).
% 0.54/0.71 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/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 0.54/0.71 fof(c29,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.54/0.71 fof(c30,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)],[c29])).
% 0.54/0.71 fof(c31,plain,((![X13]:(~cUnsatisfiable(X13)|(((?[X14]:(rf2(X13,X14)&cp2(X14)))&(?[X15]:(rf1(X13,X15)&cp1(X15))))&(?[X16]:(rr(X13,X16)&cowlThing(X16))))))&(![X17]:((((![X18]:(~rf2(X17,X18)|~cp2(X18)))|(![X19]:(~rf1(X17,X19)|~cp1(X19))))|(![X20]:(~rr(X17,X20)|~cowlThing(X20))))|cUnsatisfiable(X17)))),inference(variable_rename,[status(thm)],[c30])).
% 0.54/0.71 fof(c33,plain,(![X13]:(![X17]:(![X18]:(![X19]:(![X20]:((~cUnsatisfiable(X13)|(((rf2(X13,skolem0001(X13))&cp2(skolem0001(X13)))&(rf1(X13,skolem0002(X13))&cp1(skolem0002(X13))))&(rr(X13,skolem0003(X13))&cowlThing(skolem0003(X13)))))&((((~rf2(X17,X18)|~cp2(X18))|(~rf1(X17,X19)|~cp1(X19)))|(~rr(X17,X20)|~cowlThing(X20)))|cUnsatisfiable(X17)))))))),inference(shift_quantors,[status(thm)],[fof(c32,plain,((![X13]:(~cUnsatisfiable(X13)|(((rf2(X13,skolem0001(X13))&cp2(skolem0001(X13)))&(rf1(X13,skolem0002(X13))&cp1(skolem0002(X13))))&(rr(X13,skolem0003(X13))&cowlThing(skolem0003(X13))))))&(![X17]:((((![X18]:(~rf2(X17,X18)|~cp2(X18)))|(![X19]:(~rf1(X17,X19)|~cp1(X19))))|(![X20]:(~rr(X17,X20)|~cowlThing(X20))))|cUnsatisfiable(X17)))),inference(skolemize,[status(esa)],[c31])).])).
% 0.54/0.71 fof(c34,plain,(![X13]:(![X17]:(![X18]:(![X19]:(![X20]:(((((~cUnsatisfiable(X13)|rf2(X13,skolem0001(X13)))&(~cUnsatisfiable(X13)|cp2(skolem0001(X13))))&((~cUnsatisfiable(X13)|rf1(X13,skolem0002(X13)))&(~cUnsatisfiable(X13)|cp1(skolem0002(X13)))))&((~cUnsatisfiable(X13)|rr(X13,skolem0003(X13)))&(~cUnsatisfiable(X13)|cowlThing(skolem0003(X13)))))&((((~rf2(X17,X18)|~cp2(X18))|(~rf1(X17,X19)|~cp1(X19)))|(~rr(X17,X20)|~cowlThing(X20)))|cUnsatisfiable(X17)))))))),inference(distribute,[status(thm)],[c33])).
% 0.54/0.71 cnf(c38,plain,~cUnsatisfiable(X75)|cp1(skolem0002(X75)),inference(split_conjunct,[status(thm)],[c34])).
% 0.54/0.71 cnf(c100,plain,cp1(skolem0002(i2003_11_14_17_19_17492)),inference(resolution,[status(thm)],[c38, c16])).
% 0.54/0.71 fof(axiom_3,axiom,(![X]:(cp1(X)=>(~cp2(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 0.54/0.71 fof(c25,plain,(![X]:(cp1(X)=>~cp2(X))),inference(fof_simplification,[status(thm)],[axiom_3])).
% 0.54/0.71 fof(c26,plain,(![X]:(~cp1(X)|~cp2(X))),inference(fof_nnf,[status(thm)],[c25])).
% 0.54/0.71 fof(c27,plain,(![X12]:(~cp1(X12)|~cp2(X12))),inference(variable_rename,[status(thm)],[c26])).
% 0.54/0.71 cnf(c28,plain,~cp1(X60)|~cp2(X60),inference(split_conjunct,[status(thm)],[c27])).
% 0.54/0.71 cnf(c36,plain,~cUnsatisfiable(X74)|cp2(skolem0001(X74)),inference(split_conjunct,[status(thm)],[c34])).
% 0.54/0.71 cnf(c98,plain,cp2(skolem0001(i2003_11_14_17_19_17492)),inference(resolution,[status(thm)],[c36, c16])).
% 0.54/0.71 cnf(c4,axiom,X94!=X93|~cp2(X94)|cp2(X93),theory(equality)).
% 0.54/0.71 fof(axiom_0,axiom,(![X]:(cowlThing(X)&(~cowlNothing(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_0)).
% 0.54/0.71 fof(c49,plain,(![X]:(cowlThing(X)&~cowlNothing(X))),inference(fof_simplification,[status(thm)],[axiom_0])).
% 0.54/0.71 fof(c50,plain,((![X]:cowlThing(X))&(![X]:~cowlNothing(X))),inference(shift_quantors,[status(thm)],[c49])).
% 0.54/0.71 fof(c52,plain,(![X23]:(![X24]:(cowlThing(X23)&~cowlNothing(X24)))),inference(shift_quantors,[status(thm)],[fof(c51,plain,((![X23]:cowlThing(X23))&(![X24]:~cowlNothing(X24))),inference(variable_rename,[status(thm)],[c50])).])).
% 0.54/0.71 cnf(c53,plain,cowlThing(X57),inference(split_conjunct,[status(thm)],[c52])).
% 0.54/0.71 fof(axiom_7,axiom,(![X]:(![Y]:(rr(X,Y)=>rf1(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_7)).
% 0.54/0.71 fof(c13,plain,(![X]:(![Y]:(~rr(X,Y)|rf1(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_7])).
% 0.54/0.71 fof(c14,plain,(![X4]:(![X5]:(~rr(X4,X5)|rf1(X4,X5)))),inference(variable_rename,[status(thm)],[c13])).
% 0.54/0.71 cnf(c15,plain,~rr(X72,X73)|rf1(X72,X73),inference(split_conjunct,[status(thm)],[c14])).
% 0.54/0.71 cnf(c39,plain,~cUnsatisfiable(X87)|rr(X87,skolem0003(X87)),inference(split_conjunct,[status(thm)],[c34])).
% 0.54/0.71 cnf(c104,plain,rr(i2003_11_14_17_19_17492,skolem0003(i2003_11_14_17_19_17492)),inference(resolution,[status(thm)],[c39, c16])).
% 0.54/0.71 cnf(c106,plain,rf1(i2003_11_14_17_19_17492,skolem0003(i2003_11_14_17_19_17492)),inference(resolution,[status(thm)],[c104, c15])).
% 0.54/0.71 fof(rf1_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rf1(C,A))=>rf1(C,B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rf1_substitution_2)).
% 0.54/0.71 fof(c73,plain,(![A]:(![B]:(![C]:((A!=B|~rf1(C,A))|rf1(C,B))))),inference(fof_nnf,[status(thm)],[rf1_substitution_2])).
% 0.54/0.71 fof(c74,plain,(![X41]:(![X42]:(![X43]:((X41!=X42|~rf1(X43,X41))|rf1(X43,X42))))),inference(variable_rename,[status(thm)],[c73])).
% 0.54/0.71 cnf(c75,plain,X142!=X141|~rf1(X140,X142)|rf1(X140,X141),inference(split_conjunct,[status(thm)],[c74])).
% 0.54/0.71 cnf(c123,plain,skolem0003(i2003_11_14_17_19_17492)!=X167|rf1(i2003_11_14_17_19_17492,X167),inference(resolution,[status(thm)],[c75, c106])).
% 0.54/0.71 cnf(symmetry,axiom,X62!=X61|X61=X62,theory(equality)).
% 0.54/0.71 cnf(c35,plain,~cUnsatisfiable(X85)|rf2(X85,skolem0001(X85)),inference(split_conjunct,[status(thm)],[c34])).
% 0.54/0.71 cnf(c102,plain,rf2(i2003_11_14_17_19_17492,skolem0001(i2003_11_14_17_19_17492)),inference(resolution,[status(thm)],[c35, c16])).
% 0.54/0.71 fof(axiom_8,axiom,(![X]:(![Y]:(rr(X,Y)=>rf2(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_8)).
% 0.54/0.71 fof(c10,plain,(![X]:(![Y]:(~rr(X,Y)|rf2(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_8])).
% 0.54/0.71 fof(c11,plain,(![X2]:(![X3]:(~rr(X2,X3)|rf2(X2,X3)))),inference(variable_rename,[status(thm)],[c10])).
% 0.54/0.71 cnf(c12,plain,~rr(X68,X67)|rf2(X68,X67),inference(split_conjunct,[status(thm)],[c11])).
% 0.54/0.71 cnf(c105,plain,rf2(i2003_11_14_17_19_17492,skolem0003(i2003_11_14_17_19_17492)),inference(resolution,[status(thm)],[c104, c12])).
% 0.54/0.71 fof(axiom_5,axiom,(![X]:(cowlThing(X)=>(![Y0]:(![Y1]:((rf2(X,Y0)&rf2(X,Y1))=>Y0=Y1))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_5)).
% 0.54/0.71 fof(c17,plain,(![X]:(~cowlThing(X)|(![Y0]:(![Y1]:((~rf2(X,Y0)|~rf2(X,Y1))|Y0=Y1))))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.54/0.71 fof(c19,plain,(![X6]:(![X7]:(![X8]:(~cowlThing(X6)|((~rf2(X6,X7)|~rf2(X6,X8))|X7=X8))))),inference(shift_quantors,[status(thm)],[fof(c18,plain,(![X6]:(~cowlThing(X6)|(![X7]:(![X8]:((~rf2(X6,X7)|~rf2(X6,X8))|X7=X8))))),inference(variable_rename,[status(thm)],[c17])).])).
% 0.54/0.71 cnf(c20,plain,~cowlThing(X149)|~rf2(X149,X147)|~rf2(X149,X148)|X147=X148,inference(split_conjunct,[status(thm)],[c19])).
% 0.54/0.71 cnf(c128,plain,~cowlThing(i2003_11_14_17_19_17492)|~rf2(i2003_11_14_17_19_17492,X185)|X185=skolem0003(i2003_11_14_17_19_17492),inference(resolution,[status(thm)],[c20, c105])).
% 0.54/0.71 cnf(c149,plain,~cowlThing(i2003_11_14_17_19_17492)|skolem0001(i2003_11_14_17_19_17492)=skolem0003(i2003_11_14_17_19_17492),inference(resolution,[status(thm)],[c128, c102])).
% 0.54/0.71 cnf(c150,plain,skolem0001(i2003_11_14_17_19_17492)=skolem0003(i2003_11_14_17_19_17492),inference(resolution,[status(thm)],[c149, c53])).
% 0.54/0.71 cnf(c157,plain,skolem0003(i2003_11_14_17_19_17492)=skolem0001(i2003_11_14_17_19_17492),inference(resolution,[status(thm)],[c150, symmetry])).
% 0.54/0.71 cnf(c166,plain,rf1(i2003_11_14_17_19_17492,skolem0001(i2003_11_14_17_19_17492)),inference(resolution,[status(thm)],[c157, c123])).
% 0.54/0.71 cnf(c37,plain,~cUnsatisfiable(X86)|rf1(X86,skolem0002(X86)),inference(split_conjunct,[status(thm)],[c34])).
% 0.54/0.71 cnf(c103,plain,rf1(i2003_11_14_17_19_17492,skolem0002(i2003_11_14_17_19_17492)),inference(resolution,[status(thm)],[c37, c16])).
% 0.54/0.71 fof(axiom_4,axiom,(![X]:(cowlThing(X)=>(![Y0]:(![Y1]:((rf1(X,Y0)&rf1(X,Y1))=>Y0=Y1))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_4)).
% 0.54/0.71 fof(c21,plain,(![X]:(~cowlThing(X)|(![Y0]:(![Y1]:((~rf1(X,Y0)|~rf1(X,Y1))|Y0=Y1))))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.54/0.71 fof(c23,plain,(![X9]:(![X10]:(![X11]:(~cowlThing(X9)|((~rf1(X9,X10)|~rf1(X9,X11))|X10=X11))))),inference(shift_quantors,[status(thm)],[fof(c22,plain,(![X9]:(~cowlThing(X9)|(![X10]:(![X11]:((~rf1(X9,X10)|~rf1(X9,X11))|X10=X11))))),inference(variable_rename,[status(thm)],[c21])).])).
% 0.54/0.71 cnf(c24,plain,~cowlThing(X154)|~rf1(X154,X156)|~rf1(X154,X155)|X156=X155,inference(split_conjunct,[status(thm)],[c23])).
% 0.54/0.71 cnf(c133,plain,~cowlThing(i2003_11_14_17_19_17492)|~rf1(i2003_11_14_17_19_17492,X187)|X187=skolem0002(i2003_11_14_17_19_17492),inference(resolution,[status(thm)],[c24, c103])).
% 0.54/0.71 cnf(c180,plain,~cowlThing(i2003_11_14_17_19_17492)|skolem0001(i2003_11_14_17_19_17492)=skolem0002(i2003_11_14_17_19_17492),inference(resolution,[status(thm)],[c133, c166])).
% 0.54/0.71 cnf(c218,plain,skolem0001(i2003_11_14_17_19_17492)=skolem0002(i2003_11_14_17_19_17492),inference(resolution,[status(thm)],[c180, c53])).
% 0.54/0.71 cnf(c220,plain,~cp2(skolem0001(i2003_11_14_17_19_17492))|cp2(skolem0002(i2003_11_14_17_19_17492)),inference(resolution,[status(thm)],[c218, c4])).
% 0.54/0.71 cnf(c280,plain,cp2(skolem0002(i2003_11_14_17_19_17492)),inference(resolution,[status(thm)],[c220, c98])).
% 0.54/0.71 cnf(c281,plain,~cp1(skolem0002(i2003_11_14_17_19_17492)),inference(resolution,[status(thm)],[c280, c28])).
% 0.54/0.71 cnf(c282,plain,$false,inference(resolution,[status(thm)],[c281, c100])).
% 0.54/0.71 % SZS output end CNFRefutation
% 0.54/0.71
% 0.54/0.71 % Initial clauses : 43
% 0.54/0.71 % Processed clauses : 96
% 0.54/0.71 % Factors computed : 3
% 0.54/0.71 % Resolvents computed: 186
% 0.54/0.71 % Tautologies deleted: 8
% 0.54/0.71 % Forward subsumed : 80
% 0.54/0.71 % Backward subsumed : 5
% 0.54/0.71 % -------- CPU Time ---------
% 0.54/0.71 % User time : 0.322 s
% 0.54/0.71 % System time : 0.013 s
% 0.54/0.71 % Total time : 0.335 s
%------------------------------------------------------------------------------