%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS020+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n017.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:29 EDT 2024
% Result : Satisfiable 0.48s 0.68s
% Output : Saturation 0.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : KRS020+1 : TPTP v8.1.2. Released v3.1.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n017.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 9 00:12:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.48/0.68 % Version: 1.5
% 0.48/0.68 % SZS status Satisfiable
% 0.48/0.68 % SZS output start Saturation
% 0.48/0.68 fof(axiom_7,axiom,(![X]:(cnotA(X)<=>(![Y]:(rq(X,Y)=>cNothing(Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_7)).
% 0.48/0.68 fof(c26,plain,(![X]:((~cnotA(X)|(![Y]:(~rq(X,Y)|cNothing(Y))))&((?[Y]:(rq(X,Y)&~cNothing(Y)))|cnotA(X)))),inference(fof_nnf,[status(thm)],[axiom_7])).
% 0.48/0.68 fof(c27,plain,((![X]:(~cnotA(X)|(![Y]:(~rq(X,Y)|cNothing(Y)))))&(![X]:((?[Y]:(rq(X,Y)&~cNothing(Y)))|cnotA(X)))),inference(shift_quantors,[status(thm)],[c26])).
% 0.48/0.68 fof(c28,plain,((![X12]:(~cnotA(X12)|(![X13]:(~rq(X12,X13)|cNothing(X13)))))&(![X14]:((?[X15]:(rq(X14,X15)&~cNothing(X15)))|cnotA(X14)))),inference(variable_rename,[status(thm)],[c27])).
% 0.48/0.68 fof(c30,plain,(![X12]:(![X13]:(![X14]:((~cnotA(X12)|(~rq(X12,X13)|cNothing(X13)))&((rq(X14,skolem0003(X14))&~cNothing(skolem0003(X14)))|cnotA(X14)))))),inference(shift_quantors,[status(thm)],[fof(c29,plain,((![X12]:(~cnotA(X12)|(![X13]:(~rq(X12,X13)|cNothing(X13)))))&(![X14]:((rq(X14,skolem0003(X14))&~cNothing(skolem0003(X14)))|cnotA(X14)))),inference(skolemize,[status(esa)],[c28])).])).
% 0.48/0.68 fof(c31,plain,(![X12]:(![X13]:(![X14]:((~cnotA(X12)|(~rq(X12,X13)|cNothing(X13)))&((rq(X14,skolem0003(X14))|cnotA(X14))&(~cNothing(skolem0003(X14))|cnotA(X14))))))),inference(distribute,[status(thm)],[c30])).
% 0.48/0.68 cnf(c32,plain,~cnotA(X63)|~rq(X63,X62)|cNothing(X62),inference(split_conjunct,[status(thm)],[c31])).
% 0.48/0.68 fof(axiom_10,axiom,(![X]:(cnotB(X)<=>(![Y]:(rr(X,Y)=>cNothing(Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_10)).
% 0.48/0.68 fof(c0,plain,(![X]:((~cnotB(X)|(![Y]:(~rr(X,Y)|cNothing(Y))))&((?[Y]:(rr(X,Y)&~cNothing(Y)))|cnotB(X)))),inference(fof_nnf,[status(thm)],[axiom_10])).
% 0.48/0.68 fof(c1,plain,((![X]:(~cnotB(X)|(![Y]:(~rr(X,Y)|cNothing(Y)))))&(![X]:((?[Y]:(rr(X,Y)&~cNothing(Y)))|cnotB(X)))),inference(shift_quantors,[status(thm)],[c0])).
% 0.48/0.68 fof(c2,plain,((![X2]:(~cnotB(X2)|(![X3]:(~rr(X2,X3)|cNothing(X3)))))&(![X4]:((?[X5]:(rr(X4,X5)&~cNothing(X5)))|cnotB(X4)))),inference(variable_rename,[status(thm)],[c1])).
% 0.48/0.68 fof(c4,plain,(![X2]:(![X3]:(![X4]:((~cnotB(X2)|(~rr(X2,X3)|cNothing(X3)))&((rr(X4,skolem0001(X4))&~cNothing(skolem0001(X4)))|cnotB(X4)))))),inference(shift_quantors,[status(thm)],[fof(c3,plain,((![X2]:(~cnotB(X2)|(![X3]:(~rr(X2,X3)|cNothing(X3)))))&(![X4]:((rr(X4,skolem0001(X4))&~cNothing(skolem0001(X4)))|cnotB(X4)))),inference(skolemize,[status(esa)],[c2])).])).
% 0.48/0.68 fof(c5,plain,(![X2]:(![X3]:(![X4]:((~cnotB(X2)|(~rr(X2,X3)|cNothing(X3)))&((rr(X4,skolem0001(X4))|cnotB(X4))&(~cNothing(skolem0001(X4))|cnotB(X4))))))),inference(distribute,[status(thm)],[c4])).
% 0.48/0.68 cnf(c7,plain,rr(X49,skolem0001(X49))|cnotB(X49),inference(split_conjunct,[status(thm)],[c5])).
% 0.48/0.68 fof(axiom_9,axiom,(![X]:(cnotAorB(X)<=>(cnotB(X)&cnotA(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_9)).
% 0.48/0.68 fof(c9,plain,(![X]:((~cnotAorB(X)|(cnotB(X)&cnotA(X)))&((~cnotB(X)|~cnotA(X))|cnotAorB(X)))),inference(fof_nnf,[status(thm)],[axiom_9])).
% 0.48/0.68 fof(c10,plain,((![X]:(~cnotAorB(X)|(cnotB(X)&cnotA(X))))&(![X]:((~cnotB(X)|~cnotA(X))|cnotAorB(X)))),inference(shift_quantors,[status(thm)],[c9])).
% 0.48/0.68 fof(c12,plain,(![X6]:(![X7]:((~cnotAorB(X6)|(cnotB(X6)&cnotA(X6)))&((~cnotB(X7)|~cnotA(X7))|cnotAorB(X7))))),inference(shift_quantors,[status(thm)],[fof(c11,plain,((![X6]:(~cnotAorB(X6)|(cnotB(X6)&cnotA(X6))))&(![X7]:((~cnotB(X7)|~cnotA(X7))|cnotAorB(X7)))),inference(variable_rename,[status(thm)],[c10])).])).
% 0.48/0.68 fof(c13,plain,(![X6]:(![X7]:(((~cnotAorB(X6)|cnotB(X6))&(~cnotAorB(X6)|cnotA(X6)))&((~cnotB(X7)|~cnotA(X7))|cnotAorB(X7))))),inference(distribute,[status(thm)],[c12])).
% 0.48/0.68 cnf(c16,plain,~cnotB(X54)|~cnotA(X54)|cnotAorB(X54),inference(split_conjunct,[status(thm)],[c13])).
% 0.48/0.68 fof(axiom_2,axiom,(![X]:(cA(X)<=>(?[Y]:(rq(X,Y)&cowlThing(Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 0.48/0.68 fof(c61,plain,(![X]:((~cA(X)|(?[Y]:(rq(X,Y)&cowlThing(Y))))&((![Y]:(~rq(X,Y)|~cowlThing(Y)))|cA(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.48/0.68 fof(c62,plain,((![X]:(~cA(X)|(?[Y]:(rq(X,Y)&cowlThing(Y)))))&(![X]:((![Y]:(~rq(X,Y)|~cowlThing(Y)))|cA(X)))),inference(shift_quantors,[status(thm)],[c61])).
% 0.48/0.68 fof(c63,plain,((![X28]:(~cA(X28)|(?[X29]:(rq(X28,X29)&cowlThing(X29)))))&(![X30]:((![X31]:(~rq(X30,X31)|~cowlThing(X31)))|cA(X30)))),inference(variable_rename,[status(thm)],[c62])).
% 0.48/0.68 fof(c65,plain,(![X28]:(![X30]:(![X31]:((~cA(X28)|(rq(X28,skolem0007(X28))&cowlThing(skolem0007(X28))))&((~rq(X30,X31)|~cowlThing(X31))|cA(X30)))))),inference(shift_quantors,[status(thm)],[fof(c64,plain,((![X28]:(~cA(X28)|(rq(X28,skolem0007(X28))&cowlThing(skolem0007(X28)))))&(![X30]:((![X31]:(~rq(X30,X31)|~cowlThing(X31)))|cA(X30)))),inference(skolemize,[status(esa)],[c63])).])).
% 0.48/0.68 fof(c66,plain,(![X28]:(![X30]:(![X31]:(((~cA(X28)|rq(X28,skolem0007(X28)))&(~cA(X28)|cowlThing(skolem0007(X28))))&((~rq(X30,X31)|~cowlThing(X31))|cA(X30)))))),inference(distribute,[status(thm)],[c65])).
% 0.48/0.68 cnf(c67,plain,~cA(X64)|rq(X64,skolem0007(X64)),inference(split_conjunct,[status(thm)],[c66])).
% 0.48/0.68 fof(axiom_0,axiom,(![X]:(cowlThing(X)&(~cowlNothing(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_0)).
% 0.48/0.68 fof(c77,plain,(![X]:(cowlThing(X)&~cowlNothing(X))),inference(fof_simplification,[status(thm)],[axiom_0])).
% 0.48/0.68 fof(c78,plain,((![X]:cowlThing(X))&(![X]:~cowlNothing(X))),inference(shift_quantors,[status(thm)],[c77])).
% 0.48/0.68 fof(c80,plain,(![X34]:(![X35]:(cowlThing(X34)&~cowlNothing(X35)))),inference(shift_quantors,[status(thm)],[fof(c79,plain,((![X34]:cowlThing(X34))&(![X35]:~cowlNothing(X35))),inference(variable_rename,[status(thm)],[c78])).])).
% 0.48/0.68 cnf(c81,plain,cowlThing(X36),inference(split_conjunct,[status(thm)],[c80])).
% 0.48/0.68 cnf(c33,plain,rq(X58,skolem0003(X58))|cnotA(X58),inference(split_conjunct,[status(thm)],[c31])).
% 0.48/0.68 cnf(c69,plain,~rq(X71,X72)|~cowlThing(X72)|cA(X71),inference(split_conjunct,[status(thm)],[c66])).
% 0.48/0.68 cnf(c97,plain,~cowlThing(skolem0003(X95))|cA(X95)|cnotA(X95),inference(resolution,[status(thm)],[c69, c33])).
% 0.48/0.68 cnf(c124,plain,cA(X97)|cnotA(X97),inference(resolution,[status(thm)],[c97, c81])).
% 0.48/0.68 cnf(c125,plain,cnotA(X98)|rq(X98,skolem0007(X98)),inference(resolution,[status(thm)],[c124, c67])).
% 0.48/0.68 cnf(c127,plain,rq(X119,skolem0007(X119))|~cnotB(X119)|cnotAorB(X119),inference(resolution,[status(thm)],[c125, c16])).
% 0.48/0.68 cnf(c162,plain,rq(X160,skolem0007(X160))|cnotAorB(X160)|rr(X160,skolem0001(X160)),inference(resolution,[status(thm)],[c127, c7])).
% 0.48/0.68 cnf(c203,plain,cnotAorB(X191)|rr(X191,skolem0001(X191))|~cnotA(X191)|cNothing(skolem0007(X191)),inference(resolution,[status(thm)],[c162, c32])).
% 0.48/0.68 fof(axiom_4,axiom,(![X]:(cB(X)<=>(?[Y]:(rr(X,Y)&cowlThing(Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_4)).
% 0.48/0.68 fof(c43,plain,(![X]:((~cB(X)|(?[Y]:(rr(X,Y)&cowlThing(Y))))&((![Y]:(~rr(X,Y)|~cowlThing(Y)))|cB(X)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.48/0.68 fof(c44,plain,((![X]:(~cB(X)|(?[Y]:(rr(X,Y)&cowlThing(Y)))))&(![X]:((![Y]:(~rr(X,Y)|~cowlThing(Y)))|cB(X)))),inference(shift_quantors,[status(thm)],[c43])).
% 0.48/0.68 fof(c45,plain,((![X20]:(~cB(X20)|(?[X21]:(rr(X20,X21)&cowlThing(X21)))))&(![X22]:((![X23]:(~rr(X22,X23)|~cowlThing(X23)))|cB(X22)))),inference(variable_rename,[status(thm)],[c44])).
% 0.48/0.68 fof(c47,plain,(![X20]:(![X22]:(![X23]:((~cB(X20)|(rr(X20,skolem0005(X20))&cowlThing(skolem0005(X20))))&((~rr(X22,X23)|~cowlThing(X23))|cB(X22)))))),inference(shift_quantors,[status(thm)],[fof(c46,plain,((![X20]:(~cB(X20)|(rr(X20,skolem0005(X20))&cowlThing(skolem0005(X20)))))&(![X22]:((![X23]:(~rr(X22,X23)|~cowlThing(X23)))|cB(X22)))),inference(skolemize,[status(esa)],[c45])).])).
% 0.48/0.68 fof(c48,plain,(![X20]:(![X22]:(![X23]:(((~cB(X20)|rr(X20,skolem0005(X20)))&(~cB(X20)|cowlThing(skolem0005(X20))))&((~rr(X22,X23)|~cowlThing(X23))|cB(X22)))))),inference(distribute,[status(thm)],[c47])).
% 0.48/0.68 cnf(c49,plain,~cB(X60)|rr(X60,skolem0005(X60)),inference(split_conjunct,[status(thm)],[c48])).
% 0.48/0.68 cnf(c51,plain,~rr(X67,X68)|~cowlThing(X68)|cB(X67),inference(split_conjunct,[status(thm)],[c48])).
% 0.48/0.68 cnf(c93,plain,~cowlThing(skolem0001(X79))|cB(X79)|cnotB(X79),inference(resolution,[status(thm)],[c51, c7])).
% 0.48/0.68 cnf(c100,plain,cB(X80)|cnotB(X80),inference(resolution,[status(thm)],[c93, c81])).
% 0.48/0.68 cnf(c101,plain,cnotB(X81)|rr(X81,skolem0005(X81)),inference(resolution,[status(thm)],[c100, c49])).
% 0.48/0.69 cnf(c161,plain,rq(X159,skolem0007(X159))|cnotAorB(X159)|rr(X159,skolem0005(X159)),inference(resolution,[status(thm)],[c127, c101])).
% 0.48/0.69 cnf(c197,plain,cnotAorB(X187)|rr(X187,skolem0005(X187))|~cnotA(X187)|cNothing(skolem0007(X187)),inference(resolution,[status(thm)],[c161, c32])).
% 0.48/0.69 cnf(c88,plain,rq(X78,skolem0003(X78))|~cnotB(X78)|cnotAorB(X78),inference(resolution,[status(thm)],[c33, c16])).
% 0.48/0.69 cnf(c103,plain,rr(X114,skolem0005(X114))|rq(X114,skolem0003(X114))|cnotAorB(X114),inference(resolution,[status(thm)],[c101, c88])).
% 0.48/0.69 cnf(c154,plain,rr(X172,skolem0005(X172))|cnotAorB(X172)|~cnotA(X172)|cNothing(skolem0003(X172)),inference(resolution,[status(thm)],[c103, c32])).
% 0.48/0.69 cnf(c126,plain,cA(X99)|~cnotB(X99)|cnotAorB(X99),inference(resolution,[status(thm)],[c124, c16])).
% 0.48/0.69 cnf(c130,plain,cA(X100)|cnotAorB(X100)|cB(X100),inference(resolution,[status(thm)],[c126, c100])).
% 0.48/0.69 cnf(c136,plain,cnotAorB(X125)|cB(X125)|rq(X125,skolem0007(X125)),inference(resolution,[status(thm)],[c130, c67])).
% 0.48/0.69 cnf(c177,plain,cnotAorB(X147)|cB(X147)|~cnotA(X147)|cNothing(skolem0007(X147)),inference(resolution,[status(thm)],[c136, c32])).
% 0.48/0.69 cnf(c102,plain,cB(X108)|rq(X108,skolem0003(X108))|cnotAorB(X108),inference(resolution,[status(thm)],[c100, c88])).
% 0.48/0.69 cnf(c148,plain,cB(X140)|cnotAorB(X140)|~cnotA(X140)|cNothing(skolem0003(X140)),inference(resolution,[status(thm)],[c102, c32])).
% 0.48/0.69 cnf(c99,plain,rq(X102,skolem0003(X102))|cnotAorB(X102)|rr(X102,skolem0001(X102)),inference(resolution,[status(thm)],[c88, c7])).
% 0.48/0.69 cnf(c141,plain,cnotAorB(X138)|rr(X138,skolem0001(X138))|~cnotA(X138)|cNothing(skolem0003(X138)),inference(resolution,[status(thm)],[c99, c32])).
% 0.48/0.69 cnf(c135,plain,cA(X124)|cnotAorB(X124)|rr(X124,skolem0001(X124)),inference(resolution,[status(thm)],[c126, c7])).
% 0.48/0.69 cnf(c134,plain,cA(X123)|cnotAorB(X123)|rr(X123,skolem0005(X123)),inference(resolution,[status(thm)],[c126, c101])).
% 0.48/0.69 fof(axiom_3,axiom,(![X]:(cAorB(X)<=>(?[Y]:(rs(X,Y)&cowlThing(Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 0.48/0.69 fof(c52,plain,(![X]:((~cAorB(X)|(?[Y]:(rs(X,Y)&cowlThing(Y))))&((![Y]:(~rs(X,Y)|~cowlThing(Y)))|cAorB(X)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.48/0.69 fof(c53,plain,((![X]:(~cAorB(X)|(?[Y]:(rs(X,Y)&cowlThing(Y)))))&(![X]:((![Y]:(~rs(X,Y)|~cowlThing(Y)))|cAorB(X)))),inference(shift_quantors,[status(thm)],[c52])).
% 0.48/0.69 fof(c54,plain,((![X24]:(~cAorB(X24)|(?[X25]:(rs(X24,X25)&cowlThing(X25)))))&(![X26]:((![X27]:(~rs(X26,X27)|~cowlThing(X27)))|cAorB(X26)))),inference(variable_rename,[status(thm)],[c53])).
% 0.48/0.69 fof(c56,plain,(![X24]:(![X26]:(![X27]:((~cAorB(X24)|(rs(X24,skolem0006(X24))&cowlThing(skolem0006(X24))))&((~rs(X26,X27)|~cowlThing(X27))|cAorB(X26)))))),inference(shift_quantors,[status(thm)],[fof(c55,plain,((![X24]:(~cAorB(X24)|(rs(X24,skolem0006(X24))&cowlThing(skolem0006(X24)))))&(![X26]:((![X27]:(~rs(X26,X27)|~cowlThing(X27)))|cAorB(X26)))),inference(skolemize,[status(esa)],[c54])).])).
% 0.48/0.69 fof(c57,plain,(![X24]:(![X26]:(![X27]:(((~cAorB(X24)|rs(X24,skolem0006(X24)))&(~cAorB(X24)|cowlThing(skolem0006(X24))))&((~rs(X26,X27)|~cowlThing(X27))|cAorB(X26)))))),inference(distribute,[status(thm)],[c56])).
% 0.48/0.69 cnf(c58,plain,~cAorB(X61)|rs(X61,skolem0006(X61)),inference(split_conjunct,[status(thm)],[c57])).
% 0.48/0.69 cnf(c14,plain,~cnotAorB(X38)|cnotB(X38),inference(split_conjunct,[status(thm)],[c13])).
% 0.48/0.69 fof(axiom_8,axiom,(![X]:(cnotAorB(X)<=>(![Y]:(rs(X,Y)=>cNothing(Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_8)).
% 0.48/0.69 fof(c17,plain,(![X]:((~cnotAorB(X)|(![Y]:(~rs(X,Y)|cNothing(Y))))&((?[Y]:(rs(X,Y)&~cNothing(Y)))|cnotAorB(X)))),inference(fof_nnf,[status(thm)],[axiom_8])).
% 0.48/0.69 fof(c18,plain,((![X]:(~cnotAorB(X)|(![Y]:(~rs(X,Y)|cNothing(Y)))))&(![X]:((?[Y]:(rs(X,Y)&~cNothing(Y)))|cnotAorB(X)))),inference(shift_quantors,[status(thm)],[c17])).
% 0.48/0.69 fof(c19,plain,((![X8]:(~cnotAorB(X8)|(![X9]:(~rs(X8,X9)|cNothing(X9)))))&(![X10]:((?[X11]:(rs(X10,X11)&~cNothing(X11)))|cnotAorB(X10)))),inference(variable_rename,[status(thm)],[c18])).
% 0.48/0.69 fof(c21,plain,(![X8]:(![X9]:(![X10]:((~cnotAorB(X8)|(~rs(X8,X9)|cNothing(X9)))&((rs(X10,skolem0002(X10))&~cNothing(skolem0002(X10)))|cnotAorB(X10)))))),inference(shift_quantors,[status(thm)],[fof(c20,plain,((![X8]:(~cnotAorB(X8)|(![X9]:(~rs(X8,X9)|cNothing(X9)))))&(![X10]:((rs(X10,skolem0002(X10))&~cNothing(skolem0002(X10)))|cnotAorB(X10)))),inference(skolemize,[status(esa)],[c19])).])).
% 0.48/0.69 fof(c22,plain,(![X8]:(![X9]:(![X10]:((~cnotAorB(X8)|(~rs(X8,X9)|cNothing(X9)))&((rs(X10,skolem0002(X10))|cnotAorB(X10))&(~cNothing(skolem0002(X10))|cnotAorB(X10))))))),inference(distribute,[status(thm)],[c21])).
% 0.48/0.69 cnf(c24,plain,rs(X57,skolem0002(X57))|cnotAorB(X57),inference(split_conjunct,[status(thm)],[c22])).
% 0.48/0.69 cnf(c60,plain,~rs(X69,X70)|~cowlThing(X70)|cAorB(X69),inference(split_conjunct,[status(thm)],[c57])).
% 0.48/0.69 cnf(c94,plain,~cowlThing(skolem0002(X82))|cAorB(X82)|cnotAorB(X82),inference(resolution,[status(thm)],[c60, c24])).
% 0.48/0.69 cnf(c106,plain,cAorB(X83)|cnotAorB(X83),inference(resolution,[status(thm)],[c94, c81])).
% 0.48/0.69 cnf(c109,plain,cAorB(X86)|cnotB(X86),inference(resolution,[status(thm)],[c106, c14])).
% 0.48/0.69 cnf(c112,plain,cnotB(X91)|rs(X91,skolem0006(X91)),inference(resolution,[status(thm)],[c109, c58])).
% 0.48/0.69 cnf(c15,plain,~cnotAorB(X39)|cnotA(X39),inference(split_conjunct,[status(thm)],[c13])).
% 0.48/0.69 cnf(c108,plain,cAorB(X85)|cnotA(X85),inference(resolution,[status(thm)],[c106, c15])).
% 0.48/0.69 cnf(c110,plain,cnotA(X88)|rs(X88,skolem0006(X88)),inference(resolution,[status(thm)],[c108, c58])).
% 0.48/0.69 cnf(c107,plain,cnotAorB(X87)|rs(X87,skolem0006(X87)),inference(resolution,[status(thm)],[c106, c58])).
% 0.48/0.69 cnf(c87,plain,rs(X66,skolem0002(X66))|cnotB(X66),inference(resolution,[status(thm)],[c24, c14])).
% 0.48/0.69 cnf(c86,plain,rs(X65,skolem0002(X65))|cnotA(X65),inference(resolution,[status(thm)],[c24, c15])).
% 0.48/0.69 fof(axiom_6,axiom,(![X]:(cNothing(X)=>(?[Y0]:rp(X,Y0)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_6)).
% 0.48/0.69 fof(c35,plain,(![X]:(~cNothing(X)|(?[Y0]:rp(X,Y0)))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 0.48/0.69 fof(c36,plain,(![X16]:(~cNothing(X16)|(?[X17]:rp(X16,X17)))),inference(variable_rename,[status(thm)],[c35])).
% 0.48/0.69 fof(c37,plain,(![X16]:(~cNothing(X16)|rp(X16,skolem0004(X16)))),inference(skolemize,[status(esa)],[c36])).
% 0.48/0.69 cnf(c38,plain,~cNothing(X59)|rp(X59,skolem0004(X59)),inference(split_conjunct,[status(thm)],[c37])).
% 0.48/0.69 cnf(c23,plain,~cnotAorB(X56)|~rs(X56,X55)|cNothing(X55),inference(split_conjunct,[status(thm)],[c22])).
% 0.48/0.69 cnf(c34,plain,~cNothing(skolem0003(X50))|cnotA(X50),inference(split_conjunct,[status(thm)],[c31])).
% 0.48/0.69 cnf(c25,plain,~cNothing(skolem0002(X48))|cnotAorB(X48),inference(split_conjunct,[status(thm)],[c22])).
% 0.48/0.69 cnf(c8,plain,~cNothing(skolem0001(X47))|cnotB(X47),inference(split_conjunct,[status(thm)],[c5])).
% 0.48/0.69 fof(axiom_5,axiom,(![X]:(cNothing(X)=>(~(?[Y]:rp(X,Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_5)).
% 0.48/0.69 fof(c39,plain,(![X]:(~cNothing(X)|(![Y]:~rp(X,Y)))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.48/0.69 fof(c41,plain,(![X18]:(![X19]:(~cNothing(X18)|~rp(X18,X19)))),inference(shift_quantors,[status(thm)],[fof(c40,plain,(![X18]:(~cNothing(X18)|(![X19]:~rp(X18,X19)))),inference(variable_rename,[status(thm)],[c39])).])).
% 0.48/0.69 cnf(c42,plain,~cNothing(X45)|~rp(X45,X46),inference(split_conjunct,[status(thm)],[c41])).
% 0.48/0.69 fof(axiom_1,axiom,(![X]:(xsd_string(X)<=>(~xsd_integer(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_1)).
% 0.48/0.69 fof(c70,plain,(![X]:(xsd_string(X)<=>~xsd_integer(X))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 0.48/0.69 fof(c71,plain,(![X]:((~xsd_string(X)|~xsd_integer(X))&(xsd_integer(X)|xsd_string(X)))),inference(fof_nnf,[status(thm)],[c70])).
% 0.48/0.69 fof(c72,plain,((![X]:(~xsd_string(X)|~xsd_integer(X)))&(![X]:(xsd_integer(X)|xsd_string(X)))),inference(shift_quantors,[status(thm)],[c71])).
% 0.48/0.69 fof(c74,plain,(![X32]:(![X33]:((~xsd_string(X32)|~xsd_integer(X32))&(xsd_integer(X33)|xsd_string(X33))))),inference(shift_quantors,[status(thm)],[fof(c73,plain,((![X32]:(~xsd_string(X32)|~xsd_integer(X32)))&(![X33]:(xsd_integer(X33)|xsd_string(X33)))),inference(variable_rename,[status(thm)],[c72])).])).
% 0.48/0.69 cnf(c76,plain,xsd_integer(X43)|xsd_string(X43),inference(split_conjunct,[status(thm)],[c74])).
% 0.48/0.69 cnf(c6,plain,~cnotB(X41)|~rr(X41,X42)|cNothing(X42),inference(split_conjunct,[status(thm)],[c5])).
% 0.48/0.69 cnf(c75,plain,~xsd_string(X40)|~xsd_integer(X40),inference(split_conjunct,[status(thm)],[c74])).
% 0.48/0.69 cnf(c82,plain,~cowlNothing(X37),inference(split_conjunct,[status(thm)],[c80])).
% 0.48/0.69 % SZS output end Saturation
% 0.48/0.69
% 0.48/0.69 % Initial clauses : 27
% 0.48/0.69 % Processed clauses : 57
% 0.48/0.69 % Factors computed : 0
% 0.48/0.69 % Resolvents computed: 143
% 0.48/0.69 % Tautologies deleted: 7
% 0.48/0.69 % Forward subsumed : 106
% 0.48/0.69 % Backward subsumed : 3
% 0.48/0.69 % -------- CPU Time ---------
% 0.48/0.69 % User time : 0.319 s
% 0.48/0.69 % System time : 0.015 s
% 0.48/0.69 % Total time : 0.334 s
%------------------------------------------------------------------------------