FunExperiments 40 % timbuk --fung 30 orderedTree.txt

term height= 1

term height= 2
Rejected: 0
term height= 3
Rejected: 4
term height= 4
Rejected: 12

Generated equations:
-------------------
Node(A,Node(B,Node(A,Leaf,Leaf),Leaf),Node(B,Node(A,Leaf,Leaf),Leaf)) = Node(B,Node(A,Leaf,Leaf),Leaf)
Node(A,Node(B,Node(A,Leaf,Leaf),Leaf),Node(A,Leaf,Node(B,Leaf,Leaf))) = Node(A,Leaf,Node(B,Leaf,Leaf))
Node(A,Node(B,Node(A,Leaf,Leaf),Leaf),Node(A,Leaf,Leaf)) = Node(A,Leaf,Leaf)
Node(A,Node(B,Node(A,Leaf,Leaf),Leaf),Node(B,Leaf,Leaf)) = Node(B,Leaf,Leaf)
Node(A,Node(B,Node(A,Leaf,Leaf),Leaf),Leaf) = Leaf
Node(A,Node(A,Leaf,Node(B,Leaf,Leaf)),Node(B,Node(A,Leaf,Leaf),Leaf)) = Node(B,Node(A,Leaf,Leaf),Leaf)
Node(A,Node(A,Leaf,Leaf),Node(B,Node(A,Leaf,Leaf),Leaf)) = Node(B,Node(A,Leaf,Leaf),Leaf)
Node(A,Node(B,Leaf,Leaf),Node(B,Node(A,Leaf,Leaf),Leaf)) = Node(B,Node(A,Leaf,Leaf),Leaf)
Node(A,Leaf,Node(B,Node(A,Leaf,Leaf),Leaf)) = Node(B,Node(A,Leaf,Leaf),Leaf)
Node(B,Node(B,Node(A,Leaf,Leaf),Leaf),Node(B,Node(A,Leaf,Leaf),Leaf)) = Node(B,Node(A,Leaf,Leaf),Leaf)
Node(B,Node(B,Node(A,Leaf,Leaf),Leaf),Node(A,Leaf,Node(B,Leaf,Leaf))) = Node(A,Leaf,Node(B,Leaf,Leaf))
Node(B,Node(B,Node(A,Leaf,Leaf),Leaf),Node(A,Leaf,Leaf)) = Node(A,Leaf,Leaf)
Node(B,Node(B,Node(A,Leaf,Leaf),Leaf),Node(B,Leaf,Leaf)) = Node(B,Leaf,Leaf)
Node(B,Node(B,Node(A,Leaf,Leaf),Leaf),Leaf) = Leaf
Node(B,Node(A,Leaf,Node(B,Leaf,Leaf)),Node(B,Node(A,Leaf,Leaf),Leaf)) = Node(B,Node(A,Leaf,Leaf),Leaf)
Node(B,Node(A,Leaf,Leaf),Node(B,Node(A,Leaf,Leaf),Leaf)) = Node(B,Node(A,Leaf,Leaf),Leaf)
Node(B,Node(B,Leaf,Leaf),Node(B,Node(A,Leaf,Leaf),Leaf)) = Node(B,Node(A,Leaf,Leaf),Leaf)
Node(B,Leaf,Node(B,Node(A,Leaf,Leaf),Leaf)) = Node(B,Node(A,Leaf,Leaf),Leaf)
Node(A,Node(A,Leaf,Node(B,Leaf,Leaf)),Node(A,Leaf,Node(B,Leaf,Leaf))) = Node(A,Leaf,Node(B,Leaf,Leaf))
Node(A,Node(A,Leaf,Node(B,Leaf,Leaf)),Node(A,Leaf,Leaf)) = Node(A,Leaf,Leaf)
Node(A,Node(A,Leaf,Node(B,Leaf,Leaf)),Node(B,Leaf,Leaf)) = Node(B,Leaf,Leaf)
Node(A,Node(A,Leaf,Node(B,Leaf,Leaf)),Leaf) = Leaf
Node(A,Node(A,Leaf,Leaf),Node(A,Leaf,Node(B,Leaf,Leaf))) = Node(A,Leaf,Node(B,Leaf,Leaf))
Node(A,Node(B,Leaf,Leaf),Node(A,Leaf,Node(B,Leaf,Leaf))) = Node(A,Leaf,Node(B,Leaf,Leaf))
Node(A,Leaf,Node(A,Leaf,Node(B,Leaf,Leaf))) = Node(A,Leaf,Node(B,Leaf,Leaf))
Node(B,Node(A,Leaf,Node(B,Leaf,Leaf)),Node(A,Leaf,Node(B,Leaf,Leaf))) = Node(A,Leaf,Node(B,Leaf,Leaf))
Node(B,Node(A,Leaf,Node(B,Leaf,Leaf)),Node(A,Leaf,Leaf)) = Node(A,Leaf,Leaf)
Node(B,Node(A,Leaf,Node(B,Leaf,Leaf)),Node(B,Leaf,Leaf)) = Node(B,Leaf,Leaf)
Node(B,Node(A,Leaf,Node(B,Leaf,Leaf)),Leaf) = Leaf
Node(B,Node(A,Leaf,Leaf),Node(A,Leaf,Node(B,Leaf,Leaf))) = Node(A,Leaf,Node(B,Leaf,Leaf))
Node(B,Node(B,Leaf,Leaf),Node(A,Leaf,Node(B,Leaf,Leaf))) = Node(A,Leaf,Node(B,Leaf,Leaf))
Node(B,Leaf,Node(A,Leaf,Node(B,Leaf,Leaf))) = Node(A,Leaf,Node(B,Leaf,Leaf))
Node(A,Node(A,Leaf,Leaf),Node(A,Leaf,Leaf)) = Node(A,Leaf,Leaf)
Node(A,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)) = Node(A,Leaf,Leaf)
Node(A,Node(A,Leaf,Leaf),Leaf) = Node(A,Leaf,Leaf)
Node(A,Node(B,Leaf,Leaf),Node(A,Leaf,Leaf)) = Node(A,Leaf,Leaf)
Node(A,Leaf,Node(A,Leaf,Leaf)) = Node(A,Leaf,Leaf)
Node(B,Node(A,Leaf,Leaf),Node(A,Leaf,Leaf)) = Node(A,Leaf,Leaf)
Node(B,Node(A,Leaf,Leaf),Node(B,Leaf,Leaf)) = Node(B,Leaf,Leaf)
Node(B,Node(B,Leaf,Leaf),Node(A,Leaf,Leaf)) = Node(A,Leaf,Leaf)
Node(B,Leaf,Node(A,Leaf,Leaf)) = Node(A,Leaf,Leaf)
Node(A,Node(B,Leaf,Leaf),Node(B,Leaf,Leaf)) = Node(B,Leaf,Leaf)
Node(A,Node(B,Leaf,Leaf),Leaf) = Leaf
Node(B,Node(B,Leaf,Leaf),Node(B,Leaf,Leaf)) = Node(B,Leaf,Leaf)
Node(B,Node(B,Leaf,Leaf),Leaf) = Node(B,Leaf,Leaf)
Node(B,Leaf,Node(B,Leaf,Leaf)) = Node(B,Leaf,Leaf)
B = B
ordered(U) = ordered(U)
and(U,V) = and(U,V)
A = A
true = true
Leaf = Leaf
false = false
Node(U,V,X) = Node(U,V,X)
leq(U,V) = leq(U,V)
ite(U,V,X) = ite(U,V,X)
leq(A,B) = true
leq(A,A) = true
leq(B,A) = false
leq(B,B) = true
ite(true,X,Y) = X
ite(false,X,Y) = Y
ordered(Leaf) = true
ordered(Node(X,Leaf,Leaf)) = true
ordered(Node(X,Node(Y,Z,U),Leaf)) = and(leq(Y,X),ordered(Node(Y,Z,U)))
ordered(Node(X,Leaf,Node(Y,Z,U))) = and(leq(X,Y),ordered(Node(Y,Z,U)))
ordered(Node(X,Node(X1,X2,X3),Node(Y,Z,U))) = and(leq(X1,X),and(leq(X,Y),and(ordered(Node(X1,X2,X3)),ordered(Node(Y,Z,U)))))
and(true,X) = X
and(false,X) = false

Automaton projected on constructor terms:
-----------------------------------------
States q80 
Final States q80 
Transitions
true -> q80

Regular expression:
-------------------
true

Step: 6


Automaton complete!
------------------

Proof done!
-----------


Exported comp.res file
Exported comp.res.epsi file
Completion time: 0.162319 seconds
Equation generation time: 6.732496 seconds
FunExperiments 41 % checker -fp comp.res
Post fixpoint : 
- R1*(Ainit) included in Acomp :	 OK