97 slice = false, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, |
97 slice = false, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, |
98 expect = ""} |
98 expect = ""} |
99 val problem = |
99 val problem = |
100 {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, |
100 {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n, |
101 factss = [("", facts)]} |
101 factss = [("", facts)]} |
102 val result as {outcome, used_facts, run_time, ...} = prover params problem |
102 val result0 as {outcome = outcome0, used_facts, used_from, preferred_methss, run_time, |
|
103 message} = |
|
104 prover params problem |
|
105 val result as {outcome, ...} = |
|
106 if is_none outcome0 andalso |
|
107 forall (member (fn ((s, _), ((s', _), _)) => s = s') used_from) used_facts then |
|
108 result0 |
|
109 else |
|
110 {outcome = SOME MaybeUnprovable, used_facts = [], used_from = used_from, |
|
111 preferred_methss = preferred_methss, run_time = run_time, message = message} |
103 in |
112 in |
104 print silent (fn () => |
113 print silent (fn () => |
105 (case outcome of |
114 (case outcome of |
106 SOME failure => string_of_atp_failure failure |
115 SOME failure => string_of_atp_failure failure |
107 | NONE => |
116 | NONE => |