%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWW953+1 : TPTP v8.1.0. Released v7.4.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n011.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:13 EDT 2022 % Result : Unknown 23.21s 23.38s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWW953+1 : TPTP v8.1.0. Released v7.4.0. % 0.07/0.12 % Command : otter-tptp-script %s % 0.12/0.33 % Computer : n011.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:49:55 EDT 2022 % 0.12/0.33 % CPUTime : % 2.29/2.46 ----- Otter 3.3f, August 2004 ----- % 2.29/2.46 The process was started by sandbox on n011.cluster.edu, % 2.29/2.46 Wed Jul 27 02:49:55 2022 % 2.29/2.46 The command was "./otter". The process ID is 31578. % 2.29/2.46 % 2.29/2.46 set(prolog_style_variables). % 2.29/2.46 set(auto). % 2.29/2.46 dependent: set(auto1). % 2.29/2.46 dependent: set(process_input). % 2.29/2.46 dependent: clear(print_kept). % 2.29/2.46 dependent: clear(print_new_demod). % 2.29/2.46 dependent: clear(print_back_demod). % 2.29/2.46 dependent: clear(print_back_sub). % 2.29/2.46 dependent: set(control_memory). % 2.29/2.46 dependent: assign(max_mem, 12000). % 2.29/2.46 dependent: assign(pick_given_ratio, 4). % 2.29/2.46 dependent: assign(stats_level, 1). % 2.29/2.46 dependent: assign(max_seconds, 10800). % 2.29/2.46 clear(print_given). % 2.29/2.46 % 2.29/2.46 formula_list(usable). % 2.29/2.46 all A (A=A). % 2.29/2.46 constr_CONST_0x30!=constr_CONST_1. % 2.29/2.46 constr_CONST_0x30!=constr_CONST_2. % 2.29/2.46 constr_CONST_0x30!=constr_CONST_3. % 2.29/2.46 constr_CONST_0x30!=constr_CONST_4. % 2.29/2.46 constr_CONST_0x30!=constr_QUERY_REQ. % 2.29/2.46 constr_CONST_0x30!=constr_ZERO. % 2.29/2.46 constr_CONST_0x30!=name_EPC. % 2.29/2.46 constr_CONST_0x30!=name_PIN1. % 2.29/2.46 constr_CONST_0x30!=name_PIN2. % 2.29/2.46 constr_CONST_0x30!=name_S. % 2.29/2.46 constr_CONST_0x30!=name_c. % 2.29/2.46 constr_CONST_0x30!=name_r1. % 2.29/2.46 constr_CONST_0x30!=name_r1_from_1st_round. % 2.29/2.46 constr_CONST_0x30!=name_r2_from_1st_round. % 2.29/2.46 constr_CONST_1!=constr_CONST_2. % 2.29/2.46 constr_CONST_1!=constr_CONST_3. % 2.29/2.46 constr_CONST_1!=constr_CONST_4. % 2.29/2.46 constr_CONST_1!=constr_QUERY_REQ. % 2.29/2.46 constr_CONST_1!=constr_ZERO. % 2.29/2.46 constr_CONST_1!=name_EPC. % 2.29/2.46 constr_CONST_1!=name_PIN1. % 2.29/2.46 constr_CONST_1!=name_PIN2. % 2.29/2.46 constr_CONST_1!=name_S. % 2.29/2.46 constr_CONST_1!=name_c. % 2.29/2.46 constr_CONST_1!=name_r1. % 2.29/2.46 constr_CONST_1!=name_r1_from_1st_round. % 2.29/2.46 constr_CONST_1!=name_r2_from_1st_round. % 2.29/2.46 constr_CONST_2!=constr_CONST_3. % 2.29/2.46 constr_CONST_2!=constr_CONST_4. % 2.29/2.46 constr_CONST_2!=constr_QUERY_REQ. % 2.29/2.46 constr_CONST_2!=constr_ZERO. % 2.29/2.46 constr_CONST_2!=name_EPC. % 2.29/2.46 constr_CONST_2!=name_PIN1. % 2.29/2.46 constr_CONST_2!=name_PIN2. % 2.29/2.46 constr_CONST_2!=name_S. % 2.29/2.46 constr_CONST_2!=name_c. % 2.29/2.46 constr_CONST_2!=name_r1. % 2.29/2.46 constr_CONST_2!=name_r1_from_1st_round. % 2.29/2.46 constr_CONST_2!=name_r2_from_1st_round. % 2.29/2.46 constr_CONST_3!=constr_CONST_4. % 2.29/2.46 constr_CONST_3!=constr_QUERY_REQ. % 2.29/2.46 constr_CONST_3!=constr_ZERO. % 2.29/2.46 constr_CONST_3!=name_EPC. % 2.29/2.46 constr_CONST_3!=name_PIN1. % 2.29/2.46 constr_CONST_3!=name_PIN2. % 2.29/2.46 constr_CONST_3!=name_S. % 2.29/2.46 constr_CONST_3!=name_c. % 2.29/2.46 constr_CONST_3!=name_r1. % 2.29/2.46 constr_CONST_3!=name_r1_from_1st_round. % 2.29/2.46 constr_CONST_3!=name_r2_from_1st_round. % 2.29/2.46 constr_CONST_4!=constr_QUERY_REQ. % 2.29/2.46 constr_CONST_4!=constr_ZERO. % 2.29/2.46 constr_CONST_4!=name_EPC. % 2.29/2.46 constr_CONST_4!=name_PIN1. % 2.29/2.46 constr_CONST_4!=name_PIN2. % 2.29/2.46 constr_CONST_4!=name_S. % 2.29/2.46 constr_CONST_4!=name_c. % 2.29/2.46 constr_CONST_4!=name_r1. % 2.29/2.46 constr_CONST_4!=name_r1_from_1st_round. % 2.29/2.46 constr_CONST_4!=name_r2_from_1st_round. % 2.29/2.46 constr_QUERY_REQ!=constr_ZERO. % 2.29/2.46 constr_QUERY_REQ!=name_EPC. % 2.29/2.46 constr_QUERY_REQ!=name_PIN1. % 2.29/2.46 constr_QUERY_REQ!=name_PIN2. % 2.29/2.46 constr_QUERY_REQ!=name_S. % 2.29/2.46 constr_QUERY_REQ!=name_c. % 2.29/2.46 constr_QUERY_REQ!=name_r1. % 2.29/2.46 constr_QUERY_REQ!=name_r1_from_1st_round. % 2.29/2.46 constr_QUERY_REQ!=name_r2_from_1st_round. % 2.29/2.46 constr_ZERO!=name_EPC. % 2.29/2.46 constr_ZERO!=name_PIN1. % 2.29/2.46 constr_ZERO!=name_PIN2. % 2.29/2.46 constr_ZERO!=name_S. % 2.29/2.46 constr_ZERO!=name_c. % 2.29/2.46 constr_ZERO!=name_r1. % 2.29/2.46 constr_ZERO!=name_r1_from_1st_round. % 2.29/2.46 constr_ZERO!=name_r2_from_1st_round. % 2.29/2.46 name_EPC!=name_PIN1. % 2.29/2.46 name_EPC!=name_PIN2. % 2.29/2.46 name_EPC!=name_S. % 2.29/2.46 name_EPC!=name_c. % 2.29/2.46 name_EPC!=name_r1. % 2.29/2.46 name_EPC!=name_r1_from_1st_round. % 2.29/2.46 name_EPC!=name_r2_from_1st_round. % 2.29/2.46 name_PIN1!=name_PIN2. % 2.29/2.46 name_PIN1!=name_S. % 2.29/2.46 name_PIN1!=name_c. % 2.29/2.46 name_PIN1!=name_r1. % 2.29/2.46 name_PIN1!=name_r1_from_1st_round. % 2.29/2.46 name_PIN1!=name_r2_from_1st_round. % 2.29/2.46 name_PIN2!=name_S. % 2.29/2.46 name_PIN2!=name_c. % 2.29/2.46 name_PIN2!=name_r1. % 2.29/2.46 name_PIN2!=name_r1_from_1st_round. % 2.29/2.46 name_PIN2!=name_r2_from_1st_round. % 2.29/2.46 name_S!=name_c. % 2.29/2.46 name_S!=name_r1. % 2.29/2.46 name_S!=name_r1_from_1st_round. % 2.29/2.46 name_S!=name_r2_from_1st_round. % 2.29/2.46 name_c!=name_r1. % 2.29/2.46 name_c!=name_r1_from_1st_round. % 2.29/2.46 name_c!=name_r2_from_1st_round. % 2.29/2.46 name_r1!=name_r1_from_1st_round. % 2.29/2.46 name_r1!=name_r2_from_1st_round. % 2.29/2.46 name_r1_from_1st_round!=name_r2_from_1st_round. % 2.29/2.46 constr_add(constr_ZERO,constr_ZERO)=constr_ZERO. % 2.29/2.46 all VAR_X_23 (constr_sub(VAR_X_23,constr_ZERO)=VAR_X_23). % 2.29/2.46 all VAR_X_22 (constr_add(VAR_X_22,constr_ZERO)=VAR_X_22). % 2.29/2.46 all VAR_X_21 (constr_sub(VAR_X_21,VAR_X_21)=constr_ZERO). % 2.29/2.46 all VAR_X_19 VAR_Y_20X30 (constr_sub(constr_add(VAR_X_19,VAR_Y_20X30),VAR_Y_20X30)=VAR_X_19). % 2.29/2.46 all VAR_X_16 VAR_Y_17 VAR_Z_18 (constr_add(VAR_X_16,constr_add(VAR_Y_17,VAR_Z_18))=constr_add(constr_add(VAR_X_16,VAR_Y_17),VAR_Z_18)). % 2.29/2.46 all VAR_X_14 VAR_Y_15 (constr_add(VAR_X_14,VAR_Y_15)=constr_add(VAR_Y_15,VAR_X_14)). % 2.29/2.46 all VAR_X_11 VAR_Y_12 VAR_Z_13 (constr_concat(constr_concat(VAR_X_11,VAR_Y_12),VAR_Z_13)=constr_concat(VAR_X_11,constr_concat(VAR_Y_12,VAR_Z_13))). % 2.29/2.46 all VAR_X_10X30 (constr_xor(VAR_X_10X30,VAR_X_10X30)=constr_ZERO). % 2.29/2.46 all VAR_X_9 (constr_xor(VAR_X_9,constr_ZERO)=VAR_X_9). % 2.29/2.46 all VAR_X_7 VAR_Y_8 (constr_xor(VAR_X_7,VAR_Y_8)=constr_xor(VAR_Y_8,VAR_X_7)). % 2.29/2.46 all VAR_X_0X30 VAR_Y_0X30 VAR_Z_0X30 (constr_xor(VAR_X_0X30,constr_xor(VAR_Y_0X30,VAR_Z_0X30))=constr_xor(constr_xor(VAR_X_0X30,VAR_Y_0X30),VAR_Z_0X30)). % 2.29/2.46 all VAR_V_49 VAR_V_50X30 (pred_attacker(VAR_V_49)&pred_attacker(VAR_V_50X30)->pred_attacker(constr_xor(VAR_V_49,VAR_V_50X30))). % 2.29/2.46 pred_attacker(tuple_true). % 2.29/2.46 all VAR_V_53 VAR_V_54 (pred_attacker(VAR_V_53)&pred_attacker(VAR_V_54)->pred_attacker(constr_sub(VAR_V_53,VAR_V_54))). % 2.29/2.46 all VAR_V_57 (pred_attacker(VAR_V_57)->pred_attacker(tuple_knowledge_from_1st_round_out_5(VAR_V_57))). % 2.29/2.46 all VAR_V_60X30 (pred_attacker(tuple_knowledge_from_1st_round_out_5(VAR_V_60X30))->pred_attacker(VAR_V_60X30)). % 2.29/2.46 all VAR_V_63 (pred_attacker(VAR_V_63)->pred_attacker(tuple_knowledge_from_1st_round_out_4(VAR_V_63))). % 2.29/2.46 all VAR_V_66 (pred_attacker(tuple_knowledge_from_1st_round_out_4(VAR_V_66))->pred_attacker(VAR_V_66)). % 2.29/2.46 all VAR_V_69 (pred_attacker(VAR_V_69)->pred_attacker(tuple_knowledge_from_1st_round_out_3(VAR_V_69))). % 2.29/2.46 all VAR_V_72 (pred_attacker(tuple_knowledge_from_1st_round_out_3(VAR_V_72))->pred_attacker(VAR_V_72)). % 2.29/2.46 all VAR_V_75 (pred_attacker(VAR_V_75)->pred_attacker(tuple_knowledge_from_1st_round_out_2(VAR_V_75))). % 2.29/2.46 all VAR_V_78 (pred_attacker(tuple_knowledge_from_1st_round_out_2(VAR_V_78))->pred_attacker(VAR_V_78)). % 2.29/2.46 all VAR_V_81 (pred_attacker(VAR_V_81)->pred_attacker(tuple_knowledge_from_1st_round_out_1(VAR_V_81))). % 2.29/2.46 all VAR_V_84 (pred_attacker(tuple_knowledge_from_1st_round_out_1(VAR_V_84))->pred_attacker(VAR_V_84)). % 2.29/2.46 pred_attacker(tuple_false). % 2.29/2.46 all VAR_V_87 (pred_attacker(VAR_V_87)->pred_attacker(constr_f(VAR_V_87))). % 2.29/2.46 all VAR_V_90X30 VAR_V_91 (pred_attacker(VAR_V_90X30)&pred_attacker(VAR_V_91)->pred_attacker(constr_concat(VAR_V_90X30,VAR_V_91))). % 2.29/2.46 all VAR_V_94 VAR_V_95 (pred_attacker(VAR_V_94)&pred_attacker(VAR_V_95)->pred_attacker(constr_add(VAR_V_94,VAR_V_95))). % 2.29/2.46 pred_attacker(constr_ZERO). % 2.29/2.46 all VAR_V_97 (pred_attacker(VAR_V_97)->pred_attacker(tuple_T_out_6(VAR_V_97))). % 2.29/2.46 all VAR_V_10X300X30 (pred_attacker(tuple_T_out_6(VAR_V_10X300X30))->pred_attacker(VAR_V_10X300X30)). % 2.29/2.46 all VAR_V_10X303 (pred_attacker(VAR_V_10X303)->pred_attacker(tuple_T_out_4(VAR_V_10X303))). % 2.29/2.46 all VAR_V_10X306 (pred_attacker(tuple_T_out_4(VAR_V_10X306))->pred_attacker(VAR_V_10X306)). % 2.29/2.46 all VAR_V_10X309 (pred_attacker(VAR_V_10X309)->pred_attacker(tuple_T_out_2(VAR_V_10X309))). % 2.29/2.46 all VAR_V_112 (pred_attacker(tuple_T_out_2(VAR_V_112))->pred_attacker(VAR_V_112)). % 2.29/2.46 all VAR_V_115 (pred_attacker(VAR_V_115)->pred_attacker(tuple_T_in_5(VAR_V_115))). % 2.29/2.46 all VAR_V_118 (pred_attacker(tuple_T_in_5(VAR_V_118))->pred_attacker(VAR_V_118)). % 2.29/2.46 all VAR_V_122 VAR_V_123 (pred_attacker(VAR_V_122)&pred_attacker(VAR_V_123)->pred_attacker(tuple_T_in_3(VAR_V_122,VAR_V_123))). % 2.29/2.46 all VAR_V_130X30 VAR_V_131 (pred_attacker(tuple_T_in_3(VAR_V_130X30,VAR_V_131))->pred_attacker(VAR_V_130X30)). % 2.29/2.46 all VAR_V_133 VAR_V_134 (pred_attacker(tuple_T_in_3(VAR_V_133,VAR_V_134))->pred_attacker(VAR_V_134)). % 2.29/2.46 all VAR_V_137 (pred_attacker(VAR_V_137)->pred_attacker(tuple_T_in_1(VAR_V_137))). % 2.29/2.46 all VAR_V_140X30 (pred_attacker(tuple_T_in_1(VAR_V_140X30))->pred_attacker(VAR_V_140X30)). % 2.29/2.46 pred_attacker(constr_QUERY_REQ). % 2.29/2.46 pred_attacker(constr_CONST_4). % 2.29/2.46 pred_attacker(constr_CONST_3). % 2.29/2.46 pred_attacker(constr_CONST_2). % 2.29/2.46 pred_attacker(constr_CONST_1). % 2.29/2.46 pred_attacker(constr_CONST_0x30). % 2.29/2.46 all VAR_V_143 (pred_attacker(VAR_V_143)->pred_attacker(constr_ACK(VAR_V_143))). % 2.29/2.46 all VAR_V_148 VAR_V_149 (pred_mess(VAR_V_149,VAR_V_148)&pred_attacker(VAR_V_149)->pred_attacker(VAR_V_148)). % 2.29/2.46 all VAR_V_150X30 VAR_V_151 (pred_attacker(VAR_V_151)&pred_attacker(VAR_V_150X30)->pred_mess(VAR_V_151,VAR_V_150X30)). % 2.29/2.46 pred_attacker(name_c). % 2.29/2.46 all VAR_V_153 pred_e_qual(VAR_V_153,VAR_V_153). % 2.29/2.46 all VAR_V_154 pred_attacker(name_new0x2Dname(VAR_V_154)). % 2.29/2.46 pred_attacker(tuple_knowledge_from_1st_round_out_1(constr_QUERY_REQ)). % 2.29/2.46 pred_attacker(tuple_knowledge_from_1st_round_out_2(constr_xor(name_r1_from_1st_round,name_PIN1))). % 2.29/2.46 pred_attacker(tuple_knowledge_from_1st_round_out_3(constr_ACK(constr_xor(name_r1_from_1st_round,name_PIN1)))). % 2.29/2.46 pred_attacker(tuple_knowledge_from_1st_round_out_4(constr_xor(constr_add(constr_concat(constr_ZERO,constr_concat(name_r1_from_1st_round,constr_concat(constr_xor(constr_xor(name_r2_from_1st_round,name_PIN2),name_r1_from_1st_round),constr_f(constr_xor(constr_xor(name_r2_from_1st_round,name_PIN2),name_r1_from_1st_round))))),name_S),name_EPC))). % 2.29/2.46 pred_attacker(tuple_knowledge_from_1st_round_out_5(constr_xor(name_PIN1,constr_f(constr_xor(name_r2_from_1st_round,constr_xor(name_PIN2,name_r1_from_1st_round)))))). % 2.29/2.46 pred_attacker(tuple_T_in_1(constr_QUERY_REQ))->pred_attacker(tuple_T_out_2(constr_xor(name_r1,name_PIN1))). % 2.29/2.46 all VAR_R2_421 (pred_attacker(tuple_T_in_3(constr_ACK(constr_xor(name_r1,name_PIN1)),VAR_R2_421))&pred_attacker(tuple_T_in_1(constr_QUERY_REQ))->pred_attacker(tuple_T_out_4(constr_xor(constr_add(constr_concat(constr_ZERO,constr_concat(name_r1,constr_concat(constr_xor(constr_xor(VAR_R2_421,name_PIN2),name_r1),constr_f(constr_xor(constr_xor(VAR_R2_421,name_PIN2),name_r1))))),name_S),name_EPC)))). % 2.29/2.46 -pred_attacker(name_objective). % 2.29/2.46 end_of_list. % 2.29/2.46 % 2.29/2.46 -------> usable clausifies to: % 2.29/2.46 % 2.29/2.46 list(usable). % 2.29/2.46 0 [] A=A. % 2.29/2.46 0 [] constr_CONST_0x30!=constr_CONST_1. % 2.29/2.46 0 [] constr_CONST_0x30!=constr_CONST_2. % 2.29/2.46 0 [] constr_CONST_0x30!=constr_CONST_3. % 2.29/2.46 0 [] constr_CONST_0x30!=constr_CONST_4. % 2.29/2.46 0 [] constr_CONST_0x30!=constr_QUERY_REQ. % 2.29/2.46 0 [] constr_CONST_0x30!=constr_ZERO. % 2.29/2.46 0 [] constr_CONST_0x30!=name_EPC. % 2.29/2.46 0 [] constr_CONST_0x30!=name_PIN1. % 2.29/2.46 0 [] constr_CONST_0x30!=name_PIN2. % 2.29/2.46 0 [] constr_CONST_0x30!=name_S. % 2.29/2.46 0 [] constr_CONST_0x30!=name_c. % 2.29/2.46 0 [] constr_CONST_0x30!=name_r1. % 2.29/2.46 0 [] constr_CONST_0x30!=name_r1_from_1st_round. % 2.29/2.46 0 [] constr_CONST_0x30!=name_r2_from_1st_round. % 2.29/2.46 0 [] constr_CONST_1!=constr_CONST_2. % 2.29/2.46 0 [] constr_CONST_1!=constr_CONST_3. % 2.29/2.46 0 [] constr_CONST_1!=constr_CONST_4. % 2.29/2.46 0 [] constr_CONST_1!=constr_QUERY_REQ. % 2.29/2.46 0 [] constr_CONST_1!=constr_ZERO. % 2.29/2.46 0 [] constr_CONST_1!=name_EPC. % 2.29/2.46 0 [] constr_CONST_1!=name_PIN1. % 2.29/2.46 0 [] constr_CONST_1!=name_PIN2. % 2.29/2.46 0 [] constr_CONST_1!=name_S. % 2.29/2.46 0 [] constr_CONST_1!=name_c. % 2.29/2.46 0 [] constr_CONST_1!=name_r1. % 2.29/2.46 0 [] constr_CONST_1!=name_r1_from_1st_round. % 2.29/2.46 0 [] constr_CONST_1!=name_r2_from_1st_round. % 2.29/2.46 0 [] constr_CONST_2!=constr_CONST_3. % 2.29/2.46 0 [] constr_CONST_2!=constr_CONST_4. % 2.29/2.46 0 [] constr_CONST_2!=constr_QUERY_REQ. % 2.29/2.46 0 [] constr_CONST_2!=constr_ZERO. % 2.29/2.46 0 [] constr_CONST_2!=name_EPC. % 2.29/2.46 0 [] constr_CONST_2!=name_PIN1. % 2.29/2.46 0 [] constr_CONST_2!=name_PIN2. % 2.29/2.46 0 [] constr_CONST_2!=name_S. % 2.29/2.46 0 [] constr_CONST_2!=name_c. % 2.29/2.46 0 [] constr_CONST_2!=name_r1. % 2.29/2.46 0 [] constr_CONST_2!=name_r1_from_1st_round. % 2.29/2.46 0 [] constr_CONST_2!=name_r2_from_1st_round. % 2.29/2.46 0 [] constr_CONST_3!=constr_CONST_4. % 2.29/2.46 0 [] constr_CONST_3!=constr_QUERY_REQ. % 2.29/2.46 0 [] constr_CONST_3!=constr_ZERO. % 2.29/2.46 0 [] constr_CONST_3!=name_EPC. % 2.29/2.46 0 [] constr_CONST_3!=name_PIN1. % 2.29/2.46 0 [] constr_CONST_3!=name_PIN2. % 2.29/2.46 0 [] constr_CONST_3!=name_S. % 2.29/2.46 0 [] constr_CONST_3!=name_c. % 2.29/2.46 0 [] constr_CONST_3!=name_r1. % 2.29/2.46 0 [] constr_CONST_3!=name_r1_from_1st_round. % 2.29/2.46 0 [] constr_CONST_3!=name_r2_from_1st_round. % 2.29/2.46 0 [] constr_CONST_4!=constr_QUERY_REQ. % 2.29/2.46 0 [] constr_CONST_4!=constr_ZERO. % 2.29/2.46 0 [] constr_CONST_4!=name_EPC. % 2.29/2.46 0 [] constr_CONST_4!=name_PIN1. % 2.29/2.46 0 [] constr_CONST_4!=name_PIN2. % 2.29/2.46 0 [] constr_CONST_4!=name_S. % 2.29/2.46 0 [] constr_CONST_4!=name_c. % 2.29/2.46 0 [] constr_CONST_4!=name_r1. % 2.29/2.46 0 [] constr_CONST_4!=name_r1_from_1st_round. % 2.29/2.46 0 [] constr_CONST_4!=name_r2_from_1st_round. % 2.29/2.46 0 [] constr_QUERY_REQ!=constr_ZERO. % 2.29/2.46 0 [] constr_QUERY_REQ!=name_EPC. % 2.29/2.46 0 [] constr_QUERY_REQ!=name_PIN1. % 2.29/2.46 0 [] constr_QUERY_REQ!=name_PIN2. % 2.29/2.46 0 [] constr_QUERY_REQ!=name_S. % 2.29/2.46 0 [] constr_QUERY_REQ!=name_c. % 2.29/2.46 0 [] constr_QUERY_REQ!=name_r1. % 2.29/2.46 0 [] constr_QUERY_REQ!=name_r1_from_1st_round. % 2.29/2.46 0 [] constr_QUERY_REQ!=name_r2_from_1st_round. % 2.29/2.46 0 [] constr_ZERO!=name_EPC. % 2.29/2.46 0 [] constr_ZERO!=name_PIN1. % 2.29/2.46 0 [] constr_ZERO!=name_PIN2. % 2.29/2.46 0 [] constr_ZERO!=name_S. % 2.29/2.46 0 [] constr_ZERO!=name_c. % 2.29/2.46 0 [] constr_ZERO!=name_r1. % 2.29/2.46 0 [] constr_ZERO!=name_r1_from_1st_round. % 2.29/2.46 0 [] constr_ZERO!=name_r2_from_1st_round. % 2.29/2.46 0 [] name_EPC!=name_PIN1. % 2.29/2.46 0 [] name_EPC!=name_PIN2. % 2.29/2.46 0 [] name_EPC!=name_S. % 2.29/2.46 0 [] name_EPC!=name_c. % 2.29/2.46 0 [] name_EPC!=name_r1. % 2.29/2.46 0 [] name_EPC!=name_r1_from_1st_round. % 2.29/2.46 0 [] name_EPC!=name_r2_from_1st_round. % 2.29/2.46 0 [] name_PIN1!=name_PIN2. % 2.29/2.46 0 [] name_PIN1!=name_S. % 2.29/2.46 0 [] name_PIN1!=name_c. % 2.29/2.46 0 [] name_PIN1!=name_r1. % 2.29/2.46 0 [] name_PIN1!=name_r1_from_1st_round. % 2.29/2.46 0 [] name_PIN1!=name_r2_from_1st_round. % 2.29/2.46 0 [] name_PIN2!=name_S. % 2.29/2.46 0 [] name_PIN2!=name_c. % 2.29/2.46 0 [] name_PIN2!=name_r1. % 2.29/2.46 0 [] name_PIN2!=name_r1_from_1st_round. % 2.29/2.46 0 [] name_PIN2!=name_r2_from_1st_round. % 2.29/2.46 0 [] name_S!=name_c. % 2.29/2.46 0 [] name_S!=name_r1. % 2.29/2.46 0 [] name_S!=name_r1_from_1st_round. % 2.29/2.46 0 [] name_S!=name_r2_from_1st_round. % 2.29/2.46 0 [] name_c!=name_r1. % 2.29/2.46 0 [] name_c!=name_r1_from_1st_round. % 2.29/2.46 0 [] name_c!=name_r2_from_1st_round. % 2.29/2.46 0 [] name_r1!=name_r1_from_1st_round. % 2.29/2.46 0 [] name_r1!=name_r2_from_1st_round. % 2.29/2.46 0 [] name_r1_from_1st_round!=name_r2_from_1st_round. % 2.29/2.46 0 [] constr_add(constr_ZERO,constr_ZERO)=constr_ZERO. % 2.29/2.46 0 [] constr_sub(VAR_X_23,constr_ZERO)=VAR_X_23. % 2.29/2.46 0 [] constr_add(VAR_X_22,constr_ZERO)=VAR_X_22. % 2.29/2.46 0 [] constr_sub(VAR_X_21,VAR_X_21)=constr_ZERO. % 2.29/2.46 0 [] constr_sub(constr_add(VAR_X_19,VAR_Y_20X30),VAR_Y_20X30)=VAR_X_19. % 2.29/2.46 0 [] constr_add(VAR_X_16,constr_add(VAR_Y_17,VAR_Z_18))=constr_add(constr_add(VAR_X_16,VAR_Y_17),VAR_Z_18). % 2.29/2.46 0 [] constr_add(VAR_X_14,VAR_Y_15)=constr_add(VAR_Y_15,VAR_X_14). % 2.29/2.46 0 [] constr_concat(constr_concat(VAR_X_11,VAR_Y_12),VAR_Z_13)=constr_concat(VAR_X_11,constr_concat(VAR_Y_12,VAR_Z_13)). % 2.29/2.46 0 [] constr_xor(VAR_X_10X30,VAR_X_10X30)=constr_ZERO. % 2.29/2.46 0 [] constr_xor(VAR_X_9,constr_ZERO)=VAR_X_9. % 2.29/2.46 0 [] constr_xor(VAR_X_7,VAR_Y_8)=constr_xor(VAR_Y_8,VAR_X_7). % 2.29/2.46 0 [] constr_xor(VAR_X_0X30,constr_xor(VAR_Y_0X30,VAR_Z_0X30))=constr_xor(constr_xor(VAR_X_0X30,VAR_Y_0X30),VAR_Z_0X30). % 2.29/2.46 0 [] -pred_attacker(VAR_V_49)| -pred_attacker(VAR_V_50X30)|pred_attacker(constr_xor(VAR_V_49,VAR_V_50X30)). % 2.29/2.46 0 [] pred_attacker(tuple_true). % 2.29/2.46 0 [] -pred_attacker(VAR_V_53)| -pred_attacker(VAR_V_54)|pred_attacker(constr_sub(VAR_V_53,VAR_V_54)). % 2.29/2.46 0 [] -pred_attacker(VAR_V_57)|pred_attacker(tuple_knowledge_from_1st_round_out_5(VAR_V_57)). % 2.29/2.46 0 [] -pred_attacker(tuple_knowledge_from_1st_round_out_5(VAR_V_60X30))|pred_attacker(VAR_V_60X30). % 2.29/2.46 0 [] -pred_attacker(VAR_V_63)|pred_attacker(tuple_knowledge_from_1st_round_out_4(VAR_V_63)). % 2.29/2.46 0 [] -pred_attacker(tuple_knowledge_from_1st_round_out_4(VAR_V_66))|pred_attacker(VAR_V_66). % 2.29/2.46 0 [] -pred_attacker(VAR_V_69)|pred_attacker(tuple_knowledge_from_1st_round_out_3(VAR_V_69)). % 2.29/2.46 0 [] -pred_attacker(tuple_knowledge_from_1st_round_out_3(VAR_V_72))|pred_attacker(VAR_V_72). % 2.29/2.46 0 [] -pred_attacker(VAR_V_75)|pred_attacker(tuple_knowledge_from_1st_round_out_2(VAR_V_75)). % 2.29/2.46 0 [] -pred_attacker(tuple_knowledge_from_1st_round_out_2(VAR_V_78))|pred_attacker(VAR_V_78). % 2.29/2.46 0 [] -pred_attacker(VAR_V_81)|pred_attacker(tuple_knowledge_from_1st_round_out_1(VAR_V_81)). % 2.29/2.46 0 [] -pred_attacker(tuple_knowledge_from_1st_round_out_1(VAR_V_84))|pred_attacker(VAR_V_84). % 2.29/2.46 0 [] pred_attacker(tuple_false). % 2.29/2.46 0 [] -pred_attacker(VAR_V_87)|pred_attacker(constr_f(VAR_V_87)). % 2.29/2.46 0 [] -pred_attacker(VAR_V_90X30)| -pred_attacker(VAR_V_91)|pred_attacker(constr_concat(VAR_V_90X30,VAR_V_91)). % 2.29/2.46 0 [] -pred_attacker(VAR_V_94)| -pred_attacker(VAR_V_95)|pred_attacker(constr_add(VAR_V_94,VAR_V_95)). % 2.29/2.46 0 [] pred_attacker(constr_ZERO). % 2.29/2.46 0 [] -pred_attacker(VAR_V_97)|pred_attacker(tuple_T_out_6(VAR_V_97)). % 2.29/2.46 0 [] -pred_attacker(tuple_T_out_6(VAR_V_10X300X30))|pred_attacker(VAR_V_10X300X30). % 2.29/2.46 0 [] -pred_attacker(VAR_V_10X303)|pred_attacker(tuple_T_out_4(VAR_V_10X303)). % 2.29/2.46 0 [] -pred_attacker(tuple_T_out_4(VAR_V_10X306))|pred_attacker(VAR_V_10X306). % 2.29/2.46 0 [] -pred_attacker(VAR_V_10X309)|pred_attacker(tuple_T_out_2(VAR_V_10X309)). % 2.29/2.46 0 [] -pred_attacker(tuple_T_out_2(VAR_V_112))|pred_attacker(VAR_V_112). % 2.29/2.46 0 [] -pred_attacker(VAR_V_115)|pred_attacker(tuple_T_in_5(VAR_V_115)). % 2.29/2.46 0 [] -pred_attacker(tuple_T_in_5(VAR_V_118))|pred_attacker(VAR_V_118). % 2.29/2.46 0 [] -pred_attacker(VAR_V_122)| -pred_attacker(VAR_V_123)|pred_attacker(tuple_T_in_3(VAR_V_122,VAR_V_123)). % 2.29/2.46 0 [] -pred_attacker(tuple_T_in_3(VAR_V_130X30,VAR_V_131))|pred_attacker(VAR_V_130X30). % 2.29/2.46 0 [] -pred_attacker(tuple_T_in_3(VAR_V_133,VAR_V_134))|pred_attacker(VAR_V_134). % 2.29/2.46 0 [] -pred_attacker(VAR_V_137)|pred_attacker(tuple_T_in_1(VAR_V_137)). % 2.29/2.46 0 [] -pred_attacker(tuple_T_in_1(VAR_V_140X30))|pred_attacker(VAR_V_140X30). % 2.29/2.46 0 [] pred_attacker(constr_QUERY_REQ). % 2.29/2.46 0 [] pred_attacker(constr_CONST_4). % 2.29/2.46 0 [] pred_attacker(constr_CONST_3). % 2.29/2.46 0 [] pred_attacker(constr_CONST_2). % 2.29/2.46 0 [] pred_attacker(constr_CONST_1). % 2.29/2.46 0 [] pred_attacker(constr_CONST_0x30). % 2.29/2.46 0 [] -pred_attacker(VAR_V_143)|pred_attacker(constr_ACK(VAR_V_143)). % 2.29/2.46 0 [] -pred_mess(VAR_V_149,VAR_V_148)| -pred_attacker(VAR_V_149)|pred_attacker(VAR_V_148). % 2.29/2.46 0 [] -pred_attacker(VAR_V_151)| -pred_attacker(VAR_V_150X30)|pred_mess(VAR_V_151,VAR_V_150X30). % 2.29/2.46 0 [] pred_attacker(name_c). % 2.29/2.46 0 [] pred_e_qual(VAR_V_153,VAR_V_153). % 2.29/2.46 0 [] pred_attacker(name_new0x2Dname(VAR_V_154)). % 2.29/2.46 0 [] pred_attacker(tuple_knowledge_from_1st_round_out_1(constr_QUERY_REQ)). % 2.29/2.46 0 [] pred_attacker(tuple_knowledge_from_1st_round_out_2(constr_xor(name_r1_from_1st_round,name_PIN1))). % 2.29/2.46 0 [] pred_attacker(tuple_knowledge_from_1st_round_out_3(constr_ACK(constr_xor(name_r1_from_1st_round,name_PIN1)))). % 2.29/2.46 0 [] pred_attacker(tuple_knowledge_from_1st_round_out_4(constr_xor(constr_add(constr_concat(constr_ZERO,constr_concat(name_r1_from_1st_round,constr_concat(constr_xor(constr_xor(name_r2_from_1st_round,name_PIN2),name_r1_from_1st_round),constr_f(constr_xor(constr_xor(name_r2_from_1st_round,name_PIN2),name_r1_from_1st_round))))),name_S),name_EPC))). % 2.29/2.46 0 [] pred_attacker(tuple_knowledge_from_1st_round_out_5(constr_xor(name_PIN1,constr_f(constr_xor(name_r2_from_1st_round,constr_xor(name_PIN2,name_r1_from_1st_round)))))). % 2.29/2.46 0 [] -pred_attacker(tuple_T_in_1(constr_QUERY_REQ))|pred_attacker(tuple_T_out_2(constr_xor(name_r1,name_PIN1))). % 2.29/2.46 0 [] -pred_attacker(tuple_T_in_3(constr_ACK(constr_xor(name_r1,name_PIN1)),VAR_R2_421))| -pred_attacker(tuple_T_in_1(constr_QUERY_REQ))|pred_attacker(tuple_T_out_4(constr_xor(constr_add(constr_concat(constr_ZERO,constr_concat(name_r1,constr_concat(constr_xor(constr_xor(VAR_R2_421,name_PIN2),name_r1),constr_f(constr_xor(constr_xor(VAR_R2_421,name_PIN2),name_r1))))),name_S),name_EPC))). % 2.29/2.46 0 [] -pred_attacker(name_objective). % 2.29/2.46 end_of_list. % 2.29/2.46 % 2.29/2.46 SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=3. % 2.29/2.46 % 2.29/2.46 This is a Horn set with equality. The strategy will be % 2.29/2.46 Knuth-Bendix and hyper_res, with positive clauses in % 2.29/2.46 sos and nonpositive clauses in usable. % 2.29/2.46 % 2.29/2.46 dependent: set(knuth_bendix). % 2.29/2.46 dependent: set(anl_eq). % 2.29/2.46 dependent: set(para_from). % 2.29/2.46 dependent: set(para_into). % 2.29/2.46 dependent: clear(para_from_right). % 2.29/2.46 dependent: clear(para_into_right). % 2.29/2.46 dependent: set(para_from_vars). % 2.29/2.46 dependent: set(eq_units_both_ways). % 2.29/2.46 dependent: set(dynamic_demod_all). % 2.29/2.46 dependent: set(dynamic_demod). % 2.29/2.46 dependent: set(order_eq). % 2.29/2.46 dependent: set(back_demod). % 2.29/2.46 dependent: set(lrpo). % 2.29/2.46 dependent: set(hyper_res). % 2.29/2.46 dependent: clear(order_hyper). % 2.29/2.46 % 2.29/2.46 ------------> process usable: % 2.29/2.46 ** KEPT (pick-wt=3): 2 [copy,1,flip.1] constr_CONST_1!=constr_CONST_0x30. % 2.29/2.46 ** KEPT (pick-wt=3): 4 [copy,3,flip.1] constr_CONST_2!=constr_CONST_0x30. % 2.29/2.46 ** KEPT (pick-wt=3): 6 [copy,5,flip.1] constr_CONST_3!=constr_CONST_0x30. % 2.29/2.46 ** KEPT (pick-wt=3): 8 [copy,7,flip.1] constr_CONST_4!=constr_CONST_0x30. % 2.29/2.46 ** KEPT (pick-wt=3): 10 [copy,9,flip.1] constr_QUERY_REQ!=constr_CONST_0x30. % 2.29/2.46 ** KEPT (pick-wt=3): 12 [copy,11,flip.1] constr_ZERO!=constr_CONST_0x30. % 2.29/2.46 ** KEPT (pick-wt=3): 14 [copy,13,flip.1] name_EPC!=constr_CONST_0x30. % 2.29/2.46 ** KEPT (pick-wt=3): 16 [copy,15,flip.1] name_PIN1!=constr_CONST_0x30. % 2.29/2.46 ** KEPT (pick-wt=3): 18 [copy,17,flip.1] name_PIN2!=constr_CONST_0x30. % 2.29/2.46 ** KEPT (pick-wt=3): 20 [copy,19,flip.1] name_S!=constr_CONST_0x30. % 2.29/2.46 ** KEPT (pick-wt=3): 22 [copy,21,flip.1] name_c!=constr_CONST_0x30. % 2.29/2.46 ** KEPT (pick-wt=3): 24 [copy,23,flip.1] name_r1!=constr_CONST_0x30. % 2.29/2.46 ** KEPT (pick-wt=3): 26 [copy,25,flip.1] name_r1_from_1st_round!=constr_CONST_0x30. % 2.29/2.46 ** KEPT (pick-wt=3): 28 [copy,27,flip.1] name_r2_from_1st_round!=constr_CONST_0x30. % 2.29/2.46 ** KEPT (pick-wt=3): 30 [copy,29,flip.1] constr_CONST_2!=constr_CONST_1. % 2.29/2.46 ** KEPT (pick-wt=3): 32 [copy,31,flip.1] constr_CONST_3!=constr_CONST_1. % 2.29/2.46 ** KEPT (pick-wt=3): 34 [copy,33,flip.1] constr_CONST_4!=constr_CONST_1. % 2.29/2.46 ** KEPT (pick-wt=3): 36 [copy,35,flip.1] constr_QUERY_REQ!=constr_CONST_1. % 2.29/2.46 ** KEPT (pick-wt=3): 38 [copy,37,flip.1] constr_ZERO!=constr_CONST_1. % 2.29/2.46 ** KEPT (pick-wt=3): 40 [copy,39,flip.1] name_EPC!=constr_CONST_1. % 2.29/2.46 ** KEPT (pick-wt=3): 42 [copy,41,flip.1] name_PIN1!=constr_CONST_1. % 2.29/2.46 ** KEPT (pick-wt=3): 44 [copy,43,flip.1] name_PIN2!=constr_CONST_1. % 2.29/2.46 ** KEPT (pick-wt=3): 46 [copy,45,flip.1] name_S!=constr_CONST_1. % 2.29/2.46 ** KEPT (pick-wt=3): 48 [copy,47,flip.1] name_c!=constr_CONST_1. % 2.29/2.46 ** KEPT (pick-wt=3): 50 [copy,49,flip.1] name_r1!=constr_CONST_1. % 2.29/2.46 ** KEPT (pick-wt=3): 52 [copy,51,flip.1] name_r1_from_1st_round!=constr_CONST_1. % 2.29/2.46 ** KEPT (pick-wt=3): 54 [copy,53,flip.1] name_r2_from_1st_round!=constr_CONST_1. % 2.29/2.46 ** KEPT (pick-wt=3): 56 [copy,55,flip.1] constr_CONST_3!=constr_CONST_2. % 2.29/2.46 ** KEPT (pick-wt=3): 58 [copy,57,flip.1] constr_CONST_4!=constr_CONST_2. % 2.29/2.46 ** KEPT (pick-wt=3): 60 [copy,59,flip.1] constr_QUERY_REQ!=constr_CONST_2. % 2.29/2.46 ** KEPT (pick-wt=3): 62 [copy,61,flip.1] constr_ZERO!=constr_CONST_2. % 2.29/2.46 ** KEPT (pick-wt=3): 64 [copy,63,flip.1] name_EPC!=constr_CONST_2. % 2.29/2.46 ** KEPT (pick-wt=3): 66 [copy,65,flip.1] name_PIN1!=constr_CONST_2. % 2.29/2.46 ** KEPT (pick-wt=3): 68 [copy,67,flip.1] name_PIN2!=constr_CONST_2. % 2.29/2.46 ** KEPT (pick-wt=3): 70 [copy,69,flip.1] name_S!=constr_CONST_2. % 2.29/2.46 ** KEPT (pick-wt=3): 72 [copy,71,flip.1] name_c!=constr_CONST_2. % 2.29/2.46 ** KEPT (pick-wt=3): 74 [copy,73,flip.1] name_r1!=constr_CONST_2. % 2.29/2.46 ** KEPT (pick-wt=3): 76 [copy,75,flip.1] name_r1_from_1st_round!=constr_CONST_2. % 2.29/2.46 ** KEPT (pick-wt=3): 78 [copy,77,flip.1] name_r2_from_1st_round!=constr_CONST_2. % 2.29/2.46 ** KEPT (pick-wt=3): 80 [copy,79,flip.1] constr_CONST_4!=constr_CONST_3. % 2.29/2.46 ** KEPT (pick-wt=3): 82 [copy,81,flip.1] constr_QUERY_REQ!=constr_CONST_3. % 2.29/2.46 ** KEPT (pick-wt=3): 84 [copy,83,flip.1] constr_ZERO!=constr_CONST_3. % 2.29/2.46 ** KEPT (pick-wt=3): 86 [copy,85,flip.1] name_EPC!=constr_CONST_3. % 2.29/2.46 ** KEPT (pick-wt=3): 88 [copy,87,flip.1] name_PIN1!=constr_CONST_3. % 2.29/2.46 ** KEPT (pick-wt=3): 90 [copy,89,flip.1] name_PIN2!=constr_CONST_3. % 2.29/2.46 ** KEPT (pick-wt=3): 92 [copy,91,flip.1] name_S!=constr_CONST_3. % 2.29/2.46 ** KEPT (pick-wt=3): 94 [copy,93,flip.1] name_c!=constr_CONST_3. % 2.29/2.46 ** KEPT (pick-wt=3): 96 [copy,95,flip.1] name_r1!=constr_CONST_3. % 2.29/2.46 ** KEPT (pick-wt=3): 98 [copy,97,flip.1] name_r1_from_1st_round!=constr_CONST_3. % 2.29/2.46 ** KEPT (pick-wt=3): 100 [copy,99,flip.1] name_r2_from_1st_round!=constr_CONST_3. % 2.29/2.46 ** KEPT (pick-wt=3): 102 [copy,101,flip.1] constr_QUERY_REQ!=constr_CONST_4. % 2.29/2.46 ** KEPT (pick-wt=3): 104 [copy,103,flip.1] constr_ZERO!=constr_CONST_4. % 2.29/2.46 ** KEPT (pick-wt=3): 106 [copy,105,flip.1] name_EPC!=constr_CONST_4. % 2.29/2.46 ** KEPT (pick-wt=3): 108 [copy,107,flip.1] name_PIN1!=constr_CONST_4. % 2.29/2.46 ** KEPT (pick-wt=3): 110 [copy,109,flip.1] name_PIN2!=constr_CONST_4. % 2.29/2.46 ** KEPT (pick-wt=3): 112 [copy,111,flip.1] name_S!=constr_CONST_4. % 2.29/2.46 ** KEPT (pick-wt=3): 114 [copy,113,flip.1] name_c!=constr_CONST_4. % 2.29/2.46 ** KEPT (pick-wt=3): 116 [copy,115,flip.1] name_r1!=constr_CONST_4. % 2.29/2.46 ** KEPT (pick-wt=3): 118 [copy,117,flip.1] name_r1_from_1st_round!=constr_CONST_4. % 2.29/2.46 ** KEPT (pick-wt=3): 120 [copy,119,flip.1] name_r2_from_1st_round!=constr_CONST_4. % 2.29/2.46 ** KEPT (pick-wt=3): 122 [copy,121,flip.1] constr_ZERO!=constr_QUERY_REQ. % 2.29/2.46 ** KEPT (pick-wt=3): 124 [copy,123,flip.1] name_EPC!=constr_QUERY_REQ. % 2.29/2.46 ** KEPT (pick-wt=3): 126 [copy,125,flip.1] name_PIN1!=constr_QUERY_REQ. % 2.29/2.46 ** KEPT (pick-wt=3): 128 [copy,127,flip.1] name_PIN2!=constr_QUERY_REQ. % 2.29/2.46 ** KEPT (pick-wt=3): 130 [copy,129,flip.1] name_S!=constr_QUERY_REQ. % 2.29/2.46 ** KEPT (pick-wt=3): 132 [copy,131,flip.1] name_c!=constr_QUERY_REQ. % 2.29/2.46 ** KEPT (pick-wt=3): 134 [copy,133,flip.1] name_r1!=constr_QUERY_REQ. % 2.29/2.46 ** KEPT (pick-wt=3): 136 [copy,135,flip.1] name_r1_from_1st_round!=constr_QUERY_REQ. % 2.29/2.46 ** KEPT (pick-wt=3): 138 [copy,137,flip.1] name_r2_from_1st_round!=constr_QUERY_REQ. % 2.29/2.46 ** KEPT (pick-wt=3): 140 [copy,139,flip.1] name_EPC!=constr_ZERO. % 2.29/2.46 ** KEPT (pick-wt=3): 142 [copy,141,flip.1] name_PIN1!=constr_ZERO. % 2.29/2.46 ** KEPT (pick-wt=3): 144 [copy,143,flip.1] name_PIN2!=constr_ZERO. % 2.29/2.46 ** KEPT (pick-wt=3): 146 [copy,145,flip.1] name_S!=constr_ZERO. % 2.29/2.46 ** KEPT (pick-wt=3): 148 [copy,147,flip.1] name_c!=constr_ZERO. % 2.29/2.46 ** KEPT (pick-wt=3): 150 [copy,149,flip.1] name_r1!=constr_ZERO. % 2.29/2.46 ** KEPT (pick-wt=3): 152 [copy,151,flip.1] name_r1_from_1st_round!=constr_ZERO. % 2.29/2.46 ** KEPT (pick-wt=3): 154 [copy,153,flip.1] name_r2_from_1st_round!=constr_ZERO. % 2.29/2.46 ** KEPT (pick-wt=3): 156 [copy,155,flip.1] name_PIN1!=name_EPC. % 2.29/2.46 ** KEPT (pick-wt=3): 158 [copy,157,flip.1] name_PIN2!=name_EPC. % 2.29/2.46 ** KEPT (pick-wt=3): 160 [copy,159,flip.1] name_S!=name_EPC. % 2.29/2.46 ** KEPT (pick-wt=3): 162 [copy,161,flip.1] name_c!=name_EPC. % 2.29/2.46 ** KEPT (pick-wt=3): 164 [copy,163,flip.1] name_r1!=name_EPC. % 2.29/2.46 ** KEPT (pick-wt=3): 166 [copy,165,flip.1] name_r1_from_1st_round!=name_EPC. % 2.29/2.46 ** KEPT (pick-wt=3): 168 [copy,167,flip.1] name_r2_from_1st_round!=name_EPC. % 2.29/2.46 ** KEPT (pick-wt=3): 170 [copy,169,flip.1] name_PIN2!=name_PIN1. % 2.29/2.46 ** KEPT (pick-wt=3): 172 [copy,171,flip.1] name_S!=name_PIN1. % 2.29/2.46 ** KEPT (pick-wt=3): 174 [copy,173,flip.1] name_c!=name_PIN1. % 2.29/2.46 ** KEPT (pick-wt=3): 176 [copy,175,flip.1] name_r1!=name_PIN1. % 2.29/2.46 ** KEPT (pick-wt=3): 178 [copy,177,flip.1] name_r1_from_1st_round!=name_PIN1. % 2.29/2.46 ** KEPT (pick-wt=3): 180 [copy,179,flip.1] name_r2_from_1st_round!=name_PIN1. % 2.29/2.46 ** KEPT (pick-wt=3): 182 [copy,181,flip.1] name_S!=name_PIN2. % 2.29/2.46 ** KEPT (pick-wt=3): 184 [copy,183,flip.1] name_c!=name_PIN2. % 2.29/2.46 ** KEPT (pick-wt=3): 186 [copy,185,flip.1] name_r1!=name_PIN2. % 2.29/2.46 ** KEPT (pick-wt=3): 188 [copy,187,flip.1] name_r1_from_1st_round!=name_PIN2. % 2.29/2.46 ** KEPT (pick-wt=3): 190 [copy,189,flip.1] name_r2_from_1st_round!=name_PIN2. % 2.29/2.46 ** KEPT (pick-wt=3): 192 [copy,191,flip.1] name_c!=name_S. % 2.29/2.46 ** KEPT (pick-wt=3): 194 [copy,193,flip.1] name_r1!=name_S. % 2.29/2.46 ** KEPT (pick-wt=3): 196 [copy,195,flip.1] name_r1_from_1st_round!=name_S. % 2.29/2.46 ** KEPT (pick-wt=3): 198 [copy,197,flip.1] name_r2_from_1st_round!=name_S. % 2.29/2.46 ** KEPT (pick-wt=3): 200 [copy,199,flip.1] name_r1!=name_c. % 2.29/2.46 ** KEPT (pick-wt=3): 202 [copy,201,flip.1] name_r1_from_1st_round!=name_c. % 2.29/2.46 ** KEPT (pick-wt=3): 204 [copy,203,flip.1] name_r2_from_1st_round!=name_c. % 2.29/2.46 ** KEPT (pick-wt=3): 206 [copy,205,flip.1] name_r1_from_1st_round!=name_r1. % 2.29/2.46 ** KEPT (pick-wt=3): 208 [copy,207,flip.1] name_r2_from_1st_round!=name_r1. % 2.29/2.46 ** KEPT (pick-wt=3): 210 [copy,209,flip.1] name_r2_from_1st_round!=name_r1_from_1st_round. % 2.29/2.46 ** KEPT (pick-wt=8): 211 [] -pred_attacker(A)| -pred_attacker(B)|pred_attacker(constr_xor(A,B)). % 2.29/2.46 ** KEPT (pick-wt=8): 212 [] -pred_attacker(A)| -pred_attacker(B)|pred_attacker(constr_sub(A,B)). % 2.29/2.46 ** KEPT (pick-wt=5): 213 [] -pred_attacker(A)|pred_attacker(tuple_knowledge_from_1st_round_out_5(A)). % 2.29/2.46 ** KEPT (pick-wt=5): 214 [] -pred_attacker(tuple_knowledge_from_1st_round_out_5(A))|pred_attacker(A). % 2.29/2.46 ** KEPT (pick-wt=5): 215 [] -pred_attacker(A)|pred_attacker(tuple_knowledge_from_1st_round_out_4(A)). % 2.29/2.46 ** KEPT (pick-wt=5): 216 [] -pred_attacker(tuple_knowledge_from_1st_round_out_4(A))|pred_attacker(A). % 2.29/2.46 ** KEPT (pick-wt=5): 217 [] -pred_attacker(A)|pred_attacker(tuple_knowledge_from_1st_round_out_3(A)). % 2.29/2.46 ** KEPT (pick-wt=5): 218 [] -pred_attacker(tuple_knowledge_from_1st_round_out_3(A))|pred_attacker(A). % 2.29/2.46 ** KEPT (pick-wt=5): 219 [] -pred_attacker(A)|pred_attacker(tuple_knowledge_from_1st_round_out_2(A)). % 2.29/2.46 ** KEPT (pick-wt=5): 220 [] -pred_attacker(tuple_knowledge_from_1st_round_out_2(A))|pred_attacker(A). % 2.29/2.46 ** KEPT (pick-wt=5): 221 [] -pred_attacker(A)|pred_attacker(tuple_knowledge_from_1st_round_out_1(A)). % 2.29/2.46 ** KEPT (pick-wt=5): 222 [] -pred_attacker(tuple_knowledge_from_1st_round_out_1(A))|pred_attacker(A). % 2.29/2.46 ** KEPT (pick-wt=5): 223 [] -pred_attacker(A)|pred_attacker(constr_f(A)). % 2.29/2.46 ** KEPT (pick-wt=8): 224 [] -pred_attacker(A)| -pred_attacker(B)|pred_attacker(constr_concat(A,B)). % 2.29/2.46 ** KEPT (pick-wt=8): 225 [] -pred_attacker(A)| -pred_attacker(B)|pred_attacker(constr_add(A,B)). % 2.29/2.46 ** KEPT (pick-wt=5): 226 [] -pred_attacker(A)|pred_attacker(tuple_T_out_6(A)). % 2.29/2.46 ** KEPT (pick-wt=5): 227 [] -pred_attacker(tuple_T_out_6(A))|pred_attacker(A). % 2.29/2.46 ** KEPT (pick-wt=5): 228 [] -pred_attacker(A)|pred_attacker(tuple_T_out_4(A)). % 2.29/2.46 ** KEPT (pick-wt=5): 229 [] -pred_attacker(tuple_T_out_4(A))|pred_attacker(A). % 2.29/2.46 ** KEPT (pick-wt=5): 230 [] -pred_attacker(A)|pred_attacker(tuple_T_out_2(A)). % 2.29/2.46 ** KEPT (pick-wt=5): 231 [] -pred_attacker(tuple_T_out_2(A))|pred_attacker(A). % 2.29/2.46 ** KEPT (pick-wt=5): 232 [] -pred_attacker(A)|pred_attacker(tuple_T_in_5(A)). % 2.29/2.46 ** KEPT (pick-wt=5): 233 [] -pred_attacker(tuple_T_in_5(A))|pred_attacker(A). % 2.29/2.46 ** KEPT (pick-wt=8): 234 [] -pred_attacker(A)| -pred_attacker(B)|pred_attacker(tuple_T_in_3(A,B)). % 2.29/2.46 ** KEPT (pick-wt=6): 235 [] -pred_attacker(tuple_T_in_3(A,B))|pred_attacker(A). % 2.29/2.46 ** KEPT (pick-wt=6): 236 [] -pred_attacker(tuple_T_in_3(A,B))|pred_attacker(B). % 2.29/2.46 ** KEPT (pick-wt=5): 237 [] -pred_attacker(A)|pred_attacker(tuple_T_in_1(A)). % 2.29/2.46 ** KEPT (pick-wt=5): 238 [] -pred_attacker(tuple_T_in_1(A))|pred_attacker(A). % 2.29/2.46 ** KEPT (pick-wt=5): 239 [] -pred_attacker(A)|pred_attacker(constr_ACK(A)). % 2.29/2.46 ** KEPT (pick-wt=7): 240 [] -pred_mess(A,B)| -pred_attacker(A)|pred_attacker(B). % 2.29/2.46 ** KEPT (pick-wt=7): 241 [] -pred_attacker(A)| -pred_attacker(B)|pred_mess(A,B). % 2.29/2.46 ** KEPT (pick-wt=8): 242 [] -pred_attacker(tuple_T_in_1(constr_QUERY_REQ))|pred_attacker(tuple_T_out_2(constr_xor(name_r1,name_PIN1))). % 2.29/2.46 ** KEPT (pick-wt=32): 243 [] -pred_attacker(tuple_T_in_3(constr_ACK(constr_xor(name_r1,name_PIN1)),A))| -pred_attacker(tuple_T_in_1(constr_QUERY_REQ))|pred_attacker(tuple_T_out_4(constr_xor(constr_add(constr_concat(constr_ZERO,constr_concat(name_r1,constr_concat(constr_xor(constr_xor(A,name_PIN2),name_r1),constr_f(constr_xor(constr_xor(A,name_PIN2),name_r1))))),name_S),name_EPC))). % 2.29/2.46 ** KEPT (pick-wt=2): 244 [] -pred_attacker(name_objective). % 2.29/2.46 % 2.29/2.46 ------------> process sos: % 2.29/2.46 ** KEPT (pick-wt=3): 245 [] A=A. % 2.29/2.46 ** KEPT (pick-wt=5): 246 [] constr_add(constr_ZERO,constr_ZERO)=constr_ZERO. % 2.29/2.46 ---> New Demodulator: 247 [new_demod,246] constr_add(constr_ZERO,constr_ZERO)=constr_ZERO. % 2.29/2.46 ** KEPT (pick-wt=5): 248 [] constr_sub(A,constr_ZERO)=A. % 2.29/2.46 ---> New Demodulator: 249 [new_demod,248] constr_sub(A,constr_ZERO)=A. % 2.29/2.46 ** KEPT (pick-wt=5): 250 [] constr_add(A,constr_ZERO)=A. % 2.29/2.46 ---> New Demodulator: 251 [new_demod,250] constr_add(A,constr_ZERO)=A. % 2.29/2.46 ** KEPT (pick-wt=5): 252 [] constr_sub(A,A)=constr_ZERO. % 2.29/2.46 ---> New Demodulator: 253 [new_demod,252] constr_sub(A,A)=constr_ZERO. % 2.29/2.46 ** KEPT (pick-wt=7): 254 [] constr_sub(constr_add(A,B),B)=A. % 2.29/2.46 ---> New Demodulator: 255 [new_demod,254] constr_sub(constr_add(A,B),B)=A. % 2.29/2.46 ** KEPT (pick-wt=11): 257 [copy,256,flip.1] constr_add(constr_add(A,B),C)=constr_add(A,constr_add(B,C)). % 2.29/2.46 ---> New Demodulator: 258 [new_demod,257] constr_add(constr_add(A,B),C)=constr_add(A,constr_add(B,C)). % 2.29/2.46 ** KEPT (pick-wt=7): 259 [] constr_add(A,B)=constr_add(B,A). % 2.29/2.46 ** KEPT (pick-wt=11): 260 [] constr_concat(constr_concat(A,B),C)=constr_concat(A,constr_concat(B,C)). % 2.29/2.46 ---> New Demodulator: 261 [new_demod,260] constr_concat(constr_concat(A,B),C)=constr_concat(A,constr_concat(B,C)). % 2.29/2.46 ** KEPT (pick-wt=5): 262 [] constr_xor(A,A)=constr_ZERO. % 2.29/2.46 ---> New Demodulator: 263 [new_demod,262] constr_xor(A,A)=constr_ZERO. % 2.29/2.46 ** KEPT (pick-wt=5): 264 [] constr_xor(A,constr_ZERO)=A. % 2.29/2.46 ---> New Demodulator: 265 [new_demod,264] constr_xor(A,constr_ZERO)=A. % 2.29/2.46 ** KEPT (pick-wt=7): 266 [] constr_xor(A,B)=constr_xor(B,A). % 2.29/2.46 ** KEPT (pick-wt=11): 268 [copy,267,flip.1] constr_xor(constr_xor(A,B),C)=constr_xor(A,constr_xor(B,C)). % 2.29/2.46 ---> New Demodulator: 269 [new_demod,268] constr_xor(constr_xor(A,B),C)=constr_xor(A,constr_xor(B,C)). % 2.29/2.46 ** KEPT (pick-wt=2): 270 [] pred_attacker(tuple_true). % 2.29/2.46 ** KEPT (pick-wt=2): 271 [] pred_attacker(tuple_false). % 2.29/2.46 ** KEPT (pick-wt=2): 272 [] pred_attacker(constr_ZERO). % 2.29/2.46 ** KEPT (pick-wt=2): 273 [] pred_attacker(constr_QUERY_REQ). % 2.29/2.46 ** KEPT (pick-wt=2): 274 [] pred_attacker(constr_CONST_4). % 2.29/2.46 ** KEPT (pick-wt=2): 275 [] pred_attacker(constr_CONST_3). % 2.29/2.46 ** KEPT (pick-wt=2): 276 [] pred_attacker(constr_CONST_2). % 2.29/2.46 ** KEPT (pick-wt=2): 277 [] pred_attacker(constr_CONST_1). % 2.29/2.46 ** KEPT (pick-wt=2): 278 [] pred_attacker(constr_CONST_0x30). % 2.29/2.46 ** KEPT (pick-wt=2): 279 [] pred_attacker(name_c). % 2.29/2.46 ** KEPT (pick-wt=3): 280 [] pred_e_qual(A,A). % 2.29/2.46 ** KEPT (pick-wt=3): 281 [] pred_attacker(name_new0x2Dname(A)). % 2.29/2.46 ** KEPT (pick-wt=3): 282 [] pred_attacker(tuple_knowledge_from_1st_round_out_1(constr_QUERY_REQ)). % 2.29/2.46 ** KEPT (pick-wt=5): 283 [] pred_attacker(tuple_knowledge_from_1st_round_out_2(constr_xor(name_r1_from_1st_round,name_PIN1))). % 23.21/23.38 ** KEPT (pick-wt=6): 284 [] pred_attacker(tuple_knowledge_from_1st_round_out_3(constr_ACK(constr_xor(name_r1_from_1st_round,name_PIN1)))). % 23.21/23.38 ** KEPT (pick-wt=22): 286 [copy,285,demod,269,269] pred_attacker(tuple_knowledge_from_1st_round_out_4(constr_xor(constr_add(constr_concat(constr_ZERO,constr_concat(name_r1_from_1st_round,constr_concat(constr_xor(name_r2_from_1st_round,constr_xor(name_PIN2,name_r1_from_1st_round)),constr_f(constr_xor(name_r2_from_1st_round,constr_xor(name_PIN2,name_r1_from_1st_round)))))),name_S),name_EPC))). % 23.21/23.38 ** KEPT (pick-wt=10): 287 [] pred_attacker(tuple_knowledge_from_1st_round_out_5(constr_xor(name_PIN1,constr_f(constr_xor(name_r2_from_1st_round,constr_xor(name_PIN2,name_r1_from_1st_round)))))). % 23.21/23.38 Following clause subsumed by 245 during input processing: 0 [copy,245,flip.1] A=A. % 23.21/23.38 >>>> Starting back demodulation with 247. % 23.21/23.38 >>>> Starting back demodulation with 249. % 23.21/23.38 >>>> Starting back demodulation with 251. % 23.21/23.38 >> back demodulating 246 with 251. % 23.21/23.38 >>>> Starting back demodulation with 253. % 23.21/23.38 >>>> Starting back demodulation with 255. % 23.21/23.38 >>>> Starting back demodulation with 258. % 23.21/23.38 Following clause subsumed by 259 during input processing: 0 [copy,259,flip.1] constr_add(A,B)=constr_add(B,A). % 23.21/23.38 >>>> Starting back demodulation with 261. % 23.21/23.38 >>>> Starting back demodulation with 263. % 23.21/23.38 >>>> Starting back demodulation with 265. % 23.21/23.38 Following clause subsumed by 266 during input processing: 0 [copy,266,flip.1] constr_xor(A,B)=constr_xor(B,A). % 23.21/23.38 >>>> Starting back demodulation with 269. % 23.21/23.38 >> back demodulating 243 with 269. % 23.21/23.38 % 23.21/23.38 ======= end of input processing ======= % 23.21/23.38 % 23.21/23.38 =========== start of search =========== % 23.21/23.38 % 23.21/23.38 % 23.21/23.38 Resetting weight limit to 3. % 23.21/23.38 % 23.21/23.38 % 23.21/23.38 Resetting weight limit to 3. % 23.21/23.38 % 23.21/23.38 sos_size=2080 % 23.21/23.38 % 23.21/23.38 Search stopped because sos empty. % 23.21/23.38 % 23.21/23.38 % 23.21/23.38 Search stopped because sos empty. % 23.21/23.38 % 23.21/23.38 ============ end of search ============ % 23.21/23.38 % 23.21/23.38 -------------- statistics ------------- % 23.21/23.38 clauses given 2107 % 23.21/23.38 clauses generated 19265403 % 23.21/23.38 clauses kept 2247 % 23.21/23.38 clauses forward subsumed 8874 % 23.21/23.38 clauses back subsumed 0 % 23.21/23.38 Kbytes malloced 6835 % 23.21/23.38 % 23.21/23.38 ----------- times (seconds) ----------- % 23.21/23.38 user CPU time 20.92 (0 hr, 0 min, 20 sec) % 23.21/23.38 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 23.21/23.38 wall-clock time 23 (0 hr, 0 min, 23 sec) % 23.21/23.38 % 23.21/23.38 Process 31578 finished Wed Jul 27 02:50:18 2022 % 23.21/23.38 Otter interrupted % 23.21/23.38 PROOF NOT FOUND %------------------------------------------------------------------------------