%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS116+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n007.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:44 EDT 2024
% Result : Unsatisfiable 0.79s 0.96s
% Output : Refutation 0.79s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.13 % Problem : KRS116+1 : TPTP v8.1.2. Released v3.1.0.
% 0.13/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n007.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Thu May 9 00:15:38 EDT 2024
% 0.14/0.36 % CPUTime :
% 0.79/0.96 % Version: 1.5
% 0.79/0.96 % SZS status Unsatisfiable
% 0.79/0.96 % SZS output start CNFRefutation
% 0.79/0.96 fof(axiom_17,axiom,cUnsatisfiable(i2003_11_14_17_21_33997),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_17)).
% 0.79/0.96 cnf(c0,plain,cUnsatisfiable(i2003_11_14_17_21_33997),inference(split_conjunct,[status(thm)],[axiom_17])).
% 0.79/0.96 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)=>ca(X))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 0.79/0.96 fof(c126,plain,(![X]:(~cUnsatisfiable(X)|ca(X))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.79/0.96 fof(c127,plain,(![X65]:(~cUnsatisfiable(X65)|ca(X65))),inference(variable_rename,[status(thm)],[c126])).
% 0.79/0.96 cnf(c128,plain,~cUnsatisfiable(X72)|ca(X72),inference(split_conjunct,[status(thm)],[c127])).
% 0.79/0.96 cnf(c142,plain,ca(i2003_11_14_17_21_33997),inference(resolution,[status(thm)],[c128, c0])).
% 0.79/0.96 fof(axiom_4,axiom,(![X]:(ca(X)<=>(~(?[Y]:ra_Px1(X,Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_4)).
% 0.79/0.96 fof(c113,plain,(![X]:((~ca(X)|(![Y]:~ra_Px1(X,Y)))&((?[Y]:ra_Px1(X,Y))|ca(X)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.79/0.96 fof(c114,plain,((![X]:(~ca(X)|(![Y]:~ra_Px1(X,Y))))&(![X]:((?[Y]:ra_Px1(X,Y))|ca(X)))),inference(shift_quantors,[status(thm)],[c113])).
% 0.79/0.96 fof(c115,plain,((![X59]:(~ca(X59)|(![X60]:~ra_Px1(X59,X60))))&(![X61]:((?[X62]:ra_Px1(X61,X62))|ca(X61)))),inference(variable_rename,[status(thm)],[c114])).
% 0.79/0.96 fof(c117,plain,(![X59]:(![X60]:(![X61]:((~ca(X59)|~ra_Px1(X59,X60))&(ra_Px1(X61,skolem0014(X61))|ca(X61)))))),inference(shift_quantors,[status(thm)],[fof(c116,plain,((![X59]:(~ca(X59)|(![X60]:~ra_Px1(X59,X60))))&(![X61]:(ra_Px1(X61,skolem0014(X61))|ca(X61)))),inference(skolemize,[status(esa)],[c115])).])).
% 0.79/0.96 cnf(c118,plain,~ca(X81)|~ra_Px1(X81,X82),inference(split_conjunct,[status(thm)],[c117])).
% 0.79/0.96 fof(axiom_5,axiom,(![X]:(caxcomp(X)<=>(?[Y0]:ra_Px1(X,Y0)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_5)).
% 0.79/0.96 fof(c106,plain,(![X]:((~caxcomp(X)|(?[Y0]:ra_Px1(X,Y0)))&((![Y0]:~ra_Px1(X,Y0))|caxcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.79/0.96 fof(c107,plain,((![X]:(~caxcomp(X)|(?[Y0]:ra_Px1(X,Y0))))&(![X]:((![Y0]:~ra_Px1(X,Y0))|caxcomp(X)))),inference(shift_quantors,[status(thm)],[c106])).
% 0.79/0.96 fof(c108,plain,((![X55]:(~caxcomp(X55)|(?[X56]:ra_Px1(X55,X56))))&(![X57]:((![X58]:~ra_Px1(X57,X58))|caxcomp(X57)))),inference(variable_rename,[status(thm)],[c107])).
% 0.79/0.96 fof(c110,plain,(![X55]:(![X57]:(![X58]:((~caxcomp(X55)|ra_Px1(X55,skolem0013(X55)))&(~ra_Px1(X57,X58)|caxcomp(X57)))))),inference(shift_quantors,[status(thm)],[fof(c109,plain,((![X55]:(~caxcomp(X55)|ra_Px1(X55,skolem0013(X55))))&(![X57]:((![X58]:~ra_Px1(X57,X58))|caxcomp(X57)))),inference(skolemize,[status(esa)],[c108])).])).
% 0.79/0.96 cnf(c111,plain,~caxcomp(X119)|ra_Px1(X119,skolem0013(X119)),inference(split_conjunct,[status(thm)],[c110])).
% 0.79/0.96 fof(axiom_11,axiom,(![X]:(ca_Vx6(X)<=>(![Y]:(rinvS(X,Y)=>caxcomp(Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_11)).
% 0.79/0.96 fof(c31,plain,(![X]:((~ca_Vx6(X)|(![Y]:(~rinvS(X,Y)|caxcomp(Y))))&((?[Y]:(rinvS(X,Y)&~caxcomp(Y)))|ca_Vx6(X)))),inference(fof_nnf,[status(thm)],[axiom_11])).
% 0.79/0.96 fof(c32,plain,((![X]:(~ca_Vx6(X)|(![Y]:(~rinvS(X,Y)|caxcomp(Y)))))&(![X]:((?[Y]:(rinvS(X,Y)&~caxcomp(Y)))|ca_Vx6(X)))),inference(shift_quantors,[status(thm)],[c31])).
% 0.79/0.96 fof(c33,plain,((![X21]:(~ca_Vx6(X21)|(![X22]:(~rinvS(X21,X22)|caxcomp(X22)))))&(![X23]:((?[X24]:(rinvS(X23,X24)&~caxcomp(X24)))|ca_Vx6(X23)))),inference(variable_rename,[status(thm)],[c32])).
% 0.79/0.96 fof(c35,plain,(![X21]:(![X22]:(![X23]:((~ca_Vx6(X21)|(~rinvS(X21,X22)|caxcomp(X22)))&((rinvS(X23,skolem0002(X23))&~caxcomp(skolem0002(X23)))|ca_Vx6(X23)))))),inference(shift_quantors,[status(thm)],[fof(c34,plain,((![X21]:(~ca_Vx6(X21)|(![X22]:(~rinvS(X21,X22)|caxcomp(X22)))))&(![X23]:((rinvS(X23,skolem0002(X23))&~caxcomp(skolem0002(X23)))|ca_Vx6(X23)))),inference(skolemize,[status(esa)],[c33])).])).
% 0.79/0.96 fof(c36,plain,(![X21]:(![X22]:(![X23]:((~ca_Vx6(X21)|(~rinvS(X21,X22)|caxcomp(X22)))&((rinvS(X23,skolem0002(X23))|ca_Vx6(X23))&(~caxcomp(skolem0002(X23))|ca_Vx6(X23))))))),inference(distribute,[status(thm)],[c35])).
% 0.79/0.96 cnf(c37,plain,~ca_Vx6(X107)|~rinvS(X107,X108)|caxcomp(X108),inference(split_conjunct,[status(thm)],[c36])).
% 0.79/0.96 fof(axiom_15,axiom,(![X]:(![Y]:(rinvS(X,Y)<=>rs(Y,X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_15)).
% 0.79/0.96 fof(c4,plain,(![X]:(![Y]:((~rinvS(X,Y)|rs(Y,X))&(~rs(Y,X)|rinvS(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_15])).
% 0.79/0.96 fof(c5,plain,((![X]:(![Y]:(~rinvS(X,Y)|rs(Y,X))))&(![X]:(![Y]:(~rs(Y,X)|rinvS(X,Y))))),inference(shift_quantors,[status(thm)],[c4])).
% 0.79/0.96 fof(c7,plain,(![X5]:(![X6]:(![X7]:(![X8]:((~rinvS(X5,X6)|rs(X6,X5))&(~rs(X8,X7)|rinvS(X7,X8))))))),inference(shift_quantors,[status(thm)],[fof(c6,plain,((![X5]:(![X6]:(~rinvS(X5,X6)|rs(X6,X5))))&(![X7]:(![X8]:(~rs(X8,X7)|rinvS(X7,X8))))),inference(variable_rename,[status(thm)],[c5])).])).
% 0.79/0.96 cnf(c9,plain,~rs(X85,X86)|rinvS(X86,X85),inference(split_conjunct,[status(thm)],[c7])).
% 0.79/0.96 fof(axiom_3,axiom,(![X]:(cUnsatisfiable(X)=>(?[Y]:(rs(X,Y)&ca_Ax2(Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_3)).
% 0.79/0.96 fof(c120,plain,(![X]:(~cUnsatisfiable(X)|(?[Y]:(rs(X,Y)&ca_Ax2(Y))))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.79/0.96 fof(c121,plain,(![X63]:(~cUnsatisfiable(X63)|(?[X64]:(rs(X63,X64)&ca_Ax2(X64))))),inference(variable_rename,[status(thm)],[c120])).
% 0.79/0.96 fof(c122,plain,(![X63]:(~cUnsatisfiable(X63)|(rs(X63,skolem0015(X63))&ca_Ax2(skolem0015(X63))))),inference(skolemize,[status(esa)],[c121])).
% 0.79/0.96 fof(c123,plain,(![X63]:((~cUnsatisfiable(X63)|rs(X63,skolem0015(X63)))&(~cUnsatisfiable(X63)|ca_Ax2(skolem0015(X63))))),inference(distribute,[status(thm)],[c122])).
% 0.79/0.96 cnf(c124,plain,~cUnsatisfiable(X126)|rs(X126,skolem0015(X126)),inference(split_conjunct,[status(thm)],[c123])).
% 0.79/0.96 cnf(c163,plain,rs(i2003_11_14_17_21_33997,skolem0015(i2003_11_14_17_21_33997)),inference(resolution,[status(thm)],[c124, c0])).
% 0.79/0.96 cnf(c164,plain,rinvS(skolem0015(i2003_11_14_17_21_33997),i2003_11_14_17_21_33997),inference(resolution,[status(thm)],[c163, c9])).
% 0.79/0.96 cnf(c166,plain,~ca_Vx6(skolem0015(i2003_11_14_17_21_33997))|caxcomp(i2003_11_14_17_21_33997),inference(resolution,[status(thm)],[c164, c37])).
% 0.79/0.96 fof(axiom_12,axiom,(![X]:(ca_Vx7(X)<=>(![Y]:(rinvP(X,Y)=>ca_Vx6(Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_12)).
% 0.79/0.96 fof(c22,plain,(![X]:((~ca_Vx7(X)|(![Y]:(~rinvP(X,Y)|ca_Vx6(Y))))&((?[Y]:(rinvP(X,Y)&~ca_Vx6(Y)))|ca_Vx7(X)))),inference(fof_nnf,[status(thm)],[axiom_12])).
% 0.79/0.96 fof(c23,plain,((![X]:(~ca_Vx7(X)|(![Y]:(~rinvP(X,Y)|ca_Vx6(Y)))))&(![X]:((?[Y]:(rinvP(X,Y)&~ca_Vx6(Y)))|ca_Vx7(X)))),inference(shift_quantors,[status(thm)],[c22])).
% 0.79/0.96 fof(c24,plain,((![X17]:(~ca_Vx7(X17)|(![X18]:(~rinvP(X17,X18)|ca_Vx6(X18)))))&(![X19]:((?[X20]:(rinvP(X19,X20)&~ca_Vx6(X20)))|ca_Vx7(X19)))),inference(variable_rename,[status(thm)],[c23])).
% 0.79/0.96 fof(c26,plain,(![X17]:(![X18]:(![X19]:((~ca_Vx7(X17)|(~rinvP(X17,X18)|ca_Vx6(X18)))&((rinvP(X19,skolem0001(X19))&~ca_Vx6(skolem0001(X19)))|ca_Vx7(X19)))))),inference(shift_quantors,[status(thm)],[fof(c25,plain,((![X17]:(~ca_Vx7(X17)|(![X18]:(~rinvP(X17,X18)|ca_Vx6(X18)))))&(![X19]:((rinvP(X19,skolem0001(X19))&~ca_Vx6(skolem0001(X19)))|ca_Vx7(X19)))),inference(skolemize,[status(esa)],[c24])).])).
% 0.79/0.96 fof(c27,plain,(![X17]:(![X18]:(![X19]:((~ca_Vx7(X17)|(~rinvP(X17,X18)|ca_Vx6(X18)))&((rinvP(X19,skolem0001(X19))|ca_Vx7(X19))&(~ca_Vx6(skolem0001(X19))|ca_Vx7(X19))))))),inference(distribute,[status(thm)],[c26])).
% 0.79/0.96 cnf(c28,plain,~ca_Vx7(X95)|~rinvP(X95,X96)|ca_Vx6(X96),inference(split_conjunct,[status(thm)],[c27])).
% 0.79/0.96 fof(axiom_13,axiom,(![X]:(![Y]:(rinvP(X,Y)<=>rp(Y,X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_13)).
% 0.79/0.96 fof(c16,plain,(![X]:(![Y]:((~rinvP(X,Y)|rp(Y,X))&(~rp(Y,X)|rinvP(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_13])).
% 0.79/0.96 fof(c17,plain,((![X]:(![Y]:(~rinvP(X,Y)|rp(Y,X))))&(![X]:(![Y]:(~rp(Y,X)|rinvP(X,Y))))),inference(shift_quantors,[status(thm)],[c16])).
% 0.79/0.96 fof(c19,plain,(![X13]:(![X14]:(![X15]:(![X16]:((~rinvP(X13,X14)|rp(X14,X13))&(~rp(X16,X15)|rinvP(X15,X16))))))),inference(shift_quantors,[status(thm)],[fof(c18,plain,((![X13]:(![X14]:(~rinvP(X13,X14)|rp(X14,X13))))&(![X15]:(![X16]:(~rp(X16,X15)|rinvP(X15,X16))))),inference(variable_rename,[status(thm)],[c17])).])).
% 0.79/0.97 cnf(c21,plain,~rp(X93,X94)|rinvP(X94,X93),inference(split_conjunct,[status(thm)],[c19])).
% 0.79/0.97 cnf(c125,plain,~cUnsatisfiable(X106)|ca_Ax2(skolem0015(X106)),inference(split_conjunct,[status(thm)],[c123])).
% 0.79/0.97 cnf(c148,plain,ca_Ax2(skolem0015(i2003_11_14_17_21_33997)),inference(resolution,[status(thm)],[c125, c0])).
% 0.79/0.97 fof(axiom_7,axiom,(![X]:(ca_Ax2(X)<=>((((((![Y]:(rp(X,Y)=>ca_Vx3(Y)))&(![Y]:(rp(X,Y)=>ca_Vx5(Y))))&(![Y]:(rr(X,Y)=>cc(Y))))&(?[Y]:(rr(X,Y)&cowlThing(Y))))&(?[Y]:(rp(X,Y)&cowlThing(Y))))&(![Y]:(rp(X,Y)=>ca_Vx4(Y)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_7)).
% 0.79/0.97 fof(c67,plain,(![X]:((~ca_Ax2(X)|((((((![Y]:(~rp(X,Y)|ca_Vx3(Y)))&(![Y]:(~rp(X,Y)|ca_Vx5(Y))))&(![Y]:(~rr(X,Y)|cc(Y))))&(?[Y]:(rr(X,Y)&cowlThing(Y))))&(?[Y]:(rp(X,Y)&cowlThing(Y))))&(![Y]:(~rp(X,Y)|ca_Vx4(Y)))))&(((((((?[Y]:(rp(X,Y)&~ca_Vx3(Y)))|(?[Y]:(rp(X,Y)&~ca_Vx5(Y))))|(?[Y]:(rr(X,Y)&~cc(Y))))|(![Y]:(~rr(X,Y)|~cowlThing(Y))))|(![Y]:(~rp(X,Y)|~cowlThing(Y))))|(?[Y]:(rp(X,Y)&~ca_Vx4(Y))))|ca_Ax2(X)))),inference(fof_nnf,[status(thm)],[axiom_7])).
% 0.79/0.97 fof(c68,plain,((![X]:(~ca_Ax2(X)|((((((![Y]:(~rp(X,Y)|ca_Vx3(Y)))&(![Y]:(~rp(X,Y)|ca_Vx5(Y))))&(![Y]:(~rr(X,Y)|cc(Y))))&(?[Y]:(rr(X,Y)&cowlThing(Y))))&(?[Y]:(rp(X,Y)&cowlThing(Y))))&(![Y]:(~rp(X,Y)|ca_Vx4(Y))))))&(![X]:(((((((?[Y]:(rp(X,Y)&~ca_Vx3(Y)))|(?[Y]:(rp(X,Y)&~ca_Vx5(Y))))|(?[Y]:(rr(X,Y)&~cc(Y))))|(![Y]:(~rr(X,Y)|~cowlThing(Y))))|(![Y]:(~rp(X,Y)|~cowlThing(Y))))|(?[Y]:(rp(X,Y)&~ca_Vx4(Y))))|ca_Ax2(X)))),inference(shift_quantors,[status(thm)],[c67])).
% 0.79/0.97 fof(c69,plain,((![X37]:(~ca_Ax2(X37)|((((((![X38]:(~rp(X37,X38)|ca_Vx3(X38)))&(![X39]:(~rp(X37,X39)|ca_Vx5(X39))))&(![X40]:(~rr(X37,X40)|cc(X40))))&(?[X41]:(rr(X37,X41)&cowlThing(X41))))&(?[X42]:(rp(X37,X42)&cowlThing(X42))))&(![X43]:(~rp(X37,X43)|ca_Vx4(X43))))))&(![X44]:(((((((?[X45]:(rp(X44,X45)&~ca_Vx3(X45)))|(?[X46]:(rp(X44,X46)&~ca_Vx5(X46))))|(?[X47]:(rr(X44,X47)&~cc(X47))))|(![X48]:(~rr(X44,X48)|~cowlThing(X48))))|(![X49]:(~rp(X44,X49)|~cowlThing(X49))))|(?[X50]:(rp(X44,X50)&~ca_Vx4(X50))))|ca_Ax2(X44)))),inference(variable_rename,[status(thm)],[c68])).
% 0.79/0.97 fof(c71,plain,(![X37]:(![X38]:(![X39]:(![X40]:(![X43]:(![X44]:(![X48]:(![X49]:((~ca_Ax2(X37)|((((((~rp(X37,X38)|ca_Vx3(X38))&(~rp(X37,X39)|ca_Vx5(X39)))&(~rr(X37,X40)|cc(X40)))&(rr(X37,skolem0006(X37))&cowlThing(skolem0006(X37))))&(rp(X37,skolem0007(X37))&cowlThing(skolem0007(X37))))&(~rp(X37,X43)|ca_Vx4(X43))))&(((((((rp(X44,skolem0008(X44))&~ca_Vx3(skolem0008(X44)))|(rp(X44,skolem0009(X44))&~ca_Vx5(skolem0009(X44))))|(rr(X44,skolem0010(X44))&~cc(skolem0010(X44))))|(~rr(X44,X48)|~cowlThing(X48)))|(~rp(X44,X49)|~cowlThing(X49)))|(rp(X44,skolem0011(X44))&~ca_Vx4(skolem0011(X44))))|ca_Ax2(X44))))))))))),inference(shift_quantors,[status(thm)],[fof(c70,plain,((![X37]:(~ca_Ax2(X37)|((((((![X38]:(~rp(X37,X38)|ca_Vx3(X38)))&(![X39]:(~rp(X37,X39)|ca_Vx5(X39))))&(![X40]:(~rr(X37,X40)|cc(X40))))&(rr(X37,skolem0006(X37))&cowlThing(skolem0006(X37))))&(rp(X37,skolem0007(X37))&cowlThing(skolem0007(X37))))&(![X43]:(~rp(X37,X43)|ca_Vx4(X43))))))&(![X44]:(((((((rp(X44,skolem0008(X44))&~ca_Vx3(skolem0008(X44)))|(rp(X44,skolem0009(X44))&~ca_Vx5(skolem0009(X44))))|(rr(X44,skolem0010(X44))&~cc(skolem0010(X44))))|(![X48]:(~rr(X44,X48)|~cowlThing(X48))))|(![X49]:(~rp(X44,X49)|~cowlThing(X49))))|(rp(X44,skolem0011(X44))&~ca_Vx4(skolem0011(X44))))|ca_Ax2(X44)))),inference(skolemize,[status(esa)],[c69])).])).
% 0.79/0.97 fof(c72,plain,(![X37]:(![X38]:(![X39]:(![X40]:(![X43]:(![X44]:(![X48]:(![X49]:(((((((~ca_Ax2(X37)|(~rp(X37,X38)|ca_Vx3(X38)))&(~ca_Ax2(X37)|(~rp(X37,X39)|ca_Vx5(X39))))&(~ca_Ax2(X37)|(~rr(X37,X40)|cc(X40))))&((~ca_Ax2(X37)|rr(X37,skolem0006(X37)))&(~ca_Ax2(X37)|cowlThing(skolem0006(X37)))))&((~ca_Ax2(X37)|rp(X37,skolem0007(X37)))&(~ca_Ax2(X37)|cowlThing(skolem0007(X37)))))&(~ca_Ax2(X37)|(~rp(X37,X43)|ca_Vx4(X43))))&((((((((((rp(X44,skolem0008(X44))|rp(X44,skolem0009(X44)))|rr(X44,skolem0010(X44)))|(~rr(X44,X48)|~cowlThing(X48)))|(~rp(X44,X49)|~cowlThing(X49)))|rp(X44,skolem0011(X44)))|ca_Ax2(X44))&((((((rp(X44,skolem0008(X44))|rp(X44,skolem0009(X44)))|rr(X44,skolem0010(X44)))|(~rr(X44,X48)|~cowlThing(X48)))|(~rp(X44,X49)|~cowlThing(X49)))|~ca_Vx4(skolem0011(X44)))|ca_Ax2(X44)))&(((((((rp(X44,skolem0008(X44))|rp(X44,skolem0009(X44)))|~cc(skolem0010(X44)))|(~rr(X44,X48)|~cowlThing(X48)))|(~rp(X44,X49)|~cowlThing(X49)))|rp(X44,skolem0011(X44)))|ca_Ax2(X44))&((((((rp(X44,skolem0008(X44))|rp(X44,skolem0009(X44)))|~cc(skolem0010(X44)))|(~rr(X44,X48)|~cowlThing(X48)))|(~rp(X44,X49)|~cowlThing(X49)))|~ca_Vx4(skolem0011(X44)))|ca_Ax2(X44))))&((((((((rp(X44,skolem0008(X44))|~ca_Vx5(skolem0009(X44)))|rr(X44,skolem0010(X44)))|(~rr(X44,X48)|~cowlThing(X48)))|(~rp(X44,X49)|~cowlThing(X49)))|rp(X44,skolem0011(X44)))|ca_Ax2(X44))&((((((rp(X44,skolem0008(X44))|~ca_Vx5(skolem0009(X44)))|rr(X44,skolem0010(X44)))|(~rr(X44,X48)|~cowlThing(X48)))|(~rp(X44,X49)|~cowlThing(X49)))|~ca_Vx4(skolem0011(X44)))|ca_Ax2(X44)))&(((((((rp(X44,skolem0008(X44))|~ca_Vx5(skolem0009(X44)))|~cc(skolem0010(X44)))|(~rr(X44,X48)|~cowlThing(X48)))|(~rp(X44,X49)|~cowlThing(X49)))|rp(X44,skolem0011(X44)))|ca_Ax2(X44))&((((((rp(X44,skolem0008(X44))|~ca_Vx5(skolem0009(X44)))|~cc(skolem0010(X44)))|(~rr(X44,X48)|~cowlThing(X48)))|(~rp(X44,X49)|~cowlThing(X49)))|~ca_Vx4(skolem0011(X44)))|ca_Ax2(X44)))))&(((((((((~ca_Vx3(skolem0008(X44))|rp(X44,skolem0009(X44)))|rr(X44,skolem0010(X44)))|(~rr(X44,X48)|~cowlThing(X48)))|(~rp(X44,X49)|~cowlThing(X49)))|rp(X44,skolem0011(X44)))|ca_Ax2(X44))&((((((~ca_Vx3(skolem0008(X44))|rp(X44,skolem0009(X44)))|rr(X44,skolem0010(X44)))|(~rr(X44,X48)|~cowlThing(X48)))|(~rp(X44,X49)|~cowlThing(X49)))|~ca_Vx4(skolem0011(X44)))|ca_Ax2(X44)))&(((((((~ca_Vx3(skolem0008(X44))|rp(X44,skolem0009(X44)))|~cc(skolem0010(X44)))|(~rr(X44,X48)|~cowlThing(X48)))|(~rp(X44,X49)|~cowlThing(X49)))|rp(X44,skolem0011(X44)))|ca_Ax2(X44))&((((((~ca_Vx3(skolem0008(X44))|rp(X44,skolem0009(X44)))|~cc(skolem0010(X44)))|(~rr(X44,X48)|~cowlThing(X48)))|(~rp(X44,X49)|~cowlThing(X49)))|~ca_Vx4(skolem0011(X44)))|ca_Ax2(X44))))&((((((((~ca_Vx3(skolem0008(X44))|~ca_Vx5(skolem0009(X44)))|rr(X44,skolem0010(X44)))|(~rr(X44,X48)|~cowlThing(X48)))|(~rp(X44,X49)|~cowlThing(X49)))|rp(X44,skolem0011(X44)))|ca_Ax2(X44))&((((((~ca_Vx3(skolem0008(X44))|~ca_Vx5(skolem0009(X44)))|rr(X44,skolem0010(X44)))|(~rr(X44,X48)|~cowlThing(X48)))|(~rp(X44,X49)|~cowlThing(X49)))|~ca_Vx4(skolem0011(X44)))|ca_Ax2(X44)))&(((((((~ca_Vx3(skolem0008(X44))|~ca_Vx5(skolem0009(X44)))|~cc(skolem0010(X44)))|(~rr(X44,X48)|~cowlThing(X48)))|(~rp(X44,X49)|~cowlThing(X49)))|rp(X44,skolem0011(X44)))|ca_Ax2(X44))&((((((~ca_Vx3(skolem0008(X44))|~ca_Vx5(skolem0009(X44)))|~cc(skolem0010(X44)))|(~rr(X44,X48)|~cowlThing(X48)))|(~rp(X44,X49)|~cowlThing(X49)))|~ca_Vx4(skolem0011(X44)))|ca_Ax2(X44))))))))))))))),inference(distribute,[status(thm)],[c71])).
% 0.79/0.97 cnf(c78,plain,~ca_Ax2(X117)|rp(X117,skolem0007(X117)),inference(split_conjunct,[status(thm)],[c72])).
% 0.79/0.97 cnf(c155,plain,rp(skolem0015(i2003_11_14_17_21_33997),skolem0007(skolem0015(i2003_11_14_17_21_33997))),inference(resolution,[status(thm)],[c78, c148])).
% 0.79/0.97 cnf(c227,plain,rinvP(skolem0007(skolem0015(i2003_11_14_17_21_33997)),skolem0015(i2003_11_14_17_21_33997)),inference(resolution,[status(thm)],[c155, c21])).
% 0.79/0.97 cnf(c248,plain,~ca_Vx7(skolem0007(skolem0015(i2003_11_14_17_21_33997)))|ca_Vx6(skolem0015(i2003_11_14_17_21_33997)),inference(resolution,[status(thm)],[c227, c28])).
% 0.79/0.97 cnf(c74,plain,~ca_Ax2(X139)|~rp(X139,X140)|ca_Vx5(X140),inference(split_conjunct,[status(thm)],[c72])).
% 0.79/0.97 cnf(c235,plain,~ca_Ax2(skolem0015(i2003_11_14_17_21_33997))|ca_Vx5(skolem0007(skolem0015(i2003_11_14_17_21_33997))),inference(resolution,[status(thm)],[c155, c74])).
% 0.79/0.97 cnf(c375,plain,ca_Vx5(skolem0007(skolem0015(i2003_11_14_17_21_33997))),inference(resolution,[status(thm)],[c235, c148])).
% 0.79/0.97 fof(axiom_10,axiom,(![X]:(ca_Vx5(X)<=>(![Y]:(rr(X,Y)=>cc(Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_10)).
% 0.79/0.97 fof(c40,plain,(![X]:((~ca_Vx5(X)|(![Y]:(~rr(X,Y)|cc(Y))))&((?[Y]:(rr(X,Y)&~cc(Y)))|ca_Vx5(X)))),inference(fof_nnf,[status(thm)],[axiom_10])).
% 0.79/0.97 fof(c41,plain,((![X]:(~ca_Vx5(X)|(![Y]:(~rr(X,Y)|cc(Y)))))&(![X]:((?[Y]:(rr(X,Y)&~cc(Y)))|ca_Vx5(X)))),inference(shift_quantors,[status(thm)],[c40])).
% 0.79/0.97 fof(c42,plain,((![X25]:(~ca_Vx5(X25)|(![X26]:(~rr(X25,X26)|cc(X26)))))&(![X27]:((?[X28]:(rr(X27,X28)&~cc(X28)))|ca_Vx5(X27)))),inference(variable_rename,[status(thm)],[c41])).
% 0.79/0.97 fof(c44,plain,(![X25]:(![X26]:(![X27]:((~ca_Vx5(X25)|(~rr(X25,X26)|cc(X26)))&((rr(X27,skolem0003(X27))&~cc(skolem0003(X27)))|ca_Vx5(X27)))))),inference(shift_quantors,[status(thm)],[fof(c43,plain,((![X25]:(~ca_Vx5(X25)|(![X26]:(~rr(X25,X26)|cc(X26)))))&(![X27]:((rr(X27,skolem0003(X27))&~cc(skolem0003(X27)))|ca_Vx5(X27)))),inference(skolemize,[status(esa)],[c42])).])).
% 0.79/0.97 fof(c45,plain,(![X25]:(![X26]:(![X27]:((~ca_Vx5(X25)|(~rr(X25,X26)|cc(X26)))&((rr(X27,skolem0003(X27))|ca_Vx5(X27))&(~cc(skolem0003(X27))|ca_Vx5(X27))))))),inference(distribute,[status(thm)],[c44])).
% 0.79/0.97 cnf(c46,plain,~ca_Vx5(X114)|~rr(X114,X115)|cc(X115),inference(split_conjunct,[status(thm)],[c45])).
% 0.79/0.97 fof(axiom_8,axiom,(![X]:(ca_Vx3(X)<=>(?[Y]:(rr(X,Y)&cowlThing(Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_8)).
% 0.79/0.97 fof(c58,plain,(![X]:((~ca_Vx3(X)|(?[Y]:(rr(X,Y)&cowlThing(Y))))&((![Y]:(~rr(X,Y)|~cowlThing(Y)))|ca_Vx3(X)))),inference(fof_nnf,[status(thm)],[axiom_8])).
% 0.79/0.97 fof(c59,plain,((![X]:(~ca_Vx3(X)|(?[Y]:(rr(X,Y)&cowlThing(Y)))))&(![X]:((![Y]:(~rr(X,Y)|~cowlThing(Y)))|ca_Vx3(X)))),inference(shift_quantors,[status(thm)],[c58])).
% 0.79/0.97 fof(c60,plain,((![X33]:(~ca_Vx3(X33)|(?[X34]:(rr(X33,X34)&cowlThing(X34)))))&(![X35]:((![X36]:(~rr(X35,X36)|~cowlThing(X36)))|ca_Vx3(X35)))),inference(variable_rename,[status(thm)],[c59])).
% 0.79/0.97 fof(c62,plain,(![X33]:(![X35]:(![X36]:((~ca_Vx3(X33)|(rr(X33,skolem0005(X33))&cowlThing(skolem0005(X33))))&((~rr(X35,X36)|~cowlThing(X36))|ca_Vx3(X35)))))),inference(shift_quantors,[status(thm)],[fof(c61,plain,((![X33]:(~ca_Vx3(X33)|(rr(X33,skolem0005(X33))&cowlThing(skolem0005(X33)))))&(![X35]:((![X36]:(~rr(X35,X36)|~cowlThing(X36)))|ca_Vx3(X35)))),inference(skolemize,[status(esa)],[c60])).])).
% 0.79/0.97 fof(c63,plain,(![X33]:(![X35]:(![X36]:(((~ca_Vx3(X33)|rr(X33,skolem0005(X33)))&(~ca_Vx3(X33)|cowlThing(skolem0005(X33))))&((~rr(X35,X36)|~cowlThing(X36))|ca_Vx3(X35)))))),inference(distribute,[status(thm)],[c62])).
% 0.79/0.97 cnf(c64,plain,~ca_Vx3(X113)|rr(X113,skolem0005(X113)),inference(split_conjunct,[status(thm)],[c63])).
% 0.79/0.97 cnf(c73,plain,~ca_Ax2(X132)|~rp(X132,X133)|ca_Vx3(X133),inference(split_conjunct,[status(thm)],[c72])).
% 0.79/0.97 cnf(c229,plain,~ca_Ax2(skolem0015(i2003_11_14_17_21_33997))|ca_Vx3(skolem0007(skolem0015(i2003_11_14_17_21_33997))),inference(resolution,[status(thm)],[c155, c73])).
% 0.79/0.97 cnf(c353,plain,ca_Vx3(skolem0007(skolem0015(i2003_11_14_17_21_33997))),inference(resolution,[status(thm)],[c229, c148])).
% 0.79/0.97 cnf(c354,plain,rr(skolem0007(skolem0015(i2003_11_14_17_21_33997)),skolem0005(skolem0007(skolem0015(i2003_11_14_17_21_33997)))),inference(resolution,[status(thm)],[c353, c64])).
% 0.79/0.97 cnf(c551,plain,~ca_Vx5(skolem0007(skolem0015(i2003_11_14_17_21_33997)))|cc(skolem0005(skolem0007(skolem0015(i2003_11_14_17_21_33997)))),inference(resolution,[status(thm)],[c354, c46])).
% 0.79/0.97 cnf(c827,plain,cc(skolem0005(skolem0007(skolem0015(i2003_11_14_17_21_33997)))),inference(resolution,[status(thm)],[c551, c375])).
% 0.79/0.97 fof(axiom_6,axiom,(![X]:(cc(X)<=>(![Y]:(rinvR(X,Y)=>ca_Vx7(Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_6)).
% 0.79/0.97 fof(c97,plain,(![X]:((~cc(X)|(![Y]:(~rinvR(X,Y)|ca_Vx7(Y))))&((?[Y]:(rinvR(X,Y)&~ca_Vx7(Y)))|cc(X)))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 0.79/0.97 fof(c98,plain,((![X]:(~cc(X)|(![Y]:(~rinvR(X,Y)|ca_Vx7(Y)))))&(![X]:((?[Y]:(rinvR(X,Y)&~ca_Vx7(Y)))|cc(X)))),inference(shift_quantors,[status(thm)],[c97])).
% 0.79/0.97 fof(c99,plain,((![X51]:(~cc(X51)|(![X52]:(~rinvR(X51,X52)|ca_Vx7(X52)))))&(![X53]:((?[X54]:(rinvR(X53,X54)&~ca_Vx7(X54)))|cc(X53)))),inference(variable_rename,[status(thm)],[c98])).
% 0.79/0.97 fof(c101,plain,(![X51]:(![X52]:(![X53]:((~cc(X51)|(~rinvR(X51,X52)|ca_Vx7(X52)))&((rinvR(X53,skolem0012(X53))&~ca_Vx7(skolem0012(X53)))|cc(X53)))))),inference(shift_quantors,[status(thm)],[fof(c100,plain,((![X51]:(~cc(X51)|(![X52]:(~rinvR(X51,X52)|ca_Vx7(X52)))))&(![X53]:((rinvR(X53,skolem0012(X53))&~ca_Vx7(skolem0012(X53)))|cc(X53)))),inference(skolemize,[status(esa)],[c99])).])).
% 0.79/0.97 fof(c102,plain,(![X51]:(![X52]:(![X53]:((~cc(X51)|(~rinvR(X51,X52)|ca_Vx7(X52)))&((rinvR(X53,skolem0012(X53))|cc(X53))&(~ca_Vx7(skolem0012(X53))|cc(X53))))))),inference(distribute,[status(thm)],[c101])).
% 0.79/0.97 cnf(c103,plain,~cc(X150)|~rinvR(X150,X151)|ca_Vx7(X151),inference(split_conjunct,[status(thm)],[c102])).
% 0.79/0.97 fof(axiom_14,axiom,(![X]:(![Y]:(rinvR(X,Y)<=>rr(Y,X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_14)).
% 0.79/0.97 fof(c10,plain,(![X]:(![Y]:((~rinvR(X,Y)|rr(Y,X))&(~rr(Y,X)|rinvR(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_14])).
% 0.79/0.97 fof(c11,plain,((![X]:(![Y]:(~rinvR(X,Y)|rr(Y,X))))&(![X]:(![Y]:(~rr(Y,X)|rinvR(X,Y))))),inference(shift_quantors,[status(thm)],[c10])).
% 0.79/0.97 fof(c13,plain,(![X9]:(![X10]:(![X11]:(![X12]:((~rinvR(X9,X10)|rr(X10,X9))&(~rr(X12,X11)|rinvR(X11,X12))))))),inference(shift_quantors,[status(thm)],[fof(c12,plain,((![X9]:(![X10]:(~rinvR(X9,X10)|rr(X10,X9))))&(![X11]:(![X12]:(~rr(X12,X11)|rinvR(X11,X12))))),inference(variable_rename,[status(thm)],[c11])).])).
% 0.79/0.97 cnf(c15,plain,~rr(X89,X90)|rinvR(X90,X89),inference(split_conjunct,[status(thm)],[c13])).
% 0.79/0.97 cnf(c553,plain,rinvR(skolem0005(skolem0007(skolem0015(i2003_11_14_17_21_33997))),skolem0007(skolem0015(i2003_11_14_17_21_33997))),inference(resolution,[status(thm)],[c354, c15])).
% 0.79/0.97 cnf(c628,plain,~cc(skolem0005(skolem0007(skolem0015(i2003_11_14_17_21_33997))))|ca_Vx7(skolem0007(skolem0015(i2003_11_14_17_21_33997))),inference(resolution,[status(thm)],[c553, c103])).
% 0.79/0.97 cnf(c943,plain,ca_Vx7(skolem0007(skolem0015(i2003_11_14_17_21_33997))),inference(resolution,[status(thm)],[c628, c827])).
% 0.79/0.97 cnf(c962,plain,ca_Vx6(skolem0015(i2003_11_14_17_21_33997)),inference(resolution,[status(thm)],[c943, c248])).
% 0.79/0.97 cnf(c965,plain,caxcomp(i2003_11_14_17_21_33997),inference(resolution,[status(thm)],[c962, c166])).
% 0.79/0.97 cnf(c966,plain,ra_Px1(i2003_11_14_17_21_33997,skolem0013(i2003_11_14_17_21_33997)),inference(resolution,[status(thm)],[c965, c111])).
% 0.79/0.97 cnf(c968,plain,~ca(i2003_11_14_17_21_33997),inference(resolution,[status(thm)],[c966, c118])).
% 0.79/0.97 cnf(c971,plain,$false,inference(resolution,[status(thm)],[c968, c142])).
% 0.79/0.97 % SZS output end CNFRefutation
% 0.79/0.97
% 0.79/0.97 % Initial clauses : 61
% 0.79/0.97 % Processed clauses : 256
% 0.79/0.97 % Factors computed : 5
% 0.79/0.97 % Resolvents computed: 828
% 0.79/0.97 % Tautologies deleted: 10
% 0.79/0.97 % Forward subsumed : 112
% 0.79/0.97 % Backward subsumed : 39
% 0.79/0.97 % -------- CPU Time ---------
% 0.79/0.97 % User time : 0.586 s
% 0.79/0.97 % System time : 0.016 s
% 0.79/0.97 % Total time : 0.602 s
%------------------------------------------------------------------------------