%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS055+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:35 EDT 2024
% Result : Satisfiable 0.20s 0.52s
% Output : Saturation 0.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : KRS055+1 : TPTP v8.1.2. Released v3.1.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n023.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Thu May 9 00:06:53 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.20/0.52 % Version: 1.5
% 0.20/0.52 % SZS status Satisfiable
% 0.20/0.52 % SZS output start Saturation
% 0.20/0.52 fof(axiom_1,axiom,(![X]:(xsd_string(X)<=>(~xsd_integer(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_1)).
% 0.20/0.52 fof(c14,plain,(![X]:(xsd_string(X)<=>~xsd_integer(X))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 0.20/0.52 fof(c15,plain,(![X]:((~xsd_string(X)|~xsd_integer(X))&(xsd_integer(X)|xsd_string(X)))),inference(fof_nnf,[status(thm)],[c14])).
% 0.20/0.52 fof(c16,plain,((![X]:(~xsd_string(X)|~xsd_integer(X)))&(![X]:(xsd_integer(X)|xsd_string(X)))),inference(shift_quantors,[status(thm)],[c15])).
% 0.20/0.52 fof(c18,plain,(![X8]:(![X9]:((~xsd_string(X8)|~xsd_integer(X8))&(xsd_integer(X9)|xsd_string(X9))))),inference(shift_quantors,[status(thm)],[fof(c17,plain,((![X8]:(~xsd_string(X8)|~xsd_integer(X8)))&(![X9]:(xsd_integer(X9)|xsd_string(X9)))),inference(variable_rename,[status(thm)],[c16])).])).
% 0.20/0.52 cnf(c20,plain,xsd_integer(X21)|xsd_string(X21),inference(split_conjunct,[status(thm)],[c18])).
% 0.20/0.52 cnf(c19,plain,~xsd_string(X20)|~xsd_integer(X20),inference(split_conjunct,[status(thm)],[c18])).
% 0.20/0.52 fof(axiom_2,axiom,(![X]:(((~(cE(X)&cA(X)))&(~(cE(X)&cD(X))))&(~(cA(X)&cD(X))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 0.20/0.52 fof(c7,plain,(![X]:(((~cE(X)|~cA(X))&(~cE(X)|~cD(X)))&(~cA(X)|~cD(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.20/0.52 fof(c8,plain,(((![X]:(~cE(X)|~cA(X)))&(![X]:(~cE(X)|~cD(X))))&(![X]:(~cA(X)|~cD(X)))),inference(shift_quantors,[status(thm)],[c7])).
% 0.20/0.52 fof(c10,plain,(![X5]:(![X6]:(![X7]:(((~cE(X5)|~cA(X5))&(~cE(X6)|~cD(X6)))&(~cA(X7)|~cD(X7)))))),inference(shift_quantors,[status(thm)],[fof(c9,plain,(((![X5]:(~cE(X5)|~cA(X5)))&(![X6]:(~cE(X6)|~cD(X6))))&(![X7]:(~cA(X7)|~cD(X7)))),inference(variable_rename,[status(thm)],[c8])).])).
% 0.20/0.52 cnf(c13,plain,~cA(X19)|~cD(X19),inference(split_conjunct,[status(thm)],[c10])).
% 0.20/0.52 cnf(c12,plain,~cE(X18)|~cD(X18),inference(split_conjunct,[status(thm)],[c10])).
% 0.20/0.52 cnf(c11,plain,~cE(X17)|~cA(X17),inference(split_conjunct,[status(thm)],[c10])).
% 0.20/0.52 fof(axiom_3,axiom,(![X]:(((~(cB(X)&cA(X)))&(~(cB(X)&cC(X))))&(~(cA(X)&cC(X))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_3)).
% 0.20/0.52 fof(c0,plain,(![X]:(((~cB(X)|~cA(X))&(~cB(X)|~cC(X)))&(~cA(X)|~cC(X)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.20/0.52 fof(c1,plain,(((![X]:(~cB(X)|~cA(X)))&(![X]:(~cB(X)|~cC(X))))&(![X]:(~cA(X)|~cC(X)))),inference(shift_quantors,[status(thm)],[c0])).
% 0.20/0.52 fof(c3,plain,(![X2]:(![X3]:(![X4]:(((~cB(X2)|~cA(X2))&(~cB(X3)|~cC(X3)))&(~cA(X4)|~cC(X4)))))),inference(shift_quantors,[status(thm)],[fof(c2,plain,(((![X2]:(~cB(X2)|~cA(X2)))&(![X3]:(~cB(X3)|~cC(X3))))&(![X4]:(~cA(X4)|~cC(X4)))),inference(variable_rename,[status(thm)],[c1])).])).
% 0.20/0.52 cnf(c6,plain,~cA(X16)|~cC(X16),inference(split_conjunct,[status(thm)],[c3])).
% 0.20/0.52 cnf(c5,plain,~cB(X15)|~cC(X15),inference(split_conjunct,[status(thm)],[c3])).
% 0.20/0.52 cnf(c4,plain,~cB(X14)|~cA(X14),inference(split_conjunct,[status(thm)],[c3])).
% 0.20/0.52 fof(axiom_0,axiom,(![X]:(cowlThing(X)&(~cowlNothing(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_0)).
% 0.20/0.52 fof(c21,plain,(![X]:(cowlThing(X)&~cowlNothing(X))),inference(fof_simplification,[status(thm)],[axiom_0])).
% 0.20/0.52 fof(c22,plain,((![X]:cowlThing(X))&(![X]:~cowlNothing(X))),inference(shift_quantors,[status(thm)],[c21])).
% 0.20/0.52 fof(c24,plain,(![X10]:(![X11]:(cowlThing(X10)&~cowlNothing(X11)))),inference(shift_quantors,[status(thm)],[fof(c23,plain,((![X10]:cowlThing(X10))&(![X11]:~cowlNothing(X11))),inference(variable_rename,[status(thm)],[c22])).])).
% 0.20/0.52 cnf(c26,plain,~cowlNothing(X13),inference(split_conjunct,[status(thm)],[c24])).
% 0.20/0.52 cnf(c25,plain,cowlThing(X12),inference(split_conjunct,[status(thm)],[c24])).
% 0.20/0.52 % SZS output end Saturation
% 0.20/0.52
% 0.20/0.52 % Initial clauses : 10
% 0.20/0.52 % Processed clauses : 10
% 0.20/0.52 % Factors computed : 0
% 0.20/0.52 % Resolvents computed: 1
% 0.20/0.52 % Tautologies deleted: 1
% 0.20/0.52 % Forward subsumed : 0
% 0.20/0.52 % Backward subsumed : 0
% 0.20/0.52 % -------- CPU Time ---------
% 0.20/0.52 % User time : 0.163 s
% 0.20/0.52 % System time : 0.013 s
% 0.20/0.52 % Total time : 0.176 s
%------------------------------------------------------------------------------