%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GEO661+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n023.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 : Tue May 5 06:23:59 PM UTC 2026
% Result : Satisfiable 0.45s 0.68s
% Output : Saturation 0.45s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : GEO661+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.16/0.33 % Computer : n023.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Mon May 4 21:02:23 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.45/0.68 % Version: 1.5
% 0.45/0.68 % SZS status Satisfiable
% 0.45/0.68 % SZS output start Saturation
% 0.45/0.68 fof(reflexivity_for_equidistance,axiom,(![X]:(![Y]:equidistant(X,Y,Y,X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', reflexivity_for_equidistance)).
% 0.45/0.68 fof(c50,plain,(![X55]:(![X56]:equidistant(X55,X56,X56,X55))),inference(variable_rename,[status(thm)],[reflexivity_for_equidistance])).
% 0.45/0.68 cnf(c51,plain,equidistant(X58,X59,X59,X58),inference(split_conjunct,[status(thm)],[c50])).
% 0.45/0.68 fof(transitivity_for_equidistance,axiom,(![X]:(![Y]:(![Z]:(![V]:(![V2]:(![W]:((equidistant(X,Y,Z,V)&equidistant(X,Y,V2,W))=>equidistant(Z,V,V2,W)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', transitivity_for_equidistance)).
% 0.45/0.68 fof(c47,plain,(![X]:(![Y]:(![Z]:(![V]:(![V2]:(![W]:((~equidistant(X,Y,Z,V)|~equidistant(X,Y,V2,W))|equidistant(Z,V,V2,W)))))))),inference(fof_nnf,[status(thm)],[transitivity_for_equidistance])).
% 0.45/0.68 fof(c48,plain,(![X49]:(![X50]:(![X51]:(![X52]:(![X53]:(![X54]:((~equidistant(X49,X50,X51,X52)|~equidistant(X49,X50,X53,X54))|equidistant(X51,X52,X53,X54)))))))),inference(variable_rename,[status(thm)],[c47])).
% 0.45/0.68 cnf(c49,plain,~equidistant(X87,X83,X84,X86)|~equidistant(X87,X83,X88,X85)|equidistant(X84,X86,X88,X85),inference(split_conjunct,[status(thm)],[c48])).
% 0.45/0.68 cnf(c57,plain,~equidistant(X90,X89,X91,X92)|equidistant(X91,X92,X91,X92),inference(factor,[status(thm)],[c49])).
% 0.45/0.68 cnf(c59,plain,equidistant(X94,X93,X94,X93),inference(resolution,[status(thm)],[c57, c51])).
% 0.45/0.68 fof(outer_five_segment,axiom,(![X]:(![Y]:(![X1]:(![Y1]:(![Z]:(![Z1]:(![V]:(![V1]:(((((((equidistant(X,Y,X1,Y1)&equidistant(Y,Z,Y1,Z1))&equidistant(X,V,X1,V1))&equidistant(Y,V,Y1,V1))&between(X,Y,Z))&between(X1,Y1,Z1))&X!=Y)=>equidistant(Z,V,Z1,V1)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', outer_five_segment)).
% 0.45/0.68 fof(c33,plain,(![X]:(![Y]:(![X1]:(![Y1]:(![Z]:(![Z1]:(![V]:(![V1]:(((((((~equidistant(X,Y,X1,Y1)|~equidistant(Y,Z,Y1,Z1))|~equidistant(X,V,X1,V1))|~equidistant(Y,V,Y1,V1))|~between(X,Y,Z))|~between(X1,Y1,Z1))|X=Y)|equidistant(Z,V,Z1,V1)))))))))),inference(fof_nnf,[status(thm)],[outer_five_segment])).
% 0.45/0.68 fof(c34,plain,(![X32]:(![X33]:(![X34]:(![X35]:(![X36]:(![X37]:(![X38]:(![X39]:(((((((~equidistant(X32,X33,X34,X35)|~equidistant(X33,X36,X35,X37))|~equidistant(X32,X38,X34,X39))|~equidistant(X33,X38,X35,X39))|~between(X32,X33,X36))|~between(X34,X35,X37))|X32=X33)|equidistant(X36,X38,X37,X39)))))))))),inference(variable_rename,[status(thm)],[c33])).
% 0.45/0.68 cnf(c35,plain,~equidistant(X241,X240,X235,X237)|~equidistant(X240,X239,X237,X236)|~equidistant(X241,X238,X235,X242)|~equidistant(X240,X238,X237,X242)|~between(X241,X240,X239)|~between(X235,X237,X236)|X241=X240|equidistant(X239,X238,X236,X242),inference(split_conjunct,[status(thm)],[c34])).
% 0.45/0.68 cnf(c109,plain,~equidistant(X476,X477,X475,X477)|~equidistant(X477,X478,X477,X479)|~equidistant(X476,X480,X475,X480)|~between(X476,X477,X478)|~between(X475,X477,X479)|X476=X477|equidistant(X478,X480,X479,X480),inference(resolution,[status(thm)],[c35, c59])).
% 0.45/0.68 cnf(c168,plain,~equidistant(X505,X502,X505,X502)|~equidistant(X502,X504,X502,X503)|~between(X505,X502,X504)|~between(X505,X502,X503)|X505=X502|equidistant(X504,X506,X503,X506),inference(resolution,[status(thm)],[c109, c59])).
% 0.45/0.68 cnf(c110,plain,~equidistant(X490,X493,X489,X488)|~equidistant(X493,X491,X488,X492)|~equidistant(X490,X488,X489,X493)|~between(X490,X493,X491)|~between(X489,X488,X492)|X490=X493|equidistant(X491,X488,X492,X493),inference(resolution,[status(thm)],[c35, c51])).
% 0.45/0.68 cnf(c166,plain,~equidistant(X486,X483,X487,X483)|~equidistant(X483,X485,X483,X484)|~between(X486,X483,X485)|~between(X487,X483,X484)|X486=X483|equidistant(X485,X483,X484,X483),inference(factor,[status(thm)],[c109])).
% 0.45/0.68 cnf(c107,plain,~equidistant(X445,X443,X444,X446)|~equidistant(X443,X442,X446,X447)|~equidistant(X445,X442,X444,X447)|~between(X445,X443,X442)|~between(X444,X446,X447)|X445=X443|equidistant(X442,X442,X447,X447),inference(factor,[status(thm)],[c35])).
% 0.45/0.68 cnf(c162,plain,~equidistant(X462,X461,X463,X460)|~equidistant(X461,X463,X460,X462)|~between(X462,X461,X463)|~between(X463,X460,X462)|X462=X461|equidistant(X463,X463,X462,X462),inference(resolution,[status(thm)],[c107, c51])).
% 0.45/0.68 fof(continuity,axiom,(![U]:(![V]:(![V1]:(![X]:(![X1]:(![W]:((((equidistant(U,V,U,V1)&equidistant(U,X,U,X1))&between(U,V,X))&between(V,W,X))=>(?[A]:(between(V1,A,X1)&equidistant(U,W,U,A)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', continuity)).
% 0.45/0.68 fof(c2,plain,(![U]:(![V]:(![V1]:(![X]:(![X1]:(![W]:((((~equidistant(U,V,U,V1)|~equidistant(U,X,U,X1))|~between(U,V,X))|~between(V,W,X))|(?[A]:(between(V1,A,X1)&equidistant(U,W,U,A)))))))))),inference(fof_nnf,[status(thm)],[continuity])).
% 0.45/0.68 fof(c3,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:((((~equidistant(X2,X3,X2,X4)|~equidistant(X2,X5,X2,X6))|~between(X2,X3,X5))|~between(X3,X7,X5))|(?[X8]:(between(X4,X8,X6)&equidistant(X2,X7,X2,X8)))))))))),inference(variable_rename,[status(thm)],[c2])).
% 0.45/0.68 fof(c4,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:((((~equidistant(X2,X3,X2,X4)|~equidistant(X2,X5,X2,X6))|~between(X2,X3,X5))|~between(X3,X7,X5))|(between(X4,skolem0001(X2,X3,X4,X5,X6,X7),X6)&equidistant(X2,X7,X2,skolem0001(X2,X3,X4,X5,X6,X7)))))))))),inference(skolemize,[status(esa)],[c3])).
% 0.45/0.68 fof(c5,plain,(![X2]:(![X3]:(![X4]:(![X5]:(![X6]:(![X7]:(((((~equidistant(X2,X3,X2,X4)|~equidistant(X2,X5,X2,X6))|~between(X2,X3,X5))|~between(X3,X7,X5))|between(X4,skolem0001(X2,X3,X4,X5,X6,X7),X6))&((((~equidistant(X2,X3,X2,X4)|~equidistant(X2,X5,X2,X6))|~between(X2,X3,X5))|~between(X3,X7,X5))|equidistant(X2,X7,X2,skolem0001(X2,X3,X4,X5,X6,X7)))))))))),inference(distribute,[status(thm)],[c4])).
% 0.45/0.68 cnf(c7,plain,~equidistant(X139,X137,X139,X136)|~equidistant(X139,X140,X139,X138)|~between(X139,X137,X140)|~between(X137,X141,X140)|equidistant(X139,X141,X139,skolem0001(X139,X137,X136,X140,X138,X141)),inference(split_conjunct,[status(thm)],[c5])).
% 0.45/0.68 cnf(c72,plain,~equidistant(X357,X358,X357,X355)|~between(X357,X358,X359)|~between(X358,X356,X359)|equidistant(X357,X356,X357,skolem0001(X357,X358,X355,X359,X359,X356)),inference(resolution,[status(thm)],[c7, c59])).
% 0.45/0.68 cnf(c146,plain,~between(X403,X406,X405)|~between(X406,X404,X405)|equidistant(X403,X404,X403,skolem0001(X403,X406,X406,X405,X405,X404)),inference(resolution,[status(thm)],[c72, c59])).
% 0.45/0.68 cnf(c153,plain,~between(X418,X418,X417)|equidistant(X418,X418,X418,skolem0001(X418,X418,X418,X417,X417,X418)),inference(factor,[status(thm)],[c146])).
% 0.45/0.68 fof(upper_dimension,axiom,(![X]:(![W]:(![V]:(![Y]:(![Z]:((((equidistant(X,W,X,V)&equidistant(Y,W,Y,V))&equidistant(Z,W,Z,V))&W!=V)=>((between(X,Y,Z)|between(Y,Z,X))|between(Z,X,Y)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', upper_dimension)).
% 0.45/0.68 fof(c15,plain,(![X]:(![W]:(![V]:(![Y]:(![Z]:((((~equidistant(X,W,X,V)|~equidistant(Y,W,Y,V))|~equidistant(Z,W,Z,V))|W=V)|((between(X,Y,Z)|between(Y,Z,X))|between(Z,X,Y)))))))),inference(fof_nnf,[status(thm)],[upper_dimension])).
% 0.45/0.68 fof(c16,plain,(![X16]:(![X17]:(![X18]:(![X19]:(![X20]:((((~equidistant(X16,X17,X16,X18)|~equidistant(X19,X17,X19,X18))|~equidistant(X20,X17,X20,X18))|X17=X18)|((between(X16,X19,X20)|between(X19,X20,X16))|between(X20,X16,X19)))))))),inference(variable_rename,[status(thm)],[c15])).
% 0.45/0.68 cnf(c17,plain,~equidistant(X217,X216,X217,X219)|~equidistant(X220,X216,X220,X219)|~equidistant(X218,X216,X218,X219)|X216=X219|between(X217,X220,X218)|between(X220,X218,X217)|between(X218,X217,X220),inference(split_conjunct,[status(thm)],[c16])).
% 0.45/0.68 cnf(c99,plain,~equidistant(X409,X410,X409,X408)|~equidistant(X407,X410,X407,X408)|X410=X408|between(X409,X407,X409)|between(X407,X409,X409)|between(X409,X409,X407),inference(factor,[status(thm)],[c17])).
% 0.45/0.68 cnf(c154,plain,~equidistant(X412,X413,X412,X411)|X413=X411|between(X412,X412,X412),inference(factor,[status(thm)],[c99])).
% 0.45/0.68 fof(euclid,axiom,(![X]:(![U]:(![V]:(![Y]:(![Z]:(((between(X,U,V)&between(Y,U,Z))&X!=U)=>(?[A]:(?[B]:((between(X,Y,A)&between(X,Z,B))&between(A,V,B)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', euclid)).
% 0.45/0.68 fof(c8,plain,(![X]:(![U]:(![V]:(![Y]:(![Z]:(((~between(X,U,V)|~between(Y,U,Z))|X=U)|(?[A]:(?[B]:((between(X,Y,A)&between(X,Z,B))&between(A,V,B)))))))))),inference(fof_nnf,[status(thm)],[euclid])).
% 0.45/0.69 fof(c9,plain,(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(((~between(X9,X10,X11)|~between(X12,X10,X13))|X9=X10)|(?[X14]:(?[X15]:((between(X9,X12,X14)&between(X9,X13,X15))&between(X14,X11,X15)))))))))),inference(variable_rename,[status(thm)],[c8])).
% 0.45/0.69 fof(c10,plain,(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(((~between(X9,X10,X11)|~between(X12,X10,X13))|X9=X10)|((between(X9,X12,skolem0002(X9,X10,X11,X12,X13))&between(X9,X13,skolem0003(X9,X10,X11,X12,X13)))&between(skolem0002(X9,X10,X11,X12,X13),X11,skolem0003(X9,X10,X11,X12,X13))))))))),inference(skolemize,[status(esa)],[c9])).
% 0.45/0.69 fof(c11,plain,(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(((((~between(X9,X10,X11)|~between(X12,X10,X13))|X9=X10)|between(X9,X12,skolem0002(X9,X10,X11,X12,X13)))&(((~between(X9,X10,X11)|~between(X12,X10,X13))|X9=X10)|between(X9,X13,skolem0003(X9,X10,X11,X12,X13))))&(((~between(X9,X10,X11)|~between(X12,X10,X13))|X9=X10)|between(skolem0002(X9,X10,X11,X12,X13),X11,skolem0003(X9,X10,X11,X12,X13))))))))),inference(distribute,[status(thm)],[c10])).
% 0.45/0.69 cnf(c14,plain,~between(X202,X203,X204)|~between(X200,X203,X201)|X202=X203|between(skolem0002(X202,X203,X204,X200,X201),X204,skolem0003(X202,X203,X204,X200,X201)),inference(split_conjunct,[status(thm)],[c11])).
% 0.45/0.69 cnf(c93,plain,~between(X393,X391,X392)|X393=X391|between(skolem0002(X393,X391,X392,X393,X392),X392,skolem0003(X393,X391,X392,X393,X392)),inference(factor,[status(thm)],[c14])).
% 0.45/0.69 cnf(c6,plain,~equidistant(X117,X115,X117,X114)|~equidistant(X117,X118,X117,X116)|~between(X117,X115,X118)|~between(X115,X119,X118)|between(X114,skolem0001(X117,X115,X114,X118,X116,X119),X116),inference(split_conjunct,[status(thm)],[c5])).
% 0.45/0.69 cnf(c68,plain,~equidistant(X292,X294,X292,X293)|~between(X292,X294,X295)|~between(X294,X291,X295)|between(X293,skolem0001(X292,X294,X293,X295,X295,X291),X295),inference(resolution,[status(thm)],[c6, c59])).
% 0.45/0.69 cnf(c131,plain,~between(X385,X388,X386)|~between(X388,X387,X386)|between(X388,skolem0001(X385,X388,X388,X386,X386,X387),X386),inference(resolution,[status(thm)],[c68, c59])).
% 0.45/0.69 cnf(c151,plain,~between(X390,X390,X389)|between(X390,skolem0001(X390,X390,X390,X389,X389,X390),X389),inference(factor,[status(thm)],[c131])).
% 0.45/0.69 cnf(c13,plain,~between(X184,X185,X186)|~between(X182,X185,X183)|X184=X185|between(X184,X183,skolem0003(X184,X185,X186,X182,X183)),inference(split_conjunct,[status(thm)],[c11])).
% 0.45/0.69 cnf(c88,plain,~between(X372,X373,X374)|X372=X373|between(X372,X374,skolem0003(X372,X373,X374,X372,X374)),inference(factor,[status(thm)],[c13])).
% 0.45/0.69 cnf(c12,plain,~between(X166,X167,X168)|~between(X164,X167,X165)|X166=X167|between(X166,X164,skolem0002(X166,X167,X168,X164,X165)),inference(split_conjunct,[status(thm)],[c11])).
% 0.45/0.69 cnf(c84,plain,~between(X370,X371,X369)|X370=X371|between(X370,X370,skolem0002(X370,X371,X369,X370,X369)),inference(factor,[status(thm)],[c12])).
% 0.45/0.69 cnf(reflexivity,axiom,X57=X57,theory(equality)).
% 0.45/0.69 cnf(c0,axiom,X77!=X75|X76!=X78|X72!=X73|X71!=X74|~equidistant(X77,X76,X72,X71)|equidistant(X75,X78,X73,X74),theory(equality)).
% 0.45/0.69 cnf(c61,plain,X258!=X260|X261!=X259|X258!=X256|X261!=X257|equidistant(X260,X259,X256,X257),inference(resolution,[status(thm)],[c59, c0])).
% 0.45/0.69 cnf(c120,plain,X340!=X338|X339!=X342|X340!=X341|equidistant(X338,X342,X341,X339),inference(resolution,[status(thm)],[c61, reflexivity])).
% 0.45/0.69 cnf(c143,plain,X362!=X360|X361!=X363|equidistant(X360,X363,X362,X361),inference(resolution,[status(thm)],[c120, reflexivity])).
% 0.45/0.69 cnf(c141,plain,X346!=X345|X344!=X343|equidistant(X345,X343,X345,X344),inference(factor,[status(thm)],[c120])).
% 0.45/0.69 cnf(c71,plain,~equidistant(X334,X335,X334,X337)|~between(X334,X335,X335)|~between(X335,X336,X335)|equidistant(X334,X336,X334,skolem0001(X334,X335,X337,X335,X337,X336)),inference(factor,[status(thm)],[c7])).
% 0.45/0.69 cnf(c118,plain,X304!=X307|X306!=X305|X304!=X303|equidistant(X307,X305,X303,X305),inference(factor,[status(thm)],[c61])).
% 0.45/0.69 cnf(c135,plain,X320!=X322|X319!=X321|equidistant(X322,X321,X320,X321),inference(resolution,[status(thm)],[c118, reflexivity])).
% 0.45/0.69 cnf(c137,plain,X325!=X326|equidistant(X326,X327,X325,X327),inference(resolution,[status(thm)],[c135, reflexivity])).
% 0.45/0.69 cnf(c55,plain,X154!=X155|X152!=X153|X152!=X150|X154!=X151|equidistant(X155,X153,X150,X151),inference(resolution,[status(thm)],[c0, c51])).
% 0.45/0.69 cnf(c78,plain,X253!=X251|X254!=X252|X254!=X255|equidistant(X251,X252,X255,X253),inference(resolution,[status(thm)],[c55, reflexivity])).
% 0.45/0.69 cnf(c116,plain,X286!=X285|X288!=X287|equidistant(X285,X287,X288,X286),inference(resolution,[status(thm)],[c78, reflexivity])).
% 0.45/0.69 cnf(c115,plain,X272!=X271|X270!=X273|equidistant(X271,X273,X273,X272),inference(factor,[status(thm)],[c78])).
% 0.45/0.69 cnf(c125,plain,X281!=X282|equidistant(X282,X280,X280,X281),inference(resolution,[status(thm)],[c115, reflexivity])).
% 0.45/0.69 cnf(c67,plain,~equidistant(X275,X274,X275,X277)|~between(X275,X274,X274)|~between(X274,X276,X274)|between(X277,skolem0001(X275,X274,X277,X274,X277,X276),X277),inference(factor,[status(thm)],[c6])).
% 0.45/0.69 cnf(c77,plain,X227!=X228|X227!=X225|X227!=X226|equidistant(X228,X225,X226,X226),inference(factor,[status(thm)],[c55])).
% 0.45/0.69 cnf(c105,plain,X244!=X243|X244!=X245|equidistant(X243,X245,X244,X244),inference(resolution,[status(thm)],[c77, reflexivity])).
% 0.45/0.69 cnf(c111,plain,X247!=X246|equidistant(X246,X246,X247,X247),inference(factor,[status(thm)],[c105])).
% 0.45/0.69 cnf(c76,plain,X194!=X195|X194!=X193|X194!=X196|equidistant(X195,X193,X196,X193),inference(factor,[status(thm)],[c55])).
% 0.45/0.69 cnf(c91,plain,X206!=X207|X206!=X205|equidistant(X207,X205,X205,X205),inference(factor,[status(thm)],[c76])).
% 0.45/0.69 cnf(c75,plain,X156!=X157|X159!=X158|X159!=X160|equidistant(X157,X158,X160,X157),inference(factor,[status(thm)],[c55])).
% 0.45/0.69 cnf(c81,plain,X181!=X178|X180!=X179|equidistant(X178,X179,X180,X178),inference(resolution,[status(thm)],[c75, reflexivity])).
% 0.45/0.69 cnf(c79,plain,X162!=X163|X162!=X161|equidistant(X163,X161,X163,X163),inference(factor,[status(thm)],[c75])).
% 0.45/0.69 cnf(c83,plain,X171!=X172|equidistant(X172,X171,X172,X172),inference(resolution,[status(thm)],[c79, reflexivity])).
% 0.45/0.69 fof(inner_pasch,axiom,(![X]:(![U]:(![Z]:(![Y]:(![V]:((between(X,U,Z)&between(Y,V,Z))=>(?[A]:(between(U,A,Y)&between(V,A,X))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', inner_pasch)).
% 0.45/0.69 fof(c24,plain,(![X]:(![U]:(![Z]:(![Y]:(![V]:((~between(X,U,Z)|~between(Y,V,Z))|(?[A]:(between(U,A,Y)&between(V,A,X))))))))),inference(fof_nnf,[status(thm)],[inner_pasch])).
% 0.45/0.69 fof(c25,plain,(![X24]:(![X25]:(![X26]:(![X27]:(![X28]:((~between(X24,X25,X26)|~between(X27,X28,X26))|(?[X29]:(between(X25,X29,X27)&between(X28,X29,X24))))))))),inference(variable_rename,[status(thm)],[c24])).
% 0.45/0.69 fof(c26,plain,(![X24]:(![X25]:(![X26]:(![X27]:(![X28]:((~between(X24,X25,X26)|~between(X27,X28,X26))|(between(X25,skolem0007(X24,X25,X26,X27,X28),X27)&between(X28,skolem0007(X24,X25,X26,X27,X28),X24)))))))),inference(skolemize,[status(esa)],[c25])).
% 0.45/0.69 fof(c27,plain,(![X24]:(![X25]:(![X26]:(![X27]:(![X28]:(((~between(X24,X25,X26)|~between(X27,X28,X26))|between(X25,skolem0007(X24,X25,X26,X27,X28),X27))&((~between(X24,X25,X26)|~between(X27,X28,X26))|between(X28,skolem0007(X24,X25,X26,X27,X28),X24)))))))),inference(distribute,[status(thm)],[c26])).
% 0.45/0.69 cnf(c29,plain,~between(X142,X144,X146)|~between(X143,X145,X146)|between(X145,skolem0007(X142,X144,X146,X143,X145),X142),inference(split_conjunct,[status(thm)],[c27])).
% 0.45/0.69 cnf(c28,plain,~between(X128,X130,X132)|~between(X129,X131,X132)|between(X130,skolem0007(X128,X130,X132,X129,X131),X129),inference(split_conjunct,[status(thm)],[c27])).
% 0.45/0.69 cnf(c70,plain,~between(X133,X134,X135)|between(X134,skolem0007(X133,X134,X135,X133,X134),X133),inference(factor,[status(thm)],[c28])).
% 0.45/0.69 fof(segment_construction,axiom,(![X]:(![Y]:(![A]:(![B]:(?[Z]:(between(X,Y,Z)=>equidistant(Y,Z,A,B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', segment_construction)).
% 0.45/0.69 fof(c36,plain,(![X]:(![Y]:(![A]:(![B]:(?[Z]:(~between(X,Y,Z)|equidistant(Y,Z,A,B))))))),inference(fof_nnf,[status(thm)],[segment_construction])).
% 0.45/0.69 fof(c37,plain,(![X]:(![Y]:((?[Z]:~between(X,Y,Z))|(![A]:(![B]:(?[Z]:equidistant(Y,Z,A,B))))))),inference(shift_quantors,[status(thm)],[c36])).
% 0.45/0.69 fof(c38,plain,(![X40]:(![X41]:((?[X42]:~between(X40,X41,X42))|(![X43]:(![X44]:(?[X45]:equidistant(X41,X45,X43,X44))))))),inference(variable_rename,[status(thm)],[c37])).
% 0.45/0.69 fof(c40,plain,(![X40]:(![X41]:(![X43]:(![X44]:(~between(X40,X41,skolem0008(X40,X41))|equidistant(X41,skolem0009(X40,X41,X43,X44),X43,X44)))))),inference(shift_quantors,[status(thm)],[fof(c39,plain,(![X40]:(![X41]:(~between(X40,X41,skolem0008(X40,X41))|(![X43]:(![X44]:equidistant(X41,skolem0009(X40,X41,X43,X44),X43,X44)))))),inference(skolemize,[status(esa)],[c38])).])).
% 0.45/0.69 cnf(c41,plain,~between(X126,X124,skolem0008(X126,X124))|equidistant(X124,skolem0009(X126,X124,X127,X125),X127,X125),inference(split_conjunct,[status(thm)],[c40])).
% 0.45/0.69 cnf(c62,plain,~equidistant(X110,X113,X111,X112)|equidistant(X111,X112,X110,X113),inference(resolution,[status(thm)],[c59, c49])).
% 0.45/0.69 cnf(c58,plain,~equidistant(X104,X105,X102,X103)|equidistant(X102,X103,X105,X104),inference(resolution,[status(thm)],[c49, c51])).
% 0.45/0.69 cnf(c1,axiom,X99!=X97|X98!=X100|X95!=X96|~between(X99,X98,X95)|between(X97,X100,X96),theory(equality)).
% 0.45/0.69 fof(identity_for_equidistance,axiom,(![X]:(![Y]:(![Z]:(equidistant(X,Y,Z,Z)=>X=Y)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', identity_for_equidistance)).
% 0.45/0.69 fof(c42,plain,(![X]:(![Y]:(![Z]:(~equidistant(X,Y,Z,Z)|X=Y)))),inference(fof_nnf,[status(thm)],[identity_for_equidistance])).
% 0.45/0.69 fof(c43,plain,(![X]:(![Y]:((![Z]:~equidistant(X,Y,Z,Z))|X=Y))),inference(shift_quantors,[status(thm)],[c42])).
% 0.45/0.69 fof(c45,plain,(![X46]:(![X47]:(![X48]:(~equidistant(X46,X47,X48,X48)|X46=X47)))),inference(shift_quantors,[status(thm)],[fof(c44,plain,(![X46]:(![X47]:((![X48]:~equidistant(X46,X47,X48,X48))|X46=X47))),inference(variable_rename,[status(thm)],[c43])).])).
% 0.45/0.69 cnf(c46,plain,~equidistant(X80,X81,X79,X79)|X80=X81,inference(split_conjunct,[status(thm)],[c45])).
% 0.45/0.69 fof(identity_for_betweeness,axiom,(![X]:(![Y]:(between(X,Y,X)=>X=Y))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', identity_for_betweeness)).
% 0.45/0.69 fof(c30,plain,(![X]:(![Y]:(~between(X,Y,X)|X=Y))),inference(fof_nnf,[status(thm)],[identity_for_betweeness])).
% 0.45/0.69 fof(c31,plain,(![X30]:(![X31]:(~between(X30,X31,X30)|X30=X31))),inference(variable_rename,[status(thm)],[c30])).
% 0.45/0.69 cnf(c32,plain,~between(X69,X70,X69)|X69=X70,inference(split_conjunct,[status(thm)],[c31])).
% 0.45/0.69 fof(lower_dimension,axiom,(?[A]:(?[B]:(?[C]:(((~between(A,B,C))&(~between(B,C,A)))&(~between(C,A,B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', lower_dimension)).
% 0.45/0.69 fof(c18,plain,(?[A]:(?[B]:(?[C]:((~between(A,B,C)&~between(B,C,A))&~between(C,A,B))))),inference(fof_simplification,[status(thm)],[lower_dimension])).
% 0.45/0.69 fof(c19,plain,(?[X21]:(?[X22]:(?[X23]:((~between(X21,X22,X23)&~between(X22,X23,X21))&~between(X23,X21,X22))))),inference(variable_rename,[status(thm)],[c18])).
% 0.45/0.69 fof(c20,plain,((~between(skolem0004,skolem0005,skolem0006)&~between(skolem0005,skolem0006,skolem0004))&~between(skolem0006,skolem0004,skolem0005)),inference(skolemize,[status(esa)],[c19])).
% 0.45/0.69 cnf(c23,plain,~between(skolem0006,skolem0004,skolem0005),inference(split_conjunct,[status(thm)],[c20])).
% 0.45/0.69 cnf(c22,plain,~between(skolem0005,skolem0006,skolem0004),inference(split_conjunct,[status(thm)],[c20])).
% 0.45/0.69 cnf(transitivity,axiom,X64!=X63|X63!=X65|X64=X65,theory(equality)).
% 0.45/0.69 cnf(c21,plain,~between(skolem0004,skolem0005,skolem0006),inference(split_conjunct,[status(thm)],[c20])).
% 0.45/0.69 cnf(symmetry,axiom,X61!=X60|X60=X61,theory(equality)).
% 0.45/0.69 % SZS output end Saturation
% 0.45/0.69
% 0.45/0.69 % Initial clauses : 22
% 0.45/0.69 % Processed clauses : 76
% 0.45/0.69 % Factors computed : 57
% 0.45/0.69 % Resolvents computed: 71
% 0.45/0.69 % Tautologies deleted: 5
% 0.45/0.69 % Forward subsumed : 69
% 0.45/0.69 % Backward subsumed : 14
% 0.45/0.69 % -------- CPU Time ---------
% 0.45/0.69 % User time : 0.333 s
% 0.45/0.69 % System time : 0.018 s
% 0.45/0.69 % Total time : 0.351 s
%------------------------------------------------------------------------------