%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS069+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n023.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:37 EDT 2024
% Result : Unsatisfiable 0.43s 0.63s
% Output : Refutation 0.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : KRS069+1 : TPTP v8.1.2. Released v3.1.0.
% 0.04/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n023.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 9 00:12:53 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.43/0.63 % Version: 1.5
% 0.43/0.63 % SZS status Unsatisfiable
% 0.43/0.63 % SZS output start CNFRefutation
% 0.43/0.63 fof(axiom_6,axiom,cUnsatisfiable(i2003_11_14_17_18_2750),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_6)).
% 0.43/0.63 cnf(c16,plain,cUnsatisfiable(i2003_11_14_17_18_2750),inference(split_conjunct,[status(thm)],[axiom_6])).
% 0.43/0.63 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)<=>(((?[Y]:(rf1(X,Y)&cp1(Y)))&(?[Y]:(rf2(X,Y)&(~cp1(Y)))))&(?[Y]:(rf3(X,Y)&cp2(Y)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 0.43/0.63 fof(c26,plain,(![X]:(cUnsatisfiable(X)<=>(((?[Y]:(rf1(X,Y)&cp1(Y)))&(?[Y]:(rf2(X,Y)&~cp1(Y))))&(?[Y]:(rf3(X,Y)&cp2(Y)))))),inference(fof_simplification,[status(thm)],[axiom_2])).
% 0.43/0.63 fof(c27,plain,(![X]:((~cUnsatisfiable(X)|(((?[Y]:(rf1(X,Y)&cp1(Y)))&(?[Y]:(rf2(X,Y)&~cp1(Y))))&(?[Y]:(rf3(X,Y)&cp2(Y)))))&((((![Y]:(~rf1(X,Y)|~cp1(Y)))|(![Y]:(~rf2(X,Y)|cp1(Y))))|(![Y]:(~rf3(X,Y)|~cp2(Y))))|cUnsatisfiable(X)))),inference(fof_nnf,[status(thm)],[c26])).
% 0.43/0.63 fof(c28,plain,((![X]:(~cUnsatisfiable(X)|(((?[Y]:(rf1(X,Y)&cp1(Y)))&(?[Y]:(rf2(X,Y)&~cp1(Y))))&(?[Y]:(rf3(X,Y)&cp2(Y))))))&(![X]:((((![Y]:(~rf1(X,Y)|~cp1(Y)))|(![Y]:(~rf2(X,Y)|cp1(Y))))|(![Y]:(~rf3(X,Y)|~cp2(Y))))|cUnsatisfiable(X)))),inference(shift_quantors,[status(thm)],[c27])).
% 0.43/0.63 fof(c29,plain,((![X15]:(~cUnsatisfiable(X15)|(((?[X16]:(rf1(X15,X16)&cp1(X16)))&(?[X17]:(rf2(X15,X17)&~cp1(X17))))&(?[X18]:(rf3(X15,X18)&cp2(X18))))))&(![X19]:((((![X20]:(~rf1(X19,X20)|~cp1(X20)))|(![X21]:(~rf2(X19,X21)|cp1(X21))))|(![X22]:(~rf3(X19,X22)|~cp2(X22))))|cUnsatisfiable(X19)))),inference(variable_rename,[status(thm)],[c28])).
% 0.43/0.63 fof(c31,plain,(![X15]:(![X19]:(![X20]:(![X21]:(![X22]:((~cUnsatisfiable(X15)|(((rf1(X15,skolem0001(X15))&cp1(skolem0001(X15)))&(rf2(X15,skolem0002(X15))&~cp1(skolem0002(X15))))&(rf3(X15,skolem0003(X15))&cp2(skolem0003(X15)))))&((((~rf1(X19,X20)|~cp1(X20))|(~rf2(X19,X21)|cp1(X21)))|(~rf3(X19,X22)|~cp2(X22)))|cUnsatisfiable(X19)))))))),inference(shift_quantors,[status(thm)],[fof(c30,plain,((![X15]:(~cUnsatisfiable(X15)|(((rf1(X15,skolem0001(X15))&cp1(skolem0001(X15)))&(rf2(X15,skolem0002(X15))&~cp1(skolem0002(X15))))&(rf3(X15,skolem0003(X15))&cp2(skolem0003(X15))))))&(![X19]:((((![X20]:(~rf1(X19,X20)|~cp1(X20)))|(![X21]:(~rf2(X19,X21)|cp1(X21))))|(![X22]:(~rf3(X19,X22)|~cp2(X22))))|cUnsatisfiable(X19)))),inference(skolemize,[status(esa)],[c29])).])).
% 0.43/0.63 fof(c32,plain,(![X15]:(![X19]:(![X20]:(![X21]:(![X22]:(((((~cUnsatisfiable(X15)|rf1(X15,skolem0001(X15)))&(~cUnsatisfiable(X15)|cp1(skolem0001(X15))))&((~cUnsatisfiable(X15)|rf2(X15,skolem0002(X15)))&(~cUnsatisfiable(X15)|~cp1(skolem0002(X15)))))&((~cUnsatisfiable(X15)|rf3(X15,skolem0003(X15)))&(~cUnsatisfiable(X15)|cp2(skolem0003(X15)))))&((((~rf1(X19,X20)|~cp1(X20))|(~rf2(X19,X21)|cp1(X21)))|(~rf3(X19,X22)|~cp2(X22)))|cUnsatisfiable(X19)))))))),inference(distribute,[status(thm)],[c31])).
% 0.43/0.63 cnf(c36,plain,~cUnsatisfiable(X76)|~cp1(skolem0002(X76)),inference(split_conjunct,[status(thm)],[c32])).
% 0.43/0.63 cnf(c3,axiom,X92!=X91|~cp1(X92)|cp1(X91),theory(equality)).
% 0.43/0.63 cnf(symmetry,axiom,X64!=X63|X63=X64,theory(equality)).
% 0.43/0.63 cnf(c35,plain,~cUnsatisfiable(X87)|rf2(X87,skolem0002(X87)),inference(split_conjunct,[status(thm)],[c32])).
% 0.43/0.63 cnf(c100,plain,rf2(i2003_11_14_17_18_2750,skolem0002(i2003_11_14_17_18_2750)),inference(resolution,[status(thm)],[c35, c16])).
% 0.43/0.63 fof(axiom_8,axiom,(![X]:(![Y]:(rf3(X,Y)=>rf2(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_8)).
% 0.43/0.63 fof(c10,plain,(![X]:(![Y]:(~rf3(X,Y)|rf2(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_8])).
% 0.43/0.63 fof(c11,plain,(![X2]:(![X3]:(~rf3(X2,X3)|rf2(X2,X3)))),inference(variable_rename,[status(thm)],[c10])).
% 0.43/0.63 cnf(c12,plain,~rf3(X69,X68)|rf2(X69,X68),inference(split_conjunct,[status(thm)],[c11])).
% 0.43/0.63 cnf(c37,plain,~cUnsatisfiable(X88)|rf3(X88,skolem0003(X88)),inference(split_conjunct,[status(thm)],[c32])).
% 0.43/0.63 cnf(c101,plain,rf3(i2003_11_14_17_18_2750,skolem0003(i2003_11_14_17_18_2750)),inference(resolution,[status(thm)],[c37, c16])).
% 0.43/0.63 cnf(c102,plain,rf2(i2003_11_14_17_18_2750,skolem0003(i2003_11_14_17_18_2750)),inference(resolution,[status(thm)],[c101, c12])).
% 0.43/0.63 fof(axiom_4,axiom,(![X]:(![Y]:(![Z]:((rf2(X,Y)&rf2(X,Z))=>Y=Z)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_4)).
% 0.43/0.63 fof(c20,plain,(![X]:(![Y]:(![Z]:((~rf2(X,Y)|~rf2(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.43/0.63 fof(c21,plain,(![X9]:(![X10]:(![X11]:((~rf2(X9,X10)|~rf2(X9,X11))|X10=X11)))),inference(variable_rename,[status(thm)],[c20])).
% 0.43/0.63 cnf(c22,plain,~rf2(X135,X134)|~rf2(X135,X136)|X134=X136,inference(split_conjunct,[status(thm)],[c21])).
% 0.43/0.63 cnf(c116,plain,~rf2(i2003_11_14_17_18_2750,X167)|X167=skolem0003(i2003_11_14_17_18_2750),inference(resolution,[status(thm)],[c22, c102])).
% 0.43/0.63 cnf(c134,plain,skolem0002(i2003_11_14_17_18_2750)=skolem0003(i2003_11_14_17_18_2750),inference(resolution,[status(thm)],[c116, c100])).
% 0.43/0.63 cnf(c141,plain,skolem0003(i2003_11_14_17_18_2750)=skolem0002(i2003_11_14_17_18_2750),inference(resolution,[status(thm)],[c134, symmetry])).
% 0.43/0.63 cnf(c144,plain,~cp1(skolem0003(i2003_11_14_17_18_2750))|cp1(skolem0002(i2003_11_14_17_18_2750)),inference(resolution,[status(thm)],[c141, c3])).
% 0.43/0.63 cnf(c34,plain,~cUnsatisfiable(X75)|cp1(skolem0001(X75)),inference(split_conjunct,[status(thm)],[c32])).
% 0.43/0.63 cnf(c96,plain,cp1(skolem0001(i2003_11_14_17_18_2750)),inference(resolution,[status(thm)],[c34, c16])).
% 0.43/0.63 fof(axiom_7,axiom,(![X]:(![Y]:(rf3(X,Y)=>rf1(X,Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_7)).
% 0.43/0.63 fof(c13,plain,(![X]:(![Y]:(~rf3(X,Y)|rf1(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_7])).
% 0.43/0.63 fof(c14,plain,(![X4]:(![X5]:(~rf3(X4,X5)|rf1(X4,X5)))),inference(variable_rename,[status(thm)],[c13])).
% 0.43/0.63 cnf(c15,plain,~rf3(X71,X70)|rf1(X71,X70),inference(split_conjunct,[status(thm)],[c14])).
% 0.43/0.63 cnf(c103,plain,rf1(i2003_11_14_17_18_2750,skolem0003(i2003_11_14_17_18_2750)),inference(resolution,[status(thm)],[c101, c15])).
% 0.43/0.63 cnf(c33,plain,~cUnsatisfiable(X84)|rf1(X84,skolem0001(X84)),inference(split_conjunct,[status(thm)],[c32])).
% 0.43/0.63 cnf(c99,plain,rf1(i2003_11_14_17_18_2750,skolem0001(i2003_11_14_17_18_2750)),inference(resolution,[status(thm)],[c33, c16])).
% 0.43/0.63 fof(axiom_3,axiom,(![X]:(![Y]:(![Z]:((rf1(X,Y)&rf1(X,Z))=>Y=Z)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 0.43/0.63 fof(c23,plain,(![X]:(![Y]:(![Z]:((~rf1(X,Y)|~rf1(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.43/0.63 fof(c24,plain,(![X12]:(![X13]:(![X14]:((~rf1(X12,X13)|~rf1(X12,X14))|X13=X14)))),inference(variable_rename,[status(thm)],[c23])).
% 0.43/0.63 cnf(c25,plain,~rf1(X139,X140)|~rf1(X139,X141)|X140=X141,inference(split_conjunct,[status(thm)],[c24])).
% 0.43/0.63 cnf(c119,plain,~rf1(i2003_11_14_17_18_2750,X173)|X173=skolem0001(i2003_11_14_17_18_2750),inference(resolution,[status(thm)],[c25, c99])).
% 0.43/0.63 cnf(c155,plain,skolem0003(i2003_11_14_17_18_2750)=skolem0001(i2003_11_14_17_18_2750),inference(resolution,[status(thm)],[c119, c103])).
% 0.43/0.63 cnf(c161,plain,skolem0001(i2003_11_14_17_18_2750)=skolem0003(i2003_11_14_17_18_2750),inference(resolution,[status(thm)],[c155, symmetry])).
% 0.43/0.63 cnf(c168,plain,~cp1(skolem0001(i2003_11_14_17_18_2750))|cp1(skolem0003(i2003_11_14_17_18_2750)),inference(resolution,[status(thm)],[c161, c3])).
% 0.43/0.63 cnf(c265,plain,cp1(skolem0003(i2003_11_14_17_18_2750)),inference(resolution,[status(thm)],[c168, c96])).
% 0.43/0.63 cnf(c266,plain,cp1(skolem0002(i2003_11_14_17_18_2750)),inference(resolution,[status(thm)],[c265, c144])).
% 0.43/0.63 cnf(c267,plain,~cUnsatisfiable(i2003_11_14_17_18_2750),inference(resolution,[status(thm)],[c266, c36])).
% 0.43/0.63 cnf(c268,plain,$false,inference(resolution,[status(thm)],[c267, c16])).
% 0.43/0.63 % SZS output end CNFRefutation
% 0.43/0.63
% 0.43/0.63 % Initial clauses : 43
% 0.43/0.63 % Processed clauses : 96
% 0.43/0.63 % Factors computed : 4
% 0.43/0.63 % Resolvents computed: 173
% 0.43/0.63 % Tautologies deleted: 8
% 0.43/0.63 % Forward subsumed : 67
% 0.43/0.63 % Backward subsumed : 5
% 0.43/0.63 % -------- CPU Time ---------
% 0.43/0.63 % User time : 0.267 s
% 0.43/0.63 % System time : 0.016 s
% 0.43/0.63 % Total time : 0.283 s
%------------------------------------------------------------------------------