%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GEO040-3 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:25:37 PM UTC 2026
% Result : Unsatisfiable 36.51s 5.03s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO040-3 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.34 % Computer : n017.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sun Sep 20 08:29:42 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 36.51/5.03 % Refutation found
% 36.51/5.03 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 36.51/5.03 % SZS output start CNFRefutation for theBenchmark
% 36.51/5.03 fof(f1,axiom,(
% 36.51/5.03 (![X,Y]: (equidistant(X,Y,Y,X) ))),
% 36.51/5.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 36.51/5.03 fof(f3,axiom,(
% 36.51/5.03 (![X,Y,Z]: (( ~ equidistant(X,Y,Z,Z)| X = Y ) ))),
% 36.51/5.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 36.51/5.03 fof(f4,axiom,(
% 36.51/5.03 (![X,Y,W,V]: (between(X,Y,extension(X,Y,W,V)) ))),
% 36.51/5.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 36.51/5.03 fof(f5,axiom,(
% 36.51/5.03 (![Y,X,W,V]: (equidistant(Y,extension(X,Y,W,V),W,V) ))),
% 36.51/5.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 36.51/5.03 fof(f6,axiom,(
% 36.51/5.03 (![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) ) ))),
% 36.51/5.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 36.51/5.03 fof(f7,axiom,(
% 36.51/5.03 (![X,Y]: (( ~ between(X,Y,X)| X = Y ) ))),
% 36.51/5.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 36.51/5.03 fof(f8,axiom,(
% 36.51/5.03 (![U,V,W,Y,X]: (( ~ between(U,V,W)| ~ between(Y,X,W)| between(V,inner_pasch(U,V,W,X,Y),Y) ) ))),
% 36.51/5.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 36.51/5.03 fof(f9,axiom,(
% 36.51/5.03 (![U,V,W,Y,X]: (( ~ between(U,V,W)| ~ between(Y,X,W)| between(X,inner_pasch(U,V,W,X,Y),U) ) ))),
% 36.51/5.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 36.51/5.03 fof(f18,axiom,(
% 36.51/5.03 (![U,V,V1,X,X1,W]: (( ~ equidistant(U,V,U,V1)| ~ equidistant(U,X,U,X1)| ~ between(U,V,X)| ~ between(V,W,X)| equidistant(U,W,U,continuous(U,V,V1,W,X,X1)) ) ))),
% 36.51/5.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 36.51/5.03 fof(f19,axiom,(
% 36.51/5.03 (![U,V]: (reflection(U,V) = extension(U,V,U,V) ))),
% 36.51/5.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 36.51/5.03 fof(f20,axiom,(
% 36.51/5.03 (![U,V]: (equidistant(U,V,U,V) ))),
% 36.51/5.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 36.51/5.03 fof(f21,axiom,(
% 36.51/5.03 (![U,V,W,X]: (( ~ equidistant(U,V,W,X)| equidistant(W,X,U,V) ) ))),
% 36.51/5.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 36.51/5.03 fof(f31,axiom,(
% 36.51/5.03 (![U,V]: (between(U,V,reflection(U,V)) ))),
% 36.51/5.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 36.51/5.03 fof(f32,axiom,(
% 36.51/5.03 (![V,U]: (equidistant(V,reflection(U,V),U,V) ))),
% 36.51/5.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 36.51/5.03 fof(f33,axiom,(
% 36.51/5.03 (![U,V]: (( U != V| V = reflection(U,V) ) ))),
% 36.51/5.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 36.51/5.03 fof(f38,axiom,(
% 36.51/5.03 (![U,V,W,X]: (( ~ between(U,V,W)| ~ between(U,V,X)| ~ equidistant(V,W,V,X)| U = V| W = X ) ))),
% 36.51/5.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 36.51/5.03 fof(f39,axiom,(
% 36.51/5.03 (![U,V,W]: (( ~ between(U,V,W)| U = V| W = extension(U,V,V,W) ) ))),
% 36.51/5.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 36.51/5.03 fof(f40,axiom,(
% 36.51/5.03 (![W,X,Y,Z,U,V]: (( ~ equidistant(W,X,Y,Z)| extension(U,V,W,X) = extension(U,V,Y,Z)| U = V ) ))),
% 36.51/5.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 36.51/5.03 fof(f41,axiom,(
% 36.51/5.03 (![U,V]: (( extension(U,V,U,V) = extension(U,V,V,U)| U = V ) ))),
% 36.51/5.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 36.51/5.03 fof(f43,axiom,(
% 36.51/5.03 (![U,V]: (U = reflection(reflection(U,V),V) ))),
% 36.51/5.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 36.51/5.03 fof(f44,axiom,(
% 36.51/5.03 (![U,V]: (between(U,V,V) ))),
% 36.51/5.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 36.51/5.03 fof(f45,axiom,(
% 36.51/5.03 (![U,W,X,V]: (( ~ between(U,W,X)| U != X| between(V,W,X) ) ))),
% 36.51/5.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 36.51/5.03 fof(f46,axiom,(
% 36.51/5.03 (![U,V,W]: (( ~ between(U,V,W)| between(W,V,U) ) ))),
% 36.51/5.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 36.51/5.03 fof(f47,axiom,(
% 36.51/5.03 (![U,V]: (between(U,U,V) ))),
% 36.51/5.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 36.51/5.03 fof(f48,hypothesis,(
% 36.51/5.03 between(u,v,w) ),
% 36.51/5.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 36.51/5.03 fof(f49,hypothesis,(
% 36.51/5.03 between(v,u,w) ),
% 36.51/5.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 36.51/5.03 fof(f50,negated_conjecture,(
% 36.51/5.03 u != v ),
% 36.51/5.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 36.51/5.03 fof(f51,plain,(
% 36.51/5.03 ![X0,X1]: (equidistant(X0,X1,X1,X0))),
% 36.51/5.03 inference(cnf_transformation,[status(thm)],[f1])).
% 36.51/5.03 fof(f54,plain,(
% 36.51/5.03 ![X,Y]: ((![Z]: ~equidistant(X,Y,Z,Z))|X=Y)),
% 36.51/5.03 inference(miniscoping,[status(thm)],[f3])).
% 36.51/5.03 fof(f55,plain,(
% 36.51/5.03 ![X0,X1,X2]: (~equidistant(X0,X1,X2,X2)|X0=X1)),
% 36.51/5.03 inference(cnf_transformation,[status(thm)],[f54])).
% 36.51/5.03 fof(f56,plain,(
% 36.51/5.03 ![X0,X1,X2,X3]: (between(X0,X1,extension(X0,X1,X2,X3)))),
% 36.51/5.03 inference(cnf_transformation,[status(thm)],[f4])).
% 36.51/5.03 fof(f57,plain,(
% 36.51/5.03 ![X0,X1,X2,X3]: (equidistant(X0,extension(X1,X0,X2,X3),X2,X3))),
% 36.51/5.03 inference(cnf_transformation,[status(thm)],[f5])).
% 36.51/5.03 fof(f58,plain,(
% 36.51/5.03 ![Z,Z1,V,V1]: ((![X,Y]: ((![X1,Y1]: (((((~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))),
% 36.51/5.03 inference(miniscoping,[status(thm)],[f6])).
% 36.51/5.03 fof(f59,plain,(
% 36.51/5.03 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~equidistant(X0,X1,X2,X3)|~equidistant(X1,X4,X3,X5)|~equidistant(X0,X6,X2,X7)|~equidistant(X1,X6,X3,X7)|~between(X0,X1,X4)|~between(X2,X3,X5)|X0=X1|equidistant(X4,X6,X5,X7))),
% 36.51/5.03 inference(cnf_transformation,[status(thm)],[f58])).
% 36.51/5.03 fof(f60,plain,(
% 36.51/5.03 ![X0,X1]: (~between(X0,X1,X0)|X0=X1)),
% 36.51/5.03 inference(cnf_transformation,[status(thm)],[f7])).
% 36.51/5.03 fof(f61,plain,(
% 36.51/5.03 ![X0,X1,X2,X3,X4]: (~between(X0,X1,X2)|~between(X3,X4,X2)|between(X1,inner_pasch(X0,X1,X2,X4,X3),X3))),
% 36.51/5.03 inference(cnf_transformation,[status(thm)],[f8])).
% 36.51/5.03 fof(f62,plain,(
% 36.51/5.03 ![X0,X1,X2,X3,X4]: (~between(X0,X1,X2)|~between(X3,X4,X2)|between(X4,inner_pasch(X0,X1,X2,X4,X3),X0))),
% 36.51/5.03 inference(cnf_transformation,[status(thm)],[f9])).
% 36.51/5.03 fof(f72,plain,(
% 36.51/5.03 ![X0,X1,X2,X3,X4,X5]: (~equidistant(X0,X1,X0,X2)|~equidistant(X0,X3,X0,X4)|~between(X0,X1,X3)|~between(X1,X5,X3)|equidistant(X0,X5,X0,continuous(X0,X1,X2,X5,X3,X4)))),
% 36.51/5.03 inference(cnf_transformation,[status(thm)],[f18])).
% 36.51/5.03 fof(f73,plain,(
% 36.51/5.03 ![X0,X1]: (reflection(X0,X1)=extension(X0,X1,X0,X1))),
% 36.51/5.03 inference(cnf_transformation,[status(thm)],[f19])).
% 36.51/5.03 fof(f74,plain,(
% 36.51/5.03 ![X0,X1]: (equidistant(X0,X1,X0,X1))),
% 36.51/5.03 inference(cnf_transformation,[status(thm)],[f20])).
% 36.51/5.03 fof(f75,plain,(
% 36.51/5.03 ![X0,X1,X2,X3]: (~equidistant(X0,X1,X2,X3)|equidistant(X2,X3,X0,X1))),
% 36.51/5.03 inference(cnf_transformation,[status(thm)],[f21])).
% 36.51/5.03 fof(f87,plain,(
% 36.51/5.03 ![X0,X1]: (between(X0,X1,reflection(X0,X1)))),
% 36.51/5.03 inference(cnf_transformation,[status(thm)],[f31])).
% 36.51/5.03 fof(f88,plain,(
% 36.51/5.03 ![X0,X1]: (equidistant(X0,reflection(X1,X0),X1,X0))),
% 36.51/5.03 inference(cnf_transformation,[status(thm)],[f32])).
% 36.51/5.03 fof(f89,plain,(
% 36.51/5.03 ![X0,X1]: (~X0=X1|X1=reflection(X0,X1))),
% 36.51/5.03 inference(cnf_transformation,[status(thm)],[f33])).
% 36.51/5.03 fof(f95,plain,(
% 36.51/5.03 ![W,X]: ((![U,V]: (((~between(U,V,W)|~between(U,V,X))|~equidistant(V,W,V,X))|U=V))|W=X)),
% 36.51/5.03 inference(miniscoping,[status(thm)],[f38])).
% 36.51/5.03 fof(f96,plain,(
% 36.51/5.03 ![X0,X1,X2,X3]: (~between(X0,X1,X2)|~between(X0,X1,X3)|~equidistant(X1,X2,X1,X3)|X0=X1|X2=X3)),
% 36.51/5.03 inference(cnf_transformation,[status(thm)],[f95])).
% 36.51/5.03 fof(f97,plain,(
% 36.51/5.03 ![X0,X1,X2]: (~between(X0,X1,X2)|X0=X1|X2=extension(X0,X1,X1,X2))),
% 36.51/5.03 inference(cnf_transformation,[status(thm)],[f39])).
% 36.51/5.03 fof(f98,plain,(
% 36.51/5.03 ![U,V]: ((![W,X,Y,Z]: (~equidistant(W,X,Y,Z)|extension(U,V,W,X)=extension(U,V,Y,Z)))|U=V)),
% 36.51/5.03 inference(miniscoping,[status(thm)],[f40])).
% 36.51/5.03 fof(f99,plain,(
% 36.51/5.03 ![X0,X1,X2,X3,X4,X5]: (~equidistant(X0,X1,X2,X3)|extension(X4,X5,X0,X1)=extension(X4,X5,X2,X3)|X4=X5)),
% 36.51/5.03 inference(cnf_transformation,[status(thm)],[f98])).
% 36.51/5.03 fof(f100,plain,(
% 36.51/5.03 ![X0,X1]: (extension(X0,X1,X0,X1)=extension(X0,X1,X1,X0)|X0=X1)),
% 36.51/5.03 inference(cnf_transformation,[status(thm)],[f41])).
% 36.51/5.03 fof(f102,plain,(
% 36.51/5.03 ![X0,X1]: (X0=reflection(reflection(X0,X1),X1))),
% 36.51/5.03 inference(cnf_transformation,[status(thm)],[f43])).
% 36.51/5.03 fof(f103,plain,(
% 36.51/5.03 ![X0,X1]: (between(X0,X1,X1))),
% 36.51/5.03 inference(cnf_transformation,[status(thm)],[f44])).
% 36.51/5.03 fof(f104,plain,(
% 36.51/5.03 ![W,X]: ((![U]: (~between(U,W,X)|~U=X))|(![V]: between(V,W,X)))),
% 36.51/5.03 inference(miniscoping,[status(thm)],[f45])).
% 36.51/5.03 fof(f105,plain,(
% 36.51/5.03 ![X0,X1,X2,X3]: (~between(X0,X1,X2)|~X0=X2|between(X3,X1,X2))),
% 36.51/5.03 inference(cnf_transformation,[status(thm)],[f104])).
% 36.51/5.03 fof(f106,plain,(
% 36.51/5.03 ![X0,X1,X2]: (~between(X0,X1,X2)|between(X2,X1,X0))),
% 36.51/5.03 inference(cnf_transformation,[status(thm)],[f46])).
% 36.51/5.03 fof(f107,plain,(
% 36.51/5.03 ![X0,X1]: (between(X0,X0,X1))),
% 36.51/5.03 inference(cnf_transformation,[status(thm)],[f47])).
% 36.51/5.03 fof(f108,plain,(
% 36.51/5.03 between(u,v,w)),
% 36.51/5.03 inference(cnf_transformation,[status(thm)],[f48])).
% 36.51/5.03 fof(f109,plain,(
% 36.51/5.03 between(v,u,w)),
% 36.51/5.03 inference(cnf_transformation,[status(thm)],[f49])).
% 36.51/5.03 fof(f110,plain,(
% 36.51/5.03 ~u=v),
% 36.51/5.03 inference(cnf_transformation,[status(thm)],[f50])).
% 36.51/5.03 fof(f112,plain,(
% 36.51/5.03 ![X0]: (X0=reflection(X0,X0))),
% 36.51/5.03 inference(destructive_equality_resolution,[status(thm)],[f89])).
% 36.51/5.03 fof(f113,plain,(
% 36.51/5.03 ![X0,X1,X2]: (~between(X0,X1,X0)|between(X2,X1,X0))),
% 36.51/5.03 inference(destructive_equality_resolution,[status(thm)],[f105])).
% 36.51/5.03 fof(f126,plain,(
% 36.51/5.03 ![X0,X1]: (between(reflection(X0,X1),X1,X0))),
% 36.51/5.03 inference(paramodulation,[status(thm)],[f102,f87])).
% 36.51/5.03 fof(f134,plain,(
% 36.51/5.03 ![X0,X1,X2,X3,X4,X5,X6]: (~equidistant(X0,X1,X2,X3)|~equidistant(X1,X4,X3,X5)|~equidistant(X0,X6,X2,X5)|~equidistant(X1,X6,X3,X5)|~between(X0,X1,X4)|~between(X2,X3,X5)|X0=X1|X4=X6)),
% 36.51/5.03 inference(resolution,[status(thm)],[f59,f55])).
% 36.51/5.03 fof(f144,plain,(
% 36.51/5.03 ![X0,X1,X2,X3]: (~between(X0,X1,X2)|~between(X1,X3,X2)|X1=inner_pasch(X0,X1,X2,X3,X1))),
% 36.51/5.03 inference(resolution,[status(thm)],[f61,f60])).
% 36.51/5.03 fof(f145,plain,(
% 36.51/5.03 ![X0,X1,X2,X3,X4]: (between(X0,inner_pasch(X1,X2,X3,X4,X2),X2)|~between(X1,X2,X3)|~between(X2,X4,X3))),
% 36.51/5.03 inference(resolution,[status(thm)],[f113,f61])).
% 36.51/5.03 fof(f156,plain,(
% 36.51/5.03 ![X0,X1,X2,X3,X4]: (~between(X0,X1,X2)|~between(X3,X0,X2)|between(X4,inner_pasch(X0,X1,X2,X0,X3),X0))),
% 36.51/5.03 inference(resolution,[status(thm)],[f62,f113])).
% 36.51/5.03 fof(f188,plain,(
% 36.51/5.03 ![X0,X1,X2]: (~equidistant(X0,X0,X1,X2)|X1=X2)),
% 36.51/5.03 inference(resolution,[status(thm)],[f75,f55])).
% 36.51/5.03 fof(f235,plain,(
% 36.51/5.03 v=u|w=extension(v,u,u,w)),
% 36.51/5.03 inference(resolution,[status(thm)],[f97,f109])).
% 36.51/5.03 fof(f236,plain,(
% 36.51/5.03 u=v|w=extension(u,v,v,w)),
% 36.51/5.03 inference(resolution,[status(thm)],[f97,f108])).
% 36.51/5.03 fof(f241,plain,(
% 36.51/5.03 ![X0,X1,X2,X3]: (X0=X1|extension(X0,X1,X2,X3)=extension(X0,X1,X1,extension(X0,X1,X2,X3)))),
% 36.51/5.03 inference(resolution,[status(thm)],[f97,f56])).
% 36.51/5.03 fof(f243,plain,(
% 36.51/5.03 ![X0,X1,X2]: (X0=X1|X2=extension(X0,X1,X1,X2)|~between(X2,X1,X0))),
% 36.51/5.03 inference(resolution,[status(thm)],[f97,f106])).
% 36.51/5.03 fof(f246,definition,(
% 36.51/5.03 sQ0_spl <=> (v=u)),
% 36.51/5.03 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 36.51/5.03 fof(f247,plain,(
% 36.51/5.03 v=u|~sQ0_spl),
% 36.51/5.03 inference(component_clause,[status(thm)],[f246])).
% 36.51/5.03 fof(f249,definition,(
% 36.51/5.03 sQ1_spl <=> (w=extension(v,u,u,w))),
% 36.51/5.03 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 36.51/5.03 fof(f250,plain,(
% 36.51/5.03 w=extension(v,u,u,w)|~sQ1_spl),
% 36.51/5.03 inference(component_clause,[status(thm)],[f249])).
% 36.51/5.03 fof(f252,plain,(
% 36.51/5.03 sQ0_spl|sQ1_spl),
% 36.51/5.03 inference(split_clause,[status(thm)],[f235,f246,f249])).
% 36.51/5.03 fof(f253,definition,(
% 36.51/5.03 sQ2_spl <=> (w=extension(u,v,v,w))),
% 36.51/5.03 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 36.51/5.03 fof(f254,plain,(
% 36.51/5.03 w=extension(u,v,v,w)|~sQ2_spl),
% 36.51/5.03 inference(component_clause,[status(thm)],[f253])).
% 36.51/5.03 fof(f256,plain,(
% 36.51/5.03 sQ0_spl|sQ2_spl),
% 36.51/5.03 inference(split_clause,[status(thm)],[f236,f246,f253])).
% 36.51/5.03 fof(f257,plain,(
% 36.51/5.03 $false|~sQ0_spl),
% 36.51/5.03 inference(forward_subsumption_resolution,[status(thm)],[f247,f110])).
% 36.51/5.03 fof(f258,plain,(
% 36.51/5.03 ~sQ0_spl),
% 36.51/5.03 inference(contradiction_clause,[status(thm)],[f257])).
% 36.51/5.03 fof(f266,plain,(
% 36.51/5.03 ![X0,X1]: (reflection(X0,X1)=extension(X0,X1,X1,X0)|X0=X1)),
% 36.51/5.03 inference(forward_demodulation,[status(thm)],[f73,f100])).
% 36.51/5.03 fof(f270,plain,(
% 36.51/5.03 ![X0,X1]: (equidistant(X0,reflection(X1,X0),X0,X1)|X1=X0)),
% 36.51/5.03 inference(paramodulation,[status(thm)],[f266,f57])).
% 36.51/5.03 fof(f299,plain,(
% 36.51/5.03 w=u|v=extension(w,u,u,v)),
% 36.51/5.03 inference(resolution,[status(thm)],[f243,f109])).
% 36.51/5.03 fof(f311,definition,(
% 36.51/5.03 sQ3_spl <=> (w=u)),
% 36.51/5.03 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 36.51/5.03 fof(f312,plain,(
% 36.51/5.03 w=u|~sQ3_spl),
% 36.51/5.03 inference(component_clause,[status(thm)],[f311])).
% 36.51/5.03 fof(f314,definition,(
% 36.51/5.03 sQ4_spl <=> (v=extension(w,u,u,v))),
% 36.51/5.03 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 36.51/5.03 fof(f315,plain,(
% 36.51/5.03 v=extension(w,u,u,v)|~sQ4_spl),
% 36.51/5.03 inference(component_clause,[status(thm)],[f314])).
% 36.51/5.03 fof(f317,plain,(
% 36.51/5.03 sQ3_spl|sQ4_spl),
% 36.51/5.03 inference(split_clause,[status(thm)],[f299,f311,f314])).
% 36.51/5.03 fof(f318,definition,(
% 36.51/5.03 sQ5_spl <=> (w=v)),
% 36.51/5.03 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 36.51/5.03 fof(f319,plain,(
% 36.51/5.03 w=v|~sQ5_spl),
% 36.51/5.03 inference(component_clause,[status(thm)],[f318])).
% 36.51/5.03 fof(f329,plain,(
% 36.51/5.03 ~u=w|~sQ5_spl),
% 36.51/5.03 inference(backward_demodulation,[status(thm)],[f319,f110])).
% 36.51/5.03 fof(f331,plain,(
% 36.51/5.03 ![X0,X1,X2,X3,X4]: (~equidistant(X0,X1,X0,X2)|~equidistant(X0,X3,X0,X4)|~between(X0,X1,X3)|~between(X1,X0,X3)|X0=continuous(X0,X1,X2,X0,X3,X4))),
% 36.51/5.03 inference(resolution,[status(thm)],[f72,f188])).
% 36.51/5.03 fof(f336,plain,(
% 36.51/5.03 $false|~sQ5_spl|~sQ3_spl),
% 36.51/5.03 inference(forward_subsumption_resolution,[status(thm)],[f312,f329])).
% 36.51/5.03 fof(f337,plain,(
% 36.51/5.03 ~sQ5_spl|~sQ3_spl),
% 36.51/5.03 inference(contradiction_clause,[status(thm)],[f336])).
% 36.51/5.03 fof(f353,plain,(
% 36.51/5.03 between(w,u,v)|~sQ4_spl),
% 36.51/5.03 inference(paramodulation,[status(thm)],[f315,f56])).
% 36.51/5.03 fof(f374,plain,(
% 36.51/5.03 ![X0]: (~between(u,v,X0)|~equidistant(v,X0,v,w)|u=v|X0=w)),
% 36.51/5.03 inference(resolution,[status(thm)],[f96,f108])).
% 36.51/5.03 fof(f375,plain,(
% 36.51/5.03 ![X0]: (~between(v,u,X0)|~equidistant(u,X0,u,w)|v=u|X0=w)),
% 36.51/5.03 inference(resolution,[status(thm)],[f96,f109])).
% 36.51/5.03 fof(f383,plain,(
% 36.51/5.03 ![X0,X1,X2,X3,X4]: (~between(X0,X1,X2)|~equidistant(X1,X2,X1,extension(X0,X1,X3,X4))|X0=X1|X2=extension(X0,X1,X3,X4))),
% 36.51/5.03 inference(resolution,[status(thm)],[f96,f56])).
% 36.51/5.03 fof(f396,definition,(
% 36.51/5.03 ![X0]: (sQ9_spl <=> (~between(u,v,X0)|~equidistant(v,X0,v,w)|X0=w))),
% 36.51/5.03 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 36.51/5.03 fof(f397,plain,(
% 36.51/5.03 ![X0]: (~between(u,v,X0)|~equidistant(v,X0,v,w)|X0=w|~sQ9_spl)),
% 36.51/5.03 inference(component_clause,[status(thm)],[f396])).
% 36.51/5.03 fof(f399,plain,(
% 36.51/5.03 sQ9_spl|sQ0_spl),
% 36.51/5.03 inference(split_clause,[status(thm)],[f374,f396,f246])).
% 36.51/5.03 fof(f400,definition,(
% 36.51/5.03 ![X0]: (sQ10_spl <=> (~between(v,u,X0)|~equidistant(u,X0,u,w)|X0=w))),
% 36.51/5.03 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 36.51/5.03 fof(f403,plain,(
% 36.51/5.03 sQ10_spl|sQ0_spl),
% 36.51/5.03 inference(split_clause,[status(thm)],[f375,f400,f246])).
% 36.51/5.03 fof(f411,plain,(
% 36.51/5.03 ![X0,X1,X2,X3]: (extension(X0,X1,X2,reflection(X3,X2))=extension(X0,X1,X3,X2)|X0=X1)),
% 36.51/5.03 inference(resolution,[status(thm)],[f99,f88])).
% 36.51/5.03 fof(f428,plain,(
% 36.51/5.03 ![X0,X1,X2,X3]: (extension(X0,X1,X2,X3)=extension(X0,X1,X3,X2)|X0=X1)),
% 36.51/5.03 inference(resolution,[status(thm)],[f99,f51])).
% 36.51/5.03 fof(f446,plain,(
% 36.51/5.03 between(w,v,w)|~sQ3_spl),
% 36.51/5.03 inference(forward_demodulation,[status(thm)],[f312,f108])).
% 36.51/5.03 fof(f451,plain,(
% 36.51/5.03 w=v|~sQ3_spl),
% 36.51/5.03 inference(resolution,[status(thm)],[f446,f60])).
% 36.51/5.03 fof(f461,plain,(
% 36.51/5.03 sQ5_spl|~sQ3_spl),
% 36.51/5.03 inference(split_clause,[status(thm)],[f451,f318,f311])).
% 36.51/5.03 fof(f497,plain,(
% 36.51/5.03 ![X0,X1,X2,X3]: (~equidistant(X0,X1,v,u)|~equidistant(X1,X2,u,w)|~equidistant(X0,X3,v,w)|~equidistant(X1,X3,u,w)|~between(X0,X1,X2)|X0=X1|X2=X3)),
% 36.51/5.03 inference(resolution,[status(thm)],[f134,f109])).
% 36.51/5.03 fof(f499,plain,(
% 36.51/5.03 ![X0,X1,X2,X3,X4,X5]: (~equidistant(X0,X1,reflection(X2,X3),X3)|~equidistant(X1,X4,X3,X2)|~equidistant(X0,X5,reflection(X2,X3),X2)|~equidistant(X1,X5,X3,X2)|~between(X0,X1,X4)|X0=X1|X4=X5)),
% 36.51/5.03 inference(resolution,[status(thm)],[f134,f126])).
% 36.51/5.03 fof(f505,plain,(
% 36.51/5.03 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~equidistant(X0,X1,X2,X3)|~equidistant(X1,X4,X3,extension(X2,X3,X5,X6))|~equidistant(X0,X7,X2,extension(X2,X3,X5,X6))|~equidistant(X1,X7,X3,extension(X2,X3,X5,X6))|~between(X0,X1,X4)|X0=X1|X4=X7)),
% 36.51/5.03 inference(resolution,[status(thm)],[f134,f56])).
% 36.51/5.03 fof(f506,plain,(
% 36.51/5.03 ![X0,X1,X2,X3,X4,X5]: (~equidistant(X0,X1,X2,X3)|~equidistant(X1,X4,X3,reflection(X2,X3))|~equidistant(X0,X5,X2,reflection(X2,X3))|~equidistant(X1,X5,X3,reflection(X2,X3))|~between(X0,X1,X4)|X0=X1|X4=X5)),
% 36.51/5.03 inference(resolution,[status(thm)],[f134,f87])).
% 36.51/5.03 fof(f509,plain,(
% 36.51/5.03 ![X0,X1,X2,X3,X4,X5]: (~equidistant(X0,X1,X2,X3)|~equidistant(X1,X4,X3,X3)|~equidistant(X0,X5,X2,X3)|~equidistant(X1,X5,X3,X3)|~between(X0,X1,X4)|X0=X1|X4=X5)),
% 36.51/5.03 inference(resolution,[status(thm)],[f134,f103])).
% 36.51/5.03 fof(f510,plain,(
% 36.51/5.03 ![X0]: (~between(X0,u,w)|u=inner_pasch(X0,u,w,v,u))),
% 36.51/5.03 inference(resolution,[status(thm)],[f144,f108])).
% 36.51/5.03 fof(f524,plain,(
% 36.51/5.03 ![X0,X1,X2]: (~between(X0,X1,X2)|X1=inner_pasch(X0,X1,X2,X1,X1))),
% 36.51/5.03 inference(resolution,[status(thm)],[f144,f107])).
% 36.51/5.03 fof(f525,plain,(
% 36.51/5.03 ![X0,X1,X2]: (~between(X0,X1,X2)|X1=inner_pasch(X0,X1,X2,X2,X1))),
% 36.51/5.03 inference(resolution,[status(thm)],[f144,f103])).
% 36.51/5.03 fof(f527,plain,(
% 36.51/5.03 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~between(X0,X1,X2)|~between(X1,X3,X2)|~equidistant(X4,X5,X6,inner_pasch(X0,X1,X2,X3,X1))|~equidistant(X5,X7,inner_pasch(X0,X1,X2,X3,X1),X1)|~equidistant(X4,X8,X6,X1)|~equidistant(X5,X8,inner_pasch(X0,X1,X2,X3,X1),X1)|~between(X4,X5,X7)|X4=X5|X7=X8)),
% 36.51/5.03 inference(resolution,[status(thm)],[f145,f134])).
% 36.51/5.03 fof(f533,plain,(
% 36.51/5.03 v=inner_pasch(u,v,w,v,v)),
% 36.51/5.03 inference(resolution,[status(thm)],[f524,f108])).
% 36.51/5.03 fof(f563,plain,(
% 36.51/5.03 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~between(X0,X1,X2)|~between(X3,X0,X2)|~equidistant(X4,X5,X6,inner_pasch(X0,X1,X2,X0,X3))|~equidistant(X5,X7,inner_pasch(X0,X1,X2,X0,X3),X0)|~equidistant(X4,X8,X6,X0)|~equidistant(X5,X8,inner_pasch(X0,X1,X2,X0,X3),X0)|~between(X4,X5,X7)|X4=X5|X7=X8)),
% 36.51/5.03 inference(resolution,[status(thm)],[f156,f134])).
% 36.51/5.03 fof(f591,plain,(
% 36.51/5.03 v=inner_pasch(u,v,w,w,v)),
% 36.51/5.03 inference(resolution,[status(thm)],[f525,f108])).
% 36.51/5.03 fof(f592,plain,(
% 36.51/5.03 u=inner_pasch(w,u,v,v,u)|~sQ4_spl),
% 36.51/5.03 inference(resolution,[status(thm)],[f525,f353])).
% 36.51/5.03 fof(f1044,plain,(
% 36.51/5.03 w=extension(v,u,w,u)|v=u|~sQ1_spl),
% 36.51/5.03 inference(paramodulation,[status(thm)],[f250,f428])).
% 36.51/5.03 fof(f1045,plain,(
% 36.51/5.03 w=extension(u,v,w,v)|u=v|~sQ2_spl),
% 36.51/5.03 inference(paramodulation,[status(thm)],[f254,f428])).
% 36.51/5.03 fof(f1067,plain,(
% 36.51/5.03 ![X0,X1,X2,X3]: (equidistant(X0,extension(X1,X0,X2,X3),X3,X2)|X1=X0)),
% 36.51/5.03 inference(paramodulation,[status(thm)],[f428,f57])).
% 36.51/5.03 fof(f1085,definition,(
% 36.51/5.03 sQ20_spl <=> (w=extension(v,u,w,u))),
% 36.51/5.03 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 36.51/5.03 fof(f1086,plain,(
% 36.51/5.03 w=extension(v,u,w,u)|~sQ20_spl),
% 36.51/5.03 inference(component_clause,[status(thm)],[f1085])).
% 36.51/5.03 fof(f1088,plain,(
% 36.51/5.03 sQ20_spl|sQ0_spl|~sQ1_spl),
% 36.51/5.03 inference(split_clause,[status(thm)],[f1044,f1085,f246,f249])).
% 36.51/5.03 fof(f1089,definition,(
% 36.51/5.03 sQ21_spl <=> (w=extension(u,v,w,v))),
% 36.51/5.03 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 36.51/5.03 fof(f1090,plain,(
% 36.51/5.03 w=extension(u,v,w,v)|~sQ21_spl),
% 36.51/5.03 inference(component_clause,[status(thm)],[f1089])).
% 36.51/5.03 fof(f1092,plain,(
% 36.51/5.03 sQ21_spl|sQ0_spl|~sQ2_spl),
% 36.51/5.03 inference(split_clause,[status(thm)],[f1045,f1089,f246,f253])).
% 36.51/5.03 fof(f1138,plain,(
% 36.51/5.03 equidistant(u,w,u,w)|v=u|~sQ20_spl),
% 36.51/5.03 inference(paramodulation,[status(thm)],[f1086,f1067])).
% 36.51/5.03 fof(f1139,plain,(
% 36.51/5.03 equidistant(u,w,w,u)|v=u|~sQ1_spl),
% 36.51/5.03 inference(paramodulation,[status(thm)],[f250,f1067])).
% 36.51/5.03 fof(f1140,plain,(
% 36.51/5.03 equidistant(v,w,v,w)|u=v|~sQ21_spl),
% 36.51/5.03 inference(paramodulation,[status(thm)],[f1090,f1067])).
% 36.51/5.03 fof(f1141,plain,(
% 36.51/5.03 equidistant(v,w,w,v)|u=v|~sQ2_spl),
% 36.51/5.03 inference(paramodulation,[status(thm)],[f254,f1067])).
% 36.51/5.03 fof(f1163,definition,(
% 36.51/5.03 sQ25_spl <=> (equidistant(u,w,u,w))),
% 36.51/5.03 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 36.51/5.03 fof(f1166,plain,(
% 36.51/5.03 sQ25_spl|sQ0_spl|~sQ20_spl),
% 36.51/5.03 inference(split_clause,[status(thm)],[f1138,f1163,f246,f1085])).
% 36.51/5.03 fof(f1167,definition,(
% 36.51/5.03 sQ26_spl <=> (equidistant(u,w,w,u))),
% 36.51/5.03 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 36.51/5.03 fof(f1170,plain,(
% 36.51/5.03 sQ26_spl|sQ0_spl|~sQ1_spl),
% 36.51/5.03 inference(split_clause,[status(thm)],[f1139,f1167,f246,f249])).
% 36.51/5.03 fof(f1171,definition,(
% 36.51/5.03 sQ27_spl <=> (equidistant(v,w,v,w))),
% 36.51/5.03 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 36.51/5.03 fof(f1174,plain,(
% 36.51/5.03 sQ27_spl|sQ0_spl|~sQ21_spl),
% 36.51/5.03 inference(split_clause,[status(thm)],[f1140,f1171,f246,f1089])).
% 36.51/5.03 fof(f1175,definition,(
% 36.51/5.03 sQ28_spl <=> (equidistant(v,w,w,v))),
% 36.51/5.03 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 36.51/5.03 fof(f1178,plain,(
% 36.51/5.03 sQ28_spl|sQ0_spl|~sQ2_spl),
% 36.51/5.03 inference(split_clause,[status(thm)],[f1141,f1175,f246,f253])).
% 36.51/5.03 fof(f1200,plain,(
% 36.51/5.03 ![X0]: (between(X0,v,v)|~between(u,v,w)|~between(v,v,w))),
% 36.51/5.03 inference(paramodulation,[status(thm)],[f533,f145])).
% 36.51/5.03 fof(f1201,plain,(
% 36.51/5.03 ~between(u,v,w)|~between(v,v,w)|between(v,v,u)),
% 36.51/5.03 inference(paramodulation,[status(thm)],[f533,f62])).
% 36.51/5.04 fof(f1202,plain,(
% 36.51/5.04 ~between(u,v,w)|~between(v,v,w)|between(v,v,v)),
% 36.51/5.04 inference(paramodulation,[status(thm)],[f533,f61])).
% 36.51/5.04 fof(f1203,definition,(
% 36.51/5.04 ![X0]: (sQ29_spl <=> (between(X0,v,v)))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f1206,definition,(
% 36.51/5.04 sQ30_spl <=> (between(u,v,w))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f1208,plain,(
% 36.51/5.04 ~between(u,v,w)|sQ30_spl),
% 36.51/5.04 inference(component_clause,[status(thm)],[f1206])).
% 36.51/5.04 fof(f1209,definition,(
% 36.51/5.04 sQ31_spl <=> (between(v,v,w))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f1211,plain,(
% 36.51/5.04 ~between(v,v,w)|sQ31_spl),
% 36.51/5.04 inference(component_clause,[status(thm)],[f1209])).
% 36.51/5.04 fof(f1212,plain,(
% 36.51/5.04 sQ29_spl|~sQ30_spl|~sQ31_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f1200,f1203,f1206,f1209])).
% 36.51/5.04 fof(f1213,definition,(
% 36.51/5.04 sQ32_spl <=> (between(v,v,u))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f1216,plain,(
% 36.51/5.04 ~sQ30_spl|~sQ31_spl|sQ32_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f1201,f1206,f1209,f1213])).
% 36.51/5.04 fof(f1217,definition,(
% 36.51/5.04 sQ33_spl <=> (between(v,v,v))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f1220,plain,(
% 36.51/5.04 ~sQ30_spl|~sQ31_spl|sQ33_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f1202,f1206,f1209,f1217])).
% 36.51/5.04 fof(f1221,plain,(
% 36.51/5.04 $false|sQ31_spl),
% 36.51/5.04 inference(forward_subsumption_resolution,[status(thm)],[f1211,f107])).
% 36.51/5.04 fof(f1222,plain,(
% 36.51/5.04 sQ31_spl),
% 36.51/5.04 inference(contradiction_clause,[status(thm)],[f1221])).
% 36.51/5.04 fof(f1223,plain,(
% 36.51/5.04 $false|sQ30_spl),
% 36.51/5.04 inference(forward_subsumption_resolution,[status(thm)],[f1208,f108])).
% 36.51/5.04 fof(f1224,plain,(
% 36.51/5.04 sQ30_spl),
% 36.51/5.04 inference(contradiction_clause,[status(thm)],[f1223])).
% 36.51/5.04 fof(f1231,definition,(
% 36.51/5.04 sQ35_spl <=> (between(w,u,v))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f1233,plain,(
% 36.51/5.04 ~between(w,u,v)|sQ35_spl),
% 36.51/5.04 inference(component_clause,[status(thm)],[f1231])).
% 36.51/5.04 fof(f1234,definition,(
% 36.51/5.04 sQ36_spl <=> (between(u,u,v))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f1236,plain,(
% 36.51/5.04 ~between(u,u,v)|sQ36_spl),
% 36.51/5.04 inference(component_clause,[status(thm)],[f1234])).
% 36.51/5.04 fof(f1246,plain,(
% 36.51/5.04 $false|sQ36_spl),
% 36.51/5.04 inference(forward_subsumption_resolution,[status(thm)],[f1236,f107])).
% 36.51/5.04 fof(f1247,plain,(
% 36.51/5.04 sQ36_spl),
% 36.51/5.04 inference(contradiction_clause,[status(thm)],[f1246])).
% 36.51/5.04 fof(f1248,plain,(
% 36.51/5.04 $false|~sQ4_spl|sQ35_spl),
% 36.51/5.04 inference(forward_subsumption_resolution,[status(thm)],[f1233,f353])).
% 36.51/5.04 fof(f1249,plain,(
% 36.51/5.04 ~sQ4_spl|sQ35_spl),
% 36.51/5.04 inference(contradiction_clause,[status(thm)],[f1248])).
% 36.51/5.04 fof(f1272,definition,(
% 36.51/5.04 sQ39_spl <=> (between(w,v,u))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f1281,definition,(
% 36.51/5.04 sQ40_spl <=> (between(v,u,w))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f1288,plain,(
% 36.51/5.04 ~between(u,v,w)|~between(v,w,w)|between(w,v,u)),
% 36.51/5.04 inference(paramodulation,[status(thm)],[f591,f62])).
% 36.51/5.04 fof(f1290,definition,(
% 36.51/5.04 sQ41_spl <=> (between(v,w,w))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f1292,plain,(
% 36.51/5.04 ~between(v,w,w)|sQ41_spl),
% 36.51/5.04 inference(component_clause,[status(thm)],[f1290])).
% 36.51/5.04 fof(f1294,plain,(
% 36.51/5.04 ~sQ30_spl|~sQ41_spl|sQ39_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f1288,f1206,f1290,f1272])).
% 36.51/5.04 fof(f1296,plain,(
% 36.51/5.04 $false|sQ41_spl),
% 36.51/5.04 inference(forward_subsumption_resolution,[status(thm)],[f1292,f103])).
% 36.51/5.04 fof(f1297,plain,(
% 36.51/5.04 sQ41_spl),
% 36.51/5.04 inference(contradiction_clause,[status(thm)],[f1296])).
% 36.51/5.04 fof(f1299,plain,(
% 36.51/5.04 ~between(w,u,v)|~between(u,v,v)|between(v,u,w)|~sQ4_spl),
% 36.51/5.04 inference(paramodulation,[status(thm)],[f592,f62])).
% 36.51/5.04 fof(f1301,definition,(
% 36.51/5.04 sQ42_spl <=> (between(u,v,v))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f1303,plain,(
% 36.51/5.04 ~between(u,v,v)|sQ42_spl),
% 36.51/5.04 inference(component_clause,[status(thm)],[f1301])).
% 36.51/5.04 fof(f1305,plain,(
% 36.51/5.04 ~sQ35_spl|~sQ42_spl|sQ40_spl|~sQ4_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f1299,f1231,f1301,f1281,f314])).
% 36.51/5.04 fof(f1307,plain,(
% 36.51/5.04 $false|sQ42_spl),
% 36.51/5.04 inference(forward_subsumption_resolution,[status(thm)],[f1303,f103])).
% 36.51/5.04 fof(f1308,plain,(
% 36.51/5.04 sQ42_spl),
% 36.51/5.04 inference(contradiction_clause,[status(thm)],[f1307])).
% 36.51/5.04 fof(f1402,definition,(
% 36.51/5.04 sQ45_spl <=> (between(w,w,v))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f1404,plain,(
% 36.51/5.04 ~between(w,w,v)|sQ45_spl),
% 36.51/5.04 inference(component_clause,[status(thm)],[f1402])).
% 36.51/5.04 fof(f1414,plain,(
% 36.51/5.04 $false|sQ45_spl),
% 36.51/5.04 inference(forward_subsumption_resolution,[status(thm)],[f1404,f107])).
% 36.51/5.04 fof(f1415,plain,(
% 36.51/5.04 sQ45_spl),
% 36.51/5.04 inference(contradiction_clause,[status(thm)],[f1414])).
% 36.51/5.04 fof(f1602,plain,(
% 36.51/5.04 v=u|extension(v,u,w,u)=extension(v,u,u,w)|~sQ20_spl),
% 36.51/5.04 inference(paramodulation,[status(thm)],[f1086,f241])).
% 36.51/5.04 fof(f1603,plain,(
% 36.51/5.04 v=u|extension(v,u,u,w)=extension(v,u,u,w)|~sQ1_spl),
% 36.51/5.04 inference(paramodulation,[status(thm)],[f250,f241])).
% 36.51/5.04 fof(f1604,plain,(
% 36.51/5.04 u=v|extension(u,v,w,v)=extension(u,v,v,w)|~sQ21_spl),
% 36.51/5.04 inference(paramodulation,[status(thm)],[f1090,f241])).
% 36.51/5.04 fof(f1605,plain,(
% 36.51/5.04 u=v|extension(u,v,v,w)=extension(u,v,v,w)|~sQ2_spl),
% 36.51/5.04 inference(paramodulation,[status(thm)],[f254,f241])).
% 36.51/5.04 fof(f1632,definition,(
% 36.51/5.04 sQ52_spl <=> (extension(v,u,w,u)=extension(v,u,u,w))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f1635,plain,(
% 36.51/5.04 sQ0_spl|sQ52_spl|~sQ20_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f1602,f246,f1632,f1085])).
% 36.51/5.04 fof(f1636,definition,(
% 36.51/5.04 sQ53_spl <=> (extension(v,u,u,w)=extension(v,u,u,w))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f1639,plain,(
% 36.51/5.04 sQ0_spl|sQ53_spl|~sQ1_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f1603,f246,f1636,f249])).
% 36.51/5.04 fof(f1640,definition,(
% 36.51/5.04 sQ54_spl <=> (extension(u,v,w,v)=extension(u,v,v,w))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f1643,plain,(
% 36.51/5.04 sQ0_spl|sQ54_spl|~sQ21_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f1604,f246,f1640,f1089])).
% 36.51/5.04 fof(f1644,definition,(
% 36.51/5.04 sQ55_spl <=> (extension(u,v,v,w)=extension(u,v,v,w))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f1647,plain,(
% 36.51/5.04 sQ0_spl|sQ55_spl|~sQ2_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f1605,f246,f1644,f253])).
% 36.51/5.04 fof(f1980,plain,(
% 36.51/5.04 ![X0,X1,X2,X3]: (equidistant(X0,extension(X1,X0,X2,X3),reflection(X2,X3),X3)|X1=X0|X1=X0)),
% 36.51/5.04 inference(paramodulation,[status(thm)],[f411,f1067])).
% 36.51/5.04 fof(f1998,plain,(
% 36.51/5.04 ![X0,X1,X2,X3]: (equidistant(X0,extension(X1,X0,X2,X3),reflection(X2,X3),X3)|X1=X0)),
% 36.51/5.04 inference(duplicate_literals_removal,[status(thm)],[f1980])).
% 36.51/5.04 fof(f2019,plain,(
% 36.51/5.04 equidistant(u,w,reflection(w,u),u)|v=u|~sQ20_spl),
% 36.51/5.04 inference(paramodulation,[status(thm)],[f1086,f1998])).
% 36.51/5.04 fof(f2020,plain,(
% 36.51/5.04 equidistant(u,w,reflection(u,w),w)|v=u|~sQ1_spl),
% 36.51/5.04 inference(paramodulation,[status(thm)],[f250,f1998])).
% 36.51/5.04 fof(f2021,plain,(
% 36.51/5.04 equidistant(v,w,reflection(w,v),v)|u=v|~sQ21_spl),
% 36.51/5.04 inference(paramodulation,[status(thm)],[f1090,f1998])).
% 36.51/5.04 fof(f2022,plain,(
% 36.51/5.04 equidistant(v,w,reflection(v,w),w)|u=v|~sQ2_spl),
% 36.51/5.04 inference(paramodulation,[status(thm)],[f254,f1998])).
% 36.51/5.04 fof(f2048,definition,(
% 36.51/5.04 sQ59_spl <=> (equidistant(u,w,reflection(w,u),u))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f2051,plain,(
% 36.51/5.04 sQ59_spl|sQ0_spl|~sQ20_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f2019,f2048,f246,f1085])).
% 36.51/5.04 fof(f2052,definition,(
% 36.51/5.04 sQ60_spl <=> (equidistant(u,w,reflection(u,w),w))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f2055,plain,(
% 36.51/5.04 sQ60_spl|sQ0_spl|~sQ1_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f2020,f2052,f246,f249])).
% 36.51/5.04 fof(f2056,definition,(
% 36.51/5.04 sQ61_spl <=> (equidistant(v,w,reflection(w,v),v))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f2059,plain,(
% 36.51/5.04 sQ61_spl|sQ0_spl|~sQ21_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f2021,f2056,f246,f1089])).
% 36.51/5.04 fof(f2060,definition,(
% 36.51/5.04 sQ62_spl <=> (equidistant(v,w,reflection(v,w),w))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f2063,plain,(
% 36.51/5.04 sQ62_spl|sQ0_spl|~sQ2_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f2022,f2060,f246,f253])).
% 36.51/5.04 fof(f2415,definition,(
% 36.51/5.04 sQ90_spl <=> (reflection(v,u)=v)),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f2416,plain,(
% 36.51/5.04 reflection(v,u)=v|~sQ90_spl),
% 36.51/5.04 inference(component_clause,[status(thm)],[f2415])).
% 36.51/5.04 fof(f2448,plain,(
% 36.51/5.04 between(v,u,v)|~sQ90_spl),
% 36.51/5.04 inference(paramodulation,[status(thm)],[f2416,f126])).
% 36.51/5.04 fof(f2457,definition,(
% 36.51/5.04 sQ93_spl <=> (reflection(u,v)=v)),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f2458,plain,(
% 36.51/5.04 reflection(u,v)=v|~sQ93_spl),
% 36.51/5.04 inference(component_clause,[status(thm)],[f2457])).
% 36.51/5.04 fof(f2467,definition,(
% 36.51/5.04 sQ95_spl <=> (reflection(v,u)=u)),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f2468,plain,(
% 36.51/5.04 reflection(v,u)=u|~sQ95_spl),
% 36.51/5.04 inference(component_clause,[status(thm)],[f2467])).
% 36.51/5.04 fof(f2521,plain,(
% 36.51/5.04 v=u|~sQ90_spl),
% 36.51/5.04 inference(resolution,[status(thm)],[f2448,f60])).
% 36.51/5.04 fof(f2536,plain,(
% 36.51/5.04 sQ0_spl|~sQ90_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f2521,f246,f2415])).
% 36.51/5.04 fof(f2544,definition,(
% 36.51/5.04 sQ102_spl <=> (reflection(u,v)=u)),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f2545,plain,(
% 36.51/5.04 reflection(u,v)=u|~sQ102_spl),
% 36.51/5.04 inference(component_clause,[status(thm)],[f2544])).
% 36.51/5.04 fof(f2577,plain,(
% 36.51/5.04 between(u,v,u)|~sQ102_spl),
% 36.51/5.04 inference(paramodulation,[status(thm)],[f2545,f126])).
% 36.51/5.04 fof(f2618,plain,(
% 36.51/5.04 ![X0,X1]: (~equidistant(v,w,v,extension(u,v,X0,X1))|u=v|w=extension(u,v,X0,X1))),
% 36.51/5.04 inference(resolution,[status(thm)],[f383,f108])).
% 36.51/5.04 fof(f2621,plain,(
% 36.51/5.04 ![X0,X1]: (~equidistant(u,w,u,extension(v,u,X0,X1))|v=u|w=extension(v,u,X0,X1))),
% 36.51/5.04 inference(resolution,[status(thm)],[f383,f109])).
% 36.51/5.04 fof(f2636,definition,(
% 36.51/5.04 ![X0,X1]: (sQ109_spl <=> (~equidistant(v,w,v,extension(u,v,X0,X1))|w=extension(u,v,X0,X1)))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f2639,plain,(
% 36.51/5.04 sQ109_spl|sQ0_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f2618,f2636,f246])).
% 36.51/5.04 fof(f2648,definition,(
% 36.51/5.04 ![X0,X1]: (sQ112_spl <=> (~equidistant(u,w,u,extension(v,u,X0,X1))|w=extension(v,u,X0,X1)))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f2651,plain,(
% 36.51/5.04 sQ112_spl|sQ0_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f2621,f2648,f246])).
% 36.51/5.04 fof(f2753,plain,(
% 36.51/5.04 u=v|~sQ102_spl),
% 36.51/5.04 inference(resolution,[status(thm)],[f2577,f60])).
% 36.51/5.04 fof(f2777,plain,(
% 36.51/5.04 sQ0_spl|~sQ102_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f2753,f246,f2544])).
% 36.51/5.04 fof(f2784,plain,(
% 36.51/5.04 ~equidistant(v,w,v,w)|w=w|~sQ9_spl),
% 36.51/5.04 inference(resolution,[status(thm)],[f397,f108])).
% 36.51/5.04 fof(f2791,definition,(
% 36.51/5.04 sQ124_spl <=> (w=w)),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f2794,plain,(
% 36.51/5.04 ~sQ27_spl|sQ124_spl|~sQ9_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f2784,f1171,f2791,f396])).
% 36.51/5.04 fof(f2959,plain,(
% 36.51/5.04 v=reflection(u,u)|~sQ95_spl),
% 36.51/5.04 inference(paramodulation,[status(thm)],[f2468,f102])).
% 36.51/5.04 fof(f2999,plain,(
% 36.51/5.04 v=u|~sQ95_spl),
% 36.51/5.04 inference(forward_demodulation,[status(thm)],[f112,f2959])).
% 36.51/5.04 fof(f3000,plain,(
% 36.51/5.04 $false|~sQ95_spl),
% 36.51/5.04 inference(forward_subsumption_resolution,[status(thm)],[f2999,f110])).
% 36.51/5.04 fof(f3001,plain,(
% 36.51/5.04 ~sQ95_spl),
% 36.51/5.04 inference(contradiction_clause,[status(thm)],[f3000])).
% 36.51/5.04 fof(f3289,plain,(
% 36.51/5.04 u=reflection(v,v)|~sQ93_spl),
% 36.51/5.04 inference(paramodulation,[status(thm)],[f2458,f102])).
% 36.51/5.04 fof(f3329,plain,(
% 36.51/5.04 u=v|~sQ93_spl),
% 36.51/5.04 inference(forward_demodulation,[status(thm)],[f112,f3289])).
% 36.51/5.04 fof(f3330,plain,(
% 36.51/5.04 $false|~sQ93_spl),
% 36.51/5.04 inference(forward_subsumption_resolution,[status(thm)],[f3329,f110])).
% 36.51/5.04 fof(f3331,plain,(
% 36.51/5.04 ~sQ93_spl),
% 36.51/5.04 inference(contradiction_clause,[status(thm)],[f3330])).
% 36.51/5.04 fof(f4159,plain,(
% 36.51/5.04 ![X0,X1]: (~equidistant(u,v,u,X0)|~equidistant(u,w,u,X1)|~between(u,v,w)|u=continuous(u,v,X0,u,w,X1))),
% 36.51/5.04 inference(resolution,[status(thm)],[f331,f109])).
% 36.51/5.04 fof(f4192,definition,(
% 36.51/5.04 ![X0,X1]: (sQ211_spl <=> (~equidistant(u,v,u,X0)|~equidistant(u,w,u,X1)|u=continuous(u,v,X0,u,w,X1)))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ211_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f4195,plain,(
% 36.51/5.04 sQ211_spl|~sQ30_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f4159,f4192,f1206])).
% 36.51/5.04 fof(f4645,plain,(
% 36.51/5.04 ![X0,X1]: (~equidistant(reflection(u,v),X0,u,w)|~equidistant(v,X1,v,w)|~equidistant(reflection(u,v),X1,u,w)|~between(v,reflection(u,v),X0)|v=reflection(u,v)|X0=X1|u=v)),
% 36.51/5.04 inference(resolution,[status(thm)],[f497,f270])).
% 36.51/5.04 fof(f4646,plain,(
% 36.51/5.04 ![X0,X1]: (~equidistant(reflection(v,u),X0,u,w)|~equidistant(u,X1,v,w)|~equidistant(reflection(v,u),X1,u,w)|~between(u,reflection(v,u),X0)|u=reflection(v,u)|X0=X1)),
% 36.51/5.04 inference(resolution,[status(thm)],[f497,f88])).
% 36.51/5.04 fof(f4660,plain,(
% 36.51/5.04 ![X0,X1]: (~equidistant(u,X0,u,w)|~equidistant(v,X1,v,w)|~equidistant(u,X1,u,w)|~between(v,u,X0)|v=u|X0=X1)),
% 36.51/5.04 inference(resolution,[status(thm)],[f497,f74])).
% 36.51/5.04 fof(f4661,plain,(
% 36.51/5.04 ![X0,X1]: (~equidistant(v,X0,u,w)|~equidistant(u,X1,v,w)|~equidistant(v,X1,u,w)|~between(u,v,X0)|u=v|X0=X1)),
% 36.51/5.04 inference(resolution,[status(thm)],[f497,f51])).
% 36.51/5.04 fof(f4662,definition,(
% 36.51/5.04 ![X0,X1]: (sQ221_spl <=> (~equidistant(reflection(u,v),X0,u,w)|~equidistant(v,X1,v,w)|~equidistant(reflection(u,v),X1,u,w)|~between(v,reflection(u,v),X0)|X0=X1))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ221_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f4665,plain,(
% 36.51/5.04 sQ221_spl|sQ93_spl|sQ0_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f4645,f4662,f2457,f246])).
% 36.51/5.04 fof(f4666,definition,(
% 36.51/5.04 ![X0,X1]: (sQ222_spl <=> (~equidistant(reflection(v,u),X0,u,w)|~equidistant(u,X1,v,w)|~equidistant(reflection(v,u),X1,u,w)|~between(u,reflection(v,u),X0)|X0=X1))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ222_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f4669,plain,(
% 36.51/5.04 sQ222_spl|sQ95_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f4646,f4666,f2467])).
% 36.51/5.04 fof(f4670,definition,(
% 36.51/5.04 ![X0,X1]: (sQ223_spl <=> (~equidistant(u,X0,u,w)|~equidistant(v,X1,v,w)|~equidistant(u,X1,u,w)|~between(v,u,X0)|X0=X1))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f4673,plain,(
% 36.51/5.04 sQ223_spl|sQ0_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f4660,f4670,f246])).
% 36.51/5.04 fof(f4674,definition,(
% 36.51/5.04 ![X0,X1]: (sQ224_spl <=> (~equidistant(v,X0,u,w)|~equidistant(u,X1,v,w)|~equidistant(v,X1,u,w)|~between(u,v,X0)|X0=X1))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ224_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f4677,plain,(
% 36.51/5.04 sQ224_spl|sQ0_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f4661,f4674,f246])).
% 36.51/5.04 fof(f4728,plain,(
% 36.51/5.04 ![X0,X1,X2]: (~equidistant(u,v,reflection(X0,X1),X1)|~equidistant(v,w,X1,X0)|~equidistant(u,X2,reflection(X0,X1),X0)|~equidistant(v,X2,X1,X0)|u=v|w=X2)),
% 36.51/5.04 inference(resolution,[status(thm)],[f499,f108])).
% 36.51/5.04 fof(f4731,plain,(
% 36.51/5.04 ![X0,X1,X2]: (~equidistant(v,u,reflection(X0,X1),X1)|~equidistant(u,w,X1,X0)|~equidistant(v,X2,reflection(X0,X1),X0)|~equidistant(u,X2,X1,X0)|v=u|w=X2)),
% 36.51/5.04 inference(resolution,[status(thm)],[f499,f109])).
% 36.51/5.04 fof(f4746,definition,(
% 36.51/5.04 ![X0,X1,X2]: (sQ225_spl <=> (~equidistant(u,v,reflection(X0,X1),X1)|~equidistant(v,w,X1,X0)|~equidistant(u,X2,reflection(X0,X1),X0)|~equidistant(v,X2,X1,X0)|w=X2))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ225_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f4749,plain,(
% 36.51/5.04 sQ225_spl|sQ0_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f4728,f4746,f246])).
% 36.51/5.04 fof(f4758,definition,(
% 36.51/5.04 ![X0,X1,X2]: (sQ228_spl <=> (~equidistant(v,u,reflection(X0,X1),X1)|~equidistant(u,w,X1,X0)|~equidistant(v,X2,reflection(X0,X1),X0)|~equidistant(u,X2,X1,X0)|w=X2))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ228_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f4761,plain,(
% 36.51/5.04 sQ228_spl|sQ0_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f4731,f4758,f246])).
% 36.51/5.04 fof(f5048,plain,(
% 36.51/5.04 ![X0,X1,X2,X3,X4]: (~equidistant(u,v,X0,X1)|~equidistant(v,w,X1,extension(X0,X1,X2,X3))|~equidistant(u,X4,X0,extension(X0,X1,X2,X3))|~equidistant(v,X4,X1,extension(X0,X1,X2,X3))|u=v|w=X4)),
% 36.51/5.04 inference(resolution,[status(thm)],[f505,f108])).
% 36.51/5.04 fof(f5051,plain,(
% 36.51/5.04 ![X0,X1,X2,X3,X4]: (~equidistant(v,u,X0,X1)|~equidistant(u,w,X1,extension(X0,X1,X2,X3))|~equidistant(v,X4,X0,extension(X0,X1,X2,X3))|~equidistant(u,X4,X1,extension(X0,X1,X2,X3))|v=u|w=X4)),
% 36.51/5.04 inference(resolution,[status(thm)],[f505,f109])).
% 36.51/5.04 fof(f5066,definition,(
% 36.51/5.04 ![X0,X1,X2,X3,X4]: (sQ229_spl <=> (~equidistant(u,v,X0,X1)|~equidistant(v,w,X1,extension(X0,X1,X2,X3))|~equidistant(u,X4,X0,extension(X0,X1,X2,X3))|~equidistant(v,X4,X1,extension(X0,X1,X2,X3))|w=X4))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ229_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f5069,plain,(
% 36.51/5.04 sQ229_spl|sQ0_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f5048,f5066,f246])).
% 36.51/5.04 fof(f5078,definition,(
% 36.51/5.04 ![X0,X1,X2,X3,X4]: (sQ232_spl <=> (~equidistant(v,u,X0,X1)|~equidistant(u,w,X1,extension(X0,X1,X2,X3))|~equidistant(v,X4,X0,extension(X0,X1,X2,X3))|~equidistant(u,X4,X1,extension(X0,X1,X2,X3))|w=X4))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ232_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f5081,plain,(
% 36.51/5.04 sQ232_spl|sQ0_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f5051,f5078,f246])).
% 36.51/5.04 fof(f5115,plain,(
% 36.51/5.04 ![X0,X1,X2]: (~equidistant(u,v,X0,X1)|~equidistant(v,w,X1,reflection(X0,X1))|~equidistant(u,X2,X0,reflection(X0,X1))|~equidistant(v,X2,X1,reflection(X0,X1))|u=v|w=X2)),
% 36.51/5.04 inference(resolution,[status(thm)],[f506,f108])).
% 36.51/5.04 fof(f5118,plain,(
% 36.51/5.04 ![X0,X1,X2]: (~equidistant(v,u,X0,X1)|~equidistant(u,w,X1,reflection(X0,X1))|~equidistant(v,X2,X0,reflection(X0,X1))|~equidistant(u,X2,X1,reflection(X0,X1))|v=u|w=X2)),
% 36.51/5.04 inference(resolution,[status(thm)],[f506,f109])).
% 36.51/5.04 fof(f5133,definition,(
% 36.51/5.04 ![X0,X1,X2]: (sQ233_spl <=> (~equidistant(u,v,X0,X1)|~equidistant(v,w,X1,reflection(X0,X1))|~equidistant(u,X2,X0,reflection(X0,X1))|~equidistant(v,X2,X1,reflection(X0,X1))|w=X2))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ233_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f5136,plain,(
% 36.51/5.04 sQ233_spl|sQ0_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f5115,f5133,f246])).
% 36.51/5.04 fof(f5145,definition,(
% 36.51/5.04 ![X0,X1,X2]: (sQ236_spl <=> (~equidistant(v,u,X0,X1)|~equidistant(u,w,X1,reflection(X0,X1))|~equidistant(v,X2,X0,reflection(X0,X1))|~equidistant(u,X2,X1,reflection(X0,X1))|w=X2))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ236_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f5148,plain,(
% 36.51/5.04 sQ236_spl|sQ0_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f5118,f5145,f246])).
% 36.51/5.04 fof(f5167,plain,(
% 36.51/5.04 ![X0,X1,X2]: (~equidistant(u,v,X0,X1)|~equidistant(v,w,X1,X1)|~equidistant(u,X2,X0,X1)|~equidistant(v,X2,X1,X1)|u=v|w=X2)),
% 36.51/5.04 inference(resolution,[status(thm)],[f509,f108])).
% 36.51/5.04 fof(f5170,plain,(
% 36.51/5.04 ![X0,X1,X2]: (~equidistant(v,u,X0,X1)|~equidistant(u,w,X1,X1)|~equidistant(v,X2,X0,X1)|~equidistant(u,X2,X1,X1)|v=u|w=X2)),
% 36.51/5.04 inference(resolution,[status(thm)],[f509,f109])).
% 36.51/5.04 fof(f5185,definition,(
% 36.51/5.04 ![X0,X1,X2]: (sQ237_spl <=> (~equidistant(u,v,X0,X1)|~equidistant(v,w,X1,X1)|~equidistant(u,X2,X0,X1)|~equidistant(v,X2,X1,X1)|w=X2))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ237_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f5188,plain,(
% 36.51/5.04 sQ237_spl|sQ0_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f5167,f5185,f246])).
% 36.51/5.04 fof(f5197,definition,(
% 36.51/5.04 ![X0,X1,X2]: (sQ240_spl <=> (~equidistant(v,u,X0,X1)|~equidistant(u,w,X1,X1)|~equidistant(v,X2,X0,X1)|~equidistant(u,X2,X1,X1)|w=X2))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ240_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f5200,plain,(
% 36.51/5.04 sQ240_spl|sQ0_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f5170,f5197,f246])).
% 36.51/5.04 fof(f5201,plain,(
% 36.51/5.04 u=inner_pasch(v,u,w,v,u)),
% 36.51/5.04 inference(resolution,[status(thm)],[f510,f109])).
% 36.51/5.04 fof(f5552,plain,(
% 36.51/5.04 ![X0,X1,X2]: (~between(X0,u,w)|~equidistant(u,v,X1,inner_pasch(X0,u,w,v,u))|~equidistant(v,w,inner_pasch(X0,u,w,v,u),u)|~equidistant(u,X2,X1,u)|~equidistant(v,X2,inner_pasch(X0,u,w,v,u),u)|u=v|w=X2)),
% 36.51/5.04 inference(resolution,[status(thm)],[f527,f108])).
% 36.51/5.04 fof(f5558,plain,(
% 36.51/5.04 ![X0,X1,X2]: (~between(X0,v,w)|~equidistant(v,u,X1,inner_pasch(X0,v,w,u,v))|~equidistant(u,w,inner_pasch(X0,v,w,u,v),v)|~equidistant(v,X2,X1,v)|~equidistant(u,X2,inner_pasch(X0,v,w,u,v),v)|v=u|w=X2)),
% 36.51/5.04 inference(resolution,[status(thm)],[f527,f109])).
% 36.51/5.04 fof(f5588,plain,(
% 36.51/5.04 ![X0,X1,X2,X3,X4,X5]: (~between(X0,X1,X2)|~between(X1,X3,X2)|~equidistant(u,v,X4,inner_pasch(X0,X1,X2,X3,X1))|~equidistant(v,w,inner_pasch(X0,X1,X2,X3,X1),X1)|~equidistant(u,X5,X4,X1)|~equidistant(v,X5,inner_pasch(X0,X1,X2,X3,X1),X1)|u=v|w=X5)),
% 36.51/5.04 inference(resolution,[status(thm)],[f527,f108])).
% 36.51/5.04 fof(f5591,plain,(
% 36.51/5.04 ![X0,X1,X2,X3,X4,X5]: (~between(X0,X1,X2)|~between(X1,X3,X2)|~equidistant(v,u,X4,inner_pasch(X0,X1,X2,X3,X1))|~equidistant(u,w,inner_pasch(X0,X1,X2,X3,X1),X1)|~equidistant(v,X5,X4,X1)|~equidistant(u,X5,inner_pasch(X0,X1,X2,X3,X1),X1)|v=u|w=X5)),
% 36.51/5.04 inference(resolution,[status(thm)],[f527,f109])).
% 36.51/5.04 fof(f5606,definition,(
% 36.51/5.04 ![X0,X1,X2]: (sQ241_spl <=> (~between(X0,u,w)|~equidistant(u,v,X1,inner_pasch(X0,u,w,v,u))|~equidistant(v,w,inner_pasch(X0,u,w,v,u),u)|~equidistant(u,X2,X1,u)|~equidistant(v,X2,inner_pasch(X0,u,w,v,u),u)|w=X2))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ241_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f5609,plain,(
% 36.51/5.04 sQ241_spl|sQ0_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f5552,f5606,f246])).
% 36.51/5.04 fof(f5618,definition,(
% 36.51/5.04 ![X0,X1,X2]: (sQ244_spl <=> (~between(X0,v,w)|~equidistant(v,u,X1,inner_pasch(X0,v,w,u,v))|~equidistant(u,w,inner_pasch(X0,v,w,u,v),v)|~equidistant(v,X2,X1,v)|~equidistant(u,X2,inner_pasch(X0,v,w,u,v),v)|w=X2))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ244_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f5621,plain,(
% 36.51/5.04 sQ244_spl|sQ0_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f5558,f5618,f246])).
% 36.51/5.04 fof(f5622,definition,(
% 36.51/5.04 ![X0,X1,X2,X3,X4,X5]: (sQ245_spl <=> (~between(X0,X1,X2)|~between(X1,X3,X2)|~equidistant(u,v,X4,inner_pasch(X0,X1,X2,X3,X1))|~equidistant(v,w,inner_pasch(X0,X1,X2,X3,X1),X1)|~equidistant(u,X5,X4,X1)|~equidistant(v,X5,inner_pasch(X0,X1,X2,X3,X1),X1)|w=X5))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ245_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f5625,plain,(
% 36.51/5.04 sQ245_spl|sQ0_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f5588,f5622,f246])).
% 36.51/5.04 fof(f5634,definition,(
% 36.51/5.04 ![X0,X1,X2,X3,X4,X5]: (sQ248_spl <=> (~between(X0,X1,X2)|~between(X1,X3,X2)|~equidistant(v,u,X4,inner_pasch(X0,X1,X2,X3,X1))|~equidistant(u,w,inner_pasch(X0,X1,X2,X3,X1),X1)|~equidistant(v,X5,X4,X1)|~equidistant(u,X5,inner_pasch(X0,X1,X2,X3,X1),X1)|w=X5))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ248_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f5637,plain,(
% 36.51/5.04 sQ248_spl|sQ0_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f5591,f5634,f246])).
% 36.51/5.04 fof(f5717,plain,(
% 36.51/5.04 ![X0,X1,X2]: (~between(v,X0,w)|~equidistant(u,v,X1,inner_pasch(v,X0,w,v,u))|~equidistant(v,w,inner_pasch(v,X0,w,v,u),v)|~equidistant(u,X2,X1,v)|~equidistant(v,X2,inner_pasch(v,X0,w,v,u),v)|u=v|w=X2)),
% 36.51/5.04 inference(resolution,[status(thm)],[f563,f108])).
% 36.51/5.04 fof(f5723,plain,(
% 36.51/5.04 ![X0,X1,X2]: (~between(u,X0,w)|~equidistant(v,u,X1,inner_pasch(u,X0,w,u,v))|~equidistant(u,w,inner_pasch(u,X0,w,u,v),u)|~equidistant(v,X2,X1,u)|~equidistant(u,X2,inner_pasch(u,X0,w,u,v),u)|v=u|w=X2)),
% 36.51/5.04 inference(resolution,[status(thm)],[f563,f109])).
% 36.51/5.04 fof(f5753,plain,(
% 36.51/5.04 ![X0,X1,X2,X3,X4,X5]: (~between(X0,X1,X2)|~between(X3,X0,X2)|~equidistant(u,v,X4,inner_pasch(X0,X1,X2,X0,X3))|~equidistant(v,w,inner_pasch(X0,X1,X2,X0,X3),X0)|~equidistant(u,X5,X4,X0)|~equidistant(v,X5,inner_pasch(X0,X1,X2,X0,X3),X0)|u=v|w=X5)),
% 36.51/5.04 inference(resolution,[status(thm)],[f563,f108])).
% 36.51/5.04 fof(f5756,plain,(
% 36.51/5.04 ![X0,X1,X2,X3,X4,X5]: (~between(X0,X1,X2)|~between(X3,X0,X2)|~equidistant(v,u,X4,inner_pasch(X0,X1,X2,X0,X3))|~equidistant(u,w,inner_pasch(X0,X1,X2,X0,X3),X0)|~equidistant(v,X5,X4,X0)|~equidistant(u,X5,inner_pasch(X0,X1,X2,X0,X3),X0)|v=u|w=X5)),
% 36.51/5.04 inference(resolution,[status(thm)],[f563,f109])).
% 36.51/5.04 fof(f5771,definition,(
% 36.51/5.04 ![X0,X1,X2]: (sQ249_spl <=> (~between(v,X0,w)|~equidistant(u,v,X1,inner_pasch(v,X0,w,v,u))|~equidistant(v,w,inner_pasch(v,X0,w,v,u),v)|~equidistant(u,X2,X1,v)|~equidistant(v,X2,inner_pasch(v,X0,w,v,u),v)|w=X2))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ249_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f5774,plain,(
% 36.51/5.04 sQ249_spl|sQ0_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f5717,f5771,f246])).
% 36.51/5.04 fof(f5783,definition,(
% 36.51/5.04 ![X0,X1,X2]: (sQ252_spl <=> (~between(u,X0,w)|~equidistant(v,u,X1,inner_pasch(u,X0,w,u,v))|~equidistant(u,w,inner_pasch(u,X0,w,u,v),u)|~equidistant(v,X2,X1,u)|~equidistant(u,X2,inner_pasch(u,X0,w,u,v),u)|w=X2))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ252_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f5786,plain,(
% 36.51/5.04 sQ252_spl|sQ0_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f5723,f5783,f246])).
% 36.51/5.04 fof(f5787,definition,(
% 36.51/5.04 ![X0,X1,X2,X3,X4,X5]: (sQ253_spl <=> (~between(X0,X1,X2)|~between(X3,X0,X2)|~equidistant(u,v,X4,inner_pasch(X0,X1,X2,X0,X3))|~equidistant(v,w,inner_pasch(X0,X1,X2,X0,X3),X0)|~equidistant(u,X5,X4,X0)|~equidistant(v,X5,inner_pasch(X0,X1,X2,X0,X3),X0)|w=X5))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ253_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f5790,plain,(
% 36.51/5.04 sQ253_spl|sQ0_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f5753,f5787,f246])).
% 36.51/5.04 fof(f5799,definition,(
% 36.51/5.04 ![X0,X1,X2,X3,X4,X5]: (sQ256_spl <=> (~between(X0,X1,X2)|~between(X3,X0,X2)|~equidistant(v,u,X4,inner_pasch(X0,X1,X2,X0,X3))|~equidistant(u,w,inner_pasch(X0,X1,X2,X0,X3),X0)|~equidistant(v,X5,X4,X0)|~equidistant(u,X5,inner_pasch(X0,X1,X2,X0,X3),X0)|w=X5))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f5802,plain,(
% 36.51/5.04 sQ256_spl|sQ0_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f5756,f5799,f246])).
% 36.51/5.04 fof(f5848,plain,(
% 36.51/5.04 ![X0]: (~between(v,u,w)|~between(u,v,w)|between(X0,u,v))),
% 36.51/5.04 inference(paramodulation,[status(thm)],[f5201,f156])).
% 36.51/5.04 fof(f5852,definition,(
% 36.51/5.04 ![X0]: (sQ257_spl <=> (between(X0,u,v)))),
% 36.51/5.04 introduced(definition,[new_symbols(definition,[sQ257_spl])],[split_symbol_definition])).
% 36.51/5.04 fof(f5853,plain,(
% 36.51/5.04 ![X0]: (between(X0,u,v)|~sQ257_spl)),
% 36.51/5.04 inference(component_clause,[status(thm)],[f5852])).
% 36.51/5.04 fof(f5855,plain,(
% 36.51/5.04 ~sQ40_spl|~sQ30_spl|sQ257_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f5848,f1281,f1206,f5852])).
% 36.51/5.04 fof(f5954,plain,(
% 36.51/5.04 v=u|~sQ257_spl),
% 36.51/5.04 inference(resolution,[status(thm)],[f5853,f60])).
% 36.51/5.04 fof(f5966,plain,(
% 36.51/5.04 sQ0_spl|~sQ257_spl),
% 36.51/5.04 inference(split_clause,[status(thm)],[f5954,f246,f5852])).
% 36.51/5.04 fof(f5967,plain,(
% 36.51/5.04 $false),
% 36.51/5.04 inference(sat_refutation,[status(thm)],[f252,f256,f258,f317,f337,f399,f403,f461,f1088,f1092,f1166,f1170,f1174,f1178,f1212,f1216,f1220,f1222,f1224,f1247,f1249,f1294,f1297,f1305,f1308,f1415,f1635,f1639,f1643,f1647,f2051,f2055,f2059,f2063,f2536,f2639,f2651,f2777,f2794,f3001,f3331,f4195,f4665,f4669,f4673,f4677,f4749,f4761,f5069,f5081,f5136,f5148,f5188,f5200,f5609,f5621,f5625,f5637,f5774,f5786,f5790,f5802,f5855,f5966])).
% 36.51/5.04 % SZS output end CNFRefutation for theBenchmark.p
% 36.51/5.08 % Elapsed time: 4.715348 seconds
% 36.51/5.08 % CPU time: 37.130395 seconds
% 36.51/5.08 % Total memory used: 233.537 MB
% 36.51/5.08 % Net memory used: 209.696 MB
%------------------------------------------------------------------------------