%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : GEO203+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:12:44 AM UTC 2026
% Result : Theorem 79.51s 17.85s
% Output : Refutation 80.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 58
% Number of leaves : 39
% Syntax : Number of formulae : 718 ( 133 unt; 0 typ; 3 def)
% Number of atoms : 3446 ( 480 equ; 0 cnn)
% Maximal formula atoms : 33 ( 4 avg)
% Number of connectives : 11768 (2043 ~;1936 |; 66 &;7642 @)
% ( 5 <=>; 76 =>; 0 <=; 0 <~>)
% Maximal formula depth : 54 ( 10 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 : 2102 ( 0 ^;2086 !; 13 ?;2102 :)
% ( 0 !>; 0 ?*; 0 @-; 3 @+)
% Comments :
%------------------------------------------------------------------------------
thf(convergent_lines_decl,type,
convergent_lines: $i > $i > $o ).
thf(distinct_points_decl,type,
distinct_points: $i > $i > $o ).
thf(intersection_point_decl,type,
intersection_point: $i > $i > $i ).
thf(equal_lines_decl,type,
equal_lines: $i > $i > $o ).
thf(line_connecting_decl,type,
line_connecting: $i > $i > $i ).
thf(unorthogonal_lines_decl,type,
unorthogonal_lines: $i > $i > $o ).
thf(orthogonal_through_point_decl,type,
orthogonal_through_point: $i > $i > $i ).
thf(apart_point_and_line_decl,type,
apart_point_and_line: $i > $i > $o ).
thf(distinct_lines_decl,type,
distinct_lines: $i > $i > $o ).
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(incident_point_and_line_decl,type,
incident_point_and_line: $i > $i > $o ).
thf(equal_points_decl,type,
equal_points: $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 @ ( A @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ distinct_points ) )
& ( C @ ( A @ convergent_lines ) )
& ( B @ ( A @ convergent_lines ) ) )
=> ( A @ ( C @ ( A @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ line_connecting ) @ equal_lines ) ) ) ) ) ).
thf(sk2_def,definition,
( sk2
= ( @+[A: $i] :
~ ! [B: $i] :
( ( ( B @ ( sk1 @ intersection_point ) @ ( A @ ( sk1 @ intersection_point ) @ distinct_points ) )
& ( B @ ( sk1 @ convergent_lines ) )
& ( A @ ( sk1 @ convergent_lines ) ) )
=> ( sk1 @ ( B @ ( sk1 @ intersection_point ) @ ( A @ ( sk1 @ intersection_point ) @ line_connecting ) @ equal_lines ) ) ) ) ) ).
thf(sk3_def,definition,
( sk3
= ( @+[A: $i] :
~ ( ( ( A @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ distinct_points ) )
& ( A @ ( sk1 @ convergent_lines ) )
& ( sk2 @ ( sk1 @ convergent_lines ) ) )
=> ( sk1 @ ( A @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ equal_lines ) ) ) ) ) ).
thf(10,axiom,
! [A: $i,B: $i] :
~ ( A @ ( B @ orthogonal_through_point ) @ ( A @ apart_point_and_line ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ooc2) ).
thf(67,plain,
! [A: $i,B: $i] :
~ ( A @ ( B @ orthogonal_through_point ) @ ( A @ apart_point_and_line ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(68,plain,
~ ? [A: $i,B: $i] : ( A @ ( B @ orthogonal_through_point ) @ ( A @ apart_point_and_line ) ),
inference(miniscope,[status(thm)],[67]) ).
thf(69,plain,
! [B: $i,A: $i] :
~ ( A @ ( B @ orthogonal_through_point ) @ ( A @ apart_point_and_line ) ),
inference(cnf,[status(esa)],[68]) ).
thf(1,conjecture,
! [A: $i,B: $i,C: $i] :
( ( ( C @ ( A @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ distinct_points ) )
& ( C @ ( A @ convergent_lines ) )
& ( B @ ( A @ convergent_lines ) ) )
=> ( A @ ( C @ ( A @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ line_connecting ) @ equal_lines ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',con) ).
thf(2,negated_conjecture,
~ ! [A: $i,B: $i,C: $i] :
( ( ( C @ ( A @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ distinct_points ) )
& ( C @ ( A @ convergent_lines ) )
& ( B @ ( A @ convergent_lines ) ) )
=> ( A @ ( C @ ( A @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ line_connecting ) @ equal_lines ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(38,plain,
~ ! [A: $i,B: $i,C: $i] :
( ( ( C @ ( A @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ distinct_points ) )
& ( C @ ( A @ convergent_lines ) )
& ( B @ ( A @ convergent_lines ) ) )
=> ( A @ ( C @ ( A @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ line_connecting ) @ equal_lines ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(39,plain,
( ~ ( sk1 @ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ equal_lines ) )
& ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ distinct_points ) )
& ( sk3 @ ( sk1 @ convergent_lines ) )
& ( sk2 @ ( sk1 @ convergent_lines ) ) ),
inference(cnf,[status(esa)],[38]) ).
thf(42,plain,
sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ distinct_points ),
inference(cnfConj,[status(thm)],[39]) ).
thf(17,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ distinct_points ) )
=> ( ( C @ ( B @ distinct_points ) )
| ( C @ ( A @ distinct_points ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',apart4) ).
thf(92,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)],[17]) ).
thf(93,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ distinct_points ) )
=> ! [C: $i] :
( ( C @ ( B @ distinct_points ) )
| ( C @ ( A @ distinct_points ) ) ) ),
inference(miniscope,[status(thm)],[92]) ).
thf(94,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ distinct_points ) )
| ( C @ ( A @ distinct_points ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(cnf,[status(esa)],[93]) ).
thf(1287,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ distinct_points ) )
!= ( B @ ( A @ distinct_points ) ) )
| ( C @ ( B @ distinct_points ) )
| ( C @ ( A @ distinct_points ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[42,94]) ).
thf(1288,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ distinct_points ) )
!= ( B @ ( A @ distinct_points ) ) )
| ( C @ ( B @ distinct_points ) )
| ( C @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[1287]) ).
thf(1289,plain,
! [A: $i] :
( ( A @ ( sk3 @ ( sk1 @ intersection_point ) @ distinct_points ) )
| ( A @ ( sk2 @ ( sk1 @ intersection_point ) @ distinct_points ) ) ),
inference(pattern_uni,[status(thm)],[1288:[bind(A,$thf( sk2 @ ( sk1 @ intersection_point ) )),bind(B,$thf( sk3 @ ( sk1 @ intersection_point ) )),bind(C,$thf( C ))]]) ).
thf(1326,plain,
! [A: $i] :
( ( A @ ( sk3 @ ( sk1 @ intersection_point ) @ distinct_points ) )
| ( A @ ( sk2 @ ( sk1 @ intersection_point ) @ distinct_points ) ) ),
inference(simp,[status(thm)],[1289]) ).
thf(14,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ equal_points ) )
<=> ~ ( B @ ( A @ distinct_points ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
thf(81,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)],[14]) ).
thf(82,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)],[81]) ).
thf(83,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)],[82]) ).
thf(84,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ distinct_points ) )
| ~ ( B @ ( A @ equal_points ) ) ),
inference(cnfConj,[status(thm)],[83]) ).
thf(1335,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk3 @ ( sk1 @ intersection_point ) @ distinct_points ) )
!= ( C @ ( B @ distinct_points ) ) )
| ~ $true
| ~ ( C @ ( B @ equal_points ) )
| ( A @ ( sk2 @ ( sk1 @ intersection_point ) @ distinct_points ) ) ),
inference(paramod_ordered,[status(thm)],[1326,84]) ).
thf(1336,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk3 @ ( sk1 @ intersection_point ) @ distinct_points ) )
!= ( C @ ( B @ distinct_points ) ) )
| ~ ( C @ ( B @ equal_points ) )
| ( A @ ( sk2 @ ( sk1 @ intersection_point ) @ distinct_points ) ) ),
inference(simp,[status(thm)],[1335]) ).
thf(1337,plain,
! [A: $i] :
( ~ ( A @ ( sk3 @ ( sk1 @ intersection_point ) @ equal_points ) )
| ( A @ ( sk2 @ ( sk1 @ intersection_point ) @ distinct_points ) ) ),
inference(pattern_uni,[status(thm)],[1336:[bind(A,$thf( A )),bind(B,$thf( sk3 @ ( sk1 @ intersection_point ) )),bind(C,$thf( A ))]]) ).
thf(40,plain,
sk2 @ ( sk1 @ convergent_lines ),
inference(cnfConj,[status(thm)],[39]) ).
thf(16,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ convergent_lines ) )
=> ( ( C @ ( B @ convergent_lines ) )
| ( C @ ( A @ convergent_lines ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax6) ).
thf(89,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)],[16]) ).
thf(90,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ convergent_lines ) )
=> ! [C: $i] :
( ( C @ ( B @ convergent_lines ) )
| ( C @ ( A @ convergent_lines ) ) ) ),
inference(miniscope,[status(thm)],[89]) ).
thf(91,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ convergent_lines ) )
| ( C @ ( A @ convergent_lines ) )
| ~ ( B @ ( A @ convergent_lines ) ) ),
inference(cnf,[status(esa)],[90]) ).
thf(1121,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,91]) ).
thf(1122,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)],[1121]) ).
thf(1123,plain,
! [A: $i] :
( ( A @ ( sk2 @ convergent_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[1122:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(1128,plain,
! [A: $i] :
( ( A @ ( sk2 @ convergent_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[1123]) ).
thf(1147,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ( D @ ( C @ convergent_lines ) )
| ( D @ ( B @ convergent_lines ) )
| ~ $true
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1128,91]) ).
thf(1148,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ( D @ ( C @ convergent_lines ) )
| ( D @ ( B @ convergent_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[1147]) ).
thf(1149,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ convergent_lines ) )
| ( B @ ( sk2 @ convergent_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[1148:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( A ))]]) ).
thf(1156,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ convergent_lines ) )
| ( B @ ( sk2 @ convergent_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[1149]) ).
thf(22,axiom,
! [A: $i] :
~ ( A @ ( A @ convergent_lines ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',apart3) ).
thf(104,plain,
! [A: $i] :
~ ( A @ ( A @ convergent_lines ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(105,plain,
~ ? [A: $i] : ( A @ ( A @ convergent_lines ) ),
inference(miniscope,[status(thm)],[104]) ).
thf(106,plain,
! [A: $i] :
~ ( A @ ( A @ convergent_lines ) ),
inference(cnf,[status(esa)],[105]) ).
thf(1939,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( sk2 @ convergent_lines ) )
!= ( C @ ( C @ convergent_lines ) ) )
| ~ $true
| ( B @ ( A @ convergent_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1156,106]) ).
thf(1940,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( sk2 @ convergent_lines ) )
!= ( C @ ( C @ convergent_lines ) ) )
| ( B @ ( A @ convergent_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[1939]) ).
thf(1941,plain,
! [A: $i] :
( ( sk2 @ ( A @ convergent_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[1940:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( sk2 ))]]) ).
thf(23,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ parallel_lines ) )
<=> ~ ( B @ ( A @ convergent_lines ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a3) ).
thf(107,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)],[23]) ).
thf(108,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)],[107]) ).
thf(109,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)],[108]) ).
thf(110,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ convergent_lines ) )
| ~ ( B @ ( A @ parallel_lines ) ) ),
inference(cnfConj,[status(thm)],[109]) ).
thf(2092,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ $true
| ~ ( C @ ( B @ parallel_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1941,110]) ).
thf(2093,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( C @ ( B @ parallel_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[2092]) ).
thf(2094,plain,
! [A: $i] :
( ~ ( sk2 @ ( A @ parallel_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[2093:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk2 ))]]) ).
thf(27,axiom,
! [A: $i,B: $i] :
( ( ( B @ ( A @ distinct_points ) )
& ( B @ point )
& ( A @ point ) )
=> ( B @ ( A @ line_connecting ) @ line ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',con1) ).
thf(121,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)],[27]) ).
thf(122,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ line_connecting ) @ line )
| ~ ( B @ ( A @ distinct_points ) )
| ~ ( B @ point )
| ~ ( A @ point ) ),
inference(cnf,[status(esa)],[121]) ).
thf(19,axiom,
! [A: $i,B: $i] :
( ( ( B @ ( A @ convergent_lines ) )
& ( B @ line )
& ( A @ line ) )
=> ( B @ ( A @ intersection_point ) @ point ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',int1) ).
thf(97,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)],[19]) ).
thf(98,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ intersection_point ) @ point )
| ~ ( B @ ( A @ convergent_lines ) )
| ~ ( B @ line )
| ~ ( A @ line ) ),
inference(cnf,[status(esa)],[97]) ).
thf(41,plain,
sk3 @ ( sk1 @ convergent_lines ),
inference(cnfConj,[status(thm)],[39]) ).
thf(1496,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ( B @ ( A @ intersection_point ) @ point )
| ~ $true
| ~ ( B @ line )
| ~ ( A @ line ) ),
inference(paramod_ordered,[status(thm)],[41,98]) ).
thf(1497,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ( B @ ( A @ intersection_point ) @ point )
| ~ ( B @ line )
| ~ ( A @ line ) ),
inference(simp,[status(thm)],[1496]) ).
thf(1498,plain,
( ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( sk3 @ line )
| ~ ( sk1 @ line ) ),
inference(pattern_uni,[status(thm)],[1497:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 ))]]) ).
thf(2031,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ line_connecting ) @ line )
!= ( sk3 @ line ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ $true
| ~ ( sk1 @ line )
| ~ ( B @ ( A @ distinct_points ) )
| ~ ( B @ point )
| ~ ( A @ point ) ),
inference(paramod_ordered,[status(thm)],[122,1498]) ).
thf(2032,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ line_connecting ) @ line )
!= ( sk3 @ line ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( sk1 @ line )
| ~ ( B @ ( A @ distinct_points ) )
| ~ ( B @ point )
| ~ ( A @ point ) ),
inference(simp,[status(thm)],[2031]) ).
thf(2073,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ line_connecting ) )
!= sk3 )
| ~ ( sk1 @ line )
| ~ ( B @ ( A @ distinct_points ) )
| ~ ( B @ point )
| ~ ( A @ point )
| ( sk3 @ ( sk1 @ intersection_point ) @ point ) ),
inference(simp,[status(thm)],[2032]) ).
thf(4057,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ line_connecting ) @ line )
!= ( sk1 @ line ) )
| ( ( D @ ( C @ line_connecting ) )
!= sk3 )
| ~ $true
| ~ ( D @ ( C @ distinct_points ) )
| ~ ( D @ point )
| ~ ( C @ point )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( B @ ( A @ distinct_points ) )
| ~ ( B @ point )
| ~ ( A @ point ) ),
inference(paramod_ordered,[status(thm)],[122,2073]) ).
thf(4058,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ line_connecting ) @ line )
!= ( sk1 @ line ) )
| ( ( D @ ( C @ line_connecting ) )
!= sk3 )
| ~ ( D @ ( C @ distinct_points ) )
| ~ ( D @ point )
| ~ ( C @ point )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( B @ ( A @ distinct_points ) )
| ~ ( B @ point )
| ~ ( A @ point ) ),
inference(simp,[status(thm)],[4057]) ).
thf(4059,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ line_connecting ) )
!= sk1 )
| ( ( D @ ( C @ line_connecting ) )
!= sk3 )
| ~ ( D @ ( C @ distinct_points ) )
| ~ ( D @ point )
| ~ ( C @ point )
| ~ ( B @ ( A @ distinct_points ) )
| ~ ( B @ point )
| ~ ( A @ point )
| ( sk3 @ ( sk1 @ intersection_point ) @ point ) ),
inference(simp,[status(thm)],[4058]) ).
thf(4115,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ intersection_point ) @ point )
!= ( C @ point ) )
| ( ( D @ ( C @ line_connecting ) )
!= sk1 )
| ( ( F @ ( E @ line_connecting ) )
!= sk3 )
| ~ ( F @ ( E @ distinct_points ) )
| ~ ( F @ point )
| ~ ( E @ point )
| ~ ( D @ ( C @ distinct_points ) )
| ~ ( D @ point )
| ~ $true
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( B @ ( A @ convergent_lines ) )
| ~ ( B @ line )
| ~ ( A @ line ) ),
inference(paramod_ordered,[status(thm)],[98,4059]) ).
thf(4116,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ intersection_point ) @ point )
!= ( C @ point ) )
| ( ( D @ ( C @ line_connecting ) )
!= sk1 )
| ( ( F @ ( E @ line_connecting ) )
!= sk3 )
| ~ ( F @ ( E @ distinct_points ) )
| ~ ( F @ point )
| ~ ( E @ point )
| ~ ( D @ ( C @ distinct_points ) )
| ~ ( D @ point )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( B @ ( A @ convergent_lines ) )
| ~ ( B @ line )
| ~ ( A @ line ) ),
inference(simp,[status(thm)],[4115]) ).
thf(4117,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( E @ ( D @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( C @ ( B @ line_connecting ) )
!= sk3 )
| ~ ( C @ ( B @ distinct_points ) )
| ~ ( C @ point )
| ~ ( B @ point )
| ~ ( A @ ( E @ ( D @ intersection_point ) @ distinct_points ) )
| ~ ( A @ point )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( E @ ( D @ convergent_lines ) )
| ~ ( E @ line )
| ~ ( D @ line ) ),
inference(pattern_uni,[status(thm)],[4116:[bind(A,$thf( G )),bind(B,$thf( H )),bind(C,$thf( H @ ( G @ intersection_point ) ))]]) ).
thf(4155,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( E @ ( D @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( C @ ( B @ line_connecting ) )
!= sk3 )
| ~ ( C @ ( B @ distinct_points ) )
| ~ ( C @ point )
| ~ ( B @ point )
| ~ ( A @ ( E @ ( D @ intersection_point ) @ distinct_points ) )
| ~ ( A @ point )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( E @ ( D @ convergent_lines ) )
| ~ ( E @ line )
| ~ ( D @ line ) ),
inference(simp,[status(thm)],[4117]) ).
thf(4372,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ intersection_point ) @ point )
!= ( C @ point ) )
| ( ( C @ ( G @ ( F @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( E @ ( D @ line_connecting ) )
!= sk3 )
| ~ ( E @ ( D @ distinct_points ) )
| ~ ( E @ point )
| ~ ( D @ point )
| ~ ( C @ ( G @ ( F @ intersection_point ) @ distinct_points ) )
| ~ $true
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( G @ ( F @ convergent_lines ) )
| ~ ( G @ line )
| ~ ( F @ line )
| ~ ( B @ ( A @ convergent_lines ) )
| ~ ( B @ line )
| ~ ( A @ line ) ),
inference(paramod_ordered,[status(thm)],[98,4155]) ).
thf(4373,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ intersection_point ) @ point )
!= ( C @ point ) )
| ( ( C @ ( G @ ( F @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( E @ ( D @ line_connecting ) )
!= sk3 )
| ~ ( E @ ( D @ distinct_points ) )
| ~ ( E @ point )
| ~ ( D @ point )
| ~ ( C @ ( G @ ( F @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( G @ ( F @ convergent_lines ) )
| ~ ( G @ line )
| ~ ( F @ line )
| ~ ( B @ ( A @ convergent_lines ) )
| ~ ( B @ line )
| ~ ( A @ line ) ),
inference(simp,[status(thm)],[4372]) ).
thf(4374,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( F @ ( E @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( B @ ( A @ line_connecting ) )
!= sk3 )
| ~ ( B @ ( A @ distinct_points ) )
| ~ ( B @ point )
| ~ ( A @ point )
| ~ ( F @ ( E @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( D @ ( C @ convergent_lines ) )
| ~ ( D @ line )
| ~ ( C @ line )
| ~ ( F @ ( E @ convergent_lines ) )
| ~ ( F @ line )
| ~ ( E @ line ) ),
inference(pattern_uni,[status(thm)],[4373:[bind(A,$thf( H )),bind(B,$thf( I )),bind(C,$thf( I @ ( H @ intersection_point ) ))]]) ).
thf(4462,plain,
! [F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( F @ ( E @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( B @ ( A @ line_connecting ) )
!= sk3 )
| ~ ( B @ ( A @ distinct_points ) )
| ~ ( B @ point )
| ~ ( A @ point )
| ~ ( F @ ( E @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( D @ ( C @ convergent_lines ) )
| ~ ( D @ line )
| ~ ( C @ line )
| ~ ( F @ ( E @ convergent_lines ) )
| ~ ( F @ line )
| ~ ( E @ line ) ),
inference(simp,[status(thm)],[4374]) ).
thf(4596,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ intersection_point ) @ point )
!= ( C @ point ) )
| ( ( H @ ( G @ intersection_point ) @ ( F @ ( E @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( D @ ( C @ line_connecting ) )
!= sk3 )
| ~ ( D @ ( C @ distinct_points ) )
| ~ ( D @ point )
| ~ $true
| ~ ( H @ ( G @ intersection_point ) @ ( F @ ( E @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( F @ ( E @ convergent_lines ) )
| ~ ( F @ line )
| ~ ( E @ line )
| ~ ( H @ ( G @ convergent_lines ) )
| ~ ( H @ line )
| ~ ( G @ line )
| ~ ( B @ ( A @ convergent_lines ) )
| ~ ( B @ line )
| ~ ( A @ line ) ),
inference(paramod_ordered,[status(thm)],[98,4462]) ).
thf(4597,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ intersection_point ) @ point )
!= ( C @ point ) )
| ( ( H @ ( G @ intersection_point ) @ ( F @ ( E @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( D @ ( C @ line_connecting ) )
!= sk3 )
| ~ ( D @ ( C @ distinct_points ) )
| ~ ( D @ point )
| ~ ( H @ ( G @ intersection_point ) @ ( F @ ( E @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( F @ ( E @ convergent_lines ) )
| ~ ( F @ line )
| ~ ( E @ line )
| ~ ( H @ ( G @ convergent_lines ) )
| ~ ( H @ line )
| ~ ( G @ line )
| ~ ( B @ ( A @ convergent_lines ) )
| ~ ( B @ line )
| ~ ( A @ line ) ),
inference(simp,[status(thm)],[4596]) ).
thf(4598,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( E @ ( D @ intersection_point ) @ ( C @ ( B @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( A @ ( G @ ( F @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( A @ ( G @ ( F @ intersection_point ) @ distinct_points ) )
| ~ ( A @ point )
| ~ ( E @ ( D @ intersection_point ) @ ( C @ ( B @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( C @ ( B @ convergent_lines ) )
| ~ ( C @ line )
| ~ ( B @ line )
| ~ ( E @ ( D @ convergent_lines ) )
| ~ ( E @ line )
| ~ ( D @ line )
| ~ ( G @ ( F @ convergent_lines ) )
| ~ ( G @ line )
| ~ ( F @ line ) ),
inference(pattern_uni,[status(thm)],[4597:[bind(A,$thf( I )),bind(B,$thf( J )),bind(C,$thf( J @ ( I @ intersection_point ) ))]]) ).
thf(4793,plain,
! [G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( E @ ( D @ intersection_point ) @ ( C @ ( B @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( A @ ( G @ ( F @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( A @ ( G @ ( F @ intersection_point ) @ distinct_points ) )
| ~ ( A @ point )
| ~ ( E @ ( D @ intersection_point ) @ ( C @ ( B @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( C @ ( B @ convergent_lines ) )
| ~ ( C @ line )
| ~ ( B @ line )
| ~ ( E @ ( D @ convergent_lines ) )
| ~ ( E @ line )
| ~ ( D @ line )
| ~ ( G @ ( F @ convergent_lines ) )
| ~ ( G @ line )
| ~ ( F @ line ) ),
inference(simp,[status(thm)],[4598]) ).
thf(5263,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ intersection_point ) @ point )
!= ( C @ point ) )
| ( ( G @ ( F @ intersection_point ) @ ( E @ ( D @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( C @ ( I @ ( H @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( C @ ( I @ ( H @ intersection_point ) @ distinct_points ) )
| ~ $true
| ~ ( G @ ( F @ intersection_point ) @ ( E @ ( D @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( E @ ( D @ convergent_lines ) )
| ~ ( E @ line )
| ~ ( D @ line )
| ~ ( G @ ( F @ convergent_lines ) )
| ~ ( G @ line )
| ~ ( F @ line )
| ~ ( I @ ( H @ convergent_lines ) )
| ~ ( I @ line )
| ~ ( H @ line )
| ~ ( B @ ( A @ convergent_lines ) )
| ~ ( B @ line )
| ~ ( A @ line ) ),
inference(paramod_ordered,[status(thm)],[98,4793]) ).
thf(5264,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ intersection_point ) @ point )
!= ( C @ point ) )
| ( ( G @ ( F @ intersection_point ) @ ( E @ ( D @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( C @ ( I @ ( H @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( C @ ( I @ ( H @ intersection_point ) @ distinct_points ) )
| ~ ( G @ ( F @ intersection_point ) @ ( E @ ( D @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( E @ ( D @ convergent_lines ) )
| ~ ( E @ line )
| ~ ( D @ line )
| ~ ( G @ ( F @ convergent_lines ) )
| ~ ( G @ line )
| ~ ( F @ line )
| ~ ( I @ ( H @ convergent_lines ) )
| ~ ( I @ line )
| ~ ( H @ line )
| ~ ( B @ ( A @ convergent_lines ) )
| ~ ( B @ line )
| ~ ( A @ line ) ),
inference(simp,[status(thm)],[5263]) ).
thf(5265,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( H @ ( G @ intersection_point ) @ ( F @ ( E @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( H @ ( G @ intersection_point ) @ ( F @ ( E @ intersection_point ) @ distinct_points ) )
| ~ ( D @ ( C @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( B @ ( A @ convergent_lines ) )
| ~ ( B @ line )
| ~ ( A @ line )
| ~ ( D @ ( C @ convergent_lines ) )
| ~ ( D @ line )
| ~ ( C @ line )
| ~ ( F @ ( E @ convergent_lines ) )
| ~ ( F @ line )
| ~ ( E @ line )
| ~ ( H @ ( G @ convergent_lines ) )
| ~ ( H @ line )
| ~ ( G @ line ) ),
inference(pattern_uni,[status(thm)],[5264:[bind(A,$thf( J )),bind(B,$thf( K )),bind(C,$thf( K @ ( J @ intersection_point ) ))]]) ).
thf(5550,plain,
! [H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( H @ ( G @ intersection_point ) @ ( F @ ( E @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( H @ ( G @ intersection_point ) @ ( F @ ( E @ intersection_point ) @ distinct_points ) )
| ~ ( D @ ( C @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( B @ ( A @ convergent_lines ) )
| ~ ( B @ line )
| ~ ( A @ line )
| ~ ( D @ ( C @ convergent_lines ) )
| ~ ( D @ line )
| ~ ( C @ line )
| ~ ( F @ ( E @ convergent_lines ) )
| ~ ( F @ line )
| ~ ( E @ line )
| ~ ( H @ ( G @ convergent_lines ) )
| ~ ( H @ line )
| ~ ( G @ line ) ),
inference(simp,[status(thm)],[5265]) ).
thf(6001,plain,
! [J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ line_connecting ) @ line )
!= ( I @ line ) )
| ( ( F @ ( E @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( J @ ( I @ intersection_point ) @ ( H @ ( G @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( J @ ( I @ intersection_point ) @ ( H @ ( G @ intersection_point ) @ distinct_points ) )
| ~ ( F @ ( E @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( D @ ( C @ convergent_lines ) )
| ~ ( D @ line )
| ~ ( C @ line )
| ~ ( F @ ( E @ convergent_lines ) )
| ~ ( F @ line )
| ~ ( E @ line )
| ~ ( H @ ( G @ convergent_lines ) )
| ~ ( H @ line )
| ~ ( G @ line )
| ~ ( J @ ( I @ convergent_lines ) )
| ~ ( J @ line )
| ~ $true
| ~ ( B @ ( A @ distinct_points ) )
| ~ ( B @ point )
| ~ ( A @ point ) ),
inference(paramod_ordered,[status(thm)],[122,5550]) ).
thf(6002,plain,
! [J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ line_connecting ) @ line )
!= ( I @ line ) )
| ( ( F @ ( E @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( J @ ( I @ intersection_point ) @ ( H @ ( G @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( J @ ( I @ intersection_point ) @ ( H @ ( G @ intersection_point ) @ distinct_points ) )
| ~ ( F @ ( E @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( D @ ( C @ convergent_lines ) )
| ~ ( D @ line )
| ~ ( C @ line )
| ~ ( F @ ( E @ convergent_lines ) )
| ~ ( F @ line )
| ~ ( E @ line )
| ~ ( H @ ( G @ convergent_lines ) )
| ~ ( H @ line )
| ~ ( G @ line )
| ~ ( J @ ( I @ convergent_lines ) )
| ~ ( J @ line )
| ~ ( B @ ( A @ distinct_points ) )
| ~ ( B @ point )
| ~ ( A @ point ) ),
inference(simp,[status(thm)],[6001]) ).
thf(6003,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( G @ ( I @ ( H @ line_connecting ) @ intersection_point ) @ ( F @ ( E @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( G @ ( I @ ( H @ line_connecting ) @ intersection_point ) @ ( F @ ( E @ intersection_point ) @ distinct_points ) )
| ~ ( D @ ( C @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( B @ ( A @ convergent_lines ) )
| ~ ( B @ line )
| ~ ( A @ line )
| ~ ( D @ ( C @ convergent_lines ) )
| ~ ( D @ line )
| ~ ( C @ line )
| ~ ( F @ ( E @ convergent_lines ) )
| ~ ( F @ line )
| ~ ( E @ line )
| ~ ( G @ ( I @ ( H @ line_connecting ) @ convergent_lines ) )
| ~ ( G @ line )
| ~ ( I @ ( H @ distinct_points ) )
| ~ ( I @ point )
| ~ ( H @ point ) ),
inference(pattern_uni,[status(thm)],[6002:[bind(A,$thf( K )),bind(B,$thf( L )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( E )),bind(F,$thf( F )),bind(G,$thf( G )),bind(H,$thf( H )),bind(I,$thf( L @ ( K @ line_connecting ) ))]]) ).
thf(6089,plain,
! [I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( G @ ( I @ ( H @ line_connecting ) @ intersection_point ) @ ( F @ ( E @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( G @ ( I @ ( H @ line_connecting ) @ intersection_point ) @ ( F @ ( E @ intersection_point ) @ distinct_points ) )
| ~ ( D @ ( C @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( B @ ( A @ convergent_lines ) )
| ~ ( B @ line )
| ~ ( A @ line )
| ~ ( D @ ( C @ convergent_lines ) )
| ~ ( D @ line )
| ~ ( C @ line )
| ~ ( F @ ( E @ convergent_lines ) )
| ~ ( F @ line )
| ~ ( E @ line )
| ~ ( G @ ( I @ ( H @ line_connecting ) @ convergent_lines ) )
| ~ ( G @ line )
| ~ ( I @ ( H @ distinct_points ) )
| ~ ( I @ point )
| ~ ( H @ point ) ),
inference(simp,[status(thm)],[6003]) ).
thf(6931,plain,
! [K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ line_connecting ) @ line )
!= ( I @ line ) )
| ( ( F @ ( E @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( I @ ( K @ ( J @ line_connecting ) @ intersection_point ) @ ( H @ ( G @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( I @ ( K @ ( J @ line_connecting ) @ intersection_point ) @ ( H @ ( G @ intersection_point ) @ distinct_points ) )
| ~ ( F @ ( E @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( D @ ( C @ convergent_lines ) )
| ~ ( D @ line )
| ~ ( C @ line )
| ~ ( F @ ( E @ convergent_lines ) )
| ~ ( F @ line )
| ~ ( E @ line )
| ~ ( H @ ( G @ convergent_lines ) )
| ~ ( H @ line )
| ~ ( G @ line )
| ~ ( I @ ( K @ ( J @ line_connecting ) @ convergent_lines ) )
| ~ $true
| ~ ( K @ ( J @ distinct_points ) )
| ~ ( K @ point )
| ~ ( J @ point )
| ~ ( B @ ( A @ distinct_points ) )
| ~ ( B @ point )
| ~ ( A @ point ) ),
inference(paramod_ordered,[status(thm)],[122,6089]) ).
thf(6932,plain,
! [K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ line_connecting ) @ line )
!= ( I @ line ) )
| ( ( F @ ( E @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( I @ ( K @ ( J @ line_connecting ) @ intersection_point ) @ ( H @ ( G @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( I @ ( K @ ( J @ line_connecting ) @ intersection_point ) @ ( H @ ( G @ intersection_point ) @ distinct_points ) )
| ~ ( F @ ( E @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( D @ ( C @ convergent_lines ) )
| ~ ( D @ line )
| ~ ( C @ line )
| ~ ( F @ ( E @ convergent_lines ) )
| ~ ( F @ line )
| ~ ( E @ line )
| ~ ( H @ ( G @ convergent_lines ) )
| ~ ( H @ line )
| ~ ( G @ line )
| ~ ( I @ ( K @ ( J @ line_connecting ) @ convergent_lines ) )
| ~ ( K @ ( J @ distinct_points ) )
| ~ ( K @ point )
| ~ ( J @ point )
| ~ ( B @ ( A @ distinct_points ) )
| ~ ( B @ point )
| ~ ( A @ point ) ),
inference(simp,[status(thm)],[6931]) ).
thf(6933,plain,
! [J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( J @ ( I @ line_connecting ) @ ( H @ ( G @ line_connecting ) @ intersection_point ) @ ( F @ ( E @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( J @ ( I @ line_connecting ) @ ( H @ ( G @ line_connecting ) @ intersection_point ) @ ( F @ ( E @ intersection_point ) @ distinct_points ) )
| ~ ( D @ ( C @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( B @ ( A @ convergent_lines ) )
| ~ ( B @ line )
| ~ ( A @ line )
| ~ ( D @ ( C @ convergent_lines ) )
| ~ ( D @ line )
| ~ ( C @ line )
| ~ ( F @ ( E @ convergent_lines ) )
| ~ ( F @ line )
| ~ ( E @ line )
| ~ ( J @ ( I @ line_connecting ) @ ( H @ ( G @ line_connecting ) @ convergent_lines ) )
| ~ ( H @ ( G @ distinct_points ) )
| ~ ( H @ point )
| ~ ( G @ point )
| ~ ( J @ ( I @ distinct_points ) )
| ~ ( J @ point )
| ~ ( I @ point ) ),
inference(pattern_uni,[status(thm)],[6932:[bind(A,$thf( L )),bind(B,$thf( M )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( E )),bind(F,$thf( F )),bind(G,$thf( G )),bind(H,$thf( H )),bind(I,$thf( M @ ( L @ line_connecting ) ))]]) ).
thf(6979,plain,
! [J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( J @ ( I @ line_connecting ) @ ( H @ ( G @ line_connecting ) @ intersection_point ) @ ( F @ ( E @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( J @ ( I @ line_connecting ) @ ( H @ ( G @ line_connecting ) @ intersection_point ) @ ( F @ ( E @ intersection_point ) @ distinct_points ) )
| ~ ( D @ ( C @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( B @ ( A @ convergent_lines ) )
| ~ ( B @ line )
| ~ ( A @ line )
| ~ ( D @ ( C @ convergent_lines ) )
| ~ ( D @ line )
| ~ ( C @ line )
| ~ ( F @ ( E @ convergent_lines ) )
| ~ ( F @ line )
| ~ ( E @ line )
| ~ ( J @ ( I @ line_connecting ) @ ( H @ ( G @ line_connecting ) @ convergent_lines ) )
| ~ ( H @ ( G @ distinct_points ) )
| ~ ( H @ point )
| ~ ( G @ point )
| ~ ( J @ ( I @ distinct_points ) )
| ~ ( J @ point )
| ~ ( I @ point ) ),
inference(simp,[status(thm)],[6933]) ).
thf(31,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ convergent_lines ) )
=> ( ( C @ ( A @ convergent_lines ) )
| ( C @ ( B @ distinct_lines ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ceq3) ).
thf(138,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(20,axiom,
! [A: $i,B: $i] :
~ ( ~ ( B @ ( A @ unorthogonal_lines ) )
& ~ ( B @ ( A @ convergent_lines ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',coipo1) ).
thf(99,plain,
! [A: $i,B: $i] :
~ ( ~ ( B @ ( A @ unorthogonal_lines ) )
& ~ ( B @ ( A @ convergent_lines ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(100,plain,
~ ? [A: $i,B: $i] :
( ~ ( B @ ( A @ unorthogonal_lines ) )
& ~ ( B @ ( A @ convergent_lines ) ) ),
inference(miniscope,[status(thm)],[99]) ).
thf(101,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ unorthogonal_lines ) )
| ( B @ ( A @ convergent_lines ) ) ),
inference(cnf,[status(esa)],[100]) ).
thf(1980,plain,
! [B: $i,A: $i] :
( ~ $true
| ( ( B @ ( A @ convergent_lines ) )
!= ( A @ ( sk1 @ convergent_lines ) ) )
| ( B @ ( sk2 @ convergent_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(eqfactor_ordered,[status(thm)],[1156]) ).
thf(1984,plain,
( ( sk1 @ ( sk2 @ convergent_lines ) )
| ( sk1 @ ( sk1 @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[1980:[bind(A,$thf( sk1 )),bind(B,$thf( sk1 ))]]) ).
thf(1997,plain,
( ( sk1 @ ( sk2 @ convergent_lines ) )
| $false ),
inference(rewrite,[status(thm)],[1984,106]) ).
thf(1998,plain,
sk1 @ ( sk2 @ convergent_lines ),
inference(simp,[status(thm)],[1997]) ).
thf(34,axiom,
! [A: $i,B: $i,C: $i] :
( ( ~ ( C @ ( A @ unorthogonal_lines ) )
& ~ ( B @ ( A @ unorthogonal_lines ) ) )
=> ~ ( C @ ( B @ convergent_lines ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',couo1) ).
thf(145,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(146,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ convergent_lines ) )
| ( C @ ( A @ unorthogonal_lines ) )
| ( B @ ( A @ unorthogonal_lines ) ) ),
inference(cnf,[status(esa)],[145]) ).
thf(4260,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ $true
| ( C @ ( A @ unorthogonal_lines ) )
| ( B @ ( A @ unorthogonal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1998,146]) ).
thf(4261,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ( C @ ( A @ unorthogonal_lines ) )
| ( B @ ( A @ unorthogonal_lines ) ) ),
inference(simp,[status(thm)],[4260]) ).
thf(4262,plain,
! [A: $i] :
( ( sk1 @ ( A @ unorthogonal_lines ) )
| ( sk2 @ ( A @ unorthogonal_lines ) ) ),
inference(pattern_uni,[status(thm)],[4261:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( sk1 ))]]) ).
thf(25,axiom,
! [A: $i,B: $i] :
~ ( B @ ( A @ ( B @ parallel_through_point ) @ convergent_lines ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cp1) ).
thf(115,plain,
! [A: $i,B: $i] :
~ ( B @ ( A @ ( B @ parallel_through_point ) @ convergent_lines ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(116,plain,
~ ? [A: $i,B: $i] : ( B @ ( A @ ( B @ parallel_through_point ) @ convergent_lines ) ),
inference(miniscope,[status(thm)],[115]) ).
thf(117,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ ( B @ parallel_through_point ) @ convergent_lines ) ),
inference(cnf,[status(esa)],[116]) ).
thf(2108,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ convergent_lines ) )
!= ( C @ ( B @ ( C @ parallel_through_point ) @ convergent_lines ) ) )
| ~ $true
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1941,117]) ).
thf(2109,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ convergent_lines ) )
!= ( C @ ( B @ ( C @ parallel_through_point ) @ convergent_lines ) ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[2108]) ).
thf(2110,plain,
! [A: $i] : ( A @ ( sk2 @ parallel_through_point ) @ ( sk1 @ convergent_lines ) ),
inference(pattern_uni,[status(thm)],[2109:[bind(A,$thf( E @ ( sk2 @ parallel_through_point ) )),bind(B,$thf( E )),bind(C,$thf( sk2 ))]]) ).
thf(2130,plain,
! [A: $i] : ( A @ ( sk2 @ parallel_through_point ) @ ( sk1 @ convergent_lines ) ),
inference(simp,[status(thm)],[2110]) ).
thf(2257,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ parallel_through_point ) @ ( sk1 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ( D @ ( C @ convergent_lines ) )
| ( D @ ( B @ convergent_lines ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2130,91]) ).
thf(2258,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ parallel_through_point ) @ ( sk1 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ( D @ ( C @ convergent_lines ) )
| ( D @ ( B @ convergent_lines ) ) ),
inference(simp,[status(thm)],[2257]) ).
thf(2259,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( sk2 @ parallel_through_point ) @ convergent_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[2258:[bind(A,$thf( F )),bind(B,$thf( sk1 )),bind(C,$thf( F @ ( sk2 @ parallel_through_point ) )),bind(D,$thf( D ))]]) ).
thf(2263,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( sk2 @ parallel_through_point ) @ convergent_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[2259]) ).
thf(30,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ equal_lines ) )
<=> ~ ( B @ ( A @ distinct_lines ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
thf(132,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(133,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)],[132]) ).
thf(134,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)],[133]) ).
thf(136,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ equal_lines ) )
| ( B @ ( A @ distinct_lines ) ) ),
inference(cnfConj,[status(thm)],[134]) ).
thf(137,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ equal_lines ) )
| ( B @ ( A @ distinct_lines ) ) ),
inference(simp,[status(thm)],[136]) ).
thf(9,axiom,
! [A: $i,B: $i,C: $i] :
( ( B @ ( A @ distinct_lines ) )
=> ( ( C @ ( B @ distinct_lines ) )
| ( C @ ( A @ distinct_lines ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',apart5) ).
thf(64,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)],[9]) ).
thf(65,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ distinct_lines ) )
=> ! [C: $i] :
( ( C @ ( B @ distinct_lines ) )
| ( C @ ( A @ distinct_lines ) ) ) ),
inference(miniscope,[status(thm)],[64]) ).
thf(66,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ distinct_lines ) )
| ( C @ ( A @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_lines ) ) ),
inference(cnf,[status(esa)],[65]) ).
thf(406,plain,
! [C: $i,B: $i,A: $i] :
( ~ $true
| ( ( C @ ( B @ distinct_lines ) )
!= ( C @ ( A @ distinct_lines ) ) )
| ( C @ ( A @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_lines ) ) ),
inference(eqfactor_ordered,[status(thm)],[66]) ).
thf(407,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ distinct_lines ) )
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[406:[bind(A,$thf( B ))]]) ).
thf(414,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ distinct_lines ) )
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(simp,[status(thm)],[407]) ).
thf(425,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( C @ distinct_lines ) ) )
| ( D @ ( C @ distinct_lines ) )
| ~ $true
| ( B @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[137,414]) ).
thf(426,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( C @ distinct_lines ) ) )
| ( D @ ( C @ distinct_lines ) )
| ( B @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[425]) ).
thf(427,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ distinct_lines ) )
| ( A @ ( A @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[426:[bind(A,$thf( B )),bind(B,$thf( B )),bind(C,$thf( B ))]]) ).
thf(450,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ distinct_lines ) )
| ( A @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[427]) ).
thf(8,axiom,
! [A: $i] :
~ ( A @ ( A @ distinct_lines ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',apart2) ).
thf(61,plain,
! [A: $i] :
~ ( A @ ( A @ distinct_lines ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(62,plain,
~ ? [A: $i] : ( A @ ( A @ distinct_lines ) ),
inference(miniscope,[status(thm)],[61]) ).
thf(63,plain,
! [A: $i] :
~ ( A @ ( A @ distinct_lines ) ),
inference(cnf,[status(esa)],[62]) ).
thf(376,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ distinct_lines ) )
!= ( D @ ( D @ distinct_lines ) ) )
| ~ $true
| ( C @ ( B @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[66,63]) ).
thf(377,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ distinct_lines ) )
!= ( D @ ( D @ distinct_lines ) ) )
| ( C @ ( B @ distinct_lines ) )
| ~ ( B @ ( A @ distinct_lines ) ) ),
inference(simp,[status(thm)],[376]) ).
thf(378,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ distinct_lines ) )
| ~ ( A @ ( B @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[377:[bind(A,$thf( C )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( C ))]]) ).
thf(415,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ distinct_lines ) )
| ~ ( A @ ( B @ distinct_lines ) ) ),
inference(simp,[status(thm)],[378]) ).
thf(135,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ distinct_lines ) )
| ~ ( B @ ( A @ equal_lines ) ) ),
inference(cnfConj,[status(thm)],[134]) ).
thf(472,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( D @ ( C @ distinct_lines ) ) )
| ~ $true
| ~ ( D @ ( C @ equal_lines ) )
| ~ ( A @ ( B @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[415,135]) ).
thf(473,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( D @ ( C @ distinct_lines ) ) )
| ~ ( D @ ( C @ equal_lines ) )
| ~ ( A @ ( B @ distinct_lines ) ) ),
inference(simp,[status(thm)],[472]) ).
thf(474,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ equal_lines ) )
| ~ ( A @ ( B @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[473:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(553,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( D @ distinct_lines ) ) )
| ~ ( D @ ( C @ equal_lines ) )
| ~ $true
| ( A @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[450,474]) ).
thf(554,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( D @ distinct_lines ) ) )
| ~ ( D @ ( C @ equal_lines ) )
| ( A @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[553]) ).
thf(555,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ equal_lines ) )
| ( A @ ( A @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[554:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(35,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ distinct_lines ) )
=> ( B @ ( A @ convergent_lines ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p1) ).
thf(147,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ distinct_lines ) )
=> ( B @ ( A @ convergent_lines ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(148,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ convergent_lines ) )
| ~ ( B @ ( A @ distinct_lines ) ) ),
inference(cnf,[status(esa)],[147]) ).
thf(451,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( D @ ( C @ distinct_lines ) ) )
| ( D @ ( C @ convergent_lines ) )
| ~ $true
| ~ ( A @ ( B @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[415,148]) ).
thf(452,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( D @ ( C @ distinct_lines ) ) )
| ( D @ ( C @ convergent_lines ) )
| ~ ( A @ ( B @ distinct_lines ) ) ),
inference(simp,[status(thm)],[451]) ).
thf(453,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ convergent_lines ) )
| ~ ( A @ ( B @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[452:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(611,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( D @ distinct_lines ) ) )
| ( D @ ( C @ convergent_lines ) )
| ~ $true
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[414,453]) ).
thf(612,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( D @ distinct_lines ) ) )
| ( D @ ( C @ convergent_lines ) )
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(simp,[status(thm)],[611]) ).
thf(613,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ convergent_lines ) )
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[612:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(1816,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ convergent_lines ) )
!= ( D @ ( C @ convergent_lines ) ) )
| ~ $true
| ~ ( D @ ( C @ parallel_lines ) )
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[613,110]) ).
thf(1817,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ convergent_lines ) )
!= ( D @ ( C @ convergent_lines ) ) )
| ~ ( D @ ( C @ parallel_lines ) )
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(simp,[status(thm)],[1816]) ).
thf(1818,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ parallel_lines ) )
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[1817:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(15,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/sandbox/benchmark/theBenchmark.p',cu1) ).
thf(87,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)],[15]) ).
thf(88,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)],[87]) ).
thf(26,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/sandbox/benchmark/theBenchmark.p',ceq1) ).
thf(118,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)],[26]) ).
thf(119,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)],[118]) ).
thf(120,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)],[119]) ).
thf(32,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ convergent_lines ) )
=> ~ ( B @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ci4) ).
thf(141,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(142,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) )
| ~ ( B @ ( A @ convergent_lines ) ) ),
inference(cnf,[status(esa)],[141]) ).
thf(2210,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ ( B @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1998,142]) ).
thf(2211,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ ( B @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[2210]) ).
thf(2212,plain,
~ ( sk1 @ ( sk1 @ ( sk2 @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[2211:[bind(A,$thf( sk2 )),bind(B,$thf( sk1 ))]]) ).
thf(2278,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ apart_point_and_line ) )
!= ( sk1 @ ( sk1 @ ( sk2 @ intersection_point ) @ apart_point_and_line ) ) )
| ~ $true
| ( C @ ( A @ distinct_points ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[120,2212]) ).
thf(2279,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ apart_point_and_line ) )
!= ( sk1 @ ( sk1 @ ( sk2 @ intersection_point ) @ apart_point_and_line ) ) )
| ( C @ ( A @ distinct_points ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[2278]) ).
thf(2280,plain,
! [A: $i] :
( ( sk1 @ ( sk2 @ intersection_point ) @ ( A @ distinct_points ) )
| ~ ( sk1 @ ( A @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[2279:[bind(A,$thf( A )),bind(B,$thf( sk1 )),bind(C,$thf( sk1 @ ( sk2 @ intersection_point ) ))]]) ).
thf(479,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( D @ distinct_lines ) ) )
| ( D @ ( C @ distinct_lines ) )
| ~ $true
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[414,415]) ).
thf(480,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( D @ distinct_lines ) ) )
| ( D @ ( C @ distinct_lines ) )
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(simp,[status(thm)],[479]) ).
thf(481,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ distinct_lines ) )
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[480:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(139,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ convergent_lines ) )
=> ! [C: $i] :
( ( C @ ( A @ convergent_lines ) )
| ( C @ ( B @ distinct_lines ) ) ) ),
inference(miniscope,[status(thm)],[138]) ).
thf(140,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ convergent_lines ) )
| ( C @ ( B @ distinct_lines ) )
| ~ ( B @ ( A @ convergent_lines ) ) ),
inference(cnf,[status(esa)],[139]) ).
thf(3854,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ( C @ ( A @ convergent_lines ) )
| ( C @ ( B @ distinct_lines ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1998,140]) ).
thf(3855,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ( C @ ( A @ convergent_lines ) )
| ( C @ ( B @ distinct_lines ) ) ),
inference(simp,[status(thm)],[3854]) ).
thf(3856,plain,
! [A: $i] :
( ( A @ ( sk2 @ convergent_lines ) )
| ( A @ ( sk1 @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[3855:[bind(A,$thf( sk2 )),bind(B,$thf( sk1 ))]]) ).
thf(3890,plain,
! [A: $i] :
( ( A @ ( sk2 @ convergent_lines ) )
| ( A @ ( sk1 @ distinct_lines ) ) ),
inference(simp,[status(thm)],[3856]) ).
thf(3930,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk1 @ distinct_lines ) )
!= ( B @ ( C @ distinct_lines ) ) )
| ( C @ ( B @ convergent_lines ) )
| ~ $true
| ( A @ ( sk2 @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[3890,453]) ).
thf(3931,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk1 @ distinct_lines ) )
!= ( B @ ( C @ distinct_lines ) ) )
| ( C @ ( B @ convergent_lines ) )
| ( A @ ( sk2 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[3930]) ).
thf(3932,plain,
! [A: $i] :
( ( sk1 @ ( A @ convergent_lines ) )
| ( A @ ( sk2 @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[3931:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk1 ))]]) ).
thf(9710,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ ( A @ convergent_lines ) )
!= ( C @ ( B @ ( C @ parallel_through_point ) @ convergent_lines ) ) )
| ~ $true
| ( A @ ( sk2 @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[3932,117]) ).
thf(9711,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ ( A @ convergent_lines ) )
!= ( C @ ( B @ ( C @ parallel_through_point ) @ convergent_lines ) ) )
| ( A @ ( sk2 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[9710]) ).
thf(9712,plain,
! [A: $i] : ( A @ ( sk1 @ parallel_through_point ) @ ( sk2 @ convergent_lines ) ),
inference(pattern_uni,[status(thm)],[9711:[bind(A,$thf( E @ ( sk1 @ parallel_through_point ) )),bind(B,$thf( E )),bind(C,$thf( sk1 ))]]) ).
thf(9871,plain,
! [A: $i] : ( A @ ( sk1 @ parallel_through_point ) @ ( sk2 @ convergent_lines ) ),
inference(simp,[status(thm)],[9712]) ).
thf(9917,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk1 @ parallel_through_point ) @ ( sk2 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ $true
| ~ ( C @ ( B @ parallel_lines ) ) ),
inference(paramod_ordered,[status(thm)],[9871,110]) ).
thf(9918,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk1 @ parallel_through_point ) @ ( sk2 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( C @ ( B @ parallel_lines ) ) ),
inference(simp,[status(thm)],[9917]) ).
thf(9919,plain,
! [A: $i] :
~ ( A @ ( sk1 @ parallel_through_point ) @ ( sk2 @ parallel_lines ) ),
inference(pattern_uni,[status(thm)],[9918:[bind(A,$thf( E )),bind(B,$thf( sk2 )),bind(C,$thf( E @ ( sk1 @ parallel_through_point ) ))]]) ).
thf(10039,plain,
! [A: $i] :
~ ( A @ ( sk1 @ parallel_through_point ) @ ( sk2 @ parallel_lines ) ),
inference(simp,[status(thm)],[9919]) ).
thf(200,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ distinct_points ) )
!= ( B @ ( A @ distinct_points ) ) )
| ~ $true
| ~ ( B @ ( A @ equal_points ) ) ),
inference(paramod_ordered,[status(thm)],[42,84]) ).
thf(201,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ distinct_points ) )
!= ( B @ ( A @ distinct_points ) ) )
| ~ ( B @ ( A @ equal_points ) ) ),
inference(simp,[status(thm)],[200]) ).
thf(202,plain,
~ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ equal_points ) ),
inference(pattern_uni,[status(thm)],[201:[bind(A,$thf( sk2 @ ( sk1 @ intersection_point ) )),bind(B,$thf( sk3 @ ( sk1 @ intersection_point ) ))]]) ).
thf(1079,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ( C @ ( B @ convergent_lines ) )
| ( C @ ( A @ convergent_lines ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[41,91]) ).
thf(1080,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ( C @ ( B @ convergent_lines ) )
| ( C @ ( A @ convergent_lines ) ) ),
inference(simp,[status(thm)],[1079]) ).
thf(1081,plain,
! [A: $i] :
( ( A @ ( sk3 @ convergent_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[1080:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 ))]]) ).
thf(1136,plain,
! [A: $i] :
( ( A @ ( sk3 @ convergent_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[1081]) ).
thf(1163,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk3 @ convergent_lines ) )
!= ( C @ ( B @ ( C @ parallel_through_point ) @ convergent_lines ) ) )
| ~ $true
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1136,117]) ).
thf(1164,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk3 @ convergent_lines ) )
!= ( C @ ( B @ ( C @ parallel_through_point ) @ convergent_lines ) ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[1163]) ).
thf(1171,plain,
! [C: $i,B: $i,A: $i] :
( ( A != C )
| ( ( B @ ( C @ parallel_through_point ) )
!= sk3 )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[1164]) ).
thf(1173,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ parallel_through_point ) )
!= sk3 )
| ( B @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[1171]) ).
thf(3,axiom,
! [A: $i,B: $i] :
~ ( B @ ( A @ ( B @ orthogonal_through_point ) @ unorthogonal_lines ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ooc1) ).
thf(44,plain,
! [A: $i,B: $i] :
~ ( B @ ( A @ ( B @ orthogonal_through_point ) @ unorthogonal_lines ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(45,plain,
~ ? [A: $i,B: $i] : ( B @ ( A @ ( B @ orthogonal_through_point ) @ unorthogonal_lines ) ),
inference(miniscope,[status(thm)],[44]) ).
thf(46,plain,
! [B: $i,A: $i] :
~ ( B @ ( A @ ( B @ orthogonal_through_point ) @ unorthogonal_lines ) ),
inference(cnf,[status(esa)],[45]) ).
thf(14420,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)],[4262,46]) ).
thf(14421,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)],[14420]) ).
thf(14422,plain,
! [A: $i] : ( sk1 @ ( A @ ( sk2 @ orthogonal_through_point ) @ unorthogonal_lines ) ),
inference(pattern_uni,[status(thm)],[14421:[bind(A,$thf( E @ ( sk2 @ orthogonal_through_point ) )),bind(B,$thf( E )),bind(C,$thf( sk2 ))]]) ).
thf(14445,plain,
! [A: $i] : ( sk1 @ ( A @ ( sk2 @ orthogonal_through_point ) @ unorthogonal_lines ) ),
inference(simp,[status(thm)],[14422]) ).
thf(14452,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)],[14445,46]) ).
thf(14453,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)],[14452]) ).
thf(14472,plain,
! [C: $i,B: $i,A: $i] :
( ( sk1 != C )
| ( ( A @ ( sk2 @ orthogonal_through_point ) )
!= ( B @ ( C @ orthogonal_through_point ) ) ) ),
inference(simp,[status(thm)],[14453]) ).
thf(14478,plain,
! [B: $i,A: $i] :
( ( A @ ( sk2 @ orthogonal_through_point ) )
!= ( B @ ( sk1 @ orthogonal_through_point ) ) ),
inference(simp,[status(thm)],[14472]) ).
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/sandbox/benchmark/theBenchmark.p',cotno1) ).
thf(149,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(150,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)],[149]) ).
thf(153,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)],[150]) ).
thf(329,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)],[137,148]) ).
thf(330,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)],[329]) ).
thf(331,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ convergent_lines ) )
| ( B @ ( A @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[330:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(43,plain,
~ ( sk1 @ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ equal_lines ) ),
inference(cnfConj,[status(thm)],[39]) ).
thf(353,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ equal_lines ) )
!= ( sk1 @ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ equal_lines ) ) )
| ~ $true
| ( B @ ( A @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[331,43]) ).
thf(354,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ equal_lines ) )
!= ( sk1 @ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ equal_lines ) ) )
| ( B @ ( A @ convergent_lines ) ) ),
inference(simp,[status(thm)],[353]) ).
thf(355,plain,
sk1 @ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ convergent_lines ),
inference(pattern_uni,[status(thm)],[354:[bind(A,$thf( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) )),bind(B,$thf( sk1 ))]]) ).
thf(33,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ convergent_lines ) )
=> ~ ( A @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ci3) ).
thf(143,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(144,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) )
| ~ ( B @ ( A @ convergent_lines ) ) ),
inference(cnf,[status(esa)],[143]) ).
thf(2738,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ ( A @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[355,144]) ).
thf(2739,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ ( A @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[2738]) ).
thf(2740,plain,
~ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ ( sk1 @ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[2739:[bind(A,$thf( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) )),bind(B,$thf( sk1 ))]]) ).
thf(3857,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,140]) ).
thf(3858,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)],[3857]) ).
thf(3859,plain,
! [A: $i] :
( ( A @ ( sk1 @ convergent_lines ) )
| ( A @ ( sk2 @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[3858:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(3891,plain,
! [A: $i] :
( ( A @ ( sk1 @ convergent_lines ) )
| ( A @ ( sk2 @ distinct_lines ) ) ),
inference(simp,[status(thm)],[3859]) ).
thf(4868,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ distinct_lines ) )
!= ( B @ ( C @ distinct_lines ) ) )
| ( C @ ( B @ distinct_lines ) )
| ~ $true
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[3891,415]) ).
thf(4869,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ distinct_lines ) )
!= ( B @ ( C @ distinct_lines ) ) )
| ( C @ ( B @ distinct_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[4868]) ).
thf(4870,plain,
! [A: $i] :
( ( sk2 @ ( A @ distinct_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[4869:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk2 ))]]) ).
thf(4,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/sandbox/benchmark/theBenchmark.p',ceq2) ).
thf(47,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)],[4]) ).
thf(48,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)],[47]) ).
thf(49,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)],[48]) ).
thf(13,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ incident_point_and_line ) )
<=> ~ ( B @ ( A @ apart_point_and_line ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a4) ).
thf(75,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)],[13]) ).
thf(76,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)],[75]) ).
thf(77,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)],[76]) ).
thf(78,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ apart_point_and_line ) )
| ~ ( B @ ( A @ incident_point_and_line ) ) ),
inference(cnfConj,[status(thm)],[77]) ).
thf(194,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)],[49,78]) ).
thf(195,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)],[194]) ).
thf(196,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)],[195:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( A )),bind(E,$thf( C ))]]) ).
thf(517,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( D @ distinct_lines ) ) )
| ~ ( D @ ( C @ equal_lines ) )
| ~ $true
| ( B @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[137,474]) ).
thf(518,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( D @ distinct_lines ) ) )
| ~ ( D @ ( C @ equal_lines ) )
| ( B @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[517]) ).
thf(519,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ equal_lines ) )
| ( B @ ( A @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[518:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(948,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ equal_lines ) )
!= ( D @ ( C @ equal_lines ) ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ $true
| ~ ( A @ ( B @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[519,135]) ).
thf(949,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ equal_lines ) )
!= ( D @ ( C @ equal_lines ) ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ ( A @ ( B @ equal_lines ) ) ),
inference(simp,[status(thm)],[948]) ).
thf(950,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ distinct_lines ) )
| ~ ( A @ ( B @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[949:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(13236,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ distinct_lines ) )
!= ( E @ ( D @ distinct_lines ) ) )
| ~ $true
| ~ ( D @ ( E @ equal_lines ) )
| ~ ( C @ ( A @ incident_point_and_line ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[196,950]) ).
thf(13237,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ distinct_lines ) )
!= ( E @ ( D @ distinct_lines ) ) )
| ~ ( D @ ( E @ equal_lines ) )
| ~ ( C @ ( A @ incident_point_and_line ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[13236]) ).
thf(13238,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ equal_lines ) )
| ~ ( C @ ( A @ incident_point_and_line ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[13237:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( B )),bind(E,$thf( C ))]]) ).
thf(7,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/sandbox/benchmark/theBenchmark.p',ouo1) ).
thf(58,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)],[7]) ).
thf(59,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)],[58]) ).
thf(60,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)],[59]) ).
thf(6,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ orthogonal_lines ) )
<=> ~ ( B @ ( A @ unorthogonal_lines ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a5) ).
thf(52,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)],[6]) ).
thf(53,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)],[52]) ).
thf(54,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)],[53]) ).
thf(55,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ unorthogonal_lines ) )
| ~ ( B @ ( A @ orthogonal_lines ) ) ),
inference(cnfConj,[status(thm)],[54]) ).
thf(299,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)],[60,55]) ).
thf(300,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)],[299]) ).
thf(301,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)],[300:[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(311,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)],[137,63]) ).
thf(312,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( C @ distinct_lines ) ) )
| ( B @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[311]) ).
thf(313,plain,
! [A: $i] : ( A @ ( A @ equal_lines ) ),
inference(pattern_uni,[status(thm)],[312:[bind(A,$thf( B )),bind(B,$thf( B )),bind(C,$thf( B ))]]) ).
thf(320,plain,
! [A: $i] : ( A @ ( A @ equal_lines ) ),
inference(simp,[status(thm)],[313]) ).
thf(532,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( D @ distinct_lines ) ) )
| ~ ( D @ ( C @ equal_lines ) )
| ~ $true
| ~ ( A @ ( B @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[415,474]) ).
thf(533,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( D @ distinct_lines ) ) )
| ~ ( D @ ( C @ equal_lines ) )
| ~ ( A @ ( B @ distinct_lines ) ) ),
inference(simp,[status(thm)],[532]) ).
thf(534,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ equal_lines ) )
| ~ ( A @ ( B @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[533:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(3936,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk1 @ distinct_lines ) )
!= ( B @ ( C @ distinct_lines ) ) )
| ~ ( B @ ( C @ equal_lines ) )
| ~ $true
| ( A @ ( sk2 @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[3890,534]) ).
thf(3937,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk1 @ distinct_lines ) )
!= ( B @ ( C @ distinct_lines ) ) )
| ~ ( B @ ( C @ equal_lines ) )
| ( A @ ( sk2 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[3936]) ).
thf(3938,plain,
! [A: $i] :
( ~ ( A @ ( sk1 @ equal_lines ) )
| ( A @ ( sk2 @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[3937:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk1 ))]]) ).
thf(2183,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ ( B @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[355,142]) ).
thf(2184,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ ( B @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[2183]) ).
thf(2185,plain,
~ ( sk1 @ ( sk1 @ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[2184:[bind(A,$thf( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) )),bind(B,$thf( sk1 ))]]) ).
thf(37,axiom,
! [A: $i] :
~ ( A @ ( A @ distinct_points ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',apart1) ).
thf(155,plain,
! [A: $i] :
~ ( A @ ( A @ distinct_points ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(156,plain,
~ ? [A: $i] : ( A @ ( A @ distinct_points ) ),
inference(miniscope,[status(thm)],[155]) ).
thf(157,plain,
! [A: $i] :
~ ( A @ ( A @ distinct_points ) ),
inference(cnf,[status(esa)],[156]) ).
thf(7607,plain,
! [L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ line_connecting ) @ line )
!= ( G @ line ) )
| ( ( F @ ( E @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( L @ ( K @ line_connecting ) @ ( J @ ( I @ line_connecting ) @ intersection_point ) @ ( H @ ( G @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( L @ ( K @ line_connecting ) @ ( J @ ( I @ line_connecting ) @ intersection_point ) @ ( H @ ( G @ intersection_point ) @ distinct_points ) )
| ~ ( F @ ( E @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( D @ ( C @ convergent_lines ) )
| ~ ( D @ line )
| ~ ( C @ line )
| ~ ( F @ ( E @ convergent_lines ) )
| ~ ( F @ line )
| ~ ( E @ line )
| ~ ( H @ ( G @ convergent_lines ) )
| ~ ( H @ line )
| ~ $true
| ~ ( L @ ( K @ line_connecting ) @ ( J @ ( I @ line_connecting ) @ convergent_lines ) )
| ~ ( J @ ( I @ distinct_points ) )
| ~ ( J @ point )
| ~ ( I @ point )
| ~ ( L @ ( K @ distinct_points ) )
| ~ ( L @ point )
| ~ ( K @ point )
| ~ ( B @ ( A @ distinct_points ) )
| ~ ( B @ point )
| ~ ( A @ point ) ),
inference(paramod_ordered,[status(thm)],[122,6979]) ).
thf(7608,plain,
! [L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ line_connecting ) @ line )
!= ( G @ line ) )
| ( ( F @ ( E @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( L @ ( K @ line_connecting ) @ ( J @ ( I @ line_connecting ) @ intersection_point ) @ ( H @ ( G @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( L @ ( K @ line_connecting ) @ ( J @ ( I @ line_connecting ) @ intersection_point ) @ ( H @ ( G @ intersection_point ) @ distinct_points ) )
| ~ ( F @ ( E @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( D @ ( C @ convergent_lines ) )
| ~ ( D @ line )
| ~ ( C @ line )
| ~ ( F @ ( E @ convergent_lines ) )
| ~ ( F @ line )
| ~ ( E @ line )
| ~ ( H @ ( G @ convergent_lines ) )
| ~ ( H @ line )
| ~ ( L @ ( K @ line_connecting ) @ ( J @ ( I @ line_connecting ) @ convergent_lines ) )
| ~ ( J @ ( I @ distinct_points ) )
| ~ ( J @ point )
| ~ ( I @ point )
| ~ ( L @ ( K @ distinct_points ) )
| ~ ( L @ point )
| ~ ( K @ point )
| ~ ( B @ ( A @ distinct_points ) )
| ~ ( B @ point )
| ~ ( A @ point ) ),
inference(simp,[status(thm)],[7607]) ).
thf(7609,plain,
! [K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( I @ ( H @ line_connecting ) @ ( G @ ( F @ line_connecting ) @ intersection_point ) @ ( E @ ( K @ ( J @ line_connecting ) @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( I @ ( H @ line_connecting ) @ ( G @ ( F @ line_connecting ) @ intersection_point ) @ ( E @ ( K @ ( J @ line_connecting ) @ intersection_point ) @ distinct_points ) )
| ~ ( D @ ( C @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( B @ ( A @ convergent_lines ) )
| ~ ( B @ line )
| ~ ( A @ line )
| ~ ( D @ ( C @ convergent_lines ) )
| ~ ( D @ line )
| ~ ( C @ line )
| ~ ( E @ ( K @ ( J @ line_connecting ) @ convergent_lines ) )
| ~ ( E @ line )
| ~ ( I @ ( H @ line_connecting ) @ ( G @ ( F @ line_connecting ) @ convergent_lines ) )
| ~ ( G @ ( F @ distinct_points ) )
| ~ ( G @ point )
| ~ ( F @ point )
| ~ ( I @ ( H @ distinct_points ) )
| ~ ( I @ point )
| ~ ( H @ point )
| ~ ( K @ ( J @ distinct_points ) )
| ~ ( K @ point )
| ~ ( J @ point ) ),
inference(pattern_uni,[status(thm)],[7608:[bind(A,$thf( M )),bind(B,$thf( N )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( E )),bind(F,$thf( F )),bind(G,$thf( N @ ( M @ line_connecting ) ))]]) ).
thf(7749,plain,
! [K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( I @ ( H @ line_connecting ) @ ( G @ ( F @ line_connecting ) @ intersection_point ) @ ( E @ ( K @ ( J @ line_connecting ) @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( I @ ( H @ line_connecting ) @ ( G @ ( F @ line_connecting ) @ intersection_point ) @ ( E @ ( K @ ( J @ line_connecting ) @ intersection_point ) @ distinct_points ) )
| ~ ( D @ ( C @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( B @ ( A @ convergent_lines ) )
| ~ ( B @ line )
| ~ ( A @ line )
| ~ ( D @ ( C @ convergent_lines ) )
| ~ ( D @ line )
| ~ ( C @ line )
| ~ ( E @ ( K @ ( J @ line_connecting ) @ convergent_lines ) )
| ~ ( E @ line )
| ~ ( I @ ( H @ line_connecting ) @ ( G @ ( F @ line_connecting ) @ convergent_lines ) )
| ~ ( G @ ( F @ distinct_points ) )
| ~ ( G @ point )
| ~ ( F @ point )
| ~ ( I @ ( H @ distinct_points ) )
| ~ ( I @ point )
| ~ ( H @ point )
| ~ ( K @ ( J @ distinct_points ) )
| ~ ( K @ point )
| ~ ( J @ point ) ),
inference(simp,[status(thm)],[7609]) ).
thf(8591,plain,
! [M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ line_connecting ) @ line )
!= ( G @ line ) )
| ( ( F @ ( E @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( K @ ( J @ line_connecting ) @ ( I @ ( H @ line_connecting ) @ intersection_point ) @ ( G @ ( M @ ( L @ line_connecting ) @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( K @ ( J @ line_connecting ) @ ( I @ ( H @ line_connecting ) @ intersection_point ) @ ( G @ ( M @ ( L @ line_connecting ) @ intersection_point ) @ distinct_points ) )
| ~ ( F @ ( E @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( D @ ( C @ convergent_lines ) )
| ~ ( D @ line )
| ~ ( C @ line )
| ~ ( F @ ( E @ convergent_lines ) )
| ~ ( F @ line )
| ~ ( E @ line )
| ~ ( G @ ( M @ ( L @ line_connecting ) @ convergent_lines ) )
| ~ $true
| ~ ( K @ ( J @ line_connecting ) @ ( I @ ( H @ line_connecting ) @ convergent_lines ) )
| ~ ( I @ ( H @ distinct_points ) )
| ~ ( I @ point )
| ~ ( H @ point )
| ~ ( K @ ( J @ distinct_points ) )
| ~ ( K @ point )
| ~ ( J @ point )
| ~ ( M @ ( L @ distinct_points ) )
| ~ ( M @ point )
| ~ ( L @ point )
| ~ ( B @ ( A @ distinct_points ) )
| ~ ( B @ point )
| ~ ( A @ point ) ),
inference(paramod_ordered,[status(thm)],[122,7749]) ).
thf(8592,plain,
! [M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ line_connecting ) @ line )
!= ( G @ line ) )
| ( ( F @ ( E @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( K @ ( J @ line_connecting ) @ ( I @ ( H @ line_connecting ) @ intersection_point ) @ ( G @ ( M @ ( L @ line_connecting ) @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( K @ ( J @ line_connecting ) @ ( I @ ( H @ line_connecting ) @ intersection_point ) @ ( G @ ( M @ ( L @ line_connecting ) @ intersection_point ) @ distinct_points ) )
| ~ ( F @ ( E @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( D @ ( C @ convergent_lines ) )
| ~ ( D @ line )
| ~ ( C @ line )
| ~ ( F @ ( E @ convergent_lines ) )
| ~ ( F @ line )
| ~ ( E @ line )
| ~ ( G @ ( M @ ( L @ line_connecting ) @ convergent_lines ) )
| ~ ( K @ ( J @ line_connecting ) @ ( I @ ( H @ line_connecting ) @ convergent_lines ) )
| ~ ( I @ ( H @ distinct_points ) )
| ~ ( I @ point )
| ~ ( H @ point )
| ~ ( K @ ( J @ distinct_points ) )
| ~ ( K @ point )
| ~ ( J @ point )
| ~ ( M @ ( L @ distinct_points ) )
| ~ ( M @ point )
| ~ ( L @ point )
| ~ ( B @ ( A @ distinct_points ) )
| ~ ( B @ point )
| ~ ( A @ point ) ),
inference(simp,[status(thm)],[8591]) ).
thf(8593,plain,
! [L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( H @ ( G @ line_connecting ) @ ( F @ ( E @ line_connecting ) @ intersection_point ) @ ( L @ ( K @ line_connecting ) @ ( J @ ( I @ line_connecting ) @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( H @ ( G @ line_connecting ) @ ( F @ ( E @ line_connecting ) @ intersection_point ) @ ( L @ ( K @ line_connecting ) @ ( J @ ( I @ line_connecting ) @ intersection_point ) @ distinct_points ) )
| ~ ( D @ ( C @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( B @ ( A @ convergent_lines ) )
| ~ ( B @ line )
| ~ ( A @ line )
| ~ ( D @ ( C @ convergent_lines ) )
| ~ ( D @ line )
| ~ ( C @ line )
| ~ ( L @ ( K @ line_connecting ) @ ( J @ ( I @ line_connecting ) @ convergent_lines ) )
| ~ ( H @ ( G @ line_connecting ) @ ( F @ ( E @ line_connecting ) @ convergent_lines ) )
| ~ ( F @ ( E @ distinct_points ) )
| ~ ( F @ point )
| ~ ( E @ point )
| ~ ( H @ ( G @ distinct_points ) )
| ~ ( H @ point )
| ~ ( G @ point )
| ~ ( J @ ( I @ distinct_points ) )
| ~ ( J @ point )
| ~ ( I @ point )
| ~ ( L @ ( K @ distinct_points ) )
| ~ ( L @ point )
| ~ ( K @ point ) ),
inference(pattern_uni,[status(thm)],[8592:[bind(A,$thf( N )),bind(B,$thf( O )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( E )),bind(F,$thf( F )),bind(G,$thf( O @ ( N @ line_connecting ) ))]]) ).
thf(8717,plain,
! [L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( D @ ( C @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( H @ ( G @ line_connecting ) @ ( F @ ( E @ line_connecting ) @ intersection_point ) @ ( L @ ( K @ line_connecting ) @ ( J @ ( I @ line_connecting ) @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( H @ ( G @ line_connecting ) @ ( F @ ( E @ line_connecting ) @ intersection_point ) @ ( L @ ( K @ line_connecting ) @ ( J @ ( I @ line_connecting ) @ intersection_point ) @ distinct_points ) )
| ~ ( D @ ( C @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( B @ ( A @ convergent_lines ) )
| ~ ( B @ line )
| ~ ( A @ line )
| ~ ( D @ ( C @ convergent_lines ) )
| ~ ( D @ line )
| ~ ( C @ line )
| ~ ( L @ ( K @ line_connecting ) @ ( J @ ( I @ line_connecting ) @ convergent_lines ) )
| ~ ( H @ ( G @ line_connecting ) @ ( F @ ( E @ line_connecting ) @ convergent_lines ) )
| ~ ( F @ ( E @ distinct_points ) )
| ~ ( F @ point )
| ~ ( E @ point )
| ~ ( H @ ( G @ distinct_points ) )
| ~ ( H @ point )
| ~ ( G @ point )
| ~ ( J @ ( I @ distinct_points ) )
| ~ ( J @ point )
| ~ ( I @ point )
| ~ ( L @ ( K @ distinct_points ) )
| ~ ( L @ point )
| ~ ( K @ point ) ),
inference(simp,[status(thm)],[8593]) ).
thf(9351,plain,
! [N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ line_connecting ) @ line )
!= ( E @ line ) )
| ( ( F @ ( E @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( J @ ( I @ line_connecting ) @ ( H @ ( G @ line_connecting ) @ intersection_point ) @ ( N @ ( M @ line_connecting ) @ ( L @ ( K @ line_connecting ) @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( J @ ( I @ line_connecting ) @ ( H @ ( G @ line_connecting ) @ intersection_point ) @ ( N @ ( M @ line_connecting ) @ ( L @ ( K @ line_connecting ) @ intersection_point ) @ distinct_points ) )
| ~ ( F @ ( E @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( D @ ( C @ convergent_lines ) )
| ~ ( D @ line )
| ~ ( C @ line )
| ~ ( F @ ( E @ convergent_lines ) )
| ~ ( F @ line )
| ~ $true
| ~ ( N @ ( M @ line_connecting ) @ ( L @ ( K @ line_connecting ) @ convergent_lines ) )
| ~ ( J @ ( I @ line_connecting ) @ ( H @ ( G @ line_connecting ) @ convergent_lines ) )
| ~ ( H @ ( G @ distinct_points ) )
| ~ ( H @ point )
| ~ ( G @ point )
| ~ ( J @ ( I @ distinct_points ) )
| ~ ( J @ point )
| ~ ( I @ point )
| ~ ( L @ ( K @ distinct_points ) )
| ~ ( L @ point )
| ~ ( K @ point )
| ~ ( N @ ( M @ distinct_points ) )
| ~ ( N @ point )
| ~ ( M @ point )
| ~ ( B @ ( A @ distinct_points ) )
| ~ ( B @ point )
| ~ ( A @ point ) ),
inference(paramod_ordered,[status(thm)],[122,8717]) ).
thf(9352,plain,
! [N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ line_connecting ) @ line )
!= ( E @ line ) )
| ( ( F @ ( E @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( J @ ( I @ line_connecting ) @ ( H @ ( G @ line_connecting ) @ intersection_point ) @ ( N @ ( M @ line_connecting ) @ ( L @ ( K @ line_connecting ) @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( J @ ( I @ line_connecting ) @ ( H @ ( G @ line_connecting ) @ intersection_point ) @ ( N @ ( M @ line_connecting ) @ ( L @ ( K @ line_connecting ) @ intersection_point ) @ distinct_points ) )
| ~ ( F @ ( E @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( D @ ( C @ convergent_lines ) )
| ~ ( D @ line )
| ~ ( C @ line )
| ~ ( F @ ( E @ convergent_lines ) )
| ~ ( F @ line )
| ~ ( N @ ( M @ line_connecting ) @ ( L @ ( K @ line_connecting ) @ convergent_lines ) )
| ~ ( J @ ( I @ line_connecting ) @ ( H @ ( G @ line_connecting ) @ convergent_lines ) )
| ~ ( H @ ( G @ distinct_points ) )
| ~ ( H @ point )
| ~ ( G @ point )
| ~ ( J @ ( I @ distinct_points ) )
| ~ ( J @ point )
| ~ ( I @ point )
| ~ ( L @ ( K @ distinct_points ) )
| ~ ( L @ point )
| ~ ( K @ point )
| ~ ( N @ ( M @ distinct_points ) )
| ~ ( N @ point )
| ~ ( M @ point )
| ~ ( B @ ( A @ distinct_points ) )
| ~ ( B @ point )
| ~ ( A @ point ) ),
inference(simp,[status(thm)],[9351]) ).
thf(9353,plain,
! [M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( M @ ( L @ line_connecting ) @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( G @ ( F @ line_connecting ) @ ( E @ ( D @ line_connecting ) @ intersection_point ) @ ( K @ ( J @ line_connecting ) @ ( I @ ( H @ line_connecting ) @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( G @ ( F @ line_connecting ) @ ( E @ ( D @ line_connecting ) @ intersection_point ) @ ( K @ ( J @ line_connecting ) @ ( I @ ( H @ line_connecting ) @ intersection_point ) @ distinct_points ) )
| ~ ( C @ ( M @ ( L @ line_connecting ) @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( B @ ( A @ convergent_lines ) )
| ~ ( B @ line )
| ~ ( A @ line )
| ~ ( C @ ( M @ ( L @ line_connecting ) @ convergent_lines ) )
| ~ ( C @ line )
| ~ ( K @ ( J @ line_connecting ) @ ( I @ ( H @ line_connecting ) @ convergent_lines ) )
| ~ ( G @ ( F @ line_connecting ) @ ( E @ ( D @ line_connecting ) @ convergent_lines ) )
| ~ ( E @ ( D @ distinct_points ) )
| ~ ( E @ point )
| ~ ( D @ point )
| ~ ( G @ ( F @ distinct_points ) )
| ~ ( G @ point )
| ~ ( F @ point )
| ~ ( I @ ( H @ distinct_points ) )
| ~ ( I @ point )
| ~ ( H @ point )
| ~ ( K @ ( J @ distinct_points ) )
| ~ ( K @ point )
| ~ ( J @ point )
| ~ ( M @ ( L @ distinct_points ) )
| ~ ( M @ point )
| ~ ( L @ point ) ),
inference(pattern_uni,[status(thm)],[9352:[bind(A,$thf( O )),bind(B,$thf( P )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( P @ ( O @ line_connecting ) ))]]) ).
thf(9480,plain,
! [M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( M @ ( L @ line_connecting ) @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( G @ ( F @ line_connecting ) @ ( E @ ( D @ line_connecting ) @ intersection_point ) @ ( K @ ( J @ line_connecting ) @ ( I @ ( H @ line_connecting ) @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( G @ ( F @ line_connecting ) @ ( E @ ( D @ line_connecting ) @ intersection_point ) @ ( K @ ( J @ line_connecting ) @ ( I @ ( H @ line_connecting ) @ intersection_point ) @ distinct_points ) )
| ~ ( C @ ( M @ ( L @ line_connecting ) @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( B @ ( A @ convergent_lines ) )
| ~ ( B @ line )
| ~ ( A @ line )
| ~ ( C @ ( M @ ( L @ line_connecting ) @ convergent_lines ) )
| ~ ( C @ line )
| ~ ( K @ ( J @ line_connecting ) @ ( I @ ( H @ line_connecting ) @ convergent_lines ) )
| ~ ( G @ ( F @ line_connecting ) @ ( E @ ( D @ line_connecting ) @ convergent_lines ) )
| ~ ( E @ ( D @ distinct_points ) )
| ~ ( E @ point )
| ~ ( D @ point )
| ~ ( G @ ( F @ distinct_points ) )
| ~ ( G @ point )
| ~ ( F @ point )
| ~ ( I @ ( H @ distinct_points ) )
| ~ ( I @ point )
| ~ ( H @ point )
| ~ ( K @ ( J @ distinct_points ) )
| ~ ( K @ point )
| ~ ( J @ point )
| ~ ( M @ ( L @ distinct_points ) )
| ~ ( M @ point )
| ~ ( L @ point ) ),
inference(simp,[status(thm)],[9353]) ).
thf(3755,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ( C @ ( A @ convergent_lines ) )
| ( C @ ( B @ distinct_lines ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[41,140]) ).
thf(3756,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ( C @ ( A @ convergent_lines ) )
| ( C @ ( B @ distinct_lines ) ) ),
inference(simp,[status(thm)],[3755]) ).
thf(3757,plain,
! [A: $i] :
( ( A @ ( sk1 @ convergent_lines ) )
| ( A @ ( sk3 @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[3756:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 ))]]) ).
thf(3899,plain,
! [A: $i] :
( ( A @ ( sk1 @ convergent_lines ) )
| ( A @ ( sk3 @ distinct_lines ) ) ),
inference(simp,[status(thm)],[3757]) ).
thf(6394,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk3 @ distinct_lines ) )
!= ( B @ ( C @ distinct_lines ) ) )
| ( C @ ( B @ convergent_lines ) )
| ~ $true
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[3899,453]) ).
thf(6395,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk3 @ distinct_lines ) )
!= ( B @ ( C @ distinct_lines ) ) )
| ( C @ ( B @ convergent_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[6394]) ).
thf(6396,plain,
! [A: $i] :
( ( sk3 @ ( A @ convergent_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[6395:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk3 ))]]) ).
thf(419,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( D @ ( C @ distinct_lines ) ) )
| ( D @ ( C @ convergent_lines ) )
| ~ $true
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[414,148]) ).
thf(420,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( D @ ( C @ distinct_lines ) ) )
| ( D @ ( C @ convergent_lines ) )
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(simp,[status(thm)],[419]) ).
thf(421,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ convergent_lines ) )
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[420:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(152,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)],[150]) ).
thf(56,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ orthogonal_lines ) )
| ( B @ ( A @ unorthogonal_lines ) ) ),
inference(cnfConj,[status(thm)],[54]) ).
thf(57,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ orthogonal_lines ) )
| ( B @ ( A @ unorthogonal_lines ) ) ),
inference(simp,[status(thm)],[56]) ).
thf(215,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)],[101,46]) ).
thf(216,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)],[215]) ).
thf(217,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( A @ orthogonal_through_point ) @ convergent_lines ) ),
inference(pattern_uni,[status(thm)],[216:[bind(A,$thf( F @ ( B @ orthogonal_through_point ) )),bind(B,$thf( B )),bind(C,$thf( F )),bind(D,$thf( B ))]]) ).
thf(221,plain,
! [B: $i,A: $i] : ( A @ ( B @ ( A @ orthogonal_through_point ) @ convergent_lines ) ),
inference(simp,[status(thm)],[217]) ).
thf(2156,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)],[221,142]) ).
thf(2157,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)],[2156]) ).
thf(2158,plain,
! [B: $i,A: $i] :
~ ( A @ ( A @ ( B @ ( A @ orthogonal_through_point ) @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[2157:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F @ ( E @ orthogonal_through_point ) )),bind(D,$thf( E ))]]) ).
thf(2222,plain,
! [B: $i,A: $i] :
~ ( A @ ( A @ ( B @ ( A @ orthogonal_through_point ) @ intersection_point ) @ apart_point_and_line ) ),
inference(simp,[status(thm)],[2158]) ).
thf(158,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ convergent_lines ) )
!= ( A @ ( A @ convergent_lines ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[41,106]) ).
thf(159,plain,
! [A: $i] :
( ( sk3 @ ( sk1 @ convergent_lines ) )
!= ( A @ ( A @ convergent_lines ) ) ),
inference(simp,[status(thm)],[158]) ).
thf(162,plain,
! [A: $i] :
( ( sk3 != A )
| ( sk1 != A ) ),
inference(simp,[status(thm)],[159]) ).
thf(164,plain,
sk3 != sk1,
inference(simp,[status(thm)],[162]) ).
thf(174,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ parallel_through_point ) @ convergent_lines ) )
!= ( sk2 @ ( sk1 @ convergent_lines ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[40,117]) ).
thf(175,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( B @ parallel_through_point ) @ convergent_lines ) )
!= ( sk2 @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[174]) ).
thf(177,plain,
! [B: $i,A: $i] :
( ( B != sk2 )
| ( ( A @ ( B @ parallel_through_point ) )
!= sk1 ) ),
inference(simp,[status(thm)],[175]) ).
thf(179,plain,
! [A: $i] :
( ( A @ ( sk2 @ parallel_through_point ) )
!= sk1 ),
inference(simp,[status(thm)],[177]) ).
thf(3981,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk1 @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ~ $true
| ~ ( B @ ( C @ equal_lines ) )
| ( A @ ( sk2 @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[3890,950]) ).
thf(3982,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk1 @ distinct_lines ) )
!= ( C @ ( B @ distinct_lines ) ) )
| ~ ( B @ ( C @ equal_lines ) )
| ( A @ ( sk2 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[3981]) ).
thf(3983,plain,
! [A: $i] :
( ~ ( sk1 @ ( A @ equal_lines ) )
| ( A @ ( sk2 @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[3982:[bind(A,$thf( A )),bind(B,$thf( sk1 )),bind(C,$thf( A ))]]) ).
thf(1150,plain,
! [A: $i] :
( ~ $true
| ( ( A @ ( sk2 @ convergent_lines ) )
!= ( A @ ( sk1 @ convergent_lines ) ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(eqfactor_ordered,[status(thm)],[1128]) ).
thf(1151,plain,
! [A: $i] :
( ( ( A @ ( sk2 @ convergent_lines ) )
!= ( A @ ( sk1 @ convergent_lines ) ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[1150]) ).
thf(2007,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ parallel_through_point ) @ convergent_lines ) )
!= ( sk1 @ ( sk2 @ convergent_lines ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1998,117]) ).
thf(2008,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( B @ parallel_through_point ) @ convergent_lines ) )
!= ( sk1 @ ( sk2 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[2007]) ).
thf(2016,plain,
! [B: $i,A: $i] :
( ( B != sk1 )
| ( ( A @ ( B @ parallel_through_point ) )
!= sk2 ) ),
inference(simp,[status(thm)],[2008]) ).
thf(2017,plain,
! [A: $i] :
( ( A @ ( sk1 @ parallel_through_point ) )
!= sk2 ),
inference(simp,[status(thm)],[2016]) ).
thf(1168,plain,
! [A: $i] :
( ~ $true
| ( ( A @ ( sk3 @ convergent_lines ) )
!= ( A @ ( sk1 @ convergent_lines ) ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(eqfactor_ordered,[status(thm)],[1136]) ).
thf(1169,plain,
! [A: $i] :
( ( ( A @ ( sk3 @ convergent_lines ) )
!= ( A @ ( sk1 @ convergent_lines ) ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[1168]) ).
thf(954,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ equal_lines ) )
!= ( sk1 @ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ equal_lines ) ) )
| ~ $true
| ~ ( A @ ( B @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[519,43]) ).
thf(955,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ equal_lines ) )
!= ( sk1 @ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ equal_lines ) ) )
| ~ ( A @ ( B @ equal_lines ) ) ),
inference(simp,[status(thm)],[954]) ).
thf(956,plain,
~ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ ( sk1 @ equal_lines ) ),
inference(pattern_uni,[status(thm)],[955:[bind(A,$thf( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) )),bind(B,$thf( sk1 ))]]) ).
thf(4197,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ $true
| ( C @ ( A @ unorthogonal_lines ) )
| ( B @ ( A @ unorthogonal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[41,146]) ).
thf(4198,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ( C @ ( A @ unorthogonal_lines ) )
| ( B @ ( A @ unorthogonal_lines ) ) ),
inference(simp,[status(thm)],[4197]) ).
thf(4199,plain,
! [A: $i] :
( ( sk3 @ ( A @ unorthogonal_lines ) )
| ( sk1 @ ( A @ unorthogonal_lines ) ) ),
inference(pattern_uni,[status(thm)],[4198:[bind(A,$thf( A )),bind(B,$thf( sk1 )),bind(C,$thf( sk3 ))]]) ).
thf(13365,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ unorthogonal_lines ) )
!= ( C @ ( B @ ( C @ orthogonal_through_point ) @ unorthogonal_lines ) ) )
| ~ $true
| ( sk1 @ ( A @ unorthogonal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[4199,46]) ).
thf(13366,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ unorthogonal_lines ) )
!= ( C @ ( B @ ( C @ orthogonal_through_point ) @ unorthogonal_lines ) ) )
| ( sk1 @ ( A @ unorthogonal_lines ) ) ),
inference(simp,[status(thm)],[13365]) ).
thf(13367,plain,
! [A: $i] : ( sk1 @ ( A @ ( sk3 @ orthogonal_through_point ) @ unorthogonal_lines ) ),
inference(pattern_uni,[status(thm)],[13366:[bind(A,$thf( E @ ( sk3 @ orthogonal_through_point ) )),bind(B,$thf( E )),bind(C,$thf( sk3 ))]]) ).
thf(13391,plain,
! [A: $i] : ( sk1 @ ( A @ ( sk3 @ orthogonal_through_point ) @ unorthogonal_lines ) ),
inference(simp,[status(thm)],[13367]) ).
thf(13411,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ ( A @ ( sk3 @ orthogonal_through_point ) @ unorthogonal_lines ) )
!= ( C @ ( B @ unorthogonal_lines ) ) )
| ~ $true
| ~ ( C @ ( B @ orthogonal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[13391,55]) ).
thf(13412,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ ( A @ ( sk3 @ orthogonal_through_point ) @ unorthogonal_lines ) )
!= ( C @ ( B @ unorthogonal_lines ) ) )
| ~ ( C @ ( B @ orthogonal_lines ) ) ),
inference(simp,[status(thm)],[13411]) ).
thf(13413,plain,
! [A: $i] :
~ ( sk1 @ ( A @ ( sk3 @ orthogonal_through_point ) @ orthogonal_lines ) ),
inference(pattern_uni,[status(thm)],[13412:[bind(A,$thf( E )),bind(B,$thf( E @ ( sk3 @ orthogonal_through_point ) )),bind(C,$thf( sk1 ))]]) ).
thf(13420,plain,
! [A: $i] :
~ ( sk1 @ ( A @ ( sk3 @ orthogonal_through_point ) @ orthogonal_lines ) ),
inference(simp,[status(thm)],[13413]) ).
thf(969,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ equal_lines ) )
!= ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ ( sk1 @ equal_lines ) ) )
| ~ $true
| ( B @ ( A @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[331,956]) ).
thf(970,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ equal_lines ) )
!= ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ ( sk1 @ equal_lines ) ) )
| ( B @ ( A @ convergent_lines ) ) ),
inference(simp,[status(thm)],[969]) ).
thf(971,plain,
sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ ( sk1 @ convergent_lines ),
inference(pattern_uni,[status(thm)],[970:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) ))]]) ).
thf(986,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ $true
| ~ ( B @ ( A @ parallel_lines ) ) ),
inference(paramod_ordered,[status(thm)],[971,110]) ).
thf(987,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ ( B @ ( A @ parallel_lines ) ) ),
inference(simp,[status(thm)],[986]) ).
thf(988,plain,
~ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ ( sk1 @ parallel_lines ) ),
inference(pattern_uni,[status(thm)],[987:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) ))]]) ).
thf(21,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ distinct_points ) )
=> ~ ( B @ ( A @ line_connecting ) @ ( A @ apart_point_and_line ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ci1) ).
thf(102,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)],[21]) ).
thf(103,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ line_connecting ) @ ( A @ apart_point_and_line ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(cnf,[status(esa)],[102]) ).
thf(241,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ distinct_points ) )
!= ( B @ ( A @ distinct_points ) ) )
| ~ ( B @ ( A @ line_connecting ) @ ( A @ apart_point_and_line ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[42,103]) ).
thf(242,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ distinct_points ) )
!= ( B @ ( A @ distinct_points ) ) )
| ~ ( B @ ( A @ line_connecting ) @ ( A @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[241]) ).
thf(243,plain,
~ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[242:[bind(A,$thf( sk2 @ ( sk1 @ intersection_point ) )),bind(B,$thf( sk3 @ ( sk1 @ intersection_point ) ))]]) ).
thf(10688,plain,
! [O: $i,N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ line_connecting ) @ line )
!= ( E @ line ) )
| ( ( E @ ( O @ ( N @ line_connecting ) @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( I @ ( H @ line_connecting ) @ ( G @ ( F @ line_connecting ) @ intersection_point ) @ ( M @ ( L @ line_connecting ) @ ( K @ ( J @ line_connecting ) @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( I @ ( H @ line_connecting ) @ ( G @ ( F @ line_connecting ) @ intersection_point ) @ ( M @ ( L @ line_connecting ) @ ( K @ ( J @ line_connecting ) @ intersection_point ) @ distinct_points ) )
| ~ ( E @ ( O @ ( N @ line_connecting ) @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( D @ ( C @ convergent_lines ) )
| ~ ( D @ line )
| ~ ( C @ line )
| ~ ( E @ ( O @ ( N @ line_connecting ) @ convergent_lines ) )
| ~ $true
| ~ ( M @ ( L @ line_connecting ) @ ( K @ ( J @ line_connecting ) @ convergent_lines ) )
| ~ ( I @ ( H @ line_connecting ) @ ( G @ ( F @ line_connecting ) @ convergent_lines ) )
| ~ ( G @ ( F @ distinct_points ) )
| ~ ( G @ point )
| ~ ( F @ point )
| ~ ( I @ ( H @ distinct_points ) )
| ~ ( I @ point )
| ~ ( H @ point )
| ~ ( K @ ( J @ distinct_points ) )
| ~ ( K @ point )
| ~ ( J @ point )
| ~ ( M @ ( L @ distinct_points ) )
| ~ ( M @ point )
| ~ ( L @ point )
| ~ ( O @ ( N @ distinct_points ) )
| ~ ( O @ point )
| ~ ( N @ point )
| ~ ( B @ ( A @ distinct_points ) )
| ~ ( B @ point )
| ~ ( A @ point ) ),
inference(paramod_ordered,[status(thm)],[122,9480]) ).
thf(10689,plain,
! [O: $i,N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ line_connecting ) @ line )
!= ( E @ line ) )
| ( ( E @ ( O @ ( N @ line_connecting ) @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( I @ ( H @ line_connecting ) @ ( G @ ( F @ line_connecting ) @ intersection_point ) @ ( M @ ( L @ line_connecting ) @ ( K @ ( J @ line_connecting ) @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( I @ ( H @ line_connecting ) @ ( G @ ( F @ line_connecting ) @ intersection_point ) @ ( M @ ( L @ line_connecting ) @ ( K @ ( J @ line_connecting ) @ intersection_point ) @ distinct_points ) )
| ~ ( E @ ( O @ ( N @ line_connecting ) @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( D @ ( C @ convergent_lines ) )
| ~ ( D @ line )
| ~ ( C @ line )
| ~ ( E @ ( O @ ( N @ line_connecting ) @ convergent_lines ) )
| ~ ( M @ ( L @ line_connecting ) @ ( K @ ( J @ line_connecting ) @ convergent_lines ) )
| ~ ( I @ ( H @ line_connecting ) @ ( G @ ( F @ line_connecting ) @ convergent_lines ) )
| ~ ( G @ ( F @ distinct_points ) )
| ~ ( G @ point )
| ~ ( F @ point )
| ~ ( I @ ( H @ distinct_points ) )
| ~ ( I @ point )
| ~ ( H @ point )
| ~ ( K @ ( J @ distinct_points ) )
| ~ ( K @ point )
| ~ ( J @ point )
| ~ ( M @ ( L @ distinct_points ) )
| ~ ( M @ point )
| ~ ( L @ point )
| ~ ( O @ ( N @ distinct_points ) )
| ~ ( O @ point )
| ~ ( N @ point )
| ~ ( B @ ( A @ distinct_points ) )
| ~ ( B @ point )
| ~ ( A @ point ) ),
inference(simp,[status(thm)],[10688]) ).
thf(10690,plain,
! [N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( N @ ( M @ line_connecting ) @ ( L @ ( K @ line_connecting ) @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( F @ ( E @ line_connecting ) @ ( D @ ( C @ line_connecting ) @ intersection_point ) @ ( J @ ( I @ line_connecting ) @ ( H @ ( G @ line_connecting ) @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( F @ ( E @ line_connecting ) @ ( D @ ( C @ line_connecting ) @ intersection_point ) @ ( J @ ( I @ line_connecting ) @ ( H @ ( G @ line_connecting ) @ intersection_point ) @ distinct_points ) )
| ~ ( N @ ( M @ line_connecting ) @ ( L @ ( K @ line_connecting ) @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( B @ ( A @ convergent_lines ) )
| ~ ( B @ line )
| ~ ( A @ line )
| ~ ( N @ ( M @ line_connecting ) @ ( L @ ( K @ line_connecting ) @ convergent_lines ) )
| ~ ( J @ ( I @ line_connecting ) @ ( H @ ( G @ line_connecting ) @ convergent_lines ) )
| ~ ( F @ ( E @ line_connecting ) @ ( D @ ( C @ line_connecting ) @ convergent_lines ) )
| ~ ( D @ ( C @ distinct_points ) )
| ~ ( D @ point )
| ~ ( C @ point )
| ~ ( F @ ( E @ distinct_points ) )
| ~ ( F @ point )
| ~ ( E @ point )
| ~ ( H @ ( G @ distinct_points ) )
| ~ ( H @ point )
| ~ ( G @ point )
| ~ ( J @ ( I @ distinct_points ) )
| ~ ( J @ point )
| ~ ( I @ point )
| ~ ( L @ ( K @ distinct_points ) )
| ~ ( L @ point )
| ~ ( K @ point )
| ~ ( N @ ( M @ distinct_points ) )
| ~ ( N @ point )
| ~ ( M @ point ) ),
inference(pattern_uni,[status(thm)],[10689:[bind(A,$thf( P )),bind(B,$thf( Q )),bind(C,$thf( C )),bind(D,$thf( D )),bind(E,$thf( Q @ ( P @ line_connecting ) ))]]) ).
thf(10880,plain,
! [N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( N @ ( M @ line_connecting ) @ ( L @ ( K @ line_connecting ) @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( F @ ( E @ line_connecting ) @ ( D @ ( C @ line_connecting ) @ intersection_point ) @ ( J @ ( I @ line_connecting ) @ ( H @ ( G @ line_connecting ) @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( F @ ( E @ line_connecting ) @ ( D @ ( C @ line_connecting ) @ intersection_point ) @ ( J @ ( I @ line_connecting ) @ ( H @ ( G @ line_connecting ) @ intersection_point ) @ distinct_points ) )
| ~ ( N @ ( M @ line_connecting ) @ ( L @ ( K @ line_connecting ) @ intersection_point ) @ ( B @ ( A @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( B @ ( A @ convergent_lines ) )
| ~ ( B @ line )
| ~ ( A @ line )
| ~ ( N @ ( M @ line_connecting ) @ ( L @ ( K @ line_connecting ) @ convergent_lines ) )
| ~ ( J @ ( I @ line_connecting ) @ ( H @ ( G @ line_connecting ) @ convergent_lines ) )
| ~ ( F @ ( E @ line_connecting ) @ ( D @ ( C @ line_connecting ) @ convergent_lines ) )
| ~ ( D @ ( C @ distinct_points ) )
| ~ ( D @ point )
| ~ ( C @ point )
| ~ ( F @ ( E @ distinct_points ) )
| ~ ( F @ point )
| ~ ( E @ point )
| ~ ( H @ ( G @ distinct_points ) )
| ~ ( H @ point )
| ~ ( G @ point )
| ~ ( J @ ( I @ distinct_points ) )
| ~ ( J @ point )
| ~ ( I @ point )
| ~ ( L @ ( K @ distinct_points ) )
| ~ ( L @ point )
| ~ ( K @ point )
| ~ ( N @ ( M @ distinct_points ) )
| ~ ( N @ point )
| ~ ( M @ point ) ),
inference(simp,[status(thm)],[10690]) ).
thf(11997,plain,
! [P: $i,O: $i,N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ line_connecting ) @ line )
!= ( C @ line ) )
| ( ( P @ ( O @ line_connecting ) @ ( N @ ( M @ line_connecting ) @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( H @ ( G @ line_connecting ) @ ( F @ ( E @ line_connecting ) @ intersection_point ) @ ( L @ ( K @ line_connecting ) @ ( J @ ( I @ line_connecting ) @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( H @ ( G @ line_connecting ) @ ( F @ ( E @ line_connecting ) @ intersection_point ) @ ( L @ ( K @ line_connecting ) @ ( J @ ( I @ line_connecting ) @ intersection_point ) @ distinct_points ) )
| ~ ( P @ ( O @ line_connecting ) @ ( N @ ( M @ line_connecting ) @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( D @ ( C @ convergent_lines ) )
| ~ ( D @ line )
| ~ $true
| ~ ( P @ ( O @ line_connecting ) @ ( N @ ( M @ line_connecting ) @ convergent_lines ) )
| ~ ( L @ ( K @ line_connecting ) @ ( J @ ( I @ line_connecting ) @ convergent_lines ) )
| ~ ( H @ ( G @ line_connecting ) @ ( F @ ( E @ line_connecting ) @ convergent_lines ) )
| ~ ( F @ ( E @ distinct_points ) )
| ~ ( F @ point )
| ~ ( E @ point )
| ~ ( H @ ( G @ distinct_points ) )
| ~ ( H @ point )
| ~ ( G @ point )
| ~ ( J @ ( I @ distinct_points ) )
| ~ ( J @ point )
| ~ ( I @ point )
| ~ ( L @ ( K @ distinct_points ) )
| ~ ( L @ point )
| ~ ( K @ point )
| ~ ( N @ ( M @ distinct_points ) )
| ~ ( N @ point )
| ~ ( M @ point )
| ~ ( P @ ( O @ distinct_points ) )
| ~ ( P @ point )
| ~ ( O @ point )
| ~ ( B @ ( A @ distinct_points ) )
| ~ ( B @ point )
| ~ ( A @ point ) ),
inference(paramod_ordered,[status(thm)],[122,10880]) ).
thf(11998,plain,
! [P: $i,O: $i,N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ line_connecting ) @ line )
!= ( C @ line ) )
| ( ( P @ ( O @ line_connecting ) @ ( N @ ( M @ line_connecting ) @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( H @ ( G @ line_connecting ) @ ( F @ ( E @ line_connecting ) @ intersection_point ) @ ( L @ ( K @ line_connecting ) @ ( J @ ( I @ line_connecting ) @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( H @ ( G @ line_connecting ) @ ( F @ ( E @ line_connecting ) @ intersection_point ) @ ( L @ ( K @ line_connecting ) @ ( J @ ( I @ line_connecting ) @ intersection_point ) @ distinct_points ) )
| ~ ( P @ ( O @ line_connecting ) @ ( N @ ( M @ line_connecting ) @ intersection_point ) @ ( D @ ( C @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( D @ ( C @ convergent_lines ) )
| ~ ( D @ line )
| ~ ( P @ ( O @ line_connecting ) @ ( N @ ( M @ line_connecting ) @ convergent_lines ) )
| ~ ( L @ ( K @ line_connecting ) @ ( J @ ( I @ line_connecting ) @ convergent_lines ) )
| ~ ( H @ ( G @ line_connecting ) @ ( F @ ( E @ line_connecting ) @ convergent_lines ) )
| ~ ( F @ ( E @ distinct_points ) )
| ~ ( F @ point )
| ~ ( E @ point )
| ~ ( H @ ( G @ distinct_points ) )
| ~ ( H @ point )
| ~ ( G @ point )
| ~ ( J @ ( I @ distinct_points ) )
| ~ ( J @ point )
| ~ ( I @ point )
| ~ ( L @ ( K @ distinct_points ) )
| ~ ( L @ point )
| ~ ( K @ point )
| ~ ( N @ ( M @ distinct_points ) )
| ~ ( N @ point )
| ~ ( M @ point )
| ~ ( P @ ( O @ distinct_points ) )
| ~ ( P @ point )
| ~ ( O @ point )
| ~ ( B @ ( A @ distinct_points ) )
| ~ ( B @ point )
| ~ ( A @ point ) ),
inference(simp,[status(thm)],[11997]) ).
thf(11999,plain,
! [O: $i,N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( M @ ( L @ line_connecting ) @ ( K @ ( J @ line_connecting ) @ intersection_point ) @ ( A @ ( O @ ( N @ line_connecting ) @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( E @ ( D @ line_connecting ) @ ( C @ ( B @ line_connecting ) @ intersection_point ) @ ( I @ ( H @ line_connecting ) @ ( G @ ( F @ line_connecting ) @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( E @ ( D @ line_connecting ) @ ( C @ ( B @ line_connecting ) @ intersection_point ) @ ( I @ ( H @ line_connecting ) @ ( G @ ( F @ line_connecting ) @ intersection_point ) @ distinct_points ) )
| ~ ( M @ ( L @ line_connecting ) @ ( K @ ( J @ line_connecting ) @ intersection_point ) @ ( A @ ( O @ ( N @ line_connecting ) @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( A @ ( O @ ( N @ line_connecting ) @ convergent_lines ) )
| ~ ( A @ line )
| ~ ( M @ ( L @ line_connecting ) @ ( K @ ( J @ line_connecting ) @ convergent_lines ) )
| ~ ( I @ ( H @ line_connecting ) @ ( G @ ( F @ line_connecting ) @ convergent_lines ) )
| ~ ( E @ ( D @ line_connecting ) @ ( C @ ( B @ line_connecting ) @ convergent_lines ) )
| ~ ( C @ ( B @ distinct_points ) )
| ~ ( C @ point )
| ~ ( B @ point )
| ~ ( E @ ( D @ distinct_points ) )
| ~ ( E @ point )
| ~ ( D @ point )
| ~ ( G @ ( F @ distinct_points ) )
| ~ ( G @ point )
| ~ ( F @ point )
| ~ ( I @ ( H @ distinct_points ) )
| ~ ( I @ point )
| ~ ( H @ point )
| ~ ( K @ ( J @ distinct_points ) )
| ~ ( K @ point )
| ~ ( J @ point )
| ~ ( M @ ( L @ distinct_points ) )
| ~ ( M @ point )
| ~ ( L @ point )
| ~ ( O @ ( N @ distinct_points ) )
| ~ ( O @ point )
| ~ ( N @ point ) ),
inference(pattern_uni,[status(thm)],[11998:[bind(A,$thf( Q )),bind(B,$thf( R )),bind(C,$thf( R @ ( Q @ line_connecting ) ))]]) ).
thf(12133,plain,
! [O: $i,N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( M @ ( L @ line_connecting ) @ ( K @ ( J @ line_connecting ) @ intersection_point ) @ ( A @ ( O @ ( N @ line_connecting ) @ intersection_point ) @ line_connecting ) )
!= sk1 )
| ( ( E @ ( D @ line_connecting ) @ ( C @ ( B @ line_connecting ) @ intersection_point ) @ ( I @ ( H @ line_connecting ) @ ( G @ ( F @ line_connecting ) @ intersection_point ) @ line_connecting ) )
!= sk3 )
| ~ ( E @ ( D @ line_connecting ) @ ( C @ ( B @ line_connecting ) @ intersection_point ) @ ( I @ ( H @ line_connecting ) @ ( G @ ( F @ line_connecting ) @ intersection_point ) @ distinct_points ) )
| ~ ( M @ ( L @ line_connecting ) @ ( K @ ( J @ line_connecting ) @ intersection_point ) @ ( A @ ( O @ ( N @ line_connecting ) @ intersection_point ) @ distinct_points ) )
| ( sk3 @ ( sk1 @ intersection_point ) @ point )
| ~ ( A @ ( O @ ( N @ line_connecting ) @ convergent_lines ) )
| ~ ( A @ line )
| ~ ( M @ ( L @ line_connecting ) @ ( K @ ( J @ line_connecting ) @ convergent_lines ) )
| ~ ( I @ ( H @ line_connecting ) @ ( G @ ( F @ line_connecting ) @ convergent_lines ) )
| ~ ( E @ ( D @ line_connecting ) @ ( C @ ( B @ line_connecting ) @ convergent_lines ) )
| ~ ( C @ ( B @ distinct_points ) )
| ~ ( C @ point )
| ~ ( B @ point )
| ~ ( E @ ( D @ distinct_points ) )
| ~ ( E @ point )
| ~ ( D @ point )
| ~ ( G @ ( F @ distinct_points ) )
| ~ ( G @ point )
| ~ ( F @ point )
| ~ ( I @ ( H @ distinct_points ) )
| ~ ( I @ point )
| ~ ( H @ point )
| ~ ( K @ ( J @ distinct_points ) )
| ~ ( K @ point )
| ~ ( J @ point )
| ~ ( M @ ( L @ distinct_points ) )
| ~ ( M @ point )
| ~ ( L @ point )
| ~ ( O @ ( N @ distinct_points ) )
| ~ ( O @ point )
| ~ ( N @ point ) ),
inference(simp,[status(thm)],[11999]) ).
thf(12,axiom,
! [A: $i,B: $i] :
( ( ( B @ point )
& ( A @ line ) )
=> ( B @ ( A @ orthogonal_through_point ) @ line ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',orth1) ).
thf(73,plain,
! [A: $i,B: $i] :
( ( ( B @ point )
& ( A @ line ) )
=> ( B @ ( A @ orthogonal_through_point ) @ line ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(74,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ orthogonal_through_point ) @ line )
| ~ ( B @ point )
| ~ ( A @ line ) ),
inference(cnf,[status(esa)],[73]) ).
thf(303,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ~ $true
| ( ( D @ ( C @ unorthogonal_lines ) )
!= ( D @ ( B @ unorthogonal_lines ) ) )
| ( D @ ( B @ unorthogonal_lines ) )
| ( C @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( C @ ( B @ distinct_lines ) ) ),
inference(eqfactor_ordered,[status(thm)],[60]) ).
thf(304,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ unorthogonal_lines ) )
| ( B @ ( A @ apart_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( B @ ( B @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[303:[bind(A,$thf( A )),bind(B,$thf( C ))]]) ).
thf(307,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)],[304]) ).
thf(2009,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ( B @ ( A @ intersection_point ) @ point )
| ~ $true
| ~ ( B @ line )
| ~ ( A @ line ) ),
inference(paramod_ordered,[status(thm)],[1998,98]) ).
thf(2010,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ( B @ ( A @ intersection_point ) @ point )
| ~ ( B @ line )
| ~ ( A @ line ) ),
inference(simp,[status(thm)],[2009]) ).
thf(2011,plain,
( ( sk1 @ ( sk2 @ intersection_point ) @ point )
| ~ ( sk1 @ line )
| ~ ( sk2 @ line ) ),
inference(pattern_uni,[status(thm)],[2010:[bind(A,$thf( sk2 )),bind(B,$thf( sk1 ))]]) ).
thf(833,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ distinct_points ) )
!= ( 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 ) )
| ~ ( D @ ( C @ distinct_lines ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[42,88]) ).
thf(834,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ distinct_points ) )
!= ( 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 ) )
| ~ ( D @ ( C @ distinct_lines ) ) ),
inference(simp,[status(thm)],[833]) ).
thf(835,plain,
! [B: $i,A: $i] :
( ( B @ ( sk3 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) )
| ( A @ ( sk3 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) )
| ( B @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) )
| ( A @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) )
| ~ ( B @ ( A @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[834:[bind(A,$thf( sk2 @ ( sk1 @ intersection_point ) )),bind(B,$thf( sk3 @ ( sk1 @ intersection_point ) )),bind(C,$thf( C )),bind(D,$thf( D ))]]) ).
thf(925,plain,
! [B: $i,A: $i] :
( ( B @ ( sk3 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) )
| ( A @ ( sk3 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) )
| ( B @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) )
| ( A @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) )
| ~ ( B @ ( A @ distinct_lines ) ) ),
inference(simp,[status(thm)],[835]) ).
thf(2771,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,144]) ).
thf(2772,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)],[2771]) ).
thf(2773,plain,
~ ( sk1 @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[2772:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(218,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)],[101,55]) ).
thf(219,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)],[218]) ).
thf(220,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ orthogonal_lines ) )
| ( B @ ( A @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[219:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(361,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ parallel_through_point ) @ convergent_lines ) )
!= ( sk1 @ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ convergent_lines ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[355,117]) ).
thf(362,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( B @ parallel_through_point ) @ convergent_lines ) )
!= ( sk1 @ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ convergent_lines ) ) ),
inference(simp,[status(thm)],[361]) ).
thf(364,plain,
! [B: $i,A: $i] :
( ( B != sk1 )
| ( ( A @ ( B @ parallel_through_point ) )
!= ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) ) ) ),
inference(simp,[status(thm)],[362]) ).
thf(366,plain,
! [A: $i] :
( ( A @ ( sk1 @ parallel_through_point ) )
!= ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) ) ),
inference(simp,[status(thm)],[364]) ).
thf(2242,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ parallel_through_point ) @ ( sk1 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( C @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2130,142]) ).
thf(2243,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ parallel_through_point ) @ ( sk1 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( C @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[2242]) ).
thf(2244,plain,
! [A: $i] :
~ ( A @ ( sk2 @ parallel_through_point ) @ ( A @ ( sk2 @ parallel_through_point ) @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[2243:[bind(A,$thf( E )),bind(B,$thf( sk1 )),bind(C,$thf( E @ ( sk2 @ parallel_through_point ) ))]]) ).
thf(2264,plain,
! [A: $i] :
~ ( A @ ( sk2 @ parallel_through_point ) @ ( A @ ( sk2 @ parallel_through_point ) @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ),
inference(simp,[status(thm)],[2244]) ).
thf(596,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( D @ distinct_lines ) ) )
| ( D @ ( C @ convergent_lines ) )
| ~ $true
| ( A @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[450,453]) ).
thf(597,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( D @ distinct_lines ) ) )
| ( D @ ( C @ convergent_lines ) )
| ( A @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[596]) ).
thf(598,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ convergent_lines ) )
| ( A @ ( A @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[597:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(11,axiom,
! [A: $i,B: $i] :
~ ( A @ ( B @ parallel_through_point ) @ ( A @ apart_point_and_line ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cp2) ).
thf(70,plain,
! [A: $i,B: $i] :
~ ( A @ ( B @ parallel_through_point ) @ ( A @ apart_point_and_line ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(3987,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk1 @ distinct_lines ) )
!= ( B @ ( C @ distinct_lines ) ) )
| ( C @ ( B @ distinct_lines ) )
| ~ $true
| ( A @ ( sk2 @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[3890,415]) ).
thf(3988,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk1 @ distinct_lines ) )
!= ( B @ ( C @ distinct_lines ) ) )
| ( C @ ( B @ distinct_lines ) )
| ( A @ ( sk2 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[3987]) ).
thf(3989,plain,
! [A: $i] :
( ( sk1 @ ( A @ distinct_lines ) )
| ( A @ ( sk2 @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[3988:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk1 ))]]) ).
thf(160,plain,
! [A: $i] :
( ( ( sk2 @ ( sk1 @ convergent_lines ) )
!= ( A @ ( A @ convergent_lines ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[40,106]) ).
thf(161,plain,
! [A: $i] :
( ( sk2 @ ( sk1 @ convergent_lines ) )
!= ( A @ ( A @ convergent_lines ) ) ),
inference(simp,[status(thm)],[160]) ).
thf(163,plain,
! [A: $i] :
( ( sk2 != A )
| ( sk1 != A ) ),
inference(simp,[status(thm)],[161]) ).
thf(165,plain,
sk2 != sk1,
inference(simp,[status(thm)],[163]) ).
thf(16566,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ convergent_lines ) )
!= ( C @ ( B @ ( C @ parallel_through_point ) @ convergent_lines ) ) )
| ~ $true
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[6396,117]) ).
thf(16567,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( A @ convergent_lines ) )
!= ( C @ ( B @ ( C @ parallel_through_point ) @ convergent_lines ) ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[16566]) ).
thf(16568,plain,
! [A: $i] : ( A @ ( sk3 @ parallel_through_point ) @ ( sk1 @ convergent_lines ) ),
inference(pattern_uni,[status(thm)],[16567:[bind(A,$thf( E @ ( sk3 @ parallel_through_point ) )),bind(B,$thf( E )),bind(C,$thf( sk3 ))]]) ).
thf(16781,plain,
! [A: $i] : ( A @ ( sk3 @ parallel_through_point ) @ ( sk1 @ convergent_lines ) ),
inference(simp,[status(thm)],[16568]) ).
thf(16881,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk3 @ parallel_through_point ) @ ( sk1 @ convergent_lines ) )
!= ( C @ ( B @ ( C @ parallel_through_point ) @ convergent_lines ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[16781,117]) ).
thf(16882,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( sk3 @ parallel_through_point ) @ ( sk1 @ convergent_lines ) )
!= ( C @ ( B @ ( C @ parallel_through_point ) @ convergent_lines ) ) ),
inference(simp,[status(thm)],[16881]) ).
thf(16938,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk3 @ parallel_through_point ) )
!= C )
| ( ( B @ ( C @ parallel_through_point ) )
!= sk1 ) ),
inference(simp,[status(thm)],[16882]) ).
thf(16973,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( sk3 @ parallel_through_point ) @ parallel_through_point ) )
!= sk1 ),
inference(simp,[status(thm)],[16938]) ).
thf(13397,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk1 @ ( A @ ( sk3 @ orthogonal_through_point ) @ unorthogonal_lines ) )
!= ( C @ ( B @ ( C @ orthogonal_through_point ) @ unorthogonal_lines ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[13391,46]) ).
thf(13398,plain,
! [C: $i,B: $i,A: $i] :
( ( sk1 @ ( A @ ( sk3 @ orthogonal_through_point ) @ unorthogonal_lines ) )
!= ( C @ ( B @ ( C @ orthogonal_through_point ) @ unorthogonal_lines ) ) ),
inference(simp,[status(thm)],[13397]) ).
thf(13417,plain,
! [C: $i,B: $i,A: $i] :
( ( sk1 != C )
| ( ( A @ ( sk3 @ orthogonal_through_point ) )
!= ( B @ ( C @ orthogonal_through_point ) ) ) ),
inference(simp,[status(thm)],[13398]) ).
thf(13423,plain,
! [B: $i,A: $i] :
( ( A @ ( sk3 @ orthogonal_through_point ) )
!= ( B @ ( sk1 @ orthogonal_through_point ) ) ),
inference(simp,[status(thm)],[13417]) ).
thf(273,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)],[60,78]) ).
thf(274,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)],[273]) ).
thf(275,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)],[274:[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(2756,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ ( A @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[971,144]) ).
thf(2757,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ ( A @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[2756]) ).
thf(2758,plain,
~ ( sk1 @ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[2757:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) ))]]) ).
thf(2198,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( C @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) )
| ~ $true
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1941,142]) ).
thf(2199,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk2 @ ( A @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( C @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[2198]) ).
thf(2200,plain,
! [A: $i] :
( ~ ( sk2 @ ( sk2 @ ( A @ intersection_point ) @ apart_point_and_line ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[2199:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk2 ))]]) ).
thf(1157,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk3 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ $true
| ~ ( C @ ( B @ parallel_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1136,110]) ).
thf(1158,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk3 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( C @ ( B @ parallel_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[1157]) ).
thf(1159,plain,
! [A: $i] :
( ~ ( A @ ( sk3 @ parallel_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[1158:[bind(A,$thf( A )),bind(B,$thf( sk3 )),bind(C,$thf( A ))]]) ).
thf(238,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ distinct_lines ) )
!= ( E @ ( D @ distinct_lines ) ) )
| ~ $true
| ~ ( E @ ( D @ equal_lines ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[49,135]) ).
thf(239,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ distinct_lines ) )
!= ( E @ ( D @ distinct_lines ) ) )
| ~ ( E @ ( D @ equal_lines ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[238]) ).
thf(240,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ equal_lines ) )
| ( C @ ( A @ apart_point_and_line ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[239:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( B )),bind(E,$thf( C ))]]) ).
thf(13864,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 @ equal_lines ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[240,2773]) ).
thf(13865,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( sk1 @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) )
| ~ ( C @ ( B @ equal_lines ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[13864]) ).
thf(13866,plain,
! [A: $i] :
( ~ ( sk1 @ ( A @ equal_lines ) )
| ~ ( A @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[13865:[bind(A,$thf( sk2 @ ( sk1 @ intersection_point ) )),bind(B,$thf( B )),bind(C,$thf( sk1 ))]]) ).
thf(14011,plain,
! [A: $i] :
( ~ ( sk1 @ ( A @ equal_lines ) )
| ~ ( A @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[13866]) ).
thf(13930,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( sk1 @ ( sk1 @ ( sk2 @ intersection_point ) @ apart_point_and_line ) ) )
| ~ $true
| ~ ( C @ ( B @ equal_lines ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[240,2212]) ).
thf(13931,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( sk1 @ ( sk1 @ ( sk2 @ intersection_point ) @ apart_point_and_line ) ) )
| ~ ( C @ ( B @ equal_lines ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[13930]) ).
thf(13932,plain,
! [A: $i] :
( ~ ( sk1 @ ( A @ equal_lines ) )
| ~ ( A @ ( sk1 @ ( sk2 @ intersection_point ) @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[13931:[bind(A,$thf( sk1 @ ( sk2 @ intersection_point ) )),bind(B,$thf( B )),bind(C,$thf( sk1 ))]]) ).
thf(14028,plain,
! [A: $i] :
( ~ ( sk1 @ ( A @ equal_lines ) )
| ~ ( A @ ( sk1 @ ( sk2 @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[13932]) ).
thf(1538,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,98]) ).
thf(1539,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)],[1538]) ).
thf(1540,plain,
( ( sk2 @ ( sk1 @ intersection_point ) @ point )
| ~ ( sk2 @ line )
| ~ ( sk1 @ line ) ),
inference(pattern_uni,[status(thm)],[1539:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(166,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ distinct_points ) )
!= ( A @ ( A @ distinct_points ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[42,157]) ).
thf(167,plain,
! [A: $i] :
( ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ distinct_points ) )
!= ( A @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[166]) ).
thf(168,plain,
! [A: $i] :
( ( ( sk3 @ ( sk1 @ intersection_point ) )
!= A )
| ( ( sk2 @ ( sk1 @ intersection_point ) )
!= A ) ),
inference(simp,[status(thm)],[167]) ).
thf(169,plain,
( ( sk3 @ ( sk1 @ intersection_point ) )
!= ( sk2 @ ( sk1 @ intersection_point ) ) ),
inference(simp,[status(thm)],[168]) ).
thf(2681,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)],[41,144]) ).
thf(2682,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)],[2681]) ).
thf(2683,plain,
~ ( sk1 @ ( sk3 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[2682:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 ))]]) ).
thf(13963,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( sk1 @ ( sk3 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) )
| ~ $true
| ~ ( C @ ( B @ equal_lines ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[240,2683]) ).
thf(13964,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( sk1 @ ( sk3 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) )
| ~ ( C @ ( B @ equal_lines ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[13963]) ).
thf(13965,plain,
! [A: $i] :
( ~ ( sk1 @ ( A @ equal_lines ) )
| ~ ( A @ ( sk3 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[13964:[bind(A,$thf( sk3 @ ( sk1 @ intersection_point ) )),bind(B,$thf( B )),bind(C,$thf( sk1 ))]]) ).
thf(13996,plain,
! [A: $i] :
( ~ ( sk1 @ ( A @ equal_lines ) )
| ~ ( A @ ( sk3 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[13965]) ).
thf(325,plain,
! [A: $i] :
( ( ( A @ ( A @ equal_lines ) )
!= ( sk1 @ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ equal_lines ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[320,43]) ).
thf(326,plain,
! [A: $i] :
( ( A @ ( A @ equal_lines ) )
!= ( sk1 @ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ equal_lines ) ) ),
inference(simp,[status(thm)],[325]) ).
thf(327,plain,
! [A: $i] :
( ( A != sk1 )
| ( A
!= ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) ) ) ),
inference(simp,[status(thm)],[326]) ).
thf(328,plain,
( ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) )
!= sk1 ),
inference(simp,[status(thm)],[327]) ).
thf(16832,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk3 @ parallel_through_point ) @ ( sk1 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( C @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[16781,142]) ).
thf(16833,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk3 @ parallel_through_point ) @ ( sk1 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( C @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[16832]) ).
thf(16834,plain,
! [A: $i] :
~ ( A @ ( sk3 @ parallel_through_point ) @ ( A @ ( sk3 @ parallel_through_point ) @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[16833:[bind(A,$thf( E )),bind(B,$thf( sk1 )),bind(C,$thf( E @ ( sk3 @ parallel_through_point ) ))]]) ).
thf(16986,plain,
! [A: $i] :
~ ( A @ ( sk3 @ parallel_through_point ) @ ( A @ ( sk3 @ parallel_through_point ) @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ),
inference(simp,[status(thm)],[16834]) ).
thf(5,axiom,
! [A: $i,B: $i] :
( ( ( B @ point )
& ( A @ line ) )
=> ( B @ ( A @ parallel_through_point ) @ line ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',par1) ).
thf(50,plain,
! [A: $i,B: $i] :
( ( ( B @ point )
& ( A @ line ) )
=> ( B @ ( A @ parallel_through_point ) @ line ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(51,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ parallel_through_point ) @ line )
| ~ ( B @ point )
| ~ ( A @ line ) ),
inference(cnf,[status(esa)],[50]) ).
thf(222,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ parallel_through_point ) @ line )
!= ( C @ line ) )
| ( D @ ( C @ parallel_through_point ) @ line )
| ~ ( D @ point )
| ~ $true
| ~ ( B @ point )
| ~ ( A @ line ) ),
inference(paramod_ordered,[status(thm)],[51,51]) ).
thf(223,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ parallel_through_point ) @ line )
!= ( C @ line ) )
| ( D @ ( C @ parallel_through_point ) @ line )
| ~ ( D @ point )
| ~ ( B @ point )
| ~ ( A @ line ) ),
inference(simp,[status(thm)],[222]) ).
thf(224,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ ( B @ parallel_through_point ) @ parallel_through_point ) @ line )
| ~ ( A @ point )
| ~ ( C @ point )
| ~ ( B @ line ) ),
inference(pattern_uni,[status(thm)],[223:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F @ ( E @ parallel_through_point ) ))]]) ).
thf(225,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ ( B @ parallel_through_point ) @ parallel_through_point ) @ line )
| ~ ( A @ point )
| ~ ( C @ point )
| ~ ( B @ line ) ),
inference(simp,[status(thm)],[224]) ).
thf(535,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( D @ ( C @ distinct_lines ) ) )
| ( D @ ( C @ convergent_lines ) )
| ~ $true
| ( A @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[450,148]) ).
thf(536,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( D @ ( C @ distinct_lines ) ) )
| ( D @ ( C @ convergent_lines ) )
| ( A @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[535]) ).
thf(537,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ convergent_lines ) )
| ( A @ ( A @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[536:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(13188,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ distinct_lines ) )
!= ( D @ ( E @ distinct_lines ) ) )
| ~ ( D @ ( E @ equal_lines ) )
| ~ $true
| ~ ( C @ ( A @ incident_point_and_line ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[196,534]) ).
thf(13189,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( ( C @ ( B @ distinct_lines ) )
!= ( D @ ( E @ distinct_lines ) ) )
| ~ ( D @ ( E @ equal_lines ) )
| ~ ( C @ ( A @ incident_point_and_line ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[13188]) ).
thf(13190,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ equal_lines ) )
| ~ ( C @ ( A @ incident_point_and_line ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[13189:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( C )),bind(E,$thf( B ))]]) ).
thf(1145,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ convergent_lines ) )
!= ( C @ ( B @ ( C @ parallel_through_point ) @ convergent_lines ) ) )
| ~ $true
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1128,117]) ).
thf(1146,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ convergent_lines ) )
!= ( C @ ( B @ ( C @ parallel_through_point ) @ convergent_lines ) ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[1145]) ).
thf(1153,plain,
! [C: $i,B: $i,A: $i] :
( ( A != C )
| ( ( B @ ( C @ parallel_through_point ) )
!= sk2 )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[1146]) ).
thf(1155,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ parallel_through_point ) )
!= sk2 )
| ( B @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[1153]) ).
thf(2705,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)],[221,144]) ).
thf(2706,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)],[2705]) ).
thf(2707,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)],[2706:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F @ ( E @ orthogonal_through_point ) )),bind(D,$thf( E ))]]) ).
thf(2781,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)],[2707]) ).
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/sandbox/benchmark/theBenchmark.p',oac1) ).
thf(123,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(124,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)],[123]) ).
thf(125,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)],[124]) ).
thf(129,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)],[125]) ).
thf(2201,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ ( B @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[971,142]) ).
thf(2202,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ ( B @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[2201]) ).
thf(2203,plain,
~ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[2202:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) ))]]) ).
thf(203,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ $true
| ~ ( B @ ( A @ parallel_lines ) ) ),
inference(paramod_ordered,[status(thm)],[41,110]) ).
thf(204,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ ( B @ ( A @ parallel_lines ) ) ),
inference(simp,[status(thm)],[203]) ).
thf(205,plain,
~ ( sk3 @ ( sk1 @ parallel_lines ) ),
inference(pattern_uni,[status(thm)],[204:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 ))]]) ).
thf(556,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( D @ distinct_lines ) ) )
| ( D @ ( C @ distinct_lines ) )
| ~ $true
| ( A @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[450,415]) ).
thf(557,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( D @ distinct_lines ) ) )
| ( D @ ( C @ distinct_lines ) )
| ( A @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[556]) ).
thf(558,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ distinct_lines ) )
| ( A @ ( A @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[557:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(529,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( D @ distinct_lines ) ) )
| ~ ( D @ ( C @ equal_lines ) )
| ~ $true
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[414,474]) ).
thf(530,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( D @ distinct_lines ) ) )
| ~ ( D @ ( C @ equal_lines ) )
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(simp,[status(thm)],[529]) ).
thf(531,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ equal_lines ) )
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[530:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(951,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ equal_lines ) )
!= ( C @ ( D @ equal_lines ) ) )
| ~ $true
| ~ ( C @ ( C @ distinct_lines ) )
| ~ ( A @ ( B @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[519,531]) ).
thf(952,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ equal_lines ) )
!= ( C @ ( D @ equal_lines ) ) )
| ~ ( C @ ( C @ distinct_lines ) )
| ~ ( A @ ( B @ equal_lines ) ) ),
inference(simp,[status(thm)],[951]) ).
thf(953,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( B @ distinct_lines ) )
| ~ ( A @ ( B @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[952:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(128,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)],[125]) ).
thf(231,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)],[221,106]) ).
thf(232,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( B @ ( A @ orthogonal_through_point ) @ convergent_lines ) )
!= ( C @ ( C @ convergent_lines ) ) ),
inference(simp,[status(thm)],[231]) ).
thf(234,plain,
! [C: $i,B: $i,A: $i] :
( ( A != C )
| ( ( B @ ( A @ orthogonal_through_point ) )
!= C ) ),
inference(simp,[status(thm)],[232]) ).
thf(237,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ orthogonal_through_point ) )
!= A ),
inference(simp,[status(thm)],[234]) ).
thf(1958,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ convergent_lines ) )
!= ( D @ ( C @ ( D @ parallel_through_point ) @ convergent_lines ) ) )
| ~ $true
| ( B @ ( sk2 @ convergent_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1156,117]) ).
thf(1959,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ convergent_lines ) )
!= ( D @ ( C @ ( D @ parallel_through_point ) @ convergent_lines ) ) )
| ( B @ ( sk2 @ convergent_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[1958]) ).
thf(1960,plain,
! [B: $i,A: $i] :
( ( A @ ( sk2 @ convergent_lines ) )
| ( B @ ( A @ parallel_through_point ) @ ( sk1 @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[1959:[bind(A,$thf( F @ ( B @ parallel_through_point ) )),bind(B,$thf( B )),bind(C,$thf( F )),bind(D,$thf( B ))]]) ).
thf(1991,plain,
! [B: $i,A: $i] :
( ( A @ ( sk2 @ convergent_lines ) )
| ( B @ ( A @ parallel_through_point ) @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[1960]) ).
thf(2132,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)],[41,142]) ).
thf(2133,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)],[2132]) ).
thf(2134,plain,
~ ( sk3 @ ( sk3 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[2133:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 ))]]) ).
thf(2233,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ apart_point_and_line ) )
!= ( sk3 @ ( sk3 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) )
| ~ $true
| ( C @ ( A @ distinct_points ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[120,2134]) ).
thf(2234,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( C @ apart_point_and_line ) )
!= ( sk3 @ ( sk3 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) )
| ( C @ ( A @ distinct_points ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[2233]) ).
thf(2235,plain,
! [A: $i] :
( ( sk3 @ ( sk1 @ intersection_point ) @ ( A @ distinct_points ) )
| ~ ( sk3 @ ( A @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[2234:[bind(A,$thf( A )),bind(B,$thf( sk3 )),bind(C,$thf( sk3 @ ( sk1 @ intersection_point ) ))]]) ).
thf(296,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)],[60,55]) ).
thf(297,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)],[296]) ).
thf(298,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)],[297:[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(1999,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ $true
| ~ ( B @ ( A @ parallel_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1998,110]) ).
thf(2000,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ ( B @ ( A @ parallel_lines ) ) ),
inference(simp,[status(thm)],[1999]) ).
thf(2001,plain,
~ ( sk1 @ ( sk2 @ parallel_lines ) ),
inference(pattern_uni,[status(thm)],[2000:[bind(A,$thf( sk2 )),bind(B,$thf( sk1 ))]]) ).
thf(9968,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk1 @ parallel_through_point ) @ ( sk2 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( B @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9871,144]) ).
thf(9969,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk1 @ parallel_through_point ) @ ( sk2 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( B @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[9968]) ).
thf(9970,plain,
! [A: $i] :
~ ( sk2 @ ( A @ ( sk1 @ parallel_through_point ) @ ( sk2 @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[9969:[bind(A,$thf( E )),bind(B,$thf( sk2 )),bind(C,$thf( E @ ( sk1 @ parallel_through_point ) ))]]) ).
thf(10030,plain,
! [A: $i] :
~ ( sk2 @ ( A @ ( sk1 @ parallel_through_point ) @ ( sk2 @ intersection_point ) @ apart_point_and_line ) ),
inference(simp,[status(thm)],[9970]) ).
thf(599,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( D @ distinct_lines ) ) )
| ( D @ ( C @ convergent_lines ) )
| ~ $true
| ( B @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[137,453]) ).
thf(600,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( D @ distinct_lines ) ) )
| ( D @ ( C @ convergent_lines ) )
| ( B @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[599]) ).
thf(601,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ convergent_lines ) )
| ( B @ ( A @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[600:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(570,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ convergent_lines ) )
!= ( D @ ( C @ convergent_lines ) ) )
| ~ $true
| ~ ( D @ ( C @ parallel_lines ) )
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[421,110]) ).
thf(571,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ convergent_lines ) )
!= ( D @ ( C @ convergent_lines ) ) )
| ~ ( D @ ( C @ parallel_lines ) )
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(simp,[status(thm)],[570]) ).
thf(572,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ parallel_lines ) )
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[571:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(226,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)],[221,117]) ).
thf(227,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)],[226]) ).
thf(233,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)],[227]) ).
thf(236,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( C @ orthogonal_through_point ) )
!= ( B @ ( C @ parallel_through_point ) ) ),
inference(simp,[status(thm)],[233]) ).
thf(2768,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ ( A @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1998,144]) ).
thf(2769,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk2 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ ( A @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[2768]) ).
thf(2770,plain,
~ ( sk2 @ ( sk1 @ ( sk2 @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[2769:[bind(A,$thf( sk2 )),bind(B,$thf( sk1 ))]]) ).
thf(13927,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( sk2 @ ( sk1 @ ( sk2 @ intersection_point ) @ apart_point_and_line ) ) )
| ~ $true
| ~ ( C @ ( B @ equal_lines ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[240,2770]) ).
thf(13928,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( sk2 @ ( sk1 @ ( sk2 @ intersection_point ) @ apart_point_and_line ) ) )
| ~ ( C @ ( B @ equal_lines ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[13927]) ).
thf(13929,plain,
! [A: $i] :
( ~ ( sk2 @ ( A @ equal_lines ) )
| ~ ( A @ ( sk1 @ ( sk2 @ intersection_point ) @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[13928:[bind(A,$thf( sk1 @ ( sk2 @ intersection_point ) )),bind(B,$thf( B )),bind(C,$thf( sk2 ))]]) ).
thf(14027,plain,
! [A: $i] :
( ~ ( sk2 @ ( A @ equal_lines ) )
| ~ ( A @ ( sk1 @ ( sk2 @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[13929]) ).
thf(85,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ equal_points ) )
| ( B @ ( A @ distinct_points ) ) ),
inference(cnfConj,[status(thm)],[83]) ).
thf(86,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ equal_points ) )
| ( B @ ( A @ distinct_points ) ) ),
inference(simp,[status(thm)],[85]) ).
thf(24,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ distinct_points ) )
=> ~ ( B @ ( A @ line_connecting ) @ ( B @ apart_point_and_line ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ci2) ).
thf(113,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)],[24]) ).
thf(991,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ ( B @ parallel_through_point ) @ convergent_lines ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[971,117]) ).
thf(992,plain,
! [B: $i,A: $i] :
( ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ ( B @ parallel_through_point ) @ convergent_lines ) ) ),
inference(simp,[status(thm)],[991]) ).
thf(994,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) )
!= B )
| ( ( A @ ( B @ parallel_through_point ) )
!= sk1 ) ),
inference(simp,[status(thm)],[992]) ).
thf(996,plain,
! [A: $i] :
( ( A @ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ parallel_through_point ) )
!= sk1 ),
inference(simp,[status(thm)],[994]) ).
thf(9914,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk1 @ parallel_through_point ) @ ( sk2 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( C @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9871,142]) ).
thf(9915,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk1 @ parallel_through_point ) @ ( sk2 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( C @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[9914]) ).
thf(9916,plain,
! [A: $i] :
~ ( A @ ( sk1 @ parallel_through_point ) @ ( A @ ( sk1 @ parallel_through_point ) @ ( sk2 @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[9915:[bind(A,$thf( E )),bind(B,$thf( sk2 )),bind(C,$thf( E @ ( sk1 @ parallel_through_point ) ))]]) ).
thf(10037,plain,
! [A: $i] :
~ ( A @ ( sk1 @ parallel_through_point ) @ ( A @ ( sk1 @ parallel_through_point ) @ ( sk2 @ intersection_point ) @ apart_point_and_line ) ),
inference(simp,[status(thm)],[9916]) ).
thf(206,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ $true
| ~ ( B @ ( A @ parallel_lines ) ) ),
inference(paramod_ordered,[status(thm)],[40,110]) ).
thf(207,plain,
! [B: $i,A: $i] :
( ( ( sk2 @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ ( B @ ( A @ parallel_lines ) ) ),
inference(simp,[status(thm)],[206]) ).
thf(208,plain,
~ ( sk2 @ ( sk1 @ parallel_lines ) ),
inference(pattern_uni,[status(thm)],[207:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(614,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( D @ distinct_lines ) ) )
| ( D @ ( C @ convergent_lines ) )
| ~ $true
| ~ ( A @ ( B @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[415,453]) ).
thf(615,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( D @ distinct_lines ) ) )
| ( D @ ( C @ convergent_lines ) )
| ~ ( A @ ( B @ distinct_lines ) ) ),
inference(simp,[status(thm)],[614]) ).
thf(616,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ convergent_lines ) )
| ~ ( A @ ( B @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[615:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(2106,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk1 @ convergent_lines ) )
!= ( C @ ( B @ ( C @ parallel_through_point ) @ convergent_lines ) ) )
| ~ $true
| ( sk2 @ ( A @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1941,117]) ).
thf(2107,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk1 @ convergent_lines ) )
!= ( C @ ( B @ ( C @ parallel_through_point ) @ convergent_lines ) ) )
| ( sk2 @ ( A @ convergent_lines ) ) ),
inference(simp,[status(thm)],[2106]) ).
thf(2124,plain,
! [C: $i,B: $i,A: $i] :
( ( A != C )
| ( ( B @ ( C @ parallel_through_point ) )
!= sk1 )
| ( sk2 @ ( A @ convergent_lines ) ) ),
inference(simp,[status(thm)],[2107]) ).
thf(2129,plain,
! [B: $i,A: $i] :
( ( ( A @ ( B @ parallel_through_point ) )
!= sk1 )
| ( sk2 @ ( B @ convergent_lines ) ) ),
inference(simp,[status(thm)],[2124]) ).
thf(2245,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ parallel_through_point ) @ ( sk1 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ $true
| ~ ( C @ ( B @ parallel_lines ) ) ),
inference(paramod_ordered,[status(thm)],[2130,110]) ).
thf(2246,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ parallel_through_point ) @ ( sk1 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( C @ ( B @ parallel_lines ) ) ),
inference(simp,[status(thm)],[2245]) ).
thf(2247,plain,
! [A: $i] :
~ ( A @ ( sk2 @ parallel_through_point ) @ ( sk1 @ parallel_lines ) ),
inference(pattern_uni,[status(thm)],[2246:[bind(A,$thf( E )),bind(B,$thf( sk1 )),bind(C,$thf( E @ ( sk2 @ parallel_through_point ) ))]]) ).
thf(2267,plain,
! [A: $i] :
~ ( A @ ( sk2 @ parallel_through_point ) @ ( sk1 @ parallel_lines ) ),
inference(simp,[status(thm)],[2247]) ).
thf(29,axiom,
! [A: $i,B: $i] :
( ( B @ ( A @ unorthogonal_lines ) )
| ( B @ ( A @ convergent_lines ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',occu1) ).
thf(130,plain,
! [A: $i,B: $i] :
( ( B @ ( A @ unorthogonal_lines ) )
| ( B @ ( A @ convergent_lines ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(276,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)],[60,78]) ).
thf(277,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)],[276]) ).
thf(278,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)],[277:[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(286,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 @ ( C @ unorthogonal_lines ) )
| ( D @ ( B @ unorthogonal_lines ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( C @ ( B @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[60,49]) ).
thf(287,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 @ ( C @ unorthogonal_lines ) )
| ( D @ ( B @ unorthogonal_lines ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( C @ ( B @ distinct_lines ) ) ),
inference(simp,[status(thm)],[286]) ).
thf(288,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( A @ apart_point_and_line ) )
| ( E @ ( C @ distinct_lines ) )
| ( D @ ( C @ unorthogonal_lines ) )
| ( D @ ( B @ unorthogonal_lines ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( C @ ( B @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[287:[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(306,plain,
! [E: $i,D: $i,C: $i,B: $i,A: $i] :
( ( E @ ( A @ apart_point_and_line ) )
| ( E @ ( C @ distinct_lines ) )
| ( D @ ( C @ unorthogonal_lines ) )
| ( D @ ( B @ unorthogonal_lines ) )
| ( B @ ( A @ apart_point_and_line ) )
| ~ ( C @ ( B @ distinct_lines ) ) ),
inference(simp,[status(thm)],[288]) ).
thf(2750,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk1 @ 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)],[1941,144]) ).
thf(2751,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk1 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( B @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) )
| ( sk2 @ ( A @ convergent_lines ) ) ),
inference(simp,[status(thm)],[2750]) ).
thf(2752,plain,
! [A: $i] :
( ~ ( sk1 @ ( A @ ( sk1 @ intersection_point ) @ apart_point_and_line ) )
| ( sk2 @ ( A @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[2751:[bind(A,$thf( A )),bind(B,$thf( sk1 )),bind(C,$thf( A ))]]) ).
thf(79,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ incident_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) ) ),
inference(cnfConj,[status(thm)],[77]) ).
thf(80,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ incident_point_and_line ) )
| ( B @ ( A @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[79]) ).
thf(111,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ parallel_lines ) )
| ( B @ ( A @ convergent_lines ) ) ),
inference(cnfConj,[status(thm)],[109]) ).
thf(112,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ parallel_lines ) )
| ( B @ ( A @ convergent_lines ) ) ),
inference(simp,[status(thm)],[111]) ).
thf(2372,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ parallel_through_point ) @ ( sk1 @ convergent_lines ) )
!= ( C @ ( C @ convergent_lines ) ) )
| ~ $true
| ( A @ ( sk2 @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1991,106]) ).
thf(2373,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ parallel_through_point ) @ ( sk1 @ convergent_lines ) )
!= ( C @ ( C @ convergent_lines ) ) )
| ( A @ ( sk2 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[2372]) ).
thf(2403,plain,
! [C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ parallel_through_point ) )
!= C )
| ( sk1 != C )
| ( A @ ( sk2 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[2373]) ).
thf(2407,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ parallel_through_point ) )
!= sk1 )
| ( A @ ( sk2 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[2403]) ).
thf(18,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/sandbox/benchmark/theBenchmark.p',cup1) ).
thf(95,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)],[18]) ).
thf(127,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)],[125]) ).
thf(2699,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ convergent_lines ) )
!= ( D @ ( C @ convergent_lines ) ) )
| ~ ( C @ ( D @ ( C @ intersection_point ) @ apart_point_and_line ) )
| ~ $true
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[421,144]) ).
thf(2700,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ convergent_lines ) )
!= ( D @ ( C @ convergent_lines ) ) )
| ~ ( C @ ( D @ ( C @ intersection_point ) @ apart_point_and_line ) )
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(simp,[status(thm)],[2699]) ).
thf(2701,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) )
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[2700:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(16835,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk3 @ parallel_through_point ) @ ( sk1 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ $true
| ~ ( C @ ( B @ parallel_lines ) ) ),
inference(paramod_ordered,[status(thm)],[16781,110]) ).
thf(16836,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk3 @ parallel_through_point ) @ ( sk1 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( C @ ( B @ parallel_lines ) ) ),
inference(simp,[status(thm)],[16835]) ).
thf(16837,plain,
! [A: $i] :
~ ( A @ ( sk3 @ parallel_through_point ) @ ( sk1 @ parallel_lines ) ),
inference(pattern_uni,[status(thm)],[16836:[bind(A,$thf( E )),bind(B,$thf( sk1 )),bind(C,$thf( E @ ( sk3 @ parallel_through_point ) ))]]) ).
thf(16987,plain,
! [A: $i] :
~ ( A @ ( sk3 @ parallel_through_point ) @ ( sk1 @ parallel_lines ) ),
inference(simp,[status(thm)],[16837]) ).
thf(1139,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)],[1128,110]) ).
thf(1140,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)],[1139]) ).
thf(1141,plain,
! [A: $i] :
( ~ ( A @ ( sk2 @ parallel_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[1140:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( A ))]]) ).
thf(71,plain,
~ ? [A: $i,B: $i] : ( A @ ( B @ parallel_through_point ) @ ( A @ apart_point_and_line ) ),
inference(miniscope,[status(thm)],[70]) ).
thf(72,plain,
! [B: $i,A: $i] :
~ ( A @ ( B @ parallel_through_point ) @ ( A @ apart_point_and_line ) ),
inference(cnf,[status(esa)],[71]) ).
thf(4817,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ distinct_lines ) )
!= ( B @ ( C @ distinct_lines ) ) )
| ~ ( B @ ( C @ equal_lines ) )
| ~ $true
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[3891,534]) ).
thf(4818,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ distinct_lines ) )
!= ( B @ ( C @ distinct_lines ) ) )
| ~ ( B @ ( C @ equal_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[4817]) ).
thf(4819,plain,
! [A: $i] :
( ~ ( A @ ( sk2 @ equal_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[4818:[bind(A,$thf( A )),bind(B,$thf( A )),bind(C,$thf( sk2 ))]]) ).
thf(2252,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ parallel_through_point ) @ ( sk1 @ convergent_lines ) )
!= ( C @ ( B @ ( C @ parallel_through_point ) @ convergent_lines ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2130,117]) ).
thf(2253,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( sk2 @ parallel_through_point ) @ ( sk1 @ convergent_lines ) )
!= ( C @ ( B @ ( C @ parallel_through_point ) @ convergent_lines ) ) ),
inference(simp,[status(thm)],[2252]) ).
thf(2261,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ parallel_through_point ) )
!= C )
| ( ( B @ ( C @ parallel_through_point ) )
!= sk1 ) ),
inference(simp,[status(thm)],[2253]) ).
thf(2266,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( sk2 @ parallel_through_point ) @ parallel_through_point ) )
!= sk1 ),
inference(simp,[status(thm)],[2261]) ).
thf(2213,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,142]) ).
thf(2214,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)],[2213]) ).
thf(2215,plain,
~ ( sk2 @ ( sk2 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[2214:[bind(A,$thf( sk1 )),bind(B,$thf( sk2 ))]]) ).
thf(1118,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ( C @ ( B @ convergent_lines ) )
| ( C @ ( A @ convergent_lines ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[971,91]) ).
thf(1119,plain,
! [C: $i,B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ ( sk1 @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ( C @ ( B @ convergent_lines ) )
| ( C @ ( A @ convergent_lines ) ) ),
inference(simp,[status(thm)],[1118]) ).
thf(1120,plain,
! [A: $i] :
( ( A @ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ convergent_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[1119:[bind(A,$thf( sk1 )),bind(B,$thf( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) )),bind(C,$thf( C ))]]) ).
thf(1126,plain,
! [A: $i] :
( ( A @ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ convergent_lines ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[1120]) ).
thf(170,plain,
( ( sk3 != sk2 )
| ( sk1 != sk1 ) ),
inference(simp,[status(thm)],[169]) ).
thf(171,plain,
sk3 != sk2,
inference(simp,[status(thm)],[170]) ).
thf(2762,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ convergent_lines ) )
!= ( D @ ( C @ convergent_lines ) ) )
| ~ ( C @ ( D @ ( C @ intersection_point ) @ apart_point_and_line ) )
| ~ $true
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[613,144]) ).
thf(2763,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ convergent_lines ) )
!= ( D @ ( C @ convergent_lines ) ) )
| ~ ( C @ ( D @ ( C @ intersection_point ) @ apart_point_and_line ) )
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(simp,[status(thm)],[2762]) ).
thf(2764,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ ( B @ intersection_point ) @ apart_point_and_line ) )
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[2763:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(2150,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ convergent_lines ) )
!= ( D @ ( C @ convergent_lines ) ) )
| ~ ( D @ ( D @ ( C @ intersection_point ) @ apart_point_and_line ) )
| ~ $true
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[421,142]) ).
thf(2151,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ convergent_lines ) )
!= ( D @ ( C @ convergent_lines ) ) )
| ~ ( D @ ( D @ ( C @ intersection_point ) @ apart_point_and_line ) )
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(simp,[status(thm)],[2150]) ).
thf(2152,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( B @ ( A @ intersection_point ) @ apart_point_and_line ) )
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[2151:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(114,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ line_connecting ) @ ( B @ apart_point_and_line ) )
| ~ ( B @ ( A @ distinct_points ) ) ),
inference(cnf,[status(esa)],[113]) ).
thf(13286,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ equal_lines ) )
!= ( D @ ( C @ equal_lines ) ) )
| ~ $true
| ~ ( D @ ( B @ incident_point_and_line ) )
| ~ ( C @ ( B @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[320,13190]) ).
thf(13287,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( A @ equal_lines ) )
!= ( D @ ( C @ equal_lines ) ) )
| ~ ( D @ ( B @ incident_point_and_line ) )
| ~ ( C @ ( B @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[13286]) ).
thf(13288,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ incident_point_and_line ) )
| ~ ( A @ ( B @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[13287:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( A ))]]) ).
thf(228,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)],[221,110]) ).
thf(229,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)],[228]) ).
thf(230,plain,
! [B: $i,A: $i] :
~ ( A @ ( B @ ( A @ orthogonal_through_point ) @ parallel_lines ) ),
inference(pattern_uni,[status(thm)],[229:[bind(A,$thf( E )),bind(B,$thf( F )),bind(C,$thf( F @ ( E @ orthogonal_through_point ) )),bind(D,$thf( E ))]]) ).
thf(235,plain,
! [B: $i,A: $i] :
~ ( A @ ( B @ ( A @ orthogonal_through_point ) @ parallel_lines ) ),
inference(simp,[status(thm)],[230]) ).
thf(440,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( D @ ( C @ distinct_lines ) ) )
| ~ $true
| ~ ( D @ ( C @ equal_lines ) )
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[414,135]) ).
thf(441,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( D @ ( C @ distinct_lines ) ) )
| ~ ( D @ ( C @ equal_lines ) )
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(simp,[status(thm)],[440]) ).
thf(442,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ equal_lines ) )
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[441:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( A )),bind(D,$thf( B ))]]) ).
thf(493,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( C @ distinct_lines ) ) )
| ~ ( D @ ( C @ equal_lines ) )
| ~ $true
| ( B @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[137,442]) ).
thf(494,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( C @ distinct_lines ) ) )
| ~ ( D @ ( C @ equal_lines ) )
| ( B @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[493]) ).
thf(495,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ equal_lines ) )
| ( A @ ( A @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[494:[bind(A,$thf( B )),bind(B,$thf( B )),bind(C,$thf( B ))]]) ).
thf(510,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ equal_lines ) )
| ( A @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[495]) ).
thf(151,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)],[150]) ).
thf(13807,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( sk3 @ ( sk3 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) )
| ~ $true
| ~ ( C @ ( B @ equal_lines ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(paramod_ordered,[status(thm)],[240,2134]) ).
thf(13808,plain,
! [C: $i,B: $i,A: $i] :
( ( ( C @ ( A @ apart_point_and_line ) )
!= ( sk3 @ ( sk3 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) )
| ~ ( C @ ( B @ equal_lines ) )
| ~ ( B @ ( A @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[13807]) ).
thf(13809,plain,
! [A: $i] :
( ~ ( sk3 @ ( A @ equal_lines ) )
| ~ ( A @ ( sk3 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[13808:[bind(A,$thf( sk3 @ ( sk1 @ intersection_point ) )),bind(B,$thf( B )),bind(C,$thf( sk3 ))]]) ).
thf(14030,plain,
! [A: $i] :
( ~ ( sk3 @ ( A @ equal_lines ) )
| ~ ( A @ ( sk3 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[13809]) ).
thf(2717,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( B @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) )
| ~ $true
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1128,144]) ).
thf(2718,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( B @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[2717]) ).
thf(2719,plain,
! [A: $i] :
( ~ ( sk2 @ ( A @ ( sk2 @ intersection_point ) @ apart_point_and_line ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[2718:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( A ))]]) ).
thf(14466,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)],[14445,55]) ).
thf(14467,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)],[14466]) ).
thf(14468,plain,
! [A: $i] :
~ ( sk1 @ ( A @ ( sk2 @ orthogonal_through_point ) @ orthogonal_lines ) ),
inference(pattern_uni,[status(thm)],[14467:[bind(A,$thf( E )),bind(B,$thf( E @ ( sk2 @ orthogonal_through_point ) )),bind(C,$thf( sk1 ))]]) ).
thf(14475,plain,
! [A: $i] :
~ ( sk1 @ ( A @ ( sk2 @ orthogonal_through_point ) @ orthogonal_lines ) ),
inference(simp,[status(thm)],[14468]) ).
thf(182,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)],[49,49]) ).
thf(183,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)],[182]) ).
thf(184,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)],[183:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( C )),bind(D,$thf( A )),bind(E,$thf( C ))]]) ).
thf(190,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)],[184]) ).
thf(356,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ $true
| ~ ( B @ ( A @ parallel_lines ) ) ),
inference(paramod_ordered,[status(thm)],[355,110]) ).
thf(357,plain,
! [B: $i,A: $i] :
( ( ( sk1 @ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ convergent_lines ) )
!= ( B @ ( A @ convergent_lines ) ) )
| ~ ( B @ ( A @ parallel_lines ) ) ),
inference(simp,[status(thm)],[356]) ).
thf(358,plain,
~ ( sk1 @ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ parallel_lines ) ),
inference(pattern_uni,[status(thm)],[357:[bind(A,$thf( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) )),bind(B,$thf( sk1 ))]]) ).
thf(2702,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk3 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( B @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) )
| ~ $true
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1136,144]) ).
thf(2703,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk3 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( B @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[2702]) ).
thf(2704,plain,
! [A: $i] :
( ~ ( sk3 @ ( A @ ( sk3 @ intersection_point ) @ apart_point_and_line ) )
| ( A @ ( sk1 @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[2703:[bind(A,$thf( A )),bind(B,$thf( sk3 )),bind(C,$thf( A ))]]) ).
thf(2089,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk1 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ $true
| ~ ( C @ ( B @ parallel_lines ) )
| ( sk2 @ ( A @ convergent_lines ) ) ),
inference(paramod_ordered,[status(thm)],[1941,110]) ).
thf(2090,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk1 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( C @ ( B @ parallel_lines ) )
| ( sk2 @ ( A @ convergent_lines ) ) ),
inference(simp,[status(thm)],[2089]) ).
thf(2091,plain,
! [A: $i] :
( ~ ( A @ ( sk1 @ parallel_lines ) )
| ( sk2 @ ( A @ convergent_lines ) ) ),
inference(pattern_uni,[status(thm)],[2090:[bind(A,$thf( A )),bind(B,$thf( sk1 )),bind(C,$thf( A ))]]) ).
thf(2774,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ parallel_through_point ) @ ( sk1 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( B @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2130,144]) ).
thf(2775,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk2 @ parallel_through_point ) @ ( sk1 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( B @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[2774]) ).
thf(2776,plain,
! [A: $i] :
~ ( sk1 @ ( A @ ( sk2 @ parallel_through_point ) @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[2775:[bind(A,$thf( E )),bind(B,$thf( sk1 )),bind(C,$thf( E @ ( sk2 @ parallel_through_point ) ))]]) ).
thf(2783,plain,
! [A: $i] :
~ ( sk1 @ ( A @ ( sk2 @ parallel_through_point ) @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ),
inference(simp,[status(thm)],[2776]) ).
thf(457,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( D @ distinct_lines ) ) )
| ( D @ ( C @ distinct_lines ) )
| ~ $true
| ( B @ ( A @ equal_lines ) ) ),
inference(paramod_ordered,[status(thm)],[137,415]) ).
thf(458,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( B @ ( A @ distinct_lines ) )
!= ( C @ ( D @ distinct_lines ) ) )
| ( D @ ( C @ distinct_lines ) )
| ( B @ ( A @ equal_lines ) ) ),
inference(simp,[status(thm)],[457]) ).
thf(459,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ distinct_lines ) )
| ( B @ ( A @ equal_lines ) ) ),
inference(pattern_uni,[status(thm)],[458:[bind(A,$thf( A )),bind(B,$thf( B )),bind(C,$thf( B )),bind(D,$thf( A ))]]) ).
thf(172,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ ( B @ parallel_through_point ) @ convergent_lines ) )
!= ( sk3 @ ( sk1 @ convergent_lines ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[41,117]) ).
thf(173,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( B @ parallel_through_point ) @ convergent_lines ) )
!= ( sk3 @ ( sk1 @ convergent_lines ) ) ),
inference(simp,[status(thm)],[172]) ).
thf(176,plain,
! [B: $i,A: $i] :
( ( B != sk3 )
| ( ( A @ ( B @ parallel_through_point ) )
!= sk1 ) ),
inference(simp,[status(thm)],[173]) ).
thf(178,plain,
! [A: $i] :
( ( A @ ( sk3 @ parallel_through_point ) )
!= sk1 ),
inference(simp,[status(thm)],[176]) ).
thf(9947,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk1 @ parallel_through_point ) @ ( sk2 @ convergent_lines ) )
!= ( C @ ( B @ ( C @ parallel_through_point ) @ convergent_lines ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[9871,117]) ).
thf(9948,plain,
! [C: $i,B: $i,A: $i] :
( ( A @ ( sk1 @ parallel_through_point ) @ ( sk2 @ convergent_lines ) )
!= ( C @ ( B @ ( C @ parallel_through_point ) @ convergent_lines ) ) ),
inference(simp,[status(thm)],[9947]) ).
thf(10001,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk1 @ parallel_through_point ) )
!= C )
| ( ( B @ ( C @ parallel_through_point ) )
!= sk2 ) ),
inference(simp,[status(thm)],[9948]) ).
thf(10013,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ ( sk1 @ parallel_through_point ) @ parallel_through_point ) )
!= sk2 ),
inference(simp,[status(thm)],[10001]) ).
thf(2204,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ convergent_lines ) )
!= ( D @ ( C @ convergent_lines ) ) )
| ~ ( D @ ( D @ ( C @ intersection_point ) @ apart_point_and_line ) )
| ~ $true
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(paramod_ordered,[status(thm)],[613,142]) ).
thf(2205,plain,
! [D: $i,C: $i,B: $i,A: $i] :
( ( ( A @ ( B @ convergent_lines ) )
!= ( D @ ( C @ convergent_lines ) ) )
| ~ ( D @ ( D @ ( C @ intersection_point ) @ apart_point_and_line ) )
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(simp,[status(thm)],[2204]) ).
thf(2206,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( A @ ( B @ intersection_point ) @ apart_point_and_line ) )
| ~ ( A @ ( A @ distinct_lines ) ) ),
inference(pattern_uni,[status(thm)],[2205:[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 @ ( 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)],[120,2215]) ).
thf(2296,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)],[2295]) ).
thf(2297,plain,
! [A: $i] :
( ( sk2 @ ( sk1 @ intersection_point ) @ ( A @ distinct_points ) )
| ~ ( sk2 @ ( A @ apart_point_and_line ) ) ),
inference(pattern_uni,[status(thm)],[2296:[bind(A,$thf( A )),bind(B,$thf( sk2 )),bind(C,$thf( sk2 @ ( sk1 @ intersection_point ) ))]]) ).
thf(16911,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk3 @ parallel_through_point ) @ ( sk1 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( B @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[16781,144]) ).
thf(16912,plain,
! [C: $i,B: $i,A: $i] :
( ( ( A @ ( sk3 @ parallel_through_point ) @ ( sk1 @ convergent_lines ) )
!= ( C @ ( B @ convergent_lines ) ) )
| ~ ( B @ ( C @ ( B @ intersection_point ) @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[16911]) ).
thf(16913,plain,
! [A: $i] :
~ ( sk1 @ ( A @ ( sk3 @ parallel_through_point ) @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[16912:[bind(A,$thf( E )),bind(B,$thf( sk1 )),bind(C,$thf( E @ ( sk3 @ parallel_through_point ) ))]]) ).
thf(16960,plain,
! [A: $i] :
~ ( sk1 @ ( A @ ( sk3 @ parallel_through_point ) @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ),
inference(simp,[status(thm)],[16913]) ).
thf(335,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ distinct_points ) )
!= ( B @ ( A @ distinct_points ) ) )
| ~ ( B @ ( A @ line_connecting ) @ ( B @ apart_point_and_line ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[42,114]) ).
thf(336,plain,
! [B: $i,A: $i] :
( ( ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ distinct_points ) )
!= ( B @ ( A @ distinct_points ) ) )
| ~ ( B @ ( A @ line_connecting ) @ ( B @ apart_point_and_line ) ) ),
inference(simp,[status(thm)],[335]) ).
thf(337,plain,
~ ( sk3 @ ( sk1 @ intersection_point ) @ ( sk2 @ ( sk1 @ intersection_point ) @ line_connecting ) @ ( sk3 @ ( sk1 @ intersection_point ) @ apart_point_and_line ) ),
inference(pattern_uni,[status(thm)],[336:[bind(A,$thf( sk2 @ ( sk1 @ intersection_point ) )),bind(B,$thf( sk3 @ ( sk1 @ intersection_point ) ))]]) ).
thf(24361,plain,
$false,
inference(e,[status(thm)],[69,1337,2094,6979,138,101,4262,2263,555,1818,88,2280,481,115,120,10039,202,1173,5550,6089,14478,153,2740,142,4870,13238,42,301,320,3891,52,3938,110,2185,196,157,9480,6396,421,8717,46,152,57,4793,78,2222,164,179,3983,1136,106,121,1151,84,2073,2017,147,1169,61,221,956,453,132,89,13420,988,243,12133,74,307,3899,2011,14445,925,534,102,4059,2773,60,4199,117,220,366,2264,38,598,70,3989,165,16973,13423,275,137,92,2758,4155,97,2200,1159,1128,14011,13391,519,14028,1540,169,141,10880,13996,1498,328,16986,225,537,13190,1155,2781,7749,129,41,73,2203,205,558,953,128,237,1991,2235,298,2001,3890,10030,148,64,149,601,44,118,2134,572,144,49,236,14027,86,113,81,996,10037,208,98,616,2129,103,4462,2267,140,3932,91,66,240,155,2770,130,2212,278,306,135,2752,9871,80,531,112,123,355,145,63,1156,1941,2407,414,971,95,50,67,331,127,2701,16987,1141,613,72,16781,4819,143,43,2266,450,99,87,2215,1126,104,1998,1326,40,171,2764,2130,2152,55,114,75,13288,58,235,510,151,2683,14030,2719,950,146,51,14475,190,107,358,2704,474,2091,94,2783,415,459,47,178,442,10013,2206,2297,16960,337,122]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEO203+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.14/0.61 % Computer : n013.cluster.edu
% 0.14/0.61 % Model : x86_64 x86_64
% 0.14/0.61 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.61 % Memory : 8046.5625MB
% 0.14/0.61 % OS : Linux 6.8.0-71-generic
% 0.14/0.61 % CPULimit : 300
% 0.14/0.61 % WCLimit : 300
% 0.14/0.61 % DateTime : Fri Sep 25 13:04:57 UTC 2026
% 0.14/0.61 % CPUTime :
% 0.14/0.61 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.17/0.95 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 0.92/1.09 % [INFO] Parsing done (132ms).
% 0.92/1.09 % [INFO] Running in sequential loop mode.
% 1.72/1.33 % [INFO] eprover registered as external prover.
% 1.72/1.34 % [INFO] Scanning for conjecture ...
% 1.92/1.44 % [INFO] Found a conjecture (or negated_conjecture) and 35 axioms. Running axiom selection ...
% 2.12/1.52 % [INFO] Axiom selection finished. Selected 35 axioms (removed 0 axioms).
% 2.12/1.59 % [INFO] Problem is first-order (TPTP FOF).
% 2.37/1.60 % [INFO] Type checking passed.
% 2.37/1.60 % [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 ...
% 79.51/17.84 % External prover 'e' found a proof!
% 79.51/17.84 % [INFO] Killing All external provers ...
% 79.51/17.85 % Time passed: 17102ms (effective reasoning time: 16748ms)
% 79.51/17.85 % 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)>
% 79.51/17.85 % 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
% 79.51/17.85 % No. of inferences in proof: 715
% 79.51/17.85 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 17102 ms resp. 16748 ms w/o parsing
% 80.30/18.13 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 80.64/18.13 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------