## TPTP Problem File: GEO166+1.p

View Solutions - Solve Problem

```%------------------------------------------------------------------------------
% File     : GEO166+1 : TPTP v7.0.0. Released v3.2.0.
% Domain   : Geometry
% Problem  : Case 1 in Cronheim's proof of Hessenberg's Theorem
% Version  : Especial.
% English  :

% Refs     : [Bez05] Bezem (2005), Email to Geoff Sutcliffe
% Source   : [Bez05]
% Names    : pd_hes [Bez05]

% Status   : Unknown
% Rating   : 1.00 v3.2.0
% Syntax   : Number of formulae    :   51 (  28 unit)
%            Number of atoms       :  122 (   0 equality)
%            Maximal formula depth :   42 (   3 average)
%            Number of connectives :   71 (   0   ~;   4   |;  44   &)
%                                         (   0 <=>;  23  =>;   0  <=;   0 <~>)
%                                         (   0  ~|;   0  ~&)
%            Number of predicates  :    4 (   1 propositional; 0-2 arity)
%            Number of functors    :   19 (  19 constant; 0-0 arity)
%            Number of variables   :   51 (   0 sgn;  48   !;   3   ?)
%            Maximal term depth    :    1 (   1 average)
% SPC      : FOF_UNK_RFO_NEQ

%------------------------------------------------------------------------------
fof(goal_normal,axiom,(
! [A] :
( ( line_equal(A,A)
& incident(bc,A)
& incident(ac,A)
& incident(ab,A) )
=> goal ) )).

fof(hessenberg_gap1,axiom,
( incident(a1,b2c2)
=> goal )).

fof(hessenberg_gap2,axiom,
( incident(b2,a1c1)
=> goal )).

fof(ia1b1,axiom,(
incident(a1,a1b1) )).

fof(ib1a1,axiom,(
incident(b1,a1b1) )).

fof(ia2b2,axiom,(
incident(a2,a2b2) )).

fof(ib2a2,axiom,(
incident(b2,a2b2) )).

fof(ia1c1,axiom,(
incident(a1,a1c1) )).

fof(ic1a1,axiom,(
incident(c1,a1c1) )).

fof(ia2c2,axiom,(
incident(a2,a2c2) )).

fof(ic2a2,axiom,(
incident(c2,a2c2) )).

fof(ic1b1,axiom,(
incident(c1,b1c1) )).

fof(ib1c1,axiom,(
incident(b1,b1c1) )).

fof(ic2b2,axiom,(
incident(c2,b2c2) )).

fof(ib2c2,axiom,(
incident(b2,b2c2) )).

fof(iooa,axiom,(
incident(o,oa) )).

fof(ioob,axiom,(
incident(o,ob) )).

fof(iooc,axiom,(
incident(o,oc) )).

fof(ia1oa,axiom,(
incident(a1,oa) )).

fof(ia2oa,axiom,(
incident(a2,oa) )).

fof(ib1ob,axiom,(
incident(b1,ob) )).

fof(ib2ob,axiom,(
incident(b2,ob) )).

fof(ic1oc,axiom,(
incident(c1,oc) )).

fof(ic2oc,axiom,(
incident(c2,oc) )).

fof(ibc1,axiom,(
incident(bc,b1c1) )).

fof(ibc2,axiom,(
incident(bc,b2c2) )).

fof(iac1,axiom,(
incident(ac,a1c1) )).

fof(iac2,axiom,(
incident(ac,a2c2) )).

fof(iab1,axiom,(
incident(ab,a1b1) )).

fof(iab2,axiom,(
incident(ab,a2b2) )).

fof(triangle1,axiom,(
! [A] :
( ( incident(a1,A)
& incident(b1,A)
& incident(c1,A) )
=> goal ) )).

fof(triangle2,axiom,(
! [A] :
( ( incident(a2,A)
& incident(b2,A)
& incident(c2,A) )
=> goal ) )).

fof(notaa,axiom,
( point_equal(a2,a1)
=> goal )).

fof(notbb,axiom,
( point_equal(b2,b1)
=> goal )).

fof(notcc,axiom,
( point_equal(c2,c1)
=> goal )).

fof(notbc,axiom,
( line_equal(b1c1,b2c2)
=> goal )).

fof(notac,axiom,
( line_equal(a1c1,a2c2)
=> goal )).

fof(notab,axiom,
( line_equal(a1b1,a2b2)
=> goal )).

fof(reflexivity_of_point_equal,axiom,(
! [A,B] :
( incident(A,B)
=> point_equal(A,A) ) )).

fof(symmetry_of_point_equal,axiom,(
! [A,B] :
( point_equal(A,B)
=> point_equal(B,A) ) )).

fof(transitivity_of_point_equal,axiom,(
! [A,B,C] :
( ( point_equal(A,B)
& point_equal(B,C) )
=> point_equal(A,C) ) )).

fof(reflexivity_of_line_equal,axiom,(
! [A,B] :
( incident(A,B)
=> line_equal(B,B) ) )).

fof(symmetry_of_line_equal,axiom,(
! [A,B] :
( line_equal(A,B)
=> line_equal(B,A) ) )).

fof(transitivity_of_line_equal,axiom,(
! [A,B,C] :
( ( line_equal(A,B)
& line_equal(B,C) )
=> line_equal(A,C) ) )).

fof(pcon,axiom,(
! [A,B,C] :
( ( point_equal(A,B)
& incident(B,C) )
=> incident(A,C) ) )).

fof(lcon,axiom,(
! [A,B,C] :
( ( incident(A,B)
& line_equal(B,C) )
=> incident(A,C) ) )).

fof(unique,axiom,(
! [A,B,C,D] :
( ( incident(A,C)
& incident(A,D)
& incident(B,C)
& incident(B,D) )
=> ( point_equal(A,B)
| line_equal(C,D) ) ) )).

fof(line,axiom,(
! [A,B] :
( ( point_equal(A,A)
& point_equal(B,B) )
=> ? [C] :
( incident(A,C)
& incident(B,C) ) ) )).

fof(point,axiom,(
! [A,B] :
( ( line_equal(A,A)
& line_equal(B,B) )
=> ? [C] :
( incident(C,A)
& incident(C,B) ) ) )).

fof(pappus,axiom,(
! [A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q] :
( ( incident(A,J)
& incident(B,J)
& incident(C,J)
& incident(D,K)
& incident(E,K)
& incident(F,K)
& incident(B,L)
& incident(F,L)
& incident(G,L)
& incident(C,M)
& incident(E,M)
& incident(G,M)
& incident(B,N)
& incident(D,N)
& incident(H,N)
& incident(A,O)
& incident(E,O)
& incident(H,O)
& incident(C,P)
& incident(D,P)
& incident(I,P)
& incident(A,Q)
& incident(F,Q)
& incident(I,Q) )
=> ( line_equal(L,M)
| line_equal(N,O)
| line_equal(P,Q)
| ? [R] :
( line_equal(R,R)
& incident(G,R)
& incident(H,R)
& incident(I,R) ) ) ) )).

fof(goal_to_be_proved,conjecture,(
goal )).

%------------------------------------------------------------------------------
```