pushset Lemma 2 ----> UNIT CONFLICT at 1005.07 sec ----> 14169 [binary,14168.1,22.1] $F. Length of proof is 11. Level of proof is 10.
2 [reference] p1 pair(x,y)=x. 3 [reference] p2 pair(x,y)=y. 22 [reference] p1!=p2. 23 [reference] p2!=p1. 49 [reference] closedunder pair(xs,xf)=p2|xs x !=p1|xs (xf x) =p1. 50 [reference] closedunder pair(xs,xf)=p1|xs notclosed(xs,xf) =p1. 51 [reference] closedunder pair(xs,xf)=p1|xs (xf notclosed(xs,xf)) !=p1. 64 [reference] subset pair(x1,x2)=p2|x1 xc !=p1|x2 xc =p1. 76 [reference] subset pair(xs,closure pair(xs,xf))=p1. 77 [reference] closedunder pair(closure pair(xs,xf),xf)=p1. 82 [reference] closedunder pair(x2,p2 x1)=p2|subset pair(p1 x1,x2) =p2|subset pair(closure x1,x2) =p1. 88 [reference] closure pair(notp1 charq,setof) x=p2|push x =setof x. 92 [reference] closure pair(notp1 charq,setof) x=p2|closure pair(notp1 charq,setof) (push x) =p1. 95 [reference] closure pair(notp1 charq,setof) (push x)=closure pair(notp1 charq,setof) x. 101 [reference] closure pair(notp1 charq,push) x=p2|closure pair(notp1 charq,setof) x =p1. 102 [assumption to refute] closure pair(notp1 charq,push) bad!=p1. 103 [assumption to refute] closure pair(notp1 charq,setof) bad!=p2. 128 [ur,103,92,demod,95] closure pair(notp1 charq,setof) bad=p1. 164 [ur,128,64,102] subset pair(closure pair(notp1 charq,setof),closure pair(notp1 charq,push))=p2. 531 [para_into,164.1.1,82.3.1,demod,3,2,unit_del,22] closedunder pair(closure pair(notp1 charq,push),setof)=p2|subset pair(notp1 charq,closure pair(notp1 charq,push)) =p2. 13188 [para_into,531.2.1,76.1.1,unit_del,22] closedunder pair(closure pair(notp1 charq,push),setof)=p2. 13189 [para_into,13188.1.1,51.1.1,unit_del,22] closure pair(notp1 charq,push) (setof notclosed(closure pair(notp1 charq,push),setof))!=p1. 13190 [para_into,13188.1.1,50.1.1,unit_del,22] closure pair(notp1 charq,push) notclosed(closure pair(notp1 charq,push),setof)=p1. 13213 [para_into,13190.1.1,101.1.1,unit_del,23] closure pair(notp1 charq,setof) notclosed(closure pair(notp1 charq,push),setof)=p1. 13265 [para_from,13213.1.2,22.1.1] closure pair(notp1 charq,setof) notclosed(closure pair(notp1 charq,push),setof)!=p2. 13371 [para_into,13189.1.1.2,88.2.2,unit_del,13265] closure pair(notp1 charq,push) (push notclosed(closure pair(notp1 charq,push),setof))!=p1. 14167 [ur,13371,49,13190] closedunder pair(closure pair(notp1 charq,push),push)=p2. 14168 [para_into,14167.1.1,77.1.1] p1=p2. 14169 [binary,14168.1,22.1] $F.
up | previous | next | detailed contents | brief contents | OTTER output file