%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWW958+1 : TPTP v8.1.0. Released v7.4.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n013.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:23:14 EDT 2022 % Result : Unknown 62.06s 62.18s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SWW958+1 : TPTP v8.1.0. Released v7.4.0. % 0.06/0.12 % Command : otter-tptp-script %s % 0.12/0.33 % Computer : n013.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.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Wed Jul 27 02:58:00 EDT 2022 % 0.12/0.33 % CPUTime : % 2.36/2.56 ----- Otter 3.3f, August 2004 ----- % 2.36/2.56 The process was started by sandbox on n013.cluster.edu, % 2.36/2.56 Wed Jul 27 02:58:00 2022 % 2.36/2.56 The command was "./otter". The process ID is 19763. % 2.36/2.56 % 2.36/2.56 set(prolog_style_variables). % 2.36/2.56 set(auto). % 2.36/2.56 dependent: set(auto1). % 2.36/2.56 dependent: set(process_input). % 2.36/2.56 dependent: clear(print_kept). % 2.36/2.56 dependent: clear(print_new_demod). % 2.36/2.56 dependent: clear(print_back_demod). % 2.36/2.56 dependent: clear(print_back_sub). % 2.36/2.56 dependent: set(control_memory). % 2.36/2.56 dependent: assign(max_mem, 12000). % 2.36/2.56 dependent: assign(pick_given_ratio, 4). % 2.36/2.56 dependent: assign(stats_level, 1). % 2.36/2.56 dependent: assign(max_seconds, 10800). % 2.36/2.56 clear(print_given). % 2.36/2.56 % 2.36/2.56 formula_list(usable). % 2.36/2.56 all A (A=A). % 2.36/2.56 constr_CONST_0x30!=constr_CONST_1. % 2.36/2.56 constr_CONST_0x30!=constr_CONST_2. % 2.36/2.56 constr_CONST_0x30!=constr_CONST_3. % 2.36/2.56 constr_CONST_0x30!=constr_CONST_4. % 2.36/2.56 constr_CONST_0x30!=constr_ZERO. % 2.36/2.56 constr_CONST_0x30!=name_A. % 2.36/2.56 constr_CONST_0x30!=name_B. % 2.36/2.56 constr_CONST_0x30!=name_C. % 2.36/2.56 constr_CONST_0x30!=name_D. % 2.36/2.56 constr_CONST_0x30!=name_Na. % 2.36/2.56 constr_CONST_0x30!=name_Sa. % 2.36/2.56 constr_CONST_0x30!=name_Sb. % 2.36/2.56 constr_CONST_0x30!=name_Sc. % 2.36/2.56 constr_CONST_0x30!=name_Sd. % 2.36/2.56 constr_CONST_0x30!=name_c. % 2.36/2.56 constr_CONST_0x30!=name_skA. % 2.36/2.56 constr_CONST_0x30!=name_skB. % 2.36/2.56 constr_CONST_0x30!=name_skC. % 2.36/2.56 constr_CONST_0x30!=name_skD. % 2.36/2.56 constr_CONST_1!=constr_CONST_2. % 2.36/2.56 constr_CONST_1!=constr_CONST_3. % 2.36/2.56 constr_CONST_1!=constr_CONST_4. % 2.36/2.56 constr_CONST_1!=constr_ZERO. % 2.36/2.56 constr_CONST_1!=name_A. % 2.36/2.56 constr_CONST_1!=name_B. % 2.36/2.56 constr_CONST_1!=name_C. % 2.36/2.56 constr_CONST_1!=name_D. % 2.36/2.56 constr_CONST_1!=name_Na. % 2.36/2.56 constr_CONST_1!=name_Sa. % 2.36/2.56 constr_CONST_1!=name_Sb. % 2.36/2.56 constr_CONST_1!=name_Sc. % 2.36/2.56 constr_CONST_1!=name_Sd. % 2.36/2.56 constr_CONST_1!=name_c. % 2.36/2.56 constr_CONST_1!=name_skA. % 2.36/2.56 constr_CONST_1!=name_skB. % 2.36/2.56 constr_CONST_1!=name_skC. % 2.36/2.56 constr_CONST_1!=name_skD. % 2.36/2.56 constr_CONST_2!=constr_CONST_3. % 2.36/2.56 constr_CONST_2!=constr_CONST_4. % 2.36/2.56 constr_CONST_2!=constr_ZERO. % 2.36/2.56 constr_CONST_2!=name_A. % 2.36/2.56 constr_CONST_2!=name_B. % 2.36/2.56 constr_CONST_2!=name_C. % 2.36/2.56 constr_CONST_2!=name_D. % 2.36/2.56 constr_CONST_2!=name_Na. % 2.36/2.56 constr_CONST_2!=name_Sa. % 2.36/2.56 constr_CONST_2!=name_Sb. % 2.36/2.56 constr_CONST_2!=name_Sc. % 2.36/2.56 constr_CONST_2!=name_Sd. % 2.36/2.56 constr_CONST_2!=name_c. % 2.36/2.56 constr_CONST_2!=name_skA. % 2.36/2.56 constr_CONST_2!=name_skB. % 2.36/2.56 constr_CONST_2!=name_skC. % 2.36/2.56 constr_CONST_2!=name_skD. % 2.36/2.56 constr_CONST_3!=constr_CONST_4. % 2.36/2.56 constr_CONST_3!=constr_ZERO. % 2.36/2.56 constr_CONST_3!=name_A. % 2.36/2.56 constr_CONST_3!=name_B. % 2.36/2.56 constr_CONST_3!=name_C. % 2.36/2.56 constr_CONST_3!=name_D. % 2.36/2.56 constr_CONST_3!=name_Na. % 2.36/2.56 constr_CONST_3!=name_Sa. % 2.36/2.56 constr_CONST_3!=name_Sb. % 2.36/2.56 constr_CONST_3!=name_Sc. % 2.36/2.56 constr_CONST_3!=name_Sd. % 2.36/2.56 constr_CONST_3!=name_c. % 2.36/2.56 constr_CONST_3!=name_skA. % 2.36/2.56 constr_CONST_3!=name_skB. % 2.36/2.56 constr_CONST_3!=name_skC. % 2.36/2.56 constr_CONST_3!=name_skD. % 2.36/2.56 constr_CONST_4!=constr_ZERO. % 2.36/2.56 constr_CONST_4!=name_A. % 2.36/2.56 constr_CONST_4!=name_B. % 2.36/2.56 constr_CONST_4!=name_C. % 2.36/2.56 constr_CONST_4!=name_D. % 2.36/2.56 constr_CONST_4!=name_Na. % 2.36/2.56 constr_CONST_4!=name_Sa. % 2.36/2.56 constr_CONST_4!=name_Sb. % 2.36/2.56 constr_CONST_4!=name_Sc. % 2.36/2.56 constr_CONST_4!=name_Sd. % 2.36/2.56 constr_CONST_4!=name_c. % 2.36/2.56 constr_CONST_4!=name_skA. % 2.36/2.56 constr_CONST_4!=name_skB. % 2.36/2.56 constr_CONST_4!=name_skC. % 2.36/2.56 constr_CONST_4!=name_skD. % 2.36/2.56 constr_ZERO!=name_A. % 2.36/2.56 constr_ZERO!=name_B. % 2.36/2.56 constr_ZERO!=name_C. % 2.36/2.56 constr_ZERO!=name_D. % 2.36/2.56 constr_ZERO!=name_Na. % 2.36/2.56 constr_ZERO!=name_Sa. % 2.36/2.56 constr_ZERO!=name_Sb. % 2.36/2.56 constr_ZERO!=name_Sc. % 2.36/2.56 constr_ZERO!=name_Sd. % 2.36/2.56 constr_ZERO!=name_c. % 2.36/2.56 constr_ZERO!=name_skA. % 2.36/2.56 constr_ZERO!=name_skB. % 2.36/2.56 constr_ZERO!=name_skC. % 2.36/2.56 constr_ZERO!=name_skD. % 2.36/2.56 name_A!=name_B. % 2.36/2.56 name_A!=name_C. % 2.36/2.56 name_A!=name_D. % 2.36/2.56 name_A!=name_Na. % 2.36/2.56 name_A!=name_Sa. % 2.36/2.56 name_A!=name_Sb. % 2.36/2.56 name_A!=name_Sc. % 2.36/2.56 name_A!=name_Sd. % 2.36/2.56 name_A!=name_c. % 2.36/2.56 name_A!=name_skA. % 2.36/2.56 name_A!=name_skB. % 2.36/2.56 name_A!=name_skC. % 2.36/2.56 name_A!=name_skD. % 2.36/2.56 name_B!=name_C. % 2.36/2.56 name_B!=name_D. % 2.36/2.56 name_B!=name_Na. % 2.36/2.56 name_B!=name_Sa. % 2.36/2.56 name_B!=name_Sb. % 2.36/2.56 name_B!=name_Sc. % 2.36/2.56 name_B!=name_Sd. % 2.36/2.56 name_B!=name_c. % 2.36/2.56 name_B!=name_skA. % 2.36/2.56 name_B!=name_skB. % 2.36/2.56 name_B!=name_skC. % 2.36/2.56 name_B!=name_skD. % 2.36/2.56 name_C!=name_D. % 2.36/2.56 name_C!=name_Na. % 2.36/2.56 name_C!=name_Sa. % 2.36/2.56 name_C!=name_Sb. % 2.36/2.56 name_C!=name_Sc. % 2.36/2.56 name_C!=name_Sd. % 2.36/2.56 name_C!=name_c. % 2.36/2.56 name_C!=name_skA. % 2.36/2.56 name_C!=name_skB. % 2.36/2.56 name_C!=name_skC. % 2.36/2.56 name_C!=name_skD. % 2.36/2.56 name_D!=name_Na. % 2.36/2.56 name_D!=name_Sa. % 2.36/2.56 name_D!=name_Sb. % 2.36/2.56 name_D!=name_Sc. % 2.36/2.56 name_D!=name_Sd. % 2.36/2.56 name_D!=name_c. % 2.36/2.56 name_D!=name_skA. % 2.36/2.56 name_D!=name_skB. % 2.36/2.56 name_D!=name_skC. % 2.36/2.56 name_D!=name_skD. % 2.36/2.56 name_Na!=name_Sa. % 2.36/2.56 name_Na!=name_Sb. % 2.36/2.56 name_Na!=name_Sc. % 2.36/2.56 name_Na!=name_Sd. % 2.36/2.57 name_Na!=name_c. % 2.36/2.57 name_Na!=name_skA. % 2.36/2.57 name_Na!=name_skB. % 2.36/2.57 name_Na!=name_skC. % 2.36/2.57 name_Na!=name_skD. % 2.36/2.57 name_Sa!=name_Sb. % 2.36/2.57 name_Sa!=name_Sc. % 2.36/2.57 name_Sa!=name_Sd. % 2.36/2.57 name_Sa!=name_c. % 2.36/2.57 name_Sa!=name_skA. % 2.36/2.57 name_Sa!=name_skB. % 2.36/2.57 name_Sa!=name_skC. % 2.36/2.57 name_Sa!=name_skD. % 2.36/2.57 name_Sb!=name_Sc. % 2.36/2.57 name_Sb!=name_Sd. % 2.36/2.57 name_Sb!=name_c. % 2.36/2.57 name_Sb!=name_skA. % 2.36/2.57 name_Sb!=name_skB. % 2.36/2.57 name_Sb!=name_skC. % 2.36/2.57 name_Sb!=name_skD. % 2.36/2.57 name_Sc!=name_Sd. % 2.36/2.57 name_Sc!=name_c. % 2.36/2.57 name_Sc!=name_skA. % 2.36/2.57 name_Sc!=name_skB. % 2.36/2.57 name_Sc!=name_skC. % 2.36/2.57 name_Sc!=name_skD. % 2.36/2.57 name_Sd!=name_c. % 2.36/2.57 name_Sd!=name_skA. % 2.36/2.57 name_Sd!=name_skB. % 2.36/2.57 name_Sd!=name_skC. % 2.36/2.57 name_Sd!=name_skD. % 2.36/2.57 name_c!=name_skA. % 2.36/2.57 name_c!=name_skB. % 2.36/2.57 name_c!=name_skC. % 2.36/2.57 name_c!=name_skD. % 2.36/2.57 name_skA!=name_skB. % 2.36/2.57 name_skA!=name_skC. % 2.36/2.57 name_skA!=name_skD. % 2.36/2.57 name_skB!=name_skC. % 2.36/2.57 name_skB!=name_skD. % 2.36/2.57 name_skC!=name_skD. % 2.36/2.57 all VAR_K_0X30 VAR_M_0X30 (constr_adec(constr_aenc(VAR_M_0X30,constr_pkey(VAR_K_0X30)),VAR_K_0X30)=VAR_M_0X30). % 2.36/2.57 all VAR_X_10X30 (constr_add(VAR_X_10X30,constr_neg(VAR_X_10X30))=constr_ZERO). % 2.36/2.57 all VAR_X_9 (constr_add(VAR_X_9,constr_ZERO)=VAR_X_9). % 2.36/2.57 all VAR_X_7 VAR_Y_8 (constr_add(VAR_X_7,VAR_Y_8)=constr_add(VAR_Y_8,VAR_X_7)). % 2.36/2.57 all VAR_X_0X30 VAR_Y_0X30 VAR_Z_0X30 (constr_add(VAR_X_0X30,constr_add(VAR_Y_0X30,VAR_Z_0X30))=constr_add(constr_add(VAR_X_0X30,VAR_Y_0X30),VAR_Z_0X30)). % 2.36/2.57 pred_attacker(tuple_true). % 2.36/2.57 all VAR_V_30X30 (pred_attacker(VAR_V_30X30)->pred_attacker(constr_pkey(VAR_V_30X30))). % 2.36/2.57 all VAR_V_32 (pred_attacker(VAR_V_32)->pred_attacker(tuple_out_4(VAR_V_32))). % 2.36/2.57 all VAR_V_35 (pred_attacker(tuple_out_4(VAR_V_35))->pred_attacker(VAR_V_35)). % 2.36/2.57 all VAR_V_38 (pred_attacker(VAR_V_38)->pred_attacker(tuple_out_3(VAR_V_38))). % 2.36/2.57 all VAR_V_41 (pred_attacker(tuple_out_3(VAR_V_41))->pred_attacker(VAR_V_41)). % 2.36/2.57 all VAR_V_44 (pred_attacker(VAR_V_44)->pred_attacker(tuple_out_2(VAR_V_44))). % 2.36/2.57 all VAR_V_47 (pred_attacker(tuple_out_2(VAR_V_47))->pred_attacker(VAR_V_47)). % 2.36/2.57 all VAR_V_50X30 (pred_attacker(VAR_V_50X30)->pred_attacker(tuple_out_1(VAR_V_50X30))). % 2.36/2.57 all VAR_V_53 (pred_attacker(tuple_out_1(VAR_V_53))->pred_attacker(VAR_V_53)). % 2.36/2.57 all VAR_V_57 (pred_attacker(VAR_V_57)->pred_attacker(constr_neg(VAR_V_57))). % 2.36/2.57 pred_attacker(tuple_false). % 2.36/2.57 all VAR_V_60X30 VAR_V_61 (pred_attacker(VAR_V_60X30)&pred_attacker(VAR_V_61)->pred_attacker(tuple_client_D_out_4(VAR_V_60X30,VAR_V_61))). % 2.36/2.57 all VAR_V_68 VAR_V_69 (pred_attacker(tuple_client_D_out_4(VAR_V_68,VAR_V_69))->pred_attacker(VAR_V_68)). % 2.36/2.57 all VAR_V_71 VAR_V_72 (pred_attacker(tuple_client_D_out_4(VAR_V_71,VAR_V_72))->pred_attacker(VAR_V_72)). % 2.36/2.57 all VAR_V_76 VAR_V_77 (pred_attacker(VAR_V_76)&pred_attacker(VAR_V_77)->pred_attacker(tuple_client_D_in_3(VAR_V_76,VAR_V_77))). % 2.36/2.57 all VAR_V_84 VAR_V_85 (pred_attacker(tuple_client_D_in_3(VAR_V_84,VAR_V_85))->pred_attacker(VAR_V_84)). % 2.36/2.57 all VAR_V_87 VAR_V_88 (pred_attacker(tuple_client_D_in_3(VAR_V_87,VAR_V_88))->pred_attacker(VAR_V_88)). % 2.36/2.57 all VAR_V_91 (pred_attacker(VAR_V_91)->pred_attacker(tuple_client_D_in_2(VAR_V_91))). % 2.36/2.57 all VAR_V_94 (pred_attacker(tuple_client_D_in_2(VAR_V_94))->pred_attacker(VAR_V_94)). % 2.36/2.57 all VAR_V_97 (pred_attacker(VAR_V_97)->pred_attacker(tuple_client_D_in_1(VAR_V_97))). % 2.36/2.57 all VAR_V_10X300X30 (pred_attacker(tuple_client_D_in_1(VAR_V_10X300X30))->pred_attacker(VAR_V_10X300X30)). % 2.36/2.57 all VAR_V_10X304 VAR_V_10X305 (pred_attacker(VAR_V_10X304)&pred_attacker(VAR_V_10X305)->pred_attacker(tuple_client_C_out_4(VAR_V_10X304,VAR_V_10X305))). % 2.36/2.57 all VAR_V_112 VAR_V_113 (pred_attacker(tuple_client_C_out_4(VAR_V_112,VAR_V_113))->pred_attacker(VAR_V_112)). % 2.36/2.57 all VAR_V_115 VAR_V_116 (pred_attacker(tuple_client_C_out_4(VAR_V_115,VAR_V_116))->pred_attacker(VAR_V_116)). % 2.36/2.57 all VAR_V_120X30 VAR_V_121 (pred_attacker(VAR_V_120X30)&pred_attacker(VAR_V_121)->pred_attacker(tuple_client_C_in_3(VAR_V_120X30,VAR_V_121))). % 2.36/2.57 all VAR_V_128 VAR_V_129 (pred_attacker(tuple_client_C_in_3(VAR_V_128,VAR_V_129))->pred_attacker(VAR_V_128)). % 2.36/2.57 all VAR_V_131 VAR_V_132 (pred_attacker(tuple_client_C_in_3(VAR_V_131,VAR_V_132))->pred_attacker(VAR_V_132)). % 2.36/2.57 all VAR_V_135 (pred_attacker(VAR_V_135)->pred_attacker(tuple_client_C_in_2(VAR_V_135))). % 2.36/2.57 all VAR_V_138 (pred_attacker(tuple_client_C_in_2(VAR_V_138))->pred_attacker(VAR_V_138)). % 2.36/2.57 all VAR_V_141 (pred_attacker(VAR_V_141)->pred_attacker(tuple_client_C_in_1(VAR_V_141))). % 2.36/2.57 all VAR_V_144 (pred_attacker(tuple_client_C_in_1(VAR_V_144))->pred_attacker(VAR_V_144)). % 2.36/2.57 all VAR_V_148 VAR_V_149 (pred_attacker(VAR_V_148)&pred_attacker(VAR_V_149)->pred_attacker(tuple_client_B_out_4(VAR_V_148,VAR_V_149))). % 2.36/2.57 all VAR_V_156 VAR_V_157 (pred_attacker(tuple_client_B_out_4(VAR_V_156,VAR_V_157))->pred_attacker(VAR_V_156)). % 2.36/2.57 all VAR_V_159 VAR_V_160X30 (pred_attacker(tuple_client_B_out_4(VAR_V_159,VAR_V_160X30))->pred_attacker(VAR_V_160X30)). % 2.36/2.57 all VAR_V_164 VAR_V_165 (pred_attacker(VAR_V_164)&pred_attacker(VAR_V_165)->pred_attacker(tuple_client_B_in_3(VAR_V_164,VAR_V_165))). % 2.36/2.57 all VAR_V_172 VAR_V_173 (pred_attacker(tuple_client_B_in_3(VAR_V_172,VAR_V_173))->pred_attacker(VAR_V_172)). % 2.36/2.57 all VAR_V_175 VAR_V_176 (pred_attacker(tuple_client_B_in_3(VAR_V_175,VAR_V_176))->pred_attacker(VAR_V_176)). % 2.36/2.57 all VAR_V_179 (pred_attacker(VAR_V_179)->pred_attacker(tuple_client_B_in_2(VAR_V_179))). % 2.36/2.57 all VAR_V_182 (pred_attacker(tuple_client_B_in_2(VAR_V_182))->pred_attacker(VAR_V_182)). % 2.36/2.57 all VAR_V_185 (pred_attacker(VAR_V_185)->pred_attacker(tuple_client_B_in_1(VAR_V_185))). % 2.36/2.57 all VAR_V_188 (pred_attacker(tuple_client_B_in_1(VAR_V_188))->pred_attacker(VAR_V_188)). % 2.36/2.57 all VAR_V_191 (pred_attacker(VAR_V_191)->pred_attacker(tuple_client_A_out_5(VAR_V_191))). % 2.36/2.57 all VAR_V_194 (pred_attacker(tuple_client_A_out_5(VAR_V_194))->pred_attacker(VAR_V_194)). % 2.36/2.57 all VAR_V_198 VAR_V_199 (pred_attacker(VAR_V_198)&pred_attacker(VAR_V_199)->pred_attacker(tuple_client_A_out_3(VAR_V_198,VAR_V_199))). % 2.36/2.57 all VAR_V_20X306 VAR_V_20X307 (pred_attacker(tuple_client_A_out_3(VAR_V_20X306,VAR_V_20X307))->pred_attacker(VAR_V_20X306)). % 2.36/2.57 all VAR_V_20X309 VAR_V_210X30 (pred_attacker(tuple_client_A_out_3(VAR_V_20X309,VAR_V_210X30))->pred_attacker(VAR_V_210X30)). % 2.36/2.57 all VAR_V_214 VAR_V_215 (pred_attacker(VAR_V_214)&pred_attacker(VAR_V_215)->pred_attacker(tuple_client_A_in_4(VAR_V_214,VAR_V_215))). % 2.36/2.57 all VAR_V_222 VAR_V_223 (pred_attacker(tuple_client_A_in_4(VAR_V_222,VAR_V_223))->pred_attacker(VAR_V_222)). % 2.36/2.57 all VAR_V_225 VAR_V_226 (pred_attacker(tuple_client_A_in_4(VAR_V_225,VAR_V_226))->pred_attacker(VAR_V_226)). % 2.36/2.57 all VAR_V_229 (pred_attacker(VAR_V_229)->pred_attacker(tuple_client_A_in_2(VAR_V_229))). % 2.36/2.57 all VAR_V_232 (pred_attacker(tuple_client_A_in_2(VAR_V_232))->pred_attacker(VAR_V_232)). % 2.36/2.57 all VAR_V_235 (pred_attacker(VAR_V_235)->pred_attacker(tuple_client_A_in_1(VAR_V_235))). % 2.36/2.57 all VAR_V_238 (pred_attacker(tuple_client_A_in_1(VAR_V_238))->pred_attacker(VAR_V_238)). % 2.36/2.57 all VAR_V_242 VAR_V_243 (pred_attacker(VAR_V_242)&pred_attacker(VAR_V_243)->pred_attacker(constr_aenc(VAR_V_242,VAR_V_243))). % 2.36/2.57 all VAR_V_246 VAR_V_247 (pred_attacker(VAR_V_246)&pred_attacker(VAR_V_247)->pred_attacker(constr_adec(VAR_V_246,VAR_V_247))). % 2.36/2.57 all VAR_V_250X30 VAR_V_251 (pred_attacker(VAR_V_250X30)&pred_attacker(VAR_V_251)->pred_attacker(constr_add(VAR_V_250X30,VAR_V_251))). % 2.36/2.57 pred_attacker(constr_ZERO). % 2.36/2.57 pred_attacker(constr_CONST_4). % 2.36/2.57 pred_attacker(constr_CONST_3). % 2.36/2.57 pred_attacker(constr_CONST_2). % 2.36/2.57 pred_attacker(constr_CONST_1). % 2.36/2.57 pred_attacker(constr_CONST_0x30). % 2.36/2.57 all VAR_V_256 VAR_V_257 (pred_mess(VAR_V_257,VAR_V_256)&pred_attacker(VAR_V_257)->pred_attacker(VAR_V_256)). % 2.36/2.57 all VAR_V_258 VAR_V_259 (pred_attacker(VAR_V_259)&pred_attacker(VAR_V_258)->pred_mess(VAR_V_259,VAR_V_258)). % 2.36/2.57 pred_attacker(name_c). % 2.36/2.57 pred_attacker(name_D). % 2.36/2.57 pred_attacker(name_C). % 2.36/2.57 pred_attacker(name_B). % 2.36/2.57 pred_attacker(name_A). % 2.36/2.57 all VAR_V_261 pred_e_qual(VAR_V_261,VAR_V_261). % 2.36/2.57 all VAR_V_262 pred_attacker(name_new0x2Dname(VAR_V_262)). % 2.36/2.57 pred_attacker(tuple_out_1(constr_pkey(name_skA))). % 2.36/2.57 pred_attacker(tuple_out_2(constr_pkey(name_skB))). % 2.36/2.57 pred_attacker(tuple_out_3(constr_pkey(name_skC))). % 2.36/2.57 pred_attacker(tuple_out_4(constr_pkey(name_skD))). % 2.36/2.57 all VAR_LASTT_336 VAR_PKNEXTT_337 (pred_attacker(tuple_client_A_in_2(VAR_LASTT_336))&pred_attacker(tuple_client_A_in_1(VAR_PKNEXTT_337))->pred_attacker(tuple_client_A_out_3(name_A,constr_aenc(constr_add(name_Na,name_Sa),VAR_PKNEXTT_337)))). % 2.36/2.57 all VAR_AENC_ADD_NA_SA_SB_SC_SD_377 VAR_LASTT_376 VAR_PKNEXTT_378 (pred_attacker(tuple_client_A_in_4(VAR_LASTT_376,VAR_AENC_ADD_NA_SA_SB_SC_SD_377))&pred_attacker(tuple_client_A_in_2(VAR_LASTT_376))&pred_attacker(tuple_client_A_in_1(VAR_PKNEXTT_378))->pred_attacker(tuple_client_A_out_5(constr_add(constr_adec(VAR_AENC_ADD_NA_SA_SB_SC_SD_377,name_skA),constr_neg(name_Na))))). % 2.36/2.57 all VAR_AENC_ADD_NA_SA_426 VAR_PKNEXTT_427 VAR_PREVT_425 (pred_attacker(tuple_client_B_in_3(VAR_PREVT_425,VAR_AENC_ADD_NA_SA_426))&pred_attacker(tuple_client_B_in_2(VAR_PKNEXTT_427))&pred_attacker(tuple_client_B_in_1(VAR_PREVT_425))->pred_attacker(tuple_client_B_out_4(name_B,constr_aenc(constr_add(constr_adec(VAR_AENC_ADD_NA_SA_426,name_skB),name_Sb),VAR_PKNEXTT_427)))). % 2.36/2.57 all VAR_AENC_ADD_NA_SA_SB_479 VAR_PKNEXTT_480X30 VAR_PREVT_478 (pred_attacker(tuple_client_C_in_3(VAR_PREVT_478,VAR_AENC_ADD_NA_SA_SB_479))&pred_attacker(tuple_client_C_in_2(VAR_PKNEXTT_480X30))&pred_attacker(tuple_client_C_in_1(VAR_PREVT_478))->pred_attacker(tuple_client_C_out_4(name_C,constr_aenc(constr_add(constr_adec(VAR_AENC_ADD_NA_SA_SB_479,name_skC),name_Sc),VAR_PKNEXTT_480X30)))). % 2.36/2.57 all VAR_AENC_ADD_NA_SA_SB_SC_532 VAR_PKNEXTT_533 VAR_PREVT_531 (pred_attacker(tuple_client_D_in_3(VAR_PREVT_531,VAR_AENC_ADD_NA_SA_SB_SC_532))&pred_attacker(tuple_client_D_in_2(VAR_PKNEXTT_533))&pred_attacker(tuple_client_D_in_1(VAR_PREVT_531))->pred_attacker(tuple_client_D_out_4(name_D,constr_aenc(constr_add(constr_adec(VAR_AENC_ADD_NA_SA_SB_SC_532,name_skD),name_Sd),VAR_PKNEXTT_533)))). % 2.36/2.57 -pred_attacker(name_Sa). % 2.36/2.57 end_of_list. % 2.36/2.57 % 2.36/2.57 -------> usable clausifies to: % 2.36/2.57 % 2.36/2.57 list(usable). % 2.36/2.57 0 [] A=A. % 2.36/2.57 0 [] constr_CONST_0x30!=constr_CONST_1. % 2.36/2.57 0 [] constr_CONST_0x30!=constr_CONST_2. % 2.36/2.57 0 [] constr_CONST_0x30!=constr_CONST_3. % 2.36/2.57 0 [] constr_CONST_0x30!=constr_CONST_4. % 2.36/2.57 0 [] constr_CONST_0x30!=constr_ZERO. % 2.36/2.57 0 [] constr_CONST_0x30!=name_A. % 2.36/2.57 0 [] constr_CONST_0x30!=name_B. % 2.36/2.57 0 [] constr_CONST_0x30!=name_C. % 2.36/2.57 0 [] constr_CONST_0x30!=name_D. % 2.36/2.57 0 [] constr_CONST_0x30!=name_Na. % 2.36/2.57 0 [] constr_CONST_0x30!=name_Sa. % 2.36/2.57 0 [] constr_CONST_0x30!=name_Sb. % 2.36/2.57 0 [] constr_CONST_0x30!=name_Sc. % 2.36/2.57 0 [] constr_CONST_0x30!=name_Sd. % 2.36/2.57 0 [] constr_CONST_0x30!=name_c. % 2.36/2.57 0 [] constr_CONST_0x30!=name_skA. % 2.36/2.57 0 [] constr_CONST_0x30!=name_skB. % 2.36/2.57 0 [] constr_CONST_0x30!=name_skC. % 2.36/2.57 0 [] constr_CONST_0x30!=name_skD. % 2.36/2.57 0 [] constr_CONST_1!=constr_CONST_2. % 2.36/2.57 0 [] constr_CONST_1!=constr_CONST_3. % 2.36/2.57 0 [] constr_CONST_1!=constr_CONST_4. % 2.36/2.57 0 [] constr_CONST_1!=constr_ZERO. % 2.36/2.57 0 [] constr_CONST_1!=name_A. % 2.36/2.57 0 [] constr_CONST_1!=name_B. % 2.36/2.57 0 [] constr_CONST_1!=name_C. % 2.36/2.57 0 [] constr_CONST_1!=name_D. % 2.36/2.57 0 [] constr_CONST_1!=name_Na. % 2.36/2.57 0 [] constr_CONST_1!=name_Sa. % 2.36/2.57 0 [] constr_CONST_1!=name_Sb. % 2.36/2.57 0 [] constr_CONST_1!=name_Sc. % 2.36/2.57 0 [] constr_CONST_1!=name_Sd. % 2.36/2.57 0 [] constr_CONST_1!=name_c. % 2.36/2.57 0 [] constr_CONST_1!=name_skA. % 2.36/2.57 0 [] constr_CONST_1!=name_skB. % 2.36/2.57 0 [] constr_CONST_1!=name_skC. % 2.36/2.57 0 [] constr_CONST_1!=name_skD. % 2.36/2.57 0 [] constr_CONST_2!=constr_CONST_3. % 2.36/2.57 0 [] constr_CONST_2!=constr_CONST_4. % 2.36/2.57 0 [] constr_CONST_2!=constr_ZERO. % 2.36/2.57 0 [] constr_CONST_2!=name_A. % 2.36/2.57 0 [] constr_CONST_2!=name_B. % 2.36/2.57 0 [] constr_CONST_2!=name_C. % 2.36/2.57 0 [] constr_CONST_2!=name_D. % 2.36/2.57 0 [] constr_CONST_2!=name_Na. % 2.36/2.57 0 [] constr_CONST_2!=name_Sa. % 2.36/2.57 0 [] constr_CONST_2!=name_Sb. % 2.36/2.57 0 [] constr_CONST_2!=name_Sc. % 2.36/2.57 0 [] constr_CONST_2!=name_Sd. % 2.36/2.57 0 [] constr_CONST_2!=name_c. % 2.36/2.57 0 [] constr_CONST_2!=name_skA. % 2.36/2.57 0 [] constr_CONST_2!=name_skB. % 2.36/2.57 0 [] constr_CONST_2!=name_skC. % 2.36/2.57 0 [] constr_CONST_2!=name_skD. % 2.36/2.57 0 [] constr_CONST_3!=constr_CONST_4. % 2.36/2.57 0 [] constr_CONST_3!=constr_ZERO. % 2.36/2.57 0 [] constr_CONST_3!=name_A. % 2.36/2.57 0 [] constr_CONST_3!=name_B. % 2.36/2.57 0 [] constr_CONST_3!=name_C. % 2.36/2.57 0 [] constr_CONST_3!=name_D. % 2.36/2.57 0 [] constr_CONST_3!=name_Na. % 2.36/2.57 0 [] constr_CONST_3!=name_Sa. % 2.36/2.57 0 [] constr_CONST_3!=name_Sb. % 2.36/2.57 0 [] constr_CONST_3!=name_Sc. % 2.36/2.57 0 [] constr_CONST_3!=name_Sd. % 2.36/2.57 0 [] constr_CONST_3!=name_c. % 2.36/2.57 0 [] constr_CONST_3!=name_skA. % 2.36/2.57 0 [] constr_CONST_3!=name_skB. % 2.36/2.57 0 [] constr_CONST_3!=name_skC. % 2.36/2.57 0 [] constr_CONST_3!=name_skD. % 2.36/2.57 0 [] constr_CONST_4!=constr_ZERO. % 2.36/2.57 0 [] constr_CONST_4!=name_A. % 2.36/2.57 0 [] constr_CONST_4!=name_B. % 2.36/2.57 0 [] constr_CONST_4!=name_C. % 2.36/2.57 0 [] constr_CONST_4!=name_D. % 2.36/2.57 0 [] constr_CONST_4!=name_Na. % 2.36/2.57 0 [] constr_CONST_4!=name_Sa. % 2.36/2.57 0 [] constr_CONST_4!=name_Sb. % 2.36/2.57 0 [] constr_CONST_4!=name_Sc. % 2.36/2.57 0 [] constr_CONST_4!=name_Sd. % 2.36/2.57 0 [] constr_CONST_4!=name_c. % 2.36/2.57 0 [] constr_CONST_4!=name_skA. % 2.36/2.57 0 [] constr_CONST_4!=name_skB. % 2.36/2.57 0 [] constr_CONST_4!=name_skC. % 2.36/2.57 0 [] constr_CONST_4!=name_skD. % 2.36/2.57 0 [] constr_ZERO!=name_A. % 2.36/2.57 0 [] constr_ZERO!=name_B. % 2.36/2.57 0 [] constr_ZERO!=name_C. % 2.36/2.57 0 [] constr_ZERO!=name_D. % 2.36/2.57 0 [] constr_ZERO!=name_Na. % 2.36/2.57 0 [] constr_ZERO!=name_Sa. % 2.36/2.57 0 [] constr_ZERO!=name_Sb. % 2.36/2.57 0 [] constr_ZERO!=name_Sc. % 2.36/2.57 0 [] constr_ZERO!=name_Sd. % 2.36/2.57 0 [] constr_ZERO!=name_c. % 2.36/2.57 0 [] constr_ZERO!=name_skA. % 2.36/2.57 0 [] constr_ZERO!=name_skB. % 2.36/2.57 0 [] constr_ZERO!=name_skC. % 2.36/2.57 0 [] constr_ZERO!=name_skD. % 2.36/2.57 0 [] name_A!=name_B. % 2.36/2.57 0 [] name_A!=name_C. % 2.36/2.57 0 [] name_A!=name_D. % 2.36/2.57 0 [] name_A!=name_Na. % 2.36/2.57 0 [] name_A!=name_Sa. % 2.36/2.57 0 [] name_A!=name_Sb. % 2.36/2.57 0 [] name_A!=name_Sc. % 2.36/2.57 0 [] name_A!=name_Sd. % 2.36/2.57 0 [] name_A!=name_c. % 2.36/2.57 0 [] name_A!=name_skA. % 2.36/2.57 0 [] name_A!=name_skB. % 2.36/2.57 0 [] name_A!=name_skC. % 2.36/2.57 0 [] name_A!=name_skD. % 2.36/2.57 0 [] name_B!=name_C. % 2.36/2.57 0 [] name_B!=name_D. % 2.36/2.57 0 [] name_B!=name_Na. % 2.36/2.57 0 [] name_B!=name_Sa. % 2.36/2.57 0 [] name_B!=name_Sb. % 2.36/2.57 0 [] name_B!=name_Sc. % 2.36/2.57 0 [] name_B!=name_Sd. % 2.36/2.57 0 [] name_B!=name_c. % 2.36/2.57 0 [] name_B!=name_skA. % 2.36/2.57 0 [] name_B!=name_skB. % 2.36/2.57 0 [] name_B!=name_skC. % 2.36/2.57 0 [] name_B!=name_skD. % 2.36/2.57 0 [] name_C!=name_D. % 2.36/2.57 0 [] name_C!=name_Na. % 2.36/2.57 0 [] name_C!=name_Sa. % 2.36/2.57 0 [] name_C!=name_Sb. % 2.36/2.57 0 [] name_C!=name_Sc. % 2.36/2.57 0 [] name_C!=name_Sd. % 2.36/2.57 0 [] name_C!=name_c. % 2.36/2.57 0 [] name_C!=name_skA. % 2.36/2.57 0 [] name_C!=name_skB. % 2.36/2.57 0 [] name_C!=name_skC. % 2.36/2.57 0 [] name_C!=name_skD. % 2.36/2.57 0 [] name_D!=name_Na. % 2.36/2.57 0 [] name_D!=name_Sa. % 2.36/2.57 0 [] name_D!=name_Sb. % 2.36/2.57 0 [] name_D!=name_Sc. % 2.36/2.57 0 [] name_D!=name_Sd. % 2.36/2.57 0 [] name_D!=name_c. % 2.36/2.57 0 [] name_D!=name_skA. % 2.36/2.57 0 [] name_D!=name_skB. % 2.36/2.57 0 [] name_D!=name_skC. % 2.36/2.57 0 [] name_D!=name_skD. % 2.36/2.57 0 [] name_Na!=name_Sa. % 2.36/2.57 0 [] name_Na!=name_Sb. % 2.36/2.57 0 [] name_Na!=name_Sc. % 2.36/2.57 0 [] name_Na!=name_Sd. % 2.36/2.57 0 [] name_Na!=name_c. % 2.36/2.57 0 [] name_Na!=name_skA. % 2.36/2.57 0 [] name_Na!=name_skB. % 2.36/2.57 0 [] name_Na!=name_skC. % 2.36/2.57 0 [] name_Na!=name_skD. % 2.36/2.57 0 [] name_Sa!=name_Sb. % 2.36/2.57 0 [] name_Sa!=name_Sc. % 2.36/2.57 0 [] name_Sa!=name_Sd. % 2.36/2.57 0 [] name_Sa!=name_c. % 2.36/2.57 0 [] name_Sa!=name_skA. % 2.36/2.57 0 [] name_Sa!=name_skB. % 2.36/2.57 0 [] name_Sa!=name_skC. % 2.36/2.57 0 [] name_Sa!=name_skD. % 2.36/2.57 0 [] name_Sb!=name_Sc. % 2.36/2.57 0 [] name_Sb!=name_Sd. % 2.36/2.57 0 [] name_Sb!=name_c. % 2.36/2.57 0 [] name_Sb!=name_skA. % 2.36/2.57 0 [] name_Sb!=name_skB. % 2.36/2.57 0 [] name_Sb!=name_skC. % 2.36/2.57 0 [] name_Sb!=name_skD. % 2.36/2.57 0 [] name_Sc!=name_Sd. % 2.36/2.57 0 [] name_Sc!=name_c. % 2.36/2.57 0 [] name_Sc!=name_skA. % 2.36/2.57 0 [] name_Sc!=name_skB. % 2.36/2.57 0 [] name_Sc!=name_skC. % 2.36/2.57 0 [] name_Sc!=name_skD. % 2.36/2.57 0 [] name_Sd!=name_c. % 2.36/2.57 0 [] name_Sd!=name_skA. % 2.36/2.57 0 [] name_Sd!=name_skB. % 2.36/2.57 0 [] name_Sd!=name_skC. % 2.36/2.57 0 [] name_Sd!=name_skD. % 2.36/2.57 0 [] name_c!=name_skA. % 2.36/2.57 0 [] name_c!=name_skB. % 2.36/2.57 0 [] name_c!=name_skC. % 2.36/2.57 0 [] name_c!=name_skD. % 2.36/2.57 0 [] name_skA!=name_skB. % 2.36/2.57 0 [] name_skA!=name_skC. % 2.36/2.57 0 [] name_skA!=name_skD. % 2.36/2.57 0 [] name_skB!=name_skC. % 2.36/2.57 0 [] name_skB!=name_skD. % 2.36/2.57 0 [] name_skC!=name_skD. % 2.36/2.57 0 [] constr_adec(constr_aenc(VAR_M_0X30,constr_pkey(VAR_K_0X30)),VAR_K_0X30)=VAR_M_0X30. % 2.36/2.57 0 [] constr_add(VAR_X_10X30,constr_neg(VAR_X_10X30))=constr_ZERO. % 2.36/2.57 0 [] constr_add(VAR_X_9,constr_ZERO)=VAR_X_9. % 2.36/2.57 0 [] constr_add(VAR_X_7,VAR_Y_8)=constr_add(VAR_Y_8,VAR_X_7). % 2.36/2.57 0 [] constr_add(VAR_X_0X30,constr_add(VAR_Y_0X30,VAR_Z_0X30))=constr_add(constr_add(VAR_X_0X30,VAR_Y_0X30),VAR_Z_0X30). % 2.36/2.57 0 [] pred_attacker(tuple_true). % 2.36/2.57 0 [] -pred_attacker(VAR_V_30X30)|pred_attacker(constr_pkey(VAR_V_30X30)). % 2.36/2.57 0 [] -pred_attacker(VAR_V_32)|pred_attacker(tuple_out_4(VAR_V_32)). % 2.36/2.57 0 [] -pred_attacker(tuple_out_4(VAR_V_35))|pred_attacker(VAR_V_35). % 2.36/2.57 0 [] -pred_attacker(VAR_V_38)|pred_attacker(tuple_out_3(VAR_V_38)). % 2.36/2.57 0 [] -pred_attacker(tuple_out_3(VAR_V_41))|pred_attacker(VAR_V_41). % 2.36/2.57 0 [] -pred_attacker(VAR_V_44)|pred_attacker(tuple_out_2(VAR_V_44)). % 2.36/2.57 0 [] -pred_attacker(tuple_out_2(VAR_V_47))|pred_attacker(VAR_V_47). % 2.36/2.57 0 [] -pred_attacker(VAR_V_50X30)|pred_attacker(tuple_out_1(VAR_V_50X30)). % 2.36/2.57 0 [] -pred_attacker(tuple_out_1(VAR_V_53))|pred_attacker(VAR_V_53). % 2.36/2.57 0 [] -pred_attacker(VAR_V_57)|pred_attacker(constr_neg(VAR_V_57)). % 2.36/2.57 0 [] pred_attacker(tuple_false). % 2.36/2.57 0 [] -pred_attacker(VAR_V_60X30)| -pred_attacker(VAR_V_61)|pred_attacker(tuple_client_D_out_4(VAR_V_60X30,VAR_V_61)). % 2.36/2.57 0 [] -pred_attacker(tuple_client_D_out_4(VAR_V_68,VAR_V_69))|pred_attacker(VAR_V_68). % 2.36/2.57 0 [] -pred_attacker(tuple_client_D_out_4(VAR_V_71,VAR_V_72))|pred_attacker(VAR_V_72). % 2.36/2.57 0 [] -pred_attacker(VAR_V_76)| -pred_attacker(VAR_V_77)|pred_attacker(tuple_client_D_in_3(VAR_V_76,VAR_V_77)). % 2.36/2.57 0 [] -pred_attacker(tuple_client_D_in_3(VAR_V_84,VAR_V_85))|pred_attacker(VAR_V_84). % 2.36/2.57 0 [] -pred_attacker(tuple_client_D_in_3(VAR_V_87,VAR_V_88))|pred_attacker(VAR_V_88). % 2.36/2.57 0 [] -pred_attacker(VAR_V_91)|pred_attacker(tuple_client_D_in_2(VAR_V_91)). % 2.36/2.57 0 [] -pred_attacker(tuple_client_D_in_2(VAR_V_94))|pred_attacker(VAR_V_94). % 2.36/2.57 0 [] -pred_attacker(VAR_V_97)|pred_attacker(tuple_client_D_in_1(VAR_V_97)). % 2.36/2.57 0 [] -pred_attacker(tuple_client_D_in_1(VAR_V_10X300X30))|pred_attacker(VAR_V_10X300X30). % 2.36/2.57 0 [] -pred_attacker(VAR_V_10X304)| -pred_attacker(VAR_V_10X305)|pred_attacker(tuple_client_C_out_4(VAR_V_10X304,VAR_V_10X305)). % 2.36/2.57 0 [] -pred_attacker(tuple_client_C_out_4(VAR_V_112,VAR_V_113))|pred_attacker(VAR_V_112). % 2.36/2.57 0 [] -pred_attacker(tuple_client_C_out_4(VAR_V_115,VAR_V_116))|pred_attacker(VAR_V_116). % 2.36/2.57 0 [] -pred_attacker(VAR_V_120X30)| -pred_attacker(VAR_V_121)|pred_attacker(tuple_client_C_in_3(VAR_V_120X30,VAR_V_121)). % 2.36/2.57 0 [] -pred_attacker(tuple_client_C_in_3(VAR_V_128,VAR_V_129))|pred_attacker(VAR_V_128). % 2.36/2.57 0 [] -pred_attacker(tuple_client_C_in_3(VAR_V_131,VAR_V_132))|pred_attacker(VAR_V_132). % 2.36/2.57 0 [] -pred_attacker(VAR_V_135)|pred_attacker(tuple_client_C_in_2(VAR_V_135)). % 2.36/2.57 0 [] -pred_attacker(tuple_client_C_in_2(VAR_V_138))|pred_attacker(VAR_V_138). % 2.36/2.57 0 [] -pred_attacker(VAR_V_141)|pred_attacker(tuple_client_C_in_1(VAR_V_141)). % 2.36/2.57 0 [] -pred_attacker(tuple_client_C_in_1(VAR_V_144))|pred_attacker(VAR_V_144). % 2.36/2.57 0 [] -pred_attacker(VAR_V_148)| -pred_attacker(VAR_V_149)|pred_attacker(tuple_client_B_out_4(VAR_V_148,VAR_V_149)). % 2.36/2.57 0 [] -pred_attacker(tuple_client_B_out_4(VAR_V_156,VAR_V_157))|pred_attacker(VAR_V_156). % 2.36/2.57 0 [] -pred_attacker(tuple_client_B_out_4(VAR_V_159,VAR_V_160X30))|pred_attacker(VAR_V_160X30). % 2.36/2.57 0 [] -pred_attacker(VAR_V_164)| -pred_attacker(VAR_V_165)|pred_attacker(tuple_client_B_in_3(VAR_V_164,VAR_V_165)). % 2.36/2.57 0 [] -pred_attacker(tuple_client_B_in_3(VAR_V_172,VAR_V_173))|pred_attacker(VAR_V_172). % 2.36/2.57 0 [] -pred_attacker(tuple_client_B_in_3(VAR_V_175,VAR_V_176))|pred_attacker(VAR_V_176). % 2.36/2.57 0 [] -pred_attacker(VAR_V_179)|pred_attacker(tuple_client_B_in_2(VAR_V_179)). % 2.36/2.57 0 [] -pred_attacker(tuple_client_B_in_2(VAR_V_182))|pred_attacker(VAR_V_182). % 2.36/2.57 0 [] -pred_attacker(VAR_V_185)|pred_attacker(tuple_client_B_in_1(VAR_V_185)). % 2.36/2.57 0 [] -pred_attacker(tuple_client_B_in_1(VAR_V_188))|pred_attacker(VAR_V_188). % 2.36/2.57 0 [] -pred_attacker(VAR_V_191)|pred_attacker(tuple_client_A_out_5(VAR_V_191)). % 2.36/2.57 0 [] -pred_attacker(tuple_client_A_out_5(VAR_V_194))|pred_attacker(VAR_V_194). % 2.36/2.57 0 [] -pred_attacker(VAR_V_198)| -pred_attacker(VAR_V_199)|pred_attacker(tuple_client_A_out_3(VAR_V_198,VAR_V_199)). % 2.36/2.57 0 [] -pred_attacker(tuple_client_A_out_3(VAR_V_20X306,VAR_V_20X307))|pred_attacker(VAR_V_20X306). % 2.36/2.57 0 [] -pred_attacker(tuple_client_A_out_3(VAR_V_20X309,VAR_V_210X30))|pred_attacker(VAR_V_210X30). % 2.36/2.57 0 [] -pred_attacker(VAR_V_214)| -pred_attacker(VAR_V_215)|pred_attacker(tuple_client_A_in_4(VAR_V_214,VAR_V_215)). % 2.36/2.57 0 [] -pred_attacker(tuple_client_A_in_4(VAR_V_222,VAR_V_223))|pred_attacker(VAR_V_222). % 2.36/2.57 0 [] -pred_attacker(tuple_client_A_in_4(VAR_V_225,VAR_V_226))|pred_attacker(VAR_V_226). % 2.36/2.57 0 [] -pred_attacker(VAR_V_229)|pred_attacker(tuple_client_A_in_2(VAR_V_229)). % 2.36/2.57 0 [] -pred_attacker(tuple_client_A_in_2(VAR_V_232))|pred_attacker(VAR_V_232). % 2.36/2.57 0 [] -pred_attacker(VAR_V_235)|pred_attacker(tuple_client_A_in_1(VAR_V_235)). % 2.36/2.57 0 [] -pred_attacker(tuple_client_A_in_1(VAR_V_238))|pred_attacker(VAR_V_238). % 2.36/2.57 0 [] -pred_attacker(VAR_V_242)| -pred_attacker(VAR_V_243)|pred_attacker(constr_aenc(VAR_V_242,VAR_V_243)). % 2.36/2.57 0 [] -pred_attacker(VAR_V_246)| -pred_attacker(VAR_V_247)|pred_attacker(constr_adec(VAR_V_246,VAR_V_247)). % 2.36/2.57 0 [] -pred_attacker(VAR_V_250X30)| -pred_attacker(VAR_V_251)|pred_attacker(constr_add(VAR_V_250X30,VAR_V_251)). % 2.36/2.57 0 [] pred_attacker(constr_ZERO). % 2.36/2.57 0 [] pred_attacker(constr_CONST_4). % 2.36/2.57 0 [] pred_attacker(constr_CONST_3). % 2.36/2.57 0 [] pred_attacker(constr_CONST_2). % 2.36/2.57 0 [] pred_attacker(constr_CONST_1). % 2.36/2.57 0 [] pred_attacker(constr_CONST_0x30). % 2.36/2.57 0 [] -pred_mess(VAR_V_257,VAR_V_256)| -pred_attacker(VAR_V_257)|pred_attacker(VAR_V_256). % 2.36/2.57 0 [] -pred_attacker(VAR_V_259)| -pred_attacker(VAR_V_258)|pred_mess(VAR_V_259,VAR_V_258). % 2.36/2.57 0 [] pred_attacker(name_c). % 2.36/2.57 0 [] pred_attacker(name_D). % 2.36/2.57 0 [] pred_attacker(name_C). % 2.36/2.57 0 [] pred_attacker(name_B). % 2.36/2.57 0 [] pred_attacker(name_A). % 2.36/2.57 0 [] pred_e_qual(VAR_V_261,VAR_V_261). % 2.36/2.57 0 [] pred_attacker(name_new0x2Dname(VAR_V_262)). % 2.36/2.57 0 [] pred_attacker(tuple_out_1(constr_pkey(name_skA))). % 2.36/2.57 0 [] pred_attacker(tuple_out_2(constr_pkey(name_skB))). % 2.36/2.57 0 [] pred_attacker(tuple_out_3(constr_pkey(name_skC))). % 2.36/2.57 0 [] pred_attacker(tuple_out_4(constr_pkey(name_skD))). % 2.36/2.57 0 [] -pred_attacker(tuple_client_A_in_2(VAR_LASTT_336))| -pred_attacker(tuple_client_A_in_1(VAR_PKNEXTT_337))|pred_attacker(tuple_client_A_out_3(name_A,constr_aenc(constr_add(name_Na,name_Sa),VAR_PKNEXTT_337))). % 2.36/2.57 0 [] -pred_attacker(tuple_client_A_in_4(VAR_LASTT_376,VAR_AENC_ADD_NA_SA_SB_SC_SD_377))| -pred_attacker(tuple_client_A_in_2(VAR_LASTT_376))| -pred_attacker(tuple_client_A_in_1(VAR_PKNEXTT_378))|pred_attacker(tuple_client_A_out_5(constr_add(constr_adec(VAR_AENC_ADD_NA_SA_SB_SC_SD_377,name_skA),constr_neg(name_Na)))). % 2.36/2.57 0 [] -pred_attacker(tuple_client_B_in_3(VAR_PREVT_425,VAR_AENC_ADD_NA_SA_426))| -pred_attacker(tuple_client_B_in_2(VAR_PKNEXTT_427))| -pred_attacker(tuple_client_B_in_1(VAR_PREVT_425))|pred_attacker(tuple_client_B_out_4(name_B,constr_aenc(constr_add(constr_adec(VAR_AENC_ADD_NA_SA_426,name_skB),name_Sb),VAR_PKNEXTT_427))). % 2.36/2.57 0 [] -pred_attacker(tuple_client_C_in_3(VAR_PREVT_478,VAR_AENC_ADD_NA_SA_SB_479))| -pred_attacker(tuple_client_C_in_2(VAR_PKNEXTT_480X30))| -pred_attacker(tuple_client_C_in_1(VAR_PREVT_478))|pred_attacker(tuple_client_C_out_4(name_C,constr_aenc(constr_add(constr_adec(VAR_AENC_ADD_NA_SA_SB_479,name_skC),name_Sc),VAR_PKNEXTT_480X30))). % 2.36/2.57 0 [] -pred_attacker(tuple_client_D_in_3(VAR_PREVT_531,VAR_AENC_ADD_NA_SA_SB_SC_532))| -pred_attacker(tuple_client_D_in_2(VAR_PKNEXTT_533))| -pred_attacker(tuple_client_D_in_1(VAR_PREVT_531))|pred_attacker(tuple_client_D_out_4(name_D,constr_aenc(constr_add(constr_adec(VAR_AENC_ADD_NA_SA_SB_SC_532,name_skD),name_Sd),VAR_PKNEXTT_533))). % 2.36/2.57 0 [] -pred_attacker(name_Sa). % 2.36/2.57 end_of_list. % 2.36/2.57 % 2.36/2.57 SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=4. % 2.36/2.57 % 2.36/2.57 This is a Horn set with equality. The strategy will be % 2.36/2.57 Knuth-Bendix and hyper_res, with positive clauses in % 2.36/2.57 sos and nonpositive clauses in usable. % 2.36/2.57 % 2.36/2.57 dependent: set(knuth_bendix). % 2.36/2.57 dependent: set(anl_eq). % 2.36/2.57 dependent: set(para_from). % 2.36/2.57 dependent: set(para_into). % 2.36/2.57 dependent: clear(para_from_right). % 2.36/2.57 dependent: clear(para_into_right). % 2.36/2.57 dependent: set(para_from_vars). % 2.36/2.57 dependent: set(eq_units_both_ways). % 2.36/2.57 dependent: set(dynamic_demod_all). % 2.36/2.57 dependent: set(dynamic_demod). % 2.36/2.57 dependent: set(order_eq). % 2.36/2.57 dependent: set(back_demod). % 2.36/2.57 dependent: set(lrpo). % 2.36/2.57 dependent: set(hyper_res). % 2.36/2.57 dependent: clear(order_hyper). % 2.36/2.57 % 2.36/2.57 ------------> process usable: % 2.36/2.57 ** KEPT (pick-wt=3): 2 [copy,1,flip.1] constr_CONST_1!=constr_CONST_0x30. % 2.36/2.57 ** KEPT (pick-wt=3): 4 [copy,3,flip.1] constr_CONST_2!=constr_CONST_0x30. % 2.36/2.57 ** KEPT (pick-wt=3): 6 [copy,5,flip.1] constr_CONST_3!=constr_CONST_0x30. % 2.36/2.57 ** KEPT (pick-wt=3): 8 [copy,7,flip.1] constr_CONST_4!=constr_CONST_0x30. % 2.36/2.57 ** KEPT (pick-wt=3): 10 [copy,9,flip.1] constr_ZERO!=constr_CONST_0x30. % 2.36/2.57 ** KEPT (pick-wt=3): 12 [copy,11,flip.1] name_A!=constr_CONST_0x30. % 2.36/2.57 ** KEPT (pick-wt=3): 14 [copy,13,flip.1] name_B!=constr_CONST_0x30. % 2.36/2.57 ** KEPT (pick-wt=3): 16 [copy,15,flip.1] name_C!=constr_CONST_0x30. % 2.36/2.57 ** KEPT (pick-wt=3): 18 [copy,17,flip.1] name_D!=constr_CONST_0x30. % 2.36/2.57 ** KEPT (pick-wt=3): 20 [copy,19,flip.1] name_Na!=constr_CONST_0x30. % 2.36/2.57 ** KEPT (pick-wt=3): 22 [copy,21,flip.1] name_Sa!=constr_CONST_0x30. % 2.36/2.57 ** KEPT (pick-wt=3): 24 [copy,23,flip.1] name_Sb!=constr_CONST_0x30. % 2.36/2.57 ** KEPT (pick-wt=3): 26 [copy,25,flip.1] name_Sc!=constr_CONST_0x30. % 2.36/2.57 ** KEPT (pick-wt=3): 28 [copy,27,flip.1] name_Sd!=constr_CONST_0x30. % 2.36/2.57 ** KEPT (pick-wt=3): 30 [copy,29,flip.1] name_c!=constr_CONST_0x30. % 2.36/2.57 ** KEPT (pick-wt=3): 32 [copy,31,flip.1] name_skA!=constr_CONST_0x30. % 2.36/2.57 ** KEPT (pick-wt=3): 34 [copy,33,flip.1] name_skB!=constr_CONST_0x30. % 2.36/2.57 ** KEPT (pick-wt=3): 36 [copy,35,flip.1] name_skC!=constr_CONST_0x30. % 2.36/2.57 ** KEPT (pick-wt=3): 38 [copy,37,flip.1] name_skD!=constr_CONST_0x30. % 2.36/2.57 ** KEPT (pick-wt=3): 40 [copy,39,flip.1] constr_CONST_2!=constr_CONST_1. % 2.36/2.57 ** KEPT (pick-wt=3): 42 [copy,41,flip.1] constr_CONST_3!=constr_CONST_1. % 2.36/2.57 ** KEPT (pick-wt=3): 44 [copy,43,flip.1] constr_CONST_4!=constr_CONST_1. % 2.36/2.57 ** KEPT (pick-wt=3): 46 [copy,45,flip.1] constr_ZERO!=constr_CONST_1. % 2.36/2.57 ** KEPT (pick-wt=3): 48 [copy,47,flip.1] name_A!=constr_CONST_1. % 2.36/2.57 ** KEPT (pick-wt=3): 50 [copy,49,flip.1] name_B!=constr_CONST_1. % 2.36/2.57 ** KEPT (pick-wt=3): 52 [copy,51,flip.1] name_C!=constr_CONST_1. % 2.36/2.57 ** KEPT (pick-wt=3): 54 [copy,53,flip.1] name_D!=constr_CONST_1. % 2.36/2.57 ** KEPT (pick-wt=3): 56 [copy,55,flip.1] name_Na!=constr_CONST_1. % 2.36/2.57 ** KEPT (pick-wt=3): 58 [copy,57,flip.1] name_Sa!=constr_CONST_1. % 2.36/2.57 ** KEPT (pick-wt=3): 60 [copy,59,flip.1] name_Sb!=constr_CONST_1. % 2.36/2.57 ** KEPT (pick-wt=3): 62 [copy,61,flip.1] name_Sc!=constr_CONST_1. % 2.36/2.57 ** KEPT (pick-wt=3): 64 [copy,63,flip.1] name_Sd!=constr_CONST_1. % 2.36/2.57 ** KEPT (pick-wt=3): 66 [copy,65,flip.1] name_c!=constr_CONST_1. % 2.36/2.57 ** KEPT (pick-wt=3): 68 [copy,67,flip.1] name_skA!=constr_CONST_1. % 2.36/2.57 ** KEPT (pick-wt=3): 70 [copy,69,flip.1] name_skB!=constr_CONST_1. % 2.36/2.57 ** KEPT (pick-wt=3): 72 [copy,71,flip.1] name_skC!=constr_CONST_1. % 2.36/2.57 ** KEPT (pick-wt=3): 74 [copy,73,flip.1] name_skD!=constr_CONST_1. % 2.36/2.57 ** KEPT (pick-wt=3): 76 [copy,75,flip.1] constr_CONST_3!=constr_CONST_2. % 2.36/2.57 ** KEPT (pick-wt=3): 78 [copy,77,flip.1] constr_CONST_4!=constr_CONST_2. % 2.36/2.57 ** KEPT (pick-wt=3): 80 [copy,79,flip.1] constr_ZERO!=constr_CONST_2. % 2.36/2.57 ** KEPT (pick-wt=3): 82 [copy,81,flip.1] name_A!=constr_CONST_2. % 2.36/2.57 ** KEPT (pick-wt=3): 84 [copy,83,flip.1] name_B!=constr_CONST_2. % 2.36/2.57 ** KEPT (pick-wt=3): 86 [copy,85,flip.1] name_C!=constr_CONST_2. % 2.36/2.57 ** KEPT (pick-wt=3): 88 [copy,87,flip.1] name_D!=constr_CONST_2. % 2.36/2.57 ** KEPT (pick-wt=3): 90 [copy,89,flip.1] name_Na!=constr_CONST_2. % 2.36/2.57 ** KEPT (pick-wt=3): 92 [copy,91,flip.1] name_Sa!=constr_CONST_2. % 2.36/2.57 ** KEPT (pick-wt=3): 94 [copy,93,flip.1] name_Sb!=constr_CONST_2. % 2.36/2.57 ** KEPT (pick-wt=3): 96 [copy,95,flip.1] name_Sc!=constr_CONST_2. % 2.36/2.57 ** KEPT (pick-wt=3): 98 [copy,97,flip.1] name_Sd!=constr_CONST_2. % 2.36/2.57 ** KEPT (pick-wt=3): 100 [copy,99,flip.1] name_c!=constr_CONST_2. % 2.36/2.57 ** KEPT (pick-wt=3): 102 [copy,101,flip.1] name_skA!=constr_CONST_2. % 2.36/2.57 ** KEPT (pick-wt=3): 104 [copy,103,flip.1] name_skB!=constr_CONST_2. % 2.36/2.57 ** KEPT (pick-wt=3): 106 [copy,105,flip.1] name_skC!=constr_CONST_2. % 2.36/2.57 ** KEPT (pick-wt=3): 108 [copy,107,flip.1] name_skD!=constr_CONST_2. % 2.36/2.57 ** KEPT (pick-wt=3): 110 [copy,109,flip.1] constr_CONST_4!=constr_CONST_3. % 2.36/2.57 ** KEPT (pick-wt=3): 112 [copy,111,flip.1] constr_ZERO!=constr_CONST_3. % 2.36/2.57 ** KEPT (pick-wt=3): 114 [copy,113,flip.1] name_A!=constr_CONST_3. % 2.36/2.57 ** KEPT (pick-wt=3): 116 [copy,115,flip.1] name_B!=constr_CONST_3. % 2.36/2.57 ** KEPT (pick-wt=3): 118 [copy,117,flip.1] name_C!=constr_CONST_3. % 2.36/2.57 ** KEPT (pick-wt=3): 120 [copy,119,flip.1] name_D!=constr_CONST_3. % 2.36/2.57 ** KEPT (pick-wt=3): 122 [copy,121,flip.1] name_Na!=constr_CONST_3. % 2.36/2.57 ** KEPT (pick-wt=3): 124 [copy,123,flip.1] name_Sa!=constr_CONST_3. % 2.36/2.57 ** KEPT (pick-wt=3): 126 [copy,125,flip.1] name_Sb!=constr_CONST_3. % 2.36/2.57 ** KEPT (pick-wt=3): 128 [copy,127,flip.1] name_Sc!=constr_CONST_3. % 2.36/2.57 ** KEPT (pick-wt=3): 130 [copy,129,flip.1] name_Sd!=constr_CONST_3. % 2.36/2.57 ** KEPT (pick-wt=3): 132 [copy,131,flip.1] name_c!=constr_CONST_3. % 2.36/2.57 ** KEPT (pick-wt=3): 134 [copy,133,flip.1] name_skA!=constr_CONST_3. % 2.36/2.57 ** KEPT (pick-wt=3): 136 [copy,135,flip.1] name_skB!=constr_CONST_3. % 2.36/2.57 ** KEPT (pick-wt=3): 138 [copy,137,flip.1] name_skC!=constr_CONST_3. % 2.36/2.57 ** KEPT (pick-wt=3): 140 [copy,139,flip.1] name_skD!=constr_CONST_3. % 2.36/2.57 ** KEPT (pick-wt=3): 142 [copy,141,flip.1] constr_ZERO!=constr_CONST_4. % 2.36/2.57 ** KEPT (pick-wt=3): 144 [copy,143,flip.1] name_A!=constr_CONST_4. % 2.36/2.57 ** KEPT (pick-wt=3): 146 [copy,145,flip.1] name_B!=constr_CONST_4. % 2.36/2.57 ** KEPT (pick-wt=3): 148 [copy,147,flip.1] name_C!=constr_CONST_4. % 2.36/2.57 ** KEPT (pick-wt=3): 150 [copy,149,flip.1] name_D!=constr_CONST_4. % 2.36/2.57 ** KEPT (pick-wt=3): 152 [copy,151,flip.1] name_Na!=constr_CONST_4. % 2.36/2.57 ** KEPT (pick-wt=3): 154 [copy,153,flip.1] name_Sa!=constr_CONST_4. % 2.36/2.57 ** KEPT (pick-wt=3): 156 [copy,155,flip.1] name_Sb!=constr_CONST_4. % 2.36/2.57 ** KEPT (pick-wt=3): 158 [copy,157,flip.1] name_Sc!=constr_CONST_4. % 2.36/2.57 ** KEPT (pick-wt=3): 160 [copy,159,flip.1] name_Sd!=constr_CONST_4. % 2.36/2.57 ** KEPT (pick-wt=3): 162 [copy,161,flip.1] name_c!=constr_CONST_4. % 2.36/2.57 ** KEPT (pick-wt=3): 164 [copy,163,flip.1] name_skA!=constr_CONST_4. % 2.36/2.57 ** KEPT (pick-wt=3): 166 [copy,165,flip.1] name_skB!=constr_CONST_4. % 2.36/2.57 ** KEPT (pick-wt=3): 168 [copy,167,flip.1] name_skC!=constr_CONST_4. % 2.36/2.57 ** KEPT (pick-wt=3): 170 [copy,169,flip.1] name_skD!=constr_CONST_4. % 2.36/2.57 ** KEPT (pick-wt=3): 172 [copy,171,flip.1] name_A!=constr_ZERO. % 2.36/2.57 ** KEPT (pick-wt=3): 174 [copy,173,flip.1] name_B!=constr_ZERO. % 2.36/2.57 ** KEPT (pick-wt=3): 176 [copy,175,flip.1] name_C!=constr_ZERO. % 2.36/2.57 ** KEPT (pick-wt=3): 178 [copy,177,flip.1] name_D!=constr_ZERO. % 2.36/2.57 ** KEPT (pick-wt=3): 180 [copy,179,flip.1] name_Na!=constr_ZERO. % 2.36/2.57 ** KEPT (pick-wt=3): 182 [copy,181,flip.1] name_Sa!=constr_ZERO. % 2.36/2.57 ** KEPT (pick-wt=3): 184 [copy,183,flip.1] name_Sb!=constr_ZERO. % 2.36/2.57 ** KEPT (pick-wt=3): 186 [copy,185,flip.1] name_Sc!=constr_ZERO. % 2.36/2.57 ** KEPT (pick-wt=3): 188 [copy,187,flip.1] name_Sd!=constr_ZERO. % 2.36/2.57 ** KEPT (pick-wt=3): 190 [copy,189,flip.1] name_c!=constr_ZERO. % 2.36/2.57 ** KEPT (pick-wt=3): 192 [copy,191,flip.1] name_skA!=constr_ZERO. % 2.36/2.57 ** KEPT (pick-wt=3): 194 [copy,193,flip.1] name_skB!=constr_ZERO. % 2.36/2.57 ** KEPT (pick-wt=3): 196 [copy,195,flip.1] name_skC!=constr_ZERO. % 2.36/2.57 ** KEPT (pick-wt=3): 198 [copy,197,flip.1] name_skD!=constr_ZERO. % 2.36/2.57 ** KEPT (pick-wt=3): 200 [copy,199,flip.1] name_B!=name_A. % 2.36/2.57 ** KEPT (pick-wt=3): 202 [copy,201,flip.1] name_C!=name_A. % 2.36/2.57 ** KEPT (pick-wt=3): 204 [copy,203,flip.1] name_D!=name_A. % 2.36/2.57 ** KEPT (pick-wt=3): 206 [copy,205,flip.1] name_Na!=name_A. % 2.36/2.57 ** KEPT (pick-wt=3): 208 [copy,207,flip.1] name_Sa!=name_A. % 2.36/2.57 ** KEPT (pick-wt=3): 210 [copy,209,flip.1] name_Sb!=name_A. % 2.36/2.57 ** KEPT (pick-wt=3): 212 [copy,211,flip.1] name_Sc!=name_A. % 2.36/2.57 ** KEPT (pick-wt=3): 214 [copy,213,flip.1] name_Sd!=name_A. % 2.36/2.57 ** KEPT (pick-wt=3): 216 [copy,215,flip.1] name_c!=name_A. % 2.36/2.57 ** KEPT (pick-wt=3): 218 [copy,217,flip.1] name_skA!=name_A. % 2.36/2.57 ** KEPT (pick-wt=3): 220 [copy,219,flip.1] name_skB!=name_A. % 2.36/2.57 ** KEPT (pick-wt=3): 222 [copy,221,flip.1] name_skC!=name_A. % 2.36/2.57 ** KEPT (pick-wt=3): 224 [copy,223,flip.1] name_skD!=name_A. % 2.36/2.57 ** KEPT (pick-wt=3): 226 [copy,225,flip.1] name_C!=name_B. % 2.36/2.57 ** KEPT (pick-wt=3): 228 [copy,227,flip.1] name_D!=name_B. % 2.36/2.57 ** KEPT (pick-wt=3): 230 [copy,229,flip.1] name_Na!=name_B. % 2.36/2.57 ** KEPT (pick-wt=3): 232 [copy,231,flip.1] name_Sa!=name_B. % 2.36/2.57 ** KEPT (pick-wt=3): 234 [copy,233,flip.1] name_Sb!=name_B. % 2.36/2.57 ** KEPT (pick-wt=3): 236 [copy,235,flip.1] name_Sc!=name_B. % 2.36/2.57 ** KEPT (pick-wt=3): 238 [copy,237,flip.1] name_Sd!=name_B. % 2.36/2.57 ** KEPT (pick-wt=3): 240 [copy,239,flip.1] name_c!=name_B. % 2.36/2.57 ** KEPT (pick-wt=3): 242 [copy,241,flip.1] name_skA!=name_B. % 2.36/2.57 ** KEPT (pick-wt=3): 244 [copy,243,flip.1] name_skB!=name_B. % 2.36/2.57 ** KEPT (pick-wt=3): 246 [copy,245,flip.1] name_skC!=name_B. % 2.36/2.57 ** KEPT (pick-wt=3): 248 [copy,247,flip.1] name_skD!=name_B. % 2.36/2.57 ** KEPT (pick-wt=3): 250 [copy,249,flip.1] name_D!=name_C. % 2.36/2.57 ** KEPT (pick-wt=3): 252 [copy,251,flip.1] name_Na!=name_C. % 2.36/2.57 ** KEPT (pick-wt=3): 254 [copy,253,flip.1] name_Sa!=name_C. % 2.36/2.57 ** KEPT (pick-wt=3): 256 [copy,255,flip.1] name_Sb!=name_C. % 2.36/2.57 ** KEPT (pick-wt=3): 258 [copy,257,flip.1] name_Sc!=name_C. % 2.36/2.57 ** KEPT (pick-wt=3): 260 [copy,259,flip.1] name_Sd!=name_C. % 2.36/2.57 ** KEPT (pick-wt=3): 262 [copy,261,flip.1] name_c!=name_C. % 2.36/2.57 ** KEPT (pick-wt=3): 264 [copy,263,flip.1] name_skA!=name_C. % 2.36/2.57 ** KEPT (pick-wt=3): 266 [copy,265,flip.1] name_skB!=name_C. % 2.36/2.57 ** KEPT (pick-wt=3): 268 [copy,267,flip.1] name_skC!=name_C. % 2.36/2.57 ** KEPT (pick-wt=3): 270 [copy,269,flip.1] name_skD!=name_C. % 2.36/2.57 ** KEPT (pick-wt=3): 272 [copy,271,flip.1] name_Na!=name_D. % 2.36/2.57 ** KEPT (pick-wt=3): 274 [copy,273,flip.1] name_Sa!=name_D. % 2.36/2.57 ** KEPT (pick-wt=3): 276 [copy,275,flip.1] name_Sb!=name_D. % 2.36/2.57 ** KEPT (pick-wt=3): 278 [copy,277,flip.1] name_Sc!=name_D. % 2.36/2.57 ** KEPT (pick-wt=3): 280 [copy,279,flip.1] name_Sd!=name_D. % 2.36/2.57 ** KEPT (pick-wt=3): 282 [copy,281,flip.1] name_c!=name_D. % 2.36/2.57 ** KEPT (pick-wt=3): 284 [copy,283,flip.1] name_skA!=name_D. % 2.36/2.57 ** KEPT (pick-wt=3): 286 [copy,285,flip.1] name_skB!=name_D. % 2.36/2.57 ** KEPT (pick-wt=3): 288 [copy,287,flip.1] name_skC!=name_D. % 2.36/2.57 ** KEPT (pick-wt=3): 290 [copy,289,flip.1] name_skD!=name_D. % 2.36/2.57 ** KEPT (pick-wt=3): 292 [copy,291,flip.1] name_Sa!=name_Na. % 2.36/2.57 ** KEPT (pick-wt=3): 294 [copy,293,flip.1] name_Sb!=name_Na. % 2.36/2.57 ** KEPT (pick-wt=3): 296 [copy,295,flip.1] name_Sc!=name_Na. % 2.36/2.57 ** KEPT (pick-wt=3): 298 [copy,297,flip.1] name_Sd!=name_Na. % 2.36/2.57 ** KEPT (pick-wt=3): 300 [copy,299,flip.1] name_c!=name_Na. % 2.36/2.57 ** KEPT (pick-wt=3): 302 [copy,301,flip.1] name_skA!=name_Na. % 2.36/2.57 ** KEPT (pick-wt=3): 304 [copy,303,flip.1] name_skB!=name_Na. % 2.36/2.57 ** KEPT (pick-wt=3): 306 [copy,305,flip.1] name_skC!=name_Na. % 2.36/2.57 ** KEPT (pick-wt=3): 308 [copy,307,flip.1] name_skD!=name_Na. % 2.36/2.57 ** KEPT (pick-wt=3): 310 [copy,309,flip.1] name_Sb!=name_Sa. % 2.36/2.57 ** KEPT (pick-wt=3): 312 [copy,311,flip.1] name_Sc!=name_Sa. % 2.36/2.57 ** KEPT (pick-wt=3): 314 [copy,313,flip.1] name_Sd!=name_Sa. % 2.36/2.57 ** KEPT (pick-wt=3): 316 [copy,315,flip.1] name_c!=name_Sa. % 2.36/2.57 ** KEPT (pick-wt=3): 318 [copy,317,flip.1] name_skA!=name_Sa. % 2.36/2.57 ** KEPT (pick-wt=3): 320 [copy,319,flip.1] name_skB!=name_Sa. % 2.36/2.57 ** KEPT (pick-wt=3): 322 [copy,321,flip.1] name_skC!=name_Sa. % 2.36/2.57 ** KEPT (pick-wt=3): 324 [copy,323,flip.1] name_skD!=name_Sa. % 2.36/2.57 ** KEPT (pick-wt=3): 326 [copy,325,flip.1] name_Sc!=name_Sb. % 2.36/2.57 ** KEPT (pick-wt=3): 328 [copy,327,flip.1] name_Sd!=name_Sb. % 2.36/2.57 ** KEPT (pick-wt=3): 330 [copy,329,flip.1] name_c!=name_Sb. % 2.36/2.57 ** KEPT (pick-wt=3): 332 [copy,331,flip.1] name_skA!=name_Sb. % 2.36/2.57 ** KEPT (pick-wt=3): 334 [copy,333,flip.1] name_skB!=name_Sb. % 2.36/2.57 ** KEPT (pick-wt=3): 336 [copy,335,flip.1] name_skC!=name_Sb. % 2.36/2.57 ** KEPT (pick-wt=3): 338 [copy,337,flip.1] name_skD!=name_Sb. % 2.36/2.57 ** KEPT (pick-wt=3): 340 [copy,339,flip.1] name_Sd!=name_Sc. % 2.36/2.57 ** KEPT (pick-wt=3): 342 [copy,341,flip.1] name_c!=name_Sc. % 2.36/2.57 ** KEPT (pick-wt=3): 344 [copy,343,flip.1] name_skA!=name_Sc. % 2.36/2.57 ** KEPT (pick-wt=3): 346 [copy,345,flip.1] name_skB!=name_Sc. % 2.36/2.57 ** KEPT (pick-wt=3): 348 [copy,347,flip.1] name_skC!=name_Sc. % 2.36/2.57 ** KEPT (pick-wt=3): 350 [copy,349,flip.1] name_skD!=name_Sc. % 2.36/2.57 ** KEPT (pick-wt=3): 352 [copy,351,flip.1] name_c!=name_Sd. % 2.36/2.57 ** KEPT (pick-wt=3): 354 [copy,353,flip.1] name_skA!=name_Sd. % 2.36/2.57 ** KEPT (pick-wt=3): 356 [copy,355,flip.1] name_skB!=name_Sd. % 2.36/2.57 ** KEPT (pick-wt=3): 358 [copy,357,flip.1] name_skC!=name_Sd. % 2.36/2.57 ** KEPT (pick-wt=3): 360 [copy,359,flip.1] name_skD!=name_Sd. % 2.36/2.57 ** KEPT (pick-wt=3): 362 [copy,361,flip.1] name_skA!=name_c. % 2.36/2.57 ** KEPT (pick-wt=3): 364 [copy,363,flip.1] name_skB!=name_c. % 2.36/2.57 ** KEPT (pick-wt=3): 366 [copy,365,flip.1] name_skC!=name_c. % 2.36/2.57 ** KEPT (pick-wt=3): 368 [copy,367,flip.1] name_skD!=name_c. % 2.36/2.57 ** KEPT (pick-wt=3): 370 [copy,369,flip.1] name_skB!=name_skA. % 2.36/2.57 ** KEPT (pick-wt=3): 372 [copy,371,flip.1] name_skC!=name_skA. % 2.36/2.57 ** KEPT (pick-wt=3): 374 [copy,373,flip.1] name_skD!=name_skA. % 2.36/2.57 ** KEPT (pick-wt=3): 376 [copy,375,flip.1] name_skC!=name_skB. % 2.36/2.57 ** KEPT (pick-wt=3): 378 [copy,377,flip.1] name_skD!=name_skB. % 2.36/2.57 ** KEPT (pick-wt=3): 380 [copy,379,flip.1] name_skD!=name_skC. % 2.36/2.57 ** KEPT (pick-wt=5): 381 [] -pred_attacker(A)|pred_attacker(constr_pkey(A)). % 2.36/2.57 ** KEPT (pick-wt=5): 382 [] -pred_attacker(A)|pred_attacker(tuple_out_4(A)). % 2.36/2.57 ** KEPT (pick-wt=5): 383 [] -pred_attacker(tuple_out_4(A))|pred_attacker(A). % 2.36/2.57 ** KEPT (pick-wt=5): 384 [] -pred_attacker(A)|pred_attacker(tuple_out_3(A)). % 2.36/2.57 ** KEPT (pick-wt=5): 385 [] -pred_attacker(tuple_out_3(A))|pred_attacker(A). % 2.36/2.57 ** KEPT (pick-wt=5): 386 [] -pred_attacker(A)|pred_attacker(tuple_out_2(A)). % 2.36/2.57 ** KEPT (pick-wt=5): 387 [] -pred_attacker(tuple_out_2(A))|pred_attacker(A). % 2.36/2.57 ** KEPT (pick-wt=5): 388 [] -pred_attacker(A)|pred_attacker(tuple_out_1(A)). % 2.36/2.57 ** KEPT (pick-wt=5): 389 [] -pred_attacker(tuple_out_1(A))|pred_attacker(A). % 2.36/2.57 ** KEPT (pick-wt=5): 390 [] -pred_attacker(A)|pred_attacker(constr_neg(A)). % 2.36/2.57 ** KEPT (pick-wt=8): 391 [] -pred_attacker(A)| -pred_attacker(B)|pred_attacker(tuple_client_D_out_4(A,B)). % 2.36/2.57 ** KEPT (pick-wt=6): 392 [] -pred_attacker(tuple_client_D_out_4(A,B))|pred_attacker(A). % 2.36/2.57 ** KEPT (pick-wt=6): 393 [] -pred_attacker(tuple_client_D_out_4(A,B))|pred_attacker(B). % 2.36/2.57 ** KEPT (pick-wt=8): 394 [] -pred_attacker(A)| -pred_attacker(B)|pred_attacker(tuple_client_D_in_3(A,B)). % 2.36/2.57 ** KEPT (pick-wt=6): 395 [] -pred_attacker(tuple_client_D_in_3(A,B))|pred_attacker(A). % 2.36/2.57 ** KEPT (pick-wt=6): 396 [] -pred_attacker(tuple_client_D_in_3(A,B))|pred_attacker(B). % 2.36/2.57 ** KEPT (pick-wt=5): 397 [] -pred_attacker(A)|pred_attacker(tuple_client_D_in_2(A)). % 2.36/2.57 ** KEPT (pick-wt=5): 398 [] -pred_attacker(tuple_client_D_in_2(A))|pred_attacker(A). % 2.36/2.57 ** KEPT (pick-wt=5): 399 [] -pred_attacker(A)|pred_attacker(tuple_client_D_in_1(A)). % 2.36/2.57 ** KEPT (pick-wt=5): 400 [] -pred_attacker(tuple_client_D_in_1(A))|pred_attacker(A). % 2.36/2.57 ** KEPT (pick-wt=8): 401 [] -pred_attacker(A)| -pred_attacker(B)|pred_attacker(tuple_client_C_out_4(A,B)). % 2.36/2.57 ** KEPT (pick-wt=6): 402 [] -pred_attacker(tuple_client_C_out_4(A,B))|pred_attacker(A). % 2.36/2.57 ** KEPT (pick-wt=6): 403 [] -pred_attacker(tuple_client_C_out_4(A,B))|pred_attacker(B). % 2.36/2.57 ** KEPT (pick-wt=8): 404 [] -pred_attacker(A)| -pred_attacker(B)|pred_attacker(tuple_client_C_in_3(A,B)). % 2.36/2.57 ** KEPT (pick-wt=6): 405 [] -pred_attacker(tuple_client_C_in_3(A,B))|pred_attacker(A). % 2.36/2.57 ** KEPT (pick-wt=6): 406 [] -pred_attacker(tuple_client_C_in_3(A,B))|pred_attacker(B). % 2.36/2.57 ** KEPT (pick-wt=5): 407 [] -pred_attacker(A)|pred_attacker(tuple_client_C_in_2(A)). % 2.36/2.57 ** KEPT (pick-wt=5): 408 [] -pred_attacker(tuple_client_C_in_2(A))|pred_attacker(A). % 2.36/2.57 ** KEPT (pick-wt=5): 409 [] -pred_attacker(A)|pred_attacker(tuple_client_C_in_1(A)). % 2.36/2.57 ** KEPT (pick-wt=5): 410 [] -pred_attacker(tuple_client_C_in_1(A))|pred_attacker(A). % 2.36/2.57 ** KEPT (pick-wt=8): 411 [] -pred_attacker(A)| -pred_attacker(B)|pred_attacker(tuple_client_B_out_4(A,B)). % 2.36/2.57 ** KEPT (pick-wt=6): 412 [] -pred_attacker(tuple_client_B_out_4(A,B))|pred_attacker(A). % 2.36/2.57 ** KEPT (pick-wt=6): 413 [] -pred_attacker(tuple_client_B_out_4(A,B))|pred_attacker(B). % 2.36/2.57 ** KEPT (pick-wt=8): 414 [] -pred_attacker(A)| -pred_attacker(B)|pred_attacker(tuple_client_B_in_3(A,B)). % 2.36/2.57 ** KEPT (pick-wt=6): 415 [] -pred_attacker(tuple_client_B_in_3(A,B))|pred_attacker(A). % 2.36/2.57 ** KEPT (pick-wt=6): 416 [] -pred_attacker(tuple_client_B_in_3(A,B))|pred_attacker(B). % 2.36/2.57 ** KEPT (pick-wt=5): 417 [] -pred_attacker(A)|pred_attacker(tuple_client_B_in_2(A)). % 2.36/2.57 ** KEPT (pick-wt=5): 418 [] -pred_attacker(tuple_client_B_in_2(A))|pred_attacker(A). % 2.36/2.57 ** KEPT (pick-wt=5): 419 [] -pred_attacker(A)|pred_attacker(tuple_client_B_in_1(A)). % 2.36/2.57 ** KEPT (pick-wt=5): 420 [] -pred_attacker(tuple_client_B_in_1(A))|pred_attacker(A). % 2.36/2.57 ** KEPT (pick-wt=5): 421 [] -pred_attacker(A)|pred_attacker(tuple_client_A_out_5(A)). % 2.36/2.57 ** KEPT (pick-wt=5): 422 [] -pred_attacker(tuple_client_A_out_5(A))|pred_attacker(A). % 2.36/2.57 ** KEPT (pick-wt=8): 423 [] -pred_attacker(A)| -pred_attacker(B)|pred_attacker(tuple_client_A_out_3(A,B)). % 2.36/2.57 ** KEPT (pick-wt=6): 424 [] -pred_attacker(tuple_client_A_out_3(A,B))|pred_attacker(A). % 2.36/2.57 ** KEPT (pick-wt=6): 425 [] -pred_attacker(tuple_client_A_out_3(A,B))|pred_attacker(B). % 2.36/2.57 ** KEPT (pick-wt=8): 426 [] -pred_attacker(A)| -pred_attacker(B)|pred_attacker(tuple_client_A_in_4(A,B)). % 2.36/2.57 ** KEPT (pick-wt=6): 427 [] -pred_attacker(tuple_client_A_in_4(A,B))|pred_attacker(A). % 2.36/2.57 ** KEPT (pick-wt=6): 428 [] -pred_attacker(tuple_client_A_in_4(A,B))|pred_attacker(B). % 2.36/2.57 ** KEPT (pick-wt=5): 429 [] -pred_attacker(A)|pred_attacker(tuple_client_A_in_2(A)). % 2.36/2.57 ** KEPT (pick-wt=5): 430 [] -pred_attacker(tuple_client_A_in_2(A))|pred_attacker(A). % 2.36/2.57 ** KEPT (pick-wt=5): 431 [] -pred_attacker(A)|pred_attacker(tuple_client_A_in_1(A)). % 2.36/2.57 ** KEPT (pick-wt=5): 432 [] -pred_attacker(tuple_client_A_in_1(A))|pred_attacker(A). % 2.36/2.57 ** KEPT (pick-wt=8): 433 [] -pred_attacker(A)| -pred_attacker(B)|pred_attacker(constr_aenc(A,B)). % 2.36/2.57 ** KEPT (pick-wt=8): 434 [] -pred_attacker(A)| -pred_attacker(B)|pred_attacker(constr_adec(A,B)). % 2.36/2.57 ** KEPT (pick-wt=8): 435 [] -pred_attacker(A)| -pred_attacker(B)|pred_attacker(constr_add(A,B)). % 2.36/2.57 ** KEPT (pick-wt=7): 436 [] -pred_mess(A,B)| -pred_attacker(A)|pred_attacker(B). % 2.36/2.57 ** KEPT (pick-wt=7): 437 [] -pred_attacker(A)| -pred_attacker(B)|pred_mess(A,B). % 2.36/2.57 ** KEPT (pick-wt=14): 438 [] -pred_attacker(tuple_client_A_in_2(A))| -pred_attacker(tuple_client_A_in_1(B))|pred_attacker(tuple_client_A_out_3(name_A,constr_aenc(constr_add(name_Na,name_Sa),B))). % 2.36/2.57 ** KEPT (pick-wt=18): 439 [] -pred_attacker(tuple_client_A_in_4(A,B))| -pred_attacker(tuple_client_A_in_2(A))| -pred_attacker(tuple_client_A_in_1(C))|pred_attacker(tuple_client_A_out_5(constr_add(constr_adec(B,name_skA),constr_neg(name_Na)))). % 2.36/2.57 ** KEPT (pick-wt=20): 440 [] -pred_attacker(tuple_client_B_in_3(A,B))| -pred_attacker(tuple_client_B_in_2(C))| -pred_attacker(tuple_client_B_in_1(A))|pred_attacker(tuple_client_B_out_4(name_B,constr_aenc(constr_add(constr_adec(B,name_skB),name_Sb),C))). % 62.06/62.18 ** KEPT (pick-wt=20): 441 [] -pred_attacker(tuple_client_C_in_3(A,B))| -pred_attacker(tuple_client_C_in_2(C))| -pred_attacker(tuple_client_C_in_1(A))|pred_attacker(tuple_client_C_out_4(name_C,constr_aenc(constr_add(constr_adec(B,name_skC),name_Sc),C))). % 62.06/62.18 ** KEPT (pick-wt=20): 442 [] -pred_attacker(tuple_client_D_in_3(A,B))| -pred_attacker(tuple_client_D_in_2(C))| -pred_attacker(tuple_client_D_in_1(A))|pred_attacker(tuple_client_D_out_4(name_D,constr_aenc(constr_add(constr_adec(B,name_skD),name_Sd),C))). % 62.06/62.18 ** KEPT (pick-wt=2): 443 [] -pred_attacker(name_Sa). % 62.06/62.18 % 62.06/62.18 ------------> process sos: % 62.06/62.18 ** KEPT (pick-wt=3): 444 [] A=A. % 62.06/62.18 ** KEPT (pick-wt=8): 445 [] constr_adec(constr_aenc(A,constr_pkey(B)),B)=A. % 62.06/62.18 ---> New Demodulator: 446 [new_demod,445] constr_adec(constr_aenc(A,constr_pkey(B)),B)=A. % 62.06/62.18 ** KEPT (pick-wt=6): 447 [] constr_add(A,constr_neg(A))=constr_ZERO. % 62.06/62.18 ---> New Demodulator: 448 [new_demod,447] constr_add(A,constr_neg(A))=constr_ZERO. % 62.06/62.18 ** KEPT (pick-wt=5): 449 [] constr_add(A,constr_ZERO)=A. % 62.06/62.18 ---> New Demodulator: 450 [new_demod,449] constr_add(A,constr_ZERO)=A. % 62.06/62.18 ** KEPT (pick-wt=7): 451 [] constr_add(A,B)=constr_add(B,A). % 62.06/62.18 ** KEPT (pick-wt=11): 453 [copy,452,flip.1] constr_add(constr_add(A,B),C)=constr_add(A,constr_add(B,C)). % 62.06/62.18 ---> New Demodulator: 454 [new_demod,453] constr_add(constr_add(A,B),C)=constr_add(A,constr_add(B,C)). % 62.06/62.18 ** KEPT (pick-wt=2): 455 [] pred_attacker(tuple_true). % 62.06/62.18 ** KEPT (pick-wt=2): 456 [] pred_attacker(tuple_false). % 62.06/62.18 ** KEPT (pick-wt=2): 457 [] pred_attacker(constr_ZERO). % 62.06/62.18 ** KEPT (pick-wt=2): 458 [] pred_attacker(constr_CONST_4). % 62.06/62.18 ** KEPT (pick-wt=2): 459 [] pred_attacker(constr_CONST_3). % 62.06/62.18 ** KEPT (pick-wt=2): 460 [] pred_attacker(constr_CONST_2). % 62.06/62.18 ** KEPT (pick-wt=2): 461 [] pred_attacker(constr_CONST_1). % 62.06/62.18 ** KEPT (pick-wt=2): 462 [] pred_attacker(constr_CONST_0x30). % 62.06/62.18 ** KEPT (pick-wt=2): 463 [] pred_attacker(name_c). % 62.06/62.18 ** KEPT (pick-wt=2): 464 [] pred_attacker(name_D). % 62.06/62.18 ** KEPT (pick-wt=2): 465 [] pred_attacker(name_C). % 62.06/62.18 ** KEPT (pick-wt=2): 466 [] pred_attacker(name_B). % 62.06/62.18 ** KEPT (pick-wt=2): 467 [] pred_attacker(name_A). % 62.06/62.18 ** KEPT (pick-wt=3): 468 [] pred_e_qual(A,A). % 62.06/62.18 ** KEPT (pick-wt=3): 469 [] pred_attacker(name_new0x2Dname(A)). % 62.06/62.18 ** KEPT (pick-wt=4): 470 [] pred_attacker(tuple_out_1(constr_pkey(name_skA))). % 62.06/62.18 ** KEPT (pick-wt=4): 471 [] pred_attacker(tuple_out_2(constr_pkey(name_skB))). % 62.06/62.18 ** KEPT (pick-wt=4): 472 [] pred_attacker(tuple_out_3(constr_pkey(name_skC))). % 62.06/62.18 ** KEPT (pick-wt=4): 473 [] pred_attacker(tuple_out_4(constr_pkey(name_skD))). % 62.06/62.18 Following clause subsumed by 444 during input processing: 0 [copy,444,flip.1] A=A. % 62.06/62.18 >>>> Starting back demodulation with 446. % 62.06/62.18 >>>> Starting back demodulation with 448. % 62.06/62.18 >>>> Starting back demodulation with 450. % 62.06/62.18 Following clause subsumed by 451 during input processing: 0 [copy,451,flip.1] constr_add(A,B)=constr_add(B,A). % 62.06/62.18 >>>> Starting back demodulation with 454. % 62.06/62.18 % 62.06/62.18 ======= end of input processing ======= % 62.06/62.18 % 62.06/62.18 =========== start of search =========== % 62.06/62.18 % 62.06/62.18 % 62.06/62.18 Resetting weight limit to 3. % 62.06/62.18 % 62.06/62.18 % 62.06/62.18 Resetting weight limit to 3. % 62.06/62.18 % 62.06/62.18 sos_size=2558 % 62.06/62.18 % 62.06/62.18 Search stopped because sos empty. % 62.06/62.18 % 62.06/62.18 % 62.06/62.18 Search stopped because sos empty. % 62.06/62.18 % 62.06/62.18 ============ end of search ============ % 62.06/62.18 % 62.06/62.18 -------------- statistics ------------- % 62.06/62.18 clauses given 2582 % 62.06/62.18 clauses generated 67709530 % 62.06/62.18 clauses kept 2835 % 62.06/62.18 clauses forward subsumed 4098 % 62.06/62.18 clauses back subsumed 0 % 62.06/62.18 Kbytes malloced 6835 % 62.06/62.18 % 62.06/62.18 ----------- times (seconds) ----------- % 62.06/62.18 user CPU time 59.62 (0 hr, 0 min, 59 sec) % 62.06/62.18 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 62.06/62.18 wall-clock time 61 (0 hr, 1 min, 1 sec) % 62.06/62.18 % 62.06/62.18 Process 19763 finished Wed Jul 27 02:59:01 2022 % 62.06/62.18 Otter interrupted % 62.06/62.18 PROOF NOT FOUND %------------------------------------------------------------------------------