cnf(2,axiom,(e_twoway(e_paris,e_chartres)),file('graph.tstp', c_0_2)).
cnf(7,axiom,(e_twoway(e_chartres,e_lemans)),file('graph.tstp', c_0_7)).
cnf(8,axiom,(e_twoway(e_lemans,e_angers)),file('graph.tstp', c_0_8)).
cnf(10,axiom,(e_oneway(e_angers,e_nantes)),file('graph.tstp', c_0_10)).
cnf(11,axiom,(e_path(X1,X2)|~e_oneway(X1,X2)),file('graph.tstp', c_0_11)).
cnf(13,axiom,(e_path(X1,X2)|~e_twoway(X2,X1)),file('graph.tstp', c_0_13)).
cnf(14,axiom,(e_twoway(X1,X2)|~e_twoway(X2,X1)),file('graph.tstp', c_0_14)).
cnf(15,axiom,(e_path(X1,X2)|~e_path(X1,X3)|~e_path(X3,X2)),file('graph.tstp', c_0_15)).
cnf(16,axiom,(e_parijs=e_paris),file('graph.tstp', c_0_16)).
cnf(17,axiom,(e_path(X1,X2)=e_route(X1,X2)),file('graph.tstp', c_0_17)).
cnf(18,conjecture,(~e_route(e_parijs,e_nantes)),file('graph.tstp', c_0_18)).
cnf(19,conjecture-derived,(~e_path(e_parijs,e_nantes)),inference(rw,[status(thm)],[18,17,theory(equality)]),['unfolding']).
cnf(20,conjecture-derived,(~e_path(e_paris,e_nantes)),inference(rw,[status(thm)],[19,16,theory(equality)])).
cnf(22,derived,(e_twoway(e_chartres,e_paris)),inference(spm,[status(thm)],[14,2,theory(equality)])).
cnf(26,derived,(e_twoway(e_lemans,e_chartres)),inference(spm,[status(thm)],[14,7,theory(equality)])).
cnf(29,derived,(e_twoway(e_angers,e_lemans)),inference(spm,[status(thm)],[14,8,theory(equality)])).
cnf(31,derived,(e_path(e_angers,e_nantes)),inference(spm,[status(thm)],[11,10,theory(equality)])).
cnf(33,derived,(e_path(X1,X2)|~e_path(X1,X3)|~e_twoway(X2,X3)),inference(spm,[status(thm)],[15,13,theory(equality)])).
cnf(52,derived,(e_path(X1,e_nantes)|~e_path(X1,e_angers)),inference(spm,[status(thm)],[15,31,theory(equality)])).
cnf(55,conjecture-derived,(~e_path(e_paris,e_angers)),inference(spm,[status(thm)],[20,52,theory(equality)])).
cnf(71,derived,(e_path(X1,e_lemans)|~e_path(X1,e_chartres)),inference(spm,[status(thm)],[33,26,theory(equality)])).
cnf(74,derived,(e_path(X1,e_angers)|~e_path(X1,e_lemans)),inference(spm,[status(thm)],[33,29,theory(equality)])).
cnf(125,derived,(e_path(X1,e_lemans)|~e_twoway(e_chartres,X1)),inference(spm,[status(thm)],[71,13,theory(equality)])).
cnf(135,conjecture-derived,(~e_path(e_paris,e_lemans)),inference(spm,[status(thm)],[55,74,theory(equality)])).
cnf(179,conjecture-derived,(~e_twoway(e_chartres,e_paris)),inference(spm,[status(thm)],[135,125,theory(equality)])).
cnf(183,conjecture-derived,($false),inference(rw,[status(thm)],[179,22,theory(equality)])).
cnf(184,conjecture-derived,($false),inference(cn,[status(thm)],[183,theory(equality)])).
cnf(185,conjecture-derived,($false),184,['proof']).