%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : GEO545+1 : TPTP v9.3.1. Released v7.5.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 : n026.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:13:29 AM UTC 2026
% Result : Theorem 14.24s 4.86s
% Output : Refutation 15.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 116
% Syntax : Number of formulae : 265 ( 54 unt; 0 typ; 21 def)
% Number of atoms : 1241 ( 58 equ; 0 cnn)
% Maximal formula atoms : 28 ( 4 avg)
% Number of connectives : 5818 ( 100 ~; 58 |; 676 &;4783 @)
% ( 0 <=>; 201 =>; 0 <=; 0 <~>)
% Maximal formula depth : 53 ( 12 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 35 ( 32 usr; 22 con; 0-8 aty)
% Number of variables : 1404 ( 2 ^;1161 !; 220 ?;1404 :)
% ( 0 !>; 0 ?*; 0 @-; 21 @+)
% Comments :
%------------------------------------------------------------------------------
thf(perp_decl,type,
perp: $i > $i > $i > $i > $o ).
thf(midp_decl,type,
midp: $i > $i > $i > $o ).
thf(contri_decl,type,
contri: $i > $i > $i > $i > $i > $i > $o ).
thf(simtri_decl,type,
simtri: $i > $i > $i > $i > $i > $i > $o ).
thf(cong_decl,type,
cong: $i > $i > $i > $i > $o ).
thf(eqangle_decl,type,
eqangle: $i > $i > $i > $i > $i > $i > $i > $i > $o ).
thf(eqratio_decl,type,
eqratio: $i > $i > $i > $i > $i > $i > $i > $i > $o ).
thf(cyclic_decl,type,
cyclic: $i > $i > $i > $i > $o ).
thf(coll_decl,type,
coll: $i > $i > $i > $o ).
thf(para_decl,type,
para: $i > $i > $i > $i > $o ).
thf(circle_decl,type,
circle: $i > $i > $i > $i > $o ).
thf(sk1_decl,type,
sk1: $i ).
thf(sk2_decl,type,
sk2: $i ).
thf(sk3_decl,type,
sk3: $i ).
thf(sk4_decl,type,
sk4: $i ).
thf(sk5_decl,type,
sk5: $i ).
thf(sk6_decl,type,
sk6: $i ).
thf(sk7_decl,type,
sk7: $i ).
thf(sk8_decl,type,
sk8: $i ).
thf(sk9_decl,type,
sk9: $i ).
thf(sk10_decl,type,
sk10: $i ).
thf(sk11_decl,type,
sk11: $i ).
thf(sk12_decl,type,
sk12: $i ).
thf(sk13_decl,type,
sk13: $i ).
thf(sk14_decl,type,
sk14: $i ).
thf(sk15_decl,type,
sk15: $i ).
thf(sk16_decl,type,
sk16: $i ).
thf(sk17_decl,type,
sk17: $i ).
thf(sk18_decl,type,
sk18: $i ).
thf(sk19_decl,type,
sk19: $i ).
thf(sk20_decl,type,
sk20: $i ).
thf(sk36_decl,type,
sk36: $i > $i > $i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i] :
~ ! [B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( ? [I: $i] :
( ? [J: $i] :
( ? [K: $i] :
( ? [L: $i] :
( ? [M: $i] :
( ? [N: $i] :
( ? [O: $i] :
( ? [P: $i] :
( ? [Q: $i] :
( ? [R: $i] :
( ? [S: $i] :
( ? [T: $i] :
( ( H @ ( T @ ( C @ ( D @ perp ) ) ) )
& ( C @ ( D @ ( T @ midp ) ) ) )
& ( H @ ( S @ ( C @ ( B @ perp ) ) ) )
& ( C @ ( B @ ( S @ midp ) ) ) )
& ( H @ ( R @ ( D @ ( B @ perp ) ) ) )
& ( D @ ( B @ ( R @ midp ) ) ) )
& ( G @ ( Q @ ( C @ ( D @ perp ) ) ) )
& ( C @ ( D @ ( Q @ midp ) ) ) )
& ( G @ ( P @ ( C @ ( A @ perp ) ) ) )
& ( C @ ( A @ ( P @ midp ) ) ) )
& ( G @ ( O @ ( D @ ( A @ perp ) ) ) )
& ( D @ ( A @ ( O @ midp ) ) ) )
& ( F @ ( N @ ( D @ ( B @ perp ) ) ) )
& ( D @ ( B @ ( N @ midp ) ) ) )
& ( F @ ( M @ ( D @ ( A @ perp ) ) ) )
& ( D @ ( A @ ( M @ midp ) ) ) )
& ( F @ ( L @ ( B @ ( A @ perp ) ) ) )
& ( B @ ( A @ ( L @ midp ) ) ) )
& ( E @ ( K @ ( C @ ( B @ perp ) ) ) )
& ( C @ ( B @ ( K @ midp ) ) ) )
& ( E @ ( J @ ( C @ ( A @ perp ) ) ) )
& ( C @ ( A @ ( J @ midp ) ) ) )
& ( E @ ( I @ ( B @ ( A @ perp ) ) ) )
& ( B @ ( A @ ( I @ midp ) ) ) )
& ( D @ ( A @ ( C @ ( B @ perp ) ) ) )
& ( D @ ( B @ ( C @ ( A @ perp ) ) ) )
& ( D @ ( C @ ( B @ ( A @ perp ) ) ) ) )
=> ( F @ ( G @ ( E @ ( H @ perp ) ) ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: $i] :
~ ! [B: $i,C: $i,D: $i,E: $i,F: $i,G: $i] :
( ( ? [H: $i] :
( ? [I: $i] :
( ? [J: $i] :
( ? [K: $i] :
( ? [L: $i] :
( ? [M: $i] :
( ? [N: $i] :
( ? [O: $i] :
( ? [P: $i] :
( ? [Q: $i] :
( ? [R: $i] :
( ? [S: $i] :
( ( G @ ( S @ ( B @ ( C @ perp ) ) ) )
& ( B @ ( C @ ( S @ midp ) ) ) )
& ( G @ ( R @ ( B @ ( A @ perp ) ) ) )
& ( B @ ( A @ ( R @ midp ) ) ) )
& ( G @ ( Q @ ( C @ ( A @ perp ) ) ) )
& ( C @ ( A @ ( Q @ midp ) ) ) )
& ( F @ ( P @ ( B @ ( C @ perp ) ) ) )
& ( B @ ( C @ ( P @ midp ) ) ) )
& ( F @ ( O @ ( B @ ( sk1 @ perp ) ) ) )
& ( B @ ( sk1 @ ( O @ midp ) ) ) )
& ( F @ ( N @ ( C @ ( sk1 @ perp ) ) ) )
& ( C @ ( sk1 @ ( N @ midp ) ) ) )
& ( E @ ( M @ ( C @ ( A @ perp ) ) ) )
& ( C @ ( A @ ( M @ midp ) ) ) )
& ( E @ ( L @ ( C @ ( sk1 @ perp ) ) ) )
& ( C @ ( sk1 @ ( L @ midp ) ) ) )
& ( E @ ( K @ ( A @ ( sk1 @ perp ) ) ) )
& ( A @ ( sk1 @ ( K @ midp ) ) ) )
& ( D @ ( J @ ( B @ ( A @ perp ) ) ) )
& ( B @ ( A @ ( J @ midp ) ) ) )
& ( D @ ( I @ ( B @ ( sk1 @ perp ) ) ) )
& ( B @ ( sk1 @ ( I @ midp ) ) ) )
& ( D @ ( H @ ( A @ ( sk1 @ perp ) ) ) )
& ( A @ ( sk1 @ ( H @ midp ) ) ) )
& ( C @ ( sk1 @ ( B @ ( A @ perp ) ) ) )
& ( C @ ( A @ ( B @ ( sk1 @ perp ) ) ) )
& ( C @ ( B @ ( A @ ( sk1 @ perp ) ) ) ) )
=> ( E @ ( F @ ( D @ ( G @ perp ) ) ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: $i] :
~ ! [B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( ? [G: $i] :
( ? [H: $i] :
( ? [I: $i] :
( ? [J: $i] :
( ? [K: $i] :
( ? [L: $i] :
( ? [M: $i] :
( ? [N: $i] :
( ? [O: $i] :
( ? [P: $i] :
( ? [Q: $i] :
( ? [R: $i] :
( ( F @ ( R @ ( A @ ( B @ perp ) ) ) )
& ( A @ ( B @ ( R @ midp ) ) ) )
& ( F @ ( Q @ ( A @ ( sk2 @ perp ) ) ) )
& ( A @ ( sk2 @ ( Q @ midp ) ) ) )
& ( F @ ( P @ ( B @ ( sk2 @ perp ) ) ) )
& ( B @ ( sk2 @ ( P @ midp ) ) ) )
& ( E @ ( O @ ( A @ ( B @ perp ) ) ) )
& ( A @ ( B @ ( O @ midp ) ) ) )
& ( E @ ( N @ ( A @ ( sk1 @ perp ) ) ) )
& ( A @ ( sk1 @ ( N @ midp ) ) ) )
& ( E @ ( M @ ( B @ ( sk1 @ perp ) ) ) )
& ( B @ ( sk1 @ ( M @ midp ) ) ) )
& ( D @ ( L @ ( B @ ( sk2 @ perp ) ) ) )
& ( B @ ( sk2 @ ( L @ midp ) ) ) )
& ( D @ ( K @ ( B @ ( sk1 @ perp ) ) ) )
& ( B @ ( sk1 @ ( K @ midp ) ) ) )
& ( D @ ( J @ ( sk2 @ ( sk1 @ perp ) ) ) )
& ( sk2 @ ( sk1 @ ( J @ midp ) ) ) )
& ( C @ ( I @ ( A @ ( sk2 @ perp ) ) ) )
& ( A @ ( sk2 @ ( I @ midp ) ) ) )
& ( C @ ( H @ ( A @ ( sk1 @ perp ) ) ) )
& ( A @ ( sk1 @ ( H @ midp ) ) ) )
& ( C @ ( G @ ( sk2 @ ( sk1 @ perp ) ) ) )
& ( sk2 @ ( sk1 @ ( G @ midp ) ) ) )
& ( B @ ( sk1 @ ( A @ ( sk2 @ perp ) ) ) )
& ( B @ ( sk2 @ ( A @ ( sk1 @ perp ) ) ) )
& ( B @ ( A @ ( sk2 @ ( sk1 @ perp ) ) ) ) )
=> ( D @ ( E @ ( C @ ( F @ perp ) ) ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( @+[A: $i] :
~ ! [B: $i,C: $i,D: $i,E: $i] :
( ( ? [F: $i] :
( ? [G: $i] :
( ? [H: $i] :
( ? [I: $i] :
( ? [J: $i] :
( ? [K: $i] :
( ? [L: $i] :
( ? [M: $i] :
( ? [N: $i] :
( ? [O: $i] :
( ? [P: $i] :
( ? [Q: $i] :
( ( E @ ( Q @ ( sk3 @ ( A @ perp ) ) ) )
& ( sk3 @ ( A @ ( Q @ midp ) ) ) )
& ( E @ ( P @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk3 @ ( sk2 @ ( P @ midp ) ) ) )
& ( E @ ( O @ ( A @ ( sk2 @ perp ) ) ) )
& ( A @ ( sk2 @ ( O @ midp ) ) ) )
& ( D @ ( N @ ( sk3 @ ( A @ perp ) ) ) )
& ( sk3 @ ( A @ ( N @ midp ) ) ) )
& ( D @ ( M @ ( sk3 @ ( sk1 @ perp ) ) ) )
& ( sk3 @ ( sk1 @ ( M @ midp ) ) ) )
& ( D @ ( L @ ( A @ ( sk1 @ perp ) ) ) )
& ( A @ ( sk1 @ ( L @ midp ) ) ) )
& ( C @ ( K @ ( A @ ( sk2 @ perp ) ) ) )
& ( A @ ( sk2 @ ( K @ midp ) ) ) )
& ( C @ ( J @ ( A @ ( sk1 @ perp ) ) ) )
& ( A @ ( sk1 @ ( J @ midp ) ) ) )
& ( C @ ( I @ ( sk2 @ ( sk1 @ perp ) ) ) )
& ( sk2 @ ( sk1 @ ( I @ midp ) ) ) )
& ( B @ ( H @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk3 @ ( sk2 @ ( H @ midp ) ) ) )
& ( B @ ( G @ ( sk3 @ ( sk1 @ perp ) ) ) )
& ( sk3 @ ( sk1 @ ( G @ midp ) ) ) )
& ( B @ ( F @ ( sk2 @ ( sk1 @ perp ) ) ) )
& ( sk2 @ ( sk1 @ ( F @ midp ) ) ) )
& ( A @ ( sk1 @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( A @ ( sk2 @ ( sk3 @ ( sk1 @ perp ) ) ) )
& ( A @ ( sk3 @ ( sk2 @ ( sk1 @ perp ) ) ) ) )
=> ( C @ ( D @ ( B @ ( E @ perp ) ) ) ) ) ) ) ).
thf(sk5_def,definition,
( sk5
= ( @+[A: $i] :
~ ! [B: $i,C: $i,D: $i] :
( ( ? [E: $i] :
( ? [F: $i] :
( ? [G: $i] :
( ? [H: $i] :
( ? [I: $i] :
( ? [J: $i] :
( ? [K: $i] :
( ? [L: $i] :
( ? [M: $i] :
( ? [N: $i] :
( ? [O: $i] :
( ? [P: $i] :
( ( D @ ( P @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( P @ midp ) ) ) )
& ( D @ ( O @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk3 @ ( sk2 @ ( O @ midp ) ) ) )
& ( D @ ( N @ ( sk4 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( N @ midp ) ) ) )
& ( C @ ( M @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( M @ midp ) ) ) )
& ( C @ ( L @ ( sk3 @ ( sk1 @ perp ) ) ) )
& ( sk3 @ ( sk1 @ ( L @ midp ) ) ) )
& ( C @ ( K @ ( sk4 @ ( sk1 @ perp ) ) ) )
& ( sk4 @ ( sk1 @ ( K @ midp ) ) ) )
& ( B @ ( J @ ( sk4 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( J @ midp ) ) ) )
& ( B @ ( I @ ( sk4 @ ( sk1 @ perp ) ) ) )
& ( sk4 @ ( sk1 @ ( I @ midp ) ) ) )
& ( B @ ( H @ ( sk2 @ ( sk1 @ perp ) ) ) )
& ( sk2 @ ( sk1 @ ( H @ midp ) ) ) )
& ( A @ ( G @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk3 @ ( sk2 @ ( G @ midp ) ) ) )
& ( A @ ( F @ ( sk3 @ ( sk1 @ perp ) ) ) )
& ( sk3 @ ( sk1 @ ( F @ midp ) ) ) )
& ( A @ ( E @ ( sk2 @ ( sk1 @ perp ) ) ) )
& ( sk2 @ ( sk1 @ ( E @ midp ) ) ) )
& ( sk4 @ ( sk1 @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( sk3 @ ( sk1 @ perp ) ) ) )
& ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ perp ) ) ) ) )
=> ( B @ ( C @ ( A @ ( D @ perp ) ) ) ) ) ) ) ).
thf(sk6_def,definition,
( sk6
= ( @+[A: $i] :
~ ! [B: $i,C: $i] :
( ( ? [D: $i] :
( ? [E: $i] :
( ? [F: $i] :
( ? [G: $i] :
( ? [H: $i] :
( ? [I: $i] :
( ? [J: $i] :
( ? [K: $i] :
( ? [L: $i] :
( ? [M: $i] :
( ? [N: $i] :
( ? [O: $i] :
( ( C @ ( O @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( O @ midp ) ) ) )
& ( C @ ( N @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk3 @ ( sk2 @ ( N @ midp ) ) ) )
& ( C @ ( M @ ( sk4 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( M @ midp ) ) ) )
& ( B @ ( L @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( L @ midp ) ) ) )
& ( B @ ( K @ ( sk3 @ ( sk1 @ perp ) ) ) )
& ( sk3 @ ( sk1 @ ( K @ midp ) ) ) )
& ( B @ ( J @ ( sk4 @ ( sk1 @ perp ) ) ) )
& ( sk4 @ ( sk1 @ ( J @ midp ) ) ) )
& ( A @ ( I @ ( sk4 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( I @ midp ) ) ) )
& ( A @ ( H @ ( sk4 @ ( sk1 @ perp ) ) ) )
& ( sk4 @ ( sk1 @ ( H @ midp ) ) ) )
& ( A @ ( G @ ( sk2 @ ( sk1 @ perp ) ) ) )
& ( sk2 @ ( sk1 @ ( G @ midp ) ) ) )
& ( sk5 @ ( F @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk3 @ ( sk2 @ ( F @ midp ) ) ) )
& ( sk5 @ ( E @ ( sk3 @ ( sk1 @ perp ) ) ) )
& ( sk3 @ ( sk1 @ ( E @ midp ) ) ) )
& ( sk5 @ ( D @ ( sk2 @ ( sk1 @ perp ) ) ) )
& ( sk2 @ ( sk1 @ ( D @ midp ) ) ) )
& ( sk4 @ ( sk1 @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( sk3 @ ( sk1 @ perp ) ) ) )
& ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ perp ) ) ) ) )
=> ( A @ ( B @ ( sk5 @ ( C @ perp ) ) ) ) ) ) ) ).
thf(sk7_def,definition,
( sk7
= ( @+[A: $i] :
~ ! [B: $i] :
( ( ? [C: $i] :
( ? [D: $i] :
( ? [E: $i] :
( ? [F: $i] :
( ? [G: $i] :
( ? [H: $i] :
( ? [I: $i] :
( ? [J: $i] :
( ? [K: $i] :
( ? [L: $i] :
( ? [M: $i] :
( ? [N: $i] :
( ( B @ ( N @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( N @ midp ) ) ) )
& ( B @ ( M @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk3 @ ( sk2 @ ( M @ midp ) ) ) )
& ( B @ ( L @ ( sk4 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( L @ midp ) ) ) )
& ( A @ ( K @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( K @ midp ) ) ) )
& ( A @ ( J @ ( sk3 @ ( sk1 @ perp ) ) ) )
& ( sk3 @ ( sk1 @ ( J @ midp ) ) ) )
& ( A @ ( I @ ( sk4 @ ( sk1 @ perp ) ) ) )
& ( sk4 @ ( sk1 @ ( I @ midp ) ) ) )
& ( sk6 @ ( H @ ( sk4 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( H @ midp ) ) ) )
& ( sk6 @ ( G @ ( sk4 @ ( sk1 @ perp ) ) ) )
& ( sk4 @ ( sk1 @ ( G @ midp ) ) ) )
& ( sk6 @ ( F @ ( sk2 @ ( sk1 @ perp ) ) ) )
& ( sk2 @ ( sk1 @ ( F @ midp ) ) ) )
& ( sk5 @ ( E @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk3 @ ( sk2 @ ( E @ midp ) ) ) )
& ( sk5 @ ( D @ ( sk3 @ ( sk1 @ perp ) ) ) )
& ( sk3 @ ( sk1 @ ( D @ midp ) ) ) )
& ( sk5 @ ( C @ ( sk2 @ ( sk1 @ perp ) ) ) )
& ( sk2 @ ( sk1 @ ( C @ midp ) ) ) )
& ( sk4 @ ( sk1 @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( sk3 @ ( sk1 @ perp ) ) ) )
& ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ perp ) ) ) ) )
=> ( sk6 @ ( A @ ( sk5 @ ( B @ perp ) ) ) ) ) ) ) ).
thf(sk8_def,definition,
( sk8
= ( @+[A: $i] :
~ ( ( ? [B: $i] :
( ? [C: $i] :
( ? [D: $i] :
( ? [E: $i] :
( ? [F: $i] :
( ? [G: $i] :
( ? [H: $i] :
( ? [I: $i] :
( ? [J: $i] :
( ? [K: $i] :
( ? [L: $i] :
( ? [M: $i] :
( ( A @ ( M @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( M @ midp ) ) ) )
& ( A @ ( L @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk3 @ ( sk2 @ ( L @ midp ) ) ) )
& ( A @ ( K @ ( sk4 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( K @ midp ) ) ) )
& ( sk7 @ ( J @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( J @ midp ) ) ) )
& ( sk7 @ ( I @ ( sk3 @ ( sk1 @ perp ) ) ) )
& ( sk3 @ ( sk1 @ ( I @ midp ) ) ) )
& ( sk7 @ ( H @ ( sk4 @ ( sk1 @ perp ) ) ) )
& ( sk4 @ ( sk1 @ ( H @ midp ) ) ) )
& ( sk6 @ ( G @ ( sk4 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( G @ midp ) ) ) )
& ( sk6 @ ( F @ ( sk4 @ ( sk1 @ perp ) ) ) )
& ( sk4 @ ( sk1 @ ( F @ midp ) ) ) )
& ( sk6 @ ( E @ ( sk2 @ ( sk1 @ perp ) ) ) )
& ( sk2 @ ( sk1 @ ( E @ midp ) ) ) )
& ( sk5 @ ( D @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk3 @ ( sk2 @ ( D @ midp ) ) ) )
& ( sk5 @ ( C @ ( sk3 @ ( sk1 @ perp ) ) ) )
& ( sk3 @ ( sk1 @ ( C @ midp ) ) ) )
& ( sk5 @ ( B @ ( sk2 @ ( sk1 @ perp ) ) ) )
& ( sk2 @ ( sk1 @ ( B @ midp ) ) ) )
& ( sk4 @ ( sk1 @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( sk3 @ ( sk1 @ perp ) ) ) )
& ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ perp ) ) ) ) )
=> ( sk6 @ ( sk7 @ ( sk5 @ ( A @ perp ) ) ) ) ) ) ) ).
thf(sk9_def,definition,
( sk9
= ( @+[A: $i] :
( ? [B: $i] :
( ? [C: $i] :
( ? [D: $i] :
( ? [E: $i] :
( ? [F: $i] :
( ? [G: $i] :
( ? [H: $i] :
( ? [I: $i] :
( ? [J: $i] :
( ? [K: $i] :
( ? [L: $i] :
( ( sk8 @ ( L @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( L @ midp ) ) ) )
& ( sk8 @ ( K @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk3 @ ( sk2 @ ( K @ midp ) ) ) )
& ( sk8 @ ( J @ ( sk4 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( J @ midp ) ) ) )
& ( sk7 @ ( I @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( I @ midp ) ) ) )
& ( sk7 @ ( H @ ( sk3 @ ( sk1 @ perp ) ) ) )
& ( sk3 @ ( sk1 @ ( H @ midp ) ) ) )
& ( sk7 @ ( G @ ( sk4 @ ( sk1 @ perp ) ) ) )
& ( sk4 @ ( sk1 @ ( G @ midp ) ) ) )
& ( sk6 @ ( F @ ( sk4 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( F @ midp ) ) ) )
& ( sk6 @ ( E @ ( sk4 @ ( sk1 @ perp ) ) ) )
& ( sk4 @ ( sk1 @ ( E @ midp ) ) ) )
& ( sk6 @ ( D @ ( sk2 @ ( sk1 @ perp ) ) ) )
& ( sk2 @ ( sk1 @ ( D @ midp ) ) ) )
& ( sk5 @ ( C @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk3 @ ( sk2 @ ( C @ midp ) ) ) )
& ( sk5 @ ( B @ ( sk3 @ ( sk1 @ perp ) ) ) )
& ( sk3 @ ( sk1 @ ( B @ midp ) ) ) )
& ( sk5 @ ( A @ ( sk2 @ ( sk1 @ perp ) ) ) )
& ( sk2 @ ( sk1 @ ( A @ midp ) ) ) ) ) ) ).
thf(sk10_def,definition,
( sk10
= ( @+[A: $i] :
( ? [B: $i] :
( ? [C: $i] :
( ? [D: $i] :
( ? [E: $i] :
( ? [F: $i] :
( ? [G: $i] :
( ? [H: $i] :
( ? [I: $i] :
( ? [J: $i] :
( ? [K: $i] :
( ( sk8 @ ( K @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( K @ midp ) ) ) )
& ( sk8 @ ( J @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk3 @ ( sk2 @ ( J @ midp ) ) ) )
& ( sk8 @ ( I @ ( sk4 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( I @ midp ) ) ) )
& ( sk7 @ ( H @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( H @ midp ) ) ) )
& ( sk7 @ ( G @ ( sk3 @ ( sk1 @ perp ) ) ) )
& ( sk3 @ ( sk1 @ ( G @ midp ) ) ) )
& ( sk7 @ ( F @ ( sk4 @ ( sk1 @ perp ) ) ) )
& ( sk4 @ ( sk1 @ ( F @ midp ) ) ) )
& ( sk6 @ ( E @ ( sk4 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( E @ midp ) ) ) )
& ( sk6 @ ( D @ ( sk4 @ ( sk1 @ perp ) ) ) )
& ( sk4 @ ( sk1 @ ( D @ midp ) ) ) )
& ( sk6 @ ( C @ ( sk2 @ ( sk1 @ perp ) ) ) )
& ( sk2 @ ( sk1 @ ( C @ midp ) ) ) )
& ( sk5 @ ( B @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk3 @ ( sk2 @ ( B @ midp ) ) ) )
& ( sk5 @ ( A @ ( sk3 @ ( sk1 @ perp ) ) ) )
& ( sk3 @ ( sk1 @ ( A @ midp ) ) ) ) ) ) ).
thf(sk11_def,definition,
( sk11
= ( @+[A: $i] :
( ? [B: $i] :
( ? [C: $i] :
( ? [D: $i] :
( ? [E: $i] :
( ? [F: $i] :
( ? [G: $i] :
( ? [H: $i] :
( ? [I: $i] :
( ? [J: $i] :
( ( sk8 @ ( J @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( J @ midp ) ) ) )
& ( sk8 @ ( I @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk3 @ ( sk2 @ ( I @ midp ) ) ) )
& ( sk8 @ ( H @ ( sk4 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( H @ midp ) ) ) )
& ( sk7 @ ( G @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( G @ midp ) ) ) )
& ( sk7 @ ( F @ ( sk3 @ ( sk1 @ perp ) ) ) )
& ( sk3 @ ( sk1 @ ( F @ midp ) ) ) )
& ( sk7 @ ( E @ ( sk4 @ ( sk1 @ perp ) ) ) )
& ( sk4 @ ( sk1 @ ( E @ midp ) ) ) )
& ( sk6 @ ( D @ ( sk4 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( D @ midp ) ) ) )
& ( sk6 @ ( C @ ( sk4 @ ( sk1 @ perp ) ) ) )
& ( sk4 @ ( sk1 @ ( C @ midp ) ) ) )
& ( sk6 @ ( B @ ( sk2 @ ( sk1 @ perp ) ) ) )
& ( sk2 @ ( sk1 @ ( B @ midp ) ) ) )
& ( sk5 @ ( A @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk3 @ ( sk2 @ ( A @ midp ) ) ) ) ) ) ).
thf(sk12_def,definition,
( sk12
= ( @+[A: $i] :
( ? [B: $i] :
( ? [C: $i] :
( ? [D: $i] :
( ? [E: $i] :
( ? [F: $i] :
( ? [G: $i] :
( ? [H: $i] :
( ? [I: $i] :
( ( sk8 @ ( I @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( I @ midp ) ) ) )
& ( sk8 @ ( H @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk3 @ ( sk2 @ ( H @ midp ) ) ) )
& ( sk8 @ ( G @ ( sk4 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( G @ midp ) ) ) )
& ( sk7 @ ( F @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( F @ midp ) ) ) )
& ( sk7 @ ( E @ ( sk3 @ ( sk1 @ perp ) ) ) )
& ( sk3 @ ( sk1 @ ( E @ midp ) ) ) )
& ( sk7 @ ( D @ ( sk4 @ ( sk1 @ perp ) ) ) )
& ( sk4 @ ( sk1 @ ( D @ midp ) ) ) )
& ( sk6 @ ( C @ ( sk4 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( C @ midp ) ) ) )
& ( sk6 @ ( B @ ( sk4 @ ( sk1 @ perp ) ) ) )
& ( sk4 @ ( sk1 @ ( B @ midp ) ) ) )
& ( sk6 @ ( A @ ( sk2 @ ( sk1 @ perp ) ) ) )
& ( sk2 @ ( sk1 @ ( A @ midp ) ) ) ) ) ) ).
thf(sk13_def,definition,
( sk13
= ( @+[A: $i] :
( ? [B: $i] :
( ? [C: $i] :
( ? [D: $i] :
( ? [E: $i] :
( ? [F: $i] :
( ? [G: $i] :
( ? [H: $i] :
( ( sk8 @ ( H @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( H @ midp ) ) ) )
& ( sk8 @ ( G @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk3 @ ( sk2 @ ( G @ midp ) ) ) )
& ( sk8 @ ( F @ ( sk4 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( F @ midp ) ) ) )
& ( sk7 @ ( E @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( E @ midp ) ) ) )
& ( sk7 @ ( D @ ( sk3 @ ( sk1 @ perp ) ) ) )
& ( sk3 @ ( sk1 @ ( D @ midp ) ) ) )
& ( sk7 @ ( C @ ( sk4 @ ( sk1 @ perp ) ) ) )
& ( sk4 @ ( sk1 @ ( C @ midp ) ) ) )
& ( sk6 @ ( B @ ( sk4 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( B @ midp ) ) ) )
& ( sk6 @ ( A @ ( sk4 @ ( sk1 @ perp ) ) ) )
& ( sk4 @ ( sk1 @ ( A @ midp ) ) ) ) ) ) ).
thf(sk14_def,definition,
( sk14
= ( @+[A: $i] :
( ? [B: $i] :
( ? [C: $i] :
( ? [D: $i] :
( ? [E: $i] :
( ? [F: $i] :
( ? [G: $i] :
( ( sk8 @ ( G @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( G @ midp ) ) ) )
& ( sk8 @ ( F @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk3 @ ( sk2 @ ( F @ midp ) ) ) )
& ( sk8 @ ( E @ ( sk4 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( E @ midp ) ) ) )
& ( sk7 @ ( D @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( D @ midp ) ) ) )
& ( sk7 @ ( C @ ( sk3 @ ( sk1 @ perp ) ) ) )
& ( sk3 @ ( sk1 @ ( C @ midp ) ) ) )
& ( sk7 @ ( B @ ( sk4 @ ( sk1 @ perp ) ) ) )
& ( sk4 @ ( sk1 @ ( B @ midp ) ) ) )
& ( sk6 @ ( A @ ( sk4 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( A @ midp ) ) ) ) ) ) ).
thf(sk15_def,definition,
( sk15
= ( @+[A: $i] :
( ? [B: $i] :
( ? [C: $i] :
( ? [D: $i] :
( ? [E: $i] :
( ? [F: $i] :
( ( sk8 @ ( F @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( F @ midp ) ) ) )
& ( sk8 @ ( E @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk3 @ ( sk2 @ ( E @ midp ) ) ) )
& ( sk8 @ ( D @ ( sk4 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( D @ midp ) ) ) )
& ( sk7 @ ( C @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( C @ midp ) ) ) )
& ( sk7 @ ( B @ ( sk3 @ ( sk1 @ perp ) ) ) )
& ( sk3 @ ( sk1 @ ( B @ midp ) ) ) )
& ( sk7 @ ( A @ ( sk4 @ ( sk1 @ perp ) ) ) )
& ( sk4 @ ( sk1 @ ( A @ midp ) ) ) ) ) ) ).
thf(sk16_def,definition,
( sk16
= ( @+[A: $i] :
( ? [B: $i] :
( ? [C: $i] :
( ? [D: $i] :
( ? [E: $i] :
( ( sk8 @ ( E @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( E @ midp ) ) ) )
& ( sk8 @ ( D @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk3 @ ( sk2 @ ( D @ midp ) ) ) )
& ( sk8 @ ( C @ ( sk4 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( C @ midp ) ) ) )
& ( sk7 @ ( B @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( B @ midp ) ) ) )
& ( sk7 @ ( A @ ( sk3 @ ( sk1 @ perp ) ) ) )
& ( sk3 @ ( sk1 @ ( A @ midp ) ) ) ) ) ) ).
thf(sk17_def,definition,
( sk17
= ( @+[A: $i] :
( ? [B: $i] :
( ? [C: $i] :
( ? [D: $i] :
( ( sk8 @ ( D @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( D @ midp ) ) ) )
& ( sk8 @ ( C @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk3 @ ( sk2 @ ( C @ midp ) ) ) )
& ( sk8 @ ( B @ ( sk4 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( B @ midp ) ) ) )
& ( sk7 @ ( A @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( A @ midp ) ) ) ) ) ) ).
thf(sk18_def,definition,
( sk18
= ( @+[A: $i] :
( ? [B: $i] :
( ? [C: $i] :
( ( sk8 @ ( C @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( C @ midp ) ) ) )
& ( sk8 @ ( B @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk3 @ ( sk2 @ ( B @ midp ) ) ) )
& ( sk8 @ ( A @ ( sk4 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( A @ midp ) ) ) ) ) ) ).
thf(sk19_def,definition,
( sk19
= ( @+[A: $i] :
( ? [B: $i] :
( ( sk8 @ ( B @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( B @ midp ) ) ) )
& ( sk8 @ ( A @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk3 @ ( sk2 @ ( A @ midp ) ) ) ) ) ) ).
thf(sk20_def,definition,
( sk20
= ( @+[A: $i] :
( ( sk8 @ ( A @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( A @ midp ) ) ) ) ) ) ).
thf(sk36_def,definition,
( sk36
= ( ^ [A: $i,B: $i] :
@+[C: $i] : ( A @ ( B @ ( C @ midp ) ) ) ) ) ).
thf(22,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ coll ) ) )
=> ( B @ ( C @ ( A @ coll ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD1) ).
thf(169,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ coll ) ) )
=> ( B @ ( C @ ( A @ coll ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(1,conjecture,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i,I: $i,J: $i,K: $i,L: $i,M: $i,N: $i,O: $i,P: $i,Q: $i,R: $i,S: $i,T: $i] :
( ( ( H @ ( T @ ( C @ ( D @ perp ) ) ) )
& ( C @ ( D @ ( T @ midp ) ) )
& ( H @ ( S @ ( C @ ( B @ perp ) ) ) )
& ( C @ ( B @ ( S @ midp ) ) )
& ( H @ ( R @ ( D @ ( B @ perp ) ) ) )
& ( D @ ( B @ ( R @ midp ) ) )
& ( G @ ( Q @ ( C @ ( D @ perp ) ) ) )
& ( C @ ( D @ ( Q @ midp ) ) )
& ( G @ ( P @ ( C @ ( A @ perp ) ) ) )
& ( C @ ( A @ ( P @ midp ) ) )
& ( G @ ( O @ ( D @ ( A @ perp ) ) ) )
& ( D @ ( A @ ( O @ midp ) ) )
& ( F @ ( N @ ( D @ ( B @ perp ) ) ) )
& ( D @ ( B @ ( N @ midp ) ) )
& ( F @ ( M @ ( D @ ( A @ perp ) ) ) )
& ( D @ ( A @ ( M @ midp ) ) )
& ( F @ ( L @ ( B @ ( A @ perp ) ) ) )
& ( B @ ( A @ ( L @ midp ) ) )
& ( E @ ( K @ ( C @ ( B @ perp ) ) ) )
& ( C @ ( B @ ( K @ midp ) ) )
& ( E @ ( J @ ( C @ ( A @ perp ) ) ) )
& ( C @ ( A @ ( J @ midp ) ) )
& ( E @ ( I @ ( B @ ( A @ perp ) ) ) )
& ( B @ ( A @ ( I @ midp ) ) )
& ( D @ ( A @ ( C @ ( B @ perp ) ) ) )
& ( D @ ( B @ ( C @ ( A @ perp ) ) ) )
& ( D @ ( C @ ( B @ ( A @ perp ) ) ) ) )
=> ( F @ ( G @ ( E @ ( H @ perp ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',exemplo6GDDFULL012005) ).
thf(2,negated_conjecture,
~ ! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i,I: $i,J: $i,K: $i,L: $i,M: $i,N: $i,O: $i,P: $i,Q: $i,R: $i,S: $i,T: $i] :
( ( ( H @ ( T @ ( C @ ( D @ perp ) ) ) )
& ( C @ ( D @ ( T @ midp ) ) )
& ( H @ ( S @ ( C @ ( B @ perp ) ) ) )
& ( C @ ( B @ ( S @ midp ) ) )
& ( H @ ( R @ ( D @ ( B @ perp ) ) ) )
& ( D @ ( B @ ( R @ midp ) ) )
& ( G @ ( Q @ ( C @ ( D @ perp ) ) ) )
& ( C @ ( D @ ( Q @ midp ) ) )
& ( G @ ( P @ ( C @ ( A @ perp ) ) ) )
& ( C @ ( A @ ( P @ midp ) ) )
& ( G @ ( O @ ( D @ ( A @ perp ) ) ) )
& ( D @ ( A @ ( O @ midp ) ) )
& ( F @ ( N @ ( D @ ( B @ perp ) ) ) )
& ( D @ ( B @ ( N @ midp ) ) )
& ( F @ ( M @ ( D @ ( A @ perp ) ) ) )
& ( D @ ( A @ ( M @ midp ) ) )
& ( F @ ( L @ ( B @ ( A @ perp ) ) ) )
& ( B @ ( A @ ( L @ midp ) ) )
& ( E @ ( K @ ( C @ ( B @ perp ) ) ) )
& ( C @ ( B @ ( K @ midp ) ) )
& ( E @ ( J @ ( C @ ( A @ perp ) ) ) )
& ( C @ ( A @ ( J @ midp ) ) )
& ( E @ ( I @ ( B @ ( A @ perp ) ) ) )
& ( B @ ( A @ ( I @ midp ) ) )
& ( D @ ( A @ ( C @ ( B @ perp ) ) ) )
& ( D @ ( B @ ( C @ ( A @ perp ) ) ) )
& ( D @ ( C @ ( B @ ( A @ perp ) ) ) ) )
=> ( F @ ( G @ ( E @ ( H @ perp ) ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(97,plain,
~ ! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i,I: $i,J: $i,K: $i,L: $i,M: $i,N: $i,O: $i,P: $i,Q: $i,R: $i,S: $i,T: $i] :
( ( ( H @ ( T @ ( C @ ( D @ perp ) ) ) )
& ( C @ ( D @ ( T @ midp ) ) )
& ( H @ ( S @ ( C @ ( B @ perp ) ) ) )
& ( C @ ( B @ ( S @ midp ) ) )
& ( H @ ( R @ ( D @ ( B @ perp ) ) ) )
& ( D @ ( B @ ( R @ midp ) ) )
& ( G @ ( Q @ ( C @ ( D @ perp ) ) ) )
& ( C @ ( D @ ( Q @ midp ) ) )
& ( G @ ( P @ ( C @ ( A @ perp ) ) ) )
& ( C @ ( A @ ( P @ midp ) ) )
& ( G @ ( O @ ( D @ ( A @ perp ) ) ) )
& ( D @ ( A @ ( O @ midp ) ) )
& ( F @ ( N @ ( D @ ( B @ perp ) ) ) )
& ( D @ ( B @ ( N @ midp ) ) )
& ( F @ ( M @ ( D @ ( A @ perp ) ) ) )
& ( D @ ( A @ ( M @ midp ) ) )
& ( F @ ( L @ ( B @ ( A @ perp ) ) ) )
& ( B @ ( A @ ( L @ midp ) ) )
& ( E @ ( K @ ( C @ ( B @ perp ) ) ) )
& ( C @ ( B @ ( K @ midp ) ) )
& ( E @ ( J @ ( C @ ( A @ perp ) ) ) )
& ( C @ ( A @ ( J @ midp ) ) )
& ( E @ ( I @ ( B @ ( A @ perp ) ) ) )
& ( B @ ( A @ ( I @ midp ) ) )
& ( D @ ( A @ ( C @ ( B @ perp ) ) ) )
& ( D @ ( B @ ( C @ ( A @ perp ) ) ) )
& ( D @ ( C @ ( B @ ( A @ perp ) ) ) ) )
=> ( F @ ( G @ ( E @ ( H @ perp ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(98,plain,
~ ! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( ? [I: $i] :
( ? [J: $i] :
( ? [K: $i] :
( ? [L: $i] :
( ? [M: $i] :
( ? [N: $i] :
( ? [O: $i] :
( ? [P: $i] :
( ? [Q: $i] :
( ? [R: $i] :
( ? [S: $i] :
( ? [T: $i] :
( ( H @ ( T @ ( C @ ( D @ perp ) ) ) )
& ( C @ ( D @ ( T @ midp ) ) ) )
& ( H @ ( S @ ( C @ ( B @ perp ) ) ) )
& ( C @ ( B @ ( S @ midp ) ) ) )
& ( H @ ( R @ ( D @ ( B @ perp ) ) ) )
& ( D @ ( B @ ( R @ midp ) ) ) )
& ( G @ ( Q @ ( C @ ( D @ perp ) ) ) )
& ( C @ ( D @ ( Q @ midp ) ) ) )
& ( G @ ( P @ ( C @ ( A @ perp ) ) ) )
& ( C @ ( A @ ( P @ midp ) ) ) )
& ( G @ ( O @ ( D @ ( A @ perp ) ) ) )
& ( D @ ( A @ ( O @ midp ) ) ) )
& ( F @ ( N @ ( D @ ( B @ perp ) ) ) )
& ( D @ ( B @ ( N @ midp ) ) ) )
& ( F @ ( M @ ( D @ ( A @ perp ) ) ) )
& ( D @ ( A @ ( M @ midp ) ) ) )
& ( F @ ( L @ ( B @ ( A @ perp ) ) ) )
& ( B @ ( A @ ( L @ midp ) ) ) )
& ( E @ ( K @ ( C @ ( B @ perp ) ) ) )
& ( C @ ( B @ ( K @ midp ) ) ) )
& ( E @ ( J @ ( C @ ( A @ perp ) ) ) )
& ( C @ ( A @ ( J @ midp ) ) ) )
& ( E @ ( I @ ( B @ ( A @ perp ) ) ) )
& ( B @ ( A @ ( I @ midp ) ) ) )
& ( D @ ( A @ ( C @ ( B @ perp ) ) ) )
& ( D @ ( B @ ( C @ ( A @ perp ) ) ) )
& ( D @ ( C @ ( B @ ( A @ perp ) ) ) ) )
=> ( F @ ( G @ ( E @ ( H @ perp ) ) ) ) ),
inference(miniscope,[status(thm)],[97]) ).
thf(99,plain,
( ~ ( sk6 @ ( sk7 @ ( sk5 @ ( sk8 @ perp ) ) ) )
& ( sk8 @ ( sk20 @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( sk20 @ midp ) ) )
& ( sk8 @ ( sk19 @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk3 @ ( sk2 @ ( sk19 @ midp ) ) )
& ( sk8 @ ( sk18 @ ( sk4 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( sk18 @ midp ) ) )
& ( sk7 @ ( sk17 @ ( sk3 @ ( sk4 @ perp ) ) ) )
& ( sk3 @ ( sk4 @ ( sk17 @ midp ) ) )
& ( sk7 @ ( sk16 @ ( sk3 @ ( sk1 @ perp ) ) ) )
& ( sk3 @ ( sk1 @ ( sk16 @ midp ) ) )
& ( sk7 @ ( sk15 @ ( sk4 @ ( sk1 @ perp ) ) ) )
& ( sk4 @ ( sk1 @ ( sk15 @ midp ) ) )
& ( sk6 @ ( sk14 @ ( sk4 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( sk14 @ midp ) ) )
& ( sk6 @ ( sk13 @ ( sk4 @ ( sk1 @ perp ) ) ) )
& ( sk4 @ ( sk1 @ ( sk13 @ midp ) ) )
& ( sk6 @ ( sk12 @ ( sk2 @ ( sk1 @ perp ) ) ) )
& ( sk2 @ ( sk1 @ ( sk12 @ midp ) ) )
& ( sk5 @ ( sk11 @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk3 @ ( sk2 @ ( sk11 @ midp ) ) )
& ( sk5 @ ( sk10 @ ( sk3 @ ( sk1 @ perp ) ) ) )
& ( sk3 @ ( sk1 @ ( sk10 @ midp ) ) )
& ( sk5 @ ( sk9 @ ( sk2 @ ( sk1 @ perp ) ) ) )
& ( sk2 @ ( sk1 @ ( sk9 @ midp ) ) )
& ( sk4 @ ( sk1 @ ( sk3 @ ( sk2 @ perp ) ) ) )
& ( sk4 @ ( sk2 @ ( sk3 @ ( sk1 @ perp ) ) ) )
& ( sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ perp ) ) ) ) ),
inference(cnf,[status(esa)],[98]) ).
thf(124,plain,
sk6 @ ( sk14 @ ( sk4 @ ( sk2 @ perp ) ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(108,plain,
~ ( sk6 @ ( sk7 @ ( sk5 @ ( sk8 @ perp ) ) ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(735,plain,
( ( ( sk6 @ ( sk7 @ ( sk5 @ ( sk8 @ perp ) ) ) )
!= ( sk6 @ ( sk14 @ ( sk4 @ ( sk2 @ perp ) ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[124,108]) ).
thf(736,plain,
( ( sk6 @ ( sk7 @ ( sk5 @ ( sk8 @ perp ) ) ) )
!= ( sk6 @ ( sk14 @ ( sk4 @ ( sk2 @ perp ) ) ) ) ),
inference(simp,[status(thm)],[735]) ).
thf(737,plain,
( ( sk6 != sk6 )
| ( sk14 != sk7 )
| ( sk5 != sk4 )
| ( sk8 != sk2 ) ),
inference(simp,[status(thm)],[736]) ).
thf(738,plain,
( ( sk14 != sk7 )
| ( sk5 != sk4 )
| ( sk8 != sk2 ) ),
inference(simp,[status(thm)],[737]) ).
thf(8,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i,I: $i] :
( ( ( I @ ( H @ ( G @ ( F @ ( E @ ( D @ simtri ) ) ) ) ) )
& ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ simtri ) ) ) ) ) ) )
=> ( I @ ( H @ ( G @ ( C @ ( B @ ( A @ simtri ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD34) ).
thf(138,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i,I: $i] :
( ( ( I @ ( H @ ( G @ ( F @ ( E @ ( D @ simtri ) ) ) ) ) )
& ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ simtri ) ) ) ) ) ) )
=> ( I @ ( H @ ( G @ ( C @ ( B @ ( A @ simtri ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(101,plain,
sk7 @ ( sk16 @ ( sk3 @ ( sk1 @ perp ) ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(115,plain,
sk3 @ ( sk2 @ ( sk19 @ midp ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(74,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
? [E: $i] :
( ( C @ ( B @ ( A @ ( D @ circle ) ) ) )
=> ( D @ ( A @ ( A @ ( E @ perp ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleX11) ).
thf(308,plain,
! [A: $i,B: $i,C: $i,D: $i] :
? [E: $i] :
( ( C @ ( B @ ( A @ ( D @ circle ) ) ) )
=> ( D @ ( A @ ( A @ ( E @ perp ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[74]) ).
thf(120,plain,
sk8 @ ( sk18 @ ( sk4 @ ( sk2 @ perp ) ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(96,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( ( F @ ( E @ ( D @ ( C @ perp ) ) ) )
& ( D @ ( C @ ( B @ ( A @ perp ) ) ) ) )
=> ( F @ ( E @ ( B @ ( A @ para ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD9) ).
thf(379,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( ( F @ ( E @ ( D @ ( C @ perp ) ) ) )
& ( D @ ( C @ ( B @ ( A @ perp ) ) ) ) )
=> ( F @ ( E @ ( B @ ( A @ para ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[96]) ).
thf(34,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( D @ ( B @ ( E @ coll ) ) )
& ( C @ ( A @ ( E @ coll ) ) )
& ( D @ ( C @ ( B @ ( A @ para ) ) ) ) )
=> ( D @ ( B @ ( B @ ( E @ ( C @ ( A @ ( A @ ( E @ eqratio ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD65) ).
thf(202,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( D @ ( B @ ( E @ coll ) ) )
& ( C @ ( A @ ( E @ coll ) ) )
& ( D @ ( C @ ( B @ ( A @ para ) ) ) ) )
=> ( D @ ( B @ ( B @ ( E @ ( C @ ( A @ ( A @ ( E @ eqratio ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(10,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( E @ ( F @ ( D @ ( B @ ( C @ ( A @ simtri ) ) ) ) ) )
=> ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ simtri ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD31) ).
thf(142,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( E @ ( F @ ( D @ ( B @ ( C @ ( A @ simtri ) ) ) ) ) )
=> ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ simtri ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(15,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ coll ) ) )
=> ( C @ ( A @ ( B @ coll ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD2) ).
thf(153,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ coll ) ) )
=> ( C @ ( A @ ( B @ coll ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(27,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ eqratio ) ) ) ) ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ ( H @ ( G @ ( F @ ( E @ eqratio ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD28) ).
thf(184,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ eqratio ) ) ) ) ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ ( H @ ( G @ ( F @ ( E @ eqratio ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(94,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( C @ ( A @ ( E @ coll ) ) )
& ( C @ ( B @ ( E @ ( D @ para ) ) ) )
& ( B @ ( A @ ( D @ midp ) ) ) )
=> ( C @ ( A @ ( E @ midp ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD45) ).
thf(372,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( C @ ( A @ ( E @ coll ) ) )
& ( C @ ( B @ ( E @ ( D @ para ) ) ) )
& ( B @ ( A @ ( D @ midp ) ) ) )
=> ( C @ ( A @ ( E @ midp ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[94]) ).
thf(110,plain,
sk3 @ ( sk4 @ ( sk17 @ midp ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(31,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) )
=> ( F @ ( E @ ( H @ ( G @ ( B @ ( A @ ( D @ ( C @ eqangle ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD19) ).
thf(196,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) )
=> ( F @ ( E @ ( H @ ( G @ ( B @ ( A @ ( D @ ( C @ eqangle ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(125,plain,
sk4 @ ( sk3 @ ( sk2 @ ( sk1 @ perp ) ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(84,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( C @ ( B @ ( E @ midp ) ) )
& ( C @ ( B @ ( A @ ( D @ circle ) ) ) ) )
=> ( E @ ( D @ ( B @ ( D @ ( C @ ( A @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD50) ).
thf(344,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( C @ ( B @ ( E @ midp ) ) )
& ( C @ ( B @ ( A @ ( D @ circle ) ) ) ) )
=> ( E @ ( D @ ( B @ ( D @ ( C @ ( A @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[84]) ).
thf(81,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i] :
? [H: $i] :
( ( ( B @ ( A @ ( D @ coll ) ) )
& ( B @ ( A @ ( C @ coll ) ) )
& ( D @ ( C @ ( F @ midp ) ) )
& ( B @ ( A @ ( E @ midp ) ) ) )
=> ( G @ ( A @ ( H @ midp ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleX7) ).
thf(336,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i] :
? [H: $i] :
( ( ( B @ ( A @ ( D @ coll ) ) )
& ( B @ ( A @ ( C @ coll ) ) )
& ( D @ ( C @ ( F @ midp ) ) )
& ( B @ ( A @ ( E @ midp ) ) ) )
=> ( G @ ( A @ ( H @ midp ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[81]) ).
thf(337,plain,
! [A: $i] :
( ? [B: $i] :
( ? [C: $i,D: $i] :
( ( B @ ( A @ ( D @ coll ) ) )
& ( B @ ( A @ ( C @ coll ) ) )
& ? [E: $i] : ( D @ ( C @ ( E @ midp ) ) ) )
& ? [C: $i] : ( B @ ( A @ ( C @ midp ) ) ) )
=> ! [B: $i] :
? [C: $i] : ( B @ ( A @ ( C @ midp ) ) ) ),
inference(miniscope,[status(thm)],[336]) ).
thf(338,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( G @ ( A @ ( A @ ( G @ sk36 ) @ midp ) ) )
| ~ ( B @ ( A @ ( E @ coll ) ) )
| ~ ( B @ ( A @ ( D @ coll ) ) )
| ~ ( E @ ( D @ ( F @ midp ) ) )
| ~ ( B @ ( A @ ( C @ midp ) ) ) ),
inference(cnf,[status(esa)],[337]) ).
thf(387,plain,
! [N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( G @ ( A @ ( A @ ( G @ sk36 ) @ midp ) ) )
!= ( I @ ( H @ ( J @ midp ) ) ) )
| ( N @ ( H @ ( H @ ( N @ sk36 ) @ midp ) ) )
| ~ ( I @ ( H @ ( L @ coll ) ) )
| ~ ( I @ ( H @ ( K @ coll ) ) )
| ~ ( L @ ( K @ ( M @ midp ) ) )
| ~ $true
| ~ ( B @ ( A @ ( E @ coll ) ) )
| ~ ( B @ ( A @ ( D @ coll ) ) )
| ~ ( E @ ( D @ ( F @ midp ) ) )
| ~ ( B @ ( A @ ( C @ midp ) ) ) ),
inference(paramod_ordered,[status(thm)],[338,338]) ).
thf(388,plain,
! [N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( G @ ( A @ ( A @ ( G @ sk36 ) @ midp ) ) )
!= ( I @ ( H @ ( J @ midp ) ) ) )
| ( N @ ( H @ ( H @ ( N @ sk36 ) @ midp ) ) )
| ~ ( I @ ( H @ ( L @ coll ) ) )
| ~ ( I @ ( H @ ( K @ coll ) ) )
| ~ ( L @ ( K @ ( M @ midp ) ) )
| ~ ( B @ ( A @ ( E @ coll ) ) )
| ~ ( B @ ( A @ ( D @ coll ) ) )
| ~ ( E @ ( D @ ( F @ midp ) ) )
| ~ ( B @ ( A @ ( C @ midp ) ) ) ),
inference(simp,[status(thm)],[387]) ).
thf(389,plain,
! [K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( I @ ( K @ ( K @ ( I @ sk36 ) @ midp ) ) )
| ~ ( J @ ( K @ ( G @ coll ) ) )
| ~ ( J @ ( K @ ( F @ coll ) ) )
| ~ ( G @ ( F @ ( H @ midp ) ) )
| ~ ( A @ ( K @ ( D @ coll ) ) )
| ~ ( A @ ( K @ ( C @ coll ) ) )
| ~ ( D @ ( C @ ( E @ midp ) ) )
| ~ ( A @ ( K @ ( B @ midp ) ) ) ),
inference(pattern_uni,[status(thm)],[388:[bind(A,$thf( P )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( E )),bind(F,$thf( F )),bind(G,$thf( O )),bind(H,$thf( P )),bind(I,$thf( O )),bind(J,$thf( P @ ( O @ sk36 ) ))]]) ).
thf(416,plain,
! [K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( I @ ( K @ ( K @ ( I @ sk36 ) @ midp ) ) )
| ~ ( J @ ( K @ ( G @ coll ) ) )
| ~ ( J @ ( K @ ( F @ coll ) ) )
| ~ ( G @ ( F @ ( H @ midp ) ) )
| ~ ( A @ ( K @ ( D @ coll ) ) )
| ~ ( A @ ( K @ ( C @ coll ) ) )
| ~ ( D @ ( C @ ( E @ midp ) ) )
| ~ ( A @ ( K @ ( B @ midp ) ) ) ),
inference(simp,[status(thm)],[389]) ).
thf(45,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( ( F @ ( E @ ( D @ ( C @ para ) ) ) )
& ( D @ ( C @ ( B @ ( A @ para ) ) ) ) )
=> ( F @ ( E @ ( B @ ( A @ para ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD6) ).
thf(228,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( ( F @ ( E @ ( D @ ( C @ para ) ) ) )
& ( D @ ( C @ ( B @ ( A @ para ) ) ) ) )
=> ( F @ ( E @ ( B @ ( A @ para ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(39,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( A @ ( B @ ( A @ para ) ) ) )
=> ( C @ ( B @ ( A @ coll ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD66) ).
thf(216,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( A @ ( B @ ( A @ para ) ) ) )
=> ( C @ ( B @ ( A @ coll ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(25,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ cyclic ) ) ) )
=> ( D @ ( C @ ( A @ ( B @ cyclic ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD16) ).
thf(179,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ cyclic ) ) ) )
=> ( D @ ( C @ ( A @ ( B @ cyclic ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(38,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
? [G: $i] :
( ( ( B @ ( A @ ( F @ coll ) ) )
& ( D @ ( B @ ( E @ coll ) ) )
& ( C @ ( A @ ( E @ coll ) ) )
& ( D @ ( C @ ( B @ ( A @ para ) ) ) ) )
=> ( ( D @ ( C @ ( G @ coll ) ) )
& ( G @ ( F @ ( E @ coll ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleX18) ).
thf(211,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
? [G: $i] :
( ( ( B @ ( A @ ( F @ coll ) ) )
& ( D @ ( B @ ( E @ coll ) ) )
& ( C @ ( A @ ( E @ coll ) ) )
& ( D @ ( C @ ( B @ ( A @ para ) ) ) ) )
=> ( ( D @ ( C @ ( G @ coll ) ) )
& ( G @ ( F @ ( E @ coll ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(106,plain,
sk5 @ ( sk11 @ ( sk3 @ ( sk2 @ perp ) ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(121,plain,
sk7 @ ( sk15 @ ( sk4 @ ( sk1 @ perp ) ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(86,axiom,
! [A: $i,B: $i,C: $i] :
? [D: $i] :
( ( ( B @ ( C @ ( C @ ( A @ perp ) ) ) )
& ( B @ ( C @ ( A @ ( C @ cong ) ) ) ) )
=> ( ( D @ ( C @ ( A @ ( C @ cong ) ) ) )
& ( D @ ( C @ ( A @ coll ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleX17) ).
thf(348,plain,
! [A: $i,B: $i,C: $i] :
? [D: $i] :
( ( ( B @ ( C @ ( C @ ( A @ perp ) ) ) )
& ( B @ ( C @ ( A @ ( C @ cong ) ) ) ) )
=> ( ( D @ ( C @ ( A @ ( C @ cong ) ) ) )
& ( D @ ( C @ ( A @ coll ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[86]) ).
thf(87,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
? [G: $i] :
( ( ( D @ ( C @ ( F @ midp ) ) )
& ( B @ ( A @ ( E @ midp ) ) ) )
=> ( ( C @ ( A @ ( F @ ( G @ para ) ) ) )
& ( D @ ( B @ ( E @ ( G @ para ) ) ) )
& ( D @ ( A @ ( G @ midp ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleX6) ).
thf(353,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
? [G: $i] :
( ( ( D @ ( C @ ( F @ midp ) ) )
& ( B @ ( A @ ( E @ midp ) ) ) )
=> ( ( C @ ( A @ ( F @ ( G @ para ) ) ) )
& ( D @ ( B @ ( E @ ( G @ para ) ) ) )
& ( D @ ( A @ ( G @ midp ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[87]) ).
thf(65,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ~ ( D @ ( C @ ( B @ ( A @ para ) ) ) )
& ( B @ ( A @ ( D @ ( C @ ( D @ ( C @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ perp ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD71) ).
thf(280,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ~ ( D @ ( C @ ( B @ ( A @ para ) ) ) )
& ( B @ ( A @ ( D @ ( C @ ( D @ ( C @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ perp ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[65]) ).
thf(100,plain,
sk8 @ ( sk20 @ ( sk3 @ ( sk4 @ perp ) ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(451,plain,
( ( ( sk6 @ ( sk7 @ ( sk5 @ ( sk8 @ perp ) ) ) )
!= ( sk8 @ ( sk20 @ ( sk3 @ ( sk4 @ perp ) ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[100,108]) ).
thf(452,plain,
( ( sk6 @ ( sk7 @ ( sk5 @ ( sk8 @ perp ) ) ) )
!= ( sk8 @ ( sk20 @ ( sk3 @ ( sk4 @ perp ) ) ) ) ),
inference(simp,[status(thm)],[451]) ).
thf(453,plain,
( ( sk8 != sk6 )
| ( sk20 != sk7 )
| ( sk5 != sk3 )
| ( sk8 != sk4 ) ),
inference(simp,[status(thm)],[452]) ).
thf(5,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( C @ ( B @ ( A @ ( F @ ( E @ ( D @ contri ) ) ) ) ) )
=> ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ contri ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD37) ).
thf(132,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( C @ ( B @ ( A @ ( F @ ( E @ ( D @ contri ) ) ) ) ) )
=> ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ contri ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(36,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i,I: $i,J: $i,K: $i,L: $i] :
( ( ( H @ ( G @ ( F @ ( E @ ( L @ ( K @ ( J @ ( I @ eqratio ) ) ) ) ) ) ) )
& ( L @ ( K @ ( J @ ( I @ ( D @ ( C @ ( B @ ( A @ eqratio ) ) ) ) ) ) ) ) )
=> ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ eqratio ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD30) ).
thf(206,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i,I: $i,J: $i,K: $i,L: $i] :
( ( ( H @ ( G @ ( F @ ( E @ ( L @ ( K @ ( J @ ( I @ eqratio ) ) ) ) ) ) ) )
& ( L @ ( K @ ( J @ ( I @ ( D @ ( C @ ( B @ ( A @ eqratio ) ) ) ) ) ) ) ) )
=> ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ eqratio ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(116,plain,
sk3 @ ( sk1 @ ( sk16 @ midp ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(48,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ contri ) ) ) ) ) )
=> ( E @ ( D @ ( B @ ( A @ cong ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD62) ).
thf(243,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ contri ) ) ) ) ) )
=> ( E @ ( D @ ( B @ ( A @ cong ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).
thf(68,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
? [F: $i] :
( ( ( E @ ( B @ ( B @ ( A @ perp ) ) ) )
& ( D @ ( E @ ( C @ ( E @ cong ) ) ) ) )
=> ( ( F @ ( B @ ( C @ ( B @ cong ) ) ) )
& ( B @ ( A @ ( C @ ( F @ para ) ) ) )
& ( F @ ( E @ ( C @ ( E @ cong ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleX9) ).
thf(292,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
? [F: $i] :
( ( ( E @ ( B @ ( B @ ( A @ perp ) ) ) )
& ( D @ ( E @ ( C @ ( E @ cong ) ) ) ) )
=> ( ( F @ ( B @ ( C @ ( B @ cong ) ) ) )
& ( B @ ( A @ ( C @ ( F @ para ) ) ) )
& ( F @ ( E @ ( C @ ( E @ cong ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[68]) ).
thf(50,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ simtri ) ) ) ) ) )
=> ( F @ ( D @ ( E @ ( D @ ( C @ ( A @ ( B @ ( A @ eqratio ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD59) ).
thf(248,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ simtri ) ) ) ) ) )
=> ( F @ ( D @ ( E @ ( D @ ( C @ ( A @ ( B @ ( A @ eqratio ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).
thf(117,plain,
sk4 @ ( sk1 @ ( sk3 @ ( sk2 @ perp ) ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(102,plain,
sk6 @ ( sk13 @ ( sk4 @ ( sk1 @ perp ) ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(41,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ para ) ) ) )
=> ( C @ ( D @ ( B @ ( A @ para ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD4) ).
thf(220,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ para ) ) ) )
=> ( C @ ( D @ ( B @ ( A @ para ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(91,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( E @ ( A @ ( A @ ( D @ perp ) ) ) )
& ( C @ ( B @ ( A @ ( D @ circle ) ) ) ) )
=> ( B @ ( C @ ( A @ ( C @ ( B @ ( A @ ( E @ ( A @ eqangle ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD48) ).
thf(366,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( E @ ( A @ ( A @ ( D @ perp ) ) ) )
& ( C @ ( B @ ( A @ ( D @ circle ) ) ) ) )
=> ( B @ ( C @ ( A @ ( C @ ( B @ ( A @ ( E @ ( A @ eqangle ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[91]) ).
thf(80,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ midp ) ) )
=> ( C @ ( A @ ( B @ ( A @ cong ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD68) ).
thf(334,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ midp ) ) )
=> ( C @ ( A @ ( B @ ( A @ cong ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[80]) ).
thf(71,axiom,
! [A: $i,B: $i,C: $i] :
( ( A @ ( B @ ( C @ midp ) ) )
=> ( B @ ( A @ ( C @ midp ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD11) ).
thf(302,plain,
! [A: $i,B: $i,C: $i] :
( ( A @ ( B @ ( C @ midp ) ) )
=> ( B @ ( A @ ( C @ midp ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[71]) ).
thf(56,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( B @ ( D @ ( C @ coll ) ) )
& ( B @ ( D @ ( A @ ( D @ ( B @ ( C @ ( A @ ( C @ eqangle ) ) ) ) ) ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ cyclic ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD42b) ).
thf(260,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( B @ ( D @ ( C @ coll ) ) )
& ( B @ ( D @ ( A @ ( D @ ( B @ ( C @ ( A @ ( C @ eqangle ) ) ) ) ) ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ cyclic ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[56]) ).
thf(18,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( ( H @ ( G @ ( F @ ( E @ cong ) ) ) )
& ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ eqratio ) ) ) ) ) ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ cong ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD75) ).
thf(160,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( ( H @ ( G @ ( F @ ( E @ cong ) ) ) )
& ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ eqratio ) ) ) ) ) ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ cong ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(63,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ midp ) ) )
=> ( C @ ( B @ ( A @ coll ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD69) ).
thf(275,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ ( A @ midp ) ) )
=> ( C @ ( B @ ( A @ coll ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[63]) ).
thf(20,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ ( H @ ( G @ ( F @ ( E @ eqangle ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD20) ).
thf(165,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ ( H @ ( G @ ( F @ ( E @ eqangle ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(52,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ cong ) ) ) )
=> ( C @ ( D @ ( B @ ( A @ cong ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD23) ).
thf(252,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ cong ) ) ) )
=> ( C @ ( D @ ( B @ ( A @ cong ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[52]) ).
thf(89,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ ( A @ coll ) ) )
& ( C @ ( A @ ( B @ ( A @ cong ) ) ) ) )
=> ( C @ ( B @ ( A @ midp ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD67) ).
thf(361,plain,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ ( A @ coll ) ) )
& ( C @ ( A @ ( B @ ( A @ cong ) ) ) ) )
=> ( C @ ( B @ ( A @ midp ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[89]) ).
thf(43,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ eqratio ) ) ) ) ) ) ) )
=> ( H @ ( G @ ( D @ ( C @ ( F @ ( E @ ( B @ ( A @ eqratio ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD29) ).
thf(224,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ eqratio ) ) ) ) ) ) ) )
=> ( H @ ( G @ ( D @ ( C @ ( F @ ( E @ ( B @ ( A @ eqratio ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[43]) ).
thf(82,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( ( F @ ( E @ ( D @ ( C @ perp ) ) ) )
& ( D @ ( C @ ( B @ ( A @ para ) ) ) ) )
=> ( F @ ( E @ ( B @ ( A @ perp ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD10) ).
thf(339,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( ( F @ ( E @ ( D @ ( C @ perp ) ) ) )
& ( D @ ( C @ ( B @ ( A @ para ) ) ) ) )
=> ( F @ ( E @ ( B @ ( A @ perp ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[82]) ).
thf(30,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( D @ ( C @ ( B @ ( A @ para ) ) ) )
=> ( F @ ( E @ ( D @ ( C @ ( F @ ( E @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD40) ).
thf(193,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( D @ ( C @ ( B @ ( A @ para ) ) ) )
=> ( F @ ( E @ ( D @ ( C @ ( F @ ( E @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(109,plain,
sk7 @ ( sk17 @ ( sk3 @ ( sk4 @ perp ) ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(54,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ cyclic ) ) ) )
=> ( D @ ( B @ ( C @ ( A @ cyclic ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD15) ).
thf(256,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ cyclic ) ) ) )
=> ( D @ ( B @ ( C @ ( A @ cyclic ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[54]) ).
thf(6,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i,I: $i] :
( ( ( I @ ( H @ ( G @ ( F @ ( E @ ( D @ contri ) ) ) ) ) )
& ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ contri ) ) ) ) ) ) )
=> ( I @ ( H @ ( G @ ( C @ ( B @ ( A @ contri ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD38) ).
thf(134,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i,I: $i] :
( ( ( I @ ( H @ ( G @ ( F @ ( E @ ( D @ contri ) ) ) ) ) )
& ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ contri ) ) ) ) ) ) )
=> ( I @ ( H @ ( G @ ( C @ ( B @ ( A @ contri ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(3,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( F @ ( D @ ( E @ ( C @ ( A @ ( B @ contri ) ) ) ) ) )
=> ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ contri ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD36) ).
thf(128,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( F @ ( D @ ( E @ ( C @ ( A @ ( B @ contri ) ) ) ) ) )
=> ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ contri ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(105,plain,
sk3 @ ( sk2 @ ( sk11 @ midp ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(59,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( C @ ( A @ ( E @ midp ) ) )
& ( B @ ( A @ ( D @ midp ) ) ) )
=> ( C @ ( B @ ( E @ ( D @ para ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD44) ).
thf(266,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( C @ ( A @ ( E @ midp ) ) )
& ( B @ ( A @ ( D @ midp ) ) ) )
=> ( C @ ( B @ ( E @ ( D @ para ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[59]) ).
thf(75,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
? [E: $i,F: $i] :
( ( ( C @ ( A @ ( D @ ( B @ perp ) ) ) )
& ( C @ ( B @ ( D @ ( A @ perp ) ) ) ) )
=> ( ( A @ ( C @ ( F @ ( B @ perp ) ) ) )
& ( A @ ( C @ ( F @ coll ) ) )
& ( B @ ( C @ ( E @ ( A @ perp ) ) ) )
& ( B @ ( C @ ( E @ coll ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleX10) ).
thf(311,plain,
! [A: $i,B: $i,C: $i,D: $i] :
? [E: $i,F: $i] :
( ( ( C @ ( A @ ( D @ ( B @ perp ) ) ) )
& ( C @ ( B @ ( D @ ( A @ perp ) ) ) ) )
=> ( ( A @ ( C @ ( F @ ( B @ perp ) ) ) )
& ( A @ ( C @ ( F @ coll ) ) )
& ( B @ ( C @ ( E @ ( A @ perp ) ) ) )
& ( B @ ( C @ ( E @ coll ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[75]) ).
thf(69,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( ( D @ ( C @ ( F @ midp ) ) )
& ( B @ ( A @ ( E @ midp ) ) ) )
=> ( D @ ( C @ ( C @ ( F @ ( B @ ( A @ ( A @ ( E @ eqratio ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD70) ).
thf(298,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( ( D @ ( C @ ( F @ midp ) ) )
& ( B @ ( A @ ( E @ midp ) ) ) )
=> ( D @ ( C @ ( C @ ( F @ ( B @ ( A @ ( A @ ( E @ eqratio ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[69]) ).
thf(13,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ eqratio ) ) ) ) ) ) ) )
=> ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( A @ ( B @ eqratio ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD26) ).
thf(148,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ eqratio ) ) ) ) ) ) ) )
=> ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( A @ ( B @ eqratio ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(58,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( B @ ( C @ ( A @ ( C @ ( B @ ( A @ ( E @ ( A @ eqangle ) ) ) ) ) ) ) )
& ( C @ ( B @ ( A @ ( D @ circle ) ) ) ) )
=> ( E @ ( A @ ( A @ ( D @ perp ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD49) ).
thf(264,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( B @ ( C @ ( A @ ( C @ ( B @ ( A @ ( E @ ( A @ eqangle ) ) ) ) ) ) ) )
& ( C @ ( B @ ( A @ ( D @ circle ) ) ) ) )
=> ( E @ ( A @ ( A @ ( D @ perp ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[58]) ).
thf(24,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( D @ ( E @ ( A @ ( E @ cong ) ) ) )
& ( C @ ( E @ ( A @ ( E @ cong ) ) ) )
& ( B @ ( E @ ( A @ ( E @ cong ) ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ cyclic ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD13) ).
thf(176,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( D @ ( E @ ( A @ ( E @ cong ) ) ) )
& ( C @ ( E @ ( A @ ( E @ cong ) ) ) )
& ( B @ ( E @ ( A @ ( E @ cong ) ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ cyclic ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(29,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ cong ) ) ) )
=> ( B @ ( A @ ( D @ ( C @ cong ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD24) ).
thf(191,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ cong ) ) ) )
=> ( B @ ( A @ ( D @ ( C @ cong ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(118,plain,
sk5 @ ( sk10 @ ( sk3 @ ( sk1 @ perp ) ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(35,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ eqratio ) ) ) ) ) ) ) )
=> ( F @ ( E @ ( H @ ( G @ ( B @ ( A @ ( D @ ( C @ eqratio ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD27) ).
thf(204,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ eqratio ) ) ) ) ) ) ) )
=> ( F @ ( E @ ( H @ ( G @ ( B @ ( A @ ( D @ ( C @ eqratio ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(11,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( F @ ( D @ ( E @ ( C @ ( A @ ( B @ simtri ) ) ) ) ) )
=> ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ simtri ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD32) ).
thf(144,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( F @ ( D @ ( E @ ( C @ ( A @ ( B @ simtri ) ) ) ) ) )
=> ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ simtri ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(111,plain,
sk6 @ ( sk12 @ ( sk2 @ ( sk1 @ perp ) ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(710,plain,
( ( ( sk6 @ ( sk7 @ ( sk5 @ ( sk8 @ perp ) ) ) )
!= ( sk6 @ ( sk12 @ ( sk2 @ ( sk1 @ perp ) ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[111,108]) ).
thf(711,plain,
( ( sk6 @ ( sk7 @ ( sk5 @ ( sk8 @ perp ) ) ) )
!= ( sk6 @ ( sk12 @ ( sk2 @ ( sk1 @ perp ) ) ) ) ),
inference(simp,[status(thm)],[710]) ).
thf(712,plain,
( ( sk6 != sk6 )
| ( sk12 != sk7 )
| ( sk5 != sk2 )
| ( sk8 != sk1 ) ),
inference(simp,[status(thm)],[711]) ).
thf(713,plain,
( ( sk12 != sk7 )
| ( sk5 != sk2 )
| ( sk8 != sk1 ) ),
inference(simp,[status(thm)],[712]) ).
thf(26,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( F @ ( E @ ( D @ ( C @ ( F @ ( E @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ para ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD39) ).
thf(181,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( F @ ( E @ ( D @ ( C @ ( F @ ( E @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ para ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(113,plain,
sk3 @ ( sk4 @ ( sk20 @ midp ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(46,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
? [G: $i,H: $i] :
( ( ( E != F )
& ( B @ ( F @ ( A @ ( F @ cong ) ) ) )
& ( D @ ( E @ ( A @ ( E @ cong ) ) ) )
& ( C @ ( B @ ( A @ ( E @ circle ) ) ) ) )
=> ( ( A @ ( F @ ( F @ ( H @ cong ) ) ) )
& ( D @ ( B @ ( H @ coll ) ) )
& ( A @ ( F @ ( F @ ( G @ cong ) ) ) )
& ( C @ ( A @ ( G @ coll ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleX12) ).
thf(230,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
? [G: $i,H: $i] :
( ( ( E != F )
& ( B @ ( F @ ( A @ ( F @ cong ) ) ) )
& ( D @ ( E @ ( A @ ( E @ cong ) ) ) )
& ( C @ ( B @ ( A @ ( E @ circle ) ) ) ) )
=> ( ( A @ ( F @ ( F @ ( H @ cong ) ) ) )
& ( D @ ( B @ ( H @ coll ) ) )
& ( A @ ( F @ ( F @ ( G @ cong ) ) ) )
& ( C @ ( A @ ( G @ coll ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(76,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
? [F: $i] :
( ( ( E @ ( D @ ( B @ coll ) ) )
& ( B @ ( C @ ( C @ ( A @ perp ) ) ) ) )
=> ( ( E @ ( D @ ( A @ ( F @ perp ) ) ) )
& ( E @ ( D @ ( F @ coll ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleX15) ).
thf(318,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
? [F: $i] :
( ( ( E @ ( D @ ( B @ coll ) ) )
& ( B @ ( C @ ( C @ ( A @ perp ) ) ) ) )
=> ( ( E @ ( D @ ( A @ ( F @ perp ) ) ) )
& ( E @ ( D @ ( F @ coll ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[76]) ).
thf(61,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ perp ) ) ) )
=> ( C @ ( D @ ( B @ ( A @ perp ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD7) ).
thf(271,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ perp ) ) ) )
=> ( C @ ( D @ ( B @ ( A @ perp ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[61]) ).
thf(103,plain,
sk2 @ ( sk1 @ ( sk9 @ midp ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(77,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( C @ ( A @ ( D @ coll ) ) )
& ( C @ ( B @ ( A @ ( D @ circle ) ) ) ) )
=> ( C @ ( B @ ( B @ ( A @ perp ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD53) ).
thf(323,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( C @ ( A @ ( D @ coll ) ) )
& ( C @ ( B @ ( A @ ( D @ circle ) ) ) ) )
=> ( C @ ( B @ ( B @ ( A @ perp ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[77]) ).
thf(9,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( ( E @ ( D @ ( B @ ( A @ cong ) ) ) )
& ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ simtri ) ) ) ) ) ) )
=> ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ contri ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD61) ).
thf(140,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( ( E @ ( D @ ( B @ ( A @ cong ) ) ) )
& ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ simtri ) ) ) ) ) ) )
=> ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ contri ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(16,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( ( H @ ( G @ ( F @ ( E @ para ) ) ) )
& ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ para ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD73) ).
thf(155,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( ( H @ ( G @ ( F @ ( E @ para ) ) ) )
& ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ para ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(32,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( C @ ( A @ ( C @ cong ) ) ) )
=> ( B @ ( C @ ( B @ ( A @ ( B @ ( A @ ( A @ ( C @ eqangle ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD46) ).
thf(198,plain,
! [A: $i,B: $i,C: $i] :
( ( B @ ( C @ ( A @ ( C @ cong ) ) ) )
=> ( B @ ( C @ ( B @ ( A @ ( B @ ( A @ ( A @ ( C @ eqangle ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(4,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( E @ ( F @ ( D @ ( B @ ( C @ ( A @ contri ) ) ) ) ) )
=> ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ contri ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD35) ).
thf(130,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( E @ ( F @ ( D @ ( B @ ( C @ ( A @ contri ) ) ) ) ) )
=> ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ contri ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(73,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( C @ ( B @ ( D @ ( A @ para ) ) ) )
& ( D @ ( B @ ( C @ ( A @ para ) ) ) )
& ( B @ ( A @ ( E @ midp ) ) ) )
=> ( D @ ( C @ ( E @ midp ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD64) ).
thf(306,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( C @ ( B @ ( D @ ( A @ para ) ) ) )
& ( D @ ( B @ ( C @ ( A @ para ) ) ) )
& ( B @ ( A @ ( E @ midp ) ) ) )
=> ( D @ ( C @ ( E @ midp ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[73]) ).
thf(44,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( D @ ( C @ ( B @ ( A @ para ) ) ) )
& ( D @ ( C @ ( B @ ( A @ cyclic ) ) ) ) )
=> ( B @ ( C @ ( D @ ( C @ ( D @ ( C @ ( D @ ( A @ eqangle ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD54) ).
thf(226,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( D @ ( C @ ( B @ ( A @ para ) ) ) )
& ( D @ ( C @ ( B @ ( A @ cyclic ) ) ) ) )
=> ( B @ ( C @ ( D @ ( C @ ( D @ ( C @ ( D @ ( A @ eqangle ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(47,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( E @ ( C @ ( B @ ( A @ cyclic ) ) ) )
& ( D @ ( C @ ( B @ ( A @ cyclic ) ) ) ) )
=> ( E @ ( D @ ( C @ ( B @ cyclic ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD17) ).
thf(241,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( E @ ( C @ ( B @ ( A @ cyclic ) ) ) )
& ( D @ ( C @ ( B @ ( A @ cyclic ) ) ) ) )
=> ( E @ ( D @ ( C @ ( B @ cyclic ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).
thf(21,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ cyclic ) ) ) )
=> ( B @ ( D @ ( A @ ( D @ ( B @ ( C @ ( A @ ( C @ eqangle ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD41) ).
thf(167,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ cyclic ) ) ) )
=> ( B @ ( D @ ( A @ ( D @ ( B @ ( C @ ( A @ ( C @ eqangle ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(95,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i] :
? [H: $i] :
( ( ( F @ ( E @ ( D @ coll ) ) )
& ( E @ ( B @ ( D @ ( A @ para ) ) ) )
& ( G @ ( F @ ( D @ ( A @ para ) ) ) )
& ( B @ ( A @ ( G @ midp ) ) ) )
=> ( ( F @ ( G @ ( H @ coll ) ) )
& ( E @ ( A @ ( H @ coll ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleX8) ).
thf(374,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
? [G: $i] :
( ( ( E @ ( D @ ( C @ coll ) ) )
& ( D @ ( B @ ( C @ ( A @ para ) ) ) )
& ( F @ ( E @ ( C @ ( A @ para ) ) ) )
& ( B @ ( A @ ( F @ midp ) ) ) )
=> ( ( E @ ( F @ ( G @ coll ) ) )
& ( D @ ( A @ ( G @ coll ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[95]) ).
thf(37,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( ( F @ ( E @ ( D @ ( C @ cong ) ) ) )
& ( D @ ( C @ ( B @ ( A @ cong ) ) ) ) )
=> ( F @ ( E @ ( B @ ( A @ cong ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD25) ).
thf(209,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( ( F @ ( E @ ( D @ ( C @ cong ) ) ) )
& ( D @ ( C @ ( B @ ( A @ cong ) ) ) ) )
=> ( F @ ( E @ ( B @ ( A @ cong ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(112,plain,
sk4 @ ( sk2 @ ( sk18 @ midp ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(123,plain,
sk4 @ ( sk1 @ ( sk13 @ midp ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(66,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
? [E: $i] :
( ( ( B @ ( C @ ( A @ ( C @ cong ) ) ) )
& ( B @ ( A @ ( D @ ( C @ perp ) ) ) ) )
=> ( ( D @ ( C @ ( E @ coll ) ) )
& ( E @ ( A @ ( B @ coll ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleX4) ).
thf(282,plain,
! [A: $i,B: $i,C: $i,D: $i] :
? [E: $i] :
( ( ( B @ ( C @ ( A @ ( C @ cong ) ) ) )
& ( B @ ( A @ ( D @ ( C @ perp ) ) ) ) )
=> ( ( D @ ( C @ ( E @ coll ) ) )
& ( E @ ( A @ ( B @ coll ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[66]) ).
thf(14,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( ( E @ ( F @ ( D @ ( F @ ( B @ ( C @ ( A @ ( C @ eqangle ) ) ) ) ) ) ) )
& ( F @ ( C @ ( B @ ( A @ cyclic ) ) ) )
& ( E @ ( C @ ( B @ ( A @ cyclic ) ) ) )
& ( D @ ( C @ ( B @ ( A @ cyclic ) ) ) ) )
=> ( E @ ( D @ ( B @ ( A @ cong ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD43) ).
thf(150,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( ( E @ ( F @ ( D @ ( F @ ( B @ ( C @ ( A @ ( C @ eqangle ) ) ) ) ) ) ) )
& ( F @ ( C @ ( B @ ( A @ cyclic ) ) ) )
& ( E @ ( C @ ( B @ ( A @ cyclic ) ) ) )
& ( D @ ( C @ ( B @ ( A @ cyclic ) ) ) ) )
=> ( E @ ( D @ ( B @ ( A @ cong ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(79,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( ( H @ ( G @ ( F @ ( E @ perp ) ) ) )
& ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ perp ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD74) ).
thf(331,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( ( H @ ( G @ ( F @ ( E @ perp ) ) ) )
& ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ perp ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[79]) ).
thf(93,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( E @ ( D @ ( B @ ( D @ ( C @ ( A @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) )
& ( C @ ( B @ ( E @ coll ) ) )
& ( C @ ( B @ ( A @ ( D @ circle ) ) ) ) )
=> ( C @ ( B @ ( E @ midp ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD51) ).
thf(370,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( E @ ( D @ ( B @ ( D @ ( C @ ( A @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) )
& ( C @ ( B @ ( E @ coll ) ) )
& ( C @ ( B @ ( A @ ( D @ circle ) ) ) ) )
=> ( C @ ( B @ ( E @ midp ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[93]) ).
thf(127,plain,
sk4 @ ( sk1 @ ( sk15 @ midp ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(88,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( D @ ( B @ ( D @ ( A @ cong ) ) ) )
& ( C @ ( B @ ( C @ ( A @ cong ) ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ perp ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD56) ).
thf(359,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( D @ ( B @ ( D @ ( A @ cong ) ) ) )
& ( C @ ( B @ ( C @ ( A @ cong ) ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ perp ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[88]) ).
thf(700,plain,
( ( ( sk6 @ ( sk7 @ ( sk5 @ ( sk8 @ perp ) ) ) )
!= ( sk6 @ ( sk13 @ ( sk4 @ ( sk1 @ perp ) ) ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[102,108]) ).
thf(701,plain,
( ( sk6 @ ( sk7 @ ( sk5 @ ( sk8 @ perp ) ) ) )
!= ( sk6 @ ( sk13 @ ( sk4 @ ( sk1 @ perp ) ) ) ) ),
inference(simp,[status(thm)],[700]) ).
thf(702,plain,
( ( sk6 != sk6 )
| ( sk13 != sk7 )
| ( sk5 != sk4 )
| ( sk8 != sk1 ) ),
inference(simp,[status(thm)],[701]) ).
thf(703,plain,
( ( sk13 != sk7 )
| ( sk5 != sk4 )
| ( sk8 != sk1 ) ),
inference(simp,[status(thm)],[702]) ).
thf(154,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ ( B @ coll ) ) )
| ~ ( C @ ( B @ ( A @ coll ) ) ) ),
inference(cnf,[status(esa)],[153]) ).
thf(51,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) )
=> ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( A @ ( B @ eqangle ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD18) ).
thf(250,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) )
=> ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( A @ ( B @ eqangle ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[51]) ).
thf(90,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( D @ ( C @ ( E @ midp ) ) )
& ( B @ ( A @ ( E @ midp ) ) ) )
=> ( D @ ( B @ ( C @ ( A @ para ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD63) ).
thf(363,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
( ( ( D @ ( C @ ( E @ midp ) ) )
& ( B @ ( A @ ( E @ midp ) ) ) )
=> ( D @ ( B @ ( C @ ( A @ para ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[90]) ).
thf(40,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) )
=> ( H @ ( G @ ( D @ ( C @ ( F @ ( E @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD21) ).
thf(218,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i] :
( ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) )
=> ( H @ ( G @ ( D @ ( C @ ( F @ ( E @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(104,plain,
sk2 @ ( sk1 @ ( sk12 @ midp ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(92,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ~ ( D @ ( C @ ( B @ ( A @ perp ) ) ) )
& ( B @ ( A @ ( D @ ( C @ ( D @ ( C @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ para ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD72) ).
thf(368,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ~ ( D @ ( C @ ( B @ ( A @ perp ) ) ) )
& ( B @ ( A @ ( D @ ( C @ ( D @ ( C @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ para ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[92]) ).
thf(72,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( B @ ( A @ ( C @ ( D @ perp ) ) ) )
& ( B @ ( A @ ( C @ midp ) ) ) )
=> ( B @ ( D @ ( A @ ( D @ cong ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD55) ).
thf(304,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( B @ ( A @ ( C @ ( D @ perp ) ) ) )
& ( B @ ( A @ ( C @ midp ) ) ) )
=> ( B @ ( D @ ( A @ ( D @ cong ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[72]) ).
thf(55,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i,I: $i,J: $i,K: $i,L: $i] :
( ( ( L @ ( K @ ( J @ ( I @ ( H @ ( G @ ( F @ ( E @ eqangle ) ) ) ) ) ) ) )
& ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) ) )
=> ( L @ ( K @ ( J @ ( I @ ( D @ ( C @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD22) ).
thf(258,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i,G: $i,H: $i,I: $i,J: $i,K: $i,L: $i] :
( ( ( L @ ( K @ ( J @ ( I @ ( H @ ( G @ ( F @ ( E @ eqangle ) ) ) ) ) ) ) )
& ( H @ ( G @ ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) ) )
=> ( L @ ( K @ ( J @ ( I @ ( D @ ( C @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[55]) ).
thf(17,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( C @ ( D @ ( A @ ( D @ cong ) ) ) )
& ( B @ ( D @ ( A @ ( D @ cong ) ) ) ) )
=> ( C @ ( B @ ( A @ ( D @ circle ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD12) ).
thf(158,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( C @ ( D @ ( A @ ( D @ cong ) ) ) )
& ( B @ ( D @ ( A @ ( D @ cong ) ) ) ) )
=> ( C @ ( B @ ( A @ ( D @ circle ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(28,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
? [E: $i] :
( ( ( B @ ( C @ ( D @ ( C @ ( D @ ( C @ ( C @ ( A @ eqangle ) ) ) ) ) ) ) )
& ( B @ ( C @ ( A @ ( C @ cong ) ) ) ) )
=> ( ( D @ ( C @ ( E @ coll ) ) )
& ( E @ ( A @ ( B @ coll ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleX2) ).
thf(186,plain,
! [A: $i,B: $i,C: $i,D: $i] :
? [E: $i] :
( ( ( B @ ( C @ ( D @ ( C @ ( D @ ( C @ ( C @ ( A @ eqangle ) ) ) ) ) ) ) )
& ( B @ ( C @ ( A @ ( C @ cong ) ) ) ) )
=> ( ( D @ ( C @ ( E @ coll ) ) )
& ( E @ ( A @ ( B @ coll ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(114,plain,
sk5 @ ( sk9 @ ( sk2 @ ( sk1 @ perp ) ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(23,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
? [F: $i] :
( ( ~ ( C @ ( B @ ( A @ coll ) ) )
& ( E @ ( B @ ( D @ ( A @ ( C @ ( B @ ( C @ ( A @ eqangle ) ) ) ) ) ) ) ) )
=> ( ( F @ ( C @ ( B @ ( D @ cyclic ) ) ) )
& ( F @ ( B @ ( F @ ( A @ ( C @ ( B @ ( C @ ( A @ eqangle ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleX5) ).
thf(171,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
? [F: $i] :
( ( ~ ( C @ ( B @ ( A @ coll ) ) )
& ( E @ ( B @ ( D @ ( A @ ( C @ ( B @ ( C @ ( A @ eqangle ) ) ) ) ) ) ) ) )
=> ( ( F @ ( C @ ( B @ ( D @ cyclic ) ) ) )
& ( F @ ( B @ ( F @ ( A @ ( C @ ( B @ ( C @ ( A @ eqangle ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(119,plain,
sk4 @ ( sk2 @ ( sk3 @ ( sk1 @ perp ) ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(49,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ~ ( A @ ( D @ ( C @ coll ) ) )
& ( B @ ( D @ ( A @ ( D @ ( B @ ( C @ ( A @ ( C @ eqangle ) ) ) ) ) ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ cyclic ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD42a) ).
thf(246,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ~ ( A @ ( D @ ( C @ coll ) ) )
& ( B @ ( D @ ( A @ ( D @ ( B @ ( C @ ( A @ ( C @ eqangle ) ) ) ) ) ) ) ) )
=> ( D @ ( C @ ( B @ ( A @ cyclic ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[49]) ).
thf(85,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( C @ ( A @ ( D @ midp ) ) )
& ( C @ ( B @ ( B @ ( A @ perp ) ) ) ) )
=> ( D @ ( B @ ( D @ ( A @ cong ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD52) ).
thf(346,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( C @ ( A @ ( D @ midp ) ) )
& ( C @ ( B @ ( B @ ( A @ perp ) ) ) ) )
=> ( D @ ( B @ ( D @ ( A @ cong ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[85]) ).
thf(67,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
? [E: $i] :
( ( ( B @ ( C @ ( D @ ( C @ ( D @ ( C @ ( C @ ( A @ eqangle ) ) ) ) ) ) ) )
& ( B @ ( A @ ( D @ ( C @ perp ) ) ) ) )
=> ( ( D @ ( C @ ( E @ coll ) ) )
& ( E @ ( A @ ( B @ coll ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleX3) ).
thf(287,plain,
! [A: $i,B: $i,C: $i,D: $i] :
? [E: $i] :
( ( ( B @ ( C @ ( D @ ( C @ ( D @ ( C @ ( C @ ( A @ eqangle ) ) ) ) ) ) ) )
& ( B @ ( A @ ( D @ ( C @ perp ) ) ) ) )
=> ( ( D @ ( C @ ( E @ coll ) ) )
& ( E @ ( A @ ( B @ coll ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[67]) ).
thf(70,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ perp ) ) ) )
=> ( B @ ( A @ ( D @ ( C @ perp ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD8) ).
thf(300,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ perp ) ) ) )
=> ( B @ ( A @ ( D @ ( C @ perp ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[70]) ).
thf(57,axiom,
! [A: $i,B: $i,C: $i] :
( ( ~ ( B @ ( A @ ( C @ coll ) ) )
& ( B @ ( C @ ( B @ ( A @ ( B @ ( A @ ( A @ ( C @ eqangle ) ) ) ) ) ) ) ) )
=> ( B @ ( C @ ( A @ ( C @ cong ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD47) ).
thf(262,plain,
! [A: $i,B: $i,C: $i] :
( ( ~ ( B @ ( A @ ( C @ coll ) ) )
& ( B @ ( C @ ( B @ ( A @ ( B @ ( A @ ( A @ ( C @ eqangle ) ) ) ) ) ) ) ) )
=> ( B @ ( C @ ( A @ ( C @ cong ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).
thf(12,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ simtri ) ) ) ) ) )
=> ( F @ ( E @ ( E @ ( D @ ( C @ ( B @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD60) ).
thf(146,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ simtri ) ) ) ) ) )
=> ( F @ ( E @ ( E @ ( D @ ( C @ ( B @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(62,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( D @ ( C @ ( B @ ( A @ cyclic ) ) ) )
& ( D @ ( B @ ( D @ ( A @ cong ) ) ) )
& ( C @ ( B @ ( C @ ( A @ cong ) ) ) ) )
=> ( D @ ( A @ ( A @ ( C @ perp ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD57) ).
thf(273,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( D @ ( C @ ( B @ ( A @ cyclic ) ) ) )
& ( D @ ( B @ ( D @ ( A @ cong ) ) ) )
& ( C @ ( B @ ( C @ ( A @ cong ) ) ) ) )
=> ( D @ ( A @ ( A @ ( C @ perp ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[62]) ).
thf(83,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
? [F: $i] :
( ( ( D @ ( B @ ( E @ midp ) ) )
& ( D @ ( C @ ( A @ ( C @ perp ) ) ) )
& ( C @ ( A @ ( B @ ( A @ perp ) ) ) ) )
=> ( C @ ( A @ ( F @ midp ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleX16) ).
thf(341,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
? [F: $i] :
( ( ( D @ ( B @ ( E @ midp ) ) )
& ( D @ ( C @ ( A @ ( C @ perp ) ) ) )
& ( C @ ( A @ ( B @ ( A @ perp ) ) ) ) )
=> ( C @ ( A @ ( F @ midp ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[83]) ).
thf(60,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
? [E: $i] :
( ( ( D @ ( C @ ( B @ ( A @ cyclic ) ) ) )
& ( B @ ( C @ ( C @ ( A @ perp ) ) ) ) )
=> ( C @ ( B @ ( A @ ( E @ circle ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleX14) ).
thf(268,plain,
! [A: $i,B: $i,C: $i,D: $i] :
? [E: $i] :
( ( ( D @ ( C @ ( B @ ( A @ cyclic ) ) ) )
& ( B @ ( C @ ( C @ ( A @ perp ) ) ) ) )
=> ( C @ ( B @ ( A @ ( E @ circle ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[60]) ).
thf(78,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
? [E: $i] :
( ( ( C @ ( A @ ( C @ ( B @ ( C @ ( B @ ( C @ ( D @ eqangle ) ) ) ) ) ) ) )
& ( A @ ( B @ ( B @ ( C @ perp ) ) ) ) )
=> ( ( D @ ( C @ ( E @ coll ) ) )
& ( B @ ( A @ ( E @ coll ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleX1) ).
thf(326,plain,
! [A: $i,B: $i,C: $i,D: $i] :
? [E: $i] :
( ( ( C @ ( A @ ( C @ ( B @ ( C @ ( B @ ( C @ ( D @ eqangle ) ) ) ) ) ) ) )
& ( A @ ( B @ ( B @ ( C @ perp ) ) ) ) )
=> ( ( D @ ( C @ ( E @ coll ) ) )
& ( B @ ( A @ ( E @ coll ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[78]) ).
thf(107,plain,
sk3 @ ( sk1 @ ( sk10 @ midp ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(126,plain,
sk4 @ ( sk2 @ ( sk14 @ midp ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(7,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( C @ ( B @ ( A @ ( F @ ( E @ ( D @ simtri ) ) ) ) ) )
=> ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ simtri ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD33) ).
thf(136,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( C @ ( B @ ( A @ ( F @ ( E @ ( D @ simtri ) ) ) ) ) )
=> ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ simtri ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(64,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
? [F: $i] :
( ( ( B @ ( A @ ( E @ midp ) ) )
& ( D @ ( C @ ( B @ ( A @ para ) ) ) )
& ( D @ ( C @ ( B @ ( A @ cyclic ) ) ) ) )
=> ( C @ ( B @ ( A @ ( F @ circle ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleX13) ).
thf(277,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i] :
? [F: $i] :
( ( ( B @ ( A @ ( E @ midp ) ) )
& ( D @ ( C @ ( B @ ( A @ para ) ) ) )
& ( D @ ( C @ ( B @ ( A @ cyclic ) ) ) ) )
=> ( C @ ( B @ ( A @ ( F @ circle ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[64]) ).
thf(19,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ cyclic ) ) ) )
=> ( C @ ( D @ ( B @ ( A @ cyclic ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD14) ).
thf(163,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ cyclic ) ) ) )
=> ( C @ ( D @ ( B @ ( A @ cyclic ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(33,axiom,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( ~ ( C @ ( B @ ( A @ coll ) ) )
& ( F @ ( E @ ( F @ ( D @ ( C @ ( B @ ( C @ ( A @ eqangle ) ) ) ) ) ) ) )
& ( F @ ( E @ ( E @ ( D @ ( C @ ( B @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) ) )
=> ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ simtri ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD58) ).
thf(200,plain,
! [A: $i,B: $i,C: $i,D: $i,E: $i,F: $i] :
( ( ~ ( C @ ( B @ ( A @ coll ) ) )
& ( F @ ( E @ ( F @ ( D @ ( C @ ( B @ ( C @ ( A @ eqangle ) ) ) ) ) ) ) )
& ( F @ ( E @ ( E @ ( D @ ( C @ ( B @ ( B @ ( A @ eqangle ) ) ) ) ) ) ) ) )
=> ( F @ ( E @ ( D @ ( C @ ( B @ ( A @ simtri ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(53,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ para ) ) ) )
=> ( B @ ( A @ ( D @ ( C @ para ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD5) ).
thf(254,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( D @ ( C @ ( B @ ( A @ para ) ) ) )
=> ( B @ ( A @ ( D @ ( C @ para ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).
thf(122,plain,
sk8 @ ( sk19 @ ( sk3 @ ( sk2 @ perp ) ) ),
inference(cnfConj,[status(thm)],[99]) ).
thf(42,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( D @ ( B @ ( A @ coll ) ) )
& ( C @ ( B @ ( A @ coll ) ) ) )
=> ( A @ ( D @ ( C @ coll ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ruleD3) ).
thf(222,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( D @ ( B @ ( A @ coll ) ) )
& ( C @ ( B @ ( A @ coll ) ) ) )
=> ( A @ ( D @ ( C @ coll ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(909,plain,
$false,
inference(e,[status(thm)],[169,738,138,101,115,308,120,379,202,142,153,184,372,110,196,125,344,416,228,216,179,211,106,121,348,353,280,453,132,206,116,243,292,248,117,102,220,366,334,302,260,160,275,165,252,361,97,224,124,339,193,109,256,134,128,105,266,311,298,148,264,176,191,118,204,144,713,181,113,230,318,271,103,323,140,155,198,108,130,306,226,241,167,374,209,112,123,282,150,331,370,127,338,359,336,703,154,250,363,218,104,368,304,258,158,186,114,171,119,246,346,287,300,262,146,273,341,268,326,107,126,136,277,163,200,111,254,122,222,100]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GEO545+1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.08 % 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.15/0.61 % Computer : n026.cluster.edu
% 0.15/0.61 % Model : x86_64 x86_64
% 0.15/0.61 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.61 % Memory : 8046.5625MB
% 0.15/0.61 % OS : Linux 6.8.0-71-generic
% 0.15/0.61 % CPULimit : 300
% 0.15/0.61 % WCLimit : 300
% 0.15/0.61 % DateTime : Fri Sep 25 13:43:55 UTC 2026
% 0.15/0.61 % CPUTime :
% 0.15/0.61 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.91/1.19 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.41/1.50 % [INFO] Parsing done (300ms).
% 1.87/1.51 % [INFO] Running in sequential loop mode.
% 2.92/1.91 % [INFO] eprover registered as external prover.
% 2.92/1.92 % [INFO] Scanning for conjecture ...
% 3.20/2.08 % [INFO] Found a conjecture (or negated_conjecture) and 94 axioms. Running axiom selection ...
% 3.40/2.18 % [INFO] Axiom selection finished. Selected 94 axioms (removed 0 axioms).
% 3.84/2.33 % [INFO] Problem is first-order (TPTP FOF).
% 3.84/2.36 % [INFO] Type checking passed.
% 3.84/2.37 % [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 ...
% 14.24/4.86 % External prover 'e' found a proof!
% 14.24/4.86 % [INFO] Killing All external provers ...
% 14.24/4.86 % Time passed: 4106ms (effective reasoning time: 3343ms)
% 14.24/4.86 % Solved by 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)>
% 14.24/4.86 % Axioms used in derivation (94): ruleD34, ruleD66, ruleD52, ruleX16, ruleD61, ruleD23, ruleD56, ruleD9, ruleD18, ruleD62, ruleD8, ruleD39, ruleD21, ruleD45, ruleX18, ruleX7, ruleD68, ruleD11, ruleD49, ruleD44, ruleD51, ruleD33, ruleX2, ruleD73, ruleD14, ruleX12, ruleD55, ruleD24, ruleD29, ruleD40, ruleD4, ruleX6, ruleD42a, ruleD41, ruleX17, ruleD59, ruleD20, ruleD19, ruleD74, ruleD26, ruleD38, ruleD7, ruleD48, ruleD67, ruleD10, ruleD25, ruleX3, ruleD63, ruleX13, ruleX10, ruleD15, ruleD30, ruleD70, ruleD60, ruleD58, ruleD75, ruleD3, ruleD47, ruleD36, ruleX4, ruleD6, ruleD16, ruleD37, ruleD53, ruleD27, ruleX5, ruleX14, ruleD2, ruleD12, ruleX9, ruleD42b, ruleD64, ruleD31, ruleD71, ruleD35, ruleX8, ruleX11, ruleX1, ruleD57, ruleD17, ruleD46, ruleD22, ruleD5, ruleD32, ruleD13, ruleD72, ruleD1, ruleD28, ruleD43, ruleD50, ruleD65, ruleD54, ruleX15, ruleD69
% 14.24/4.86 % No. of inferences in proof: 244
% 14.24/4.86 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 4106 ms resp. 3343 ms w/o parsing
% 15.43/5.05 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 15.43/5.05 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------