Z3---4.15.1.UNS-Prf.s

%------------------------------------------------------------------------------
% File     : Z3---4.15.1
% Problem  : GEO022-2 : TPTP v9.0.0. Released v1.0.0.
% Transfm  : none
% Format   : tptp
% Command  : run_E %s %d THM

% Computer : n010.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 : Sat Jun 21 05:05:21 AM UTC 2025

% Result   : Unsatisfiable 198.16s 198.32s
% Output   : Proof 198.16s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   13
%            Number of leaves      :   47
% Syntax   : Number of formulae    :  113 (  39 unt;   0 typ;   0 def)
%            Number of atoms       :  446 (  50 equ)
%            Maximal formula atoms :   12 (   3 avg)
%            Number of connectives :  599 ( 280   ~; 270   |;   0   &)
%                                         (  49 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   13 (   6 avg)
%            Maximal term depth    :    5 (   1 avg)
%            Number of FOOLs       :   14 (  14 fml;   0 var)
%            Number of types       :    2 (   0 usr)
%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
%            Number of predicates  :    8 (   6 usr;   1 prp; 0-4 aty)
%            Number of functors    :   12 (  12 usr;   9 con; 0-5 aty)
%            Number of variables   :  468 ( 433   !;   0   ?; 468   :)

% Comments : 
%------------------------------------------------------------------------------
tff(equidistant_type,type,
    equidistant: ( $i * $i * $i * $i ) > $o ).

tff(extension_type,type,
    extension: ( $i * $i * $i * $i ) > $i ).

tff(lower_dimension_point_2_type,type,
    lower_dimension_point_2: $i ).

tff(z_type,type,
    z: $i ).

tff(v_type,type,
    v: $i ).

tff(lower_dimension_point_1_type,type,
    lower_dimension_point_1: $i ).

tff(lower_dimension_point_3_type,type,
    lower_dimension_point_3: $i ).

tff(inner_pasch_type,type,
    inner_pasch: ( $i * $i * $i * $i * $i ) > $i ).

tff(u_type,type,
    u: $i ).

tff(euclid1_type,type,
    euclid1: ( $i * $i * $i * $i * $i ) > $i ).

tff(x_type,type,
    x: $i ).

tff(w_type,type,
    w: $i ).

tff(between_type,type,
    between: ( $i * $i * $i ) > $o ).

tff(y_type,type,
    y: $i ).

tff(1,plain,
    ^ [W: $i,V: $i,Y: $i,X: $i] :
      refl(( equidistant(Y,extension(X,Y,W,V),W,V)
      <=> equidistant(Y,extension(X,Y,W,V),W,V) )),
    inference(bind,[status(th)],[]) ).

tff(2,plain,
    ( ! [W: $i,V: $i,Y: $i,X: $i] : equidistant(Y,extension(X,Y,W,V),W,V)
  <=> ! [W: $i,V: $i,Y: $i,X: $i] : equidistant(Y,extension(X,Y,W,V),W,V) ),
    inference(quant_intro,[status(thm)],[1]) ).

tff(3,plain,
    ( ! [W: $i,V: $i,Y: $i,X: $i] : equidistant(Y,extension(X,Y,W,V),W,V)
  <=> ! [W: $i,V: $i,Y: $i,X: $i] : equidistant(Y,extension(X,Y,W,V),W,V) ),
    inference(rewrite,[status(thm)],[]) ).

tff(4,axiom,
    ! [W: $i,V: $i,Y: $i,X: $i] : equidistant(Y,extension(X,Y,W,V),W,V),
    file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',segment_construction2) ).

tff(5,plain,
    ! [W: $i,V: $i,Y: $i,X: $i] : equidistant(Y,extension(X,Y,W,V),W,V),
    inference(modus_ponens,[status(thm)],[4,3]) ).

tff(6,plain,
    ! [W: $i,V: $i,Y: $i,X: $i] : equidistant(Y,extension(X,Y,W,V),W,V),
    inference(skolemize,[status(sab)],[5]) ).

tff(7,plain,
    ! [W: $i,V: $i,Y: $i,X: $i] : equidistant(Y,extension(X,Y,W,V),W,V),
    inference(modus_ponens,[status(thm)],[6,2]) ).

tff(8,plain,
    ( ~ ! [W: $i,V: $i,Y: $i,X: $i] : equidistant(Y,extension(X,Y,W,V),W,V)
    | equidistant(v,extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)) ),
    inference(quant_inst,[status(thm)],[]) ).

tff(9,plain,
    equidistant(v,extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),
    inference(unit_resolution,[status(thm)],[8,7]) ).

tff(10,plain,
    ^ [Z: $i,Y: $i,X: $i] :
      refl(( ( ~ equidistant(X,Y,Z,Z)
          | ( X = Y ) )
      <=> ( ~ equidistant(X,Y,Z,Z)
          | ( X = Y ) ) )),
    inference(bind,[status(th)],[]) ).

tff(11,plain,
    ( ! [Z: $i,Y: $i,X: $i] :
        ( ~ equidistant(X,Y,Z,Z)
        | ( X = Y ) )
  <=> ! [Z: $i,Y: $i,X: $i] :
        ( ~ equidistant(X,Y,Z,Z)
        | ( X = Y ) ) ),
    inference(quant_intro,[status(thm)],[10]) ).

tff(12,plain,
    ( ! [Z: $i,Y: $i,X: $i] :
        ( ~ equidistant(X,Y,Z,Z)
        | ( X = Y ) )
  <=> ! [Z: $i,Y: $i,X: $i] :
        ( ~ equidistant(X,Y,Z,Z)
        | ( X = Y ) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(13,axiom,
    ! [Z: $i,Y: $i,X: $i] :
      ( ~ equidistant(X,Y,Z,Z)
      | ( X = Y ) ),
    file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',identity_for_equidistance) ).

tff(14,plain,
    ! [Z: $i,Y: $i,X: $i] :
      ( ~ equidistant(X,Y,Z,Z)
      | ( X = Y ) ),
    inference(modus_ponens,[status(thm)],[13,12]) ).

tff(15,plain,
    ! [Z: $i,Y: $i,X: $i] :
      ( ~ equidistant(X,Y,Z,Z)
      | ( X = Y ) ),
    inference(skolemize,[status(sab)],[14]) ).

tff(16,plain,
    ! [Z: $i,Y: $i,X: $i] :
      ( ~ equidistant(X,Y,Z,Z)
      | ( X = Y ) ),
    inference(modus_ponens,[status(thm)],[15,11]) ).

tff(17,plain,
    ( ( ~ ! [Z: $i,Y: $i,X: $i] :
            ( ~ equidistant(X,Y,Z,Z)
            | ( X = Y ) )
      | ~ equidistant(v,extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))
      | ( v = extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)) ) )
  <=> ( ~ ! [Z: $i,Y: $i,X: $i] :
            ( ~ equidistant(X,Y,Z,Z)
            | ( X = Y ) )
      | ~ equidistant(v,extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))
      | ( v = extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)) ) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(18,plain,
    ( ~ ! [Z: $i,Y: $i,X: $i] :
          ( ~ equidistant(X,Y,Z,Z)
          | ( X = Y ) )
    | ~ equidistant(v,extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))
    | ( v = extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)) ) ),
    inference(quant_inst,[status(thm)],[]) ).

tff(19,plain,
    ( ~ ! [Z: $i,Y: $i,X: $i] :
          ( ~ equidistant(X,Y,Z,Z)
          | ( X = Y ) )
    | ~ equidistant(v,extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))
    | ( v = extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)) ) ),
    inference(modus_ponens,[status(thm)],[18,17]) ).

tff(20,plain,
    v = extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),
    inference(unit_resolution,[status(thm)],[19,16,9]) ).

tff(21,plain,
    extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)) = v,
    inference(symmetry,[status(thm)],[20]) ).

tff(22,plain,
    ^ [W: $i,V: $i,Y: $i,X: $i] :
      refl(( between(X,Y,extension(X,Y,W,V))
      <=> between(X,Y,extension(X,Y,W,V)) )),
    inference(bind,[status(th)],[]) ).

tff(23,plain,
    ( ! [W: $i,V: $i,Y: $i,X: $i] : between(X,Y,extension(X,Y,W,V))
  <=> ! [W: $i,V: $i,Y: $i,X: $i] : between(X,Y,extension(X,Y,W,V)) ),
    inference(quant_intro,[status(thm)],[22]) ).

tff(24,plain,
    ( ! [W: $i,V: $i,Y: $i,X: $i] : between(X,Y,extension(X,Y,W,V))
  <=> ! [W: $i,V: $i,Y: $i,X: $i] : between(X,Y,extension(X,Y,W,V)) ),
    inference(rewrite,[status(thm)],[]) ).

tff(25,axiom,
    ! [W: $i,V: $i,Y: $i,X: $i] : between(X,Y,extension(X,Y,W,V)),
    file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',segment_construction1) ).

tff(26,plain,
    ! [W: $i,V: $i,Y: $i,X: $i] : between(X,Y,extension(X,Y,W,V)),
    inference(modus_ponens,[status(thm)],[25,24]) ).

tff(27,plain,
    ! [W: $i,V: $i,Y: $i,X: $i] : between(X,Y,extension(X,Y,W,V)),
    inference(skolemize,[status(sab)],[26]) ).

tff(28,plain,
    ! [W: $i,V: $i,Y: $i,X: $i] : between(X,Y,extension(X,Y,W,V)),
    inference(modus_ponens,[status(thm)],[27,23]) ).

tff(29,plain,
    ( ~ ! [W: $i,V: $i,Y: $i,X: $i] : between(X,Y,extension(X,Y,W,V))
    | between(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)) ),
    inference(quant_inst,[status(thm)],[]) ).

tff(30,plain,
    between(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),
    inference(unit_resolution,[status(thm)],[29,28]) ).

tff(31,plain,
    ^ [W: $i,V: $i,Y: $i,U: $i,X: $i] :
      refl(( ( ~ between(Y,X,W)
          | ~ between(U,V,W)
          | between(X,inner_pasch(U,V,W,X,Y),U) )
      <=> ( ~ between(Y,X,W)
          | ~ between(U,V,W)
          | between(X,inner_pasch(U,V,W,X,Y),U) ) )),
    inference(bind,[status(th)],[]) ).

tff(32,plain,
    ( ! [W: $i,V: $i,Y: $i,U: $i,X: $i] :
        ( ~ between(Y,X,W)
        | ~ between(U,V,W)
        | between(X,inner_pasch(U,V,W,X,Y),U) )
  <=> ! [W: $i,V: $i,Y: $i,U: $i,X: $i] :
        ( ~ between(Y,X,W)
        | ~ between(U,V,W)
        | between(X,inner_pasch(U,V,W,X,Y),U) ) ),
    inference(quant_intro,[status(thm)],[31]) ).

tff(33,plain,
    ( ! [W: $i,V: $i,Y: $i,U: $i,X: $i] :
        ( ~ between(Y,X,W)
        | ~ between(U,V,W)
        | between(X,inner_pasch(U,V,W,X,Y),U) )
  <=> ! [W: $i,V: $i,Y: $i,U: $i,X: $i] :
        ( ~ between(Y,X,W)
        | ~ between(U,V,W)
        | between(X,inner_pasch(U,V,W,X,Y),U) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(34,plain,
    ^ [W: $i,V: $i,Y: $i,U: $i,X: $i] :
      rewrite(( ( ~ between(U,V,W)
          | ~ between(Y,X,W)
          | between(X,inner_pasch(U,V,W,X,Y),U) )
      <=> ( ~ between(Y,X,W)
          | ~ between(U,V,W)
          | between(X,inner_pasch(U,V,W,X,Y),U) ) )),
    inference(bind,[status(th)],[]) ).

tff(35,plain,
    ( ! [W: $i,V: $i,Y: $i,U: $i,X: $i] :
        ( ~ between(U,V,W)
        | ~ between(Y,X,W)
        | between(X,inner_pasch(U,V,W,X,Y),U) )
  <=> ! [W: $i,V: $i,Y: $i,U: $i,X: $i] :
        ( ~ between(Y,X,W)
        | ~ between(U,V,W)
        | between(X,inner_pasch(U,V,W,X,Y),U) ) ),
    inference(quant_intro,[status(thm)],[34]) ).

tff(36,axiom,
    ! [W: $i,V: $i,Y: $i,U: $i,X: $i] :
      ( ~ between(U,V,W)
      | ~ between(Y,X,W)
      | between(X,inner_pasch(U,V,W,X,Y),U) ),
    file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',inner_pasch2) ).

tff(37,plain,
    ! [W: $i,V: $i,Y: $i,U: $i,X: $i] :
      ( ~ between(Y,X,W)
      | ~ between(U,V,W)
      | between(X,inner_pasch(U,V,W,X,Y),U) ),
    inference(modus_ponens,[status(thm)],[36,35]) ).

tff(38,plain,
    ! [W: $i,V: $i,Y: $i,U: $i,X: $i] :
      ( ~ between(Y,X,W)
      | ~ between(U,V,W)
      | between(X,inner_pasch(U,V,W,X,Y),U) ),
    inference(modus_ponens,[status(thm)],[37,33]) ).

tff(39,plain,
    ! [W: $i,V: $i,Y: $i,U: $i,X: $i] :
      ( ~ between(Y,X,W)
      | ~ between(U,V,W)
      | between(X,inner_pasch(U,V,W,X,Y),U) ),
    inference(skolemize,[status(sab)],[38]) ).

tff(40,plain,
    ! [W: $i,V: $i,Y: $i,U: $i,X: $i] :
      ( ~ between(Y,X,W)
      | ~ between(U,V,W)
      | between(X,inner_pasch(U,V,W,X,Y),U) ),
    inference(modus_ponens,[status(thm)],[39,32]) ).

tff(41,plain,
    ( ( ~ ! [W: $i,V: $i,Y: $i,U: $i,X: $i] :
            ( ~ between(Y,X,W)
            | ~ between(U,V,W)
            | between(X,inner_pasch(U,V,W,X,Y),U) )
      | between(u,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),u)
      | ~ between(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)) )
  <=> ( ~ ! [W: $i,V: $i,Y: $i,U: $i,X: $i] :
            ( ~ between(Y,X,W)
            | ~ between(U,V,W)
            | between(X,inner_pasch(U,V,W,X,Y),U) )
      | between(u,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),u)
      | ~ between(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(42,plain,
    ( ( ~ between(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))
      | ~ between(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))
      | between(u,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),u) )
  <=> ( between(u,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),u)
      | ~ between(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(43,plain,
    ( ( ~ ! [W: $i,V: $i,Y: $i,U: $i,X: $i] :
            ( ~ between(Y,X,W)
            | ~ between(U,V,W)
            | between(X,inner_pasch(U,V,W,X,Y),U) )
      | ~ between(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))
      | ~ between(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))
      | between(u,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),u) )
  <=> ( ~ ! [W: $i,V: $i,Y: $i,U: $i,X: $i] :
            ( ~ between(Y,X,W)
            | ~ between(U,V,W)
            | between(X,inner_pasch(U,V,W,X,Y),U) )
      | between(u,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),u)
      | ~ between(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)) ) ),
    inference(monotonicity,[status(thm)],[42]) ).

tff(44,plain,
    ( ( ~ ! [W: $i,V: $i,Y: $i,U: $i,X: $i] :
            ( ~ between(Y,X,W)
            | ~ between(U,V,W)
            | between(X,inner_pasch(U,V,W,X,Y),U) )
      | ~ between(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))
      | ~ between(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))
      | between(u,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),u) )
  <=> ( ~ ! [W: $i,V: $i,Y: $i,U: $i,X: $i] :
            ( ~ between(Y,X,W)
            | ~ between(U,V,W)
            | between(X,inner_pasch(U,V,W,X,Y),U) )
      | between(u,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),u)
      | ~ between(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)) ) ),
    inference(transitivity,[status(thm)],[43,41]) ).

tff(45,plain,
    ( ~ ! [W: $i,V: $i,Y: $i,U: $i,X: $i] :
          ( ~ between(Y,X,W)
          | ~ between(U,V,W)
          | between(X,inner_pasch(U,V,W,X,Y),U) )
    | ~ between(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))
    | ~ between(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))
    | between(u,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),u) ),
    inference(quant_inst,[status(thm)],[]) ).

tff(46,plain,
    ( ~ ! [W: $i,V: $i,Y: $i,U: $i,X: $i] :
          ( ~ between(Y,X,W)
          | ~ between(U,V,W)
          | between(X,inner_pasch(U,V,W,X,Y),U) )
    | between(u,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),u)
    | ~ between(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)) ),
    inference(modus_ponens,[status(thm)],[45,44]) ).

tff(47,plain,
    between(u,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),u),
    inference(unit_resolution,[status(thm)],[46,40,30]) ).

tff(48,plain,
    ^ [Y: $i,X: $i] :
      refl(( ( ~ between(X,Y,X)
          | ( X = Y ) )
      <=> ( ~ between(X,Y,X)
          | ( X = Y ) ) )),
    inference(bind,[status(th)],[]) ).

tff(49,plain,
    ( ! [Y: $i,X: $i] :
        ( ~ between(X,Y,X)
        | ( X = Y ) )
  <=> ! [Y: $i,X: $i] :
        ( ~ between(X,Y,X)
        | ( X = Y ) ) ),
    inference(quant_intro,[status(thm)],[48]) ).

tff(50,plain,
    ( ! [Y: $i,X: $i] :
        ( ~ between(X,Y,X)
        | ( X = Y ) )
  <=> ! [Y: $i,X: $i] :
        ( ~ between(X,Y,X)
        | ( X = Y ) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(51,axiom,
    ! [Y: $i,X: $i] :
      ( ~ between(X,Y,X)
      | ( X = Y ) ),
    file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',identity_for_betweeness) ).

tff(52,plain,
    ! [Y: $i,X: $i] :
      ( ~ between(X,Y,X)
      | ( X = Y ) ),
    inference(modus_ponens,[status(thm)],[51,50]) ).

tff(53,plain,
    ! [Y: $i,X: $i] :
      ( ~ between(X,Y,X)
      | ( X = Y ) ),
    inference(skolemize,[status(sab)],[52]) ).

tff(54,plain,
    ! [Y: $i,X: $i] :
      ( ~ between(X,Y,X)
      | ( X = Y ) ),
    inference(modus_ponens,[status(thm)],[53,49]) ).

tff(55,plain,
    ( ( ~ ! [Y: $i,X: $i] :
            ( ~ between(X,Y,X)
            | ( X = Y ) )
      | ~ between(u,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),u)
      | ( u = inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u) ) )
  <=> ( ~ ! [Y: $i,X: $i] :
            ( ~ between(X,Y,X)
            | ( X = Y ) )
      | ~ between(u,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),u)
      | ( u = inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u) ) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(56,plain,
    ( ~ ! [Y: $i,X: $i] :
          ( ~ between(X,Y,X)
          | ( X = Y ) )
    | ~ between(u,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),u)
    | ( u = inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u) ) ),
    inference(quant_inst,[status(thm)],[]) ).

tff(57,plain,
    ( ~ ! [Y: $i,X: $i] :
          ( ~ between(X,Y,X)
          | ( X = Y ) )
    | ~ between(u,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),u)
    | ( u = inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u) ) ),
    inference(modus_ponens,[status(thm)],[56,55]) ).

tff(58,plain,
    u = inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),
    inference(unit_resolution,[status(thm)],[57,54,47]) ).

tff(59,plain,
    inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u) = u,
    inference(symmetry,[status(thm)],[58]) ).

tff(60,plain,
    ( ~ ! [W: $i,V: $i,Y: $i,X: $i] : equidistant(Y,extension(X,Y,W,V),W,V)
    | equidistant(x,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))) ),
    inference(quant_inst,[status(thm)],[]) ).

tff(61,plain,
    equidistant(x,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))),
    inference(unit_resolution,[status(thm)],[60,7]) ).

tff(62,plain,
    ( ( ~ ! [Z: $i,Y: $i,X: $i] :
            ( ~ equidistant(X,Y,Z,Z)
            | ( X = Y ) )
      | ~ equidistant(x,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)))
      | ( x = extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))) ) )
  <=> ( ~ ! [Z: $i,Y: $i,X: $i] :
            ( ~ equidistant(X,Y,Z,Z)
            | ( X = Y ) )
      | ~ equidistant(x,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)))
      | ( x = extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))) ) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(63,plain,
    ( ~ ! [Z: $i,Y: $i,X: $i] :
          ( ~ equidistant(X,Y,Z,Z)
          | ( X = Y ) )
    | ~ equidistant(x,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)))
    | ( x = extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))) ) ),
    inference(quant_inst,[status(thm)],[]) ).

tff(64,plain,
    ( ~ ! [Z: $i,Y: $i,X: $i] :
          ( ~ equidistant(X,Y,Z,Z)
          | ( X = Y ) )
    | ~ equidistant(x,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)))
    | ( x = extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))) ) ),
    inference(modus_ponens,[status(thm)],[63,62]) ).

tff(65,plain,
    x = extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))),
    inference(unit_resolution,[status(thm)],[64,16,61]) ).

tff(66,plain,
    extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))) = x,
    inference(symmetry,[status(thm)],[65]) ).

tff(67,plain,
    ( equidistant(w,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
  <=> equidistant(w,x,u,v) ),
    inference(monotonicity,[status(thm)],[66,59,21]) ).

tff(68,plain,
    ( equidistant(w,x,u,v)
  <=> equidistant(w,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))) ),
    inference(symmetry,[status(thm)],[67]) ).

tff(69,plain,
    ( ~ equidistant(w,x,u,v)
  <=> ~ equidistant(w,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))) ),
    inference(monotonicity,[status(thm)],[68]) ).

tff(70,plain,
    ( ~ equidistant(u,v,y,z)
  <=> ~ equidistant(u,v,y,z) ),
    inference(rewrite,[status(thm)],[]) ).

tff(71,axiom,
    ~ equidistant(u,v,y,z),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_transitivity) ).

tff(72,plain,
    ~ equidistant(u,v,y,z),
    inference(modus_ponens,[status(thm)],[71,70]) ).

tff(73,plain,
    ( equidistant(w,x,y,z)
  <=> equidistant(w,x,y,z) ),
    inference(rewrite,[status(thm)],[]) ).

tff(74,axiom,
    equidistant(w,x,y,z),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',w_to_x_equals_y_to_z) ).

tff(75,plain,
    equidistant(w,x,y,z),
    inference(modus_ponens,[status(thm)],[74,73]) ).

tff(76,plain,
    ^ [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
      refl(( ( equidistant(Z,V,V2,W)
          | ~ equidistant(X,Y,V2,W)
          | ~ equidistant(X,Y,Z,V) )
      <=> ( equidistant(Z,V,V2,W)
          | ~ equidistant(X,Y,V2,W)
          | ~ equidistant(X,Y,Z,V) ) )),
    inference(bind,[status(th)],[]) ).

tff(77,plain,
    ( ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
        ( equidistant(Z,V,V2,W)
        | ~ equidistant(X,Y,V2,W)
        | ~ equidistant(X,Y,Z,V) )
  <=> ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
        ( equidistant(Z,V,V2,W)
        | ~ equidistant(X,Y,V2,W)
        | ~ equidistant(X,Y,Z,V) ) ),
    inference(quant_intro,[status(thm)],[76]) ).

tff(78,plain,
    ( ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
        ( equidistant(Z,V,V2,W)
        | ~ equidistant(X,Y,V2,W)
        | ~ equidistant(X,Y,Z,V) )
  <=> ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
        ( equidistant(Z,V,V2,W)
        | ~ equidistant(X,Y,V2,W)
        | ~ equidistant(X,Y,Z,V) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(79,plain,
    ^ [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
      trans(monotonicity(rewrite(( ( ~ equidistant(X,Y,Z,V)
              | ~ equidistant(X,Y,V2,W) )
          <=> ( ~ equidistant(X,Y,V2,W)
              | ~ equidistant(X,Y,Z,V) ) )),
          ( ( ~ equidistant(X,Y,Z,V)
            | ~ equidistant(X,Y,V2,W)
            | equidistant(Z,V,V2,W) )
        <=> ( ~ equidistant(X,Y,V2,W)
            | ~ equidistant(X,Y,Z,V)
            | equidistant(Z,V,V2,W) ) )),
        rewrite(( ( ~ equidistant(X,Y,V2,W)
            | ~ equidistant(X,Y,Z,V)
            | equidistant(Z,V,V2,W) )
        <=> ( equidistant(Z,V,V2,W)
            | ~ equidistant(X,Y,V2,W)
            | ~ equidistant(X,Y,Z,V) ) )),
        ( ( ~ equidistant(X,Y,Z,V)
          | ~ equidistant(X,Y,V2,W)
          | equidistant(Z,V,V2,W) )
      <=> ( equidistant(Z,V,V2,W)
          | ~ equidistant(X,Y,V2,W)
          | ~ equidistant(X,Y,Z,V) ) )),
    inference(bind,[status(th)],[]) ).

tff(80,plain,
    ( ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
        ( ~ equidistant(X,Y,Z,V)
        | ~ equidistant(X,Y,V2,W)
        | equidistant(Z,V,V2,W) )
  <=> ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
        ( equidistant(Z,V,V2,W)
        | ~ equidistant(X,Y,V2,W)
        | ~ equidistant(X,Y,Z,V) ) ),
    inference(quant_intro,[status(thm)],[79]) ).

tff(81,axiom,
    ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
      ( ~ equidistant(X,Y,Z,V)
      | ~ equidistant(X,Y,V2,W)
      | equidistant(Z,V,V2,W) ),
    file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-0.ax',transitivity_for_equidistance) ).

tff(82,plain,
    ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
      ( equidistant(Z,V,V2,W)
      | ~ equidistant(X,Y,V2,W)
      | ~ equidistant(X,Y,Z,V) ),
    inference(modus_ponens,[status(thm)],[81,80]) ).

tff(83,plain,
    ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
      ( equidistant(Z,V,V2,W)
      | ~ equidistant(X,Y,V2,W)
      | ~ equidistant(X,Y,Z,V) ),
    inference(modus_ponens,[status(thm)],[82,78]) ).

tff(84,plain,
    ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
      ( equidistant(Z,V,V2,W)
      | ~ equidistant(X,Y,V2,W)
      | ~ equidistant(X,Y,Z,V) ),
    inference(skolemize,[status(sab)],[83]) ).

tff(85,plain,
    ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
      ( equidistant(Z,V,V2,W)
      | ~ equidistant(X,Y,V2,W)
      | ~ equidistant(X,Y,Z,V) ),
    inference(modus_ponens,[status(thm)],[84,77]) ).

tff(86,plain,
    ( ( ~ ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
            ( equidistant(Z,V,V2,W)
            | ~ equidistant(X,Y,V2,W)
            | ~ equidistant(X,Y,Z,V) )
      | equidistant(u,v,y,z)
      | ~ equidistant(w,x,y,z)
      | ~ equidistant(w,x,u,v) )
  <=> ( ~ ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
            ( equidistant(Z,V,V2,W)
            | ~ equidistant(X,Y,V2,W)
            | ~ equidistant(X,Y,Z,V) )
      | equidistant(u,v,y,z)
      | ~ equidistant(w,x,y,z)
      | ~ equidistant(w,x,u,v) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(87,plain,
    ( ~ ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
          ( equidistant(Z,V,V2,W)
          | ~ equidistant(X,Y,V2,W)
          | ~ equidistant(X,Y,Z,V) )
    | equidistant(u,v,y,z)
    | ~ equidistant(w,x,y,z)
    | ~ equidistant(w,x,u,v) ),
    inference(quant_inst,[status(thm)],[]) ).

tff(88,plain,
    ( ~ ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
          ( equidistant(Z,V,V2,W)
          | ~ equidistant(X,Y,V2,W)
          | ~ equidistant(X,Y,Z,V) )
    | equidistant(u,v,y,z)
    | ~ equidistant(w,x,y,z)
    | ~ equidistant(w,x,u,v) ),
    inference(modus_ponens,[status(thm)],[87,86]) ).

tff(89,plain,
    ~ equidistant(w,x,u,v),
    inference(unit_resolution,[status(thm)],[88,85,75,72]) ).

tff(90,plain,
    ~ equidistant(w,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))),
    inference(modus_ponens,[status(thm)],[89,69]) ).

tff(91,plain,
    ( ~ ! [W: $i,V: $i,Y: $i,X: $i] : equidistant(Y,extension(X,Y,W,V),W,V)
    | equidistant(y,extension(euclid1(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_3),extension(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),w,extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2))),y,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))) ),
    inference(quant_inst,[status(thm)],[]) ).

tff(92,plain,
    equidistant(y,extension(euclid1(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_3),extension(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),w,extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2))),y,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))),
    inference(unit_resolution,[status(thm)],[91,7]) ).

tff(93,plain,
    ( ( ~ ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
            ( equidistant(Z,V,V2,W)
            | ~ equidistant(X,Y,V2,W)
            | ~ equidistant(X,Y,Z,V) )
      | ~ equidistant(y,extension(euclid1(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_3),extension(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),w,extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2))),y,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
      | equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))) )
  <=> ( ~ ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
            ( equidistant(Z,V,V2,W)
            | ~ equidistant(X,Y,V2,W)
            | ~ equidistant(X,Y,Z,V) )
      | ~ equidistant(y,extension(euclid1(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_3),extension(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),w,extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2))),y,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
      | equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(94,plain,
    ( ( equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
      | ~ equidistant(y,extension(euclid1(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_3),extension(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),w,extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2))),y,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
      | ~ equidistant(y,extension(euclid1(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_3),extension(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),w,extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2))),y,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))) )
  <=> ( ~ equidistant(y,extension(euclid1(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_3),extension(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),w,extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2))),y,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
      | equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(95,plain,
    ( ( ~ ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
            ( equidistant(Z,V,V2,W)
            | ~ equidistant(X,Y,V2,W)
            | ~ equidistant(X,Y,Z,V) )
      | equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
      | ~ equidistant(y,extension(euclid1(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_3),extension(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),w,extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2))),y,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
      | ~ equidistant(y,extension(euclid1(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_3),extension(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),w,extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2))),y,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))) )
  <=> ( ~ ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
            ( equidistant(Z,V,V2,W)
            | ~ equidistant(X,Y,V2,W)
            | ~ equidistant(X,Y,Z,V) )
      | ~ equidistant(y,extension(euclid1(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_3),extension(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),w,extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2))),y,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
      | equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))) ) ),
    inference(monotonicity,[status(thm)],[94]) ).

tff(96,plain,
    ( ( ~ ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
            ( equidistant(Z,V,V2,W)
            | ~ equidistant(X,Y,V2,W)
            | ~ equidistant(X,Y,Z,V) )
      | equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
      | ~ equidistant(y,extension(euclid1(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_3),extension(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),w,extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2))),y,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
      | ~ equidistant(y,extension(euclid1(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_3),extension(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),w,extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2))),y,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))) )
  <=> ( ~ ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
            ( equidistant(Z,V,V2,W)
            | ~ equidistant(X,Y,V2,W)
            | ~ equidistant(X,Y,Z,V) )
      | ~ equidistant(y,extension(euclid1(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_3),extension(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),w,extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2))),y,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
      | equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))) ) ),
    inference(transitivity,[status(thm)],[95,93]) ).

tff(97,plain,
    ( ~ ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
          ( equidistant(Z,V,V2,W)
          | ~ equidistant(X,Y,V2,W)
          | ~ equidistant(X,Y,Z,V) )
    | equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
    | ~ equidistant(y,extension(euclid1(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_3),extension(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),w,extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2))),y,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
    | ~ equidistant(y,extension(euclid1(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_3),extension(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),w,extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2))),y,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))) ),
    inference(quant_inst,[status(thm)],[]) ).

tff(98,plain,
    ( ~ ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
          ( equidistant(Z,V,V2,W)
          | ~ equidistant(X,Y,V2,W)
          | ~ equidistant(X,Y,Z,V) )
    | ~ equidistant(y,extension(euclid1(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_3),extension(extension(lower_dimension_point_1,u,y,z),extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,y),w,extension(lower_dimension_point_2,lower_dimension_point_3,lower_dimension_point_1,lower_dimension_point_2))),y,inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
    | equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))) ),
    inference(modus_ponens,[status(thm)],[97,96]) ).

tff(99,plain,
    equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))),
    inference(unit_resolution,[status(thm)],[98,85,92]) ).

tff(100,plain,
    ( equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),w,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))))
  <=> equidistant(u,v,w,x) ),
    inference(monotonicity,[status(thm)],[59,21,66]) ).

tff(101,plain,
    ( equidistant(u,v,w,x)
  <=> equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),w,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)))) ),
    inference(symmetry,[status(thm)],[100]) ).

tff(102,plain,
    ( equidistant(u,v,w,x)
  <=> equidistant(u,v,w,x) ),
    inference(rewrite,[status(thm)],[]) ).

tff(103,axiom,
    equidistant(u,v,w,x),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',u_to_v_equals_w_to_x) ).

tff(104,plain,
    equidistant(u,v,w,x),
    inference(modus_ponens,[status(thm)],[103,102]) ).

tff(105,plain,
    equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),w,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)))),
    inference(modus_ponens,[status(thm)],[104,101]) ).

tff(106,plain,
    ( ( ~ ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
            ( equidistant(Z,V,V2,W)
            | ~ equidistant(X,Y,V2,W)
            | ~ equidistant(X,Y,Z,V) )
      | ~ equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),w,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))))
      | ~ equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
      | equidistant(w,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))) )
  <=> ( ~ ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
            ( equidistant(Z,V,V2,W)
            | ~ equidistant(X,Y,V2,W)
            | ~ equidistant(X,Y,Z,V) )
      | ~ equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),w,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))))
      | ~ equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
      | equidistant(w,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(107,plain,
    ( ( equidistant(w,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
      | ~ equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
      | ~ equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),w,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)))) )
  <=> ( ~ equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),w,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))))
      | ~ equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
      | equidistant(w,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(108,plain,
    ( ( ~ ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
            ( equidistant(Z,V,V2,W)
            | ~ equidistant(X,Y,V2,W)
            | ~ equidistant(X,Y,Z,V) )
      | equidistant(w,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
      | ~ equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
      | ~ equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),w,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)))) )
  <=> ( ~ ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
            ( equidistant(Z,V,V2,W)
            | ~ equidistant(X,Y,V2,W)
            | ~ equidistant(X,Y,Z,V) )
      | ~ equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),w,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))))
      | ~ equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
      | equidistant(w,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))) ) ),
    inference(monotonicity,[status(thm)],[107]) ).

tff(109,plain,
    ( ( ~ ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
            ( equidistant(Z,V,V2,W)
            | ~ equidistant(X,Y,V2,W)
            | ~ equidistant(X,Y,Z,V) )
      | equidistant(w,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
      | ~ equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
      | ~ equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),w,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)))) )
  <=> ( ~ ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
            ( equidistant(Z,V,V2,W)
            | ~ equidistant(X,Y,V2,W)
            | ~ equidistant(X,Y,Z,V) )
      | ~ equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),w,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))))
      | ~ equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
      | equidistant(w,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))) ) ),
    inference(transitivity,[status(thm)],[108,106]) ).

tff(110,plain,
    ( ~ ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
          ( equidistant(Z,V,V2,W)
          | ~ equidistant(X,Y,V2,W)
          | ~ equidistant(X,Y,Z,V) )
    | equidistant(w,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
    | ~ equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
    | ~ equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),w,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)))) ),
    inference(quant_inst,[status(thm)],[]) ).

tff(111,plain,
    ( ~ ! [W: $i,V: $i,Z: $i,Y: $i,X: $i,V2: $i] :
          ( equidistant(Z,V,V2,W)
          | ~ equidistant(X,Y,V2,W)
          | ~ equidistant(X,Y,Z,V) )
    | ~ equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),w,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))))
    | ~ equidistant(inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2)))
    | equidistant(w,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))) ),
    inference(modus_ponens,[status(thm)],[110,109]) ).

tff(112,plain,
    equidistant(w,extension(x,x,euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1)),euclid1(lower_dimension_point_3,u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),extension(lower_dimension_point_3,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1))),inner_pasch(u,u,extension(u,u,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),lower_dimension_point_1),u,u),extension(lower_dimension_point_3,v,extension(lower_dimension_point_1,v,z,lower_dimension_point_2),extension(lower_dimension_point_1,v,z,lower_dimension_point_2))),
    inference(unit_resolution,[status(thm)],[111,85,105,99]) ).

tff(113,plain,
    $false,
    inference(unit_resolution,[status(thm)],[112,90]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12  % Problem    : GEO022-2 : TPTP v9.0.0. Released v1.0.0.
% 0.11/0.12  % Command    : run_E %s %d THM
% 0.12/0.33  % Computer : n010.cluster.edu
% 0.12/0.33  % Model    : x86_64 x86_64
% 0.12/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33  % Memory   : 8042.1875MB
% 0.12/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33  % CPULimit   : 300
% 0.12/0.33  % WCLimit    : 300
% 0.12/0.33  % DateTime   : Thu Jun 19 14:07:26 EDT 2025
% 0.12/0.33  % CPUTime    : 
% 198.16/198.32  % SZS status Unsatisfiable
% 198.16/198.32  % SZS output start Proof
% See solution above
% 198.16/198.39  % E exiting
%------------------------------------------------------------------------------