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