Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
% Reduction of 8 cases to 2 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(t1in2,axiom, ((i(a1, b2c2) & i(b1, a2c2) & i(c1, a2b2)) => ((goal)))). fof(t2in1,axiom, ((i(a2, b1c1) & i(b2, a1c1) & i(c2, a1b1)) => ((goal)))). fof(gap_a,axiom, (((i(a1, b2c2)) | (i(b2, a1c1))))). fof(gap_b,axiom, (((i(b1, a2c2)) | (i(c2, a1b1))))). fof(gap_c,axiom, (((i(c1, a2b2)) | (i(a2, b1c1))))). 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(goal_to_be_proved,conjecture,goal).