%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWW472+1 : TPTP v8.1.0. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n021.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:22:38 EDT 2022 % Result : Unknown 3.54s 3.65s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW472+1 : TPTP v8.1.0. Released v5.3.0. % 0.12/0.13 % Command : otter-tptp-script %s % 0.12/0.33 % Computer : n021.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Wed Jul 27 02:59:23 EDT 2022 % 0.12/0.34 % CPUTime : % 2.22/2.41 ----- Otter 3.3f, August 2004 ----- % 2.22/2.41 The process was started by sandbox on n021.cluster.edu, % 2.22/2.41 Wed Jul 27 02:59:23 2022 % 2.22/2.41 The command was "./otter". The process ID is 27375. % 2.22/2.41 % 2.22/2.41 set(prolog_style_variables). % 2.22/2.41 set(auto). % 2.22/2.41 dependent: set(auto1). % 2.22/2.41 dependent: set(process_input). % 2.22/2.41 dependent: clear(print_kept). % 2.22/2.41 dependent: clear(print_new_demod). % 2.22/2.41 dependent: clear(print_back_demod). % 2.22/2.41 dependent: clear(print_back_sub). % 2.22/2.41 dependent: set(control_memory). % 2.22/2.41 dependent: assign(max_mem, 12000). % 2.22/2.41 dependent: assign(pick_given_ratio, 4). % 2.22/2.41 dependent: assign(stats_level, 1). % 2.22/2.41 dependent: assign(max_seconds, 10800). % 2.22/2.41 clear(print_given). % 2.22/2.41 % 2.22/2.41 formula_list(usable). % 2.22/2.41 all A (A=A). % 2.22/2.41 all B_1_1 B_2_1 is_bool(big_se883361720_state(B_1_1,B_2_1)). % 2.22/2.41 all B_1_1 B_2_1 is_bool(finite354701905_state(B_1_1,B_2_1)). % 2.22/2.41 all B_1_1 B_2_1 is_bool(finite86813460_state(B_1_1,B_2_1)). % 2.22/2.41 is_bool(bot_bot_bool). % 2.22/2.41 is_bool(fFalse). % 2.22/2.41 is_bool(fTrue). % 2.22/2.41 all B_1_1 B_2_1 is_bool(hAPP_state_bool(B_1_1,B_2_1)). % 2.22/2.41 all B_1_1 B_2_1 (is_bool(B_2_1)->is_bool(hAPP_bool_bool(B_1_1,B_2_1))). % 2.22/2.41 all B_1_1 B_2_1 is_bool(hAPP_H78829294e_bool(B_1_1,B_2_1)). % 2.22/2.41 all B_1_1 B_2_1 is_bool(hAPP_f971112728l_bool(B_1_1,B_2_1)). % 2.22/2.41 all G_1 hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),bot_bo620288102e_bool)). % 2.22/2.41 all Fun1_2 Com_2 Fun2_2 Fun1_1 Com_1 Fun2_1 (hoare_2082236334_state(Fun1_2,Com_2,Fun2_2)=hoare_2082236334_state(Fun1_1,Com_1,Fun2_1)<->Fun1_2=Fun1_1&Com_2=Com_1&Fun2_2=Fun2_1). % 2.22/2.41 all G_1 Ts (hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),Ts))->hBOOL(hAPP_f971112728l_bool(hoare_2004700328_state(G_1),Ts))). % 2.22/2.41 all G_1 G_2 Ts (hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_2),Ts))-> (hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),G_2))->hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),Ts)))). % 2.22/2.41 all Ts G_1 T (hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(T,bot_bo620288102e_bool)))-> (hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),Ts))->hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(T,Ts))))). % 2.22/2.41 all G_1 T Ts (hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(T,Ts)))->hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(T,bot_bo620288102e_bool)))&hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),Ts))). % 2.22/2.41 all Qa G_1 Pa Ca Q_2 (hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(Pa,Ca,Q_2),bot_bo620288102e_bool)))-> ((all Z_1 S (hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(Q_2,Z_1),S))->hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(Qa,Z_1),S))))->hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(Pa,Ca,Qa),bot_bo620288102e_bool))))). % 2.22/2.41 all Pa G_1 P_2 Ca Qa (hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(P_2,Ca,Qa),bot_bo620288102e_bool)))-> ((all Z_1 S (hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(Pa,Z_1),S))->hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(P_2,Z_1),S))))->hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(Pa,Ca,Qa),bot_bo620288102e_bool))))). % 2.22/2.41 all A B_1 A_1 (hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),insert1415133716_state(B_1,A_1)))-> (A!=B_1->hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),A_1)))). % 2.22/2.41 all B_1 A B ((-hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),B))->A=B_1)->hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),insert1415133716_state(B_1,B)))). % 2.22/2.41 all Qa Pa G_1 P_2 Ca Q_2 (hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(P_2,Ca,Q_2),bot_bo620288102e_bool)))-> ((all Z_1 S (hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(Pa,Z_1),S))-> (all S_1 ((all Z_2 (hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(P_2,Z_2),S))->hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(Q_2,Z_2),S_1))))->hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(Qa,Z_1),S_1))))))->hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(Pa,Ca,Qa),bot_bo620288102e_bool))))). % 2.22/2.41 all A (-hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),bot_bo620288102e_bool))). % 2.22/2.41 all A A_1 (bot_bo620288102e_bool!=insert1415133716_state(A,A_1)). % 2.22/2.41 all A A_1 (insert1415133716_state(A,A_1)!=bot_bo620288102e_bool). % 2.22/2.41 all B_1 A (hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,B_1),insert1415133716_state(A,bot_bo620288102e_bool)))<->B_1=A). % 2.22/2.41 all A B_1 Ca D (insert1415133716_state(A,insert1415133716_state(B_1,bot_bo620288102e_bool))=insert1415133716_state(Ca,insert1415133716_state(D,bot_bo620288102e_bool))<->A=Ca&B_1=D|A=D&B_1=Ca). % 2.22/2.41 all A A_1 (A_1=bot_bo620288102e_bool-> -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),A_1))). % 2.22/2.41 all Pa (collec307967673_state(Pa)=bot_bo620288102e_bool<-> (all X_2 (-hBOOL(hAPP_H78829294e_bool(Pa,X_2))))). % 2.22/2.41 all Ca (-hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,Ca),bot_bo620288102e_bool))). % 2.22/2.41 all Pa (bot_bo620288102e_bool=collec307967673_state(Pa)<-> (all X_2 (-hBOOL(hAPP_H78829294e_bool(Pa,X_2))))). % 2.22/2.41 all A_1 ((exists X_2 hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_2),A_1)))<->A_1!=bot_bo620288102e_bool). % 2.22/2.41 all A_1 ((all X_2 (-hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_2),A_1))))<->A_1=bot_bo620288102e_bool). % 2.22/2.41 bot_bo620288102e_bool=collec307967673_state(cOMBK_659609255_state(fFalse)). % 2.22/2.41 all A A_1 (hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),A_1))->insert1415133716_state(A,A_1)=A_1). % 2.22/2.41 all B_1 A B (hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),B))->hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),insert1415133716_state(B_1,B)))). % 2.22/2.41 all B X_1 A_1 (-hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_1),A_1))-> (-hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_1),B))-> (insert1415133716_state(X_1,A_1)=insert1415133716_state(X_1,B)<->A_1=B))). % 2.22/2.41 all Y_2 A_1 X_1 (hBOOL(hAPP_H78829294e_bool(insert1415133716_state(Y_2,A_1),X_1))<->Y_2=X_1|hBOOL(hAPP_H78829294e_bool(A_1,X_1))). % 2.22/2.41 all A B_1 A_1 (hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),insert1415133716_state(B_1,A_1)))<->A=B_1|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),A_1))). % 2.22/2.41 all X_1 Y_2 A_1 (insert1415133716_state(X_1,insert1415133716_state(Y_2,A_1))=insert1415133716_state(Y_2,insert1415133716_state(X_1,A_1))). % 2.22/2.41 all X_1 A_1 (insert1415133716_state(X_1,insert1415133716_state(X_1,A_1))=insert1415133716_state(X_1,A_1)). % 2.22/2.41 all A Pa (insert1415133716_state(A,collec307967673_state(Pa))=collec307967673_state(cOMBS_458705923l_bool(cOMBB_962198420_state(fimplies,cOMBB_2144135922_state(fNot,cOMBC_654211620e_bool(fe_qual1111551311_state,A))),Pa))). % 2.22/2.41 all A B (insert1415133716_state(A,B)=collec307967673_state(cOMBS_458705923l_bool(cOMBB_962198420_state(fdisj,cOMBC_654211620e_bool(fe_qual1111551311_state,A)),cOMBC_1734175330l_bool(member1338687867_state,B)))). % 2.22/2.41 all A B hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),insert1415133716_state(A,B))). % 2.22/2.41 all A B_1 (insert1415133716_state(A,bot_bo620288102e_bool)=insert1415133716_state(B_1,bot_bo620288102e_bool)->A=B_1). % 2.22/2.41 all B_1 A (hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,B_1),insert1415133716_state(A,bot_bo620288102e_bool)))->B_1=A). % 2.22/2.41 all X_1 (hAPP_f1387463497_state(the_el1751439279_state,insert1415133716_state(X_1,bot_bo620288102e_bool))=X_1). % 2.22/2.41 all X_1 (hBOOL(hAPP_H78829294e_bool(bot_bo620288102e_bool,X_1))<->hBOOL(bot_bot_bool)). % 2.22/2.41 all X_2 (hBOOL(hAPP_H78829294e_bool(bot_bo620288102e_bool,X_2))<->hBOOL(bot_bot_bool)). % 2.22/2.41 all G_1 Pa hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(Pa,skip,Pa),bot_bo620288102e_bool))). % 2.22/2.41 all D R_1 G_1 Pa Ca Qa (hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(Pa,Ca,Qa),bot_bo620288102e_bool)))-> (hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(Qa,D,R_1),bot_bo620288102e_bool)))->hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(Pa,semi(Ca,D),R_1),bot_bo620288102e_bool))))). % 2.22/2.41 all Y_2 (-(all Fun1 Com Fun2 (Y_2!=hoare_2082236334_state(Fun1,Com,Fun2)))). % 2.22/2.41 all X_1 A_1 (hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_1),A_1))-> -(all B_2 (A_1=insert1415133716_state(X_1,B_2)->hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_1),B_2))))). % 2.22/2.41 all A A_1 (hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),A_1))-> (exists B_2 (A_1=insert1415133716_state(A,B_2)& -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),B_2))))). % 2.22/2.41 all Com1_2 Com2_2 (semi(Com1_2,Com2_2)!=skip). % 2.22/2.41 all Com1_2 Com2_2 (skip!=semi(Com1_2,Com2_2)). % 2.22/2.41 all A_1 ((all Y_1 (-hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,Y_1),A_1))))->A_1=bot_bo620288102e_bool). % 2.22/2.41 all Qa G_1 Ca Pa ((all Z_1 S (hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(Pa,Z_1),S))-> (exists P_1 Q_1 (hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(P_1,Ca,Q_1),bot_bo620288102e_bool)))& (all S_1 ((all Z_2 (hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(P_1,Z_2),S))->hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(Q_1,Z_2),S_1))))->hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(Qa,Z_1),S_1))))))))->hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(Pa,Ca,Qa),bot_bo620288102e_bool)))). % 2.22/2.41 all Com1_1 Com2_1 Com1 Com2 (semi(Com1_1,Com2_1)=semi(Com1,Com2)<->Com1_1=Com1&Com2_1=Com2). % 2.22/2.41 all A_1 (A_1!=bot_bo620288102e_bool<-> (exists X_2 B_2 (A_1=insert1415133716_state(X_2,B_2)& -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_2),B_2))))). % 2.22/2.41 all X_2 (hBOOL(hAPP_H78829294e_bool(bot_bo620288102e_bool,X_2))<->hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_2),bot_bo620288102e_bool))). % 2.22/2.41 all F_1 A B_1 (hBOOL(hAPP_H78829294e_bool(finite1736999486_state(F_1,insert1415133716_state(A,bot_bo620288102e_bool)),B_1))<->A=B_1). % 2.22/2.41 all X_1 F_1 F (hBOOL(finite354701905_state(F_1,F))->hAPP_f1387463497_state(F,insert1415133716_state(X_1,bot_bo620288102e_bool))=X_1). % 2.22/2.41 all F_1 A (hAPP_f1387463497_state(finite926392750_state(F_1),insert1415133716_state(A,bot_bo620288102e_bool))=A). % 2.22/2.41 all A G F_1 (G=finite926392750_state(F_1)->hAPP_f1387463497_state(G,insert1415133716_state(A,bot_bo620288102e_bool))=A). % 2.22/2.41 all F_1 X_1 (-hBOOL(hAPP_H78829294e_bool(finite1736999486_state(F_1,bot_bo620288102e_bool),X_1))). % 2.22/2.41 all F_1 A_1 X_1 (hBOOL(hAPP_H78829294e_bool(finite1736999486_state(F_1,A_1),X_1))->A_1!=bot_bo620288102e_bool). % 2.22/2.41 all F_1 A A_1 X_1 (hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,A,A_1),X_1))-> (-hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),A_1))->hBOOL(hAPP_H78829294e_bool(finite1736999486_state(F_1,insert1415133716_state(A,A_1)),X_1)))). % 2.22/2.41 all X_1 A_1 F_1 F (hBOOL(finite354701905_state(F_1,F))-> (hBOOL(hAPP_f971112728l_bool(finite364844667_state,A_1))-> (-hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_1),A_1))-> (A_1!=bot_bo620288102e_bool->hAPP_f1387463497_state(F,insert1415133716_state(X_1,A_1))=hAPP_H1150764575_state(hAPP_H1855735728_state(F_1,X_1),hAPP_f1387463497_state(F,A_1)))))). % 2.22/2.41 all A_1 F_1 F (hBOOL(finite354701905_state(F_1,F))-> (hBOOL(hAPP_f971112728l_bool(finite364844667_state,A_1))->hAPP_f1387463497_state(F,A_1)=hAPP_f1387463497_state(finite926392750_state(F_1),A_1))). % 2.22/2.41 hBOOL(hAPP_f971112728l_bool(finite364844667_state,bot_bo620288102e_bool)). % 2.22/2.41 all A A_1 (hBOOL(hAPP_f971112728l_bool(finite364844667_state,A_1))->hBOOL(hAPP_f971112728l_bool(finite364844667_state,insert1415133716_state(A,A_1)))). % 2.22/2.41 all F_1 Z hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,Z,bot_bo620288102e_bool),Z)). % 2.22/2.41 all F_1 Z X_1 (hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,Z,bot_bo620288102e_bool),X_1))->X_1=Z). % 2.22/2.41 all F_1 Z Y_2 X_1 A_1 (-hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_1),A_1))-> (hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,Z,A_1),Y_2))->hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,Z,insert1415133716_state(X_1,A_1)),hAPP_H1150764575_state(hAPP_H1855735728_state(F_1,X_1),Y_2))))). % 2.22/2.41 all A A_1 (hBOOL(hAPP_f971112728l_bool(finite364844667_state,insert1415133716_state(A,A_1)))<->hBOOL(hAPP_f971112728l_bool(finite364844667_state,A_1))). % 2.22/2.41 all A_1 F_1 F (hBOOL(finite354701905_state(F_1,F))-> (hBOOL(hAPP_f971112728l_bool(finite364844667_state,A_1))-> (A_1!=bot_bo620288102e_bool-> ((all X_2 Y_1 hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,hAPP_H1150764575_state(hAPP_H1855735728_state(F_1,X_2),Y_1)),insert1415133716_state(X_2,insert1415133716_state(Y_1,bot_bo620288102e_bool)))))->hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,hAPP_f1387463497_state(F,A_1)),A_1)))))). % 2.22/2.41 all F_1 A X_3 X_1 (hBOOL(hAPP_H78829294e_bool(finite1736999486_state(F_1,insert1415133716_state(A,X_3)),X_1))-> -(all A_3 A_2 (insert1415133716_state(A,X_3)=insert1415133716_state(A_3,A_2)-> (hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,A_3,A_2),X_1))->hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A_3),A_2)))))). % 2.22/2.41 all F_1 A_1 (hBOOL(hAPP_f971112728l_bool(finite364844667_state,A_1))-> (A_1!=bot_bo620288102e_bool-> (exists X1 hBOOL(hAPP_H78829294e_bool(finite1736999486_state(F_1,A_1),X1))))). % 2.22/2.41 all Pa F (hBOOL(hAPP_f971112728l_bool(finite364844667_state,F))-> (hBOOL(hAPP_f971112728l_bool(Pa,bot_bo620288102e_bool))-> ((all X_2 F_2 (hBOOL(hAPP_f971112728l_bool(finite364844667_state,F_2))-> (-hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_2),F_2))-> (hBOOL(hAPP_f971112728l_bool(Pa,F_2))->hBOOL(hAPP_f971112728l_bool(Pa,insert1415133716_state(X_2,F_2)))))))->hBOOL(hAPP_f971112728l_bool(Pa,F))))). % 2.22/2.41 all X_1 A_1 (hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_1),A_1))<->hBOOL(hAPP_H78829294e_bool(A_1,X_1))). % 2.22/2.41 all Pa (collec307967673_state(Pa)=Pa). % 2.22/2.41 all A (hBOOL(hAPP_f971112728l_bool(finite364844667_state,A))<->A=bot_bo620288102e_bool| (exists A_2 A_3 (A=insert1415133716_state(A_3,A_2)&hBOOL(hAPP_f971112728l_bool(finite364844667_state,A_2))))). % 2.22/2.41 all F_1 Z A_1 (hBOOL(hAPP_f971112728l_bool(finite364844667_state,A_1))-> (exists X1 hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,Z,A_1),X1)))). % 2.22/2.41 all F_1 A1 A2 (hBOOL(hAPP_H78829294e_bool(finite1736999486_state(F_1,A1),A2))<-> (exists A_3 A_2 X_2 (A1=insert1415133716_state(A_3,A_2)&A2=X_2&hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,A_3,A_2),X_2))& -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A_3),A_2))))). % 2.22/2.41 all F_1 Z A1 A2 (hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,Z,A1),A2))<->A1=bot_bo620288102e_bool&A2=Z| (exists X_2 A_2 Y_1 (A1=insert1415133716_state(X_2,A_2)&A2=hAPP_H1150764575_state(hAPP_H1855735728_state(F_1,X_2),Y_1)& -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_2),A_2))&hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,Z,A_2),Y_1))))). % 2.22/2.41 all X_1 A_1 F_1 F (hBOOL(finite86813460_state(F_1,F))-> (hBOOL(hAPP_f971112728l_bool(finite364844667_state,A_1))-> (A_1!=bot_bo620288102e_bool->hAPP_f1387463497_state(F,insert1415133716_state(X_1,A_1))=hAPP_H1150764575_state(hAPP_H1855735728_state(F_1,X_1),hAPP_f1387463497_state(F,A_1))))). % 2.22/2.41 all X_1 F_1 F (hBOOL(finite86813460_state(F_1,F))->hAPP_H1150764575_state(hAPP_H1855735728_state(F_1,X_1),X_1)=X_1). % 2.22/2.41 all X_1 A_1 F_1 F (hBOOL(finite86813460_state(F_1,F))-> (hBOOL(hAPP_f971112728l_bool(finite364844667_state,A_1))-> (hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_1),A_1))->hAPP_H1150764575_state(hAPP_H1855735728_state(F_1,X_1),hAPP_f1387463497_state(F,A_1))=hAPP_f1387463497_state(F,A_1)))). % 2.22/2.41 all Pa F (hBOOL(hAPP_f971112728l_bool(finite364844667_state,F))-> (F!=bot_bo620288102e_bool-> ((all X_2 hBOOL(hAPP_f971112728l_bool(Pa,insert1415133716_state(X_2,bot_bo620288102e_bool))))-> ((all X_2 F_2 (hBOOL(hAPP_f971112728l_bool(finite364844667_state,F_2))-> (F_2!=bot_bo620288102e_bool-> (-hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_2),F_2))-> (hBOOL(hAPP_f971112728l_bool(Pa,F_2))->hBOOL(hAPP_f971112728l_bool(Pa,insert1415133716_state(X_2,F_2))))))))->hBOOL(hAPP_f971112728l_bool(Pa,F)))))). % 2.22/2.41 all A_1 F_1 F (hBOOL(big_se883361720_state(F_1,F))-> (hBOOL(hAPP_f971112728l_bool(finite364844667_state,A_1))->hAPP_f1387463497_state(F,A_1)=hAPP_f1387463497_state(finite926392750_state(F_1),A_1))). % 2.22/2.41 all X_1 A_1 F_1 F (hBOOL(finite354701905_state(F_1,F))-> (hBOOL(hAPP_f971112728l_bool(finite364844667_state,A_1))-> (hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_1),A_1))-> (minus_1641527009e_bool(A_1,insert1415133716_state(X_1,bot_bo620288102e_bool))=bot_bo620288102e_bool->hAPP_f1387463497_state(F,A_1)=X_1)& (minus_1641527009e_bool(A_1,insert1415133716_state(X_1,bot_bo620288102e_bool))!=bot_bo620288102e_bool->hAPP_f1387463497_state(F,A_1)=hAPP_H1150764575_state(hAPP_H1855735728_state(F_1,X_1),hAPP_f1387463497_state(F,minus_1641527009e_bool(A_1,insert1415133716_state(X_1,bot_bo620288102e_bool)))))))). % 2.22/2.41 all B Ca A_1 (hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,Ca),A_1))-> (-hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,Ca),B))->hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,Ca),minus_1641527009e_bool(A_1,B))))). % 2.22/2.41 all Ca A_1 B (hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,Ca),minus_1641527009e_bool(A_1,B)))-> -(hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,Ca),A_1))->hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,Ca),B)))). % 2.22/2.41 all B A_1 (hBOOL(hAPP_f971112728l_bool(finite364844667_state,A_1))->hBOOL(hAPP_f971112728l_bool(finite364844667_state,minus_1641527009e_bool(A_1,B)))). % 2.22/2.41 all A A_1 (hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),A_1))->insert1415133716_state(A,minus_1641527009e_bool(A_1,insert1415133716_state(A,bot_bo620288102e_bool)))=A_1). % 2.22/2.41 all X_1 A_1 (-hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_1),A_1))->minus_1641527009e_bool(insert1415133716_state(X_1,A_1),insert1415133716_state(X_1,bot_bo620288102e_bool))=A_1). % 2.22/2.41 all A A_1 (insert1415133716_state(A,minus_1641527009e_bool(A_1,insert1415133716_state(A,bot_bo620288102e_bool)))=insert1415133716_state(A,A_1)). % 2.22/2.41 all A_1 A B (minus_1641527009e_bool(A_1,insert1415133716_state(A,B))=minus_1641527009e_bool(minus_1641527009e_bool(A_1,insert1415133716_state(A,bot_bo620288102e_bool)),B)). % 2.22/2.41 all A_1 A B (minus_1641527009e_bool(A_1,insert1415133716_state(A,B))=minus_1641527009e_bool(minus_1641527009e_bool(A_1,B),insert1415133716_state(A,bot_bo620288102e_bool))). % 2.22/2.41 all A_1 A B (hBOOL(hAPP_f971112728l_bool(finite364844667_state,minus_1641527009e_bool(A_1,insert1415133716_state(A,B))))<->hBOOL(hAPP_f971112728l_bool(finite364844667_state,minus_1641527009e_bool(A_1,B)))). % 2.22/2.41 all P (-hBOOL(hAPP_bool_bool(fNot,P))| -hBOOL(P)). % 2.22/2.41 all P (hBOOL(P)|hBOOL(hAPP_bool_bool(fNot,P))). % 2.22/2.41 all Q P (-hBOOL(P)|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(fdisj,P),Q))). % 2.22/2.41 all P Q (-hBOOL(Q)|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(fdisj,P),Q))). % 2.22/2.41 all P Q (-hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(fdisj,P),Q))|hBOOL(P)|hBOOL(Q)). % 2.22/2.41 -hBOOL(fFalse). % 2.22/2.41 all P (is_bool(P)->P=fTrue|P=fFalse). % 2.22/2.41 all Q P (hBOOL(P)|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(fimplies,P),Q))). % 2.22/2.41 all P Q (-hBOOL(Q)|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(fimplies,P),Q))). % 2.22/2.41 all P Q (-hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(fimplies,P),Q))| -hBOOL(P)|hBOOL(Q)). % 2.22/2.41 all X Y (-hBOOL(hAPP_H78829294e_bool(hAPP_H1049623551e_bool(fe_qual1111551311_state,X),Y))|X=Y). % 2.22/2.41 all X Y (X!=Y|hBOOL(hAPP_H78829294e_bool(hAPP_H1049623551e_bool(fe_qual1111551311_state,X),Y))). % 2.22/2.41 all P Q (is_bool(P)->hAPP_H78829294e_bool(cOMBK_659609255_state(P),Q)=P). % 2.22/2.41 all P Q R (hAPP_H78829294e_bool(cOMBB_2144135922_state(P,Q),R)=hAPP_bool_bool(P,hAPP_H78829294e_bool(Q,R))). % 2.22/2.41 all P Q R (hAPP_H78829294e_bool(cOMBS_458705923l_bool(P,Q),R)=hAPP_bool_bool(hAPP_H1187982158l_bool(P,R),hAPP_H78829294e_bool(Q,R))). % 2.22/2.41 all P Q R (hAPP_H1187982158l_bool(cOMBB_962198420_state(P,Q),R)=hAPP_b589554111l_bool(P,hAPP_H78829294e_bool(Q,R))). % 2.22/2.41 all P Q R (hAPP_H78829294e_bool(cOMBC_654211620e_bool(P,Q),R)=hAPP_H78829294e_bool(hAPP_H1049623551e_bool(P,R),Q)). % 2.22/2.41 all P Q R (hAPP_H78829294e_bool(cOMBC_1734175330l_bool(P,Q),R)=hAPP_f971112728l_bool(hAPP_H30606679l_bool(P,R),Q)). % 2.22/2.41 hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(bot_bo620288102e_bool),insert1415133716_state(hoare_Mirabelle_MGT(c),bot_bo620288102e_bool))). % 2.22/2.41 hBOOL(hAPP_f971112728l_bool(hoare_2004700328_state(bot_bo620288102e_bool),insert1415133716_state(hoare_2082236334_state(p,c,q),bot_bo620288102e_bool))). % 2.22/2.41 -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(bot_bo620288102e_bool),insert1415133716_state(hoare_2082236334_state(p,c,q),bot_bo620288102e_bool))). % 2.22/2.41 end_of_list. % 2.22/2.41 % 2.22/2.41 -------> usable clausifies to: % 2.22/2.41 % 2.22/2.41 list(usable). % 2.22/2.41 0 [] A=A. % 2.22/2.41 0 [] is_bool(big_se883361720_state(B_1_1,B_2_1)). % 2.22/2.41 0 [] is_bool(finite354701905_state(B_1_1,B_2_1)). % 2.22/2.41 0 [] is_bool(finite86813460_state(B_1_1,B_2_1)). % 2.22/2.41 0 [] is_bool(bot_bot_bool). % 2.22/2.41 0 [] is_bool(fFalse). % 2.22/2.41 0 [] is_bool(fTrue). % 2.22/2.41 0 [] is_bool(hAPP_state_bool(B_1_1,B_2_1)). % 2.22/2.41 0 [] -is_bool(B_2_1)|is_bool(hAPP_bool_bool(B_1_1,B_2_1)). % 2.22/2.41 0 [] is_bool(hAPP_H78829294e_bool(B_1_1,B_2_1)). % 2.22/2.41 0 [] is_bool(hAPP_f971112728l_bool(B_1_1,B_2_1)). % 2.22/2.41 0 [] hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),bot_bo620288102e_bool)). % 2.22/2.41 0 [] hoare_2082236334_state(Fun1_2,Com_2,Fun2_2)!=hoare_2082236334_state(Fun1_1,Com_1,Fun2_1)|Fun1_2=Fun1_1. % 2.22/2.41 0 [] hoare_2082236334_state(Fun1_2,Com_2,Fun2_2)!=hoare_2082236334_state(Fun1_1,Com_1,Fun2_1)|Com_2=Com_1. % 2.22/2.41 0 [] hoare_2082236334_state(Fun1_2,Com_2,Fun2_2)!=hoare_2082236334_state(Fun1_1,Com_1,Fun2_1)|Fun2_2=Fun2_1. % 2.22/2.41 0 [] hoare_2082236334_state(Fun1_2,Com_2,Fun2_2)=hoare_2082236334_state(Fun1_1,Com_1,Fun2_1)|Fun1_2!=Fun1_1|Com_2!=Com_1|Fun2_2!=Fun2_1. % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),Ts))|hBOOL(hAPP_f971112728l_bool(hoare_2004700328_state(G_1),Ts)). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_2),Ts))| -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),G_2))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),Ts)). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(T,bot_bo620288102e_bool)))| -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),Ts))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(T,Ts))). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(T,Ts)))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(T,bot_bo620288102e_bool))). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(T,Ts)))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),Ts)). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(Pa,Ca,Q_2),bot_bo620288102e_bool)))|hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(Q_2,$f2(Qa,G_1,Pa,Ca,Q_2)),$f1(Qa,G_1,Pa,Ca,Q_2)))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(Pa,Ca,Qa),bot_bo620288102e_bool))). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(Pa,Ca,Q_2),bot_bo620288102e_bool)))| -hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(Qa,$f2(Qa,G_1,Pa,Ca,Q_2)),$f1(Qa,G_1,Pa,Ca,Q_2)))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(Pa,Ca,Qa),bot_bo620288102e_bool))). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(P_2,Ca,Qa),bot_bo620288102e_bool)))|hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(Pa,$f4(Pa,G_1,P_2,Ca,Qa)),$f3(Pa,G_1,P_2,Ca,Qa)))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(Pa,Ca,Qa),bot_bo620288102e_bool))). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(P_2,Ca,Qa),bot_bo620288102e_bool)))| -hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(P_2,$f4(Pa,G_1,P_2,Ca,Qa)),$f3(Pa,G_1,P_2,Ca,Qa)))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(Pa,Ca,Qa),bot_bo620288102e_bool))). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),insert1415133716_state(B_1,A_1)))|A=B_1|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),A_1)). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),B))|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),insert1415133716_state(B_1,B))). % 2.22/2.41 0 [] A!=B_1|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),insert1415133716_state(B_1,B))). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(P_2,Ca,Q_2),bot_bo620288102e_bool)))|hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(Pa,$f7(Qa,Pa,G_1,P_2,Ca,Q_2)),$f6(Qa,Pa,G_1,P_2,Ca,Q_2)))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(Pa,Ca,Qa),bot_bo620288102e_bool))). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(P_2,Ca,Q_2),bot_bo620288102e_bool)))| -hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(P_2,Z_2),$f6(Qa,Pa,G_1,P_2,Ca,Q_2)))|hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(Q_2,Z_2),$f5(Qa,Pa,G_1,P_2,Ca,Q_2)))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(Pa,Ca,Qa),bot_bo620288102e_bool))). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(P_2,Ca,Q_2),bot_bo620288102e_bool)))| -hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(Qa,$f7(Qa,Pa,G_1,P_2,Ca,Q_2)),$f5(Qa,Pa,G_1,P_2,Ca,Q_2)))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(Pa,Ca,Qa),bot_bo620288102e_bool))). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),bot_bo620288102e_bool)). % 2.22/2.41 0 [] bot_bo620288102e_bool!=insert1415133716_state(A,A_1). % 2.22/2.41 0 [] insert1415133716_state(A,A_1)!=bot_bo620288102e_bool. % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,B_1),insert1415133716_state(A,bot_bo620288102e_bool)))|B_1=A. % 2.22/2.41 0 [] hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,B_1),insert1415133716_state(A,bot_bo620288102e_bool)))|B_1!=A. % 2.22/2.41 0 [] insert1415133716_state(A,insert1415133716_state(B_1,bot_bo620288102e_bool))!=insert1415133716_state(Ca,insert1415133716_state(D,bot_bo620288102e_bool))|A=Ca|A=D. % 2.22/2.41 0 [] insert1415133716_state(A,insert1415133716_state(B_1,bot_bo620288102e_bool))!=insert1415133716_state(Ca,insert1415133716_state(D,bot_bo620288102e_bool))|A=Ca|B_1=Ca. % 2.22/2.41 0 [] insert1415133716_state(A,insert1415133716_state(B_1,bot_bo620288102e_bool))!=insert1415133716_state(Ca,insert1415133716_state(D,bot_bo620288102e_bool))|B_1=D|A=D. % 2.22/2.41 0 [] insert1415133716_state(A,insert1415133716_state(B_1,bot_bo620288102e_bool))!=insert1415133716_state(Ca,insert1415133716_state(D,bot_bo620288102e_bool))|B_1=D|B_1=Ca. % 2.22/2.41 0 [] insert1415133716_state(A,insert1415133716_state(B_1,bot_bo620288102e_bool))=insert1415133716_state(Ca,insert1415133716_state(D,bot_bo620288102e_bool))|A!=Ca|B_1!=D. % 2.22/2.41 0 [] insert1415133716_state(A,insert1415133716_state(B_1,bot_bo620288102e_bool))=insert1415133716_state(Ca,insert1415133716_state(D,bot_bo620288102e_bool))|A!=D|B_1!=Ca. % 2.22/2.41 0 [] A_1!=bot_bo620288102e_bool| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),A_1)). % 2.22/2.41 0 [] collec307967673_state(Pa)!=bot_bo620288102e_bool| -hBOOL(hAPP_H78829294e_bool(Pa,X_2)). % 2.22/2.41 0 [] collec307967673_state(Pa)=bot_bo620288102e_bool|hBOOL(hAPP_H78829294e_bool(Pa,$f8(Pa))). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,Ca),bot_bo620288102e_bool)). % 2.22/2.41 0 [] bot_bo620288102e_bool!=collec307967673_state(Pa)| -hBOOL(hAPP_H78829294e_bool(Pa,X_2)). % 2.22/2.41 0 [] bot_bo620288102e_bool=collec307967673_state(Pa)|hBOOL(hAPP_H78829294e_bool(Pa,$f9(Pa))). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_2),A_1))|A_1!=bot_bo620288102e_bool. % 2.22/2.41 0 [] hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,$f10(A_1)),A_1))|A_1=bot_bo620288102e_bool. % 2.22/2.41 0 [] hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,$f11(A_1)),A_1))|A_1=bot_bo620288102e_bool. % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_2),A_1))|A_1!=bot_bo620288102e_bool. % 2.22/2.41 0 [] bot_bo620288102e_bool=collec307967673_state(cOMBK_659609255_state(fFalse)). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),A_1))|insert1415133716_state(A,A_1)=A_1. % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),B))|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),insert1415133716_state(B_1,B))). % 2.22/2.41 0 [] hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_1),A_1))|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_1),B))|insert1415133716_state(X_1,A_1)!=insert1415133716_state(X_1,B)|A_1=B. % 2.22/2.41 0 [] hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_1),A_1))|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_1),B))|insert1415133716_state(X_1,A_1)=insert1415133716_state(X_1,B)|A_1!=B. % 2.22/2.41 0 [] -hBOOL(hAPP_H78829294e_bool(insert1415133716_state(Y_2,A_1),X_1))|Y_2=X_1|hBOOL(hAPP_H78829294e_bool(A_1,X_1)). % 2.22/2.41 0 [] hBOOL(hAPP_H78829294e_bool(insert1415133716_state(Y_2,A_1),X_1))|Y_2!=X_1. % 2.22/2.41 0 [] hBOOL(hAPP_H78829294e_bool(insert1415133716_state(Y_2,A_1),X_1))| -hBOOL(hAPP_H78829294e_bool(A_1,X_1)). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),insert1415133716_state(B_1,A_1)))|A=B_1|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),A_1)). % 2.22/2.41 0 [] hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),insert1415133716_state(B_1,A_1)))|A!=B_1. % 2.22/2.41 0 [] hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),insert1415133716_state(B_1,A_1)))| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),A_1)). % 2.22/2.41 0 [] insert1415133716_state(X_1,insert1415133716_state(Y_2,A_1))=insert1415133716_state(Y_2,insert1415133716_state(X_1,A_1)). % 2.22/2.41 0 [] insert1415133716_state(X_1,insert1415133716_state(X_1,A_1))=insert1415133716_state(X_1,A_1). % 2.22/2.41 0 [] insert1415133716_state(A,collec307967673_state(Pa))=collec307967673_state(cOMBS_458705923l_bool(cOMBB_962198420_state(fimplies,cOMBB_2144135922_state(fNot,cOMBC_654211620e_bool(fe_qual1111551311_state,A))),Pa)). % 2.22/2.41 0 [] insert1415133716_state(A,B)=collec307967673_state(cOMBS_458705923l_bool(cOMBB_962198420_state(fdisj,cOMBC_654211620e_bool(fe_qual1111551311_state,A)),cOMBC_1734175330l_bool(member1338687867_state,B))). % 2.22/2.41 0 [] hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),insert1415133716_state(A,B))). % 2.22/2.41 0 [] insert1415133716_state(A,bot_bo620288102e_bool)!=insert1415133716_state(B_1,bot_bo620288102e_bool)|A=B_1. % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,B_1),insert1415133716_state(A,bot_bo620288102e_bool)))|B_1=A. % 2.22/2.41 0 [] hAPP_f1387463497_state(the_el1751439279_state,insert1415133716_state(X_1,bot_bo620288102e_bool))=X_1. % 2.22/2.41 0 [] -hBOOL(hAPP_H78829294e_bool(bot_bo620288102e_bool,X_1))|hBOOL(bot_bot_bool). % 2.22/2.41 0 [] hBOOL(hAPP_H78829294e_bool(bot_bo620288102e_bool,X_1))| -hBOOL(bot_bot_bool). % 2.22/2.41 0 [] -hBOOL(hAPP_H78829294e_bool(bot_bo620288102e_bool,X_2))|hBOOL(bot_bot_bool). % 2.22/2.41 0 [] hBOOL(hAPP_H78829294e_bool(bot_bo620288102e_bool,X_2))| -hBOOL(bot_bot_bool). % 2.22/2.41 0 [] hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(Pa,skip,Pa),bot_bo620288102e_bool))). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(Pa,Ca,Qa),bot_bo620288102e_bool)))| -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(Qa,D,R_1),bot_bo620288102e_bool)))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(Pa,semi(Ca,D),R_1),bot_bo620288102e_bool))). % 2.22/2.41 0 [] Y_2=hoare_2082236334_state($f14(Y_2),$f13(Y_2),$f12(Y_2)). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_1),A_1))|A_1=insert1415133716_state(X_1,$f15(X_1,A_1)). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_1),A_1))| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_1),$f15(X_1,A_1))). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),A_1))|A_1=insert1415133716_state(A,$f16(A,A_1)). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),A_1))| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),$f16(A,A_1))). % 2.22/2.41 0 [] semi(Com1_2,Com2_2)!=skip. % 2.22/2.41 0 [] skip!=semi(Com1_2,Com2_2). % 2.22/2.41 0 [] hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,$f17(A_1)),A_1))|A_1=bot_bo620288102e_bool. % 2.22/2.41 0 [] hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(Pa,$f20(Qa,G_1,Ca,Pa)),$f19(Qa,G_1,Ca,Pa)))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(Pa,Ca,Qa),bot_bo620288102e_bool))). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(P_1,Ca,Q_1),bot_bo620288102e_bool)))| -hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(P_1,Z_2),$f19(Qa,G_1,Ca,Pa)))|hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(Q_1,Z_2),$f18(Qa,G_1,Ca,Pa,P_1,Q_1)))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(Pa,Ca,Qa),bot_bo620288102e_bool))). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(P_1,Ca,Q_1),bot_bo620288102e_bool)))| -hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(Qa,$f20(Qa,G_1,Ca,Pa)),$f18(Qa,G_1,Ca,Pa,P_1,Q_1)))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(G_1),insert1415133716_state(hoare_2082236334_state(Pa,Ca,Qa),bot_bo620288102e_bool))). % 2.22/2.41 0 [] semi(Com1_1,Com2_1)!=semi(Com1,Com2)|Com1_1=Com1. % 2.22/2.41 0 [] semi(Com1_1,Com2_1)!=semi(Com1,Com2)|Com2_1=Com2. % 2.22/2.41 0 [] semi(Com1_1,Com2_1)=semi(Com1,Com2)|Com1_1!=Com1|Com2_1!=Com2. % 2.22/2.41 0 [] A_1=bot_bo620288102e_bool|A_1=insert1415133716_state($f22(A_1),$f21(A_1)). % 2.22/2.41 0 [] A_1=bot_bo620288102e_bool| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,$f22(A_1)),$f21(A_1))). % 2.22/2.41 0 [] A_1!=bot_bo620288102e_bool|A_1!=insert1415133716_state(X_2,B_2)|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_2),B_2)). % 2.22/2.41 0 [] -hBOOL(hAPP_H78829294e_bool(bot_bo620288102e_bool,X_2))|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_2),bot_bo620288102e_bool)). % 2.22/2.41 0 [] hBOOL(hAPP_H78829294e_bool(bot_bo620288102e_bool,X_2))| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_2),bot_bo620288102e_bool)). % 2.22/2.41 0 [] -hBOOL(hAPP_H78829294e_bool(finite1736999486_state(F_1,insert1415133716_state(A,bot_bo620288102e_bool)),B_1))|A=B_1. % 2.22/2.41 0 [] hBOOL(hAPP_H78829294e_bool(finite1736999486_state(F_1,insert1415133716_state(A,bot_bo620288102e_bool)),B_1))|A!=B_1. % 2.22/2.41 0 [] -hBOOL(finite354701905_state(F_1,F))|hAPP_f1387463497_state(F,insert1415133716_state(X_1,bot_bo620288102e_bool))=X_1. % 2.22/2.41 0 [] hAPP_f1387463497_state(finite926392750_state(F_1),insert1415133716_state(A,bot_bo620288102e_bool))=A. % 2.22/2.41 0 [] G!=finite926392750_state(F_1)|hAPP_f1387463497_state(G,insert1415133716_state(A,bot_bo620288102e_bool))=A. % 2.22/2.41 0 [] -hBOOL(hAPP_H78829294e_bool(finite1736999486_state(F_1,bot_bo620288102e_bool),X_1)). % 2.22/2.41 0 [] -hBOOL(hAPP_H78829294e_bool(finite1736999486_state(F_1,A_1),X_1))|A_1!=bot_bo620288102e_bool. % 2.22/2.41 0 [] -hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,A,A_1),X_1))|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),A_1))|hBOOL(hAPP_H78829294e_bool(finite1736999486_state(F_1,insert1415133716_state(A,A_1)),X_1)). % 2.22/2.41 0 [] -hBOOL(finite354701905_state(F_1,F))| -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A_1))|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_1),A_1))|A_1=bot_bo620288102e_bool|hAPP_f1387463497_state(F,insert1415133716_state(X_1,A_1))=hAPP_H1150764575_state(hAPP_H1855735728_state(F_1,X_1),hAPP_f1387463497_state(F,A_1)). % 2.22/2.41 0 [] -hBOOL(finite354701905_state(F_1,F))| -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A_1))|hAPP_f1387463497_state(F,A_1)=hAPP_f1387463497_state(finite926392750_state(F_1),A_1). % 2.22/2.41 0 [] hBOOL(hAPP_f971112728l_bool(finite364844667_state,bot_bo620288102e_bool)). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A_1))|hBOOL(hAPP_f971112728l_bool(finite364844667_state,insert1415133716_state(A,A_1))). % 2.22/2.41 0 [] hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,Z,bot_bo620288102e_bool),Z)). % 2.22/2.41 0 [] -hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,Z,bot_bo620288102e_bool),X_1))|X_1=Z. % 2.22/2.41 0 [] hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_1),A_1))| -hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,Z,A_1),Y_2))|hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,Z,insert1415133716_state(X_1,A_1)),hAPP_H1150764575_state(hAPP_H1855735728_state(F_1,X_1),Y_2))). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,insert1415133716_state(A,A_1)))|hBOOL(hAPP_f971112728l_bool(finite364844667_state,A_1)). % 2.22/2.41 0 [] hBOOL(hAPP_f971112728l_bool(finite364844667_state,insert1415133716_state(A,A_1)))| -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A_1)). % 2.22/2.41 0 [] -hBOOL(finite354701905_state(F_1,F))| -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A_1))|A_1=bot_bo620288102e_bool| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,hAPP_H1150764575_state(hAPP_H1855735728_state(F_1,$f24(A_1,F_1,F)),$f23(A_1,F_1,F))),insert1415133716_state($f24(A_1,F_1,F),insert1415133716_state($f23(A_1,F_1,F),bot_bo620288102e_bool))))|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,hAPP_f1387463497_state(F,A_1)),A_1)). % 2.22/2.41 0 [] -hBOOL(hAPP_H78829294e_bool(finite1736999486_state(F_1,insert1415133716_state(A,X_3)),X_1))|insert1415133716_state(A,X_3)=insert1415133716_state($f26(F_1,A,X_3,X_1),$f25(F_1,A,X_3,X_1)). % 2.22/2.41 0 [] -hBOOL(hAPP_H78829294e_bool(finite1736999486_state(F_1,insert1415133716_state(A,X_3)),X_1))|hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,$f26(F_1,A,X_3,X_1),$f25(F_1,A,X_3,X_1)),X_1)). % 2.22/2.41 0 [] -hBOOL(hAPP_H78829294e_bool(finite1736999486_state(F_1,insert1415133716_state(A,X_3)),X_1))| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,$f26(F_1,A,X_3,X_1)),$f25(F_1,A,X_3,X_1))). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A_1))|A_1=bot_bo620288102e_bool|hBOOL(hAPP_H78829294e_bool(finite1736999486_state(F_1,A_1),$f27(F_1,A_1))). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,F))| -hBOOL(hAPP_f971112728l_bool(Pa,bot_bo620288102e_bool))|hBOOL(hAPP_f971112728l_bool(finite364844667_state,$f28(Pa,F)))|hBOOL(hAPP_f971112728l_bool(Pa,F)). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,F))| -hBOOL(hAPP_f971112728l_bool(Pa,bot_bo620288102e_bool))| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,$f29(Pa,F)),$f28(Pa,F)))|hBOOL(hAPP_f971112728l_bool(Pa,F)). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,F))| -hBOOL(hAPP_f971112728l_bool(Pa,bot_bo620288102e_bool))|hBOOL(hAPP_f971112728l_bool(Pa,$f28(Pa,F)))|hBOOL(hAPP_f971112728l_bool(Pa,F)). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,F))| -hBOOL(hAPP_f971112728l_bool(Pa,bot_bo620288102e_bool))| -hBOOL(hAPP_f971112728l_bool(Pa,insert1415133716_state($f29(Pa,F),$f28(Pa,F))))|hBOOL(hAPP_f971112728l_bool(Pa,F)). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_1),A_1))|hBOOL(hAPP_H78829294e_bool(A_1,X_1)). % 2.22/2.41 0 [] hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_1),A_1))| -hBOOL(hAPP_H78829294e_bool(A_1,X_1)). % 2.22/2.41 0 [] collec307967673_state(Pa)=Pa. % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A))|A=bot_bo620288102e_bool|A=insert1415133716_state($f30(A),$f31(A)). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A))|A=bot_bo620288102e_bool|hBOOL(hAPP_f971112728l_bool(finite364844667_state,$f31(A))). % 2.22/2.41 0 [] hBOOL(hAPP_f971112728l_bool(finite364844667_state,A))|A!=bot_bo620288102e_bool. % 2.22/2.41 0 [] hBOOL(hAPP_f971112728l_bool(finite364844667_state,A))|A!=insert1415133716_state(A_3,A_2)| -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A_2)). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A_1))|hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,Z,A_1),$f32(F_1,Z,A_1))). % 2.22/2.41 0 [] -hBOOL(hAPP_H78829294e_bool(finite1736999486_state(F_1,A1),A2))|A1=insert1415133716_state($f35(F_1,A1,A2),$f34(F_1,A1,A2)). % 2.22/2.41 0 [] -hBOOL(hAPP_H78829294e_bool(finite1736999486_state(F_1,A1),A2))|A2=$f33(F_1,A1,A2). % 2.22/2.41 0 [] -hBOOL(hAPP_H78829294e_bool(finite1736999486_state(F_1,A1),A2))|hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,$f35(F_1,A1,A2),$f34(F_1,A1,A2)),$f33(F_1,A1,A2))). % 2.22/2.41 0 [] -hBOOL(hAPP_H78829294e_bool(finite1736999486_state(F_1,A1),A2))| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,$f35(F_1,A1,A2)),$f34(F_1,A1,A2))). % 2.22/2.41 0 [] hBOOL(hAPP_H78829294e_bool(finite1736999486_state(F_1,A1),A2))|A1!=insert1415133716_state(A_3,A_2)|A2!=X_2| -hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,A_3,A_2),X_2))|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A_3),A_2)). % 2.22/2.41 0 [] -hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,Z,A1),A2))|A1=bot_bo620288102e_bool|A1=insert1415133716_state($f38(F_1,Z,A1,A2),$f37(F_1,Z,A1,A2)). % 2.22/2.41 0 [] -hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,Z,A1),A2))|A1=bot_bo620288102e_bool|A2=hAPP_H1150764575_state(hAPP_H1855735728_state(F_1,$f38(F_1,Z,A1,A2)),$f36(F_1,Z,A1,A2)). % 2.22/2.41 0 [] -hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,Z,A1),A2))|A1=bot_bo620288102e_bool| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,$f38(F_1,Z,A1,A2)),$f37(F_1,Z,A1,A2))). % 2.22/2.41 0 [] -hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,Z,A1),A2))|A1=bot_bo620288102e_bool|hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,Z,$f37(F_1,Z,A1,A2)),$f36(F_1,Z,A1,A2))). % 2.22/2.41 0 [] -hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,Z,A1),A2))|A2=Z|A1=insert1415133716_state($f38(F_1,Z,A1,A2),$f37(F_1,Z,A1,A2)). % 2.22/2.41 0 [] -hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,Z,A1),A2))|A2=Z|A2=hAPP_H1150764575_state(hAPP_H1855735728_state(F_1,$f38(F_1,Z,A1,A2)),$f36(F_1,Z,A1,A2)). % 2.22/2.41 0 [] -hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,Z,A1),A2))|A2=Z| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,$f38(F_1,Z,A1,A2)),$f37(F_1,Z,A1,A2))). % 2.22/2.41 0 [] -hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,Z,A1),A2))|A2=Z|hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,Z,$f37(F_1,Z,A1,A2)),$f36(F_1,Z,A1,A2))). % 2.22/2.41 0 [] hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,Z,A1),A2))|A1!=bot_bo620288102e_bool|A2!=Z. % 2.22/2.41 0 [] hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,Z,A1),A2))|A1!=insert1415133716_state(X_2,A_2)|A2!=hAPP_H1150764575_state(hAPP_H1855735728_state(F_1,X_2),Y_1)|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_2),A_2))| -hBOOL(hAPP_H78829294e_bool(finite374952848_state(F_1,Z,A_2),Y_1)). % 2.22/2.41 0 [] -hBOOL(finite86813460_state(F_1,F))| -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A_1))|A_1=bot_bo620288102e_bool|hAPP_f1387463497_state(F,insert1415133716_state(X_1,A_1))=hAPP_H1150764575_state(hAPP_H1855735728_state(F_1,X_1),hAPP_f1387463497_state(F,A_1)). % 2.22/2.41 0 [] -hBOOL(finite86813460_state(F_1,F))|hAPP_H1150764575_state(hAPP_H1855735728_state(F_1,X_1),X_1)=X_1. % 2.22/2.41 0 [] -hBOOL(finite86813460_state(F_1,F))| -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A_1))| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_1),A_1))|hAPP_H1150764575_state(hAPP_H1855735728_state(F_1,X_1),hAPP_f1387463497_state(F,A_1))=hAPP_f1387463497_state(F,A_1). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,F))|F=bot_bo620288102e_bool| -hBOOL(hAPP_f971112728l_bool(Pa,insert1415133716_state($f39(Pa,F),bot_bo620288102e_bool)))|hBOOL(hAPP_f971112728l_bool(finite364844667_state,$f40(Pa,F)))|hBOOL(hAPP_f971112728l_bool(Pa,F)). % 2.22/2.41 0 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,F))|F=bot_bo620288102e_bool| -hBOOL(hAPP_f971112728l_bool(Pa,insert1415133716_state($f39(Pa,F),bot_bo620288102e_bool)))|$f40(Pa,F)!=bot_bo620288102e_bool|hBOOL(hAPP_f971112728l_bool(Pa,F)). % 2.22/2.42 0 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,F))|F=bot_bo620288102e_bool| -hBOOL(hAPP_f971112728l_bool(Pa,insert1415133716_state($f39(Pa,F),bot_bo620288102e_bool)))| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,$f41(Pa,F)),$f40(Pa,F)))|hBOOL(hAPP_f971112728l_bool(Pa,F)). % 2.22/2.42 0 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,F))|F=bot_bo620288102e_bool| -hBOOL(hAPP_f971112728l_bool(Pa,insert1415133716_state($f39(Pa,F),bot_bo620288102e_bool)))|hBOOL(hAPP_f971112728l_bool(Pa,$f40(Pa,F)))|hBOOL(hAPP_f971112728l_bool(Pa,F)). % 2.22/2.42 0 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,F))|F=bot_bo620288102e_bool| -hBOOL(hAPP_f971112728l_bool(Pa,insert1415133716_state($f39(Pa,F),bot_bo620288102e_bool)))| -hBOOL(hAPP_f971112728l_bool(Pa,insert1415133716_state($f41(Pa,F),$f40(Pa,F))))|hBOOL(hAPP_f971112728l_bool(Pa,F)). % 2.22/2.42 0 [] -hBOOL(big_se883361720_state(F_1,F))| -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A_1))|hAPP_f1387463497_state(F,A_1)=hAPP_f1387463497_state(finite926392750_state(F_1),A_1). % 2.22/2.42 0 [] -hBOOL(finite354701905_state(F_1,F))| -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A_1))| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_1),A_1))|minus_1641527009e_bool(A_1,insert1415133716_state(X_1,bot_bo620288102e_bool))!=bot_bo620288102e_bool|hAPP_f1387463497_state(F,A_1)=X_1. % 2.22/2.42 0 [] -hBOOL(finite354701905_state(F_1,F))| -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A_1))| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_1),A_1))|minus_1641527009e_bool(A_1,insert1415133716_state(X_1,bot_bo620288102e_bool))=bot_bo620288102e_bool|hAPP_f1387463497_state(F,A_1)=hAPP_H1150764575_state(hAPP_H1855735728_state(F_1,X_1),hAPP_f1387463497_state(F,minus_1641527009e_bool(A_1,insert1415133716_state(X_1,bot_bo620288102e_bool)))). % 2.22/2.42 0 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,Ca),A_1))|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,Ca),B))|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,Ca),minus_1641527009e_bool(A_1,B))). % 2.22/2.42 0 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,Ca),minus_1641527009e_bool(A_1,B)))|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,Ca),A_1)). % 2.22/2.42 0 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,Ca),minus_1641527009e_bool(A_1,B)))| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,Ca),B)). % 2.22/2.42 0 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A_1))|hBOOL(hAPP_f971112728l_bool(finite364844667_state,minus_1641527009e_bool(A_1,B))). % 2.22/2.42 0 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),A_1))|insert1415133716_state(A,minus_1641527009e_bool(A_1,insert1415133716_state(A,bot_bo620288102e_bool)))=A_1. % 2.22/2.42 0 [] hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,X_1),A_1))|minus_1641527009e_bool(insert1415133716_state(X_1,A_1),insert1415133716_state(X_1,bot_bo620288102e_bool))=A_1. % 2.22/2.42 0 [] insert1415133716_state(A,minus_1641527009e_bool(A_1,insert1415133716_state(A,bot_bo620288102e_bool)))=insert1415133716_state(A,A_1). % 2.22/2.42 0 [] minus_1641527009e_bool(A_1,insert1415133716_state(A,B))=minus_1641527009e_bool(minus_1641527009e_bool(A_1,insert1415133716_state(A,bot_bo620288102e_bool)),B). % 2.22/2.42 0 [] minus_1641527009e_bool(A_1,insert1415133716_state(A,B))=minus_1641527009e_bool(minus_1641527009e_bool(A_1,B),insert1415133716_state(A,bot_bo620288102e_bool)). % 2.22/2.42 0 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,minus_1641527009e_bool(A_1,insert1415133716_state(A,B))))|hBOOL(hAPP_f971112728l_bool(finite364844667_state,minus_1641527009e_bool(A_1,B))). % 2.22/2.42 0 [] hBOOL(hAPP_f971112728l_bool(finite364844667_state,minus_1641527009e_bool(A_1,insert1415133716_state(A,B))))| -hBOOL(hAPP_f971112728l_bool(finite364844667_state,minus_1641527009e_bool(A_1,B))). % 2.22/2.42 0 [] -hBOOL(hAPP_bool_bool(fNot,P))| -hBOOL(P). % 2.22/2.42 0 [] hBOOL(P)|hBOOL(hAPP_bool_bool(fNot,P)). % 2.22/2.42 0 [] -hBOOL(P)|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(fdisj,P),Q)). % 2.22/2.42 0 [] -hBOOL(Q)|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(fdisj,P),Q)). % 2.22/2.42 0 [] -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(fdisj,P),Q))|hBOOL(P)|hBOOL(Q). % 2.22/2.42 0 [] -hBOOL(fFalse). % 2.22/2.42 0 [] -is_bool(P)|P=fTrue|P=fFalse. % 2.22/2.42 0 [] hBOOL(P)|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(fimplies,P),Q)). % 2.22/2.42 0 [] -hBOOL(Q)|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(fimplies,P),Q)). % 2.22/2.42 0 [] -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(fimplies,P),Q))| -hBOOL(P)|hBOOL(Q). % 2.22/2.42 0 [] -hBOOL(hAPP_H78829294e_bool(hAPP_H1049623551e_bool(fe_qual1111551311_state,X),Y))|X=Y. % 2.22/2.42 0 [] X!=Y|hBOOL(hAPP_H78829294e_bool(hAPP_H1049623551e_bool(fe_qual1111551311_state,X),Y)). % 2.22/2.42 0 [] -is_bool(P)|hAPP_H78829294e_bool(cOMBK_659609255_state(P),Q)=P. % 2.22/2.42 0 [] hAPP_H78829294e_bool(cOMBB_2144135922_state(P,Q),R)=hAPP_bool_bool(P,hAPP_H78829294e_bool(Q,R)). % 2.22/2.42 0 [] hAPP_H78829294e_bool(cOMBS_458705923l_bool(P,Q),R)=hAPP_bool_bool(hAPP_H1187982158l_bool(P,R),hAPP_H78829294e_bool(Q,R)). % 2.22/2.42 0 [] hAPP_H1187982158l_bool(cOMBB_962198420_state(P,Q),R)=hAPP_b589554111l_bool(P,hAPP_H78829294e_bool(Q,R)). % 2.22/2.42 0 [] hAPP_H78829294e_bool(cOMBC_654211620e_bool(P,Q),R)=hAPP_H78829294e_bool(hAPP_H1049623551e_bool(P,R),Q). % 2.22/2.42 0 [] hAPP_H78829294e_bool(cOMBC_1734175330l_bool(P,Q),R)=hAPP_f971112728l_bool(hAPP_H30606679l_bool(P,R),Q). % 2.22/2.42 0 [] hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(bot_bo620288102e_bool),insert1415133716_state(hoare_Mirabelle_MGT(c),bot_bo620288102e_bool))). % 2.22/2.42 0 [] hBOOL(hAPP_f971112728l_bool(hoare_2004700328_state(bot_bo620288102e_bool),insert1415133716_state(hoare_2082236334_state(p,c,q),bot_bo620288102e_bool))). % 2.22/2.42 0 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(bot_bo620288102e_bool),insert1415133716_state(hoare_2082236334_state(p,c,q),bot_bo620288102e_bool))). % 2.22/2.42 end_of_list. % 2.22/2.42 % 2.22/2.42 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=5. % 2.22/2.42 % 2.22/2.42 This ia a non-Horn set with equality. The strategy will be % 2.22/2.42 Knuth-Bendix, ordered hyper_res, factoring, and unit % 2.22/2.42 deletion, with positive clauses in sos and nonpositive % 2.22/2.42 clauses in usable. % 2.22/2.42 % 2.22/2.42 dependent: set(knuth_bendix). % 2.22/2.42 dependent: set(anl_eq). % 2.22/2.42 dependent: set(para_from). % 2.22/2.42 dependent: set(para_into). % 2.22/2.42 dependent: clear(para_from_right). % 2.22/2.42 dependent: clear(para_into_right). % 2.22/2.42 dependent: set(para_from_vars). % 2.22/2.42 dependent: set(eq_units_both_ways). % 2.22/2.42 dependent: set(dynamic_demod_all). % 2.22/2.42 dependent: set(dynamic_demod). % 2.22/2.42 dependent: set(order_eq). % 2.22/2.42 dependent: set(back_demod). % 2.22/2.42 dependent: set(lrpo). % 2.22/2.42 dependent: set(hyper_res). % 2.22/2.42 dependent: set(unit_deletion). % 2.22/2.42 dependent: set(factor). % 2.22/2.42 % 2.22/2.42 ------------> process usable: % 2.22/2.42 ** KEPT (pick-wt=6): 1 [] -is_bool(A)|is_bool(hAPP_bool_bool(B,A)). % 2.22/2.42 ** KEPT (pick-wt=12): 2 [] hoare_2082236334_state(A,B,C)!=hoare_2082236334_state(D,E,F)|A=D. % 2.22/2.42 ** KEPT (pick-wt=12): 3 [] hoare_2082236334_state(A,B,C)!=hoare_2082236334_state(D,E,F)|B=E. % 2.22/2.42 ** KEPT (pick-wt=12): 4 [] hoare_2082236334_state(A,B,C)!=hoare_2082236334_state(D,E,F)|C=F. % 2.22/2.42 ** KEPT (pick-wt=18): 5 [] hoare_2082236334_state(A,B,C)=hoare_2082236334_state(D,E,F)|A!=D|B!=E|C!=F. % 2.22/2.42 ** KEPT (pick-wt=10): 6 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),B))|hBOOL(hAPP_f971112728l_bool(hoare_2004700328_state(A),B)). % 2.22/2.42 ** KEPT (pick-wt=15): 7 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),B))| -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(C),A))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(C),B)). % 2.22/2.42 ** KEPT (pick-wt=19): 8 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),insert1415133716_state(B,bot_bo620288102e_bool)))| -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),C))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),insert1415133716_state(B,C))). % 2.22/2.42 ** KEPT (pick-wt=14): 9 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),insert1415133716_state(B,C)))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),insert1415133716_state(B,bot_bo620288102e_bool))). % 2.22/2.42 ** KEPT (pick-wt=12): 10 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),insert1415133716_state(B,C)))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),C)). % 2.22/2.42 ** KEPT (pick-wt=36): 11 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),insert1415133716_state(hoare_2082236334_state(B,C,D),bot_bo620288102e_bool)))|hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(D,$f2(E,A,B,C,D)),$f1(E,A,B,C,D)))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),insert1415133716_state(hoare_2082236334_state(B,C,E),bot_bo620288102e_bool))). % 2.22/2.42 ** KEPT (pick-wt=36): 12 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),insert1415133716_state(hoare_2082236334_state(B,C,D),bot_bo620288102e_bool)))| -hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(E,$f2(E,A,B,C,D)),$f1(E,A,B,C,D)))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),insert1415133716_state(hoare_2082236334_state(B,C,E),bot_bo620288102e_bool))). % 2.22/2.42 ** KEPT (pick-wt=36): 13 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),insert1415133716_state(hoare_2082236334_state(B,C,D),bot_bo620288102e_bool)))|hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(E,$f4(E,A,B,C,D)),$f3(E,A,B,C,D)))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),insert1415133716_state(hoare_2082236334_state(E,C,D),bot_bo620288102e_bool))). % 2.22/2.42 ** KEPT (pick-wt=36): 14 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),insert1415133716_state(hoare_2082236334_state(B,C,D),bot_bo620288102e_bool)))| -hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(B,$f4(E,A,B,C,D)),$f3(E,A,B,C,D)))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),insert1415133716_state(hoare_2082236334_state(E,C,D),bot_bo620288102e_bool))). % 2.22/2.42 ** KEPT (pick-wt=17): 15 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),insert1415133716_state(B,C)))|A=B|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),C)). % 2.22/2.42 ** KEPT (pick-wt=14): 16 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),B))|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),insert1415133716_state(C,B))). % 2.22/2.42 ** KEPT (pick-wt=11): 17 [] A!=B|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),insert1415133716_state(B,C))). % 2.22/2.42 ** KEPT (pick-wt=38): 18 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),insert1415133716_state(hoare_2082236334_state(B,C,D),bot_bo620288102e_bool)))|hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(E,$f7(F,E,A,B,C,D)),$f6(F,E,A,B,C,D)))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),insert1415133716_state(hoare_2082236334_state(E,C,F),bot_bo620288102e_bool))). % 2.22/2.42 ** KEPT (pick-wt=44): 19 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),insert1415133716_state(hoare_2082236334_state(B,C,D),bot_bo620288102e_bool)))| -hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(B,E),$f6(F,G,A,B,C,D)))|hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(D,E),$f5(F,G,A,B,C,D)))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),insert1415133716_state(hoare_2082236334_state(G,C,F),bot_bo620288102e_bool))). % 2.22/2.42 ** KEPT (pick-wt=38): 20 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),insert1415133716_state(hoare_2082236334_state(B,C,D),bot_bo620288102e_bool)))| -hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(E,$f7(E,F,A,B,C,D)),$f5(E,F,A,B,C,D)))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),insert1415133716_state(hoare_2082236334_state(F,C,E),bot_bo620288102e_bool))). % 2.22/2.42 ** KEPT (pick-wt=6): 21 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),bot_bo620288102e_bool)). % 2.22/2.42 ** KEPT (pick-wt=5): 23 [copy,22,flip.1] insert1415133716_state(A,B)!=bot_bo620288102e_bool. % 2.22/2.42 Following clause subsumed by 23 during input processing: 0 [] insert1415133716_state(A,B)!=bot_bo620288102e_bool. % 2.22/2.42 ** KEPT (pick-wt=11): 24 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),insert1415133716_state(B,bot_bo620288102e_bool)))|A=B. % 2.22/2.42 Following clause subsumed by 17 during input processing: 0 [] hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),insert1415133716_state(B,bot_bo620288102e_bool)))|A!=B. % 2.22/2.42 ** KEPT (pick-wt=17): 25 [] insert1415133716_state(A,insert1415133716_state(B,bot_bo620288102e_bool))!=insert1415133716_state(C,insert1415133716_state(D,bot_bo620288102e_bool))|A=C|A=D. % 2.22/2.42 ** KEPT (pick-wt=17): 26 [] insert1415133716_state(A,insert1415133716_state(B,bot_bo620288102e_bool))!=insert1415133716_state(C,insert1415133716_state(D,bot_bo620288102e_bool))|A=C|B=C. % 2.22/2.42 ** KEPT (pick-wt=17): 27 [] insert1415133716_state(A,insert1415133716_state(B,bot_bo620288102e_bool))!=insert1415133716_state(C,insert1415133716_state(D,bot_bo620288102e_bool))|B=D|A=D. % 2.22/2.42 ** KEPT (pick-wt=17): 28 [] insert1415133716_state(A,insert1415133716_state(B,bot_bo620288102e_bool))!=insert1415133716_state(C,insert1415133716_state(D,bot_bo620288102e_bool))|B=D|B=C. % 2.22/2.42 ** KEPT (pick-wt=17): 29 [] insert1415133716_state(A,insert1415133716_state(B,bot_bo620288102e_bool))=insert1415133716_state(C,insert1415133716_state(D,bot_bo620288102e_bool))|A!=C|B!=D. % 2.22/2.42 ** KEPT (pick-wt=17): 30 [] insert1415133716_state(A,insert1415133716_state(B,bot_bo620288102e_bool))=insert1415133716_state(C,insert1415133716_state(D,bot_bo620288102e_bool))|A!=D|B!=C. % 2.22/2.42 ** KEPT (pick-wt=9): 31 [] A!=bot_bo620288102e_bool| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,B),A)). % 2.22/2.42 ** KEPT (pick-wt=8): 32 [] collec307967673_state(A)!=bot_bo620288102e_bool| -hBOOL(hAPP_H78829294e_bool(A,B)). % 2.22/2.42 Following clause subsumed by 21 during input processing: 0 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),bot_bo620288102e_bool)). % 2.22/2.42 Following clause subsumed by 32 during input processing: 0 [flip.1] collec307967673_state(A)!=bot_bo620288102e_bool| -hBOOL(hAPP_H78829294e_bool(A,B)). % 2.22/2.42 Following clause subsumed by 31 during input processing: 0 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),B))|B!=bot_bo620288102e_bool. % 2.22/2.42 Following clause subsumed by 31 during input processing: 0 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),B))|B!=bot_bo620288102e_bool. % 2.22/2.42 ** KEPT (pick-wt=11): 33 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),B))|insert1415133716_state(A,B)=B. % 2.22/2.42 Following clause subsumed by 16 during input processing: 0 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),B))|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),insert1415133716_state(C,B))). % 2.22/2.42 ** KEPT (pick-wt=22): 34 [] hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),B))|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),C))|insert1415133716_state(A,B)!=insert1415133716_state(A,C)|B=C. % 2.22/2.42 ** KEPT (pick-wt=22): 35 [] hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),B))|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),C))|insert1415133716_state(A,B)=insert1415133716_state(A,C)|B!=C. % 2.22/2.42 ** KEPT (pick-wt=13): 36 [] -hBOOL(hAPP_H78829294e_bool(insert1415133716_state(A,B),C))|A=C|hBOOL(hAPP_H78829294e_bool(B,C)). % 2.22/2.42 ** KEPT (pick-wt=9): 37 [] hBOOL(hAPP_H78829294e_bool(insert1415133716_state(A,B),C))|A!=C. % 2.22/2.42 ** KEPT (pick-wt=10): 38 [] hBOOL(hAPP_H78829294e_bool(insert1415133716_state(A,B),C))| -hBOOL(hAPP_H78829294e_bool(B,C)). % 2.22/2.42 Following clause subsumed by 15 during input processing: 0 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),insert1415133716_state(B,C)))|A=B|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),C)). % 2.22/2.42 Following clause subsumed by 17 during input processing: 0 [] hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),insert1415133716_state(B,C)))|A!=B. % 2.22/2.42 Following clause subsumed by 16 during input processing: 0 [] hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),insert1415133716_state(B,C)))| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),C)). % 2.22/2.42 ** KEPT (pick-wt=10): 39 [] insert1415133716_state(A,bot_bo620288102e_bool)!=insert1415133716_state(B,bot_bo620288102e_bool)|A=B. % 2.22/2.42 Following clause subsumed by 24 during input processing: 0 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),insert1415133716_state(B,bot_bo620288102e_bool)))|A=B. % 2.22/2.42 ** KEPT (pick-wt=6): 40 [] -hBOOL(hAPP_H78829294e_bool(bot_bo620288102e_bool,A))|hBOOL(bot_bot_bool). % 2.22/2.42 ** KEPT (pick-wt=6): 41 [] hBOOL(hAPP_H78829294e_bool(bot_bo620288102e_bool,A))| -hBOOL(bot_bot_bool). % 2.22/2.42 Following clause subsumed by 40 during input processing: 0 [] -hBOOL(hAPP_H78829294e_bool(bot_bo620288102e_bool,A))|hBOOL(bot_bot_bool). % 2.22/2.42 Following clause subsumed by 41 during input processing: 0 [] hBOOL(hAPP_H78829294e_bool(bot_bo620288102e_bool,A))| -hBOOL(bot_bot_bool). % 2.22/2.42 ** KEPT (pick-wt=32): 42 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),insert1415133716_state(hoare_2082236334_state(B,C,D),bot_bo620288102e_bool)))| -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),insert1415133716_state(hoare_2082236334_state(D,E,F),bot_bo620288102e_bool)))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),insert1415133716_state(hoare_2082236334_state(B,semi(C,E),F),bot_bo620288102e_bool))). % 2.22/2.42 ** KEPT (pick-wt=13): 44 [copy,43,flip.2] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),B))|insert1415133716_state(A,$f15(A,B))=B. % 2.22/2.42 ** KEPT (pick-wt=14): 45 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),B))| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),$f15(A,B))). % 2.22/2.42 ** KEPT (pick-wt=13): 47 [copy,46,flip.2] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),B))|insert1415133716_state(A,$f16(A,B))=B. % 2.22/2.42 ** KEPT (pick-wt=14): 48 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),B))| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),$f16(A,B))). % 2.22/2.42 ** KEPT (pick-wt=5): 49 [] semi(A,B)!=skip. % 2.22/2.42 Following clause subsumed by 49 during input processing: 0 [flip.1] semi(A,B)!=skip. % 2.22/2.42 ** KEPT (pick-wt=42): 50 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),insert1415133716_state(hoare_2082236334_state(B,C,D),bot_bo620288102e_bool)))| -hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(B,E),$f19(F,A,C,G)))|hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(D,E),$f18(F,A,C,G,B,D)))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),insert1415133716_state(hoare_2082236334_state(G,C,F),bot_bo620288102e_bool))). % 2.22/2.42 ** KEPT (pick-wt=36): 51 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),insert1415133716_state(hoare_2082236334_state(B,C,D),bot_bo620288102e_bool)))| -hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(E,$f20(E,A,C,F)),$f18(E,A,C,F,B,D)))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),insert1415133716_state(hoare_2082236334_state(F,C,E),bot_bo620288102e_bool))). % 2.22/2.42 ** KEPT (pick-wt=10): 52 [] semi(A,B)!=semi(C,D)|A=C. % 2.22/2.42 ** KEPT (pick-wt=10): 53 [] semi(A,B)!=semi(C,D)|B=D. % 2.22/2.42 ** KEPT (pick-wt=13): 54 [] semi(A,B)=semi(C,D)|A!=C|B!=D. % 2.22/2.42 ** KEPT (pick-wt=11): 55 [] A=bot_bo620288102e_bool| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,$f22(A)),$f21(A))). % 2.22/2.42 ** KEPT (pick-wt=14): 56 [] A!=bot_bo620288102e_bool|A!=insert1415133716_state(B,C)|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,B),C)). % 2.22/2.42 ** KEPT (pick-wt=4): 58 [copy,57,unit_del,21] -hBOOL(hAPP_H78829294e_bool(bot_bo620288102e_bool,A)). % 2.22/2.42 Following clause subsumed by 21 during input processing: 0 [unit_del,58] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),bot_bo620288102e_bool)). % 2.22/2.42 ** KEPT (pick-wt=11): 59 [] -hBOOL(hAPP_H78829294e_bool(finite1736999486_state(A,insert1415133716_state(B,bot_bo620288102e_bool)),C))|B=C. % 2.22/2.42 ** KEPT (pick-wt=11): 60 [] hBOOL(hAPP_H78829294e_bool(finite1736999486_state(A,insert1415133716_state(B,bot_bo620288102e_bool)),C))|B!=C. % 2.22/2.42 ** KEPT (pick-wt=11): 61 [] -hBOOL(finite354701905_state(A,B))|hAPP_f1387463497_state(B,insert1415133716_state(C,bot_bo620288102e_bool))=C. % 2.22/2.42 ** KEPT (pick-wt=11): 62 [] A!=finite926392750_state(B)|hAPP_f1387463497_state(A,insert1415133716_state(C,bot_bo620288102e_bool))=C. % 2.22/2.42 ** KEPT (pick-wt=6): 63 [] -hBOOL(hAPP_H78829294e_bool(finite1736999486_state(A,bot_bo620288102e_bool),B)). % 2.22/2.42 ** KEPT (pick-wt=9): 64 [] -hBOOL(hAPP_H78829294e_bool(finite1736999486_state(A,B),C))|B!=bot_bo620288102e_bool. % 2.22/2.42 ** KEPT (pick-wt=21): 65 [] -hBOOL(hAPP_H78829294e_bool(finite374952848_state(A,B,C),D))|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,B),C))|hBOOL(hAPP_H78829294e_bool(finite1736999486_state(A,insert1415133716_state(B,C)),D)). % 2.22/2.42 ** KEPT (pick-wt=30): 66 [] -hBOOL(finite354701905_state(A,B))| -hBOOL(hAPP_f971112728l_bool(finite364844667_state,C))|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,D),C))|C=bot_bo620288102e_bool|hAPP_f1387463497_state(B,insert1415133716_state(D,C))=hAPP_H1150764575_state(hAPP_H1855735728_state(A,D),hAPP_f1387463497_state(B,C)). % 2.22/2.42 ** KEPT (pick-wt=16): 67 [] -hBOOL(finite354701905_state(A,B))| -hBOOL(hAPP_f971112728l_bool(finite364844667_state,C))|hAPP_f1387463497_state(B,C)=hAPP_f1387463497_state(finite926392750_state(A),C). % 2.22/2.42 ** KEPT (pick-wt=10): 68 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A))|hBOOL(hAPP_f971112728l_bool(finite364844667_state,insert1415133716_state(B,A))). % 2.22/2.42 ** KEPT (pick-wt=10): 69 [] -hBOOL(hAPP_H78829294e_bool(finite374952848_state(A,B,bot_bo620288102e_bool),C))|C=B. % 2.22/2.42 ** KEPT (pick-wt=26): 70 [] hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),B))| -hBOOL(hAPP_H78829294e_bool(finite374952848_state(C,D,B),E))|hBOOL(hAPP_H78829294e_bool(finite374952848_state(C,D,insert1415133716_state(A,B)),hAPP_H1150764575_state(hAPP_H1855735728_state(C,A),E))). % 2.22/2.42 ** KEPT (pick-wt=10): 71 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,insert1415133716_state(A,B)))|hBOOL(hAPP_f971112728l_bool(finite364844667_state,B)). % 2.22/2.42 Following clause subsumed by 68 during input processing: 0 [] hBOOL(hAPP_f971112728l_bool(finite364844667_state,insert1415133716_state(A,B)))| -hBOOL(hAPP_f971112728l_bool(finite364844667_state,B)). % 2.22/2.42 ** KEPT (pick-wt=45): 72 [] -hBOOL(finite354701905_state(A,B))| -hBOOL(hAPP_f971112728l_bool(finite364844667_state,C))|C=bot_bo620288102e_bool| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,hAPP_H1150764575_state(hAPP_H1855735728_state(A,$f24(C,A,B)),$f23(C,A,B))),insert1415133716_state($f24(C,A,B),insert1415133716_state($f23(C,A,B),bot_bo620288102e_bool))))|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,hAPP_f1387463497_state(B,C)),C)). % 2.22/2.42 ** KEPT (pick-wt=23): 74 [copy,73,flip.2] -hBOOL(hAPP_H78829294e_bool(finite1736999486_state(A,insert1415133716_state(B,C)),D))|insert1415133716_state($f26(A,B,C,D),$f25(A,B,C,D))=insert1415133716_state(B,C). % 2.22/2.42 ** KEPT (pick-wt=23): 75 [] -hBOOL(hAPP_H78829294e_bool(finite1736999486_state(A,insert1415133716_state(B,C)),D))|hBOOL(hAPP_H78829294e_bool(finite374952848_state(A,$f26(A,B,C,D),$f25(A,B,C,D)),D)). % 2.22/2.42 ** KEPT (pick-wt=22): 76 [] -hBOOL(hAPP_H78829294e_bool(finite1736999486_state(A,insert1415133716_state(B,C)),D))| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,$f26(A,B,C,D)),$f25(A,B,C,D))). % 2.22/2.42 ** KEPT (pick-wt=15): 77 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A))|A=bot_bo620288102e_bool|hBOOL(hAPP_H78829294e_bool(finite1736999486_state(B,A),$f27(B,A))). % 2.22/2.42 ** KEPT (pick-wt=18): 78 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A))| -hBOOL(hAPP_f971112728l_bool(B,bot_bo620288102e_bool))|hBOOL(hAPP_f971112728l_bool(finite364844667_state,$f28(B,A)))|hBOOL(hAPP_f971112728l_bool(B,A)). % 2.22/2.42 ** KEPT (pick-wt=22): 79 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A))| -hBOOL(hAPP_f971112728l_bool(B,bot_bo620288102e_bool))| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,$f29(B,A)),$f28(B,A)))|hBOOL(hAPP_f971112728l_bool(B,A)). % 2.22/2.42 ** KEPT (pick-wt=18): 80 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A))| -hBOOL(hAPP_f971112728l_bool(B,bot_bo620288102e_bool))|hBOOL(hAPP_f971112728l_bool(B,$f28(B,A)))|hBOOL(hAPP_f971112728l_bool(B,A)). % 2.22/2.42 ** KEPT (pick-wt=22): 81 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A))| -hBOOL(hAPP_f971112728l_bool(B,bot_bo620288102e_bool))| -hBOOL(hAPP_f971112728l_bool(B,insert1415133716_state($f29(B,A),$f28(B,A))))|hBOOL(hAPP_f971112728l_bool(B,A)). % 2.22/2.42 ** KEPT (pick-wt=10): 82 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),B))|hBOOL(hAPP_H78829294e_bool(B,A)). % 2.22/2.42 ** KEPT (pick-wt=10): 83 [] hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),B))| -hBOOL(hAPP_H78829294e_bool(B,A)). % 2.22/2.42 ** KEPT (pick-wt=14): 85 [copy,84,flip.3] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A))|A=bot_bo620288102e_bool|insert1415133716_state($f30(A),$f31(A))=A. % 2.22/2.42 ** KEPT (pick-wt=12): 86 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A))|A=bot_bo620288102e_bool|hBOOL(hAPP_f971112728l_bool(finite364844667_state,$f31(A))). % 2.22/2.42 ** KEPT (pick-wt=7): 87 [] hBOOL(hAPP_f971112728l_bool(finite364844667_state,A))|A!=bot_bo620288102e_bool. % 2.22/2.42 ** KEPT (pick-wt=13): 88 [] hBOOL(hAPP_f971112728l_bool(finite364844667_state,A))|A!=insert1415133716_state(B,C)| -hBOOL(hAPP_f971112728l_bool(finite364844667_state,C)). % 2.22/2.42 ** KEPT (pick-wt=14): 89 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A))|hBOOL(hAPP_H78829294e_bool(finite374952848_state(B,C,A),$f32(B,C,A))). % 2.22/2.42 ** KEPT (pick-wt=17): 91 [copy,90,flip.2] -hBOOL(hAPP_H78829294e_bool(finite1736999486_state(A,B),C))|insert1415133716_state($f35(A,B,C),$f34(A,B,C))=B. % 2.22/2.42 ** KEPT (pick-wt=12): 93 [copy,92,flip.2] -hBOOL(hAPP_H78829294e_bool(finite1736999486_state(A,B),C))|$f33(A,B,C)=C. % 2.22/2.42 ** KEPT (pick-wt=22): 94 [] -hBOOL(hAPP_H78829294e_bool(finite1736999486_state(A,B),C))|hBOOL(hAPP_H78829294e_bool(finite374952848_state(A,$f35(A,B,C),$f34(A,B,C)),$f33(A,B,C))). % 2.22/2.42 ** KEPT (pick-wt=18): 95 [] -hBOOL(hAPP_H78829294e_bool(finite1736999486_state(A,B),C))| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,$f35(A,B,C)),$f34(A,B,C))). % 2.22/2.42 ** KEPT (pick-wt=27): 96 [] hBOOL(hAPP_H78829294e_bool(finite1736999486_state(A,B),C))|B!=insert1415133716_state(D,E)|C!=F| -hBOOL(hAPP_H78829294e_bool(finite374952848_state(A,D,E),F))|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,D),E)). % 2.22/2.42 ** KEPT (pick-wt=23): 98 [copy,97,flip.3] -hBOOL(hAPP_H78829294e_bool(finite374952848_state(A,B,C),D))|C=bot_bo620288102e_bool|insert1415133716_state($f38(A,B,C,D),$f37(A,B,C,D))=C. % 2.22/2.42 ** KEPT (pick-wt=25): 100 [copy,99,flip.3] -hBOOL(hAPP_H78829294e_bool(finite374952848_state(A,B,C),D))|C=bot_bo620288102e_bool|hAPP_H1150764575_state(hAPP_H1855735728_state(A,$f38(A,B,C,D)),$f36(A,B,C,D))=D. % 2.22/2.42 ** KEPT (pick-wt=24): 101 [] -hBOOL(hAPP_H78829294e_bool(finite374952848_state(A,B,C),D))|C=bot_bo620288102e_bool| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,$f38(A,B,C,D)),$f37(A,B,C,D))). % 2.22/2.42 ** KEPT (pick-wt=25): 102 [] -hBOOL(hAPP_H78829294e_bool(finite374952848_state(A,B,C),D))|C=bot_bo620288102e_bool|hBOOL(hAPP_H78829294e_bool(finite374952848_state(A,B,$f37(A,B,C,D)),$f36(A,B,C,D))). % 2.22/2.42 ** KEPT (pick-wt=23): 104 [copy,103,flip.3] -hBOOL(hAPP_H78829294e_bool(finite374952848_state(A,B,C),D))|D=B|insert1415133716_state($f38(A,B,C,D),$f37(A,B,C,D))=C. % 2.22/2.42 ** KEPT (pick-wt=25): 106 [copy,105,flip.3] -hBOOL(hAPP_H78829294e_bool(finite374952848_state(A,B,C),D))|D=B|hAPP_H1150764575_state(hAPP_H1855735728_state(A,$f38(A,B,C,D)),$f36(A,B,C,D))=D. % 2.22/2.42 ** KEPT (pick-wt=24): 107 [] -hBOOL(hAPP_H78829294e_bool(finite374952848_state(A,B,C),D))|D=B| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,$f38(A,B,C,D)),$f37(A,B,C,D))). % 2.22/2.42 ** KEPT (pick-wt=25): 108 [] -hBOOL(hAPP_H78829294e_bool(finite374952848_state(A,B,C),D))|D=B|hBOOL(hAPP_H78829294e_bool(finite374952848_state(A,B,$f37(A,B,C,D)),$f36(A,B,C,D))). % 2.22/2.42 ** KEPT (pick-wt=13): 109 [] hBOOL(hAPP_H78829294e_bool(finite374952848_state(A,B,C),D))|C!=bot_bo620288102e_bool|D!=B. % 2.22/2.42 ** KEPT (pick-wt=32): 110 [] hBOOL(hAPP_H78829294e_bool(finite374952848_state(A,B,C),D))|C!=insert1415133716_state(E,F)|D!=hAPP_H1150764575_state(hAPP_H1855735728_state(A,E),G)|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,E),F))| -hBOOL(hAPP_H78829294e_bool(finite374952848_state(A,B,F),G)). % 2.22/2.42 ** KEPT (pick-wt=24): 111 [] -hBOOL(finite86813460_state(A,B))| -hBOOL(hAPP_f971112728l_bool(finite364844667_state,C))|C=bot_bo620288102e_bool|hAPP_f1387463497_state(B,insert1415133716_state(D,C))=hAPP_H1150764575_state(hAPP_H1855735728_state(A,D),hAPP_f1387463497_state(B,C)). % 2.22/2.42 ** KEPT (pick-wt=11): 112 [] -hBOOL(finite86813460_state(A,B))|hAPP_H1150764575_state(hAPP_H1855735728_state(A,C),C)=C. % 2.22/2.42 ** KEPT (pick-wt=25): 113 [] -hBOOL(finite86813460_state(A,B))| -hBOOL(hAPP_f971112728l_bool(finite364844667_state,C))| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,D),C))|hAPP_H1150764575_state(hAPP_H1855735728_state(A,D),hAPP_f1387463497_state(B,C))=hAPP_f1387463497_state(B,C). % 2.22/2.42 ** KEPT (pick-wt=25): 114 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A))|A=bot_bo620288102e_bool| -hBOOL(hAPP_f971112728l_bool(B,insert1415133716_state($f39(B,A),bot_bo620288102e_bool)))|hBOOL(hAPP_f971112728l_bool(finite364844667_state,$f40(B,A)))|hBOOL(hAPP_f971112728l_bool(B,A)). % 2.22/2.42 ** KEPT (pick-wt=24): 115 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A))|A=bot_bo620288102e_bool| -hBOOL(hAPP_f971112728l_bool(B,insert1415133716_state($f39(B,A),bot_bo620288102e_bool)))|$f40(B,A)!=bot_bo620288102e_bool|hBOOL(hAPP_f971112728l_bool(B,A)). % 2.22/2.42 ** KEPT (pick-wt=29): 116 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A))|A=bot_bo620288102e_bool| -hBOOL(hAPP_f971112728l_bool(B,insert1415133716_state($f39(B,A),bot_bo620288102e_bool)))| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,$f41(B,A)),$f40(B,A)))|hBOOL(hAPP_f971112728l_bool(B,A)). % 2.22/2.42 ** KEPT (pick-wt=25): 117 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A))|A=bot_bo620288102e_bool| -hBOOL(hAPP_f971112728l_bool(B,insert1415133716_state($f39(B,A),bot_bo620288102e_bool)))|hBOOL(hAPP_f971112728l_bool(B,$f40(B,A)))|hBOOL(hAPP_f971112728l_bool(B,A)). % 2.22/2.42 ** KEPT (pick-wt=29): 118 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A))|A=bot_bo620288102e_bool| -hBOOL(hAPP_f971112728l_bool(B,insert1415133716_state($f39(B,A),bot_bo620288102e_bool)))| -hBOOL(hAPP_f971112728l_bool(B,insert1415133716_state($f41(B,A),$f40(B,A))))|hBOOL(hAPP_f971112728l_bool(B,A)). % 2.22/2.42 ** KEPT (pick-wt=16): 119 [] -hBOOL(big_se883361720_state(A,B))| -hBOOL(hAPP_f971112728l_bool(finite364844667_state,C))|hAPP_f1387463497_state(B,C)=hAPP_f1387463497_state(finite926392750_state(A),C). % 2.22/2.42 ** KEPT (pick-wt=26): 120 [] -hBOOL(finite354701905_state(A,B))| -hBOOL(hAPP_f971112728l_bool(finite364844667_state,C))| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,D),C))|minus_1641527009e_bool(C,insert1415133716_state(D,bot_bo620288102e_bool))!=bot_bo620288102e_bool|hAPP_f1387463497_state(B,C)=D. % 2.22/2.42 ** KEPT (pick-wt=36): 122 [copy,121,flip.5] -hBOOL(finite354701905_state(A,B))| -hBOOL(hAPP_f971112728l_bool(finite364844667_state,C))| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,D),C))|minus_1641527009e_bool(C,insert1415133716_state(D,bot_bo620288102e_bool))=bot_bo620288102e_bool|hAPP_H1150764575_state(hAPP_H1855735728_state(A,D),hAPP_f1387463497_state(B,minus_1641527009e_bool(C,insert1415133716_state(D,bot_bo620288102e_bool))))=hAPP_f1387463497_state(B,C). % 2.22/2.42 ** KEPT (pick-wt=20): 123 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),B))|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),C))|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),minus_1641527009e_bool(B,C))). % 2.22/2.42 ** KEPT (pick-wt=14): 124 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),minus_1641527009e_bool(B,C)))|hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),B)). % 2.22/2.42 ** KEPT (pick-wt=14): 125 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),minus_1641527009e_bool(B,C)))| -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),C)). % 2.22/2.42 ** KEPT (pick-wt=10): 126 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,A))|hBOOL(hAPP_f971112728l_bool(finite364844667_state,minus_1641527009e_bool(A,B))). % 2.22/2.42 ** KEPT (pick-wt=15): 127 [] -hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),B))|insert1415133716_state(A,minus_1641527009e_bool(B,insert1415133716_state(A,bot_bo620288102e_bool)))=B. % 2.22/2.42 ** KEPT (pick-wt=14): 128 [] -hBOOL(hAPP_f971112728l_bool(finite364844667_state,minus_1641527009e_bool(A,insert1415133716_state(B,C))))|hBOOL(hAPP_f971112728l_bool(finite364844667_state,minus_1641527009e_bool(A,C))). % 2.22/2.42 ** KEPT (pick-wt=14): 129 [] hBOOL(hAPP_f971112728l_bool(finite364844667_state,minus_1641527009e_bool(A,insert1415133716_state(B,C))))| -hBOOL(hAPP_f971112728l_bool(finite364844667_state,minus_1641527009e_bool(A,C))). % 2.22/2.42 ** KEPT (pick-wt=6): 130 [] -hBOOL(hAPP_bool_bool(fNot,A))| -hBOOL(A). % 2.22/2.42 ** KEPT (pick-wt=8): 131 [] -hBOOL(A)|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(fdisj,A),B)). % 2.22/2.42 ** KEPT (pick-wt=8): 132 [] -hBOOL(A)|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(fdisj,B),A)). % 2.22/2.42 ** KEPT (pick-wt=10): 133 [] -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(fdisj,A),B))|hBOOL(A)|hBOOL(B). % 2.22/2.42 ** KEPT (pick-wt=2): 134 [] -hBOOL(fFalse). % 2.22/2.42 ** KEPT (pick-wt=8): 135 [] -is_bool(A)|A=fTrue|A=fFalse. % 2.22/2.42 ** KEPT (pick-wt=8): 136 [] -hBOOL(A)|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(fimplies,B),A)). % 2.22/2.42 ** KEPT (pick-wt=10): 137 [] -hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(fimplies,A),B))| -hBOOL(A)|hBOOL(B). % 2.22/2.42 ** KEPT (pick-wt=9): 138 [] -hBOOL(hAPP_H78829294e_bool(hAPP_H1049623551e_bool(fe_qual1111551311_state,A),B))|A=B. % 2.22/2.42 ** KEPT (pick-wt=9): 139 [] A!=B|hBOOL(hAPP_H78829294e_bool(hAPP_H1049623551e_bool(fe_qual1111551311_state,A),B)). % 2.22/2.42 ** KEPT (pick-wt=8): 140 [] -is_bool(A)|hAPP_H78829294e_bool(cOMBK_659609255_state(A),B)=A. % 2.22/2.42 ** KEPT (pick-wt=10): 141 [] -hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(bot_bo620288102e_bool),insert1415133716_state(hoare_2082236334_state(p,c,q),bot_bo620288102e_bool))). % 2.22/2.42 58 back subsumes 40. % 2.22/2.42 % 2.22/2.42 ------------> process sos: % 2.22/2.42 ** KEPT (pick-wt=3): 159 [] A=A. % 2.22/2.42 ** KEPT (pick-wt=4): 160 [] is_bool(big_se883361720_state(A,B)). % 2.22/2.42 ** KEPT (pick-wt=4): 161 [] is_bool(finite354701905_state(A,B)). % 2.22/2.42 ** KEPT (pick-wt=4): 162 [] is_bool(finite86813460_state(A,B)). % 2.22/2.42 ** KEPT (pick-wt=2): 163 [] is_bool(bot_bot_bool). % 2.22/2.42 ** KEPT (pick-wt=2): 164 [] is_bool(fFalse). % 2.22/2.42 ** KEPT (pick-wt=2): 165 [] is_bool(fTrue). % 2.22/2.42 ** KEPT (pick-wt=4): 166 [] is_bool(hAPP_state_bool(A,B)). % 2.22/2.42 ** KEPT (pick-wt=4): 167 [] is_bool(hAPP_H78829294e_bool(A,B)). % 2.22/2.42 ** KEPT (pick-wt=4): 168 [] is_bool(hAPP_f971112728l_bool(A,B)). % 2.22/2.42 ** KEPT (pick-wt=5): 169 [] hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),bot_bo620288102e_bool)). % 2.22/2.42 ** KEPT (pick-wt=9): 170 [] collec307967673_state(A)=bot_bo620288102e_bool|hBOOL(hAPP_H78829294e_bool(A,$f8(A))). % 2.22/2.42 ** KEPT (pick-wt=9): 172 [copy,171,flip.1] collec307967673_state(A)=bot_bo620288102e_bool|hBOOL(hAPP_H78829294e_bool(A,$f9(A))). % 2.22/2.42 ** KEPT (pick-wt=10): 173 [] hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,$f10(A)),A))|A=bot_bo620288102e_bool. % 2.22/2.42 ** KEPT (pick-wt=10): 174 [] hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,$f11(A)),A))|A=bot_bo620288102e_bool. % 2.22/2.42 ** KEPT (pick-wt=5): 176 [copy,175,flip.1] collec307967673_state(cOMBK_659609255_state(fFalse))=bot_bo620288102e_bool. % 2.22/2.42 ---> New Demodulator: 177 [new_demod,176] collec307967673_state(cOMBK_659609255_state(fFalse))=bot_bo620288102e_bool. % 2.22/2.42 ** KEPT (pick-wt=11): 178 [] insert1415133716_state(A,insert1415133716_state(B,C))=insert1415133716_state(B,insert1415133716_state(A,C)). % 2.22/2.42 ** KEPT (pick-wt=9): 179 [] insert1415133716_state(A,insert1415133716_state(A,B))=insert1415133716_state(A,B). % 2.22/2.42 ---> New Demodulator: 180 [new_demod,179] insert1415133716_state(A,insert1415133716_state(A,B))=insert1415133716_state(A,B). % 2.22/2.42 ** KEPT (pick-wt=15): 182 [copy,181,flip.1] collec307967673_state(cOMBS_458705923l_bool(cOMBB_962198420_state(fimplies,cOMBB_2144135922_state(fNot,cOMBC_654211620e_bool(fe_qual1111551311_state,A))),B))=insert1415133716_state(A,collec307967673_state(B)). % 2.22/2.42 ---> New Demodulator: 183 [new_demod,182] collec307967673_state(cOMBS_458705923l_bool(cOMBB_962198420_state(fimplies,cOMBB_2144135922_state(fNot,cOMBC_654211620e_bool(fe_qual1111551311_state,A))),B))=insert1415133716_state(A,collec307967673_state(B)). % 2.22/2.42 ** KEPT (pick-wt=14): 185 [copy,184,flip.1] collec307967673_state(cOMBS_458705923l_bool(cOMBB_962198420_state(fdisj,cOMBC_654211620e_bool(fe_qual1111551311_state,A)),cOMBC_1734175330l_bool(member1338687867_state,B)))=insert1415133716_state(A,B). % 2.22/2.42 ---> New Demodulator: 186 [new_demod,185] collec307967673_state(cOMBS_458705923l_bool(cOMBB_962198420_state(fdisj,cOMBC_654211620e_bool(fe_qual1111551311_state,A)),cOMBC_1734175330l_bool(member1338687867_state,B)))=insert1415133716_state(A,B). % 2.22/2.42 ** KEPT (pick-wt=8): 187 [] hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),insert1415133716_state(A,B))). % 2.22/2.42 ** KEPT (pick-wt=7): 188 [] hAPP_f1387463497_state(the_el1751439279_state,insert1415133716_state(A,bot_bo620288102e_bool))=A. % 2.22/2.42 ---> New Demodulator: 189 [new_demod,188] hAPP_f1387463497_state(the_el1751439279_state,insert1415133716_state(A,bot_bo620288102e_bool))=A. % 2.22/2.42 ** KEPT (pick-wt=10): 190 [] hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(A),insert1415133716_state(hoare_2082236334_state(B,skip,B),bot_bo620288102e_bool))). % 2.22/2.42 ** KEPT (pick-wt=9): 192 [copy,191,flip.1] hoare_2082236334_state($f14(A),$f13(A),$f12(A))=A. % 2.22/2.42 ---> New Demodulator: 193 [new_demod,192] hoare_2082236334_state($f14(A),$f13(A),$f12(A))=A. % 2.22/2.42 ** KEPT (pick-wt=10): 194 [] hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,$f17(A)),A))|A=bot_bo620288102e_bool. % 2.22/2.42 ** KEPT (pick-wt=24): 195 [] hBOOL(hAPP_state_bool(hAPP_s1806633685e_bool(A,$f20(B,C,D,A)),$f19(B,C,D,A)))|hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(C),insert1415133716_state(hoare_2082236334_state(A,D,B),bot_bo620288102e_bool))). % 2.22/2.42 ** KEPT (pick-wt=10): 197 [copy,196,flip.2] A=bot_bo620288102e_bool|insert1415133716_state($f22(A),$f21(A))=A. % 2.22/2.42 ** KEPT (pick-wt=8): 198 [] hAPP_f1387463497_state(finite926392750_state(A),insert1415133716_state(B,bot_bo620288102e_bool))=B. % 2.22/2.42 ---> New Demodulator: 199 [new_demod,198] hAPP_f1387463497_state(finite926392750_state(A),insert1415133716_state(B,bot_bo620288102e_bool))=B. % 2.22/2.42 ** KEPT (pick-wt=4): 200 [] hBOOL(hAPP_f971112728l_bool(finite364844667_state,bot_bo620288102e_bool)). % 2.22/2.42 ** KEPT (pick-wt=7): 201 [] hBOOL(hAPP_H78829294e_bool(finite374952848_state(A,B,bot_bo620288102e_bool),B)). % 2.22/2.42 ** KEPT (pick-wt=4): 202 [] collec307967673_state(A)=A. % 2.22/2.42 ---> New Demodulator: 203 [new_demod,202] collec307967673_state(A)=A. % 2.22/2.42 ** KEPT (pick-wt=15): 204 [] hBOOL(hAPP_f971112728l_bool(hAPP_H30606679l_bool(member1338687867_state,A),B))|minus_1641527009e_bool(insert1415133716_state(A,B),insert1415133716_state(A,bot_bo620288102e_bool))=B. % 2.22/2.42 ** KEPT (pick-wt=11): 205 [] insert1415133716_state(A,minus_1641527009e_bool(B,insert1415133716_state(A,bot_bo620288102e_bool)))=insert1415133716_state(A,B). % 2.22/2.42 ---> New Demodulator: 206 [new_demod,205] insert1415133716_state(A,minus_1641527009e_bool(B,insert1415133716_state(A,bot_bo620288102e_bool)))=insert1415133716_state(A,B). % 2.22/2.42 ** KEPT (pick-wt=13): 208 [copy,207,flip.1] minus_1641527009e_bool(minus_1641527009e_bool(A,insert1415133716_state(B,bot_bo620288102e_bool)),C)=minus_1641527009e_bool(A,insert1415133716_state(B,C)). % 2.22/2.42 ---> New Demodulator: 209 [new_demod,208] minus_1641527009e_bool(minus_1641527009e_bool(A,insert1415133716_state(B,bot_bo620288102e_bool)),C)=minus_1641527009e_bool(A,insert1415133716_state(B,C)). % 2.22/2.42 ** KEPT (pick-wt=13): 211 [copy,210,flip.1] minus_1641527009e_bool(minus_1641527009e_bool(A,B),insert1415133716_state(C,bot_bo620288102e_bool))=minus_1641527009e_bool(A,insert1415133716_state(C,B)). % 2.22/2.42 ---> New Demodulator: 212 [new_demod,211] minus_1641527009e_bool(minus_1641527009e_bool(A,B),insert1415133716_state(C,bot_bo620288102e_bool))=minus_1641527009e_bool(A,insert1415133716_state(C,B)). % 2.22/2.42 ** KEPT (pick-wt=6): 213 [] hBOOL(A)|hBOOL(hAPP_bool_bool(fNot,A)). % 2.22/2.42 ** KEPT (pick-wt=8): 214 [] hBOOL(A)|hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(fimplies,A),B)). % 2.22/2.42 ** KEPT (pick-wt=11): 216 [copy,215,flip.1] hAPP_bool_bool(A,hAPP_H78829294e_bool(B,C))=hAPP_H78829294e_bool(cOMBB_2144135922_state(A,B),C). % 2.22/2.42 ---> New Demodulator: 217 [new_demod,216] hAPP_bool_bool(A,hAPP_H78829294e_bool(B,C))=hAPP_H78829294e_bool(cOMBB_2144135922_state(A,B),C). % 2.22/2.42 ** KEPT (pick-wt=13): 219 [copy,218,demod,217] hAPP_H78829294e_bool(cOMBS_458705923l_bool(A,B),C)=hAPP_H78829294e_bool(cOMBB_2144135922_state(hAPP_H1187982158l_bool(A,C),B),C). % 2.22/2.42 ** KEPT (pick-wt=11): 221 [copy,220,flip.1] hAPP_b589554111l_bool(A,hAPP_H78829294e_bool(B,C))=hAPP_H1187982158l_bool(cOMBB_962198420_state(A,B),C). % 2.22/2.42 ---> New Demodulator: 222 [new_demod,221] hAPP_b589554111l_bool(A,hAPP_H78829294e_bool(B,C))=hAPP_H1187982158l_bool(cOMBB_962198420_state(A,B),C). % 2.22/2.42 ** KEPT (pick-wt=11): 223 [] hAPP_H78829294e_bool(cOMBC_654211620e_bool(A,B),C)=hAPP_H78829294e_bool(hAPP_H1049623551e_bool(A,C),B). % 2.22/2.42 ** KEPT (pick-wt=11): 225 [copy,224,flip.1] hAPP_f971112728l_bool(hAPP_H30606679l_bool(A,B),C)=hAPP_H78829294e_bool(cOMBC_1734175330l_bool(A,C),B). % 2.22/2.42 ---> New Demodulator: 226 [new_demod,225] hAPP_f971112728l_bool(hAPP_H30606679l_bool(A,B),C)=hAPP_H78829294e_bool(cOMBC_1734175330l_bool(A,C),B). % 2.22/2.42 ** KEPT (pick-wt=8): 227 [] hBOOL(hAPP_f971112728l_bool(hoare_1598289066_state(bot_bo620288102e_bool),insert1415133716_state(hoare_Mirabelle_MGT(c),bot_bo620288102e_bool))). % 2.22/2.42 ** KEPT (pick-wt=10): 228 [] hBOOL(hAPP_f971112728l_bool(hoare_2004700328_state(bot_bo620288102e_bool),insert1415133716_state(hoare_2082236334_state(p,c,q),bot_bo620288102e_bool))). % 2.22/2.42 Following clause subsumed by 159 during input processing: 0 [copy,159,flip.1] A=A. % 2.22/2.42 159 back subsumes 152. % 2.22/2.42 159 back subsumes 151. % 2.22/2.42 >>>> Starting back demodulation with 177. % 2.22/2.42 Following clause subsumed by 178 during input processing: 0 [copy,178,flip.1] insert1415133716_state(A,insert1415133716_state(B,C))=insert1415133716_state(B,insert1415133716_state(A,C)). % 2.22/2.42 >>>> Starting back demodulation with 180. % 2.22/2.42 >> back demodulating 150 with 180. % 2.22/2.42 >> back demodulating 149 with 180. % 2.22/2.42 >> back demodulating 148 with 180. % 2.22/2.42 >> back demodulating 147 with 180. % 2.22/2.42 >> back demodulating 146 with 180. % 2.22/2.42 >> back demodulating 145 with 180. % 2.22/2.42 >>>> Starting back demodulation with 183. % 2.22/2.42 >>>> Starting back demodulation with 186. % 2.22/2.42 >>>> Starting back demodulation with 189. % 2.22/2.42 >>>> Starting back demodulation with 193. % 2.22/2.42 >>>> Starting back demodulation with 199. % 2.22/2.42 >>>> Starting back demodulation with 203. % 2.22/2.42 >> back demodulating 185 with 203. % 2.22/2.42 >> back demodulating 182 with 203. % 2.22/2.42 >> back demodulating 176 with 203. % 2.22/2.42 >> back demodulating 172 with 203. % 2.22/2.42 >> back demodulating 170 with 203. % 2.22/2.42 >> back demodulating 32 with 203. % 2.22/2.42 >>>> Starting back demodulation with 206. % 2.22/2.42 >> back demodulating 127 with 206. % 2.22/2.42 >>>> Starting back demodulation with 209. % 2.22/2.42 >>>> Starting back demodulation with 212. % 2.22/2.42 >>>> Starting back demodulation with 217. % 2.22/2.42 ** KEPT (pick-wt=13): 244 [copy,219,flip.1] hAPP_H78829294e_bool(cOMBB_2144135922_state(hAPP_H1187982158l_bool(A,B),C),B)=hAPP_H78829294e_bool(cOMBS_458705923l_bool(A,C),B). % 2.22/2.42 >>>> Starting back demodulation with 222. % 2.22/2.42 ** KEPT (pick-wt=11): 245 [copy,223,flip.1] hAPP_H78829294e_bool(hAPP_H1049623551e_bool(A,B),C)=hAPP_H78829294e_bool(cOMBC_654211620e_bool(A,C),B). % 2.22/2.42 >>>> Starting back demodulation with 226. % 2.22/2.42 >> back demodulating 204 with 226. % 2.22/2.42 >> back demodulating 194 with 226. % 2.22/2.42 >> back demodulating 187 with 226. % 2.22/2.42 >> back demodulating 174 with 226. % 2.22/2.42 >> back demodulating 173 with 226. % 2.22/2.42 >> back demodulating 155 with 226. % 2.22/2.42 >> back demodulating 125 with 226. % 2.22/2.42 >> back demodulating 124 with 226. % 2.22/2.42 >> back demodulating 123 with 226. % 2.22/2.42 >> back demodulating 122 with 226. % 2.22/2.42 >> back demodulating 120 with 226. % 2.22/2.42 >> back demodulating 116 with 226. % 2.22/2.42 >> back demodulating 113 with 226. % 2.22/2.42 >> back demodulating 110 with 226. % 2.22/2.42 >> back demodulating 107 with 226. % 2.22/2.42 >> back demodulating 101 with 226. % 2.22/2.42 >> back demodulating 96 with 226. % 2.22/2.42 >> back demodulating 95 with 226. % 2.22/2.42 >> back demodulating 83 with 226. % 2.22/2.42 >> back demodulating 82 with 226. % 2.22/2.42 >> back demodulating 79 with 226. % 2.22/2.42 >> back demodulating 76 with 226. % 2.22/2.42 >> back demodulating 72 with 226. % 2.22/2.42 >> back demodulating 70 with 226. % 2.22/2.42 >> back demodulating 66 with 226. % 2.22/2.42 >> back demodulating 65 with 226. % 2.22/2.42 >> back demodulating 56 with 226. % 2.22/2.42 >> back demodulating 55 with 226. % 2.22/2.42 >> back demodulating 48 with 226. % 2.22/2.42 >> back demodulating 47 with 226. % 2.22/2.42 >> back demodulating 45 with 226. % 2.22/2.42 >> back demodulating 44 with 226. % 2.22/2.42 >> back demodulating 35 with 226. % 2.22/2.42 >> back demodulating 34 with 226. % 2.22/2.42 >> back demodulating 33 with 226. % 2.22/2.42 >> back demodulating 31 with 226. % 2.22/2.42 >> back demodulating 24 with 226. % 2.22/2.42 >> back demodulating 21 with 226. % 2.22/2.42 >> back demodulating 17 with 226. % 2.22/2.42 >> back demodulating 16 with 226. % 2.22/2.42 >> back demodulating 15 with 226. % 2.22/2.42 >>>> Starting back demodulation with 235. % 2.22/2.42 >> back demodulating 233 with 235. % 2.22/2.42 >> back demodulating 232 with 235. % 2.22/2.42 >> back demodulating 231 with 235. % 2.22/2.42 >> back demodulating 230 with 235. % 2.22/2.42 >> back demodulating 229 with 235. % 2.22/2.42 >> back demodulating 228 with 235. % 2.22/2.42 >> back demodulating 227 with 235. % 2.22/2.42 >> back demodulating 211 with 235. % 2.22/2.42 >> back demodulating 208 with 235. % 2.22/2.42 >> back demodulating 205 with 235. % 2.22/2.42 >> back demodulating 198 with 235. % 2.22/2.42 >> back demodulating 197 with 235. % 2.22/2.42 >> back demodulating 195 with 235. % 2.22/2.42 >> back demodulating 190 with 235. % 2.22/2.42 >> back demodulating 188 with 235. % 2.22/2.42 >> back demodulating 179 with 235. % 2.22/2.42 >> back demodulating 178 with 235. % 2.22/2.42 >> back demodulating 153 with 235. % 2.22/2.42 >> back demodulating 141 with 235. % 2.22/2.42 >> back demodulating 129 with 235. % 2.22/2.42 >> back demodulating 128 with 235. % 2.22/2.42 >> back demodulating 118 with 235. % 2.22/2.42 >> back demodulating 117 with 235. % 2.22/2.42 >> back demodulating 115 with 235. % 2.22/2.42 >> back demodulating 114 with 235. % 2.22/2.42 >> back demodulating 111 with 235. % 2.22/2.42 >> back demodulating 104 with 235. % 2.22/2.42 >> back demodulating 98 with 235. % 2.22/2.42 >> back demodulating 91 with 235. % 2.22/2.42 >> back demodulating 88 with 235. % 2.22/2.42 >> back demodulating 85 with 235. % 2.22/2.42 >> back demodulating 81 with 235. % 2.22/2.42 >> back demodulating 75 with 235. % 2.22/2.42 >> back demodulating 74 with 235. % 2.22/2.42 >> back demodulating 71 with 235. % 2.22/2.42 >> back demodulating 68 with 235. % 2.22/2.42 >> back demodulating 62 with 235. % 2.22/2.42 >> back demodulating 61 with 235. % 2.22/2.42 >> back demodulating 60 with 235. % 2.22/2.42 >> back demodulating 59 with 235. % 2.22/2.42 >> back demodulating 51 with 235. % 2.22/2.42 >> back demodulating 50 with 235. % 2.22/2.42 >> back demodulating 42 with 235. % 2.22/2.42 >> back demodulating 39 with 235. % 2.22/2.42 >> back demodulating 38 with 235. % 2.22/2.42 >> back demodulating 37 with 235. % 2.22/2.42 >> back demodulating 36 with 235. % 2.22/2.42 >> back demodulating 30 with 235. % 2.22/2.42 >> back demodulating 29 with 235. % 2.22/2.42 >> back demodulating 28 with 235. % 2.22/2.42 >> back demodulating 27 with 235. % 2.22/2.42 >> back demodulating 26 with 235. % 2.22/2.42 >> back demodulating 25 with 235. % 2.22/2.42 >> back demodulating 23 with 235. % 2.22/2.42 >> back demodulating 20 with 235. % 2.22/2.42 >> back demodulating 19 with 235. % 2.22/2.42 >> back demodulating 18 with 235. % 2.22/2.42 >> back demodulating 14 with 235. % 2.22/2.42 >> back demodulating 13 with 235. % 2.22/2.42 >> back demodulating 12 with 235. % 2.22/2.42 >> back demodulating 11 with 235. % 2.22/2.42 >> back demodulating 10 with 235. % 2.22/2.42 >> back demodulating 9 with 235. % 2.22/2.42 >> back demodulating 8 with 235. % 2.22/2.42 >>>> Starting back demodulation with 237. % 2.22/2.42 >>>> Starting back demodulation with 239. % 2.22/2.42 Following clause subsumed by 219 during input processing: 0 [copy,244,flip.1] hAPP_H78829294e_bool(cOMBS_458705923l_bool(A,B),C)=hAPP_H78829294e_bool(cOMBB_2144135922_state(hAPP_H1187982158l_bool(A,C),B),C). % 2.22/2.43 Following clause subsumed by 223 during input processing: 0 [copy,245,flip.1] hAPP_H78829294e_bool(cOMBC_654211620e_bool(A,B),C)=hAPP_H78829294e_bool(hAPP_H1049623551e_bool(A,C),B). % 2.22/2.43 >>>> Starting back demodulation with 295. % 2.22/2.43 >>>> Starting back demodulation with 297. % 2.22/2.43 >>>> Starting back demodulation with 299. % 2.22/2.43 >> back demodulating 243 with 299. % 2.22/2.43 >>>> Starting back demodulation with 301. % 2.22/2.43 >>>> Starting back demodulation with 306. % 2.22/2.43 >>>> Starting back demodulation with 308. % 2.22/2.43 Following clause subsumed by 309 during input processing: 0 [copy,309,flip.1] cOMBS_458705923l_bool(cOMBB_962198420_state(fdisj,cOMBC_654211620e_bool(fe_qual1111551311_state,A)),cOMBC_1734175330l_bool(member1338687867_state,cOMBS_458705923l_bool(cOMBB_962198420_state(fdisj,cOMBC_654211620e_bool(fe_qual1111551311_state,B)),cOMBC_1734175330l_bool(member1338687867_state,C))))=cOMBS_458705923l_bool(cOMBB_962198420_state(fdisj,cOMBC_654211620e_bool(fe_qual1111551311_state,B)),cOMBC_1734175330l_bool(member1338687867_state,cOMBS_458705923l_bool(cOMBB_962198420_state(fdisj,cOMBC_654211620e_bool(fe_qual1111551311_state,A)),cOMBC_1734175330l_bool(member1338687867_state,C)))). % 3.43/3.65 % 3.43/3.65 ======= end of input processing ======= % 3.43/3.65 % 3.43/3.65 =========== start of search =========== % 3.43/3.65 % 3.43/3.65 % 3.43/3.65 Resetting weight limit to 4. % 3.43/3.65 % 3.43/3.65 % 3.43/3.65 Resetting weight limit to 4. % 3.43/3.65 % 3.43/3.65 sos_size=134 % 3.43/3.65 % 3.43/3.65 Search stopped because sos empty. % 3.43/3.65 % 3.43/3.65 % 3.43/3.65 Search stopped because sos empty. % 3.43/3.65 % 3.43/3.65 ============ end of search ============ % 3.43/3.65 % 3.43/3.65 -------------- statistics ------------- % 3.43/3.65 clauses given 141 % 3.43/3.65 clauses generated 101687 % 3.43/3.65 clauses kept 314 % 3.43/3.65 clauses forward subsumed 174 % 3.43/3.65 clauses back subsumed 4 % 3.43/3.65 Kbytes malloced 8789 % 3.43/3.65 % 3.43/3.65 ----------- times (seconds) ----------- % 3.43/3.65 user CPU time 1.24 (0 hr, 0 min, 1 sec) % 3.43/3.65 system CPU time 0.00 (0 hr, 0 min, 0 sec) % 3.43/3.65 wall-clock time 3 (0 hr, 0 min, 3 sec) % 3.43/3.65 % 3.43/3.65 Process 27375 finished Wed Jul 27 02:59:26 2022 % 3.43/3.65 Otter interrupted % 3.43/3.65 PROOF NOT FOUND %------------------------------------------------------------------------------