% Case 1 in Cronheim's proof of Hessenberg's Theorem % p partial equality for points, l p.e. for lines, i point-line incidence fof(goal_normal,axiom, ! [A]:((l(A, A) & i(bc, A) & i(ac, A) & i(ab, A)) => ((goal)))). fof(hessenberg_gap1,axiom, ((i(a1, b2c2)) => ((goal)))). fof(hessenberg_gap2,axiom, ((i(b2, a1c1)) => ((goal)))). fof(ia1b1,axiom, (((i(a1, a1b1))))). fof(ib1a1,axiom, (((i(b1, a1b1))))). fof(ia2b2,axiom, (((i(a2, a2b2))))). fof(ib2a2,axiom, (((i(b2, a2b2))))). fof(ia1c1,axiom, (((i(a1, a1c1))))). fof(ic1a1,axiom, (((i(c1, a1c1))))). fof(ia2c2,axiom, (((i(a2, a2c2))))). fof(ic2a2,axiom, (((i(c2, a2c2))))). fof(ic1b1,axiom, (((i(c1, b1c1))))). fof(ib1c1,axiom, (((i(b1, b1c1))))). fof(ic2b2,axiom, (((i(c2, b2c2))))). fof(ib2c2,axiom, (((i(b2, b2c2))))). fof(iooa,axiom, (((i(o, oa))))). fof(ioob,axiom, (((i(o, ob))))). fof(iooc,axiom, (((i(o, oc))))). fof(ia1oa,axiom, (((i(a1, oa))))). fof(ia2oa,axiom, (((i(a2, oa))))). fof(ib1ob,axiom, (((i(b1, ob))))). fof(ib2ob,axiom, (((i(b2, ob))))). fof(ic1oc,axiom, (((i(c1, oc))))). fof(ic2oc,axiom, (((i(c2, oc))))). fof(ibc1,axiom, (((i(bc, b1c1))))). fof(ibc2,axiom, (((i(bc, b2c2))))). fof(iac1,axiom, (((i(ac, a1c1))))). fof(iac2,axiom, (((i(ac, a2c2))))). fof(iab1,axiom, (((i(ab, a1b1))))). fof(iab2,axiom, (((i(ab, a2b2))))). fof(triangle1,axiom, ! [A]:((i(a1, A) & i(b1, A) & i(c1, A)) => ((goal)))). fof(triangle2,axiom, ! [A]:((i(a2, A) & i(b2, A) & i(c2, A)) => ((goal)))). fof(notaa,axiom, ((p(a2, a1)) => ((goal)))). fof(notbb,axiom, ((p(b2, b1)) => ((goal)))). fof(notcc,axiom, ((p(c2, c1)) => ((goal)))). fof(notbc,axiom, ((l(b1c1, b2c2)) => ((goal)))). fof(notac,axiom, ((l(a1c1, a2c2)) => ((goal)))). fof(notab,axiom, ((l(a1b1, a2b2)) => ((goal)))). fof(pref,axiom, ! [A, B]:((i(A, B)) => ((p(A, A))))). fof(psym,axiom, ! [A, B]:((p(A, B)) => ((p(B, A))))). fof(ptra,axiom, ! [A, B, C]:((p(A, B) & p(B, C)) => ((p(A, C))))). fof(lref,axiom, ! [A, B]:((i(A, B)) => ((l(B, B))))). fof(lsym,axiom, ! [A, B]:((l(A, B)) => ((l(B, A))))). fof(ltra,axiom, ! [A, B, C]:((l(A, B) & l(B, C)) => ((l(A, C))))). fof(pcon,axiom, ! [A, B, C]:((p(A, B) & i(B, C)) => ((i(A, C))))). fof(lcon,axiom, ! [A, B, C]:((i(A, B) & l(B, C)) => ((i(A, C))))). fof(unique,axiom, ! [A, B, C, D]:((i(A, C) & i(A, D) & i(B, C) & i(B, D)) => ((p(A, B)) | (l(C, D))))). fof(line,axiom, ! [A, B]:((p(A, A) & p(B, B)) => (? [C] : (i(A, C) & i(B, C))))). fof(point,axiom, ! [A, B]:((l(A, A) & l(B, B)) => (? [C] : (i(C, A) & i(C, B))))). fof(papp,axiom, ! [A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q]:((i(A, J) & i(B, J) & i(C, J) & i(D, K) & i(E, K) & i(F, K) & i(B, L) & i(F, L) & i(G, L) & i(C, M) & i(E, M) & i(G, M) & i(B, N) & i(D, N) & i(H, N) & i(A, O) & i(E, O) & i(H, O) & i(C, P) & i(D, P) & i(I, P) & i(A, Q) & i(F, Q) & i(I, Q)) => ((l(L, M)) | (l(N, O)) | (l(P, Q)) | ? [R] : (l(R, R) & i(G, R) & i(H, R) & i(I, R))))). fof(goal_to_be_proved,conjecture,goal).