setof is one-to-one weight_list(pick_and_purge). weight(x,1000). weight(noteq(bad1,bad2),1). weight(a(setof,bad1),1). weight(a(setof,bad2),1). end_of_list. -----> EMPTY CLAUSE at 49.38 sec ----> 4119 [para_into,785.1.1,35.2.1,demod,3,2,unit_del,74,8] $F. Length of proof is 7. Level of proof is 4.
2 [reference] p1 pair(x,y)=x. 3 [reference] p2 pair(x,y)=y. 8 [reference] x=x. 15 [reference] x!=y|eq pair(x,y) =p1. 16 [reference] x=y|eq pair(x,y) =p2. 17 [reference] x=y|x noteq(x,y) !=y noteq(x,y). 18 [reference] p1!=p2. 34 [reference] setof xf pair(x,y)=p2|xf x =y. 35 [reference] p2 xy!=xf (p1 xy) |setof xf xy =p1. 38 [assumption to refute] setof bad1=setof bad2. 39 [assumption to refute] bad1!=bad2. 41,40 [ur,38,15] eq pair(setof bad1,setof bad2)=p1. 56 [ur,39,17,flip.1] bad2 noteq(bad1,bad2)!=bad1 noteq(bad1,bad2). 71 [para_into,40.1.1,16.2.1,flip.2] p2=p1|setof bad2 =setof bad1. 74 [para_from,40.1.2,18.1.1,demod,41,flip.1] p2!=p1. 94 [ur,71,74] setof bad2=setof bad1. 97 [ur,56,34] setof bad2 pair(noteq(bad1,bad2),bad1 noteq(bad1,bad2))=p2. 785 [para_into,97.1.1.1,94.1.1] setof bad1 pair(noteq(bad1,bad2),bad1 noteq(bad1,bad2))=p2. 4119 [para_into,785.1.1,35.2.1,demod,3,2,unit_del,74,8] $F.
up | previous | next | detailed contents | brief contents | OTTER output file