%% domain declaration
true=>dom(a).
%% domain declaration
true=>dom(b).
%% domain declaration
true=>dom(c).
%% domain declaration
true=>dom(d).
%% domain declaration
true=>dom(e).
%% domain declaration
true=>dom(f).
%% domain declaration
true=>dom(g).
%% domain declaration
true=>dom(h).
%% domain declaration
true=>dom(i).
%% domain declaration
true=>dom(l).
%% domain declaration
true=>dom(m).
%% domain declaration
true=>dom(n).
%% domain declaration
true=>dom(o).
%% domain declaration
true=>dom(p).
%% domain declaration
true=>dom(q).
%% domain declaration
true=>dom(r).
%% domain declaration
true=>dom(s).
%% _G455 axiom assump1
true=>col(a, b, c, l), col(d, e, f, m).
%% _G455 axiom assump2
true=>col(b, f, g, n), col(c, e, g, o).
%% _G455 axiom assump3
true=>col(b, d, h, p), col(a, e, h, q).
%% _G455 axiom assump4
true=>col(c, d, i, r), col(a, f, i, s).
%% _G445 axiom goalam
pl(a, m)=>goal.
%% _G445 axiom goalbm
pl(b, m)=>goal.
%% _G445 axiom goalcm
pl(c, m)=>goal.
%% _G445 axiom goaldl
pl(d, l)=>goal.
%% _G445 axiom goalel
pl(e, l)=>goal.
%% _G445 axiom goalfl
pl(f, l)=>goal.
%% _G459 axiom goal4(_G436)
pl(g, _G436), pl(h, _G436), pl(i, _G436)=>goal.
%% _G455 axiom col_elim1(_G436, _G437, _G438, _G439)
col(_G436, _G437, _G438, _G439)=>pl(_G436, _G439).
%% _G455 axiom col_elim2(_G436, _G437, _G438, _G439)
col(_G436, _G437, _G438, _G439)=>pl(_G437, _G439).
%% _G455 axiom col_elim3(_G436, _G437, _G438, _G439)
col(_G436, _G437, _G438, _G439)=>pl(_G438, _G439).
%% _G451 axiom pref(_G436, _G437)
pl(_G436, _G437)=>ep(_G436, _G436).
%% _G451 axiom psym(_G436, _G437)
ep(_G436, _G437)=>ep(_G437, _G436).
%% _G458 axiom ptra(_G436, _G437, _G438)
ep(_G436, _G437), ep(_G437, _G438)=>ep(_G436, _G438).
%% _G451 axiom lref(_G436, _G437)
pl(_G436, _G437)=>el(_G437, _G437).
%% _G451 axiom lsym(_G436, _G437)
el(_G436, _G437)=>el(_G437, _G436).
%% _G458 axiom ltra(_G436, _G437, _G438)
el(_G436, _G437), el(_G437, _G438)=>el(_G436, _G438).
%% _G458 axiom pcon(_G436, _G437, _G438)
ep(_G436, _G437), pl(_G437, _G438)=>pl(_G436, _G438).
%% _G458 axiom lcon(_G436, _G437, _G438)
pl(_G436, _G437), el(_G437, _G438)=>pl(_G436, _G438).
%% _G549 axiom papp1(_G436, _G437, _G438, _G439, _G440, _G441, _G442, _G443, _G444, _G445, _G446, _G447, _G448, _G449, _G450, _G451, _G452)
col(_G436, _G437, _G438, _G445), col(_G439, _G440, _G441, _G446), col(_G437, _G441, _G442, _G447), col(_G438, _G440, _G442, _G448), col(_G437, _G439, _G443, _G449), col(_G436, _G440, _G443, _G450), col(_G438, _G439, _G444, _G451), col(_G436, _G441, _G444, _G452)=>dom(_G515), col(_G442, _G443, _G444, _G515);el(_G447, _G448);el(_G449, _G450);el(_G451, _G452).
%% _G477 axiom unique(_G436, _G437, _G438, _G439)
pl(_G438, _G436), pl(_G438, _G437), pl(_G439, _G436), pl(_G439, _G437)=>ep(_G438, _G439);el(_G436, _G437).
%% _G468 axiom line(_G436, _G437)
ep(_G436, _G436), ep(_G437, _G437)=>dom(_G448), pl(_G436, _G448), pl(_G437, _G448).
%% _G469 axiom point(_G436, _G437, _G438)
el(_G438, _G438), el(_G437, _G437)=>dom(_G436), pl(_G436, _G437), pl(_G436, _G438).