YES(?,O(n^2)) 1173.92/295.26 YES(?,O(n^2)) 1173.92/295.28 1173.92/295.28 Problem: 1173.92/295.28 p(a(x0),p(b(x1),p(a(x2),x3))) -> p(x2,p(a(a(x0)),p(b(x1),x3))) 1173.92/295.28 1173.92/295.28 Proof: 1173.92/295.28 Complexity Transformation Processor: 1173.92/295.28 strict: 1173.92/295.28 p(a(x0),p(b(x1),p(a(x2),x3))) -> p(x2,p(a(a(x0)),p(b(x1),x3))) 1173.92/295.28 weak: 1173.92/295.28 1173.92/295.28 Root-Labeling Processor: 1173.92/295.28 strict: 1173.92/295.28 p(a,p)(a(p)(x0),p(b,p)(b(p)(x1),p(a,p)(a(p)(x2),x3))) -> 1173.92/295.28 p(p,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,p)(b(p)(x1),x3))) 1173.92/295.28 p(a,p)(a(p)(x0),p(b,p)(b(p)(x1),p(a,a)(a(p)(x2),x3))) -> 1173.92/295.28 p(p,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,a)(b(p)(x1),x3))) 1173.92/295.28 p(a,p)(a(p)(x0),p(b,p)(b(p)(x1),p(a,b)(a(p)(x2),x3))) -> 1173.92/295.28 p(p,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,b)(b(p)(x1),x3))) 1173.92/295.28 p(a,p)(a(p)(x0),p(b,p)(b(p)(x1),p(a,p)(a(a)(x2),x3))) -> 1173.92/295.28 p(a,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,p)(b(p)(x1),x3))) 1173.92/295.28 p(a,p)(a(p)(x0),p(b,p)(b(p)(x1),p(a,a)(a(a)(x2),x3))) -> 1173.92/295.28 p(a,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,a)(b(p)(x1),x3))) 1173.92/295.28 p(a,p)(a(p)(x0),p(b,p)(b(p)(x1),p(a,b)(a(a)(x2),x3))) -> 1173.92/295.28 p(a,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,b)(b(p)(x1),x3))) 1173.92/295.28 p(a,p)(a(p)(x0),p(b,p)(b(p)(x1),p(a,p)(a(b)(x2),x3))) -> 1173.92/295.28 p(b,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,p)(b(p)(x1),x3))) 1173.92/295.28 p(a,p)(a(p)(x0),p(b,p)(b(p)(x1),p(a,a)(a(b)(x2),x3))) -> 1173.92/295.28 p(b,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,a)(b(p)(x1),x3))) 1173.92/295.28 p(a,p)(a(p)(x0),p(b,p)(b(p)(x1),p(a,b)(a(b)(x2),x3))) -> 1173.92/295.28 p(b,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,b)(b(p)(x1),x3))) 1173.92/295.28 p(a,p)(a(p)(x0),p(b,p)(b(a)(x1),p(a,p)(a(p)(x2),x3))) -> 1173.92/295.28 p(p,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,p)(b(a)(x1),x3))) 1173.92/295.28 p(a,p)(a(p)(x0),p(b,p)(b(a)(x1),p(a,a)(a(p)(x2),x3))) -> 1173.92/295.28 p(p,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,a)(b(a)(x1),x3))) 1173.92/295.28 p(a,p)(a(p)(x0),p(b,p)(b(a)(x1),p(a,b)(a(p)(x2),x3))) -> 1173.92/295.28 p(p,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,b)(b(a)(x1),x3))) 1173.92/295.28 p(a,p)(a(p)(x0),p(b,p)(b(a)(x1),p(a,p)(a(a)(x2),x3))) -> 1173.92/295.28 p(a,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,p)(b(a)(x1),x3))) 1173.92/295.28 p(a,p)(a(p)(x0),p(b,p)(b(a)(x1),p(a,a)(a(a)(x2),x3))) -> 1173.92/295.28 p(a,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,a)(b(a)(x1),x3))) 1173.92/295.28 p(a,p)(a(p)(x0),p(b,p)(b(a)(x1),p(a,b)(a(a)(x2),x3))) -> 1173.92/295.28 p(a,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,b)(b(a)(x1),x3))) 1173.92/295.28 p(a,p)(a(p)(x0),p(b,p)(b(a)(x1),p(a,p)(a(b)(x2),x3))) -> 1173.92/295.28 p(b,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,p)(b(a)(x1),x3))) 1173.92/295.28 p(a,p)(a(p)(x0),p(b,p)(b(a)(x1),p(a,a)(a(b)(x2),x3))) -> 1173.92/295.28 p(b,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,a)(b(a)(x1),x3))) 1173.92/295.28 p(a,p)(a(p)(x0),p(b,p)(b(a)(x1),p(a,b)(a(b)(x2),x3))) -> 1173.92/295.28 p(b,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,b)(b(a)(x1),x3))) 1173.92/295.28 p(a,p)(a(p)(x0),p(b,p)(b(b)(x1),p(a,p)(a(p)(x2),x3))) -> 1173.92/295.28 p(p,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,p)(b(b)(x1),x3))) 1173.92/295.28 p(a,p)(a(p)(x0),p(b,p)(b(b)(x1),p(a,a)(a(p)(x2),x3))) -> 1173.92/295.28 p(p,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,a)(b(b)(x1),x3))) 1173.92/295.28 p(a,p)(a(p)(x0),p(b,p)(b(b)(x1),p(a,b)(a(p)(x2),x3))) -> 1173.92/295.28 p(p,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,b)(b(b)(x1),x3))) 1173.92/295.28 p(a,p)(a(p)(x0),p(b,p)(b(b)(x1),p(a,p)(a(a)(x2),x3))) -> 1173.92/295.28 p(a,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,p)(b(b)(x1),x3))) 1173.92/295.28 p(a,p)(a(p)(x0),p(b,p)(b(b)(x1),p(a,a)(a(a)(x2),x3))) -> 1173.92/295.28 p(a,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,a)(b(b)(x1),x3))) 1173.92/295.28 p(a,p)(a(p)(x0),p(b,p)(b(b)(x1),p(a,b)(a(a)(x2),x3))) -> 1173.92/295.28 p(a,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,b)(b(b)(x1),x3))) 1173.92/295.28 p(a,p)(a(p)(x0),p(b,p)(b(b)(x1),p(a,p)(a(b)(x2),x3))) -> 1173.92/295.28 p(b,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,p)(b(b)(x1),x3))) 1173.92/295.28 p(a,p)(a(p)(x0),p(b,p)(b(b)(x1),p(a,a)(a(b)(x2),x3))) -> 1173.92/295.28 p(b,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,a)(b(b)(x1),x3))) 1173.92/295.28 p(a,p)(a(p)(x0),p(b,p)(b(b)(x1),p(a,b)(a(b)(x2),x3))) -> 1173.92/295.28 p(b,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,b)(b(b)(x1),x3))) 1173.92/295.28 p(a,p)(a(a)(x0),p(b,p)(b(p)(x1),p(a,p)(a(p)(x2),x3))) -> 1173.92/295.28 p(p,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,p)(b(p)(x1),x3))) 1173.92/295.28 p(a,p)(a(a)(x0),p(b,p)(b(p)(x1),p(a,a)(a(p)(x2),x3))) -> 1173.92/295.28 p(p,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,a)(b(p)(x1),x3))) 1173.92/295.28 p(a,p)(a(a)(x0),p(b,p)(b(p)(x1),p(a,b)(a(p)(x2),x3))) -> 1173.92/295.28 p(p,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,b)(b(p)(x1),x3))) 1173.92/295.28 p(a,p)(a(a)(x0),p(b,p)(b(p)(x1),p(a,p)(a(a)(x2),x3))) -> 1173.92/295.28 p(a,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,p)(b(p)(x1),x3))) 1173.92/295.28 p(a,p)(a(a)(x0),p(b,p)(b(p)(x1),p(a,a)(a(a)(x2),x3))) -> 1173.92/295.28 p(a,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,a)(b(p)(x1),x3))) 1173.92/295.28 p(a,p)(a(a)(x0),p(b,p)(b(p)(x1),p(a,b)(a(a)(x2),x3))) -> 1173.92/295.29 p(a,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,b)(b(p)(x1),x3))) 1173.92/295.29 p(a,p)(a(a)(x0),p(b,p)(b(p)(x1),p(a,p)(a(b)(x2),x3))) -> 1173.92/295.29 p(b,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,p)(b(p)(x1),x3))) 1173.92/295.29 p(a,p)(a(a)(x0),p(b,p)(b(p)(x1),p(a,a)(a(b)(x2),x3))) -> 1173.92/295.29 p(b,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,a)(b(p)(x1),x3))) 1173.92/295.29 p(a,p)(a(a)(x0),p(b,p)(b(p)(x1),p(a,b)(a(b)(x2),x3))) -> 1173.92/295.29 p(b,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,b)(b(p)(x1),x3))) 1173.92/295.29 p(a,p)(a(a)(x0),p(b,p)(b(a)(x1),p(a,p)(a(p)(x2),x3))) -> 1173.92/295.29 p(p,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,p)(b(a)(x1),x3))) 1173.92/295.29 p(a,p)(a(a)(x0),p(b,p)(b(a)(x1),p(a,a)(a(p)(x2),x3))) -> 1173.92/295.29 p(p,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,a)(b(a)(x1),x3))) 1173.92/295.29 p(a,p)(a(a)(x0),p(b,p)(b(a)(x1),p(a,b)(a(p)(x2),x3))) -> 1173.92/295.29 p(p,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,b)(b(a)(x1),x3))) 1173.92/295.29 p(a,p)(a(a)(x0),p(b,p)(b(a)(x1),p(a,p)(a(a)(x2),x3))) -> 1173.92/295.29 p(a,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,p)(b(a)(x1),x3))) 1173.92/295.29 p(a,p)(a(a)(x0),p(b,p)(b(a)(x1),p(a,a)(a(a)(x2),x3))) -> 1173.92/295.29 p(a,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,a)(b(a)(x1),x3))) 1173.92/295.29 p(a,p)(a(a)(x0),p(b,p)(b(a)(x1),p(a,b)(a(a)(x2),x3))) -> 1173.92/295.29 p(a,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,b)(b(a)(x1),x3))) 1173.92/295.29 p(a,p)(a(a)(x0),p(b,p)(b(a)(x1),p(a,p)(a(b)(x2),x3))) -> 1173.92/295.29 p(b,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,p)(b(a)(x1),x3))) 1173.92/295.29 p(a,p)(a(a)(x0),p(b,p)(b(a)(x1),p(a,a)(a(b)(x2),x3))) -> 1173.92/295.29 p(b,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,a)(b(a)(x1),x3))) 1173.92/295.29 p(a,p)(a(a)(x0),p(b,p)(b(a)(x1),p(a,b)(a(b)(x2),x3))) -> 1173.92/295.29 p(b,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,b)(b(a)(x1),x3))) 1173.92/295.29 p(a,p)(a(a)(x0),p(b,p)(b(b)(x1),p(a,p)(a(p)(x2),x3))) -> 1173.92/295.29 p(p,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,p)(b(b)(x1),x3))) 1173.92/295.29 p(a,p)(a(a)(x0),p(b,p)(b(b)(x1),p(a,a)(a(p)(x2),x3))) -> 1173.92/295.29 p(p,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,a)(b(b)(x1),x3))) 1173.92/295.29 p(a,p)(a(a)(x0),p(b,p)(b(b)(x1),p(a,b)(a(p)(x2),x3))) -> 1173.92/295.29 p(p,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,b)(b(b)(x1),x3))) 1173.92/295.29 p(a,p)(a(a)(x0),p(b,p)(b(b)(x1),p(a,p)(a(a)(x2),x3))) -> 1173.92/295.29 p(a,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,p)(b(b)(x1),x3))) 1173.92/295.29 p(a,p)(a(a)(x0),p(b,p)(b(b)(x1),p(a,a)(a(a)(x2),x3))) -> 1173.92/295.29 p(a,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,a)(b(b)(x1),x3))) 1173.92/295.29 p(a,p)(a(a)(x0),p(b,p)(b(b)(x1),p(a,b)(a(a)(x2),x3))) -> 1173.92/295.29 p(a,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,b)(b(b)(x1),x3))) 1173.92/295.29 p(a,p)(a(a)(x0),p(b,p)(b(b)(x1),p(a,p)(a(b)(x2),x3))) -> 1173.92/295.29 p(b,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,p)(b(b)(x1),x3))) 1173.92/295.29 p(a,p)(a(a)(x0),p(b,p)(b(b)(x1),p(a,a)(a(b)(x2),x3))) -> 1173.92/295.29 p(b,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,a)(b(b)(x1),x3))) 1173.92/295.29 p(a,p)(a(a)(x0),p(b,p)(b(b)(x1),p(a,b)(a(b)(x2),x3))) -> 1173.92/295.29 p(b,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,b)(b(b)(x1),x3))) 1173.92/295.29 p(a,p)(a(b)(x0),p(b,p)(b(p)(x1),p(a,p)(a(p)(x2),x3))) -> 1173.92/295.29 p(p,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,p)(b(p)(x1),x3))) 1173.92/295.29 p(a,p)(a(b)(x0),p(b,p)(b(p)(x1),p(a,a)(a(p)(x2),x3))) -> 1173.92/295.29 p(p,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,a)(b(p)(x1),x3))) 1173.92/295.29 p(a,p)(a(b)(x0),p(b,p)(b(p)(x1),p(a,b)(a(p)(x2),x3))) -> 1173.92/295.29 p(p,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,b)(b(p)(x1),x3))) 1173.92/295.29 p(a,p)(a(b)(x0),p(b,p)(b(p)(x1),p(a,p)(a(a)(x2),x3))) -> 1173.92/295.29 p(a,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,p)(b(p)(x1),x3))) 1173.92/295.29 p(a,p)(a(b)(x0),p(b,p)(b(p)(x1),p(a,a)(a(a)(x2),x3))) -> 1173.92/295.29 p(a,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,a)(b(p)(x1),x3))) 1173.92/295.29 p(a,p)(a(b)(x0),p(b,p)(b(p)(x1),p(a,b)(a(a)(x2),x3))) -> 1173.92/295.29 p(a,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,b)(b(p)(x1),x3))) 1173.92/295.29 p(a,p)(a(b)(x0),p(b,p)(b(p)(x1),p(a,p)(a(b)(x2),x3))) -> 1173.92/295.29 p(b,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,p)(b(p)(x1),x3))) 1173.92/295.29 p(a,p)(a(b)(x0),p(b,p)(b(p)(x1),p(a,a)(a(b)(x2),x3))) -> 1173.92/295.29 p(b,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,a)(b(p)(x1),x3))) 1173.92/295.29 p(a,p)(a(b)(x0),p(b,p)(b(p)(x1),p(a,b)(a(b)(x2),x3))) -> 1173.92/295.29 p(b,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,b)(b(p)(x1),x3))) 1173.92/295.29 p(a,p)(a(b)(x0),p(b,p)(b(a)(x1),p(a,p)(a(p)(x2),x3))) -> 1173.92/295.29 p(p,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,p)(b(a)(x1),x3))) 1173.92/295.29 p(a,p)(a(b)(x0),p(b,p)(b(a)(x1),p(a,a)(a(p)(x2),x3))) -> 1173.92/295.29 p(p,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,a)(b(a)(x1),x3))) 1173.92/295.29 p(a,p)(a(b)(x0),p(b,p)(b(a)(x1),p(a,b)(a(p)(x2),x3))) -> 1173.92/295.29 p(p,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,b)(b(a)(x1),x3))) 1173.92/295.29 p(a,p)(a(b)(x0),p(b,p)(b(a)(x1),p(a,p)(a(a)(x2),x3))) -> 1173.92/295.29 p(a,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,p)(b(a)(x1),x3))) 1174.19/295.30 p(a,p)(a(b)(x0),p(b,p)(b(a)(x1),p(a,a)(a(a)(x2),x3))) -> 1174.19/295.30 p(a,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,a)(b(a)(x1),x3))) 1174.19/295.30 p(a,p)(a(b)(x0),p(b,p)(b(a)(x1),p(a,b)(a(a)(x2),x3))) -> 1174.19/295.30 p(a,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,b)(b(a)(x1),x3))) 1174.19/295.30 p(a,p)(a(b)(x0),p(b,p)(b(a)(x1),p(a,p)(a(b)(x2),x3))) -> 1174.19/295.30 p(b,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,p)(b(a)(x1),x3))) 1174.19/295.30 p(a,p)(a(b)(x0),p(b,p)(b(a)(x1),p(a,a)(a(b)(x2),x3))) -> 1174.19/295.30 p(b,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,a)(b(a)(x1),x3))) 1174.19/295.30 p(a,p)(a(b)(x0),p(b,p)(b(a)(x1),p(a,b)(a(b)(x2),x3))) -> 1174.19/295.30 p(b,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,b)(b(a)(x1),x3))) 1174.19/295.30 p(a,p)(a(b)(x0),p(b,p)(b(b)(x1),p(a,p)(a(p)(x2),x3))) -> 1174.19/295.30 p(p,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,p)(b(b)(x1),x3))) 1174.19/295.30 p(a,p)(a(b)(x0),p(b,p)(b(b)(x1),p(a,a)(a(p)(x2),x3))) -> 1174.19/295.30 p(p,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,a)(b(b)(x1),x3))) 1174.19/295.30 p(a,p)(a(b)(x0),p(b,p)(b(b)(x1),p(a,b)(a(p)(x2),x3))) -> 1174.19/295.30 p(p,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,b)(b(b)(x1),x3))) 1174.19/295.30 p(a,p)(a(b)(x0),p(b,p)(b(b)(x1),p(a,p)(a(a)(x2),x3))) -> 1174.19/295.30 p(a,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,p)(b(b)(x1),x3))) 1174.19/295.30 p(a,p)(a(b)(x0),p(b,p)(b(b)(x1),p(a,a)(a(a)(x2),x3))) -> 1174.19/295.30 p(a,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,a)(b(b)(x1),x3))) 1174.19/295.30 p(a,p)(a(b)(x0),p(b,p)(b(b)(x1),p(a,b)(a(a)(x2),x3))) -> 1174.19/295.30 p(a,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,b)(b(b)(x1),x3))) 1174.19/295.30 p(a,p)(a(b)(x0),p(b,p)(b(b)(x1),p(a,p)(a(b)(x2),x3))) -> 1174.19/295.30 p(b,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,p)(b(b)(x1),x3))) 1174.19/295.30 p(a,p)(a(b)(x0),p(b,p)(b(b)(x1),p(a,a)(a(b)(x2),x3))) -> 1174.19/295.30 p(b,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,a)(b(b)(x1),x3))) 1174.19/295.30 p(a,p)(a(b)(x0),p(b,p)(b(b)(x1),p(a,b)(a(b)(x2),x3))) -> 1174.19/295.30 p(b,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,b)(b(b)(x1),x3))) 1174.19/295.30 weak: 1174.19/295.30 1174.19/295.30 Matrix Interpretation Processor: dim=2 1174.19/295.30 1174.19/295.30 max_matrix: 1174.19/295.30 [1 3] 1174.19/295.30 [0 1] 1174.19/295.30 interpretation: 1174.19/295.30 [1 0] [0] 1174.19/295.30 [b(b)](x0) = [0 0]x0 + [3], 1174.19/295.30 1174.19/295.30 [1 0] 1174.19/295.30 [b(a)](x0) = [0 0]x0, 1174.19/295.30 1174.19/295.30 [0] 1174.19/295.30 [a(b)](x0) = x0 + [1], 1174.19/295.30 1174.19/295.30 [1 0] [1 0] 1174.19/295.30 [p(b,b)](x0, x1) = [0 0]x0 + [0 0]x1, 1174.19/295.30 1174.19/295.30 [1 3] [1] 1174.19/295.30 [p(a,b)](x0, x1) = x0 + [0 1]x1 + [2], 1174.19/295.30 1174.19/295.30 [1 2] [1 0] 1174.19/295.30 [p(b,a)](x0, x1) = [0 0]x0 + [0 0]x1, 1174.19/295.30 1174.19/295.30 [1 3] [3] 1174.19/295.30 [p(a,a)](x0, x1) = x0 + [0 0]x1 + [2], 1174.19/295.30 1174.19/295.30 [1 0] 1174.19/295.30 [a(a)](x0) = [0 0]x0, 1174.19/295.30 1174.19/295.30 [1 0] [1 0] [0] 1174.19/295.30 [p(p,p)](x0, x1) = [0 0]x0 + [0 0]x1 + [3], 1174.19/295.30 1174.19/295.30 [1 3] [0] 1174.19/295.30 [b(p)](x0) = [0 0]x0 + [1], 1174.19/295.30 1174.19/295.30 [1 0] [1 2] 1174.19/295.30 [p(b,p)](x0, x1) = [0 0]x0 + [0 1]x1, 1174.19/295.30 1174.19/295.30 [1 1] [0] 1174.19/295.30 [a(p)](x0) = [0 0]x0 + [1], 1174.19/295.30 1174.19/295.30 [1 0] [1 2] [0] 1174.19/295.30 [p(a,p)](x0, x1) = [0 0]x0 + [0 1]x1 + [2] 1174.19/295.30 orientation: 1174.19/295.30 [1 1] [1 3] [1 1] [1 6] [8] [1 1] [1 3] [1 0] [1 4] [0] 1174.19/295.30 p(a,p)(a(p)(x0),p(b,p)(b(p)(x1),p(a,p)(a(p)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [3] = p(p,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,p)(b(p)(x1),x3))) 1174.19/295.30 1174.19/295.30 [1 1] [1 3] [1 1] [1 3] [15] [1 1] [1 3] [1 0] [1 0] [2] 1174.19/295.30 p(a,p)(a(p)(x0),p(b,p)(b(p)(x1),p(a,a)(a(p)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [3] = p(p,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,a)(b(p)(x1),x3))) 1174.19/295.30 1174.19/295.30 [1 1] [1 3] [1 1] [1 7] [13] [1 1] [1 3] [1 0] [1 0] [0] 1174.19/295.30 p(a,p)(a(p)(x0),p(b,p)(b(p)(x1),p(a,b)(a(p)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [3] = p(p,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,b)(b(p)(x1),x3))) 1174.19/295.31 1174.19/295.31 [1 1] [1 3] [1 0] [1 6] [8] [1 1] [1 3] [1 0] [1 6] [4] 1174.19/295.31 p(a,p)(a(p)(x0),p(b,p)(b(p)(x1),p(a,p)(a(a)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] = p(a,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,p)(b(p)(x1),x3))) 1174.19/295.31 1174.19/295.31 [1 1] [1 3] [1 0] [1 3] [11] [1 1] [1 3] [1 0] [1 0] [6] 1174.19/295.31 p(a,p)(a(p)(x0),p(b,p)(b(p)(x1),p(a,a)(a(a)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [4 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [4] = p(a,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,a)(b(p)(x1),x3))) 1174.19/295.31 1174.19/295.31 [1 1] [1 3] [1 0] [1 7] [9] [1 1] [1 3] [1 0] [1 0] [4] 1174.19/295.31 p(a,p)(a(p)(x0),p(b,p)(b(p)(x1),p(a,b)(a(a)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [4] = p(a,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,b)(b(p)(x1),x3))) 1174.19/295.31 1174.19/295.31 [1 1] [1 3] [1 0] [1 6] [8] [1 1] [1 3] [1 0] [1 6] [4] 1174.19/295.31 p(a,p)(a(p)(x0),p(b,p)(b(p)(x1),p(a,p)(a(b)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [2] = p(b,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,p)(b(p)(x1),x3))) 1174.19/295.31 1174.19/295.31 [1 1] [1 3] [1 4] [1 3] [15] [1 1] [1 3] [1 0] [1 0] [6] 1174.19/295.31 p(a,p)(a(p)(x0),p(b,p)(b(p)(x1),p(a,a)(a(b)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 1]x2 + [0 0]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [2] = p(b,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,a)(b(p)(x1),x3))) 1174.19/295.31 1174.19/295.31 [1 1] [1 3] [1 4] [1 7] [13] [1 1] [1 3] [1 0] [1 0] [4] 1174.19/295.31 p(a,p)(a(p)(x0),p(b,p)(b(p)(x1),p(a,b)(a(b)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 1]x2 + [0 1]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [2] = p(b,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,b)(b(p)(x1),x3))) 1174.19/295.31 1174.19/295.31 [1 1] [1 0] [1 1] [1 6] [8] [1 1] [1 0] [1 0] [1 4] [0] 1174.19/295.31 p(a,p)(a(p)(x0),p(b,p)(b(a)(x1),p(a,p)(a(p)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [3] = p(p,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,p)(b(a)(x1),x3))) 1174.19/295.31 1174.19/295.31 [1 1] [1 0] [1 1] [1 3] [15] [1 1] [1 0] [1 0] [1 0] [0] 1174.19/295.31 p(a,p)(a(p)(x0),p(b,p)(b(a)(x1),p(a,a)(a(p)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [3] = p(p,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,a)(b(a)(x1),x3))) 1174.19/295.31 1174.19/295.31 [1 1] [1 0] [1 1] [1 7] [13] [1 1] [1 0] [1 0] [1 0] [0] 1174.19/295.31 p(a,p)(a(p)(x0),p(b,p)(b(a)(x1),p(a,b)(a(p)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [3] = p(p,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,b)(b(a)(x1),x3))) 1174.19/295.31 1174.19/295.31 [1 1] [1 0] [1 0] [1 6] [8] [1 1] [1 0] [1 0] [1 6] [4] 1174.19/295.31 p(a,p)(a(p)(x0),p(b,p)(b(a)(x1),p(a,p)(a(a)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] = p(a,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,p)(b(a)(x1),x3))) 1174.19/295.32 1174.19/295.32 [1 1] [1 0] [1 0] [1 3] [11] [1 1] [1 0] [1 0] [1 0] [4] 1174.19/295.32 p(a,p)(a(p)(x0),p(b,p)(b(a)(x1),p(a,a)(a(a)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [4 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [4] = p(a,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,a)(b(a)(x1),x3))) 1174.19/295.32 1174.19/295.32 [1 1] [1 0] [1 0] [1 7] [9] [1 1] [1 0] [1 0] [1 0] [4] 1174.19/295.32 p(a,p)(a(p)(x0),p(b,p)(b(a)(x1),p(a,b)(a(a)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [4] = p(a,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,b)(b(a)(x1),x3))) 1174.19/295.32 1174.19/295.32 [1 1] [1 0] [1 0] [1 6] [8] [1 1] [1 0] [1 0] [1 6] [4] 1174.19/295.32 p(a,p)(a(p)(x0),p(b,p)(b(a)(x1),p(a,p)(a(b)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [2] = p(b,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,p)(b(a)(x1),x3))) 1174.19/295.32 1174.19/295.32 [1 1] [1 0] [1 4] [1 3] [15] [1 1] [1 0] [1 0] [1 0] [4] 1174.19/295.32 p(a,p)(a(p)(x0),p(b,p)(b(a)(x1),p(a,a)(a(b)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 1]x2 + [0 0]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [2] = p(b,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,a)(b(a)(x1),x3))) 1174.19/295.32 1174.19/295.32 [1 1] [1 0] [1 4] [1 7] [13] [1 1] [1 0] [1 0] [1 0] [4] 1174.19/295.32 p(a,p)(a(p)(x0),p(b,p)(b(a)(x1),p(a,b)(a(b)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 1]x2 + [0 1]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [2] = p(b,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,b)(b(a)(x1),x3))) 1174.19/295.32 1174.19/295.32 [1 1] [1 0] [1 1] [1 6] [8] [1 1] [1 0] [1 0] [1 4] [0] 1174.19/295.32 p(a,p)(a(p)(x0),p(b,p)(b(b)(x1),p(a,p)(a(p)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [3] = p(p,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,p)(b(b)(x1),x3))) 1174.19/295.32 1174.19/295.32 [1 1] [1 0] [1 1] [1 3] [15] [1 1] [1 0] [1 0] [1 0] [6] 1174.19/295.32 p(a,p)(a(p)(x0),p(b,p)(b(b)(x1),p(a,a)(a(p)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [3] = p(p,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,a)(b(b)(x1),x3))) 1174.19/295.32 1174.19/295.32 [1 1] [1 0] [1 1] [1 7] [13] [1 1] [1 0] [1 0] [1 0] [0] 1174.19/295.32 p(a,p)(a(p)(x0),p(b,p)(b(b)(x1),p(a,b)(a(p)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [3] = p(p,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,b)(b(b)(x1),x3))) 1174.19/295.32 1174.19/295.32 [1 1] [1 0] [1 0] [1 6] [8] [1 1] [1 0] [1 0] [1 6] [4] 1174.19/295.32 p(a,p)(a(p)(x0),p(b,p)(b(b)(x1),p(a,p)(a(a)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] = p(a,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,p)(b(b)(x1),x3))) 1174.19/295.32 1174.19/295.32 [1 1] [1 0] [1 0] [1 3] [11] [1 1] [1 0] [1 0] [1 0] [10] 1174.19/295.32 p(a,p)(a(p)(x0),p(b,p)(b(b)(x1),p(a,a)(a(a)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [4 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [4 ] = p(a,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,a)(b(b)(x1),x3))) 1174.19/295.32 1174.19/295.32 [1 1] [1 0] [1 0] [1 7] [9] [1 1] [1 0] [1 0] [1 0] [4] 1174.19/295.32 p(a,p)(a(p)(x0),p(b,p)(b(b)(x1),p(a,b)(a(a)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [4] = p(a,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,b)(b(b)(x1),x3))) 1174.19/295.32 1174.19/295.32 [1 1] [1 0] [1 0] [1 6] [8] [1 1] [1 0] [1 0] [1 6] [4] 1174.19/295.32 p(a,p)(a(p)(x0),p(b,p)(b(b)(x1),p(a,p)(a(b)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [2] = p(b,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,p)(b(b)(x1),x3))) 1174.19/295.32 1174.19/295.32 [1 1] [1 0] [1 4] [1 3] [15] [1 1] [1 0] [1 0] [1 0] [10] 1174.19/295.32 p(a,p)(a(p)(x0),p(b,p)(b(b)(x1),p(a,a)(a(b)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 1]x2 + [0 0]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [2 ] = p(b,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,a)(b(b)(x1),x3))) 1174.19/295.32 1174.19/295.32 [1 1] [1 0] [1 4] [1 7] [13] [1 1] [1 0] [1 0] [1 0] [4] 1174.19/295.32 p(a,p)(a(p)(x0),p(b,p)(b(b)(x1),p(a,b)(a(b)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 1]x2 + [0 1]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [2] = p(b,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,b)(b(b)(x1),x3))) 1174.19/295.32 1174.19/295.32 [1 0] [1 3] [1 1] [1 6] [8] [1 0] [1 3] [1 0] [1 4] [0] 1174.19/295.32 p(a,p)(a(a)(x0),p(b,p)(b(p)(x1),p(a,p)(a(p)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [3] = p(p,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,p)(b(p)(x1),x3))) 1174.19/295.32 1174.19/295.32 [1 0] [1 3] [1 1] [1 3] [15] [1 0] [1 3] [1 0] [1 0] [2] 1174.19/295.32 p(a,p)(a(a)(x0),p(b,p)(b(p)(x1),p(a,a)(a(p)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [3] = p(p,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,a)(b(p)(x1),x3))) 1174.19/295.32 1174.19/295.32 [1 0] [1 3] [1 1] [1 7] [13] [1 0] [1 3] [1 0] [1 0] [0] 1174.19/295.32 p(a,p)(a(a)(x0),p(b,p)(b(p)(x1),p(a,b)(a(p)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [3] = p(p,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,b)(b(p)(x1),x3))) 1174.19/295.32 1174.19/295.32 [1 0] [1 3] [1 0] [1 6] [8] [1 0] [1 3] [1 0] [1 6] [4] 1174.19/295.32 p(a,p)(a(a)(x0),p(b,p)(b(p)(x1),p(a,p)(a(a)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] = p(a,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,p)(b(p)(x1),x3))) 1174.19/295.32 1174.19/295.32 [1 0] [1 3] [1 0] [1 3] [11] [1 0] [1 3] [1 0] [1 0] [6] 1174.19/295.32 p(a,p)(a(a)(x0),p(b,p)(b(p)(x1),p(a,a)(a(a)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [4 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [4] = p(a,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,a)(b(p)(x1),x3))) 1174.19/295.33 1174.19/295.33 [1 0] [1 3] [1 0] [1 7] [9] [1 0] [1 3] [1 0] [1 0] [4] 1174.19/295.33 p(a,p)(a(a)(x0),p(b,p)(b(p)(x1),p(a,b)(a(a)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [4] = p(a,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,b)(b(p)(x1),x3))) 1174.19/295.33 1174.19/295.33 [1 0] [1 3] [1 0] [1 6] [8] [1 0] [1 3] [1 0] [1 6] [4] 1174.19/295.33 p(a,p)(a(a)(x0),p(b,p)(b(p)(x1),p(a,p)(a(b)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [2] = p(b,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,p)(b(p)(x1),x3))) 1174.19/295.33 1174.19/295.33 [1 0] [1 3] [1 4] [1 3] [15] [1 0] [1 3] [1 0] [1 0] [6] 1174.19/295.33 p(a,p)(a(a)(x0),p(b,p)(b(p)(x1),p(a,a)(a(b)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 1]x2 + [0 0]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [2] = p(b,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,a)(b(p)(x1),x3))) 1174.19/295.33 1174.19/295.33 [1 0] [1 3] [1 4] [1 7] [13] [1 0] [1 3] [1 0] [1 0] [4] 1174.19/295.33 p(a,p)(a(a)(x0),p(b,p)(b(p)(x1),p(a,b)(a(b)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 1]x2 + [0 1]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [2] = p(b,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,b)(b(p)(x1),x3))) 1174.19/295.33 1174.19/295.33 [1 0] [1 0] [1 1] [1 6] [8] [1 0] [1 0] [1 0] [1 4] [0] 1174.19/295.33 p(a,p)(a(a)(x0),p(b,p)(b(a)(x1),p(a,p)(a(p)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [3] = p(p,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,p)(b(a)(x1),x3))) 1174.19/295.33 1174.19/295.33 [1 0] [1 0] [1 1] [1 3] [15] [1 0] [1 0] [1 0] [1 0] [0] 1174.19/295.33 p(a,p)(a(a)(x0),p(b,p)(b(a)(x1),p(a,a)(a(p)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [3] = p(p,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,a)(b(a)(x1),x3))) 1174.19/295.33 1174.19/295.33 [1 0] [1 0] [1 1] [1 7] [13] [1 0] [1 0] [1 0] [1 0] [0] 1174.19/295.33 p(a,p)(a(a)(x0),p(b,p)(b(a)(x1),p(a,b)(a(p)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [3] = p(p,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,b)(b(a)(x1),x3))) 1174.19/295.33 1174.19/295.33 [1 0] [1 0] [1 0] [1 6] [8] [1 0] [1 0] [1 0] [1 6] [4] 1174.19/295.33 p(a,p)(a(a)(x0),p(b,p)(b(a)(x1),p(a,p)(a(a)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] = p(a,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,p)(b(a)(x1),x3))) 1174.19/295.33 1174.19/295.33 [1 0] [1 0] [1 0] [1 3] [11] [1 0] [1 0] [1 0] [1 0] [4] 1174.19/295.33 p(a,p)(a(a)(x0),p(b,p)(b(a)(x1),p(a,a)(a(a)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [4 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [4] = p(a,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,a)(b(a)(x1),x3))) 1174.19/295.33 1174.19/295.33 [1 0] [1 0] [1 0] [1 7] [9] [1 0] [1 0] [1 0] [1 0] [4] 1174.19/295.33 p(a,p)(a(a)(x0),p(b,p)(b(a)(x1),p(a,b)(a(a)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [4] = p(a,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,b)(b(a)(x1),x3))) 1174.19/295.34 1174.19/295.34 [1 0] [1 0] [1 0] [1 6] [8] [1 0] [1 0] [1 0] [1 6] [4] 1174.19/295.34 p(a,p)(a(a)(x0),p(b,p)(b(a)(x1),p(a,p)(a(b)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [2] = p(b,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,p)(b(a)(x1),x3))) 1174.19/295.34 1174.19/295.34 [1 0] [1 0] [1 4] [1 3] [15] [1 0] [1 0] [1 0] [1 0] [4] 1174.19/295.34 p(a,p)(a(a)(x0),p(b,p)(b(a)(x1),p(a,a)(a(b)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 1]x2 + [0 0]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [2] = p(b,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,a)(b(a)(x1),x3))) 1174.19/295.34 1174.19/295.34 [1 0] [1 0] [1 4] [1 7] [13] [1 0] [1 0] [1 0] [1 0] [4] 1174.19/295.34 p(a,p)(a(a)(x0),p(b,p)(b(a)(x1),p(a,b)(a(b)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 1]x2 + [0 1]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [2] = p(b,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,b)(b(a)(x1),x3))) 1174.19/295.34 1174.19/295.34 [1 0] [1 0] [1 1] [1 6] [8] [1 0] [1 0] [1 0] [1 4] [0] 1174.19/295.34 p(a,p)(a(a)(x0),p(b,p)(b(b)(x1),p(a,p)(a(p)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [3] = p(p,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,p)(b(b)(x1),x3))) 1174.19/295.34 1174.19/295.34 [1 0] [1 0] [1 1] [1 3] [15] [1 0] [1 0] [1 0] [1 0] [6] 1174.19/295.34 p(a,p)(a(a)(x0),p(b,p)(b(b)(x1),p(a,a)(a(p)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [3] = p(p,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,a)(b(b)(x1),x3))) 1174.19/295.34 1174.19/295.34 [1 0] [1 0] [1 1] [1 7] [13] [1 0] [1 0] [1 0] [1 0] [0] 1174.19/295.34 p(a,p)(a(a)(x0),p(b,p)(b(b)(x1),p(a,b)(a(p)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [3] = p(p,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,b)(b(b)(x1),x3))) 1174.19/295.34 1174.19/295.34 [1 0] [1 0] [1 0] [1 6] [8] [1 0] [1 0] [1 0] [1 6] [4] 1174.19/295.34 p(a,p)(a(a)(x0),p(b,p)(b(b)(x1),p(a,p)(a(a)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] = p(a,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,p)(b(b)(x1),x3))) 1174.19/295.34 1174.19/295.34 [1 0] [1 0] [1 0] [1 3] [11] [1 0] [1 0] [1 0] [1 0] [10] 1174.19/295.34 p(a,p)(a(a)(x0),p(b,p)(b(b)(x1),p(a,a)(a(a)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [4 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [4 ] = p(a,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,a)(b(b)(x1),x3))) 1174.19/295.34 1174.19/295.34 [1 0] [1 0] [1 0] [1 7] [9] [1 0] [1 0] [1 0] [1 0] [4] 1174.19/295.34 p(a,p)(a(a)(x0),p(b,p)(b(b)(x1),p(a,b)(a(a)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [4] = p(a,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,b)(b(b)(x1),x3))) 1174.19/295.34 1174.19/295.34 [1 0] [1 0] [1 0] [1 6] [8] [1 0] [1 0] [1 0] [1 6] [4] 1174.19/295.35 p(a,p)(a(a)(x0),p(b,p)(b(b)(x1),p(a,p)(a(b)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [2] = p(b,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,p)(b(b)(x1),x3))) 1174.19/295.35 1174.19/295.35 [1 0] [1 0] [1 4] [1 3] [15] [1 0] [1 0] [1 0] [1 0] [10] 1174.19/295.35 p(a,p)(a(a)(x0),p(b,p)(b(b)(x1),p(a,a)(a(b)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 1]x2 + [0 0]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [2 ] = p(b,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,a)(b(b)(x1),x3))) 1174.19/295.35 1174.19/295.35 [1 0] [1 0] [1 4] [1 7] [13] [1 0] [1 0] [1 0] [1 0] [4] 1174.19/295.35 p(a,p)(a(a)(x0),p(b,p)(b(b)(x1),p(a,b)(a(b)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 1]x2 + [0 1]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [2] = p(b,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,b)(b(b)(x1),x3))) 1174.19/295.35 1174.19/295.35 [1 0] [1 3] [1 1] [1 6] [8] [1 0] [1 3] [1 0] [1 4] [0] 1174.19/295.35 p(a,p)(a(b)(x0),p(b,p)(b(p)(x1),p(a,p)(a(p)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [3] = p(p,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,p)(b(p)(x1),x3))) 1174.19/295.35 1174.19/295.35 [1 0] [1 3] [1 1] [1 3] [15] [1 0] [1 3] [1 0] [1 0] [2] 1174.19/295.35 p(a,p)(a(b)(x0),p(b,p)(b(p)(x1),p(a,a)(a(p)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [3] = p(p,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,a)(b(p)(x1),x3))) 1174.19/295.35 1174.19/295.35 [1 0] [1 3] [1 1] [1 7] [13] [1 0] [1 3] [1 0] [1 0] [0] 1174.19/295.35 p(a,p)(a(b)(x0),p(b,p)(b(p)(x1),p(a,b)(a(p)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [3] = p(p,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,b)(b(p)(x1),x3))) 1174.19/295.35 1174.19/295.35 [1 0] [1 3] [1 0] [1 6] [8] [1 0] [1 3] [1 0] [1 6] [4] 1174.19/295.35 p(a,p)(a(b)(x0),p(b,p)(b(p)(x1),p(a,p)(a(a)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] = p(a,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,p)(b(p)(x1),x3))) 1174.19/295.35 1174.19/295.35 [1 0] [1 3] [1 0] [1 3] [11] [1 0] [1 3] [1 0] [1 0] [6] 1174.19/295.35 p(a,p)(a(b)(x0),p(b,p)(b(p)(x1),p(a,a)(a(a)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [4 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [4] = p(a,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,a)(b(p)(x1),x3))) 1174.19/295.35 1174.19/295.35 [1 0] [1 3] [1 0] [1 7] [9] [1 0] [1 3] [1 0] [1 0] [4] 1174.19/295.35 p(a,p)(a(b)(x0),p(b,p)(b(p)(x1),p(a,b)(a(a)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [4] = p(a,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,b)(b(p)(x1),x3))) 1174.19/295.35 1174.19/295.35 [1 0] [1 3] [1 0] [1 6] [8] [1 0] [1 3] [1 0] [1 6] [4] 1174.19/295.35 p(a,p)(a(b)(x0),p(b,p)(b(p)(x1),p(a,p)(a(b)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [2] = p(b,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,p)(b(p)(x1),x3))) 1174.19/295.36 1174.19/295.36 [1 0] [1 3] [1 4] [1 3] [15] [1 0] [1 3] [1 0] [1 0] [6] 1174.19/295.36 p(a,p)(a(b)(x0),p(b,p)(b(p)(x1),p(a,a)(a(b)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 1]x2 + [0 0]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [2] = p(b,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,a)(b(p)(x1),x3))) 1174.19/295.36 1174.19/295.36 [1 0] [1 3] [1 4] [1 7] [13] [1 0] [1 3] [1 0] [1 0] [4] 1174.19/295.36 p(a,p)(a(b)(x0),p(b,p)(b(p)(x1),p(a,b)(a(b)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 1]x2 + [0 1]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [2] = p(b,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,b)(b(p)(x1),x3))) 1174.19/295.36 1174.19/295.36 [1 0] [1 0] [1 1] [1 6] [8] [1 0] [1 0] [1 0] [1 4] [0] 1174.19/295.36 p(a,p)(a(b)(x0),p(b,p)(b(a)(x1),p(a,p)(a(p)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [3] = p(p,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,p)(b(a)(x1),x3))) 1174.19/295.36 1174.19/295.36 [1 0] [1 0] [1 1] [1 3] [15] [1 0] [1 0] [1 0] [1 0] [0] 1174.19/295.36 p(a,p)(a(b)(x0),p(b,p)(b(a)(x1),p(a,a)(a(p)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [3] = p(p,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,a)(b(a)(x1),x3))) 1174.19/295.36 1174.19/295.36 [1 0] [1 0] [1 1] [1 7] [13] [1 0] [1 0] [1 0] [1 0] [0] 1174.19/295.36 p(a,p)(a(b)(x0),p(b,p)(b(a)(x1),p(a,b)(a(p)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [3] = p(p,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,b)(b(a)(x1),x3))) 1174.19/295.36 1174.19/295.36 [1 0] [1 0] [1 0] [1 6] [8] [1 0] [1 0] [1 0] [1 6] [4] 1174.19/295.36 p(a,p)(a(b)(x0),p(b,p)(b(a)(x1),p(a,p)(a(a)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] = p(a,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,p)(b(a)(x1),x3))) 1174.19/295.36 1174.19/295.36 [1 0] [1 0] [1 0] [1 3] [11] [1 0] [1 0] [1 0] [1 0] [4] 1174.19/295.36 p(a,p)(a(b)(x0),p(b,p)(b(a)(x1),p(a,a)(a(a)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [4 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [4] = p(a,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,a)(b(a)(x1),x3))) 1174.19/295.36 1174.19/295.36 [1 0] [1 0] [1 0] [1 7] [9] [1 0] [1 0] [1 0] [1 0] [4] 1174.19/295.36 p(a,p)(a(b)(x0),p(b,p)(b(a)(x1),p(a,b)(a(a)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [4] = p(a,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,b)(b(a)(x1),x3))) 1174.19/295.36 1174.19/295.36 [1 0] [1 0] [1 0] [1 6] [8] [1 0] [1 0] [1 0] [1 6] [4] 1174.19/295.36 p(a,p)(a(b)(x0),p(b,p)(b(a)(x1),p(a,p)(a(b)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [2] = p(b,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,p)(b(a)(x1),x3))) 1174.19/295.36 1174.19/295.36 [1 0] [1 0] [1 4] [1 3] [15] [1 0] [1 0] [1 0] [1 0] [4] 1174.19/295.36 p(a,p)(a(b)(x0),p(b,p)(b(a)(x1),p(a,a)(a(b)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 1]x2 + [0 0]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [2] = p(b,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,a)(b(a)(x1),x3))) 1174.19/295.36 1174.19/295.36 [1 0] [1 0] [1 4] [1 7] [13] [1 0] [1 0] [1 0] [1 0] [4] 1174.19/295.36 p(a,p)(a(b)(x0),p(b,p)(b(a)(x1),p(a,b)(a(b)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 1]x2 + [0 1]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [2] = p(b,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,b)(b(a)(x1),x3))) 1174.19/295.36 1174.19/295.36 [1 0] [1 0] [1 1] [1 6] [8] [1 0] [1 0] [1 0] [1 4] [0] 1174.19/295.36 p(a,p)(a(b)(x0),p(b,p)(b(b)(x1),p(a,p)(a(p)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [3] = p(p,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,p)(b(b)(x1),x3))) 1174.19/295.36 1174.19/295.36 [1 0] [1 0] [1 1] [1 3] [15] [1 0] [1 0] [1 0] [1 0] [6] 1174.19/295.36 p(a,p)(a(b)(x0),p(b,p)(b(b)(x1),p(a,a)(a(p)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [3] = p(p,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,a)(b(b)(x1),x3))) 1174.19/295.36 1174.19/295.36 [1 0] [1 0] [1 1] [1 7] [13] [1 0] [1 0] [1 0] [1 0] [0] 1174.19/295.36 p(a,p)(a(b)(x0),p(b,p)(b(b)(x1),p(a,b)(a(p)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [3] = p(p,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,b)(b(b)(x1),x3))) 1174.19/295.36 1174.19/295.36 [1 0] [1 0] [1 0] [1 6] [8] [1 0] [1 0] [1 0] [1 6] [4] 1174.19/295.36 p(a,p)(a(b)(x0),p(b,p)(b(b)(x1),p(a,p)(a(a)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] = p(a,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,p)(b(b)(x1),x3))) 1174.19/295.36 1174.19/295.36 [1 0] [1 0] [1 0] [1 3] [11] [1 0] [1 0] [1 0] [1 0] [10] 1174.19/295.36 p(a,p)(a(b)(x0),p(b,p)(b(b)(x1),p(a,a)(a(a)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [4 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [4 ] = p(a,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,a)(b(b)(x1),x3))) 1174.19/295.36 1174.19/295.36 [1 0] [1 0] [1 0] [1 7] [9] [1 0] [1 0] [1 0] [1 0] [4] 1174.19/295.36 p(a,p)(a(b)(x0),p(b,p)(b(b)(x1),p(a,b)(a(a)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [4] = p(a,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,b)(b(b)(x1),x3))) 1174.19/295.36 1174.19/295.36 [1 0] [1 0] [1 0] [1 6] [8] [1 0] [1 0] [1 0] [1 6] [4] 1174.19/295.36 p(a,p)(a(b)(x0),p(b,p)(b(b)(x1),p(a,p)(a(b)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [4] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 1]x3 + [2] = p(b,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,p)(b(b)(x1),x3))) 1174.19/295.36 1174.19/295.36 [1 0] [1 0] [1 4] [1 3] [15] [1 0] [1 0] [1 0] [1 0] [10] 1174.19/295.36 p(a,p)(a(b)(x0),p(b,p)(b(b)(x1),p(a,a)(a(b)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 1]x2 + [0 0]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [2 ] = p(b,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,a)(b(b)(x1),x3))) 1174.19/295.36 1174.19/295.36 [1 0] [1 0] [1 4] [1 7] [13] [1 0] [1 0] [1 0] [1 0] [4] 1174.19/295.37 p(a,p)(a(b)(x0),p(b,p)(b(b)(x1),p(a,b)(a(b)(x2),x3))) = [0 0]x0 + [0 0]x1 + [0 1]x2 + [0 1]x3 + [5 ] >= [0 0]x0 + [0 0]x1 + [0 0]x2 + [0 0]x3 + [2] = p(b,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,b)(b(b)(x1),x3))) 1174.19/295.37 problem: 1174.19/295.37 strict: 1174.19/295.37 1174.19/295.37 weak: 1174.19/295.37 p(a,p)(a(p)(x0),p(b,p)(b(p)(x1),p(a,p)(a(p)(x2),x3))) -> 1174.19/295.37 p(p,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,p)(b(p)(x1),x3))) 1174.19/295.37 p(a,p)(a(p)(x0),p(b,p)(b(p)(x1),p(a,a)(a(p)(x2),x3))) -> 1174.19/295.37 p(p,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,a)(b(p)(x1),x3))) 1174.19/295.37 p(a,p)(a(p)(x0),p(b,p)(b(p)(x1),p(a,b)(a(p)(x2),x3))) -> 1174.19/295.37 p(p,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,b)(b(p)(x1),x3))) 1174.19/295.37 p(a,p)(a(p)(x0),p(b,p)(b(p)(x1),p(a,p)(a(a)(x2),x3))) -> 1174.19/295.37 p(a,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,p)(b(p)(x1),x3))) 1174.19/295.37 p(a,p)(a(p)(x0),p(b,p)(b(p)(x1),p(a,a)(a(a)(x2),x3))) -> 1174.19/295.37 p(a,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,a)(b(p)(x1),x3))) 1174.19/295.37 p(a,p)(a(p)(x0),p(b,p)(b(p)(x1),p(a,b)(a(a)(x2),x3))) -> 1174.19/295.37 p(a,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,b)(b(p)(x1),x3))) 1174.19/295.37 p(a,p)(a(p)(x0),p(b,p)(b(p)(x1),p(a,p)(a(b)(x2),x3))) -> 1174.19/295.37 p(b,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,p)(b(p)(x1),x3))) 1174.19/295.37 p(a,p)(a(p)(x0),p(b,p)(b(p)(x1),p(a,a)(a(b)(x2),x3))) -> 1174.19/295.37 p(b,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,a)(b(p)(x1),x3))) 1174.19/295.37 p(a,p)(a(p)(x0),p(b,p)(b(p)(x1),p(a,b)(a(b)(x2),x3))) -> 1174.19/295.37 p(b,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,b)(b(p)(x1),x3))) 1174.19/295.37 p(a,p)(a(p)(x0),p(b,p)(b(a)(x1),p(a,p)(a(p)(x2),x3))) -> 1174.19/295.37 p(p,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,p)(b(a)(x1),x3))) 1174.19/295.37 p(a,p)(a(p)(x0),p(b,p)(b(a)(x1),p(a,a)(a(p)(x2),x3))) -> 1174.19/295.37 p(p,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,a)(b(a)(x1),x3))) 1174.19/295.37 p(a,p)(a(p)(x0),p(b,p)(b(a)(x1),p(a,b)(a(p)(x2),x3))) -> 1174.19/295.37 p(p,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,b)(b(a)(x1),x3))) 1174.19/295.37 p(a,p)(a(p)(x0),p(b,p)(b(a)(x1),p(a,p)(a(a)(x2),x3))) -> 1174.19/295.37 p(a,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,p)(b(a)(x1),x3))) 1174.19/295.37 p(a,p)(a(p)(x0),p(b,p)(b(a)(x1),p(a,a)(a(a)(x2),x3))) -> 1174.19/295.37 p(a,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,a)(b(a)(x1),x3))) 1174.19/295.37 p(a,p)(a(p)(x0),p(b,p)(b(a)(x1),p(a,b)(a(a)(x2),x3))) -> 1174.19/295.37 p(a,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,b)(b(a)(x1),x3))) 1174.19/295.37 p(a,p)(a(p)(x0),p(b,p)(b(a)(x1),p(a,p)(a(b)(x2),x3))) -> 1174.19/295.37 p(b,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,p)(b(a)(x1),x3))) 1174.19/295.37 p(a,p)(a(p)(x0),p(b,p)(b(a)(x1),p(a,a)(a(b)(x2),x3))) -> 1174.19/295.37 p(b,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,a)(b(a)(x1),x3))) 1174.19/295.37 p(a,p)(a(p)(x0),p(b,p)(b(a)(x1),p(a,b)(a(b)(x2),x3))) -> 1174.19/295.37 p(b,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,b)(b(a)(x1),x3))) 1174.19/295.37 p(a,p)(a(p)(x0),p(b,p)(b(b)(x1),p(a,p)(a(p)(x2),x3))) -> 1174.19/295.37 p(p,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,p)(b(b)(x1),x3))) 1174.19/295.37 p(a,p)(a(p)(x0),p(b,p)(b(b)(x1),p(a,a)(a(p)(x2),x3))) -> 1174.19/295.37 p(p,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,a)(b(b)(x1),x3))) 1174.19/295.37 p(a,p)(a(p)(x0),p(b,p)(b(b)(x1),p(a,b)(a(p)(x2),x3))) -> 1174.19/295.37 p(p,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,b)(b(b)(x1),x3))) 1174.19/295.37 p(a,p)(a(p)(x0),p(b,p)(b(b)(x1),p(a,p)(a(a)(x2),x3))) -> 1174.19/295.37 p(a,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,p)(b(b)(x1),x3))) 1174.19/295.37 p(a,p)(a(p)(x0),p(b,p)(b(b)(x1),p(a,a)(a(a)(x2),x3))) -> 1174.19/295.37 p(a,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,a)(b(b)(x1),x3))) 1174.19/295.37 p(a,p)(a(p)(x0),p(b,p)(b(b)(x1),p(a,b)(a(a)(x2),x3))) -> 1174.19/295.37 p(a,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,b)(b(b)(x1),x3))) 1174.19/295.37 p(a,p)(a(p)(x0),p(b,p)(b(b)(x1),p(a,p)(a(b)(x2),x3))) -> 1174.19/295.37 p(b,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,p)(b(b)(x1),x3))) 1174.19/295.37 p(a,p)(a(p)(x0),p(b,p)(b(b)(x1),p(a,a)(a(b)(x2),x3))) -> 1174.19/295.37 p(b,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,a)(b(b)(x1),x3))) 1174.19/295.37 p(a,p)(a(p)(x0),p(b,p)(b(b)(x1),p(a,b)(a(b)(x2),x3))) -> 1174.19/295.37 p(b,p)(x2,p(a,p)(a(a)(a(p)(x0)),p(b,b)(b(b)(x1),x3))) 1174.19/295.37 p(a,p)(a(a)(x0),p(b,p)(b(p)(x1),p(a,p)(a(p)(x2),x3))) -> 1174.19/295.37 p(p,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,p)(b(p)(x1),x3))) 1174.19/295.37 p(a,p)(a(a)(x0),p(b,p)(b(p)(x1),p(a,a)(a(p)(x2),x3))) -> 1174.19/295.37 p(p,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,a)(b(p)(x1),x3))) 1174.19/295.37 p(a,p)(a(a)(x0),p(b,p)(b(p)(x1),p(a,b)(a(p)(x2),x3))) -> 1174.19/295.37 p(p,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,b)(b(p)(x1),x3))) 1174.19/295.37 p(a,p)(a(a)(x0),p(b,p)(b(p)(x1),p(a,p)(a(a)(x2),x3))) -> 1174.19/295.37 p(a,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,p)(b(p)(x1),x3))) 1174.19/295.38 p(a,p)(a(a)(x0),p(b,p)(b(p)(x1),p(a,a)(a(a)(x2),x3))) -> 1174.19/295.38 p(a,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,a)(b(p)(x1),x3))) 1174.19/295.38 p(a,p)(a(a)(x0),p(b,p)(b(p)(x1),p(a,b)(a(a)(x2),x3))) -> 1174.19/295.38 p(a,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,b)(b(p)(x1),x3))) 1174.19/295.38 p(a,p)(a(a)(x0),p(b,p)(b(p)(x1),p(a,p)(a(b)(x2),x3))) -> 1174.19/295.38 p(b,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,p)(b(p)(x1),x3))) 1174.19/295.38 p(a,p)(a(a)(x0),p(b,p)(b(p)(x1),p(a,a)(a(b)(x2),x3))) -> 1174.19/295.38 p(b,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,a)(b(p)(x1),x3))) 1174.19/295.38 p(a,p)(a(a)(x0),p(b,p)(b(p)(x1),p(a,b)(a(b)(x2),x3))) -> 1174.19/295.38 p(b,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,b)(b(p)(x1),x3))) 1174.19/295.38 p(a,p)(a(a)(x0),p(b,p)(b(a)(x1),p(a,p)(a(p)(x2),x3))) -> 1174.19/295.38 p(p,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,p)(b(a)(x1),x3))) 1174.19/295.38 p(a,p)(a(a)(x0),p(b,p)(b(a)(x1),p(a,a)(a(p)(x2),x3))) -> 1174.19/295.38 p(p,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,a)(b(a)(x1),x3))) 1174.19/295.38 p(a,p)(a(a)(x0),p(b,p)(b(a)(x1),p(a,b)(a(p)(x2),x3))) -> 1174.19/295.38 p(p,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,b)(b(a)(x1),x3))) 1174.19/295.38 p(a,p)(a(a)(x0),p(b,p)(b(a)(x1),p(a,p)(a(a)(x2),x3))) -> 1174.19/295.38 p(a,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,p)(b(a)(x1),x3))) 1174.19/295.38 p(a,p)(a(a)(x0),p(b,p)(b(a)(x1),p(a,a)(a(a)(x2),x3))) -> 1174.19/295.38 p(a,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,a)(b(a)(x1),x3))) 1174.19/295.38 p(a,p)(a(a)(x0),p(b,p)(b(a)(x1),p(a,b)(a(a)(x2),x3))) -> 1174.19/295.38 p(a,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,b)(b(a)(x1),x3))) 1174.19/295.38 p(a,p)(a(a)(x0),p(b,p)(b(a)(x1),p(a,p)(a(b)(x2),x3))) -> 1174.19/295.38 p(b,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,p)(b(a)(x1),x3))) 1174.19/295.38 p(a,p)(a(a)(x0),p(b,p)(b(a)(x1),p(a,a)(a(b)(x2),x3))) -> 1174.19/295.38 p(b,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,a)(b(a)(x1),x3))) 1174.19/295.38 p(a,p)(a(a)(x0),p(b,p)(b(a)(x1),p(a,b)(a(b)(x2),x3))) -> 1174.19/295.38 p(b,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,b)(b(a)(x1),x3))) 1174.19/295.38 p(a,p)(a(a)(x0),p(b,p)(b(b)(x1),p(a,p)(a(p)(x2),x3))) -> 1174.19/295.38 p(p,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,p)(b(b)(x1),x3))) 1174.19/295.38 p(a,p)(a(a)(x0),p(b,p)(b(b)(x1),p(a,a)(a(p)(x2),x3))) -> 1174.19/295.38 p(p,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,a)(b(b)(x1),x3))) 1174.19/295.38 p(a,p)(a(a)(x0),p(b,p)(b(b)(x1),p(a,b)(a(p)(x2),x3))) -> 1174.19/295.38 p(p,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,b)(b(b)(x1),x3))) 1174.19/295.38 p(a,p)(a(a)(x0),p(b,p)(b(b)(x1),p(a,p)(a(a)(x2),x3))) -> 1174.19/295.38 p(a,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,p)(b(b)(x1),x3))) 1174.19/295.38 p(a,p)(a(a)(x0),p(b,p)(b(b)(x1),p(a,a)(a(a)(x2),x3))) -> 1174.19/295.38 p(a,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,a)(b(b)(x1),x3))) 1174.19/295.38 p(a,p)(a(a)(x0),p(b,p)(b(b)(x1),p(a,b)(a(a)(x2),x3))) -> 1174.19/295.38 p(a,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,b)(b(b)(x1),x3))) 1174.19/295.38 p(a,p)(a(a)(x0),p(b,p)(b(b)(x1),p(a,p)(a(b)(x2),x3))) -> 1174.19/295.38 p(b,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,p)(b(b)(x1),x3))) 1174.19/295.38 p(a,p)(a(a)(x0),p(b,p)(b(b)(x1),p(a,a)(a(b)(x2),x3))) -> 1174.19/295.38 p(b,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,a)(b(b)(x1),x3))) 1174.19/295.38 p(a,p)(a(a)(x0),p(b,p)(b(b)(x1),p(a,b)(a(b)(x2),x3))) -> 1174.19/295.38 p(b,p)(x2,p(a,p)(a(a)(a(a)(x0)),p(b,b)(b(b)(x1),x3))) 1174.19/295.38 p(a,p)(a(b)(x0),p(b,p)(b(p)(x1),p(a,p)(a(p)(x2),x3))) -> 1174.19/295.38 p(p,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,p)(b(p)(x1),x3))) 1174.19/295.38 p(a,p)(a(b)(x0),p(b,p)(b(p)(x1),p(a,a)(a(p)(x2),x3))) -> 1174.19/295.38 p(p,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,a)(b(p)(x1),x3))) 1174.19/295.38 p(a,p)(a(b)(x0),p(b,p)(b(p)(x1),p(a,b)(a(p)(x2),x3))) -> 1174.19/295.38 p(p,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,b)(b(p)(x1),x3))) 1174.19/295.38 p(a,p)(a(b)(x0),p(b,p)(b(p)(x1),p(a,p)(a(a)(x2),x3))) -> 1174.19/295.38 p(a,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,p)(b(p)(x1),x3))) 1174.19/295.38 p(a,p)(a(b)(x0),p(b,p)(b(p)(x1),p(a,a)(a(a)(x2),x3))) -> 1174.19/295.38 p(a,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,a)(b(p)(x1),x3))) 1174.19/295.38 p(a,p)(a(b)(x0),p(b,p)(b(p)(x1),p(a,b)(a(a)(x2),x3))) -> 1174.19/295.38 p(a,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,b)(b(p)(x1),x3))) 1174.19/295.38 p(a,p)(a(b)(x0),p(b,p)(b(p)(x1),p(a,p)(a(b)(x2),x3))) -> 1174.19/295.38 p(b,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,p)(b(p)(x1),x3))) 1174.19/295.38 p(a,p)(a(b)(x0),p(b,p)(b(p)(x1),p(a,a)(a(b)(x2),x3))) -> 1174.19/295.38 p(b,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,a)(b(p)(x1),x3))) 1174.19/295.38 p(a,p)(a(b)(x0),p(b,p)(b(p)(x1),p(a,b)(a(b)(x2),x3))) -> 1174.19/295.38 p(b,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,b)(b(p)(x1),x3))) 1174.19/295.38 p(a,p)(a(b)(x0),p(b,p)(b(a)(x1),p(a,p)(a(p)(x2),x3))) -> 1174.19/295.38 p(p,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,p)(b(a)(x1),x3))) 1174.19/295.39 p(a,p)(a(b)(x0),p(b,p)(b(a)(x1),p(a,a)(a(p)(x2),x3))) -> 1174.19/295.39 p(p,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,a)(b(a)(x1),x3))) 1174.19/295.39 p(a,p)(a(b)(x0),p(b,p)(b(a)(x1),p(a,b)(a(p)(x2),x3))) -> 1174.19/295.39 p(p,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,b)(b(a)(x1),x3))) 1174.19/295.39 p(a,p)(a(b)(x0),p(b,p)(b(a)(x1),p(a,p)(a(a)(x2),x3))) -> 1174.19/295.39 p(a,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,p)(b(a)(x1),x3))) 1174.19/295.39 p(a,p)(a(b)(x0),p(b,p)(b(a)(x1),p(a,a)(a(a)(x2),x3))) -> 1174.19/295.39 p(a,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,a)(b(a)(x1),x3))) 1174.19/295.39 p(a,p)(a(b)(x0),p(b,p)(b(a)(x1),p(a,b)(a(a)(x2),x3))) -> 1174.19/295.39 p(a,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,b)(b(a)(x1),x3))) 1174.19/295.39 p(a,p)(a(b)(x0),p(b,p)(b(a)(x1),p(a,p)(a(b)(x2),x3))) -> 1174.19/295.39 p(b,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,p)(b(a)(x1),x3))) 1174.19/295.39 p(a,p)(a(b)(x0),p(b,p)(b(a)(x1),p(a,a)(a(b)(x2),x3))) -> 1174.19/295.39 p(b,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,a)(b(a)(x1),x3))) 1174.19/295.39 p(a,p)(a(b)(x0),p(b,p)(b(a)(x1),p(a,b)(a(b)(x2),x3))) -> 1174.19/295.39 p(b,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,b)(b(a)(x1),x3))) 1174.19/295.39 p(a,p)(a(b)(x0),p(b,p)(b(b)(x1),p(a,p)(a(p)(x2),x3))) -> 1174.19/295.39 p(p,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,p)(b(b)(x1),x3))) 1174.19/295.39 p(a,p)(a(b)(x0),p(b,p)(b(b)(x1),p(a,a)(a(p)(x2),x3))) -> 1174.19/295.39 p(p,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,a)(b(b)(x1),x3))) 1174.19/295.39 p(a,p)(a(b)(x0),p(b,p)(b(b)(x1),p(a,b)(a(p)(x2),x3))) -> 1174.19/295.39 p(p,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,b)(b(b)(x1),x3))) 1174.19/295.39 p(a,p)(a(b)(x0),p(b,p)(b(b)(x1),p(a,p)(a(a)(x2),x3))) -> 1174.19/295.39 p(a,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,p)(b(b)(x1),x3))) 1174.19/295.39 p(a,p)(a(b)(x0),p(b,p)(b(b)(x1),p(a,a)(a(a)(x2),x3))) -> 1174.19/295.39 p(a,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,a)(b(b)(x1),x3))) 1174.19/295.39 p(a,p)(a(b)(x0),p(b,p)(b(b)(x1),p(a,b)(a(a)(x2),x3))) -> 1174.19/295.39 p(a,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,b)(b(b)(x1),x3))) 1174.19/295.39 p(a,p)(a(b)(x0),p(b,p)(b(b)(x1),p(a,p)(a(b)(x2),x3))) -> 1174.19/295.39 p(b,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,p)(b(b)(x1),x3))) 1174.19/295.39 p(a,p)(a(b)(x0),p(b,p)(b(b)(x1),p(a,a)(a(b)(x2),x3))) -> 1174.19/295.39 p(b,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,a)(b(b)(x1),x3))) 1174.19/295.39 p(a,p)(a(b)(x0),p(b,p)(b(b)(x1),p(a,b)(a(b)(x2),x3))) -> 1174.19/295.39 p(b,p)(x2,p(a,p)(a(a)(a(b)(x0)),p(b,b)(b(b)(x1),x3))) 1174.19/295.39 Qed 1174.19/295.39 EOF