pushset Lemma 3 -----> EMPTY CLAUSE at 558.66 sec ----> 10196 [back_demod,398,demod,10187,10187,unit_del,12,23] $F. Length of proof is 4. Level of proof is 3.
12 [reference] x=x. 21 [reference] x=y|x noteq(x,y) !=y noteq(x,y). 23 [reference] p2!=p1. 79 [reference] closure x y=p1|closure x y =p2. 101 [reference] closure pair(notp1 charq,push) x=p2|closure pair(notp1 charq,setof) x =p1. 102 [reference] closure pair(notp1 charq,push) x=p1|closure pair(notp1 charq,setof) x =p2. 103 [assumption to refute] closure pair(notp1 charq,push)!=closure pair(notp1 charq,setof). 110 [ur,103,21,flip.1] closure pair(notp1 charq,setof) noteq(closure pair(notp1 charq,push),closure pair(notp1 charq,setof))!=closure pair(notp1 charq,push) noteq(closure pair(notp1 charq,push),closure pair(notp1 charq,setof)). 397 [para_into,110.1.1,102.2.1,flip.1] closure pair(notp1 charq,push) noteq(closure pair(notp1 charq,push),closure pair(notp1 charq,setof))!=p2|closure pair(notp1 charq,push) noteq(closure pair(notp1 charq,push),closure pair(notp1 charq,setof)) =p1. 398 [para_into,110.1.1,101.2.1,flip.1] closure pair(notp1 charq,push) noteq(closure pair(notp1 charq,push),closure pair(notp1 charq,setof))!=p1|closure pair(notp1 charq,push) noteq(closure pair(notp1 charq,push),closure pair(notp1 charq,setof)) =p2. 10187,10186 [para_into,397.1.1,79.2.1,unit_del,12] closure pair(notp1 charq,push) noteq(closure pair(notp1 charq,push),closure pair(notp1 charq,setof))=p1. 10196 [back_demod,398,demod,10187,10187,unit_del,12,23] $F.
up | previous | next | detailed contents | brief contents | OTTER output file