%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS057+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n020.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.47s 0.69s
% Output : Saturation 0.47s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : KRS057+1 : TPTP v8.1.2. Released v3.1.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n020.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:06:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.47/0.69 % Version: 1.5
% 0.47/0.69 % SZS status Satisfiable
% 0.47/0.69 % SZS output start Saturation
% 0.47/0.69 fof(axiom_3,axiom,(![X]:((((((cB(X)<=>cC(X))&(cB(X)<=>X=iA))&(cB(X)<=>(~cD(X))))&(cC(X)<=>X=iA))&(cC(X)<=>(~cD(X))))&(X=iA<=>(~cD(X))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 0.47/0.69 fof(c7,plain,(![X]:((((((cB(X)<=>cC(X))&(cB(X)<=>X=iA))&(cB(X)<=>~cD(X)))&(cC(X)<=>X=iA))&(cC(X)<=>~cD(X)))&(X=iA<=>~cD(X)))),inference(fof_simplification,[status(thm)],[axiom_3])).
% 0.47/0.69 fof(c8,plain,(![X]:(((((((~cB(X)|cC(X))&(~cC(X)|cB(X)))&((~cB(X)|X=iA)&(X!=iA|cB(X))))&((~cB(X)|~cD(X))&(cD(X)|cB(X))))&((~cC(X)|X=iA)&(X!=iA|cC(X))))&((~cC(X)|~cD(X))&(cD(X)|cC(X))))&((X!=iA|~cD(X))&(cD(X)|X=iA)))),inference(fof_nnf,[status(thm)],[c7])).
% 0.47/0.69 fof(c9,plain,(((((((![X]:(~cB(X)|cC(X)))&(![X]:(~cC(X)|cB(X))))&((![X]:(~cB(X)|X=iA))&(![X]:(X!=iA|cB(X)))))&((![X]:(~cB(X)|~cD(X)))&(![X]:(cD(X)|cB(X)))))&((![X]:(~cC(X)|X=iA))&(![X]:(X!=iA|cC(X)))))&((![X]:(~cC(X)|~cD(X)))&(![X]:(cD(X)|cC(X)))))&((![X]:(X!=iA|~cD(X)))&(![X]:(cD(X)|X=iA)))),inference(shift_quantors,[status(thm)],[c8])).
% 0.47/0.69 fof(c11,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(((((((~cB(X2)|cC(X2))&(~cC(X3)|cB(X3)))&((~cB(X4)|X4=iA)&(X5!=iA|cB(X5))))&((~cB(X6)|~cD(X6))&(cD(X7)|cB(X7))))&((~cC(X8)|X8=iA)&(X9!=iA|cC(X9))))&((~cC(X10)|~cD(X10))&(cD(X11)|cC(X11))))&((X12!=iA|~cD(X12))&(cD(X13)|X13=iA))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c10,plain,(((((((![X2]:(~cB(X2)|cC(X2)))&(![X3]:(~cC(X3)|cB(X3))))&((![X4]:(~cB(X4)|X4=iA))&(![X5]:(X5!=iA|cB(X5)))))&((![X6]:(~cB(X6)|~cD(X6)))&(![X7]:(cD(X7)|cB(X7)))))&((![X8]:(~cC(X8)|X8=iA))&(![X9]:(X9!=iA|cC(X9)))))&((![X10]:(~cC(X10)|~cD(X10)))&(![X11]:(cD(X11)|cC(X11)))))&((![X12]:(X12!=iA|~cD(X12)))&(![X13]:(cD(X13)|X13=iA)))),inference(variable_rename,[status(thm)],[c9])).])).
% 0.47/0.69 cnf(c20,plain,~cC(X42)|~cD(X42),inference(split_conjunct,[status(thm)],[c11])).
% 0.47/0.69 cnf(c5,axiom,X77!=X76|~xsd_integer(X77)|xsd_integer(X76),theory(equality)).
% 0.47/0.69 cnf(symmetry,axiom,X36!=X37|X37=X36,theory(equality)).
% 0.47/0.69 cnf(c23,plain,cD(X74)|X74=iA,inference(split_conjunct,[status(thm)],[c11])).
% 0.47/0.69 cnf(c86,plain,cD(X93)|iA=X93,inference(resolution,[status(thm)],[c23, symmetry])).
% 0.47/0.69 cnf(c108,plain,cD(X126)|~xsd_integer(iA)|xsd_integer(X126),inference(resolution,[status(thm)],[c86, c5])).
% 0.47/0.69 fof(axiom_1,axiom,(![X]:(xsd_string(X)<=>(~xsd_integer(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_1)).
% 0.47/0.69 fof(c25,plain,(![X]:(xsd_string(X)<=>~xsd_integer(X))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 0.47/0.69 fof(c26,plain,(![X]:((~xsd_string(X)|~xsd_integer(X))&(xsd_integer(X)|xsd_string(X)))),inference(fof_nnf,[status(thm)],[c25])).
% 0.47/0.69 fof(c27,plain,((![X]:(~xsd_string(X)|~xsd_integer(X)))&(![X]:(xsd_integer(X)|xsd_string(X)))),inference(shift_quantors,[status(thm)],[c26])).
% 0.47/0.69 fof(c29,plain,(![X14]:(![X15]:((~xsd_string(X14)|~xsd_integer(X14))&(xsd_integer(X15)|xsd_string(X15))))),inference(shift_quantors,[status(thm)],[fof(c28,plain,((![X14]:(~xsd_string(X14)|~xsd_integer(X14)))&(![X15]:(xsd_integer(X15)|xsd_string(X15)))),inference(variable_rename,[status(thm)],[c27])).])).
% 0.47/0.69 cnf(c31,plain,xsd_integer(X48)|xsd_string(X48),inference(split_conjunct,[status(thm)],[c29])).
% 0.47/0.69 cnf(c95,plain,~xsd_integer(X115)|xsd_integer(iA)|cD(X115),inference(resolution,[status(thm)],[c5, c23])).
% 0.47/0.69 cnf(c115,plain,xsd_integer(iA)|cD(X128)|xsd_string(X128),inference(resolution,[status(thm)],[c95, c31])).
% 0.47/0.69 cnf(c125,plain,cD(X142)|xsd_string(X142)|cD(X143)|xsd_integer(X143),inference(resolution,[status(thm)],[c115, c108])).
% 0.47/0.69 cnf(c168,plain,cD(X220)|xsd_string(X220)|xsd_integer(X219)|~cC(X219),inference(resolution,[status(thm)],[c125, c20])).
% 0.47/0.69 cnf(c16,plain,~cB(X40)|~cD(X40),inference(split_conjunct,[status(thm)],[c11])).
% 0.47/0.69 cnf(c167,plain,cD(X215)|xsd_string(X215)|xsd_integer(X214)|~cB(X214),inference(resolution,[status(thm)],[c125, c16])).
% 0.47/0.69 cnf(c163,plain,xsd_string(X211)|cD(X212)|xsd_integer(X212)|~cC(X211),inference(resolution,[status(thm)],[c125, c20])).
% 0.47/0.69 cnf(transitivity,axiom,X44!=X45|X45!=X43|X44=X43,theory(equality)).
% 0.47/0.69 cnf(c103,plain,cD(X123)|X124!=iA|X124=X123,inference(resolution,[status(thm)],[c86, transitivity])).
% 0.47/0.69 cnf(c122,plain,cD(X131)|X132=X131|cD(X132),inference(resolution,[status(thm)],[c103, c23])).
% 0.47/0.69 cnf(c148,plain,cD(X204)|cD(X206)|X205!=X206|X205=X204,inference(resolution,[status(thm)],[c122, transitivity])).
% 0.47/0.69 cnf(c162,plain,xsd_string(X201)|cD(X202)|xsd_integer(X202)|~cB(X201),inference(resolution,[status(thm)],[c125, c16])).
% 0.47/0.69 cnf(c6,axiom,X85!=X84|~xsd_string(X85)|xsd_string(X84),theory(equality)).
% 0.47/0.69 cnf(c155,plain,cD(X199)|cD(X200)|~xsd_string(X200)|xsd_string(X199),inference(resolution,[status(thm)],[c122, c6])).
% 0.47/0.69 cnf(c154,plain,cD(X198)|cD(X197)|~xsd_integer(X197)|xsd_integer(X198),inference(resolution,[status(thm)],[c122, c5])).
% 0.47/0.69 cnf(c159,plain,cD(X168)|X169=X168|~cC(X169),inference(resolution,[status(thm)],[c122, c20])).
% 0.47/0.69 cnf(c158,plain,cD(X164)|X165=X164|~cB(X165),inference(resolution,[status(thm)],[c122, c16])).
% 0.47/0.69 cnf(c144,plain,X156=X155|cD(X156)|~cC(X155),inference(resolution,[status(thm)],[c122, c20])).
% 0.47/0.69 cnf(c143,plain,X153=X152|cD(X153)|~cB(X152),inference(resolution,[status(thm)],[c122, c16])).
% 0.47/0.69 cnf(c97,plain,~xsd_string(X120)|xsd_string(iA)|cD(X120),inference(resolution,[status(thm)],[c6, c23])).
% 0.47/0.69 cnf(c119,plain,xsd_string(iA)|cD(X130)|xsd_integer(X130),inference(resolution,[status(thm)],[c97, c31])).
% 0.47/0.69 cnf(c137,plain,xsd_string(iA)|xsd_integer(X149)|~cC(X149),inference(resolution,[status(thm)],[c119, c20])).
% 0.47/0.69 cnf(c136,plain,xsd_string(iA)|xsd_integer(X148)|~cB(X148),inference(resolution,[status(thm)],[c119, c16])).
% 0.47/0.69 cnf(c130,plain,xsd_integer(iA)|xsd_string(X146)|~cC(X146),inference(resolution,[status(thm)],[c115, c20])).
% 0.47/0.69 cnf(c129,plain,xsd_integer(iA)|xsd_string(X145)|~cB(X145),inference(resolution,[status(thm)],[c115, c16])).
% 0.47/0.69 cnf(c109,plain,cD(X127)|~xsd_string(iA)|xsd_string(X127),inference(resolution,[status(thm)],[c86, c6])).
% 0.47/0.69 cnf(c88,plain,cD(X117)|X116!=X117|X116=iA,inference(resolution,[status(thm)],[c23, transitivity])).
% 0.47/0.69 cnf(c100,plain,iA=X98|~cC(X98),inference(resolution,[status(thm)],[c86, c20])).
% 0.47/0.69 cnf(c99,plain,iA=X95|~cB(X95),inference(resolution,[status(thm)],[c86, c16])).
% 0.47/0.69 cnf(reflexivity,axiom,X34=X34,theory(equality)).
% 0.47/0.69 cnf(c22,plain,X71!=iA|~cD(X71),inference(split_conjunct,[status(thm)],[c11])).
% 0.47/0.69 cnf(c80,plain,~cD(iA),inference(resolution,[status(thm)],[c22, reflexivity])).
% 0.47/0.69 cnf(c19,plain,X70!=iA|cC(X70),inference(split_conjunct,[status(thm)],[c11])).
% 0.47/0.69 cnf(c18,plain,~cC(X67)|X67=iA,inference(split_conjunct,[status(thm)],[c11])).
% 0.47/0.69 cnf(c12,plain,~cB(X35)|cC(X35),inference(split_conjunct,[status(thm)],[c11])).
% 0.47/0.69 cnf(c15,plain,X63!=iA|cB(X63),inference(split_conjunct,[status(thm)],[c11])).
% 0.47/0.69 cnf(c72,plain,cB(iA),inference(resolution,[status(thm)],[c15, reflexivity])).
% 0.47/0.69 cnf(c73,plain,cC(iA),inference(resolution,[status(thm)],[c72, c12])).
% 0.47/0.69 cnf(c2,axiom,X65!=X64|~cD(X65)|cD(X64),theory(equality)).
% 0.47/0.69 cnf(c14,plain,~cB(X62)|X62=iA,inference(split_conjunct,[status(thm)],[c11])).
% 0.47/0.69 cnf(c1,axiom,X59!=X58|~cC(X59)|cC(X58),theory(equality)).
% 0.47/0.69 cnf(c0,axiom,X52!=X51|~cB(X52)|cB(X51),theory(equality)).
% 0.47/0.69 cnf(c30,plain,~xsd_string(X47)|~xsd_integer(X47),inference(split_conjunct,[status(thm)],[c29])).
% 0.47/0.69 cnf(c21,plain,cD(X46)|cC(X46),inference(split_conjunct,[status(thm)],[c11])).
% 0.47/0.69 cnf(c17,plain,cD(X41)|cB(X41),inference(split_conjunct,[status(thm)],[c11])).
% 0.47/0.69 cnf(c13,plain,~cC(X39)|cB(X39),inference(split_conjunct,[status(thm)],[c11])).
% 0.47/0.69 fof(axiom_0,axiom,(![X]:(cowlThing(X)&(~cowlNothing(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_0)).
% 0.47/0.69 fof(c32,plain,(![X]:(cowlThing(X)&~cowlNothing(X))),inference(fof_simplification,[status(thm)],[axiom_0])).
% 0.47/0.69 fof(c33,plain,((![X]:cowlThing(X))&(![X]:~cowlNothing(X))),inference(shift_quantors,[status(thm)],[c32])).
% 0.47/0.69 fof(c35,plain,(![X16]:(![X17]:(cowlThing(X16)&~cowlNothing(X17)))),inference(shift_quantors,[status(thm)],[fof(c34,plain,((![X16]:cowlThing(X16))&(![X17]:~cowlNothing(X17))),inference(variable_rename,[status(thm)],[c33])).])).
% 0.47/0.69 cnf(c37,plain,~cowlNothing(X33),inference(split_conjunct,[status(thm)],[c35])).
% 0.47/0.69 cnf(c36,plain,cowlThing(X32),inference(split_conjunct,[status(thm)],[c35])).
% 0.47/0.69 % SZS output end Saturation
% 0.47/0.69
% 0.47/0.69 % Initial clauses : 34
% 0.47/0.69 % Processed clauses : 55
% 0.47/0.69 % Factors computed : 3
% 0.47/0.69 % Resolvents computed: 146
% 0.47/0.69 % Tautologies deleted: 15
% 0.47/0.69 % Forward subsumed : 113
% 0.47/0.69 % Backward subsumed : 0
% 0.47/0.69 % -------- CPU Time ---------
% 0.47/0.69 % User time : 0.309 s
% 0.47/0.69 % System time : 0.018 s
% 0.47/0.69 % Total time : 0.327 s
%------------------------------------------------------------------------------