%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS174+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n019.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:52 EDT 2024
% Result : Theorem 1.31s 1.52s
% Output : Refutation 1.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : KRS174+1 : TPTP v8.1.2. Released v3.1.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n019.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 9 00:10:38 EDT 2024
% 0.13/0.35 % CPUTime :
% 1.31/1.52 % Version: 1.5
% 1.31/1.52 % SZS status Theorem
% 1.31/1.52 % SZS output start CNFRefutation
% 1.31/1.52 fof(axiom_1,axiom,(![X]:(xsd_string(X)<=>(~xsd_integer(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_1)).
% 1.31/1.52 fof(c42,plain,(![X]:(xsd_string(X)<=>~xsd_integer(X))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 1.31/1.52 fof(c43,plain,(![X]:((~xsd_string(X)|~xsd_integer(X))&(xsd_integer(X)|xsd_string(X)))),inference(fof_nnf,[status(thm)],[c42])).
% 1.31/1.52 fof(c44,plain,((![X]:(~xsd_string(X)|~xsd_integer(X)))&(![X]:(xsd_integer(X)|xsd_string(X)))),inference(shift_quantors,[status(thm)],[c43])).
% 1.31/1.52 fof(c46,plain,(![X12]:(![X13]:((~xsd_string(X12)|~xsd_integer(X12))&(xsd_integer(X13)|xsd_string(X13))))),inference(shift_quantors,[status(thm)],[fof(c45,plain,((![X12]:(~xsd_string(X12)|~xsd_integer(X12)))&(![X13]:(xsd_integer(X13)|xsd_string(X13)))),inference(variable_rename,[status(thm)],[c44])).])).
% 1.31/1.52 cnf(c47,plain,~xsd_string(X36)|~xsd_integer(X36),inference(split_conjunct,[status(thm)],[c46])).
% 1.31/1.52 fof(axiom_0,axiom,(![X]:(cowlThing(X)&(~cowlNothing(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_0)).
% 1.31/1.52 fof(c49,plain,(![X]:(cowlThing(X)&~cowlNothing(X))),inference(fof_simplification,[status(thm)],[axiom_0])).
% 1.31/1.52 fof(c50,plain,((![X]:cowlThing(X))&(![X]:~cowlNothing(X))),inference(shift_quantors,[status(thm)],[c49])).
% 1.31/1.52 fof(c52,plain,(![X14]:(![X15]:(cowlThing(X14)&~cowlNothing(X15)))),inference(shift_quantors,[status(thm)],[fof(c51,plain,((![X14]:cowlThing(X14))&(![X15]:~cowlNothing(X15))),inference(variable_rename,[status(thm)],[c50])).])).
% 1.31/1.52 cnf(c54,plain,~cowlNothing(X31),inference(split_conjunct,[status(thm)],[c52])).
% 1.31/1.52 cnf(c53,plain,cowlThing(X30),inference(split_conjunct,[status(thm)],[c52])).
% 1.31/1.52 cnf(c48,plain,xsd_integer(X37)|xsd_string(X37),inference(split_conjunct,[status(thm)],[c46])).
% 1.31/1.52 fof(axiom_3,axiom,(![X]:(cA_and_B(X)<=>(X=ib|X=ia))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 1.31/1.52 fof(c28,plain,(![X]:((~cA_and_B(X)|(X=ib|X=ia))&((X!=ib&X!=ia)|cA_and_B(X)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 1.31/1.52 fof(c29,plain,((![X]:(~cA_and_B(X)|(X=ib|X=ia)))&(![X]:((X!=ib&X!=ia)|cA_and_B(X)))),inference(shift_quantors,[status(thm)],[c28])).
% 1.31/1.52 fof(c31,plain,(![X8]:(![X9]:((~cA_and_B(X8)|(X8=ib|X8=ia))&((X9!=ib&X9!=ia)|cA_and_B(X9))))),inference(shift_quantors,[status(thm)],[fof(c30,plain,((![X8]:(~cA_and_B(X8)|(X8=ib|X8=ia)))&(![X9]:((X9!=ib&X9!=ia)|cA_and_B(X9)))),inference(variable_rename,[status(thm)],[c29])).])).
% 1.31/1.52 fof(c32,plain,(![X8]:(![X9]:((~cA_and_B(X8)|(X8=ib|X8=ia))&((X9!=ib|cA_and_B(X9))&(X9!=ia|cA_and_B(X9)))))),inference(distribute,[status(thm)],[c31])).
% 1.31/1.52 cnf(c35,plain,X48!=ia|cA_and_B(X48),inference(split_conjunct,[status(thm)],[c32])).
% 1.31/1.52 fof(axiom_2,axiom,(![X]:(cA(X)<=>X=ia)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 1.31/1.52 fof(c36,plain,(![X]:((~cA(X)|X=ia)&(X!=ia|cA(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 1.31/1.52 fof(c37,plain,((![X]:(~cA(X)|X=ia))&(![X]:(X!=ia|cA(X)))),inference(shift_quantors,[status(thm)],[c36])).
% 1.31/1.52 fof(c39,plain,(![X10]:(![X11]:((~cA(X10)|X10=ia)&(X11!=ia|cA(X11))))),inference(shift_quantors,[status(thm)],[fof(c38,plain,((![X10]:(~cA(X10)|X10=ia))&(![X11]:(X11!=ia|cA(X11)))),inference(variable_rename,[status(thm)],[c37])).])).
% 1.31/1.52 cnf(c40,plain,~cA(X49)|X49=ia,inference(split_conjunct,[status(thm)],[c39])).
% 1.31/1.52 cnf(c34,plain,X44!=ib|cA_and_B(X44),inference(split_conjunct,[status(thm)],[c32])).
% 1.31/1.52 fof(axiom_4,axiom,(![X]:(cB(X)<=>X=ib)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_4)).
% 1.31/1.52 fof(c22,plain,(![X]:((~cB(X)|X=ib)&(X!=ib|cB(X)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 1.31/1.52 fof(c23,plain,((![X]:(~cB(X)|X=ib))&(![X]:(X!=ib|cB(X)))),inference(shift_quantors,[status(thm)],[c22])).
% 1.31/1.52 fof(c25,plain,(![X6]:(![X7]:((~cB(X6)|X6=ib)&(X7!=ib|cB(X7))))),inference(shift_quantors,[status(thm)],[fof(c24,plain,((![X6]:(~cB(X6)|X6=ib))&(![X7]:(X7!=ib|cB(X7)))),inference(variable_rename,[status(thm)],[c23])).])).
% 1.31/1.52 cnf(c26,plain,~cB(X39)|X39=ib,inference(split_conjunct,[status(thm)],[c25])).
% 1.31/1.52 cnf(c27,plain,X43!=ib|cB(X43),inference(split_conjunct,[status(thm)],[c25])).
% 1.31/1.52 cnf(c41,plain,X50!=ia|cA(X50),inference(split_conjunct,[status(thm)],[c39])).
% 1.31/1.52 cnf(c33,plain,~cA_and_B(X84)|X84=ib|X84=ia,inference(split_conjunct,[status(thm)],[c32])).
% 1.31/1.52 fof(the_axiom,conjecture,(((![X]:(cowlThing(X)&(~cowlNothing(X))))&(![X]:(xsd_string(X)<=>(~xsd_integer(X)))))&(![X]:(cA_and_B(X)<=>(cB(X)|cA(X))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', the_axiom)).
% 1.31/1.52 fof(c7,negated_conjecture,(~(((![X]:(cowlThing(X)&(~cowlNothing(X))))&(![X]:(xsd_string(X)<=>(~xsd_integer(X)))))&(![X]:(cA_and_B(X)<=>(cB(X)|cA(X)))))),inference(assume_negation,[status(cth)],[the_axiom])).
% 1.31/1.52 fof(c8,negated_conjecture,(~(((![X]:(cowlThing(X)&~cowlNothing(X)))&(![X]:(xsd_string(X)<=>~xsd_integer(X))))&(![X]:(cA_and_B(X)<=>(cB(X)|cA(X)))))),inference(fof_simplification,[status(thm)],[c7])).
% 1.31/1.52 fof(c9,negated_conjecture,(((?[X]:(~cowlThing(X)|cowlNothing(X)))|(?[X]:((~xsd_string(X)|xsd_integer(X))&(xsd_string(X)|~xsd_integer(X)))))|(?[X]:((~cA_and_B(X)|(~cB(X)&~cA(X)))&(cA_and_B(X)|(cB(X)|cA(X)))))),inference(fof_nnf,[status(thm)],[c8])).
% 1.31/1.52 fof(c10,negated_conjecture,((((?[X]:~cowlThing(X))|(?[X]:cowlNothing(X)))|(?[X]:((~xsd_string(X)|xsd_integer(X))&(xsd_string(X)|~xsd_integer(X)))))|(?[X]:((~cA_and_B(X)|(~cB(X)&~cA(X)))&(cA_and_B(X)|(cB(X)|cA(X)))))),inference(shift_quantors,[status(thm)],[c9])).
% 1.31/1.52 fof(c11,negated_conjecture,((((?[X2]:~cowlThing(X2))|(?[X3]:cowlNothing(X3)))|(?[X4]:((~xsd_string(X4)|xsd_integer(X4))&(xsd_string(X4)|~xsd_integer(X4)))))|(?[X5]:((~cA_and_B(X5)|(~cB(X5)&~cA(X5)))&(cA_and_B(X5)|(cB(X5)|cA(X5)))))),inference(variable_rename,[status(thm)],[c10])).
% 1.31/1.52 fof(c12,negated_conjecture,(((~cowlThing(skolem0001)|cowlNothing(skolem0002))|((~xsd_string(skolem0003)|xsd_integer(skolem0003))&(xsd_string(skolem0003)|~xsd_integer(skolem0003))))|((~cA_and_B(skolem0004)|(~cB(skolem0004)&~cA(skolem0004)))&(cA_and_B(skolem0004)|(cB(skolem0004)|cA(skolem0004))))),inference(skolemize,[status(esa)],[c11])).
% 1.31/1.52 fof(c13,negated_conjecture,((((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(~xsd_string(skolem0003)|xsd_integer(skolem0003)))|(~cA_and_B(skolem0004)|~cB(skolem0004)))&(((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(~xsd_string(skolem0003)|xsd_integer(skolem0003)))|(~cA_and_B(skolem0004)|~cA(skolem0004))))&(((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(~xsd_string(skolem0003)|xsd_integer(skolem0003)))|(cA_and_B(skolem0004)|(cB(skolem0004)|cA(skolem0004)))))&(((((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(xsd_string(skolem0003)|~xsd_integer(skolem0003)))|(~cA_and_B(skolem0004)|~cB(skolem0004)))&(((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(xsd_string(skolem0003)|~xsd_integer(skolem0003)))|(~cA_and_B(skolem0004)|~cA(skolem0004))))&(((~cowlThing(skolem0001)|cowlNothing(skolem0002))|(xsd_string(skolem0003)|~xsd_integer(skolem0003)))|(cA_and_B(skolem0004)|(cB(skolem0004)|cA(skolem0004)))))),inference(distribute,[status(thm)],[c12])).
% 1.31/1.52 cnf(c16,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|cA_and_B(skolem0004)|cB(skolem0004)|cA(skolem0004),inference(split_conjunct,[status(thm)],[c13])).
% 1.31/1.52 cnf(c93,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_integer(skolem0003)|cA_and_B(skolem0004)|cB(skolem0004)|cA(skolem0004),inference(resolution,[status(thm)],[c16, c48])).
% 1.31/1.52 cnf(c94,plain,cowlNothing(skolem0002)|xsd_integer(skolem0003)|cA_and_B(skolem0004)|cB(skolem0004)|cA(skolem0004),inference(resolution,[status(thm)],[c93, c53])).
% 1.31/1.52 cnf(c96,plain,xsd_integer(skolem0003)|cA_and_B(skolem0004)|cB(skolem0004)|cA(skolem0004),inference(resolution,[status(thm)],[c94, c54])).
% 1.31/1.52 cnf(c111,plain,xsd_integer(skolem0003)|cA_and_B(skolem0004)|cA(skolem0004)|skolem0004=ib,inference(resolution,[status(thm)],[c96, c26])).
% 1.31/1.52 cnf(c122,plain,xsd_integer(skolem0003)|cA_and_B(skolem0004)|cA(skolem0004),inference(resolution,[status(thm)],[c111, c34])).
% 1.31/1.52 cnf(c134,plain,xsd_integer(skolem0003)|cA_and_B(skolem0004)|skolem0004=ia,inference(resolution,[status(thm)],[c122, c40])).
% 1.31/1.52 cnf(c139,plain,xsd_integer(skolem0003)|skolem0004=ia|skolem0004=ib,inference(resolution,[status(thm)],[c134, c33])).
% 1.31/1.52 cnf(c154,plain,xsd_integer(skolem0003)|skolem0004=ib|cA(skolem0004),inference(resolution,[status(thm)],[c139, c41])).
% 1.31/1.52 cnf(c178,plain,xsd_integer(skolem0003)|cA(skolem0004)|cB(skolem0004),inference(resolution,[status(thm)],[c154, c27])).
% 1.31/1.52 cnf(c184,plain,cA(skolem0004)|cB(skolem0004)|~xsd_string(skolem0003),inference(resolution,[status(thm)],[c178, c47])).
% 1.31/1.52 cnf(c19,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|cA_and_B(skolem0004)|cB(skolem0004)|cA(skolem0004),inference(split_conjunct,[status(thm)],[c13])).
% 1.31/1.52 cnf(c95,plain,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|cA_and_B(skolem0004)|cB(skolem0004)|cA(skolem0004),inference(resolution,[status(thm)],[c19, c48])).
% 1.31/1.52 cnf(c131,plain,cowlNothing(skolem0002)|xsd_string(skolem0003)|cA_and_B(skolem0004)|cB(skolem0004)|cA(skolem0004),inference(resolution,[status(thm)],[c95, c53])).
% 1.31/1.52 cnf(c375,plain,xsd_string(skolem0003)|cA_and_B(skolem0004)|cB(skolem0004)|cA(skolem0004),inference(resolution,[status(thm)],[c131, c54])).
% 1.31/1.52 cnf(c409,plain,cA_and_B(skolem0004)|cB(skolem0004)|cA(skolem0004),inference(resolution,[status(thm)],[c375, c184])).
% 1.31/1.52 cnf(c423,plain,cA_and_B(skolem0004)|cA(skolem0004)|skolem0004=ib,inference(resolution,[status(thm)],[c409, c26])).
% 1.31/1.52 cnf(c433,plain,cA_and_B(skolem0004)|cA(skolem0004),inference(resolution,[status(thm)],[c423, c34])).
% 1.31/1.52 cnf(c446,plain,cA_and_B(skolem0004)|skolem0004=ia,inference(resolution,[status(thm)],[c433, c40])).
% 1.31/1.52 cnf(c458,plain,cA_and_B(skolem0004),inference(resolution,[status(thm)],[c446, c35])).
% 1.31/1.52 cnf(c14,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|~cA_and_B(skolem0004)|~cB(skolem0004),inference(split_conjunct,[status(thm)],[c13])).
% 1.31/1.52 cnf(c15,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|xsd_integer(skolem0003)|~cA_and_B(skolem0004)|~cA(skolem0004),inference(split_conjunct,[status(thm)],[c13])).
% 1.31/1.52 cnf(c186,plain,xsd_integer(skolem0003)|cB(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003)|~cA_and_B(skolem0004),inference(resolution,[status(thm)],[c178, c15])).
% 1.31/1.52 cnf(c600,plain,xsd_integer(skolem0003)|cB(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|~xsd_string(skolem0003),inference(resolution,[status(thm)],[c186, c458])).
% 1.31/1.52 cnf(c1197,plain,xsd_integer(skolem0003)|cB(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002),inference(resolution,[status(thm)],[c600, c48])).
% 1.31/1.52 cnf(c1198,plain,xsd_integer(skolem0003)|cB(skolem0004)|cowlNothing(skolem0002),inference(resolution,[status(thm)],[c1197, c53])).
% 1.31/1.52 cnf(c1205,plain,xsd_integer(skolem0003)|cowlNothing(skolem0002)|~cowlThing(skolem0001)|~xsd_string(skolem0003)|~cA_and_B(skolem0004),inference(resolution,[status(thm)],[c1198, c14])).
% 1.31/1.52 cnf(c1590,plain,xsd_integer(skolem0003)|cowlNothing(skolem0002)|~cowlThing(skolem0001)|~xsd_string(skolem0003),inference(resolution,[status(thm)],[c1205, c458])).
% 1.31/1.52 cnf(c1591,plain,xsd_integer(skolem0003)|cowlNothing(skolem0002)|~cowlThing(skolem0001),inference(resolution,[status(thm)],[c1590, c48])).
% 1.31/1.52 cnf(c1592,plain,xsd_integer(skolem0003)|cowlNothing(skolem0002),inference(resolution,[status(thm)],[c1591, c53])).
% 1.31/1.52 cnf(c1594,plain,xsd_integer(skolem0003),inference(resolution,[status(thm)],[c1592, c54])).
% 1.31/1.52 cnf(c1595,plain,~xsd_string(skolem0003),inference(resolution,[status(thm)],[c1594, c47])).
% 1.31/1.52 cnf(c17,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|~cA_and_B(skolem0004)|~cB(skolem0004),inference(split_conjunct,[status(thm)],[c13])).
% 1.31/1.52 cnf(c18,negated_conjecture,~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|~cA_and_B(skolem0004)|~cA(skolem0004),inference(split_conjunct,[status(thm)],[c13])).
% 1.31/1.52 cnf(c448,plain,skolem0004=ia|skolem0004=ib,inference(resolution,[status(thm)],[c446, c33])).
% 1.31/1.52 cnf(c462,plain,skolem0004=ib|cA(skolem0004),inference(resolution,[status(thm)],[c448, c41])).
% 1.31/1.52 cnf(c487,plain,cA(skolem0004)|cB(skolem0004),inference(resolution,[status(thm)],[c462, c27])).
% 1.31/1.52 cnf(c497,plain,cB(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003)|~cA_and_B(skolem0004),inference(resolution,[status(thm)],[c487, c18])).
% 1.31/1.52 cnf(c1332,plain,cB(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003)|~xsd_integer(skolem0003),inference(resolution,[status(thm)],[c497, c458])).
% 1.31/1.52 cnf(c1597,plain,cB(skolem0004)|~cowlThing(skolem0001)|cowlNothing(skolem0002)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c1332, c1594])).
% 1.31/1.52 cnf(c1599,plain,cB(skolem0004)|cowlNothing(skolem0002)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c1597, c53])).
% 1.31/1.52 cnf(c1600,plain,cowlNothing(skolem0002)|xsd_string(skolem0003)|~cowlThing(skolem0001)|~xsd_integer(skolem0003)|~cA_and_B(skolem0004),inference(resolution,[status(thm)],[c1599, c17])).
% 1.31/1.52 cnf(c1775,plain,cowlNothing(skolem0002)|xsd_string(skolem0003)|~cowlThing(skolem0001)|~xsd_integer(skolem0003),inference(resolution,[status(thm)],[c1600, c458])).
% 1.31/1.52 cnf(c1776,plain,cowlNothing(skolem0002)|xsd_string(skolem0003)|~cowlThing(skolem0001),inference(resolution,[status(thm)],[c1775, c1594])).
% 1.31/1.52 cnf(c1778,plain,cowlNothing(skolem0002)|xsd_string(skolem0003),inference(resolution,[status(thm)],[c1776, c53])).
% 1.31/1.52 cnf(c1779,plain,xsd_string(skolem0003),inference(resolution,[status(thm)],[c1778, c54])).
% 1.31/1.52 cnf(c1781,plain,$false,inference(resolution,[status(thm)],[c1779, c1595])).
% 1.31/1.52 % SZS output end CNFRefutation
% 1.31/1.52
% 1.31/1.52 % Initial clauses : 36
% 1.31/1.52 % Processed clauses : 318
% 1.31/1.52 % Factors computed : 1
% 1.31/1.52 % Resolvents computed: 1705
% 1.31/1.52 % Tautologies deleted: 60
% 1.31/1.52 % Forward subsumed : 1342
% 1.31/1.52 % Backward subsumed : 257
% 1.31/1.52 % -------- CPU Time ---------
% 1.31/1.52 % User time : 1.114 s
% 1.31/1.52 % System time : 0.016 s
% 1.31/1.52 % Total time : 1.130 s
%------------------------------------------------------------------------------