[()]
[()]
[()]
[()]
[()]
[()]
[()]
[()]
[()]
[(: ((r8 ((r8 r3) r4)) ((r8 r6) ((r7 r1) r2))) (≤ 7 (plus 3 9))), (: ((r8 ((r8 r4) r6)) ((r7 r1) ((r8 r3) r2))) (≤ 7 (plus 3 9))), (: ((r8 ((r8 r4) r6)) ((r7 r1) ((r8 r2) r3))) (≤ 7 (plus 3 9))), (: ((r8 ((r8 r4) r6)) ((r7 r1) r2)) (≤ 7 (plus 3 9))), (: ((r8 ((r8 r4) r6)) ((r8 r3) ((r7 r1) r2))) (≤ 7 (plus 3 9))), (: ((r8 ((r8 r4) r3)) ((r8 r6) ((r7 r1) r2))) (≤ 7 (plus 3 9))), (: ((r8 ((r8 r2) r4)) ((r8 r6) ((r7 r1) r3))) (≤ 7 (plus 3 9))), (: ((r8 r4) ((r8 r6) ((r7 r1) r2))) (≤ 7 (plus 3 9)))]
20.40user 0.02system 0:20.43elapsed 99%CPU (0avgtext+0avgdata 67040maxresident)k
0inputs+0outputs (0major+11829minor)pagefaults 0swaps