%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : KRS052+1 : TPTP v8.1.2. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n015.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:34 EDT 2024
% Result : Satisfiable 7.49s 7.65s
% Output : Saturation 7.49s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : KRS052+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 : n015.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:07:38 EDT 2024
% 0.14/0.36 % CPUTime :
% 7.49/7.65 % Version: 1.5
% 7.49/7.65 % SZS status Satisfiable
% 7.49/7.65 % SZS output start Saturation
% 7.49/7.65 fof(axiom_6,axiom,(![X]:(cinfinite(X)<=>((?[Y0]:(?[Y1]:(?[Y2]:(?[Y3]:(?[Y4]:((((((((((((((rinvR_N_times_M_to_1(X,Y0)&rinvR_N_times_M_to_1(X,Y1))&rinvR_N_times_M_to_1(X,Y2))&rinvR_N_times_M_to_1(X,Y3))&rinvR_N_times_M_to_1(X,Y4))&Y0!=Y1)&Y0!=Y2)&Y0!=Y3)&Y0!=Y4)&Y1!=Y2)&Y1!=Y3)&Y1!=Y4)&Y2!=Y3)&Y2!=Y4)&Y3!=Y4))))))&(![Y0]:(![Y1]:(![Y2]:(![Y3]:(![Y4]:(![Y5]:((((((rinvR_N_times_M_to_1(X,Y0)&rinvR_N_times_M_to_1(X,Y1))&rinvR_N_times_M_to_1(X,Y2))&rinvR_N_times_M_to_1(X,Y3))&rinvR_N_times_M_to_1(X,Y4))&rinvR_N_times_M_to_1(X,Y5))=>((((((((((((((Y0=Y1|Y0=Y2)|Y0=Y3)|Y0=Y4)|Y0=Y5)|Y1=Y2)|Y1=Y3)|Y1=Y4)|Y1=Y5)|Y2=Y3)|Y2=Y4)|Y2=Y5)|Y3=Y4)|Y3=Y5)|Y4=Y5))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_6)).
% 7.49/7.65 fof(c80,plain,(![X]:((~cinfinite(X)|((?[Y0]:(?[Y1]:(?[Y2]:(?[Y3]:(?[Y4]:((((((((((((((rinvR_N_times_M_to_1(X,Y0)&rinvR_N_times_M_to_1(X,Y1))&rinvR_N_times_M_to_1(X,Y2))&rinvR_N_times_M_to_1(X,Y3))&rinvR_N_times_M_to_1(X,Y4))&Y0!=Y1)&Y0!=Y2)&Y0!=Y3)&Y0!=Y4)&Y1!=Y2)&Y1!=Y3)&Y1!=Y4)&Y2!=Y3)&Y2!=Y4)&Y3!=Y4))))))&(![Y0]:(![Y1]:(![Y2]:(![Y3]:(![Y4]:(![Y5]:((((((~rinvR_N_times_M_to_1(X,Y0)|~rinvR_N_times_M_to_1(X,Y1))|~rinvR_N_times_M_to_1(X,Y2))|~rinvR_N_times_M_to_1(X,Y3))|~rinvR_N_times_M_to_1(X,Y4))|~rinvR_N_times_M_to_1(X,Y5))|((((((((((((((Y0=Y1|Y0=Y2)|Y0=Y3)|Y0=Y4)|Y0=Y5)|Y1=Y2)|Y1=Y3)|Y1=Y4)|Y1=Y5)|Y2=Y3)|Y2=Y4)|Y2=Y5)|Y3=Y4)|Y3=Y5)|Y4=Y5))))))))))&(((![Y0]:(![Y1]:(![Y2]:(![Y3]:(![Y4]:((((((((((((((~rinvR_N_times_M_to_1(X,Y0)|~rinvR_N_times_M_to_1(X,Y1))|~rinvR_N_times_M_to_1(X,Y2))|~rinvR_N_times_M_to_1(X,Y3))|~rinvR_N_times_M_to_1(X,Y4))|Y0=Y1)|Y0=Y2)|Y0=Y3)|Y0=Y4)|Y1=Y2)|Y1=Y3)|Y1=Y4)|Y2=Y3)|Y2=Y4)|Y3=Y4))))))|(?[Y0]:(?[Y1]:(?[Y2]:(?[Y3]:(?[Y4]:(?[Y5]:((((((rinvR_N_times_M_to_1(X,Y0)&rinvR_N_times_M_to_1(X,Y1))&rinvR_N_times_M_to_1(X,Y2))&rinvR_N_times_M_to_1(X,Y3))&rinvR_N_times_M_to_1(X,Y4))&rinvR_N_times_M_to_1(X,Y5))&((((((((((((((Y0!=Y1&Y0!=Y2)&Y0!=Y3)&Y0!=Y4)&Y0!=Y5)&Y1!=Y2)&Y1!=Y3)&Y1!=Y4)&Y1!=Y5)&Y2!=Y3)&Y2!=Y4)&Y2!=Y5)&Y3!=Y4)&Y3!=Y5)&Y4!=Y5)))))))))|cinfinite(X)))),inference(fof_nnf,[status(thm)],[axiom_6])).
% 7.49/7.65 fof(c81,plain,((![X]:(~cinfinite(X)|((?[Y0]:(?[Y1]:(?[Y2]:(?[Y3]:(?[Y4]:((((((((((((((rinvR_N_times_M_to_1(X,Y0)&rinvR_N_times_M_to_1(X,Y1))&rinvR_N_times_M_to_1(X,Y2))&rinvR_N_times_M_to_1(X,Y3))&rinvR_N_times_M_to_1(X,Y4))&Y0!=Y1)&Y0!=Y2)&Y0!=Y3)&Y0!=Y4)&Y1!=Y2)&Y1!=Y3)&Y1!=Y4)&Y2!=Y3)&Y2!=Y4)&Y3!=Y4))))))&(![Y0]:(![Y1]:(![Y2]:(![Y3]:(![Y4]:(![Y5]:((((((~rinvR_N_times_M_to_1(X,Y0)|~rinvR_N_times_M_to_1(X,Y1))|~rinvR_N_times_M_to_1(X,Y2))|~rinvR_N_times_M_to_1(X,Y3))|~rinvR_N_times_M_to_1(X,Y4))|~rinvR_N_times_M_to_1(X,Y5))|((((((((((((((Y0=Y1|Y0=Y2)|Y0=Y3)|Y0=Y4)|Y0=Y5)|Y1=Y2)|Y1=Y3)|Y1=Y4)|Y1=Y5)|Y2=Y3)|Y2=Y4)|Y2=Y5)|Y3=Y4)|Y3=Y5)|Y4=Y5)))))))))))&(![X]:(((![Y0]:(![Y1]:(![Y2]:(![Y3]:(![Y4]:((((((((((((((~rinvR_N_times_M_to_1(X,Y0)|~rinvR_N_times_M_to_1(X,Y1))|~rinvR_N_times_M_to_1(X,Y2))|~rinvR_N_times_M_to_1(X,Y3))|~rinvR_N_times_M_to_1(X,Y4))|Y0=Y1)|Y0=Y2)|Y0=Y3)|Y0=Y4)|Y1=Y2)|Y1=Y3)|Y1=Y4)|Y2=Y3)|Y2=Y4)|Y3=Y4))))))|(?[Y0]:(?[Y1]:(?[Y2]:(?[Y3]:(?[Y4]:(?[Y5]:((((((rinvR_N_times_M_to_1(X,Y0)&rinvR_N_times_M_to_1(X,Y1))&rinvR_N_times_M_to_1(X,Y2))&rinvR_N_times_M_to_1(X,Y3))&rinvR_N_times_M_to_1(X,Y4))&rinvR_N_times_M_to_1(X,Y5))&((((((((((((((Y0!=Y1&Y0!=Y2)&Y0!=Y3)&Y0!=Y4)&Y0!=Y5)&Y1!=Y2)&Y1!=Y3)&Y1!=Y4)&Y1!=Y5)&Y2!=Y3)&Y2!=Y4)&Y2!=Y5)&Y3!=Y4)&Y3!=Y5)&Y4!=Y5)))))))))|cinfinite(X)))),inference(shift_quantors,[status(thm)],[c80])).
% 7.49/7.65 fof(c82,plain,((![X47]:(~cinfinite(X47)|((?[X48]:(?[X49]:(?[X50]:(?[X51]:(?[X52]:((((((((((((((rinvR_N_times_M_to_1(X47,X48)&rinvR_N_times_M_to_1(X47,X49))&rinvR_N_times_M_to_1(X47,X50))&rinvR_N_times_M_to_1(X47,X51))&rinvR_N_times_M_to_1(X47,X52))&X48!=X49)&X48!=X50)&X48!=X51)&X48!=X52)&X49!=X50)&X49!=X51)&X49!=X52)&X50!=X51)&X50!=X52)&X51!=X52))))))&(![X53]:(![X54]:(![X55]:(![X56]:(![X57]:(![X58]:((((((~rinvR_N_times_M_to_1(X47,X53)|~rinvR_N_times_M_to_1(X47,X54))|~rinvR_N_times_M_to_1(X47,X55))|~rinvR_N_times_M_to_1(X47,X56))|~rinvR_N_times_M_to_1(X47,X57))|~rinvR_N_times_M_to_1(X47,X58))|((((((((((((((X53=X54|X53=X55)|X53=X56)|X53=X57)|X53=X58)|X54=X55)|X54=X56)|X54=X57)|X54=X58)|X55=X56)|X55=X57)|X55=X58)|X56=X57)|X56=X58)|X57=X58)))))))))))&(![X59]:(((![X60]:(![X61]:(![X62]:(![X63]:(![X64]:((((((((((((((~rinvR_N_times_M_to_1(X59,X60)|~rinvR_N_times_M_to_1(X59,X61))|~rinvR_N_times_M_to_1(X59,X62))|~rinvR_N_times_M_to_1(X59,X63))|~rinvR_N_times_M_to_1(X59,X64))|X60=X61)|X60=X62)|X60=X63)|X60=X64)|X61=X62)|X61=X63)|X61=X64)|X62=X63)|X62=X64)|X63=X64))))))|(?[X65]:(?[X66]:(?[X67]:(?[X68]:(?[X69]:(?[X70]:((((((rinvR_N_times_M_to_1(X59,X65)&rinvR_N_times_M_to_1(X59,X66))&rinvR_N_times_M_to_1(X59,X67))&rinvR_N_times_M_to_1(X59,X68))&rinvR_N_times_M_to_1(X59,X69))&rinvR_N_times_M_to_1(X59,X70))&((((((((((((((X65!=X66&X65!=X67)&X65!=X68)&X65!=X69)&X65!=X70)&X66!=X67)&X66!=X68)&X66!=X69)&X66!=X70)&X67!=X68)&X67!=X69)&X67!=X70)&X68!=X69)&X68!=X70)&X69!=X70)))))))))|cinfinite(X59)))),inference(variable_rename,[status(thm)],[c81])).
% 7.49/7.65 fof(c84,plain,(![X47]:(![X53]:(![X54]:(![X55]:(![X56]:(![X57]:(![X58]:(![X59]:(![X60]:(![X61]:(![X62]:(![X63]:(![X64]:((~cinfinite(X47)|(((((((((((((((rinvR_N_times_M_to_1(X47,skolem0006(X47))&rinvR_N_times_M_to_1(X47,skolem0007(X47)))&rinvR_N_times_M_to_1(X47,skolem0008(X47)))&rinvR_N_times_M_to_1(X47,skolem0009(X47)))&rinvR_N_times_M_to_1(X47,skolem0010(X47)))&skolem0006(X47)!=skolem0007(X47))&skolem0006(X47)!=skolem0008(X47))&skolem0006(X47)!=skolem0009(X47))&skolem0006(X47)!=skolem0010(X47))&skolem0007(X47)!=skolem0008(X47))&skolem0007(X47)!=skolem0009(X47))&skolem0007(X47)!=skolem0010(X47))&skolem0008(X47)!=skolem0009(X47))&skolem0008(X47)!=skolem0010(X47))&skolem0009(X47)!=skolem0010(X47))&((((((~rinvR_N_times_M_to_1(X47,X53)|~rinvR_N_times_M_to_1(X47,X54))|~rinvR_N_times_M_to_1(X47,X55))|~rinvR_N_times_M_to_1(X47,X56))|~rinvR_N_times_M_to_1(X47,X57))|~rinvR_N_times_M_to_1(X47,X58))|((((((((((((((X53=X54|X53=X55)|X53=X56)|X53=X57)|X53=X58)|X54=X55)|X54=X56)|X54=X57)|X54=X58)|X55=X56)|X55=X57)|X55=X58)|X56=X57)|X56=X58)|X57=X58))))&((((((((((((((((~rinvR_N_times_M_to_1(X59,X60)|~rinvR_N_times_M_to_1(X59,X61))|~rinvR_N_times_M_to_1(X59,X62))|~rinvR_N_times_M_to_1(X59,X63))|~rinvR_N_times_M_to_1(X59,X64))|X60=X61)|X60=X62)|X60=X63)|X60=X64)|X61=X62)|X61=X63)|X61=X64)|X62=X63)|X62=X64)|X63=X64)|((((((rinvR_N_times_M_to_1(X59,skolem0011(X59))&rinvR_N_times_M_to_1(X59,skolem0012(X59)))&rinvR_N_times_M_to_1(X59,skolem0013(X59)))&rinvR_N_times_M_to_1(X59,skolem0014(X59)))&rinvR_N_times_M_to_1(X59,skolem0015(X59)))&rinvR_N_times_M_to_1(X59,skolem0016(X59)))&((((((((((((((skolem0011(X59)!=skolem0012(X59)&skolem0011(X59)!=skolem0013(X59))&skolem0011(X59)!=skolem0014(X59))&skolem0011(X59)!=skolem0015(X59))&skolem0011(X59)!=skolem0016(X59))&skolem0012(X59)!=skolem0013(X59))&skolem0012(X59)!=skolem0014(X59))&skolem0012(X59)!=skolem0015(X59))&skolem0012(X59)!=skolem0016(X59))&skolem0013(X59)!=skolem0014(X59))&skolem0013(X59)!=skolem0015(X59))&skolem0013(X59)!=skolem0016(X59))&skolem0014(X59)!=skolem0015(X59))&skolem0014(X59)!=skolem0016(X59))&skolem0015(X59)!=skolem0016(X59))))|cinfinite(X59)))))))))))))))),inference(shift_quantors,[status(thm)],[fof(c83,plain,((![X47]:(~cinfinite(X47)|(((((((((((((((rinvR_N_times_M_to_1(X47,skolem0006(X47))&rinvR_N_times_M_to_1(X47,skolem0007(X47)))&rinvR_N_times_M_to_1(X47,skolem0008(X47)))&rinvR_N_times_M_to_1(X47,skolem0009(X47)))&rinvR_N_times_M_to_1(X47,skolem0010(X47)))&skolem0006(X47)!=skolem0007(X47))&skolem0006(X47)!=skolem0008(X47))&skolem0006(X47)!=skolem0009(X47))&skolem0006(X47)!=skolem0010(X47))&skolem0007(X47)!=skolem0008(X47))&skolem0007(X47)!=skolem0009(X47))&skolem0007(X47)!=skolem0010(X47))&skolem0008(X47)!=skolem0009(X47))&skolem0008(X47)!=skolem0010(X47))&skolem0009(X47)!=skolem0010(X47))&(![X53]:(![X54]:(![X55]:(![X56]:(![X57]:(![X58]:((((((~rinvR_N_times_M_to_1(X47,X53)|~rinvR_N_times_M_to_1(X47,X54))|~rinvR_N_times_M_to_1(X47,X55))|~rinvR_N_times_M_to_1(X47,X56))|~rinvR_N_times_M_to_1(X47,X57))|~rinvR_N_times_M_to_1(X47,X58))|((((((((((((((X53=X54|X53=X55)|X53=X56)|X53=X57)|X53=X58)|X54=X55)|X54=X56)|X54=X57)|X54=X58)|X55=X56)|X55=X57)|X55=X58)|X56=X57)|X56=X58)|X57=X58)))))))))))&(![X59]:(((![X60]:(![X61]:(![X62]:(![X63]:(![X64]:((((((((((((((~rinvR_N_times_M_to_1(X59,X60)|~rinvR_N_times_M_to_1(X59,X61))|~rinvR_N_times_M_to_1(X59,X62))|~rinvR_N_times_M_to_1(X59,X63))|~rinvR_N_times_M_to_1(X59,X64))|X60=X61)|X60=X62)|X60=X63)|X60=X64)|X61=X62)|X61=X63)|X61=X64)|X62=X63)|X62=X64)|X63=X64))))))|((((((rinvR_N_times_M_to_1(X59,skolem0011(X59))&rinvR_N_times_M_to_1(X59,skolem0012(X59)))&rinvR_N_times_M_to_1(X59,skolem0013(X59)))&rinvR_N_times_M_to_1(X59,skolem0014(X59)))&rinvR_N_times_M_to_1(X59,skolem0015(X59)))&rinvR_N_times_M_to_1(X59,skolem0016(X59)))&((((((((((((((skolem0011(X59)!=skolem0012(X59)&skolem0011(X59)!=skolem0013(X59))&skolem0011(X59)!=skolem0014(X59))&skolem0011(X59)!=skolem0015(X59))&skolem0011(X59)!=skolem0016(X59))&skolem0012(X59)!=skolem0013(X59))&skolem0012(X59)!=skolem0014(X59))&skolem0012(X59)!=skolem0015(X59))&skolem0012(X59)!=skolem0016(X59))&skolem0013(X59)!=skolem0014(X59))&skolem0013(X59)!=skolem0015(X59))&skolem0013(X59)!=skolem0016(X59))&skolem0014(X59)!=skolem0015(X59))&skolem0014(X59)!=skolem0016(X59))&skolem0015(X59)!=skolem0016(X59))))|cinfinite(X59)))),inference(skolemize,[status(esa)],[c82])).])).
% 7.49/7.65 fof(c85,plain,(![X47]:(![X53]:(![X54]:(![X55]:(![X56]:(![X57]:(![X58]:(![X59]:(![X60]:(![X61]:(![X62]:(![X63]:(![X64]:(((((((((((((((((~cinfinite(X47)|rinvR_N_times_M_to_1(X47,skolem0006(X47)))&(~cinfinite(X47)|rinvR_N_times_M_to_1(X47,skolem0007(X47))))&(~cinfinite(X47)|rinvR_N_times_M_to_1(X47,skolem0008(X47))))&(~cinfinite(X47)|rinvR_N_times_M_to_1(X47,skolem0009(X47))))&(~cinfinite(X47)|rinvR_N_times_M_to_1(X47,skolem0010(X47))))&(~cinfinite(X47)|skolem0006(X47)!=skolem0007(X47)))&(~cinfinite(X47)|skolem0006(X47)!=skolem0008(X47)))&(~cinfinite(X47)|skolem0006(X47)!=skolem0009(X47)))&(~cinfinite(X47)|skolem0006(X47)!=skolem0010(X47)))&(~cinfinite(X47)|skolem0007(X47)!=skolem0008(X47)))&(~cinfinite(X47)|skolem0007(X47)!=skolem0009(X47)))&(~cinfinite(X47)|skolem0007(X47)!=skolem0010(X47)))&(~cinfinite(X47)|skolem0008(X47)!=skolem0009(X47)))&(~cinfinite(X47)|skolem0008(X47)!=skolem0010(X47)))&(~cinfinite(X47)|skolem0009(X47)!=skolem0010(X47)))&(~cinfinite(X47)|((((((~rinvR_N_times_M_to_1(X47,X53)|~rinvR_N_times_M_to_1(X47,X54))|~rinvR_N_times_M_to_1(X47,X55))|~rinvR_N_times_M_to_1(X47,X56))|~rinvR_N_times_M_to_1(X47,X57))|~rinvR_N_times_M_to_1(X47,X58))|((((((((((((((X53=X54|X53=X55)|X53=X56)|X53=X57)|X53=X58)|X54=X55)|X54=X56)|X54=X57)|X54=X58)|X55=X56)|X55=X57)|X55=X58)|X56=X57)|X56=X58)|X57=X58))))&((((((((((((((((((((((~rinvR_N_times_M_to_1(X59,X60)|~rinvR_N_times_M_to_1(X59,X61))|~rinvR_N_times_M_to_1(X59,X62))|~rinvR_N_times_M_to_1(X59,X63))|~rinvR_N_times_M_to_1(X59,X64))|X60=X61)|X60=X62)|X60=X63)|X60=X64)|X61=X62)|X61=X63)|X61=X64)|X62=X63)|X62=X64)|X63=X64)|rinvR_N_times_M_to_1(X59,skolem0011(X59)))|cinfinite(X59))&((((((((((((((((~rinvR_N_times_M_to_1(X59,X60)|~rinvR_N_times_M_to_1(X59,X61))|~rinvR_N_times_M_to_1(X59,X62))|~rinvR_N_times_M_to_1(X59,X63))|~rinvR_N_times_M_to_1(X59,X64))|X60=X61)|X60=X62)|X60=X63)|X60=X64)|X61=X62)|X61=X63)|X61=X64)|X62=X63)|X62=X64)|X63=X64)|rinvR_N_times_M_to_1(X59,skolem0012(X59)))|cinfinite(X59)))&((((((((((((((((~rinvR_N_times_M_to_1(X59,X60)|~rinvR_N_times_M_to_1(X59,X61))|~rinvR_N_times_M_to_1(X59,X62))|~rinvR_N_times_M_to_1(X59,X63))|~rinvR_N_times_M_to_1(X59,X64))|X60=X61)|X60=X62)|X60=X63)|X60=X64)|X61=X62)|X61=X63)|X61=X64)|X62=X63)|X62=X64)|X63=X64)|rinvR_N_times_M_to_1(X59,skolem0013(X59)))|cinfinite(X59)))&((((((((((((((((~rinvR_N_times_M_to_1(X59,X60)|~rinvR_N_times_M_to_1(X59,X61))|~rinvR_N_times_M_to_1(X59,X62))|~rinvR_N_times_M_to_1(X59,X63))|~rinvR_N_times_M_to_1(X59,X64))|X60=X61)|X60=X62)|X60=X63)|X60=X64)|X61=X62)|X61=X63)|X61=X64)|X62=X63)|X62=X64)|X63=X64)|rinvR_N_times_M_to_1(X59,skolem0014(X59)))|cinfinite(X59)))&((((((((((((((((~rinvR_N_times_M_to_1(X59,X60)|~rinvR_N_times_M_to_1(X59,X61))|~rinvR_N_times_M_to_1(X59,X62))|~rinvR_N_times_M_to_1(X59,X63))|~rinvR_N_times_M_to_1(X59,X64))|X60=X61)|X60=X62)|X60=X63)|X60=X64)|X61=X62)|X61=X63)|X61=X64)|X62=X63)|X62=X64)|X63=X64)|rinvR_N_times_M_to_1(X59,skolem0015(X59)))|cinfinite(X59)))&((((((((((((((((~rinvR_N_times_M_to_1(X59,X60)|~rinvR_N_times_M_to_1(X59,X61))|~rinvR_N_times_M_to_1(X59,X62))|~rinvR_N_times_M_to_1(X59,X63))|~rinvR_N_times_M_to_1(X59,X64))|X60=X61)|X60=X62)|X60=X63)|X60=X64)|X61=X62)|X61=X63)|X61=X64)|X62=X63)|X62=X64)|X63=X64)|rinvR_N_times_M_to_1(X59,skolem0016(X59)))|cinfinite(X59)))&((((((((((((((((((((((((((((((~rinvR_N_times_M_to_1(X59,X60)|~rinvR_N_times_M_to_1(X59,X61))|~rinvR_N_times_M_to_1(X59,X62))|~rinvR_N_times_M_to_1(X59,X63))|~rinvR_N_times_M_to_1(X59,X64))|X60=X61)|X60=X62)|X60=X63)|X60=X64)|X61=X62)|X61=X63)|X61=X64)|X62=X63)|X62=X64)|X63=X64)|skolem0011(X59)!=skolem0012(X59))|cinfinite(X59))&((((((((((((((((~rinvR_N_times_M_to_1(X59,X60)|~rinvR_N_times_M_to_1(X59,X61))|~rinvR_N_times_M_to_1(X59,X62))|~rinvR_N_times_M_to_1(X59,X63))|~rinvR_N_times_M_to_1(X59,X64))|X60=X61)|X60=X62)|X60=X63)|X60=X64)|X61=X62)|X61=X63)|X61=X64)|X62=X63)|X62=X64)|X63=X64)|skolem0011(X59)!=skolem0013(X59))|cinfinite(X59)))&((((((((((((((((~rinvR_N_times_M_to_1(X59,X60)|~rinvR_N_times_M_to_1(X59,X61))|~rinvR_N_times_M_to_1(X59,X62))|~rinvR_N_times_M_to_1(X59,X63))|~rinvR_N_times_M_to_1(X59,X64))|X60=X61)|X60=X62)|X60=X63)|X60=X64)|X61=X62)|X61=X63)|X61=X64)|X62=X63)|X62=X64)|X63=X64)|skolem0011(X59)!=skolem0014(X59))|cinfinite(X59)))&((((((((((((((((~rinvR_N_times_M_to_1(X59,X60)|~rinvR_N_times_M_to_1(X59,X61))|~rinvR_N_times_M_to_1(X59,X62))|~rinvR_N_times_M_to_1(X59,X63))|~rinvR_N_times_M_to_1(X59,X64))|X60=X61)|X60=X62)|X60=X63)|X60=X64)|X61=X62)|X61=X63)|X61=X64)|X62=X63)|X62=X64)|X63=X64)|skolem0011(X59)!=skolem0015(X59))|cinfinite(X59)))&((((((((((((((((~rinvR_N_times_M_to_1(X59,X60)|~rinvR_N_times_M_to_1(X59,X61))|~rinvR_N_times_M_to_1(X59,X62))|~rinvR_N_times_M_to_1(X59,X63))|~rinvR_N_times_M_to_1(X59,X64))|X60=X61)|X60=X62)|X60=X63)|X60=X64)|X61=X62)|X61=X63)|X61=X64)|X62=X63)|X62=X64)|X63=X64)|skolem0011(X59)!=skolem0016(X59))|cinfinite(X59)))&((((((((((((((((~rinvR_N_times_M_to_1(X59,X60)|~rinvR_N_times_M_to_1(X59,X61))|~rinvR_N_times_M_to_1(X59,X62))|~rinvR_N_times_M_to_1(X59,X63))|~rinvR_N_times_M_to_1(X59,X64))|X60=X61)|X60=X62)|X60=X63)|X60=X64)|X61=X62)|X61=X63)|X61=X64)|X62=X63)|X62=X64)|X63=X64)|skolem0012(X59)!=skolem0013(X59))|cinfinite(X59)))&((((((((((((((((~rinvR_N_times_M_to_1(X59,X60)|~rinvR_N_times_M_to_1(X59,X61))|~rinvR_N_times_M_to_1(X59,X62))|~rinvR_N_times_M_to_1(X59,X63))|~rinvR_N_times_M_to_1(X59,X64))|X60=X61)|X60=X62)|X60=X63)|X60=X64)|X61=X62)|X61=X63)|X61=X64)|X62=X63)|X62=X64)|X63=X64)|skolem0012(X59)!=skolem0014(X59))|cinfinite(X59)))&((((((((((((((((~rinvR_N_times_M_to_1(X59,X60)|~rinvR_N_times_M_to_1(X59,X61))|~rinvR_N_times_M_to_1(X59,X62))|~rinvR_N_times_M_to_1(X59,X63))|~rinvR_N_times_M_to_1(X59,X64))|X60=X61)|X60=X62)|X60=X63)|X60=X64)|X61=X62)|X61=X63)|X61=X64)|X62=X63)|X62=X64)|X63=X64)|skolem0012(X59)!=skolem0015(X59))|cinfinite(X59)))&((((((((((((((((~rinvR_N_times_M_to_1(X59,X60)|~rinvR_N_times_M_to_1(X59,X61))|~rinvR_N_times_M_to_1(X59,X62))|~rinvR_N_times_M_to_1(X59,X63))|~rinvR_N_times_M_to_1(X59,X64))|X60=X61)|X60=X62)|X60=X63)|X60=X64)|X61=X62)|X61=X63)|X61=X64)|X62=X63)|X62=X64)|X63=X64)|skolem0012(X59)!=skolem0016(X59))|cinfinite(X59)))&((((((((((((((((~rinvR_N_times_M_to_1(X59,X60)|~rinvR_N_times_M_to_1(X59,X61))|~rinvR_N_times_M_to_1(X59,X62))|~rinvR_N_times_M_to_1(X59,X63))|~rinvR_N_times_M_to_1(X59,X64))|X60=X61)|X60=X62)|X60=X63)|X60=X64)|X61=X62)|X61=X63)|X61=X64)|X62=X63)|X62=X64)|X63=X64)|skolem0013(X59)!=skolem0014(X59))|cinfinite(X59)))&((((((((((((((((~rinvR_N_times_M_to_1(X59,X60)|~rinvR_N_times_M_to_1(X59,X61))|~rinvR_N_times_M_to_1(X59,X62))|~rinvR_N_times_M_to_1(X59,X63))|~rinvR_N_times_M_to_1(X59,X64))|X60=X61)|X60=X62)|X60=X63)|X60=X64)|X61=X62)|X61=X63)|X61=X64)|X62=X63)|X62=X64)|X63=X64)|skolem0013(X59)!=skolem0015(X59))|cinfinite(X59)))&((((((((((((((((~rinvR_N_times_M_to_1(X59,X60)|~rinvR_N_times_M_to_1(X59,X61))|~rinvR_N_times_M_to_1(X59,X62))|~rinvR_N_times_M_to_1(X59,X63))|~rinvR_N_times_M_to_1(X59,X64))|X60=X61)|X60=X62)|X60=X63)|X60=X64)|X61=X62)|X61=X63)|X61=X64)|X62=X63)|X62=X64)|X63=X64)|skolem0013(X59)!=skolem0016(X59))|cinfinite(X59)))&((((((((((((((((~rinvR_N_times_M_to_1(X59,X60)|~rinvR_N_times_M_to_1(X59,X61))|~rinvR_N_times_M_to_1(X59,X62))|~rinvR_N_times_M_to_1(X59,X63))|~rinvR_N_times_M_to_1(X59,X64))|X60=X61)|X60=X62)|X60=X63)|X60=X64)|X61=X62)|X61=X63)|X61=X64)|X62=X63)|X62=X64)|X63=X64)|skolem0014(X59)!=skolem0015(X59))|cinfinite(X59)))&((((((((((((((((~rinvR_N_times_M_to_1(X59,X60)|~rinvR_N_times_M_to_1(X59,X61))|~rinvR_N_times_M_to_1(X59,X62))|~rinvR_N_times_M_to_1(X59,X63))|~rinvR_N_times_M_to_1(X59,X64))|X60=X61)|X60=X62)|X60=X63)|X60=X64)|X61=X62)|X61=X63)|X61=X64)|X62=X63)|X62=X64)|X63=X64)|skolem0014(X59)!=skolem0016(X59))|cinfinite(X59)))&((((((((((((((((~rinvR_N_times_M_to_1(X59,X60)|~rinvR_N_times_M_to_1(X59,X61))|~rinvR_N_times_M_to_1(X59,X62))|~rinvR_N_times_M_to_1(X59,X63))|~rinvR_N_times_M_to_1(X59,X64))|X60=X61)|X60=X62)|X60=X63)|X60=X64)|X61=X62)|X61=X63)|X61=X64)|X62=X63)|X62=X64)|X63=X64)|skolem0015(X59)!=skolem0016(X59))|cinfinite(X59)))))))))))))))))),inference(distribute,[status(thm)],[c84])).
% 7.49/7.65 cnf(c122,plain,~rinvR_N_times_M_to_1(X708,X704)|~rinvR_N_times_M_to_1(X708,X706)|~rinvR_N_times_M_to_1(X708,X709)|~rinvR_N_times_M_to_1(X708,X707)|~rinvR_N_times_M_to_1(X708,X705)|X704=X706|X704=X709|X704=X707|X704=X705|X706=X709|X706=X707|X706=X705|X709=X707|X709=X705|X707=X705|skolem0015(X708)!=skolem0016(X708)|cinfinite(X708),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c121,plain,~rinvR_N_times_M_to_1(X702,X698)|~rinvR_N_times_M_to_1(X702,X700)|~rinvR_N_times_M_to_1(X702,X703)|~rinvR_N_times_M_to_1(X702,X701)|~rinvR_N_times_M_to_1(X702,X699)|X698=X700|X698=X703|X698=X701|X698=X699|X700=X703|X700=X701|X700=X699|X703=X701|X703=X699|X701=X699|skolem0014(X702)!=skolem0016(X702)|cinfinite(X702),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c120,plain,~rinvR_N_times_M_to_1(X696,X692)|~rinvR_N_times_M_to_1(X696,X694)|~rinvR_N_times_M_to_1(X696,X697)|~rinvR_N_times_M_to_1(X696,X695)|~rinvR_N_times_M_to_1(X696,X693)|X692=X694|X692=X697|X692=X695|X692=X693|X694=X697|X694=X695|X694=X693|X697=X695|X697=X693|X695=X693|skolem0014(X696)!=skolem0015(X696)|cinfinite(X696),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c119,plain,~rinvR_N_times_M_to_1(X690,X686)|~rinvR_N_times_M_to_1(X690,X688)|~rinvR_N_times_M_to_1(X690,X691)|~rinvR_N_times_M_to_1(X690,X689)|~rinvR_N_times_M_to_1(X690,X687)|X686=X688|X686=X691|X686=X689|X686=X687|X688=X691|X688=X689|X688=X687|X691=X689|X691=X687|X689=X687|skolem0013(X690)!=skolem0016(X690)|cinfinite(X690),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c118,plain,~rinvR_N_times_M_to_1(X684,X680)|~rinvR_N_times_M_to_1(X684,X682)|~rinvR_N_times_M_to_1(X684,X685)|~rinvR_N_times_M_to_1(X684,X683)|~rinvR_N_times_M_to_1(X684,X681)|X680=X682|X680=X685|X680=X683|X680=X681|X682=X685|X682=X683|X682=X681|X685=X683|X685=X681|X683=X681|skolem0013(X684)!=skolem0015(X684)|cinfinite(X684),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c117,plain,~rinvR_N_times_M_to_1(X678,X674)|~rinvR_N_times_M_to_1(X678,X676)|~rinvR_N_times_M_to_1(X678,X679)|~rinvR_N_times_M_to_1(X678,X677)|~rinvR_N_times_M_to_1(X678,X675)|X674=X676|X674=X679|X674=X677|X674=X675|X676=X679|X676=X677|X676=X675|X679=X677|X679=X675|X677=X675|skolem0013(X678)!=skolem0014(X678)|cinfinite(X678),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c116,plain,~rinvR_N_times_M_to_1(X672,X668)|~rinvR_N_times_M_to_1(X672,X670)|~rinvR_N_times_M_to_1(X672,X673)|~rinvR_N_times_M_to_1(X672,X671)|~rinvR_N_times_M_to_1(X672,X669)|X668=X670|X668=X673|X668=X671|X668=X669|X670=X673|X670=X671|X670=X669|X673=X671|X673=X669|X671=X669|skolem0012(X672)!=skolem0016(X672)|cinfinite(X672),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c115,plain,~rinvR_N_times_M_to_1(X666,X662)|~rinvR_N_times_M_to_1(X666,X664)|~rinvR_N_times_M_to_1(X666,X667)|~rinvR_N_times_M_to_1(X666,X665)|~rinvR_N_times_M_to_1(X666,X663)|X662=X664|X662=X667|X662=X665|X662=X663|X664=X667|X664=X665|X664=X663|X667=X665|X667=X663|X665=X663|skolem0012(X666)!=skolem0015(X666)|cinfinite(X666),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c114,plain,~rinvR_N_times_M_to_1(X660,X656)|~rinvR_N_times_M_to_1(X660,X658)|~rinvR_N_times_M_to_1(X660,X661)|~rinvR_N_times_M_to_1(X660,X659)|~rinvR_N_times_M_to_1(X660,X657)|X656=X658|X656=X661|X656=X659|X656=X657|X658=X661|X658=X659|X658=X657|X661=X659|X661=X657|X659=X657|skolem0012(X660)!=skolem0014(X660)|cinfinite(X660),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c113,plain,~rinvR_N_times_M_to_1(X654,X650)|~rinvR_N_times_M_to_1(X654,X652)|~rinvR_N_times_M_to_1(X654,X655)|~rinvR_N_times_M_to_1(X654,X653)|~rinvR_N_times_M_to_1(X654,X651)|X650=X652|X650=X655|X650=X653|X650=X651|X652=X655|X652=X653|X652=X651|X655=X653|X655=X651|X653=X651|skolem0012(X654)!=skolem0013(X654)|cinfinite(X654),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c112,plain,~rinvR_N_times_M_to_1(X648,X644)|~rinvR_N_times_M_to_1(X648,X646)|~rinvR_N_times_M_to_1(X648,X649)|~rinvR_N_times_M_to_1(X648,X647)|~rinvR_N_times_M_to_1(X648,X645)|X644=X646|X644=X649|X644=X647|X644=X645|X646=X649|X646=X647|X646=X645|X649=X647|X649=X645|X647=X645|skolem0011(X648)!=skolem0016(X648)|cinfinite(X648),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c111,plain,~rinvR_N_times_M_to_1(X642,X638)|~rinvR_N_times_M_to_1(X642,X640)|~rinvR_N_times_M_to_1(X642,X643)|~rinvR_N_times_M_to_1(X642,X641)|~rinvR_N_times_M_to_1(X642,X639)|X638=X640|X638=X643|X638=X641|X638=X639|X640=X643|X640=X641|X640=X639|X643=X641|X643=X639|X641=X639|skolem0011(X642)!=skolem0015(X642)|cinfinite(X642),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c110,plain,~rinvR_N_times_M_to_1(X636,X632)|~rinvR_N_times_M_to_1(X636,X634)|~rinvR_N_times_M_to_1(X636,X637)|~rinvR_N_times_M_to_1(X636,X635)|~rinvR_N_times_M_to_1(X636,X633)|X632=X634|X632=X637|X632=X635|X632=X633|X634=X637|X634=X635|X634=X633|X637=X635|X637=X633|X635=X633|skolem0011(X636)!=skolem0014(X636)|cinfinite(X636),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c109,plain,~rinvR_N_times_M_to_1(X604,X600)|~rinvR_N_times_M_to_1(X604,X602)|~rinvR_N_times_M_to_1(X604,X605)|~rinvR_N_times_M_to_1(X604,X603)|~rinvR_N_times_M_to_1(X604,X601)|X600=X602|X600=X605|X600=X603|X600=X601|X602=X605|X602=X603|X602=X601|X605=X603|X605=X601|X603=X601|skolem0011(X604)!=skolem0013(X604)|cinfinite(X604),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c108,plain,~rinvR_N_times_M_to_1(X573,X569)|~rinvR_N_times_M_to_1(X573,X571)|~rinvR_N_times_M_to_1(X573,X574)|~rinvR_N_times_M_to_1(X573,X572)|~rinvR_N_times_M_to_1(X573,X570)|X569=X571|X569=X574|X569=X572|X569=X570|X571=X574|X571=X572|X571=X570|X574=X572|X574=X570|X572=X570|skolem0011(X573)!=skolem0012(X573)|cinfinite(X573),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c107,plain,~rinvR_N_times_M_to_1(X542,X538)|~rinvR_N_times_M_to_1(X542,X540)|~rinvR_N_times_M_to_1(X542,X543)|~rinvR_N_times_M_to_1(X542,X541)|~rinvR_N_times_M_to_1(X542,X539)|X538=X540|X538=X543|X538=X541|X538=X539|X540=X543|X540=X541|X540=X539|X543=X541|X543=X539|X541=X539|rinvR_N_times_M_to_1(X542,skolem0016(X542))|cinfinite(X542),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c106,plain,~rinvR_N_times_M_to_1(X511,X507)|~rinvR_N_times_M_to_1(X511,X509)|~rinvR_N_times_M_to_1(X511,X512)|~rinvR_N_times_M_to_1(X511,X510)|~rinvR_N_times_M_to_1(X511,X508)|X507=X509|X507=X512|X507=X510|X507=X508|X509=X512|X509=X510|X509=X508|X512=X510|X512=X508|X510=X508|rinvR_N_times_M_to_1(X511,skolem0015(X511))|cinfinite(X511),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c105,plain,~rinvR_N_times_M_to_1(X480,X476)|~rinvR_N_times_M_to_1(X480,X478)|~rinvR_N_times_M_to_1(X480,X481)|~rinvR_N_times_M_to_1(X480,X479)|~rinvR_N_times_M_to_1(X480,X477)|X476=X478|X476=X481|X476=X479|X476=X477|X478=X481|X478=X479|X478=X477|X481=X479|X481=X477|X479=X477|rinvR_N_times_M_to_1(X480,skolem0014(X480))|cinfinite(X480),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 fof(axiom_2,axiom,(![X]:(ccardinality_N(X)<=>((?[Y0]:(?[Y1]:(?[Y2]:(((((rinvQ_1_to_M(X,Y0)&rinvQ_1_to_M(X,Y1))&rinvQ_1_to_M(X,Y2))&Y0!=Y1)&Y0!=Y2)&Y1!=Y2))))&(![Y0]:(![Y1]:(![Y2]:(![Y3]:((((rinvQ_1_to_M(X,Y0)&rinvQ_1_to_M(X,Y1))&rinvQ_1_to_M(X,Y2))&rinvQ_1_to_M(X,Y3))=>(((((Y0=Y1|Y0=Y2)|Y0=Y3)|Y1=Y2)|Y1=Y3)|Y2=Y3))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_2)).
% 7.49/7.66 fof(c150,plain,(![X]:((~ccardinality_N(X)|((?[Y0]:(?[Y1]:(?[Y2]:(((((rinvQ_1_to_M(X,Y0)&rinvQ_1_to_M(X,Y1))&rinvQ_1_to_M(X,Y2))&Y0!=Y1)&Y0!=Y2)&Y1!=Y2))))&(![Y0]:(![Y1]:(![Y2]:(![Y3]:((((~rinvQ_1_to_M(X,Y0)|~rinvQ_1_to_M(X,Y1))|~rinvQ_1_to_M(X,Y2))|~rinvQ_1_to_M(X,Y3))|(((((Y0=Y1|Y0=Y2)|Y0=Y3)|Y1=Y2)|Y1=Y3)|Y2=Y3))))))))&(((![Y0]:(![Y1]:(![Y2]:(((((~rinvQ_1_to_M(X,Y0)|~rinvQ_1_to_M(X,Y1))|~rinvQ_1_to_M(X,Y2))|Y0=Y1)|Y0=Y2)|Y1=Y2))))|(?[Y0]:(?[Y1]:(?[Y2]:(?[Y3]:((((rinvQ_1_to_M(X,Y0)&rinvQ_1_to_M(X,Y1))&rinvQ_1_to_M(X,Y2))&rinvQ_1_to_M(X,Y3))&(((((Y0!=Y1&Y0!=Y2)&Y0!=Y3)&Y1!=Y2)&Y1!=Y3)&Y2!=Y3)))))))|ccardinality_N(X)))),inference(fof_nnf,[status(thm)],[axiom_2])).
% 7.49/7.66 fof(c151,plain,((![X]:(~ccardinality_N(X)|((?[Y0]:(?[Y1]:(?[Y2]:(((((rinvQ_1_to_M(X,Y0)&rinvQ_1_to_M(X,Y1))&rinvQ_1_to_M(X,Y2))&Y0!=Y1)&Y0!=Y2)&Y1!=Y2))))&(![Y0]:(![Y1]:(![Y2]:(![Y3]:((((~rinvQ_1_to_M(X,Y0)|~rinvQ_1_to_M(X,Y1))|~rinvQ_1_to_M(X,Y2))|~rinvQ_1_to_M(X,Y3))|(((((Y0=Y1|Y0=Y2)|Y0=Y3)|Y1=Y2)|Y1=Y3)|Y2=Y3)))))))))&(![X]:(((![Y0]:(![Y1]:(![Y2]:(((((~rinvQ_1_to_M(X,Y0)|~rinvQ_1_to_M(X,Y1))|~rinvQ_1_to_M(X,Y2))|Y0=Y1)|Y0=Y2)|Y1=Y2))))|(?[Y0]:(?[Y1]:(?[Y2]:(?[Y3]:((((rinvQ_1_to_M(X,Y0)&rinvQ_1_to_M(X,Y1))&rinvQ_1_to_M(X,Y2))&rinvQ_1_to_M(X,Y3))&(((((Y0!=Y1&Y0!=Y2)&Y0!=Y3)&Y1!=Y2)&Y1!=Y3)&Y2!=Y3)))))))|ccardinality_N(X)))),inference(shift_quantors,[status(thm)],[c150])).
% 7.49/7.66 fof(c152,plain,((![X83]:(~ccardinality_N(X83)|((?[X84]:(?[X85]:(?[X86]:(((((rinvQ_1_to_M(X83,X84)&rinvQ_1_to_M(X83,X85))&rinvQ_1_to_M(X83,X86))&X84!=X85)&X84!=X86)&X85!=X86))))&(![X87]:(![X88]:(![X89]:(![X90]:((((~rinvQ_1_to_M(X83,X87)|~rinvQ_1_to_M(X83,X88))|~rinvQ_1_to_M(X83,X89))|~rinvQ_1_to_M(X83,X90))|(((((X87=X88|X87=X89)|X87=X90)|X88=X89)|X88=X90)|X89=X90)))))))))&(![X91]:(((![X92]:(![X93]:(![X94]:(((((~rinvQ_1_to_M(X91,X92)|~rinvQ_1_to_M(X91,X93))|~rinvQ_1_to_M(X91,X94))|X92=X93)|X92=X94)|X93=X94))))|(?[X95]:(?[X96]:(?[X97]:(?[X98]:((((rinvQ_1_to_M(X91,X95)&rinvQ_1_to_M(X91,X96))&rinvQ_1_to_M(X91,X97))&rinvQ_1_to_M(X91,X98))&(((((X95!=X96&X95!=X97)&X95!=X98)&X96!=X97)&X96!=X98)&X97!=X98)))))))|ccardinality_N(X91)))),inference(variable_rename,[status(thm)],[c151])).
% 7.49/7.66 fof(c154,plain,(![X83]:(![X87]:(![X88]:(![X89]:(![X90]:(![X91]:(![X92]:(![X93]:(![X94]:((~ccardinality_N(X83)|((((((rinvQ_1_to_M(X83,skolem0020(X83))&rinvQ_1_to_M(X83,skolem0021(X83)))&rinvQ_1_to_M(X83,skolem0022(X83)))&skolem0020(X83)!=skolem0021(X83))&skolem0020(X83)!=skolem0022(X83))&skolem0021(X83)!=skolem0022(X83))&((((~rinvQ_1_to_M(X83,X87)|~rinvQ_1_to_M(X83,X88))|~rinvQ_1_to_M(X83,X89))|~rinvQ_1_to_M(X83,X90))|(((((X87=X88|X87=X89)|X87=X90)|X88=X89)|X88=X90)|X89=X90))))&(((((((~rinvQ_1_to_M(X91,X92)|~rinvQ_1_to_M(X91,X93))|~rinvQ_1_to_M(X91,X94))|X92=X93)|X92=X94)|X93=X94)|((((rinvQ_1_to_M(X91,skolem0023(X91))&rinvQ_1_to_M(X91,skolem0024(X91)))&rinvQ_1_to_M(X91,skolem0025(X91)))&rinvQ_1_to_M(X91,skolem0026(X91)))&(((((skolem0023(X91)!=skolem0024(X91)&skolem0023(X91)!=skolem0025(X91))&skolem0023(X91)!=skolem0026(X91))&skolem0024(X91)!=skolem0025(X91))&skolem0024(X91)!=skolem0026(X91))&skolem0025(X91)!=skolem0026(X91))))|ccardinality_N(X91)))))))))))),inference(shift_quantors,[status(thm)],[fof(c153,plain,((![X83]:(~ccardinality_N(X83)|((((((rinvQ_1_to_M(X83,skolem0020(X83))&rinvQ_1_to_M(X83,skolem0021(X83)))&rinvQ_1_to_M(X83,skolem0022(X83)))&skolem0020(X83)!=skolem0021(X83))&skolem0020(X83)!=skolem0022(X83))&skolem0021(X83)!=skolem0022(X83))&(![X87]:(![X88]:(![X89]:(![X90]:((((~rinvQ_1_to_M(X83,X87)|~rinvQ_1_to_M(X83,X88))|~rinvQ_1_to_M(X83,X89))|~rinvQ_1_to_M(X83,X90))|(((((X87=X88|X87=X89)|X87=X90)|X88=X89)|X88=X90)|X89=X90)))))))))&(![X91]:(((![X92]:(![X93]:(![X94]:(((((~rinvQ_1_to_M(X91,X92)|~rinvQ_1_to_M(X91,X93))|~rinvQ_1_to_M(X91,X94))|X92=X93)|X92=X94)|X93=X94))))|((((rinvQ_1_to_M(X91,skolem0023(X91))&rinvQ_1_to_M(X91,skolem0024(X91)))&rinvQ_1_to_M(X91,skolem0025(X91)))&rinvQ_1_to_M(X91,skolem0026(X91)))&(((((skolem0023(X91)!=skolem0024(X91)&skolem0023(X91)!=skolem0025(X91))&skolem0023(X91)!=skolem0026(X91))&skolem0024(X91)!=skolem0025(X91))&skolem0024(X91)!=skolem0026(X91))&skolem0025(X91)!=skolem0026(X91))))|ccardinality_N(X91)))),inference(skolemize,[status(esa)],[c152])).])).
% 7.49/7.66 fof(c155,plain,(![X83]:(![X87]:(![X88]:(![X89]:(![X90]:(![X91]:(![X92]:(![X93]:(![X94]:((((((((~ccardinality_N(X83)|rinvQ_1_to_M(X83,skolem0020(X83)))&(~ccardinality_N(X83)|rinvQ_1_to_M(X83,skolem0021(X83))))&(~ccardinality_N(X83)|rinvQ_1_to_M(X83,skolem0022(X83))))&(~ccardinality_N(X83)|skolem0020(X83)!=skolem0021(X83)))&(~ccardinality_N(X83)|skolem0020(X83)!=skolem0022(X83)))&(~ccardinality_N(X83)|skolem0021(X83)!=skolem0022(X83)))&(~ccardinality_N(X83)|((((~rinvQ_1_to_M(X83,X87)|~rinvQ_1_to_M(X83,X88))|~rinvQ_1_to_M(X83,X89))|~rinvQ_1_to_M(X83,X90))|(((((X87=X88|X87=X89)|X87=X90)|X88=X89)|X88=X90)|X89=X90))))&(((((((((((~rinvQ_1_to_M(X91,X92)|~rinvQ_1_to_M(X91,X93))|~rinvQ_1_to_M(X91,X94))|X92=X93)|X92=X94)|X93=X94)|rinvQ_1_to_M(X91,skolem0023(X91)))|ccardinality_N(X91))&(((((((~rinvQ_1_to_M(X91,X92)|~rinvQ_1_to_M(X91,X93))|~rinvQ_1_to_M(X91,X94))|X92=X93)|X92=X94)|X93=X94)|rinvQ_1_to_M(X91,skolem0024(X91)))|ccardinality_N(X91)))&(((((((~rinvQ_1_to_M(X91,X92)|~rinvQ_1_to_M(X91,X93))|~rinvQ_1_to_M(X91,X94))|X92=X93)|X92=X94)|X93=X94)|rinvQ_1_to_M(X91,skolem0025(X91)))|ccardinality_N(X91)))&(((((((~rinvQ_1_to_M(X91,X92)|~rinvQ_1_to_M(X91,X93))|~rinvQ_1_to_M(X91,X94))|X92=X93)|X92=X94)|X93=X94)|rinvQ_1_to_M(X91,skolem0026(X91)))|ccardinality_N(X91)))&((((((((((((~rinvQ_1_to_M(X91,X92)|~rinvQ_1_to_M(X91,X93))|~rinvQ_1_to_M(X91,X94))|X92=X93)|X92=X94)|X93=X94)|skolem0023(X91)!=skolem0024(X91))|ccardinality_N(X91))&(((((((~rinvQ_1_to_M(X91,X92)|~rinvQ_1_to_M(X91,X93))|~rinvQ_1_to_M(X91,X94))|X92=X93)|X92=X94)|X93=X94)|skolem0023(X91)!=skolem0025(X91))|ccardinality_N(X91)))&(((((((~rinvQ_1_to_M(X91,X92)|~rinvQ_1_to_M(X91,X93))|~rinvQ_1_to_M(X91,X94))|X92=X93)|X92=X94)|X93=X94)|skolem0023(X91)!=skolem0026(X91))|ccardinality_N(X91)))&(((((((~rinvQ_1_to_M(X91,X92)|~rinvQ_1_to_M(X91,X93))|~rinvQ_1_to_M(X91,X94))|X92=X93)|X92=X94)|X93=X94)|skolem0024(X91)!=skolem0025(X91))|ccardinality_N(X91)))&(((((((~rinvQ_1_to_M(X91,X92)|~rinvQ_1_to_M(X91,X93))|~rinvQ_1_to_M(X91,X94))|X92=X93)|X92=X94)|X93=X94)|skolem0024(X91)!=skolem0026(X91))|ccardinality_N(X91)))&(((((((~rinvQ_1_to_M(X91,X92)|~rinvQ_1_to_M(X91,X93))|~rinvQ_1_to_M(X91,X94))|X92=X93)|X92=X94)|X93=X94)|skolem0025(X91)!=skolem0026(X91))|ccardinality_N(X91)))))))))))))),inference(distribute,[status(thm)],[c154])).
% 7.49/7.66 cnf(c162,plain,~ccardinality_N(X463)|~rinvQ_1_to_M(X463,X462)|~rinvQ_1_to_M(X463,X461)|~rinvQ_1_to_M(X463,X460)|~rinvQ_1_to_M(X463,X459)|X462=X461|X462=X460|X462=X459|X461=X460|X461=X459|X460=X459,inference(split_conjunct,[status(thm)],[c155])).
% 7.49/7.66 cnf(c172,plain,~rinvQ_1_to_M(X457,X458)|~rinvQ_1_to_M(X457,X455)|~rinvQ_1_to_M(X457,X456)|X458=X455|X458=X456|X455=X456|skolem0025(X457)!=skolem0026(X457)|ccardinality_N(X457),inference(split_conjunct,[status(thm)],[c155])).
% 7.49/7.66 cnf(c104,plain,~rinvR_N_times_M_to_1(X453,X449)|~rinvR_N_times_M_to_1(X453,X451)|~rinvR_N_times_M_to_1(X453,X454)|~rinvR_N_times_M_to_1(X453,X452)|~rinvR_N_times_M_to_1(X453,X450)|X449=X451|X449=X454|X449=X452|X449=X450|X451=X454|X451=X452|X451=X450|X454=X452|X454=X450|X452=X450|rinvR_N_times_M_to_1(X453,skolem0013(X453))|cinfinite(X453),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c171,plain,~rinvQ_1_to_M(X447,X448)|~rinvQ_1_to_M(X447,X445)|~rinvQ_1_to_M(X447,X446)|X448=X445|X448=X446|X445=X446|skolem0024(X447)!=skolem0026(X447)|ccardinality_N(X447),inference(split_conjunct,[status(thm)],[c155])).
% 7.49/7.66 cnf(c170,plain,~rinvQ_1_to_M(X443,X444)|~rinvQ_1_to_M(X443,X441)|~rinvQ_1_to_M(X443,X442)|X444=X441|X444=X442|X441=X442|skolem0024(X443)!=skolem0025(X443)|ccardinality_N(X443),inference(split_conjunct,[status(thm)],[c155])).
% 7.49/7.66 cnf(c169,plain,~rinvQ_1_to_M(X439,X440)|~rinvQ_1_to_M(X439,X437)|~rinvQ_1_to_M(X439,X438)|X440=X437|X440=X438|X437=X438|skolem0023(X439)!=skolem0026(X439)|ccardinality_N(X439),inference(split_conjunct,[status(thm)],[c155])).
% 7.49/7.66 cnf(c168,plain,~rinvQ_1_to_M(X435,X436)|~rinvQ_1_to_M(X435,X433)|~rinvQ_1_to_M(X435,X434)|X436=X433|X436=X434|X433=X434|skolem0023(X435)!=skolem0025(X435)|ccardinality_N(X435),inference(split_conjunct,[status(thm)],[c155])).
% 7.49/7.66 cnf(c167,plain,~rinvQ_1_to_M(X431,X432)|~rinvQ_1_to_M(X431,X429)|~rinvQ_1_to_M(X431,X430)|X432=X429|X432=X430|X429=X430|skolem0023(X431)!=skolem0024(X431)|ccardinality_N(X431),inference(split_conjunct,[status(thm)],[c155])).
% 7.49/7.66 cnf(c103,plain,~rinvR_N_times_M_to_1(X427,X423)|~rinvR_N_times_M_to_1(X427,X425)|~rinvR_N_times_M_to_1(X427,X428)|~rinvR_N_times_M_to_1(X427,X426)|~rinvR_N_times_M_to_1(X427,X424)|X423=X425|X423=X428|X423=X426|X423=X424|X425=X428|X425=X426|X425=X424|X428=X426|X428=X424|X426=X424|rinvR_N_times_M_to_1(X427,skolem0012(X427))|cinfinite(X427),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c166,plain,~rinvQ_1_to_M(X415,X416)|~rinvQ_1_to_M(X415,X413)|~rinvQ_1_to_M(X415,X414)|X416=X413|X416=X414|X413=X414|rinvQ_1_to_M(X415,skolem0026(X415))|ccardinality_N(X415),inference(split_conjunct,[status(thm)],[c155])).
% 7.49/7.66 cnf(c102,plain,~rinvR_N_times_M_to_1(X405,X401)|~rinvR_N_times_M_to_1(X405,X403)|~rinvR_N_times_M_to_1(X405,X406)|~rinvR_N_times_M_to_1(X405,X404)|~rinvR_N_times_M_to_1(X405,X402)|X401=X403|X401=X406|X401=X404|X401=X402|X403=X406|X403=X404|X403=X402|X406=X404|X406=X402|X404=X402|rinvR_N_times_M_to_1(X405,skolem0011(X405))|cinfinite(X405),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c165,plain,~rinvQ_1_to_M(X399,X400)|~rinvQ_1_to_M(X399,X397)|~rinvQ_1_to_M(X399,X398)|X400=X397|X400=X398|X397=X398|rinvQ_1_to_M(X399,skolem0025(X399))|ccardinality_N(X399),inference(split_conjunct,[status(thm)],[c155])).
% 7.49/7.66 cnf(c164,plain,~rinvQ_1_to_M(X389,X390)|~rinvQ_1_to_M(X389,X387)|~rinvQ_1_to_M(X389,X388)|X390=X387|X390=X388|X387=X388|rinvQ_1_to_M(X389,skolem0024(X389))|ccardinality_N(X389),inference(split_conjunct,[status(thm)],[c155])).
% 7.49/7.66 cnf(c101,plain,~cinfinite(X377)|~rinvR_N_times_M_to_1(X377,X378)|~rinvR_N_times_M_to_1(X377,X381)|~rinvR_N_times_M_to_1(X377,X383)|~rinvR_N_times_M_to_1(X377,X382)|~rinvR_N_times_M_to_1(X377,X379)|~rinvR_N_times_M_to_1(X377,X380)|X378=X381|X378=X383|X378=X382|X378=X379|X378=X380|X381=X383|X381=X382|X381=X379|X381=X380|X383=X382|X383=X379|X383=X380|X382=X379|X382=X380|X379=X380,inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c163,plain,~rinvQ_1_to_M(X372,X373)|~rinvQ_1_to_M(X372,X370)|~rinvQ_1_to_M(X372,X371)|X373=X370|X373=X371|X370=X371|rinvQ_1_to_M(X372,skolem0023(X372))|ccardinality_N(X372),inference(split_conjunct,[status(thm)],[c155])).
% 7.49/7.66 fof(axiom_7,axiom,(![X]:(cinfinite(X)<=>((?[Y0]:(?[Y1]:((rinvP_1_to_N(X,Y0)&rinvP_1_to_N(X,Y1))&Y0!=Y1)))&(![Y0]:(![Y1]:(![Y2]:(((rinvP_1_to_N(X,Y0)&rinvP_1_to_N(X,Y1))&rinvP_1_to_N(X,Y2))=>((Y0=Y1|Y0=Y2)|Y1=Y2)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_7)).
% 7.49/7.66 fof(c64,plain,(![X]:((~cinfinite(X)|((?[Y0]:(?[Y1]:((rinvP_1_to_N(X,Y0)&rinvP_1_to_N(X,Y1))&Y0!=Y1)))&(![Y0]:(![Y1]:(![Y2]:(((~rinvP_1_to_N(X,Y0)|~rinvP_1_to_N(X,Y1))|~rinvP_1_to_N(X,Y2))|((Y0=Y1|Y0=Y2)|Y1=Y2)))))))&(((![Y0]:(![Y1]:((~rinvP_1_to_N(X,Y0)|~rinvP_1_to_N(X,Y1))|Y0=Y1)))|(?[Y0]:(?[Y1]:(?[Y2]:(((rinvP_1_to_N(X,Y0)&rinvP_1_to_N(X,Y1))&rinvP_1_to_N(X,Y2))&((Y0!=Y1&Y0!=Y2)&Y1!=Y2))))))|cinfinite(X)))),inference(fof_nnf,[status(thm)],[axiom_7])).
% 7.49/7.66 fof(c65,plain,((![X]:(~cinfinite(X)|((?[Y0]:(?[Y1]:((rinvP_1_to_N(X,Y0)&rinvP_1_to_N(X,Y1))&Y0!=Y1)))&(![Y0]:(![Y1]:(![Y2]:(((~rinvP_1_to_N(X,Y0)|~rinvP_1_to_N(X,Y1))|~rinvP_1_to_N(X,Y2))|((Y0=Y1|Y0=Y2)|Y1=Y2))))))))&(![X]:(((![Y0]:(![Y1]:((~rinvP_1_to_N(X,Y0)|~rinvP_1_to_N(X,Y1))|Y0=Y1)))|(?[Y0]:(?[Y1]:(?[Y2]:(((rinvP_1_to_N(X,Y0)&rinvP_1_to_N(X,Y1))&rinvP_1_to_N(X,Y2))&((Y0!=Y1&Y0!=Y2)&Y1!=Y2))))))|cinfinite(X)))),inference(shift_quantors,[status(thm)],[c64])).
% 7.49/7.66 fof(c66,plain,((![X35]:(~cinfinite(X35)|((?[X36]:(?[X37]:((rinvP_1_to_N(X35,X36)&rinvP_1_to_N(X35,X37))&X36!=X37)))&(![X38]:(![X39]:(![X40]:(((~rinvP_1_to_N(X35,X38)|~rinvP_1_to_N(X35,X39))|~rinvP_1_to_N(X35,X40))|((X38=X39|X38=X40)|X39=X40))))))))&(![X41]:(((![X42]:(![X43]:((~rinvP_1_to_N(X41,X42)|~rinvP_1_to_N(X41,X43))|X42=X43)))|(?[X44]:(?[X45]:(?[X46]:(((rinvP_1_to_N(X41,X44)&rinvP_1_to_N(X41,X45))&rinvP_1_to_N(X41,X46))&((X44!=X45&X44!=X46)&X45!=X46))))))|cinfinite(X41)))),inference(variable_rename,[status(thm)],[c65])).
% 7.49/7.66 fof(c68,plain,(![X35]:(![X38]:(![X39]:(![X40]:(![X41]:(![X42]:(![X43]:((~cinfinite(X35)|(((rinvP_1_to_N(X35,skolem0001(X35))&rinvP_1_to_N(X35,skolem0002(X35)))&skolem0001(X35)!=skolem0002(X35))&(((~rinvP_1_to_N(X35,X38)|~rinvP_1_to_N(X35,X39))|~rinvP_1_to_N(X35,X40))|((X38=X39|X38=X40)|X39=X40))))&((((~rinvP_1_to_N(X41,X42)|~rinvP_1_to_N(X41,X43))|X42=X43)|(((rinvP_1_to_N(X41,skolem0003(X41))&rinvP_1_to_N(X41,skolem0004(X41)))&rinvP_1_to_N(X41,skolem0005(X41)))&((skolem0003(X41)!=skolem0004(X41)&skolem0003(X41)!=skolem0005(X41))&skolem0004(X41)!=skolem0005(X41))))|cinfinite(X41)))))))))),inference(shift_quantors,[status(thm)],[fof(c67,plain,((![X35]:(~cinfinite(X35)|(((rinvP_1_to_N(X35,skolem0001(X35))&rinvP_1_to_N(X35,skolem0002(X35)))&skolem0001(X35)!=skolem0002(X35))&(![X38]:(![X39]:(![X40]:(((~rinvP_1_to_N(X35,X38)|~rinvP_1_to_N(X35,X39))|~rinvP_1_to_N(X35,X40))|((X38=X39|X38=X40)|X39=X40))))))))&(![X41]:(((![X42]:(![X43]:((~rinvP_1_to_N(X41,X42)|~rinvP_1_to_N(X41,X43))|X42=X43)))|(((rinvP_1_to_N(X41,skolem0003(X41))&rinvP_1_to_N(X41,skolem0004(X41)))&rinvP_1_to_N(X41,skolem0005(X41)))&((skolem0003(X41)!=skolem0004(X41)&skolem0003(X41)!=skolem0005(X41))&skolem0004(X41)!=skolem0005(X41))))|cinfinite(X41)))),inference(skolemize,[status(esa)],[c66])).])).
% 7.49/7.66 fof(c69,plain,(![X35]:(![X38]:(![X39]:(![X40]:(![X41]:(![X42]:(![X43]:(((((~cinfinite(X35)|rinvP_1_to_N(X35,skolem0001(X35)))&(~cinfinite(X35)|rinvP_1_to_N(X35,skolem0002(X35))))&(~cinfinite(X35)|skolem0001(X35)!=skolem0002(X35)))&(~cinfinite(X35)|(((~rinvP_1_to_N(X35,X38)|~rinvP_1_to_N(X35,X39))|~rinvP_1_to_N(X35,X40))|((X38=X39|X38=X40)|X39=X40))))&(((((((~rinvP_1_to_N(X41,X42)|~rinvP_1_to_N(X41,X43))|X42=X43)|rinvP_1_to_N(X41,skolem0003(X41)))|cinfinite(X41))&((((~rinvP_1_to_N(X41,X42)|~rinvP_1_to_N(X41,X43))|X42=X43)|rinvP_1_to_N(X41,skolem0004(X41)))|cinfinite(X41)))&((((~rinvP_1_to_N(X41,X42)|~rinvP_1_to_N(X41,X43))|X42=X43)|rinvP_1_to_N(X41,skolem0005(X41)))|cinfinite(X41)))&((((((~rinvP_1_to_N(X41,X42)|~rinvP_1_to_N(X41,X43))|X42=X43)|skolem0003(X41)!=skolem0004(X41))|cinfinite(X41))&((((~rinvP_1_to_N(X41,X42)|~rinvP_1_to_N(X41,X43))|X42=X43)|skolem0003(X41)!=skolem0005(X41))|cinfinite(X41)))&((((~rinvP_1_to_N(X41,X42)|~rinvP_1_to_N(X41,X43))|X42=X43)|skolem0004(X41)!=skolem0005(X41))|cinfinite(X41)))))))))))),inference(distribute,[status(thm)],[c68])).
% 7.49/7.66 cnf(c79,plain,~rinvP_1_to_N(X364,X366)|~rinvP_1_to_N(X364,X365)|X366=X365|skolem0004(X364)!=skolem0005(X364)|cinfinite(X364),inference(split_conjunct,[status(thm)],[c69])).
% 7.49/7.66 cnf(c78,plain,~rinvP_1_to_N(X361,X363)|~rinvP_1_to_N(X361,X362)|X363=X362|skolem0003(X361)!=skolem0005(X361)|cinfinite(X361),inference(split_conjunct,[status(thm)],[c69])).
% 7.49/7.66 cnf(c77,plain,~rinvP_1_to_N(X358,X360)|~rinvP_1_to_N(X358,X359)|X360=X359|skolem0003(X358)!=skolem0004(X358)|cinfinite(X358),inference(split_conjunct,[status(thm)],[c69])).
% 7.49/7.66 cnf(c76,plain,~rinvP_1_to_N(X353,X355)|~rinvP_1_to_N(X353,X354)|X355=X354|rinvP_1_to_N(X353,skolem0005(X353))|cinfinite(X353),inference(split_conjunct,[status(thm)],[c69])).
% 7.49/7.66 cnf(c75,plain,~rinvP_1_to_N(X343,X345)|~rinvP_1_to_N(X343,X344)|X345=X344|rinvP_1_to_N(X343,skolem0004(X343))|cinfinite(X343),inference(split_conjunct,[status(thm)],[c69])).
% 7.49/7.66 fof(rinvP_1_to_N_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rinvP_1_to_N(A,C))=>rinvP_1_to_N(B,C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rinvP_1_to_N_substitution_1)).
% 7.49/7.66 fof(c225,plain,(![A]:(![B]:(![C]:((A!=B|~rinvP_1_to_N(A,C))|rinvP_1_to_N(B,C))))),inference(fof_nnf,[status(thm)],[rinvP_1_to_N_substitution_1])).
% 7.49/7.66 fof(c226,plain,(![X140]:(![X141]:(![X142]:((X140!=X141|~rinvP_1_to_N(X140,X142))|rinvP_1_to_N(X141,X142))))),inference(variable_rename,[status(thm)],[c225])).
% 7.49/7.66 cnf(c227,plain,X340!=X342|~rinvP_1_to_N(X340,X341)|rinvP_1_to_N(X342,X341),inference(split_conjunct,[status(thm)],[c226])).
% 7.49/7.66 fof(rinvP_1_to_N_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rinvP_1_to_N(C,A))=>rinvP_1_to_N(C,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rinvP_1_to_N_substitution_2)).
% 7.49/7.66 fof(c222,plain,(![A]:(![B]:(![C]:((A!=B|~rinvP_1_to_N(C,A))|rinvP_1_to_N(C,B))))),inference(fof_nnf,[status(thm)],[rinvP_1_to_N_substitution_2])).
% 7.49/7.66 fof(c223,plain,(![X137]:(![X138]:(![X139]:((X137!=X138|~rinvP_1_to_N(X139,X137))|rinvP_1_to_N(X139,X138))))),inference(variable_rename,[status(thm)],[c222])).
% 7.49/7.66 cnf(c224,plain,X338!=X337|~rinvP_1_to_N(X339,X338)|rinvP_1_to_N(X339,X337),inference(split_conjunct,[status(thm)],[c223])).
% 7.49/7.66 fof(rinvQ_1_to_M_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rinvQ_1_to_M(A,C))=>rinvQ_1_to_M(B,C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rinvQ_1_to_M_substitution_1)).
% 7.49/7.66 fof(c219,plain,(![A]:(![B]:(![C]:((A!=B|~rinvQ_1_to_M(A,C))|rinvQ_1_to_M(B,C))))),inference(fof_nnf,[status(thm)],[rinvQ_1_to_M_substitution_1])).
% 7.49/7.66 fof(c220,plain,(![X134]:(![X135]:(![X136]:((X134!=X135|~rinvQ_1_to_M(X134,X136))|rinvQ_1_to_M(X135,X136))))),inference(variable_rename,[status(thm)],[c219])).
% 7.49/7.66 cnf(c221,plain,X335!=X334|~rinvQ_1_to_M(X335,X336)|rinvQ_1_to_M(X334,X336),inference(split_conjunct,[status(thm)],[c220])).
% 7.49/7.66 fof(rinvQ_1_to_M_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rinvQ_1_to_M(C,A))=>rinvQ_1_to_M(C,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rinvQ_1_to_M_substitution_2)).
% 7.49/7.66 fof(c216,plain,(![A]:(![B]:(![C]:((A!=B|~rinvQ_1_to_M(C,A))|rinvQ_1_to_M(C,B))))),inference(fof_nnf,[status(thm)],[rinvQ_1_to_M_substitution_2])).
% 7.49/7.66 fof(c217,plain,(![X131]:(![X132]:(![X133]:((X131!=X132|~rinvQ_1_to_M(X133,X131))|rinvQ_1_to_M(X133,X132))))),inference(variable_rename,[status(thm)],[c216])).
% 7.49/7.66 cnf(c218,plain,X333!=X331|~rinvQ_1_to_M(X332,X333)|rinvQ_1_to_M(X332,X331),inference(split_conjunct,[status(thm)],[c217])).
% 7.49/7.66 fof(rinvR_N_times_M_to_1_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rinvR_N_times_M_to_1(A,C))=>rinvR_N_times_M_to_1(B,C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rinvR_N_times_M_to_1_substitution_1)).
% 7.49/7.66 fof(c213,plain,(![A]:(![B]:(![C]:((A!=B|~rinvR_N_times_M_to_1(A,C))|rinvR_N_times_M_to_1(B,C))))),inference(fof_nnf,[status(thm)],[rinvR_N_times_M_to_1_substitution_1])).
% 7.49/7.66 fof(c214,plain,(![X128]:(![X129]:(![X130]:((X128!=X129|~rinvR_N_times_M_to_1(X128,X130))|rinvR_N_times_M_to_1(X129,X130))))),inference(variable_rename,[status(thm)],[c213])).
% 7.49/7.66 cnf(c215,plain,X330!=X329|~rinvR_N_times_M_to_1(X330,X328)|rinvR_N_times_M_to_1(X329,X328),inference(split_conjunct,[status(thm)],[c214])).
% 7.49/7.66 cnf(c74,plain,~rinvP_1_to_N(X325,X327)|~rinvP_1_to_N(X325,X326)|X327=X326|rinvP_1_to_N(X325,skolem0003(X325))|cinfinite(X325),inference(split_conjunct,[status(thm)],[c69])).
% 7.49/7.66 fof(rinvR_N_times_M_to_1_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rinvR_N_times_M_to_1(C,A))=>rinvR_N_times_M_to_1(C,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rinvR_N_times_M_to_1_substitution_2)).
% 7.49/7.66 fof(c210,plain,(![A]:(![B]:(![C]:((A!=B|~rinvR_N_times_M_to_1(C,A))|rinvR_N_times_M_to_1(C,B))))),inference(fof_nnf,[status(thm)],[rinvR_N_times_M_to_1_substitution_2])).
% 7.49/7.66 fof(c211,plain,(![X125]:(![X126]:(![X127]:((X125!=X126|~rinvR_N_times_M_to_1(X127,X125))|rinvR_N_times_M_to_1(X127,X126))))),inference(variable_rename,[status(thm)],[c210])).
% 7.49/7.66 cnf(c212,plain,X324!=X323|~rinvR_N_times_M_to_1(X322,X324)|rinvR_N_times_M_to_1(X322,X323),inference(split_conjunct,[status(thm)],[c211])).
% 7.49/7.66 fof(rp_N_to_1_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rp_N_to_1(A,C))=>rp_N_to_1(B,C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rp_N_to_1_substitution_1)).
% 7.49/7.66 fof(c207,plain,(![A]:(![B]:(![C]:((A!=B|~rp_N_to_1(A,C))|rp_N_to_1(B,C))))),inference(fof_nnf,[status(thm)],[rp_N_to_1_substitution_1])).
% 7.49/7.66 fof(c208,plain,(![X122]:(![X123]:(![X124]:((X122!=X123|~rp_N_to_1(X122,X124))|rp_N_to_1(X123,X124))))),inference(variable_rename,[status(thm)],[c207])).
% 7.49/7.66 cnf(c209,plain,X320!=X319|~rp_N_to_1(X320,X321)|rp_N_to_1(X319,X321),inference(split_conjunct,[status(thm)],[c208])).
% 7.49/7.66 fof(rp_N_to_1_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rp_N_to_1(C,A))=>rp_N_to_1(C,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rp_N_to_1_substitution_2)).
% 7.49/7.66 fof(c204,plain,(![A]:(![B]:(![C]:((A!=B|~rp_N_to_1(C,A))|rp_N_to_1(C,B))))),inference(fof_nnf,[status(thm)],[rp_N_to_1_substitution_2])).
% 7.49/7.66 fof(c205,plain,(![X119]:(![X120]:(![X121]:((X119!=X120|~rp_N_to_1(X121,X119))|rp_N_to_1(X121,X120))))),inference(variable_rename,[status(thm)],[c204])).
% 7.49/7.66 cnf(c206,plain,X317!=X316|~rp_N_to_1(X318,X317)|rp_N_to_1(X318,X316),inference(split_conjunct,[status(thm)],[c205])).
% 7.49/7.66 fof(rq_M_to_1_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rq_M_to_1(A,C))=>rq_M_to_1(B,C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rq_M_to_1_substitution_1)).
% 7.49/7.66 fof(c201,plain,(![A]:(![B]:(![C]:((A!=B|~rq_M_to_1(A,C))|rq_M_to_1(B,C))))),inference(fof_nnf,[status(thm)],[rq_M_to_1_substitution_1])).
% 7.49/7.66 fof(c202,plain,(![X116]:(![X117]:(![X118]:((X116!=X117|~rq_M_to_1(X116,X118))|rq_M_to_1(X117,X118))))),inference(variable_rename,[status(thm)],[c201])).
% 7.49/7.66 cnf(c203,plain,X314!=X315|~rq_M_to_1(X314,X313)|rq_M_to_1(X315,X313),inference(split_conjunct,[status(thm)],[c202])).
% 7.49/7.66 fof(rq_M_to_1_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rq_M_to_1(C,A))=>rq_M_to_1(C,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rq_M_to_1_substitution_2)).
% 7.49/7.66 fof(c198,plain,(![A]:(![B]:(![C]:((A!=B|~rq_M_to_1(C,A))|rq_M_to_1(C,B))))),inference(fof_nnf,[status(thm)],[rq_M_to_1_substitution_2])).
% 7.49/7.66 fof(c199,plain,(![X113]:(![X114]:(![X115]:((X113!=X114|~rq_M_to_1(X115,X113))|rq_M_to_1(X115,X114))))),inference(variable_rename,[status(thm)],[c198])).
% 7.49/7.66 cnf(c200,plain,X311!=X312|~rq_M_to_1(X310,X311)|rq_M_to_1(X310,X312),inference(split_conjunct,[status(thm)],[c199])).
% 7.49/7.66 cnf(c73,plain,~cinfinite(X308)|~rinvP_1_to_N(X308,X309)|~rinvP_1_to_N(X308,X307)|~rinvP_1_to_N(X308,X306)|X309=X307|X309=X306|X307=X306,inference(split_conjunct,[status(thm)],[c69])).
% 7.49/7.66 fof(rr_N_times_M_to_1_substitution_1,axiom,(![A]:(![B]:(![C]:((A=B&rr_N_times_M_to_1(A,C))=>rr_N_times_M_to_1(B,C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rr_N_times_M_to_1_substitution_1)).
% 7.49/7.66 fof(c195,plain,(![A]:(![B]:(![C]:((A!=B|~rr_N_times_M_to_1(A,C))|rr_N_times_M_to_1(B,C))))),inference(fof_nnf,[status(thm)],[rr_N_times_M_to_1_substitution_1])).
% 7.49/7.66 fof(c196,plain,(![X110]:(![X111]:(![X112]:((X110!=X111|~rr_N_times_M_to_1(X110,X112))|rr_N_times_M_to_1(X111,X112))))),inference(variable_rename,[status(thm)],[c195])).
% 7.49/7.66 cnf(c197,plain,X304!=X305|~rr_N_times_M_to_1(X304,X303)|rr_N_times_M_to_1(X305,X303),inference(split_conjunct,[status(thm)],[c196])).
% 7.49/7.66 fof(rr_N_times_M_to_1_substitution_2,axiom,(![A]:(![B]:(![C]:((A=B&rr_N_times_M_to_1(C,A))=>rr_N_times_M_to_1(C,B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rr_N_times_M_to_1_substitution_2)).
% 7.49/7.66 fof(c192,plain,(![A]:(![B]:(![C]:((A!=B|~rr_N_times_M_to_1(C,A))|rr_N_times_M_to_1(C,B))))),inference(fof_nnf,[status(thm)],[rr_N_times_M_to_1_substitution_2])).
% 7.49/7.66 fof(c193,plain,(![X107]:(![X108]:(![X109]:((X107!=X108|~rr_N_times_M_to_1(X109,X107))|rr_N_times_M_to_1(X109,X108))))),inference(variable_rename,[status(thm)],[c192])).
% 7.49/7.66 cnf(c194,plain,X301!=X302|~rr_N_times_M_to_1(X300,X301)|rr_N_times_M_to_1(X300,X302),inference(split_conjunct,[status(thm)],[c193])).
% 7.49/7.66 fof(axiom_8,axiom,(![X]:(![Y]:(![Z]:((rp_N_to_1(X,Y)&rp_N_to_1(X,Z))=>Y=Z)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_8)).
% 7.49/7.66 fof(c61,plain,(![X]:(![Y]:(![Z]:((~rp_N_to_1(X,Y)|~rp_N_to_1(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_8])).
% 7.49/7.66 fof(c62,plain,(![X32]:(![X33]:(![X34]:((~rp_N_to_1(X32,X33)|~rp_N_to_1(X32,X34))|X33=X34)))),inference(variable_rename,[status(thm)],[c61])).
% 7.49/7.66 cnf(c63,plain,~rp_N_to_1(X296,X297)|~rp_N_to_1(X296,X295)|X297=X295,inference(split_conjunct,[status(thm)],[c62])).
% 7.49/7.66 fof(axiom_12,axiom,(![X]:(![Y]:(![Z]:((rq_M_to_1(X,Y)&rq_M_to_1(X,Z))=>Y=Z)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_12)).
% 7.49/7.66 fof(c44,plain,(![X]:(![Y]:(![Z]:((~rq_M_to_1(X,Y)|~rq_M_to_1(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_12])).
% 7.49/7.66 fof(c45,plain,(![X21]:(![X22]:(![X23]:((~rq_M_to_1(X21,X22)|~rq_M_to_1(X21,X23))|X22=X23)))),inference(variable_rename,[status(thm)],[c44])).
% 7.49/7.66 cnf(c46,plain,~rq_M_to_1(X291,X290)|~rq_M_to_1(X291,X292)|X290=X292,inference(split_conjunct,[status(thm)],[c45])).
% 7.49/7.66 fof(axiom_16,axiom,(![X]:(![Y]:(![Z]:((rr_N_times_M_to_1(X,Y)&rr_N_times_M_to_1(X,Z))=>Y=Z)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_16)).
% 7.49/7.66 fof(c27,plain,(![X]:(![Y]:(![Z]:((~rr_N_times_M_to_1(X,Y)|~rr_N_times_M_to_1(X,Z))|Y=Z)))),inference(fof_nnf,[status(thm)],[axiom_16])).
% 7.49/7.66 fof(c28,plain,(![X10]:(![X11]:(![X12]:((~rr_N_times_M_to_1(X10,X11)|~rr_N_times_M_to_1(X10,X12))|X11=X12)))),inference(variable_rename,[status(thm)],[c27])).
% 7.49/7.66 cnf(c29,plain,~rr_N_times_M_to_1(X285,X287)|~rr_N_times_M_to_1(X285,X286)|X287=X286,inference(split_conjunct,[status(thm)],[c28])).
% 7.49/7.66 cnf(c161,plain,~ccardinality_N(X284)|skolem0021(X284)!=skolem0022(X284),inference(split_conjunct,[status(thm)],[c155])).
% 7.49/7.66 cnf(c160,plain,~ccardinality_N(X283)|skolem0020(X283)!=skolem0022(X283),inference(split_conjunct,[status(thm)],[c155])).
% 7.49/7.66 cnf(c159,plain,~ccardinality_N(X282)|skolem0020(X282)!=skolem0021(X282),inference(split_conjunct,[status(thm)],[c155])).
% 7.49/7.66 cnf(c10,axiom,X280!=X281|X278!=X279|~rr_N_times_M_to_1(X280,X278)|rr_N_times_M_to_1(X281,X279),theory(equality)).
% 7.49/7.66 cnf(c100,plain,~cinfinite(X277)|skolem0009(X277)!=skolem0010(X277),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c99,plain,~cinfinite(X276)|skolem0008(X276)!=skolem0010(X276),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c98,plain,~cinfinite(X275)|skolem0008(X275)!=skolem0009(X275),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c97,plain,~cinfinite(X274)|skolem0007(X274)!=skolem0010(X274),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c96,plain,~cinfinite(X273)|skolem0007(X273)!=skolem0009(X273),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c9,axiom,X271!=X272|X269!=X270|~rq_M_to_1(X271,X269)|rq_M_to_1(X272,X270),theory(equality)).
% 7.49/7.66 cnf(c95,plain,~cinfinite(X268)|skolem0007(X268)!=skolem0008(X268),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c94,plain,~cinfinite(X267)|skolem0006(X267)!=skolem0010(X267),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c93,plain,~cinfinite(X266)|skolem0006(X266)!=skolem0009(X266),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c92,plain,~cinfinite(X265)|skolem0006(X265)!=skolem0008(X265),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c91,plain,~cinfinite(X264)|skolem0006(X264)!=skolem0007(X264),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c8,axiom,X262!=X263|X260!=X261|~rp_N_to_1(X262,X260)|rp_N_to_1(X263,X261),theory(equality)).
% 7.49/7.66 cnf(c72,plain,~cinfinite(X259)|skolem0001(X259)!=skolem0002(X259),inference(split_conjunct,[status(thm)],[c69])).
% 7.49/7.66 cnf(c7,axiom,X249!=X250|X247!=X248|~rinvR_N_times_M_to_1(X249,X247)|rinvR_N_times_M_to_1(X250,X248),theory(equality)).
% 7.49/7.66 cnf(c6,axiom,X235!=X236|X233!=X234|~rinvQ_1_to_M(X235,X233)|rinvQ_1_to_M(X236,X234),theory(equality)).
% 7.49/7.66 cnf(c12,axiom,X228!=X229|~xsd_string(X228)|xsd_string(X229),theory(equality)).
% 7.49/7.66 cnf(c11,axiom,X225!=X226|~xsd_integer(X225)|xsd_integer(X226),theory(equality)).
% 7.49/7.66 cnf(c5,axiom,X223!=X224|X221!=X222|~rinvP_1_to_N(X223,X221)|rinvP_1_to_N(X224,X222),theory(equality)).
% 7.49/7.66 cnf(c158,plain,~ccardinality_N(X220)|rinvQ_1_to_M(X220,skolem0022(X220)),inference(split_conjunct,[status(thm)],[c155])).
% 7.49/7.66 cnf(c157,plain,~ccardinality_N(X219)|rinvQ_1_to_M(X219,skolem0021(X219)),inference(split_conjunct,[status(thm)],[c155])).
% 7.49/7.66 cnf(c156,plain,~ccardinality_N(X218)|rinvQ_1_to_M(X218,skolem0020(X218)),inference(split_conjunct,[status(thm)],[c155])).
% 7.49/7.66 fof(axiom_3,axiom,(![X]:(ccardinality_N(X)<=>(?[Y]:(rp_N_to_1(X,Y)&cinfinite(Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_3)).
% 7.49/7.66 fof(c141,plain,(![X]:((~ccardinality_N(X)|(?[Y]:(rp_N_to_1(X,Y)&cinfinite(Y))))&((![Y]:(~rp_N_to_1(X,Y)|~cinfinite(Y)))|ccardinality_N(X)))),inference(fof_nnf,[status(thm)],[axiom_3])).
% 7.49/7.66 fof(c142,plain,((![X]:(~ccardinality_N(X)|(?[Y]:(rp_N_to_1(X,Y)&cinfinite(Y)))))&(![X]:((![Y]:(~rp_N_to_1(X,Y)|~cinfinite(Y)))|ccardinality_N(X)))),inference(shift_quantors,[status(thm)],[c141])).
% 7.49/7.66 fof(c143,plain,((![X79]:(~ccardinality_N(X79)|(?[X80]:(rp_N_to_1(X79,X80)&cinfinite(X80)))))&(![X81]:((![X82]:(~rp_N_to_1(X81,X82)|~cinfinite(X82)))|ccardinality_N(X81)))),inference(variable_rename,[status(thm)],[c142])).
% 7.49/7.66 fof(c145,plain,(![X79]:(![X81]:(![X82]:((~ccardinality_N(X79)|(rp_N_to_1(X79,skolem0019(X79))&cinfinite(skolem0019(X79))))&((~rp_N_to_1(X81,X82)|~cinfinite(X82))|ccardinality_N(X81)))))),inference(shift_quantors,[status(thm)],[fof(c144,plain,((![X79]:(~ccardinality_N(X79)|(rp_N_to_1(X79,skolem0019(X79))&cinfinite(skolem0019(X79)))))&(![X81]:((![X82]:(~rp_N_to_1(X81,X82)|~cinfinite(X82)))|ccardinality_N(X81)))),inference(skolemize,[status(esa)],[c143])).])).
% 7.49/7.66 fof(c146,plain,(![X79]:(![X81]:(![X82]:(((~ccardinality_N(X79)|rp_N_to_1(X79,skolem0019(X79)))&(~ccardinality_N(X79)|cinfinite(skolem0019(X79))))&((~rp_N_to_1(X81,X82)|~cinfinite(X82))|ccardinality_N(X81)))))),inference(distribute,[status(thm)],[c145])).
% 7.49/7.66 cnf(c147,plain,~ccardinality_N(X217)|rp_N_to_1(X217,skolem0019(X217)),inference(split_conjunct,[status(thm)],[c146])).
% 7.49/7.66 fof(axiom_4,axiom,(![X]:(ccardinality_N_times_M(X)<=>(?[Y]:(rq_M_to_1(X,Y)&ccardinality_N(Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_4)).
% 7.49/7.66 fof(c132,plain,(![X]:((~ccardinality_N_times_M(X)|(?[Y]:(rq_M_to_1(X,Y)&ccardinality_N(Y))))&((![Y]:(~rq_M_to_1(X,Y)|~ccardinality_N(Y)))|ccardinality_N_times_M(X)))),inference(fof_nnf,[status(thm)],[axiom_4])).
% 7.49/7.66 fof(c133,plain,((![X]:(~ccardinality_N_times_M(X)|(?[Y]:(rq_M_to_1(X,Y)&ccardinality_N(Y)))))&(![X]:((![Y]:(~rq_M_to_1(X,Y)|~ccardinality_N(Y)))|ccardinality_N_times_M(X)))),inference(shift_quantors,[status(thm)],[c132])).
% 7.49/7.66 fof(c134,plain,((![X75]:(~ccardinality_N_times_M(X75)|(?[X76]:(rq_M_to_1(X75,X76)&ccardinality_N(X76)))))&(![X77]:((![X78]:(~rq_M_to_1(X77,X78)|~ccardinality_N(X78)))|ccardinality_N_times_M(X77)))),inference(variable_rename,[status(thm)],[c133])).
% 7.49/7.66 fof(c136,plain,(![X75]:(![X77]:(![X78]:((~ccardinality_N_times_M(X75)|(rq_M_to_1(X75,skolem0018(X75))&ccardinality_N(skolem0018(X75))))&((~rq_M_to_1(X77,X78)|~ccardinality_N(X78))|ccardinality_N_times_M(X77)))))),inference(shift_quantors,[status(thm)],[fof(c135,plain,((![X75]:(~ccardinality_N_times_M(X75)|(rq_M_to_1(X75,skolem0018(X75))&ccardinality_N(skolem0018(X75)))))&(![X77]:((![X78]:(~rq_M_to_1(X77,X78)|~ccardinality_N(X78)))|ccardinality_N_times_M(X77)))),inference(skolemize,[status(esa)],[c134])).])).
% 7.49/7.66 fof(c137,plain,(![X75]:(![X77]:(![X78]:(((~ccardinality_N_times_M(X75)|rq_M_to_1(X75,skolem0018(X75)))&(~ccardinality_N_times_M(X75)|ccardinality_N(skolem0018(X75))))&((~rq_M_to_1(X77,X78)|~ccardinality_N(X78))|ccardinality_N_times_M(X77)))))),inference(distribute,[status(thm)],[c136])).
% 7.49/7.66 cnf(c138,plain,~ccardinality_N_times_M(X216)|rq_M_to_1(X216,skolem0018(X216)),inference(split_conjunct,[status(thm)],[c137])).
% 7.49/7.66 fof(axiom_5,axiom,(![X]:(ccardinality_N_times_M(X)<=>(?[Y]:(rr_N_times_M_to_1(X,Y)&cinfinite(Y))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_5)).
% 7.49/7.66 fof(c123,plain,(![X]:((~ccardinality_N_times_M(X)|(?[Y]:(rr_N_times_M_to_1(X,Y)&cinfinite(Y))))&((![Y]:(~rr_N_times_M_to_1(X,Y)|~cinfinite(Y)))|ccardinality_N_times_M(X)))),inference(fof_nnf,[status(thm)],[axiom_5])).
% 7.49/7.66 fof(c124,plain,((![X]:(~ccardinality_N_times_M(X)|(?[Y]:(rr_N_times_M_to_1(X,Y)&cinfinite(Y)))))&(![X]:((![Y]:(~rr_N_times_M_to_1(X,Y)|~cinfinite(Y)))|ccardinality_N_times_M(X)))),inference(shift_quantors,[status(thm)],[c123])).
% 7.49/7.66 fof(c125,plain,((![X71]:(~ccardinality_N_times_M(X71)|(?[X72]:(rr_N_times_M_to_1(X71,X72)&cinfinite(X72)))))&(![X73]:((![X74]:(~rr_N_times_M_to_1(X73,X74)|~cinfinite(X74)))|ccardinality_N_times_M(X73)))),inference(variable_rename,[status(thm)],[c124])).
% 7.49/7.66 fof(c127,plain,(![X71]:(![X73]:(![X74]:((~ccardinality_N_times_M(X71)|(rr_N_times_M_to_1(X71,skolem0017(X71))&cinfinite(skolem0017(X71))))&((~rr_N_times_M_to_1(X73,X74)|~cinfinite(X74))|ccardinality_N_times_M(X73)))))),inference(shift_quantors,[status(thm)],[fof(c126,plain,((![X71]:(~ccardinality_N_times_M(X71)|(rr_N_times_M_to_1(X71,skolem0017(X71))&cinfinite(skolem0017(X71)))))&(![X73]:((![X74]:(~rr_N_times_M_to_1(X73,X74)|~cinfinite(X74)))|ccardinality_N_times_M(X73)))),inference(skolemize,[status(esa)],[c125])).])).
% 7.49/7.66 fof(c128,plain,(![X71]:(![X73]:(![X74]:(((~ccardinality_N_times_M(X71)|rr_N_times_M_to_1(X71,skolem0017(X71)))&(~ccardinality_N_times_M(X71)|cinfinite(skolem0017(X71))))&((~rr_N_times_M_to_1(X73,X74)|~cinfinite(X74))|ccardinality_N_times_M(X73)))))),inference(distribute,[status(thm)],[c127])).
% 7.49/7.66 cnf(c129,plain,~ccardinality_N_times_M(X213)|rr_N_times_M_to_1(X213,skolem0017(X213)),inference(split_conjunct,[status(thm)],[c128])).
% 7.49/7.66 cnf(c90,plain,~cinfinite(X212)|rinvR_N_times_M_to_1(X212,skolem0010(X212)),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c89,plain,~cinfinite(X211)|rinvR_N_times_M_to_1(X211,skolem0009(X211)),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c88,plain,~cinfinite(X210)|rinvR_N_times_M_to_1(X210,skolem0008(X210)),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c87,plain,~cinfinite(X209)|rinvR_N_times_M_to_1(X209,skolem0007(X209)),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c86,plain,~cinfinite(X206)|rinvR_N_times_M_to_1(X206,skolem0006(X206)),inference(split_conjunct,[status(thm)],[c85])).
% 7.49/7.66 cnf(c71,plain,~cinfinite(X205)|rinvP_1_to_N(X205,skolem0002(X205)),inference(split_conjunct,[status(thm)],[c69])).
% 7.49/7.66 cnf(c70,plain,~cinfinite(X204)|rinvP_1_to_N(X204,skolem0001(X204)),inference(split_conjunct,[status(thm)],[c69])).
% 7.49/7.66 cnf(c2,axiom,X199!=X200|~cinfinite(X199)|cinfinite(X200),theory(equality)).
% 7.49/7.66 cnf(c148,plain,~ccardinality_N(X197)|cinfinite(skolem0019(X197)),inference(split_conjunct,[status(thm)],[c146])).
% 7.49/7.66 cnf(c139,plain,~ccardinality_N_times_M(X196)|ccardinality_N(skolem0018(X196)),inference(split_conjunct,[status(thm)],[c137])).
% 7.49/7.66 cnf(c130,plain,~ccardinality_N_times_M(X195)|cinfinite(skolem0017(X195)),inference(split_conjunct,[status(thm)],[c128])).
% 7.49/7.66 cnf(c1,axiom,X192!=X193|~ccardinality_N_times_M(X192)|ccardinality_N_times_M(X193),theory(equality)).
% 7.49/7.66 fof(axiom_11,axiom,(![X]:(![Y]:(rp_N_to_1(X,Y)<=>rinvP_1_to_N(Y,X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_11)).
% 7.49/7.66 fof(c47,plain,(![X]:(![Y]:((~rp_N_to_1(X,Y)|rinvP_1_to_N(Y,X))&(~rinvP_1_to_N(Y,X)|rp_N_to_1(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_11])).
% 7.49/7.66 fof(c48,plain,((![X]:(![Y]:(~rp_N_to_1(X,Y)|rinvP_1_to_N(Y,X))))&(![X]:(![Y]:(~rinvP_1_to_N(Y,X)|rp_N_to_1(X,Y))))),inference(shift_quantors,[status(thm)],[c47])).
% 7.49/7.66 fof(c50,plain,(![X24]:(![X25]:(![X26]:(![X27]:((~rp_N_to_1(X24,X25)|rinvP_1_to_N(X25,X24))&(~rinvP_1_to_N(X27,X26)|rp_N_to_1(X26,X27))))))),inference(shift_quantors,[status(thm)],[fof(c49,plain,((![X24]:(![X25]:(~rp_N_to_1(X24,X25)|rinvP_1_to_N(X25,X24))))&(![X26]:(![X27]:(~rinvP_1_to_N(X27,X26)|rp_N_to_1(X26,X27))))),inference(variable_rename,[status(thm)],[c48])).])).
% 7.49/7.66 cnf(c52,plain,~rinvP_1_to_N(X190,X191)|rp_N_to_1(X191,X190),inference(split_conjunct,[status(thm)],[c50])).
% 7.49/7.66 cnf(c51,plain,~rp_N_to_1(X189,X188)|rinvP_1_to_N(X188,X189),inference(split_conjunct,[status(thm)],[c50])).
% 7.49/7.66 fof(axiom_15,axiom,(![X]:(![Y]:(rq_M_to_1(X,Y)<=>rinvQ_1_to_M(Y,X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_15)).
% 7.49/7.66 fof(c30,plain,(![X]:(![Y]:((~rq_M_to_1(X,Y)|rinvQ_1_to_M(Y,X))&(~rinvQ_1_to_M(Y,X)|rq_M_to_1(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_15])).
% 7.49/7.66 fof(c31,plain,((![X]:(![Y]:(~rq_M_to_1(X,Y)|rinvQ_1_to_M(Y,X))))&(![X]:(![Y]:(~rinvQ_1_to_M(Y,X)|rq_M_to_1(X,Y))))),inference(shift_quantors,[status(thm)],[c30])).
% 7.49/7.66 fof(c33,plain,(![X13]:(![X14]:(![X15]:(![X16]:((~rq_M_to_1(X13,X14)|rinvQ_1_to_M(X14,X13))&(~rinvQ_1_to_M(X16,X15)|rq_M_to_1(X15,X16))))))),inference(shift_quantors,[status(thm)],[fof(c32,plain,((![X13]:(![X14]:(~rq_M_to_1(X13,X14)|rinvQ_1_to_M(X14,X13))))&(![X15]:(![X16]:(~rinvQ_1_to_M(X16,X15)|rq_M_to_1(X15,X16))))),inference(variable_rename,[status(thm)],[c31])).])).
% 7.49/7.66 cnf(c35,plain,~rinvQ_1_to_M(X186,X187)|rq_M_to_1(X187,X186),inference(split_conjunct,[status(thm)],[c33])).
% 7.49/7.66 cnf(c34,plain,~rq_M_to_1(X185,X184)|rinvQ_1_to_M(X184,X185),inference(split_conjunct,[status(thm)],[c33])).
% 7.49/7.66 cnf(c0,axiom,X181!=X182|~ccardinality_N(X181)|ccardinality_N(X182),theory(equality)).
% 7.49/7.66 fof(axiom_19,axiom,(![X]:(![Y]:(rr_N_times_M_to_1(X,Y)<=>rinvR_N_times_M_to_1(Y,X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_19)).
% 7.49/7.66 fof(c13,plain,(![X]:(![Y]:((~rr_N_times_M_to_1(X,Y)|rinvR_N_times_M_to_1(Y,X))&(~rinvR_N_times_M_to_1(Y,X)|rr_N_times_M_to_1(X,Y))))),inference(fof_nnf,[status(thm)],[axiom_19])).
% 7.49/7.66 fof(c14,plain,((![X]:(![Y]:(~rr_N_times_M_to_1(X,Y)|rinvR_N_times_M_to_1(Y,X))))&(![X]:(![Y]:(~rinvR_N_times_M_to_1(Y,X)|rr_N_times_M_to_1(X,Y))))),inference(shift_quantors,[status(thm)],[c13])).
% 7.49/7.66 fof(c16,plain,(![X2]:(![X3]:(![X4]:(![X5]:((~rr_N_times_M_to_1(X2,X3)|rinvR_N_times_M_to_1(X3,X2))&(~rinvR_N_times_M_to_1(X5,X4)|rr_N_times_M_to_1(X4,X5))))))),inference(shift_quantors,[status(thm)],[fof(c15,plain,((![X2]:(![X3]:(~rr_N_times_M_to_1(X2,X3)|rinvR_N_times_M_to_1(X3,X2))))&(![X4]:(![X5]:(~rinvR_N_times_M_to_1(X5,X4)|rr_N_times_M_to_1(X4,X5))))),inference(variable_rename,[status(thm)],[c14])).])).
% 7.49/7.66 cnf(c18,plain,~rinvR_N_times_M_to_1(X180,X179)|rr_N_times_M_to_1(X179,X180),inference(split_conjunct,[status(thm)],[c16])).
% 7.49/7.66 cnf(c17,plain,~rr_N_times_M_to_1(X178,X177)|rinvR_N_times_M_to_1(X177,X178),inference(split_conjunct,[status(thm)],[c16])).
% 7.49/7.66 fof(axiom_9,axiom,(![X]:(![Y]:(rp_N_to_1(X,Y)=>ccardinality_N(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_9)).
% 7.49/7.66 fof(c56,plain,(![X]:(![Y]:(~rp_N_to_1(X,Y)|ccardinality_N(X)))),inference(fof_nnf,[status(thm)],[axiom_9])).
% 7.49/7.66 fof(c57,plain,(![X]:((![Y]:~rp_N_to_1(X,Y))|ccardinality_N(X))),inference(shift_quantors,[status(thm)],[c56])).
% 7.49/7.66 fof(c59,plain,(![X30]:(![X31]:(~rp_N_to_1(X30,X31)|ccardinality_N(X30)))),inference(shift_quantors,[status(thm)],[fof(c58,plain,(![X30]:((![X31]:~rp_N_to_1(X30,X31))|ccardinality_N(X30))),inference(variable_rename,[status(thm)],[c57])).])).
% 7.49/7.66 cnf(c60,plain,~rp_N_to_1(X176,X175)|ccardinality_N(X176),inference(split_conjunct,[status(thm)],[c59])).
% 7.49/7.66 fof(axiom_10,axiom,(![X]:(![Y]:(rp_N_to_1(X,Y)=>cinfinite(Y)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_10)).
% 7.49/7.66 fof(c53,plain,(![X]:(![Y]:(~rp_N_to_1(X,Y)|cinfinite(Y)))),inference(fof_nnf,[status(thm)],[axiom_10])).
% 7.49/7.66 fof(c54,plain,(![X28]:(![X29]:(~rp_N_to_1(X28,X29)|cinfinite(X29)))),inference(variable_rename,[status(thm)],[c53])).
% 7.49/7.66 cnf(c55,plain,~rp_N_to_1(X173,X174)|cinfinite(X174),inference(split_conjunct,[status(thm)],[c54])).
% 7.49/7.66 fof(axiom_13,axiom,(![X]:(![Y]:(rq_M_to_1(X,Y)=>ccardinality_N_times_M(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_13)).
% 7.49/7.66 fof(c39,plain,(![X]:(![Y]:(~rq_M_to_1(X,Y)|ccardinality_N_times_M(X)))),inference(fof_nnf,[status(thm)],[axiom_13])).
% 7.49/7.66 fof(c40,plain,(![X]:((![Y]:~rq_M_to_1(X,Y))|ccardinality_N_times_M(X))),inference(shift_quantors,[status(thm)],[c39])).
% 7.49/7.66 fof(c42,plain,(![X19]:(![X20]:(~rq_M_to_1(X19,X20)|ccardinality_N_times_M(X19)))),inference(shift_quantors,[status(thm)],[fof(c41,plain,(![X19]:((![X20]:~rq_M_to_1(X19,X20))|ccardinality_N_times_M(X19))),inference(variable_rename,[status(thm)],[c40])).])).
% 7.49/7.66 cnf(c43,plain,~rq_M_to_1(X171,X172)|ccardinality_N_times_M(X171),inference(split_conjunct,[status(thm)],[c42])).
% 7.49/7.66 cnf(transitivity,axiom,X169!=X168|X168!=X170|X169=X170,theory(equality)).
% 7.49/7.66 fof(axiom_14,axiom,(![X]:(![Y]:(rq_M_to_1(X,Y)=>ccardinality_N(Y)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_14)).
% 7.49/7.66 fof(c36,plain,(![X]:(![Y]:(~rq_M_to_1(X,Y)|ccardinality_N(Y)))),inference(fof_nnf,[status(thm)],[axiom_14])).
% 7.49/7.66 fof(c37,plain,(![X17]:(![X18]:(~rq_M_to_1(X17,X18)|ccardinality_N(X18)))),inference(variable_rename,[status(thm)],[c36])).
% 7.49/7.66 cnf(c38,plain,~rq_M_to_1(X166,X167)|ccardinality_N(X167),inference(split_conjunct,[status(thm)],[c37])).
% 7.49/7.66 fof(axiom_17,axiom,(![X]:(![Y]:(rr_N_times_M_to_1(X,Y)=>ccardinality_N_times_M(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_17)).
% 7.49/7.66 fof(c22,plain,(![X]:(![Y]:(~rr_N_times_M_to_1(X,Y)|ccardinality_N_times_M(X)))),inference(fof_nnf,[status(thm)],[axiom_17])).
% 7.49/7.66 fof(c23,plain,(![X]:((![Y]:~rr_N_times_M_to_1(X,Y))|ccardinality_N_times_M(X))),inference(shift_quantors,[status(thm)],[c22])).
% 7.49/7.66 fof(c25,plain,(![X8]:(![X9]:(~rr_N_times_M_to_1(X8,X9)|ccardinality_N_times_M(X8)))),inference(shift_quantors,[status(thm)],[fof(c24,plain,(![X8]:((![X9]:~rr_N_times_M_to_1(X8,X9))|ccardinality_N_times_M(X8))),inference(variable_rename,[status(thm)],[c23])).])).
% 7.49/7.66 cnf(c26,plain,~rr_N_times_M_to_1(X164,X165)|ccardinality_N_times_M(X164),inference(split_conjunct,[status(thm)],[c25])).
% 7.49/7.66 fof(axiom_18,axiom,(![X]:(![Y]:(rr_N_times_M_to_1(X,Y)=>cinfinite(Y)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_18)).
% 7.49/7.66 fof(c19,plain,(![X]:(![Y]:(~rr_N_times_M_to_1(X,Y)|cinfinite(Y)))),inference(fof_nnf,[status(thm)],[axiom_18])).
% 7.49/7.66 fof(c20,plain,(![X6]:(![X7]:(~rr_N_times_M_to_1(X6,X7)|cinfinite(X7)))),inference(variable_rename,[status(thm)],[c19])).
% 7.49/7.66 cnf(c21,plain,~rr_N_times_M_to_1(X163,X162)|cinfinite(X162),inference(split_conjunct,[status(thm)],[c20])).
% 7.49/7.66 cnf(symmetry,axiom,X159!=X158|X158=X159,theory(equality)).
% 7.49/7.66 fof(axiom_1,axiom,(![X]:(xsd_string(X)<=>(~xsd_integer(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_1)).
% 7.49/7.66 fof(c173,plain,(![X]:(xsd_string(X)<=>~xsd_integer(X))),inference(fof_simplification,[status(thm)],[axiom_1])).
% 7.49/7.66 fof(c174,plain,(![X]:((~xsd_string(X)|~xsd_integer(X))&(xsd_integer(X)|xsd_string(X)))),inference(fof_nnf,[status(thm)],[c173])).
% 7.49/7.66 fof(c175,plain,((![X]:(~xsd_string(X)|~xsd_integer(X)))&(![X]:(xsd_integer(X)|xsd_string(X)))),inference(shift_quantors,[status(thm)],[c174])).
% 7.49/7.66 fof(c177,plain,(![X99]:(![X100]:((~xsd_string(X99)|~xsd_integer(X99))&(xsd_integer(X100)|xsd_string(X100))))),inference(shift_quantors,[status(thm)],[fof(c176,plain,((![X99]:(~xsd_string(X99)|~xsd_integer(X99)))&(![X100]:(xsd_integer(X100)|xsd_string(X100)))),inference(variable_rename,[status(thm)],[c175])).])).
% 7.49/7.66 cnf(c179,plain,xsd_integer(X157)|xsd_string(X157),inference(split_conjunct,[status(thm)],[c177])).
% 7.49/7.66 cnf(c178,plain,~xsd_string(X156)|~xsd_integer(X156),inference(split_conjunct,[status(thm)],[c177])).
% 7.49/7.66 cnf(reflexivity,axiom,X155=X155,theory(equality)).
% 7.49/7.66 fof(axiom_0,axiom,(![X]:(cowlThing(X)&(~cowlNothing(X)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_0)).
% 7.49/7.66 fof(c180,plain,(![X]:(cowlThing(X)&~cowlNothing(X))),inference(fof_simplification,[status(thm)],[axiom_0])).
% 7.49/7.66 fof(c181,plain,((![X]:cowlThing(X))&(![X]:~cowlNothing(X))),inference(shift_quantors,[status(thm)],[c180])).
% 7.49/7.66 fof(c183,plain,(![X101]:(![X102]:(cowlThing(X101)&~cowlNothing(X102)))),inference(shift_quantors,[status(thm)],[fof(c182,plain,((![X101]:cowlThing(X101))&(![X102]:~cowlNothing(X102))),inference(variable_rename,[status(thm)],[c181])).])).
% 7.49/7.66 cnf(c185,plain,~cowlNothing(X154),inference(split_conjunct,[status(thm)],[c183])).
% 7.49/7.66 cnf(c184,plain,cowlThing(X153),inference(split_conjunct,[status(thm)],[c183])).
% 7.49/7.66 % SZS output end Saturation
% 7.49/7.66
% 7.49/7.66 % Initial clauses : 127
% 7.49/7.66 % Processed clauses : 115
% 7.49/7.66 % Factors computed : 49
% 7.49/7.66 % Resolvents computed: 8
% 7.49/7.66 % Tautologies deleted: 8
% 7.49/7.66 % Forward subsumed : 61
% 7.49/7.66 % Backward subsumed : 0
% 7.49/7.66 % -------- CPU Time ---------
% 7.49/7.66 % User time : 7.277 s
% 7.49/7.66 % System time : 0.027 s
% 7.49/7.66 % Total time : 7.304 s
%------------------------------------------------------------------------------