push, case 2 closure pair(notp1 charq,setof) bad != p2, was placed in the usable list, while the other, push bad != setof bad was placed in the set of support.-----> EMPTY CLAUSE at 2.17 sec ----> 264 [para_into,88.1.1.1.2.2.1,79.1.1,demod,7,2,unit_del,12,86] $F. Length of proof is 1. Level of proof is 1.
1 [reference] k(x) y=x. 2 [reference] p1 pair(x,y)=x. 4 [reference] pair(x,y) z=pair(x z,y z). 5 [reference] pair(p1 x,p2 x)=x. 6 [reference] abst x y z=x k(z) (y z). 7 [reference] eq pair(x,x)=p1. 12 [reference] x=x. 55 [reference] abst k(x) k(y)=k(x y). 79 [reference] closure x y=p1|closure x y =p2. 83 [reference] push=abst (abst k(eq) pair(k(k(p1)),abst k(closure pair(notp1 charq,setof)))) pair(setof,pair(p1,p2)). 85 [assumption to refute] p. 86 [assumption to refute] closure pair(notp1 charq,setof) bad!=p2. 87 [assumption to refute] -p|push bad !=setof bad. 88 [ur,87,85,demod,83,6,6,1,4,1,55,4,4,5] eq pair(k(p1),k(closure pair(notp1 charq,setof) bad)) pair(setof bad,bad)!=setof bad. 264 [para_into,88.1.1.1.2.2.1,79.1.1,demod,7,2,unit_del,12,86] $F.
up | previous | next | detailed contents | brief contents | OTTER output file