YES
0 QTRS
↳1 QTRS Reverse (⇔, 0 ms)
↳2 QTRS
↳3 QTRSRoofMatchBoundsTAProof (⇔, 832 ms)
↳4 YES
0(1(2(1(x)))) → 1(2(1(1(0(1(2(0(1(2(x))))))))))
0(1(2(1(x)))) → 1(2(1(1(0(1(2(0(1(2(0(1(2(x)))))))))))))
0(1(2(1(x)))) → 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(x))))))))))))))))
0(1(2(1(x)))) → 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x)))))))))))))))))))
0(1(2(1(x)))) → 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x))))))))))))))))))))))
0(1(2(1(x)))) → 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x)))))))))))))))))))))))))
0(1(2(1(x)))) → 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x))))))))))))))))))))))))))))
0(1(2(1(x)))) → 1(2(1(1(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(0(1(2(x)))))))))))))))))))))))))))))))
1(2(1(0(x)))) → 2(1(0(2(1(0(1(1(2(1(x))))))))))
1(2(1(0(x)))) → 2(1(0(2(1(0(2(1(0(1(1(2(1(x)))))))))))))
1(2(1(0(x)))) → 2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x))))))))))))))))
1(2(1(0(x)))) → 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x)))))))))))))))))))
1(2(1(0(x)))) → 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x))))))))))))))))))))))
1(2(1(0(x)))) → 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x)))))))))))))))))))))))))
1(2(1(0(x)))) → 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x))))))))))))))))))))))))))))
1(2(1(0(x)))) → 2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(2(1(0(1(1(2(1(x)))))))))))))))))))))))))))))))