%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS039+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n009.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:32 EDT 2024
% Result : Satisfiable 0.20s 0.54s
% Output : Saturation 0.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : KRS039+1 : TPTP v8.1.2. Released v3.1.0.
% 0.04/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.33 % Computer : n009.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % 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:05:07 EDT 2024
% 0.14/0.34 % CPUTime :
% 0.20/0.54 % Version: 1.5
% 0.20/0.54 % SZS status Satisfiable
% 0.20/0.54 % SZS output start Saturation
% 0.20/0.54 fof(axiom_2,axiom,(![X]:(cSatisfiable(X)<=>((?[Y]:(rr(X,Y)&(![Z]:(rinvR(Y,Z)=>(![W]:(rr1(Z,W)=>cp(W)))))))&(?[Y]:(rr(X,Y)&(![Z]:(rinvR(Y,Z)=>(![W]:(rr1(Z,W)=>(~cp(W))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 0.20/0.54 fof(c7,plain,(![X]:(cSatisfiable(X)<=>((?[Y]:(rr(X,Y)&(![Z]:(rinvR(Y,Z)=>(![W]:(rr1(Z,W)=>cp(W)))))))&(?[Y]:(rr(X,Y)&(![Z]:(rinvR(Y,Z)=>(![W]:(rr1(Z,W)=>~cp(W)))))))))),inference(fof_simplification,[status(thm)],[axiom_2])).
% 0.20/0.54 fof(c8,plain,(![X]:((~cSatisfiable(X)|((?[Y]:(rr(X,Y)&(![Z]:(~rinvR(Y,Z)|(![W]:(~rr1(Z,W)|cp(W)))))))&(?[Y]:(rr(X,Y)&(![Z]:(~rinvR(Y,Z)|(![W]:(~rr1(Z,W)|~cp(W)))))))))&(((![Y]:(~rr(X,Y)|(?[Z]:(rinvR(Y,Z)&(?[W]:(rr1(Z,W)&~cp(W)))))))|(![Y]:(~rr(X,Y)|(?[Z]:(rinvR(Y,Z)&(?[W]:(rr1(Z,W)&cp(W))))))))|cSatisfiable(X)))),inference(fof_nnf,[status(thm)],[c7])).
% 0.20/0.54 fof(c9,plain,((![X]:(~cSatisfiable(X)|((?[Y]:(rr(X,Y)&(![Z]:(~rinvR(Y,Z)|(![W]:(~rr1(Z,W)|cp(W)))))))&(?[Y]:(rr(X,Y)&(![Z]:(~rinvR(Y,Z)|(![W]:(~rr1(Z,W)|~cp(W))))))))))&(![X]:(((![Y]:(~rr(X,Y)|(?[Z]:(rinvR(Y,Z)&(?[W]:(rr1(Z,W)&~cp(W)))))))|(![Y]:(~rr(X,Y)|(?[Z]:(rinvR(Y,Z)&(?[W]:(rr1(Z,W)&cp(W))))))))|cSatisfiable(X)))),inference(shift_quantors,[status(thm)],[c8])).
% 0.20/0.54 fof(c10,plain,((![X6]:(~cSatisfiable(X6)|((?[X7]:(rr(X6,X7)&(![X8]:(~rinvR(X7,X8)|(![X9]:(~rr1(X8,X9)|cp(X9)))))))&(?[X10]:(rr(X6,X10)&(![X11]:(~rinvR(X10,X11)|(![X12]:(~rr1(X11,X12)|~cp(X12))))))))))&(![X13]:(((![X14]:(~rr(X13,X14)|(?[X15]:(rinvR(X14,X15)&(?[X16]:(rr1(X15,X16)&~cp(X16)))))))|(![X17]:(~rr(X13,X17)|(?[X18]:(rinvR(X17,X18)&(?[X19]:(rr1(X18,X19)&cp(X19))))))))|cSatisfiable(X13)))),inference(variable_rename,[status(thm)],[c9])).
% 0.20/0.54 fof(c12,plain,(![X6]:(![X8]:(![X9]:(![X11]:(![X12]:(![X13]:(![X14]:(![X17]:((~cSatisfiable(X6)|((rr(X6,skolem0001(X6))&(~rinvR(skolem0001(X6),X8)|(~rr1(X8,X9)|cp(X9))))&(rr(X6,skolem0002(X6))&(~rinvR(skolem0002(X6),X11)|(~rr1(X11,X12)|~cp(X12))))))&(((~rr(X13,X14)|(rinvR(X14,skolem0003(X13,X14))&(rr1(skolem0003(X13,X14),skolem0004(X13,X14))&~cp(skolem0004(X13,X14)))))|(~rr(X13,X17)|(rinvR(X17,skolem0005(X13,X17))&(rr1(skolem0005(X13,X17),skolem0006(X13,X17))&cp(skolem0006(X13,X17))))))|cSatisfiable(X13))))))))))),inference(shift_quantors,[status(thm)],[fof(c11,plain,((![X6]:(~cSatisfiable(X6)|((rr(X6,skolem0001(X6))&(![X8]:(~rinvR(skolem0001(X6),X8)|(![X9]:(~rr1(X8,X9)|cp(X9))))))&(rr(X6,skolem0002(X6))&(![X11]:(~rinvR(skolem0002(X6),X11)|(![X12]:(~rr1(X11,X12)|~cp(X12)))))))))&(![X13]:(((![X14]:(~rr(X13,X14)|(rinvR(X14,skolem0003(X13,X14))&(rr1(skolem0003(X13,X14),skolem0004(X13,X14))&~cp(skolem0004(X13,X14))))))|(![X17]:(~rr(X13,X17)|(rinvR(X17,skolem0005(X13,X17))&(rr1(skolem0005(X13,X17),skolem0006(X13,X17))&cp(skolem0006(X13,X17)))))))|cSatisfiable(X13)))),inference(skolemize,[status(esa)],[c10])).])).
% 0.20/0.54 fof(c13,plain,(![X6]:(![X8]:(![X9]:(![X11]:(![X12]:(![X13]:(![X14]:(![X17]:((((~cSatisfiable(X6)|rr(X6,skolem0001(X6)))&(~cSatisfiable(X6)|(~rinvR(skolem0001(X6),X8)|(~rr1(X8,X9)|cp(X9)))))&((~cSatisfiable(X6)|rr(X6,skolem0002(X6)))&(~cSatisfiable(X6)|(~rinvR(skolem0002(X6),X11)|(~rr1(X11,X12)|~cp(X12))))))&(((((~rr(X13,X14)|rinvR(X14,skolem0003(X13,X14)))|(~rr(X13,X17)|rinvR(X17,skolem0005(X13,X17))))|cSatisfiable(X13))&((((~rr(X13,X14)|rinvR(X14,skolem0003(X13,X14)))|(~rr(X13,X17)|rr1(skolem0005(X13,X17),skolem0006(X13,X17))))|cSatisfiable(X13))&(((~rr(X13,X14)|rinvR(X14,skolem0003(X13,X14)))|(~rr(X13,X17)|cp(skolem0006(X13,X17))))|cSatisfiable(X13))))&(((((~rr(X13,X14)|rr1(skolem0003(X13,X14),skolem0004(X13,X14)))|(~rr(X13,X17)|rinvR(X17,skolem0005(X13,X17))))|cSatisfiable(X13))&((((~rr(X13,X14)|rr1(skolem0003(X13,X14),skolem0004(X13,X14)))|(~rr(X13,X17)|rr1(skolem0005(X13,X17),skolem0006(X13,X17))))|cSatisfiable(X13))&(((~rr(X13,X14)|rr1(skolem0003(X13,X14),skolem0004(X13,X14)))|(~rr(X13,X17)|cp(skolem0006(X13,X17))))|cSatisfiable(X13))))&((((~rr(X13,X14)|~cp(skolem0004(X13,X14)))|(~rr(X13,X17)|rinvR(X17,skolem0005(X13,X17))))|cSatisfiable(X13))&((((~rr(X13,X14)|~cp(skolem0004(X13,X14)))|(~rr(X13,X17)|rr1(skolem0005(X13,X17),skolem0006(X13,X17))))|cSatisfiable(X13))&(((~rr(X13,X14)|~cp(skolem0004(X13,X14)))|(~rr(X13,X17)|cp(skolem0006(X13,X17))))|cSatisfiable(X13))))))))))))))),inference(distribute,[status(thm)],[c12])).
% 0.20/0.54 cnf(c22,plain,~rr(X80,X81)|rr1(skolem0003(X80,X81),skolem0004(X80,X81))|~rr(X80,X79)|rr1(skolem0005(X80,X79),skolem0006(X80,X79))|cSatisfiable(X80),inference(split_conjunct,[status(thm)],[c13])).
% 0.20/0.54 cnf(c74,plain,~rr(X83,X82)|rr1(skolem0003(X83,X82),skolem0004(X83,X82))|rr1(skolem0005(X83,X82),skolem0006(X83,X82))|cSatisfiable(X83),inference(factor,[status(thm)],[c22])).
% 0.20/0.54 cnf(c21,plain,~rr(X75,X76)|rr1(skolem0003(X75,X76),skolem0004(X75,X76))|~rr(X75,X74)|rinvR(X74,skolem0005(X75,X74))|cSatisfiable(X75),inference(split_conjunct,[status(thm)],[c13])).
% 0.20/0.54 cnf(c69,plain,~rr(X77,X78)|rr1(skolem0003(X77,X78),skolem0004(X77,X78))|rinvR(X78,skolem0005(X77,X78))|cSatisfiable(X77),inference(factor,[status(thm)],[c21])).
% 0.20/0.54 cnf(c19,plain,~rr(X68,X69)|rinvR(X69,skolem0003(X68,X69))|~rr(X68,X67)|rr1(skolem0005(X68,X67),skolem0006(X68,X67))|cSatisfiable(X68),inference(split_conjunct,[status(thm)],[c13])).
% 0.20/0.54 cnf(c64,plain,~rr(X70,X71)|rinvR(X71,skolem0003(X70,X71))|rr1(skolem0005(X70,X71),skolem0006(X70,X71))|cSatisfiable(X70),inference(factor,[status(thm)],[c19])).
% 0.20/0.54 cnf(c25,plain,~rr(X65,X66)|~cp(skolem0004(X65,X66))|~rr(X65,X64)|rr1(skolem0005(X65,X64),skolem0006(X65,X64))|cSatisfiable(X65),inference(split_conjunct,[status(thm)],[c13])).
% 0.20/0.54 cnf(c23,plain,~rr(X60,X61)|rr1(skolem0003(X60,X61),skolem0004(X60,X61))|~rr(X60,X59)|cp(skolem0006(X60,X59))|cSatisfiable(X60),inference(split_conjunct,[status(thm)],[c13])).
% 0.20/0.54 cnf(c59,plain,~rr(X63,X62)|rr1(skolem0003(X63,X62),skolem0004(X63,X62))|cp(skolem0006(X63,X62))|cSatisfiable(X63),inference(factor,[status(thm)],[c23])).
% 0.20/0.54 cnf(c24,plain,~rr(X57,X58)|~cp(skolem0004(X57,X58))|~rr(X57,X56)|rinvR(X56,skolem0005(X57,X56))|cSatisfiable(X57),inference(split_conjunct,[status(thm)],[c13])).
% 0.20/0.54 cnf(c18,plain,~rr(X52,X53)|rinvR(X53,skolem0003(X52,X53))|~rr(X52,X51)|rinvR(X51,skolem0005(X52,X51))|cSatisfiable(X52),inference(split_conjunct,[status(thm)],[c13])).
% 0.20/0.54 cnf(c54,plain,~rr(X54,X55)|rinvR(X55,skolem0003(X54,X55))|rinvR(X55,skolem0005(X54,X55))|cSatisfiable(X54),inference(factor,[status(thm)],[c18])).
% 0.20/0.54 cnf(c20,plain,~rr(X47,X48)|rinvR(X48,skolem0003(X47,X48))|~rr(X47,X46)|cp(skolem0006(X47,X46))|cSatisfiable(X47),inference(split_conjunct,[status(thm)],[c13])).
% 0.20/0.54 cnf(c49,plain,~rr(X50,X49)|rinvR(X49,skolem0003(X50,X49))|cp(skolem0006(X50,X49))|cSatisfiable(X50),inference(factor,[status(thm)],[c20])).
% 0.20/0.54 cnf(c26,plain,~rr(X44,X45)|~cp(skolem0004(X44,X45))|~rr(X44,X43)|cp(skolem0006(X44,X43))|cSatisfiable(X44),inference(split_conjunct,[status(thm)],[c13])).
% 0.20/0.54 fof(axiom_3,axiom,(![X]:(![Y]:(rinvR(X,Y)<=>rr(Y,X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 0.20/0.54 fof(c1,plain,(![X]:(![Y]:((~rinvR(X,Y)|rr(Y,X))&(~rr(Y,X)|rinvR(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.20/0.54 fof(c2,plain,((![X]:(![Y]:(~rinvR(X,Y)|rr(Y,X))))&(![X]:(![Y]:(~rr(Y,X)|rinvR(X,Y))))),inference(shift_quantors,[status(thm)],[c1])).
% 0.20/0.54 fof(c4,plain,(![X2]:(![X3]:(![X4]:(![X5]:((~rinvR(X2,X3)|rr(X3,X2))&(~rr(X5,X4)|rinvR(X4,X5))))))),inference(shift_quantors,[status(thm)],[fof(c3,plain,((![X2]:(![X3]:(~rinvR(X2,X3)|rr(X3,X2))))&(![X4]:(![X5]:(~rr(X5,X4)|rinvR(X4,X5))))),inference(variable_rename,[status(thm)],[c2])).])).
% 0.20/0.54 cnf(c6,plain,~rr(X32,X31)|rinvR(X31,X32),inference(split_conjunct,[status(thm)],[c4])).
% 0.20/0.54 fof(axiom_4,axiom,cSatisfiable(i2003_11_14_17_15_58383),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_4)).
% 0.20/0.54 cnf(c0,plain,cSatisfiable(i2003_11_14_17_15_58383),inference(split_conjunct,[status(thm)],[axiom_4])).
% 0.20/0.54 cnf(c16,plain,~cSatisfiable(X37)|rr(X37,skolem0002(X37)),inference(split_conjunct,[status(thm)],[c13])).
% 0.20/0.54 cnf(c45,plain,rr(i2003_11_14_17_15_58383,skolem0002(i2003_11_14_17_15_58383)),inference(resolution,[status(thm)],[c16, c0])).
% 0.20/0.54 cnf(c46,plain,rinvR(skolem0002(i2003_11_14_17_15_58383),i2003_11_14_17_15_58383),inference(resolution,[status(thm)],[c45, c6])).
% 0.20/0.54 cnf(c17,plain,~cSatisfiable(X38)|~rinvR(skolem0002(X38),X40)|~rr1(X40,X39)|~cp(X39),inference(split_conjunct,[status(thm)],[c13])).
% 0.20/0.54 cnf(c48,plain,~cSatisfiable(i2003_11_14_17_15_58383)|~rr1(i2003_11_14_17_15_58383,X42)|~cp(X42),inference(resolution,[status(thm)],[c17, c46])).
% 0.20/0.54 cnf(c14,plain,~cSatisfiable(X33)|rr(X33,skolem0001(X33)),inference(split_conjunct,[status(thm)],[c13])).
% 0.20/0.54 cnf(c41,plain,rr(i2003_11_14_17_15_58383,skolem0001(i2003_11_14_17_15_58383)),inference(resolution,[status(thm)],[c14, c0])).
% 0.20/0.54 cnf(c42,plain,rinvR(skolem0001(i2003_11_14_17_15_58383),i2003_11_14_17_15_58383),inference(resolution,[status(thm)],[c41, c6])).
% 0.20/0.54 cnf(c15,plain,~cSatisfiable(X34)|~rinvR(skolem0001(X34),X36)|~rr1(X36,X35)|cp(X35),inference(split_conjunct,[status(thm)],[c13])).
% 0.20/0.54 cnf(c44,plain,~cSatisfiable(i2003_11_14_17_15_58383)|~rr1(i2003_11_14_17_15_58383,X41)|cp(X41),inference(resolution,[status(thm)],[c15, c42])).
% 0.20/0.54 cnf(c5,plain,~rinvR(X28,X29)|rr(X29,X28),inference(split_conjunct,[status(thm)],[c4])).
% 0.20/0.54 fof(axiom_1,axiom,(![X]:(xsd_string(X)<=>(~xsd_integer(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_1)).
% 0.20/0.54 fof(c27,plain,(![X]:(xsd_string(X)<=>~xsd_integer(X))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 0.20/0.54 fof(c28,plain,(![X]:((~xsd_string(X)|~xsd_integer(X))&(xsd_integer(X)|xsd_string(X)))),inference(fof_nnf,[status(thm)],[c27])).
% 0.20/0.54 fof(c29,plain,((![X]:(~xsd_string(X)|~xsd_integer(X)))&(![X]:(xsd_integer(X)|xsd_string(X)))),inference(shift_quantors,[status(thm)],[c28])).
% 0.20/0.54 fof(c31,plain,(![X20]:(![X21]:((~xsd_string(X20)|~xsd_integer(X20))&(xsd_integer(X21)|xsd_string(X21))))),inference(shift_quantors,[status(thm)],[fof(c30,plain,((![X20]:(~xsd_string(X20)|~xsd_integer(X20)))&(![X21]:(xsd_integer(X21)|xsd_string(X21)))),inference(variable_rename,[status(thm)],[c29])).])).
% 0.20/0.54 cnf(c33,plain,xsd_integer(X27)|xsd_string(X27),inference(split_conjunct,[status(thm)],[c31])).
% 0.20/0.54 cnf(c32,plain,~xsd_string(X26)|~xsd_integer(X26),inference(split_conjunct,[status(thm)],[c31])).
% 0.20/0.54 fof(axiom_0,axiom,(![X]:(cowlThing(X)&(~cowlNothing(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_0)).
% 0.20/0.54 fof(c34,plain,(![X]:(cowlThing(X)&~cowlNothing(X))),inference(fof_simplification,[status(thm)],[axiom_0])).
% 0.20/0.54 fof(c35,plain,((![X]:cowlThing(X))&(![X]:~cowlNothing(X))),inference(shift_quantors,[status(thm)],[c34])).
% 0.20/0.54 fof(c37,plain,(![X22]:(![X23]:(cowlThing(X22)&~cowlNothing(X23)))),inference(shift_quantors,[status(thm)],[fof(c36,plain,((![X22]:cowlThing(X22))&(![X23]:~cowlNothing(X23))),inference(variable_rename,[status(thm)],[c35])).])).
% 0.20/0.54 cnf(c39,plain,~cowlNothing(X25),inference(split_conjunct,[status(thm)],[c37])).
% 0.20/0.54 cnf(c38,plain,cowlThing(X24),inference(split_conjunct,[status(thm)],[c37])).
% 0.20/0.54 % SZS output end Saturation
% 0.20/0.54
% 0.20/0.54 % Initial clauses : 20
% 0.20/0.54 % Processed clauses : 32
% 0.20/0.54 % Factors computed : 6
% 0.20/0.54 % Resolvents computed: 33
% 0.20/0.54 % Tautologies deleted: 1
% 0.20/0.54 % Forward subsumed : 26
% 0.20/0.54 % Backward subsumed : 0
% 0.20/0.54 % -------- CPU Time ---------
% 0.20/0.54 % User time : 0.185 s
% 0.20/0.54 % System time : 0.012 s
% 0.20/0.54 % Total time : 0.197 s
%------------------------------------------------------------------------------