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
% Pappus2 implies Pappus1 % el equality for lines, ep equality for points % col collinearity, pl point-line incidence fof(assump1,axiom, (((col(a, b, c, l) & col(d, e, f, m))))). fof(assump2,axiom, (((col(b, f, g, n) & col(c, e, g, o))))). fof(assump3,axiom, (((col(b, d, h, p) & col(a, e, h, q))))). fof(assump4,axiom, (((col(c, d, i, r) & col(a, f, i, s))))). fof(goalam,axiom, ((pl(a, m)) => ((goal)))). fof(goalbm,axiom, ((pl(b, m)) => ((goal)))). fof(goalcm,axiom, ((pl(c, m)) => ((goal)))). fof(goaldl,axiom, ((pl(d, l)) => ((goal)))). fof(goalel,axiom, ((pl(e, l)) => ((goal)))). fof(goalfl,axiom, ((pl(f, l)) => ((goal)))). fof(goal4,axiom, ! [A]:((pl(g, A) & pl(h, A) & pl(i, A)) => ((goal)))). fof(col_elim1,axiom, ! [A, B, C, D]:((col(A, B, C, D)) => ((pl(A, D))))). fof(col_elim2,axiom, ! [A, B, C, D]:((col(A, B, C, D)) => ((pl(B, D))))). fof(col_elim3,axiom, ! [A, B, C, D]:((col(A, B, C, D)) => ((pl(C, D))))). fof(pref,axiom, ! [A, B]:((pl(A, B)) => ((ep(A, A))))). fof(psym,axiom, ! [A, B]:((ep(A, B)) => ((ep(B, A))))). fof(ptra,axiom, ! [A, B, C]:((ep(A, B) & ep(B, C)) => ((ep(A, C))))). fof(lref,axiom, ! [A, B]:((pl(A, B)) => ((el(B, B))))). fof(lsym,axiom, ! [A, B]:((el(A, B)) => ((el(B, A))))). fof(ltra,axiom, ! [A, B, C]:((el(A, B) & el(B, C)) => ((el(A, C))))). fof(pcon,axiom, ! [A, B, C]:((ep(A, B) & pl(B, C)) => ((pl(A, C))))). fof(lcon,axiom, ! [A, B, C]:((pl(A, B) & el(B, C)) => ((pl(A, C))))). fof(papp1,axiom, ! [A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q]:((col(A, B, C, J) & col(D, E, F, K) & col(B, F, G, L) & col(C, E, G, M) & col(B, D, H, N) & col(A, E, H, O) & col(C, D, I, P) & col(A, F, I, Q)) => (? [R] : (col(G, H, I, R)) | (el(L, M)) | (el(N, O)) | (el(P, Q))))). fof(unique,axiom, ! [A, B, C, D]:((pl(C, A) & pl(C, B) & pl(D, A) & pl(D, B)) => ((ep(C, D)) | (el(A, B))))). fof(line,axiom, ! [A, B]:((ep(A, A) & ep(B, B)) => (? [C] : (pl(A, C) & pl(B, C))))). fof(point,axiom, ! [A, B, C]:((el(C, C) & el(B, B)) => (? [A] : (pl(A, B) & pl(A, C))))). fof(goal_to_be_proved,conjecture,goal).