| sub: | let (_x_0 : op_choice) = List.hd choices in
+((calc _x_0) :: (rest _x_0.two (rest _x_0.one nums))) target` from `apply_choices choices nums target`| original: | apply_choices choices nums target | | sub: | let (_x_0 : op_choice) = List.hd choices in
apply_choices (List.tl choices)
((calc _x_0) :: (rest _x_0.two (rest _x_0.one nums))) target | | original ordinal: | Ordinal.Int (_cnt choices) | | sub ordinal: | Ordinal.Int (_cnt (List.tl choices)) | | path: | [let (_x_0 : op_choice) = List.hd choices in
let (_x_1 : int list) = rest _x_0.one nums in
@@ -4116,12 +4142,12 @@
&& List.is_empty (List.tl choices))
&& valid_choice (List.hd choices) nums
&& choices <> []
- && List.length choices < List.length nums] | | proof: | | ground_instances: | 9 | | definitions: | 0 | | inductions: | 0 | | search_time: | 0.024s | | details: | | smt_stats: | | arith offset eqs: | 13 | | num checks: | 20 | | arith assert lower: | 85 | | arith tableau max rows: | 40 | | arith tableau max columns: | 76 | | arith pivots: | 27 | | rlimit count: | 30610 | | mk clause: | 340 | | datatype occurs check: | 216 | | mk bool var: | 499 | | arith assert upper: | 226 | | datatype splits: | 91 | | decisions: | 1158 | | arith row summations: | 78 | | arith bound prop: | 4 | | propagations: | 1272 | | interface eqs: | 2 | | conflicts: | 30 | | arith fixed eqs: | 27 | | arith assume eqs: | 2 | | datatype accessor ax: | 34 | | minimized lits: | 5 | | arith conflicts: | 4 | | arith num rows: | 40 | | arith assert diseq: | 116 | | datatype constructor ax: | 70 | | num allocs: | 49276706 | | final checks: | 27 | | added eqs: | 578 | | del clause: | 58 | | arith eq adapter: | 73 | | memory: | 17.680000 | | max memory: | 17.680000 |
|
|
|
start[0.031s]
let (_x_0 : op_choice) = List.hd choices in
let (_x_1 : int) = _x_0.one in
let (_x_2 : int) = _x_0.two in
@@ -4150,209 +4176,199 @@
else if _x_4 then _x_1 > _x_2 else true))
in
let (_x_9 : int list) = rest _x_1 nums in
- let (_x_10 : int list) = rest _x_2 _x_9 in
- let (_x_11 : int) = _x_1 - _x_2 in
- let (_x_12 : int) = _x_1 + _x_2 in
- let (_x_13 : bool) = _x_3 = Plus in
- let (_x_14 : op_choice list) = List.tl choices in
- let (_x_15 : bool) = _x_14 <> [] in
- let (_x_16 : int) = count.list count.op_choice choices in
- let (_x_17 : int) = count.list count.op_choice _x_14 in
- let (_x_18 : op_choice) = List.hd _x_14 in
- let (_x_19 : int) = _x_18.one in
- let (_x_20 : int list)
- = (if _x_13 then _x_12 else if _x_4 then _x_11 else …) :: _x_10
+ let (_x_10 : op_choice list) = List.tl … in
+ let (_x_11 : int) = count.list count.op_choice _x_10 in
+ let (_x_12 : op_choice) = List.hd _x_10 in
+ let (_x_13 : int) = _x_12.one in
+ let (_x_14 : op_choice) = List.hd … in
+ let (_x_15 : op) = _x_14.op in
+ let (_x_16 : int) = _x_14.one in
+ let (_x_17 : int) = _x_14.two in
+ let (_x_18 : int list)
+ = (if _x_15 = Plus then _x_16 + _x_17
+ else if _x_15 = Minus then … else …)
+ :: (rest _x_17 (rest _x_16 …))
in
- let (_x_21 : int) = _x_18.two in
- let (_x_22 : op) = _x_18.op in
- let (_x_23 : bool) = _x_22 = Minus in
- let (_x_24 : bool) = _x_21 >= 0 in
- let (_x_25 : bool) = _x_19 >= 0 in
- let (_x_26 : bool)
- = List.mem _x_19 _x_20
- && (List.mem _x_21 _x_20
- && (if _x_22 = Divides
+ let (_x_19 : int) = _x_12.two in
+ let (_x_20 : op) = _x_12.op in
+ let (_x_21 : bool) = _x_20 = Minus in
+ let (_x_22 : bool) = _x_19 >= 0 in
+ let (_x_23 : bool) = _x_13 >= 0 in
+ let (_x_24 : bool)
+ = List.mem _x_13 _x_18
+ && (List.mem _x_19 _x_18
+ && (if _x_20 = Divides
then
- not (_x_19 = 0)
- && (not (_x_19 = 1)
- && (not (_x_21 = 1)
- && (not (_x_21 = 0)
- && ((if _x_25
+ not (_x_13 = 0)
+ && (not (_x_13 = 1)
+ && (not (_x_19 = 1)
+ && (not (_x_19 = 0)
+ && ((if _x_23
then
- if _x_24 then R.mod_psd _x_19 _x_21
- else 0 - R.mod_psd _x_19 …
+ if _x_22 then R.mod_psd _x_13 _x_19
+ else 0 - R.mod_psd _x_13 …
else
- if _x_24 then 0 - R.mod_psd … _x_21
+ if _x_22 then 0 - R.mod_psd … _x_19
else _x_5)
= 0))))
- else if _x_23 then _x_19 > _x_21 else true))
+ else if _x_21 then _x_13 > _x_19 else true))
in
- let (_x_27 : int list) = rest _x_19 _x_20 in
+ let (_x_25 : int list) = rest _x_13 _x_18 in
not
(_x_8
&& (choose_and_rest _x_1 nums _x_9
- && (choose_and_rest _x_2 _x_9 _x_10
- && ((if _x_13 then _x_12
+ && (choose_and_rest _x_2 _x_9 (rest _x_2 _x_9)
+ && ((if _x_3 = Plus then _x_1 + _x_2
else
- if _x_4 then _x_11
+ if _x_4 then _x_1 - _x_2
else
if _x_3 = Times then R.( * ) _x_1 _x_2
else if _x_7 then … else …)
= target)))
- && not _x_15)
+ && not ((List.tl choices) <> []))
&& (_x_8
&& (choices <> []
&& ((List.length choices < List.length nums)
- && ((_x_16 >= 0) && (_x_17 >= 0)))))
+ && ((count.list count.op_choice choices >= 0) && (_x_11 >= 0)))))
==> not
(not
- (_x_26
- && (choose_and_rest _x_19 _x_20 _x_27
- && (choose_and_rest _x_21 _x_27 (rest _x_21 _x_27)
- && ((if _x_22 = Plus then _x_19 + _x_21
+ (_x_24
+ && (choose_and_rest _x_13 _x_18 _x_25
+ && (choose_and_rest _x_19 _x_25 (rest _x_19 _x_25)
+ && ((if _x_20 = Plus then _x_13 + _x_19
else
- if _x_23 then _x_19 - _x_21
+ if _x_21 then _x_13 - _x_19
else
- if _x_22 = Times then R.( * ) _x_19 _x_21
- else if _x_25 then … else …)
+ if _x_20 = Times then R.( * ) _x_13 _x_19
+ else if _x_23 then … else …)
= target)))
- && not ((List.tl _x_14) <> []))
- && (_x_26 && (_x_15 && (List.length _x_14 < List.length _x_20))))
- || Ordinal.( << ) (Ordinal.Int _x_17) (Ordinal.Int _x_16)simplify| into: | let (_x_0 : op_choice list) = List.tl choices in
-let (_x_1 : int) = count.list count.op_choice _x_0 in
-let (_x_2 : int) = count.list count.op_choice choices in
-let (_x_3 : op_choice) = List.hd _x_0 in
-let (_x_4 : int) = _x_3.one in
-let (_x_5 : op_choice) = List.hd choices in
-let (_x_6 : int) = _x_5.one in
-let (_x_7 : int) = (-1) * _x_6 in
-let (_x_8 : int) = _x_5.two in
-let (_x_9 : int) = (-1) * _x_8 in
-let (_x_10 : bool) = _x_8 >= 0 in
-let (_x_11 : bool) = _x_6 >= 0 in
-let (_x_12 : int) = R.( * ) _x_6 _x_8 in
-let (_x_13 : op) = _x_5.op in
-let (_x_14 : bool) = _x_13 = Times in
-let (_x_15 : bool) = _x_13 = Minus in
-let (_x_16 : int) = _x_6 + _x_8 in
-let (_x_17 : bool) = _x_13 = Plus in
-let (_x_18 : int list) = rest _x_6 nums in
-let (_x_19 : int list) = rest _x_8 _x_18 in
-let (_x_20 : int list)
- = (if _x_17 then _x_16
- else
- if _x_15 then _x_6 + _x_9
- else
- if _x_14 then _x_12
- else
- if _x_11
- then if _x_10 then R.div_psd _x_6 _x_8 else (-1) * R.div_psd _x_6 _x_9
- else
- if _x_10 then (-1) * R.div_psd _x_7 _x_8
- else (-1) * R.div_psd _x_7 _x_9)
- :: _x_19
+ && not ((List.tl _x_10) <> []))
+ && (_x_24 && (_x_10 <> [] && (List.length _x_10 < List.length _x_18))))
+ || Ordinal.( << ) (Ordinal.Int _x_11)
+ (Ordinal.Int (count.list count.op_choice …)) simplify| into: | let (_x_0 : op_choice list) = List.tl … in
+let (_x_1 : op_choice) = List.hd _x_0 in
+let (_x_2 : int) = _x_1.one in
+let (_x_3 : op_choice) = List.hd … in
+let (_x_4 : op) = _x_3.op in
+let (_x_5 : int) = _x_3.one in
+let (_x_6 : int) = _x_3.two in
+let (_x_7 : int list)
+ = (if _x_4 = Plus then _x_5 + _x_6 else if _x_4 = Minus then … else …)
+ :: (rest _x_6 (rest _x_5 …))
in
-let (_x_21 : bool) = List.mem _x_4 _x_20 in
-let (_x_22 : int) = _x_3.two in
-let (_x_23 : bool) = List.mem _x_22 _x_20 in
-let (_x_24 : op) = _x_3.op in
-let (_x_25 : bool) = _x_24 = Minus in
-let (_x_26 : int) = (-1) * R.mod_psd … … in
-let (_x_27 : bool) = _x_22 >= 0 in
-let (_x_28 : bool) = _x_4 >= 0 in
-let (_x_29 : bool)
- = if _x_24 = Divides
+let (_x_8 : bool) = List.mem _x_2 _x_7 in
+let (_x_9 : int) = _x_1.two in
+let (_x_10 : bool) = List.mem _x_9 _x_7 in
+let (_x_11 : op) = _x_1.op in
+let (_x_12 : bool) = _x_11 = Minus in
+let (_x_13 : int) = (-1) * R.mod_psd … … in
+let (_x_14 : bool) = _x_9 >= 0 in
+let (_x_15 : bool) = _x_2 >= 0 in
+let (_x_16 : bool)
+ = if _x_11 = Divides
then
- not (_x_4 = 0) && not (_x_4 = 1) && not (_x_22 = 1)
- && not (_x_22 = 0)
- && ((if _x_28
+ not (_x_2 = 0) && not (_x_2 = 1) && not (_x_9 = 1) && not (_x_9 = 0)
+ && ((if _x_15
then
- if _x_27 then R.mod_psd _x_4 _x_22
- else (-1) * R.mod_psd _x_4 …
- else if _x_27 then (-1) * R.mod_psd … _x_22 else _x_26)
+ if _x_14 then R.mod_psd _x_2 _x_9
+ else (-1) * R.mod_psd _x_2 …
+ else if _x_14 then (-1) * R.mod_psd … _x_9 else _x_13)
= 0)
- else not (_x_4 <= _x_22) || not _x_25
+ else not (_x_2 <= _x_9) || not _x_12
in
-let (_x_30 : int list) = rest _x_4 _x_20 in
-let (_x_31 : bool) = _x_0 <> [] in
-let (_x_32 : bool) = List.mem _x_6 nums in
-let (_x_33 : bool) = List.mem _x_8 nums in
-let (_x_34 : bool)
- = if _x_13 = Divides
+let (_x_17 : int list) = rest _x_2 _x_7 in
+let (_x_18 : op_choice) = List.hd choices in
+let (_x_19 : int) = _x_18.one in
+let (_x_20 : bool) = List.mem _x_19 nums in
+let (_x_21 : int) = _x_18.two in
+let (_x_22 : bool) = List.mem _x_21 nums in
+let (_x_23 : op) = _x_18.op in
+let (_x_24 : bool) = _x_23 = Minus in
+let (_x_25 : bool) = _x_21 >= 0 in
+let (_x_26 : bool) = _x_19 >= 0 in
+let (_x_27 : bool)
+ = if _x_23 = Divides
then
- not (_x_6 = 0) && not (_x_6 = 1) && not (_x_8 = 1) && not (_x_8 = 0)
- && ((if _x_11
+ not (_x_19 = 0) && not (_x_19 = 1) && not (_x_21 = 1)
+ && not (_x_21 = 0)
+ && ((if _x_26
then
- if _x_10 then R.mod_psd _x_6 _x_8
- else (-1) * R.mod_psd _x_6 …
- else if _x_10 then (-1) * R.mod_psd … _x_8 else _x_26)
+ if _x_25 then R.mod_psd _x_19 _x_21
+ else (-1) * R.mod_psd _x_19 …
+ else if _x_25 then (-1) * R.mod_psd … _x_21 else _x_13)
= 0)
- else not (_x_6 <= _x_8) || not _x_15
+ else not (_x_19 <= _x_21) || not _x_24
in
-Ordinal.( << ) (Ordinal.Int _x_1) (Ordinal.Int _x_2)
+let (_x_28 : int list) = rest _x_19 nums in
+let (_x_29 : op_choice list) = List.tl choices in
+Ordinal.( << ) (Ordinal.Int (count.list count.op_choice _x_0))
+(Ordinal.Int (count.list count.op_choice …))
|| not
(not
- (_x_21 && _x_23 && _x_29 && choose_and_rest _x_4 _x_20 _x_30
- && choose_and_rest _x_22 _x_30 (rest _x_22 _x_30)
- && ((if _x_24 = Plus then _x_4 + _x_22
+ (_x_8 && _x_10 && _x_16 && choose_and_rest _x_2 _x_7 _x_17
+ && choose_and_rest _x_9 _x_17 (rest _x_9 _x_17)
+ && ((if _x_11 = Plus then _x_2 + _x_9
else
- if _x_25 then _x_4 + …
+ if _x_12 then _x_2 + …
else
- if _x_24 = Times then R.( * ) _x_4 _x_22
- else if _x_28 then … else …)
+ if _x_11 = Times then R.( * ) _x_2 _x_9
+ else if _x_15 then … else …)
= target)
&& not ((List.tl _x_0) <> []))
- && _x_21 && _x_23 && _x_29 && _x_31
- && not (List.length _x_20 <= List.length _x_0))
+ && _x_8 && _x_10 && _x_16 && _x_0 <> []
+ && not (List.length _x_7 <= List.length _x_0))
|| not
(not
- (_x_32 && _x_33 && _x_34 && choose_and_rest _x_6 nums _x_18
- && choose_and_rest _x_8 _x_18 _x_19
- && ((if _x_17 then _x_16
+ (_x_20 && _x_22 && _x_27 && choose_and_rest _x_19 nums _x_28
+ && choose_and_rest _x_21 _x_28 (rest _x_21 _x_28)
+ && ((if _x_23 = Plus then _x_19 + _x_21
+ else
+ if _x_24 then _x_19 + …
else
- if _x_15 then _x_6 + …
- else if _x_14 then _x_12 else if _x_11 then … else …)
+ if _x_23 = Times then R.( * ) _x_19 _x_21
+ else if _x_26 then … else …)
= target)
- && not _x_31)
- && _x_32 && _x_33 && _x_34 && choices <> []
- && not (List.length nums <= List.length choices) && (_x_2 >= 0)
- && (_x_1 >= 0)) | | expansions: | [] | | rewrite_steps: | | | forward_chaining: | |
unroll | expr: | (let ((a!1 (+ (one_1289/client (|get.::.0_698/server| choices_720/server))
+ && not (_x_29 <> []))
+ && _x_20 && _x_22 && _x_27 && choices <> []
+ && not (List.length nums <= List.length choices)
+ && (count.list count.op_choice choices >= 0)
+ && (count.list count.op_choice _x_29 >= 0)) | | expansions: | [] | | rewrite_steps: | | | forward_chaining: | |
unroll | expr: | (let ((a!1 (+ (one_1294/client (|get.::.0_699/server| choices_721/server))
(* (- 1)
- … | | expansions: | |
unroll | expr: | (let ((a!1 (+ (one_1289/client (|get.::.0_698/server| choices_720/server))
+ … | | expansions: | |
unroll | expr: | (let ((a!1 (+ (one_1294/client (|get.::.0_699/server| choices_721/server))
(* (- 1)
- … | | expansions: | |
unroll | expr: | (let ((a!1 (+ (one_1289/client (|get.::.0_698/server| choices_720/server))
+ … | | expansions: | |
unroll | expr: | (let ((a!1 (+ (one_1294/client (|get.::.0_699/server| choices_721/server))
(* (- 1)
- … | | expansions: | |
unroll | expr: | (let ((a!1 (+ (one_1289/client (|get.::.0_698/server| choices_720/server))
+ … | | expansions: | |
unroll | expr: | (let ((a!1 (+ (one_1294/client (|get.::.0_699/server| choices_721/server))
(* (- 1)
- … | | expansions: | |
unroll | expr: | (let ((a!1 (* (- 1)
- (one_1289/client (|get.::.0_698/server|
- … | | expansions: | |
unroll | expr: | (let ((a!1 (+ (one_1289/client (|get.::.0_698/server| choices_720/server))
+ … | | expansions: | |
unroll | expr: | (let ((a!1 (* (- 1)
+ (one_1294/client (|get.::.0_699/server|
+ … | | expansions: | |
unroll | expr: | (let ((a!1 (+ (one_1294/client (|get.::.0_699/server| choices_721/server))
(* (- 1)
- … | | expansions: | |
unroll | expr: | (|Ordinal.<<| (|Ordinal.Int_79/boot|
- (|count.list_735/server|
- (|ge… | | expansions: | |
unroll | expr: | (|count.list_735/server| (|get.::.1_699/server| choices_720/server)) | | expansions: | |
unroll | expr: | (|count.list_735/server| choices_720/server) | | expansions: | |
- Unsat
|
- Instance (after 74 steps, 0.253s):
+Instance (after 79 steps, 0.287s):
let cs : op_choice list =
[{op = Times; one = 3; two = 5}; {op = Plus; one = 15; two = 2}]
- Instance | ground_instances: | 74 | | definitions: | 0 | | inductions: | 0 | | search_time: | 0.253s | | details: | | smt_stats: | | arith offset eqs: | 4920 | | arith assert lower: | 6606 | | arith patches_succ: | 2 | | datatype occurs check: | 6560 | | datatype splits: | 1356 | | arith bound prop: | 823 | | arith branch var: | 6 | | propagations: | 48639 | | arith patches: | 8 | | interface eqs: | 201 | | conflicts: | 368 | | arith fixed eqs: | 4187 | | datatype constructor ax: | 1771 | | num allocs: | 113183241 | | final checks: | 455 | | added eqs: | 36688 | | del clause: | 4957 | | num checks: | 149 | | arith tableau max rows: | 197 | | arith tableau max columns: | 335 | | arith pivots: | 1127 | | rlimit count: | 588040 | | mk clause: | 7255 | | mk bool var: | 14329 | | arith gcd tests: | 144 | | arith assert upper: | 6085 | | decisions: | 18676 | | arith row summations: | 9192 | | arith assume eqs: | 205 | | datatype accessor ax: | 856 | | minimized lits: | 296 | | arith conflicts: | 60 | | arith num rows: | 197 | | arith assert diseq: | 4104 | | arith ineq splits: | 6 | | arith eq adapter: | 4559 | | time: | 0.007000 | | memory: | 22.420000 | | max memory: | 22.420000 |
|
| ground_instances: | 79 | | definitions: | 0 | | inductions: | 0 | | search_time: | 0.287s | | details: | | smt_stats: | | arith offset eqs: | 4561 | | arith assert lower: | 6798 | | datatype occurs check: | 5092 | | datatype splits: | 846 | | arith bound prop: | 713 | | arith branch var: | 2 | | propagations: | 53449 | | arith patches: | 2 | | interface eqs: | 149 | | conflicts: | 385 | | arith fixed eqs: | 4326 | | datatype constructor ax: | 1619 | | num allocs: | 115238853 | | final checks: | 376 | | added eqs: | 38765 | | del clause: | 4251 | | num checks: | 159 | | arith tableau max rows: | 185 | | arith tableau max columns: | 327 | | arith pivots: | 1008 | | rlimit count: | 588581 | | mk clause: | 6552 | | mk bool var: | 13519 | | arith gcd tests: | 29 | | arith assert upper: | 7313 | | decisions: | 17204 | | arith row summations: | 9500 | | arith assume eqs: | 155 | | datatype accessor ax: | 732 | | minimized lits: | 502 | | arith conflicts: | 31 | | arith num rows: | 185 | | arith assert diseq: | 4655 | | arith ineq splits: | 2 | | arith eq adapter: | 4657 | | time: | 0.006000 | | memory: | 22.260000 | | max memory: | 22.260000 |
|
|
| | expansions: | |
unroll | expr: | (let ((a!1 (|::| 2 (|::| 3 (|::| 4 (|::| 5 |[]|))))))
+(let ((a!2 (rest_1306/client (two_1295/client … | | expansions: | |
unroll | expr: | (let ((a!1 (|::| 2 (|::| 3 (|::| 4 (|::| 5 |[]|))))))
+(let ((a!2 (rest_1306/client (two_1295/client … | | expansions: | |
unroll | expr: | (let ((a!1 (|::| 2 (|::| 3 (|::| 4 (|::| 5 |[]|))))))
+(let ((a!2 (rest_1306/client (two_1295/client … | | expansions: | |
unroll | expr: | (let ((a!1 (ite (<= 0 (one_1294/client (|get.::.0_949/server| cs_1332/client)))
+ (|R.… | | expansions: | |
-
-
-
-
- Unknown (Verified up to bound 100) | expanded: | - List.mem (List.hd (List.tl x)).one
-((calc …) :: (rest ….two (rest ….one (List.rev …))))
- let (_x_0 : op_choice) = List.hd (List.tl x) in
-let (_x_1 : op_choice) = List.hd x in
-rest _x_0.two (rest _x_0.one ((calc _x_1) :: (rest _x_1.two (rest … …))))
- List.mem (List.hd x).one (List.tl nums)
- List.length (List.tl (List.tl (List.rev nums)))
- let (_x_0 : int) = ….one in
-let (_x_1 : int list) = List.rev … in
-choose_and_rest _x_0 (List.tl _x_1) ((List.hd _x_1) :: (rest _x_0 _x_1))
- List.length (List.tl (List.tl (List.tl (List.tl (List.rev …)))))
- rest ….two (rest ….one (List.rev …))
- let (_x_0 : int list) = List.tl … in
-choose_and_rest … (List.tl _x_0)
-((List.hd _x_0) :: ((List.hd …) :: (rest … …)))
- List.length (List.tl (List.tl (List.tl (List.tl (List.tl …)))))
- List.length (List.tl (rest ….two (rest ….one …)))
- let (_x_0 : op_choice) = List.hd x in
-apply_choices (List.tl x)
-((calc _x_0) :: (rest _x_0.two (rest _x_0.one (List.rev nums)))) target
- List.length (List.tl (List.tl (List.tl (List.tl nums))))
- List.rev nums
- List.mem (List.hd x).one (List.tl (List.rev nums))
- List.length (List.tl x)
- let (_x_0 : op_choice) = List.hd (List.tl x) in R.div_psd _x_0.one _x_0.two
- let (_x_0 : op_choice) = List.hd x in
-let (_x_1 : int) = _x_0.two in
-let (_x_2 : int list) = rest _x_0.one nums in
-choose_and_rest _x_1 _x_2 (rest _x_1 _x_2)
- let (_x_0 : int) = (List.hd (List.tl x)).one in
-let (_x_1 : op_choice) = List.hd x in
-let (_x_2 : int list) = (calc _x_1) :: (rest _x_1.two (rest … …)) in
-choose_and_rest _x_0 _x_2 (rest _x_0 _x_2)
- List.append (List.tl (List.tl (List.tl (List.tl (List.rev (List.tl …))))))
-[List.hd …]
- let (_x_0 : op_choice) = List.hd x in R.div_psd _x_0.one (R.( - ) 0 _x_0.two)
- List.length (List.rev nums)
- let (_x_0 : op_choice) = List.hd x in
-R.mod_psd (R.( - ) 0 _x_0.one) (R.( - ) 0 _x_0.two)
- List.length (List.tl (List.tl nums))
- List.mem (List.hd x).two (List.tl (List.tl (List.rev …)))
- let (_x_0 : int list) = List.rev … in
-let (_x_1 : int list) = rest ….one _x_0 in
-choose_and_rest (List.hd x).two (List.tl (rest … _x_0))
-((List.hd _x_1) :: (rest ….two _x_1))
- let (_x_0 : op_choice) = List.hd (List.tl x) in R.( * ) _x_0.one _x_0.two
- let (_x_0 : int) = (List.hd x).one in
-let (_x_1 : int list) = List.rev nums in
-choose_and_rest _x_0 _x_1 (rest _x_0 _x_1)
- let (_x_0 : op_choice) = List.hd x in R.mod_psd _x_0.one _x_0.two
- let (_x_0 : int) = R.( - ) 0 (List.hd x).two in
-R.div_psd (R.( - ) … _x_0) _x_0
- List.rev (List.tl nums)
- let (_x_0 : int list) = List.tl (List.tl (List.tl (List.tl …))) in
-List.append (List.rev (List.tl _x_0)) [List.hd _x_0]
- let (_x_0 : op_choice) = List.hd x in
-List.length ((calc _x_0) :: (rest _x_0.two (rest _x_0.one (List.rev nums))))
- let (_x_0 : int) = (List.hd x).one in
-choose_and_rest _x_0 (List.tl nums) ((List.hd nums) :: (rest _x_0 nums))
- List.rev (List.tl (List.tl (List.tl nums)))
- let (_x_0 : op_choice) = List.hd (List.tl x) in
-R.div_psd _x_0.one (R.( - ) 0 _x_0.two)
- let (_x_0 : int list) = List.tl (List.tl (List.tl …)) in
-List.append (List.tl (List.rev (List.tl _x_0))) [List.hd _x_0]
- let (_x_0 : int) = (List.hd x).two in
-let (_x_1 : int list) = rest … … in
-choose_and_rest _x_0 (List.tl _x_1) ((List.hd _x_1) :: (rest _x_0 _x_1))
- List.length (List.tl (List.tl x))
- List.length (List.tl (List.tl (List.tl (List.tl (List.tl (List.rev …))))))
- List.mem (List.hd x).two nums
- apply_choices x nums target
- rest (List.hd x).one nums
- let (_x_0 : int list) = List.tl (List.tl (List.tl nums)) in
-List.append (List.rev (List.tl _x_0)) [List.hd _x_0]
- let (_x_0 : op_choice) = List.hd x in
-List.length (rest _x_0.two (rest _x_0.one nums))
- List.length (List.tl (List.tl (List.tl (List.rev nums))))
- List.mem … (List.tl (List.tl (List.rev …)))
- let (_x_0 : op_choice) = List.hd x in
-List.mem (List.hd (List.tl x)).two
-((calc _x_0) :: (rest _x_0.two (rest … …)))
- let (_x_0 : int) = (List.hd x).two in
-R.div_psd (R.( - ) (R.( - ) 0 …) _x_0) _x_0
- let (_x_0 : op_choice) = List.hd x in
-R.div_psd (R.( - ) 0 _x_0.one) (R.( - ) 0 _x_0.two)
- let (_x_0 : int list) = List.tl nums in
-List.append (List.tl (List.rev (List.tl _x_0))) [List.hd _x_0]
- List.length (rest (List.hd x).two (rest … (List.rev …)))
- let (_x_0 : op_choice) = List.hd x in
-rest (List.hd (List.tl x)).one
-((calc _x_0) :: (rest _x_0.two (rest _x_0.one nums)))
- let (_x_0 : op_choice) = List.hd x in R.div_psd _x_0.one _x_0.two
- List.length nums
- let (_x_0 : op_choice) = List.hd x in R.mod_psd (R.( - ) 0 _x_0.one) _x_0.two
- let (_x_0 : int list) = List.tl (List.tl nums) in
-List.append (List.tl (List.rev (List.tl _x_0))) [List.hd _x_0]
- let (_x_0 : op_choice) = List.hd x in
-let (_x_1 : int) = _x_0.two in
-let (_x_2 : int list) = rest _x_0.one (List.rev nums) in
-choose_and_rest _x_1 _x_2 (rest _x_1 _x_2)
- List.rev (List.tl (List.tl (List.tl (List.tl (List.tl nums)))))
- let (_x_0 : op_choice) = List.hd x in R.( * ) _x_0.one _x_0.two
- List.mem (List.hd x).one nums
- let (_x_0 : int) = (List.hd x).one in
-choose_and_rest _x_0 nums (rest _x_0 nums)
- let (_x_0 : op_choice) = List.hd (List.tl x) in
-R.div_psd (R.( - ) 0 _x_0.one) _x_0.two
- List.mem (List.hd x).two (List.rev nums)
- apply_choices x (List.rev nums) target
- List.rev (List.tl (List.tl (List.tl (List.tl nums))))
- let (_x_0 : op_choice) = List.hd x in
-List.length ((calc _x_0) :: (rest _x_0.two (rest _x_0.one nums)))
- rest (List.hd x).one (List.rev nums)
- let (_x_0 : op_choice) = List.hd x in rest _x_0.two (rest _x_0.one nums)
- let (_x_0 : int list) = List.tl (List.tl nums) in
-List.append (List.rev (List.tl _x_0)) [List.hd _x_0]
- List.mem (List.hd (List.tl x)).two
-((calc …) :: (rest ….two (rest ….one (List.rev …))))
- rest … (List.tl (List.tl …))
- let (_x_0 : op_choice) = List.hd x in
-List.mem (List.hd (List.tl x)).one
-((calc _x_0) :: (rest _x_0.two (rest _x_0.one nums)))
- List.mem (List.hd x).two (List.tl nums)
- List.length (List.tl nums)
- rest (List.hd x).one (List.tl nums)
- List.append (List.tl (List.tl (List.tl (List.rev (List.tl nums)))))
-[List.hd nums]
- List.length (List.tl (List.tl (List.tl nums)))
- let (_x_0 : int list) = List.tl … in
-List.append (List.tl (List.tl (List.tl (List.rev (List.tl _x_0)))))
-[List.hd _x_0]
- List.rev (List.tl (List.tl nums))
- List.length (List.tl (List.rev nums))
- let (_x_0 : op_choice) = List.hd (List.tl x) in
-R.div_psd (R.( - ) 0 _x_0.one) (R.( - ) 0 _x_0.two)
- let (_x_0 : op_choice) = List.hd (List.tl x) in
+
+
+
+
+ Unknown (Verified up to bound 100) | ground_instances: | 100 | | definitions: | 0 | | inductions: | 0 | | search_time: | 0.351s |
| ground_instances: | 100 | | definitions: | 0 | | inductions: | 0 | | search_time: | 0.379s |
|
|
-
+