push is onto the characteristic functions -----> EMPTY CLAUSE at 18.25 sec ----> 3467 [para_into,119.4.1,152.1.1,unit_del,12,592,23] $ans(notclosed(remove_singleton pair(closure pair(notp1 charq,push),k(bad)),push))|$ans(bad). Length of proof is 5. Level of proof is 3.
12 [reference] x=x. 23 [reference] p2!=p1. 31 [reference] x y!=p1|notp1 x y =p2. 87 [reference] closure pair(notp1 charq,setof) x=p1|push x =x. 100 [reference] xf notclosed(remove_singleton pair(closure pair(xs,xf),k(x)),xf)=x|closure pair(xs,xf) x =p2|xs x =p1. 103 [reference] closure pair(notp1 charq,push)=closure pair(notp1 charq,setof). 104 [assumption to refute] push x!=bad|$ans(x). 105 [assumption to refute] charq bad=p1. 109 [ur,104,87] $ans(bad)|closure pair(notp1 charq,setof) bad =p1. 119 [para_into,104.1.1,100.1.1] x!=bad|$ans(notclosed(remove_singleton pair(closure pair(y,push),k(x)),push))|closure pair(y,push) x =p2|y x =p1. 152 [ur,105,31] notp1 charq bad=p2. 457 [para_from,109.1.2,23.1.2,flip.1] closure pair(notp1 charq,setof) bad!=p2|$ans(bad). 592 [para_into,457.1.1.1,103.1.2] closure pair(notp1 charq,push) bad!=p2|$ans(bad). 3467 [para_into,119.4.1,152.1.1,unit_del,12,592,23] $ans(notclosed(remove_singleton pair(closure pair(notp1 charq,push),k(bad)),push))|$ans(bad).
up | previous | detailed contents | brief contents | OTTER output file