%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWC414-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n009.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jul 27 13:19:37 EDT 2022 % Result : Timeout 299.95s 300.04s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : SWC414-1 : TPTP v8.1.0. Released v2.4.0. % 0.07/0.13 % Command : otter-tptp-script %s % 0.13/0.34 % Computer : n009.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Jul 27 04:46:36 EDT 2022 % 0.13/0.35 % CPUTime : % 16.00/16.14 ----- Otter 3.3f, August 2004 ----- % 16.00/16.14 The process was started by sandbox2 on n009.cluster.edu, % 16.00/16.14 Wed Jul 27 04:46:36 2022 % 16.00/16.14 The command was "./otter". The process ID is 22606. % 16.00/16.14 % 16.00/16.14 set(prolog_style_variables). % 16.00/16.14 set(auto). % 16.00/16.14 dependent: set(auto1). % 16.00/16.14 dependent: set(process_input). % 16.00/16.14 dependent: clear(print_kept). % 16.00/16.14 dependent: clear(print_new_demod). % 16.00/16.14 dependent: clear(print_back_demod). % 16.00/16.14 dependent: clear(print_back_sub). % 16.00/16.14 dependent: set(control_memory). % 16.00/16.14 dependent: assign(max_mem, 12000). % 16.00/16.14 dependent: assign(pick_given_ratio, 4). % 16.00/16.14 dependent: assign(stats_level, 1). % 16.00/16.14 dependent: assign(max_seconds, 10800). % 16.00/16.14 clear(print_given). % 16.00/16.14 % 16.00/16.14 list(usable). % 16.00/16.14 0 [] A=A. % 16.00/16.14 0 [] e_qualelemsP(nil). % 16.00/16.14 0 [] duplicatefreeP(nil). % 16.00/16.14 0 [] strictorderedP(nil). % 16.00/16.14 0 [] totalorderedP(nil). % 16.00/16.14 0 [] strictorderP(nil). % 16.00/16.14 0 [] totalorderP(nil). % 16.00/16.14 0 [] cyclefreeP(nil). % 16.00/16.14 0 [] ssList(nil). % 16.00/16.14 0 [] ssItem(skac3). % 16.00/16.14 0 [] ssItem(skac2). % 16.00/16.14 0 [] -singletonP(nil). % 16.00/16.14 0 [] ssItem(skaf83(U)). % 16.00/16.14 0 [] ssList(skaf82(U)). % 16.00/16.14 0 [] ssList(skaf81(U)). % 16.00/16.14 0 [] ssList(skaf80(U)). % 16.00/16.14 0 [] ssItem(skaf79(U)). % 16.00/16.15 0 [] ssItem(skaf78(U)). % 16.00/16.15 0 [] ssList(skaf77(U)). % 16.00/16.15 0 [] ssList(skaf76(U)). % 16.00/16.15 0 [] ssList(skaf75(U)). % 16.00/16.15 0 [] ssItem(skaf74(U)). % 16.00/16.15 0 [] ssList(skaf73(U)). % 16.00/16.15 0 [] ssList(skaf72(U)). % 16.00/16.15 0 [] ssList(skaf71(U)). % 16.00/16.15 0 [] ssItem(skaf70(U)). % 16.00/16.15 0 [] ssItem(skaf69(U)). % 16.00/16.15 0 [] ssList(skaf68(U)). % 16.00/16.15 0 [] ssList(skaf67(U)). % 16.00/16.15 0 [] ssList(skaf66(U)). % 16.00/16.15 0 [] ssItem(skaf65(U)). % 16.00/16.15 0 [] ssItem(skaf64(U)). % 16.00/16.15 0 [] ssList(skaf63(U)). % 16.00/16.15 0 [] ssList(skaf62(U)). % 16.00/16.15 0 [] ssList(skaf61(U)). % 16.00/16.15 0 [] ssItem(skaf60(U)). % 16.00/16.15 0 [] ssItem(skaf59(U)). % 16.00/16.15 0 [] ssList(skaf58(U)). % 16.00/16.15 0 [] ssList(skaf57(U)). % 16.00/16.15 0 [] ssList(skaf56(U)). % 16.00/16.15 0 [] ssItem(skaf55(U)). % 16.00/16.15 0 [] ssItem(skaf54(U)). % 16.00/16.15 0 [] ssList(skaf53(U)). % 16.00/16.15 0 [] ssList(skaf52(U)). % 16.00/16.15 0 [] ssList(skaf51(U)). % 16.00/16.15 0 [] ssItem(skaf50(U)). % 16.00/16.15 0 [] ssItem(skaf49(U)). % 16.00/16.15 0 [] ssItem(skaf44(U)). % 16.00/16.15 0 [] ssList(skaf48(U,V)). % 16.00/16.15 0 [] ssList(skaf47(U,V)). % 16.00/16.15 0 [] ssList(skaf46(U,V)). % 16.00/16.15 0 [] ssList(skaf45(U,V)). % 16.00/16.15 0 [] ssList(skaf43(U,V)). % 16.00/16.15 0 [] ssList(skaf42(U,V)). % 16.00/16.15 0 [] skac3!=skac2. % 16.00/16.15 0 [] -ssItem(U)|ge_q(U,U). % 16.00/16.15 0 [] -ssList(U)|segmentP(U,nil). % 16.00/16.15 0 [] -ssList(U)|segmentP(U,U). % 16.00/16.15 0 [] -ssList(U)|rearsegP(U,nil). % 16.00/16.15 0 [] -ssList(U)|rearsegP(U,U). % 16.00/16.15 0 [] -ssList(U)|frontsegP(U,nil). % 16.00/16.15 0 [] -ssList(U)|frontsegP(U,U). % 16.00/16.15 0 [] -ssItem(U)|le_q(U,U). % 16.00/16.15 0 [] -lt(U,U)| -ssItem(U). % 16.00/16.15 0 [] -ssItem(U)|e_qualelemsP(cons(U,nil)). % 16.00/16.15 0 [] -ssItem(U)|duplicatefreeP(cons(U,nil)). % 16.00/16.15 0 [] -ssItem(U)|strictorderedP(cons(U,nil)). % 16.00/16.15 0 [] -ssItem(U)|totalorderedP(cons(U,nil)). % 16.00/16.15 0 [] -ssItem(U)|strictorderP(cons(U,nil)). % 16.00/16.15 0 [] -ssItem(U)|totalorderP(cons(U,nil)). % 16.00/16.15 0 [] -ssItem(U)|cyclefreeP(cons(U,nil)). % 16.00/16.15 0 [] -memberP(nil,U)| -ssItem(U). % 16.00/16.15 0 [] -ssList(U)|duplicatefreeP(U)|ssItem(V). % 16.00/16.15 0 [] -ssList(U)|app(U,nil)=U. % 16.00/16.15 0 [] -ssList(U)|app(nil,U)=U. % 16.00/16.15 0 [] -ssList(U)|ssList(tl(U))|nil=U. % 16.00/16.15 0 [] -ssList(U)|ssItem(hd(U))|nil=U. % 16.00/16.15 0 [] -ssList(U)|ssList(tl(U))|nil=U. % 16.00/16.15 0 [] -ssList(U)|ssItem(hd(U))|nil=U. % 16.00/16.15 0 [] nil!=U| -ssList(U)|segmentP(nil,U). % 16.00/16.15 0 [] -segmentP(nil,U)| -ssList(U)|nil=U. % 16.00/16.15 0 [] nil!=U| -ssList(U)|rearsegP(nil,U). % 16.00/16.15 0 [] -rearsegP(nil,U)| -ssList(U)|nil=U. % 16.00/16.15 0 [] nil!=U| -ssList(U)|frontsegP(nil,U). % 16.00/16.15 0 [] -frontsegP(nil,U)| -ssList(U)|nil=U. % 16.00/16.15 0 [] -ssList(U)| -ssList(V)|ssList(app(V,U)). % 16.00/16.15 0 [] -ssItem(U)| -ssList(V)|ssList(cons(U,V)). % 16.00/16.15 0 [] -ssList(U)|cyclefreeP(U)|le_q(skaf50(U),skaf49(U)). % 16.00/16.15 0 [] -ssList(U)|cyclefreeP(U)|le_q(skaf49(U),skaf50(U)). % 16.00/16.15 0 [] skaf79(U)!=skaf78(U)| -ssList(U)|e_qualelemsP(U). % 16.00/16.15 0 [] -lt(skaf69(U),skaf70(U))| -ssList(U)|strictorderedP(U). % 16.00/16.15 0 [] -le_q(skaf64(U),skaf65(U))| -ssList(U)|totalorderedP(U). % 16.00/16.15 0 [] -lt(skaf60(U),skaf59(U))| -ssList(U)|strictorderP(U). % 16.00/16.15 0 [] -lt(skaf59(U),skaf60(U))| -ssList(U)|strictorderP(U). % 16.00/16.15 0 [] -le_q(skaf55(U),skaf54(U))| -ssList(U)|totalorderP(U). % 16.00/16.15 0 [] -le_q(skaf54(U),skaf55(U))| -ssList(U)|totalorderP(U). % 16.00/16.15 0 [] -ssItem(U)| -ssList(V)|tl(cons(U,V))=V. % 16.00/16.15 0 [] -ssItem(U)| -ssList(V)|hd(cons(U,V))=U. % 16.00/16.15 0 [] cons(U,V)!=nil| -ssItem(U)| -ssList(V). % 16.00/16.15 0 [] cons(U,V)!=V| -ssItem(U)| -ssList(V). % 16.00/16.15 0 [] -ssList(U)| -ssList(V)|ne_q(V,U)|V=U. % 16.00/16.15 0 [] -singletonP(U)| -ssList(U)|cons(skaf44(U),nil)=U. % 16.00/16.15 0 [] -ssItem(U)| -ssItem(V)|ne_q(V,U)|V=U. % 16.00/16.15 0 [] -lt(U,V)| -ssItem(V)| -ssItem(U)|le_q(U,V). % 16.00/16.15 0 [] -ssList(U)|cons(hd(U),tl(U))=U|nil=U. % 16.00/16.15 0 [] -gt(U,V)| -ssItem(V)| -ssItem(U)|lt(V,U). % 16.00/16.15 0 [] -lt(U,V)| -ssItem(U)| -ssItem(V)|gt(V,U). % 16.00/16.15 0 [] -ge_q(U,V)| -ssItem(V)| -ssItem(U)|le_q(V,U). % 16.00/16.15 0 [] -le_q(U,V)| -ssItem(U)| -ssItem(V)|ge_q(V,U). % 16.00/16.15 0 [] -ssList(U)|cons(skaf83(U),skaf82(U))=U|nil=U. % 16.00/16.15 0 [] -gt(U,V)| -gt(V,U)| -ssItem(U)| -ssItem(V). % 16.00/16.15 0 [] U!=V| -lt(U,V)| -ssItem(V)| -ssItem(U). % 16.00/16.15 0 [] nil!=U| -ssList(U)| -ssItem(V)|strictorderedP(cons(V,U)). % 16.00/16.15 0 [] nil!=U| -ssList(U)| -ssItem(V)|totalorderedP(cons(V,U)). % 16.00/16.15 0 [] -lt(U,V)| -lt(V,U)| -ssItem(U)| -ssItem(V). % 16.00/16.15 0 [] U!=V| -ne_q(U,V)| -ssList(V)| -ssList(U). % 16.00/16.15 0 [] cons(U,nil)!=V| -ssItem(U)| -ssList(V)|singletonP(V). % 16.00/16.15 0 [] U!=V| -ne_q(U,V)| -ssItem(V)| -ssItem(U). % 16.00/16.15 0 [] app(U,V)!=nil| -ssList(V)| -ssList(U)|nil=U. % 16.00/16.15 0 [] app(U,V)!=nil| -ssList(V)| -ssList(U)|nil=V. % 16.00/16.15 0 [] -ssItem(U)| -ssList(V)|app(cons(U,nil),V)=cons(U,V). % 16.00/16.15 0 [] -le_q(U,V)| -ssItem(V)| -ssItem(U)|lt(U,V)|U=V. % 16.00/16.15 0 [] -le_q(U,V)| -ssItem(V)| -ssItem(U)|lt(U,V)|U=V. % 16.00/16.15 0 [] -ssList(U)| -ssList(V)|nil=V|hd(app(V,U))=hd(V). % 16.00/16.15 0 [] -strictorderedP(cons(U,V))| -ssList(V)| -ssItem(U)|strictorderedP(V)|nil=V. % 16.00/16.15 0 [] -totalorderedP(cons(U,V))| -ssList(V)| -ssItem(U)|totalorderedP(V)|nil=V. % 16.00/16.15 0 [] -ge_q(U,V)| -ge_q(V,U)| -ssItem(U)| -ssItem(V)|V=U. % 16.00/16.15 0 [] -segmentP(U,V)| -segmentP(V,U)| -ssList(U)| -ssList(V)|V=U. % 16.00/16.15 0 [] -rearsegP(U,V)| -rearsegP(V,U)| -ssList(U)| -ssList(V)|V=U. % 16.00/16.15 0 [] -frontsegP(U,V)| -frontsegP(V,U)| -ssList(U)| -ssList(V)|V=U. % 16.00/16.15 0 [] -le_q(U,V)| -le_q(V,U)| -ssItem(U)| -ssItem(V)|V=U. % 16.00/16.15 0 [] -rearsegP(U,V)| -ssList(V)| -ssList(U)|app(skaf46(U,V),V)=U. % 16.00/16.15 0 [] -frontsegP(U,V)| -ssList(V)| -ssList(U)|app(V,skaf45(U,V))=U. % 16.00/16.15 0 [] -ssList(U)| -ssList(V)|nil=V|tl(app(V,U))=app(tl(V),U). % 16.00/16.15 0 [] -strictorderedP(cons(U,V))| -ssList(V)| -ssItem(U)|lt(U,hd(V))|nil=V. % 16.00/16.15 0 [] -totalorderedP(cons(U,V))| -ssList(V)| -ssItem(U)|le_q(U,hd(V))|nil=V. % 16.00/16.15 0 [] -rearsegP(U,V)| -ssList(W)| -ssList(V)| -ssList(U)|rearsegP(app(W,U),V). % 16.00/16.15 0 [] -frontsegP(U,V)| -ssList(W)| -ssList(V)| -ssList(U)|frontsegP(app(U,W),V). % 16.00/16.15 0 [] U!=V| -ssList(W)| -ssItem(V)| -ssItem(U)|memberP(cons(V,W),U). % 16.00/16.15 0 [] -memberP(U,V)| -ssList(U)| -ssItem(W)| -ssItem(V)|memberP(cons(W,U),V). % 16.00/16.15 0 [] -memberP(U,V)| -ssList(W)| -ssList(U)| -ssItem(V)|memberP(app(U,W),V). % 16.00/16.15 0 [] -memberP(U,V)| -ssList(U)| -ssList(W)| -ssItem(V)|memberP(app(W,U),V). % 16.00/16.15 0 [] -ssList(U)|e_qualelemsP(U)|app(skaf80(U),cons(skaf78(U),cons(skaf79(U),skaf81(U))))=U. % 16.00/16.15 0 [] app(U,V)!=W| -ssList(U)| -ssList(V)| -ssList(W)|rearsegP(W,V). % 16.00/16.15 0 [] app(U,V)!=W| -ssList(V)| -ssList(U)| -ssList(W)|frontsegP(W,U). % 16.00/16.15 0 [] nil!=U|nil!=V| -ssList(V)| -ssList(U)|app(U,V)=nil. % 16.00/16.15 0 [] -gt(U,V)| -gt(V,W)| -ssItem(W)| -ssItem(V)| -ssItem(U)|gt(U,W). % 16.00/16.15 0 [] -le_q(U,V)| -lt(V,W)| -ssItem(W)| -ssItem(V)| -ssItem(U)|lt(U,W). % 16.00/16.15 0 [] -ge_q(U,V)| -ge_q(V,W)| -ssItem(W)| -ssItem(V)| -ssItem(U)|ge_q(U,W). % 16.00/16.15 0 [] -ssList(U)| -ssList(V)| -ssList(W)|app(app(W,V),U)=app(W,app(V,U)). % 16.00/16.15 0 [] app(U,V)!=app(U,W)| -ssList(V)| -ssList(U)| -ssList(W)|V=W. % 16.00/16.15 0 [] app(U,V)!=app(W,V)| -ssList(U)| -ssList(V)| -ssList(W)|U=W. % 16.00/16.15 0 [] -segmentP(U,V)| -segmentP(V,W)| -ssList(W)| -ssList(V)| -ssList(U)|segmentP(U,W). % 16.00/16.15 0 [] -rearsegP(U,V)| -rearsegP(V,W)| -ssList(W)| -ssList(V)| -ssList(U)|rearsegP(U,W). % 16.00/16.15 0 [] -frontsegP(U,V)| -frontsegP(V,W)| -ssList(W)| -ssList(V)| -ssList(U)|frontsegP(U,W). % 16.00/16.15 0 [] -lt(U,V)| -lt(V,W)| -ssItem(W)| -ssItem(V)| -ssItem(U)|lt(U,W). % 16.00/16.15 0 [] -le_q(U,V)| -le_q(V,W)| -ssItem(W)| -ssItem(V)| -ssItem(U)|le_q(U,W). % 16.00/16.15 0 [] -ssItem(U)| -ssList(V)| -ssList(W)|cons(U,app(V,W))=app(cons(U,V),W). % 16.00/16.15 0 [] -memberP(app(U,V),W)| -ssList(V)| -ssList(U)| -ssItem(W)|memberP(V,W)|memberP(U,W). % 16.00/16.15 0 [] -le_q(U,hd(V))| -totalorderedP(V)| -ssList(V)| -ssItem(U)|totalorderedP(cons(U,V))|nil=V. % 16.00/16.15 0 [] -lt(U,hd(V))| -strictorderedP(V)| -ssList(V)| -ssItem(U)|strictorderedP(cons(U,V))|nil=V. % 16.00/16.15 0 [] -memberP(cons(U,V),W)| -ssList(V)| -ssItem(U)| -ssItem(W)|memberP(V,W)|W=U. % 16.00/16.15 0 [] -ssList(U)|duplicatefreeP(U)|app(app(skaf75(U),cons(skaf74(U),skaf76(U))),cons(skaf74(U),skaf77(U)))=U. % 16.00/16.15 0 [] -ssList(U)|strictorderedP(U)|app(app(skaf71(U),cons(skaf69(U),skaf72(U))),cons(skaf70(U),skaf73(U)))=U. % 16.00/16.15 0 [] -ssList(U)|totalorderedP(U)|app(app(skaf66(U),cons(skaf64(U),skaf67(U))),cons(skaf65(U),skaf68(U)))=U. % 16.00/16.15 0 [] -ssList(U)|strictorderP(U)|app(app(skaf61(U),cons(skaf59(U),skaf62(U))),cons(skaf60(U),skaf63(U)))=U. % 16.00/16.15 0 [] -ssList(U)|totalorderP(U)|app(app(skaf56(U),cons(skaf54(U),skaf57(U))),cons(skaf55(U),skaf58(U)))=U. % 16.00/16.15 0 [] -ssList(U)|cyclefreeP(U)|app(app(skaf51(U),cons(skaf49(U),skaf52(U))),cons(skaf50(U),skaf53(U)))=U. % 16.00/16.15 0 [] -segmentP(U,V)| -ssList(V)| -ssList(U)|app(app(skaf47(U,V),V),skaf48(V,U))=U. % 16.00/16.15 0 [] -memberP(U,V)| -ssItem(V)| -ssList(U)|app(skaf42(U,V),cons(V,skaf43(V,U)))=U. % 16.00/16.15 0 [] cons(U,V)!=cons(W,X)| -ssItem(W)| -ssItem(U)| -ssList(X)| -ssList(V)|U=W. % 16.00/16.15 0 [] cons(U,V)!=cons(W,X)| -ssItem(W)| -ssItem(U)| -ssList(X)| -ssList(V)|X=V. % 16.00/16.15 0 [] -segmentP(U,V)| -ssList(W)| -ssList(X)| -ssList(V)| -ssList(U)|segmentP(app(app(X,U),W),V). % 16.00/16.15 0 [] app(app(U,V),W)!=X| -ssList(W)| -ssList(U)| -ssList(V)| -ssList(X)|segmentP(X,V). % 16.00/16.15 0 [] -frontsegP(cons(U,V),cons(W,X))| -ssList(X)| -ssList(V)| -ssItem(W)| -ssItem(U)|frontsegP(V,X). % 16.00/16.15 0 [] app(U,cons(V,W))!=X| -ssList(W)| -ssList(U)| -ssItem(V)| -ssList(X)|memberP(X,V). % 16.00/16.15 0 [] -frontsegP(cons(U,V),cons(W,X))| -ssList(X)| -ssList(V)| -ssItem(W)| -ssItem(U)|U=W. % 16.00/16.15 0 [] tl(U)!=tl(V)|hd(U)!=hd(V)| -ssList(U)| -ssList(V)|nil=V|U=V|nil=U. % 16.00/16.15 0 [] -frontsegP(U,V)|W!=X| -ssList(V)| -ssList(U)| -ssItem(X)| -ssItem(W)|frontsegP(cons(W,U),cons(X,V)). % 16.00/16.15 0 [] app(app(U,cons(V,W)),cons(V,X))!=Y| -ssList(X)| -ssList(W)| -ssList(U)| -ssItem(V)| -duplicatefreeP(Y)| -ssList(Y). % 16.00/16.15 0 [] app(U,cons(V,cons(W,X)))!=Y| -ssList(X)| -ssList(U)| -ssItem(W)| -ssItem(V)| -e_qualelemsP(Y)| -ssList(Y)|V=W. % 16.00/16.15 0 [] app(app(U,cons(V,W)),cons(X,Y))!=Z| -ssList(Y)| -ssList(W)| -ssList(U)| -ssItem(X)| -ssItem(V)| -strictorderedP(Z)| -ssList(Z)|lt(V,X). % 16.00/16.15 0 [] app(app(U,cons(V,W)),cons(X,Y))!=Z| -ssList(Y)| -ssList(W)| -ssList(U)| -ssItem(X)| -ssItem(V)| -totalorderedP(Z)| -ssList(Z)|le_q(V,X). % 16.00/16.15 0 [] app(app(U,cons(V,W)),cons(X,Y))!=Z| -ssList(Y)| -ssList(W)| -ssList(U)| -ssItem(X)| -ssItem(V)| -strictorderP(Z)| -ssList(Z)|lt(V,X)|lt(X,V). % 16.00/16.15 0 [] app(app(U,cons(V,W)),cons(X,Y))!=Z| -ssList(Y)| -ssList(W)| -ssList(U)| -ssItem(X)| -ssItem(V)| -totalorderP(Z)| -ssList(Z)|le_q(V,X)|le_q(X,V). % 16.00/16.15 0 [] -le_q(U,V)| -le_q(V,U)|app(app(W,cons(U,X)),cons(V,Y))!=Z| -ssList(Y)| -ssList(X)| -ssList(W)| -ssItem(V)| -ssItem(U)| -cyclefreeP(Z)| -ssList(Z). % 16.00/16.15 0 [] ssList(sk1). % 16.00/16.15 0 [] ssList(sk2). % 16.00/16.15 0 [] ssList(sk3). % 16.00/16.15 0 [] ssList(sk4). % 16.00/16.15 0 [] sk2=sk4. % 16.00/16.15 0 [] sk1=sk3. % 16.00/16.15 0 [] -ssItem(A)| -ssItem(B)| -ssList(C)| -ssList(D)| -ssList(E)|app(app(app(app(C,cons(A,nil)),D),cons(B,nil)),E)!=sk2|app(app(app(app(C,cons(B,nil)),D),cons(A,nil)),E)!=sk1| -ssItem(F)| -ssItem(G)| -ssList(H)|app(app(cons(F,nil),cons(G,nil)),H)!=sk4. % 16.00/16.15 0 [] -ssItem(A)| -ssItem(B)| -ssList(C)| -ssList(D)| -ssList(E)|app(app(app(app(C,cons(A,nil)),D),cons(B,nil)),E)!=sk2|app(app(app(app(C,cons(B,nil)),D),cons(A,nil)),E)!=sk1|ssItem(sk11). % 16.00/16.15 0 [] -ssItem(A)| -ssItem(B)| -ssList(C)| -ssList(D)| -ssList(E)|app(app(app(app(C,cons(A,nil)),D),cons(B,nil)),E)!=sk2|app(app(app(app(C,cons(B,nil)),D),cons(A,nil)),E)!=sk1|ssItem(sk12). % 16.00/16.15 0 [] -ssItem(A)| -ssItem(B)| -ssList(C)| -ssList(D)| -ssList(E)|app(app(app(app(C,cons(A,nil)),D),cons(B,nil)),E)!=sk2|app(app(app(app(C,cons(B,nil)),D),cons(A,nil)),E)!=sk1|ssList(sk13). % 16.00/16.15 0 [] -ssItem(A)| -ssItem(B)| -ssList(C)| -ssList(D)| -ssList(E)|app(app(app(app(C,cons(A,nil)),D),cons(B,nil)),E)!=sk2|app(app(app(app(C,cons(B,nil)),D),cons(A,nil)),E)!=sk1|app(app(cons(sk11,nil),cons(sk12,nil)),sk13)=sk2. % 16.00/16.15 0 [] ssItem(sk5)| -ssItem(A)| -ssItem(B)| -ssList(C)|app(app(cons(A,nil),cons(B,nil)),C)!=sk4. % 16.00/16.15 0 [] ssItem(sk6)| -ssItem(A)| -ssItem(B)| -ssList(C)|app(app(cons(A,nil),cons(B,nil)),C)!=sk4. % 16.00/16.15 0 [] ssList(sk7)| -ssItem(A)| -ssItem(B)| -ssList(C)|app(app(cons(A,nil),cons(B,nil)),C)!=sk4. % 16.00/16.15 0 [] app(app(cons(sk5,nil),cons(sk6,nil)),sk7)=sk2| -ssItem(A)| -ssItem(B)| -ssList(C)|app(app(cons(A,nil),cons(B,nil)),C)!=sk4. % 16.00/16.15 0 [] ssItem(sk8)| -ssItem(A)| -ssItem(B)| -ssList(C)|app(app(cons(A,nil),cons(B,nil)),C)!=sk4. % 16.00/16.15 0 [] ssItem(sk9)| -ssItem(A)| -ssItem(B)| -ssList(C)|app(app(cons(A,nil),cons(B,nil)),C)!=sk4. % 16.00/16.15 0 [] ssList(sk10)| -ssItem(A)| -ssItem(B)| -ssList(C)|app(app(cons(A,nil),cons(B,nil)),C)!=sk4. % 16.00/16.15 0 [] app(app(cons(sk8,nil),cons(sk9,nil)),sk10)=sk4| -ssItem(A)| -ssItem(B)| -ssList(C)|app(app(cons(A,nil),cons(B,nil)),C)!=sk4. % 16.00/16.15 0 [] app(app(cons(sk9,nil),cons(sk8,nil)),sk10)=sk3| -ssItem(A)| -ssItem(B)| -ssList(C)|app(app(cons(A,nil),cons(B,nil)),C)!=sk4. % 16.00/16.15 0 [] ssItem(sk5)|ssItem(sk11). % 16.00/16.15 0 [] ssItem(sk6)|ssItem(sk11). % 16.00/16.15 0 [] ssList(sk7)|ssItem(sk11). % 16.00/16.15 0 [] app(app(cons(sk5,nil),cons(sk6,nil)),sk7)=sk2|ssItem(sk11). % 16.00/16.15 0 [] ssItem(sk5)|ssItem(sk12). % 16.00/16.15 0 [] ssItem(sk5)|ssList(sk13). % 16.00/16.15 0 [] ssItem(sk5)|app(app(cons(sk11,nil),cons(sk12,nil)),sk13)=sk2. % 16.00/16.15 0 [] ssItem(sk6)|ssItem(sk12). % 16.00/16.15 0 [] ssList(sk7)|ssItem(sk12). % 16.00/16.15 0 [] app(app(cons(sk5,nil),cons(sk6,nil)),sk7)=sk2|ssItem(sk12). % 16.00/16.15 0 [] ssItem(sk6)|ssList(sk13). % 16.00/16.15 0 [] ssItem(sk6)|app(app(cons(sk11,nil),cons(sk12,nil)),sk13)=sk2. % 16.00/16.15 0 [] ssList(sk7)|ssList(sk13). % 16.00/16.15 0 [] app(app(cons(sk5,nil),cons(sk6,nil)),sk7)=sk2|ssList(sk13). % 16.00/16.15 0 [] ssList(sk7)|app(app(cons(sk11,nil),cons(sk12,nil)),sk13)=sk2. % 16.00/16.15 0 [] app(app(cons(sk5,nil),cons(sk6,nil)),sk7)=sk2|app(app(cons(sk11,nil),cons(sk12,nil)),sk13)=sk2. % 16.00/16.15 0 [] ssItem(sk8)|ssItem(sk11). % 16.00/16.15 0 [] ssItem(sk9)|ssItem(sk11). % 16.00/16.15 0 [] ssList(sk10)|ssItem(sk11). % 16.00/16.15 0 [] app(app(cons(sk8,nil),cons(sk9,nil)),sk10)=sk4|ssItem(sk11). % 16.00/16.15 0 [] app(app(cons(sk9,nil),cons(sk8,nil)),sk10)=sk3|ssItem(sk11). % 16.00/16.15 0 [] ssItem(sk8)|ssItem(sk12). % 16.00/16.15 0 [] ssItem(sk8)|ssList(sk13). % 16.00/16.15 0 [] ssItem(sk8)|app(app(cons(sk11,nil),cons(sk12,nil)),sk13)=sk2. % 16.00/16.15 0 [] ssItem(sk9)|ssItem(sk12). % 16.00/16.15 0 [] ssList(sk10)|ssItem(sk12). % 16.00/16.15 0 [] app(app(cons(sk8,nil),cons(sk9,nil)),sk10)=sk4|ssItem(sk12). % 16.00/16.15 0 [] app(app(cons(sk9,nil),cons(sk8,nil)),sk10)=sk3|ssItem(sk12). % 16.00/16.15 0 [] ssItem(sk9)|ssList(sk13). % 16.00/16.15 0 [] ssItem(sk9)|app(app(cons(sk11,nil),cons(sk12,nil)),sk13)=sk2. % 16.00/16.15 0 [] ssList(sk10)|ssList(sk13). % 16.00/16.15 0 [] app(app(cons(sk8,nil),cons(sk9,nil)),sk10)=sk4|ssList(sk13). % 16.00/16.15 0 [] app(app(cons(sk9,nil),cons(sk8,nil)),sk10)=sk3|ssList(sk13). % 16.00/16.15 0 [] ssList(sk10)|app(app(cons(sk11,nil),cons(sk12,nil)),sk13)=sk2. % 16.00/16.15 0 [] app(app(cons(sk8,nil),cons(sk9,nil)),sk10)=sk4|app(app(cons(sk11,nil),cons(sk12,nil)),sk13)=sk2. % 16.00/16.15 0 [] app(app(cons(sk9,nil),cons(sk8,nil)),sk10)=sk3|app(app(cons(sk11,nil),cons(sk12,nil)),sk13)=sk2. % 16.00/16.15 end_of_list. % 16.00/16.15 % 16.00/16.15 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=11. % 16.00/16.15 % 16.00/16.15 This ia a non-Horn set with equality. The strategy will be % 16.00/16.15 Knuth-Bendix, ordered hyper_res, factoring, and unit % 16.00/16.15 deletion, with positive clauses in sos and nonpositive % 16.00/16.15 clauses in usable. % 16.00/16.15 % 16.00/16.15 dependent: set(knuth_bendix). % 16.00/16.15 dependent: set(anl_eq). % 16.00/16.15 dependent: set(para_from). % 16.00/16.15 dependent: set(para_into). % 16.00/16.15 dependent: clear(para_from_right). % 16.00/16.15 dependent: clear(para_into_right). % 16.00/16.15 dependent: set(para_from_vars). % 16.00/16.15 dependent: set(eq_units_both_ways). % 16.00/16.15 dependent: set(dynamic_demod_all). % 16.00/16.15 dependent: set(dynamic_demod). % 16.00/16.15 dependent: set(order_eq). % 16.00/16.15 dependent: set(back_demod). % 16.00/16.15 dependent: set(lrpo). % 16.00/16.15 dependent: set(hyper_res). % 16.00/16.15 dependent: set(unit_deletion). % 16.00/16.15 dependent: set(factor). % 16.00/16.15 % 16.00/16.15 ------------> process usable: % 16.00/16.15 ** KEPT (pick-wt=2): 1 [] -singletonP(nil). % 16.00/16.15 ** KEPT (pick-wt=3): 2 [] skac3!=skac2. % 16.00/16.15 ** KEPT (pick-wt=5): 3 [] -ssItem(A)|ge_q(A,A). % 16.00/16.15 ** KEPT (pick-wt=5): 4 [] -ssList(A)|segmentP(A,nil). % 16.00/16.15 ** KEPT (pick-wt=5): 5 [] -ssList(A)|segmentP(A,A). % 16.00/16.15 ** KEPT (pick-wt=5): 6 [] -ssList(A)|rearsegP(A,nil). % 16.00/16.15 ** KEPT (pick-wt=5): 7 [] -ssList(A)|rearsegP(A,A). % 16.00/16.15 ** KEPT (pick-wt=5): 8 [] -ssList(A)|frontsegP(A,nil). % 16.00/16.15 ** KEPT (pick-wt=5): 9 [] -ssList(A)|frontsegP(A,A). % 16.00/16.15 ** KEPT (pick-wt=5): 10 [] -ssItem(A)|le_q(A,A). % 16.00/16.15 ** KEPT (pick-wt=5): 11 [] -lt(A,A)| -ssItem(A). % 16.00/16.15 ** KEPT (pick-wt=6): 12 [] -ssItem(A)|e_qualelemsP(cons(A,nil)). % 16.00/16.15 ** KEPT (pick-wt=6): 13 [] -ssItem(A)|duplicatefreeP(cons(A,nil)). % 16.00/16.15 ** KEPT (pick-wt=6): 14 [] -ssItem(A)|strictorderedP(cons(A,nil)). % 16.00/16.15 ** KEPT (pick-wt=6): 15 [] -ssItem(A)|totalorderedP(cons(A,nil)). % 16.00/16.15 ** KEPT (pick-wt=6): 16 [] -ssItem(A)|strictorderP(cons(A,nil)). % 16.00/16.15 ** KEPT (pick-wt=6): 17 [] -ssItem(A)|totalorderP(cons(A,nil)). % 16.00/16.15 ** KEPT (pick-wt=6): 18 [] -ssItem(A)|cyclefreeP(cons(A,nil)). % 16.00/16.15 ** KEPT (pick-wt=5): 19 [] -memberP(nil,A)| -ssItem(A). % 16.00/16.15 ** KEPT (pick-wt=6): 20 [] -ssList(A)|duplicatefreeP(A)|ssItem(B). % 16.00/16.15 ** KEPT (pick-wt=7): 21 [] -ssList(A)|app(A,nil)=A. % 16.00/16.15 ** KEPT (pick-wt=7): 22 [] -ssList(A)|app(nil,A)=A. % 16.00/16.15 ** KEPT (pick-wt=8): 23 [] -ssList(A)|ssList(tl(A))|nil=A. % 16.00/16.15 ** KEPT (pick-wt=8): 24 [] -ssList(A)|ssItem(hd(A))|nil=A. % 16.00/16.15 Following clause subsumed by 23 during input processing: 0 [] -ssList(A)|ssList(tl(A))|nil=A. % 16.00/16.15 Following clause subsumed by 24 during input processing: 0 [] -ssList(A)|ssItem(hd(A))|nil=A. % 16.00/16.15 ** KEPT (pick-wt=8): 25 [] nil!=A| -ssList(A)|segmentP(nil,A). % 16.00/16.15 ** KEPT (pick-wt=8): 26 [] -segmentP(nil,A)| -ssList(A)|nil=A. % 16.00/16.15 ** KEPT (pick-wt=8): 27 [] nil!=A| -ssList(A)|rearsegP(nil,A). % 16.00/16.15 ** KEPT (pick-wt=8): 28 [] -rearsegP(nil,A)| -ssList(A)|nil=A. % 16.00/16.15 ** KEPT (pick-wt=8): 29 [] nil!=A| -ssList(A)|frontsegP(nil,A). % 16.00/16.15 ** KEPT (pick-wt=8): 30 [] -frontsegP(nil,A)| -ssList(A)|nil=A. % 16.00/16.15 ** KEPT (pick-wt=8): 31 [] -ssList(A)| -ssList(B)|ssList(app(B,A)). % 16.00/16.15 ** KEPT (pick-wt=8): 32 [] -ssItem(A)| -ssList(B)|ssList(cons(A,B)). % 16.00/16.15 ** KEPT (pick-wt=9): 33 [] -ssList(A)|cyclefreeP(A)|le_q(skaf50(A),skaf49(A)). % 16.00/16.15 ** KEPT (pick-wt=9): 34 [] -ssList(A)|cyclefreeP(A)|le_q(skaf49(A),skaf50(A)). % 16.00/16.15 ** KEPT (pick-wt=9): 35 [] skaf79(A)!=skaf78(A)| -ssList(A)|e_qualelemsP(A). % 16.00/16.15 ** KEPT (pick-wt=9): 36 [] -lt(skaf69(A),skaf70(A))| -ssList(A)|strictorderedP(A). % 16.00/16.15 ** KEPT (pick-wt=9): 37 [] -le_q(skaf64(A),skaf65(A))| -ssList(A)|totalorderedP(A). % 16.00/16.15 ** KEPT (pick-wt=9): 38 [] -lt(skaf60(A),skaf59(A))| -ssList(A)|strictorderP(A). % 16.00/16.15 ** KEPT (pick-wt=9): 39 [] -lt(skaf59(A),skaf60(A))| -ssList(A)|strictorderP(A). % 16.00/16.15 ** KEPT (pick-wt=9): 40 [] -le_q(skaf55(A),skaf54(A))| -ssList(A)|totalorderP(A). % 16.00/16.15 ** KEPT (pick-wt=9): 41 [] -le_q(skaf54(A),skaf55(A))| -ssList(A)|totalorderP(A). % 16.00/16.15 ** KEPT (pick-wt=10): 42 [] -ssItem(A)| -ssList(B)|tl(cons(A,B))=B. % 16.00/16.15 ** KEPT (pick-wt=10): 43 [] -ssItem(A)| -ssList(B)|hd(cons(A,B))=A. % 16.00/16.15 ** KEPT (pick-wt=9): 44 [] cons(A,B)!=nil| -ssItem(A)| -ssList(B). % 16.00/16.15 ** KEPT (pick-wt=9): 45 [] cons(A,B)!=B| -ssItem(A)| -ssList(B). % 16.00/16.15 ** KEPT (pick-wt=10): 46 [] -ssList(A)| -ssList(B)|ne_q(B,A)|B=A. % 16.00/16.15 ** KEPT (pick-wt=10): 47 [] -singletonP(A)| -ssList(A)|cons(skaf44(A),nil)=A. % 16.00/16.15 ** KEPT (pick-wt=10): 48 [] -ssItem(A)| -ssItem(B)|ne_q(B,A)|B=A. % 16.00/16.15 ** KEPT (pick-wt=10): 49 [] -lt(A,B)| -ssItem(B)| -ssItem(A)|le_q(A,B). % 16.00/16.15 ** KEPT (pick-wt=12): 50 [] -ssList(A)|cons(hd(A),tl(A))=A|nil=A. % 16.00/16.15 ** KEPT (pick-wt=10): 51 [] -gt(A,B)| -ssItem(B)| -ssItem(A)|lt(B,A). % 16.00/16.15 ** KEPT (pick-wt=10): 52 [] -lt(A,B)| -ssItem(A)| -ssItem(B)|gt(B,A). % 16.00/16.15 ** KEPT (pick-wt=10): 53 [] -ge_q(A,B)| -ssItem(B)| -ssItem(A)|le_q(B,A). % 16.00/16.15 ** KEPT (pick-wt=10): 54 [] -le_q(A,B)| -ssItem(A)| -ssItem(B)|ge_q(B,A). % 16.00/16.15 ** KEPT (pick-wt=12): 55 [] -ssList(A)|cons(skaf83(A),skaf82(A))=A|nil=A. % 16.00/16.15 ** KEPT (pick-wt=10): 56 [] -gt(A,B)| -gt(B,A)| -ssItem(A)| -ssItem(B). % 16.00/16.15 ** KEPT (pick-wt=10): 57 [] A!=B| -lt(A,B)| -ssItem(B)| -ssItem(A). % 16.00/16.15 ** KEPT (pick-wt=11): 58 [] nil!=A| -ssList(A)| -ssItem(B)|strictorderedP(cons(B,A)). % 16.00/16.15 ** KEPT (pick-wt=11): 59 [] nil!=A| -ssList(A)| -ssItem(B)|totalorderedP(cons(B,A)). % 16.00/16.15 ** KEPT (pick-wt=10): 60 [] -lt(A,B)| -lt(B,A)| -ssItem(A)| -ssItem(B). % 16.00/16.15 ** KEPT (pick-wt=10): 61 [] A!=B| -ne_q(A,B)| -ssList(B)| -ssList(A). % 16.00/16.15 ** KEPT (pick-wt=11): 62 [] cons(A,nil)!=B| -ssItem(A)| -ssList(B)|singletonP(B). % 16.00/16.15 ** KEPT (pick-wt=10): 63 [] A!=B| -ne_q(A,B)| -ssItem(B)| -ssItem(A). % 16.00/16.15 ** KEPT (pick-wt=12): 64 [] app(A,B)!=nil| -ssList(B)| -ssList(A)|nil=A. % 16.00/16.15 ** KEPT (pick-wt=12): 65 [] app(A,B)!=nil| -ssList(B)| -ssList(A)|nil=B. % 16.00/16.15 ** KEPT (pick-wt=13): 66 [] -ssItem(A)| -ssList(B)|app(cons(A,nil),B)=cons(A,B). % 16.00/16.15 ** KEPT (pick-wt=13): 67 [] -le_q(A,B)| -ssItem(B)| -ssItem(A)|lt(A,B)|A=B. % 16.00/16.15 Following clause subsumed by 67 during input processing: 0 [] -le_q(A,B)| -ssItem(B)| -ssItem(A)|lt(A,B)|A=B. % 16.00/16.15 ** KEPT (pick-wt=14): 68 [] -ssList(A)| -ssList(B)|nil=B|hd(app(B,A))=hd(B). % 16.00/16.15 ** KEPT (pick-wt=13): 69 [] -strictorderedP(cons(A,B))| -ssList(B)| -ssItem(A)|strictorderedP(B)|nil=B. % 16.00/16.15 ** KEPT (pick-wt=13): 70 [] -totalorderedP(cons(A,B))| -ssList(B)| -ssItem(A)|totalorderedP(B)|nil=B. % 16.00/16.15 ** KEPT (pick-wt=13): 71 [] -ge_q(A,B)| -ge_q(B,A)| -ssItem(A)| -ssItem(B)|B=A. % 16.00/16.15 ** KEPT (pick-wt=13): 72 [] -segmentP(A,B)| -segmentP(B,A)| -ssList(A)| -ssList(B)|B=A. % 16.00/16.15 ** KEPT (pick-wt=13): 73 [] -rearsegP(A,B)| -rearsegP(B,A)| -ssList(A)| -ssList(B)|B=A. % 16.00/16.15 ** KEPT (pick-wt=13): 74 [] -frontsegP(A,B)| -frontsegP(B,A)| -ssList(A)| -ssList(B)|B=A. % 16.00/16.15 ** KEPT (pick-wt=13): 75 [] -le_q(A,B)| -le_q(B,A)| -ssItem(A)| -ssItem(B)|B=A. % 16.00/16.15 ** KEPT (pick-wt=14): 76 [] -rearsegP(A,B)| -ssList(B)| -ssList(A)|app(skaf46(A,B),B)=A. % 16.00/16.15 ** KEPT (pick-wt=14): 77 [] -frontsegP(A,B)| -ssList(B)| -ssList(A)|app(B,skaf45(A,B))=A. % 16.00/16.15 ** KEPT (pick-wt=16): 78 [] -ssList(A)| -ssList(B)|nil=B|tl(app(B,A))=app(tl(B),A). % 16.00/16.15 ** KEPT (pick-wt=15): 79 [] -strictorderedP(cons(A,B))| -ssList(B)| -ssItem(A)|lt(A,hd(B))|nil=B. % 16.00/16.15 ** KEPT (pick-wt=15): 80 [] -totalorderedP(cons(A,B))| -ssList(B)| -ssItem(A)|le_q(A,hd(B))|nil=B. % 16.00/16.15 ** KEPT (pick-wt=14): 81 [] -rearsegP(A,B)| -ssList(C)| -ssList(B)| -ssList(A)|rearsegP(app(C,A),B). % 16.00/16.15 ** KEPT (pick-wt=14): 82 [] -frontsegP(A,B)| -ssList(C)| -ssList(B)| -ssList(A)|frontsegP(app(A,C),B). % 16.00/16.15 ** KEPT (pick-wt=14): 83 [] A!=B| -ssList(C)| -ssItem(B)| -ssItem(A)|memberP(cons(B,C),A). % 16.00/16.15 ** KEPT (pick-wt=14): 84 [] -memberP(A,B)| -ssList(A)| -ssItem(C)| -ssItem(B)|memberP(cons(C,A),B). % 16.00/16.15 ** KEPT (pick-wt=14): 85 [] -memberP(A,B)| -ssList(C)| -ssList(A)| -ssItem(B)|memberP(app(A,C),B). % 16.00/16.15 ** KEPT (pick-wt=14): 86 [] -memberP(A,B)| -ssList(A)| -ssList(C)| -ssItem(B)|memberP(app(C,A),B). % 16.00/16.15 ** KEPT (pick-wt=17): 87 [] -ssList(A)|e_qualelemsP(A)|app(skaf80(A),cons(skaf78(A),cons(skaf79(A),skaf81(A))))=A. % 16.00/16.15 ** KEPT (pick-wt=14): 88 [] app(A,B)!=C| -ssList(A)| -ssList(B)| -ssList(C)|rearsegP(C,B). % 16.00/16.15 ** KEPT (pick-wt=14): 89 [] app(A,B)!=C| -ssList(B)| -ssList(A)| -ssList(C)|frontsegP(C,A). % 16.00/16.15 ** KEPT (pick-wt=15): 90 [] nil!=A|nil!=B| -ssList(B)| -ssList(A)|app(A,B)=nil. % 16.00/16.15 ** KEPT (pick-wt=15): 91 [] -gt(A,B)| -gt(B,C)| -ssItem(C)| -ssItem(B)| -ssItem(A)|gt(A,C). % 16.00/16.15 ** KEPT (pick-wt=15): 92 [] -le_q(A,B)| -lt(B,C)| -ssItem(C)| -ssItem(B)| -ssItem(A)|lt(A,C). % 16.00/16.15 ** KEPT (pick-wt=15): 93 [] -ge_q(A,B)| -ge_q(B,C)| -ssItem(C)| -ssItem(B)| -ssItem(A)|ge_q(A,C). % 16.00/16.15 ** KEPT (pick-wt=17): 94 [] -ssList(A)| -ssList(B)| -ssList(C)|app(app(C,B),A)=app(C,app(B,A)). % 16.00/16.15 ** KEPT (pick-wt=16): 95 [] app(A,B)!=app(A,C)| -ssList(B)| -ssList(A)| -ssList(C)|B=C. % 16.00/16.15 ** KEPT (pick-wt=16): 96 [] app(A,B)!=app(C,B)| -ssList(A)| -ssList(B)| -ssList(C)|A=C. % 16.00/16.15 ** KEPT (pick-wt=15): 97 [] -segmentP(A,B)| -segmentP(B,C)| -ssList(C)| -ssList(B)| -ssList(A)|segmentP(A,C). % 16.00/16.15 ** KEPT (pick-wt=15): 98 [] -rearsegP(A,B)| -rearsegP(B,C)| -ssList(C)| -ssList(B)| -ssList(A)|rearsegP(A,C). % 16.00/16.15 ** KEPT (pick-wt=15): 99 [] -frontsegP(A,B)| -frontsegP(B,C)| -ssList(C)| -ssList(B)| -ssList(A)|frontsegP(A,C). % 16.00/16.15 ** KEPT (pick-wt=15): 100 [] -lt(A,B)| -lt(B,C)| -ssItem(C)| -ssItem(B)| -ssItem(A)|lt(A,C). % 16.00/16.15 ** KEPT (pick-wt=15): 101 [] -le_q(A,B)| -le_q(B,C)| -ssItem(C)| -ssItem(B)| -ssItem(A)|le_q(A,C). % 16.00/16.15 ** KEPT (pick-wt=17): 102 [] -ssItem(A)| -ssList(B)| -ssList(C)|cons(A,app(B,C))=app(cons(A,B),C). % 16.00/16.15 ** KEPT (pick-wt=17): 103 [] -memberP(app(A,B),C)| -ssList(B)| -ssList(A)| -ssItem(C)|memberP(B,C)|memberP(A,C). % 16.00/16.15 ** KEPT (pick-wt=17): 104 [] -le_q(A,hd(B))| -totalorderedP(B)| -ssList(B)| -ssItem(A)|totalorderedP(cons(A,B))|nil=B. % 16.00/16.15 ** KEPT (pick-wt=17): 105 [] -lt(A,hd(B))| -strictorderedP(B)| -ssList(B)| -ssItem(A)|strictorderedP(cons(A,B))|nil=B. % 16.00/16.15 ** KEPT (pick-wt=17): 106 [] -memberP(cons(A,B),C)| -ssList(B)| -ssItem(A)| -ssItem(C)|memberP(B,C)|C=A. % 16.00/16.15 ** KEPT (pick-wt=20): 107 [] -ssList(A)|duplicatefreeP(A)|app(app(skaf75(A),cons(skaf74(A),skaf76(A))),cons(skaf74(A),skaf77(A)))=A. % 16.00/16.15 ** KEPT (pick-wt=20): 108 [] -ssList(A)|strictorderedP(A)|app(app(skaf71(A),cons(skaf69(A),skaf72(A))),cons(skaf70(A),skaf73(A)))=A. % 16.00/16.15 ** KEPT (pick-wt=20): 109 [] -ssList(A)|totalorderedP(A)|app(app(skaf66(A),cons(skaf64(A),skaf67(A))),cons(skaf65(A),skaf68(A)))=A. % 16.00/16.15 ** KEPT (pick-wt=20): 110 [] -ssList(A)|strictorderP(A)|app(app(skaf61(A),cons(skaf59(A),skaf62(A))),cons(skaf60(A),skaf63(A)))=A. % 16.00/16.15 ** KEPT (pick-wt=20): 111 [] -ssList(A)|totalorderP(A)|app(app(skaf56(A),cons(skaf54(A),skaf57(A))),cons(skaf55(A),skaf58(A)))=A. % 16.00/16.15 ** KEPT (pick-wt=20): 112 [] -ssList(A)|cyclefreeP(A)|app(app(skaf51(A),cons(skaf49(A),skaf52(A))),cons(skaf50(A),skaf53(A)))=A. % 17.12/17.24 ** KEPT (pick-wt=18): 113 [] -segmentP(A,B)| -ssList(B)| -ssList(A)|app(app(skaf47(A,B),B),skaf48(B,A))=A. % 17.12/17.24 ** KEPT (pick-wt=18): 114 [] -memberP(A,B)| -ssItem(B)| -ssList(A)|app(skaf42(A,B),cons(B,skaf43(B,A)))=A. % 17.12/17.24 ** KEPT (pick-wt=18): 115 [] cons(A,B)!=cons(C,D)| -ssItem(C)| -ssItem(A)| -ssList(D)| -ssList(B)|A=C. % 17.12/17.24 ** KEPT (pick-wt=18): 116 [] cons(A,B)!=cons(C,D)| -ssItem(C)| -ssItem(A)| -ssList(D)| -ssList(B)|D=B. % 17.12/17.24 ** KEPT (pick-wt=18): 117 [] -segmentP(A,B)| -ssList(C)| -ssList(D)| -ssList(B)| -ssList(A)|segmentP(app(app(D,A),C),B). % 17.12/17.24 ** KEPT (pick-wt=18): 118 [] app(app(A,B),C)!=D| -ssList(C)| -ssList(A)| -ssList(B)| -ssList(D)|segmentP(D,B). % 17.12/17.24 ** KEPT (pick-wt=18): 119 [] -frontsegP(cons(A,B),cons(C,D))| -ssList(D)| -ssList(B)| -ssItem(C)| -ssItem(A)|frontsegP(B,D). % 17.12/17.24 ** KEPT (pick-wt=18): 120 [] app(A,cons(B,C))!=D| -ssList(C)| -ssList(A)| -ssItem(B)| -ssList(D)|memberP(D,B). % 17.12/17.24 ** KEPT (pick-wt=18): 121 [] -frontsegP(cons(A,B),cons(C,D))| -ssList(D)| -ssList(B)| -ssItem(C)| -ssItem(A)|A=C. % 17.12/17.24 ** KEPT (pick-wt=23): 122 [] tl(A)!=tl(B)|hd(A)!=hd(B)| -ssList(A)| -ssList(B)|nil=B|A=B|nil=A. % 17.12/17.24 ** KEPT (pick-wt=21): 123 [] -frontsegP(A,B)|C!=D| -ssList(B)| -ssList(A)| -ssItem(D)| -ssItem(C)|frontsegP(cons(C,A),cons(D,B)). % 17.12/17.24 ** KEPT (pick-wt=23): 124 [] app(app(A,cons(B,C)),cons(B,D))!=E| -ssList(D)| -ssList(C)| -ssList(A)| -ssItem(B)| -duplicatefreeP(E)| -ssList(E). % 17.12/17.24 ** KEPT (pick-wt=24): 125 [] app(A,cons(B,cons(C,D)))!=E| -ssList(D)| -ssList(A)| -ssItem(C)| -ssItem(B)| -e_qualelemsP(E)| -ssList(E)|B=C. % 17.12/17.24 ** KEPT (pick-wt=28): 126 [] app(app(A,cons(B,C)),cons(D,E))!=F| -ssList(E)| -ssList(C)| -ssList(A)| -ssItem(D)| -ssItem(B)| -strictorderedP(F)| -ssList(F)|lt(B,D). % 17.12/17.24 ** KEPT (pick-wt=28): 127 [] app(app(A,cons(B,C)),cons(D,E))!=F| -ssList(E)| -ssList(C)| -ssList(A)| -ssItem(D)| -ssItem(B)| -totalorderedP(F)| -ssList(F)|le_q(B,D). % 17.12/17.24 ** KEPT (pick-wt=31): 128 [] app(app(A,cons(B,C)),cons(D,E))!=F| -ssList(E)| -ssList(C)| -ssList(A)| -ssItem(D)| -ssItem(B)| -strictorderP(F)| -ssList(F)|lt(B,D)|lt(D,B). % 17.12/17.24 ** KEPT (pick-wt=31): 129 [] app(app(A,cons(B,C)),cons(D,E))!=F| -ssList(E)| -ssList(C)| -ssList(A)| -ssItem(D)| -ssItem(B)| -totalorderP(F)| -ssList(F)|le_q(B,D)|le_q(D,B). % 17.12/17.24 ** KEPT (pick-wt=31): 130 [] -le_q(A,B)| -le_q(B,A)|app(app(C,cons(A,D)),cons(B,E))!=F| -ssList(E)| -ssList(D)| -ssList(C)| -ssItem(B)| -ssItem(A)| -cyclefreeP(F)| -ssList(F). % 17.12/17.24 ** KEPT (pick-wt=57): 131 [] -ssItem(A)| -ssItem(B)| -ssList(C)| -ssList(D)| -ssList(E)|app(app(app(app(C,cons(A,nil)),D),cons(B,nil)),E)!=sk2|app(app(app(app(C,cons(B,nil)),D),cons(A,nil)),E)!=sk1| -ssItem(F)| -ssItem(G)| -ssList(H)|app(app(cons(F,nil),cons(G,nil)),H)!=sk4. % 17.12/17.24 ** KEPT (pick-wt=42): 132 [] -ssItem(A)| -ssItem(B)| -ssList(C)| -ssList(D)| -ssList(E)|app(app(app(app(C,cons(A,nil)),D),cons(B,nil)),E)!=sk2|app(app(app(app(C,cons(B,nil)),D),cons(A,nil)),E)!=sk1|ssItem(sk11). % 17.12/17.24 ** KEPT (pick-wt=42): 133 [] -ssItem(A)| -ssItem(B)| -ssList(C)| -ssList(D)| -ssList(E)|app(app(app(app(C,cons(A,nil)),D),cons(B,nil)),E)!=sk2|app(app(app(app(C,cons(B,nil)),D),cons(A,nil)),E)!=sk1|ssItem(sk12). % 17.12/17.24 ** KEPT (pick-wt=42): 134 [] -ssItem(A)| -ssItem(B)| -ssList(C)| -ssList(D)| -ssList(E)|app(app(app(app(C,cons(A,nil)),D),cons(B,nil)),E)!=sk2|app(app(app(app(C,cons(B,nil)),D),cons(A,nil)),E)!=sk1|ssList(sk13). % 17.12/17.24 ** KEPT (pick-wt=51): 135 [] -ssItem(A)| -ssItem(B)| -ssList(C)| -ssList(D)| -ssList(E)|app(app(app(app(C,cons(A,nil)),D),cons(B,nil)),E)!=sk2|app(app(app(app(C,cons(B,nil)),D),cons(A,nil)),E)!=sk1|app(app(cons(sk11,nil),cons(sk12,nil)),sk13)=sk2. % 17.12/17.24 ** KEPT (pick-wt=19): 136 [] ssItem(sk5)| -ssItem(A)| -ssItem(B)| -ssList(C)|app(app(cons(A,nil),cons(B,nil)),C)!=sk4. % 17.12/17.24 ** KEPT (pick-wt=19): 137 [] ssItem(sk6)| -ssItem(A)| -ssItem(B)| -ssList(C)|app(app(cons(A,nil),cons(B,nil)),C)!=sk4. % 17.12/17.24 ** KEPT (pick-wt=19): 138 [] ssList(sk7)| -ssItem(A)| -ssItem(B)| -ssList(C)|app(app(cons(A,nil),cons(B,nil)),C)!=sk4. % 17.12/17.24 ** KEPT (pick-wt=28): 139 [] app(app(cons(sk5,nil),cons(sk6,nil)),sk7)=sk2| -ssItem(A)| -ssItem(B)| -ssList(C)|app(app(cons(A,nil),cons(B,nil)),C)!=sk4. % 17.12/17.24 ** KEPT (pick-wt=19): 140 [] ssItem(sk8)| -ssItem(A)| -ssItem(B)| -ssList(C)|app(app(cons(A,nil),cons(B,nil)),C)!=sk4. % 17.12/17.26 ** KEPT (pick-wt=19): 141 [] ssItem(sk9)| -ssItem(A)| -ssItem(B)| -ssList(C)|app(app(cons(A,nil),cons(B,nil)),C)!=sk4. % 17.12/17.26 ** KEPT (pick-wt=19): 142 [] ssList(sk10)| -ssItem(A)| -ssItem(B)| -ssList(C)|app(app(cons(A,nil),cons(B,nil)),C)!=sk4. % 17.12/17.26 ** KEPT (pick-wt=28): 143 [] app(app(cons(sk8,nil),cons(sk9,nil)),sk10)=sk4| -ssItem(A)| -ssItem(B)| -ssList(C)|app(app(cons(A,nil),cons(B,nil)),C)!=sk4. % 17.12/17.26 ** KEPT (pick-wt=28): 144 [] app(app(cons(sk9,nil),cons(sk8,nil)),sk10)=sk3| -ssItem(A)| -ssItem(B)| -ssList(C)|app(app(cons(A,nil),cons(B,nil)),C)!=sk4. % 17.12/17.26 149 back subsumes 148. % 17.12/17.26 159 back subsumes 153. % 17.12/17.26 % 17.12/17.26 ------------> process sos: % 17.12/17.26 ** KEPT (pick-wt=3): 645 [] A=A. % 17.12/17.26 ** KEPT (pick-wt=2): 646 [] e_qualelemsP(nil). % 17.12/17.26 ** KEPT (pick-wt=2): 647 [] duplicatefreeP(nil). % 17.12/17.26 ** KEPT (pick-wt=2): 648 [] strictorderedP(nil). % 17.12/17.26 ** KEPT (pick-wt=2): 649 [] totalorderedP(nil). % 17.12/17.26 ** KEPT (pick-wt=2): 650 [] strictorderP(nil). % 17.12/17.26 ** KEPT (pick-wt=2): 651 [] totalorderP(nil). % 17.12/17.26 ** KEPT (pick-wt=2): 652 [] cyclefreeP(nil). % 17.12/17.26 ** KEPT (pick-wt=2): 653 [] ssList(nil). % 17.12/17.26 ** KEPT (pick-wt=2): 654 [] ssItem(skac3). % 17.12/17.26 ** KEPT (pick-wt=2): 655 [] ssItem(skac2). % 17.12/17.26 ** KEPT (pick-wt=3): 656 [] ssItem(skaf83(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 657 [] ssList(skaf82(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 658 [] ssList(skaf81(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 659 [] ssList(skaf80(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 660 [] ssItem(skaf79(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 661 [] ssItem(skaf78(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 662 [] ssList(skaf77(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 663 [] ssList(skaf76(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 664 [] ssList(skaf75(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 665 [] ssItem(skaf74(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 666 [] ssList(skaf73(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 667 [] ssList(skaf72(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 668 [] ssList(skaf71(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 669 [] ssItem(skaf70(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 670 [] ssItem(skaf69(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 671 [] ssList(skaf68(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 672 [] ssList(skaf67(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 673 [] ssList(skaf66(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 674 [] ssItem(skaf65(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 675 [] ssItem(skaf64(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 676 [] ssList(skaf63(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 677 [] ssList(skaf62(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 678 [] ssList(skaf61(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 679 [] ssItem(skaf60(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 680 [] ssItem(skaf59(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 681 [] ssList(skaf58(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 682 [] ssList(skaf57(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 683 [] ssList(skaf56(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 684 [] ssItem(skaf55(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 685 [] ssItem(skaf54(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 686 [] ssList(skaf53(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 687 [] ssList(skaf52(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 688 [] ssList(skaf51(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 689 [] ssItem(skaf50(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 690 [] ssItem(skaf49(A)). % 17.12/17.26 ** KEPT (pick-wt=3): 691 [] ssItem(skaf44(A)). % 17.12/17.26 ** KEPT (pick-wt=4): 692 [] ssList(skaf48(A,B)). % 17.12/17.26 ** KEPT (pick-wt=4): 693 [] ssList(skaf47(A,B)). % 17.12/17.26 ** KEPT (pick-wt=4): 694 [] ssList(skaf46(A,B)). % 17.12/17.26 ** KEPT (pick-wt=4): 695 [] ssList(skaf45(A,B)). % 17.12/17.26 ** KEPT (pick-wt=4): 696 [] ssList(skaf43(A,B)). % 17.12/17.26 ** KEPT (pick-wt=4): 697 [] ssList(skaf42(A,B)). % 17.12/17.26 ** KEPT (pick-wt=2): 698 [] ssList(sk1). % 17.12/17.26 ** KEPT (pick-wt=2): 699 [] ssList(sk2). % 17.12/17.26 ** KEPT (pick-wt=2): 700 [] ssList(sk3). % 17.12/17.26 ** KEPT (pick-wt=2): 701 [] ssList(sk4). % 17.12/17.26 ** KEPT (pick-wt=3): 703 [copy,702,flip.1] sk4=sk2. % 17.12/17.26 ---> New Demodulator: 704 [new_demod,703] sk4=sk2. % 17.12/17.26 ** KEPT (pick-wt=3): 706 [copy,705,flip.1] sk3=sk1. % 17.12/17.26 ---> New Demodulator: 707 [new_demod,706] sk3=sk1. % 17.12/17.26 ** KEPT (pick-wt=4): 708 [] ssItem(sk5)|ssItem(sk11). % 17.12/17.26 ** KEPT (pick-wt=4): 709 [] ssItem(sk6)|ssItem(sk11). % 17.12/17.26 ** KEPT (pick-wt=4): 710 [] ssList(sk7)|ssItem(sk11). % 17.12/17.26 ** KEPT (pick-wt=13): 711 [] app(app(cons(sk5,nil),cons(sk6,nil)),sk7)=sk2|ssItem(sk11). % 17.12/17.26 ** KEPT (pick-wt=4): 712 [] ssItem(sk5)|ssItem(sk12). % 17.12/17.26 ** KEPT (pick-wt=4): 713 [] ssItem(sk5)|ssList(sk13). % 17.12/17.26 ** KEPT (pick-wt=13): 714 [] ssItem(sk5)|app(app(cons(sk11,nil),cons(sk12,nil)),sk13)=sk2. % 17.12/17.26 ** KEPT (pick-wt=4): 715 [] ssItem(sk6)|ssItem(sk12). % 17.12/17.26 ** KEPT (pick-wt=4): 716 [] ssList(sk7)|ssItem(sk12). % 17.33/17.43 ** KEPT (pick-wt=13): 717 [] app(app(cons(sk5,nil),cons(sk6,nil)),sk7)=sk2|ssItem(sk12). % 17.33/17.43 ** KEPT (pick-wt=4): 718 [] ssItem(sk6)|ssList(sk13). % 17.33/17.43 ** KEPT (pick-wt=13): 719 [] ssItem(sk6)|app(app(cons(sk11,nil),cons(sk12,nil)),sk13)=sk2. % 17.33/17.43 ** KEPT (pick-wt=4): 720 [] ssList(sk7)|ssList(sk13). % 17.33/17.43 ** KEPT (pick-wt=13): 721 [] app(app(cons(sk5,nil),cons(sk6,nil)),sk7)=sk2|ssList(sk13). % 17.33/17.43 ** KEPT (pick-wt=13): 722 [] ssList(sk7)|app(app(cons(sk11,nil),cons(sk12,nil)),sk13)=sk2. % 17.33/17.43 ** KEPT (pick-wt=22): 723 [] app(app(cons(sk5,nil),cons(sk6,nil)),sk7)=sk2|app(app(cons(sk11,nil),cons(sk12,nil)),sk13)=sk2. % 17.33/17.43 ** KEPT (pick-wt=4): 724 [] ssItem(sk8)|ssItem(sk11). % 17.33/17.43 ** KEPT (pick-wt=4): 725 [] ssItem(sk9)|ssItem(sk11). % 17.33/17.43 ** KEPT (pick-wt=4): 726 [] ssList(sk10)|ssItem(sk11). % 17.33/17.43 ** KEPT (pick-wt=13): 728 [copy,727,demod,704] app(app(cons(sk8,nil),cons(sk9,nil)),sk10)=sk2|ssItem(sk11). % 17.33/17.43 ** KEPT (pick-wt=13): 730 [copy,729,demod,707] app(app(cons(sk9,nil),cons(sk8,nil)),sk10)=sk1|ssItem(sk11). % 17.33/17.43 ** KEPT (pick-wt=4): 731 [] ssItem(sk8)|ssItem(sk12). % 17.33/17.43 ** KEPT (pick-wt=4): 732 [] ssItem(sk8)|ssList(sk13). % 17.33/17.43 ** KEPT (pick-wt=13): 733 [] ssItem(sk8)|app(app(cons(sk11,nil),cons(sk12,nil)),sk13)=sk2. % 17.33/17.43 ** KEPT (pick-wt=4): 734 [] ssItem(sk9)|ssItem(sk12). % 17.33/17.43 ** KEPT (pick-wt=4): 735 [] ssList(sk10)|ssItem(sk12). % 17.33/17.43 ** KEPT (pick-wt=13): 737 [copy,736,demod,704] app(app(cons(sk8,nil),cons(sk9,nil)),sk10)=sk2|ssItem(sk12). % 17.33/17.43 ** KEPT (pick-wt=13): 739 [copy,738,demod,707] app(app(cons(sk9,nil),cons(sk8,nil)),sk10)=sk1|ssItem(sk12). % 17.33/17.43 ** KEPT (pick-wt=4): 740 [] ssItem(sk9)|ssList(sk13). % 17.33/17.43 ** KEPT (pick-wt=13): 741 [] ssItem(sk9)|app(app(cons(sk11,nil),cons(sk12,nil)),sk13)=sk2. % 17.33/17.43 ** KEPT (pick-wt=4): 742 [] ssList(sk10)|ssList(sk13). % 17.33/17.43 ** KEPT (pick-wt=13): 744 [copy,743,demod,704] app(app(cons(sk8,nil),cons(sk9,nil)),sk10)=sk2|ssList(sk13). % 17.33/17.43 ** KEPT (pick-wt=13): 746 [copy,745,demod,707] app(app(cons(sk9,nil),cons(sk8,nil)),sk10)=sk1|ssList(sk13). % 17.33/17.43 ** KEPT (pick-wt=13): 747 [] ssList(sk10)|app(app(cons(sk11,nil),cons(sk12,nil)),sk13)=sk2. % 17.33/17.43 ** KEPT (pick-wt=22): 749 [copy,748,demod,704] app(app(cons(sk8,nil),cons(sk9,nil)),sk10)=sk2|app(app(cons(sk11,nil),cons(sk12,nil)),sk13)=sk2. % 17.33/17.43 ** KEPT (pick-wt=22): 751 [copy,750,demod,707] app(app(cons(sk9,nil),cons(sk8,nil)),sk10)=sk1|app(app(cons(sk11,nil),cons(sk12,nil)),sk13)=sk2. % 17.33/17.43 Following clause subsumed by 645 during input processing: 0 [copy,645,flip.1] A=A. % 17.33/17.43 645 back subsumes 449. % 17.33/17.43 645 back subsumes 327. % 17.33/17.43 645 back subsumes 326. % 17.33/17.43 645 back subsumes 325. % 17.33/17.43 645 back subsumes 315. % 17.33/17.43 645 back subsumes 302. % 17.33/17.43 645 back subsumes 301. % 17.33/17.43 645 back subsumes 300. % 17.33/17.43 645 back subsumes 226. % 17.33/17.43 645 back subsumes 214. % 17.33/17.43 645 back subsumes 213. % 17.33/17.43 645 back subsumes 212. % 17.33/17.43 645 back subsumes 211. % 17.33/17.43 645 back subsumes 194. % 17.33/17.43 645 back subsumes 191. % 17.33/17.43 645 back subsumes 189. % 17.33/17.43 645 back subsumes 185. % 17.33/17.43 645 back subsumes 182. % 17.33/17.43 645 back subsumes 159. % 17.33/17.43 645 back subsumes 158. % 17.33/17.43 645 back subsumes 157. % 17.33/17.43 645 back subsumes 156. % 17.33/17.43 645 back subsumes 155. % 17.33/17.43 645 back subsumes 147. % 17.33/17.43 645 back subsumes 146. % 17.33/17.43 >>>> Starting back demodulation with 704. % 17.33/17.43 >> back demodulating 701 with 704. % 17.33/17.43 >> back demodulating 644 with 704. % 17.33/17.43 >> back demodulating 643 with 704. % 17.33/17.43 >> back demodulating 642 with 704. % 17.33/17.43 >> back demodulating 641 with 704. % 17.33/17.43 >> back demodulating 640 with 704. % 17.33/17.43 >> back demodulating 639 with 704. % 17.33/17.43 >> back demodulating 638 with 704. % 17.33/17.43 >> back demodulating 637 with 704. % 17.33/17.43 >> back demodulating 636 with 704. % 17.33/17.43 >> back demodulating 635 with 704. % 17.33/17.43 >> back demodulating 634 with 704. % 17.33/17.43 >> back demodulating 633 with 704. % 17.33/17.43 >> back demodulating 632 with 704. % 17.33/17.43 >> back demodulating 631 with 704. % 17.33/17.43 >> back demodulating 630 with 704. % 17.33/17.43 >> back demodulating 629 with 704. % 17.33/17.43 >> back demodulating 628 with 704. % 17.33/17.43 >> back demodulating 627 with 704. % 17.33/17.43 >> back demodulating 626 with 704. % 17.33/17.43 >> back demodulating 625 with 704. % 17.33/17.43 >> back demodulating 624 with 704. % 17.33/17.43 >> back demodulating 623 with 704. % 17.33/17.43 >> back demodulating 622 with 704. % 17.33/17.43 >> back demodulating 621 with 704. % 17.33/17.43 >> back demodulating 620 with 704. % 17.33/17.43 >> back demodulating 619 with 704. % 17.33/17.43 >> back demodulating 618 with 704. % 17.89/17.98 >> back demodulating 617 with 704. % 17.89/17.98 >> back demodulating 616 with 704. % 17.89/17.98 >> back demodulating 615 with 704. % 17.89/17.98 >> back demodulating 614 with 704. % 17.89/17.98 >> back demodulating 613 with 704. % 17.89/17.98 >> back demodulating 612 with 704. % 17.89/17.98 >> back demodulating 611 with 704. % 17.89/17.98 >> back demodulating 610 with 704. % 17.89/17.98 >> back demodulating 609 with 704. % 17.89/17.98 >> back demodulating 608 with 704. % 17.89/17.98 >> back demodulating 607 with 704. % 17.89/17.98 >> back demodulating 606 with 704. % 17.89/17.98 >> back demodulating 605 with 704. % 17.89/17.98 >> back demodulating 604 with 704. % 17.89/17.98 >> back demodulating 603 with 704. % 17.89/17.98 >> back demodulating 602 with 704. % 17.89/17.98 >> back demodulating 601 with 704. % 17.89/17.98 >> back demodulating 600 with 704. % 17.89/17.98 >> back demodulating 599 with 704. % 17.89/17.98 >> back demodulating 598 with 704. % 17.89/17.98 >> back demodulating 597 with 704. % 17.89/17.98 >> back demodulating 596 with 704. % 17.89/17.98 >> back demodulating 595 with 704. % 17.89/17.98 >> back demodulating 594 with 704. % 17.89/17.98 >> back demodulating 593 with 704. % 17.89/17.98 >> back demodulating 592 with 704. % 17.89/17.98 >> back demodulating 591 with 704. % 17.89/17.98 >> back demodulating 590 with 704. % 17.89/17.98 >> back demodulating 589 with 704. % 17.89/17.98 >> back demodulating 588 with 704. % 17.89/17.98 >> back demodulating 587 with 704. % 17.89/17.98 >> back demodulating 586 with 704. % 17.89/17.98 >> back demodulating 585 with 704. % 17.89/17.98 >> back demodulating 584 with 704. % 17.89/17.98 >> back demodulating 583 with 704. % 17.89/17.98 >> back demodulating 582 with 704. % 17.89/17.98 >> back demodulating 581 with 704. % 17.89/17.98 >> back demodulating 580 with 704. % 17.89/17.98 >> back demodulating 579 with 704. % 17.89/17.98 >> back demodulating 578 with 704. % 17.89/17.98 >> back demodulating 577 with 704. % 17.89/17.98 >> back demodulating 576 with 704. % 17.89/17.98 >> back demodulating 575 with 704. % 17.89/17.98 >> back demodulating 574 with 704. % 17.89/17.98 >> back demodulating 573 with 704. % 17.89/17.98 >> back demodulating 572 with 704. % 17.89/17.98 >> back demodulating 571 with 704. % 17.89/17.98 >> back demodulating 570 with 704. % 17.89/17.98 >> back demodulating 569 with 704. % 17.89/17.98 >> back demodulating 561 with 704. % 17.89/17.98 >> back demodulating 560 with 704. % 17.89/17.98 >> back demodulating 559 with 704. % 17.89/17.98 >> back demodulating 558 with 704. % 17.89/17.98 >> back demodulating 557 with 704. % 17.89/17.98 >> back demodulating 556 with 704. % 17.89/17.98 >> back demodulating 555 with 704. % 17.89/17.98 >> back demodulating 554 with 704. % 17.89/17.98 >> back demodulating 553 with 704. % 17.89/17.98 >> back demodulating 552 with 704. % 17.89/17.98 >> back demodulating 551 with 704. % 17.89/17.98 >> back demodulating 550 with 704. % 17.89/17.98 >> back demodulating 549 with 704. % 17.89/17.98 >> back demodulating 548 with 704. % 17.89/17.98 >> back demodulating 547 with 704. % 17.89/17.98 >> back demodulating 546 with 704. % 17.89/17.98 >> back demodulating 545 with 704. % 17.89/17.98 >> back demodulating 544 with 704. % 17.89/17.98 >> back demodulating 543 with 704. % 17.89/17.98 >> back demodulating 542 with 704. % 17.89/17.98 >> back demodulating 541 with 704. % 17.89/17.98 >> back demodulating 540 with 704. % 17.89/17.98 >> back demodulating 539 with 704. % 17.89/17.98 >> back demodulating 538 with 704. % 17.89/17.98 >> back demodulating 537 with 704. % 17.89/17.98 >> back demodulating 536 with 704. % 17.89/17.98 >> back demodulating 535 with 704. % 17.89/17.98 >> back demodulating 534 with 704. % 17.89/17.98 >> back demodulating 533 with 704. % 17.89/17.98 >> back demodulating 532 with 704. % 17.89/17.98 >> back demodulating 531 with 704. % 17.89/17.98 >> back demodulating 530 with 704. % 17.89/17.98 >> back demodulating 529 with 704. % 17.89/17.98 >> back demodulating 528 with 704. % 17.89/17.98 >> back demodulating 527 with 704. % 17.89/17.98 >> back demodulating 526 with 704. % 17.89/17.98 >> back demodulating 525 with 704. % 17.89/17.98 >> back demodulating 524 with 704. % 17.89/17.98 >> back demodulating 523 with 704. % 17.89/17.98 >> back demodulating 522 with 704. % 17.89/17.98 >> back demodulating 521 with 704. % 17.89/17.98 >> back demodulating 520 with 704. % 17.89/17.98 >> back demodulating 519 with 704. % 17.89/17.98 >> back demodulating 518 with 704. % 17.89/17.98 >> back demodulating 517 with 704. % 17.89/17.98 >> back demodulating 516 with 704. % 17.89/17.98 >> back demodulating 515 with 704. % 17.89/17.98 >> back demodulating 514 with 704. % 17.89/17.98 >> back demodulating 513 with 704. % 17.89/17.98 >> back demodulating 512 with 704. % 17.89/17.98 >> back demodulating 511 with 704. % 17.89/17.98 >> back demodulating 510 with 704. % 17.89/17.98 >> back demodulating 509 with 704. % 17.89/17.98 >> back demodulating 508 with 704. % 17.89/17.98 >> back demodulating 507 with 704. % 17.89/17.98 >> back demodulating 506 with 704. % 18.68/18.79 >> back demodulating 505 with 704. % 18.68/18.79 >> back demodulating 504 with 704. % 18.68/18.79 >> back demodulating 503 with 704. % 18.68/18.79 >> back demodulating 502 with 704. % 18.68/18.79 >> back demodulating 501 with 704. % 18.68/18.79 >> back demodulating 500 with 704. % 18.68/18.79 >> back demodulating 499 with 704. % 18.68/18.79 >> back demodulating 498 with 704. % 18.68/18.79 >> back demodulating 497 with 704. % 18.68/18.79 >> back demodulating 496 with 704. % 18.68/18.79 >> back demodulating 495 with 704. % 18.68/18.79 >> back demodulating 494 with 704. % 18.68/18.79 >> back demodulating 493 with 704. % 18.68/18.79 >> back demodulating 492 with 704. % 18.68/18.79 >> back demodulating 491 with 704. % 18.68/18.79 >> back demodulating 490 with 704. % 18.68/18.79 >> back demodulating 489 with 704. % 18.68/18.79 >> back demodulating 488 with 704. % 18.68/18.79 >> back demodulating 487 with 704. % 18.68/18.79 >> back demodulating 486 with 704. % 18.68/18.79 >> back demodulating 485 with 704. % 18.68/18.79 >> back demodulating 484 with 704. % 18.68/18.79 >> back demodulating 483 with 704. % 18.68/18.79 >> back demodulating 482 with 704. % 18.68/18.79 >> back demodulating 481 with 704. % 18.68/18.79 >> back demodulating 480 with 704. % 18.68/18.79 >> back demodulating 479 with 704. % 18.68/18.79 >> back demodulating 478 with 704. % 18.68/18.79 >> back demodulating 477 with 704. % 18.68/18.79 >> back demodulating 476 with 704. % 18.68/18.79 >> back demodulating 430 with 704. % 18.68/18.79 >> back demodulating 429 with 704. % 18.68/18.79 >> back demodulating 428 with 704. % 18.68/18.79 >> back demodulating 427 with 704. % 18.68/18.79 >> back demodulating 426 with 704. % 18.68/18.79 >> back demodulating 425 with 704. % 18.68/18.79 >> back demodulating 424 with 704. % 18.68/18.79 >> back demodulating 423 with 704. % 18.68/18.79 >> back demodulating 422 with 704. % 18.68/18.79 >> back demodulating 421 with 704. % 18.68/18.79 >> back demodulating 420 with 704. % 18.68/18.79 >> back demodulating 419 with 704. % 18.68/18.79 >> back demodulating 418 with 704. % 18.68/18.79 >> back demodulating 417 with 704. % 18.68/18.79 >> back demodulating 416 with 704. % 18.68/18.79 >> back demodulating 415 with 704. % 18.68/18.79 >> back demodulating 414 with 704. % 18.68/18.79 >> back demodulating 413 with 704. % 18.68/18.79 >> back demodulating 412 with 704. % 18.68/18.79 >> back demodulating 411 with 704. % 18.68/18.79 >> back demodulating 410 with 704. % 18.68/18.79 >> back demodulating 409 with 704. % 18.68/18.79 >> back demodulating 408 with 704. % 18.68/18.79 >> back demodulating 407 with 704. % 18.68/18.79 >> back demodulating 406 with 704. % 18.68/18.79 >> back demodulating 405 with 704. % 18.68/18.79 >> back demodulating 404 with 704. % 18.68/18.79 >> back demodulating 403 with 704. % 18.68/18.79 >> back demodulating 402 with 704. % 18.68/18.79 >> back demodulating 401 with 704. % 18.68/18.79 >> back demodulating 400 with 704. % 18.68/18.79 >> back demodulating 399 with 704. % 18.68/18.79 >> back demodulating 398 with 704. % 18.68/18.79 >> back demodulating 397 with 704. % 18.68/18.79 >> back demodulating 396 with 704. % 18.68/18.79 >> back demodulating 395 with 704. % 18.68/18.79 >> back demodulating 394 with 704. % 18.68/18.79 >> back demodulating 393 with 704. % 18.68/18.79 >> back demodulating 392 with 704. % 18.68/18.79 >> back demodulating 391 with 704. % 18.68/18.79 >> back demodulating 390 with 704. % 18.68/18.79 >> back demodulating 389 with 704. % 18.68/18.79 >> back demodulating 388 with 704. % 18.68/18.79 >> back demodulating 387 with 704. % 18.68/18.79 >> back demodulating 386 with 704. % 18.68/18.79 >> back demodulating 385 with 704. % 18.68/18.79 >> back demodulating 384 with 704. % 18.68/18.79 >> back demodulating 383 with 704. % 18.68/18.79 >> back demodulating 382 with 704. % 18.68/18.80 >> back demodulating 381 with 704. % 18.68/18.80 >> back demodulating 296 with 704. % 18.68/18.80 >> back demodulating 295 with 704. % 18.68/18.80 >> back demodulating 294 with 704. % 18.68/18.80 >> back demodulating 293 with 704. % 18.68/18.80 >> back demodulating 292 with 704. % 18.68/18.80 >> back demodulating 291 with 704. % 18.68/18.80 >> back demodulating 290 with 704. % 18.68/18.80 >> back demodulating 289 with 704. % 18.68/18.80 >> back demodulating 288 with 704. % 18.68/18.80 >> back demodulating 271 with 704. % 18.68/18.80 >> back demodulating 270 with 704. % 18.68/18.80 >> back demodulating 269 with 704. % 18.68/18.80 >> back demodulating 268 with 704. % 18.68/18.80 >> back demodulating 267 with 704. % 18.68/18.80 >> back demodulating 266 with 704. % 18.68/18.80 >> back demodulating 265 with 704. % 18.68/18.80 >> back demodulating 264 with 704. % 18.68/18.80 >> back demodulating 263 with 704. % 18.68/18.80 >> back demodulating 262 with 704. % 18.68/18.80 >> back demodulating 261 with 704. % 18.68/18.80 >> back demodulating 260 with 704. % 18.68/18.80 >> back demodulating 144 with 704. % 18.68/18.80 >> back demodulating 143 with 704. % 18.68/18.80 >> back demodulating 142 with 704. % 18.68/18.80 >> back demodulating 141 withAlarm clock % 299.95/300.04 Otter interrupted % 299.95/300.04 PROOF NOT FOUND %------------------------------------------------------------------------------