premises
#ax_branch_bet

point(1)
point(2)
point(3)

conclusions

bet(1, 2, 3)

|
~bet(1, 2, 3)


premises
#ax_branch_col

point(1)
point(2)
point(3)
~eq_point(1, 2)
~eq_point(1, 3)
~eq_point(2, 3)

conclusions

col(1, 2, 3)

|
~col(1, 2, 3)


premises
#ax_branch_cop

point(1)
point(2)
point(3)
point(4)
~eq_point(1, 2)
~eq_point(1, 3)
~eq_point(1, 4)
~eq_point(2, 3)
~eq_point(2, 4)
~eq_point(3, 4)

conclusions

cop(1, 2, 3, 4)

|
~cop(1, 2, 3, 4)


premises
#ax_branch_cut

point(2)
point(3)
~eq_point(2, 3)
line(1)

conclusions

cut(1, 2, 3)

|
~cut(1, 2, 3)


premises
#ax_branch_inc_l_pl

line(1)
plane(2)

conclusions

inc_l_pl(1, 2)

|
~inc_l_pl(1, 2)


premises
#ax_branch_inc_po_l

point(1)
line(2)

conclusions

inc_po_l(1, 2)

|
~inc_po_l(1, 2)


premises
#ax_branch_inc_po_pl

point(1)
plane(2)

conclusions

inc_po_pl(1, 2)

|
~inc_po_pl(1, 2)


premises
#ax_branch_int_l_l

line(1)
line(2)
~eq_line(1, 2)

conclusions

int_l_l(1, 2)

|
~int_l_l(1, 2)


premises
#ax_branch_int_l_pl

line(1)
plane(2)

conclusions

int_l_pl(1, 2)

|
~int_l_pl(1, 2)


premises
#ax_branch_int_pl_pl

plane(1)
plane(2)
~eq_plane(1, 2)

conclusions

int_pl_pl(1, 2)

|
~int_pl_pl(1, 2)


premises
#ax_branch_pash

point(1)
point(2)
point(3)
~eq_point(1, 2)
~eq_point(1, 3)
~eq_point(2, 3)
line(4)
plane(5)

conclusions

pash(1, 2, 3, 4, 5)

|
~pash(1, 2, 3, 4, 5)


premises
#ax_cut_1

point(2)
point(3)
line(1)
point(4)
~inc_po_l(2, 1)
~inc_po_l(3, 1)
inc_po_l(4, 1)
bet(2, 4, 3)

conclusions

cut(1, 2, 3)

premises
#ax_cut_2

point(2)
point(3)
line(1)
cut(1, 2, 3)

conclusions

point(4)
~inc_po_l(2, 1)
~inc_po_l(3, 1)
inc_po_l(4, 1)
bet(2, 4, 3)

premises
#ax_D10

line(1)
plane(2)
int_l_pl(1, 2)

conclusions

point(3)
inc_po_l(3, 1)
inc_po_pl(3, 2)
~inc_l_pl(1, 2)

premises
#ax_D11a

line(1)
plane(2)
~inc_l_pl(1, 2)

conclusions

point(3)
inc_po_l(3, 1)
~inc_po_pl(3, 2)

premises
#ax_D11b

point(1)
line(2)
plane(3)
inc_po_l(1, 2)
~inc_po_pl(1, 3)

conclusions

~inc_l_pl(2, 3)

premises
#ax_D11

point(1)
line(2)
plane(3)
inc_l_pl(2, 3)
inc_po_l(1, 2)

conclusions

inc_po_pl(1, 3)

premises
#ax_D1a

point(1)
point(2)
~eq_point(1, 2)
point(3)
line(4)
inc_po_l(1, 4)
inc_po_l(2, 4)
~inc_po_l(3, 4)

conclusions

~col(1, 2, 3)

premises
#ax_D1

point(1)
point(2)
point(3)
line(4)
inc_po_l(1, 4)
inc_po_l(2, 4)
inc_po_l(3, 4)

conclusions

col(1, 2, 3)

premises
#ax_D2a

point(1)
point(2)
~eq_point(1, 2)
point(3)
line(4)
inc_po_l(1, 4)
inc_po_l(2, 4)
~col(1, 2, 3)

conclusions

~inc_po_l(3, 4)

premises
#ax_D2

point(1)
point(2)
point(3)
col(1, 2, 3)

conclusions

line(4)
inc_po_l(1, 4)
inc_po_l(2, 4)
inc_po_l(3, 4)

premises
#ax_D3a

point(1)
point(2)
point(3)
~col(1, 2, 3)
point(4)
plane(5)
inc_po_pl(1, 5)
inc_po_pl(2, 5)
inc_po_pl(3, 5)
~inc_po_pl(4, 5)

conclusions

~cop(1, 2, 3, 4)

premises
#ax_D3

point(1)
point(2)
point(3)
point(4)
plane(5)
inc_po_pl(1, 5)
inc_po_pl(2, 5)
inc_po_pl(3, 5)
inc_po_pl(4, 5)

conclusions

cop(1, 2, 3, 4)

premises
#ax_D4a

point(1)
point(2)
point(3)
~col(1, 2, 3)
point(4)
plane(5)
inc_po_pl(1, 5)
inc_po_pl(2, 5)
inc_po_pl(3, 5)
~cop(1, 2, 3, 4)

conclusions

~inc_po_pl(4, 5)

premises
#ax_D4

point(1)
point(2)
point(3)
point(4)
cop(1, 2, 3, 4)

conclusions

plane(5)
inc_po_pl(1, 5)
inc_po_pl(2, 5)
inc_po_pl(3, 5)
inc_po_pl(4, 5)

premises
#ax_D5a

line(1)
line(2)
point(3)
~eq_line(1, 2)
~int_l_l(1, 2)
inc_po_l(3, 1)

conclusions

~inc_po_l(3, 2)

premises
#ax_D5

line(1)
line(2)
point(3)
~eq_line(1, 2)
inc_po_l(3, 1)
inc_po_l(3, 2)

conclusions

int_l_l(1, 2)

premises
#ax_D6

line(1)
line(2)
int_l_l(1, 2)

conclusions

point(3)
~eq_line(1, 2)
inc_po_l(3, 1)
inc_po_l(3, 2)

premises
#ax_D7a

plane(1)
plane(2)
point(3)
~eq_plane(1, 2)
inc_po_pl(3, 1)
~int_pl_pl(1, 2)

conclusions

~inc_po_pl(3, 2)

premises
#ax_D7

plane(1)
plane(2)
point(3)
~eq_plane(1, 2)
inc_po_pl(3, 1)
inc_po_pl(3, 2)

conclusions

int_pl_pl(1, 2)

premises
#ax_D8

plane(1)
plane(2)
int_pl_pl(1, 2)

conclusions

point(3)
~eq_plane(1, 2)
inc_po_pl(3, 1)
inc_po_pl(3, 2)

premises
#ax_D9a

line(1)
plane(2)
point(3)
~inc_l_pl(1, 2)
~int_l_pl(1, 2)
inc_po_l(3, 1)

conclusions

~inc_po_pl(3, 2)

premises
#ax_D9b

line(1)
plane(2)
point(3)
~inc_l_pl(1, 2)
~int_l_pl(1, 2)
inc_po_pl(3, 2)

conclusions

~inc_po_l(3, 1)

premises
#ax_D9

line(1)
plane(2)
point(3)
~inc_l_pl(1, 2)
inc_po_l(3, 1)
inc_po_pl(3, 2)

conclusions

int_l_pl(1, 2)

premises
#ax_false_bet

point(1)
point(2)
point(3)
bet(1, 2, 3)
~bet(1, 2, 3)

conclusions



premises
#ax_false_col

point(1)
point(2)
point(3)
col(1, 2, 3)
~col(1, 2, 3)

conclusions



premises
#ax_false_cop

point(1)
point(2)
point(3)
point(4)
cop(1, 2, 3, 4)
~cop(1, 2, 3, 4)

conclusions



premises
#ax_false_cut

point(2)
point(3)
line(1)
cut(1, 2, 3)
~cut(1, 2, 3)

conclusions



premises
#ax_false_inc_l_pl

line(1)
plane(2)
inc_l_pl(1, 2)
~inc_l_pl(1, 2)

conclusions



premises
#ax_false_inc_po_l

point(1)
line(2)
inc_po_l(1, 2)
~inc_po_l(1, 2)

conclusions



premises
#ax_false_inc_po_pl

point(1)
plane(2)
inc_po_pl(1, 2)
~inc_po_pl(1, 2)

conclusions



premises
#ax_false_int_l_l

line(1)
line(2)
int_l_l(1, 2)
~int_l_l(1, 2)

conclusions



premises
#ax_false_int_l_pl

line(1)
plane(2)
int_l_pl(1, 2)
~int_l_pl(1, 2)

conclusions



premises
#ax_false_int_pl_pl

plane(1)
plane(2)
int_pl_pl(1, 2)
~int_pl_pl(1, 2)

conclusions



premises
#ax_false_pash

point(1)
point(2)
point(3)
line(4)
plane(5)
pash(1, 2, 3, 4, 5)
~pash(1, 2, 3, 4, 5)

conclusions



premises
#ax_I1

point(1)
point(2)
~eq_point(1, 2)

conclusions

line(3)
inc_po_l(1, 3)
inc_po_l(2, 3)

premises
#ax_I2

point(1)
point(2)
line(3)
line(4)
~eq_point(1, 2)
inc_po_l(1, 3)
inc_po_l(2, 3)
inc_po_l(1, 4)
inc_po_l(2, 4)

conclusions

eq_line(3, 4)

premises
#ax_I3a

line(1)

conclusions

point(2)
point(3)
~eq_point(2, 3)
inc_po_l(2, 1)
inc_po_l(3, 1)

premises
#ax_I3b


conclusions

point(1)
point(2)
point(3)
~col(1, 2, 3)

premises
#ax_I4a

point(1)
point(2)
point(3)
~col(1, 2, 3)

conclusions

plane(4)
inc_po_pl(1, 4)
inc_po_pl(2, 4)
inc_po_pl(3, 4)

premises
#ax_I4b

plane(1)

conclusions

point(2)
inc_po_pl(2, 1)

premises
#ax_I5

point(1)
point(2)
point(3)
plane(4)
plane(5)
~col(1, 2, 3)
inc_po_pl(1, 4)
inc_po_pl(2, 4)
inc_po_pl(3, 4)
inc_po_pl(1, 5)
inc_po_pl(2, 5)
inc_po_pl(3, 5)

conclusions

eq_plane(4, 5)

premises
#ax_I6

point(1)
point(2)
line(3)
plane(4)
~eq_point(1, 2)
inc_po_l(1, 3)
inc_po_l(2, 3)
inc_po_pl(1, 4)
inc_po_pl(2, 4)

conclusions

inc_l_pl(3, 4)

premises
#ax_I7

plane(1)
plane(2)
point(3)
~eq_plane(1, 2)
inc_po_pl(3, 1)
inc_po_pl(3, 2)

conclusions

point(4)
~eq_point(3, 4)
inc_po_pl(4, 1)
inc_po_pl(4, 2)

premises
#ax_I8


conclusions

point(1)
point(2)
point(3)
point(4)
~cop(1, 2, 3, 4)

premises
#ax_II1

point(1)
point(2)
point(3)
bet(1, 2, 3)

conclusions

~eq_point(1, 2)
~eq_point(1, 3)
~eq_point(2, 3)
col(1, 2, 3)
bet(3, 2, 1)

premises
#ax_II2

point(1)
point(2)
~eq_point(1, 2)

conclusions

point(3)
bet(1, 2, 3)

premises
#ax_II3

point(1)
point(2)
point(3)
~eq_point(1, 2)
~eq_point(1, 3)
~eq_point(2, 3)
bet(1, 2, 3)

conclusions

~bet(2, 3, 1)
~bet(3, 1, 2)

premises
#ax_II4

point(1)
point(2)
point(3)
line(4)
plane(5)
pash(1, 2, 3, 4, 5)

conclusions

cut(4, 3, 1)

|
cut(4, 1, 2)


premises
#ax_pash_1

point(1)
point(2)
point(3)
line(4)
plane(5)
~col(1, 2, 3)
inc_po_pl(1, 5)
inc_po_pl(2, 5)
inc_po_pl(3, 5)
inc_l_pl(4, 5)
~inc_po_l(1, 4)
~inc_po_l(2, 4)
~inc_po_l(3, 4)
cut(4, 2, 3)

conclusions

pash(1, 2, 3, 4, 5)

premises
#ax_pash_2

point(1)
point(2)
point(3)
line(4)
plane(5)
pash(1, 2, 3, 4, 5)

conclusions

~col(1, 2, 3)
inc_po_pl(1, 5)
inc_po_pl(2, 5)
inc_po_pl(3, 5)
inc_l_pl(4, 5)
~inc_po_l(1, 4)
~inc_po_l(2, 4)
~inc_po_l(3, 4)
cut(4, 2, 3)

premises
#ax_sym_col1

point(1)
point(2)
point(3)
col(1, 2, 3)

conclusions

col(2, 3, 1)

premises
#ax_sym_col2

point(1)
point(2)
point(3)
col(1, 2, 3)

conclusions

col(2, 1, 3)

premises
#ax_sym_col

point(1)
point(2)
point(3)
col(1, 2, 3)

conclusions

col(1, 3, 2)
col(2, 1, 3)
col(2, 3, 1)
col(3, 1, 2)
col(3, 2, 1)

premises
#ax_sym_cop1

point(1)
point(2)
point(3)
point(4)
cop(1, 2, 3, 4)

conclusions

cop(2, 3, 4, 1)

premises
#ax_sym_cop2

point(1)
point(2)
point(3)
point(4)
cop(1, 2, 3, 4)

conclusions

cop(2, 1, 3, 4)

premises
#ax_sym_cop

point(1)
point(2)
point(3)
point(4)
cop(1, 2, 3, 4)

conclusions

cop(1, 2, 4, 3)
cop(1, 3, 2, 4)
cop(1, 3, 4, 2)
cop(1, 4, 2, 3)
cop(1, 4, 3, 2)
cop(2, 1, 3, 4)
cop(2, 1, 4, 3)
cop(2, 3, 1, 4)
cop(2, 3, 4, 1)
cop(2, 4, 1, 3)
cop(2, 4, 3, 1)
cop(3, 1, 2, 4)
cop(3, 1, 4, 2)
cop(3, 2, 1, 4)
cop(3, 2, 4, 1)
cop(3, 4, 1, 2)
cop(3, 4, 2, 1)
cop(4, 1, 2, 3)
cop(4, 1, 3, 2)
cop(4, 2, 1, 3)
cop(4, 2, 3, 1)
cop(4, 3, 1, 2)
cop(4, 3, 2, 1)

premises
#ax_sym_int_l_l

line(1)
line(2)
int_l_l(1, 2)

conclusions

int_l_l(2, 1)

premises
#ax_sym_int_pl_pl

plane(1)
plane(2)
int_pl_pl(1, 2)

conclusions

int_pl_pl(2, 1)

premises
#ax_sym_ncol1

point(1)
point(2)
point(3)
~col(1, 2, 3)

conclusions

~col(2, 3, 1)

premises
#ax_sym_ncol2

point(1)
point(2)
point(3)
~col(1, 2, 3)

conclusions

~col(2, 1, 3)

premises
#ax_sym_ncol

point(1)
point(2)
point(3)
~col(1, 2, 3)

conclusions

~col(1, 3, 2)
~col(2, 1, 3)
~col(2, 3, 1)
~col(3, 1, 2)
~col(3, 2, 1)

premises
#ax_sym_ncop1

point(1)
point(2)
point(3)
point(4)
~cop(1, 2, 3, 4)

conclusions

~cop(2, 3, 4, 1)

premises
#ax_sym_ncop2

point(1)
point(2)
point(3)
point(4)
~cop(1, 2, 3, 4)

conclusions

~cop(2, 1, 3, 4)

premises
#ax_sym_ncop

point(1)
point(2)
point(3)
point(4)
~cop(1, 2, 3, 4)

conclusions

~cop(1, 2, 4, 3)
~cop(1, 3, 2, 4)
~cop(1, 3, 4, 2)
~cop(1, 4, 2, 3)
~cop(1, 4, 3, 2)
~cop(2, 1, 3, 4)
~cop(2, 1, 4, 3)
~cop(2, 3, 1, 4)
~cop(2, 3, 4, 1)
~cop(2, 4, 1, 3)
~cop(2, 4, 3, 1)
~cop(3, 1, 2, 4)
~cop(3, 1, 4, 2)
~cop(3, 2, 1, 4)
~cop(3, 2, 4, 1)
~cop(3, 4, 1, 2)
~cop(3, 4, 2, 1)
~cop(4, 1, 2, 3)
~cop(4, 1, 3, 2)
~cop(4, 2, 1, 3)
~cop(4, 2, 3, 1)
~cop(4, 3, 1, 2)
~cop(4, 3, 2, 1)

premises
#ax_sym_nint_l_l

line(1)
line(2)
~int_l_l(1, 2)

conclusions

~int_l_l(2, 1)

premises
#ax_sym_nint_pl_pl

plane(1)
plane(2)
~int_pl_pl(1, 2)

conclusions

~int_pl_pl(2, 1)

