+let problem_of div convs =\r
+ let rec conv_join = function\r
+ | [] -> "@"\r
+ | x::xs -> conv_join xs ^ " ("^ x ^")" in\r
+ print_hline ();\r
+ let conv = conv_join convs in\r
+ let [@warning "-8"] [div; conv], var_names = parse ([div; conv]) in\r
+ let varno = List.length var_names in\r
+ let p = {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; stepped=[]; phase=`One} in\r
+ (* initial sanity check *)\r
+ sanity p\r
+;;\r
+\r
+let solve p =\r
+ if eta_subterm p.div p.conv\r
+ then print_endline "!!! div is subterm of conv. Problem was not run !!!"\r
+ else check p (auto p)\r
+;;\r
+\r
+let run x y = solve (problem_of x y);;\r
+\r
+(* Example usage of interactive: *)\r
+\r
+(* let interactive div conv cmds =\r