%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS104+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n012.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:42 EDT 2024
% Result : Unsatisfiable 0.46s 0.64s
% Output : Refutation 0.46s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : KRS104+1 : TPTP v8.1.2. Released v3.1.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n012.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:07:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.46/0.64 % Version: 1.5
% 0.46/0.64 % SZS status Unsatisfiable
% 0.46/0.64 % SZS output start CNFRefutation
% 0.46/0.64 fof(axiom_23,axiom,cUnsatisfiable(i2003_11_14_17_20_50869),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_23)).
% 0.46/0.64 cnf(c0,plain,cUnsatisfiable(i2003_11_14_17_20_50869),inference(split_conjunct,[status(thm)],[axiom_23])).
% 0.46/0.64 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)<=>(~(?[Y]:ra_Px5(X,Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 0.46/0.64 fof(c139,plain,(![X]:((~cUnsatisfiable(X)|(![Y]:~ra_Px5(X,Y)))&((?[Y]:ra_Px5(X,Y))|cUnsatisfiable(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 0.46/0.64 fof(c140,plain,((![X]:(~cUnsatisfiable(X)|(![Y]:~ra_Px5(X,Y))))&(![X]:((?[Y]:ra_Px5(X,Y))|cUnsatisfiable(X)))),inference(shift_quantors,[status(thm)],[c139])).
% 0.46/0.64 fof(c141,plain,((![X66]:(~cUnsatisfiable(X66)|(![X67]:~ra_Px5(X66,X67))))&(![X68]:((?[X69]:ra_Px5(X68,X69))|cUnsatisfiable(X68)))),inference(variable_rename,[status(thm)],[c140])).
% 0.46/0.64 fof(c143,plain,(![X66]:(![X67]:(![X68]:((~cUnsatisfiable(X66)|~ra_Px5(X66,X67))&(ra_Px5(X68,skolem0014(X68))|cUnsatisfiable(X68)))))),inference(shift_quantors,[status(thm)],[fof(c142,plain,((![X66]:(~cUnsatisfiable(X66)|(![X67]:~ra_Px5(X66,X67))))&(![X68]:(ra_Px5(X68,skolem0014(X68))|cUnsatisfiable(X68)))),inference(skolemize,[status(esa)],[c141])).])).
% 0.46/0.64 cnf(c144,plain,~cUnsatisfiable(X136)|~ra_Px5(X136,X137),inference(split_conjunct,[status(thm)],[c143])).
% 0.46/0.64 fof(axiom_4,axiom,(![X]:(cUnsatisfiablexcomp(X)<=>(?[Y0]:ra_Px5(X,Y0)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_4)).
% 0.46/0.64 fof(c123,plain,(![X]:((~cUnsatisfiablexcomp(X)|(?[Y0]:ra_Px5(X,Y0)))&((![Y0]:~ra_Px5(X,Y0))|cUnsatisfiablexcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 0.46/0.64 fof(c124,plain,((![X]:(~cUnsatisfiablexcomp(X)|(?[Y0]:ra_Px5(X,Y0))))&(![X]:((![Y0]:~ra_Px5(X,Y0))|cUnsatisfiablexcomp(X)))),inference(shift_quantors,[status(thm)],[c123])).
% 0.46/0.64 fof(c125,plain,((![X60]:(~cUnsatisfiablexcomp(X60)|(?[X61]:ra_Px5(X60,X61))))&(![X62]:((![X63]:~ra_Px5(X62,X63))|cUnsatisfiablexcomp(X62)))),inference(variable_rename,[status(thm)],[c124])).
% 0.46/0.64 fof(c127,plain,(![X60]:(![X62]:(![X63]:((~cUnsatisfiablexcomp(X60)|ra_Px5(X60,skolem0013(X60)))&(~ra_Px5(X62,X63)|cUnsatisfiablexcomp(X62)))))),inference(shift_quantors,[status(thm)],[fof(c126,plain,((![X60]:(~cUnsatisfiablexcomp(X60)|ra_Px5(X60,skolem0013(X60))))&(![X62]:((![X63]:~ra_Px5(X62,X63))|cUnsatisfiablexcomp(X62)))),inference(skolemize,[status(esa)],[c125])).])).
% 0.46/0.64 cnf(c128,plain,~cUnsatisfiablexcomp(X165)|ra_Px5(X165,skolem0013(X165)),inference(split_conjunct,[status(thm)],[c127])).
% 0.46/0.64 fof(axiom_11,axiom,(![X]:(ca_Cx1(X)<=>(cbxcomp(X)&ccxcomp(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_11)).
% 0.46/0.64 fof(c81,plain,(![X]:((~ca_Cx1(X)|(cbxcomp(X)&ccxcomp(X)))&((~cbxcomp(X)|~ccxcomp(X))|ca_Cx1(X)))),inference(fof_nnf,[status(thm)],[axiom_11])).
% 0.46/0.64 fof(c82,plain,((![X]:(~ca_Cx1(X)|(cbxcomp(X)&ccxcomp(X))))&(![X]:((~cbxcomp(X)|~ccxcomp(X))|ca_Cx1(X)))),inference(shift_quantors,[status(thm)],[c81])).
% 0.46/0.64 fof(c84,plain,(![X40]:(![X41]:((~ca_Cx1(X40)|(cbxcomp(X40)&ccxcomp(X40)))&((~cbxcomp(X41)|~ccxcomp(X41))|ca_Cx1(X41))))),inference(shift_quantors,[status(thm)],[fof(c83,plain,((![X40]:(~ca_Cx1(X40)|(cbxcomp(X40)&ccxcomp(X40))))&(![X41]:((~cbxcomp(X41)|~ccxcomp(X41))|ca_Cx1(X41)))),inference(variable_rename,[status(thm)],[c82])).])).
% 0.46/0.64 fof(c85,plain,(![X40]:(![X41]:(((~ca_Cx1(X40)|cbxcomp(X40))&(~ca_Cx1(X40)|ccxcomp(X40)))&((~cbxcomp(X41)|~ccxcomp(X41))|ca_Cx1(X41))))),inference(distribute,[status(thm)],[c84])).
% 0.46/0.64 cnf(c87,plain,~ca_Cx1(X85)|ccxcomp(X85),inference(split_conjunct,[status(thm)],[c85])).
% 0.46/0.64 fof(axiom_5,axiom,(![X]:(ca(X)=>ca_Cx1(X))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_5)).
% 0.46/0.64 fof(c120,plain,(![X]:(~ca(X)|ca_Cx1(X))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 0.46/0.64 fof(c121,plain,(![X59]:(~ca(X59)|ca_Cx1(X59))),inference(variable_rename,[status(thm)],[c120])).
% 0.46/0.64 cnf(c122,plain,~ca(X87)|ca_Cx1(X87),inference(split_conjunct,[status(thm)],[c121])).
% 0.46/0.64 fof(axiom_18,axiom,(![X]:(ca_Cx7xcomp(X)<=>(cc(X)&ca(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_18)).
% 0.46/0.64 fof(c30,plain,(![X]:((~ca_Cx7xcomp(X)|(cc(X)&ca(X)))&((~cc(X)|~ca(X))|ca_Cx7xcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_18])).
% 0.46/0.64 fof(c31,plain,((![X]:(~ca_Cx7xcomp(X)|(cc(X)&ca(X))))&(![X]:((~cc(X)|~ca(X))|ca_Cx7xcomp(X)))),inference(shift_quantors,[status(thm)],[c30])).
% 0.46/0.64 fof(c33,plain,(![X16]:(![X17]:((~ca_Cx7xcomp(X16)|(cc(X16)&ca(X16)))&((~cc(X17)|~ca(X17))|ca_Cx7xcomp(X17))))),inference(shift_quantors,[status(thm)],[fof(c32,plain,((![X16]:(~ca_Cx7xcomp(X16)|(cc(X16)&ca(X16))))&(![X17]:((~cc(X17)|~ca(X17))|ca_Cx7xcomp(X17)))),inference(variable_rename,[status(thm)],[c31])).])).
% 0.46/0.64 fof(c34,plain,(![X16]:(![X17]:(((~ca_Cx7xcomp(X16)|cc(X16))&(~ca_Cx7xcomp(X16)|ca(X16)))&((~cc(X17)|~ca(X17))|ca_Cx7xcomp(X17))))),inference(distribute,[status(thm)],[c33])).
% 0.46/0.64 cnf(c36,plain,~ca_Cx7xcomp(X80)|ca(X80),inference(split_conjunct,[status(thm)],[c34])).
% 0.46/0.64 fof(axiom_17,axiom,(![X]:(ca_Cx7(X)<=>(?[Y0]:ra_Px7(X,Y0)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_17)).
% 0.46/0.64 fof(c38,plain,(![X]:((~ca_Cx7(X)|(?[Y0]:ra_Px7(X,Y0)))&((![Y0]:~ra_Px7(X,Y0))|ca_Cx7(X)))),inference(fof_nnf,[status(thm)],[axiom_17])).
% 0.46/0.64 fof(c39,plain,((![X]:(~ca_Cx7(X)|(?[Y0]:ra_Px7(X,Y0))))&(![X]:((![Y0]:~ra_Px7(X,Y0))|ca_Cx7(X)))),inference(shift_quantors,[status(thm)],[c38])).
% 0.46/0.64 fof(c40,plain,((![X18]:(~ca_Cx7(X18)|(?[X19]:ra_Px7(X18,X19))))&(![X20]:((![X21]:~ra_Px7(X20,X21))|ca_Cx7(X20)))),inference(variable_rename,[status(thm)],[c39])).
% 0.46/0.64 fof(c42,plain,(![X18]:(![X20]:(![X21]:((~ca_Cx7(X18)|ra_Px7(X18,skolem0004(X18)))&(~ra_Px7(X20,X21)|ca_Cx7(X20)))))),inference(shift_quantors,[status(thm)],[fof(c41,plain,((![X18]:(~ca_Cx7(X18)|ra_Px7(X18,skolem0004(X18))))&(![X20]:((![X21]:~ra_Px7(X20,X21))|ca_Cx7(X20)))),inference(skolemize,[status(esa)],[c40])).])).
% 0.46/0.64 cnf(c44,plain,~ra_Px7(X106,X107)|ca_Cx7(X106),inference(split_conjunct,[status(thm)],[c42])).
% 0.46/0.64 fof(axiom_19,axiom,(![X]:(ca_Cx7xcomp(X)<=>(~(?[Y]:ra_Px7(X,Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_19)).
% 0.46/0.64 fof(c23,plain,(![X]:((~ca_Cx7xcomp(X)|(![Y]:~ra_Px7(X,Y)))&((?[Y]:ra_Px7(X,Y))|ca_Cx7xcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_19])).
% 0.46/0.64 fof(c24,plain,((![X]:(~ca_Cx7xcomp(X)|(![Y]:~ra_Px7(X,Y))))&(![X]:((?[Y]:ra_Px7(X,Y))|ca_Cx7xcomp(X)))),inference(shift_quantors,[status(thm)],[c23])).
% 0.46/0.64 fof(c25,plain,((![X12]:(~ca_Cx7xcomp(X12)|(![X13]:~ra_Px7(X12,X13))))&(![X14]:((?[X15]:ra_Px7(X14,X15))|ca_Cx7xcomp(X14)))),inference(variable_rename,[status(thm)],[c24])).
% 0.46/0.64 fof(c27,plain,(![X12]:(![X13]:(![X14]:((~ca_Cx7xcomp(X12)|~ra_Px7(X12,X13))&(ra_Px7(X14,skolem0003(X14))|ca_Cx7xcomp(X14)))))),inference(shift_quantors,[status(thm)],[fof(c26,plain,((![X12]:(~ca_Cx7xcomp(X12)|(![X13]:~ra_Px7(X12,X13))))&(![X14]:(ra_Px7(X14,skolem0003(X14))|ca_Cx7xcomp(X14)))),inference(skolemize,[status(esa)],[c25])).])).
% 0.46/0.64 cnf(c29,plain,ra_Px7(X116,skolem0003(X116))|ca_Cx7xcomp(X116),inference(split_conjunct,[status(thm)],[c27])).
% 0.46/0.64 cnf(c168,plain,ca_Cx7xcomp(X118)|ca_Cx7(X118),inference(resolution,[status(thm)],[c29, c44])).
% 0.46/0.64 cnf(c172,plain,ca_Cx7(X120)|ca(X120),inference(resolution,[status(thm)],[c168, c36])).
% 0.46/0.64 cnf(c173,plain,ca_Cx7(X121)|ca_Cx1(X121),inference(resolution,[status(thm)],[c172, c122])).
% 0.46/0.64 cnf(c175,plain,ca_Cx7(X124)|ccxcomp(X124),inference(resolution,[status(thm)],[c173, c87])).
% 0.46/0.64 fof(axiom_10,axiom,(![X]:(ccxcomp(X)<=>(~(?[Y]:ra_Px2(X,Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_10)).
% 0.46/0.64 fof(c89,plain,(![X]:((~ccxcomp(X)|(![Y]:~ra_Px2(X,Y)))&((?[Y]:ra_Px2(X,Y))|ccxcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_10])).
% 0.46/0.64 fof(c90,plain,((![X]:(~ccxcomp(X)|(![Y]:~ra_Px2(X,Y))))&(![X]:((?[Y]:ra_Px2(X,Y))|ccxcomp(X)))),inference(shift_quantors,[status(thm)],[c89])).
% 0.46/0.64 fof(c91,plain,((![X42]:(~ccxcomp(X42)|(![X43]:~ra_Px2(X42,X43))))&(![X44]:((?[X45]:ra_Px2(X44,X45))|ccxcomp(X44)))),inference(variable_rename,[status(thm)],[c90])).
% 0.46/0.64 fof(c93,plain,(![X42]:(![X43]:(![X44]:((~ccxcomp(X42)|~ra_Px2(X42,X43))&(ra_Px2(X44,skolem0009(X44))|ccxcomp(X44)))))),inference(shift_quantors,[status(thm)],[fof(c92,plain,((![X42]:(~ccxcomp(X42)|(![X43]:~ra_Px2(X42,X43))))&(![X44]:(ra_Px2(X44,skolem0009(X44))|ccxcomp(X44)))),inference(skolemize,[status(esa)],[c91])).])).
% 0.46/0.65 cnf(c94,plain,~ccxcomp(X125)|~ra_Px2(X125,X126),inference(split_conjunct,[status(thm)],[c93])).
% 0.46/0.65 cnf(c35,plain,~ca_Cx7xcomp(X79)|cc(X79),inference(split_conjunct,[status(thm)],[c34])).
% 0.46/0.65 cnf(c171,plain,ca_Cx7(X119)|cc(X119),inference(resolution,[status(thm)],[c168, c35])).
% 0.46/0.65 fof(axiom_9,axiom,(![X]:(cc(X)<=>(?[Y0]:ra_Px2(X,Y0)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_9)).
% 0.46/0.65 fof(c96,plain,(![X]:((~cc(X)|(?[Y0]:ra_Px2(X,Y0)))&((![Y0]:~ra_Px2(X,Y0))|cc(X)))),inference(fof_nnf,[status(thm)],[axiom_9])).
% 0.46/0.65 fof(c97,plain,((![X]:(~cc(X)|(?[Y0]:ra_Px2(X,Y0))))&(![X]:((![Y0]:~ra_Px2(X,Y0))|cc(X)))),inference(shift_quantors,[status(thm)],[c96])).
% 0.46/0.65 fof(c98,plain,((![X46]:(~cc(X46)|(?[X47]:ra_Px2(X46,X47))))&(![X48]:((![X49]:~ra_Px2(X48,X49))|cc(X48)))),inference(variable_rename,[status(thm)],[c97])).
% 0.46/0.65 fof(c100,plain,(![X46]:(![X48]:(![X49]:((~cc(X46)|ra_Px2(X46,skolem0010(X46)))&(~ra_Px2(X48,X49)|cc(X48)))))),inference(shift_quantors,[status(thm)],[fof(c99,plain,((![X46]:(~cc(X46)|ra_Px2(X46,skolem0010(X46))))&(![X48]:((![X49]:~ra_Px2(X48,X49))|cc(X48)))),inference(skolemize,[status(esa)],[c98])).])).
% 0.46/0.65 cnf(c101,plain,~cc(X158)|ra_Px2(X158,skolem0010(X158)),inference(split_conjunct,[status(thm)],[c100])).
% 0.46/0.65 cnf(c211,plain,ra_Px2(X241,skolem0010(X241))|ca_Cx7(X241),inference(resolution,[status(thm)],[c101, c171])).
% 0.46/0.65 cnf(c336,plain,ca_Cx7(X243)|~ccxcomp(X243),inference(resolution,[status(thm)],[c211, c94])).
% 0.46/0.65 cnf(c348,plain,ca_Cx7(X244),inference(resolution,[status(thm)],[c336, c175])).
% 0.46/0.65 fof(axiom_7,axiom,(![X]:(cb(X)=>ccxcomp(X))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_7)).
% 0.46/0.65 fof(c110,plain,(![X]:(~cb(X)|ccxcomp(X))),inference(fof_nnf,[status(thm)],[axiom_7])).
% 0.46/0.65 fof(c111,plain,(![X54]:(~cb(X54)|ccxcomp(X54))),inference(variable_rename,[status(thm)],[c110])).
% 0.46/0.65 cnf(c112,plain,~cb(X86)|ccxcomp(X86),inference(split_conjunct,[status(thm)],[c111])).
% 0.46/0.65 fof(axiom_22,axiom,(![X]:(ca_Cx8xcomp(X)<=>(cc(X)&cb(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_22)).
% 0.46/0.65 fof(c1,plain,(![X]:((~ca_Cx8xcomp(X)|(cc(X)&cb(X)))&((~cc(X)|~cb(X))|ca_Cx8xcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_22])).
% 0.46/0.65 fof(c2,plain,((![X]:(~ca_Cx8xcomp(X)|(cc(X)&cb(X))))&(![X]:((~cc(X)|~cb(X))|ca_Cx8xcomp(X)))),inference(shift_quantors,[status(thm)],[c1])).
% 0.46/0.65 fof(c4,plain,(![X2]:(![X3]:((~ca_Cx8xcomp(X2)|(cc(X2)&cb(X2)))&((~cc(X3)|~cb(X3))|ca_Cx8xcomp(X3))))),inference(shift_quantors,[status(thm)],[fof(c3,plain,((![X2]:(~ca_Cx8xcomp(X2)|(cc(X2)&cb(X2))))&(![X3]:((~cc(X3)|~cb(X3))|ca_Cx8xcomp(X3)))),inference(variable_rename,[status(thm)],[c2])).])).
% 0.46/0.65 fof(c5,plain,(![X2]:(![X3]:(((~ca_Cx8xcomp(X2)|cc(X2))&(~ca_Cx8xcomp(X2)|cb(X2)))&((~cc(X3)|~cb(X3))|ca_Cx8xcomp(X3))))),inference(distribute,[status(thm)],[c4])).
% 0.46/0.65 cnf(c7,plain,~ca_Cx8xcomp(X77)|cb(X77),inference(split_conjunct,[status(thm)],[c5])).
% 0.46/0.65 fof(axiom_21,axiom,(![X]:(ca_Cx8xcomp(X)<=>(?[Y0]:ra_Px8(X,Y0)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_21)).
% 0.46/0.65 fof(c9,plain,(![X]:((~ca_Cx8xcomp(X)|(?[Y0]:ra_Px8(X,Y0)))&((![Y0]:~ra_Px8(X,Y0))|ca_Cx8xcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_21])).
% 0.46/0.65 fof(c10,plain,((![X]:(~ca_Cx8xcomp(X)|(?[Y0]:ra_Px8(X,Y0))))&(![X]:((![Y0]:~ra_Px8(X,Y0))|ca_Cx8xcomp(X)))),inference(shift_quantors,[status(thm)],[c9])).
% 0.46/0.65 fof(c11,plain,((![X4]:(~ca_Cx8xcomp(X4)|(?[X5]:ra_Px8(X4,X5))))&(![X6]:((![X7]:~ra_Px8(X6,X7))|ca_Cx8xcomp(X6)))),inference(variable_rename,[status(thm)],[c10])).
% 0.46/0.65 fof(c13,plain,(![X4]:(![X6]:(![X7]:((~ca_Cx8xcomp(X4)|ra_Px8(X4,skolem0001(X4)))&(~ra_Px8(X6,X7)|ca_Cx8xcomp(X6)))))),inference(shift_quantors,[status(thm)],[fof(c12,plain,((![X4]:(~ca_Cx8xcomp(X4)|ra_Px8(X4,skolem0001(X4))))&(![X6]:((![X7]:~ra_Px8(X6,X7))|ca_Cx8xcomp(X6)))),inference(skolemize,[status(esa)],[c11])).])).
% 0.46/0.65 cnf(c15,plain,~ra_Px8(X91,X90)|ca_Cx8xcomp(X91),inference(split_conjunct,[status(thm)],[c13])).
% 0.46/0.65 fof(axiom_20,axiom,(![X]:(ca_Cx8(X)<=>(~(?[Y]:ra_Px8(X,Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_20)).
% 0.46/0.65 fof(c16,plain,(![X]:((~ca_Cx8(X)|(![Y]:~ra_Px8(X,Y)))&((?[Y]:ra_Px8(X,Y))|ca_Cx8(X)))),inference(fof_nnf,[status(thm)],[axiom_20])).
% 0.46/0.65 fof(c17,plain,((![X]:(~ca_Cx8(X)|(![Y]:~ra_Px8(X,Y))))&(![X]:((?[Y]:ra_Px8(X,Y))|ca_Cx8(X)))),inference(shift_quantors,[status(thm)],[c16])).
% 0.46/0.65 fof(c18,plain,((![X8]:(~ca_Cx8(X8)|(![X9]:~ra_Px8(X8,X9))))&(![X10]:((?[X11]:ra_Px8(X10,X11))|ca_Cx8(X10)))),inference(variable_rename,[status(thm)],[c17])).
% 0.46/0.65 fof(c20,plain,(![X8]:(![X9]:(![X10]:((~ca_Cx8(X8)|~ra_Px8(X8,X9))&(ra_Px8(X10,skolem0002(X10))|ca_Cx8(X10)))))),inference(shift_quantors,[status(thm)],[fof(c19,plain,((![X8]:(~ca_Cx8(X8)|(![X9]:~ra_Px8(X8,X9))))&(![X10]:(ra_Px8(X10,skolem0002(X10))|ca_Cx8(X10)))),inference(skolemize,[status(esa)],[c18])).])).
% 0.46/0.65 cnf(c22,plain,ra_Px8(X98,skolem0002(X98))|ca_Cx8(X98),inference(split_conjunct,[status(thm)],[c20])).
% 0.46/0.65 cnf(c160,plain,ca_Cx8(X99)|ca_Cx8xcomp(X99),inference(resolution,[status(thm)],[c22, c15])).
% 0.46/0.65 cnf(c164,plain,ca_Cx8(X102)|cb(X102),inference(resolution,[status(thm)],[c160, c7])).
% 0.46/0.65 cnf(c165,plain,ca_Cx8(X103)|ccxcomp(X103),inference(resolution,[status(thm)],[c164, c112])).
% 0.46/0.65 cnf(c6,plain,~ca_Cx8xcomp(X76)|cc(X76),inference(split_conjunct,[status(thm)],[c5])).
% 0.46/0.65 cnf(c163,plain,ca_Cx8(X101)|cc(X101),inference(resolution,[status(thm)],[c160, c6])).
% 0.46/0.65 cnf(c210,plain,ra_Px2(X231,skolem0010(X231))|ca_Cx8(X231),inference(resolution,[status(thm)],[c101, c163])).
% 0.46/0.65 cnf(c319,plain,ca_Cx8(X232)|~ccxcomp(X232),inference(resolution,[status(thm)],[c210, c94])).
% 0.46/0.65 cnf(c325,plain,ca_Cx8(X233),inference(resolution,[status(thm)],[c319, c165])).
% 0.46/0.65 fof(axiom_3,axiom,(![X]:(cUnsatisfiablexcomp(X)<=>((ca_Cx7(X)&ca_Cx8(X))&ca_Cx6(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_3)).
% 0.46/0.65 fof(c130,plain,(![X]:((~cUnsatisfiablexcomp(X)|((ca_Cx7(X)&ca_Cx8(X))&ca_Cx6(X)))&(((~ca_Cx7(X)|~ca_Cx8(X))|~ca_Cx6(X))|cUnsatisfiablexcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 0.46/0.65 fof(c131,plain,((![X]:(~cUnsatisfiablexcomp(X)|((ca_Cx7(X)&ca_Cx8(X))&ca_Cx6(X))))&(![X]:(((~ca_Cx7(X)|~ca_Cx8(X))|~ca_Cx6(X))|cUnsatisfiablexcomp(X)))),inference(shift_quantors,[status(thm)],[c130])).
% 0.46/0.65 fof(c133,plain,(![X64]:(![X65]:((~cUnsatisfiablexcomp(X64)|((ca_Cx7(X64)&ca_Cx8(X64))&ca_Cx6(X64)))&(((~ca_Cx7(X65)|~ca_Cx8(X65))|~ca_Cx6(X65))|cUnsatisfiablexcomp(X65))))),inference(shift_quantors,[status(thm)],[fof(c132,plain,((![X64]:(~cUnsatisfiablexcomp(X64)|((ca_Cx7(X64)&ca_Cx8(X64))&ca_Cx6(X64))))&(![X65]:(((~ca_Cx7(X65)|~ca_Cx8(X65))|~ca_Cx6(X65))|cUnsatisfiablexcomp(X65)))),inference(variable_rename,[status(thm)],[c131])).])).
% 0.46/0.65 fof(c134,plain,(![X64]:(![X65]:((((~cUnsatisfiablexcomp(X64)|ca_Cx7(X64))&(~cUnsatisfiablexcomp(X64)|ca_Cx8(X64)))&(~cUnsatisfiablexcomp(X64)|ca_Cx6(X64)))&(((~ca_Cx7(X65)|~ca_Cx8(X65))|~ca_Cx6(X65))|cUnsatisfiablexcomp(X65))))),inference(distribute,[status(thm)],[c133])).
% 0.46/0.65 cnf(c138,plain,~ca_Cx7(X170)|~ca_Cx8(X170)|~ca_Cx6(X170)|cUnsatisfiablexcomp(X170),inference(split_conjunct,[status(thm)],[c134])).
% 0.46/0.65 cnf(c86,plain,~ca_Cx1(X83)|cbxcomp(X83),inference(split_conjunct,[status(thm)],[c85])).
% 0.46/0.65 fof(axiom_15,axiom,(![X]:(ca_Cx6xcomp(X)<=>(ca(X)&cb(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_15)).
% 0.46/0.65 fof(c52,plain,(![X]:((~ca_Cx6xcomp(X)|(ca(X)&cb(X)))&((~ca(X)|~cb(X))|ca_Cx6xcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_15])).
% 0.46/0.65 fof(c53,plain,((![X]:(~ca_Cx6xcomp(X)|(ca(X)&cb(X))))&(![X]:((~ca(X)|~cb(X))|ca_Cx6xcomp(X)))),inference(shift_quantors,[status(thm)],[c52])).
% 0.46/0.65 fof(c55,plain,(![X26]:(![X27]:((~ca_Cx6xcomp(X26)|(ca(X26)&cb(X26)))&((~ca(X27)|~cb(X27))|ca_Cx6xcomp(X27))))),inference(shift_quantors,[status(thm)],[fof(c54,plain,((![X26]:(~ca_Cx6xcomp(X26)|(ca(X26)&cb(X26))))&(![X27]:((~ca(X27)|~cb(X27))|ca_Cx6xcomp(X27)))),inference(variable_rename,[status(thm)],[c53])).])).
% 0.46/0.65 fof(c56,plain,(![X26]:(![X27]:(((~ca_Cx6xcomp(X26)|ca(X26))&(~ca_Cx6xcomp(X26)|cb(X26)))&((~ca(X27)|~cb(X27))|ca_Cx6xcomp(X27))))),inference(distribute,[status(thm)],[c55])).
% 0.46/0.65 cnf(c57,plain,~ca_Cx6xcomp(X81)|ca(X81),inference(split_conjunct,[status(thm)],[c56])).
% 0.46/0.65 fof(axiom_16,axiom,(![X]:(ca_Cx6xcomp(X)<=>(?[Y0]:ra_Px6(X,Y0)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_16)).
% 0.46/0.65 fof(c45,plain,(![X]:((~ca_Cx6xcomp(X)|(?[Y0]:ra_Px6(X,Y0)))&((![Y0]:~ra_Px6(X,Y0))|ca_Cx6xcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_16])).
% 0.46/0.65 fof(c46,plain,((![X]:(~ca_Cx6xcomp(X)|(?[Y0]:ra_Px6(X,Y0))))&(![X]:((![Y0]:~ra_Px6(X,Y0))|ca_Cx6xcomp(X)))),inference(shift_quantors,[status(thm)],[c45])).
% 0.46/0.65 fof(c47,plain,((![X22]:(~ca_Cx6xcomp(X22)|(?[X23]:ra_Px6(X22,X23))))&(![X24]:((![X25]:~ra_Px6(X24,X25))|ca_Cx6xcomp(X24)))),inference(variable_rename,[status(thm)],[c46])).
% 0.46/0.65 fof(c49,plain,(![X22]:(![X24]:(![X25]:((~ca_Cx6xcomp(X22)|ra_Px6(X22,skolem0005(X22)))&(~ra_Px6(X24,X25)|ca_Cx6xcomp(X24)))))),inference(shift_quantors,[status(thm)],[fof(c48,plain,((![X22]:(~ca_Cx6xcomp(X22)|ra_Px6(X22,skolem0005(X22))))&(![X24]:((![X25]:~ra_Px6(X24,X25))|ca_Cx6xcomp(X24)))),inference(skolemize,[status(esa)],[c47])).])).
% 0.46/0.65 cnf(c51,plain,~ra_Px6(X108,X109)|ca_Cx6xcomp(X108),inference(split_conjunct,[status(thm)],[c49])).
% 0.46/0.65 fof(axiom_14,axiom,(![X]:(ca_Cx6(X)<=>(~(?[Y]:ra_Px6(X,Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_14)).
% 0.46/0.65 fof(c60,plain,(![X]:((~ca_Cx6(X)|(![Y]:~ra_Px6(X,Y)))&((?[Y]:ra_Px6(X,Y))|ca_Cx6(X)))),inference(fof_nnf,[status(thm)],[axiom_14])).
% 0.46/0.65 fof(c61,plain,((![X]:(~ca_Cx6(X)|(![Y]:~ra_Px6(X,Y))))&(![X]:((?[Y]:ra_Px6(X,Y))|ca_Cx6(X)))),inference(shift_quantors,[status(thm)],[c60])).
% 0.46/0.65 fof(c62,plain,((![X28]:(~ca_Cx6(X28)|(![X29]:~ra_Px6(X28,X29))))&(![X30]:((?[X31]:ra_Px6(X30,X31))|ca_Cx6(X30)))),inference(variable_rename,[status(thm)],[c61])).
% 0.46/0.65 fof(c64,plain,(![X28]:(![X29]:(![X30]:((~ca_Cx6(X28)|~ra_Px6(X28,X29))&(ra_Px6(X30,skolem0006(X30))|ca_Cx6(X30)))))),inference(shift_quantors,[status(thm)],[fof(c63,plain,((![X28]:(~ca_Cx6(X28)|(![X29]:~ra_Px6(X28,X29))))&(![X30]:(ra_Px6(X30,skolem0006(X30))|ca_Cx6(X30)))),inference(skolemize,[status(esa)],[c62])).])).
% 0.46/0.65 cnf(c66,plain,ra_Px6(X140,skolem0006(X140))|ca_Cx6(X140),inference(split_conjunct,[status(thm)],[c64])).
% 0.46/0.65 cnf(c184,plain,ca_Cx6(X141)|ca_Cx6xcomp(X141),inference(resolution,[status(thm)],[c66, c51])).
% 0.46/0.65 cnf(c186,plain,ca_Cx6(X143)|ca(X143),inference(resolution,[status(thm)],[c184, c57])).
% 0.46/0.65 cnf(c189,plain,ca_Cx6(X145)|ca_Cx1(X145),inference(resolution,[status(thm)],[c186, c122])).
% 0.46/0.65 cnf(c194,plain,ca_Cx6(X148)|cbxcomp(X148),inference(resolution,[status(thm)],[c189, c86])).
% 0.46/0.65 fof(axiom_8,axiom,(![X]:(cbxcomp(X)<=>(~(?[Y]:ra_Px3(X,Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_8)).
% 0.46/0.65 fof(c103,plain,(![X]:((~cbxcomp(X)|(![Y]:~ra_Px3(X,Y)))&((?[Y]:ra_Px3(X,Y))|cbxcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_8])).
% 0.46/0.65 fof(c104,plain,((![X]:(~cbxcomp(X)|(![Y]:~ra_Px3(X,Y))))&(![X]:((?[Y]:ra_Px3(X,Y))|cbxcomp(X)))),inference(shift_quantors,[status(thm)],[c103])).
% 0.46/0.65 fof(c105,plain,((![X50]:(~cbxcomp(X50)|(![X51]:~ra_Px3(X50,X51))))&(![X52]:((?[X53]:ra_Px3(X52,X53))|cbxcomp(X52)))),inference(variable_rename,[status(thm)],[c104])).
% 0.46/0.65 fof(c107,plain,(![X50]:(![X51]:(![X52]:((~cbxcomp(X50)|~ra_Px3(X50,X51))&(ra_Px3(X52,skolem0011(X52))|cbxcomp(X52)))))),inference(shift_quantors,[status(thm)],[fof(c106,plain,((![X50]:(~cbxcomp(X50)|(![X51]:~ra_Px3(X50,X51))))&(![X52]:(ra_Px3(X52,skolem0011(X52))|cbxcomp(X52)))),inference(skolemize,[status(esa)],[c105])).])).
% 0.46/0.65 cnf(c108,plain,~cbxcomp(X130)|~ra_Px3(X130,X129),inference(split_conjunct,[status(thm)],[c107])).
% 0.46/0.65 cnf(c58,plain,~ca_Cx6xcomp(X82)|cb(X82),inference(split_conjunct,[status(thm)],[c56])).
% 0.46/0.65 cnf(c187,plain,ca_Cx6(X144)|cb(X144),inference(resolution,[status(thm)],[c184, c58])).
% 0.46/0.65 fof(axiom_6,axiom,(![X]:(cb(X)<=>(?[Y0]:ra_Px3(X,Y0)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_6)).
% 0.46/0.65 fof(c113,plain,(![X]:((~cb(X)|(?[Y0]:ra_Px3(X,Y0)))&((![Y0]:~ra_Px3(X,Y0))|cb(X)))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 0.46/0.65 fof(c114,plain,((![X]:(~cb(X)|(?[Y0]:ra_Px3(X,Y0))))&(![X]:((![Y0]:~ra_Px3(X,Y0))|cb(X)))),inference(shift_quantors,[status(thm)],[c113])).
% 0.46/0.65 fof(c115,plain,((![X55]:(~cb(X55)|(?[X56]:ra_Px3(X55,X56))))&(![X57]:((![X58]:~ra_Px3(X57,X58))|cb(X57)))),inference(variable_rename,[status(thm)],[c114])).
% 0.46/0.65 fof(c117,plain,(![X55]:(![X57]:(![X58]:((~cb(X55)|ra_Px3(X55,skolem0012(X55)))&(~ra_Px3(X57,X58)|cb(X57)))))),inference(shift_quantors,[status(thm)],[fof(c116,plain,((![X55]:(~cb(X55)|ra_Px3(X55,skolem0012(X55))))&(![X57]:((![X58]:~ra_Px3(X57,X58))|cb(X57)))),inference(skolemize,[status(esa)],[c115])).])).
% 0.46/0.65 cnf(c118,plain,~cb(X164)|ra_Px3(X164,skolem0012(X164)),inference(split_conjunct,[status(thm)],[c117])).
% 0.46/0.65 cnf(c222,plain,ra_Px3(X263,skolem0012(X263))|ca_Cx6(X263),inference(resolution,[status(thm)],[c118, c187])).
% 0.46/0.65 cnf(c367,plain,ca_Cx6(X265)|~cbxcomp(X265),inference(resolution,[status(thm)],[c222, c108])).
% 0.46/0.65 cnf(c372,plain,ca_Cx6(X267),inference(resolution,[status(thm)],[c367, c194])).
% 0.46/0.65 cnf(c377,plain,~ca_Cx7(X325)|~ca_Cx8(X325)|cUnsatisfiablexcomp(X325),inference(resolution,[status(thm)],[c372, c138])).
% 0.46/0.65 cnf(c394,plain,~ca_Cx7(X327)|cUnsatisfiablexcomp(X327),inference(resolution,[status(thm)],[c377, c325])).
% 0.46/0.65 cnf(c395,plain,cUnsatisfiablexcomp(X328),inference(resolution,[status(thm)],[c394, c348])).
% 0.46/0.65 cnf(c396,plain,ra_Px5(X329,skolem0013(X329)),inference(resolution,[status(thm)],[c395, c128])).
% 0.46/0.65 cnf(c397,plain,~cUnsatisfiable(X330),inference(resolution,[status(thm)],[c396, c144])).
% 0.46/0.65 cnf(c398,plain,$false,inference(resolution,[status(thm)],[c397, c0])).
% 0.46/0.65 % SZS output end CNFRefutation
% 0.46/0.65
% 0.46/0.65 % Initial clauses : 51
% 0.46/0.65 % Processed clauses : 131
% 0.46/0.65 % Factors computed : 0
% 0.46/0.65 % Resolvents computed: 241
% 0.46/0.65 % Tautologies deleted: 16
% 0.46/0.65 % Forward subsumed : 97
% 0.46/0.65 % Backward subsumed : 72
% 0.46/0.65 % -------- CPU Time ---------
% 0.46/0.65 % User time : 0.278 s
% 0.46/0.65 % System time : 0.019 s
% 0.46/0.65 % Total time : 0.297 s
%------------------------------------------------------------------------------