0.51/0.53	MAYBE
0.51/0.53	(ignored inputs)COMMENT doi:10.1007/978-3-319-13770-4_3 [151] Example 1 submitted by: Raul Gutierrez and Salvador Lucas
0.51/0.53	Conditional Rewrite Rules:
0.51/0.53	   [ or(0,?x) -> ?x,
0.51/0.53	     or(?x,0) -> ?x,
0.51/0.53	     or(1,?x) -> 1,
0.51/0.53	     or(?x,1) -> 1,
0.51/0.53	     or(?x,not(?x)) -> 1,
0.51/0.53	     or(not(?x),?x) -> 1,
0.51/0.53	     and(0,?x) -> 0,
0.51/0.53	     and(?x,0) -> 0,
0.51/0.53	     and(1,?x) -> ?x,
0.51/0.53	     and(?x,1) -> ?x,
0.51/0.53	     and(?x,not(?x)) -> 0,
0.51/0.53	     and(not(?x),?x) -> 0,
0.51/0.53	     not(1) -> 0,
0.51/0.53	     not(0) -> 1,
0.51/0.53	     implies(?x,?y) -> 1 | not(?x) == 1,
0.51/0.53	     implies(?x,?y) -> 1 | ?y == 1,
0.51/0.53	     implies(?x,?y) -> 0 | ?x == 1,?y == 0,
0.51/0.53	     f(?x) -> f(0) | implies(?x,0) == ?y,implies(?x,?y) == ?z,implies(?z,0) == 1 ]
0.51/0.53	Check whether all rules are type 3
0.51/0.53	OK
0.51/0.53	Check whether the input is deterministic
0.51/0.53	OK
0.51/0.53	Result of unraveling:
0.51/0.53	   [ or(0,?x) -> ?x,
0.51/0.53	     or(?x,0) -> ?x,
0.51/0.53	     or(1,?x) -> 1,
0.51/0.53	     or(?x,1) -> 1,
0.51/0.53	     or(?x,not(?x)) -> 1,
0.51/0.53	     or(not(?x),?x) -> 1,
0.51/0.53	     and(0,?x) -> 0,
0.51/0.53	     and(?x,0) -> 0,
0.51/0.53	     and(1,?x) -> ?x,
0.51/0.53	     and(?x,1) -> ?x,
0.51/0.53	     and(?x,not(?x)) -> 0,
0.51/0.53	     and(not(?x),?x) -> 0,
0.51/0.53	     not(1) -> 0,
0.51/0.53	     not(0) -> 1,
0.51/0.53	     implies(?x,?y) -> U2(not(?x),?x,?y),
0.51/0.53	     U2(1,?x,?y) -> 1,
0.51/0.53	     implies(?x,?y) -> U2(?y,?x,?y),
0.51/0.53	     implies(?x,?y) -> U2(?x,?x,?y),
0.51/0.53	     U2(1,?x,?y) -> U3(?y,?x,?y),
0.51/0.53	     U3(0,?x,?y) -> 0,
0.51/0.53	     f(?x) -> U4(implies(?x,0),?x),
0.51/0.53	     U4(?y,?x) -> U5(implies(?x,?y),?x,?y),
0.51/0.53	     U5(?z,?x,?y) -> U6(implies(?z,0),?x,?y,?z),
0.51/0.53	     U6(1,?x,?y,?z) -> f(0) ]
0.51/0.53	Check whether U(R) is terminating
0.51/0.53	failed to show termination
0.51/0.53	Check whether the input is weakly left-linear
0.51/0.53	OK
0.51/0.53	Conditional critical pairs (CCPs):
0.51/0.53	   [ 0 = 0,
0.51/0.53	     1 = 1,
0.51/0.53	     1 = not(0),
0.51/0.53	     0 = 0,
0.51/0.53	     1 = 1,
0.51/0.53	     1 = not(0),
0.51/0.53	     1 = 1,
0.51/0.53	     1 = 1,
0.51/0.53	     1 = 1,
0.51/0.53	     1 = 1,
0.51/0.53	     1 = 1,
0.51/0.53	     1 = 1,
0.51/0.53	     not(0) = 1,
0.51/0.53	     1 = 1,
0.51/0.53	     or(1,0) = 1,
0.51/0.53	     or(0,1) = 1,
0.51/0.53	     not(0) = 1,
0.51/0.53	     1 = 1,
0.51/0.53	     or(0,1) = 1,
0.51/0.53	     or(1,0) = 1,
0.51/0.53	     0 = 0,
0.51/0.53	     0 = 0,
0.51/0.53	     0 = 0,
0.51/0.53	     0 = 0,
0.51/0.53	     0 = 0,
0.51/0.53	     0 = 0,
0.51/0.53	     0 = 0,
0.51/0.53	     1 = 1,
0.51/0.53	     0 = not(1),
0.51/0.53	     0 = 0,
0.51/0.53	     1 = 1,
0.51/0.53	     0 = not(1),
0.51/0.53	     0 = 0,
0.51/0.53	     not(1) = 0,
0.51/0.54	     and(1,0) = 0,
0.51/0.54	     and(0,1) = 0,
0.51/0.54	     0 = 0,
0.51/0.54	     not(1) = 0,
0.51/0.54	     and(0,1) = 0,
0.51/0.54	     and(1,0) = 0,
0.51/0.54	     1 = 1 | ?y_13 == 1,not(?x_13) == 1,
0.51/0.54	     0 = 1 | ?x_14 == 1,?y_14 == 0,not(?x_14) == 1,
0.51/0.54	     1 = 1 | not(?x_12) == 1,?y_12 == 1,
0.51/0.54	     0 = 1 | ?x_14 == 1,?y_14 == 0,?y_14 == 1,
0.51/0.54	     1 = 0 | not(?x_12) == 1,?x_12 == 1,?y_12 == 0,
0.51/0.54	     1 = 0 | ?y_13 == 1,?x_13 == 1,?y_13 == 0 ]
0.51/0.54	Check whether the input is almost orthogonale
0.51/0.54	not almost orthogonal
0.51/0.54	OK
0.51/0.54	Check U(R) is confluent
0.51/0.54	Rewrite Rules:
0.51/0.54	   [ or(0,?x) -> ?x,
0.51/0.54	     or(?x,0) -> ?x,
0.51/0.54	     or(1,?x) -> 1,
0.51/0.54	     or(?x,1) -> 1,
0.51/0.54	     or(?x,not(?x)) -> 1,
0.51/0.54	     or(not(?x),?x) -> 1,
0.51/0.54	     and(0,?x) -> 0,
0.51/0.54	     and(?x,0) -> 0,
0.51/0.54	     and(1,?x) -> ?x,
0.51/0.54	     and(?x,1) -> ?x,
0.51/0.54	     and(?x,not(?x)) -> 0,
0.51/0.54	     and(not(?x),?x) -> 0,
0.51/0.54	     not(1) -> 0,
0.51/0.54	     not(0) -> 1,
0.51/0.54	     implies(?x,?y) -> U2(not(?x),?x,?y),
0.51/0.54	     U2(1,?x,?y) -> 1,
0.51/0.54	     implies(?x,?y) -> U2(?y,?x,?y),
0.51/0.54	     implies(?x,?y) -> U2(?x,?x,?y),
0.51/0.54	     U2(1,?x,?y) -> U3(?y,?x,?y),
0.51/0.54	     U3(0,?x,?y) -> 0,
0.51/0.54	     f(?x) -> U4(implies(?x,0),?x),
0.51/0.54	     U4(?y,?x) -> U5(implies(?x,?y),?x,?y),
0.51/0.54	     U5(?z,?x,?y) -> U6(implies(?z,0),?x,?y,?z),
0.51/0.54	     U6(1,?x,?y,?z) -> f(0) ]
0.51/0.54	Apply Direct Methods...
0.51/0.54	Inner CPs:
0.51/0.54	   [ or(1,0) = 1,
0.51/0.54	     or(0,1) = 1,
0.51/0.54	     or(0,1) = 1,
0.51/0.54	     or(1,0) = 1,
0.51/0.54	     and(1,0) = 0,
0.51/0.54	     and(0,1) = 0,
0.51/0.54	     and(0,1) = 0,
0.51/0.54	     and(1,0) = 0 ]
0.51/0.54	Outer CPs:
0.51/0.54	   [ 0 = 0,
0.51/0.54	     1 = 1,
0.51/0.54	     not(0) = 1,
0.51/0.54	     1 = 1,
0.51/0.54	     not(0) = 1,
0.51/0.54	     1 = 1,
0.51/0.54	     1 = 1,
0.51/0.54	     1 = 1,
0.51/0.54	     0 = 0,
0.51/0.54	     0 = 0,
0.51/0.54	     0 = 0,
0.51/0.54	     0 = 0,
0.51/0.54	     0 = 0,
0.51/0.54	     1 = 1,
0.51/0.54	     not(1) = 0,
0.51/0.54	     not(1) = 0,
0.51/0.54	     U2(not(?x_12),?x_12,?y_12) = U2(?y_12,?x_12,?y_12),
0.51/0.54	     U2(not(?x_12),?x_12,?y_12) = U2(?x_12,?x_12,?y_12),
0.51/0.54	     1 = U3(?y_13,?x_13,?y_13),
0.51/0.54	     U2(?y_14,?x_14,?y_14) = U2(?x_14,?x_14,?y_14) ]
0.51/0.54	not Overlay, check Termination...
0.51/0.54	unknown/not Terminating
0.51/0.54	unknown Knuth & Bendix
0.51/0.54	not Left-Linear, not Right-Linear
0.51/0.54	unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
0.51/0.54	unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
0.51/0.54	unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
0.51/0.54	   [ or(0,?x) -> ?x,
0.51/0.54	     or(?x_1,0) -> ?x_1,
0.51/0.54	     or(1,?x_2) -> 1,
0.51/0.54	     or(?x_3,1) -> 1,
0.51/0.54	     or(?x_4,not(?x_4)) -> 1,
0.51/0.54	     or(not(?x_5),?x_5) -> 1,
0.51/0.54	     and(0,?x_6) -> 0,
0.51/0.54	     and(?x_7,0) -> 0,
0.51/0.54	     and(1,?x_8) -> ?x_8,
0.51/0.54	     and(?x_9,1) -> ?x_9,
0.51/0.54	     and(?x_10,not(?x_10)) -> 0,
0.51/0.54	     and(not(?x_11),?x_11) -> 0,
0.51/0.54	     not(1) -> 0,
0.51/0.54	     not(0) -> 1,
0.51/0.54	     implies(?x_12,?y_12) -> U2(not(?x_12),?x_12,?y_12),
0.51/0.54	     U2(1,?x_13,?y_13) -> 1,
0.51/0.54	     implies(?x_14,?y_14) -> U2(?y_14,?x_14,?y_14),
0.51/0.54	     implies(?x_15,?y_15) -> U2(?x_15,?x_15,?y_15),
0.51/0.54	     U2(1,?x_16,?y_16) -> U3(?y_16,?x_16,?y_16),
0.51/0.54	     U3(0,?x_17,?y_17) -> 0,
0.51/0.54	     f(?x_18) -> U4(implies(?x_18,0),?x_18),
0.51/0.54	     U4(?y_19,?x_19) -> U5(implies(?x_19,?y_19),?x_19,?y_19),
0.51/0.54	     U5(?z_20,?x_20,?y_20) -> U6(implies(?z_20,0),?x_20,?y_20,?z_20),
0.51/0.54	     U6(1,?x_21,?y_21,?z_21) -> f(0) ]
0.51/0.54	Sort Assignment:
0.51/0.54	 0 : =>56
0.51/0.54	 1 : =>56
0.51/0.54	 f : 56=>69
0.51/0.54	 U2 : 56*56*56=>56
0.51/0.54	 U3 : 56*56*56=>56
0.51/0.54	 U4 : 56*56=>69
0.51/0.54	 U5 : 56*56*56=>69
0.51/0.54	 U6 : 56*56*56*56=>69
0.51/0.54	 or : 56*56=>56
0.51/0.54	 and : 56*56=>56
0.51/0.54	 not : 56=>56
0.51/0.54	 implies : 56*56=>56
0.51/0.54	non-linear variables: {?x_4,?x_5,?x_10,?x_11}
0.51/0.54	non-linear types: {56}
0.51/0.54	types leq non-linear types: {56}
0.51/0.54	rules applicable to terms of non-linear types:
0.51/0.54	   [ or(0,?x) -> ?x,
0.51/0.54	     or(?x_1,0) -> ?x_1,
0.51/0.54	     or(1,?x_2) -> 1,
0.51/0.54	     or(?x_3,1) -> 1,
0.51/0.54	     or(?x_4,not(?x_4)) -> 1,
0.51/0.54	     or(not(?x_5),?x_5) -> 1,
0.51/0.54	     and(0,?x_6) -> 0,
0.51/0.54	     and(?x_7,0) -> 0,
0.51/0.54	     and(1,?x_8) -> ?x_8,
0.51/0.54	     and(?x_9,1) -> ?x_9,
0.51/0.54	     and(?x_10,not(?x_10)) -> 0,
0.51/0.54	     and(not(?x_11),?x_11) -> 0,
0.51/0.54	     not(1) -> 0,
0.51/0.54	     not(0) -> 1,
0.51/0.54	     implies(?x_12,?y_12) -> U2(not(?x_12),?x_12,?y_12),
0.51/0.54	     U2(1,?x_13,?y_13) -> 1,
0.51/0.54	     implies(?x_14,?y_14) -> U2(?y_14,?x_14,?y_14),
0.51/0.54	     implies(?x_15,?y_15) -> U2(?x_15,?x_15,?y_15),
0.51/0.54	     U2(1,?x_16,?y_16) -> U3(?y_16,?x_16,?y_16),
0.51/0.54	     U3(0,?x_17,?y_17) -> 0 ]
0.51/0.54	terms of non-linear types are innermost terminating
0.51/0.54	inner CP <p,q> = <or(1,0), 1>
0.51/0.54	parallel reducts of p: {or(1,0),1,1}
0.51/0.54	is {?x_1:=1} ground inst. preserving? (yes)
0.51/0.54	inner CP <p,q> = <or(0,1), 1>
0.51/0.54	parallel reducts of p: {or(0,1),1,1}
0.51/0.54	is {?x:=1} ground inst. preserving? (yes)
0.51/0.54	inner CP <p,q> = <or(0,1), 1>
0.51/0.54	parallel reducts of p: {or(0,1),1,1}
0.51/0.54	is {?x:=1} ground inst. preserving? (yes)
0.51/0.54	inner CP <p,q> = <or(1,0), 1>
0.51/0.54	parallel reducts of p: {or(1,0),1,1}
0.51/0.54	is {?x_1:=1} ground inst. preserving? (yes)
0.51/0.54	inner CP <p,q> = <and(1,0), 0>
0.51/0.54	parallel reducts of p: {and(1,0),0,0}
0.51/0.54	is {?x_7:=1} ground inst. preserving? (yes)
0.51/0.54	inner CP <p,q> = <and(0,1), 0>
0.51/0.54	parallel reducts of p: {and(0,1),0,0}
0.51/0.54	is {?x_6:=1} ground inst. preserving? (yes)
0.51/0.54	inner CP <p,q> = <and(0,1), 0>
0.51/0.54	parallel reducts of p: {and(0,1),0,0}
0.51/0.54	is {?x_6:=1} ground inst. preserving? (yes)
0.51/0.54	inner CP <p,q> = <and(1,0), 0>
0.51/0.54	parallel reducts of p: {and(1,0),0,0}
0.51/0.54	is {?x_7:=1} ground inst. preserving? (yes)
0.51/0.54	outer CP <p,q> = <0, 0>
0.51/0.54	parallel reducts of p: {0}
0.51/0.54	parallel reducts of q: {0}
0.51/0.54	join at 0
0.51/0.54	check subst from p
0.51/0.54	check subst from q
0.51/0.54	outer CP <p,q> = <1, 1>
0.51/0.54	parallel reducts of p: {1}
0.51/0.54	parallel reducts of q: {1}
0.51/0.54	join at 1
0.51/0.54	check subst from p
0.51/0.54	check subst from q
0.51/0.54	outer CP <p,q> = <not(0), 1>
0.51/0.54	parallel reducts of p: {not(0),1}
0.51/0.54	parallel reducts of q: {1}
0.51/0.54	join at 1
0.51/0.54	check subst from p
0.51/0.54	is {} ground inst. preserving? (yes)
0.51/0.54	check subst from q
0.51/0.54	outer CP <p,q> = <1, 1>
0.51/0.54	parallel reducts of p: {1}
0.51/0.54	parallel reducts of q: {1}
0.51/0.54	join at 1
0.51/0.54	check subst from p
0.51/0.54	check subst from q
0.51/0.54	outer CP <p,q> = <not(0), 1>
0.51/0.54	parallel reducts of p: {not(0),1}
0.51/0.54	parallel reducts of q: {1}
0.51/0.54	join at 1
0.51/0.54	check subst from p
0.51/0.54	is {} ground inst. preserving? (yes)
0.51/0.54	check subst from q
0.51/0.54	outer CP <p,q> = <1, 1>
0.51/0.54	parallel reducts of p: {1}
0.51/0.54	parallel reducts of q: {1}
0.51/0.54	join at 1
0.51/0.54	check subst from p
0.51/0.54	check subst from q
0.51/0.54	outer CP <p,q> = <1, 1>
0.51/0.54	parallel reducts of p: {1}
0.51/0.54	parallel reducts of q: {1}
0.51/0.54	join at 1
0.51/0.54	check subst from p
0.51/0.54	check subst from q
0.51/0.54	outer CP <p,q> = <1, 1>
0.51/0.54	parallel reducts of p: {1}
0.51/0.54	parallel reducts of q: {1}
0.51/0.54	join at 1
0.51/0.54	check subst from p
0.51/0.54	check subst from q
0.51/0.54	outer CP <p,q> = <0, 0>
0.51/0.54	parallel reducts of p: {0}
0.51/0.54	parallel reducts of q: {0}
0.51/0.54	join at 0
0.51/0.54	check subst from p
0.51/0.54	check subst from q
0.51/0.54	outer CP <p,q> = <0, 0>
0.51/0.54	parallel reducts of p: {0}
0.51/0.54	parallel reducts of q: {0}
0.51/0.54	join at 0
0.51/0.54	check subst from p
0.51/0.54	check subst from q
0.51/0.54	outer CP <p,q> = <0, 0>
0.51/0.54	parallel reducts of p: {0}
0.51/0.54	parallel reducts of q: {0}
0.51/0.54	join at 0
0.51/0.54	check subst from p
0.51/0.54	check subst from q
0.51/0.54	outer CP <p,q> = <0, 0>
0.51/0.54	parallel reducts of p: {0}
0.51/0.54	parallel reducts of q: {0}
0.51/0.54	join at 0
0.51/0.54	check subst from p
0.51/0.54	check subst from q
0.51/0.54	outer CP <p,q> = <0, 0>
0.51/0.54	parallel reducts of p: {0}
0.51/0.54	parallel reducts of q: {0}
0.51/0.54	join at 0
0.51/0.54	check subst from p
0.51/0.54	check subst from q
0.51/0.54	outer CP <p,q> = <1, 1>
0.51/0.54	parallel reducts of p: {1}
0.51/0.54	parallel reducts of q: {1}
0.51/0.54	join at 1
0.51/0.54	check subst from p
0.51/0.54	check subst from q
0.51/0.54	outer CP <p,q> = <not(1), 0>
0.51/0.54	parallel reducts of p: {not(1),0}
0.51/0.54	parallel reducts of q: {0}
0.51/0.54	join at 0
0.51/0.54	check subst from p
0.51/0.54	is {} ground inst. preserving? (yes)
0.51/0.54	check subst from q
0.51/0.54	outer CP <p,q> = <not(1), 0>
0.51/0.54	parallel reducts of p: {not(1),0}
0.51/0.54	parallel reducts of q: {0}
0.51/0.54	join at 0
0.51/0.54	check subst from p
0.51/0.54	is {} ground inst. preserving? (yes)
0.51/0.54	check subst from q
0.51/0.54	outer CP <p,q> = <U2(not(?x_12:56),?x_12:56,?y_12:56), U2(?y_12:56,?x_12:56,?y_12:56)>
0.51/0.54	parallel reducts of p: {U2(not(?x_12:56),?x_12:56,?y_12:56)}
0.51/0.54	parallel reducts of q: {U2(?y_12:56,?x_12:56,?y_12:56)}
0.51/0.54	unknown Quasi-Left-Linear & Parallel-Closed
0.51/0.54	   [ or(0,?x) -> ?x,
0.51/0.54	     or(?x_1,0) -> ?x_1,
0.51/0.54	     or(1,?x_2) -> 1,
0.51/0.54	     or(?x_3,1) -> 1,
0.51/0.54	     or(?x_4,not(?x_4)) -> 1,
0.51/0.54	     or(not(?x_5),?x_5) -> 1,
0.51/0.54	     and(0,?x_6) -> 0,
0.51/0.54	     and(?x_7,0) -> 0,
0.51/0.54	     and(1,?x_8) -> ?x_8,
0.51/0.54	     and(?x_9,1) -> ?x_9,
0.51/0.54	     and(?x_10,not(?x_10)) -> 0,
0.51/0.54	     and(not(?x_11),?x_11) -> 0,
0.51/0.54	     not(1) -> 0,
0.51/0.54	     not(0) -> 1,
0.51/0.54	     implies(?x_12,?y_12) -> U2(not(?x_12),?x_12,?y_12),
0.51/0.54	     U2(1,?x_13,?y_13) -> 1,
0.51/0.54	     implies(?x_14,?y_14) -> U2(?y_14,?x_14,?y_14),
0.51/0.54	     implies(?x_15,?y_15) -> U2(?x_15,?x_15,?y_15),
0.51/0.54	     U2(1,?x_16,?y_16) -> U3(?y_16,?x_16,?y_16),
0.51/0.54	     U3(0,?x_17,?y_17) -> 0,
0.51/0.54	     f(?x_18) -> U4(implies(?x_18,0),?x_18),
0.51/0.54	     U4(?y_19,?x_19) -> U5(implies(?x_19,?y_19),?x_19,?y_19),
0.51/0.54	     U5(?z_20,?x_20,?y_20) -> U6(implies(?z_20,0),?x_20,?y_20,?z_20),
0.51/0.54	     U6(1,?x_21,?y_21,?z_21) -> f(0) ]
0.51/0.54	Sort Assignment:
0.51/0.54	 0 : =>56
0.51/0.54	 1 : =>56
0.51/0.54	 f : 56=>69
0.51/0.54	 U2 : 56*56*56=>56
0.51/0.54	 U3 : 56*56*56=>56
0.51/0.54	 U4 : 56*56=>69
0.51/0.54	 U5 : 56*56*56=>69
0.51/0.54	 U6 : 56*56*56*56=>69
0.51/0.54	 or : 56*56=>56
0.51/0.54	 and : 56*56=>56
0.51/0.54	 not : 56=>56
0.51/0.54	 implies : 56*56=>56
0.51/0.54	non-linear variables: {?x_4,?x_5,?x_10,?x_11,?x_12,?y_14,?x_15,?y_16,?x_18,?x_19,?y_19,?z_20}
0.51/0.54	non-linear types: {56}
0.51/0.54	types leq non-linear types: {56}
0.51/0.54	rules applicable to terms of non-linear types:
0.51/0.54	   [ or(0,?x) -> ?x,
0.51/0.54	     or(?x_1,0) -> ?x_1,
0.51/0.54	     or(1,?x_2) -> 1,
0.51/0.54	     or(?x_3,1) -> 1,
0.51/0.54	     or(?x_4,not(?x_4)) -> 1,
0.51/0.54	     or(not(?x_5),?x_5) -> 1,
0.51/0.54	     and(0,?x_6) -> 0,
0.51/0.54	     and(?x_7,0) -> 0,
0.51/0.54	     and(1,?x_8) -> ?x_8,
0.51/0.54	     and(?x_9,1) -> ?x_9,
0.51/0.54	     and(?x_10,not(?x_10)) -> 0,
0.51/0.54	     and(not(?x_11),?x_11) -> 0,
0.51/0.54	     not(1) -> 0,
0.51/0.54	     not(0) -> 1,
0.51/0.54	     implies(?x_12,?y_12) -> U2(not(?x_12),?x_12,?y_12),
0.51/0.54	     U2(1,?x_13,?y_13) -> 1,
0.51/0.54	     implies(?x_14,?y_14) -> U2(?y_14,?x_14,?y_14),
0.51/0.54	     implies(?x_15,?y_15) -> U2(?x_15,?x_15,?y_15),
0.51/0.54	     U2(1,?x_16,?y_16) -> U3(?y_16,?x_16,?y_16),
0.51/0.54	     U3(0,?x_17,?y_17) -> 0 ]
0.51/0.54	Rnl:
0.51/0.54	0: {}
0.51/0.54	1: {}
0.51/0.54	2: {}
0.51/0.54	3: {}
0.51/0.54	4: {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19}
0.51/0.54	5: {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19}
0.51/0.54	6: {}
0.51/0.54	7: {}
0.51/0.54	8: {}
0.51/0.54	9: {}
0.51/0.54	10: {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19}
0.51/0.54	11: {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19}
0.51/0.54	12: {}
0.51/0.54	13: {}
0.51/0.54	14: {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19}
0.51/0.54	15: {}
0.51/0.54	16: {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19}
0.51/0.54	17: {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19}
0.51/0.54	18: {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19}
0.51/0.54	19: {}
0.51/0.54	20: {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19}
0.51/0.54	21: {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19}
0.51/0.54	22: {0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19}
0.51/0.54	23: {}
0.51/0.54	terms of non-linear types are innermost terminating
0.51/0.54	Critical Pair <or(1,0), 1> by Rules <12, 4>
0.51/0.54	 convertible by a reduction of rules [->(1)]
0.51/0.54	 convertible by a reduction of rules [->(2)]
0.51/0.54	 convertible by a reduction of rules [(13)<-,->(5)]
0.51/0.54	Critical Pair <or(0,1), 1> by Rules <13, 4>
0.51/0.54	 convertible by a reduction of rules [->(0)]
0.51/0.54	 convertible by a reduction of rules [->(3)]
0.51/0.54	 convertible by a reduction of rules [(12)<-,->(5)]
0.51/0.54	Critical Pair <or(0,1), 1> by Rules <12, 5>
0.51/0.54	 convertible by a reduction of rules [->(0)]
0.51/0.54	 convertible by a reduction of rules [->(3)]
0.51/0.54	 convertible by a reduction of rules [(13)<-,->(4)]
0.51/0.54	Critical Pair <or(1,0), 1> by Rules <13, 5>
0.51/0.54	 convertible by a reduction of rules [->(1)]
0.51/0.54	 convertible by a reduction of rules [->(2)]
0.51/0.54	 convertible by a reduction of rules [(12)<-,->(4)]
0.51/0.54	Critical Pair <and(1,0), 0> by Rules <12, 10>
0.51/0.54	 convertible by a reduction of rules [->(7)]
0.51/0.54	 convertible by a reduction of rules [->(8)]
0.51/0.54	 convertible by a reduction of rules [(13)<-,->(11)]
0.51/0.54	Critical Pair <and(0,1), 0> by Rules <13, 10>
0.51/0.54	 convertible by a reduction of rules [->(6)]
0.51/0.54	 convertible by a reduction of rules [->(9)]
0.51/0.54	 convertible by a reduction of rules [(12)<-,->(11)]
0.51/0.54	Critical Pair <and(0,1), 0> by Rules <12, 11>
0.51/0.54	 convertible by a reduction of rules [->(6)]
0.51/0.54	 convertible by a reduction of rules [->(9)]
0.51/0.54	 convertible by a reduction of rules [(13)<-,->(10)]
0.51/0.54	Critical Pair <and(1,0), 0> by Rules <13, 11>
0.51/0.54	 convertible by a reduction of rules [->(7)]
0.51/0.54	 convertible by a reduction of rules [->(8)]
0.51/0.54	 convertible by a reduction of rules [(12)<-,->(10)]
0.51/0.54	Critical Pair <0, 0> by Rules <1, 0>
0.51/0.54	 convertible by a reduction of rules []
0.51/0.54	Critical Pair <1, 1> by Rules <3, 0>
0.51/0.54	 convertible by a reduction of rules []
0.51/0.54	Critical Pair <1, not(0)> by Rules <4, 0>
0.51/0.54	 convertible by a reduction of rules [(13)<-]
0.51/0.54	Critical Pair <1, 1> by Rules <2, 1>
0.51/0.54	 convertible by a reduction of rules []
0.51/0.54	Critical Pair <1, not(0)> by Rules <5, 1>
0.51/0.54	 convertible by a reduction of rules [(13)<-]
0.51/0.54	Critical Pair <1, 1> by Rules <3, 2>
0.51/0.54	 convertible by a reduction of rules []
0.51/0.54	Critical Pair <1, 1> by Rules <4, 2>
0.51/0.54	 convertible by a reduction of rules []
0.51/0.54	Critical Pair <1, 1> by Rules <5, 3>
0.51/0.54	 convertible by a reduction of rules []
0.51/0.54	Critical Pair <0, 0> by Rules <7, 6>
0.51/0.54	 convertible by a reduction of rules []
0.51/0.54	Critical Pair <0, 0> by Rules <9, 6>
0.51/0.54	 convertible by a reduction of rules []
0.51/0.54	Critical Pair <0, 0> by Rules <10, 6>
0.51/0.54	 convertible by a reduction of rules []
0.51/0.54	Critical Pair <0, 0> by Rules <8, 7>
0.51/0.54	 convertible by a reduction of rules []
0.51/0.54	Critical Pair <0, 0> by Rules <11, 7>
0.51/0.54	 convertible by a reduction of rules []
0.51/0.54	Critical Pair <1, 1> by Rules <9, 8>
0.51/0.54	 convertible by a reduction of rules []
0.51/0.54	Critical Pair <0, not(1)> by Rules <10, 8>
0.51/0.54	 convertible by a reduction of rules [(12)<-]
0.51/0.54	Critical Pair <0, not(1)> by Rules <11, 9>
0.51/0.54	 convertible by a reduction of rules [(12)<-]
0.51/0.54	Critical Pair <U2(?y_14,?x_14,?y_14), U2(not(?x_14),?x_14,?y_14)> by Rules <16, 14>
0.51/0.54	no joinable sequence for some critical pairs
0.51/0.54	unknown Quasi-Linear & Linearized-Decreasing
0.51/0.54	   [ or(0,?x) -> ?x,
0.51/0.54	     or(?x_1,0) -> ?x_1,
0.51/0.54	     or(1,?x_2) -> 1,
0.51/0.54	     or(?x_3,1) -> 1,
0.51/0.54	     or(?x_4,not(?x_4)) -> 1,
0.51/0.54	     or(not(?x_5),?x_5) -> 1,
0.51/0.54	     and(0,?x_6) -> 0,
0.51/0.54	     and(?x_7,0) -> 0,
0.51/0.54	     and(1,?x_8) -> ?x_8,
0.51/0.54	     and(?x_9,1) -> ?x_9,
0.51/0.54	     and(?x_10,not(?x_10)) -> 0,
0.51/0.54	     and(not(?x_11),?x_11) -> 0,
0.51/0.54	     not(1) -> 0,
0.51/0.54	     not(0) -> 1,
0.51/0.54	     implies(?x_12,?y_12) -> U2(not(?x_12),?x_12,?y_12),
0.51/0.54	     U2(1,?x_13,?y_13) -> 1,
0.51/0.54	     implies(?x_14,?y_14) -> U2(?y_14,?x_14,?y_14),
0.51/0.54	     implies(?x_15,?y_15) -> U2(?x_15,?x_15,?y_15),
0.51/0.54	     U2(1,?x_16,?y_16) -> U3(?y_16,?x_16,?y_16),
0.51/0.54	     U3(0,?x_17,?y_17) -> 0,
0.51/0.54	     f(?x_18) -> U4(implies(?x_18,0),?x_18),
0.51/0.54	     U4(?y_19,?x_19) -> U5(implies(?x_19,?y_19),?x_19,?y_19),
0.51/0.54	     U5(?z_20,?x_20,?y_20) -> U6(implies(?z_20,0),?x_20,?y_20,?z_20),
0.51/0.54	     U6(1,?x_21,?y_21,?z_21) -> f(0) ]
0.51/0.54	Sort Assignment:
0.51/0.54	 0 : =>56
0.51/0.54	 1 : =>56
0.51/0.54	 f : 56=>69
0.51/0.54	 U2 : 56*56*56=>56
0.51/0.54	 U3 : 56*56*56=>56
0.51/0.54	 U4 : 56*56=>69
0.51/0.54	 U5 : 56*56*56=>69
0.51/0.54	 U6 : 56*56*56*56=>69
0.51/0.54	 or : 56*56=>56
0.51/0.54	 and : 56*56=>56
0.51/0.54	 not : 56=>56
0.51/0.54	 implies : 56*56=>56
0.51/0.54	non-linear variables: {?x_4,?x_5,?x_10,?x_11,?x_12,?y_14,?x_15,?y_16,?x_18,?x_19,?y_19,?z_20}
0.51/0.54	non-linear types: {56}
0.51/0.54	types leq non-linear types: {56}
0.51/0.54	rules applicable to terms of non-linear types:
0.51/0.54	   [ or(0,?x) -> ?x,
0.51/0.54	     or(?x_1,0) -> ?x_1,
0.51/0.54	     or(1,?x_2) -> 1,
0.51/0.54	     or(?x_3,1) -> 1,
0.51/0.54	     or(?x_4,not(?x_4)) -> 1,
0.51/0.54	     or(not(?x_5),?x_5) -> 1,
0.51/0.54	     and(0,?x_6) -> 0,
0.51/0.54	     and(?x_7,0) -> 0,
0.51/0.54	     and(1,?x_8) -> ?x_8,
0.51/0.54	     and(?x_9,1) -> ?x_9,
0.51/0.54	     and(?x_10,not(?x_10)) -> 0,
0.51/0.54	     and(not(?x_11),?x_11) -> 0,
0.51/0.54	     not(1) -> 0,
0.51/0.54	     not(0) -> 1,
0.51/0.54	     implies(?x_12,?y_12) -> U2(not(?x_12),?x_12,?y_12),
0.51/0.54	     U2(1,?x_13,?y_13) -> 1,
0.51/0.54	     implies(?x_14,?y_14) -> U2(?y_14,?x_14,?y_14),
0.51/0.54	     implies(?x_15,?y_15) -> U2(?x_15,?x_15,?y_15),
0.51/0.54	     U2(1,?x_16,?y_16) -> U3(?y_16,?x_16,?y_16),
0.51/0.54	     U3(0,?x_17,?y_17) -> 0 ]
0.51/0.54	terms of non-linear types are terminating
0.51/0.54	Check Joinablility of CP from NLR:
0.51/0.54	Critical Pair <or(1,0), 1> by Rules <12, 4>
0.51/0.54	Critical Pair <or(0,1), 1> by Rules <13, 4>
0.51/0.54	Critical Pair <or(0,1), 1> by Rules <12, 5>
0.51/0.54	Critical Pair <or(1,0), 1> by Rules <13, 5>
0.51/0.54	Critical Pair <and(1,0), 0> by Rules <12, 10>
0.51/0.54	Critical Pair <and(0,1), 0> by Rules <13, 10>
0.51/0.54	Critical Pair <and(0,1), 0> by Rules <12, 11>
0.51/0.54	Critical Pair <and(1,0), 0> by Rules <13, 11>
0.51/0.54	Critical Pair <0, 0> by Rules <1, 0>
0.51/0.54	Critical Pair <1, 1> by Rules <3, 0>
0.51/0.54	Critical Pair <1, not(0)> by Rules <4, 0>
0.51/0.54	Critical Pair <1, 1> by Rules <2, 1>
0.51/0.54	Critical Pair <1, not(0)> by Rules <5, 1>
0.51/0.54	Critical Pair <1, 1> by Rules <3, 2>
0.51/0.54	Critical Pair <1, 1> by Rules <4, 2>
0.51/0.54	Critical Pair <1, 1> by Rules <5, 3>
0.51/0.54	Critical Pair <0, 0> by Rules <7, 6>
0.51/0.54	Critical Pair <0, 0> by Rules <9, 6>
0.51/0.54	Critical Pair <0, 0> by Rules <10, 6>
0.51/0.54	Critical Pair <0, 0> by Rules <8, 7>
0.51/0.54	Critical Pair <0, 0> by Rules <11, 7>
0.51/0.54	Critical Pair <1, 1> by Rules <9, 8>
0.51/0.54	Critical Pair <0, not(1)> by Rules <10, 8>
0.51/0.54	Critical Pair <0, not(1)> by Rules <11, 9>
0.51/0.54	Critical Pair <U2(?y_14,?x_14,?y_14), U2(not(?x_14),?x_14,?y_14)> by Rules <16, 14>
0.51/0.54	Critical Pair <U2(?x_15,?x_15,?y_15), U2(not(?x_15),?x_15,?y_15)> by Rules <17, 14>
0.51/0.54	Critical Pair <U3(?y_16,?x_16,?y_16), 1> by Rules <18, 15>
0.51/0.54	Critical Pair <U2(?x_15,?x_15,?y_15), U2(?y_15,?x_15,?y_15)> by Rules <17, 16>
0.51/0.54	no joinable sequence for some critical pairs
0.51/0.54	unknown Strongly Quasi-Linear & Hierarchically Decreasing
0.51/0.54	check by Reduction-Preserving Completion...
0.51/0.54	failure(empty P)
0.51/0.54	unknown Reduction-Preserving Completion
0.51/0.54	check by Ordered Rewriting...
0.51/0.54	remove redundants rules and split
0.51/0.54	R-part:
0.51/0.54	   [ or(0,?x) -> ?x,
0.51/0.54	     or(?x,0) -> ?x,
0.51/0.54	     or(1,?x) -> 1,
0.51/0.54	     or(?x,1) -> 1,
0.51/0.54	     or(?x,not(?x)) -> 1,
0.51/0.54	     or(not(?x),?x) -> 1,
0.51/0.54	     and(0,?x) -> 0,
0.51/0.54	     and(?x,0) -> 0,
0.51/0.54	     and(1,?x) -> ?x,
0.51/0.54	     and(?x,1) -> ?x,
0.51/0.54	     and(?x,not(?x)) -> 0,
0.51/0.54	     and(not(?x),?x) -> 0,
0.51/0.54	     not(1) -> 0,
0.51/0.54	     not(0) -> 1,
0.51/0.54	     implies(?x,?y) -> U2(not(?x),?x,?y),
0.51/0.54	     U2(1,?x,?y) -> 1,
0.51/0.54	     implies(?x,?y) -> U2(?y,?x,?y),
0.51/0.54	     implies(?x,?y) -> U2(?x,?x,?y),
0.51/0.54	     U2(1,?x,?y) -> U3(?y,?x,?y),
0.51/0.54	     U3(0,?x,?y) -> 0,
0.51/0.54	     f(?x) -> U4(implies(?x,0),?x),
0.51/0.54	     U4(?y,?x) -> U5(implies(?x,?y),?x,?y),
0.51/0.54	     U5(?z,?x,?y) -> U6(implies(?z,0),?x,?y,?z),
0.51/0.54	     U6(1,?x,?y,?z) -> f(0) ]
0.51/0.54	E-part:
0.51/0.54	   [ ]
0.51/0.54	...failed to find a suitable LPO.
0.51/0.54	unknown Confluence by Ordered Rewriting
0.51/0.54	Direct Methods: Can't judge
0.51/0.54	
0.51/0.54	Try Persistent Decomposition for...
0.51/0.54	   [ or(0,?x) -> ?x,
0.51/0.54	     or(?x,0) -> ?x,
0.51/0.54	     or(1,?x) -> 1,
0.51/0.54	     or(?x,1) -> 1,
0.51/0.54	     or(?x,not(?x)) -> 1,
0.51/0.54	     or(not(?x),?x) -> 1,
0.51/0.54	     and(0,?x) -> 0,
0.51/0.54	     and(?x,0) -> 0,
0.51/0.54	     and(1,?x) -> ?x,
0.51/0.54	     and(?x,1) -> ?x,
0.51/0.54	     and(?x,not(?x)) -> 0,
0.51/0.54	     and(not(?x),?x) -> 0,
0.51/0.54	     not(1) -> 0,
0.51/0.54	     not(0) -> 1,
0.51/0.54	     implies(?x,?y) -> U2(not(?x),?x,?y),
0.51/0.54	     U2(1,?x,?y) -> 1,
0.51/0.54	     implies(?x,?y) -> U2(?y,?x,?y),
0.51/0.54	     implies(?x,?y) -> U2(?x,?x,?y),
0.51/0.54	     U2(1,?x,?y) -> U3(?y,?x,?y),
0.51/0.54	     U3(0,?x,?y) -> 0,
0.51/0.54	     f(?x) -> U4(implies(?x,0),?x),
0.51/0.54	     U4(?y,?x) -> U5(implies(?x,?y),?x,?y),
0.51/0.54	     U5(?z,?x,?y) -> U6(implies(?z,0),?x,?y,?z),
0.51/0.54	     U6(1,?x,?y,?z) -> f(0) ]
0.51/0.54	Sort Assignment:
0.51/0.54	 0 : =>56
0.51/0.54	 1 : =>56
0.51/0.54	 f : 56=>69
0.51/0.54	 U2 : 56*56*56=>56
0.51/0.54	 U3 : 56*56*56=>56
0.51/0.54	 U4 : 56*56=>69
0.51/0.54	 U5 : 56*56*56=>69
0.51/0.54	 U6 : 56*56*56*56=>69
0.51/0.54	 or : 56*56=>56
0.51/0.54	 and : 56*56=>56
0.51/0.54	 not : 56=>56
0.51/0.54	 implies : 56*56=>56
0.51/0.54	maximal types: {56,69}
0.51/0.54	Persistent Decomposition failed: Can't judge
0.51/0.54	
0.51/0.54	Try Layer Preserving Decomposition for...
0.51/0.54	   [ or(0,?x) -> ?x,
0.51/0.54	     or(?x,0) -> ?x,
0.51/0.54	     or(1,?x) -> 1,
0.51/0.54	     or(?x,1) -> 1,
0.51/0.54	     or(?x,not(?x)) -> 1,
0.51/0.54	     or(not(?x),?x) -> 1,
0.51/0.54	     and(0,?x) -> 0,
0.51/0.54	     and(?x,0) -> 0,
0.51/0.54	     and(1,?x) -> ?x,
0.51/0.54	     and(?x,1) -> ?x,
0.51/0.54	     and(?x,not(?x)) -> 0,
0.51/0.54	     and(not(?x),?x) -> 0,
0.51/0.54	     not(1) -> 0,
0.51/0.54	     not(0) -> 1,
0.51/0.54	     implies(?x,?y) -> U2(not(?x),?x,?y),
0.51/0.54	     U2(1,?x,?y) -> 1,
0.51/0.54	     implies(?x,?y) -> U2(?y,?x,?y),
0.51/0.54	     implies(?x,?y) -> U2(?x,?x,?y),
0.51/0.54	     U2(1,?x,?y) -> U3(?y,?x,?y),
0.51/0.54	     U3(0,?x,?y) -> 0,
0.51/0.54	     f(?x) -> U4(implies(?x,0),?x),
0.51/0.54	     U4(?y,?x) -> U5(implies(?x,?y),?x,?y),
0.51/0.54	     U5(?z,?x,?y) -> U6(implies(?z,0),?x,?y,?z),
0.51/0.54	     U6(1,?x,?y,?z) -> f(0) ]
0.51/0.54	Layer Preserving Decomposition failed: Can't judge
0.51/0.54	
0.51/0.54	Try Commutative Decomposition for...
0.51/0.54	   [ or(0,?x) -> ?x,
0.51/0.54	     or(?x,0) -> ?x,
0.51/0.54	     or(1,?x) -> 1,
0.51/0.54	     or(?x,1) -> 1,
0.51/0.54	     or(?x,not(?x)) -> 1,
0.51/0.54	     or(not(?x),?x) -> 1,
0.51/0.54	     and(0,?x) -> 0,
0.51/0.54	     and(?x,0) -> 0,
0.51/0.54	     and(1,?x) -> ?x,
0.51/0.54	     and(?x,1) -> ?x,
0.51/0.54	     and(?x,not(?x)) -> 0,
0.51/0.54	     and(not(?x),?x) -> 0,
0.51/0.54	     not(1) -> 0,
0.51/0.54	     not(0) -> 1,
0.51/0.54	     implies(?x,?y) -> U2(not(?x),?x,?y),
0.51/0.54	     U2(1,?x,?y) -> 1,
0.51/0.54	     implies(?x,?y) -> U2(?y,?x,?y),
0.51/0.54	     implies(?x,?y) -> U2(?x,?x,?y),
0.51/0.54	     U2(1,?x,?y) -> U3(?y,?x,?y),
0.51/0.54	     U3(0,?x,?y) -> 0,
0.51/0.54	     f(?x) -> U4(implies(?x,0),?x),
0.51/0.54	     U4(?y,?x) -> U5(implies(?x,?y),?x,?y),
0.51/0.54	     U5(?z,?x,?y) -> U6(implies(?z,0),?x,?y,?z),
0.51/0.54	     U6(1,?x,?y,?z) -> f(0) ]
0.51/0.54	Commutative Decomposition failed (not left-linear): Can't judge
0.51/0.54	No further decomposition possible
0.51/0.54	
0.51/0.54	
0.51/0.54	Combined result: Can't judge
0.51/0.54	failed to show confluence of U(R)
0.51/0.54	/export/starexec/sandbox/benchmark/theBenchmark.trs: Failure(unknown CR)
0.51/0.54	(480 msec.)
0.51/0.54	EOF