%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : GEO205+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:12:46 AM UTC 2026
% Result : Theorem 88.06s 19.27s
% Output : Refutation 75.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 39
% Syntax : Number of formulae : 728 ( 109 unt; 0 typ; 3 def)
% Number of atoms : 2883 ( 396 equ; 0 cnn)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 8270 (1305 ~;1378 |; 65 &;5441 @)
% ( 5 <=>; 76 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 8 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 22 ( 19 usr; 5 con; 0-2 aty)
% Number of variables : 1928 ( 0 ^;1912 !; 13 ?;1928 :)
% ( 0 !>; 0 ?*; 0 @-; 3 @+)
% Comments :
%------------------------------------------------------------------------------
thf(convergent_lines_decl,type,
convergent_lines: $i > $i > $o ).
thf(equal_lines_decl,type,
equal_lines: $i > $i > $o ).
thf(equal_points_decl,type,
equal_points: $i > $i > $o ).
thf(intersection_point_decl,type,
intersection_point: $i > $i > $i ).
thf(distinct_points_decl,type,
distinct_points: $i > $i > $o ).
thf(distinct_lines_decl,type,
distinct_lines: $i > $i > $o ).
thf(apart_point_and_line_decl,type,
apart_point_and_line: $i > $i > $o ).
thf(unorthogonal_lines_decl,type,
unorthogonal_lines: $i > $i > $o ).
thf(orthogonal_through_point_decl,type,
orthogonal_through_point: $i > $i > $i ).
thf(line_decl,type,
line: $i > $o ).
thf(point_decl,type,
point: $i > $o ).
thf(parallel_through_point_decl,type,
parallel_through_point: $i > $i > $i ).
thf(orthogonal_lines_decl,type,
orthogonal_lines: $i > $i > $o ).
thf(line_connecting_decl,type,
line_connecting: $i > $i > $i ).
thf(incident_point_and_line_decl,type,
incident_point_and_line: $i > $i > $o ).
thf(parallel_lines_decl,type,
parallel_lines: $i > $i > $o ).
thf(sk1_decl,type,
sk1: $i ).
thf(sk2_decl,type,
sk2: $i ).
thf(sk3_decl,type,
sk3: $i ).
thf(sk1_def,definition,
( sk1
= ( @+[A: $i] :
~ ! [B: $i,C: $i] :
( ( ( C @ ( B @ equal_lines ) )
& ( B @ ( A @ convergent_lines ) ) )
=> ( ( C @ ( A @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ equal_points ) )
& ( C @ ( A @ convergent_lines ) ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: $i] :
~ ! [B: $i] :
( ( ( B @ ( A @ equal_lines ) )
& ( A @ ( sk1 @ convergent_lines ) ) )
=> ( ( B @ ( sk1 @ intersection_point ) @ ( A @ ( sk1 @ intersection_point ) @ equal_points ) )
& ( B @ ( sk1 @ convergent_lines ) ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: $i] :
~ ( ( ( A @ ( sk2 @ equal_lines ) )
& ( sk2 @ ( sk1 @ convergent_lines ) ) )
=> ( ( A @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ equal_points ) )
& ( A @ ( sk1 @ convergent_lines ) ) ) ) ) ) ).
thf(12,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ distinct_points ) )
=> ( ( C @ ( B @ distinct_points ) )
| ( C @ ( A @ distinct_points ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',apart4) ).
thf(69,plain,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ distinct_points ) )
=> ( ( C @ ( B @ distinct_points ) )
| ( C @ ( A @ distinct_points ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(30,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ equal_lines ) )
<=> ~ ( B @ ( A @ distinct_lines ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
thf(131,plain,
! [A: $i,B: $i] :
( ( ~ ( B @ ( A @ distinct_lines ) )
=> ( B @ ( A @ equal_lines ) ) )
& ( ( B @ ( A @ equal_lines ) )
=> ~ ( B @ ( A @ distinct_lines ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(132,plain,
( ! [A: $i,B: $i] :
( ~ ( B @ ( A @ distinct_lines ) )
=> ( B @ ( A @ equal_lines ) ) )
& ! [A: $i,B: $i] :
( ( B @ ( A @ equal_lines ) )
=> ~ ( B @ ( A @ distinct_lines ) ) ) ),
inference(miniscope,[status(thm)],[131]) ).
thf(133,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ equal_lines ) )
| ( D @ ( C @ distinct_lines ) ) )
& ( ~ ( B @ ( A @ distinct_lines ) )
| ~ ( B @ ( A @ equal_lines ) ) ) ),
inference(cnf,[status(esa)],[132]) ).
thf(135,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ equal_lines ) )
| ( B @ ( A @ distinct_lines ) ) ),
inference(cnfConj,[status(thm)],[133]) ).
thf(136,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ equal_lines ) )
| ( B @ ( A @ distinct_lines ) ) ),
inference(simp,[status(thm)],[135]) ).
thf(14,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ distinct_lines ) )
=> ( ( C @ ( B @ distinct_lines ) )
| ( C @ ( A @ distinct_lines ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',apart5) ).
thf(75,plain,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ distinct_lines ) )
=> ( ( C @ ( B @ distinct_lines ) )
| ( C @ ( A @ distinct_lines ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(76,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ distinct_lines ) )
=> ! [C: $i] :
( ( C @ ( B @ distinct_lines ) )
| ( C @ ( A @ distinct_lines ) ) ) ),
inference(miniscope,[status(thm)],[75]) ).
thf(77,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ distinct_lines ) )
| ( C @ ( A @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_lines ) ) ),
inference(cnf,[status(esa)],[76]) ).
thf(1,conjecture,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ equal_lines ) )
& ( B @ ( A @ convergent_lines ) ) )
=> ( ( C @ ( A @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ equal_points ) )
& ( C @ ( A @ convergent_lines ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',con) ).
thf(2,negated_conjecture,
~ ! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ equal_lines ) )
& ( B @ ( A @ convergent_lines ) ) )
=> ( ( C @ ( A @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ equal_points ) )
& ( C @ ( A @ convergent_lines ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(38,plain,
~ ! [A: $i,B: $i,C: $i] :
( ( ( C @ ( B @ equal_lines ) )
& ( B @ ( A @ convergent_lines ) ) )
=> ( ( C @ ( A @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ equal_points ) )
& ( C @ ( A @ convergent_lines ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(39,plain,
( ( ~ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ equal_points ) )
| ~ ( sk3 @ ( sk1 @ convergent_lines ) ) )
& ( sk3 @ ( sk2 @ equal_lines ) )
& ( sk2 @ ( sk1 @ convergent_lines ) ) ),
inference(cnf,[status(esa)],[38]) ).
thf(41,plain,
sk3 @ ( sk2 @ equal_lines ),
inference(cnfConj,[status(thm)],[39]) ).
thf(134,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ distinct_lines ) )
| ~ ( B @ ( A @ equal_lines ) ) ),
inference(cnfConj,[status(thm)],[133]) ).
thf(408,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk2 @ equal_lines ) )
!= ( B @ ( A @ equal_lines ) ) )
| ~ ( B @ ( A @ distinct_lines ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[41,134]) ).
thf(409,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk2 @ equal_lines ) )
!= ( B @ ( A @ equal_lines ) ) )
| ~ ( B @ ( A @ distinct_lines ) ) ),
inference(simp,[status(thm)],[408]) ).
thf(410,plain,
~ ( sk3 @ ( sk2 @ distinct_lines ) ),
inference(pattern_uni,[status(thm)],[409:[bind(A,$thf( sk2 )),bind(B,$thf( sk3 ))]]) ).
thf(1674,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ distinct_lines ) )
!= ( sk3 @ ( sk2 @ distinct_lines ) ) )
| ~ $true
| ( C @ ( A @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[77,410]) ).
thf(1675,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ distinct_lines ) )
!= ( sk3 @ ( sk2 @ distinct_lines ) ) )
| ( C @ ( A @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_lines ) ) ),
inference(simp,[status(thm)],[1674]) ).
thf(1676,plain,
! [A: $i] :
( ( sk3 @ ( A @ distinct_lines ) )
| ~ ( sk2 @ ( A @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[1675:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( sk3 ))]]) ).
thf(13,axiom,
! [A: $i] :
~ ( A @ ( A @ distinct_lines ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',apart2) ).
thf(72,plain,
! [A: $i] :
~ ( A @ ( A @ distinct_lines ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(73,plain,
~ ? [A: $i] : ( A @ ( A @ distinct_lines ) ),
inference(miniscope,[status(thm)],[72]) ).
thf(74,plain,
! [A: $i] :
~ ( A @ ( A @ distinct_lines ) ),
inference(cnf,[status(esa)],[73]) ).
thf(1710,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( A @ distinct_lines ) )
!= ( B @ ( B @ distinct_lines ) ) )
| ~ $true
| ~ ( sk2 @ ( A @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1676,74]) ).
thf(1711,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( A @ distinct_lines ) )
!= ( B @ ( B @ distinct_lines ) ) )
| ~ ( sk2 @ ( A @ distinct_lines ) ) ),
inference(simp,[status(thm)],[1710]) ).
thf(1712,plain,
~ ( sk2 @ ( sk3 @ distinct_lines ) ),
inference(pattern_uni,[status(thm)],[1711:[bind(A,$thf( sk3 )),bind(B,$thf( sk3 ))]]) ).
thf(1760,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ distinct_lines ) )
!= ( sk2 @ ( sk3 @ distinct_lines ) ) )
| ~ $true
| ( C @ ( B @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[77,1712]) ).
thf(1761,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ distinct_lines ) )
!= ( sk2 @ ( sk3 @ distinct_lines ) ) )
| ( C @ ( B @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_lines ) ) ),
inference(simp,[status(thm)],[1760]) ).
thf(1762,plain,
! [A: $i] :
( ( sk2 @ ( A @ distinct_lines ) )
| ~ ( A @ ( sk3 @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[1761:[bind(A,$thf( sk3 )),bind(B,$thf( B )),bind(C,$thf( sk2 ))]]) ).
thf(1775,plain,
! [A: $i] :
( ( sk2 @ ( A @ distinct_lines ) )
| ~ ( A @ ( sk3 @ distinct_lines ) ) ),
inference(simp,[status(thm)],[1762]) ).
thf(2231,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( sk3 @ distinct_lines ) ) )
| ( sk2 @ ( C @ distinct_lines ) )
| ~ $true
| ( B @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[136,1775]) ).
thf(2232,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( sk3 @ distinct_lines ) ) )
| ( sk2 @ ( C @ distinct_lines ) )
| ( B @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[2231]) ).
thf(2233,plain,
! [A: $i] :
( ( sk2 @ ( A @ distinct_lines ) )
| ( A @ ( sk3 @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[2232:[bind(A,$thf( sk3 )),bind(B,$thf( B )),bind(C,$thf( B ))]]) ).
thf(2249,plain,
! [A: $i] :
( ( sk2 @ ( A @ distinct_lines ) )
| ( A @ ( sk3 @ equal_lines ) ) ),
inference(simp,[status(thm)],[2233]) ).
thf(4199,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( sk2 @ ( B @ distinct_lines ) ) )
| ( sk3 @ ( B @ distinct_lines ) )
| ~ $true
| ( A @ ( sk3 @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[2249,1676]) ).
thf(4200,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( sk2 @ ( B @ distinct_lines ) ) )
| ( sk3 @ ( B @ distinct_lines ) )
| ( A @ ( sk3 @ equal_lines ) ) ),
inference(simp,[status(thm)],[4199]) ).
thf(4201,plain,
! [A: $i] :
( ( sk3 @ ( A @ distinct_lines ) )
| ( A @ ( sk3 @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[4200:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(26,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ equal_points ) )
<=> ~ ( B @ ( A @ distinct_points ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
thf(113,plain,
! [A: $i,B: $i] :
( ( ~ ( B @ ( A @ distinct_points ) )
=> ( B @ ( A @ equal_points ) ) )
& ( ( B @ ( A @ equal_points ) )
=> ~ ( B @ ( A @ distinct_points ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(114,plain,
( ! [A: $i,B: $i] :
( ~ ( B @ ( A @ distinct_points ) )
=> ( B @ ( A @ equal_points ) ) )
& ! [A: $i,B: $i] :
( ( B @ ( A @ equal_points ) )
=> ~ ( B @ ( A @ distinct_points ) ) ) ),
inference(miniscope,[status(thm)],[113]) ).
thf(115,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ equal_points ) )
| ( D @ ( C @ distinct_points ) ) )
& ( ~ ( B @ ( A @ distinct_points ) )
| ~ ( B @ ( A @ equal_points ) ) ) ),
inference(cnf,[status(esa)],[114]) ).
thf(117,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ equal_points ) )
| ( B @ ( A @ distinct_points ) ) ),
inference(cnfConj,[status(thm)],[115]) ).
thf(118,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ equal_points ) )
| ( B @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[117]) ).
thf(19,axiom,
! [A: $i] :
~ ( A @ ( A @ distinct_points ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',apart1) ).
thf(92,plain,
! [A: $i] :
~ ( A @ ( A @ distinct_points ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(93,plain,
~ ? [A: $i] : ( A @ ( A @ distinct_points ) ),
inference(miniscope,[status(thm)],[92]) ).
thf(94,plain,
! [A: $i] :
~ ( A @ ( A @ distinct_points ) ),
inference(cnf,[status(esa)],[93]) ).
thf(361,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_points ) )
!= ( C @ ( C @ distinct_points ) ) )
| ~ $true
| ( B @ ( A @ equal_points ) ) ),
inference(paramod_ordered,[status(thm)],[118,94]) ).
thf(362,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_points ) )
!= ( C @ ( C @ distinct_points ) ) )
| ( B @ ( A @ equal_points ) ) ),
inference(simp,[status(thm)],[361]) ).
thf(363,plain,
! [A: $i] : ( A @ ( A @ equal_points ) ),
inference(pattern_uni,[status(thm)],[362:[bind(A,$thf( B )),bind(B,$thf( B )),bind(C,$thf( B ))]]) ).
thf(365,plain,
! [A: $i] : ( A @ ( A @ equal_points ) ),
inference(simp,[status(thm)],[363]) ).
thf(23,axiom,
! [A: $i,B: $i] :
~ ( ~ ( B @ ( A @ unorthogonal_lines ) )
& ~ ( B @ ( A @ convergent_lines ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',coipo1) ).
thf(101,plain,
! [A: $i,B: $i] :
~ ( ~ ( B @ ( A @ unorthogonal_lines ) )
& ~ ( B @ ( A @ convergent_lines ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(3,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( D @ ( C @ distinct_lines ) )
& ( B @ ( A @ distinct_points ) ) )
=> ( ( D @ ( B @ apart_point_and_line ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cu1) ).
thf(43,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( ( D @ ( C @ distinct_lines ) )
& ( B @ ( A @ distinct_points ) ) )
=> ( ( D @ ( B @ apart_point_and_line ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(44,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ apart_point_and_line ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(cnf,[status(esa)],[43]) ).
thf(6,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ apart_point_and_line ) )
=> ( ( C @ ( A @ apart_point_and_line ) )
| ( C @ ( B @ distinct_lines ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ceq2) ).
thf(51,plain,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ apart_point_and_line ) )
=> ( ( C @ ( A @ apart_point_and_line ) )
| ( C @ ( B @ distinct_lines ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(52,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ apart_point_and_line ) )
=> ! [C: $i] :
( ( C @ ( A @ apart_point_and_line ) )
| ( C @ ( B @ distinct_lines ) ) ) ),
inference(miniscope,[status(thm)],[51]) ).
thf(53,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ apart_point_and_line ) )
| ( C @ ( B @ distinct_lines ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(cnf,[status(esa)],[52]) ).
thf(333,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( F @ ( E @ apart_point_and_line ) ) )
| ( G @ ( E @ apart_point_and_line ) )
| ( G @ ( F @ distinct_lines ) )
| ~ $true
| ( D @ ( B @ apart_point_and_line ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(paramod_ordered,[status(thm)],[44,53]) ).
thf(334,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( F @ ( E @ apart_point_and_line ) ) )
| ( G @ ( E @ apart_point_and_line ) )
| ( G @ ( F @ distinct_lines ) )
| ( D @ ( B @ apart_point_and_line ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[333]) ).
thf(335,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( A @ apart_point_and_line ) )
| ( E @ ( C @ distinct_lines ) )
| ( D @ ( B @ apart_point_and_line ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(pattern_uni,[status(thm)],[334:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( A )),bind(F,$thf( C ))]]) ).
thf(347,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( A @ apart_point_and_line ) )
| ( E @ ( C @ distinct_lines ) )
| ( D @ ( B @ apart_point_and_line ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[335]) ).
thf(35,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ distinct_lines ) )
=> ( B @ ( A @ convergent_lines ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p1) ).
thf(146,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ distinct_lines ) )
=> ( B @ ( A @ convergent_lines ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(147,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ convergent_lines ) )
| ~ ( B @ ( A @ distinct_lines ) ) ),
inference(cnf,[status(esa)],[146]) ).
thf(466,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( D @ ( C @ distinct_lines ) ) )
| ( D @ ( C @ convergent_lines ) )
| ~ $true
| ( B @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[136,147]) ).
thf(467,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( D @ ( C @ distinct_lines ) ) )
| ( D @ ( C @ convergent_lines ) )
| ( B @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[466]) ).
thf(468,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ convergent_lines ) )
| ( B @ ( A @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[467:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(16,axiom,
! [A: $i,B: $i] :
~ ( A @ ( B @ parallel_through_point ) @ ( A @ apart_point_and_line ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cp2) ).
thf(81,plain,
! [A: $i,B: $i] :
~ ( A @ ( B @ parallel_through_point ) @ ( A @ apart_point_and_line ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(82,plain,
~ ? [A: $i,B: $i] : ( A @ ( B @ parallel_through_point ) @ ( A @ apart_point_and_line ) ),
inference(miniscope,[status(thm)],[81]) ).
thf(83,plain,
! [B: $i,A: $i] :
~ ( A @ ( B @ parallel_through_point ) @ ( A @ apart_point_and_line ) ),
inference(cnf,[status(esa)],[82]) ).
thf(319,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( D @ ( E @ parallel_through_point ) @ ( D @ apart_point_and_line ) ) )
| ~ $true
| ( C @ ( B @ distinct_lines ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[53,83]) ).
thf(320,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( D @ ( E @ parallel_through_point ) @ ( D @ apart_point_and_line ) ) )
| ( C @ ( B @ distinct_lines ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[319]) ).
thf(321,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ parallel_through_point ) @ ( A @ distinct_lines ) )
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[320:[bind(A,$thf( G )),bind(B,$thf( B )),bind(C,$thf( G @ ( F @ parallel_through_point ) )),bind(D,$thf( G )),bind(E,$thf( F ))]]) ).
thf(345,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ parallel_through_point ) @ ( A @ distinct_lines ) )
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[321]) ).
thf(2209,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ~ $true
| ~ ( C @ ( B @ equal_lines ) )
| ~ ( A @ ( sk3 @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1775,134]) ).
thf(2210,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ~ ( C @ ( B @ equal_lines ) )
| ~ ( A @ ( sk3 @ distinct_lines ) ) ),
inference(simp,[status(thm)],[2209]) ).
thf(2211,plain,
! [A: $i] :
( ~ ( sk2 @ ( A @ equal_lines ) )
| ~ ( A @ ( sk3 @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[2210:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk2 ))]]) ).
thf(2283,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ parallel_through_point ) @ ( A @ distinct_lines ) )
!= ( D @ ( sk3 @ distinct_lines ) ) )
| ~ ( sk2 @ ( D @ equal_lines ) )
| ~ $true
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[345,2211]) ).
thf(2284,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ parallel_through_point ) @ ( A @ distinct_lines ) )
!= ( D @ ( sk3 @ distinct_lines ) ) )
| ~ ( sk2 @ ( D @ equal_lines ) )
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[2283]) ).
thf(2285,plain,
! [B: $i,A: $i] :
( ~ ( sk2 @ ( B @ ( A @ parallel_through_point ) @ equal_lines ) )
| ~ ( sk3 @ ( B @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[2284:[bind(A,$thf( sk3 )),bind(B,$thf( E )),bind(C,$thf( F )),bind(D,$thf( F @ ( E @ parallel_through_point ) ))]]) ).
thf(2306,plain,
! [B: $i,A: $i] :
( ~ ( sk2 @ ( B @ ( A @ parallel_through_point ) @ equal_lines ) )
| ~ ( sk3 @ ( B @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[2285]) ).
thf(1763,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ distinct_lines ) )
!= ( sk2 @ ( sk3 @ distinct_lines ) ) )
| ~ $true
| ( C @ ( A @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[77,1712]) ).
thf(1764,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ distinct_lines ) )
!= ( sk2 @ ( sk3 @ distinct_lines ) ) )
| ( C @ ( A @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_lines ) ) ),
inference(simp,[status(thm)],[1763]) ).
thf(1765,plain,
! [A: $i] :
( ( sk2 @ ( A @ distinct_lines ) )
| ~ ( sk3 @ ( A @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[1764:[bind(A,$thf( A )),bind(B,$thf( sk3 )),bind(C,$thf( sk2 ))]]) ).
thf(2162,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( sk3 @ ( C @ distinct_lines ) ) )
| ( sk2 @ ( C @ distinct_lines ) )
| ~ $true
| ( B @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[136,1765]) ).
thf(2163,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( sk3 @ ( C @ distinct_lines ) ) )
| ( sk2 @ ( C @ distinct_lines ) )
| ( B @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[2162]) ).
thf(2164,plain,
! [A: $i] :
( ( sk2 @ ( A @ distinct_lines ) )
| ( sk3 @ ( A @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[2163:[bind(A,$thf( A )),bind(B,$thf( sk3 )),bind(C,$thf( A ))]]) ).
thf(3343,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ( C @ ( B @ convergent_lines ) )
| ~ $true
| ( sk3 @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[2164,147]) ).
thf(3344,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ( C @ ( B @ convergent_lines ) )
| ( sk3 @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[3343]) ).
thf(3345,plain,
! [A: $i] :
( ( sk2 @ ( A @ convergent_lines ) )
| ( sk3 @ ( A @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[3344:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk2 ))]]) ).
thf(40,plain,
sk2 @ ( sk1 @ convergent_lines ),
inference(cnfConj,[status(thm)],[39]) ).
thf(27,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ convergent_lines ) )
=> ( ( C @ ( B @ convergent_lines ) )
| ( C @ ( A @ convergent_lines ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax6) ).
thf(119,plain,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ convergent_lines ) )
=> ( ( C @ ( B @ convergent_lines ) )
| ( C @ ( A @ convergent_lines ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(120,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ convergent_lines ) )
=> ! [C: $i] :
( ( C @ ( B @ convergent_lines ) )
| ( C @ ( A @ convergent_lines ) ) ) ),
inference(miniscope,[status(thm)],[119]) ).
thf(121,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ convergent_lines ) )
| ( C @ ( A @ convergent_lines ) )
| ~ ( B @ ( A @ convergent_lines ) ) ),
inference(cnf,[status(esa)],[120]) ).
thf(2359,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ( C @ ( B @ convergent_lines ) )
| ( C @ ( A @ convergent_lines ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[40,121]) ).
thf(2360,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ( C @ ( B @ convergent_lines ) )
| ( C @ ( A @ convergent_lines ) ) ),
inference(simp,[status(thm)],[2359]) ).
thf(2361,plain,
! [A: $i] :
( ( A @ ( sk2 @ convergent_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[2360:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(2383,plain,
! [A: $i] :
( ( A @ ( sk2 @ convergent_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[2361]) ).
thf(31,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ convergent_lines ) )
=> ( ( C @ ( A @ convergent_lines ) )
| ( C @ ( B @ distinct_lines ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ceq3) ).
thf(137,plain,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ convergent_lines ) )
=> ( ( C @ ( A @ convergent_lines ) )
| ( C @ ( B @ distinct_lines ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(138,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ convergent_lines ) )
=> ! [C: $i] :
( ( C @ ( A @ convergent_lines ) )
| ( C @ ( B @ distinct_lines ) ) ) ),
inference(miniscope,[status(thm)],[137]) ).
thf(139,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ convergent_lines ) )
| ( C @ ( B @ distinct_lines ) )
| ~ ( B @ ( A @ convergent_lines ) ) ),
inference(cnf,[status(esa)],[138]) ).
thf(3254,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ distinct_lines ) )
!= ( sk2 @ ( sk3 @ distinct_lines ) ) )
| ~ $true
| ( C @ ( A @ convergent_lines ) )
| ~ ( B @ ( A @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[139,1712]) ).
thf(3255,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ distinct_lines ) )
!= ( sk2 @ ( sk3 @ distinct_lines ) ) )
| ( C @ ( A @ convergent_lines ) )
| ~ ( B @ ( A @ convergent_lines ) ) ),
inference(simp,[status(thm)],[3254]) ).
thf(3256,plain,
! [A: $i] :
( ( sk2 @ ( A @ convergent_lines ) )
| ~ ( sk3 @ ( A @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[3255:[bind(A,$thf( A )),bind(B,$thf( sk3 )),bind(C,$thf( sk2 ))]]) ).
thf(8765,plain,
! [B: $i,A: $i] :
( ( ( A @ ( sk2 @ convergent_lines ) )
!= ( sk3 @ ( B @ convergent_lines ) ) )
| ( sk2 @ ( B @ convergent_lines ) )
| ~ $true
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[2383,3256]) ).
thf(8766,plain,
! [B: $i,A: $i] :
( ( ( A @ ( sk2 @ convergent_lines ) )
!= ( sk3 @ ( B @ convergent_lines ) ) )
| ( sk2 @ ( B @ convergent_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[8765]) ).
thf(8767,plain,
( ( sk2 @ ( sk2 @ convergent_lines ) )
| ( sk3 @ ( sk1 @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[8766:[bind(A,$thf( sk3 )),bind(B,$thf( sk2 ))]]) ).
thf(37,axiom,
! [A: $i] :
~ ( A @ ( A @ convergent_lines ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',apart3) ).
thf(154,plain,
! [A: $i] :
~ ( A @ ( A @ convergent_lines ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(155,plain,
~ ? [A: $i] : ( A @ ( A @ convergent_lines ) ),
inference(miniscope,[status(thm)],[154]) ).
thf(156,plain,
! [A: $i] :
~ ( A @ ( A @ convergent_lines ) ),
inference(cnf,[status(esa)],[155]) ).
thf(8867,plain,
( $false
| ( sk3 @ ( sk1 @ convergent_lines ) ) ),
inference(rewrite,[status(thm)],[8767,156]) ).
thf(8868,plain,
sk3 @ ( sk1 @ convergent_lines ),
inference(simp,[status(thm)],[8867]) ).
thf(32,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ convergent_lines ) )
=> ~ ( B @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ci4) ).
thf(140,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ convergent_lines ) )
=> ~ ( B @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(141,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) )
| ~ ( B @ ( A @ convergent_lines ) ) ),
inference(cnf,[status(esa)],[140]) ).
thf(8881,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ ( B @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8868,141]) ).
thf(8882,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ ( B @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[8881]) ).
thf(8883,plain,
~ ( sk3 @ ( sk3 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[8882:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 ))]]) ).
thf(4,axiom,
! [A: $i,B: $i,C: $i,D: $i] :
( ( C @ ( B @ distinct_lines ) )
=> ( ( D @ ( C @ unorthogonal_lines ) )
| ( D @ ( B @ unorthogonal_lines ) )
| ( C @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ouo1) ).
thf(45,plain,
! [A: $i,B: $i,C: $i,D: $i] :
( ( C @ ( B @ distinct_lines ) )
=> ( ( D @ ( C @ unorthogonal_lines ) )
| ( D @ ( B @ unorthogonal_lines ) )
| ( C @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(46,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ distinct_lines ) )
=> ( ! [D: $i] :
( ( D @ ( C @ unorthogonal_lines ) )
| ( D @ ( B @ unorthogonal_lines ) ) )
| ( C @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) ) ) ),
inference(miniscope,[status(thm)],[45]) ).
thf(47,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ unorthogonal_lines ) )
| ( D @ ( B @ unorthogonal_lines ) )
| ( C @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( C @ ( B @ distinct_lines ) ) ),
inference(cnf,[status(esa)],[46]) ).
thf(5,axiom,
! [A: $i,B: $i] :
~ ( B @ ( A @ ( B @ orthogonal_through_point ) @ unorthogonal_lines ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ooc1) ).
thf(48,plain,
! [A: $i,B: $i] :
~ ( B @ ( A @ ( B @ orthogonal_through_point ) @ unorthogonal_lines ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(49,plain,
~ ? [A: $i,B: $i] : ( B @ ( A @ ( B @ orthogonal_through_point ) @ unorthogonal_lines ) ),
inference(miniscope,[status(thm)],[48]) ).
thf(50,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ ( B @ orthogonal_through_point ) @ unorthogonal_lines ) ),
inference(cnf,[status(esa)],[49]) ).
thf(248,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( B @ unorthogonal_lines ) )
!= ( F @ ( E @ ( F @ orthogonal_through_point ) @ unorthogonal_lines ) ) )
| ~ $true
| ( D @ ( C @ unorthogonal_lines ) )
| ( C @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( C @ ( B @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[47,50]) ).
thf(249,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( B @ unorthogonal_lines ) )
!= ( F @ ( E @ ( F @ orthogonal_through_point ) @ unorthogonal_lines ) ) )
| ( D @ ( C @ unorthogonal_lines ) )
| ( C @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( C @ ( B @ distinct_lines ) ) ),
inference(simp,[status(thm)],[248]) ).
thf(250,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( B @ unorthogonal_lines ) )
| ( B @ ( A @ apart_point_and_line ) )
| ( D @ ( C @ orthogonal_through_point ) @ ( A @ apart_point_and_line ) )
| ~ ( B @ ( D @ ( C @ orthogonal_through_point ) @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[249:[bind(A,$thf( A )),bind(B,$thf( H @ ( D @ orthogonal_through_point ) )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( H )),bind(F,$thf( D ))]]) ).
thf(276,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( B @ unorthogonal_lines ) )
| ( B @ ( A @ apart_point_and_line ) )
| ( D @ ( C @ orthogonal_through_point ) @ ( A @ apart_point_and_line ) )
| ~ ( B @ ( D @ ( C @ orthogonal_through_point ) @ distinct_lines ) ) ),
inference(simp,[status(thm)],[250]) ).
thf(422,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( E @ ( D @ distinct_lines ) ) )
| ( F @ ( E @ unorthogonal_lines ) )
| ( F @ ( D @ unorthogonal_lines ) )
| ( E @ ( C @ apart_point_and_line ) )
| ( D @ ( C @ apart_point_and_line ) )
| ~ $true
| ( B @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[136,47]) ).
thf(423,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( E @ ( D @ distinct_lines ) ) )
| ( F @ ( E @ unorthogonal_lines ) )
| ( F @ ( D @ unorthogonal_lines ) )
| ( E @ ( C @ apart_point_and_line ) )
| ( D @ ( C @ apart_point_and_line ) )
| ( B @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[422]) ).
thf(424,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ unorthogonal_lines ) )
| ( D @ ( A @ unorthogonal_lines ) )
| ( B @ ( C @ apart_point_and_line ) )
| ( A @ ( C @ apart_point_and_line ) )
| ( B @ ( A @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[423:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( A )),bind(E,$thf( B ))]]) ).
thf(431,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( B @ unorthogonal_lines ) )
| ( D @ ( A @ unorthogonal_lines ) )
| ( B @ ( C @ apart_point_and_line ) )
| ( A @ ( C @ apart_point_and_line ) )
| ( B @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[424]) ).
thf(614,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ $true
| ( ( B @ ( C @ apart_point_and_line ) )
!= ( A @ ( C @ apart_point_and_line ) ) )
| ( D @ ( B @ unorthogonal_lines ) )
| ( D @ ( A @ unorthogonal_lines ) )
| ( A @ ( C @ apart_point_and_line ) )
| ( B @ ( A @ equal_lines ) ) ),
inference(eqfactor_ordered,[status(thm)],[431]) ).
thf(616,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ unorthogonal_lines ) )
| ( C @ ( A @ unorthogonal_lines ) )
| ( A @ ( B @ apart_point_and_line ) )
| ( A @ ( A @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[614:[bind(A,$thf( B ))]]) ).
thf(618,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ unorthogonal_lines ) )
| ( A @ ( B @ apart_point_and_line ) )
| ( A @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[616]) ).
thf(102,plain,
~ ? [A: $i,B: $i] :
( ~ ( B @ ( A @ unorthogonal_lines ) )
& ~ ( B @ ( A @ convergent_lines ) ) ),
inference(miniscope,[status(thm)],[101]) ).
thf(103,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unorthogonal_lines ) )
| ( B @ ( A @ convergent_lines ) ) ),
inference(cnf,[status(esa)],[102]) ).
thf(237,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unorthogonal_lines ) )
!= ( D @ ( C @ ( D @ orthogonal_through_point ) @ unorthogonal_lines ) ) )
| ~ $true
| ( B @ ( A @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[103,50]) ).
thf(238,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unorthogonal_lines ) )
!= ( D @ ( C @ ( D @ orthogonal_through_point ) @ unorthogonal_lines ) ) )
| ( B @ ( A @ convergent_lines ) ) ),
inference(simp,[status(thm)],[237]) ).
thf(239,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( A @ orthogonal_through_point ) @ convergent_lines ) ),
inference(pattern_uni,[status(thm)],[238:[bind(A,$thf( F @ ( B @ orthogonal_through_point ) )),bind(B,$thf( B )),bind(C,$thf( F )),bind(D,$thf( B ))]]) ).
thf(243,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( A @ orthogonal_through_point ) @ convergent_lines ) ),
inference(simp,[status(thm)],[239]) ).
thf(508,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ orthogonal_through_point ) @ convergent_lines ) )
!= ( D @ ( C @ convergent_lines ) ) )
| ~ ( D @ ( D @ ( C @ intersection_point ) @ apart_point_and_line ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[243,141]) ).
thf(509,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ orthogonal_through_point ) @ convergent_lines ) )
!= ( D @ ( C @ convergent_lines ) ) )
| ~ ( D @ ( D @ ( C @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[508]) ).
thf(510,plain,
! [B: $i,A: $i] :
~ ( A @ ( A @ ( B @ ( A @ orthogonal_through_point ) @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[509:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F @ ( E @ orthogonal_through_point ) )),bind(D,$thf( E ))]]) ).
thf(536,plain,
! [B: $i,A: $i] :
~ ( A @ ( A @ ( B @ ( A @ orthogonal_through_point ) @ intersection_point ) @ apart_point_and_line ) ),
inference(simp,[status(thm)],[510]) ).
thf(1041,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ apart_point_and_line ) )
!= ( D @ ( D @ ( E @ ( D @ orthogonal_through_point ) @ intersection_point ) @ apart_point_and_line ) ) )
| ~ $true
| ( C @ ( A @ unorthogonal_lines ) )
| ( A @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[618,536]) ).
thf(1042,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ apart_point_and_line ) )
!= ( D @ ( D @ ( E @ ( D @ orthogonal_through_point ) @ intersection_point ) @ apart_point_and_line ) ) )
| ( C @ ( A @ unorthogonal_lines ) )
| ( A @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[1041]) ).
thf(1043,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unorthogonal_lines ) )
| ( A @ ( A @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[1042:[bind(A,$thf( A )),bind(B,$thf( A @ ( I @ ( A @ orthogonal_through_point ) @ intersection_point ) )),bind(C,$thf( C )),bind(D,$thf( A )),bind(E,$thf( I ))]]) ).
thf(1048,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unorthogonal_lines ) )
| ( A @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[1043]) ).
thf(8,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ orthogonal_lines ) )
<=> ~ ( B @ ( A @ unorthogonal_lines ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a5) ).
thf(56,plain,
! [A: $i,B: $i] :
( ( ~ ( B @ ( A @ unorthogonal_lines ) )
=> ( B @ ( A @ orthogonal_lines ) ) )
& ( ( B @ ( A @ orthogonal_lines ) )
=> ~ ( B @ ( A @ unorthogonal_lines ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(57,plain,
( ! [A: $i,B: $i] :
( ~ ( B @ ( A @ unorthogonal_lines ) )
=> ( B @ ( A @ orthogonal_lines ) ) )
& ! [A: $i,B: $i] :
( ( B @ ( A @ orthogonal_lines ) )
=> ~ ( B @ ( A @ unorthogonal_lines ) ) ) ),
inference(miniscope,[status(thm)],[56]) ).
thf(58,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ orthogonal_lines ) )
| ( D @ ( C @ unorthogonal_lines ) ) )
& ( ~ ( B @ ( A @ unorthogonal_lines ) )
| ~ ( B @ ( A @ orthogonal_lines ) ) ) ),
inference(cnf,[status(esa)],[57]) ).
thf(59,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ unorthogonal_lines ) )
| ~ ( B @ ( A @ orthogonal_lines ) ) ),
inference(cnfConj,[status(thm)],[58]) ).
thf(1140,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unorthogonal_lines ) )
!= ( D @ ( C @ unorthogonal_lines ) ) )
| ~ $true
| ~ ( D @ ( C @ orthogonal_lines ) )
| ( A @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1048,59]) ).
thf(1141,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unorthogonal_lines ) )
!= ( D @ ( C @ unorthogonal_lines ) ) )
| ~ ( D @ ( C @ orthogonal_lines ) )
| ( A @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[1140]) ).
thf(1142,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ orthogonal_lines ) )
| ( A @ ( A @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[1141:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(267,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ unorthogonal_lines ) )
!= ( F @ ( E @ unorthogonal_lines ) ) )
| ~ $true
| ~ ( F @ ( E @ orthogonal_lines ) )
| ( D @ ( B @ unorthogonal_lines ) )
| ( C @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( C @ ( B @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[47,59]) ).
thf(268,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ unorthogonal_lines ) )
!= ( F @ ( E @ unorthogonal_lines ) ) )
| ~ ( F @ ( E @ orthogonal_lines ) )
| ( D @ ( B @ unorthogonal_lines ) )
| ( C @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( C @ ( B @ distinct_lines ) ) ),
inference(simp,[status(thm)],[267]) ).
thf(269,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( D @ ( C @ orthogonal_lines ) )
| ( D @ ( B @ unorthogonal_lines ) )
| ( C @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( C @ ( B @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[268:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( C )),bind(F,$thf( D ))]]) ).
thf(1671,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ distinct_lines ) )
!= ( sk3 @ ( sk2 @ distinct_lines ) ) )
| ~ $true
| ( C @ ( B @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[77,410]) ).
thf(1672,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ distinct_lines ) )
!= ( sk3 @ ( sk2 @ distinct_lines ) ) )
| ( C @ ( B @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_lines ) ) ),
inference(simp,[status(thm)],[1671]) ).
thf(1673,plain,
! [A: $i] :
( ( sk3 @ ( A @ distinct_lines ) )
| ~ ( A @ ( sk2 @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[1672:[bind(A,$thf( sk2 )),bind(B,$thf( B )),bind(C,$thf( sk3 ))]]) ).
thf(1691,plain,
! [A: $i] :
( ( sk3 @ ( A @ distinct_lines ) )
| ~ ( A @ ( sk2 @ distinct_lines ) ) ),
inference(simp,[status(thm)],[1673]) ).
thf(2143,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( A @ distinct_lines ) )
!= ( sk3 @ ( B @ distinct_lines ) ) )
| ( sk2 @ ( B @ distinct_lines ) )
| ~ $true
| ~ ( A @ ( sk2 @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1691,1765]) ).
thf(2144,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( A @ distinct_lines ) )
!= ( sk3 @ ( B @ distinct_lines ) ) )
| ( sk2 @ ( B @ distinct_lines ) )
| ~ ( A @ ( sk2 @ distinct_lines ) ) ),
inference(simp,[status(thm)],[2143]) ).
thf(2145,plain,
! [A: $i] :
( ( sk2 @ ( A @ distinct_lines ) )
| ~ ( A @ ( sk2 @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[2144:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(3133,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ~ $true
| ~ ( C @ ( B @ equal_lines ) )
| ~ ( A @ ( sk2 @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[2145,134]) ).
thf(3134,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ~ ( C @ ( B @ equal_lines ) )
| ~ ( A @ ( sk2 @ distinct_lines ) ) ),
inference(simp,[status(thm)],[3133]) ).
thf(3135,plain,
! [A: $i] :
( ~ ( sk2 @ ( A @ equal_lines ) )
| ~ ( A @ ( sk2 @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[3134:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk2 ))]]) ).
thf(33,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ convergent_lines ) )
=> ~ ( A @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ci3) ).
thf(142,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ convergent_lines ) )
=> ~ ( A @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(280,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ orthogonal_through_point ) @ convergent_lines ) )
!= ( C @ ( C @ convergent_lines ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[243,156]) ).
thf(281,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ ( A @ orthogonal_through_point ) @ convergent_lines ) )
!= ( C @ ( C @ convergent_lines ) ) ),
inference(simp,[status(thm)],[280]) ).
thf(285,plain,
! [C: $i,B: $i,A: $i] :
( ( A != C )
| ( ( B @ ( A @ orthogonal_through_point ) )
!= C ) ),
inference(simp,[status(thm)],[281]) ).
thf(288,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ orthogonal_through_point ) )
!= A ),
inference(simp,[status(thm)],[285]) ).
thf(3287,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ distinct_lines ) )
!= ( sk3 @ ( sk2 @ distinct_lines ) ) )
| ~ $true
| ( C @ ( A @ convergent_lines ) )
| ~ ( B @ ( A @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[139,410]) ).
thf(3288,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ distinct_lines ) )
!= ( sk3 @ ( sk2 @ distinct_lines ) ) )
| ( C @ ( A @ convergent_lines ) )
| ~ ( B @ ( A @ convergent_lines ) ) ),
inference(simp,[status(thm)],[3287]) ).
thf(3289,plain,
! [A: $i] :
( ( sk3 @ ( A @ convergent_lines ) )
| ~ ( sk2 @ ( A @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[3288:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( sk3 ))]]) ).
thf(10964,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ orthogonal_through_point ) @ convergent_lines ) )
!= ( sk2 @ ( C @ convergent_lines ) ) )
| ( sk3 @ ( C @ convergent_lines ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[243,3289]) ).
thf(10965,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ orthogonal_through_point ) @ convergent_lines ) )
!= ( sk2 @ ( C @ convergent_lines ) ) )
| ( sk3 @ ( C @ convergent_lines ) ) ),
inference(simp,[status(thm)],[10964]) ).
thf(10966,plain,
! [A: $i] : ( sk3 @ ( A @ ( sk2 @ orthogonal_through_point ) @ convergent_lines ) ),
inference(pattern_uni,[status(thm)],[10965:[bind(A,$thf( sk2 )),bind(B,$thf( E )),bind(C,$thf( E @ ( sk2 @ orthogonal_through_point ) ))]]) ).
thf(11041,plain,
! [A: $i] : ( sk3 @ ( A @ ( sk2 @ orthogonal_through_point ) @ convergent_lines ) ),
inference(simp,[status(thm)],[10966]) ).
thf(25,axiom,
! [A: $i,B: $i] :
~ ( B @ ( A @ ( B @ parallel_through_point ) @ convergent_lines ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cp1) ).
thf(110,plain,
! [A: $i,B: $i] :
~ ( B @ ( A @ ( B @ parallel_through_point ) @ convergent_lines ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(111,plain,
~ ? [A: $i,B: $i] : ( B @ ( A @ ( B @ parallel_through_point ) @ convergent_lines ) ),
inference(miniscope,[status(thm)],[110]) ).
thf(112,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ ( B @ parallel_through_point ) @ convergent_lines ) ),
inference(cnf,[status(esa)],[111]) ).
thf(11541,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ ( sk2 @ orthogonal_through_point ) @ convergent_lines ) )
!= ( C @ ( B @ ( C @ parallel_through_point ) @ convergent_lines ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[11041,112]) ).
thf(11542,plain,
! [C: $i,B: $i,A: $i] :
( ( sk3 @ ( A @ ( sk2 @ orthogonal_through_point ) @ convergent_lines ) )
!= ( C @ ( B @ ( C @ parallel_through_point ) @ convergent_lines ) ) ),
inference(simp,[status(thm)],[11541]) ).
thf(11573,plain,
! [C: $i,B: $i,A: $i] :
( ( sk3 != C )
| ( ( A @ ( sk2 @ orthogonal_through_point ) )
!= ( B @ ( C @ parallel_through_point ) ) ) ),
inference(simp,[status(thm)],[11542]) ).
thf(11588,plain,
! [B: $i,A: $i] :
( ( A @ ( sk2 @ orthogonal_through_point ) )
!= ( B @ ( sk3 @ parallel_through_point ) ) ),
inference(simp,[status(thm)],[11573]) ).
thf(3101,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ( C @ ( B @ convergent_lines ) )
| ~ $true
| ~ ( A @ ( sk2 @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[2145,147]) ).
thf(3102,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ( C @ ( B @ convergent_lines ) )
| ~ ( A @ ( sk2 @ distinct_lines ) ) ),
inference(simp,[status(thm)],[3101]) ).
thf(3103,plain,
! [A: $i] :
( ( sk2 @ ( A @ convergent_lines ) )
| ~ ( A @ ( sk2 @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[3102:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk2 ))]]) ).
thf(8762,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ orthogonal_through_point ) @ convergent_lines ) )
!= ( sk3 @ ( C @ convergent_lines ) ) )
| ( sk2 @ ( C @ convergent_lines ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[243,3256]) ).
thf(8763,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ orthogonal_through_point ) @ convergent_lines ) )
!= ( sk3 @ ( C @ convergent_lines ) ) )
| ( sk2 @ ( C @ convergent_lines ) ) ),
inference(simp,[status(thm)],[8762]) ).
thf(8764,plain,
! [A: $i] : ( sk2 @ ( A @ ( sk3 @ orthogonal_through_point ) @ convergent_lines ) ),
inference(pattern_uni,[status(thm)],[8763:[bind(A,$thf( sk3 )),bind(B,$thf( E )),bind(C,$thf( E @ ( sk3 @ orthogonal_through_point ) ))]]) ).
thf(8788,plain,
! [A: $i] : ( sk2 @ ( A @ ( sk3 @ orthogonal_through_point ) @ convergent_lines ) ),
inference(simp,[status(thm)],[8764]) ).
thf(8807,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ ( sk3 @ orthogonal_through_point ) @ convergent_lines ) )
!= ( C @ ( B @ ( C @ parallel_through_point ) @ convergent_lines ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8788,112]) ).
thf(8808,plain,
! [C: $i,B: $i,A: $i] :
( ( sk2 @ ( A @ ( sk3 @ orthogonal_through_point ) @ convergent_lines ) )
!= ( C @ ( B @ ( C @ parallel_through_point ) @ convergent_lines ) ) ),
inference(simp,[status(thm)],[8807]) ).
thf(8840,plain,
! [C: $i,B: $i,A: $i] :
( ( sk2 != C )
| ( ( A @ ( sk3 @ orthogonal_through_point ) )
!= ( B @ ( C @ parallel_through_point ) ) ) ),
inference(simp,[status(thm)],[8808]) ).
thf(8851,plain,
! [B: $i,A: $i] :
( ( A @ ( sk3 @ orthogonal_through_point ) )
!= ( B @ ( sk2 @ parallel_through_point ) ) ),
inference(simp,[status(thm)],[8840]) ).
thf(1707,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ( C @ ( B @ convergent_lines ) )
| ~ $true
| ~ ( sk2 @ ( A @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1676,147]) ).
thf(1708,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ( C @ ( B @ convergent_lines ) )
| ~ ( sk2 @ ( A @ distinct_lines ) ) ),
inference(simp,[status(thm)],[1707]) ).
thf(1709,plain,
! [A: $i] :
( ( sk3 @ ( A @ convergent_lines ) )
| ~ ( sk2 @ ( A @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[1708:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk3 ))]]) ).
thf(2183,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ( C @ ( B @ convergent_lines ) )
| ~ $true
| ~ ( A @ ( sk3 @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1775,147]) ).
thf(2184,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ( C @ ( B @ convergent_lines ) )
| ~ ( A @ ( sk3 @ distinct_lines ) ) ),
inference(simp,[status(thm)],[2183]) ).
thf(2185,plain,
! [A: $i] :
( ( sk2 @ ( A @ convergent_lines ) )
| ~ ( A @ ( sk3 @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[2184:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk2 ))]]) ).
thf(1915,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ~ $true
| ~ ( C @ ( B @ equal_lines ) )
| ~ ( A @ ( sk2 @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1691,134]) ).
thf(1916,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ~ ( C @ ( B @ equal_lines ) )
| ~ ( A @ ( sk2 @ distinct_lines ) ) ),
inference(simp,[status(thm)],[1915]) ).
thf(1917,plain,
! [A: $i] :
( ~ ( sk3 @ ( A @ equal_lines ) )
| ~ ( A @ ( sk2 @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[1916:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk3 ))]]) ).
thf(1981,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ parallel_through_point ) @ ( A @ distinct_lines ) )
!= ( D @ ( sk2 @ distinct_lines ) ) )
| ~ ( sk3 @ ( D @ equal_lines ) )
| ~ $true
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[345,1917]) ).
thf(1982,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ parallel_through_point ) @ ( A @ distinct_lines ) )
!= ( D @ ( sk2 @ distinct_lines ) ) )
| ~ ( sk3 @ ( D @ equal_lines ) )
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[1981]) ).
thf(1983,plain,
! [B: $i,A: $i] :
( ~ ( sk3 @ ( B @ ( A @ parallel_through_point ) @ equal_lines ) )
| ~ ( sk2 @ ( B @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[1982:[bind(A,$thf( sk2 )),bind(B,$thf( E )),bind(C,$thf( F )),bind(D,$thf( F @ ( E @ parallel_through_point ) ))]]) ).
thf(2000,plain,
! [B: $i,A: $i] :
( ~ ( sk3 @ ( B @ ( A @ parallel_through_point ) @ equal_lines ) )
| ~ ( sk2 @ ( B @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[1983]) ).
thf(2850,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( B @ ( A @ parallel_through_point ) @ equal_lines ) )
!= ( sk3 @ ( sk2 @ equal_lines ) ) )
| ~ $true
| ~ ( sk2 @ ( B @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[41,2000]) ).
thf(2851,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( B @ ( A @ parallel_through_point ) @ equal_lines ) )
!= ( sk3 @ ( sk2 @ equal_lines ) ) )
| ~ ( sk2 @ ( B @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[2850]) ).
thf(2889,plain,
! [B: $i,A: $i] :
( ( sk3 != sk3 )
| ( ( B @ ( A @ parallel_through_point ) )
!= sk2 )
| ~ ( sk2 @ ( B @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[2851]) ).
thf(2897,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ parallel_through_point ) )
!= sk2 )
| ~ ( sk2 @ ( B @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[2889]) ).
thf(15,axiom,
! [A: $i,B: $i] :
~ ( A @ ( B @ orthogonal_through_point ) @ ( A @ apart_point_and_line ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ooc2) ).
thf(78,plain,
! [A: $i,B: $i] :
~ ( A @ ( B @ orthogonal_through_point ) @ ( A @ apart_point_and_line ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(79,plain,
~ ? [A: $i,B: $i] : ( A @ ( B @ orthogonal_through_point ) @ ( A @ apart_point_and_line ) ),
inference(miniscope,[status(thm)],[78]) ).
thf(80,plain,
! [B: $i,A: $i] :
~ ( A @ ( B @ orthogonal_through_point ) @ ( A @ apart_point_and_line ) ),
inference(cnf,[status(esa)],[79]) ).
thf(183,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( E @ ( F @ orthogonal_through_point ) @ ( E @ apart_point_and_line ) ) )
| ~ $true
| ( D @ ( B @ apart_point_and_line ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(paramod_ordered,[status(thm)],[44,80]) ).
thf(184,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( E @ ( F @ orthogonal_through_point ) @ ( E @ apart_point_and_line ) ) )
| ( D @ ( B @ apart_point_and_line ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[183]) ).
thf(185,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ apart_point_and_line ) )
| ( D @ ( C @ orthogonal_through_point ) @ ( A @ apart_point_and_line ) )
| ( B @ ( D @ apart_point_and_line ) )
| ~ ( B @ ( D @ ( C @ orthogonal_through_point ) @ distinct_lines ) )
| ~ ( A @ ( D @ distinct_points ) ) ),
inference(pattern_uni,[status(thm)],[184:[bind(A,$thf( H )),bind(B,$thf( B )),bind(C,$thf( H @ ( G @ orthogonal_through_point ) )),bind(D,$thf( D )),bind(E,$thf( H )),bind(F,$thf( G ))]]) ).
thf(196,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ apart_point_and_line ) )
| ( D @ ( C @ orthogonal_through_point ) @ ( A @ apart_point_and_line ) )
| ( B @ ( D @ apart_point_and_line ) )
| ~ ( B @ ( D @ ( C @ orthogonal_through_point ) @ distinct_lines ) )
| ~ ( A @ ( D @ distinct_points ) ) ),
inference(simp,[status(thm)],[185]) ).
thf(526,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ ( B @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[40,141]) ).
thf(527,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ ( B @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[526]) ).
thf(528,plain,
~ ( sk2 @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[527:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(537,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( sk2 @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) )
| ~ $true
| ( C @ ( B @ distinct_lines ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[53,528]) ).
thf(538,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( sk2 @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) )
| ( C @ ( B @ distinct_lines ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[537]) ).
thf(539,plain,
! [A: $i] :
( ( sk2 @ ( A @ distinct_lines ) )
| ~ ( A @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[538:[bind(A,$thf( sk2 @ ( sk1 @ intersection_point ) )),bind(B,$thf( B )),bind(C,$thf( sk2 ))]]) ).
thf(559,plain,
! [A: $i] :
( ( sk2 @ ( A @ distinct_lines ) )
| ~ ( A @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[539]) ).
thf(1890,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ( C @ ( B @ convergent_lines ) )
| ~ $true
| ~ ( A @ ( sk2 @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1691,147]) ).
thf(1891,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ( C @ ( B @ convergent_lines ) )
| ~ ( A @ ( sk2 @ distinct_lines ) ) ),
inference(simp,[status(thm)],[1890]) ).
thf(1892,plain,
! [A: $i] :
( ( sk3 @ ( A @ convergent_lines ) )
| ~ ( A @ ( sk2 @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[1891:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk3 ))]]) ).
thf(3361,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ~ $true
| ~ ( C @ ( B @ equal_lines ) )
| ( sk3 @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[2164,134]) ).
thf(3362,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ~ ( C @ ( B @ equal_lines ) )
| ( sk3 @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[3361]) ).
thf(3363,plain,
! [A: $i] :
( ~ ( sk2 @ ( A @ equal_lines ) )
| ( sk3 @ ( A @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[3362:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk2 ))]]) ).
thf(13940,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ equal_lines ) )
!= ( C @ ( B @ equal_lines ) ) )
| ~ ( C @ ( B @ distinct_lines ) )
| ~ $true
| ~ ( sk2 @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[3363,134]) ).
thf(13941,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ equal_lines ) )
!= ( C @ ( B @ equal_lines ) ) )
| ~ ( C @ ( B @ distinct_lines ) )
| ~ ( sk2 @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[13940]) ).
thf(13942,plain,
! [A: $i] :
( ~ ( sk3 @ ( A @ distinct_lines ) )
| ~ ( sk2 @ ( A @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[13941:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk3 ))]]) ).
thf(36,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( ~ ( C @ ( A @ unorthogonal_lines ) )
| ~ ( C @ ( A @ convergent_lines ) ) )
& ( ~ ( B @ ( A @ unorthogonal_lines ) )
| ~ ( B @ ( A @ convergent_lines ) ) ) )
=> ( ~ ( C @ ( B @ unorthogonal_lines ) )
| ~ ( C @ ( B @ convergent_lines ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cotno1) ).
thf(148,plain,
! [A: $i,B: $i,C: $i] :
( ( ( ~ ( C @ ( A @ unorthogonal_lines ) )
| ~ ( C @ ( A @ convergent_lines ) ) )
& ( ~ ( B @ ( A @ unorthogonal_lines ) )
| ~ ( B @ ( A @ convergent_lines ) ) ) )
=> ( ~ ( C @ ( B @ unorthogonal_lines ) )
| ~ ( C @ ( B @ convergent_lines ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(149,plain,
! [C: $i,B: $i,A: $i] :
( ( ~ ( C @ ( B @ unorthogonal_lines ) )
| ~ ( C @ ( B @ convergent_lines ) )
| ( C @ ( A @ unorthogonal_lines ) )
| ( B @ ( A @ unorthogonal_lines ) ) )
& ( ~ ( C @ ( B @ unorthogonal_lines ) )
| ~ ( C @ ( B @ convergent_lines ) )
| ( C @ ( A @ convergent_lines ) )
| ( B @ ( A @ unorthogonal_lines ) ) )
& ( ~ ( C @ ( B @ unorthogonal_lines ) )
| ~ ( C @ ( B @ convergent_lines ) )
| ( C @ ( A @ unorthogonal_lines ) )
| ( B @ ( A @ convergent_lines ) ) )
& ( ~ ( C @ ( B @ unorthogonal_lines ) )
| ~ ( C @ ( B @ convergent_lines ) )
| ( C @ ( A @ convergent_lines ) )
| ( B @ ( A @ convergent_lines ) ) ) ),
inference(cnf,[status(esa)],[148]) ).
thf(152,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ unorthogonal_lines ) )
| ~ ( C @ ( B @ convergent_lines ) )
| ( C @ ( A @ convergent_lines ) )
| ( B @ ( A @ unorthogonal_lines ) ) ),
inference(cnfConj,[status(thm)],[149]) ).
thf(282,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ orthogonal_through_point ) @ convergent_lines ) )
!= ( D @ ( C @ ( D @ parallel_through_point ) @ convergent_lines ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[243,112]) ).
thf(283,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A @ ( B @ ( A @ orthogonal_through_point ) @ convergent_lines ) )
!= ( D @ ( C @ ( D @ parallel_through_point ) @ convergent_lines ) ) ),
inference(simp,[status(thm)],[282]) ).
thf(286,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( A != D )
| ( ( B @ ( A @ orthogonal_through_point ) )
!= ( C @ ( D @ parallel_through_point ) ) ) ),
inference(simp,[status(thm)],[283]) ).
thf(289,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ orthogonal_through_point ) )
!= ( B @ ( C @ parallel_through_point ) ) ),
inference(simp,[status(thm)],[286]) ).
thf(42,plain,
( ~ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ equal_points ) )
| ~ ( sk3 @ ( sk1 @ convergent_lines ) ) ),
inference(cnfConj,[status(thm)],[39]) ).
thf(8869,plain,
( ~ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ equal_points ) )
| ~ $true ),
inference(rewrite,[status(thm)],[42,8868]) ).
thf(8870,plain,
~ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ equal_points ) ),
inference(simp,[status(thm)],[8869]) ).
thf(161,plain,
! [A: $i] :
( ( ( sk2 @ ( sk1 @ convergent_lines ) )
!= ( A @ ( A @ convergent_lines ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[40,156]) ).
thf(162,plain,
! [A: $i] :
( ( sk2 @ ( sk1 @ convergent_lines ) )
!= ( A @ ( A @ convergent_lines ) ) ),
inference(simp,[status(thm)],[161]) ).
thf(163,plain,
! [A: $i] :
( ( sk2 != A )
| ( sk1 != A ) ),
inference(simp,[status(thm)],[162]) ).
thf(164,plain,
sk2 != sk1,
inference(simp,[status(thm)],[163]) ).
thf(1704,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ~ $true
| ~ ( C @ ( B @ equal_lines ) )
| ~ ( sk2 @ ( A @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1676,134]) ).
thf(1705,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ~ ( C @ ( B @ equal_lines ) )
| ~ ( sk2 @ ( A @ distinct_lines ) ) ),
inference(simp,[status(thm)],[1704]) ).
thf(1706,plain,
! [A: $i] :
( ~ ( sk3 @ ( A @ equal_lines ) )
| ~ ( sk2 @ ( A @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[1705:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk3 ))]]) ).
thf(2226,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( sk2 @ ( B @ distinct_lines ) ) )
| ~ ( sk3 @ ( B @ equal_lines ) )
| ~ $true
| ~ ( A @ ( sk3 @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1775,1706]) ).
thf(2227,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( sk2 @ ( B @ distinct_lines ) ) )
| ~ ( sk3 @ ( B @ equal_lines ) )
| ~ ( A @ ( sk3 @ distinct_lines ) ) ),
inference(simp,[status(thm)],[2226]) ).
thf(2228,plain,
! [A: $i] :
( ~ ( sk3 @ ( A @ equal_lines ) )
| ~ ( A @ ( sk3 @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[2227:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(2443,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( sk3 @ distinct_lines ) ) )
| ~ ( sk3 @ ( C @ equal_lines ) )
| ~ $true
| ( B @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[136,2228]) ).
thf(2444,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( sk3 @ distinct_lines ) ) )
| ~ ( sk3 @ ( C @ equal_lines ) )
| ( B @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[2443]) ).
thf(2445,plain,
! [A: $i] :
( ~ ( sk3 @ ( A @ equal_lines ) )
| ( A @ ( sk3 @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[2444:[bind(A,$thf( sk3 )),bind(B,$thf( B )),bind(C,$thf( B ))]]) ).
thf(2451,plain,
! [A: $i] :
( ~ ( sk3 @ ( A @ equal_lines ) )
| ( A @ ( sk3 @ equal_lines ) ) ),
inference(simp,[status(thm)],[2445]) ).
thf(208,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( B @ apart_point_and_line ) )
!= ( E @ ( F @ parallel_through_point ) @ ( E @ apart_point_and_line ) ) )
| ~ $true
| ( C @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(paramod_ordered,[status(thm)],[44,83]) ).
thf(209,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( B @ apart_point_and_line ) )
!= ( E @ ( F @ parallel_through_point ) @ ( E @ apart_point_and_line ) ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[208]) ).
thf(210,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( D @ apart_point_and_line ) )
| ( D @ ( C @ parallel_through_point ) @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ parallel_through_point ) @ ( B @ distinct_lines ) )
| ~ ( D @ ( A @ distinct_points ) ) ),
inference(pattern_uni,[status(thm)],[209:[bind(A,$thf( A )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( G @ parallel_through_point ) )),bind(E,$thf( H )),bind(F,$thf( G ))]]) ).
thf(211,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( D @ apart_point_and_line ) )
| ( D @ ( C @ parallel_through_point ) @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ parallel_through_point ) @ ( B @ distinct_lines ) )
| ~ ( D @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[210]) ).
thf(17,axiom,
! [A: $i,B: $i] :
( ( ( B @ point )
& ( A @ line ) )
=> ( B @ ( A @ orthogonal_through_point ) @ line ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',orth1) ).
thf(84,plain,
! [A: $i,B: $i] :
( ( ( B @ point )
& ( A @ line ) )
=> ( B @ ( A @ orthogonal_through_point ) @ line ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(10970,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( A @ convergent_lines ) )
!= ( B @ ( B @ convergent_lines ) ) )
| ~ $true
| ~ ( sk2 @ ( A @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[3289,156]) ).
thf(10971,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( A @ convergent_lines ) )
!= ( B @ ( B @ convergent_lines ) ) )
| ~ ( sk2 @ ( A @ convergent_lines ) ) ),
inference(simp,[status(thm)],[10970]) ).
thf(10972,plain,
~ ( sk2 @ ( sk3 @ convergent_lines ) ),
inference(pattern_uni,[status(thm)],[10971:[bind(A,$thf( sk3 )),bind(B,$thf( sk3 ))]]) ).
thf(336,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( A @ apart_point_and_line ) )
!= ( F @ ( E @ apart_point_and_line ) ) )
| ( G @ ( E @ apart_point_and_line ) )
| ( G @ ( F @ distinct_lines ) )
| ~ $true
| ( D @ ( B @ apart_point_and_line ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(paramod_ordered,[status(thm)],[44,53]) ).
thf(337,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( A @ apart_point_and_line ) )
!= ( F @ ( E @ apart_point_and_line ) ) )
| ( G @ ( E @ apart_point_and_line ) )
| ( G @ ( F @ distinct_lines ) )
| ( D @ ( B @ apart_point_and_line ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[336]) ).
thf(338,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( A @ apart_point_and_line ) )
| ( E @ ( D @ distinct_lines ) )
| ( D @ ( B @ apart_point_and_line ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(pattern_uni,[status(thm)],[337:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( A )),bind(F,$thf( D ))]]) ).
thf(348,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( A @ apart_point_and_line ) )
| ( E @ ( D @ distinct_lines ) )
| ( D @ ( B @ apart_point_and_line ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[338]) ).
thf(10986,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ convergent_lines ) )
!= ( C @ ( B @ ( C @ parallel_through_point ) @ convergent_lines ) ) )
| ~ $true
| ~ ( sk2 @ ( A @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[3289,112]) ).
thf(10987,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ convergent_lines ) )
!= ( C @ ( B @ ( C @ parallel_through_point ) @ convergent_lines ) ) )
| ~ ( sk2 @ ( A @ convergent_lines ) ) ),
inference(simp,[status(thm)],[10986]) ).
thf(10988,plain,
! [A: $i] :
~ ( sk2 @ ( A @ ( sk3 @ parallel_through_point ) @ convergent_lines ) ),
inference(pattern_uni,[status(thm)],[10987:[bind(A,$thf( E @ ( sk3 @ parallel_through_point ) )),bind(B,$thf( E )),bind(C,$thf( sk3 ))]]) ).
thf(11047,plain,
! [A: $i] :
~ ( sk2 @ ( A @ ( sk3 @ parallel_through_point ) @ convergent_lines ) ),
inference(simp,[status(thm)],[10988]) ).
thf(60,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ orthogonal_lines ) )
| ( B @ ( A @ unorthogonal_lines ) ) ),
inference(cnfConj,[status(thm)],[58]) ).
thf(61,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ orthogonal_lines ) )
| ( B @ ( A @ unorthogonal_lines ) ) ),
inference(simp,[status(thm)],[60]) ).
thf(18,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ incident_point_and_line ) )
<=> ~ ( B @ ( A @ apart_point_and_line ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a4) ).
thf(86,plain,
! [A: $i,B: $i] :
( ( ~ ( B @ ( A @ apart_point_and_line ) )
=> ( B @ ( A @ incident_point_and_line ) ) )
& ( ( B @ ( A @ incident_point_and_line ) )
=> ~ ( B @ ( A @ apart_point_and_line ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(87,plain,
( ! [A: $i,B: $i] :
( ~ ( B @ ( A @ apart_point_and_line ) )
=> ( B @ ( A @ incident_point_and_line ) ) )
& ! [A: $i,B: $i] :
( ( B @ ( A @ incident_point_and_line ) )
=> ~ ( B @ ( A @ apart_point_and_line ) ) ) ),
inference(miniscope,[status(thm)],[86]) ).
thf(88,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ incident_point_and_line ) )
| ( D @ ( C @ apart_point_and_line ) ) )
& ( ~ ( B @ ( A @ apart_point_and_line ) )
| ~ ( B @ ( A @ incident_point_and_line ) ) ) ),
inference(cnf,[status(esa)],[87]) ).
thf(89,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ apart_point_and_line ) )
| ~ ( B @ ( A @ incident_point_and_line ) ) ),
inference(cnfConj,[status(thm)],[88]) ).
thf(116,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ distinct_points ) )
| ~ ( B @ ( A @ equal_points ) ) ),
inference(cnfConj,[status(thm)],[115]) ).
thf(24,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ parallel_lines ) )
<=> ~ ( B @ ( A @ convergent_lines ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a3) ).
thf(104,plain,
! [A: $i,B: $i] :
( ( ~ ( B @ ( A @ convergent_lines ) )
=> ( B @ ( A @ parallel_lines ) ) )
& ( ( B @ ( A @ parallel_lines ) )
=> ~ ( B @ ( A @ convergent_lines ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(105,plain,
( ! [A: $i,B: $i] :
( ~ ( B @ ( A @ convergent_lines ) )
=> ( B @ ( A @ parallel_lines ) ) )
& ! [A: $i,B: $i] :
( ( B @ ( A @ parallel_lines ) )
=> ~ ( B @ ( A @ convergent_lines ) ) ) ),
inference(miniscope,[status(thm)],[104]) ).
thf(106,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ parallel_lines ) )
| ( D @ ( C @ convergent_lines ) ) )
& ( ~ ( B @ ( A @ convergent_lines ) )
| ~ ( B @ ( A @ parallel_lines ) ) ) ),
inference(cnf,[status(esa)],[105]) ).
thf(107,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ convergent_lines ) )
| ~ ( B @ ( A @ parallel_lines ) ) ),
inference(cnfConj,[status(thm)],[106]) ).
thf(290,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ $true
| ~ ( B @ ( A @ parallel_lines ) ) ),
inference(paramod_ordered,[status(thm)],[40,107]) ).
thf(291,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ ( B @ ( A @ parallel_lines ) ) ),
inference(simp,[status(thm)],[290]) ).
thf(292,plain,
~ ( sk2 @ ( sk1 @ parallel_lines ) ),
inference(pattern_uni,[status(thm)],[291:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(143,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) )
| ~ ( B @ ( A @ convergent_lines ) ) ),
inference(cnf,[status(esa)],[142]) ).
thf(918,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ ( A @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[40,143]) ).
thf(919,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ ( A @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[918]) ).
thf(920,plain,
~ ( sk1 @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[919:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(85,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ orthogonal_through_point ) @ line )
| ~ ( B @ point )
| ~ ( A @ line ) ),
inference(cnf,[status(esa)],[84]) ).
thf(1186,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ parallel_through_point ) @ ( A @ distinct_lines ) )
!= ( sk3 @ ( sk2 @ distinct_lines ) ) )
| ~ $true
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[345,410]) ).
thf(1187,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ parallel_through_point ) @ ( A @ distinct_lines ) )
!= ( sk3 @ ( sk2 @ distinct_lines ) ) )
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[1186]) ).
thf(1197,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ parallel_through_point ) )
!= sk3 )
| ( A != sk2 )
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[1187]) ).
thf(1206,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ parallel_through_point ) )
!= sk3 )
| ~ ( sk2 @ ( B @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[1197]) ).
thf(231,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ apart_point_and_line ) )
!= ( F @ ( E @ apart_point_and_line ) ) )
| ~ $true
| ~ ( F @ ( E @ incident_point_and_line ) )
| ( D @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(paramod_ordered,[status(thm)],[44,89]) ).
thf(232,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ apart_point_and_line ) )
!= ( F @ ( E @ apart_point_and_line ) ) )
| ~ ( F @ ( E @ incident_point_and_line ) )
| ( D @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[231]) ).
thf(233,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ incident_point_and_line ) )
| ( D @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(pattern_uni,[status(thm)],[232:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( B )),bind(F,$thf( C ))]]) ).
thf(8887,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ parallel_through_point ) @ convergent_lines ) )
!= ( sk3 @ ( sk1 @ convergent_lines ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8868,112]) ).
thf(8888,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( B @ parallel_through_point ) @ convergent_lines ) )
!= ( sk3 @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[8887]) ).
thf(8920,plain,
! [B: $i,A: $i] :
( ( B != sk3 )
| ( ( A @ ( B @ parallel_through_point ) )
!= sk1 ) ),
inference(simp,[status(thm)],[8888]) ).
thf(8927,plain,
! [A: $i] :
( ( A @ ( sk3 @ parallel_through_point ) )
!= sk1 ),
inference(simp,[status(thm)],[8920]) ).
thf(10973,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( C @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) )
| ~ $true
| ~ ( sk2 @ ( A @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[3289,141]) ).
thf(10974,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( C @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) )
| ~ ( sk2 @ ( A @ convergent_lines ) ) ),
inference(simp,[status(thm)],[10973]) ).
thf(10975,plain,
! [A: $i] :
( ~ ( sk3 @ ( sk3 @ ( A @ intersection_point ) @ apart_point_and_line ) )
| ~ ( sk2 @ ( A @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[10974:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk3 ))]]) ).
thf(3337,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( sk2 @ ( B @ distinct_lines ) ) )
| ( sk3 @ ( B @ convergent_lines ) )
| ~ $true
| ( sk3 @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[2164,1709]) ).
thf(3338,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( sk2 @ ( B @ distinct_lines ) ) )
| ( sk3 @ ( B @ convergent_lines ) )
| ( sk3 @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[3337]) ).
thf(3339,plain,
! [A: $i] :
( ( sk3 @ ( A @ convergent_lines ) )
| ( sk3 @ ( A @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[3338:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(258,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ apart_point_and_line ) )
!= ( F @ ( E @ apart_point_and_line ) ) )
| ~ $true
| ~ ( F @ ( E @ incident_point_and_line ) )
| ( D @ ( C @ unorthogonal_lines ) )
| ( D @ ( B @ unorthogonal_lines ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( C @ ( B @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[47,89]) ).
thf(259,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ apart_point_and_line ) )
!= ( F @ ( E @ apart_point_and_line ) ) )
| ~ ( F @ ( E @ incident_point_and_line ) )
| ( D @ ( C @ unorthogonal_lines ) )
| ( D @ ( B @ unorthogonal_lines ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( C @ ( B @ distinct_lines ) ) ),
inference(simp,[status(thm)],[258]) ).
thf(260,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( B @ ( A @ incident_point_and_line ) )
| ( D @ ( C @ unorthogonal_lines ) )
| ( D @ ( B @ unorthogonal_lines ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( C @ ( B @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[259:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( A )),bind(F,$thf( B ))]]) ).
thf(307,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( D @ ( E @ orthogonal_through_point ) @ ( D @ apart_point_and_line ) ) )
| ~ $true
| ( C @ ( B @ distinct_lines ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[53,80]) ).
thf(308,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( D @ ( E @ orthogonal_through_point ) @ ( D @ apart_point_and_line ) ) )
| ( C @ ( B @ distinct_lines ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[307]) ).
thf(309,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ orthogonal_through_point ) @ ( A @ distinct_lines ) )
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[308:[bind(A,$thf( G )),bind(B,$thf( B )),bind(C,$thf( G @ ( F @ orthogonal_through_point ) )),bind(D,$thf( G )),bind(E,$thf( F ))]]) ).
thf(349,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ orthogonal_through_point ) @ ( A @ distinct_lines ) )
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[309]) ).
thf(186,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( A @ apart_point_and_line ) )
!= ( E @ ( F @ orthogonal_through_point ) @ ( E @ apart_point_and_line ) ) )
| ~ $true
| ( D @ ( B @ apart_point_and_line ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(paramod_ordered,[status(thm)],[44,80]) ).
thf(187,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( A @ apart_point_and_line ) )
!= ( E @ ( F @ orthogonal_through_point ) @ ( E @ apart_point_and_line ) ) )
| ( D @ ( B @ apart_point_and_line ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[186]) ).
thf(188,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ orthogonal_through_point ) @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ( B @ ( D @ apart_point_and_line ) )
| ~ ( D @ ( C @ orthogonal_through_point ) @ ( B @ distinct_lines ) )
| ~ ( A @ ( D @ distinct_points ) ) ),
inference(pattern_uni,[status(thm)],[187:[bind(A,$thf( H )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( H @ ( G @ orthogonal_through_point ) )),bind(E,$thf( H )),bind(F,$thf( G ))]]) ).
thf(197,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ orthogonal_through_point ) @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ( B @ ( D @ apart_point_and_line ) )
| ~ ( D @ ( C @ orthogonal_through_point ) @ ( B @ distinct_lines ) )
| ~ ( A @ ( D @ distinct_points ) ) ),
inference(simp,[status(thm)],[188]) ).
thf(21,axiom,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ distinct_lines ) )
=> ( ( C @ ( B @ convergent_lines ) )
| ( C @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cup1) ).
thf(97,plain,
! [A: $i,B: $i,C: $i] :
( ( C @ ( B @ distinct_lines ) )
=> ( ( C @ ( B @ convergent_lines ) )
| ( C @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(2177,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( sk2 @ ( B @ distinct_lines ) ) )
| ( sk3 @ ( B @ distinct_lines ) )
| ~ $true
| ~ ( A @ ( sk3 @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1775,1676]) ).
thf(2178,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( sk2 @ ( B @ distinct_lines ) ) )
| ( sk3 @ ( B @ distinct_lines ) )
| ~ ( A @ ( sk3 @ distinct_lines ) ) ),
inference(simp,[status(thm)],[2177]) ).
thf(2179,plain,
! [A: $i] :
( ( sk3 @ ( A @ distinct_lines ) )
| ~ ( A @ ( sk3 @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[2178:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(11605,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( A @ ( sk3 @ orthogonal_through_point ) @ convergent_lines ) )
!= ( sk2 @ ( B @ ( sk3 @ parallel_through_point ) @ convergent_lines ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8788,11047]) ).
thf(11606,plain,
! [B: $i,A: $i] :
( ( sk2 @ ( A @ ( sk3 @ orthogonal_through_point ) @ convergent_lines ) )
!= ( sk2 @ ( B @ ( sk3 @ parallel_through_point ) @ convergent_lines ) ) ),
inference(simp,[status(thm)],[11605]) ).
thf(11636,plain,
! [B: $i,A: $i] :
( ( sk2 != sk2 )
| ( ( A @ ( sk3 @ orthogonal_through_point ) )
!= ( B @ ( sk3 @ parallel_through_point ) ) ) ),
inference(simp,[status(thm)],[11606]) ).
thf(11646,plain,
! [B: $i,A: $i] :
( ( A @ ( sk3 @ orthogonal_through_point ) )
!= ( B @ ( sk3 @ parallel_through_point ) ) ),
inference(simp,[status(thm)],[11636]) ).
thf(322,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( E @ ( D @ apart_point_and_line ) ) )
| ~ $true
| ~ ( E @ ( D @ incident_point_and_line ) )
| ( C @ ( B @ distinct_lines ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[53,89]) ).
thf(323,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( E @ ( D @ apart_point_and_line ) ) )
| ~ ( E @ ( D @ incident_point_and_line ) )
| ( C @ ( B @ distinct_lines ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[322]) ).
thf(324,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ incident_point_and_line ) )
| ( C @ ( B @ distinct_lines ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[323:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( A )),bind(E,$thf( C ))]]) ).
thf(4190,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ( C @ ( B @ convergent_lines ) )
| ~ $true
| ( A @ ( sk3 @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[2249,147]) ).
thf(4191,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ( C @ ( B @ convergent_lines ) )
| ( A @ ( sk3 @ equal_lines ) ) ),
inference(simp,[status(thm)],[4190]) ).
thf(4192,plain,
! [A: $i] :
( ( sk2 @ ( A @ convergent_lines ) )
| ( A @ ( sk3 @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[4191:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk2 ))]]) ).
thf(626,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( D @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) )
| ( sk2 @ ( D @ distinct_lines ) )
| ~ $true
| ( C @ ( B @ distinct_lines ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[53,559]) ).
thf(627,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( D @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) )
| ( sk2 @ ( D @ distinct_lines ) )
| ( C @ ( B @ distinct_lines ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[626]) ).
thf(628,plain,
! [B: $i,A: $i] :
( ( sk2 @ ( B @ distinct_lines ) )
| ( B @ ( A @ distinct_lines ) )
| ~ ( A @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[627:[bind(A,$thf( sk2 @ ( sk1 @ intersection_point ) )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( C ))]]) ).
thf(650,plain,
! [B: $i,A: $i] :
( ( sk2 @ ( B @ distinct_lines ) )
| ( B @ ( A @ distinct_lines ) )
| ~ ( A @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[628]) ).
thf(70,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ distinct_points ) )
=> ! [C: $i] :
( ( C @ ( B @ distinct_points ) )
| ( C @ ( A @ distinct_points ) ) ) ),
inference(miniscope,[status(thm)],[69]) ).
thf(71,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ distinct_points ) )
| ( C @ ( A @ distinct_points ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(cnf,[status(esa)],[70]) ).
thf(1368,plain,
! [C: $i,B: $i,A: $i] :
( ~ $true
| ( ( C @ ( B @ distinct_points ) )
!= ( C @ ( A @ distinct_points ) ) )
| ( C @ ( A @ distinct_points ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(eqfactor_ordered,[status(thm)],[71]) ).
thf(1369,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ distinct_points ) )
| ~ ( A @ ( A @ distinct_points ) ) ),
inference(pattern_uni,[status(thm)],[1368:[bind(A,$thf( B ))]]) ).
thf(1375,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ distinct_points ) )
| ~ ( A @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[1369]) ).
thf(11060,plain,
! [A: $i] :
( ( ( sk2 @ ( A @ ( sk3 @ orthogonal_through_point ) @ convergent_lines ) )
!= ( sk2 @ ( sk3 @ convergent_lines ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8788,10972]) ).
thf(11061,plain,
! [A: $i] :
( ( sk2 @ ( A @ ( sk3 @ orthogonal_through_point ) @ convergent_lines ) )
!= ( sk2 @ ( sk3 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[11060]) ).
thf(11083,plain,
! [A: $i] :
( ( sk2 != sk2 )
| ( ( A @ ( sk3 @ orthogonal_through_point ) )
!= sk3 ) ),
inference(simp,[status(thm)],[11061]) ).
thf(11089,plain,
! [A: $i] :
( ( A @ ( sk3 @ orthogonal_through_point ) )
!= sk3 ),
inference(simp,[status(thm)],[11083]) ).
thf(1770,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( sk2 @ ( sk3 @ distinct_lines ) ) )
| ~ $true
| ( B @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[136,1712]) ).
thf(1771,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( sk2 @ ( sk3 @ distinct_lines ) ) )
| ( B @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[1770]) ).
thf(1772,plain,
sk2 @ ( sk3 @ equal_lines ),
inference(pattern_uni,[status(thm)],[1771:[bind(A,$thf( sk3 )),bind(B,$thf( sk2 ))]]) ).
thf(654,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( D @ ( C @ distinct_lines ) ) )
| ~ $true
| ~ ( D @ ( C @ equal_lines ) )
| ( sk2 @ ( B @ distinct_lines ) )
| ~ ( A @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[650,134]) ).
thf(655,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( D @ ( C @ distinct_lines ) ) )
| ~ ( D @ ( C @ equal_lines ) )
| ( sk2 @ ( B @ distinct_lines ) )
| ~ ( A @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[654]) ).
thf(656,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ equal_lines ) )
| ( sk2 @ ( B @ distinct_lines ) )
| ~ ( A @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[655:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(1821,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk3 @ equal_lines ) )
!= ( B @ ( A @ equal_lines ) ) )
| ~ $true
| ( sk2 @ ( B @ distinct_lines ) )
| ~ ( A @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[1772,656]) ).
thf(1822,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk3 @ equal_lines ) )
!= ( B @ ( A @ equal_lines ) ) )
| ( sk2 @ ( B @ distinct_lines ) )
| ~ ( A @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[1821]) ).
thf(1823,plain,
( ( sk2 @ ( sk2 @ distinct_lines ) )
| ~ ( sk3 @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[1822:[bind(A,$thf( sk3 )),bind(B,$thf( sk2 ))]]) ).
thf(1850,plain,
( $false
| ~ ( sk3 @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) ),
inference(rewrite,[status(thm)],[1823,74]) ).
thf(1851,plain,
~ ( sk3 @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ),
inference(simp,[status(thm)],[1850]) ).
thf(108,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ parallel_lines ) )
| ( B @ ( A @ convergent_lines ) ) ),
inference(cnfConj,[status(thm)],[106]) ).
thf(109,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ parallel_lines ) )
| ( B @ ( A @ convergent_lines ) ) ),
inference(simp,[status(thm)],[108]) ).
thf(4719,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ $true
| ~ ( C @ ( B @ parallel_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[2383,107]) ).
thf(4720,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( C @ ( B @ parallel_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[4719]) ).
thf(4721,plain,
! [A: $i] :
( ~ ( A @ ( sk2 @ parallel_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[4720:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( A ))]]) ).
thf(199,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( E @ ( F @ parallel_through_point ) @ ( E @ apart_point_and_line ) ) )
| ~ $true
| ( D @ ( B @ apart_point_and_line ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(paramod_ordered,[status(thm)],[44,83]) ).
thf(200,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( E @ ( F @ parallel_through_point ) @ ( E @ apart_point_and_line ) ) )
| ( D @ ( B @ apart_point_and_line ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[199]) ).
thf(201,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ apart_point_and_line ) )
| ( D @ ( C @ parallel_through_point ) @ ( A @ apart_point_and_line ) )
| ( B @ ( D @ apart_point_and_line ) )
| ~ ( B @ ( D @ ( C @ parallel_through_point ) @ distinct_lines ) )
| ~ ( A @ ( D @ distinct_points ) ) ),
inference(pattern_uni,[status(thm)],[200:[bind(A,$thf( H )),bind(B,$thf( B )),bind(C,$thf( H @ ( G @ parallel_through_point ) )),bind(D,$thf( D )),bind(E,$thf( H )),bind(F,$thf( G ))]]) ).
thf(212,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( A @ apart_point_and_line ) )
| ( D @ ( C @ parallel_through_point ) @ ( A @ apart_point_and_line ) )
| ( B @ ( D @ apart_point_and_line ) )
| ~ ( B @ ( D @ ( C @ parallel_through_point ) @ distinct_lines ) )
| ~ ( A @ ( D @ distinct_points ) ) ),
inference(simp,[status(thm)],[201]) ).
thf(20,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ distinct_points ) )
=> ~ ( B @ ( A @ line_connecting ) @ ( A @ apart_point_and_line ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ci1) ).
thf(95,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ distinct_points ) )
=> ~ ( B @ ( A @ line_connecting ) @ ( A @ apart_point_and_line ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(96,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ line_connecting ) @ ( A @ apart_point_and_line ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(cnf,[status(esa)],[95]) ).
thf(1766,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ parallel_through_point ) @ ( A @ distinct_lines ) )
!= ( sk2 @ ( sk3 @ distinct_lines ) ) )
| ~ $true
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[345,1712]) ).
thf(1767,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ parallel_through_point ) @ ( A @ distinct_lines ) )
!= ( sk2 @ ( sk3 @ distinct_lines ) ) )
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[1766]) ).
thf(1773,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ parallel_through_point ) )
!= sk2 )
| ( A != sk3 )
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[1767]) ).
thf(1776,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ parallel_through_point ) )
!= sk2 )
| ~ ( sk3 @ ( B @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[1773]) ).
thf(2431,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ parallel_through_point ) @ ( A @ distinct_lines ) )
!= ( D @ ( sk3 @ distinct_lines ) ) )
| ~ ( sk3 @ ( D @ equal_lines ) )
| ~ $true
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[345,2228]) ).
thf(2432,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ parallel_through_point ) @ ( A @ distinct_lines ) )
!= ( D @ ( sk3 @ distinct_lines ) ) )
| ~ ( sk3 @ ( D @ equal_lines ) )
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[2431]) ).
thf(2433,plain,
! [B: $i,A: $i] :
( ~ ( sk3 @ ( B @ ( A @ parallel_through_point ) @ equal_lines ) )
| ~ ( sk3 @ ( B @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[2432:[bind(A,$thf( sk3 )),bind(B,$thf( E )),bind(C,$thf( F )),bind(D,$thf( F @ ( E @ parallel_through_point ) ))]]) ).
thf(2450,plain,
! [B: $i,A: $i] :
( ~ ( sk3 @ ( B @ ( A @ parallel_through_point ) @ equal_lines ) )
| ~ ( sk3 @ ( B @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[2433]) ).
thf(1740,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( sk2 @ ( C @ distinct_lines ) ) )
| ( sk3 @ ( C @ distinct_lines ) )
| ~ $true
| ( B @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[136,1676]) ).
thf(1741,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( sk2 @ ( C @ distinct_lines ) ) )
| ( sk3 @ ( C @ distinct_lines ) )
| ( B @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[1740]) ).
thf(1742,plain,
! [A: $i] :
( ( sk3 @ ( A @ distinct_lines ) )
| ( sk2 @ ( A @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[1741:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( A ))]]) ).
thf(2004,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ( C @ ( B @ convergent_lines ) )
| ~ $true
| ( sk2 @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1742,147]) ).
thf(2005,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ( C @ ( B @ convergent_lines ) )
| ( sk2 @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[2004]) ).
thf(2006,plain,
! [A: $i] :
( ( sk3 @ ( A @ convergent_lines ) )
| ( sk2 @ ( A @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[2005:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk3 ))]]) ).
thf(29,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ unorthogonal_lines ) )
| ( B @ ( A @ convergent_lines ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',occu1) ).
thf(129,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ unorthogonal_lines ) )
| ( B @ ( A @ convergent_lines ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(11058,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ orthogonal_through_point ) @ convergent_lines ) )
!= ( sk2 @ ( sk3 @ convergent_lines ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[243,10972]) ).
thf(11059,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ orthogonal_through_point ) @ convergent_lines ) )
!= ( sk2 @ ( sk3 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[11058]) ).
thf(11087,plain,
! [B: $i,A: $i] :
( ( A != sk2 )
| ( ( B @ ( A @ orthogonal_through_point ) )
!= sk3 ) ),
inference(simp,[status(thm)],[11059]) ).
thf(11093,plain,
! [A: $i] :
( ( A @ ( sk2 @ orthogonal_through_point ) )
!= sk3 ),
inference(simp,[status(thm)],[11087]) ).
thf(20855,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ orthogonal_through_point ) @ ( A @ distinct_lines ) )
!= ( D @ ( sk2 @ distinct_lines ) ) )
| ~ ( sk2 @ ( D @ equal_lines ) )
| ~ $true
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[349,3135]) ).
thf(20856,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ orthogonal_through_point ) @ ( A @ distinct_lines ) )
!= ( D @ ( sk2 @ distinct_lines ) ) )
| ~ ( sk2 @ ( D @ equal_lines ) )
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[20855]) ).
thf(20857,plain,
! [B: $i,A: $i] :
( ~ ( sk2 @ ( B @ ( A @ orthogonal_through_point ) @ equal_lines ) )
| ~ ( sk2 @ ( B @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[20856:[bind(A,$thf( sk2 )),bind(B,$thf( E )),bind(C,$thf( F )),bind(D,$thf( F @ ( E @ orthogonal_through_point ) ))]]) ).
thf(21270,plain,
! [B: $i,A: $i] :
( ~ ( sk2 @ ( B @ ( A @ orthogonal_through_point ) @ equal_lines ) )
| ~ ( sk2 @ ( B @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[20857]) ).
thf(8801,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ ( sk3 @ orthogonal_through_point ) @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( C @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8788,141]) ).
thf(8802,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ ( sk3 @ orthogonal_through_point ) @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( C @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[8801]) ).
thf(8803,plain,
! [A: $i] :
~ ( sk2 @ ( sk2 @ ( A @ ( sk3 @ orthogonal_through_point ) @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[8802:[bind(A,$thf( E )),bind(B,$thf( E @ ( sk3 @ orthogonal_through_point ) )),bind(C,$thf( sk2 ))]]) ).
thf(8846,plain,
! [A: $i] :
~ ( sk2 @ ( sk2 @ ( A @ ( sk3 @ orthogonal_through_point ) @ intersection_point ) @ apart_point_and_line ) ),
inference(simp,[status(thm)],[8803]) ).
thf(28,axiom,
! [A: $i,B: $i,C: $i] :
( ( ( B @ ( A @ unorthogonal_lines ) )
& ( B @ ( A @ convergent_lines ) ) )
=> ( ( ( C @ ( B @ unorthogonal_lines ) )
& ( C @ ( B @ convergent_lines ) ) )
| ( ( C @ ( A @ unorthogonal_lines ) )
& ( C @ ( A @ convergent_lines ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',oac1) ).
thf(122,plain,
! [A: $i,B: $i,C: $i] :
( ( ( B @ ( A @ unorthogonal_lines ) )
& ( B @ ( A @ convergent_lines ) ) )
=> ( ( ( C @ ( B @ unorthogonal_lines ) )
& ( C @ ( B @ convergent_lines ) ) )
| ( ( C @ ( A @ unorthogonal_lines ) )
& ( C @ ( A @ convergent_lines ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(123,plain,
! [A: $i,B: $i] :
( ( ( B @ ( A @ unorthogonal_lines ) )
& ( B @ ( A @ convergent_lines ) ) )
=> ! [C: $i] :
( ( ( C @ ( B @ unorthogonal_lines ) )
& ( C @ ( B @ convergent_lines ) ) )
| ( ( C @ ( A @ unorthogonal_lines ) )
& ( C @ ( A @ convergent_lines ) ) ) ) ),
inference(miniscope,[status(thm)],[122]) ).
thf(124,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ unorthogonal_lines ) )
| ( C @ ( A @ unorthogonal_lines ) )
| ~ ( B @ ( A @ unorthogonal_lines ) )
| ~ ( B @ ( A @ convergent_lines ) ) )
& ( ( C @ ( B @ convergent_lines ) )
| ( C @ ( A @ unorthogonal_lines ) )
| ~ ( B @ ( A @ unorthogonal_lines ) )
| ~ ( B @ ( A @ convergent_lines ) ) )
& ( ( C @ ( B @ unorthogonal_lines ) )
| ( C @ ( A @ convergent_lines ) )
| ~ ( B @ ( A @ unorthogonal_lines ) )
| ~ ( B @ ( A @ convergent_lines ) ) )
& ( ( C @ ( B @ convergent_lines ) )
| ( C @ ( A @ convergent_lines ) )
| ~ ( B @ ( A @ unorthogonal_lines ) )
| ~ ( B @ ( A @ convergent_lines ) ) ) ),
inference(cnf,[status(esa)],[123]) ).
thf(128,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ unorthogonal_lines ) )
| ( C @ ( A @ unorthogonal_lines ) )
| ~ ( B @ ( A @ unorthogonal_lines ) )
| ~ ( B @ ( A @ convergent_lines ) ) ),
inference(cnfConj,[status(thm)],[124]) ).
thf(264,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( B @ unorthogonal_lines ) )
!= ( F @ ( E @ unorthogonal_lines ) ) )
| ~ $true
| ~ ( F @ ( E @ orthogonal_lines ) )
| ( D @ ( C @ unorthogonal_lines ) )
| ( C @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( C @ ( B @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[47,59]) ).
thf(265,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( B @ unorthogonal_lines ) )
!= ( F @ ( E @ unorthogonal_lines ) ) )
| ~ ( F @ ( E @ orthogonal_lines ) )
| ( D @ ( C @ unorthogonal_lines ) )
| ( C @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( C @ ( B @ distinct_lines ) ) ),
inference(simp,[status(thm)],[264]) ).
thf(266,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( D @ ( B @ orthogonal_lines ) )
| ( D @ ( C @ unorthogonal_lines ) )
| ( C @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( C @ ( B @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[265:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( B )),bind(F,$thf( D ))]]) ).
thf(1356,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ distinct_points ) )
!= ( D @ ( D @ distinct_points ) ) )
| ~ $true
| ( C @ ( B @ distinct_points ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(paramod_ordered,[status(thm)],[71,94]) ).
thf(1357,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ distinct_points ) )
!= ( D @ ( D @ distinct_points ) ) )
| ( C @ ( B @ distinct_points ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[1356]) ).
thf(1358,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ distinct_points ) )
| ~ ( A @ ( B @ distinct_points ) ) ),
inference(pattern_uni,[status(thm)],[1357:[bind(A,$thf( C )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( C ))]]) ).
thf(1374,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ distinct_points ) )
| ~ ( A @ ( B @ distinct_points ) ) ),
inference(simp,[status(thm)],[1358]) ).
thf(1382,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_points ) )
!= ( D @ ( C @ distinct_points ) ) )
| ~ $true
| ~ ( D @ ( C @ equal_points ) )
| ~ ( A @ ( B @ distinct_points ) ) ),
inference(paramod_ordered,[status(thm)],[1374,116]) ).
thf(1383,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_points ) )
!= ( D @ ( C @ distinct_points ) ) )
| ~ ( D @ ( C @ equal_points ) )
| ~ ( A @ ( B @ distinct_points ) ) ),
inference(simp,[status(thm)],[1382]) ).
thf(1384,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ equal_points ) )
| ~ ( A @ ( B @ distinct_points ) ) ),
inference(pattern_uni,[status(thm)],[1383:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(1464,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_points ) )
!= ( C @ ( D @ distinct_points ) ) )
| ~ ( D @ ( C @ equal_points ) )
| ~ $true
| ~ ( A @ ( B @ distinct_points ) ) ),
inference(paramod_ordered,[status(thm)],[1374,1384]) ).
thf(1465,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_points ) )
!= ( C @ ( D @ distinct_points ) ) )
| ~ ( D @ ( C @ equal_points ) )
| ~ ( A @ ( B @ distinct_points ) ) ),
inference(simp,[status(thm)],[1464]) ).
thf(1466,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ equal_points ) )
| ~ ( A @ ( B @ distinct_points ) ) ),
inference(pattern_uni,[status(thm)],[1465:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(3783,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( B @ ( A @ parallel_through_point ) @ equal_lines ) )
!= ( sk2 @ ( sk3 @ equal_lines ) ) )
| ~ $true
| ~ ( sk3 @ ( B @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[1772,2306]) ).
thf(3784,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( B @ ( A @ parallel_through_point ) @ equal_lines ) )
!= ( sk2 @ ( sk3 @ equal_lines ) ) )
| ~ ( sk3 @ ( B @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[3783]) ).
thf(3827,plain,
! [B: $i,A: $i] :
( ( sk2 != sk2 )
| ( ( B @ ( A @ parallel_through_point ) )
!= sk3 )
| ~ ( sk3 @ ( B @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[3784]) ).
thf(3841,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ parallel_through_point ) )
!= sk3 )
| ~ ( sk3 @ ( B @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[3827]) ).
thf(10,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ apart_point_and_line ) )
=> ( ( B @ ( C @ apart_point_and_line ) )
| ( C @ ( A @ distinct_points ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ceq1) ).
thf(64,plain,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ apart_point_and_line ) )
=> ( ( B @ ( C @ apart_point_and_line ) )
| ( C @ ( A @ distinct_points ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(11009,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( B @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) )
| ~ $true
| ~ ( sk2 @ ( A @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[3289,143]) ).
thf(11010,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( B @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) )
| ~ ( sk2 @ ( A @ convergent_lines ) ) ),
inference(simp,[status(thm)],[11009]) ).
thf(11011,plain,
! [A: $i] :
( ~ ( A @ ( sk3 @ ( A @ intersection_point ) @ apart_point_and_line ) )
| ~ ( sk2 @ ( A @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[11010:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk3 ))]]) ).
thf(8901,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ ( A @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8868,143]) ).
thf(8902,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ ( A @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[8901]) ).
thf(8903,plain,
~ ( sk1 @ ( sk3 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[8902:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 ))]]) ).
thf(2174,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( sk2 @ ( B @ distinct_lines ) ) )
| ( sk3 @ ( B @ convergent_lines ) )
| ~ $true
| ~ ( A @ ( sk3 @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1775,1709]) ).
thf(2175,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( sk2 @ ( B @ distinct_lines ) ) )
| ( sk3 @ ( B @ convergent_lines ) )
| ~ ( A @ ( sk3 @ distinct_lines ) ) ),
inference(simp,[status(thm)],[2174]) ).
thf(2176,plain,
! [A: $i] :
( ( sk3 @ ( A @ convergent_lines ) )
| ~ ( A @ ( sk3 @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[2175:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(169,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ $true
| ( ( D @ ( B @ apart_point_and_line ) )
!= ( D @ ( A @ apart_point_and_line ) ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(eqfactor_ordered,[status(thm)],[44]) ).
thf(173,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( A @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( C @ ( B @ distinct_lines ) )
| ~ ( A @ ( A @ distinct_points ) ) ),
inference(pattern_uni,[status(thm)],[169:[bind(A,$thf( B ))]]) ).
thf(180,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( C @ ( B @ distinct_lines ) )
| ~ ( A @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[173]) ).
thf(293,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ orthogonal_through_point ) @ convergent_lines ) )
!= ( D @ ( C @ convergent_lines ) ) )
| ~ $true
| ~ ( D @ ( C @ parallel_lines ) ) ),
inference(paramod_ordered,[status(thm)],[243,107]) ).
thf(294,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ orthogonal_through_point ) @ convergent_lines ) )
!= ( D @ ( C @ convergent_lines ) ) )
| ~ ( D @ ( C @ parallel_lines ) ) ),
inference(simp,[status(thm)],[293]) ).
thf(295,plain,
! [B: $i,A: $i] :
~ ( A @ ( B @ ( A @ orthogonal_through_point ) @ parallel_lines ) ),
inference(pattern_uni,[status(thm)],[294:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F @ ( E @ orthogonal_through_point ) )),bind(D,$thf( E ))]]) ).
thf(296,plain,
! [B: $i,A: $i] :
~ ( A @ ( B @ ( A @ orthogonal_through_point ) @ parallel_lines ) ),
inference(simp,[status(thm)],[295]) ).
thf(370,plain,
! [A: $i] :
( ( ( A @ ( A @ equal_points ) )
!= ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ equal_points ) ) )
| ~ $true
| ~ ( sk3 @ ( sk1 @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[365,42]) ).
thf(371,plain,
! [A: $i] :
( ( ( A @ ( A @ equal_points ) )
!= ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ equal_points ) ) )
| ~ ( sk3 @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[370]) ).
thf(377,plain,
! [A: $i] :
( ( A
!= ( sk3 @ ( sk1 @ intersection_point ) ) )
| ( A
!= ( sk2 @ ( sk1 @ intersection_point ) ) )
| ~ ( sk3 @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[371]) ).
thf(380,plain,
( ( ( sk3 @ ( sk1 @ intersection_point ) )
!= ( sk2 @ ( sk1 @ intersection_point ) ) )
| ~ ( sk3 @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[377]) ).
thf(8871,plain,
( ( ( sk3 @ ( sk1 @ intersection_point ) )
!= ( sk2 @ ( sk1 @ intersection_point ) ) )
| ~ $true ),
inference(rewrite,[status(thm)],[380,8868]) ).
thf(8872,plain,
( ( sk3 @ ( sk1 @ intersection_point ) )
!= ( sk2 @ ( sk1 @ intersection_point ) ) ),
inference(simp,[status(thm)],[8871]) ).
thf(3430,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ parallel_through_point ) @ ( A @ distinct_lines ) )
!= ( D @ ( sk2 @ distinct_lines ) ) )
| ~ ( sk2 @ ( D @ equal_lines ) )
| ~ $true
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[345,3135]) ).
thf(3431,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ parallel_through_point ) @ ( A @ distinct_lines ) )
!= ( D @ ( sk2 @ distinct_lines ) ) )
| ~ ( sk2 @ ( D @ equal_lines ) )
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[3430]) ).
thf(3432,plain,
! [B: $i,A: $i] :
( ~ ( sk2 @ ( B @ ( A @ parallel_through_point ) @ equal_lines ) )
| ~ ( sk2 @ ( B @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[3431:[bind(A,$thf( sk2 )),bind(B,$thf( E )),bind(C,$thf( F )),bind(D,$thf( F @ ( E @ parallel_through_point ) ))]]) ).
thf(3458,plain,
! [B: $i,A: $i] :
( ~ ( sk2 @ ( B @ ( A @ parallel_through_point ) @ equal_lines ) )
| ~ ( sk2 @ ( B @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[3432]) ).
thf(891,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ orthogonal_through_point ) @ convergent_lines ) )
!= ( D @ ( C @ convergent_lines ) ) )
| ~ ( C @ ( D @ ( C @ intersection_point ) @ apart_point_and_line ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[243,143]) ).
thf(892,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ ( A @ orthogonal_through_point ) @ convergent_lines ) )
!= ( D @ ( C @ convergent_lines ) ) )
| ~ ( C @ ( D @ ( C @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[891]) ).
thf(893,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ orthogonal_through_point ) @ ( A @ ( B @ ( A @ orthogonal_through_point ) @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[892:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F @ ( E @ orthogonal_through_point ) )),bind(D,$thf( E ))]]) ).
thf(936,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ orthogonal_through_point ) @ ( A @ ( B @ ( A @ orthogonal_through_point ) @ intersection_point ) @ apart_point_and_line ) ),
inference(simp,[status(thm)],[893]) ).
thf(4184,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( sk2 @ ( B @ distinct_lines ) ) )
| ( sk3 @ ( B @ convergent_lines ) )
| ~ $true
| ( A @ ( sk3 @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[2249,1709]) ).
thf(4185,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( sk2 @ ( B @ distinct_lines ) ) )
| ( sk3 @ ( B @ convergent_lines ) )
| ( A @ ( sk3 @ equal_lines ) ) ),
inference(simp,[status(thm)],[4184]) ).
thf(4186,plain,
! [A: $i] :
( ( sk3 @ ( A @ convergent_lines ) )
| ( A @ ( sk3 @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[4185:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(2165,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( A @ distinct_lines ) )
!= ( sk3 @ ( B @ distinct_lines ) ) )
| ( sk2 @ ( B @ distinct_lines ) )
| ~ $true
| ( sk2 @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1742,1765]) ).
thf(2166,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( A @ distinct_lines ) )
!= ( sk3 @ ( B @ distinct_lines ) ) )
| ( sk2 @ ( B @ distinct_lines ) )
| ( sk2 @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[2165]) ).
thf(2167,plain,
! [A: $i] :
( ( sk2 @ ( A @ distinct_lines ) )
| ( sk2 @ ( A @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[2166:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(3724,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ( C @ ( B @ convergent_lines ) )
| ~ $true
| ( sk2 @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[2167,147]) ).
thf(3725,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ( C @ ( B @ convergent_lines ) )
| ( sk2 @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[3724]) ).
thf(3726,plain,
! [A: $i] :
( ( sk2 @ ( A @ convergent_lines ) )
| ( sk2 @ ( A @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[3725:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk2 ))]]) ).
thf(65,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ apart_point_and_line ) )
=> ! [C: $i] :
( ( B @ ( C @ apart_point_and_line ) )
| ( C @ ( A @ distinct_points ) ) ) ),
inference(miniscope,[status(thm)],[64]) ).
thf(66,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ apart_point_and_line ) )
| ( C @ ( A @ distinct_points ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(cnf,[status(esa)],[65]) ).
thf(785,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ apart_point_and_line ) )
!= ( sk2 @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) )
| ~ $true
| ( C @ ( A @ distinct_points ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[66,528]) ).
thf(786,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ apart_point_and_line ) )
!= ( sk2 @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) )
| ( C @ ( A @ distinct_points ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[785]) ).
thf(787,plain,
! [A: $i] :
( ( sk2 @ ( sk1 @ intersection_point ) @ ( A @ distinct_points ) )
| ~ ( sk2 @ ( A @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[786:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( sk2 @ ( sk1 @ intersection_point ) ))]]) ).
thf(1933,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( sk2 @ distinct_lines ) ) )
| ( sk3 @ ( C @ distinct_lines ) )
| ~ $true
| ( B @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[136,1691]) ).
thf(1934,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( sk2 @ distinct_lines ) ) )
| ( sk3 @ ( C @ distinct_lines ) )
| ( B @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[1933]) ).
thf(1935,plain,
! [A: $i] :
( ( sk3 @ ( A @ distinct_lines ) )
| ( A @ ( sk2 @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[1934:[bind(A,$thf( sk2 )),bind(B,$thf( B )),bind(C,$thf( B ))]]) ).
thf(1944,plain,
! [A: $i] :
( ( sk3 @ ( A @ distinct_lines ) )
| ( A @ ( sk2 @ equal_lines ) ) ),
inference(simp,[status(thm)],[1935]) ).
thf(2624,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( A @ distinct_lines ) )
!= ( sk3 @ ( B @ distinct_lines ) ) )
| ( sk2 @ ( B @ distinct_lines ) )
| ~ $true
| ( A @ ( sk2 @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1944,1765]) ).
thf(2625,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( A @ distinct_lines ) )
!= ( sk3 @ ( B @ distinct_lines ) ) )
| ( sk2 @ ( B @ distinct_lines ) )
| ( A @ ( sk2 @ equal_lines ) ) ),
inference(simp,[status(thm)],[2624]) ).
thf(2626,plain,
! [A: $i] :
( ( sk2 @ ( A @ distinct_lines ) )
| ( A @ ( sk2 @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[2625:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(6792,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ( C @ ( B @ convergent_lines ) )
| ~ $true
| ( A @ ( sk2 @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[2626,147]) ).
thf(6793,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ( C @ ( B @ convergent_lines ) )
| ( A @ ( sk2 @ equal_lines ) ) ),
inference(simp,[status(thm)],[6792]) ).
thf(6794,plain,
! [A: $i] :
( ( sk2 @ ( A @ convergent_lines ) )
| ( A @ ( sk2 @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[6793:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk2 ))]]) ).
thf(1991,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( sk2 @ distinct_lines ) ) )
| ~ ( sk3 @ ( C @ equal_lines ) )
| ~ $true
| ( B @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[136,1917]) ).
thf(1992,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( sk2 @ distinct_lines ) ) )
| ~ ( sk3 @ ( C @ equal_lines ) )
| ( B @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[1991]) ).
thf(1993,plain,
! [A: $i] :
( ~ ( sk3 @ ( A @ equal_lines ) )
| ( A @ ( sk2 @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[1992:[bind(A,$thf( sk2 )),bind(B,$thf( B )),bind(C,$thf( B ))]]) ).
thf(1997,plain,
! [A: $i] :
( ~ ( sk3 @ ( A @ equal_lines ) )
| ( A @ ( sk2 @ equal_lines ) ) ),
inference(simp,[status(thm)],[1993]) ).
thf(339,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ apart_point_and_line ) )
!= ( F @ ( E @ apart_point_and_line ) ) )
| ( G @ ( E @ apart_point_and_line ) )
| ( G @ ( F @ distinct_lines ) )
| ~ $true
| ( D @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(paramod_ordered,[status(thm)],[44,53]) ).
thf(340,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ apart_point_and_line ) )
!= ( F @ ( E @ apart_point_and_line ) ) )
| ( G @ ( E @ apart_point_and_line ) )
| ( G @ ( F @ distinct_lines ) )
| ( D @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[339]) ).
thf(341,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( B @ apart_point_and_line ) )
| ( E @ ( C @ distinct_lines ) )
| ( D @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(pattern_uni,[status(thm)],[340:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( B )),bind(F,$thf( C ))]]) ).
thf(350,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( B @ apart_point_and_line ) )
| ( E @ ( C @ distinct_lines ) )
| ( D @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[341]) ).
thf(157,plain,
( ( ( sk3 @ ( sk1 @ convergent_lines ) )
!= ( sk2 @ ( sk1 @ convergent_lines ) ) )
| ~ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ equal_points ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[40,42]) ).
thf(158,plain,
( ( ( sk3 @ ( sk1 @ convergent_lines ) )
!= ( sk2 @ ( sk1 @ convergent_lines ) ) )
| ~ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ equal_points ) ) ),
inference(simp,[status(thm)],[157]) ).
thf(159,plain,
( ( sk3 != sk2 )
| ( sk1 != sk1 )
| ~ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ equal_points ) ) ),
inference(simp,[status(thm)],[158]) ).
thf(160,plain,
( ( sk3 != sk2 )
| ~ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ equal_points ) ) ),
inference(simp,[status(thm)],[159]) ).
thf(366,plain,
! [A: $i] :
( ( ( A @ ( A @ equal_points ) )
!= ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ equal_points ) ) )
| ( sk3 != sk2 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[365,160]) ).
thf(367,plain,
! [A: $i] :
( ( ( A @ ( A @ equal_points ) )
!= ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ equal_points ) ) )
| ( sk3 != sk2 ) ),
inference(simp,[status(thm)],[366]) ).
thf(375,plain,
! [A: $i] :
( ( A
!= ( sk3 @ ( sk1 @ intersection_point ) ) )
| ( A
!= ( sk2 @ ( sk1 @ intersection_point ) ) )
| ( sk3 != sk2 ) ),
inference(simp,[status(thm)],[367]) ).
thf(378,plain,
( ( ( sk3 @ ( sk1 @ intersection_point ) )
!= ( sk2 @ ( sk1 @ intersection_point ) ) )
| ( sk3 != sk2 ) ),
inference(simp,[status(thm)],[375]) ).
thf(381,plain,
( ( sk3 != sk2 )
| ( sk1 != sk1 )
| ( sk3 != sk2 ) ),
inference(simp,[status(thm)],[378]) ).
thf(382,plain,
sk3 != sk2,
inference(simp,[status(thm)],[381]) ).
thf(7,axiom,
! [A: $i,B: $i] :
( ( ( B @ point )
& ( A @ line ) )
=> ( B @ ( A @ parallel_through_point ) @ line ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',par1) ).
thf(54,plain,
! [A: $i,B: $i] :
( ( ( B @ point )
& ( A @ line ) )
=> ( B @ ( A @ parallel_through_point ) @ line ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(8829,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ ( sk3 @ orthogonal_through_point ) @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ $true
| ~ ( C @ ( B @ parallel_lines ) ) ),
inference(paramod_ordered,[status(thm)],[8788,107]) ).
thf(8830,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ ( sk3 @ orthogonal_through_point ) @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( C @ ( B @ parallel_lines ) ) ),
inference(simp,[status(thm)],[8829]) ).
thf(8831,plain,
! [A: $i] :
~ ( sk2 @ ( A @ ( sk3 @ orthogonal_through_point ) @ parallel_lines ) ),
inference(pattern_uni,[status(thm)],[8830:[bind(A,$thf( E )),bind(B,$thf( E @ ( sk3 @ orthogonal_through_point ) )),bind(C,$thf( sk2 ))]]) ).
thf(8862,plain,
! [A: $i] :
~ ( sk2 @ ( A @ ( sk3 @ orthogonal_through_point ) @ parallel_lines ) ),
inference(simp,[status(thm)],[8831]) ).
thf(34,axiom,
! [A: $i,B: $i,C: $i] :
( ( ~ ( C @ ( A @ unorthogonal_lines ) )
& ~ ( B @ ( A @ unorthogonal_lines ) ) )
=> ~ ( C @ ( B @ convergent_lines ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',couo1) ).
thf(144,plain,
! [A: $i,B: $i,C: $i] :
( ( ~ ( C @ ( A @ unorthogonal_lines ) )
& ~ ( B @ ( A @ unorthogonal_lines ) ) )
=> ~ ( C @ ( B @ convergent_lines ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(234,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( B @ apart_point_and_line ) )
!= ( F @ ( E @ apart_point_and_line ) ) )
| ~ $true
| ~ ( F @ ( E @ incident_point_and_line ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(paramod_ordered,[status(thm)],[44,89]) ).
thf(235,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( B @ apart_point_and_line ) )
!= ( F @ ( E @ apart_point_and_line ) ) )
| ~ ( F @ ( E @ incident_point_and_line ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[234]) ).
thf(236,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( D @ ( B @ incident_point_and_line ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(pattern_uni,[status(thm)],[235:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( B )),bind(F,$thf( D ))]]) ).
thf(228,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( A @ apart_point_and_line ) )
!= ( F @ ( E @ apart_point_and_line ) ) )
| ~ $true
| ~ ( F @ ( E @ incident_point_and_line ) )
| ( D @ ( B @ apart_point_and_line ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(paramod_ordered,[status(thm)],[44,89]) ).
thf(229,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( A @ apart_point_and_line ) )
!= ( F @ ( E @ apart_point_and_line ) ) )
| ~ ( F @ ( E @ incident_point_and_line ) )
| ( D @ ( B @ apart_point_and_line ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[228]) ).
thf(230,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( D @ ( A @ incident_point_and_line ) )
| ( D @ ( B @ apart_point_and_line ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(pattern_uni,[status(thm)],[229:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( A )),bind(F,$thf( D ))]]) ).
thf(8879,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ convergent_lines ) )
!= ( A @ ( A @ convergent_lines ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8868,156]) ).
thf(8880,plain,
! [A: $i] :
( ( sk3 @ ( sk1 @ convergent_lines ) )
!= ( A @ ( A @ convergent_lines ) ) ),
inference(simp,[status(thm)],[8879]) ).
thf(8919,plain,
! [A: $i] :
( ( sk3 != A )
| ( sk1 != A ) ),
inference(simp,[status(thm)],[8880]) ).
thf(8926,plain,
sk3 != sk1,
inference(simp,[status(thm)],[8919]) ).
thf(270,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ $true
| ( ( C @ ( A @ apart_point_and_line ) )
!= ( B @ ( A @ apart_point_and_line ) ) )
| ( D @ ( C @ unorthogonal_lines ) )
| ( D @ ( B @ unorthogonal_lines ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( C @ ( B @ distinct_lines ) ) ),
inference(eqfactor_ordered,[status(thm)],[47]) ).
thf(272,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ unorthogonal_lines ) )
| ( C @ ( B @ unorthogonal_lines ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( B @ ( B @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[270:[bind(A,$thf( A )),bind(B,$thf( C ))]]) ).
thf(274,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ unorthogonal_lines ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( B @ ( B @ distinct_lines ) ) ),
inference(simp,[status(thm)],[272]) ).
thf(425,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( C @ distinct_lines ) ) )
| ~ $true
| ( B @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[136,74]) ).
thf(426,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( C @ distinct_lines ) ) )
| ( B @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[425]) ).
thf(427,plain,
! [A: $i] : ( A @ ( A @ equal_lines ) ),
inference(pattern_uni,[status(thm)],[426:[bind(A,$thf( B )),bind(B,$thf( B )),bind(C,$thf( B ))]]) ).
thf(432,plain,
! [A: $i] : ( A @ ( A @ equal_lines ) ),
inference(simp,[status(thm)],[427]) ).
thf(23195,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ equal_lines ) )
!= ( sk2 @ ( C @ ( B @ orthogonal_through_point ) @ equal_lines ) ) )
| ~ $true
| ~ ( sk2 @ ( C @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[432,21270]) ).
thf(23196,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ equal_lines ) )
!= ( sk2 @ ( C @ ( B @ orthogonal_through_point ) @ equal_lines ) ) )
| ~ ( sk2 @ ( C @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[23195]) ).
thf(23258,plain,
! [C: $i,B: $i,A: $i] :
( ( A != sk2 )
| ( A
!= ( C @ ( B @ orthogonal_through_point ) ) )
| ~ ( sk2 @ ( C @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[23196]) ).
thf(23324,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ orthogonal_through_point ) )
!= sk2 )
| ~ ( sk2 @ ( B @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[23258]) ).
thf(202,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( A @ apart_point_and_line ) )
!= ( E @ ( F @ parallel_through_point ) @ ( E @ apart_point_and_line ) ) )
| ~ $true
| ( D @ ( B @ apart_point_and_line ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(paramod_ordered,[status(thm)],[44,83]) ).
thf(203,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( A @ apart_point_and_line ) )
!= ( E @ ( F @ parallel_through_point ) @ ( E @ apart_point_and_line ) ) )
| ( D @ ( B @ apart_point_and_line ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[202]) ).
thf(204,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ parallel_through_point ) @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ( B @ ( D @ apart_point_and_line ) )
| ~ ( D @ ( C @ parallel_through_point ) @ ( B @ distinct_lines ) )
| ~ ( A @ ( D @ distinct_points ) ) ),
inference(pattern_uni,[status(thm)],[203:[bind(A,$thf( H )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( H @ ( G @ parallel_through_point ) )),bind(E,$thf( H )),bind(F,$thf( G ))]]) ).
thf(213,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( C @ parallel_through_point ) @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ( B @ ( D @ apart_point_and_line ) )
| ~ ( D @ ( C @ parallel_through_point ) @ ( B @ distinct_lines ) )
| ~ ( A @ ( D @ distinct_points ) ) ),
inference(simp,[status(thm)],[204]) ).
thf(11564,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ ( sk2 @ orthogonal_through_point ) @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ $true
| ~ ( C @ ( B @ parallel_lines ) ) ),
inference(paramod_ordered,[status(thm)],[11041,107]) ).
thf(11565,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ ( sk2 @ orthogonal_through_point ) @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( C @ ( B @ parallel_lines ) ) ),
inference(simp,[status(thm)],[11564]) ).
thf(11566,plain,
! [A: $i] :
~ ( sk3 @ ( A @ ( sk2 @ orthogonal_through_point ) @ parallel_lines ) ),
inference(pattern_uni,[status(thm)],[11565:[bind(A,$thf( E )),bind(B,$thf( E @ ( sk2 @ orthogonal_through_point ) )),bind(C,$thf( sk3 ))]]) ).
thf(11583,plain,
! [A: $i] :
~ ( sk3 @ ( A @ ( sk2 @ orthogonal_through_point ) @ parallel_lines ) ),
inference(simp,[status(thm)],[11566]) ).
thf(189,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ apart_point_and_line ) )
!= ( E @ ( F @ orthogonal_through_point ) @ ( E @ apart_point_and_line ) ) )
| ~ $true
| ( D @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(paramod_ordered,[status(thm)],[44,80]) ).
thf(190,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ apart_point_and_line ) )
!= ( E @ ( F @ orthogonal_through_point ) @ ( E @ apart_point_and_line ) ) )
| ( D @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[189]) ).
thf(191,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( D @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ( D @ ( C @ orthogonal_through_point ) @ ( A @ apart_point_and_line ) )
| ~ ( B @ ( D @ ( C @ orthogonal_through_point ) @ distinct_lines ) )
| ~ ( D @ ( A @ distinct_points ) ) ),
inference(pattern_uni,[status(thm)],[190:[bind(A,$thf( A )),bind(B,$thf( H )),bind(C,$thf( H @ ( G @ orthogonal_through_point ) )),bind(D,$thf( D )),bind(E,$thf( H )),bind(F,$thf( G ))]]) ).
thf(198,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( D @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ( D @ ( C @ orthogonal_through_point ) @ ( A @ apart_point_and_line ) )
| ~ ( B @ ( D @ ( C @ orthogonal_through_point ) @ distinct_lines ) )
| ~ ( D @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[191]) ).
thf(21021,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ orthogonal_through_point ) @ ( A @ distinct_lines ) )
!= ( sk2 @ ( sk3 @ distinct_lines ) ) )
| ~ $true
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[349,1712]) ).
thf(21022,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ orthogonal_through_point ) @ ( A @ distinct_lines ) )
!= ( sk2 @ ( sk3 @ distinct_lines ) ) )
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[21021]) ).
thf(21227,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ orthogonal_through_point ) )
!= sk2 )
| ( A != sk3 )
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[21022]) ).
thf(21341,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ orthogonal_through_point ) )
!= sk2 )
| ~ ( sk3 @ ( B @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[21227]) ).
thf(145,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ convergent_lines ) )
| ( C @ ( A @ unorthogonal_lines ) )
| ( B @ ( A @ unorthogonal_lines ) ) ),
inference(cnf,[status(esa)],[144]) ).
thf(3504,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ $true
| ( C @ ( A @ unorthogonal_lines ) )
| ( B @ ( A @ unorthogonal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[40,145]) ).
thf(3505,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ( C @ ( A @ unorthogonal_lines ) )
| ( B @ ( A @ unorthogonal_lines ) ) ),
inference(simp,[status(thm)],[3504]) ).
thf(3506,plain,
! [A: $i] :
( ( sk2 @ ( A @ unorthogonal_lines ) )
| ( sk1 @ ( A @ unorthogonal_lines ) ) ),
inference(pattern_uni,[status(thm)],[3505:[bind(A,$thf( A )),bind(B,$thf( sk1 )),bind(C,$thf( sk2 ))]]) ).
thf(14963,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ unorthogonal_lines ) )
!= ( C @ ( B @ ( C @ orthogonal_through_point ) @ unorthogonal_lines ) ) )
| ~ $true
| ( sk1 @ ( A @ unorthogonal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[3506,50]) ).
thf(14964,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ unorthogonal_lines ) )
!= ( C @ ( B @ ( C @ orthogonal_through_point ) @ unorthogonal_lines ) ) )
| ( sk1 @ ( A @ unorthogonal_lines ) ) ),
inference(simp,[status(thm)],[14963]) ).
thf(14965,plain,
! [A: $i] : ( sk1 @ ( A @ ( sk2 @ orthogonal_through_point ) @ unorthogonal_lines ) ),
inference(pattern_uni,[status(thm)],[14964:[bind(A,$thf( E @ ( sk2 @ orthogonal_through_point ) )),bind(B,$thf( E )),bind(C,$thf( sk2 ))]]) ).
thf(14979,plain,
! [A: $i] : ( sk1 @ ( A @ ( sk2 @ orthogonal_through_point ) @ unorthogonal_lines ) ),
inference(simp,[status(thm)],[14965]) ).
thf(15211,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ ( A @ ( sk2 @ orthogonal_through_point ) @ unorthogonal_lines ) )
!= ( C @ ( B @ ( C @ orthogonal_through_point ) @ unorthogonal_lines ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[14979,50]) ).
thf(15212,plain,
! [C: $i,B: $i,A: $i] :
( ( sk1 @ ( A @ ( sk2 @ orthogonal_through_point ) @ unorthogonal_lines ) )
!= ( C @ ( B @ ( C @ orthogonal_through_point ) @ unorthogonal_lines ) ) ),
inference(simp,[status(thm)],[15211]) ).
thf(15222,plain,
! [C: $i,B: $i,A: $i] :
( ( sk1 != C )
| ( ( A @ ( sk2 @ orthogonal_through_point ) )
!= ( B @ ( C @ orthogonal_through_point ) ) ) ),
inference(simp,[status(thm)],[15212]) ).
thf(15227,plain,
! [B: $i,A: $i] :
( ( A @ ( sk2 @ orthogonal_through_point ) )
!= ( B @ ( sk1 @ orthogonal_through_point ) ) ),
inference(simp,[status(thm)],[15222]) ).
thf(21152,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ orthogonal_through_point ) @ ( A @ distinct_lines ) )
!= ( sk3 @ ( sk2 @ distinct_lines ) ) )
| ~ $true
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[349,410]) ).
thf(21153,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ orthogonal_through_point ) @ ( A @ distinct_lines ) )
!= ( sk3 @ ( sk2 @ distinct_lines ) ) )
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[21152]) ).
thf(21231,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ orthogonal_through_point ) )
!= sk3 )
| ( A != sk2 )
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[21153]) ).
thf(21346,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ orthogonal_through_point ) )
!= sk3 )
| ~ ( sk2 @ ( B @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[21231]) ).
thf(90,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ incident_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) ) ),
inference(cnfConj,[status(thm)],[88]) ).
thf(91,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ incident_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[90]) ).
thf(1394,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_points ) )
!= ( C @ ( D @ distinct_points ) ) )
| ( D @ ( C @ distinct_points ) )
| ~ $true
| ( B @ ( A @ equal_points ) ) ),
inference(paramod_ordered,[status(thm)],[118,1374]) ).
thf(1395,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_points ) )
!= ( C @ ( D @ distinct_points ) ) )
| ( D @ ( C @ distinct_points ) )
| ( B @ ( A @ equal_points ) ) ),
inference(simp,[status(thm)],[1394]) ).
thf(1396,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ distinct_points ) )
| ( B @ ( A @ equal_points ) ) ),
inference(pattern_uni,[status(thm)],[1395:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(2295,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( sk3 @ distinct_lines ) ) )
| ~ ( sk2 @ ( C @ equal_lines ) )
| ~ $true
| ( B @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[136,2211]) ).
thf(2296,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( sk3 @ distinct_lines ) ) )
| ~ ( sk2 @ ( C @ equal_lines ) )
| ( B @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[2295]) ).
thf(2297,plain,
! [A: $i] :
( ~ ( sk2 @ ( A @ equal_lines ) )
| ( A @ ( sk3 @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[2296:[bind(A,$thf( sk3 )),bind(B,$thf( B )),bind(C,$thf( B ))]]) ).
thf(2303,plain,
! [A: $i] :
( ~ ( sk2 @ ( A @ equal_lines ) )
| ( A @ ( sk3 @ equal_lines ) ) ),
inference(simp,[status(thm)],[2297]) ).
thf(22,axiom,
! [A: $i,B: $i] :
( ( ( B @ ( A @ convergent_lines ) )
& ( B @ line )
& ( A @ line ) )
=> ( B @ ( A @ intersection_point ) @ point ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',int1) ).
thf(99,plain,
! [A: $i,B: $i] :
( ( ( B @ ( A @ convergent_lines ) )
& ( B @ line )
& ( A @ line ) )
=> ( B @ ( A @ intersection_point ) @ point ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(100,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ intersection_point ) @ point )
| ~ ( B @ ( A @ convergent_lines ) )
| ~ ( B @ line )
| ~ ( A @ line ) ),
inference(cnf,[status(esa)],[99]) ).
thf(2105,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ( B @ ( A @ intersection_point ) @ point )
| ~ $true
| ~ ( B @ line )
| ~ ( A @ line ) ),
inference(paramod_ordered,[status(thm)],[40,100]) ).
thf(2106,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ( B @ ( A @ intersection_point ) @ point )
| ~ ( B @ line )
| ~ ( A @ line ) ),
inference(simp,[status(thm)],[2105]) ).
thf(2107,plain,
( ( sk2 @ ( sk1 @ intersection_point ) @ point )
| ~ ( sk2 @ line )
| ~ ( sk1 @ line ) ),
inference(pattern_uni,[status(thm)],[2106:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(20985,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ orthogonal_through_point ) @ ( A @ distinct_lines ) )
!= ( D @ ( sk3 @ distinct_lines ) ) )
| ~ ( sk2 @ ( D @ equal_lines ) )
| ~ $true
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[349,2211]) ).
thf(20986,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ orthogonal_through_point ) @ ( A @ distinct_lines ) )
!= ( D @ ( sk3 @ distinct_lines ) ) )
| ~ ( sk2 @ ( D @ equal_lines ) )
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[20985]) ).
thf(20987,plain,
! [B: $i,A: $i] :
( ~ ( sk2 @ ( B @ ( A @ orthogonal_through_point ) @ equal_lines ) )
| ~ ( sk3 @ ( B @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[20986:[bind(A,$thf( sk3 )),bind(B,$thf( E )),bind(C,$thf( F )),bind(D,$thf( F @ ( E @ orthogonal_through_point ) ))]]) ).
thf(21350,plain,
! [B: $i,A: $i] :
( ~ ( sk2 @ ( B @ ( A @ orthogonal_through_point ) @ equal_lines ) )
| ~ ( sk3 @ ( B @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[20987]) ).
thf(11555,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ ( sk2 @ orthogonal_through_point ) @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( B @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[11041,143]) ).
thf(11556,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ ( sk2 @ orthogonal_through_point ) @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( B @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[11555]) ).
thf(11557,plain,
! [A: $i] :
~ ( A @ ( sk2 @ orthogonal_through_point ) @ ( sk3 @ ( A @ ( sk2 @ orthogonal_through_point ) @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[11556:[bind(A,$thf( E )),bind(B,$thf( E @ ( sk2 @ orthogonal_through_point ) )),bind(C,$thf( sk3 ))]]) ).
thf(11579,plain,
! [A: $i] :
~ ( A @ ( sk2 @ orthogonal_through_point ) @ ( sk3 @ ( A @ ( sk2 @ orthogonal_through_point ) @ intersection_point ) @ apart_point_and_line ) ),
inference(simp,[status(thm)],[11557]) ).
thf(9,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ distinct_points ) )
=> ~ ( B @ ( A @ line_connecting ) @ ( B @ apart_point_and_line ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ci2) ).
thf(62,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ distinct_points ) )
=> ~ ( B @ ( A @ line_connecting ) @ ( B @ apart_point_and_line ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(63,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ line_connecting ) @ ( B @ apart_point_and_line ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(cnf,[status(esa)],[62]) ).
thf(13965,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( A @ equal_lines ) )
!= ( sk3 @ ( B @ equal_lines ) ) )
| ~ $true
| ~ ( sk2 @ ( B @ distinct_lines ) )
| ~ ( sk2 @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[3363,1706]) ).
thf(13966,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( A @ equal_lines ) )
!= ( sk3 @ ( B @ equal_lines ) ) )
| ~ ( sk2 @ ( B @ distinct_lines ) )
| ~ ( sk2 @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[13965]) ).
thf(13967,plain,
! [A: $i] :
( ~ ( sk2 @ ( A @ distinct_lines ) )
| ~ ( sk2 @ ( A @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[13966:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(150,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ unorthogonal_lines ) )
| ~ ( C @ ( B @ convergent_lines ) )
| ( C @ ( A @ convergent_lines ) )
| ( B @ ( A @ convergent_lines ) ) ),
inference(cnfConj,[status(thm)],[149]) ).
thf(3450,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( sk2 @ distinct_lines ) ) )
| ~ ( sk2 @ ( C @ equal_lines ) )
| ~ $true
| ( B @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[136,3135]) ).
thf(3451,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( sk2 @ distinct_lines ) ) )
| ~ ( sk2 @ ( C @ equal_lines ) )
| ( B @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[3450]) ).
thf(3452,plain,
! [A: $i] :
( ~ ( sk2 @ ( A @ equal_lines ) )
| ( A @ ( sk2 @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[3451:[bind(A,$thf( sk2 )),bind(B,$thf( B )),bind(C,$thf( B ))]]) ).
thf(3462,plain,
! [A: $i] :
( ~ ( sk2 @ ( A @ equal_lines ) )
| ( A @ ( sk2 @ equal_lines ) ) ),
inference(simp,[status(thm)],[3452]) ).
thf(261,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( F @ ( E @ apart_point_and_line ) ) )
| ~ $true
| ~ ( F @ ( E @ incident_point_and_line ) )
| ( D @ ( C @ unorthogonal_lines ) )
| ( D @ ( B @ unorthogonal_lines ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( C @ ( B @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[47,89]) ).
thf(262,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( F @ ( E @ apart_point_and_line ) ) )
| ~ ( F @ ( E @ incident_point_and_line ) )
| ( D @ ( C @ unorthogonal_lines ) )
| ( D @ ( B @ unorthogonal_lines ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( C @ ( B @ distinct_lines ) ) ),
inference(simp,[status(thm)],[261]) ).
thf(263,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ incident_point_and_line ) )
| ( D @ ( C @ unorthogonal_lines ) )
| ( D @ ( B @ unorthogonal_lines ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( C @ ( B @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[262:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( A )),bind(F,$thf( C ))]]) ).
thf(11,axiom,
! [A: $i,B: $i] :
( ( ( B @ ( A @ distinct_points ) )
& ( B @ point )
& ( A @ point ) )
=> ( B @ ( A @ line_connecting ) @ line ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',con1) ).
thf(67,plain,
! [A: $i,B: $i] :
( ( ( B @ ( A @ distinct_points ) )
& ( B @ point )
& ( A @ point ) )
=> ( B @ ( A @ line_connecting ) @ line ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(21219,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ orthogonal_through_point ) @ ( A @ distinct_lines ) )
!= ( D @ ( sk2 @ distinct_lines ) ) )
| ~ ( sk3 @ ( D @ equal_lines ) )
| ~ $true
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[349,1917]) ).
thf(21220,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ orthogonal_through_point ) @ ( A @ distinct_lines ) )
!= ( D @ ( sk2 @ distinct_lines ) ) )
| ~ ( sk3 @ ( D @ equal_lines ) )
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[21219]) ).
thf(21221,plain,
! [B: $i,A: $i] :
( ~ ( sk3 @ ( B @ ( A @ orthogonal_through_point ) @ equal_lines ) )
| ~ ( sk2 @ ( B @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[21220:[bind(A,$thf( sk2 )),bind(B,$thf( E )),bind(C,$thf( F )),bind(D,$thf( F @ ( E @ orthogonal_through_point ) ))]]) ).
thf(21333,plain,
! [B: $i,A: $i] :
( ~ ( sk3 @ ( B @ ( A @ orthogonal_through_point ) @ equal_lines ) )
| ~ ( sk2 @ ( B @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[21221]) ).
thf(1811,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( sk2 @ ( C @ distinct_lines ) ) )
| ~ ( sk3 @ ( C @ equal_lines ) )
| ~ $true
| ( B @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[136,1706]) ).
thf(1812,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( sk2 @ ( C @ distinct_lines ) ) )
| ~ ( sk3 @ ( C @ equal_lines ) )
| ( B @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[1811]) ).
thf(1813,plain,
! [A: $i] :
( ~ ( sk3 @ ( A @ equal_lines ) )
| ( sk2 @ ( A @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[1812:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( A ))]]) ).
thf(168,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ $true
| ( ( D @ ( B @ apart_point_and_line ) )
!= ( C @ ( A @ apart_point_and_line ) ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(eqfactor_ordered,[status(thm)],[44]) ).
thf(176,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( B @ ( B @ distinct_lines ) )
| ~ ( A @ ( A @ distinct_points ) ) ),
inference(pattern_uni,[status(thm)],[168:[bind(A,$thf( B )),bind(B,$thf( B )),bind(C,$thf( D ))]]) ).
thf(177,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ apart_point_and_line ) )
| ~ ( B @ ( B @ distinct_lines ) )
| ~ ( A @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[176]) ).
thf(127,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ convergent_lines ) )
| ( C @ ( A @ unorthogonal_lines ) )
| ~ ( B @ ( A @ unorthogonal_lines ) )
| ~ ( B @ ( A @ convergent_lines ) ) ),
inference(cnfConj,[status(thm)],[124]) ).
thf(8799,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( A @ ( sk3 @ orthogonal_through_point ) @ convergent_lines ) )
!= ( B @ ( B @ convergent_lines ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8788,156]) ).
thf(8800,plain,
! [B: $i,A: $i] :
( ( sk2 @ ( A @ ( sk3 @ orthogonal_through_point ) @ convergent_lines ) )
!= ( B @ ( B @ convergent_lines ) ) ),
inference(simp,[status(thm)],[8799]) ).
thf(8839,plain,
! [B: $i,A: $i] :
( ( sk2 != B )
| ( ( A @ ( sk3 @ orthogonal_through_point ) )
!= B ) ),
inference(simp,[status(thm)],[8800]) ).
thf(8850,plain,
! [A: $i] :
( ( A @ ( sk3 @ orthogonal_through_point ) )
!= sk2 ),
inference(simp,[status(thm)],[8839]) ).
thf(1419,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_points ) )
!= ( D @ ( C @ distinct_points ) ) )
| ~ $true
| ~ ( D @ ( C @ equal_points ) )
| ~ ( A @ ( A @ distinct_points ) ) ),
inference(paramod_ordered,[status(thm)],[1375,116]) ).
thf(1420,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_points ) )
!= ( D @ ( C @ distinct_points ) ) )
| ~ ( D @ ( C @ equal_points ) )
| ~ ( A @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[1419]) ).
thf(1421,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ equal_points ) )
| ~ ( A @ ( A @ distinct_points ) ) ),
inference(pattern_uni,[status(thm)],[1420:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(215,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ parallel_through_point ) @ convergent_lines ) )
!= ( sk2 @ ( sk1 @ convergent_lines ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[40,112]) ).
thf(216,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( B @ parallel_through_point ) @ convergent_lines ) )
!= ( sk2 @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[215]) ).
thf(217,plain,
! [B: $i,A: $i] :
( ( B != sk2 )
| ( ( A @ ( B @ parallel_through_point ) )
!= sk1 ) ),
inference(simp,[status(thm)],[216]) ).
thf(218,plain,
! [A: $i] :
( ( A @ ( sk2 @ parallel_through_point ) )
!= sk1 ),
inference(simp,[status(thm)],[217]) ).
thf(11533,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ ( sk2 @ orthogonal_through_point ) @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( C @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[11041,141]) ).
thf(11534,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ ( sk2 @ orthogonal_through_point ) @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( C @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[11533]) ).
thf(11535,plain,
! [A: $i] :
~ ( sk3 @ ( sk3 @ ( A @ ( sk2 @ orthogonal_through_point ) @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[11534:[bind(A,$thf( E )),bind(B,$thf( E @ ( sk2 @ orthogonal_through_point ) )),bind(C,$thf( sk3 ))]]) ).
thf(11584,plain,
! [A: $i] :
~ ( sk3 @ ( sk3 @ ( A @ ( sk2 @ orthogonal_through_point ) @ intersection_point ) @ apart_point_and_line ) ),
inference(simp,[status(thm)],[11535]) ).
thf(310,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ distinct_lines ) )
!= ( F @ ( E @ distinct_lines ) ) )
| ( G @ ( F @ unorthogonal_lines ) )
| ( G @ ( E @ unorthogonal_lines ) )
| ( F @ ( D @ apart_point_and_line ) )
| ( E @ ( D @ apart_point_and_line ) )
| ~ $true
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[53,47]) ).
thf(311,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ distinct_lines ) )
!= ( F @ ( E @ distinct_lines ) ) )
| ( G @ ( F @ unorthogonal_lines ) )
| ( G @ ( E @ unorthogonal_lines ) )
| ( F @ ( D @ apart_point_and_line ) )
| ( E @ ( D @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[310]) ).
thf(312,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ unorthogonal_lines ) )
| ( E @ ( B @ unorthogonal_lines ) )
| ( C @ ( D @ apart_point_and_line ) )
| ( B @ ( D @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[311:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( B )),bind(F,$thf( C ))]]) ).
thf(351,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( C @ unorthogonal_lines ) )
| ( E @ ( B @ unorthogonal_lines ) )
| ( C @ ( D @ apart_point_and_line ) )
| ( B @ ( D @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[312]) ).
thf(3334,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( sk2 @ ( B @ distinct_lines ) ) )
| ( sk3 @ ( B @ distinct_lines ) )
| ~ $true
| ( sk3 @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[2164,1676]) ).
thf(3335,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( A @ distinct_lines ) )
!= ( sk2 @ ( B @ distinct_lines ) ) )
| ( sk3 @ ( B @ distinct_lines ) )
| ( sk3 @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[3334]) ).
thf(3336,plain,
! [A: $i] :
( ( sk3 @ ( A @ distinct_lines ) )
| ( sk3 @ ( A @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[3335:[bind(A,$thf( A )),bind(B,$thf( A ))]]) ).
thf(8910,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ $true
| ~ ( B @ ( A @ parallel_lines ) ) ),
inference(paramod_ordered,[status(thm)],[8868,107]) ).
thf(8911,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ ( B @ ( A @ parallel_lines ) ) ),
inference(simp,[status(thm)],[8910]) ).
thf(8912,plain,
~ ( sk3 @ ( sk1 @ parallel_lines ) ),
inference(pattern_uni,[status(thm)],[8911:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 ))]]) ).
thf(15205,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ ( A @ ( sk2 @ orthogonal_through_point ) @ unorthogonal_lines ) )
!= ( C @ ( B @ unorthogonal_lines ) ) )
| ~ $true
| ~ ( C @ ( B @ orthogonal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[14979,59]) ).
thf(15206,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ ( A @ ( sk2 @ orthogonal_through_point ) @ unorthogonal_lines ) )
!= ( C @ ( B @ unorthogonal_lines ) ) )
| ~ ( C @ ( B @ orthogonal_lines ) ) ),
inference(simp,[status(thm)],[15205]) ).
thf(15207,plain,
! [A: $i] :
~ ( sk1 @ ( A @ ( sk2 @ orthogonal_through_point ) @ orthogonal_lines ) ),
inference(pattern_uni,[status(thm)],[15206:[bind(A,$thf( E )),bind(B,$thf( E @ ( sk2 @ orthogonal_through_point ) )),bind(C,$thf( sk1 ))]]) ).
thf(15228,plain,
! [A: $i] :
~ ( sk1 @ ( A @ ( sk2 @ orthogonal_through_point ) @ orthogonal_lines ) ),
inference(simp,[status(thm)],[15207]) ).
thf(55,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ parallel_through_point ) @ line )
| ~ ( B @ point )
| ~ ( A @ line ) ),
inference(cnf,[status(esa)],[54]) ).
thf(1148,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ parallel_through_point ) @ ( A @ distinct_lines ) )
!= ( E @ ( D @ distinct_lines ) ) )
| ~ $true
| ~ ( E @ ( D @ equal_lines ) )
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[345,134]) ).
thf(1149,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ parallel_through_point ) @ ( A @ distinct_lines ) )
!= ( E @ ( D @ distinct_lines ) ) )
| ~ ( E @ ( D @ equal_lines ) )
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[1148]) ).
thf(1150,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ parallel_through_point ) @ ( A @ equal_lines ) )
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[1149:[bind(A,$thf( A )),bind(B,$thf( F )),bind(C,$thf( G )),bind(D,$thf( A )),bind(E,$thf( G @ ( F @ parallel_through_point ) ))]]) ).
thf(1212,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ parallel_through_point ) @ ( A @ equal_lines ) )
| ~ ( A @ ( C @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[1150]) ).
thf(327,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( E @ ( D @ apart_point_and_line ) ) )
| ( F @ ( D @ apart_point_and_line ) )
| ( F @ ( E @ distinct_lines ) )
| ~ $true
| ( C @ ( B @ distinct_lines ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[53,53]) ).
thf(328,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( E @ ( D @ apart_point_and_line ) ) )
| ( F @ ( D @ apart_point_and_line ) )
| ( F @ ( E @ distinct_lines ) )
| ( C @ ( B @ distinct_lines ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[327]) ).
thf(329,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( A @ apart_point_and_line ) )
| ( D @ ( C @ distinct_lines ) )
| ( C @ ( B @ distinct_lines ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[328:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( A )),bind(E,$thf( C ))]]) ).
thf(346,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( D @ ( A @ apart_point_and_line ) )
| ( D @ ( C @ distinct_lines ) )
| ( C @ ( B @ distinct_lines ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[329]) ).
thf(205,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ apart_point_and_line ) )
!= ( E @ ( F @ parallel_through_point ) @ ( E @ apart_point_and_line ) ) )
| ~ $true
| ( D @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(paramod_ordered,[status(thm)],[44,83]) ).
thf(206,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ apart_point_and_line ) )
!= ( E @ ( F @ parallel_through_point ) @ ( E @ apart_point_and_line ) ) )
| ( D @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[205]) ).
thf(207,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( D @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ( D @ ( C @ parallel_through_point ) @ ( A @ apart_point_and_line ) )
| ~ ( B @ ( D @ ( C @ parallel_through_point ) @ distinct_lines ) )
| ~ ( D @ ( A @ distinct_points ) ) ),
inference(pattern_uni,[status(thm)],[206:[bind(A,$thf( A )),bind(B,$thf( H )),bind(C,$thf( H @ ( G @ parallel_through_point ) )),bind(D,$thf( D )),bind(E,$thf( H )),bind(F,$thf( G ))]]) ).
thf(214,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( D @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ( D @ ( C @ parallel_through_point ) @ ( A @ apart_point_and_line ) )
| ~ ( B @ ( D @ ( C @ parallel_through_point ) @ distinct_lines ) )
| ~ ( D @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[207]) ).
thf(151,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ unorthogonal_lines ) )
| ~ ( C @ ( B @ convergent_lines ) )
| ( C @ ( A @ unorthogonal_lines ) )
| ( B @ ( A @ convergent_lines ) ) ),
inference(cnfConj,[status(thm)],[149]) ).
thf(938,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( sk1 @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) )
| ~ $true
| ( C @ ( B @ distinct_lines ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[53,920]) ).
thf(939,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( sk1 @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) )
| ( C @ ( B @ distinct_lines ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[938]) ).
thf(940,plain,
! [A: $i] :
( ( sk1 @ ( A @ distinct_lines ) )
| ~ ( A @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[939:[bind(A,$thf( sk2 @ ( sk1 @ intersection_point ) )),bind(B,$thf( B )),bind(C,$thf( sk1 ))]]) ).
thf(967,plain,
! [A: $i] :
( ( sk1 @ ( A @ distinct_lines ) )
| ~ ( A @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[940]) ).
thf(240,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unorthogonal_lines ) )
!= ( D @ ( C @ unorthogonal_lines ) ) )
| ~ $true
| ~ ( D @ ( C @ orthogonal_lines ) )
| ( B @ ( A @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[103,59]) ).
thf(241,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ unorthogonal_lines ) )
!= ( D @ ( C @ unorthogonal_lines ) ) )
| ~ ( D @ ( C @ orthogonal_lines ) )
| ( B @ ( A @ convergent_lines ) ) ),
inference(simp,[status(thm)],[240]) ).
thf(242,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ orthogonal_lines ) )
| ( B @ ( A @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[241:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(192,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( B @ apart_point_and_line ) )
!= ( E @ ( F @ orthogonal_through_point ) @ ( E @ apart_point_and_line ) ) )
| ~ $true
| ( C @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(paramod_ordered,[status(thm)],[44,80]) ).
thf(193,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( B @ apart_point_and_line ) )
!= ( E @ ( F @ orthogonal_through_point ) @ ( E @ apart_point_and_line ) ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[192]) ).
thf(194,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( D @ apart_point_and_line ) )
| ( D @ ( C @ orthogonal_through_point ) @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ orthogonal_through_point ) @ ( B @ distinct_lines ) )
| ~ ( D @ ( A @ distinct_points ) ) ),
inference(pattern_uni,[status(thm)],[193:[bind(A,$thf( A )),bind(B,$thf( H )),bind(C,$thf( C )),bind(D,$thf( H @ ( G @ orthogonal_through_point ) )),bind(E,$thf( H )),bind(F,$thf( G ))]]) ).
thf(195,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( B @ ( D @ apart_point_and_line ) )
| ( D @ ( C @ orthogonal_through_point ) @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ orthogonal_through_point ) @ ( B @ distinct_lines ) )
| ~ ( D @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[194]) ).
thf(11026,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ $true
| ~ ( C @ ( B @ parallel_lines ) )
| ~ ( sk2 @ ( A @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[3289,107]) ).
thf(11027,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( C @ ( B @ parallel_lines ) )
| ~ ( sk2 @ ( A @ convergent_lines ) ) ),
inference(simp,[status(thm)],[11026]) ).
thf(11028,plain,
! [A: $i] :
( ~ ( sk3 @ ( A @ parallel_lines ) )
| ~ ( sk2 @ ( A @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[11027:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk3 ))]]) ).
thf(126,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ unorthogonal_lines ) )
| ( C @ ( A @ convergent_lines ) )
| ~ ( B @ ( A @ unorthogonal_lines ) )
| ~ ( B @ ( A @ convergent_lines ) ) ),
inference(cnfConj,[status(thm)],[124]) ).
thf(953,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ apart_point_and_line ) )
!= ( sk1 @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) )
| ~ $true
| ( C @ ( A @ distinct_points ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[66,920]) ).
thf(954,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ apart_point_and_line ) )
!= ( sk1 @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) )
| ( C @ ( A @ distinct_points ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[953]) ).
thf(955,plain,
! [A: $i] :
( ( sk2 @ ( sk1 @ intersection_point ) @ ( A @ distinct_points ) )
| ~ ( sk1 @ ( A @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[954:[bind(A,$thf( A )),bind(B,$thf( sk1 )),bind(C,$thf( sk2 @ ( sk1 @ intersection_point ) ))]]) ).
thf(2492,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( sk2 @ distinct_lines ) ) )
| ( sk3 @ ( C @ convergent_lines ) )
| ~ $true
| ( B @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[136,1892]) ).
thf(2493,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( sk2 @ distinct_lines ) ) )
| ( sk3 @ ( C @ convergent_lines ) )
| ( B @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[2492]) ).
thf(2494,plain,
! [A: $i] :
( ( sk3 @ ( A @ convergent_lines ) )
| ( A @ ( sk2 @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[2493:[bind(A,$thf( sk2 )),bind(B,$thf( B )),bind(C,$thf( B ))]]) ).
thf(2502,plain,
! [A: $i] :
( ( sk3 @ ( A @ convergent_lines ) )
| ( A @ ( sk2 @ equal_lines ) ) ),
inference(simp,[status(thm)],[2494]) ).
thf(330,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ distinct_lines ) )
!= ( G @ ( F @ distinct_lines ) ) )
| ( G @ ( E @ apart_point_and_line ) )
| ( F @ ( E @ apart_point_and_line ) )
| ( G @ ( D @ apart_point_and_line ) )
| ( F @ ( D @ apart_point_and_line ) )
| ~ $true
| ~ ( E @ ( D @ distinct_points ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[53,44]) ).
thf(331,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ distinct_lines ) )
!= ( G @ ( F @ distinct_lines ) ) )
| ( G @ ( E @ apart_point_and_line ) )
| ( F @ ( E @ apart_point_and_line ) )
| ( G @ ( D @ apart_point_and_line ) )
| ( F @ ( D @ apart_point_and_line ) )
| ~ ( E @ ( D @ distinct_points ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[330]) ).
thf(332,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( E @ apart_point_and_line ) )
| ( B @ ( E @ apart_point_and_line ) )
| ( C @ ( D @ apart_point_and_line ) )
| ( B @ ( D @ apart_point_and_line ) )
| ~ ( E @ ( D @ distinct_points ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[331:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( E )),bind(F,$thf( B )),bind(G,$thf( C ))]]) ).
thf(68,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ line_connecting ) @ line )
| ~ ( B @ ( A @ distinct_points ) )
| ~ ( B @ point )
| ~ ( A @ point ) ),
inference(cnf,[status(esa)],[67]) ).
thf(170,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ $true
| ( ( D @ ( B @ apart_point_and_line ) )
!= ( C @ ( B @ apart_point_and_line ) ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(eqfactor_ordered,[status(thm)],[44]) ).
thf(171,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( C @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(pattern_uni,[status(thm)],[170:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( D ))]]) ).
thf(178,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ apart_point_and_line ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( C @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[171]) ).
thf(251,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ unorthogonal_lines ) )
!= ( F @ ( E @ ( F @ orthogonal_through_point ) @ unorthogonal_lines ) ) )
| ~ $true
| ( D @ ( B @ unorthogonal_lines ) )
| ( C @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( C @ ( B @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[47,50]) ).
thf(252,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ unorthogonal_lines ) )
!= ( F @ ( E @ ( F @ orthogonal_through_point ) @ unorthogonal_lines ) ) )
| ( D @ ( B @ unorthogonal_lines ) )
| ( C @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( C @ ( B @ distinct_lines ) ) ),
inference(simp,[status(thm)],[251]) ).
thf(253,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( B @ unorthogonal_lines ) )
| ( D @ ( C @ orthogonal_through_point ) @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ orthogonal_through_point ) @ ( B @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[252:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( H @ ( D @ orthogonal_through_point ) )),bind(D,$thf( D )),bind(E,$thf( H )),bind(F,$thf( D ))]]) ).
thf(277,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( C @ ( B @ unorthogonal_lines ) )
| ( D @ ( C @ orthogonal_through_point ) @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ orthogonal_through_point ) @ ( B @ distinct_lines ) ) ),
inference(simp,[status(thm)],[253]) ).
thf(8820,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ ( sk3 @ orthogonal_through_point ) @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( B @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[8788,143]) ).
thf(8821,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ ( sk3 @ orthogonal_through_point ) @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( B @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[8820]) ).
thf(8822,plain,
! [A: $i] :
~ ( A @ ( sk3 @ orthogonal_through_point ) @ ( sk2 @ ( A @ ( sk3 @ orthogonal_through_point ) @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[8821:[bind(A,$thf( E )),bind(B,$thf( E @ ( sk3 @ orthogonal_through_point ) )),bind(C,$thf( sk2 ))]]) ).
thf(8857,plain,
! [A: $i] :
~ ( A @ ( sk3 @ orthogonal_through_point ) @ ( sk2 @ ( A @ ( sk3 @ orthogonal_through_point ) @ intersection_point ) @ apart_point_and_line ) ),
inference(simp,[status(thm)],[8822]) ).
thf(225,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( F @ ( E @ apart_point_and_line ) ) )
| ~ $true
| ~ ( F @ ( E @ incident_point_and_line ) )
| ( D @ ( B @ apart_point_and_line ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(paramod_ordered,[status(thm)],[44,89]) ).
thf(226,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( F @ ( E @ apart_point_and_line ) ) )
| ~ ( F @ ( E @ incident_point_and_line ) )
| ( D @ ( B @ apart_point_and_line ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[225]) ).
thf(227,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ ( C @ ( A @ incident_point_and_line ) )
| ( D @ ( B @ apart_point_and_line ) )
| ( C @ ( B @ apart_point_and_line ) )
| ( D @ ( A @ apart_point_and_line ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(pattern_uni,[status(thm)],[226:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( A )),bind(F,$thf( C ))]]) ).
thf(1461,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_points ) )
!= ( C @ ( D @ distinct_points ) ) )
| ~ ( D @ ( C @ equal_points ) )
| ~ $true
| ~ ( A @ ( A @ distinct_points ) ) ),
inference(paramod_ordered,[status(thm)],[1375,1384]) ).
thf(1462,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_points ) )
!= ( C @ ( D @ distinct_points ) ) )
| ~ ( D @ ( C @ equal_points ) )
| ~ ( A @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[1461]) ).
thf(1463,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ equal_points ) )
| ~ ( A @ ( A @ distinct_points ) ) ),
inference(pattern_uni,[status(thm)],[1462:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(3278,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ( C @ ( A @ convergent_lines ) )
| ( C @ ( B @ distinct_lines ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[40,139]) ).
thf(3279,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ( C @ ( A @ convergent_lines ) )
| ( C @ ( B @ distinct_lines ) ) ),
inference(simp,[status(thm)],[3278]) ).
thf(3280,plain,
! [A: $i] :
( ( A @ ( sk1 @ convergent_lines ) )
| ( A @ ( sk2 @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[3279:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(3316,plain,
! [A: $i] :
( ( A @ ( sk1 @ convergent_lines ) )
| ( A @ ( sk2 @ distinct_lines ) ) ),
inference(simp,[status(thm)],[3280]) ).
thf(30668,plain,
$false,
inference(e,[status(thm)],[69,4201,365,101,347,468,2306,3345,8883,276,1142,269,56,3135,142,288,11588,3103,8851,1709,110,2185,2897,196,559,1892,13942,152,289,78,8870,164,2451,211,121,84,10972,348,147,11047,61,89,74,116,243,292,920,85,2164,2000,1206,233,1691,8927,2249,10975,137,3339,260,349,1676,38,92,197,97,2179,11646,2211,2228,324,8788,4192,650,156,1375,53,11089,141,1851,1772,109,77,4721,212,96,1776,2450,2006,129,41,11093,21270,134,8846,128,266,1712,1466,3841,618,148,45,3289,64,1374,11011,8903,2176,180,296,44,8872,59,3458,118,71,936,4186,3726,787,6794,1997,350,86,382,54,8862,144,1765,236,113,81,1048,8868,230,8926,274,2383,23324,345,103,140,213,66,11583,198,21341,14979,15227,21346,91,1396,11041,1775,3363,2303,431,80,2107,112,21350,11579,145,48,63,13967,150,95,3462,263,50,67,21333,1813,177,127,656,154,2145,72,8850,3256,143,43,1421,2626,99,218,104,2167,11584,40,351,3336,8912,139,15228,55,75,119,1706,1212,346,536,214,151,432,146,51,410,967,107,242,195,11028,94,1742,126,136,3506,955,2502,332,1384,528,68,62,178,277,8857,131,47,227,122,1944,83,1463,1917,3316,100]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO205+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.13/0.38 % Computer : n006.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.39 % DateTime : Fri Sep 25 13:05:41 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 1.12/1.08 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.66/1.34 % [INFO] Parsing done (254ms).
% 1.66/1.36 % [INFO] Running in sequential loop mode.
% 2.62/1.83 % [INFO] eprover registered as external prover.
% 2.62/1.84 % [INFO] Scanning for conjecture ...
% 2.81/1.97 % [INFO] Found a conjecture (or negated_conjecture) and 35 axioms. Running axiom selection ...
% 3.06/2.08 % [INFO] Axiom selection finished. Selected 35 axioms (removed 0 axioms).
% 3.29/2.17 % [INFO] Problem is first-order (TPTP FOF).
% 3.29/2.19 % [INFO] Type checking passed.
% 3.29/2.20 % [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 ...
% 88.06/19.26 % External prover 'e' found a proof!
% 88.06/19.26 % [INFO] Killing All external provers ...
% 88.06/19.26 % Time passed: 18671ms (effective reasoning time: 17899ms)
% 88.06/19.26 % 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)>
% 88.06/19.27 % Axioms used in derivation (35): par1, ouo1, ooc2, apart4, a5, ceq2, a4, ax1, oac1, orth1, ax2, a3, occu1, con1, cp2, apart3, ooc1, ceq3, ax6, cup1, ci4, couo1, int1, apart5, coipo1, ci3, apart1, ci2, cp1, ceq1, cu1, ci1, apart2, p1, cotno1
% 88.06/19.27 % No. of inferences in proof: 725
% 88.06/19.27 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 18671 ms resp. 17899 ms w/o parsing
% 75.06/19.63 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 75.06/19.64 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------