MAYBE 1127.96/299.59 MAYBE 1127.96/299.59 1127.96/299.59 We are left with following problem, upon which TcT provides the 1127.96/299.59 certificate MAYBE. 1127.96/299.59 1127.96/299.59 Strict Trs: 1127.96/299.59 { 0(0(0(0(0(0(0(0(2(1(0(1(2(0(0(2(0(1(0(2(2(2(1(0(2(0(1(1(2(1(0(1(2(1(2(2(2(2(1(2(1(x1))))))))))))))))))))))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 1(1(0(1(1(1(1(1(1(0(1(0(0(2(1(1(2(2(1(1(1(2(2(0(1(0(0(2(0(2(2(2(0(0(0(0(1(1(2(1(1(0(0(2(1(0(1(1(2(x1))))))))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.59 , 0(0(0(0(1(x1))))) -> 1(1(0(1(0(0(x1)))))) 1127.96/299.59 , 0(0(0(1(2(0(2(2(1(1(0(2(0(1(1(1(1(1(0(1(0(2(0(2(1(2(2(1(2(2(0(2(0(0(2(0(0(1(2(0(2(1(0(2(0(1(0(1(x1)))))))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 0(0(0(0(1(0(2(1(0(2(2(0(1(2(0(1(2(2(2(2(0(0(2(1(1(0(0(1(0(1(0(0(2(1(0(1(2(0(2(0(0(1(2(2(1(2(2(0(1(x1))))))))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.59 , 0(0(0(1(2(2(1(1(2(0(2(1(1(2(2(2(0(2(0(0(0(1(0(1(0(2(1(0(2(0(1(0(0(2(1(0(x1)))))))))))))))))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 1(1(1(0(1(0(0(2(1(1(1(2(1(2(1(1(2(1(0(1(0(2(0(0(2(1(0(0(1(2(2(2(1(1(0(1(1(0(x1)))))))))))))))))))))))))))))))))))))) 1127.96/299.59 , 0(0(0(2(0(0(0(0(0(0(0(2(2(1(2(0(0(0(1(1(1(1(2(2(2(1(0(2(2(1(2(0(0(0(2(2(0(1(x1)))))))))))))))))))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 0(0(2(0(0(2(1(2(1(0(2(1(0(2(2(1(0(1(1(0(0(0(0(1(2(1(2(2(1(1(1(0(0(2(1(1(2(0(1(0(x1)))))))))))))))))))))))))))))))))))))))) 1127.96/299.59 , 0(0(0(2(1(2(x1)))))) -> 1(1(0(0(0(1(2(x1))))))) 1127.96/299.59 , 0(0(1(2(2(2(2(0(1(1(0(1(2(2(2(2(1(1(0(2(2(0(0(0(2(1(2(1(0(1(1(0(2(2(0(1(1(0(2(2(2(1(0(2(x1)))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 0(0(2(0(2(0(2(1(0(2(1(1(2(1(1(1(2(2(0(1(0(0(0(0(1(1(0(0(1(2(0(0(1(0(0(2(0(2(0(0(2(0(2(2(2(x1))))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.59 , 0(0(2(1(0(1(1(1(0(x1))))))))) -> 1(0(0(1(0(1(1(1(1(0(x1)))))))))) 1127.96/299.59 , 0(0(2(1(2(2(0(1(0(1(1(2(1(2(0(1(2(1(0(1(0(1(1(1(2(0(0(2(0(1(0(0(0(2(1(1(0(2(0(2(0(1(2(1(1(x1))))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 1(1(1(0(0(0(0(1(2(2(1(2(0(1(1(1(1(1(2(2(1(0(0(0(2(1(2(2(1(0(1(1(2(1(0(0(2(0(1(0(0(0(1(0(1(0(1(x1))))))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.59 , 0(0(2(2(0(0(1(0(1(2(1(0(1(1(2(1(1(2(0(0(1(1(x1)))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 0(0(2(2(2(1(0(0(1(1(1(0(0(0(1(1(2(2(1(0(2(1(0(x1))))))))))))))))))))))) 1127.96/299.59 , 0(1(0(1(2(0(1(1(2(0(1(2(2(1(1(0(1(1(2(2(1(2(0(2(0(2(1(2(2(0(1(0(0(x1))))))))))))))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 0(2(1(0(2(0(1(1(0(0(1(1(2(2(0(2(1(1(0(2(1(0(0(2(0(0(1(1(1(2(1(0(0(0(0(x1))))))))))))))))))))))))))))))))))) 1127.96/299.59 , 0(1(0(2(0(2(0(2(0(2(1(2(1(2(2(1(1(1(2(0(0(2(2(1(2(0(0(2(0(1(2(x1))))))))))))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 0(2(0(2(0(2(0(2(0(1(1(1(2(2(2(1(2(2(1(0(1(2(1(0(2(0(2(0(0(1(2(x1))))))))))))))))))))))))))))))) 1127.96/299.59 , 0(1(1(0(1(1(2(2(2(2(2(2(1(1(1(1(1(0(2(2(0(0(2(0(x1)))))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 0(2(2(2(1(1(1(1(0(1(1(0(0(1(0(2(2(1(2(1(1(1(1(1(0(2(1(0(0(x1))))))))))))))))))))))))))))) 1127.96/299.59 , 0(1(1(1(1(1(0(1(1(0(2(2(2(0(2(1(2(2(1(1(2(0(0(0(0(2(2(2(0(2(0(1(0(2(1(1(2(x1))))))))))))))))))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 0(0(0(0(1(1(2(2(1(2(0(2(1(1(2(1(1(0(1(2(0(1(0(2(1(2(2(1(2(0(2(1(0(0(2(2(1(2(x1)))))))))))))))))))))))))))))))))))))) 1127.96/299.59 , 0(2(0(2(0(2(2(0(0(0(1(1(0(1(1(1(2(0(2(1(2(1(0(1(0(2(2(1(2(0(x1)))))))))))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 0(2(0(1(2(1(1(1(1(0(0(0(0(1(2(1(2(0(0(1(2(2(1(2(0(1(1(2(0(0(1(1(0(x1))))))))))))))))))))))))))))))))) 1127.96/299.59 , 0(2(1(0(2(0(1(1(0(2(1(2(0(1(1(2(1(2(2(0(0(x1))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 0(2(2(1(2(1(2(1(2(1(0(2(2(1(1(0(0(0(0(1(0(0(x1)))))))))))))))))))))) 1127.96/299.59 , 0(2(1(2(1(1(1(0(2(1(2(2(1(x1))))))))))))) -> 1127.96/299.59 0(2(2(0(1(2(2(2(1(0(0(2(0(1(x1)))))))))))))) 1127.96/299.59 , 1(0(1(0(2(2(0(1(1(1(1(2(2(2(2(1(0(2(0(2(2(1(1(1(1(0(2(0(1(0(2(2(2(2(2(0(x1)))))))))))))))))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 2(0(0(0(1(0(2(2(2(1(0(0(2(2(1(0(1(0(0(1(2(0(1(2(1(0(1(0(2(2(2(0(1(1(0(0(2(0(0(x1))))))))))))))))))))))))))))))))))))))) 1127.96/299.59 , 1(0(1(1(1(2(2(1(1(0(0(1(2(2(0(2(0(2(0(0(2(2(1(0(0(2(2(2(2(2(0(0(2(2(0(1(1(1(0(1(2(0(1(1(0(2(1(x1))))))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 2(1(1(0(2(0(0(0(0(2(0(1(0(1(1(1(1(2(1(0(2(1(0(2(2(1(1(2(2(0(1(1(0(0(1(1(1(0(1(1(1(0(0(0(1(0(1(1(2(x1))))))))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.59 , 1(0(2(0(2(0(1(2(0(2(1(0(2(0(0(2(1(1(0(1(0(2(0(0(1(x1))))))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 1(0(1(0(0(1(2(1(1(1(1(1(1(1(2(0(0(0(1(0(1(2(1(0(0(0(x1)))))))))))))))))))))))))) 1127.96/299.59 , 1(0(2(0(2(1(0(2(1(0(2(0(2(2(1(1(1(2(2(0(1(0(2(0(2(1(0(1(2(2(0(1(1(1(0(1(0(x1))))))))))))))))))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 2(0(2(2(0(1(0(2(1(1(1(0(0(1(0(0(2(1(2(2(2(1(1(1(2(0(2(0(0(0(1(0(1(0(0(2(1(1(1(1(0(0(x1)))))))))))))))))))))))))))))))))))))))))) 1127.96/299.59 , 1(0(2(1(0(0(1(1(2(0(1(1(0(1(0(1(1(1(0(2(1(2(0(2(0(1(1(0(1(0(2(2(0(2(0(1(x1)))))))))))))))))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 2(1(0(1(0(1(2(2(0(1(1(2(2(0(2(0(1(0(0(1(1(1(1(0(2(0(0(2(1(0(0(1(1(0(1(0(0(0(x1)))))))))))))))))))))))))))))))))))))) 1127.96/299.59 , 1(0(2(2(1(2(0(0(1(0(1(0(2(1(0(2(1(1(2(0(1(2(0(0(1(0(0(2(2(1(2(2(1(1(1(0(0(2(1(0(0(2(2(0(x1)))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 2(1(1(0(2(2(0(1(0(2(1(0(1(1(0(1(0(0(0(2(0(2(2(2(1(2(0(1(0(0(1(1(1(1(1(1(0(0(0(1(1(2(2(1(0(2(0(x1))))))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.59 , 1(0(2(2(2(1(1(0(0(2(1(0(1(0(1(1(2(0(0(2(2(0(0(0(1(1(2(2(2(0(1(2(2(1(1(1(2(1(1(2(0(1(1(0(x1)))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 1(0(2(1(1(0(1(0(0(2(1(0(1(0(1(1(2(0(0(2(2(2(0(2(0(1(2(2(2(2(1(1(0(1(1(1(1(2(2(1(0(2(1(0(x1)))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.59 , 1(0(2(2(2(2(1(0(1(2(1(0(2(1(2(1(1(1(1(0(2(1(1(0(1(0(2(2(2(1(0(2(1(0(0(0(2(0(2(0(0(2(0(0(1(0(x1)))))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 1(2(0(1(2(2(0(1(1(1(1(0(0(0(0(0(1(2(1(2(2(0(0(2(0(0(2(0(2(2(1(0(1(1(2(2(0(1(1(0(0(0(2(0(1(1(0(x1))))))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.59 , 1(1(0(1(0(2(0(1(1(2(1(2(0(0(0(2(0(2(1(0(1(x1))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 1(1(1(1(2(1(0(2(1(1(1(1(1(0(1(0(0(1(1(0(1(2(x1)))))))))))))))))))))) 1127.96/299.59 , 1(1(0(2(0(1(0(0(1(x1))))))))) -> 1127.96/299.59 1(0(1(1(0(1(0(0(1(2(1(x1))))))))))) 1127.96/299.59 , 1(1(0(2(1(0(1(2(2(0(0(1(0(x1))))))))))))) -> 1127.96/299.59 2(2(1(0(2(1(1(1(1(1(0(1(1(1(0(0(0(x1))))))))))))))))) 1127.96/299.59 , 1(1(0(2(2(2(0(0(0(2(1(1(1(1(2(1(1(2(x1)))))))))))))))))) -> 1127.96/299.59 1(0(0(2(1(2(0(1(1(0(0(2(0(1(0(0(1(0(0(x1))))))))))))))))))) 1127.96/299.59 , 1(1(1(0(2(2(1(1(1(1(2(0(2(1(1(2(1(1(1(1(1(2(1(0(2(1(2(0(1(0(2(2(0(2(1(1(2(2(1(1(1(0(1(0(x1)))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 2(1(1(1(0(0(1(2(1(1(0(0(1(2(2(1(0(2(2(0(2(1(2(0(0(0(0(0(2(2(1(2(0(2(1(2(1(0(0(0(2(1(0(0(1(2(0(x1))))))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.59 , 1(1(1(1(0(2(0(2(0(0(2(0(0(2(1(1(2(0(0(1(2(0(1(1(2(0(0(2(2(0(0(0(2(0(2(1(1(1(2(2(1(x1))))))))))))))))))))))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 1(2(0(0(0(2(2(0(2(2(0(2(1(1(2(0(1(0(1(2(1(2(1(0(2(2(1(0(1(1(1(0(1(0(0(2(1(1(0(1(0(1(0(1(1(1(0(0(1(x1))))))))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.59 , 1(1(1(1(0(2(0(2(1(0(2(1(0(1(1(0(2(2(0(2(1(0(2(2(x1)))))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 1(0(2(0(1(0(0(1(1(2(0(0(2(2(2(0(2(1(2(0(0(0(1(0(0(x1))))))))))))))))))))))))) 1127.96/299.59 , 1(1(1(2(0(1(2(1(0(0(2(2(0(0(1(2(0(1(0(1(2(2(1(0(0(1(0(2(0(2(1(2(1(x1))))))))))))))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 0(2(1(2(1(2(1(1(2(1(2(2(0(1(0(1(2(0(1(0(1(1(1(0(0(2(1(0(1(0(0(0(1(0(1(x1))))))))))))))))))))))))))))))))))) 1127.96/299.59 , 1(1(1(2(1(2(1(1(2(0(2(0(2(0(2(2(2(2(0(1(2(2(1(1(0(2(2(0(0(1(2(1(0(0(2(1(2(2(2(2(1(1(1(2(1(1(2(1(2(x1))))))))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 0(0(0(0(1(0(0(1(2(2(1(2(2(2(1(2(0(2(2(0(2(1(0(0(2(0(2(1(1(2(0(0(2(0(1(1(2(1(2(1(0(1(2(1(2(1(2(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.59 , 1(1(2(1(1(0(2(0(2(1(0(2(1(0(1(2(1(0(1(2(0(x1))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 2(0(1(1(1(0(0(2(0(0(2(1(2(0(0(2(2(1(1(1(1(1(1(1(0(0(0(x1))))))))))))))))))))))))))) 1127.96/299.59 , 1(1(2(1(2(0(0(0(1(2(2(2(0(0(0(1(2(2(1(0(2(0(0(0(0(0(1(2(0(0(1(0(1(2(2(1(2(2(1(1(1(1(2(0(1(x1))))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 1(2(1(2(0(1(0(1(0(2(2(0(1(0(1(1(0(1(0(1(0(0(2(0(2(2(1(1(1(2(1(0(1(0(1(1(1(1(0(1(0(0(1(2(1(2(0(0(0(0(x1)))))))))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.59 , 1(1(2(2(1(1(0(1(0(1(2(2(1(0(2(1(1(0(2(0(1(0(2(1(1(2(2(2(1(0(0(2(2(1(1(x1))))))))))))))))))))))))))))))))))) 1127.96/299.59 -> 1127.96/299.59 1(0(0(0(0(0(0(2(0(2(0(2(1(1(1(0(0(0(0(1(1(1(0(0(0(1(0(2(1(1(0(2(2(2(0(1(1(0(x1)))))))))))))))))))))))))))))))))))))) 1127.96/299.59 , 1(2(0(0(1(0(0(0(2(0(1(0(1(0(1(x1))))))))))))))) -> 1127.96/299.59 1(0(0(0(2(2(0(0(1(1(0(1(1(0(0(x1))))))))))))))) 1127.96/299.60 , 1(2(0(0(1(1(2(0(1(1(2(2(1(0(2(2(2(1(2(2(1(x1))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 2(2(0(1(1(2(1(1(0(0(2(1(0(0(0(1(0(1(2(1(1(1(2(x1))))))))))))))))))))))) 1127.96/299.60 , 1(2(0(0(2(2(2(0(1(0(2(2(1(0(0(0(2(0(1(2(0(2(0(1(0(0(1(2(2(2(0(1(1(0(1(0(2(x1))))))))))))))))))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 1(0(0(1(2(0(0(1(1(1(1(1(0(0(1(0(1(2(2(2(0(2(1(2(1(2(2(2(2(1(2(2(0(1(0(1(2(2(0(2(2(x1))))))))))))))))))))))))))))))))))))))))) 1127.96/299.60 , 1(2(0(1(0(0(0(0(1(1(2(2(2(1(1(0(1(2(0(0(1(2(1(2(2(2(0(0(0(2(1(2(1(0(1(2(2(2(1(0(0(1(x1)))))))))))))))))))))))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 2(1(0(1(2(0(2(0(1(0(0(0(0(0(2(0(2(2(1(2(2(1(0(0(1(2(0(2(1(1(2(0(1(2(1(1(1(0(1(1(1(0(0(1(0(0(0(x1))))))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.60 , 1(2(0(1(1(1(1(0(1(1(1(0(2(2(1(2(x1)))))))))))))))) -> 1127.96/299.60 0(1(0(1(2(2(1(1(1(1(2(1(1(1(0(2(x1)))))))))))))))) 1127.96/299.60 , 1(2(1(0(0(1(1(2(0(2(2(2(1(2(0(0(2(2(0(2(1(2(1(2(0(1(1(0(1(0(2(1(2(1(1(2(1(0(1(2(1(2(0(2(x1)))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 1(1(1(0(0(0(0(1(2(0(0(2(1(2(0(2(2(1(2(0(2(0(0(2(1(1(0(2(1(1(1(0(0(0(1(0(1(0(1(1(1(0(0(0(1(1(0(2(0(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.60 , 1(2(1(1(1(0(2(0(0(2(1(0(1(2(0(1(2(x1))))))))))))))))) -> 1127.96/299.60 0(0(2(0(1(1(0(0(2(1(0(2(0(0(2(0(0(0(x1)))))))))))))))))) 1127.96/299.60 , 1(2(1(2(1(0(0(0(1(2(2(2(2(1(1(2(2(2(1(2(0(2(2(1(0(1(2(0(2(0(0(0(0(2(2(1(0(2(1(x1))))))))))))))))))))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 1(2(1(1(1(0(0(2(1(2(0(2(2(1(0(1(2(0(2(2(0(1(2(2(0(2(2(1(2(0(1(0(2(2(2(0(0(2(1(x1))))))))))))))))))))))))))))))))))))))) 1127.96/299.60 , 1(2(1(2(1(2(1(1(2(2(2(0(0(1(0(0(1(2(0(1(2(1(2(2(0(1(0(2(2(0(1(x1))))))))))))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 0(2(0(1(1(1(1(0(1(0(1(0(0(0(1(0(1(0(0(0(1(1(2(1(0(2(1(0(0(2(1(2(1(2(x1)))))))))))))))))))))))))))))))))) 1127.96/299.60 , 2(0(0(0(0(1(0(1(0(0(2(2(1(1(2(1(1(1(2(1(0(2(1(2(0(2(0(1(2(0(1(2(1(2(0(0(2(2(2(x1))))))))))))))))))))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 1(1(2(1(2(0(2(2(0(0(0(1(1(1(1(1(0(0(2(1(1(1(0(0(0(2(1(1(1(1(0(1(2(2(1(2(0(2(0(1(2(1(2(x1))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.60 , 2(0(0(0(0(2(1(2(1(1(0(2(1(1(0(2(1(0(2(0(1(0(1(2(0(1(0(0(2(2(1(2(2(0(1(1(2(2(2(1(0(0(2(1(1(x1))))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 2(0(2(2(1(0(0(1(2(2(1(1(0(2(0(2(1(0(2(0(1(1(2(0(1(0(1(2(1(0(1(1(1(1(0(0(0(0(2(2(2(0(2(2(0(2(1(0(x1)))))))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.60 , 2(0(0(2(0(0(0(0(2(0(1(1(2(1(2(0(1(0(1(1(1(1(2(0(2(0(0(0(1(1(1(1(0(0(1(2(0(2(2(2(0(0(0(0(1(2(1(0(1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 1(0(0(2(2(0(0(0(2(0(1(1(2(1(2(0(1(2(1(1(1(1(2(0(0(0(0(0(2(0(1(1(0(0(0(2(1(2(2(2(1(0(1(0(1(0(0(0(1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.60 , 2(0(1(0(1(1(2(2(1(2(2(2(2(2(0(0(2(1(1(0(0(0(0(2(0(2(x1)))))))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 1(0(0(1(0(2(2(2(2(0(1(1(1(1(2(1(1(0(0(2(2(0(2(1(0(0(2(x1))))))))))))))))))))))))))) 1127.96/299.60 , 2(0(1(1(0(1(1(0(2(0(0(0(1(0(0(2(0(2(1(1(1(2(1(0(0(1(1(1(0(1(2(2(2(1(1(1(1(2(2(2(1(2(0(2(2(x1))))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 2(1(1(1(0(2(1(0(0(0(0(1(0(2(2(1(1(0(0(2(2(2(0(1(1(0(1(0(1(1(0(0(0(2(1(1(2(2(1(1(0(1(1(1(2(0(2(x1))))))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.60 , 2(0(1(2(1(2(0(0(0(2(2(2(1(1(0(1(2(x1))))))))))))))))) -> 1127.96/299.60 0(0(1(1(1(2(1(1(0(1(2(1(0(1(0(1(1(1(0(0(x1)))))))))))))))))))) 1127.96/299.60 , 2(0(1(2(2(1(1(1(2(0(1(1(1(2(0(0(2(1(2(0(1(2(1(1(2(1(0(2(1(2(2(1(0(2(2(1(2(0(2(0(1(x1))))))))))))))))))))))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 1(2(2(0(1(2(2(1(0(2(0(1(0(1(1(1(0(1(2(0(0(1(1(1(1(1(1(0(0(1(0(2(1(0(2(0(1(1(2(2(0(0(x1)))))))))))))))))))))))))))))))))))))))))) 1127.96/299.60 , 2(0(1(2(2(2(1(2(1(1(2(2(2(2(0(2(1(0(0(0(1(2(1(0(x1)))))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 1(1(0(1(0(2(0(0(0(0(0(1(1(1(0(0(0(0(0(1(0(0(2(1(1(0(x1)))))))))))))))))))))))))) 1127.96/299.60 , 2(0(2(0(0(2(0(2(2(1(2(0(0(0(1(1(1(1(2(2(1(2(1(x1))))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 1(0(1(1(0(0(2(2(1(1(1(2(0(2(1(1(2(1(2(2(1(0(1(2(x1)))))))))))))))))))))))) 1127.96/299.60 , 2(0(2(0(0(2(2(1(2(1(2(0(0(0(1(2(0(0(0(2(x1)))))))))))))))))))) -> 1127.96/299.60 0(2(1(0(2(2(2(0(2(0(0(1(0(0(1(0(2(0(2(2(x1)))))))))))))))))))) 1127.96/299.60 , 2(0(2(0(2(2(1(2(2(1(2(1(2(1(2(2(0(2(2(1(2(0(0(1(0(1(0(2(0(1(1(x1))))))))))))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 2(1(0(1(2(1(1(0(1(0(0(1(0(0(0(2(0(2(1(1(2(1(0(2(1(1(2(2(1(2(1(0(x1)))))))))))))))))))))))))))))))) 1127.96/299.60 , 2(0(2(1(0(1(2(2(1(2(1(1(2(2(1(1(0(0(0(2(2(2(1(1(2(0(0(1(2(1(0(x1))))))))))))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 1(0(1(2(2(0(0(1(1(0(1(0(0(2(1(1(0(0(1(2(0(1(0(1(0(1(1(2(1(1(2(1(0(x1))))))))))))))))))))))))))))))))) 1127.96/299.60 , 2(0(2(2(0(0(2(1(2(2(2(1(0(2(1(0(2(2(2(0(2(0(2(0(1(1(0(1(0(1(0(2(0(0(0(0(2(1(0(2(2(x1))))))))))))))))))))))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 1(2(1(2(1(1(1(0(1(1(1(0(0(2(1(2(1(2(0(2(0(0(0(2(1(0(2(2(1(0(0(2(2(2(1(1(2(2(2(2(1(1(0(0(0(2(1(2(x1)))))))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.60 , 2(0(2(2(0(1(2(2(0(x1))))))))) -> 0(2(0(1(1(1(0(1(0(0(x1)))))))))) 1127.96/299.60 , 2(1(0(0(2(2(2(2(1(2(1(1(2(2(2(0(1(2(0(0(0(0(1(2(0(2(2(1(x1)))))))))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 1(1(0(1(0(0(2(0(2(1(0(0(0(0(0(0(1(2(1(1(0(2(0(2(1(1(2(2(1(x1))))))))))))))))))))))))))))) 1127.96/299.60 , 2(1(0(1(0(1(0(1(1(2(2(0(1(0(2(2(0(0(0(1(2(0(1(0(0(0(2(2(0(2(1(1(2(x1))))))))))))))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 0(2(1(0(1(1(1(1(1(0(1(0(0(1(1(1(1(2(0(1(2(2(0(1(0(1(1(1(2(1(2(2(1(0(2(x1))))))))))))))))))))))))))))))))))) 1127.96/299.60 , 2(1(0(1(0(2(2(2(0(2(1(2(0(2(0(0(2(1(0(2(2(2(2(0(2(1(1(x1))))))))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 0(1(1(2(1(1(1(1(0(1(0(0(1(2(0(2(0(2(2(1(1(0(1(2(0(1(0(0(0(x1))))))))))))))))))))))))))))) 1127.96/299.60 , 2(1(1(0(0(0(1(0(0(0(0(0(2(2(1(1(2(0(1(0(2(0(2(2(1(2(x1)))))))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 2(0(2(0(1(2(1(1(0(1(2(1(1(2(2(2(2(2(2(1(1(1(1(1(1(0(0(2(x1)))))))))))))))))))))))))))) 1127.96/299.60 , 2(1(1(1(1(1(1(1(0(2(2(1(2(2(1(1(2(0(0(1(1(0(0(0(x1)))))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 1(1(2(1(0(2(2(1(2(1(2(2(1(1(1(1(1(1(1(0(0(0(0(0(x1)))))))))))))))))))))))) 1127.96/299.60 , 2(1(1(2(1(2(0(2(2(2(0(1(2(2(0(0(0(1(2(0(1(1(2(0(2(0(0(0(2(0(2(2(0(0(1(2(0(1(2(2(0(1(x1)))))))))))))))))))))))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 2(0(0(2(2(1(2(2(2(2(0(2(2(1(2(0(0(0(1(0(1(1(1(2(0(0(1(1(0(2(0(1(0(1(2(0(2(0(1(1(0(0(1(0(x1)))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.60 , 2(1(2(1(0(2(1(0(1(1(0(2(1(1(2(2(2(0(1(2(1(0(2(0(1(0(1(0(2(0(0(1(0(2(1(x1))))))))))))))))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 0(2(1(0(0(2(2(1(2(1(0(1(2(1(2(0(1(0(1(0(1(0(0(2(1(0(1(1(2(1(0(1(2(0(2(2(0(1(x1)))))))))))))))))))))))))))))))))))))) 1127.96/299.60 , 2(1(2(1(2(2(2(0(1(0(2(2(2(2(2(2(1(2(1(1(x1)))))))))))))))))))) -> 1127.96/299.60 2(2(0(1(1(0(0(1(1(1(0(0(0(0(0(0(1(1(2(2(1(1(x1)))))))))))))))))))))) 1127.96/299.60 , 2(2(0(0(2(0(0(2(2(0(0(0(2(0(0(2(1(1(2(0(2(1(x1)))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 0(2(1(1(0(0(2(0(1(1(2(0(1(0(0(0(1(0(2(1(1(1(2(1(0(x1))))))))))))))))))))))))) 1127.96/299.60 , 2(2(0(1(1(1(1(1(1(2(1(2(1(1(1(0(2(2(1(0(0(1(2(0(1(x1))))))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 0(1(1(1(1(1(0(2(0(1(2(1(0(0(0(2(1(0(2(2(1(1(1(1(0(0(0(x1))))))))))))))))))))))))))) 1127.96/299.60 , 2(2(1(2(1(2(1(1(1(0(1(1(2(1(0(2(0(0(2(1(2(0(x1)))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 1(0(0(2(1(2(0(2(0(1(1(2(2(1(0(2(2(0(1(2(0(1(0(x1))))))))))))))))))))))) 1127.96/299.60 , 2(2(2(0(0(0(0(2(0(2(2(2(1(0(2(2(1(2(2(2(1(2(0(2(2(x1))))))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 0(2(2(1(0(0(0(2(0(2(2(2(2(1(2(2(1(2(2(0(2(2(0(2(2(x1))))))))))))))))))))))))) 1127.96/299.60 , 2(2(2(1(1(2(1(2(2(0(0(x1))))))))))) -> 1127.96/299.60 2(0(0(1(2(2(0(0(2(1(1(0(0(x1))))))))))))) 1127.96/299.60 , 2(2(2(1(2(1(2(0(0(2(1(0(1(0(2(1(0(0(2(0(1(2(2(1(1(2(2(0(2(1(2(0(2(2(x1)))))))))))))))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 0(2(1(1(1(1(0(0(0(0(2(0(2(1(0(0(1(0(2(1(1(0(2(1(1(0(1(0(0(0(2(1(0(1(2(1(2(0(1(1(2(x1))))))))))))))))))))))))))))))))))))))))) 1127.96/299.60 , 2(2(2(2(0(2(1(1(2(2(2(0(2(0(2(1(0(0(2(0(2(1(0(1(1(2(2(1(1(0(0(1(2(1(1(2(1(2(1(2(0(0(0(0(0(1(0(0(1(x1))))))))))))))))))))))))))))))))))))))))))))))))) 1127.96/299.60 -> 1127.96/299.60 2(2(1(1(1(1(0(1(2(1(2(2(2(0(2(1(1(1(0(0(1(1(2(2(0(2(2(1(0(0(1(1(1(1(0(0(0(1(2(0(2(1(0(2(0(1(1(0(2(1(x1)))))))))))))))))))))))))))))))))))))))))))))))))) } 1127.96/299.60 Obligation: 1127.96/299.60 derivational complexity 1127.96/299.60 Answer: 1127.96/299.60 MAYBE 1127.96/299.60 1127.96/299.60 None of the processors succeeded. 1127.96/299.60 1127.96/299.60 Details of failed attempt(s): 1127.96/299.60 ----------------------------- 1127.96/299.60 1) 'bsearch-matrix (timeout of 297 seconds)' failed due to the 1127.96/299.60 following reason: 1127.96/299.60 1127.96/299.60 Computation stopped due to timeout after 297.0 seconds. 1127.96/299.60 1127.96/299.60 2) 'iteProgress (timeout of 297 seconds)' failed due to the 1127.96/299.60 following reason: 1127.96/299.60 1127.96/299.60 Computation stopped due to timeout after 297.0 seconds. 1127.96/299.60 1127.96/299.60 3) 'Inspecting Problem... (timeout of 297 seconds)' failed due to 1127.96/299.60 the following reason: 1128.31/299.60 1128.31/299.60 Computation stopped due to timeout after 297.0 seconds. 1128.31/299.60 1128.31/299.60 4) 'Fastest (timeout of 60 seconds)' failed due to the following 1128.31/299.60 reason: 1128.31/299.60 1128.31/299.60 Computation stopped due to timeout after 60.0 seconds. 1128.31/299.60 1128.31/299.60 1128.31/299.60 Arrrr.. 1128.71/300.10 EOF