%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GEO012-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n013.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 : Fri Sep 25 01:19:32 PM UTC 2026
% Result : Unsatisfiable 27.10s 4.77s
% Output : CNFRefutation 27.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 58
% Number of leaves : 33
% Syntax : Number of formulae : 489 ( 25 unt; 0 def)
% Number of atoms : 2021 ( 177 equ)
% Maximal formula atoms : 8 ( 4 avg)
% Number of connectives : 1781 ( 249 ~;1532 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 316 ( 0 sgn 316 !; 0 ?; 218 :)
% Comments :
%------------------------------------------------------------------------------
fof(f19,axiom,
! [X2,X0,X1] :
( colinear(X0,X1,X2)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-1.ax',colinearity1) ).
fof(f20,axiom,
! [X2,X0,X1] :
( colinear(X2,X0,X1)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-1.ax',colinearity2) ).
fof(f21,axiom,
! [X2,X0,X1] :
( colinear(X1,X2,X0)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-1.ax',colinearity3) ).
fof(f22,axiom,
! [X2,X0,X1] :
( between(X2,X0,X1)
| between(X1,X2,X0)
| between(X0,X1,X2)
| ~ colinear(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GEO002-1.ax',colinearity4) ).
fof(f56,axiom,
! [X0,X1] : between(X0,X1,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3) ).
fof(f58,axiom,
! [X2,X0,X1] :
( between(X2,X1,X0)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1) ).
fof(f59,axiom,
! [X0,X1] : between(X0,X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2) ).
fof(f60,axiom,
! [X2,X0,X1] :
( X0 = X1
| ~ between(X1,X0,X2)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b2) ).
fof(f61,axiom,
! [X2,X0,X1] :
( X1 = X2
| ~ between(X0,X2,X1)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b3) ).
fof(f65,axiom,
! [X2,X3,X0,X1] :
( between(X1,X2,X3)
| ~ between(X0,X2,X3)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b5) ).
fof(f66,axiom,
! [X2,X3,X0,X1] :
( X1 = X2
| between(X0,X2,X3)
| ~ between(X1,X2,X3)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b6) ).
fof(f67,axiom,
! [X2,X3,X0,X1] :
( X1 = X2
| between(X0,X1,X3)
| ~ between(X1,X2,X3)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b7) ).
fof(f68,axiom,
! [X2,X3,X0,X1] :
( between(X0,X3,X2)
| ~ between(X1,X3,X2)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b8) ).
fof(f69,axiom,
! [X2,X3,X0,X1] :
( between(X0,X1,X3)
| ~ between(X0,X2,X3)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b9) ).
fof(f90,axiom,
! [X2,X3,X0,X1] :
( between(X0,X3,X2)
| between(X0,X2,X3)
| X0 = X1
| ~ between(X0,X1,X3)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b12) ).
fof(f91,axiom,
! [X2,X3,X0,X1] :
( between(X1,X3,X2)
| between(X1,X2,X3)
| X0 = X1
| ~ between(X0,X1,X3)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b13) ).
fof(f92,axiom,
! [X2,X3,X0,X1] :
( between(X3,X0,X1)
| between(X0,X3,X1)
| X1 = X2
| ~ between(X3,X1,X2)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7) ).
fof(f93,axiom,
! [X2,X3,X0,X1] :
( between(X0,X3,X1)
| between(X0,X1,X3)
| ~ between(X0,X3,X2)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t9) ).
fof(f94,axiom,
! [X2,X3,X0,X1] :
( between(X3,X1,X2)
| between(X1,X3,X2)
| ~ between(X0,X3,X2)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b14) ).
fof(f95,axiom,
! [X2,X3,X0,X1,X4] :
( between(X0,X3,X2)
| ~ between(X0,X4,X2)
| ~ between(X1,X3,X4)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8) ).
fof(f97,axiom,
! [X2,X0,X1] :
( colinear(X2,X1,X0)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c2_1) ).
fof(f98,axiom,
! [X2,X0,X1] :
( colinear(X0,X2,X1)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c2_2) ).
fof(f99,axiom,
! [X2,X0,X1] :
( colinear(X1,X0,X2)
| ~ between(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c2_3) ).
fof(f101,axiom,
! [X2,X0,X1] :
( colinear(X1,X2,X0)
| ~ colinear(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t10_2) ).
fof(f102,axiom,
! [X2,X0,X1] :
( colinear(X0,X2,X1)
| ~ colinear(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t10_3) ).
fof(f103,axiom,
! [X2,X0,X1] :
( colinear(X2,X0,X1)
| ~ colinear(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t10_4) ).
fof(f104,axiom,
! [X2,X0,X1] :
( colinear(X1,X0,X2)
| ~ colinear(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t10_5) ).
fof(f106,axiom,
! [X0,X1] : colinear(X0,X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c3_1) ).
fof(f109,axiom,
! [X2,X0,X1] :
( colinear(X0,X2,X1)
| X0 != X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c3_4) ).
fof(f111,axiom,
a != b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_not_b) ).
fof(f112,axiom,
colinear(a,b,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',abc_colinear) ).
fof(f113,axiom,
colinear(a,b,d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',abd_colinear) ).
fof(f114,negated_conjecture,
( ~ colinear(b,c,d)
| ~ colinear(a,c,d) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_colinearity) ).
fof(f130,plain,
! [X2,X1] : colinear(X1,X2,X1),
inference(equality_resolution,[],[f109]) ).
tcf(c_172,plain,
! [X0: $i,X1: $i,X2: $i] :
( colinear(X0,X1,X2)
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[],[f19]) ).
tcf(c_173,plain,
! [X0: $i,X1: $i,X2: $i] :
( colinear(X2,X0,X1)
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_174,plain,
! [X0: $i,X1: $i,X2: $i] :
( colinear(X1,X2,X0)
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_175,plain,
! [X0: $i,X1: $i,X2: $i] :
( between(X2,X0,X1)
| between(X1,X2,X0)
| between(X0,X1,X2)
| ~ colinear(X0,X1,X2) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_200,plain,
! [X0: $i,X1: $i] : between(X0,X1,X1),
inference(cnf_transformation,[],[f56]) ).
tcf(c_202,plain,
! [X0: $i,X1: $i,X2: $i] :
( between(X2,X1,X0)
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_203,plain,
! [X0: $i,X1: $i] : between(X0,X0,X1),
inference(cnf_transformation,[],[f59]) ).
tcf(c_204,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = X1 )
| ~ between(X1,X0,X2)
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_205,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X1 = X2 )
| ~ between(X0,X2,X1)
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[],[f61]) ).
tcf(c_208,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( between(X1,X2,X3)
| ~ between(X0,X2,X3)
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[],[f65]) ).
tcf(c_209,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( between(X3,X1,X2)
| ( X0 = X1 )
| ~ between(X3,X0,X1)
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_210,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( between(X3,X0,X2)
| ( X0 = X1 )
| ~ between(X3,X0,X1)
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_211,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( between(X3,X1,X2)
| ~ between(X3,X0,X2)
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_212,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( between(X0,X1,X3)
| ~ between(X0,X2,X3)
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[],[f69]) ).
tcf(c_231,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( between(X0,X3,X2)
| between(X0,X2,X3)
| ( X0 = X1 )
| ~ between(X0,X1,X3)
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_232,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( between(X1,X3,X2)
| between(X1,X2,X3)
| ( X0 = X1 )
| ~ between(X0,X1,X3)
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[],[f91]) ).
tcf(c_233,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( between(X3,X0,X1)
| between(X0,X3,X1)
| ( X1 = X2 )
| ~ between(X3,X1,X2)
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[],[f92]) ).
tcf(c_234,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( between(X0,X3,X1)
| between(X0,X1,X3)
| ~ between(X0,X3,X2)
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[],[f93]) ).
tcf(c_235,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( between(X3,X1,X2)
| between(X1,X3,X2)
| ~ between(X0,X3,X2)
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_236,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( between(X3,X1,X4)
| ~ between(X3,X2,X4)
| ~ between(X3,X0,X4)
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[],[f95]) ).
tcf(c_238,plain,
! [X0: $i,X1: $i,X2: $i] :
( colinear(X2,X1,X0)
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[],[f97]) ).
tcf(c_239,plain,
! [X0: $i,X1: $i,X2: $i] :
( colinear(X0,X2,X1)
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[],[f98]) ).
tcf(c_240,plain,
! [X0: $i,X1: $i,X2: $i] :
( colinear(X1,X0,X2)
| ~ between(X0,X1,X2) ),
inference(cnf_transformation,[],[f99]) ).
tcf(c_242,plain,
! [X0: $i,X1: $i,X2: $i] :
( colinear(X1,X2,X0)
| ~ colinear(X0,X1,X2) ),
inference(cnf_transformation,[],[f101]) ).
tcf(c_243,plain,
! [X0: $i,X1: $i,X2: $i] :
( colinear(X0,X2,X1)
| ~ colinear(X0,X1,X2) ),
inference(cnf_transformation,[],[f102]) ).
tcf(c_244,plain,
! [X0: $i,X1: $i,X2: $i] :
( colinear(X2,X0,X1)
| ~ colinear(X0,X1,X2) ),
inference(cnf_transformation,[],[f103]) ).
tcf(c_245,plain,
! [X0: $i,X1: $i,X2: $i] :
( colinear(X1,X0,X2)
| ~ colinear(X0,X1,X2) ),
inference(cnf_transformation,[],[f104]) ).
tcf(c_247,plain,
! [X0: $i,X1: $i] : colinear(X0,X0,X1),
inference(cnf_transformation,[],[f106]) ).
tcf(c_250,plain,
! [X0: $i,X1: $i] : colinear(X0,X1,X0),
inference(cnf_transformation,[],[f130]) ).
tcf(c_252,plain,
a != b,
inference(cnf_transformation,[],[f111]) ).
tcf(c_253,plain,
colinear(a,b,c),
inference(cnf_transformation,[],[f112]) ).
tcf(c_254,plain,
colinear(a,b,d),
inference(cnf_transformation,[],[f113]) ).
tcf(c_255,negated_conjecture,
( ~ colinear(b,c,d)
| ~ colinear(a,c,d) ),
inference(cnf_transformation,[],[f114]) ).
tcf(c_291,plain,
colinear(a,c,b),
inference(superposition,[status(thm)],[c_253,c_243]) ).
tcf(c_593,plain,
colinear(b,a,c),
inference(superposition,[status(thm)],[c_253,c_245]) ).
tcf(c_594,plain,
colinear(b,a,d),
inference(superposition,[status(thm)],[c_254,c_245]) ).
tcf(c_740,plain,
( between(c,a,b)
| between(b,c,a)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_253,c_175]) ).
tcf(c_741,plain,
( between(d,a,b)
| between(b,d,a)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_254,c_175]) ).
tcf(c_840,plain,
( between(d,b,a)
| between(b,a,d)
| between(a,d,b) ),
inference(superposition,[status(thm)],[c_594,c_175]) ).
tcf(c_846,plain,
( between(c,b,a)
| between(b,a,c)
| between(a,c,b) ),
inference(superposition,[status(thm)],[c_593,c_175]) ).
tcf(c_914,plain,
! [X0: $i] :
( between(b,d,a)
| between(a,b,d)
| between(d,X0,a)
| between(X0,d,a)
| ( a = b )
| ~ between(X0,a,b) ),
inference(superposition,[status(thm)],[c_741,c_233]) ).
tcf(c_920,plain,
( between(b,d,a)
| between(a,b,d)
| ( a = d )
| ~ between(a,d,b) ),
inference(superposition,[status(thm)],[c_741,c_204]) ).
tcf(c_928,plain,
( between(b,d,a)
| between(b,a,d)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_741,c_202]) ).
tcf(c_951,plain,
! [X0: $i] :
( between(b,c,a)
| between(a,b,c)
| between(c,X0,a)
| between(X0,c,a)
| ( a = b )
| ~ between(X0,a,b) ),
inference(superposition,[status(thm)],[c_740,c_233]) ).
tcf(c_954,plain,
! [X0: $i] :
( between(b,c,a)
| between(a,b,c)
| between(X0,c,b)
| ( a = c )
| ~ between(X0,c,a) ),
inference(superposition,[status(thm)],[c_740,c_210]) ).
tcf(c_957,plain,
( between(b,c,a)
| between(a,b,c)
| ( a = c )
| ~ between(a,c,b) ),
inference(superposition,[status(thm)],[c_740,c_204]) ).
tcf(c_965,plain,
( between(b,c,a)
| between(b,a,c)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_740,c_202]) ).
tcf(c_985,plain,
colinear(b,a,c),
inference(superposition,[status(thm)],[c_253,c_245]) ).
tcf(c_986,plain,
colinear(b,a,d),
inference(superposition,[status(thm)],[c_254,c_245]) ).
tcf(c_1011,plain,
! [X0: $i] :
( between(b,a,d)
| between(a,d,b)
| between(d,X0,b)
| between(X0,d,b)
| ( a = b )
| ~ between(X0,b,a) ),
inference(superposition,[status(thm)],[c_840,c_233]) ).
tcf(c_1015,plain,
! [X0: $i] :
( between(b,a,d)
| between(a,d,b)
| between(d,b,X0)
| between(d,X0,b)
| ~ between(d,X0,a) ),
inference(superposition,[status(thm)],[c_840,c_234]) ).
tcf(c_1025,plain,
( between(b,a,d)
| between(a,d,b)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_840,c_202]) ).
tcf(c_1076,plain,
! [X0: $i,X1: $i] :
( between(b,a,c)
| between(a,c,b)
| between(X0,b,X1)
| ~ between(X0,c,X1)
| ~ between(X0,a,X1) ),
inference(superposition,[status(thm)],[c_846,c_236]) ).
tcf(c_1078,plain,
! [X0: $i] :
( between(b,a,c)
| between(a,c,b)
| between(X0,c,a)
| ( b = c )
| ~ between(X0,c,b) ),
inference(superposition,[status(thm)],[c_846,c_210]) ).
tcf(c_1079,plain,
! [X0: $i] :
( between(b,a,c)
| between(a,c,b)
| between(c,b,X0)
| between(c,X0,b)
| ~ between(c,X0,a) ),
inference(superposition,[status(thm)],[c_846,c_234]) ).
tcf(c_1089,plain,
( between(b,a,c)
| between(a,c,b)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_846,c_202]) ).
tcf(c_1213,plain,
( between(c,a,b)
| between(b,c,a)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_253,c_175]) ).
tcf(c_1214,plain,
( between(d,a,b)
| between(b,d,a)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_254,c_175]) ).
tcf(c_1262,plain,
! [X0: $i] :
( between(b,a,d)
| between(a,b,d)
| between(d,a,X0)
| between(d,X0,a)
| ( b = d )
| ~ between(b,d,X0) ),
inference(superposition,[status(thm)],[c_928,c_232]) ).
tcf(c_1263,plain,
! [X0: $i] :
( between(b,a,d)
| between(a,b,d)
| between(b,X0,d)
| between(X0,b,d)
| ( a = d )
| ~ between(X0,d,a) ),
inference(superposition,[status(thm)],[c_928,c_233]) ).
tcf(c_1267,plain,
! [X0: $i] :
( between(b,a,d)
| between(a,b,d)
| between(b,d,X0)
| between(b,X0,d)
| ~ between(b,X0,a) ),
inference(superposition,[status(thm)],[c_928,c_234]) ).
tcf(c_1268,plain,
! [X0: $i] :
( between(b,a,d)
| between(a,b,d)
| between(d,X0,a)
| between(X0,d,a)
| ~ between(b,X0,a) ),
inference(superposition,[status(thm)],[c_928,c_235]) ).
tcf(c_1271,plain,
! [X0: $i] :
( between(b,a,d)
| between(a,b,d)
| between(d,a,X0)
| ~ between(b,a,X0) ),
inference(superposition,[status(thm)],[c_928,c_208]) ).
tcf(c_1272,plain,
! [X0: $i] :
( between(b,a,d)
| between(a,b,d)
| between(X0,d,a)
| ~ between(X0,b,a) ),
inference(superposition,[status(thm)],[c_928,c_211]) ).
tcf(c_1273,plain,
! [X0: $i] :
( between(b,a,d)
| between(a,b,d)
| between(b,d,X0)
| ~ between(b,a,X0) ),
inference(superposition,[status(thm)],[c_928,c_212]) ).
tcf(c_1350,plain,
( between(d,b,a)
| between(b,a,d)
| between(a,d,b) ),
inference(superposition,[status(thm)],[c_986,c_175]) ).
tcf(c_1356,plain,
( between(c,b,a)
| between(b,a,c)
| between(a,c,b) ),
inference(superposition,[status(thm)],[c_985,c_175]) ).
tcf(c_1424,plain,
! [X0: $i] :
( between(b,d,a)
| between(a,b,d)
| between(d,X0,a)
| between(X0,d,a)
| ( a = b )
| ~ between(X0,a,b) ),
inference(superposition,[status(thm)],[c_1214,c_233]) ).
tcf(c_1438,plain,
( between(b,d,a)
| between(b,a,d)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_1214,c_202]) ).
tcf(c_1488,plain,
( between(b,d,a)
| ~ between(a,d,b) ),
inference(forward_subsumption_resolution,[status(thm)],[c_920,c_202,c_202]) ).
tcf(c_1559,plain,
! [X0: $i] :
( between(b,d,a)
| between(a,b,d)
| between(d,X0,a)
| between(X0,d,a)
| ~ between(X0,a,b) ),
inference(global_subsumption_just,[status(thm)],[c_914,c_252,c_914]) ).
tcf(c_1625,plain,
( between(b,c,a)
| between(b,a,c)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_1213,c_202]) ).
tcf(c_1637,plain,
! [X0: $i] :
( between(b,a,c)
| between(a,b,c)
| between(b,X0,c)
| between(X0,b,c)
| ( a = c )
| ~ between(X0,c,a) ),
inference(superposition,[status(thm)],[c_965,c_233]) ).
tcf(c_1641,plain,
! [X0: $i] :
( between(b,a,c)
| between(a,b,c)
| between(b,c,X0)
| between(b,X0,c)
| ~ between(b,X0,a) ),
inference(superposition,[status(thm)],[c_965,c_234]) ).
tcf(c_1645,plain,
! [X0: $i] :
( between(b,a,c)
| between(a,b,c)
| between(c,a,X0)
| ~ between(b,a,X0) ),
inference(superposition,[status(thm)],[c_965,c_208]) ).
tcf(c_1646,plain,
! [X0: $i] :
( between(b,a,c)
| between(a,b,c)
| between(X0,c,a)
| ~ between(X0,b,a) ),
inference(superposition,[status(thm)],[c_965,c_211]) ).
tcf(c_1647,plain,
! [X0: $i] :
( between(b,a,c)
| between(a,b,c)
| between(b,c,X0)
| ~ between(b,a,X0) ),
inference(superposition,[status(thm)],[c_965,c_212]) ).
tcf(c_1712,plain,
( between(b,c,a)
| ~ between(a,c,b) ),
inference(forward_subsumption_resolution,[status(thm)],[c_957,c_202,c_202]) ).
tcf(c_1784,plain,
! [X0: $i] :
( between(b,c,a)
| between(a,b,c)
| between(c,X0,a)
| between(X0,c,a)
| ~ between(X0,a,b) ),
inference(global_subsumption_just,[status(thm)],[c_951,c_252,c_951]) ).
tcf(c_1843,plain,
! [X0: $i] :
( between(b,a,d)
| between(a,d,b)
| between(d,X0,b)
| between(X0,d,b)
| ( a = b )
| ~ between(X0,b,a) ),
inference(superposition,[status(thm)],[c_1350,c_233]) ).
tcf(c_1846,plain,
! [X0: $i] :
( between(b,a,d)
| between(a,d,b)
| between(X0,d,a)
| ( b = d )
| ~ between(X0,d,b) ),
inference(superposition,[status(thm)],[c_1350,c_210]) ).
tcf(c_1857,plain,
( between(b,a,d)
| between(a,d,b)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_1350,c_202]) ).
tcf(c_1867,plain,
! [X0: $i] :
( between(a,d,b)
| between(a,b,d)
| between(b,d,X0)
| between(b,X0,d)
| ( a = b )
| ~ between(b,a,X0) ),
inference(superposition,[status(thm)],[c_1025,c_231]) ).
tcf(c_1868,plain,
! [X0: $i] :
( between(a,d,b)
| between(a,b,d)
| between(a,d,X0)
| between(a,X0,d)
| ( a = b )
| ~ between(b,a,X0) ),
inference(superposition,[status(thm)],[c_1025,c_232]) ).
tcf(c_1871,plain,
! [X0: $i] :
( between(a,d,b)
| between(a,b,d)
| between(X0,a,d)
| ( a = b )
| ~ between(X0,b,a) ),
inference(superposition,[status(thm)],[c_1025,c_209]) ).
tcf(c_1872,plain,
! [X0: $i] :
( between(a,d,b)
| between(a,b,d)
| between(X0,b,d)
| ( a = b )
| ~ between(X0,b,a) ),
inference(superposition,[status(thm)],[c_1025,c_210]) ).
tcf(c_1877,plain,
! [X0: $i] :
( between(a,d,b)
| between(a,b,d)
| between(a,d,X0)
| ~ between(b,d,X0) ),
inference(superposition,[status(thm)],[c_1025,c_208]) ).
tcf(c_1883,plain,
( between(d,a,b)
| between(a,d,b)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_1025,c_202]) ).
tcf(c_2015,plain,
! [X0: $i] :
( between(b,a,d)
| between(a,d,b)
| between(d,X0,b)
| between(X0,d,b)
| ~ between(X0,b,a) ),
inference(global_subsumption_just,[status(thm)],[c_1011,c_252,c_1011]) ).
tcf(c_2030,plain,
( between(d,c,b)
| between(c,d,b)
| between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,c,b) ),
inference(superposition,[status(thm)],[c_846,c_2015]) ).
tcf(c_2040,plain,
! [X0: $i,X1: $i] :
( between(b,a,c)
| between(a,c,b)
| between(X0,b,X1)
| ~ between(X0,c,X1)
| ~ between(X0,a,X1) ),
inference(superposition,[status(thm)],[c_1356,c_236]) ).
tcf(c_2042,plain,
! [X0: $i] :
( between(b,a,c)
| between(a,c,b)
| between(X0,c,a)
| ( b = c )
| ~ between(X0,c,b) ),
inference(superposition,[status(thm)],[c_1356,c_210]) ).
tcf(c_2053,plain,
( between(b,a,c)
| between(a,c,b)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_1356,c_202]) ).
tcf(c_2091,plain,
! [X0: $i] :
( between(a,c,b)
| between(a,b,c)
| between(b,c,X0)
| between(b,X0,c)
| ( a = b )
| ~ between(b,a,X0) ),
inference(superposition,[status(thm)],[c_1089,c_231]) ).
tcf(c_2092,plain,
! [X0: $i] :
( between(a,c,b)
| between(a,b,c)
| between(a,c,X0)
| between(a,X0,c)
| ( a = b )
| ~ between(b,a,X0) ),
inference(superposition,[status(thm)],[c_1089,c_232]) ).
tcf(c_2094,plain,
! [X0: $i,X1: $i] :
( between(a,c,b)
| between(a,b,c)
| between(X0,a,X1)
| ~ between(X0,c,X1)
| ~ between(X0,b,X1) ),
inference(superposition,[status(thm)],[c_1089,c_236]) ).
tcf(c_2095,plain,
! [X0: $i] :
( between(a,c,b)
| between(a,b,c)
| between(X0,a,c)
| ( a = b )
| ~ between(X0,b,a) ),
inference(superposition,[status(thm)],[c_1089,c_209]) ).
tcf(c_2096,plain,
! [X0: $i] :
( between(a,c,b)
| between(a,b,c)
| between(X0,b,c)
| ( a = b )
| ~ between(X0,b,a) ),
inference(superposition,[status(thm)],[c_1089,c_210]) ).
tcf(c_2098,plain,
! [X0: $i] :
( between(a,c,b)
| between(a,b,c)
| between(a,X0,c)
| between(X0,a,c)
| ~ between(b,X0,c) ),
inference(superposition,[status(thm)],[c_1089,c_235]) ).
tcf(c_2107,plain,
( between(c,a,b)
| between(a,c,b)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_1089,c_202]) ).
tcf(c_2236,plain,
! [X0: $i] :
( between(b,a,c)
| between(a,c,b)
| between(a,b,X0)
| ~ between(a,c,X0) ),
inference(superposition,[status(thm)],[c_203,c_1076]) ).
tcf(c_2251,plain,
! [X0: $i,X1: $i] :
( between(b,a,d)
| between(a,b,d)
| between(X0,d,X1)
| ~ between(X0,b,X1)
| ~ between(X0,a,X1) ),
inference(superposition,[status(thm)],[c_1438,c_236]) ).
tcf(c_2254,plain,
! [X0: $i] :
( between(b,a,d)
| between(a,b,d)
| between(b,d,X0)
| between(b,X0,d)
| ~ between(b,X0,a) ),
inference(superposition,[status(thm)],[c_1438,c_234]) ).
tcf(c_2255,plain,
! [X0: $i] :
( between(b,a,d)
| between(a,b,d)
| between(d,X0,a)
| between(X0,d,a)
| ~ between(b,X0,a) ),
inference(superposition,[status(thm)],[c_1438,c_235]) ).
tcf(c_2260,plain,
! [X0: $i] :
( between(b,a,d)
| between(a,b,d)
| between(b,d,X0)
| ~ between(b,a,X0) ),
inference(superposition,[status(thm)],[c_1438,c_212]) ).
tcf(c_2322,plain,
( between(b,d,c)
| between(b,a,d)
| between(a,c,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_1089,c_1273]) ).
tcf(c_2333,plain,
( between(c,d,a)
| between(b,a,d)
| between(b,a,c)
| between(a,c,b)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_846,c_1272]) ).
tcf(c_2344,plain,
( between(d,a,c)
| between(b,a,d)
| between(a,c,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_1089,c_1271]) ).
tcf(c_2366,plain,
( between(d,c,a)
| between(c,d,a)
| between(b,a,d)
| between(b,a,c)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_965,c_1268]) ).
tcf(c_2373,plain,
! [X0: $i] :
( between(a,b,d)
| between(b,d,X0)
| between(b,X0,d)
| ~ between(b,X0,a) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1267,c_212]) ).
tcf(c_2388,plain,
( between(b,d,c)
| between(b,c,d)
| between(b,a,c)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_965,c_2373]) ).
tcf(c_2658,plain,
( between(b,c,d)
| between(b,a,c)
| between(a,d,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_1025,c_1647]) ).
tcf(c_2669,plain,
( between(d,c,a)
| between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_840,c_1646]) ).
tcf(c_2680,plain,
( between(c,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_1025,c_1645]) ).
tcf(c_2734,plain,
! [X0: $i] :
( between(a,b,c)
| between(b,c,X0)
| between(b,X0,c)
| ~ between(b,X0,a) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1641,c_212]) ).
tcf(c_2750,plain,
( between(b,d,c)
| between(b,c,d)
| between(b,a,d)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_928,c_2734]) ).
tcf(c_2816,plain,
! [X0: $i] :
( between(b,d,a)
| between(a,b,d)
| between(d,X0,a)
| between(X0,d,a)
| ~ between(X0,a,b) ),
inference(global_subsumption_just,[status(thm)],[c_1424,c_252,c_914]) ).
tcf(c_2829,plain,
( between(d,c,a)
| between(c,d,a)
| between(b,d,a)
| between(b,c,a)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_1213,c_2816]) ).
tcf(c_2925,plain,
! [X0: $i] :
( between(a,d,b)
| between(a,b,d)
| between(d,X0,a)
| between(X0,d,a)
| ( a = b )
| ~ between(X0,a,b) ),
inference(superposition,[status(thm)],[c_1883,c_233]) ).
tcf(c_2928,plain,
! [X0: $i] :
( between(a,d,b)
| between(a,b,d)
| between(X0,d,b)
| ( a = d )
| ~ between(X0,d,a) ),
inference(superposition,[status(thm)],[c_1883,c_210]) ).
tcf(c_2950,plain,
( between(d,c,a)
| between(c,d,a)
| between(b,c,a)
| between(a,d,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_1883,c_1784]) ).
tcf(c_3003,plain,
! [X0: $i] :
( between(b,a,c)
| between(a,b,c)
| between(b,c,X0)
| between(b,X0,c)
| ~ between(b,X0,a) ),
inference(superposition,[status(thm)],[c_1625,c_234]) ).
tcf(c_3007,plain,
! [X0: $i] :
( between(b,a,c)
| between(a,b,c)
| between(c,a,X0)
| ~ between(b,a,X0) ),
inference(superposition,[status(thm)],[c_1625,c_208]) ).
tcf(c_3009,plain,
! [X0: $i] :
( between(b,a,c)
| between(a,b,c)
| between(b,c,X0)
| ~ between(b,a,X0) ),
inference(superposition,[status(thm)],[c_1625,c_212]) ).
tcf(c_3089,plain,
! [X0: $i] :
( between(a,d,b)
| between(a,b,d)
| between(X0,b,d)
| ~ between(X0,b,a) ),
inference(global_subsumption_just,[status(thm)],[c_1872,c_252,c_1872]) ).
tcf(c_3102,plain,
( between(c,b,d)
| between(b,a,c)
| between(a,d,b)
| between(a,c,b)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_846,c_3089]) ).
tcf(c_3103,plain,
! [X0: $i] :
( between(a,d,b)
| between(a,b,d)
| between(X0,a,d)
| ~ between(X0,b,a) ),
inference(global_subsumption_just,[status(thm)],[c_1871,c_252,c_1871]) ).
tcf(c_3116,plain,
( between(c,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,c,b)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_846,c_3103]) ).
tcf(c_3144,plain,
! [X0: $i] :
( between(a,d,b)
| between(a,b,d)
| between(a,d,X0)
| between(a,X0,d)
| ~ between(b,a,X0) ),
inference(global_subsumption_just,[status(thm)],[c_1868,c_252,c_1868]) ).
tcf(c_3159,plain,
( between(a,d,c)
| between(a,d,b)
| between(a,c,d)
| between(a,c,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_1089,c_3144]) ).
tcf(c_3160,plain,
! [X0: $i] :
( between(a,d,b)
| between(a,b,d)
| between(b,d,X0)
| between(b,X0,d)
| ~ between(b,a,X0) ),
inference(global_subsumption_just,[status(thm)],[c_1867,c_252,c_1867]) ).
tcf(c_3175,plain,
( between(b,d,c)
| between(b,c,d)
| between(a,d,b)
| between(a,c,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_1089,c_3160]) ).
tcf(c_3234,plain,
! [X0: $i] :
( between(c,d,b)
| between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,c,b)
| between(d,c,X0)
| ~ between(d,b,X0) ),
inference(superposition,[status(thm)],[c_2030,c_212]) ).
tcf(c_3241,plain,
( colinear(c,d,b)
| between(c,d,b)
| between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,c,b) ),
inference(superposition,[status(thm)],[c_2030,c_240]) ).
tcf(c_3366,plain,
! [X0: $i] :
( between(a,c,b)
| between(a,b,c)
| between(X0,c,b)
| ( a = c )
| ~ between(X0,c,a) ),
inference(superposition,[status(thm)],[c_2107,c_210]) ).
tcf(c_3372,plain,
! [X0: $i] :
( between(a,c,b)
| between(a,b,c)
| between(X0,a,b)
| ~ between(X0,c,b) ),
inference(superposition,[status(thm)],[c_2107,c_211]) ).
tcf(c_3515,plain,
! [X0: $i] :
( between(a,d,b)
| between(a,b,d)
| between(a,d,X0)
| ~ between(b,d,X0) ),
inference(superposition,[status(thm)],[c_1857,c_208]) ).
tcf(c_3521,plain,
( between(d,a,b)
| between(a,d,b)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_1857,c_202]) ).
tcf(c_3539,plain,
! [X0: $i] :
( between(a,c,b)
| between(a,X0,c)
| between(X0,a,c)
| ~ between(b,X0,c) ),
inference(forward_subsumption_resolution,[status(thm)],[c_2098,c_211]) ).
tcf(c_3568,plain,
! [X0: $i] :
( between(a,c,b)
| between(a,b,c)
| between(X0,b,c)
| ~ between(X0,b,a) ),
inference(global_subsumption_just,[status(thm)],[c_2096,c_252,c_2096]) ).
tcf(c_3580,plain,
( between(d,b,c)
| between(b,a,d)
| between(a,d,b)
| between(a,c,b)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_840,c_3568]) ).
tcf(c_3582,plain,
! [X0: $i] :
( between(a,c,b)
| between(a,b,c)
| between(X0,a,c)
| ~ between(X0,b,a) ),
inference(global_subsumption_just,[status(thm)],[c_2095,c_252,c_2095]) ).
tcf(c_3594,plain,
( between(d,a,c)
| between(b,a,d)
| between(a,d,b)
| between(a,c,b)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_840,c_3582]) ).
tcf(c_3608,plain,
( between(d,a,a)
| between(b,a,d)
| between(a,d,b)
| between(a,c,b)
| between(a,b,c)
| ~ between(d,c,a) ),
inference(superposition,[status(thm)],[c_840,c_2094]) ).
tcf(c_3640,plain,
! [X0: $i] :
( between(a,c,b)
| between(a,b,c)
| between(b,c,X0)
| between(b,X0,c)
| ~ between(b,a,X0) ),
inference(global_subsumption_just,[status(thm)],[c_2091,c_252,c_2091]) ).
tcf(c_3731,plain,
( colinear(b,c,d)
| between(b,a,d)
| between(a,c,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_2322,c_239]) ).
tcf(c_3838,plain,
! [X0: $i] :
( between(b,a,d)
| between(b,a,c)
| between(a,c,b)
| between(a,b,d)
| between(d,X0,a)
| between(X0,d,a)
| ~ between(c,X0,a) ),
inference(superposition,[status(thm)],[c_2333,c_235]) ).
tcf(c_3845,plain,
( colinear(a,c,d)
| between(b,a,d)
| between(b,a,c)
| between(a,c,b)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_2333,c_173]) ).
tcf(c_3847,plain,
( between(b,a,d)
| between(b,a,c)
| between(a,d,c)
| between(a,c,b)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_2333,c_202]) ).
tcf(c_3851,plain,
( between(c,b,d)
| between(b,c,d)
| between(b,a,d)
| between(b,a,c)
| between(a,c,b)
| between(a,b,d)
| ( a = d ) ),
inference(superposition,[status(thm)],[c_2333,c_1263]) ).
tcf(c_3858,plain,
( between(c,d,b)
| between(c,b,d)
| between(b,a,d)
| between(b,a,c)
| between(a,c,b)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_2333,c_1079]) ).
tcf(c_3919,plain,
! [X0: $i] :
( between(b,a,d)
| between(a,d,b)
| between(d,X0,b)
| between(X0,d,b)
| ~ between(X0,b,a) ),
inference(global_subsumption_just,[status(thm)],[c_1843,c_252,c_1011]) ).
tcf(c_3933,plain,
( between(d,c,b)
| between(c,d,b)
| between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,c,b) ),
inference(superposition,[status(thm)],[c_1356,c_3919]) ).
tcf(c_3968,plain,
! [X0: $i] :
( between(a,c,b)
| between(a,b,c)
| between(b,c,X0)
| between(b,X0,c)
| ( a = b )
| ~ between(b,a,X0) ),
inference(superposition,[status(thm)],[c_2053,c_231]) ).
tcf(c_3969,plain,
! [X0: $i] :
( between(a,c,b)
| between(a,b,c)
| between(a,c,X0)
| between(a,X0,c)
| ( a = b )
| ~ between(b,a,X0) ),
inference(superposition,[status(thm)],[c_2053,c_232]) ).
tcf(c_4016,plain,
( colinear(a,c,d)
| between(b,a,d)
| between(a,c,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_2344,c_174]) ).
tcf(c_4084,plain,
( colinear(c,d,a)
| between(c,d,a)
| between(b,a,d)
| between(b,a,c)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_2366,c_240]) ).
tcf(c_4246,plain,
( colinear(d,b,c)
| between(b,c,d)
| between(b,a,c)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_2388,c_240]) ).
tcf(c_4250,plain,
( between(b,c,d)
| between(b,a,c)
| between(a,d,c)
| between(a,d,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_2388,c_1877]) ).
tcf(c_4320,plain,
( between(b,d,c)
| between(b,a,d)
| between(a,c,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_2053,c_2260]) ).
tcf(c_4364,plain,
( between(d,c,a)
| between(c,d,a)
| between(b,a,d)
| between(b,a,c)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_1625,c_2255]) ).
tcf(c_4371,plain,
! [X0: $i] :
( between(a,b,d)
| between(b,d,X0)
| between(b,X0,d)
| ~ between(b,X0,a) ),
inference(forward_subsumption_resolution,[status(thm)],[c_2254,c_212]) ).
tcf(c_4386,plain,
( between(b,d,c)
| between(b,c,d)
| between(b,a,c)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_1625,c_4371]) ).
tcf(c_4531,plain,
! [X0: $i] :
( between(b,a,d)
| between(a,b,d)
| between(X0,d,b)
| ~ between(X0,a,b) ),
inference(superposition,[status(thm)],[c_200,c_2251]) ).
tcf(c_4655,plain,
( colinear(c,d,a)
| between(c,d,a)
| between(b,d,a)
| between(b,c,a)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_2829,c_240]) ).
tcf(c_4732,plain,
( between(b,c,d)
| between(b,a,c)
| between(a,d,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_1857,c_3009]) ).
tcf(c_4840,plain,
! [X0: $i] :
( between(a,b,c)
| between(b,c,X0)
| between(b,X0,c)
| ~ between(b,X0,a) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3003,c_212]) ).
tcf(c_4856,plain,
( between(b,d,c)
| between(b,c,d)
| between(b,a,d)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_1438,c_4840]) ).
tcf(c_5121,plain,
( between(d,b,b)
| between(b,a,c)
| between(a,d,b)
| between(a,c,b)
| between(a,b,d)
| ~ between(d,c,b) ),
inference(superposition,[status(thm)],[c_3521,c_2040]) ).
tcf(c_5275,plain,
( colinear(b,c,d)
| between(b,a,c)
| between(a,d,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_2658,c_172]) ).
tcf(c_5414,plain,
! [X0: $i] :
( between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,b,c)
| between(d,c,X0)
| between(d,X0,c)
| ~ between(d,X0,a) ),
inference(superposition,[status(thm)],[c_2669,c_234]) ).
tcf(c_5415,plain,
! [X0: $i] :
( between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,b,c)
| between(c,X0,a)
| between(X0,c,a)
| ~ between(d,X0,a) ),
inference(superposition,[status(thm)],[c_2669,c_235]) ).
tcf(c_5425,plain,
( colinear(a,c,d)
| between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_2669,c_238]) ).
tcf(c_5430,plain,
( between(d,c,b)
| between(d,b,c)
| between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_2669,c_1015]) ).
tcf(c_5432,plain,
( between(d,b,c)
| between(b,d,c)
| between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,b,c)
| ( a = c ) ),
inference(superposition,[status(thm)],[c_2669,c_1637]) ).
tcf(c_5564,plain,
! [X0: $i] :
( between(c,d,b)
| between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,c,b)
| between(d,c,X0)
| ~ between(d,b,X0) ),
inference(superposition,[status(thm)],[c_3933,c_212]) ).
tcf(c_5568,plain,
( between(c,d,b)
| between(b,c,d)
| between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,c,b) ),
inference(superposition,[status(thm)],[c_3933,c_202]) ).
tcf(c_5575,plain,
( between(d,c,a)
| between(c,d,b)
| between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,c,b)
| ( b = c ) ),
inference(superposition,[status(thm)],[c_3933,c_2042]) ).
tcf(c_5609,plain,
( colinear(a,c,d)
| between(b,a,c)
| between(a,d,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_2680,c_240]) ).
tcf(c_5659,plain,
! [X0: $i] :
( between(b,c,d)
| between(b,a,d)
| between(a,b,d)
| between(a,b,c)
| between(d,c,X0)
| ~ between(b,c,X0) ),
inference(superposition,[status(thm)],[c_2750,c_208]) ).
tcf(c_5667,plain,
( colinear(b,c,d)
| between(b,c,d)
| between(b,a,d)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_2750,c_239]) ).
tcf(c_5676,plain,
( between(d,c,a)
| between(d,a,c)
| between(b,c,d)
| between(b,a,d)
| between(a,b,d)
| between(a,b,c)
| ( b = d ) ),
inference(superposition,[status(thm)],[c_2750,c_1262]) ).
tcf(c_5868,plain,
( between(c,d,b)
| between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,c,b)
| between(a,b,d)
| ( a = d ) ),
inference(superposition,[status(thm)],[c_2333,c_2928]) ).
tcf(c_5923,plain,
( between(d,c,b)
| between(c,d,a)
| between(b,c,a)
| between(a,d,b)
| between(a,b,d)
| between(a,b,c)
| ( a = c ) ),
inference(superposition,[status(thm)],[c_2950,c_954]) ).
tcf(c_6047,plain,
! [X0: $i] :
( between(a,d,b)
| between(a,b,d)
| between(d,X0,a)
| between(X0,d,a)
| ~ between(X0,a,b) ),
inference(global_subsumption_just,[status(thm)],[c_2925,c_252,c_2925]) ).
tcf(c_6125,plain,
! [X0: $i] :
( between(a,c,b)
| between(a,b,c)
| between(a,c,X0)
| between(a,X0,c)
| ~ between(b,a,X0) ),
inference(global_subsumption_just,[status(thm)],[c_3969,c_252,c_2092]) ).
tcf(c_6190,plain,
( colinear(b,c,d)
| between(b,a,c)
| between(a,d,b)
| between(a,c,b)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_3102,c_240]) ).
tcf(c_6214,plain,
! [X0: $i] :
( between(a,c,b)
| between(a,b,c)
| between(b,c,X0)
| between(b,X0,c)
| ~ between(b,a,X0) ),
inference(global_subsumption_just,[status(thm)],[c_3968,c_3640]) ).
tcf(c_6276,plain,
( between(a,b,c)
| between(a,b,d)
| between(a,c,b)
| between(b,a,d) ),
inference(global_subsumption_just,[status(thm)],[c_4320,c_255,c_3731,c_4016]) ).
tcf(c_6277,plain,
( between(b,a,d)
| between(a,c,b)
| between(a,b,d)
| between(a,b,c) ),
inference(renaming,[status(thm)],[c_6276]) ).
tcf(c_6307,plain,
( between(b,d,c)
| between(b,c,d)
| between(a,c,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_6277,c_6214]) ).
tcf(c_6308,plain,
( between(a,d,c)
| between(a,c,d)
| between(a,c,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_6277,c_6125]) ).
tcf(c_6359,plain,
( colinear(a,c,d)
| between(b,a,c)
| between(a,d,b)
| between(a,c,b)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_3116,c_240]) ).
tcf(c_6384,plain,
( between(a,d,c)
| between(a,b,c)
| between(a,b,d)
| between(a,c,b)
| between(a,c,d) ),
inference(global_subsumption_just,[status(thm)],[c_3159,c_6308]) ).
tcf(c_6385,plain,
( between(a,d,c)
| between(a,c,d)
| between(a,c,b)
| between(a,b,d)
| between(a,b,c) ),
inference(renaming,[status(thm)],[c_6384]) ).
tcf(c_6415,plain,
( colinear(d,a,c)
| between(a,c,d)
| between(a,c,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_6385,c_240]) ).
tcf(c_6475,plain,
( between(b,d,c)
| between(b,c,d)
| between(a,b,c)
| between(a,b,d)
| between(a,c,b) ),
inference(global_subsumption_just,[status(thm)],[c_3175,c_6307]) ).
tcf(c_6476,plain,
( between(b,d,c)
| between(b,c,d)
| between(a,c,b)
| between(a,b,d)
| between(a,b,c) ),
inference(renaming,[status(thm)],[c_6475]) ).
tcf(c_6505,plain,
( colinear(b,c,d)
| between(b,c,d)
| between(a,c,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_6476,c_239]) ).
tcf(c_6506,plain,
( colinear(d,b,c)
| between(b,c,d)
| between(a,c,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_6476,c_240]) ).
tcf(c_6516,plain,
( between(d,a,c)
| between(b,c,d)
| between(a,d,c)
| between(a,c,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_6476,c_3539]) ).
tcf(c_6536,plain,
( colinear(c,d,b)
| between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,c,b) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3241,c_172]) ).
tcf(c_6556,plain,
( colinear(b,c,d)
| between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,c,b) ),
inference(superposition,[status(thm)],[c_6536,c_244]) ).
tcf(c_6654,plain,
( colinear(c,d,a)
| between(c,d,a)
| between(b,a,d)
| between(b,a,c)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_4364,c_240]) ).
tcf(c_6761,plain,
( between(b,c,d)
| between(b,a,c)
| between(a,d,c)
| between(a,d,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_4386,c_3515]) ).
tcf(c_6784,plain,
( between(d,c,a)
| between(c,d,b)
| between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,c,b) ),
inference(superposition,[status(thm)],[c_840,c_3234]) ).
tcf(c_7161,plain,
( between(d,c,b)
| between(c,d,a)
| between(b,c,a)
| between(a,d,b)
| between(a,c,b)
| between(a,b,d)
| between(a,b,c)
| ( a = c ) ),
inference(superposition,[status(thm)],[c_2950,c_3366]) ).
tcf(c_7252,plain,
( between(c,d,b)
| between(b,c,a)
| between(b,a,d)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_1213,c_4531]) ).
tcf(c_7271,plain,
( colinear(c,d,a)
| between(b,d,a)
| between(b,c,a)
| between(a,b,d)
| between(a,b,c) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4655,c_172]) ).
tcf(c_7292,plain,
( colinear(d,c,a)
| between(b,d,a)
| between(b,c,a)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_7271,c_245]) ).
tcf(c_7433,plain,
! [X0: $i] :
( between(b,a,d)
| between(a,d,b)
| between(a,c,b)
| between(a,b,c)
| between(d,b,X0)
| ~ between(d,c,X0) ),
inference(superposition,[status(thm)],[c_3580,c_212]) ).
tcf(c_7436,plain,
( colinear(b,c,d)
| between(b,a,d)
| between(a,d,b)
| between(a,c,b)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_3580,c_174]) ).
tcf(c_7492,plain,
( colinear(a,c,d)
| between(b,a,d)
| between(a,d,b)
| between(a,c,b)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_3594,c_174]) ).
tcf(c_7518,plain,
( between(a,b,c)
| between(a,c,b)
| between(a,d,b)
| between(b,a,d) ),
inference(global_subsumption_just,[status(thm)],[c_3608,c_255,c_7436,c_7492]) ).
tcf(c_7519,plain,
( between(b,a,d)
| between(a,d,b)
| between(a,c,b)
| between(a,b,c) ),
inference(renaming,[status(thm)],[c_7518]) ).
tcf(c_7536,plain,
( between(a,d,b)
| between(a,c,b)
| between(a,b,c)
| ( a = b )
| ~ between(a,b,d) ),
inference(superposition,[status(thm)],[c_7519,c_204]) ).
tcf(c_7778,plain,
! [X0: $i] :
( between(b,a,c)
| between(a,d,c)
| between(a,c,b)
| between(a,b,d)
| between(b,X0,a)
| between(X0,b,a)
| ( a = d )
| ~ between(X0,a,d) ),
inference(superposition,[status(thm)],[c_3847,c_233]) ).
tcf(c_7780,plain,
! [X0: $i] :
( between(b,a,c)
| between(a,d,c)
| between(a,c,b)
| between(a,b,d)
| between(X0,a,d)
| ( a = b )
| ~ between(X0,b,a) ),
inference(superposition,[status(thm)],[c_3847,c_209]) ).
tcf(c_7781,plain,
! [X0: $i] :
( between(b,a,c)
| between(a,d,c)
| between(a,c,b)
| between(a,b,d)
| between(X0,b,d)
| ( a = b )
| ~ between(X0,b,a) ),
inference(superposition,[status(thm)],[c_3847,c_210]) ).
tcf(c_7785,plain,
( between(b,a,c)
| between(a,d,c)
| between(a,c,b)
| between(a,b,d)
| ( a = d )
| ~ between(b,d,a) ),
inference(superposition,[status(thm)],[c_3847,c_205]) ).
tcf(c_7852,plain,
( between(b,a,d)
| between(b,a,c)
| between(a,c,b)
| between(a,b,d)
| ~ colinear(b,c,d) ),
inference(superposition,[status(thm)],[c_3845,c_255]) ).
tcf(c_7897,plain,
( colinear(b,c,d)
| between(c,b,d)
| between(b,a,d)
| between(b,a,c)
| between(a,c,b)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_3858,c_173]) ).
tcf(c_8096,plain,
( between(a,b,c)
| between(a,b,d)
| between(a,d,b)
| between(b,a,c) ),
inference(global_subsumption_just,[status(thm)],[c_4732,c_255,c_5275,c_5609]) ).
tcf(c_8097,plain,
( between(b,a,c)
| between(a,d,b)
| between(a,b,d)
| between(a,b,c) ),
inference(renaming,[status(thm)],[c_8096]) ).
tcf(c_8153,plain,
( between(c,b,d)
| between(a,b,d)
| between(a,c,b)
| between(b,a,c)
| between(b,a,d) ),
inference(global_subsumption_just,[status(thm)],[c_3851,c_7852,c_7897]) ).
tcf(c_8154,plain,
( between(c,b,d)
| between(b,a,d)
| between(b,a,c)
| between(a,c,b)
| between(a,b,d) ),
inference(renaming,[status(thm)],[c_8153]) ).
tcf(c_8184,plain,
( colinear(b,c,d)
| between(b,a,d)
| between(b,a,c)
| between(a,c,b)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_8154,c_240]) ).
tcf(c_8214,plain,
( between(b,a,d)
| between(b,a,c)
| between(a,c,b)
| between(a,b,d) ),
inference(global_subsumption_just,[status(thm)],[c_3838,c_7852,c_8184]) ).
tcf(c_8228,plain,
! [X0: $i] :
( between(b,a,c)
| between(a,c,b)
| between(a,b,d)
| between(X0,a,d)
| ( a = b )
| ~ between(X0,b,a) ),
inference(superposition,[status(thm)],[c_8214,c_209]) ).
tcf(c_8229,plain,
! [X0: $i] :
( between(b,a,c)
| between(a,c,b)
| between(a,b,d)
| between(X0,b,d)
| ( a = b )
| ~ between(X0,b,a) ),
inference(superposition,[status(thm)],[c_8214,c_210]) ).
tcf(c_8233,plain,
( between(b,a,c)
| between(a,c,b)
| between(a,b,d)
| ( a = d )
| ~ between(b,d,a) ),
inference(superposition,[status(thm)],[c_8214,c_205]) ).
tcf(c_8316,plain,
( colinear(c,d,a)
| between(b,a,d)
| between(b,a,c)
| between(a,b,d)
| between(a,b,c) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4084,c_172]) ).
tcf(c_8336,plain,
( colinear(a,c,d)
| between(b,a,d)
| between(b,a,c)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_8316,c_244]) ).
tcf(c_8337,plain,
( colinear(d,c,a)
| between(b,a,d)
| between(b,a,c)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_8316,c_245]) ).
tcf(c_8788,plain,
( between(c,d,b)
| between(b,c,d)
| between(b,a,d)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_4856,c_202]) ).
tcf(c_8856,plain,
( colinear(d,b,c)
| between(b,a,c)
| between(a,b,d)
| between(a,b,c) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4246,c_173]) ).
tcf(c_8871,plain,
( colinear(b,c,d)
| between(b,a,c)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_8856,c_242]) ).
tcf(c_8941,plain,
( between(a,d,b)
| between(a,b,d)
| between(a,b,c)
| between(b,a,c) ),
inference(global_subsumption_just,[status(thm)],[c_4250,c_255,c_5275,c_5609]) ).
tcf(c_8942,plain,
( between(b,a,c)
| between(a,d,b)
| between(a,b,d)
| between(a,b,c) ),
inference(renaming,[status(thm)],[c_8941]) ).
tcf(c_8955,plain,
! [X0: $i] :
( between(a,d,b)
| between(a,b,d)
| between(a,b,c)
| between(X0,a,c)
| ( a = b )
| ~ between(X0,b,a) ),
inference(superposition,[status(thm)],[c_8942,c_209]) ).
tcf(c_8956,plain,
! [X0: $i] :
( between(a,d,b)
| between(a,b,d)
| between(a,b,c)
| between(X0,b,c)
| ( a = b )
| ~ between(X0,b,a) ),
inference(superposition,[status(thm)],[c_8942,c_210]) ).
tcf(c_8960,plain,
( between(a,d,b)
| between(a,b,d)
| between(a,b,c)
| ( a = c )
| ~ between(b,c,a) ),
inference(superposition,[status(thm)],[c_8942,c_205]) ).
tcf(c_8974,plain,
( between(b,d,c)
| between(b,c,d)
| between(a,d,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_8942,c_3160]) ).
tcf(c_9692,plain,
( between(a,b,d)
| between(a,c,b)
| between(a,d,b)
| between(b,a,c) ),
inference(global_subsumption_just,[status(thm)],[c_5121,c_255,c_6190,c_6359]) ).
tcf(c_9693,plain,
( between(b,a,c)
| between(a,d,b)
| between(a,c,b)
| between(a,b,d) ),
inference(renaming,[status(thm)],[c_9692]) ).
tcf(c_9710,plain,
( between(a,d,b)
| between(a,c,b)
| between(a,b,d)
| ( a = b )
| ~ between(a,b,c) ),
inference(superposition,[status(thm)],[c_9693,c_204]) ).
tcf(c_9975,plain,
( between(c,d,a)
| between(b,c,d)
| between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,c,b)
| ( b = d ) ),
inference(superposition,[status(thm)],[c_5568,c_1846]) ).
tcf(c_10245,plain,
( between(d,c,a)
| between(c,d,b)
| between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,c,b) ),
inference(global_subsumption_just,[status(thm)],[c_5575,c_6784]) ).
tcf(c_10276,plain,
( colinear(a,c,d)
| between(c,d,b)
| between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,c,b) ),
inference(superposition,[status(thm)],[c_10245,c_238]) ).
tcf(c_10587,plain,
( between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,b,c)
| ~ colinear(b,c,d) ),
inference(superposition,[status(thm)],[c_5425,c_255]) ).
tcf(c_10722,plain,
( colinear(b,c,d)
| between(d,b,c)
| between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_5430,c_238]) ).
tcf(c_10751,plain,
( between(c,d,b)
| between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,c,b) ),
inference(global_subsumption_just,[status(thm)],[c_5564,c_255,c_6556,c_10276]) ).
tcf(c_11070,plain,
( between(d,b,c)
| between(a,b,c)
| between(a,d,b)
| between(b,a,c)
| between(b,a,d) ),
inference(global_subsumption_just,[status(thm)],[c_5432,c_10587,c_10722]) ).
tcf(c_11071,plain,
( between(d,b,c)
| between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,b,c) ),
inference(renaming,[status(thm)],[c_11070]) ).
tcf(c_11097,plain,
( colinear(b,c,d)
| between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_11071,c_174]) ).
tcf(c_11131,plain,
( between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,b,c) ),
inference(global_subsumption_just,[status(thm)],[c_5415,c_10587,c_11097]) ).
tcf(c_11149,plain,
( between(b,a,c)
| between(a,d,b)
| between(a,b,c)
| ( a = b )
| ~ between(a,b,d) ),
inference(superposition,[status(thm)],[c_11131,c_204]) ).
tcf(c_11186,plain,
( between(a,b,c)
| between(a,d,b)
| between(b,a,c) ),
inference(global_subsumption_just,[status(thm)],[c_5414,c_252,c_8097,c_11149]) ).
tcf(c_11187,plain,
( between(b,a,c)
| between(a,d,b)
| between(a,b,c) ),
inference(renaming,[status(thm)],[c_11186]) ).
tcf(c_11197,plain,
! [X0: $i,X1: $i] :
( between(a,d,b)
| between(a,b,c)
| between(X0,a,X1)
| ~ between(X0,c,X1)
| ~ between(X0,b,X1) ),
inference(superposition,[status(thm)],[c_11187,c_236]) ).
tcf(c_11198,plain,
! [X0: $i] :
( between(a,d,b)
| between(a,b,c)
| between(X0,a,c)
| ( a = b )
| ~ between(X0,b,a) ),
inference(superposition,[status(thm)],[c_11187,c_209]) ).
tcf(c_11199,plain,
! [X0: $i] :
( between(a,d,b)
| between(a,b,c)
| between(X0,b,c)
| ( a = b )
| ~ between(X0,b,a) ),
inference(superposition,[status(thm)],[c_11187,c_210]) ).
tcf(c_11203,plain,
( between(a,d,b)
| between(a,b,c)
| ( a = c )
| ~ between(b,c,a) ),
inference(superposition,[status(thm)],[c_11187,c_205]) ).
tcf(c_11210,plain,
( between(c,a,b)
| between(a,d,b)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_11187,c_202]) ).
tcf(c_11567,plain,
( between(d,a,c)
| between(b,c,d)
| between(b,a,d)
| between(a,c,d)
| between(a,b,d)
| between(a,b,c)
| ( b = d ) ),
inference(superposition,[status(thm)],[c_5676,c_202]) ).
tcf(c_11568,plain,
( colinear(a,c,d)
| between(d,a,c)
| between(b,c,d)
| between(b,a,d)
| between(a,b,d)
| between(a,b,c)
| ( b = d ) ),
inference(superposition,[status(thm)],[c_5676,c_238]) ).
tcf(c_11570,plain,
( colinear(c,d,a)
| between(d,a,c)
| between(b,c,d)
| between(b,a,d)
| between(a,b,d)
| between(a,b,c)
| ( b = d ) ),
inference(superposition,[status(thm)],[c_5676,c_240]) ).
tcf(c_11936,plain,
( between(c,d,b)
| between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,c,b) ),
inference(global_subsumption_just,[status(thm)],[c_5868,c_10751]) ).
tcf(c_11948,plain,
! [X0: $i] :
( between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,c,b)
| between(c,b,X0)
| between(c,X0,b)
| ( c = d )
| ~ between(c,d,X0) ),
inference(superposition,[status(thm)],[c_11936,c_231]) ).
tcf(c_11949,plain,
! [X0: $i] :
( between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,c,b)
| between(d,b,X0)
| between(d,X0,b)
| ( c = d )
| ~ between(c,d,X0) ),
inference(superposition,[status(thm)],[c_11936,c_232]) ).
tcf(c_11960,plain,
! [X0: $i] :
( between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,c,b)
| between(c,d,X0)
| ~ between(c,b,X0) ),
inference(superposition,[status(thm)],[c_11936,c_212]) ).
tcf(c_12133,plain,
( between(d,c,b)
| between(c,d,a)
| between(a,b,c)
| ( a = c )
| between(a,d,b) ),
inference(global_subsumption_just,[status(thm)],[c_5923,c_252,c_957,c_5923,c_7536,c_11203]) ).
tcf(c_12134,plain,
( between(d,c,b)
| between(c,d,a)
| between(a,d,b)
| between(a,b,c)
| ( a = c ) ),
inference(renaming,[status(thm)],[c_12133]) ).
tcf(c_12169,plain,
( between(d,a,b)
| between(c,d,a)
| between(a,d,b)
| between(a,c,b)
| between(a,b,c)
| ( a = c ) ),
inference(superposition,[status(thm)],[c_12134,c_3372]) ).
tcf(c_12812,plain,
( colinear(d,a,c)
| between(a,c,b)
| between(a,b,d)
| between(a,b,c) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6415,c_173]) ).
tcf(c_12827,plain,
( colinear(a,c,d)
| between(a,c,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_12812,c_242]) ).
tcf(c_12980,plain,
( between(b,a,d)
| between(b,a,c)
| between(a,b,d)
| between(a,b,c) ),
inference(global_subsumption_just,[status(thm)],[c_6654,c_255,c_8336,c_8871]) ).
tcf(c_13017,plain,
( between(c,a,d)
| between(b,a,c)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_12980,c_3007]) ).
tcf(c_13073,plain,
( between(a,d,b)
| between(a,b,c)
| between(b,a,c) ),
inference(global_subsumption_just,[status(thm)],[c_6761,c_252,c_8097,c_11149]) ).
tcf(c_13074,plain,
( between(b,a,c)
| between(a,d,b)
| between(a,b,c) ),
inference(renaming,[status(thm)],[c_13073]) ).
tcf(c_13087,plain,
! [X0: $i] :
( between(a,d,b)
| between(a,b,c)
| between(b,a,X0)
| between(b,X0,a)
| ~ between(b,X0,c) ),
inference(superposition,[status(thm)],[c_13074,c_234]) ).
tcf(c_13384,plain,
( colinear(d,c,b)
| between(b,c,a)
| between(b,a,d)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_7252,c_240]) ).
tcf(c_13434,plain,
( between(a,b,c)
| between(a,b,d)
| between(a,c,b)
| between(b,c,d) ),
inference(global_subsumption_just,[status(thm)],[c_6506,c_255,c_6505,c_12827]) ).
tcf(c_13435,plain,
( between(b,c,d)
| between(a,c,b)
| between(a,b,d)
| between(a,b,c) ),
inference(renaming,[status(thm)],[c_13434]) ).
tcf(c_13457,plain,
( colinear(b,c,d)
| between(a,c,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_13435,c_172]) ).
tcf(c_13488,plain,
( between(a,b,c)
| between(a,b,d)
| between(a,c,b) ),
inference(global_subsumption_just,[status(thm)],[c_6516,c_255,c_12827,c_13457]) ).
tcf(c_13489,plain,
( between(a,c,b)
| between(a,b,d)
| between(a,b,c) ),
inference(renaming,[status(thm)],[c_13488]) ).
tcf(c_13516,plain,
( between(b,c,a)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_13489,c_1712]) ).
tcf(c_13804,plain,
( between(a,b,d)
| between(a,c,b)
| between(a,d,b) ),
inference(global_subsumption_just,[status(thm)],[c_7161,c_252,c_9710,c_13489]) ).
tcf(c_13805,plain,
( between(a,d,b)
| between(a,c,b)
| between(a,b,d) ),
inference(renaming,[status(thm)],[c_13804]) ).
tcf(c_13832,plain,
( between(b,d,a)
| between(a,c,b)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_13805,c_1488]) ).
tcf(c_13899,plain,
( between(a,b,c)
| between(a,c,b)
| between(a,d,b) ),
inference(global_subsumption_just,[status(thm)],[c_7433,c_252,c_7536,c_13805]) ).
tcf(c_13900,plain,
( between(a,d,b)
| between(a,c,b)
| between(a,b,c) ),
inference(renaming,[status(thm)],[c_13899]) ).
tcf(c_14079,plain,
( between(b,a,c)
| ( a = d )
| between(a,b,d)
| between(a,c,b) ),
inference(global_subsumption_just,[status(thm)],[c_7785,c_8233,c_13832]) ).
tcf(c_14080,plain,
( between(b,a,c)
| between(a,c,b)
| between(a,b,d)
| ( a = d ) ),
inference(renaming,[status(thm)],[c_14079]) ).
tcf(c_14097,plain,
( between(a,c,b)
| between(a,b,d)
| ( a = d )
| ( a = b )
| ~ between(a,b,c) ),
inference(superposition,[status(thm)],[c_14080,c_204]) ).
tcf(c_14142,plain,
! [X0: $i] :
( between(b,a,c)
| ~ between(X0,b,a)
| between(X0,b,d)
| between(a,b,d)
| between(a,c,b) ),
inference(global_subsumption_just,[status(thm)],[c_7781,c_252,c_8229]) ).
tcf(c_14143,plain,
! [X0: $i] :
( between(b,a,c)
| between(a,c,b)
| between(a,b,d)
| between(X0,b,d)
| ~ between(X0,b,a) ),
inference(renaming,[status(thm)],[c_14142]) ).
tcf(c_14157,plain,
( between(c,b,d)
| between(b,a,c)
| between(a,c,b)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_846,c_14143]) ).
tcf(c_14158,plain,
! [X0: $i] :
( between(b,a,c)
| ~ between(X0,b,a)
| between(X0,a,d)
| between(a,b,d)
| between(a,c,b) ),
inference(global_subsumption_just,[status(thm)],[c_7780,c_252,c_8228]) ).
tcf(c_14159,plain,
! [X0: $i] :
( between(b,a,c)
| between(a,c,b)
| between(a,b,d)
| between(X0,a,d)
| ~ between(X0,b,a) ),
inference(renaming,[status(thm)],[c_14158]) ).
tcf(c_14173,plain,
( between(c,a,d)
| between(b,a,c)
| between(a,c,b)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_846,c_14159]) ).
tcf(c_14176,plain,
( between(a,c,b)
| between(a,b,d)
| ( a = d ) ),
inference(global_subsumption_just,[status(thm)],[c_7778,c_252,c_13489,c_14097]) ).
tcf(c_14207,plain,
( between(b,a,c)
| between(a,c,b)
| between(a,c,a)
| between(a,b,d)
| ( b = c )
| ( a = d ) ),
inference(superposition,[status(thm)],[c_14176,c_1078]) ).
tcf(c_14209,plain,
( between(b,a,c)
| between(a,c,b)
| between(a,b,d)
| between(a,b,b)
| ( a = d ) ),
inference(superposition,[status(thm)],[c_14176,c_2236]) ).
tcf(c_14504,plain,
( between(a,b,c)
| between(a,b,d)
| between(b,a,c)
| between(b,a,d) ),
inference(global_subsumption_just,[status(thm)],[c_8337,c_12980]) ).
tcf(c_14505,plain,
( between(b,a,d)
| between(b,a,c)
| between(a,b,d)
| between(a,b,c) ),
inference(renaming,[status(thm)],[c_14504]) ).
tcf(c_14542,plain,
( between(b,c,d)
| between(b,a,c)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_14505,c_1647]) ).
tcf(c_15193,plain,
( colinear(d,b,c)
| between(b,c,d)
| between(a,d,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_8974,c_240]) ).
tcf(c_15232,plain,
( between(a,d,b)
| ( a = c )
| between(a,b,c) ),
inference(global_subsumption_just,[status(thm)],[c_8960,c_957,c_11203,c_13900]) ).
tcf(c_15233,plain,
( between(a,d,b)
| between(a,b,c)
| ( a = c ) ),
inference(renaming,[status(thm)],[c_15232]) ).
tcf(c_15249,plain,
( between(a,b,c)
| ( b = d )
| ( a = c )
| ~ between(a,b,d) ),
inference(superposition,[status(thm)],[c_15233,c_205]) ).
tcf(c_15289,plain,
! [X0: $i] :
( between(a,d,b)
| ~ between(X0,b,a)
| between(X0,b,c)
| between(a,b,c) ),
inference(global_subsumption_just,[status(thm)],[c_8956,c_252,c_11199]) ).
tcf(c_15290,plain,
! [X0: $i] :
( between(a,d,b)
| between(a,b,c)
| between(X0,b,c)
| ~ between(X0,b,a) ),
inference(renaming,[status(thm)],[c_15289]) ).
tcf(c_15301,plain,
( between(d,b,c)
| between(b,a,d)
| between(a,d,b)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_840,c_15290]) ).
tcf(c_15303,plain,
! [X0: $i] :
( between(a,d,b)
| ~ between(X0,b,a)
| between(X0,a,c)
| between(a,b,c) ),
inference(global_subsumption_just,[status(thm)],[c_8955,c_252,c_11198]) ).
tcf(c_15304,plain,
! [X0: $i] :
( between(a,d,b)
| between(a,b,c)
| between(X0,a,c)
| ~ between(X0,b,a) ),
inference(renaming,[status(thm)],[c_15303]) ).
tcf(c_15315,plain,
( between(d,a,c)
| between(b,a,d)
| between(a,d,b)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_840,c_15304]) ).
tcf(c_15885,plain,
( between(d,c,a)
| between(c,d,a)
| between(a,d,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_11210,c_6047]) ).
tcf(c_15889,plain,
( between(d,c,a)
| between(c,d,a)
| between(b,d,a)
| between(a,d,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_11210,c_1559]) ).
tcf(c_16001,plain,
( between(d,a,a)
| between(b,a,d)
| between(a,d,b)
| between(a,b,c)
| ~ between(d,c,a) ),
inference(superposition,[status(thm)],[c_840,c_11197]) ).
tcf(c_16301,plain,
( ( b = d )
| between(a,b,c)
| between(a,b,d)
| between(b,a,d)
| between(b,c,d)
| between(d,a,c) ),
inference(global_subsumption_just,[status(thm)],[c_11570,c_255,c_5667,c_11568]) ).
tcf(c_16302,plain,
( between(d,a,c)
| between(b,c,d)
| between(b,a,d)
| between(a,b,d)
| between(a,b,c)
| ( b = d ) ),
inference(renaming,[status(thm)],[c_16301]) ).
tcf(c_16330,plain,
( colinear(a,c,d)
| between(b,c,d)
| between(b,a,d)
| between(a,b,d)
| between(a,b,c)
| ( b = d ) ),
inference(superposition,[status(thm)],[c_16302,c_174]) ).
tcf(c_16357,plain,
( between(a,b,d)
| between(a,b,c)
| ( b = d )
| between(b,a,d)
| between(b,c,d) ),
inference(global_subsumption_just,[status(thm)],[c_11567,c_255,c_5667,c_16330]) ).
tcf(c_16358,plain,
( between(b,c,d)
| between(b,a,d)
| between(a,b,d)
| between(a,b,c)
| ( b = d ) ),
inference(renaming,[status(thm)],[c_16357]) ).
tcf(c_16371,plain,
! [X0: $i] :
( between(b,a,d)
| between(a,b,d)
| between(a,b,c)
| between(b,X0,c)
| between(X0,b,c)
| ( c = d )
| ( b = d )
| ~ between(X0,c,d) ),
inference(superposition,[status(thm)],[c_16358,c_233]) ).
tcf(c_16376,plain,
! [X0: $i] :
( between(b,a,d)
| between(a,b,d)
| between(a,b,c)
| between(c,X0,d)
| between(X0,c,d)
| ( b = d )
| ~ between(b,X0,d) ),
inference(superposition,[status(thm)],[c_16358,c_235]) ).
tcf(c_16378,plain,
( between(b,a,d)
| between(a,b,d)
| between(a,b,c)
| ( c = d )
| ( b = d )
| ~ between(b,d,c) ),
inference(superposition,[status(thm)],[c_16358,c_205]) ).
tcf(c_16563,plain,
( between(b,c,a)
| between(a,b,d)
| between(a,b,c) ),
inference(global_subsumption_just,[status(thm)],[c_7292,c_13516]) ).
tcf(c_16572,plain,
! [X0: $i] :
( between(a,b,d)
| between(a,b,c)
| between(c,a,X0)
| between(c,X0,a)
| ( b = c )
| ~ between(b,c,X0) ),
inference(superposition,[status(thm)],[c_16563,c_232]) ).
tcf(c_16993,plain,
( between(b,c,d)
| between(b,a,d)
| between(a,b,d)
| between(a,b,c)
| ( c = d )
| ~ between(d,c,b) ),
inference(superposition,[status(thm)],[c_8788,c_204]) ).
tcf(c_17639,plain,
( between(c,d,a)
| between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,c,b) ),
inference(superposition,[status(thm)],[c_846,c_11960]) ).
tcf(c_18124,plain,
( between(c,d,a)
| between(a,c,b)
| between(a,d,b)
| between(b,a,c)
| between(b,a,d) ),
inference(global_subsumption_just,[status(thm)],[c_9975,c_17639]) ).
tcf(c_18125,plain,
( between(c,d,a)
| between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,c,b) ),
inference(renaming,[status(thm)],[c_18124]) ).
tcf(c_18150,plain,
( colinear(a,c,d)
| between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,c,b) ),
inference(superposition,[status(thm)],[c_18125,c_173]) ).
tcf(c_18178,plain,
( between(b,a,d)
| between(b,a,c)
| between(a,d,b)
| between(a,c,b) ),
inference(global_subsumption_just,[status(thm)],[c_11949,c_255,c_6556,c_18150]) ).
tcf(c_18196,plain,
( between(b,a,c)
| between(a,d,b)
| between(a,c,b)
| ( a = b )
| ~ between(a,b,d) ),
inference(superposition,[status(thm)],[c_18178,c_204]) ).
tcf(c_18238,plain,
( between(a,c,b)
| between(a,d,b)
| between(b,a,c) ),
inference(global_subsumption_just,[status(thm)],[c_11948,c_252,c_9710,c_13489,c_18196]) ).
tcf(c_18239,plain,
( between(b,a,c)
| between(a,d,b)
| between(a,c,b) ),
inference(renaming,[status(thm)],[c_18238]) ).
tcf(c_18254,plain,
( between(a,d,b)
| between(a,c,b)
| ( a = b )
| ~ between(a,b,c) ),
inference(superposition,[status(thm)],[c_18239,c_204]) ).
tcf(c_18361,plain,
( between(a,d,b)
| between(a,c,b) ),
inference(global_subsumption_just,[status(thm)],[c_12169,c_252,c_13900,c_18254]) ).
tcf(c_18376,plain,
( between(a,c,b)
| ( b = d )
| ~ between(a,b,d) ),
inference(superposition,[status(thm)],[c_18361,c_205]) ).
tcf(c_18728,plain,
! [X0: $i] :
( between(a,b,d)
| between(a,b,c)
| between(c,a,X0)
| ~ between(b,a,X0) ),
inference(superposition,[status(thm)],[c_13516,c_208]) ).
tcf(c_18730,plain,
! [X0: $i] :
( between(a,b,d)
| between(a,b,c)
| between(b,c,X0)
| ~ between(b,a,X0) ),
inference(superposition,[status(thm)],[c_13516,c_212]) ).
tcf(c_18747,plain,
( between(b,d,c)
| between(b,c,d)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_13516,c_2373]) ).
tcf(c_18748,plain,
( between(d,c,a)
| between(c,d,a)
| between(b,a,d)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_13516,c_1268]) ).
tcf(c_18751,plain,
( between(d,c,a)
| between(b,c,d)
| between(b,a,d)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_13516,c_5659]) ).
tcf(c_19709,plain,
( colinear(b,c,d)
| between(b,a,c)
| between(a,c,b)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_14157,c_240]) ).
tcf(c_19772,plain,
( colinear(a,c,d)
| between(b,a,c)
| between(a,c,b)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_14173,c_240]) ).
tcf(c_19876,plain,
( colinear(a,c,d)
| between(b,a,c)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_13017,c_240]) ).
tcf(c_19949,plain,
( between(b,a,c)
| between(a,c,b)
| between(a,b,d) ),
inference(global_subsumption_just,[status(thm)],[c_14209,c_255,c_19709,c_19772]) ).
tcf(c_19965,plain,
( between(a,c,b)
| between(a,b,d)
| ( a = b )
| ~ between(a,b,c) ),
inference(superposition,[status(thm)],[c_19949,c_204]) ).
tcf(c_20083,plain,
( between(a,b,d)
| between(a,c,b) ),
inference(global_subsumption_just,[status(thm)],[c_14207,c_252,c_13489,c_19965]) ).
tcf(c_20084,plain,
( between(a,c,b)
| between(a,b,d) ),
inference(renaming,[status(thm)],[c_20083]) ).
tcf(c_20109,plain,
( between(b,c,a)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_20084,c_1712]) ).
tcf(c_20185,plain,
( between(a,b,c)
| between(a,b,d)
| between(b,a,c) ),
inference(global_subsumption_just,[status(thm)],[c_14542,c_255,c_8871,c_19876]) ).
tcf(c_20186,plain,
( between(b,a,c)
| between(a,b,d)
| between(a,b,c) ),
inference(renaming,[status(thm)],[c_20185]) ).
tcf(c_20202,plain,
( between(a,b,d)
| between(a,b,c)
| ( a = c )
| ~ between(b,c,a) ),
inference(superposition,[status(thm)],[c_20186,c_205]) ).
tcf(c_20205,plain,
! [X0: $i] :
( between(a,b,d)
| between(a,b,c)
| between(b,a,X0)
| ~ between(b,c,X0) ),
inference(superposition,[status(thm)],[c_20186,c_212]) ).
tcf(c_20223,plain,
( between(b,d,c)
| between(b,a,d)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_20186,c_1273]) ).
tcf(c_20483,plain,
( colinear(d,b,c)
| between(a,d,b)
| between(a,b,d)
| between(a,b,c) ),
inference(forward_subsumption_resolution,[status(thm)],[c_15193,c_173]) ).
tcf(c_20498,plain,
( colinear(b,c,d)
| between(a,d,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_20483,c_242]) ).
tcf(c_20917,plain,
( between(a,b,c)
| ( b = d )
| ( a = c ) ),
inference(global_subsumption_just,[status(thm)],[c_15249,c_957,c_15249,c_18376,c_20084,c_20202]) ).
tcf(c_20934,plain,
( ( b = d )
| ( b = c )
| ( a = c )
| ~ between(a,c,b) ),
inference(superposition,[status(thm)],[c_20917,c_205]) ).
tcf(c_20941,plain,
( between(c,b,a)
| ( b = d )
| ( a = c ) ),
inference(superposition,[status(thm)],[c_20917,c_202]) ).
tcf(c_21118,plain,
( colinear(b,c,d)
| between(b,a,d)
| between(a,d,b)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_15301,c_174]) ).
tcf(c_21179,plain,
( colinear(a,c,d)
| between(b,a,d)
| between(a,d,b)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_15315,c_174]) ).
tcf(c_21292,plain,
( colinear(a,c,d)
| between(c,d,a)
| between(a,d,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_15885,c_238]) ).
tcf(c_21477,plain,
( between(a,d,b)
| between(a,b,d)
| between(a,b,c)
| between(c,d,a) ),
inference(global_subsumption_just,[status(thm)],[c_15889,c_255,c_20498,c_21292]) ).
tcf(c_21478,plain,
( between(c,d,a)
| between(a,d,b)
| between(a,b,d)
| between(a,b,c) ),
inference(renaming,[status(thm)],[c_21477]) ).
tcf(c_21501,plain,
( colinear(a,c,d)
| between(a,d,b)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_21478,c_173]) ).
tcf(c_21609,plain,
( between(a,b,c)
| between(a,d,b)
| between(b,a,d) ),
inference(global_subsumption_just,[status(thm)],[c_16001,c_255,c_21118,c_21179]) ).
tcf(c_21610,plain,
( between(b,a,d)
| between(a,d,b)
| between(a,b,c) ),
inference(renaming,[status(thm)],[c_21609]) ).
tcf(c_21625,plain,
( between(a,d,b)
| between(a,b,c)
| ( a = b )
| ~ between(a,b,d) ),
inference(superposition,[status(thm)],[c_21610,c_204]) ).
tcf(c_21826,plain,
( between(b,a,d)
| between(a,b,d)
| between(a,b,c)
| ( c = d )
| ( b = d ) ),
inference(global_subsumption_just,[status(thm)],[c_16378,c_16378,c_20223]) ).
tcf(c_21887,plain,
( between(a,d,b)
| between(a,b,c) ),
inference(global_subsumption_just,[status(thm)],[c_13087,c_252,c_255,c_20498,c_21501,c_21625]) ).
tcf(c_21902,plain,
( between(a,b,c)
| ( b = d )
| ~ between(a,b,d) ),
inference(superposition,[status(thm)],[c_21887,c_205]) ).
tcf(c_21947,plain,
( between(a,b,d)
| between(b,c,a) ),
inference(global_subsumption_just,[status(thm)],[c_13384,c_20109]) ).
tcf(c_21948,plain,
( between(b,c,a)
| between(a,b,d) ),
inference(renaming,[status(thm)],[c_21947]) ).
tcf(c_21963,plain,
! [X0: $i] :
( between(a,b,d)
| between(c,a,X0)
| ~ between(b,a,X0) ),
inference(superposition,[status(thm)],[c_21948,c_208]) ).
tcf(c_21965,plain,
! [X0: $i] :
( between(a,b,d)
| between(b,c,X0)
| ~ between(b,a,X0) ),
inference(superposition,[status(thm)],[c_21948,c_212]) ).
tcf(c_21982,plain,
( between(b,d,c)
| between(b,c,d)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_21948,c_4371]) ).
tcf(c_21983,plain,
( between(d,c,a)
| between(c,d,a)
| between(b,a,d)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_21948,c_2255]) ).
tcf(c_22128,plain,
! [X0: $i] :
( between(a,b,d)
| between(a,b,c)
| between(c,a,X0)
| ~ between(b,c,X0) ),
inference(global_subsumption_just,[status(thm)],[c_16572,c_20205,c_21963]) ).
tcf(c_22256,plain,
! [X0: $i] :
( between(b,a,d)
| ~ between(b,X0,d)
| ( b = d )
| between(X0,c,d)
| between(c,X0,d)
| between(a,b,c) ),
inference(global_subsumption_just,[status(thm)],[c_16376,c_16376,c_21902]) ).
tcf(c_22257,plain,
! [X0: $i] :
( between(b,a,d)
| between(a,b,c)
| between(c,X0,d)
| between(X0,c,d)
| ( b = d )
| ~ between(b,X0,d) ),
inference(renaming,[status(thm)],[c_22256]) ).
tcf(c_22272,plain,
( between(c,b,d)
| between(b,c,d)
| between(b,a,d)
| between(a,b,c)
| ( b = d ) ),
inference(superposition,[status(thm)],[c_203,c_22257]) ).
tcf(c_22358,plain,
( between(b,a,d)
| ( b = d )
| ( c = d )
| between(a,b,c) ),
inference(global_subsumption_just,[status(thm)],[c_16371,c_21826,c_21902]) ).
tcf(c_22359,plain,
( between(b,a,d)
| between(a,b,c)
| ( c = d )
| ( b = d ) ),
inference(renaming,[status(thm)],[c_22358]) ).
tcf(c_22380,plain,
! [X0: $i] :
( between(a,b,c)
| between(b,a,X0)
| ( c = d )
| ( b = d )
| ~ between(b,d,X0) ),
inference(superposition,[status(thm)],[c_22359,c_212]) ).
tcf(c_22395,plain,
( between(c,a,d)
| between(b,a,c)
| between(a,b,c)
| ( c = d )
| ( b = d ) ),
inference(superposition,[status(thm)],[c_22359,c_1645]) ).
tcf(c_23027,plain,
( between(a,c,b)
| ( b = d ) ),
inference(global_subsumption_just,[status(thm)],[c_18376,c_18376,c_20084]) ).
tcf(c_23040,plain,
! [X0: $i] :
( between(c,X0,b)
| between(X0,c,b)
| ( b = d )
| ~ between(a,X0,b) ),
inference(superposition,[status(thm)],[c_23027,c_235]) ).
tcf(c_23042,plain,
( ( b = d )
| ( b = c )
| ~ between(a,b,c) ),
inference(superposition,[status(thm)],[c_23027,c_205]) ).
tcf(c_23053,plain,
( between(b,c,a)
| ( b = d ) ),
inference(superposition,[status(thm)],[c_23027,c_1712]) ).
tcf(c_23224,plain,
( between(b,d,c)
| between(b,c,d)
| between(a,b,d) ),
inference(global_subsumption_just,[status(thm)],[c_18747,c_21982]) ).
tcf(c_23250,plain,
( colinear(b,c,d)
| between(b,c,d)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_23224,c_239]) ).
tcf(c_23251,plain,
( colinear(d,b,c)
| between(b,c,d)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_23224,c_240]) ).
tcf(c_23279,plain,
! [X0: $i] :
( between(a,b,d)
| ~ between(b,a,X0)
| between(b,c,X0) ),
inference(global_subsumption_just,[status(thm)],[c_18730,c_21965]) ).
tcf(c_23280,plain,
! [X0: $i] :
( between(a,b,d)
| between(b,c,X0)
| ~ between(b,a,X0) ),
inference(renaming,[status(thm)],[c_23279]) ).
tcf(c_23322,plain,
! [X0: $i] :
( between(a,b,d)
| ~ between(b,a,X0)
| between(c,a,X0) ),
inference(global_subsumption_just,[status(thm)],[c_18728,c_21963]) ).
tcf(c_23323,plain,
! [X0: $i] :
( between(a,b,d)
| between(c,a,X0)
| ~ between(b,a,X0) ),
inference(renaming,[status(thm)],[c_23322]) ).
tcf(c_23390,plain,
( between(d,c,a)
| between(b,c,d)
| between(a,b,d)
| between(a,b,c) ),
inference(forward_subsumption_resolution,[status(thm)],[c_18751,c_23280]) ).
tcf(c_23420,plain,
( colinear(a,c,d)
| between(b,c,d)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_23390,c_238]) ).
tcf(c_23445,plain,
( between(d,c,a)
| between(c,d,a)
| between(b,a,d)
| between(a,b,d) ),
inference(global_subsumption_just,[status(thm)],[c_18748,c_21983]) ).
tcf(c_23471,plain,
( between(c,d,a)
| between(b,a,d)
| between(a,c,d)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_23445,c_202]) ).
tcf(c_23472,plain,
( colinear(a,c,d)
| between(c,d,a)
| between(b,a,d)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_23445,c_238]) ).
tcf(c_23474,plain,
( colinear(c,d,a)
| between(c,d,a)
| between(b,a,d)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_23445,c_240]) ).
tcf(c_23829,plain,
( between(b,c,d)
| between(a,b,c)
| between(a,b,d) ),
inference(global_subsumption_just,[status(thm)],[c_16993,c_255,c_23250,c_23420]) ).
tcf(c_23830,plain,
( between(b,c,d)
| between(a,b,d)
| between(a,b,c) ),
inference(renaming,[status(thm)],[c_23829]) ).
tcf(c_23861,plain,
( between(c,a,d)
| between(a,b,d)
| between(a,b,c) ),
inference(superposition,[status(thm)],[c_23830,c_22128]) ).
tcf(c_25212,plain,
( ( b = d )
| ( b = c )
| ( a = c )
| ~ between(b,c,a) ),
inference(superposition,[status(thm)],[c_20941,c_204]) ).
tcf(c_25251,plain,
( between(d,c,b)
| between(c,d,b)
| between(b,a,d)
| between(a,d,b)
| ( b = d )
| ( a = c ) ),
inference(superposition,[status(thm)],[c_20941,c_2015]) ).
tcf(c_25295,plain,
( ( b = d )
| ( b = c )
| ( a = c ) ),
inference(global_subsumption_just,[status(thm)],[c_20934,c_23053,c_25212]) ).
tcf(c_25389,plain,
( ( b = c )
| ( a = c )
| ~ colinear(b,c,d)
| ~ colinear(a,c,b) ),
inference(superposition,[status(thm)],[c_25295,c_255]) ).
tcf(c_26251,plain,
( between(a,b,c)
| ( b = d )
| between(b,c,d) ),
inference(global_subsumption_just,[status(thm)],[c_22272,c_21902,c_23830]) ).
tcf(c_26252,plain,
( between(b,c,d)
| between(a,b,c)
| ( b = d ) ),
inference(renaming,[status(thm)],[c_26251]) ).
tcf(c_26273,plain,
( colinear(b,c,d)
| between(a,b,c)
| ( b = d ) ),
inference(superposition,[status(thm)],[c_26252,c_172]) ).
tcf(c_26445,plain,
( between(c,a,d)
| ( b = d )
| between(a,b,c) ),
inference(global_subsumption_just,[status(thm)],[c_22395,c_21902,c_23861]) ).
tcf(c_26446,plain,
( between(c,a,d)
| between(a,b,c)
| ( b = d ) ),
inference(renaming,[status(thm)],[c_26445]) ).
tcf(c_26473,plain,
( colinear(a,c,d)
| between(a,b,c)
| ( b = d ) ),
inference(superposition,[status(thm)],[c_26446,c_240]) ).
tcf(c_26600,plain,
( between(a,b,c)
| ( b = d ) ),
inference(global_subsumption_just,[status(thm)],[c_22380,c_255,c_26273,c_26473]) ).
tcf(c_27241,plain,
( ( b = d )
| ( b = c ) ),
inference(global_subsumption_just,[status(thm)],[c_23042,c_23042,c_26600]) ).
tcf(c_27335,plain,
( ( b = c )
| ~ colinear(b,c,d)
| ~ colinear(a,c,b) ),
inference(superposition,[status(thm)],[c_27241,c_255]) ).
tcf(c_27849,plain,
( colinear(d,b,c)
| between(a,b,d) ),
inference(forward_subsumption_resolution,[status(thm)],[c_23251,c_173]) ).
tcf(c_27859,plain,
( colinear(b,c,d)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_27849,c_242]) ).
tcf(c_29007,plain,
( between(a,b,d)
| between(b,a,d)
| between(c,d,a) ),
inference(global_subsumption_just,[status(thm)],[c_23474,c_255,c_23472,c_27859]) ).
tcf(c_29008,plain,
( between(c,d,a)
| between(b,a,d)
| between(a,b,d) ),
inference(renaming,[status(thm)],[c_29007]) ).
tcf(c_29030,plain,
( colinear(a,c,d)
| between(b,a,d)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_29008,c_173]) ).
tcf(c_29054,plain,
( between(a,b,d)
| between(b,a,d) ),
inference(global_subsumption_just,[status(thm)],[c_23471,c_255,c_27859,c_29030]) ).
tcf(c_29055,plain,
( between(b,a,d)
| between(a,b,d) ),
inference(renaming,[status(thm)],[c_29054]) ).
tcf(c_29077,plain,
( between(d,a,b)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_29055,c_202]) ).
tcf(c_29090,plain,
( between(c,a,d)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_29055,c_23323]) ).
tcf(c_30611,plain,
( between(d,c,b)
| between(c,d,b)
| between(b,a,d)
| ( b = d )
| ( a = c ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_25251,c_23040]) ).
tcf(c_30647,plain,
( colinear(c,d,b)
| between(c,d,b)
| between(b,a,d)
| ( b = d )
| ( a = c ) ),
inference(superposition,[status(thm)],[c_30611,c_240]) ).
tcf(c_30842,plain,
( ( b = c )
| ~ colinear(b,c,d) ),
inference(global_subsumption_just,[status(thm)],[c_25389,c_291,c_27335]) ).
tcf(c_30848,plain,
( ( b = c )
| ~ colinear(b,c,b) ),
inference(superposition,[status(thm)],[c_27241,c_30842]) ).
tcf(c_34124,plain,
( colinear(a,c,d)
| between(a,b,d) ),
inference(superposition,[status(thm)],[c_29090,c_240]) ).
tcf(c_34144,plain,
between(a,b,d),
inference(global_subsumption_just,[status(thm)],[c_29077,c_255,c_27859,c_34124]) ).
tcf(c_34155,plain,
( ( a = b )
| ~ between(b,a,d) ),
inference(superposition,[status(thm)],[c_34144,c_204]) ).
tcf(c_34693,plain,
( colinear(c,d,b)
| between(c,d,b)
| ( a = c )
| ( b = d ) ),
inference(global_subsumption_just,[status(thm)],[c_30647,c_252,c_30647,c_34155]) ).
tcf(c_34694,plain,
( colinear(c,d,b)
| between(c,d,b)
| ( b = d )
| ( a = c ) ),
inference(renaming,[status(thm)],[c_34693]) ).
tcf(c_34699,plain,
( colinear(c,d,b)
| ( b = d )
| ( a = c ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_34694,c_172]) ).
tcf(c_34714,plain,
( colinear(b,c,d)
| ( b = d )
| ( a = c ) ),
inference(superposition,[status(thm)],[c_34699,c_244]) ).
tcf(c_34715,plain,
( colinear(d,c,b)
| ( b = d )
| ( a = c ) ),
inference(superposition,[status(thm)],[c_34699,c_245]) ).
tcf(c_35142,plain,
b = c,
inference(forward_subsumption_resolution,[status(thm)],[c_30848,c_250]) ).
tcf(c_35204,plain,
( ~ colinear(b,c,d)
| ~ colinear(a,b,d) ),
inference(superposition,[status(thm)],[c_35142,c_255]) ).
tcf(c_36156,plain,
( ( a = c )
| ( b = d ) ),
inference(global_subsumption_just,[status(thm)],[c_34715,c_254,c_34714,c_35204]) ).
tcf(c_36157,plain,
( ( b = d )
| ( a = c ) ),
inference(renaming,[status(thm)],[c_36156]) ).
tcf(c_36160,plain,
( ( b = d )
| ( a = b ) ),
inference(light_normalisation,[status(thm)],[c_36157,c_35142]) ).
tcf(c_36163,plain,
b = d,
inference(forward_subsumption_resolution,[status(thm)],[c_36160,c_252]) ).
tcf(c_36365,plain,
~ colinear(b,c,d),
inference(global_subsumption_just,[status(thm)],[c_35204,c_254,c_35204]) ).
tcf(c_36367,plain,
~ colinear(b,b,b),
inference(light_normalisation,[status(thm)],[c_36365,c_35142,c_36163]) ).
tcf(c_36368,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_36367,c_247]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO012-3 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.12/0.59 % Computer : n013.cluster.edu
% 0.12/0.59 % Model : x86_64 x86_64
% 0.12/0.59 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.59 % Memory : 8046.5625MB
% 0.12/0.59 % OS : Linux 6.8.0-71-generic
% 0.12/0.60 % CPULimit : 300
% 0.12/0.60 % WCLimit : 300
% 0.12/0.60 % DateTime : Wed Sep 23 10:22:07 UTC 2026
% 0.12/0.60 % CPUTime :
% 0.12/0.60 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.16/0.66 Running first-order theorem proving
% 0.16/0.66 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.67
% 0.16/0.67 % ======== iProver multi-core TPTP/SMT =========
% 0.16/0.67
% 0.16/0.68 % Detected problem language: tptp
% 0.16/0.70 % Proving...
% 27.10/4.77 % SZS status Started for theBenchmark.p
% 27.10/4.77 % SZS status Unsatisfiable for theBenchmark.p
% 27.10/4.77
% 27.10/4.77 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 27.10/4.77
% 27.10/4.77 % ------ iProver source info
% 27.10/4.77
% 27.10/4.77 % git: date: 2026-07-19 20:42:38 +0200
% 27.10/4.77 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 27.10/4.77 % git: non_committed_changes: false
% 27.10/4.77
% 27.10/4.77 % ------ Parsing...% successful
% 27.10/4.77
% 27.10/4.77
% 27.10/4.77 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 27.10/4.77 % ------ Proving...
% 27.10/4.77 % ------ Problem Properties
% 27.10/4.77
% 27.10/4.77 %
% 27.10/4.77 % clauses 102
% 27.10/4.77 % conjectures 1
% 27.10/4.77 % EPR 72
% 27.10/4.77 % Horn 81
% 27.10/4.77 % unary 33
% 27.10/4.77 % binary 27
% 27.10/4.77 % lits 266
% 27.10/4.77 % lits eq 43
% 27.10/4.77 % fd_pure 0
% 27.10/4.77 % fd_pseudo 0
% 27.10/4.77 % fd_cond 0
% 27.10/4.77 % fd_pseudo_cond 23
% 27.10/4.77 % AC symbols 0
% 27.10/4.77
% 27.10/4.77 % ------ Input Options Time Limit: Unbounded
% 27.10/4.77
% 27.10/4.77
% 27.10/4.77 % ------
% 27.10/4.77 % Current options:
% 27.10/4.77 % ------
% 27.10/4.77
% 27.10/4.77
% 27.10/4.77 %
% 27.10/4.77
% 27.10/4.77 % ------ Proving...
% 27.10/4.77 %
% 27.10/4.77
% 27.10/4.77 % ------ Proving...
% 27.10/4.77 %
% 27.10/4.77
% 27.10/4.77 % SZS status Unsatisfiable for theBenchmark.p
% 27.10/4.77
% 27.10/4.77 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 27.10/4.78
% 27.10/4.78
%------------------------------------------------------------------------------