%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS108+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n002.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:43 EDT 2024
% Result : Unsatisfiable 1.98s 2.20s
% Output : Refutation 1.98s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : KRS108+1 : TPTP v8.1.2. Released v3.1.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n002.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:10:08 EDT 2024
% 0.14/0.36 % CPUTime :
% 1.98/2.20 % Version: 1.5
% 1.98/2.20 % SZS status Unsatisfiable
% 1.98/2.20 % SZS output start CNFRefutation
% 1.98/2.20 fof(axiom_16,axiom,(![X]:(ca_Cx1(X)<=>(((cp2xcomp(X)&cp5xcomp(X))&cp3xcomp(X))&cp4xcomp(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_16)).
% 1.98/2.20 fof(c96,plain,(![X]:((~ca_Cx1(X)|(((cp2xcomp(X)&cp5xcomp(X))&cp3xcomp(X))&cp4xcomp(X)))&((((~cp2xcomp(X)|~cp5xcomp(X))|~cp3xcomp(X))|~cp4xcomp(X))|ca_Cx1(X)))),inference(fof_nnf,[status(thm)],[axiom_16])).
% 1.98/2.20 fof(c97,plain,((![X]:(~ca_Cx1(X)|(((cp2xcomp(X)&cp5xcomp(X))&cp3xcomp(X))&cp4xcomp(X))))&(![X]:((((~cp2xcomp(X)|~cp5xcomp(X))|~cp3xcomp(X))|~cp4xcomp(X))|ca_Cx1(X)))),inference(shift_quantors,[status(thm)],[c96])).
% 1.98/2.20 fof(c99,plain,(![X34]:(![X35]:((~ca_Cx1(X34)|(((cp2xcomp(X34)&cp5xcomp(X34))&cp3xcomp(X34))&cp4xcomp(X34)))&((((~cp2xcomp(X35)|~cp5xcomp(X35))|~cp3xcomp(X35))|~cp4xcomp(X35))|ca_Cx1(X35))))),inference(shift_quantors,[status(thm)],[fof(c98,plain,((![X34]:(~ca_Cx1(X34)|(((cp2xcomp(X34)&cp5xcomp(X34))&cp3xcomp(X34))&cp4xcomp(X34))))&(![X35]:((((~cp2xcomp(X35)|~cp5xcomp(X35))|~cp3xcomp(X35))|~cp4xcomp(X35))|ca_Cx1(X35)))),inference(variable_rename,[status(thm)],[c97])).])).
% 1.98/2.20 fof(c100,plain,(![X34]:(![X35]:(((((~ca_Cx1(X34)|cp2xcomp(X34))&(~ca_Cx1(X34)|cp5xcomp(X34)))&(~ca_Cx1(X34)|cp3xcomp(X34)))&(~ca_Cx1(X34)|cp4xcomp(X34)))&((((~cp2xcomp(X35)|~cp5xcomp(X35))|~cp3xcomp(X35))|~cp4xcomp(X35))|ca_Cx1(X35))))),inference(distribute,[status(thm)],[c99])).
% 1.98/2.20 cnf(c101,plain,~ca_Cx1(X198)|cp2xcomp(X198),inference(split_conjunct,[status(thm)],[c100])).
% 1.98/2.20 fof(axiom_17,axiom,(![X]:(ca_Cx1(X)<=>(?[Y0]:ra_Px1(X,Y0)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_17)).
% 1.98/2.20 fof(c89,plain,(![X]:((~ca_Cx1(X)|(?[Y0]:ra_Px1(X,Y0)))&((![Y0]:~ra_Px1(X,Y0))|ca_Cx1(X)))),inference(fof_nnf,[status(thm)],[axiom_17])).
% 1.98/2.20 fof(c90,plain,((![X]:(~ca_Cx1(X)|(?[Y0]:ra_Px1(X,Y0))))&(![X]:((![Y0]:~ra_Px1(X,Y0))|ca_Cx1(X)))),inference(shift_quantors,[status(thm)],[c89])).
% 1.98/2.20 fof(c91,plain,((![X30]:(~ca_Cx1(X30)|(?[X31]:ra_Px1(X30,X31))))&(![X32]:((![X33]:~ra_Px1(X32,X33))|ca_Cx1(X32)))),inference(variable_rename,[status(thm)],[c90])).
% 1.98/2.20 fof(c93,plain,(![X30]:(![X32]:(![X33]:((~ca_Cx1(X30)|ra_Px1(X30,skolem0006(X30)))&(~ra_Px1(X32,X33)|ca_Cx1(X32)))))),inference(shift_quantors,[status(thm)],[fof(c92,plain,((![X30]:(~ca_Cx1(X30)|ra_Px1(X30,skolem0006(X30))))&(![X32]:((![X33]:~ra_Px1(X32,X33))|ca_Cx1(X32)))),inference(skolemize,[status(esa)],[c91])).])).
% 1.98/2.20 cnf(c95,plain,~ra_Px1(X236,X235)|ca_Cx1(X236),inference(split_conjunct,[status(thm)],[c93])).
% 1.98/2.20 fof(axiom_18,axiom,(![X]:(ca_Cx1xcomp(X)<=>(~(?[Y]:ra_Px1(X,Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_18)).
% 1.98/2.20 fof(c82,plain,(![X]:((~ca_Cx1xcomp(X)|(![Y]:~ra_Px1(X,Y)))&((?[Y]:ra_Px1(X,Y))|ca_Cx1xcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_18])).
% 1.98/2.20 fof(c83,plain,((![X]:(~ca_Cx1xcomp(X)|(![Y]:~ra_Px1(X,Y))))&(![X]:((?[Y]:ra_Px1(X,Y))|ca_Cx1xcomp(X)))),inference(shift_quantors,[status(thm)],[c82])).
% 1.98/2.20 fof(c84,plain,((![X26]:(~ca_Cx1xcomp(X26)|(![X27]:~ra_Px1(X26,X27))))&(![X28]:((?[X29]:ra_Px1(X28,X29))|ca_Cx1xcomp(X28)))),inference(variable_rename,[status(thm)],[c83])).
% 1.98/2.20 fof(c86,plain,(![X26]:(![X27]:(![X28]:((~ca_Cx1xcomp(X26)|~ra_Px1(X26,X27))&(ra_Px1(X28,skolem0005(X28))|ca_Cx1xcomp(X28)))))),inference(shift_quantors,[status(thm)],[fof(c85,plain,((![X26]:(~ca_Cx1xcomp(X26)|(![X27]:~ra_Px1(X26,X27))))&(![X28]:(ra_Px1(X28,skolem0005(X28))|ca_Cx1xcomp(X28)))),inference(skolemize,[status(esa)],[c84])).])).
% 1.98/2.20 cnf(c88,plain,ra_Px1(X301,skolem0005(X301))|ca_Cx1xcomp(X301),inference(split_conjunct,[status(thm)],[c86])).
% 1.98/2.20 cnf(c383,plain,ca_Cx1xcomp(X305)|ca_Cx1(X305),inference(resolution,[status(thm)],[c88, c95])).
% 1.98/2.20 cnf(c388,plain,ca_Cx1xcomp(X312)|cp2xcomp(X312),inference(resolution,[status(thm)],[c383, c101])).
% 1.98/2.20 fof(axiom_6,axiom,(![X]:(cp2xcomp(X)<=>(~(?[Y]:ra_Px5(X,Y))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_6)).
% 1.98/2.20 fof(c166,plain,(![X]:((~cp2xcomp(X)|(![Y]:~ra_Px5(X,Y)))&((?[Y]:ra_Px5(X,Y))|cp2xcomp(X)))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 1.98/2.20 fof(c167,plain,((![X]:(~cp2xcomp(X)|(![Y]:~ra_Px5(X,Y))))&(![X]:((?[Y]:ra_Px5(X,Y))|cp2xcomp(X)))),inference(shift_quantors,[status(thm)],[c166])).
% 1.98/2.20 fof(c168,plain,((![X70]:(~cp2xcomp(X70)|(![X71]:~ra_Px5(X70,X71))))&(![X72]:((?[X73]:ra_Px5(X72,X73))|cp2xcomp(X72)))),inference(variable_rename,[status(thm)],[c167])).
% 1.98/2.20 fof(c170,plain,(![X70]:(![X71]:(![X72]:((~cp2xcomp(X70)|~ra_Px5(X70,X71))&(ra_Px5(X72,skolem0016(X72))|cp2xcomp(X72)))))),inference(shift_quantors,[status(thm)],[fof(c169,plain,((![X70]:(~cp2xcomp(X70)|(![X71]:~ra_Px5(X70,X71))))&(![X72]:(ra_Px5(X72,skolem0016(X72))|cp2xcomp(X72)))),inference(skolemize,[status(esa)],[c168])).])).
% 1.98/2.20 cnf(c171,plain,~cp2xcomp(X256)|~ra_Px5(X256,X255),inference(split_conjunct,[status(thm)],[c170])).
% 1.98/2.20 fof(axiom_26,axiom,cUnsatisfiable(i2003_11_14_17_21_04740),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_26)).
% 1.98/2.20 cnf(c30,plain,cUnsatisfiable(i2003_11_14_17_21_04740),inference(split_conjunct,[status(thm)],[axiom_26])).
% 1.98/2.20 fof(axiom_2,axiom,(![X]:(cUnsatisfiable(X)<=>((?[Y]:(rinvR(X,Y)&ca_Ax14(Y)))&cp2(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_2)).
% 1.98/2.21 fof(c186,plain,(![X]:((~cUnsatisfiable(X)|((?[Y]:(rinvR(X,Y)&ca_Ax14(Y)))&cp2(X)))&(((![Y]:(~rinvR(X,Y)|~ca_Ax14(Y)))|~cp2(X))|cUnsatisfiable(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 1.98/2.21 fof(c187,plain,((![X]:(~cUnsatisfiable(X)|((?[Y]:(rinvR(X,Y)&ca_Ax14(Y)))&cp2(X))))&(![X]:(((![Y]:(~rinvR(X,Y)|~ca_Ax14(Y)))|~cp2(X))|cUnsatisfiable(X)))),inference(shift_quantors,[status(thm)],[c186])).
% 1.98/2.21 fof(c188,plain,((![X80]:(~cUnsatisfiable(X80)|((?[X81]:(rinvR(X80,X81)&ca_Ax14(X81)))&cp2(X80))))&(![X82]:(((![X83]:(~rinvR(X82,X83)|~ca_Ax14(X83)))|~cp2(X82))|cUnsatisfiable(X82)))),inference(variable_rename,[status(thm)],[c187])).
% 1.98/2.21 fof(c190,plain,(![X80]:(![X82]:(![X83]:((~cUnsatisfiable(X80)|((rinvR(X80,skolem0018(X80))&ca_Ax14(skolem0018(X80)))&cp2(X80)))&(((~rinvR(X82,X83)|~ca_Ax14(X83))|~cp2(X82))|cUnsatisfiable(X82)))))),inference(shift_quantors,[status(thm)],[fof(c189,plain,((![X80]:(~cUnsatisfiable(X80)|((rinvR(X80,skolem0018(X80))&ca_Ax14(skolem0018(X80)))&cp2(X80))))&(![X82]:(((![X83]:(~rinvR(X82,X83)|~ca_Ax14(X83)))|~cp2(X82))|cUnsatisfiable(X82)))),inference(skolemize,[status(esa)],[c188])).])).
% 1.98/2.21 fof(c191,plain,(![X80]:(![X82]:(![X83]:((((~cUnsatisfiable(X80)|rinvR(X80,skolem0018(X80)))&(~cUnsatisfiable(X80)|ca_Ax14(skolem0018(X80))))&(~cUnsatisfiable(X80)|cp2(X80)))&(((~rinvR(X82,X83)|~ca_Ax14(X83))|~cp2(X82))|cUnsatisfiable(X82)))))),inference(distribute,[status(thm)],[c190])).
% 1.98/2.21 cnf(c194,plain,~cUnsatisfiable(X208)|cp2(X208),inference(split_conjunct,[status(thm)],[c191])).
% 1.98/2.21 cnf(c330,plain,cp2(i2003_11_14_17_21_04740),inference(resolution,[status(thm)],[c194, c30])).
% 1.98/2.21 fof(axiom_4,axiom,(![X]:(cp2(X)<=>(?[Y0]:ra_Px5(X,Y0)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_4)).
% 1.98/2.21 fof(c176,plain,(![X]:((~cp2(X)|(?[Y0]:ra_Px5(X,Y0)))&((![Y0]:~ra_Px5(X,Y0))|cp2(X)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 1.98/2.21 fof(c177,plain,((![X]:(~cp2(X)|(?[Y0]:ra_Px5(X,Y0))))&(![X]:((![Y0]:~ra_Px5(X,Y0))|cp2(X)))),inference(shift_quantors,[status(thm)],[c176])).
% 1.98/2.21 fof(c178,plain,((![X75]:(~cp2(X75)|(?[X76]:ra_Px5(X75,X76))))&(![X77]:((![X78]:~ra_Px5(X77,X78))|cp2(X77)))),inference(variable_rename,[status(thm)],[c177])).
% 1.98/2.21 fof(c180,plain,(![X75]:(![X77]:(![X78]:((~cp2(X75)|ra_Px5(X75,skolem0017(X75)))&(~ra_Px5(X77,X78)|cp2(X77)))))),inference(shift_quantors,[status(thm)],[fof(c179,plain,((![X75]:(~cp2(X75)|ra_Px5(X75,skolem0017(X75))))&(![X77]:((![X78]:~ra_Px5(X77,X78))|cp2(X77)))),inference(skolemize,[status(esa)],[c178])).])).
% 1.98/2.21 cnf(c181,plain,~cp2(X372)|ra_Px5(X372,skolem0017(X372)),inference(split_conjunct,[status(thm)],[c180])).
% 1.98/2.21 cnf(c458,plain,ra_Px5(i2003_11_14_17_21_04740,skolem0017(i2003_11_14_17_21_04740)),inference(resolution,[status(thm)],[c181, c330])).
% 1.98/2.21 cnf(c461,plain,~cp2xcomp(i2003_11_14_17_21_04740),inference(resolution,[status(thm)],[c458, c171])).
% 1.98/2.21 cnf(c462,plain,ca_Cx1xcomp(i2003_11_14_17_21_04740),inference(resolution,[status(thm)],[c461, c388])).
% 1.98/2.21 cnf(c87,plain,~ca_Cx1xcomp(X234)|~ra_Px1(X234,X233),inference(split_conjunct,[status(thm)],[c86])).
% 1.98/2.21 fof(ra_Px1_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&ra_Px1(A,C))=>ra_Px1(B,C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', ra_Px1_substitution_1)).
% 1.98/2.21 fof(c266,plain,(![A]:(![B]:(![C]:((A!=B|~ra_Px1(A,C))|ra_Px1(B,C))))),inference(fof_nnf,[status(thm)],[ra_Px1_substitution_1])).
% 1.98/2.21 fof(c267,plain,(![X143]:(![X144]:(![X145]:((X143!=X144|~ra_Px1(X143,X145))|ra_Px1(X144,X145))))),inference(variable_rename,[status(thm)],[c266])).
% 1.98/2.21 cnf(c268,plain,X590!=X592|~ra_Px1(X590,X591)|ra_Px1(X592,X591),inference(split_conjunct,[status(thm)],[c267])).
% 1.98/2.21 fof(axiom_3,axiom,(![X]:(cp1(X)=>ca_Cx1(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_3)).
% 1.98/2.21 fof(c183,plain,(![X]:(~cp1(X)|ca_Cx1(X))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 1.98/2.21 fof(c184,plain,(![X79]:(~cp1(X79)|ca_Cx1(X79))),inference(variable_rename,[status(thm)],[c183])).
% 1.98/2.21 cnf(c185,plain,~cp1(X207)|ca_Cx1(X207),inference(split_conjunct,[status(thm)],[c184])).
% 1.98/2.21 fof(axiom_15,axiom,(![X]:(ca_Ax14(X)<=>((?[Y]:(rr(X,Y)&cp1(Y)))&(![Y0]:(![Y1]:((rr(X,Y0)&rr(X,Y1))=>Y0=Y1)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_15)).
% 1.98/2.21 fof(c106,plain,(![X]:((~ca_Ax14(X)|((?[Y]:(rr(X,Y)&cp1(Y)))&(![Y0]:(![Y1]:((~rr(X,Y0)|~rr(X,Y1))|Y0=Y1)))))&(((![Y]:(~rr(X,Y)|~cp1(Y)))|(?[Y0]:(?[Y1]:((rr(X,Y0)&rr(X,Y1))&Y0!=Y1))))|ca_Ax14(X)))),inference(fof_nnf,[status(thm)],[axiom_15])).
% 1.98/2.21 fof(c107,plain,((![X]:(~ca_Ax14(X)|((?[Y]:(rr(X,Y)&cp1(Y)))&(![Y0]:(![Y1]:((~rr(X,Y0)|~rr(X,Y1))|Y0=Y1))))))&(![X]:(((![Y]:(~rr(X,Y)|~cp1(Y)))|(?[Y0]:(?[Y1]:((rr(X,Y0)&rr(X,Y1))&Y0!=Y1))))|ca_Ax14(X)))),inference(shift_quantors,[status(thm)],[c106])).
% 1.98/2.21 fof(c108,plain,((![X36]:(~ca_Ax14(X36)|((?[X37]:(rr(X36,X37)&cp1(X37)))&(![X38]:(![X39]:((~rr(X36,X38)|~rr(X36,X39))|X38=X39))))))&(![X40]:(((![X41]:(~rr(X40,X41)|~cp1(X41)))|(?[X42]:(?[X43]:((rr(X40,X42)&rr(X40,X43))&X42!=X43))))|ca_Ax14(X40)))),inference(variable_rename,[status(thm)],[c107])).
% 1.98/2.21 fof(c110,plain,(![X36]:(![X38]:(![X39]:(![X40]:(![X41]:((~ca_Ax14(X36)|((rr(X36,skolem0007(X36))&cp1(skolem0007(X36)))&((~rr(X36,X38)|~rr(X36,X39))|X38=X39)))&(((~rr(X40,X41)|~cp1(X41))|((rr(X40,skolem0008(X40))&rr(X40,skolem0009(X40)))&skolem0008(X40)!=skolem0009(X40)))|ca_Ax14(X40)))))))),inference(shift_quantors,[status(thm)],[fof(c109,plain,((![X36]:(~ca_Ax14(X36)|((rr(X36,skolem0007(X36))&cp1(skolem0007(X36)))&(![X38]:(![X39]:((~rr(X36,X38)|~rr(X36,X39))|X38=X39))))))&(![X40]:(((![X41]:(~rr(X40,X41)|~cp1(X41)))|((rr(X40,skolem0008(X40))&rr(X40,skolem0009(X40)))&skolem0008(X40)!=skolem0009(X40)))|ca_Ax14(X40)))),inference(skolemize,[status(esa)],[c108])).])).
% 1.98/2.21 fof(c111,plain,(![X36]:(![X38]:(![X39]:(![X40]:(![X41]:((((~ca_Ax14(X36)|rr(X36,skolem0007(X36)))&(~ca_Ax14(X36)|cp1(skolem0007(X36))))&(~ca_Ax14(X36)|((~rr(X36,X38)|~rr(X36,X39))|X38=X39)))&(((((~rr(X40,X41)|~cp1(X41))|rr(X40,skolem0008(X40)))|ca_Ax14(X40))&(((~rr(X40,X41)|~cp1(X41))|rr(X40,skolem0009(X40)))|ca_Ax14(X40)))&(((~rr(X40,X41)|~cp1(X41))|skolem0008(X40)!=skolem0009(X40))|ca_Ax14(X40))))))))),inference(distribute,[status(thm)],[c110])).
% 1.98/2.21 cnf(c113,plain,~ca_Ax14(X266)|cp1(skolem0007(X266)),inference(split_conjunct,[status(thm)],[c111])).
% 1.98/2.21 cnf(c193,plain,~cUnsatisfiable(X267)|ca_Ax14(skolem0018(X267)),inference(split_conjunct,[status(thm)],[c191])).
% 1.98/2.21 cnf(c343,plain,ca_Ax14(skolem0018(i2003_11_14_17_21_04740)),inference(resolution,[status(thm)],[c193, c30])).
% 1.98/2.21 cnf(c344,plain,cp1(skolem0007(skolem0018(i2003_11_14_17_21_04740))),inference(resolution,[status(thm)],[c343, c113])).
% 1.98/2.21 cnf(c345,plain,ca_Cx1(skolem0007(skolem0018(i2003_11_14_17_21_04740))),inference(resolution,[status(thm)],[c344, c185])).
% 1.98/2.21 cnf(c94,plain,~ca_Cx1(X314)|ra_Px1(X314,skolem0006(X314)),inference(split_conjunct,[status(thm)],[c93])).
% 1.98/2.21 cnf(c391,plain,ra_Px1(skolem0007(skolem0018(i2003_11_14_17_21_04740)),skolem0006(skolem0007(skolem0018(i2003_11_14_17_21_04740)))),inference(resolution,[status(thm)],[c94, c345])).
% 1.98/2.21 cnf(c958,plain,skolem0007(skolem0018(i2003_11_14_17_21_04740))!=X1925|ra_Px1(X1925,skolem0006(skolem0007(skolem0018(i2003_11_14_17_21_04740)))),inference(resolution,[status(thm)],[c391, c268])).
% 1.98/2.21 cnf(c112,plain,~ca_Ax14(X315)|rr(X315,skolem0007(X315)),inference(split_conjunct,[status(thm)],[c111])).
% 1.98/2.21 cnf(c393,plain,rr(skolem0018(i2003_11_14_17_21_04740),skolem0007(skolem0018(i2003_11_14_17_21_04740))),inference(resolution,[status(thm)],[c112, c343])).
% 1.98/2.21 fof(axiom_25,axiom,(![X]:(![Y]:(rinvR(X,Y)<=>rr(Y,X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_25)).
% 1.98/2.21 fof(c31,plain,(![X]:(![Y]:((~rinvR(X,Y)|rr(Y,X))&(~rr(Y,X)|rinvR(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_25])).
% 1.98/2.21 fof(c32,plain,((![X]:(![Y]:(~rinvR(X,Y)|rr(Y,X))))&(![X]:(![Y]:(~rr(Y,X)|rinvR(X,Y))))),inference(shift_quantors,[status(thm)],[c31])).
% 1.98/2.21 fof(c34,plain,(![X2]:(![X3]:(![X4]:(![X5]:((~rinvR(X2,X3)|rr(X3,X2))&(~rr(X5,X4)|rinvR(X4,X5))))))),inference(shift_quantors,[status(thm)],[fof(c33,plain,((![X2]:(![X3]:(~rinvR(X2,X3)|rr(X3,X2))))&(![X4]:(![X5]:(~rr(X5,X4)|rinvR(X4,X5))))),inference(variable_rename,[status(thm)],[c32])).])).
% 1.98/2.21 cnf(c35,plain,~rinvR(X259,X260)|rr(X260,X259),inference(split_conjunct,[status(thm)],[c34])).
% 1.98/2.21 cnf(c192,plain,~cUnsatisfiable(X381)|rinvR(X381,skolem0018(X381)),inference(split_conjunct,[status(thm)],[c191])).
% 1.98/2.21 cnf(c475,plain,rinvR(i2003_11_14_17_21_04740,skolem0018(i2003_11_14_17_21_04740)),inference(resolution,[status(thm)],[c192, c30])).
% 1.98/2.21 cnf(c476,plain,rr(skolem0018(i2003_11_14_17_21_04740),i2003_11_14_17_21_04740),inference(resolution,[status(thm)],[c475, c35])).
% 1.98/2.21 cnf(c114,plain,~ca_Ax14(X416)|~rr(X416,X417)|~rr(X416,X415)|X417=X415,inference(split_conjunct,[status(thm)],[c111])).
% 1.98/2.21 cnf(c538,plain,~ca_Ax14(skolem0018(i2003_11_14_17_21_04740))|~rr(skolem0018(i2003_11_14_17_21_04740),X956)|X956=i2003_11_14_17_21_04740,inference(resolution,[status(thm)],[c114, c476])).
% 1.98/2.21 cnf(c1472,plain,~ca_Ax14(skolem0018(i2003_11_14_17_21_04740))|skolem0007(skolem0018(i2003_11_14_17_21_04740))=i2003_11_14_17_21_04740,inference(resolution,[status(thm)],[c538, c393])).
% 1.98/2.21 cnf(c3230,plain,skolem0007(skolem0018(i2003_11_14_17_21_04740))=i2003_11_14_17_21_04740,inference(resolution,[status(thm)],[c1472, c343])).
% 1.98/2.21 cnf(c3241,plain,ra_Px1(i2003_11_14_17_21_04740,skolem0006(skolem0007(skolem0018(i2003_11_14_17_21_04740)))),inference(resolution,[status(thm)],[c3230, c958])).
% 1.98/2.21 cnf(c3472,plain,~ca_Cx1xcomp(i2003_11_14_17_21_04740),inference(resolution,[status(thm)],[c3241, c87])).
% 1.98/2.21 cnf(c3486,plain,$false,inference(resolution,[status(thm)],[c3472, c462])).
% 1.98/2.21 % SZS output end CNFRefutation
% 1.98/2.21
% 1.98/2.21 % Initial clauses : 133
% 1.98/2.21 % Processed clauses : 652
% 1.98/2.21 % Factors computed : 2
% 1.98/2.21 % Resolvents computed: 3164
% 1.98/2.21 % Tautologies deleted: 62
% 1.98/2.21 % Forward subsumed : 1620
% 1.98/2.21 % Backward subsumed : 25
% 1.98/2.21 % -------- CPU Time ---------
% 1.98/2.21 % User time : 1.826 s
% 1.98/2.21 % System time : 0.020 s
% 1.98/2.21 % Total time : 1.846 s
%------------------------------------------------------------------------------