1 var 1
2 var 1
3 var 1 
4 eq 1 1 2
5 eq 1 2 3
6 eq 1 1 3
7 and 1 4 5
8 implies 1 7 6
9 root 1 -8