%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : GEO047-2 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:12:10 AM UTC 2026
% Result : Unsatisfiable 89.72s 21.46s
% Output : Refutation 87.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 21
% Syntax : Number of formulae : 568 ( 192 unt; 0 typ; 0 def)
% Number of atoms : 1626 ( 671 equ; 0 cnn)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 5894 (1117 ~; 716 |; 0 &;4061 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 8 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 17 ( 14 usr; 9 con; 0-6 aty)
% Number of variables : 1584 ( 0 ^;1584 !; 0 ?;1584 :)
% Comments :
%------------------------------------------------------------------------------
thf(between_decl,type,
between: $i > $i > $i > $o ).
thf(u_decl,type,
u: $i ).
thf(v_decl,type,
v: $i ).
thf(x_decl,type,
x: $i ).
thf(equidistant_decl,type,
equidistant: $i > $i > $i > $i > $o ).
thf(extension_decl,type,
extension: $i > $i > $i > $i > $i ).
thf(inner_pasch_decl,type,
inner_pasch: $i > $i > $i > $i > $i > $i ).
thf(continuous_decl,type,
continuous: $i > $i > $i > $i > $i > $i > $i ).
thf(lower_dimension_point_2_decl,type,
lower_dimension_point_2: $i ).
thf(lower_dimension_point_3_decl,type,
lower_dimension_point_3: $i ).
thf(lower_dimension_point_1_decl,type,
lower_dimension_point_1: $i ).
thf(w_decl,type,
w: $i ).
thf(euclid2_decl,type,
euclid2: $i > $i > $i > $i > $i > $i ).
thf(euclid1_decl,type,
euclid1: $i > $i > $i > $i > $i > $i ).
thf(21,axiom,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',segment_construction1) ).
thf(65,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(8,axiom,
! [B: $i,A: $i] :
( ( A = B )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_for_betweeness) ).
thf(35,plain,
! [B: $i,A: $i] :
( ( A = B )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(36,plain,
! [B: $i,A: $i] :
( ( A = B )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(cnf,[status(esa)],[35]) ).
thf(37,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ ( A @ between ) ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[36]) ).
thf(5,axiom,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',segment_construction2) ).
thf(30,plain,
! [D: $i,C: $i,B: $i,A: $i] : ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(3,axiom,
! [C: $i,B: $i,A: $i] :
( ( A = B )
| ~ ( C @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',identity_for_equidistance) ).
thf(26,plain,
! [C: $i,B: $i,A: $i] :
( ( A = B )
| ~ ( C @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(27,plain,
! [C: $i,B: $i,A: $i] :
( ( A = B )
| ~ ( C @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(cnf,[status(esa)],[26]) ).
thf(28,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( C @ ( B @ ( A @ equidistant ) ) ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[27]) ).
thf(235,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) )
!= ( G @ ( G @ ( F @ ( E @ equidistant ) ) ) ) )
| ~ $true
| ( E = F ) ),
inference(paramod_ordered,[status(thm)],[30,28]) ).
thf(236,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) )
!= ( G @ ( G @ ( F @ ( E @ equidistant ) ) ) ) )
| ( E = F ) ),
inference(simp,[status(thm)],[235]) ).
thf(237,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( C @ ( B @ ( A @ extension ) ) ) )
= B ),
inference(pattern_uni,[status(thm)],[236:[bind(A,$thf( I )),bind(B,$thf( H )),bind(C,$thf( K )),bind(D,$thf( K )),bind(E,$thf( I )),bind(F,$thf( K @ ( K @ ( I @ ( H @ extension ) ) ) )),bind(G,$thf( K ))]]) ).
thf(394,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( C @ ( B @ ( A @ extension ) ) ) )
= B ),
inference(simp,[status(thm)],[237]) ).
thf(1,negated_conjecture,
~ ( x @ ( v @ ( u @ between ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_v_between_u_and_x) ).
thf(22,plain,
~ ( x @ ( v @ ( u @ between ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[1]) ).
thf(23,plain,
~ ( x @ ( v @ ( u @ between ) ) ),
inference(polarity_switch,[status(thm)],[22]) ).
thf(117,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( x @ ( v @ ( u @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[65,23]) ).
thf(118,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( x @ ( v @ ( u @ between ) ) ) ),
inference(simp,[status(thm)],[117]) ).
thf(122,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) )
!= x )
| ( B != v )
| ( A != u ) ),
inference(simp,[status(thm)],[118]) ).
thf(126,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( v @ ( u @ extension ) ) ) )
!= x ),
inference(simp,[status(thm)],[122]) ).
thf(548,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ ( B @ ( A @ extension ) ) ) )
!= ( E @ ( D @ ( v @ ( u @ extension ) ) ) ) )
| ( B != x ) ),
inference(paramod_ordered,[status(thm)],[394,126]) ).
thf(549,plain,
x != v,
inference(pattern_uni,[status(thm)],[548:[bind(A,$thf( u )),bind(B,$thf( v )),bind(C,$thf( C )),bind(D,$thf( C )),bind(E,$thf( C ))]]) ).
thf(1489,plain,
! [B: $i,A: $i] :
( ( A != x )
| ( B != v )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,549]) ).
thf(1490,plain,
! [A: $i] :
( ( A != v )
| ~ ( x @ ( A @ ( x @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[1489:[bind(A,$thf( x ))]]) ).
thf(1688,plain,
~ ( x @ ( v @ ( x @ between ) ) ),
inference(simp,[status(thm)],[1490]) ).
thf(3841,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( x @ ( v @ ( x @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[65,1688]) ).
thf(3842,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( x @ ( v @ ( x @ between ) ) ) ),
inference(simp,[status(thm)],[3841]) ).
thf(3867,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) )
!= x )
| ( B != v )
| ( A != x ) ),
inference(simp,[status(thm)],[3842]) ).
thf(3883,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( v @ ( x @ extension ) ) ) )
!= x ),
inference(simp,[status(thm)],[3867]) ).
thf(11,axiom,
x @ ( w @ ( u @ between ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',w_between_u_and_x) ).
thf(42,plain,
x @ ( w @ ( u @ between ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(66,plain,
( ( ( x @ ( w @ ( u @ between ) ) )
!= ( x @ ( v @ ( u @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[42,23]) ).
thf(67,plain,
( ( x @ ( w @ ( u @ between ) ) )
!= ( x @ ( v @ ( u @ between ) ) ) ),
inference(simp,[status(thm)],[66]) ).
thf(72,plain,
( ( x != x )
| ( w != v )
| ( u != u ) ),
inference(simp,[status(thm)],[67]) ).
thf(75,plain,
w != v,
inference(simp,[status(thm)],[72]) ).
thf(1485,plain,
! [B: $i,A: $i] :
( ( A != w )
| ( B != v )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,75]) ).
thf(1486,plain,
! [A: $i] :
( ( A != v )
| ~ ( w @ ( A @ ( w @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[1485:[bind(A,$thf( w ))]]) ).
thf(1686,plain,
~ ( w @ ( v @ ( w @ between ) ) ),
inference(simp,[status(thm)],[1486]) ).
thf(1948,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( w @ ( v @ ( w @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[65,1686]) ).
thf(1949,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( w @ ( v @ ( w @ between ) ) ) ),
inference(simp,[status(thm)],[1948]) ).
thf(1986,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) )
!= w )
| ( B != v )
| ( A != w ) ),
inference(simp,[status(thm)],[1949]) ).
thf(1992,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( v @ ( w @ extension ) ) ) )
!= w ),
inference(simp,[status(thm)],[1986]) ).
thf(10305,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ ( C @ ( v @ ( w @ extension ) ) ) ) )
| ( A != w )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,1992]) ).
thf(10306,plain,
! [C: $i,B: $i,A: $i] :
( ( A != w )
| ~ ( A @ ( C @ ( B @ ( v @ ( w @ extension ) ) ) @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[10305:[bind(A,$thf( A )),bind(B,$thf( H @ ( G @ ( v @ ( w @ extension ) ) ) )),bind(C,$thf( G )),bind(D,$thf( H ))]]) ).
thf(10373,plain,
! [B: $i,A: $i] :
~ ( w @ ( B @ ( A @ ( v @ ( w @ extension ) ) ) @ ( w @ between ) ) ),
inference(simp,[status(thm)],[10306]) ).
thf(2,axiom,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ ( D @ ( C @ equidistant ) ) ) )
| ~ ( F @ ( E @ ( B @ ( A @ equidistant ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity_for_equidistance) ).
thf(24,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ ( D @ ( C @ equidistant ) ) ) )
| ~ ( F @ ( E @ ( B @ ( A @ equidistant ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(25,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ ( D @ ( C @ equidistant ) ) ) )
| ~ ( F @ ( E @ ( B @ ( A @ equidistant ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(cnf,[status(esa)],[24]) ).
thf(98,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ $true
| ( ( F @ ( E @ ( B @ ( A @ equidistant ) ) ) )
!= ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) )
| ( F @ ( E @ ( D @ ( C @ equidistant ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(eqfactor_ordered,[status(thm)],[25]) ).
thf(99,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( D @ ( C @ equidistant ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(pattern_uni,[status(thm)],[98:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( E )),bind(D,$thf( F ))]]) ).
thf(101,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( D @ ( C @ equidistant ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[99]) ).
thf(17,axiom,
w @ ( v @ ( u @ between ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',v_between_u_and_w) ).
thf(55,plain,
w @ ( v @ ( u @ between ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(1982,plain,
( ( ( w @ ( v @ ( w @ between ) ) )
!= ( w @ ( v @ ( u @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[55,1686]) ).
thf(1983,plain,
( ( w @ ( v @ ( w @ between ) ) )
!= ( w @ ( v @ ( u @ between ) ) ) ),
inference(simp,[status(thm)],[1982]) ).
thf(1988,plain,
( ( w != w )
| ( v != v )
| ( w != u ) ),
inference(simp,[status(thm)],[1983]) ).
thf(1995,plain,
w != u,
inference(simp,[status(thm)],[1988]) ).
thf(4,axiom,
! [B: $i,A: $i] : ( A @ ( B @ ( B @ ( A @ equidistant ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_for_equidistance) ).
thf(29,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( B @ ( A @ equidistant ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(106,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ ( A @ equidistant ) ) ) )
!= ( H @ ( G @ ( D @ ( C @ equidistant ) ) ) ) )
| ( H @ ( G @ ( F @ ( E @ equidistant ) ) ) )
| ~ $true
| ~ ( F @ ( E @ ( D @ ( C @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[29,25]) ).
thf(107,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ ( A @ equidistant ) ) ) )
!= ( H @ ( G @ ( D @ ( C @ equidistant ) ) ) ) )
| ( H @ ( G @ ( F @ ( E @ equidistant ) ) ) )
| ~ ( F @ ( E @ ( D @ ( C @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[106]) ).
thf(108,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(pattern_uni,[status(thm)],[107:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B )),bind(E,$thf( E )),bind(F,$thf( F )),bind(G,$thf( B )),bind(H,$thf( A ))]]) ).
thf(110,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[108]) ).
thf(227,plain,
! [C: $i,B: $i,A: $i] :
( ( A != w )
| ( B != v )
| ~ ( C @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,75]) ).
thf(228,plain,
! [B: $i,A: $i] :
( ( A != v )
| ~ ( B @ ( B @ ( A @ ( w @ equidistant ) ) ) ) ),
inference(pattern_uni,[status(thm)],[227:[bind(A,$thf( w ))]]) ).
thf(390,plain,
! [A: $i] :
~ ( A @ ( A @ ( v @ ( w @ equidistant ) ) ) ),
inference(simp,[status(thm)],[228]) ).
thf(21134,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( v @ ( w @ equidistant ) ) ) ) )
| ~ $true
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[110,390]) ).
thf(21135,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( v @ ( w @ equidistant ) ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[21134]) ).
thf(21136,plain,
! [A: $i] :
~ ( v @ ( w @ ( A @ ( A @ equidistant ) ) ) ),
inference(pattern_uni,[status(thm)],[21135:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( w )),bind(D,$thf( v )),bind(E,$thf( A ))]]) ).
thf(9,axiom,
~ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ between ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lower_dimension2) ).
thf(38,plain,
~ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ between ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(39,plain,
~ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ between ) ) ),
inference(polarity_switch,[status(thm)],[38]) ).
thf(81,plain,
( ( ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ between ) ) )
!= ( w @ ( v @ ( u @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[55,39]) ).
thf(82,plain,
( ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ between ) ) )
!= ( w @ ( v @ ( u @ between ) ) ) ),
inference(simp,[status(thm)],[81]) ).
thf(88,plain,
( ( w != lower_dimension_point_1 )
| ( lower_dimension_point_3 != v )
| ( lower_dimension_point_2 != u ) ),
inference(simp,[status(thm)],[82]) ).
thf(540,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ ( B @ ( A @ extension ) ) ) )
!= ( G @ ( F @ ( E @ ( D @ extension ) ) ) ) )
| ( B @ ( E @ ( D @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[394,65]) ).
thf(541,plain,
! [B: $i,A: $i] : ( B @ ( B @ ( A @ between ) ) ),
inference(pattern_uni,[status(thm)],[540:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( A )),bind(E,$thf( B )),bind(F,$thf( C )),bind(G,$thf( C ))]]) ).
thf(13,axiom,
~ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ between ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lower_dimension3) ).
thf(46,plain,
~ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ between ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(47,plain,
~ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ between ) ) ),
inference(polarity_switch,[status(thm)],[46]) ).
thf(754,plain,
! [B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ between ) ) )
!= ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[541,47]) ).
thf(755,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ between ) ) )
!= ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ between ) ) ) ),
inference(simp,[status(thm)],[754]) ).
thf(763,plain,
! [B: $i,A: $i] :
( ( B != lower_dimension_point_2 )
| ( B != lower_dimension_point_1 )
| ( A != lower_dimension_point_3 ) ),
inference(simp,[status(thm)],[755]) ).
thf(767,plain,
lower_dimension_point_1 != lower_dimension_point_2,
inference(simp,[status(thm)],[763]) ).
thf(905,plain,
! [C: $i,B: $i,A: $i] :
( ( A != lower_dimension_point_1 )
| ( B != lower_dimension_point_2 )
| ~ ( C @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,767]) ).
thf(906,plain,
! [B: $i,A: $i] :
( ( A != lower_dimension_point_2 )
| ~ ( B @ ( B @ ( A @ ( lower_dimension_point_1 @ equidistant ) ) ) ) ),
inference(pattern_uni,[status(thm)],[905:[bind(A,$thf( lower_dimension_point_1 ))]]) ).
thf(909,plain,
! [A: $i] :
~ ( A @ ( A @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ equidistant ) ) ) ),
inference(simp,[status(thm)],[906]) ).
thf(1491,plain,
! [B: $i,A: $i] :
( ( B != x )
| ( A != v )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,549]) ).
thf(1492,plain,
! [A: $i] :
( ( A != v )
| ~ ( A @ ( x @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[1491:[bind(A,$thf( A )),bind(B,$thf( x ))]]) ).
thf(1689,plain,
~ ( v @ ( x @ ( v @ between ) ) ),
inference(simp,[status(thm)],[1492]) ).
thf(3944,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( v @ ( x @ ( v @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[65,1689]) ).
thf(3945,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( v @ ( x @ ( v @ between ) ) ) ),
inference(simp,[status(thm)],[3944]) ).
thf(3971,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) )
!= v )
| ( B != x )
| ( A != v ) ),
inference(simp,[status(thm)],[3945]) ).
thf(3979,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( x @ ( v @ extension ) ) ) )
!= v ),
inference(simp,[status(thm)],[3971]) ).
thf(553,plain,
! [C: $i,B: $i,A: $i] :
( ( A != x )
| ( B != v )
| ~ ( C @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,549]) ).
thf(554,plain,
! [B: $i,A: $i] :
( ( A != v )
| ~ ( B @ ( B @ ( A @ ( x @ equidistant ) ) ) ) ),
inference(pattern_uni,[status(thm)],[553:[bind(A,$thf( x ))]]) ).
thf(557,plain,
! [A: $i] :
~ ( A @ ( A @ ( v @ ( x @ equidistant ) ) ) ),
inference(simp,[status(thm)],[554]) ).
thf(567,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) )
!= ( E @ ( E @ ( v @ ( x @ equidistant ) ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[30,557]) ).
thf(568,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) )
!= ( E @ ( E @ ( v @ ( x @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[567]) ).
thf(575,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D != E )
| ( C != E )
| ( ( D @ ( C @ ( A @ ( B @ extension ) ) ) )
!= v )
| ( A != x ) ),
inference(simp,[status(thm)],[568]) ).
thf(582,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( x @ ( A @ extension ) ) ) )
!= v ),
inference(simp,[status(thm)],[575]) ).
thf(1517,plain,
! [B: $i,A: $i] :
( ( A != lower_dimension_point_1 )
| ( B != lower_dimension_point_2 )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,767]) ).
thf(1518,plain,
! [A: $i] :
( ( A != lower_dimension_point_2 )
| ~ ( lower_dimension_point_1 @ ( A @ ( lower_dimension_point_1 @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[1517:[bind(A,$thf( lower_dimension_point_1 ))]]) ).
thf(1702,plain,
~ ( lower_dimension_point_1 @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ between ) ) ),
inference(simp,[status(thm)],[1518]) ).
thf(4001,plain,
( ( ( lower_dimension_point_1 @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ between ) ) )
!= ( x @ ( w @ ( u @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[42,1702]) ).
thf(4002,plain,
( ( lower_dimension_point_1 @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ between ) ) )
!= ( x @ ( w @ ( u @ between ) ) ) ),
inference(simp,[status(thm)],[4001]) ).
thf(4075,plain,
( ( lower_dimension_point_1 != x )
| ( w != lower_dimension_point_2 )
| ( lower_dimension_point_1 != u ) ),
inference(simp,[status(thm)],[4002]) ).
thf(10,axiom,
~ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ between ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lower_dimension1) ).
thf(40,plain,
~ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ between ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(41,plain,
~ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ between ) ) ),
inference(polarity_switch,[status(thm)],[40]) ).
thf(111,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[65,41]) ).
thf(112,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ between ) ) ) ),
inference(simp,[status(thm)],[111]) ).
thf(119,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) )
!= lower_dimension_point_3 )
| ( B != lower_dimension_point_2 )
| ( A != lower_dimension_point_1 ) ),
inference(simp,[status(thm)],[112]) ).
thf(123,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ extension ) ) ) )
!= lower_dimension_point_3 ),
inference(simp,[status(thm)],[119]) ).
thf(544,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ ( B @ ( A @ extension ) ) ) )
!= ( E @ ( D @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ extension ) ) ) ) )
| ( B != lower_dimension_point_3 ) ),
inference(paramod_ordered,[status(thm)],[394,123]) ).
thf(545,plain,
lower_dimension_point_3 != lower_dimension_point_2,
inference(pattern_uni,[status(thm)],[544:[bind(A,$thf( lower_dimension_point_1 )),bind(B,$thf( lower_dimension_point_2 )),bind(C,$thf( C )),bind(D,$thf( C )),bind(E,$thf( C ))]]) ).
thf(1178,plain,
! [B: $i,A: $i] :
( ( B != lower_dimension_point_3 )
| ( A != lower_dimension_point_2 )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,545]) ).
thf(1179,plain,
! [A: $i] :
( ( A != lower_dimension_point_2 )
| ~ ( A @ ( lower_dimension_point_3 @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[1178:[bind(A,$thf( A )),bind(B,$thf( lower_dimension_point_3 ))]]) ).
thf(1552,plain,
~ ( lower_dimension_point_2 @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ between ) ) ),
inference(simp,[status(thm)],[1179]) ).
thf(1770,plain,
( ( ( lower_dimension_point_2 @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ between ) ) )
!= ( x @ ( w @ ( u @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[42,1552]) ).
thf(1771,plain,
( ( lower_dimension_point_2 @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ between ) ) )
!= ( x @ ( w @ ( u @ between ) ) ) ),
inference(simp,[status(thm)],[1770]) ).
thf(1808,plain,
( ( lower_dimension_point_2 != x )
| ( w != lower_dimension_point_3 )
| ( lower_dimension_point_2 != u ) ),
inference(simp,[status(thm)],[1771]) ).
thf(79,plain,
( ( ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ between ) ) )
!= ( w @ ( v @ ( u @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[55,41]) ).
thf(80,plain,
( ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ between ) ) )
!= ( w @ ( v @ ( u @ between ) ) ) ),
inference(simp,[status(thm)],[79]) ).
thf(87,plain,
( ( w != lower_dimension_point_3 )
| ( lower_dimension_point_2 != v )
| ( lower_dimension_point_1 != u ) ),
inference(simp,[status(thm)],[80]) ).
thf(1212,plain,
! [B: $i,A: $i] :
( ( B != lower_dimension_point_2 )
| ( w != lower_dimension_point_3 )
| ( A != v )
| ( lower_dimension_point_1 != u )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,87]) ).
thf(1213,plain,
! [A: $i] :
( ( w != lower_dimension_point_3 )
| ( A != v )
| ( lower_dimension_point_1 != u )
| ~ ( A @ ( lower_dimension_point_2 @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[1212:[bind(A,$thf( A )),bind(B,$thf( lower_dimension_point_2 ))]]) ).
thf(1569,plain,
( ( w != lower_dimension_point_3 )
| ( lower_dimension_point_1 != u )
| ~ ( v @ ( lower_dimension_point_2 @ ( v @ between ) ) ) ),
inference(simp,[status(thm)],[1213]) ).
thf(12,axiom,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( E @ ( B @ ( D @ ( A @ euclid2 ) ) ) ) @ ( E @ ( A @ between ) ) )
| ( A = B )
| ~ ( E @ ( B @ ( D @ between ) ) )
| ~ ( C @ ( B @ ( A @ between ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',euclid2) ).
thf(43,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( E @ ( B @ ( D @ ( A @ euclid2 ) ) ) ) @ ( E @ ( A @ between ) ) )
| ( A = B )
| ~ ( E @ ( B @ ( D @ between ) ) )
| ~ ( C @ ( B @ ( A @ between ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(44,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( E @ ( B @ ( D @ ( A @ euclid2 ) ) ) ) @ ( E @ ( A @ between ) ) )
| ( A = B )
| ~ ( E @ ( B @ ( D @ between ) ) )
| ~ ( C @ ( B @ ( A @ between ) ) ) ),
inference(cnf,[status(esa)],[43]) ).
thf(45,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( E @ ( B @ ( D @ ( A @ euclid2 ) ) ) ) @ ( E @ ( A @ between ) ) )
| ~ ( E @ ( B @ ( D @ between ) ) )
| ~ ( C @ ( B @ ( A @ between ) ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[44]) ).
thf(3428,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( w @ ( v @ ( u @ between ) ) )
!= ( C @ ( B @ ( A @ between ) ) ) )
| ( C @ ( E @ ( B @ ( D @ ( A @ euclid2 ) ) ) ) @ ( E @ ( A @ between ) ) )
| ~ ( E @ ( B @ ( D @ between ) ) )
| ~ $true
| ( A = B ) ),
inference(paramod_ordered,[status(thm)],[55,45]) ).
thf(3429,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( w @ ( v @ ( u @ between ) ) )
!= ( C @ ( B @ ( A @ between ) ) ) )
| ( C @ ( E @ ( B @ ( D @ ( A @ euclid2 ) ) ) ) @ ( E @ ( A @ between ) ) )
| ~ ( E @ ( B @ ( D @ between ) ) )
| ( A = B ) ),
inference(simp,[status(thm)],[3428]) ).
thf(3430,plain,
! [B: $i,A: $i] :
( ( w @ ( B @ ( v @ ( A @ ( u @ euclid2 ) ) ) ) @ ( B @ ( u @ between ) ) )
| ~ ( B @ ( v @ ( A @ between ) ) )
| ( v = u ) ),
inference(pattern_uni,[status(thm)],[3429:[bind(A,$thf( u )),bind(B,$thf( v )),bind(C,$thf( w ))]]) ).
thf(3684,plain,
! [B: $i,A: $i] :
( ( w @ ( B @ ( v @ ( A @ ( u @ euclid2 ) ) ) ) @ ( B @ ( u @ between ) ) )
| ~ ( B @ ( v @ ( A @ between ) ) )
| ( v = u ) ),
inference(simp,[status(thm)],[3430]) ).
thf(4612,plain,
! [B: $i,A: $i] :
( ( ( w @ ( v @ ( u @ between ) ) )
!= ( B @ ( v @ ( A @ between ) ) ) )
| ( w @ ( B @ ( v @ ( A @ ( u @ euclid2 ) ) ) ) @ ( B @ ( u @ between ) ) )
| ~ $true
| ( v = u ) ),
inference(paramod_ordered,[status(thm)],[55,3684]) ).
thf(4613,plain,
! [B: $i,A: $i] :
( ( ( w @ ( v @ ( u @ between ) ) )
!= ( B @ ( v @ ( A @ between ) ) ) )
| ( w @ ( B @ ( v @ ( A @ ( u @ euclid2 ) ) ) ) @ ( B @ ( u @ between ) ) )
| ( v = u ) ),
inference(simp,[status(thm)],[4612]) ).
thf(4614,plain,
( ( w @ ( w @ ( v @ ( u @ ( u @ euclid2 ) ) ) ) @ ( w @ ( u @ between ) ) )
| ( v = u ) ),
inference(pattern_uni,[status(thm)],[4613:[bind(A,$thf( u )),bind(B,$thf( w ))]]) ).
thf(2849,plain,
! [C: $i,B: $i,A: $i] :
( ( A != w )
| ( B != u )
| ~ ( C @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,1995]) ).
thf(2850,plain,
! [B: $i,A: $i] :
( ( A != u )
| ~ ( B @ ( B @ ( A @ ( w @ equidistant ) ) ) ) ),
inference(pattern_uni,[status(thm)],[2849:[bind(A,$thf( w ))]]) ).
thf(2854,plain,
! [A: $i] :
~ ( A @ ( A @ ( u @ ( w @ equidistant ) ) ) ),
inference(simp,[status(thm)],[2850]) ).
thf(113,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[65,39]) ).
thf(114,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ between ) ) ) ),
inference(simp,[status(thm)],[113]) ).
thf(120,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) )
!= lower_dimension_point_1 )
| ( B != lower_dimension_point_3 )
| ( A != lower_dimension_point_2 ) ),
inference(simp,[status(thm)],[114]) ).
thf(124,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ extension ) ) ) )
!= lower_dimension_point_1 ),
inference(simp,[status(thm)],[120]) ).
thf(542,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ ( B @ ( A @ extension ) ) ) )
!= ( E @ ( D @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ extension ) ) ) ) )
| ( B != lower_dimension_point_1 ) ),
inference(paramod_ordered,[status(thm)],[394,124]) ).
thf(543,plain,
lower_dimension_point_1 != lower_dimension_point_3,
inference(pattern_uni,[status(thm)],[542:[bind(A,$thf( lower_dimension_point_2 )),bind(B,$thf( lower_dimension_point_3 )),bind(C,$thf( C )),bind(D,$thf( C )),bind(E,$thf( C ))]]) ).
thf(1523,plain,
! [B: $i,A: $i] :
( ( B != lower_dimension_point_1 )
| ( A != lower_dimension_point_3 )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,543]) ).
thf(1524,plain,
! [A: $i] :
( ( A != lower_dimension_point_3 )
| ~ ( A @ ( lower_dimension_point_1 @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[1523:[bind(A,$thf( A )),bind(B,$thf( lower_dimension_point_1 ))]]) ).
thf(1705,plain,
~ ( lower_dimension_point_3 @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ between ) ) ),
inference(simp,[status(thm)],[1524]) ).
thf(18,axiom,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( E @ ( B @ ( D @ ( A @ euclid1 ) ) ) ) @ ( D @ ( A @ between ) ) )
| ( A = B )
| ~ ( E @ ( B @ ( D @ between ) ) )
| ~ ( C @ ( B @ ( A @ between ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',euclid1) ).
thf(56,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( E @ ( B @ ( D @ ( A @ euclid1 ) ) ) ) @ ( D @ ( A @ between ) ) )
| ( A = B )
| ~ ( E @ ( B @ ( D @ between ) ) )
| ~ ( C @ ( B @ ( A @ between ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(546,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( C @ ( B @ ( A @ extension ) ) ) )
!= ( G @ ( F @ ( D @ ( E @ extension ) ) ) ) )
| ( G @ ( F @ ( B @ ( D @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[394,30]) ).
thf(547,plain,
! [B: $i,A: $i] : ( B @ ( B @ ( A @ ( A @ equidistant ) ) ) ),
inference(pattern_uni,[status(thm)],[546:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( B )),bind(E,$thf( A )),bind(F,$thf( C )),bind(G,$thf( C ))]]) ).
thf(550,plain,
! [B: $i,A: $i] : ( B @ ( B @ ( A @ ( A @ equidistant ) ) ) ),
inference(simp,[status(thm)],[547]) ).
thf(1176,plain,
! [B: $i,A: $i] :
( ( A != lower_dimension_point_3 )
| ( B != lower_dimension_point_2 )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,545]) ).
thf(1177,plain,
! [A: $i] :
( ( A != lower_dimension_point_2 )
| ~ ( lower_dimension_point_3 @ ( A @ ( lower_dimension_point_3 @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[1176:[bind(A,$thf( lower_dimension_point_3 ))]]) ).
thf(1551,plain,
~ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ ( lower_dimension_point_3 @ between ) ) ),
inference(simp,[status(thm)],[1177]) ).
thf(1713,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ ( lower_dimension_point_3 @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[65,1551]) ).
thf(1714,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ ( lower_dimension_point_3 @ between ) ) ) ),
inference(simp,[status(thm)],[1713]) ).
thf(1749,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) )
!= lower_dimension_point_3 )
| ( B != lower_dimension_point_2 )
| ( A != lower_dimension_point_3 ) ),
inference(simp,[status(thm)],[1714]) ).
thf(1761,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( lower_dimension_point_2 @ ( lower_dimension_point_3 @ extension ) ) ) )
!= lower_dimension_point_3 ),
inference(simp,[status(thm)],[1749]) ).
thf(8003,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ ( C @ ( lower_dimension_point_2 @ ( lower_dimension_point_3 @ extension ) ) ) ) )
| ( A != lower_dimension_point_3 )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,1761]) ).
thf(8004,plain,
! [C: $i,B: $i,A: $i] :
( ( A != lower_dimension_point_3 )
| ~ ( A @ ( C @ ( B @ ( lower_dimension_point_2 @ ( lower_dimension_point_3 @ extension ) ) ) @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[8003:[bind(A,$thf( A )),bind(B,$thf( H @ ( G @ ( lower_dimension_point_2 @ ( lower_dimension_point_3 @ extension ) ) ) )),bind(C,$thf( G )),bind(D,$thf( H ))]]) ).
thf(8057,plain,
! [B: $i,A: $i] :
~ ( lower_dimension_point_3 @ ( B @ ( A @ ( lower_dimension_point_2 @ ( lower_dimension_point_3 @ extension ) ) ) @ ( lower_dimension_point_3 @ between ) ) ),
inference(simp,[status(thm)],[8004]) ).
thf(555,plain,
! [C: $i,B: $i,A: $i] :
( ( B != x )
| ( A != v )
| ~ ( C @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,549]) ).
thf(556,plain,
! [B: $i,A: $i] :
( ( A != v )
| ~ ( B @ ( B @ ( x @ ( A @ equidistant ) ) ) ) ),
inference(pattern_uni,[status(thm)],[555:[bind(A,$thf( A )),bind(B,$thf( x ))]]) ).
thf(558,plain,
! [A: $i] :
~ ( A @ ( A @ ( x @ ( v @ equidistant ) ) ) ),
inference(simp,[status(thm)],[556]) ).
thf(658,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) )
!= ( E @ ( E @ ( x @ ( v @ equidistant ) ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[30,558]) ).
thf(659,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) )
!= ( E @ ( E @ ( x @ ( v @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[658]) ).
thf(666,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D != E )
| ( C != E )
| ( ( D @ ( C @ ( A @ ( B @ extension ) ) ) )
!= x )
| ( A != v ) ),
inference(simp,[status(thm)],[659]) ).
thf(670,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( v @ ( A @ extension ) ) ) )
!= x ),
inference(simp,[status(thm)],[666]) ).
thf(70,plain,
( ( ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ between ) ) )
!= ( x @ ( w @ ( u @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[42,41]) ).
thf(71,plain,
( ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ between ) ) )
!= ( x @ ( w @ ( u @ between ) ) ) ),
inference(simp,[status(thm)],[70]) ).
thf(74,plain,
( ( lower_dimension_point_3 != x )
| ( w != lower_dimension_point_2 )
| ( lower_dimension_point_1 != u ) ),
inference(simp,[status(thm)],[71]) ).
thf(135,plain,
! [C: $i,B: $i,A: $i] :
( ( A != lower_dimension_point_1 )
| ( lower_dimension_point_3 != x )
| ( w != lower_dimension_point_2 )
| ( B != u )
| ~ ( C @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,74]) ).
thf(136,plain,
! [B: $i,A: $i] :
( ( lower_dimension_point_3 != x )
| ( w != lower_dimension_point_2 )
| ( A != u )
| ~ ( B @ ( B @ ( A @ ( lower_dimension_point_1 @ equidistant ) ) ) ) ),
inference(pattern_uni,[status(thm)],[135:[bind(A,$thf( lower_dimension_point_1 ))]]) ).
thf(320,plain,
! [A: $i] :
( ( lower_dimension_point_3 != x )
| ( w != lower_dimension_point_2 )
| ~ ( A @ ( A @ ( u @ ( lower_dimension_point_1 @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[136]) ).
thf(2851,plain,
! [C: $i,B: $i,A: $i] :
( ( B != w )
| ( A != u )
| ~ ( C @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,1995]) ).
thf(2852,plain,
! [B: $i,A: $i] :
( ( A != u )
| ~ ( B @ ( B @ ( w @ ( A @ equidistant ) ) ) ) ),
inference(pattern_uni,[status(thm)],[2851:[bind(A,$thf( A )),bind(B,$thf( w ))]]) ).
thf(2855,plain,
! [A: $i] :
~ ( A @ ( A @ ( w @ ( u @ equidistant ) ) ) ),
inference(simp,[status(thm)],[2852]) ).
thf(7302,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) )
!= ( E @ ( E @ ( w @ ( u @ equidistant ) ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[30,2855]) ).
thf(7303,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) )
!= ( E @ ( E @ ( w @ ( u @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[7302]) ).
thf(7305,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D != E )
| ( C != E )
| ( ( D @ ( C @ ( A @ ( B @ extension ) ) ) )
!= w )
| ( A != u ) ),
inference(simp,[status(thm)],[7303]) ).
thf(7311,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( u @ ( A @ extension ) ) ) )
!= w ),
inference(simp,[status(thm)],[7305]) ).
thf(644,plain,
! [C: $i,B: $i,A: $i] :
( ( A != lower_dimension_point_3 )
| ( B != lower_dimension_point_2 )
| ~ ( C @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,545]) ).
thf(645,plain,
! [B: $i,A: $i] :
( ( A != lower_dimension_point_2 )
| ~ ( B @ ( B @ ( A @ ( lower_dimension_point_3 @ equidistant ) ) ) ) ),
inference(pattern_uni,[status(thm)],[644:[bind(A,$thf( lower_dimension_point_3 ))]]) ).
thf(648,plain,
! [A: $i] :
~ ( A @ ( A @ ( lower_dimension_point_2 @ ( lower_dimension_point_3 @ equidistant ) ) ) ),
inference(simp,[status(thm)],[645]) ).
thf(21122,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( lower_dimension_point_2 @ ( lower_dimension_point_3 @ equidistant ) ) ) ) )
| ~ $true
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[110,648]) ).
thf(21123,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( lower_dimension_point_2 @ ( lower_dimension_point_3 @ equidistant ) ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[21122]) ).
thf(21124,plain,
! [A: $i] :
~ ( lower_dimension_point_2 @ ( lower_dimension_point_3 @ ( A @ ( A @ equidistant ) ) ) ),
inference(pattern_uni,[status(thm)],[21123:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( lower_dimension_point_3 )),bind(D,$thf( lower_dimension_point_2 )),bind(E,$thf( A ))]]) ).
thf(4348,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( lower_dimension_point_3 @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[65,1705]) ).
thf(4349,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( lower_dimension_point_3 @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ between ) ) ) ),
inference(simp,[status(thm)],[4348]) ).
thf(4372,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) )
!= lower_dimension_point_3 )
| ( B != lower_dimension_point_1 )
| ( A != lower_dimension_point_3 ) ),
inference(simp,[status(thm)],[4349]) ).
thf(4386,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ extension ) ) ) )
!= lower_dimension_point_3 ),
inference(simp,[status(thm)],[4372]) ).
thf(1519,plain,
! [B: $i,A: $i] :
( ( B != lower_dimension_point_1 )
| ( A != lower_dimension_point_2 )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,767]) ).
thf(1520,plain,
! [A: $i] :
( ( A != lower_dimension_point_2 )
| ~ ( A @ ( lower_dimension_point_1 @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[1519:[bind(A,$thf( A )),bind(B,$thf( lower_dimension_point_1 ))]]) ).
thf(1703,plain,
~ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ ( lower_dimension_point_2 @ between ) ) ),
inference(simp,[status(thm)],[1520]) ).
thf(15,axiom,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( H @ ( F @ ( G @ ( E @ equidistant ) ) ) )
| ( A = B )
| ~ ( F @ ( D @ ( C @ between ) ) )
| ~ ( E @ ( B @ ( A @ between ) ) )
| ~ ( H @ ( D @ ( G @ ( B @ equidistant ) ) ) )
| ~ ( H @ ( C @ ( G @ ( A @ equidistant ) ) ) )
| ~ ( F @ ( D @ ( E @ ( B @ equidistant ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',outer_five_segment) ).
thf(50,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( H @ ( F @ ( G @ ( E @ equidistant ) ) ) )
| ( A = B )
| ~ ( F @ ( D @ ( C @ between ) ) )
| ~ ( E @ ( B @ ( A @ between ) ) )
| ~ ( H @ ( D @ ( G @ ( B @ equidistant ) ) ) )
| ~ ( H @ ( C @ ( G @ ( A @ equidistant ) ) ) )
| ~ ( F @ ( D @ ( E @ ( B @ equidistant ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(51,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( H @ ( F @ ( G @ ( E @ equidistant ) ) ) )
| ( A = B )
| ~ ( F @ ( D @ ( C @ between ) ) )
| ~ ( E @ ( B @ ( A @ between ) ) )
| ~ ( H @ ( D @ ( G @ ( B @ equidistant ) ) ) )
| ~ ( H @ ( C @ ( G @ ( A @ equidistant ) ) ) )
| ~ ( F @ ( D @ ( E @ ( B @ equidistant ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(cnf,[status(esa)],[50]) ).
thf(52,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( H @ ( F @ ( G @ ( E @ equidistant ) ) ) )
| ~ ( F @ ( D @ ( C @ between ) ) )
| ~ ( E @ ( B @ ( A @ between ) ) )
| ~ ( H @ ( D @ ( G @ ( B @ equidistant ) ) ) )
| ~ ( H @ ( C @ ( G @ ( A @ equidistant ) ) ) )
| ~ ( F @ ( D @ ( E @ ( B @ equidistant ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[51]) ).
thf(115,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[65,47]) ).
thf(116,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ between ) ) ) ),
inference(simp,[status(thm)],[115]) ).
thf(121,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) )
!= lower_dimension_point_2 )
| ( B != lower_dimension_point_1 )
| ( A != lower_dimension_point_3 ) ),
inference(simp,[status(thm)],[116]) ).
thf(125,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ extension ) ) ) )
!= lower_dimension_point_2 ),
inference(simp,[status(thm)],[121]) ).
thf(85,plain,
( ( ( w @ ( v @ ( u @ between ) ) )
!= ( x @ ( v @ ( u @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[55,23]) ).
thf(86,plain,
( ( w @ ( v @ ( u @ between ) ) )
!= ( x @ ( v @ ( u @ between ) ) ) ),
inference(simp,[status(thm)],[85]) ).
thf(90,plain,
( ( w != x )
| ( v != v )
| ( u != u ) ),
inference(simp,[status(thm)],[86]) ).
thf(91,plain,
w != x,
inference(simp,[status(thm)],[90]) ).
thf(1190,plain,
! [B: $i,A: $i] :
( ( B != w )
| ( A != x )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,91]) ).
thf(1191,plain,
! [A: $i] :
( ( A != x )
| ~ ( A @ ( w @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[1190:[bind(A,$thf( A )),bind(B,$thf( w ))]]) ).
thf(1558,plain,
~ ( x @ ( w @ ( x @ between ) ) ),
inference(simp,[status(thm)],[1191]) ).
thf(1882,plain,
( ( ( x @ ( w @ ( x @ between ) ) )
!= ( x @ ( w @ ( u @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[42,1558]) ).
thf(1883,plain,
( ( x @ ( w @ ( x @ between ) ) )
!= ( x @ ( w @ ( u @ between ) ) ) ),
inference(simp,[status(thm)],[1882]) ).
thf(1918,plain,
( ( x != x )
| ( w != w )
| ( x != u ) ),
inference(simp,[status(thm)],[1883]) ).
thf(1933,plain,
x != u,
inference(simp,[status(thm)],[1918]) ).
thf(1938,plain,
! [B: $i,A: $i] :
( ( B != x )
| ( A != u )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,1933]) ).
thf(1939,plain,
! [A: $i] :
( ( A != u )
| ~ ( A @ ( x @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[1938:[bind(A,$thf( A )),bind(B,$thf( x ))]]) ).
thf(1945,plain,
~ ( u @ ( x @ ( u @ between ) ) ),
inference(simp,[status(thm)],[1939]) ).
thf(5105,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( u @ ( x @ ( u @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[65,1945]) ).
thf(5106,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( u @ ( x @ ( u @ between ) ) ) ),
inference(simp,[status(thm)],[5105]) ).
thf(5137,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) )
!= u )
| ( B != x )
| ( A != u ) ),
inference(simp,[status(thm)],[5106]) ).
thf(5150,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( x @ ( u @ extension ) ) ) )
!= u ),
inference(simp,[status(thm)],[5137]) ).
thf(13498,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ ( C @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ extension ) ) ) ) )
| ( A != lower_dimension_point_3 )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,4386]) ).
thf(13499,plain,
! [C: $i,B: $i,A: $i] :
( ( A != lower_dimension_point_3 )
| ~ ( A @ ( C @ ( B @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ extension ) ) ) @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[13498:[bind(A,$thf( A )),bind(B,$thf( H @ ( G @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ extension ) ) ) )),bind(C,$thf( G )),bind(D,$thf( H ))]]) ).
thf(13608,plain,
! [B: $i,A: $i] :
~ ( lower_dimension_point_3 @ ( B @ ( A @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ extension ) ) ) @ ( lower_dimension_point_3 @ between ) ) ),
inference(simp,[status(thm)],[13499]) ).
thf(2841,plain,
! [B: $i,A: $i] :
( ( A != w )
| ( B != u )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,1995]) ).
thf(2842,plain,
! [A: $i] :
( ( A != u )
| ~ ( w @ ( A @ ( w @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[2841:[bind(A,$thf( w ))]]) ).
thf(2856,plain,
~ ( w @ ( u @ ( w @ between ) ) ),
inference(simp,[status(thm)],[2842]) ).
thf(5216,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( w @ ( u @ ( w @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[65,2856]) ).
thf(5217,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( w @ ( u @ ( w @ between ) ) ) ),
inference(simp,[status(thm)],[5216]) ).
thf(5244,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) )
!= w )
| ( B != u )
| ( A != w ) ),
inference(simp,[status(thm)],[5217]) ).
thf(5279,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( u @ ( w @ extension ) ) ) )
!= w ),
inference(simp,[status(thm)],[5244]) ).
thf(1880,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( x @ ( w @ ( x @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[65,1558]) ).
thf(1881,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( x @ ( w @ ( x @ between ) ) ) ),
inference(simp,[status(thm)],[1880]) ).
thf(1920,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) )
!= x )
| ( B != w )
| ( A != x ) ),
inference(simp,[status(thm)],[1881]) ).
thf(1922,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( w @ ( x @ extension ) ) ) )
!= x ),
inference(simp,[status(thm)],[1920]) ).
thf(2843,plain,
! [B: $i,A: $i] :
( ( B != w )
| ( A != u )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,1995]) ).
thf(2844,plain,
! [A: $i] :
( ( A != u )
| ~ ( A @ ( w @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[2843:[bind(A,$thf( A )),bind(B,$thf( w ))]]) ).
thf(2857,plain,
~ ( u @ ( w @ ( u @ between ) ) ),
inference(simp,[status(thm)],[2844]) ).
thf(1521,plain,
! [B: $i,A: $i] :
( ( A != lower_dimension_point_1 )
| ( B != lower_dimension_point_3 )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,543]) ).
thf(1522,plain,
! [A: $i] :
( ( A != lower_dimension_point_3 )
| ~ ( lower_dimension_point_1 @ ( A @ ( lower_dimension_point_1 @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[1521:[bind(A,$thf( lower_dimension_point_1 ))]]) ).
thf(1704,plain,
~ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ ( lower_dimension_point_1 @ between ) ) ),
inference(simp,[status(thm)],[1522]) ).
thf(1210,plain,
! [B: $i,A: $i] :
( ( B != lower_dimension_point_1 )
| ( w != lower_dimension_point_3 )
| ( lower_dimension_point_2 != v )
| ( A != u )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,87]) ).
thf(1211,plain,
! [A: $i] :
( ( w != lower_dimension_point_3 )
| ( lower_dimension_point_2 != v )
| ( A != u )
| ~ ( A @ ( lower_dimension_point_1 @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[1210:[bind(A,$thf( A )),bind(B,$thf( lower_dimension_point_1 ))]]) ).
thf(1568,plain,
( ( w != lower_dimension_point_3 )
| ( lower_dimension_point_2 != v )
| ~ ( u @ ( lower_dimension_point_1 @ ( u @ between ) ) ) ),
inference(simp,[status(thm)],[1211]) ).
thf(201,plain,
! [C: $i,B: $i,A: $i] :
( ( B != w )
| ( A != x )
| ~ ( C @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,91]) ).
thf(202,plain,
! [B: $i,A: $i] :
( ( A != x )
| ~ ( B @ ( B @ ( w @ ( A @ equidistant ) ) ) ) ),
inference(pattern_uni,[status(thm)],[201:[bind(A,$thf( A )),bind(B,$thf( w ))]]) ).
thf(377,plain,
! [A: $i] :
~ ( A @ ( A @ ( w @ ( x @ equidistant ) ) ) ),
inference(simp,[status(thm)],[202]) ).
thf(436,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) )
!= ( E @ ( E @ ( w @ ( x @ equidistant ) ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[30,377]) ).
thf(437,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) )
!= ( E @ ( E @ ( w @ ( x @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[436]) ).
thf(443,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D != E )
| ( C != E )
| ( ( D @ ( C @ ( A @ ( B @ extension ) ) ) )
!= w )
| ( A != x ) ),
inference(simp,[status(thm)],[437]) ).
thf(448,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( x @ ( A @ extension ) ) ) )
!= w ),
inference(simp,[status(thm)],[443]) ).
thf(256,plain,
! [C: $i,B: $i,A: $i] :
( ( B != lower_dimension_point_3 )
| ~ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ ( A @ between ) ) )
| ~ ( C @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,47]) ).
thf(257,plain,
! [B: $i,A: $i] :
( ~ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ ( A @ between ) ) )
| ~ ( B @ ( B @ ( lower_dimension_point_3 @ ( A @ equidistant ) ) ) ) ),
inference(pattern_uni,[status(thm)],[256:[bind(A,$thf( A )),bind(B,$thf( lower_dimension_point_3 ))]]) ).
thf(316,plain,
! [B: $i,A: $i] :
( ~ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ ( A @ between ) ) )
| ~ ( B @ ( B @ ( lower_dimension_point_3 @ ( A @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[257]) ).
thf(76,plain,
( ( ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ between ) ) )
!= ( x @ ( w @ ( u @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[42,47]) ).
thf(77,plain,
( ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ between ) ) )
!= ( x @ ( w @ ( u @ between ) ) ) ),
inference(simp,[status(thm)],[76]) ).
thf(78,plain,
( ( lower_dimension_point_2 != x )
| ( w != lower_dimension_point_1 )
| ( lower_dimension_point_3 != u ) ),
inference(simp,[status(thm)],[77]) ).
thf(4146,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ ( lower_dimension_point_2 @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[65,1703]) ).
thf(4147,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ ( lower_dimension_point_2 @ between ) ) ) ),
inference(simp,[status(thm)],[4146]) ).
thf(4175,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) )
!= lower_dimension_point_2 )
| ( B != lower_dimension_point_1 )
| ( A != lower_dimension_point_2 ) ),
inference(simp,[status(thm)],[4147]) ).
thf(4184,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( lower_dimension_point_1 @ ( lower_dimension_point_2 @ extension ) ) ) )
!= lower_dimension_point_2 ),
inference(simp,[status(thm)],[4175]) ).
thf(13240,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ ( C @ ( lower_dimension_point_1 @ ( lower_dimension_point_2 @ extension ) ) ) ) )
| ( A != lower_dimension_point_2 )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,4184]) ).
thf(13241,plain,
! [C: $i,B: $i,A: $i] :
( ( A != lower_dimension_point_2 )
| ~ ( A @ ( C @ ( B @ ( lower_dimension_point_1 @ ( lower_dimension_point_2 @ extension ) ) ) @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[13240:[bind(A,$thf( A )),bind(B,$thf( H @ ( G @ ( lower_dimension_point_1 @ ( lower_dimension_point_2 @ extension ) ) ) )),bind(C,$thf( G )),bind(D,$thf( H ))]]) ).
thf(13350,plain,
! [B: $i,A: $i] :
~ ( lower_dimension_point_2 @ ( B @ ( A @ ( lower_dimension_point_1 @ ( lower_dimension_point_2 @ extension ) ) ) @ ( lower_dimension_point_2 @ between ) ) ),
inference(simp,[status(thm)],[13241]) ).
thf(1940,plain,
! [C: $i,B: $i,A: $i] :
( ( A != x )
| ( B != u )
| ~ ( C @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,1933]) ).
thf(1941,plain,
! [B: $i,A: $i] :
( ( A != u )
| ~ ( B @ ( B @ ( A @ ( x @ equidistant ) ) ) ) ),
inference(pattern_uni,[status(thm)],[1940:[bind(A,$thf( x ))]]) ).
thf(1946,plain,
! [A: $i] :
~ ( A @ ( A @ ( u @ ( x @ equidistant ) ) ) ),
inference(simp,[status(thm)],[1941]) ).
thf(4102,plain,
( ( ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ ( lower_dimension_point_2 @ between ) ) )
!= ( x @ ( w @ ( u @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[42,1703]) ).
thf(4103,plain,
( ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ ( lower_dimension_point_2 @ between ) ) )
!= ( x @ ( w @ ( u @ between ) ) ) ),
inference(simp,[status(thm)],[4102]) ).
thf(4173,plain,
( ( lower_dimension_point_2 != x )
| ( w != lower_dimension_point_1 )
| ( lower_dimension_point_2 != u ) ),
inference(simp,[status(thm)],[4103]) ).
thf(10535,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ ( C @ ( v @ ( x @ extension ) ) ) ) )
| ( A != x )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,3883]) ).
thf(10536,plain,
! [C: $i,B: $i,A: $i] :
( ( A != x )
| ~ ( A @ ( C @ ( B @ ( v @ ( x @ extension ) ) ) @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[10535:[bind(A,$thf( A )),bind(B,$thf( H @ ( G @ ( v @ ( x @ extension ) ) ) )),bind(C,$thf( G )),bind(D,$thf( H ))]]) ).
thf(10626,plain,
! [B: $i,A: $i] :
~ ( x @ ( B @ ( A @ ( v @ ( x @ extension ) ) ) @ ( x @ between ) ) ),
inference(simp,[status(thm)],[10536]) ).
thf(199,plain,
! [C: $i,B: $i,A: $i] :
( ( A != w )
| ( B != x )
| ~ ( C @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,91]) ).
thf(200,plain,
! [B: $i,A: $i] :
( ( A != x )
| ~ ( B @ ( B @ ( A @ ( w @ equidistant ) ) ) ) ),
inference(pattern_uni,[status(thm)],[199:[bind(A,$thf( w ))]]) ).
thf(376,plain,
! [A: $i] :
~ ( A @ ( A @ ( x @ ( w @ equidistant ) ) ) ),
inference(simp,[status(thm)],[200]) ).
thf(21005,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ equidistant ) ) ) ) )
| ~ $true
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[110,909]) ).
thf(21006,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ equidistant ) ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[21005]) ).
thf(21007,plain,
! [A: $i] :
~ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ ( A @ ( A @ equidistant ) ) ) ),
inference(pattern_uni,[status(thm)],[21006:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( lower_dimension_point_1 )),bind(D,$thf( lower_dimension_point_2 )),bind(E,$thf( A ))]]) ).
thf(10649,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ ( C @ ( x @ ( v @ extension ) ) ) ) )
| ( A != v )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,3979]) ).
thf(10650,plain,
! [C: $i,B: $i,A: $i] :
( ( A != v )
| ~ ( A @ ( C @ ( B @ ( x @ ( v @ extension ) ) ) @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[10649:[bind(A,$thf( A )),bind(B,$thf( H @ ( G @ ( x @ ( v @ extension ) ) ) )),bind(C,$thf( G )),bind(D,$thf( H ))]]) ).
thf(10734,plain,
! [B: $i,A: $i] :
~ ( v @ ( B @ ( A @ ( x @ ( v @ extension ) ) ) @ ( v @ between ) ) ),
inference(simp,[status(thm)],[10650]) ).
thf(21116,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( w @ ( x @ equidistant ) ) ) ) )
| ~ $true
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[110,377]) ).
thf(21117,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( w @ ( x @ equidistant ) ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[21116]) ).
thf(21118,plain,
! [A: $i] :
~ ( w @ ( x @ ( A @ ( A @ equidistant ) ) ) ),
inference(pattern_uni,[status(thm)],[21117:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( x )),bind(D,$thf( w )),bind(E,$thf( A ))]]) ).
thf(19,axiom,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( B = C )
| ( D @ ( A @ ( E @ between ) ) )
| ( A @ ( E @ ( D @ between ) ) )
| ( E @ ( D @ ( A @ between ) ) )
| ~ ( C @ ( E @ ( B @ ( E @ equidistant ) ) ) )
| ~ ( C @ ( D @ ( B @ ( D @ equidistant ) ) ) )
| ~ ( C @ ( A @ ( B @ ( A @ equidistant ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',upper_dimension) ).
thf(59,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( B = C )
| ( D @ ( A @ ( E @ between ) ) )
| ( A @ ( E @ ( D @ between ) ) )
| ( E @ ( D @ ( A @ between ) ) )
| ~ ( C @ ( E @ ( B @ ( E @ equidistant ) ) ) )
| ~ ( C @ ( D @ ( B @ ( D @ equidistant ) ) ) )
| ~ ( C @ ( A @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(60,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( B = C )
| ( D @ ( A @ ( E @ between ) ) )
| ( A @ ( E @ ( D @ between ) ) )
| ( E @ ( D @ ( A @ between ) ) )
| ~ ( C @ ( E @ ( B @ ( E @ equidistant ) ) ) )
| ~ ( C @ ( D @ ( B @ ( D @ equidistant ) ) ) )
| ~ ( C @ ( A @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(cnf,[status(esa)],[59]) ).
thf(61,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( A @ ( E @ between ) ) )
| ( A @ ( E @ ( D @ between ) ) )
| ( E @ ( D @ ( A @ between ) ) )
| ~ ( C @ ( E @ ( B @ ( E @ equidistant ) ) ) )
| ~ ( C @ ( D @ ( B @ ( D @ equidistant ) ) ) )
| ~ ( C @ ( A @ ( B @ ( A @ equidistant ) ) ) )
| ( B = C ) ),
inference(lifteq,[status(thm)],[60]) ).
thf(5327,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( u @ ( w @ ( u @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[65,2857]) ).
thf(5328,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( u @ ( w @ ( u @ between ) ) ) ),
inference(simp,[status(thm)],[5327]) ).
thf(5360,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) )
!= u )
| ( B != w )
| ( A != u ) ),
inference(simp,[status(thm)],[5328]) ).
thf(5384,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( w @ ( u @ extension ) ) ) )
!= u ),
inference(simp,[status(thm)],[5360]) ).
thf(83,plain,
( ( ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ between ) ) )
!= ( w @ ( v @ ( u @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[55,47]) ).
thf(84,plain,
( ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ between ) ) )
!= ( w @ ( v @ ( u @ between ) ) ) ),
inference(simp,[status(thm)],[83]) ).
thf(89,plain,
( ( w != lower_dimension_point_2 )
| ( lower_dimension_point_1 != v )
| ( lower_dimension_point_3 != u ) ),
inference(simp,[status(thm)],[84]) ).
thf(127,plain,
! [J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) )
!= ( H @ ( G @ ( F @ ( E @ equidistant ) ) ) ) )
| ( J @ ( I @ ( H @ ( G @ equidistant ) ) ) )
| ~ ( J @ ( I @ ( F @ ( E @ equidistant ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[30,25]) ).
thf(128,plain,
! [J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) )
!= ( H @ ( G @ ( F @ ( E @ equidistant ) ) ) ) )
| ( J @ ( I @ ( H @ ( G @ equidistant ) ) ) )
| ~ ( J @ ( I @ ( F @ ( E @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[127]) ).
thf(129,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( F @ ( E @ equidistant ) ) ) )
| ~ ( B @ ( A @ ( F @ ( E @ ( D @ ( C @ extension ) ) ) @ ( D @ equidistant ) ) ) ) ),
inference(pattern_uni,[status(thm)],[128:[bind(A,$thf( L )),bind(B,$thf( K )),bind(C,$thf( M )),bind(D,$thf( N )),bind(E,$thf( L )),bind(F,$thf( N @ ( M @ ( L @ ( K @ extension ) ) ) )),bind(G,$thf( M )),bind(H,$thf( N ))]]) ).
thf(133,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ ( F @ ( E @ equidistant ) ) ) )
| ~ ( B @ ( A @ ( F @ ( E @ ( D @ ( C @ extension ) ) ) @ ( D @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[129]) ).
thf(21131,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( w @ ( u @ equidistant ) ) ) ) )
| ~ $true
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[110,2855]) ).
thf(21132,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( w @ ( u @ equidistant ) ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[21131]) ).
thf(21133,plain,
! [A: $i] :
~ ( w @ ( u @ ( A @ ( A @ equidistant ) ) ) ),
inference(pattern_uni,[status(thm)],[21132:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( u )),bind(D,$thf( w )),bind(E,$thf( A ))]]) ).
thf(92,plain,
! [L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( F @ ( E @ ( D @ ( C @ equidistant ) ) ) )
!= ( J @ ( I @ ( H @ ( G @ equidistant ) ) ) ) )
| ( L @ ( K @ ( J @ ( I @ equidistant ) ) ) )
| ~ ( L @ ( K @ ( H @ ( G @ equidistant ) ) ) )
| ~ $true
| ~ ( F @ ( E @ ( B @ ( A @ equidistant ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[25,25]) ).
thf(93,plain,
! [L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( F @ ( E @ ( D @ ( C @ equidistant ) ) ) )
!= ( J @ ( I @ ( H @ ( G @ equidistant ) ) ) ) )
| ( L @ ( K @ ( J @ ( I @ equidistant ) ) ) )
| ~ ( L @ ( K @ ( H @ ( G @ equidistant ) ) ) )
| ~ ( F @ ( E @ ( B @ ( A @ equidistant ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[92]) ).
thf(94,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( H @ ( G @ ( F @ ( E @ equidistant ) ) ) )
| ~ ( H @ ( G @ ( D @ ( C @ equidistant ) ) ) )
| ~ ( F @ ( E @ ( B @ ( A @ equidistant ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(pattern_uni,[status(thm)],[93:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( E )),bind(F,$thf( F )),bind(G,$thf( C )),bind(H,$thf( D )),bind(I,$thf( E )),bind(J,$thf( F ))]]) ).
thf(102,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( H @ ( G @ ( F @ ( E @ equidistant ) ) ) )
| ~ ( H @ ( G @ ( D @ ( C @ equidistant ) ) ) )
| ~ ( F @ ( E @ ( B @ ( A @ equidistant ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[94]) ).
thf(7062,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) )
!= ( E @ ( E @ ( u @ ( x @ equidistant ) ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[30,1946]) ).
thf(7063,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) )
!= ( E @ ( E @ ( u @ ( x @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[7062]) ).
thf(7064,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D != E )
| ( C != E )
| ( ( D @ ( C @ ( A @ ( B @ extension ) ) ) )
!= u )
| ( A != x ) ),
inference(simp,[status(thm)],[7063]) ).
thf(7078,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( x @ ( A @ extension ) ) ) )
!= u ),
inference(simp,[status(thm)],[7064]) ).
thf(907,plain,
! [C: $i,B: $i,A: $i] :
( ( B != lower_dimension_point_1 )
| ( A != lower_dimension_point_2 )
| ~ ( C @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,767]) ).
thf(908,plain,
! [B: $i,A: $i] :
( ( A != lower_dimension_point_2 )
| ~ ( B @ ( B @ ( lower_dimension_point_1 @ ( A @ equidistant ) ) ) ) ),
inference(pattern_uni,[status(thm)],[907:[bind(A,$thf( A )),bind(B,$thf( lower_dimension_point_1 ))]]) ).
thf(910,plain,
! [A: $i] :
~ ( A @ ( A @ ( lower_dimension_point_1 @ ( lower_dimension_point_2 @ equidistant ) ) ) ),
inference(simp,[status(thm)],[908]) ).
thf(1747,plain,
( ( ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ ( lower_dimension_point_3 @ between ) ) )
!= ( w @ ( v @ ( u @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[55,1551]) ).
thf(1748,plain,
( ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ ( lower_dimension_point_3 @ between ) ) )
!= ( w @ ( v @ ( u @ between ) ) ) ),
inference(simp,[status(thm)],[1747]) ).
thf(1751,plain,
( ( w != lower_dimension_point_3 )
| ( lower_dimension_point_2 != v )
| ( lower_dimension_point_3 != u ) ),
inference(simp,[status(thm)],[1748]) ).
thf(1431,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ ( C @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ extension ) ) ) ) )
| ( A != lower_dimension_point_3 )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,123]) ).
thf(1432,plain,
! [C: $i,B: $i,A: $i] :
( ( A != lower_dimension_point_3 )
| ~ ( A @ ( C @ ( B @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ extension ) ) ) @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[1431:[bind(A,$thf( A )),bind(B,$thf( H @ ( G @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ extension ) ) ) )),bind(C,$thf( G )),bind(D,$thf( H ))]]) ).
thf(1666,plain,
! [B: $i,A: $i] :
~ ( lower_dimension_point_3 @ ( B @ ( A @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ extension ) ) ) @ ( lower_dimension_point_3 @ between ) ) ),
inference(simp,[status(thm)],[1432]) ).
thf(4045,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( lower_dimension_point_1 @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[65,1702]) ).
thf(4046,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( lower_dimension_point_1 @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ between ) ) ) ),
inference(simp,[status(thm)],[4045]) ).
thf(4071,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) )
!= lower_dimension_point_1 )
| ( B != lower_dimension_point_2 )
| ( A != lower_dimension_point_1 ) ),
inference(simp,[status(thm)],[4046]) ).
thf(4091,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ extension ) ) ) )
!= lower_dimension_point_1 ),
inference(simp,[status(thm)],[4071]) ).
thf(7,axiom,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( E @ ( D @ ( F @ ( C @ ( B @ ( A @ continuous ) ) ) ) ) @ ( C @ between ) ) )
| ~ ( D @ ( F @ ( B @ between ) ) )
| ~ ( D @ ( B @ ( A @ between ) ) )
| ~ ( E @ ( A @ ( D @ ( A @ equidistant ) ) ) )
| ~ ( C @ ( A @ ( B @ ( A @ equidistant ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',continuity1) ).
thf(33,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( E @ ( D @ ( F @ ( C @ ( B @ ( A @ continuous ) ) ) ) ) @ ( C @ between ) ) )
| ~ ( D @ ( F @ ( B @ between ) ) )
| ~ ( D @ ( B @ ( A @ between ) ) )
| ~ ( E @ ( A @ ( D @ ( A @ equidistant ) ) ) )
| ~ ( C @ ( A @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(1214,plain,
! [B: $i,A: $i] :
( ( B != w )
| ( A != lower_dimension_point_3 )
| ( lower_dimension_point_2 != v )
| ( lower_dimension_point_1 != u )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,87]) ).
thf(1215,plain,
! [A: $i] :
( ( A != lower_dimension_point_3 )
| ( lower_dimension_point_2 != v )
| ( lower_dimension_point_1 != u )
| ~ ( A @ ( w @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[1214:[bind(A,$thf( A )),bind(B,$thf( w ))]]) ).
thf(1570,plain,
( ( lower_dimension_point_2 != v )
| ( lower_dimension_point_1 != u )
| ~ ( lower_dimension_point_3 @ ( w @ ( lower_dimension_point_3 @ between ) ) ) ),
inference(simp,[status(thm)],[1215]) ).
thf(1487,plain,
! [B: $i,A: $i] :
( ( B != w )
| ( A != v )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,75]) ).
thf(1488,plain,
! [A: $i] :
( ( A != v )
| ~ ( A @ ( w @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[1487:[bind(A,$thf( A )),bind(B,$thf( w ))]]) ).
thf(1687,plain,
~ ( v @ ( w @ ( v @ between ) ) ),
inference(simp,[status(thm)],[1488]) ).
thf(1148,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ ( C @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ extension ) ) ) ) )
| ( A != lower_dimension_point_2 )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,125]) ).
thf(1149,plain,
! [C: $i,B: $i,A: $i] :
( ( A != lower_dimension_point_2 )
| ~ ( A @ ( C @ ( B @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ extension ) ) ) @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[1148:[bind(A,$thf( A )),bind(B,$thf( H @ ( G @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ extension ) ) ) )),bind(C,$thf( G )),bind(D,$thf( H ))]]) ).
thf(1541,plain,
! [B: $i,A: $i] :
~ ( lower_dimension_point_2 @ ( B @ ( A @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ extension ) ) ) @ ( lower_dimension_point_2 @ between ) ) ),
inference(simp,[status(thm)],[1149]) ).
thf(258,plain,
! [C: $i,B: $i,A: $i] :
( ( B != lower_dimension_point_1 )
| ~ ( lower_dimension_point_2 @ ( A @ ( lower_dimension_point_3 @ between ) ) )
| ~ ( C @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,47]) ).
thf(259,plain,
! [B: $i,A: $i] :
( ~ ( lower_dimension_point_2 @ ( A @ ( lower_dimension_point_3 @ between ) ) )
| ~ ( B @ ( B @ ( lower_dimension_point_1 @ ( A @ equidistant ) ) ) ) ),
inference(pattern_uni,[status(thm)],[258:[bind(A,$thf( A )),bind(B,$thf( lower_dimension_point_1 ))]]) ).
thf(317,plain,
! [B: $i,A: $i] :
( ~ ( lower_dimension_point_2 @ ( A @ ( lower_dimension_point_3 @ between ) ) )
| ~ ( B @ ( B @ ( lower_dimension_point_1 @ ( A @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[259]) ).
thf(13112,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ ( C @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ extension ) ) ) ) )
| ( A != lower_dimension_point_1 )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,4091]) ).
thf(13113,plain,
! [C: $i,B: $i,A: $i] :
( ( A != lower_dimension_point_1 )
| ~ ( A @ ( C @ ( B @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ extension ) ) ) @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[13112:[bind(A,$thf( A )),bind(B,$thf( H @ ( G @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ extension ) ) ) )),bind(C,$thf( G )),bind(D,$thf( H ))]]) ).
thf(13222,plain,
! [B: $i,A: $i] :
~ ( lower_dimension_point_1 @ ( B @ ( A @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ extension ) ) ) @ ( lower_dimension_point_1 @ between ) ) ),
inference(simp,[status(thm)],[13113]) ).
thf(1802,plain,
( ( ( lower_dimension_point_2 @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ between ) ) )
!= ( w @ ( v @ ( u @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[55,1552]) ).
thf(1803,plain,
( ( lower_dimension_point_2 @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ between ) ) )
!= ( w @ ( v @ ( u @ between ) ) ) ),
inference(simp,[status(thm)],[1802]) ).
thf(1804,plain,
( ( w != lower_dimension_point_2 )
| ( lower_dimension_point_3 != v )
| ( lower_dimension_point_2 != u ) ),
inference(simp,[status(thm)],[1803]) ).
thf(16,axiom,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ ( F @ ( C @ ( B @ ( A @ continuous ) ) ) ) ) @ ( A @ ( F @ ( A @ equidistant ) ) ) )
| ~ ( D @ ( F @ ( B @ between ) ) )
| ~ ( D @ ( B @ ( A @ between ) ) )
| ~ ( E @ ( A @ ( D @ ( A @ equidistant ) ) ) )
| ~ ( C @ ( A @ ( B @ ( A @ equidistant ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',continuity2) ).
thf(53,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ ( F @ ( C @ ( B @ ( A @ continuous ) ) ) ) ) @ ( A @ ( F @ ( A @ equidistant ) ) ) )
| ~ ( D @ ( F @ ( B @ between ) ) )
| ~ ( D @ ( B @ ( A @ between ) ) )
| ~ ( E @ ( A @ ( D @ ( A @ equidistant ) ) ) )
| ~ ( C @ ( A @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(1942,plain,
! [C: $i,B: $i,A: $i] :
( ( B != x )
| ( A != u )
| ~ ( C @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,1933]) ).
thf(1943,plain,
! [B: $i,A: $i] :
( ( A != u )
| ~ ( B @ ( B @ ( x @ ( A @ equidistant ) ) ) ) ),
inference(pattern_uni,[status(thm)],[1942:[bind(A,$thf( A )),bind(B,$thf( x ))]]) ).
thf(1947,plain,
! [A: $i] :
~ ( A @ ( A @ ( x @ ( u @ equidistant ) ) ) ),
inference(simp,[status(thm)],[1943]) ).
thf(21089,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( x @ ( u @ equidistant ) ) ) ) )
| ~ $true
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[110,1947]) ).
thf(21090,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( x @ ( u @ equidistant ) ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[21089]) ).
thf(21091,plain,
! [A: $i] :
~ ( x @ ( u @ ( A @ ( A @ equidistant ) ) ) ),
inference(pattern_uni,[status(thm)],[21090:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( u )),bind(D,$thf( x )),bind(E,$thf( A ))]]) ).
thf(640,plain,
! [C: $i,B: $i,A: $i] :
( ( B != lower_dimension_point_1 )
| ( A != lower_dimension_point_3 )
| ~ ( C @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,543]) ).
thf(641,plain,
! [B: $i,A: $i] :
( ( A != lower_dimension_point_3 )
| ~ ( B @ ( B @ ( lower_dimension_point_1 @ ( A @ equidistant ) ) ) ) ),
inference(pattern_uni,[status(thm)],[640:[bind(A,$thf( A )),bind(B,$thf( lower_dimension_point_1 ))]]) ).
thf(642,plain,
! [A: $i] :
~ ( A @ ( A @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ equidistant ) ) ) ),
inference(simp,[status(thm)],[641]) ).
thf(1513,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ ( C @ ( v @ ( u @ extension ) ) ) ) )
| ( A != x )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,126]) ).
thf(1514,plain,
! [C: $i,B: $i,A: $i] :
( ( A != x )
| ~ ( A @ ( C @ ( B @ ( v @ ( u @ extension ) ) ) @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[1513:[bind(A,$thf( A )),bind(B,$thf( H @ ( G @ ( v @ ( u @ extension ) ) ) )),bind(C,$thf( G )),bind(D,$thf( H ))]]) ).
thf(1700,plain,
! [B: $i,A: $i] :
~ ( x @ ( B @ ( A @ ( v @ ( u @ extension ) ) ) @ ( x @ between ) ) ),
inference(simp,[status(thm)],[1514]) ).
thf(103,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ ( A @ equidistant ) ) ) )
!= ( F @ ( E @ ( D @ ( C @ equidistant ) ) ) ) )
| ( H @ ( G @ ( F @ ( E @ equidistant ) ) ) )
| ~ ( H @ ( G @ ( D @ ( C @ equidistant ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[29,25]) ).
thf(104,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ ( A @ equidistant ) ) ) )
!= ( F @ ( E @ ( D @ ( C @ equidistant ) ) ) ) )
| ( H @ ( G @ ( F @ ( E @ equidistant ) ) ) )
| ~ ( H @ ( G @ ( D @ ( C @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[103]) ).
thf(105,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( A @ ( B @ equidistant ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(pattern_uni,[status(thm)],[104:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B )),bind(E,$thf( B )),bind(F,$thf( A ))]]) ).
thf(109,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( A @ ( B @ equidistant ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[105]) ).
thf(1208,plain,
! [B: $i,A: $i] :
( ( A != w )
| ( B != lower_dimension_point_3 )
| ( lower_dimension_point_2 != v )
| ( lower_dimension_point_1 != u )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,87]) ).
thf(1209,plain,
! [A: $i] :
( ( A != lower_dimension_point_3 )
| ( lower_dimension_point_2 != v )
| ( lower_dimension_point_1 != u )
| ~ ( w @ ( A @ ( w @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[1208:[bind(A,$thf( w ))]]) ).
thf(1567,plain,
( ( lower_dimension_point_2 != v )
| ( lower_dimension_point_1 != u )
| ~ ( w @ ( lower_dimension_point_3 @ ( w @ between ) ) ) ),
inference(simp,[status(thm)],[1209]) ).
thf(4203,plain,
( ( ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ ( lower_dimension_point_1 @ between ) ) )
!= ( x @ ( w @ ( u @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[42,1704]) ).
thf(4204,plain,
( ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ ( lower_dimension_point_1 @ between ) ) )
!= ( x @ ( w @ ( u @ between ) ) ) ),
inference(simp,[status(thm)],[4203]) ).
thf(4276,plain,
( ( lower_dimension_point_1 != x )
| ( w != lower_dimension_point_3 )
| ( lower_dimension_point_1 != u ) ),
inference(simp,[status(thm)],[4204]) ).
thf(229,plain,
! [C: $i,B: $i,A: $i] :
( ( B != w )
| ( A != v )
| ~ ( C @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,75]) ).
thf(230,plain,
! [B: $i,A: $i] :
( ( A != v )
| ~ ( B @ ( B @ ( w @ ( A @ equidistant ) ) ) ) ),
inference(pattern_uni,[status(thm)],[229:[bind(A,$thf( A )),bind(B,$thf( w ))]]) ).
thf(391,plain,
! [A: $i] :
~ ( A @ ( A @ ( w @ ( v @ equidistant ) ) ) ),
inference(simp,[status(thm)],[230]) ).
thf(21104,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( w @ ( v @ equidistant ) ) ) ) )
| ~ $true
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[110,391]) ).
thf(21105,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( w @ ( v @ equidistant ) ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[21104]) ).
thf(21106,plain,
! [A: $i] :
~ ( w @ ( v @ ( A @ ( A @ equidistant ) ) ) ),
inference(pattern_uni,[status(thm)],[21105:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( v )),bind(D,$thf( w )),bind(E,$thf( A ))]]) ).
thf(21125,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( v @ ( x @ equidistant ) ) ) ) )
| ~ $true
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[110,557]) ).
thf(21126,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( v @ ( x @ equidistant ) ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[21125]) ).
thf(21127,plain,
! [A: $i] :
~ ( v @ ( x @ ( A @ ( A @ equidistant ) ) ) ),
inference(pattern_uni,[status(thm)],[21126:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( x )),bind(D,$thf( v )),bind(E,$thf( A ))]]) ).
thf(4067,plain,
( ( ( lower_dimension_point_1 @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ between ) ) )
!= ( w @ ( v @ ( u @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[55,1702]) ).
thf(4068,plain,
( ( lower_dimension_point_1 @ ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ between ) ) )
!= ( w @ ( v @ ( u @ between ) ) ) ),
inference(simp,[status(thm)],[4067]) ).
thf(4069,plain,
( ( w != lower_dimension_point_1 )
| ( lower_dimension_point_2 != v )
| ( lower_dimension_point_1 != u ) ),
inference(simp,[status(thm)],[4068]) ).
thf(130,plain,
! [J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) )
!= ( J @ ( I @ ( F @ ( E @ equidistant ) ) ) ) )
| ( J @ ( I @ ( H @ ( G @ equidistant ) ) ) )
| ~ $true
| ~ ( H @ ( G @ ( F @ ( E @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[30,25]) ).
thf(131,plain,
! [J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) )
!= ( J @ ( I @ ( F @ ( E @ equidistant ) ) ) ) )
| ( J @ ( I @ ( H @ ( G @ equidistant ) ) ) )
| ~ ( H @ ( G @ ( F @ ( E @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[130]) ).
thf(132,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ ( B @ ( A @ equidistant ) ) ) )
| ~ ( B @ ( A @ ( F @ ( E @ ( D @ ( C @ extension ) ) ) @ ( D @ equidistant ) ) ) ) ),
inference(pattern_uni,[status(thm)],[131:[bind(A,$thf( L )),bind(B,$thf( K )),bind(C,$thf( M )),bind(D,$thf( N )),bind(E,$thf( L )),bind(F,$thf( N @ ( M @ ( L @ ( K @ extension ) ) ) )),bind(G,$thf( G )),bind(H,$thf( H )),bind(I,$thf( M )),bind(J,$thf( N ))]]) ).
thf(134,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ ( B @ ( A @ equidistant ) ) ) )
| ~ ( B @ ( A @ ( F @ ( E @ ( D @ ( C @ extension ) ) ) @ ( D @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[132]) ).
thf(21011,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ ( A @ equidistant ) ) ) )
!= ( F @ ( E @ ( D @ ( C @ equidistant ) ) ) ) )
| ( C @ ( D @ ( F @ ( E @ equidistant ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[550,110]) ).
thf(21012,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ ( A @ equidistant ) ) ) )
!= ( F @ ( E @ ( D @ ( C @ equidistant ) ) ) ) )
| ( C @ ( D @ ( F @ ( E @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[21011]) ).
thf(21013,plain,
! [B: $i,A: $i] : ( A @ ( A @ ( B @ ( B @ equidistant ) ) ) ),
inference(pattern_uni,[status(thm)],[21012:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( A )),bind(E,$thf( B )),bind(F,$thf( B ))]]) ).
thf(4247,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ ( lower_dimension_point_1 @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[65,1704]) ).
thf(4248,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ ( lower_dimension_point_1 @ between ) ) ) ),
inference(simp,[status(thm)],[4247]) ).
thf(4273,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) )
!= lower_dimension_point_1 )
| ( B != lower_dimension_point_3 )
| ( A != lower_dimension_point_1 ) ),
inference(simp,[status(thm)],[4248]) ).
thf(4296,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( lower_dimension_point_3 @ ( lower_dimension_point_1 @ extension ) ) ) )
!= lower_dimension_point_1 ),
inference(simp,[status(thm)],[4273]) ).
thf(13370,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ ( C @ ( lower_dimension_point_3 @ ( lower_dimension_point_1 @ extension ) ) ) ) )
| ( A != lower_dimension_point_1 )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,4296]) ).
thf(13371,plain,
! [C: $i,B: $i,A: $i] :
( ( A != lower_dimension_point_1 )
| ~ ( A @ ( C @ ( B @ ( lower_dimension_point_3 @ ( lower_dimension_point_1 @ extension ) ) ) @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[13370:[bind(A,$thf( A )),bind(B,$thf( H @ ( G @ ( lower_dimension_point_3 @ ( lower_dimension_point_1 @ extension ) ) ) )),bind(C,$thf( G )),bind(D,$thf( H ))]]) ).
thf(13480,plain,
! [B: $i,A: $i] :
~ ( lower_dimension_point_1 @ ( B @ ( A @ ( lower_dimension_point_3 @ ( lower_dimension_point_1 @ extension ) ) ) @ ( lower_dimension_point_1 @ between ) ) ),
inference(simp,[status(thm)],[13371]) ).
thf(68,plain,
( ( ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ between ) ) )
!= ( x @ ( w @ ( u @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[42,39]) ).
thf(69,plain,
( ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ between ) ) )
!= ( x @ ( w @ ( u @ between ) ) ) ),
inference(simp,[status(thm)],[68]) ).
thf(73,plain,
( ( lower_dimension_point_1 != x )
| ( w != lower_dimension_point_3 )
| ( lower_dimension_point_2 != u ) ),
inference(simp,[status(thm)],[69]) ).
thf(20,axiom,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( E @ ( B @ ( D @ ( A @ euclid2 ) ) ) ) @ ( C @ ( C @ ( E @ ( B @ ( D @ ( A @ euclid1 ) ) ) ) @ between ) ) )
| ( A = B )
| ~ ( E @ ( B @ ( D @ between ) ) )
| ~ ( C @ ( B @ ( A @ between ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',euclid3) ).
thf(62,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( E @ ( B @ ( D @ ( A @ euclid2 ) ) ) ) @ ( C @ ( C @ ( E @ ( B @ ( D @ ( A @ euclid1 ) ) ) ) @ between ) ) )
| ( A = B )
| ~ ( E @ ( B @ ( D @ between ) ) )
| ~ ( C @ ( B @ ( A @ between ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(63,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( E @ ( B @ ( D @ ( A @ euclid2 ) ) ) ) @ ( C @ ( C @ ( E @ ( B @ ( D @ ( A @ euclid1 ) ) ) ) @ between ) ) )
| ( A = B )
| ~ ( E @ ( B @ ( D @ between ) ) )
| ~ ( C @ ( B @ ( A @ between ) ) ) ),
inference(cnf,[status(esa)],[62]) ).
thf(64,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( E @ ( B @ ( D @ ( A @ euclid2 ) ) ) ) @ ( C @ ( C @ ( E @ ( B @ ( D @ ( A @ euclid1 ) ) ) ) @ between ) ) )
| ~ ( E @ ( B @ ( D @ between ) ) )
| ~ ( C @ ( B @ ( A @ between ) ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[63]) ).
thf(7142,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) )
!= ( E @ ( E @ ( x @ ( u @ equidistant ) ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[30,1947]) ).
thf(7143,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) )
!= ( E @ ( E @ ( x @ ( u @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[7142]) ).
thf(7144,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D != E )
| ( C != E )
| ( ( D @ ( C @ ( A @ ( B @ extension ) ) ) )
!= x )
| ( A != u ) ),
inference(simp,[status(thm)],[7143]) ).
thf(7165,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( u @ ( A @ extension ) ) ) )
!= x ),
inference(simp,[status(thm)],[7144]) ).
thf(1936,plain,
! [B: $i,A: $i] :
( ( A != x )
| ( B != u )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,1933]) ).
thf(1937,plain,
! [A: $i] :
( ( A != u )
| ~ ( x @ ( A @ ( x @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[1936:[bind(A,$thf( x ))]]) ).
thf(1944,plain,
~ ( x @ ( u @ ( x @ between ) ) ),
inference(simp,[status(thm)],[1937]) ).
thf(4995,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( x @ ( u @ ( x @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[65,1944]) ).
thf(4996,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( x @ ( u @ ( x @ between ) ) ) ),
inference(simp,[status(thm)],[4995]) ).
thf(5023,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) )
!= x )
| ( B != u )
| ( A != x ) ),
inference(simp,[status(thm)],[4996]) ).
thf(5043,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( u @ ( x @ extension ) ) ) )
!= x ),
inference(simp,[status(thm)],[5023]) ).
thf(4531,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ between ) ) )
!= ( D @ ( v @ ( C @ between ) ) ) )
| ( w @ ( D @ ( v @ ( C @ ( u @ euclid2 ) ) ) ) @ ( D @ ( u @ between ) ) )
| ~ $true
| ( v = u ) ),
inference(paramod_ordered,[status(thm)],[541,3684]) ).
thf(4532,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ between ) ) )
!= ( D @ ( v @ ( C @ between ) ) ) )
| ( w @ ( D @ ( v @ ( C @ ( u @ euclid2 ) ) ) ) @ ( D @ ( u @ between ) ) )
| ( v = u ) ),
inference(simp,[status(thm)],[4531]) ).
thf(4533,plain,
! [A: $i] :
( ( w @ ( v @ ( v @ ( A @ ( u @ euclid2 ) ) ) ) @ ( v @ ( u @ between ) ) )
| ( v = u ) ),
inference(pattern_uni,[status(thm)],[4532:[bind(A,$thf( A )),bind(B,$thf( v )),bind(C,$thf( A )),bind(D,$thf( v ))]]) ).
thf(8640,plain,
! [A: $i] :
( ( v != v )
| ( w @ ( u @ ( u @ between ) ) )
| ( w @ ( v @ ( v @ ( A @ ( u @ euclid2 ) ) ) ) @ ( v @ ( u @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[4533,55]) ).
thf(8641,plain,
! [A: $i] :
( ( w @ ( u @ ( u @ between ) ) )
| ( w @ ( v @ ( v @ ( A @ ( u @ euclid2 ) ) ) ) @ ( v @ ( u @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[8640:[]]) ).
thf(1715,plain,
( ( ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ ( lower_dimension_point_3 @ between ) ) )
!= ( x @ ( w @ ( u @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[42,1551]) ).
thf(1716,plain,
( ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ ( lower_dimension_point_3 @ between ) ) )
!= ( x @ ( w @ ( u @ between ) ) ) ),
inference(simp,[status(thm)],[1715]) ).
thf(1754,plain,
( ( lower_dimension_point_3 != x )
| ( w != lower_dimension_point_2 )
| ( lower_dimension_point_3 != u ) ),
inference(simp,[status(thm)],[1716]) ).
thf(6,axiom,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( D @ ( E @ ( C @ ( B @ ( A @ inner_pasch ) ) ) ) @ ( E @ between ) ) )
| ~ ( C @ ( E @ ( D @ between ) ) )
| ~ ( C @ ( B @ ( A @ between ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inner_pasch2) ).
thf(31,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( D @ ( E @ ( C @ ( B @ ( A @ inner_pasch ) ) ) ) @ ( E @ between ) ) )
| ~ ( C @ ( E @ ( D @ between ) ) )
| ~ ( C @ ( B @ ( A @ between ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(32,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( D @ ( E @ ( C @ ( B @ ( A @ inner_pasch ) ) ) ) @ ( E @ between ) ) )
| ~ ( C @ ( E @ ( D @ between ) ) )
| ~ ( C @ ( B @ ( A @ between ) ) ) ),
inference(cnf,[status(esa)],[31]) ).
thf(34,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( E @ ( D @ ( F @ ( C @ ( B @ ( A @ continuous ) ) ) ) ) @ ( C @ between ) ) )
| ~ ( D @ ( F @ ( B @ between ) ) )
| ~ ( D @ ( B @ ( A @ between ) ) )
| ~ ( E @ ( A @ ( D @ ( A @ equidistant ) ) ) )
| ~ ( C @ ( A @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(cnf,[status(esa)],[33]) ).
thf(5626,plain,
( ( v != v )
| ( w @ ( u @ ( u @ between ) ) )
| ( w @ ( w @ ( v @ ( u @ ( u @ euclid2 ) ) ) ) @ ( w @ ( u @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[4614,55]) ).
thf(5627,plain,
( ( w @ ( u @ ( u @ between ) ) )
| ( w @ ( w @ ( v @ ( u @ ( u @ euclid2 ) ) ) ) @ ( w @ ( u @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[5626:[]]) ).
thf(15391,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) )
!= ( H @ ( G @ ( F @ ( E @ equidistant ) ) ) ) )
| ( H @ ( G @ ( H @ ( G @ equidistant ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[30,101]) ).
thf(15392,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) )
!= ( H @ ( G @ ( F @ ( E @ equidistant ) ) ) ) )
| ( H @ ( G @ ( H @ ( G @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[15391]) ).
thf(15393,plain,
! [B: $i,A: $i] : ( B @ ( A @ ( B @ ( A @ equidistant ) ) ) ),
inference(pattern_uni,[status(thm)],[15392:[bind(A,$thf( J )),bind(B,$thf( I )),bind(C,$thf( K )),bind(D,$thf( L )),bind(E,$thf( J )),bind(F,$thf( L @ ( K @ ( J @ ( I @ extension ) ) ) )),bind(G,$thf( K )),bind(H,$thf( L ))]]) ).
thf(15433,plain,
! [B: $i,A: $i] : ( B @ ( A @ ( B @ ( A @ equidistant ) ) ) ),
inference(simp,[status(thm)],[15393]) ).
thf(20818,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ ( A @ equidistant ) ) ) )
!= ( F @ ( E @ ( D @ ( C @ equidistant ) ) ) ) )
| ( F @ ( E @ ( C @ ( D @ equidistant ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[15433,109]) ).
thf(20819,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ ( A @ equidistant ) ) ) )
!= ( F @ ( E @ ( D @ ( C @ equidistant ) ) ) ) )
| ( F @ ( E @ ( C @ ( D @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[20818]) ).
thf(20820,plain,
! [B: $i,A: $i] : ( B @ ( A @ ( A @ ( B @ equidistant ) ) ) ),
inference(pattern_uni,[status(thm)],[20819:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B )),bind(E,$thf( A )),bind(F,$thf( B ))]]) ).
thf(54,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( D @ ( F @ ( C @ ( B @ ( A @ continuous ) ) ) ) ) @ ( A @ ( F @ ( A @ equidistant ) ) ) )
| ~ ( D @ ( F @ ( B @ between ) ) )
| ~ ( D @ ( B @ ( A @ between ) ) )
| ~ ( E @ ( A @ ( D @ ( A @ equidistant ) ) ) )
| ~ ( C @ ( A @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(cnf,[status(esa)],[53]) ).
thf(1188,plain,
! [B: $i,A: $i] :
( ( A != w )
| ( B != x )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,91]) ).
thf(1189,plain,
! [A: $i] :
( ( A != x )
| ~ ( w @ ( A @ ( w @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[1188:[bind(A,$thf( w ))]]) ).
thf(1557,plain,
~ ( w @ ( x @ ( w @ between ) ) ),
inference(simp,[status(thm)],[1189]) ).
thf(1823,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( w @ ( x @ ( w @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[65,1557]) ).
thf(1824,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( w @ ( x @ ( w @ between ) ) ) ),
inference(simp,[status(thm)],[1823]) ).
thf(1859,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) )
!= w )
| ( B != x )
| ( A != w ) ),
inference(simp,[status(thm)],[1824]) ).
thf(1865,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( x @ ( w @ extension ) ) ) )
!= w ),
inference(simp,[status(thm)],[1859]) ).
thf(14,axiom,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( D @ ( E @ ( C @ ( B @ ( A @ inner_pasch ) ) ) ) @ ( B @ between ) ) )
| ~ ( C @ ( E @ ( D @ between ) ) )
| ~ ( C @ ( B @ ( A @ between ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',inner_pasch1) ).
thf(48,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( D @ ( E @ ( C @ ( B @ ( A @ inner_pasch ) ) ) ) @ ( B @ between ) ) )
| ~ ( C @ ( E @ ( D @ between ) ) )
| ~ ( C @ ( B @ ( A @ between ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(49,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( D @ ( E @ ( C @ ( B @ ( A @ inner_pasch ) ) ) ) @ ( B @ between ) ) )
| ~ ( C @ ( E @ ( D @ between ) ) )
| ~ ( C @ ( B @ ( A @ between ) ) ) ),
inference(cnf,[status(esa)],[48]) ).
thf(21092,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( x @ ( v @ equidistant ) ) ) ) )
| ~ $true
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[110,558]) ).
thf(21093,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( x @ ( v @ equidistant ) ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[21092]) ).
thf(21094,plain,
! [A: $i] :
~ ( x @ ( v @ ( A @ ( A @ equidistant ) ) ) ),
inference(pattern_uni,[status(thm)],[21093:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( v )),bind(D,$thf( x )),bind(E,$thf( A ))]]) ).
thf(5446,plain,
( ( ( w @ ( w @ ( v @ ( u @ ( u @ euclid2 ) ) ) ) @ ( w @ ( u @ between ) ) )
!= ( u @ ( w @ ( u @ between ) ) ) )
| ~ $true
| ( v = u ) ),
inference(paramod_ordered,[status(thm)],[4614,2857]) ).
thf(5447,plain,
( ( ( w @ ( w @ ( v @ ( u @ ( u @ euclid2 ) ) ) ) @ ( w @ ( u @ between ) ) )
!= ( u @ ( w @ ( u @ between ) ) ) )
| ( v = u ) ),
inference(simp,[status(thm)],[5446]) ).
thf(5655,plain,
( ( ( w @ ( w @ ( v @ ( u @ ( u @ euclid2 ) ) ) ) )
!= u )
| ( w != w )
| ( u != u )
| ( v = u ) ),
inference(simp,[status(thm)],[5447]) ).
thf(5671,plain,
( ( ( w @ ( w @ ( v @ ( u @ ( u @ euclid2 ) ) ) ) )
!= u )
| ( v = u ) ),
inference(simp,[status(thm)],[5655]) ).
thf(4370,plain,
( ( ( lower_dimension_point_3 @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ between ) ) )
!= ( w @ ( v @ ( u @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[55,1705]) ).
thf(4371,plain,
( ( lower_dimension_point_3 @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ between ) ) )
!= ( w @ ( v @ ( u @ between ) ) ) ),
inference(simp,[status(thm)],[4370]) ).
thf(4374,plain,
( ( w != lower_dimension_point_3 )
| ( lower_dimension_point_1 != v )
| ( lower_dimension_point_3 != u ) ),
inference(simp,[status(thm)],[4371]) ).
thf(646,plain,
! [C: $i,B: $i,A: $i] :
( ( B != lower_dimension_point_3 )
| ( A != lower_dimension_point_2 )
| ~ ( C @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,545]) ).
thf(647,plain,
! [B: $i,A: $i] :
( ( A != lower_dimension_point_2 )
| ~ ( B @ ( B @ ( lower_dimension_point_3 @ ( A @ equidistant ) ) ) ) ),
inference(pattern_uni,[status(thm)],[646:[bind(A,$thf( A )),bind(B,$thf( lower_dimension_point_3 ))]]) ).
thf(649,plain,
! [A: $i] :
~ ( A @ ( A @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ equidistant ) ) ) ),
inference(simp,[status(thm)],[647]) ).
thf(13874,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ ( C @ ( u @ ( x @ extension ) ) ) ) )
| ( A != x )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,5043]) ).
thf(13875,plain,
! [C: $i,B: $i,A: $i] :
( ( A != x )
| ~ ( A @ ( C @ ( B @ ( u @ ( x @ extension ) ) ) @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[13874:[bind(A,$thf( A )),bind(B,$thf( H @ ( G @ ( u @ ( x @ extension ) ) ) )),bind(C,$thf( G )),bind(D,$thf( H ))]]) ).
thf(13980,plain,
! [B: $i,A: $i] :
~ ( x @ ( B @ ( A @ ( u @ ( x @ extension ) ) ) @ ( x @ between ) ) ),
inference(simp,[status(thm)],[13875]) ).
thf(21050,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( x @ ( w @ equidistant ) ) ) ) )
| ~ $true
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[110,376]) ).
thf(21051,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( x @ ( w @ equidistant ) ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[21050]) ).
thf(21052,plain,
! [A: $i] :
~ ( x @ ( w @ ( A @ ( A @ equidistant ) ) ) ),
inference(pattern_uni,[status(thm)],[21051:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( w )),bind(D,$thf( x )),bind(E,$thf( A ))]]) ).
thf(21008,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( u @ ( w @ equidistant ) ) ) ) )
| ~ $true
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[110,2854]) ).
thf(21009,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( u @ ( w @ equidistant ) ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[21008]) ).
thf(21010,plain,
! [A: $i] :
~ ( u @ ( w @ ( A @ ( A @ equidistant ) ) ) ),
inference(pattern_uni,[status(thm)],[21009:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( w )),bind(D,$thf( u )),bind(E,$thf( A ))]]) ).
thf(2903,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( v @ ( w @ ( v @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[65,1687]) ).
thf(2904,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( v @ ( w @ ( v @ between ) ) ) ),
inference(simp,[status(thm)],[2903]) ).
thf(2915,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) )
!= v )
| ( B != w )
| ( A != v ) ),
inference(simp,[status(thm)],[2904]) ).
thf(2930,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( w @ ( v @ extension ) ) ) )
!= v ),
inference(simp,[status(thm)],[2915]) ).
thf(10417,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ ( C @ ( w @ ( v @ extension ) ) ) ) )
| ( A != v )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,2930]) ).
thf(10418,plain,
! [C: $i,B: $i,A: $i] :
( ( A != v )
| ~ ( A @ ( C @ ( B @ ( w @ ( v @ extension ) ) ) @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[10417:[bind(A,$thf( A )),bind(B,$thf( H @ ( G @ ( w @ ( v @ extension ) ) ) )),bind(C,$thf( G )),bind(D,$thf( H ))]]) ).
thf(10514,plain,
! [B: $i,A: $i] :
~ ( v @ ( B @ ( A @ ( w @ ( v @ extension ) ) ) @ ( v @ between ) ) ),
inference(simp,[status(thm)],[10418]) ).
thf(1340,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ ( C @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ extension ) ) ) ) )
| ( A != lower_dimension_point_1 )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,124]) ).
thf(1341,plain,
! [C: $i,B: $i,A: $i] :
( ( A != lower_dimension_point_1 )
| ~ ( A @ ( C @ ( B @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ extension ) ) ) @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[1340:[bind(A,$thf( A )),bind(B,$thf( H @ ( G @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ extension ) ) ) )),bind(C,$thf( G )),bind(D,$thf( H ))]]) ).
thf(1626,plain,
! [B: $i,A: $i] :
~ ( lower_dimension_point_1 @ ( B @ ( A @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ extension ) ) ) @ ( lower_dimension_point_1 @ between ) ) ),
inference(simp,[status(thm)],[1341]) ).
thf(638,plain,
! [C: $i,B: $i,A: $i] :
( ( A != lower_dimension_point_1 )
| ( B != lower_dimension_point_3 )
| ~ ( C @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[28,543]) ).
thf(639,plain,
! [B: $i,A: $i] :
( ( A != lower_dimension_point_3 )
| ~ ( B @ ( B @ ( A @ ( lower_dimension_point_1 @ equidistant ) ) ) ) ),
inference(pattern_uni,[status(thm)],[638:[bind(A,$thf( lower_dimension_point_1 ))]]) ).
thf(643,plain,
! [A: $i] :
~ ( A @ ( A @ ( lower_dimension_point_3 @ ( lower_dimension_point_1 @ equidistant ) ) ) ),
inference(simp,[status(thm)],[639]) ).
thf(21128,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( lower_dimension_point_3 @ ( lower_dimension_point_1 @ equidistant ) ) ) ) )
| ~ $true
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[110,643]) ).
thf(21129,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( lower_dimension_point_3 @ ( lower_dimension_point_1 @ equidistant ) ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[21128]) ).
thf(21130,plain,
! [A: $i] :
~ ( lower_dimension_point_3 @ ( lower_dimension_point_1 @ ( A @ ( A @ equidistant ) ) ) ),
inference(pattern_uni,[status(thm)],[21129:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( lower_dimension_point_1 )),bind(D,$thf( lower_dimension_point_3 )),bind(E,$thf( A ))]]) ).
thf(4269,plain,
( ( ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ ( lower_dimension_point_1 @ between ) ) )
!= ( w @ ( v @ ( u @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[55,1704]) ).
thf(4270,plain,
( ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ ( lower_dimension_point_1 @ between ) ) )
!= ( w @ ( v @ ( u @ between ) ) ) ),
inference(simp,[status(thm)],[4269]) ).
thf(4272,plain,
( ( w != lower_dimension_point_1 )
| ( lower_dimension_point_3 != v )
| ( lower_dimension_point_1 != u ) ),
inference(simp,[status(thm)],[4270]) ).
thf(1206,plain,
! [B: $i,A: $i] :
( ( A != lower_dimension_point_2 )
| ( w != lower_dimension_point_3 )
| ( B != v )
| ( lower_dimension_point_1 != u )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,87]) ).
thf(1207,plain,
! [A: $i] :
( ( w != lower_dimension_point_3 )
| ( A != v )
| ( lower_dimension_point_1 != u )
| ~ ( lower_dimension_point_2 @ ( A @ ( lower_dimension_point_2 @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[1206:[bind(A,$thf( lower_dimension_point_2 ))]]) ).
thf(1566,plain,
( ( w != lower_dimension_point_3 )
| ( lower_dimension_point_1 != u )
| ~ ( lower_dimension_point_2 @ ( v @ ( lower_dimension_point_2 @ between ) ) ) ),
inference(simp,[status(thm)],[1207]) ).
thf(4304,plain,
( ( ( lower_dimension_point_3 @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ between ) ) )
!= ( x @ ( w @ ( u @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[42,1705]) ).
thf(4305,plain,
( ( lower_dimension_point_3 @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ between ) ) )
!= ( x @ ( w @ ( u @ between ) ) ) ),
inference(simp,[status(thm)],[4304]) ).
thf(4377,plain,
( ( lower_dimension_point_3 != x )
| ( w != lower_dimension_point_1 )
| ( lower_dimension_point_3 != u ) ),
inference(simp,[status(thm)],[4305]) ).
thf(460,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) )
!= ( E @ ( E @ ( v @ ( w @ equidistant ) ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[30,390]) ).
thf(461,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) )
!= ( E @ ( E @ ( v @ ( w @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[460]) ).
thf(467,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D != E )
| ( C != E )
| ( ( D @ ( C @ ( A @ ( B @ extension ) ) ) )
!= v )
| ( A != w ) ),
inference(simp,[status(thm)],[461]) ).
thf(470,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( w @ ( A @ extension ) ) ) )
!= v ),
inference(simp,[status(thm)],[467]) ).
thf(1238,plain,
! [B: $i,A: $i] :
( ( A != lower_dimension_point_3 )
| ( w != lower_dimension_point_1 )
| ( B != v )
| ( lower_dimension_point_2 != u )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,88]) ).
thf(1239,plain,
! [A: $i] :
( ( w != lower_dimension_point_1 )
| ( A != v )
| ( lower_dimension_point_2 != u )
| ~ ( lower_dimension_point_3 @ ( A @ ( lower_dimension_point_3 @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[1238:[bind(A,$thf( lower_dimension_point_3 ))]]) ).
thf(1579,plain,
( ( w != lower_dimension_point_1 )
| ( lower_dimension_point_2 != u )
| ~ ( lower_dimension_point_3 @ ( v @ ( lower_dimension_point_3 @ between ) ) ) ),
inference(simp,[status(thm)],[1239]) ).
thf(7222,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) )
!= ( E @ ( E @ ( u @ ( w @ equidistant ) ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[30,2854]) ).
thf(7223,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) )
!= ( E @ ( E @ ( u @ ( w @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[7222]) ).
thf(7226,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D != E )
| ( C != E )
| ( ( D @ ( C @ ( A @ ( B @ extension ) ) ) )
!= u )
| ( A != w ) ),
inference(simp,[status(thm)],[7223]) ).
thf(7251,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( w @ ( A @ extension ) ) ) )
!= u ),
inference(simp,[status(thm)],[7226]) ).
thf(14219,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ ( C @ ( x @ ( u @ extension ) ) ) ) )
| ( A != u )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,5150]) ).
thf(14220,plain,
! [C: $i,B: $i,A: $i] :
( ( A != u )
| ~ ( A @ ( C @ ( B @ ( x @ ( u @ extension ) ) ) @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[14219:[bind(A,$thf( A )),bind(B,$thf( H @ ( G @ ( x @ ( u @ extension ) ) ) )),bind(C,$thf( G )),bind(D,$thf( H ))]]) ).
thf(14306,plain,
! [B: $i,A: $i] :
~ ( u @ ( B @ ( A @ ( x @ ( u @ extension ) ) ) @ ( u @ between ) ) ),
inference(simp,[status(thm)],[14220]) ).
thf(21086,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ equidistant ) ) ) ) )
| ~ $true
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[110,642]) ).
thf(21087,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ equidistant ) ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[21086]) ).
thf(21088,plain,
! [A: $i] :
~ ( lower_dimension_point_1 @ ( lower_dimension_point_3 @ ( A @ ( A @ equidistant ) ) ) ),
inference(pattern_uni,[status(thm)],[21087:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( lower_dimension_point_3 )),bind(D,$thf( lower_dimension_point_1 )),bind(E,$thf( A ))]]) ).
thf(4168,plain,
( ( ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ ( lower_dimension_point_2 @ between ) ) )
!= ( w @ ( v @ ( u @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[55,1703]) ).
thf(4169,plain,
( ( lower_dimension_point_2 @ ( lower_dimension_point_1 @ ( lower_dimension_point_2 @ between ) ) )
!= ( w @ ( v @ ( u @ between ) ) ) ),
inference(simp,[status(thm)],[4168]) ).
thf(4170,plain,
( ( w != lower_dimension_point_2 )
| ( lower_dimension_point_1 != v )
| ( lower_dimension_point_2 != u ) ),
inference(simp,[status(thm)],[4169]) ).
thf(21047,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( u @ ( x @ equidistant ) ) ) ) )
| ~ $true
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[110,1946]) ).
thf(21048,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( u @ ( x @ equidistant ) ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[21047]) ).
thf(21049,plain,
! [A: $i] :
~ ( u @ ( x @ ( A @ ( A @ equidistant ) ) ) ),
inference(pattern_uni,[status(thm)],[21048:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( x )),bind(D,$thf( u )),bind(E,$thf( A ))]]) ).
thf(57,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( E @ ( B @ ( D @ ( A @ euclid1 ) ) ) ) @ ( D @ ( A @ between ) ) )
| ( A = B )
| ~ ( E @ ( B @ ( D @ between ) ) )
| ~ ( C @ ( B @ ( A @ between ) ) ) ),
inference(cnf,[status(esa)],[56]) ).
thf(58,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( E @ ( B @ ( D @ ( A @ euclid1 ) ) ) ) @ ( D @ ( A @ between ) ) )
| ~ ( E @ ( B @ ( D @ between ) ) )
| ~ ( C @ ( B @ ( A @ between ) ) )
| ( A = B ) ),
inference(lifteq,[status(thm)],[57]) ).
thf(8187,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ ( C @ ( x @ ( w @ extension ) ) ) ) )
| ( A != w )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,1865]) ).
thf(8188,plain,
! [C: $i,B: $i,A: $i] :
( ( A != w )
| ~ ( A @ ( C @ ( B @ ( x @ ( w @ extension ) ) ) @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[8187:[bind(A,$thf( A )),bind(B,$thf( H @ ( G @ ( x @ ( w @ extension ) ) ) )),bind(C,$thf( G )),bind(D,$thf( H ))]]) ).
thf(8267,plain,
! [B: $i,A: $i] :
~ ( w @ ( B @ ( A @ ( x @ ( w @ extension ) ) ) @ ( w @ between ) ) ),
inference(simp,[status(thm)],[8188]) ).
thf(15306,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ ( A @ equidistant ) ) ) )
!= ( F @ ( E @ ( D @ ( C @ equidistant ) ) ) ) )
| ( F @ ( E @ ( F @ ( E @ equidistant ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[550,101]) ).
thf(15307,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( B @ ( A @ ( A @ equidistant ) ) ) )
!= ( F @ ( E @ ( D @ ( C @ equidistant ) ) ) ) )
| ( F @ ( E @ ( F @ ( E @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[15306]) ).
thf(15308,plain,
! [A: $i] : ( A @ ( A @ ( A @ ( A @ equidistant ) ) ) ),
inference(pattern_uni,[status(thm)],[15307:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( A )),bind(E,$thf( B )),bind(F,$thf( B ))]]) ).
thf(15425,plain,
! [A: $i] : ( A @ ( A @ ( A @ ( A @ equidistant ) ) ) ),
inference(simp,[status(thm)],[15308]) ).
thf(1768,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( lower_dimension_point_2 @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ between ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[65,1552]) ).
thf(1769,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( B @ ( A @ extension ) ) ) @ ( B @ ( A @ between ) ) )
!= ( lower_dimension_point_2 @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ between ) ) ) ),
inference(simp,[status(thm)],[1768]) ).
thf(1807,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( B @ ( A @ extension ) ) ) )
!= lower_dimension_point_2 )
| ( B != lower_dimension_point_3 )
| ( A != lower_dimension_point_2 ) ),
inference(simp,[status(thm)],[1769]) ).
thf(1816,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ extension ) ) ) )
!= lower_dimension_point_2 ),
inference(simp,[status(thm)],[1807]) ).
thf(8097,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ ( C @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ extension ) ) ) ) )
| ( A != lower_dimension_point_2 )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,1816]) ).
thf(8098,plain,
! [C: $i,B: $i,A: $i] :
( ( A != lower_dimension_point_2 )
| ~ ( A @ ( C @ ( B @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ extension ) ) ) @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[8097:[bind(A,$thf( A )),bind(B,$thf( H @ ( G @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ extension ) ) ) )),bind(C,$thf( G )),bind(D,$thf( H ))]]) ).
thf(8162,plain,
! [B: $i,A: $i] :
~ ( lower_dimension_point_2 @ ( B @ ( A @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ extension ) ) ) @ ( lower_dimension_point_2 @ between ) ) ),
inference(simp,[status(thm)],[8098]) ).
thf(412,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) )
!= ( E @ ( E @ ( x @ ( w @ equidistant ) ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[30,376]) ).
thf(413,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) )
!= ( E @ ( E @ ( x @ ( w @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[412]) ).
thf(419,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D != E )
| ( C != E )
| ( ( D @ ( C @ ( A @ ( B @ extension ) ) ) )
!= x )
| ( A != w ) ),
inference(simp,[status(thm)],[413]) ).
thf(422,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( w @ ( A @ extension ) ) ) )
!= x ),
inference(simp,[status(thm)],[419]) ).
thf(8279,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B
!= ( D @ ( C @ ( w @ ( x @ extension ) ) ) ) )
| ( A != x )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,1922]) ).
thf(8280,plain,
! [C: $i,B: $i,A: $i] :
( ( A != x )
| ~ ( A @ ( C @ ( B @ ( w @ ( x @ extension ) ) ) @ ( A @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[8279:[bind(A,$thf( A )),bind(B,$thf( H @ ( G @ ( w @ ( x @ extension ) ) ) )),bind(C,$thf( G )),bind(D,$thf( H ))]]) ).
thf(8341,plain,
! [B: $i,A: $i] :
~ ( x @ ( B @ ( A @ ( w @ ( x @ extension ) ) ) @ ( x @ between ) ) ),
inference(simp,[status(thm)],[8280]) ).
thf(15335,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ ( A @ equidistant ) ) ) )
!= ( F @ ( E @ ( D @ ( C @ equidistant ) ) ) ) )
| ( F @ ( E @ ( F @ ( E @ equidistant ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[29,101]) ).
thf(15336,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( B @ ( A @ equidistant ) ) ) )
!= ( F @ ( E @ ( D @ ( C @ equidistant ) ) ) ) )
| ( F @ ( E @ ( F @ ( E @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[15335]) ).
thf(15337,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( A @ ( B @ equidistant ) ) ) ),
inference(pattern_uni,[status(thm)],[15336:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B )),bind(E,$thf( B )),bind(F,$thf( A ))]]) ).
thf(1236,plain,
! [B: $i,A: $i] :
( ( A != lower_dimension_point_2 )
| ( w != lower_dimension_point_1 )
| ( lower_dimension_point_3 != v )
| ( B != u )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,88]) ).
thf(1237,plain,
! [A: $i] :
( ( w != lower_dimension_point_1 )
| ( lower_dimension_point_3 != v )
| ( A != u )
| ~ ( lower_dimension_point_2 @ ( A @ ( lower_dimension_point_2 @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[1236:[bind(A,$thf( lower_dimension_point_2 ))]]) ).
thf(1578,plain,
( ( w != lower_dimension_point_1 )
| ( lower_dimension_point_3 != v )
| ~ ( lower_dimension_point_2 @ ( u @ ( lower_dimension_point_2 @ between ) ) ) ),
inference(simp,[status(thm)],[1237]) ).
thf(21119,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ equidistant ) ) ) ) )
| ~ $true
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[110,649]) ).
thf(21120,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ equidistant ) ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[21119]) ).
thf(21121,plain,
! [A: $i] :
~ ( lower_dimension_point_3 @ ( lower_dimension_point_2 @ ( A @ ( A @ equidistant ) ) ) ),
inference(pattern_uni,[status(thm)],[21120:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( lower_dimension_point_2 )),bind(D,$thf( lower_dimension_point_3 )),bind(E,$thf( A ))]]) ).
thf(21074,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( lower_dimension_point_1 @ ( lower_dimension_point_2 @ equidistant ) ) ) ) )
| ~ $true
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[110,910]) ).
thf(21075,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( D @ ( C @ equidistant ) ) ) )
!= ( E @ ( E @ ( lower_dimension_point_1 @ ( lower_dimension_point_2 @ equidistant ) ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[21074]) ).
thf(21076,plain,
! [A: $i] :
~ ( lower_dimension_point_1 @ ( lower_dimension_point_2 @ ( A @ ( A @ equidistant ) ) ) ),
inference(pattern_uni,[status(thm)],[21075:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( lower_dimension_point_2 )),bind(D,$thf( lower_dimension_point_1 )),bind(E,$thf( A ))]]) ).
thf(1204,plain,
! [B: $i,A: $i] :
( ( A != lower_dimension_point_1 )
| ( w != lower_dimension_point_3 )
| ( lower_dimension_point_2 != v )
| ( B != u )
| ~ ( A @ ( B @ ( A @ between ) ) ) ),
inference(paramod_ordered,[status(thm)],[37,87]) ).
thf(1205,plain,
! [A: $i] :
( ( w != lower_dimension_point_3 )
| ( lower_dimension_point_2 != v )
| ( A != u )
| ~ ( lower_dimension_point_1 @ ( A @ ( lower_dimension_point_1 @ between ) ) ) ),
inference(pattern_uni,[status(thm)],[1204:[bind(A,$thf( lower_dimension_point_1 ))]]) ).
thf(1565,plain,
( ( w != lower_dimension_point_3 )
| ( lower_dimension_point_2 != v )
| ~ ( lower_dimension_point_1 @ ( u @ ( lower_dimension_point_1 @ between ) ) ) ),
inference(simp,[status(thm)],[1205]) ).
thf(484,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) )
!= ( E @ ( E @ ( w @ ( v @ equidistant ) ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[30,391]) ).
thf(485,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ ( D @ ( C @ ( A @ ( B @ extension ) ) ) @ ( A @ equidistant ) ) ) )
!= ( E @ ( E @ ( w @ ( v @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[484]) ).
thf(491,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( D != E )
| ( C != E )
| ( ( D @ ( C @ ( A @ ( B @ extension ) ) ) )
!= w )
| ( A != v ) ),
inference(simp,[status(thm)],[485]) ).
thf(496,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( v @ ( A @ extension ) ) ) )
!= w ),
inference(simp,[status(thm)],[491]) ).
thf(95,plain,
! [L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( F @ ( E @ ( D @ ( C @ equidistant ) ) ) )
!= ( L @ ( K @ ( H @ ( G @ equidistant ) ) ) ) )
| ( L @ ( K @ ( J @ ( I @ equidistant ) ) ) )
| ~ $true
| ~ ( J @ ( I @ ( H @ ( G @ equidistant ) ) ) )
| ~ ( F @ ( E @ ( B @ ( A @ equidistant ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(paramod_ordered,[status(thm)],[25,25]) ).
thf(96,plain,
! [L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( F @ ( E @ ( D @ ( C @ equidistant ) ) ) )
!= ( L @ ( K @ ( H @ ( G @ equidistant ) ) ) ) )
| ( L @ ( K @ ( J @ ( I @ equidistant ) ) ) )
| ~ ( J @ ( I @ ( H @ ( G @ equidistant ) ) ) )
| ~ ( F @ ( E @ ( B @ ( A @ equidistant ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[95]) ).
thf(97,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ ( H @ ( G @ equidistant ) ) ) )
| ~ ( H @ ( G @ ( D @ ( C @ equidistant ) ) ) )
| ~ ( F @ ( E @ ( B @ ( A @ equidistant ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(pattern_uni,[status(thm)],[96:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( E )),bind(F,$thf( F )),bind(G,$thf( C )),bind(H,$thf( D )),bind(I,$thf( I )),bind(J,$thf( J )),bind(K,$thf( E )),bind(L,$thf( F ))]]) ).
thf(100,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( F @ ( E @ ( H @ ( G @ equidistant ) ) ) )
| ~ ( H @ ( G @ ( D @ ( C @ equidistant ) ) ) )
| ~ ( F @ ( E @ ( B @ ( A @ equidistant ) ) ) )
| ~ ( D @ ( C @ ( B @ ( A @ equidistant ) ) ) ) ),
inference(simp,[status(thm)],[97]) ).
thf(40697,plain,
$false,
inference(e,[status(thm)],[3883,10373,101,1995,21136,88,1686,909,3979,582,4075,1808,1569,4614,2854,1705,56,550,8057,1761,670,42,24,320,25,7311,21124,4386,37,1703,52,110,125,5150,1992,13608,5279,1922,2857,1704,46,1568,448,316,78,13350,29,1946,4173,10626,376,21007,10734,21118,61,5384,74,89,133,21133,102,7078,910,1751,1666,4091,33,1570,28,38,65,1687,1541,317,13222,1804,53,21091,642,1700,109,1567,124,4276,21106,21127,1552,1947,41,4069,134,21013,541,558,13480,73,4184,45,64,7165,5043,8641,1754,32,34,22,5627,20820,59,545,15433,391,54,1865,49,21094,5671,2856,4374,377,1933,39,649,1557,13980,91,4296,1688,21052,21010,10514,394,35,1626,648,123,21130,1551,48,557,4272,1566,4377,50,470,1579,643,31,1702,7251,43,3684,14306,21088,87,4170,2855,40,26,390,55,23,1558,75,1689,21049,58,8267,549,15425,8162,30,422,2930,8341,15337,1578,126,1816,767,21121,47,62,4533,21076,1944,1945,1565,543,496,100]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO047-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.13/0.39 % Computer : n010.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Fri Sep 25 12:35:59 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.90/0.96 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.31/1.17 % [INFO] Parsing done (202ms).
% 1.31/1.18 % [INFO] Running in sequential loop mode.
% 2.03/1.58 % [INFO] eprover registered as external prover.
% 2.03/1.58 % [INFO] Scanning for conjecture ...
% 2.24/1.67 % [INFO] Found a conjecture (or negated_conjecture) and 20 axioms. Running axiom selection ...
% 2.45/1.74 % [INFO] Axiom selection finished. Selected 20 axioms (removed 0 axioms).
% 2.45/1.79 % [INFO] Problem is propositional (TPTP CNF).
% 2.45/1.79 % [INFO] Type checking passed.
% 2.69/1.80 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 89.72/21.46 % External prover 'e' found a proof!
% 89.72/21.46 % [INFO] Killing All external provers ...
% 89.72/21.46 % Time passed: 20929ms (effective reasoning time: 20273ms)
% 89.72/21.46 % Axioms used in derivation (20): euclid3, continuity1, lower_dimension1, continuity2, transitivity_for_equidistance, w_between_u_and_x, inner_pasch2, reflexivity_for_equidistance, lower_dimension2, identity_for_betweeness, outer_five_segment, upper_dimension, euclid1, segment_construction2, lower_dimension3, inner_pasch1, identity_for_equidistance, v_between_u_and_w, segment_construction1, euclid2
% 89.72/21.46 % No. of inferences in proof: 568
% 89.72/21.46 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p : 20929 ms resp. 20273 ms w/o parsing
% 87.94/21.73 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 87.94/21.74 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------