# PxButton # e # eprover -xAuto -tAuto -l4 --tstp-in graph.tstp | epclextract --tstp-out # PxButton # ep # eprover -xAuto -tAuto -l4 --tstp-in graph.tstp | epclextract --tstp-out > graph-proof.tstp cnf(c_0_1, axiom,(e_twoway(e_paris,e_orleans)), unknown). cnf(c_0_2, axiom,(e_twoway(e_paris,e_chartres)), unknown). cnf(c_0_3, axiom,(e_twoway(e_paris,e_amiens)), unknown). cnf(c_0_4, axiom,(e_twoway(e_orleans,e_blois)), unknown). cnf(c_0_5, axiom,(e_twoway(e_orleans,e_bourges)), unknown). cnf(c_0_6, axiom,(e_twoway(e_blois,e_tours)), unknown). cnf(c_0_7, axiom,(e_twoway(e_chartres,e_lemans)), unknown). cnf(c_0_8, axiom,(e_twoway(e_lemans,e_angers)), unknown). cnf(c_0_9, axiom,(e_twoway(e_lemans,e_tours)), unknown). cnf(c_0_10, axiom,(e_oneway(e_angers,e_nantes)), unknown). cnf(c_0_11, axiom,(e_path(X1,X2)|~e_oneway(X1,X2)), unknown). cnf(c_0_12, axiom,(e_oneway(X1,X2)|~e_twoway(X1,X2)), unknown). cnf(c_0_13, axiom,(e_path(X1,X2)|~e_twoway(X2,X1)), unknown). cnf(c_0_14, axiom,(e_twoway(X1,X2)|~e_twoway(X2,X1)), unknown). cnf(c_0_15, axiom,(e_path(X1,X2)|~e_path(X1,X3)|~e_path(X3,X2)), unknown). cnf(c_0_16, axiom,(e_parijs=e_paris), unknown). cnf(c_0_17, axiom,(e_path(X1,X2)=e_route(X1,X2)), unknown). cnf(c_0_18, conjecture,(~e_route(e_parijs,e_nantes)), unknown).