%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS090+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n026.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:40 EDT 2024
% Result : Unsatisfiable 0.44s 0.59s
% Output : Refutation 0.44s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : KRS090+1 : TPTP v8.1.2. Released v3.1.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n026.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 9 00:06:08 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.44/0.59 % Version: 1.5
% 0.44/0.59 % SZS status Unsatisfiable
% 0.44/0.59 % SZS output start CNFRefutation
% 0.44/0.59 fof(axiom_8,axiom,cTEST(i2003_11_14_17_19_57994),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_8)).
% 0.44/0.59 cnf(c0,plain,cTEST(i2003_11_14_17_19_57994),inference(split_conjunct,[status(thm)],[axiom_8])).
% 0.44/0.59 fof(axiom_7,axiom,(![X]:(cTEST(X)=>((cC4(X)&cC1(X))&cC5(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_7)).
% 0.44/0.59 fof(c1,plain,(![X]:(~cTEST(X)|((cC4(X)&cC1(X))&cC5(X)))),inference(fof_nnf,[status(thm)],[axiom_7])).
% 0.44/0.59 fof(c2,plain,(![X2]:(~cTEST(X2)|((cC4(X2)&cC1(X2))&cC5(X2)))),inference(variable_rename,[status(thm)],[c1])).
% 0.44/0.59 fof(c3,plain,(![X2]:(((~cTEST(X2)|cC4(X2))&(~cTEST(X2)|cC1(X2)))&(~cTEST(X2)|cC5(X2)))),inference(distribute,[status(thm)],[c2])).
% 0.44/0.59 cnf(c6,plain,~cTEST(X18)|cC5(X18),inference(split_conjunct,[status(thm)],[c3])).
% 0.44/0.59 cnf(c79,plain,cC5(i2003_11_14_17_19_57994),inference(resolution,[status(thm)],[c6, c0])).
% 0.44/0.59 fof(axiom_6,axiom,(![X]:(cC5(X)=>(![Y]:(rR(X,Y)=>cC3(Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_6)).
% 0.44/0.59 fof(c7,plain,(![X]:(~cC5(X)|(![Y]:(~rR(X,Y)|cC3(Y))))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 0.44/0.59 fof(c9,plain,(![X3]:(![X4]:(~cC5(X3)|(~rR(X3,X4)|cC3(X4))))),inference(shift_quantors,[status(thm)],[fof(c8,plain,(![X3]:(~cC5(X3)|(![X4]:(~rR(X3,X4)|cC3(X4))))),inference(variable_rename,[status(thm)],[c7])).])).
% 0.44/0.59 cnf(c10,plain,~cC5(X22)|~rR(X22,X21)|cC3(X21),inference(split_conjunct,[status(thm)],[c9])).
% 0.44/0.59 cnf(c4,plain,~cTEST(X16)|cC4(X16),inference(split_conjunct,[status(thm)],[c3])).
% 0.44/0.59 cnf(c77,plain,cC4(i2003_11_14_17_19_57994),inference(resolution,[status(thm)],[c4, c0])).
% 0.44/0.59 fof(axiom_5,axiom,(![X]:(cC4(X)=>(?[Y]:(rR(X,Y)&cC2(Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_5)).
% 0.44/0.59 fof(c11,plain,(![X]:(~cC4(X)|(?[Y]:(rR(X,Y)&cC2(Y))))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.44/0.59 fof(c12,plain,(![X5]:(~cC4(X5)|(?[X6]:(rR(X5,X6)&cC2(X6))))),inference(variable_rename,[status(thm)],[c11])).
% 0.44/0.59 fof(c13,plain,(![X5]:(~cC4(X5)|(rR(X5,skolem0001(X5))&cC2(skolem0001(X5))))),inference(skolemize,[status(esa)],[c12])).
% 0.44/0.59 fof(c14,plain,(![X5]:((~cC4(X5)|rR(X5,skolem0001(X5)))&(~cC4(X5)|cC2(skolem0001(X5))))),inference(distribute,[status(thm)],[c13])).
% 0.44/0.59 cnf(c15,plain,~cC4(X25)|rR(X25,skolem0001(X25)),inference(split_conjunct,[status(thm)],[c14])).
% 0.44/0.59 cnf(c82,plain,rR(i2003_11_14_17_19_57994,skolem0001(i2003_11_14_17_19_57994)),inference(resolution,[status(thm)],[c15, c77])).
% 0.44/0.59 cnf(c83,plain,~cC5(i2003_11_14_17_19_57994)|cC3(skolem0001(i2003_11_14_17_19_57994)),inference(resolution,[status(thm)],[c82, c10])).
% 0.44/0.59 cnf(c117,plain,cC3(skolem0001(i2003_11_14_17_19_57994)),inference(resolution,[status(thm)],[c83, c79])).
% 0.44/0.59 fof(axiom_4,axiom,(![X]:(cC3(X)=>(((~cB(X))|(~cA(X)))&(cB(X)|(~cA(X)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_4)).
% 0.44/0.59 fof(c17,plain,(![X]:(cC3(X)=>((~cB(X)|~cA(X))&(cB(X)|~cA(X))))),inference(fof_simplification,[status(thm)],[axiom_4])).
% 0.44/0.59 fof(c18,plain,(![X]:(~cC3(X)|((~cB(X)|~cA(X))&(cB(X)|~cA(X))))),inference(fof_nnf,[status(thm)],[c17])).
% 0.44/0.59 fof(c19,plain,(![X7]:(~cC3(X7)|((~cB(X7)|~cA(X7))&(cB(X7)|~cA(X7))))),inference(variable_rename,[status(thm)],[c18])).
% 0.44/0.59 fof(c20,plain,(![X7]:((~cC3(X7)|(~cB(X7)|~cA(X7)))&(~cC3(X7)|(cB(X7)|~cA(X7))))),inference(distribute,[status(thm)],[c19])).
% 0.44/0.59 cnf(c22,plain,~cC3(X27)|cB(X27)|~cA(X27),inference(split_conjunct,[status(thm)],[c20])).
% 0.44/0.59 cnf(c16,plain,~cC4(X24)|cC2(skolem0001(X24)),inference(split_conjunct,[status(thm)],[c14])).
% 0.44/0.59 cnf(c81,plain,cC2(skolem0001(i2003_11_14_17_19_57994)),inference(resolution,[status(thm)],[c16, c77])).
% 0.44/0.59 fof(axiom_3,axiom,(![X]:(cC2(X)=>(((~cB(X))|cA(X))&(cB(X)|cA(X))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 0.44/0.59 fof(c23,plain,(![X]:(cC2(X)=>((~cB(X)|cA(X))&(cB(X)|cA(X))))),inference(fof_simplification,[status(thm)],[axiom_3])).
% 0.44/0.59 fof(c24,plain,(![X]:(~cC2(X)|((~cB(X)|cA(X))&(cB(X)|cA(X))))),inference(fof_nnf,[status(thm)],[c23])).
% 0.44/0.59 fof(c25,plain,(![X8]:(~cC2(X8)|((~cB(X8)|cA(X8))&(cB(X8)|cA(X8))))),inference(variable_rename,[status(thm)],[c24])).
% 0.44/0.59 fof(c26,plain,(![X8]:((~cC2(X8)|(~cB(X8)|cA(X8)))&(~cC2(X8)|(cB(X8)|cA(X8))))),inference(distribute,[status(thm)],[c25])).
% 0.44/0.59 cnf(c28,plain,~cC2(X29)|cB(X29)|cA(X29),inference(split_conjunct,[status(thm)],[c26])).
% 0.44/0.59 cnf(c84,plain,cB(skolem0001(i2003_11_14_17_19_57994))|cA(skolem0001(i2003_11_14_17_19_57994)),inference(resolution,[status(thm)],[c28, c81])).
% 0.44/0.59 cnf(c119,plain,cB(skolem0001(i2003_11_14_17_19_57994))|~cC3(skolem0001(i2003_11_14_17_19_57994)),inference(resolution,[status(thm)],[c84, c22])).
% 0.44/0.59 cnf(c122,plain,cB(skolem0001(i2003_11_14_17_19_57994)),inference(resolution,[status(thm)],[c119, c117])).
% 0.44/0.59 cnf(c21,plain,~cC3(X26)|~cB(X26)|~cA(X26),inference(split_conjunct,[status(thm)],[c20])).
% 0.44/0.59 cnf(c27,plain,~cC2(X28)|~cB(X28)|cA(X28),inference(split_conjunct,[status(thm)],[c26])).
% 0.44/0.59 cnf(c118,plain,cA(skolem0001(i2003_11_14_17_19_57994))|~cC2(skolem0001(i2003_11_14_17_19_57994)),inference(resolution,[status(thm)],[c84, c27])).
% 0.44/0.59 cnf(c121,plain,cA(skolem0001(i2003_11_14_17_19_57994)),inference(resolution,[status(thm)],[c118, c81])).
% 0.44/0.59 cnf(c124,plain,~cC3(skolem0001(i2003_11_14_17_19_57994))|~cB(skolem0001(i2003_11_14_17_19_57994)),inference(resolution,[status(thm)],[c121, c21])).
% 0.44/0.59 cnf(c126,plain,~cC3(skolem0001(i2003_11_14_17_19_57994)),inference(resolution,[status(thm)],[c124, c122])).
% 0.44/0.59 cnf(c127,plain,$false,inference(resolution,[status(thm)],[c126, c117])).
% 0.44/0.59 % SZS output end CNFRefutation
% 0.44/0.59
% 0.44/0.59 % Initial clauses : 47
% 0.44/0.59 % Processed clauses : 93
% 0.44/0.59 % Factors computed : 0
% 0.44/0.59 % Resolvents computed: 51
% 0.44/0.59 % Tautologies deleted: 2
% 0.44/0.59 % Forward subsumed : 1
% 0.44/0.59 % Backward subsumed : 5
% 0.44/0.59 % -------- CPU Time ---------
% 0.44/0.59 % User time : 0.221 s
% 0.44/0.59 % System time : 0.016 s
% 0.44/0.59 % Total time : 0.237 s
%------------------------------------------------------------------------------