%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWW961+1 : TPTP v8.2.0. Released v7.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n009.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 18:10:38 EDT 2024 % Result : Theorem 14.44s 14.54s % Output : CNFRefutation 14.44s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : SWW961+1 : TPTP v8.2.0. Released v7.4.0. % 0.07/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n009.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Wed Jun 19 05:09:39 EDT 2024 % 0.12/0.34 % CPUTime : % 0.20/0.58 start to proof:theBenchmark % 14.44/14.52 %------------------------------------------- % 14.44/14.52 % File :CSE---1.7 % 14.44/14.52 % Problem :theBenchmark % 14.44/14.52 % Transform :cnf % 14.44/14.52 % Format :tptp:raw % 14.44/14.52 % Command :java -jar mcs_scs.jar %d %s % 14.44/14.52 % 14.44/14.52 % Result :Theorem 13.880000s % 14.44/14.52 % Output :CNFRefutation 13.880000s % 14.44/14.52 %------------------------------------------- % 14.44/14.52 %-------------------------------------------------------------------------- % 14.44/14.52 % File : SWW961+1 : TPTP v8.2.0. Released v7.4.0. % 14.44/14.52 % Domain : Software Verification % 14.44/14.52 % Problem : Attack on a variant of Needham-Schroeder-Lowe Public Key Protocol % 14.44/14.52 % Version : [LT19] axioms : Especial. % 14.44/14.52 % English : Attack on a modified version of Needham-Schroeder-Lowe Public Key % 14.44/14.52 % Protocol. This variant introduces a flaw by using an associative % 14.44/14.52 % pairing function. Attack demonstrates violation of weak agreement % 14.44/14.52 % property of A to B. % 14.44/14.52 % 14.44/14.52 % Refs : [BO97] Bull & Otway (1997), The Authentication Protocol % 14.44/14.52 % : [RS98] Ryan & Schneider (1998), An Attack on a Recursive Auth % 14.44/14.52 % : [LT19] Li & Tiu (2019), Combining ProVerif and Automated Theo % 14.44/14.52 % : [Li20] Li (2020), Email to Geoff Sutcliffe % 14.44/14.52 % Source : [Li20] % 14.44/14.52 % Names : NSLPK-modified-agree-A-to-B.p [LT20] % 14.44/14.52 % 14.44/14.52 % Status : Theorem % 14.44/14.52 % Rating : 0.31 v8.2.0, 0.25 v7.5.0, 0.28 v7.4.0 % 14.44/14.52 % Syntax : Number of formulae : 177 ( 111 unt; 0 def) % 14.44/14.52 % Number of atoms : 273 ( 91 equ) % 14.44/14.52 % Maximal formula atoms : 7 ( 1 avg) % 14.44/14.52 % Number of connectives : 176 ( 80 ~; 0 |; 30 &) % 14.44/14.52 % ( 0 <=>; 66 =>; 0 <=; 0 <~>) % 14.44/14.52 % Maximal formula depth : 11 ( 3 avg) % 14.44/14.52 % Maximal term depth : 6 ( 1 avg) % 14.44/14.52 % Number of predicates : 6 ( 5 usr; 0 prp; 1-2 aty) % 14.44/14.52 % Number of functors : 52 ( 52 usr; 15 con; 0-2 aty) % 14.44/14.52 % Number of variables : 130 ( 130 !; 0 ?) % 14.44/14.52 % SPC : FOF_THM_RFO_SEQ % 14.44/14.52 % 14.44/14.52 % Comments : Generated by a modified version of ProVerif used in the % 14.44/14.52 % ProVerif-ATP project [LT19]. % 14.44/14.52 %-------------------------------------------------------------------------- % 14.44/14.52 fof(ax0,axiom, % 14.44/14.52 constr_CONST_0x30 != constr_CONST_1 ). % 14.44/14.52 % 14.44/14.52 fof(ax1,axiom, % 14.44/14.52 constr_CONST_0x30 != constr_CONST_2 ). % 14.44/14.52 % 14.44/14.52 fof(ax2,axiom, % 14.44/14.52 constr_CONST_0x30 != constr_CONST_3 ). % 14.44/14.52 % 14.44/14.52 fof(ax3,axiom, % 14.44/14.52 constr_CONST_0x30 != constr_CONST_4 ). % 14.44/14.52 % 14.44/14.52 fof(ax4,axiom, % 14.44/14.52 constr_CONST_0x30 != name_A ). % 14.44/14.52 % 14.44/14.52 fof(ax5,axiom, % 14.44/14.52 constr_CONST_0x30 != name_B ). % 14.44/14.52 % 14.44/14.52 fof(ax6,axiom, % 14.44/14.52 constr_CONST_0x30 != name_I ). % 14.44/14.52 % 14.44/14.52 fof(ax7,axiom, % 14.44/14.52 constr_CONST_0x30 != name_c ). % 14.44/14.52 % 14.44/14.52 fof(ax8,axiom, % 14.44/14.52 constr_CONST_0x30 != name_objective ). % 14.44/14.52 % 14.44/14.52 fof(ax9,axiom, % 14.44/14.52 constr_CONST_0x30 != name_skA ). % 14.44/14.52 % 14.44/14.52 fof(ax10,axiom, % 14.44/14.52 constr_CONST_0x30 != name_skB ). % 14.44/14.52 % 14.44/14.52 fof(ax11,axiom, % 14.44/14.52 constr_CONST_0x30 != name_skS ). % 14.44/14.52 % 14.44/14.52 fof(ax12,axiom, % 14.44/14.52 constr_CONST_1 != constr_CONST_2 ). % 14.44/14.52 % 14.44/14.52 fof(ax13,axiom, % 14.44/14.52 constr_CONST_1 != constr_CONST_3 ). % 14.44/14.52 % 14.44/14.52 fof(ax14,axiom, % 14.44/14.52 constr_CONST_1 != constr_CONST_4 ). % 14.44/14.52 % 14.44/14.52 fof(ax15,axiom, % 14.44/14.52 constr_CONST_1 != name_A ). % 14.44/14.52 % 14.44/14.52 fof(ax16,axiom, % 14.44/14.52 constr_CONST_1 != name_B ). % 14.44/14.52 % 14.44/14.52 fof(ax17,axiom, % 14.44/14.52 constr_CONST_1 != name_I ). % 14.44/14.52 % 14.44/14.52 fof(ax18,axiom, % 14.44/14.52 constr_CONST_1 != name_c ). % 14.44/14.52 % 14.44/14.52 fof(ax19,axiom, % 14.44/14.52 constr_CONST_1 != name_objective ). % 14.44/14.52 % 14.44/14.52 fof(ax20,axiom, % 14.44/14.53 constr_CONST_1 != name_skA ). % 14.44/14.53 % 14.44/14.53 fof(ax21,axiom, % 14.44/14.53 constr_CONST_1 != name_skB ). % 14.44/14.53 % 14.44/14.53 fof(ax22,axiom, % 14.44/14.53 constr_CONST_1 != name_skS ). % 14.44/14.53 % 14.44/14.53 fof(ax23,axiom, % 14.44/14.53 constr_CONST_2 != constr_CONST_3 ). % 14.44/14.53 % 14.44/14.53 fof(ax24,axiom, % 14.44/14.53 constr_CONST_2 != constr_CONST_4 ). % 14.44/14.53 % 14.44/14.53 fof(ax25,axiom, % 14.44/14.53 constr_CONST_2 != name_A ). % 14.44/14.53 % 14.44/14.53 fof(ax26,axiom, % 14.44/14.53 constr_CONST_2 != name_B ). % 14.44/14.53 % 14.44/14.53 fof(ax27,axiom, % 14.44/14.53 constr_CONST_2 != name_I ). % 14.44/14.53 % 14.44/14.53 fof(ax28,axiom, % 14.44/14.53 constr_CONST_2 != name_c ). % 14.44/14.53 % 14.44/14.53 fof(ax29,axiom, % 14.44/14.53 constr_CONST_2 != name_objective ). % 14.44/14.53 % 14.44/14.53 fof(ax30,axiom, % 14.44/14.53 constr_CONST_2 != name_skA ). % 14.44/14.53 % 14.44/14.53 fof(ax31,axiom, % 14.44/14.53 constr_CONST_2 != name_skB ). % 14.44/14.53 % 14.44/14.53 fof(ax32,axiom, % 14.44/14.53 constr_CONST_2 != name_skS ). % 14.44/14.53 % 14.44/14.53 fof(ax33,axiom, % 14.44/14.53 constr_CONST_3 != constr_CONST_4 ). % 14.44/14.53 % 14.44/14.53 fof(ax34,axiom, % 14.44/14.53 constr_CONST_3 != name_A ). % 14.44/14.53 % 14.44/14.53 fof(ax35,axiom, % 14.44/14.53 constr_CONST_3 != name_B ). % 14.44/14.53 % 14.44/14.53 fof(ax36,axiom, % 14.44/14.53 constr_CONST_3 != name_I ). % 14.44/14.53 % 14.44/14.53 fof(ax37,axiom, % 14.44/14.53 constr_CONST_3 != name_c ). % 14.44/14.53 % 14.44/14.53 fof(ax38,axiom, % 14.44/14.53 constr_CONST_3 != name_objective ). % 14.44/14.53 % 14.44/14.53 fof(ax39,axiom, % 14.44/14.53 constr_CONST_3 != name_skA ). % 14.44/14.53 % 14.44/14.53 fof(ax40,axiom, % 14.44/14.53 constr_CONST_3 != name_skB ). % 14.44/14.53 % 14.44/14.53 fof(ax41,axiom, % 14.44/14.53 constr_CONST_3 != name_skS ). % 14.44/14.53 % 14.44/14.53 fof(ax42,axiom, % 14.44/14.53 constr_CONST_4 != name_A ). % 14.44/14.53 % 14.44/14.53 fof(ax43,axiom, % 14.44/14.53 constr_CONST_4 != name_B ). % 14.44/14.53 % 14.44/14.53 fof(ax44,axiom, % 14.44/14.53 constr_CONST_4 != name_I ). % 14.44/14.53 % 14.44/14.53 fof(ax45,axiom, % 14.44/14.53 constr_CONST_4 != name_c ). % 14.44/14.53 % 14.44/14.53 fof(ax46,axiom, % 14.44/14.53 constr_CONST_4 != name_objective ). % 14.44/14.53 % 14.44/14.53 fof(ax47,axiom, % 14.44/14.53 constr_CONST_4 != name_skA ). % 14.44/14.53 % 14.44/14.53 fof(ax48,axiom, % 14.44/14.53 constr_CONST_4 != name_skB ). % 14.44/14.53 % 14.44/14.53 fof(ax49,axiom, % 14.44/14.53 constr_CONST_4 != name_skS ). % 14.44/14.53 % 14.44/14.53 fof(ax50,axiom, % 14.44/14.53 name_A != name_B ). % 14.44/14.53 % 14.44/14.53 fof(ax51,axiom, % 14.44/14.53 name_A != name_I ). % 14.44/14.53 % 14.44/14.53 fof(ax52,axiom, % 14.44/14.53 name_A != name_c ). % 14.44/14.53 % 14.44/14.53 fof(ax53,axiom, % 14.44/14.53 name_A != name_objective ). % 14.44/14.53 % 14.44/14.53 fof(ax54,axiom, % 14.44/14.53 name_A != name_skA ). % 14.44/14.53 % 14.44/14.53 fof(ax55,axiom, % 14.44/14.53 name_A != name_skB ). % 14.44/14.53 % 14.44/14.53 fof(ax56,axiom, % 14.44/14.53 name_A != name_skS ). % 14.44/14.53 % 14.44/14.53 fof(ax57,axiom, % 14.44/14.53 name_B != name_I ). % 14.44/14.53 % 14.44/14.53 fof(ax58,axiom, % 14.44/14.53 name_B != name_c ). % 14.44/14.53 % 14.44/14.53 fof(ax59,axiom, % 14.44/14.53 name_B != name_objective ). % 14.44/14.53 % 14.44/14.53 fof(ax60,axiom, % 14.44/14.53 name_B != name_skA ). % 14.44/14.53 % 14.44/14.53 fof(ax61,axiom, % 14.44/14.53 name_B != name_skB ). % 14.44/14.53 % 14.44/14.53 fof(ax62,axiom, % 14.44/14.53 name_B != name_skS ). % 14.44/14.53 % 14.44/14.53 fof(ax63,axiom, % 14.44/14.53 name_I != name_c ). % 14.44/14.53 % 14.44/14.53 fof(ax64,axiom, % 14.44/14.53 name_I != name_objective ). % 14.44/14.53 % 14.44/14.53 fof(ax65,axiom, % 14.44/14.53 name_I != name_skA ). % 14.44/14.53 % 14.44/14.53 fof(ax66,axiom, % 14.44/14.53 name_I != name_skB ). % 14.44/14.53 % 14.44/14.53 fof(ax67,axiom, % 14.44/14.53 name_I != name_skS ). % 14.44/14.53 % 14.44/14.53 fof(ax68,axiom, % 14.44/14.53 name_c != name_objective ). % 14.44/14.53 % 14.44/14.53 fof(ax69,axiom, % 14.44/14.53 name_c != name_skA ). % 14.44/14.53 % 14.44/14.53 fof(ax70,axiom, % 14.44/14.53 name_c != name_skB ). % 14.44/14.53 % 14.44/14.53 fof(ax71,axiom, % 14.44/14.53 name_c != name_skS ). % 14.44/14.53 % 14.44/14.53 fof(ax72,axiom, % 14.44/14.53 name_objective != name_skA ). % 14.44/14.53 % 14.44/14.53 fof(ax73,axiom, % 14.44/14.53 name_objective != name_skB ). % 14.44/14.53 % 14.44/14.53 fof(ax74,axiom, % 14.44/14.53 name_objective != name_skS ). % 14.44/14.53 % 14.44/14.53 fof(ax75,axiom, % 14.44/14.53 name_skA != name_skB ). % 14.44/14.53 % 14.44/14.53 fof(ax76,axiom, % 14.44/14.53 name_skA != name_skS ). % 14.44/14.53 % 14.44/14.53 fof(ax77,axiom, % 14.44/14.53 name_skB != name_skS ). % 14.44/14.53 % 14.44/14.53 fof(ax78,axiom, % 14.44/14.53 ! [VAR_K_24,VAR_M_23] : constr_adec(constr_aenc(VAR_M_23,constr_pkey(VAR_K_24)),VAR_K_24) = VAR_M_23 ). % 14.44/14.53 % 14.44/14.53 fof(ax79,axiom, % 14.44/14.53 ! [VAR_K_22,VAR_M_21] : constr_dec(constr_enc(VAR_M_21,VAR_K_22),VAR_K_22) = VAR_M_21 ). % 14.44/14.53 % 14.44/14.53 fof(ax80,axiom, % 14.44/14.53 ! [VAR_K_20X30,VAR_M_19] : constr_getmess(constr_sign(VAR_M_19,VAR_K_20X30)) = VAR_M_19 ). % 14.44/14.53 % 14.44/14.53 fof(ax81,axiom, % 14.44/14.53 ! [VAR_K_0X30,VAR_M_0X30] : constr_checksign(constr_sign(VAR_M_0X30,VAR_K_0X30),constr_pkey(VAR_K_0X30)) = VAR_M_0X30 ). % 14.44/14.53 % 14.44/14.53 fof(ax82,axiom, % 14.44/14.53 ! [VAR_X_17,VAR_Y_18,VAR_Z_0X30] : tuple_assoc_pair(VAR_X_17,tuple_assoc_pair(VAR_Y_18,VAR_Z_0X30)) = tuple_assoc_pair(tuple_assoc_pair(VAR_X_17,VAR_Y_18),VAR_Z_0X30) ). % 14.44/14.53 % 14.44/14.53 fof(ax83,axiom, % 14.44/14.53 ! [VAR_X0X30_15,VAR_X1_16] : constr_assoc_pair_2_get_1_bitstring(tuple_assoc_pair(VAR_X0X30_15,VAR_X1_16)) = VAR_X1_16 ). % 14.44/14.53 % 14.44/14.53 fof(ax84,axiom, % 14.44/14.53 ! [VAR_X0X30_13,VAR_X1_14] : constr_assoc_pair_2_get_0x30_bitstring(tuple_assoc_pair(VAR_X0X30_13,VAR_X1_14)) = VAR_X0X30_13 ). % 14.44/14.53 % 14.44/14.53 fof(ax85,axiom, % 14.44/14.53 ! [VAR_X0X30_11,VAR_X1_12] : constr_assoc_pair_2_get_1(tuple_assoc_pair(VAR_X0X30_11,VAR_X1_12)) = VAR_X1_12 ). % 14.44/14.53 % 14.44/14.53 fof(ax86,axiom, % 14.44/14.53 ! [VAR_X0X30_9,VAR_X1_10X30] : constr_assoc_pair_2_get_0x30(tuple_assoc_pair(VAR_X0X30_9,VAR_X1_10X30)) = VAR_X0X30_9 ). % 14.44/14.53 % 14.44/14.53 fof(ax87,axiom, % 14.44/14.53 ! [VAR_X0X30_7,VAR_X1_8] : constr_tuple_2_get_1_bitstring(tuple_2(VAR_X0X30_7,VAR_X1_8)) = VAR_X1_8 ). % 14.44/14.53 % 14.44/14.53 fof(ax88,axiom, % 14.44/14.53 ! [VAR_X0X30_0X30,VAR_X1_0X30] : constr_tuple_2_get_0x30(tuple_2(VAR_X0X30_0X30,VAR_X1_0X30)) = VAR_X0X30_0X30 ). % 14.44/14.53 % 14.44/14.53 fof(ax89,axiom, % 14.44/14.53 ! [VAR_X_41,VAR_Y_42] : pred_eq_bitstring_bitstring(VAR_X_41,VAR_Y_42) ). % 14.44/14.53 % 14.44/14.53 fof(ax90,axiom, % 14.44/14.53 ! [VAR_V_48] : % 14.44/14.53 ( pred_attacker(VAR_V_48) % 14.44/14.53 => pred_attacker(constr_tuple_2_get_1_bitstring(VAR_V_48)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax91,axiom, % 14.44/14.53 ! [VAR_V_50X30] : % 14.44/14.53 ( pred_attacker(VAR_V_50X30) % 14.44/14.53 => pred_attacker(constr_tuple_2_get_0x30(VAR_V_50X30)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax92,axiom, % 14.44/14.53 pred_attacker(tuple_true) ). % 14.44/14.53 % 14.44/14.53 fof(ax93,axiom, % 14.44/14.53 ! [VAR_V_53,VAR_V_54] : % 14.44/14.53 ( ( pred_attacker(VAR_V_53) % 14.44/14.53 & pred_attacker(VAR_V_54) ) % 14.44/14.53 => pred_attacker(constr_sign(VAR_V_53,VAR_V_54)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax94,axiom, % 14.44/14.53 ! [VAR_V_56] : % 14.44/14.53 ( pred_attacker(VAR_V_56) % 14.44/14.53 => pred_attacker(constr_pkey(VAR_V_56)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax95,axiom, % 14.44/14.53 ! [VAR_V_58] : % 14.44/14.53 ( pred_attacker(VAR_V_58) % 14.44/14.53 => pred_attacker(tuple_out_3(VAR_V_58)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax96,axiom, % 14.44/14.53 ! [VAR_V_61] : % 14.44/14.53 ( pred_attacker(tuple_out_3(VAR_V_61)) % 14.44/14.53 => pred_attacker(VAR_V_61) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax97,axiom, % 14.44/14.53 ! [VAR_V_64] : % 14.44/14.53 ( pred_attacker(VAR_V_64) % 14.44/14.53 => pred_attacker(tuple_out_2(VAR_V_64)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax98,axiom, % 14.44/14.53 ! [VAR_V_67] : % 14.44/14.53 ( pred_attacker(tuple_out_2(VAR_V_67)) % 14.44/14.53 => pred_attacker(VAR_V_67) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax99,axiom, % 14.44/14.53 ! [VAR_V_70X30] : % 14.44/14.53 ( pred_attacker(VAR_V_70X30) % 14.44/14.53 => pred_attacker(tuple_out_1(VAR_V_70X30)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax100,axiom, % 14.44/14.53 ! [VAR_V_73] : % 14.44/14.53 ( pred_attacker(tuple_out_1(VAR_V_73)) % 14.44/14.53 => pred_attacker(VAR_V_73) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax101,axiom, % 14.44/14.53 ! [VAR_V_77] : % 14.44/14.53 ( pred_attacker(VAR_V_77) % 14.44/14.53 => pred_attacker(tuple_key_retrieval_server_out_2(VAR_V_77)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax102,axiom, % 14.44/14.53 ! [VAR_V_80X30] : % 14.44/14.53 ( pred_attacker(tuple_key_retrieval_server_out_2(VAR_V_80X30)) % 14.44/14.53 => pred_attacker(VAR_V_80X30) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax103,axiom, % 14.44/14.53 ! [VAR_V_84,VAR_V_85] : % 14.44/14.53 ( ( pred_attacker(VAR_V_84) % 14.44/14.53 & pred_attacker(VAR_V_85) ) % 14.44/14.53 => pred_attacker(tuple_key_retrieval_server_in_1(VAR_V_84,VAR_V_85)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax104,axiom, % 14.44/14.53 ! [VAR_V_92,VAR_V_93] : % 14.44/14.53 ( pred_attacker(tuple_key_retrieval_server_in_1(VAR_V_92,VAR_V_93)) % 14.44/14.53 => pred_attacker(VAR_V_92) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax105,axiom, % 14.44/14.53 ! [VAR_V_95,VAR_V_96] : % 14.44/14.53 ( pred_attacker(tuple_key_retrieval_server_in_1(VAR_V_95,VAR_V_96)) % 14.44/14.53 => pred_attacker(VAR_V_96) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax106,axiom, % 14.44/14.53 ! [VAR_V_10X300X30,VAR_V_10X301] : % 14.44/14.53 ( ( pred_attacker(VAR_V_10X300X30) % 14.44/14.53 & pred_attacker(VAR_V_10X301) ) % 14.44/14.53 => pred_attacker(tuple_key_register_server_in_1(VAR_V_10X300X30,VAR_V_10X301)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax107,axiom, % 14.44/14.53 ! [VAR_V_10X308,VAR_V_10X309] : % 14.44/14.53 ( pred_attacker(tuple_key_register_server_in_1(VAR_V_10X308,VAR_V_10X309)) % 14.44/14.53 => pred_attacker(VAR_V_10X308) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax108,axiom, % 14.44/14.53 ! [VAR_V_111,VAR_V_112] : % 14.44/14.53 ( pred_attacker(tuple_key_register_server_in_1(VAR_V_111,VAR_V_112)) % 14.44/14.53 => pred_attacker(VAR_V_112) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax109,axiom, % 14.44/14.53 ! [VAR_V_115] : % 14.44/14.53 ( pred_attacker(VAR_V_115) % 14.44/14.53 => pred_attacker(constr_getmess(VAR_V_115)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax110,axiom, % 14.44/14.53 pred_attacker(tuple_false) ). % 14.44/14.53 % 14.44/14.53 fof(ax111,axiom, % 14.44/14.53 ! [VAR_V_118,VAR_V_119] : % 14.44/14.53 ( ( pred_attacker(VAR_V_118) % 14.44/14.53 & pred_attacker(VAR_V_119) ) % 14.44/14.53 => pred_attacker(constr_enc(VAR_V_118,VAR_V_119)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax112,axiom, % 14.44/14.53 ! [VAR_V_122,VAR_V_123] : % 14.44/14.53 ( ( pred_attacker(VAR_V_122) % 14.44/14.53 & pred_attacker(VAR_V_123) ) % 14.44/14.53 => pred_attacker(constr_dec(VAR_V_122,VAR_V_123)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax113,axiom, % 14.44/14.53 ! [VAR_V_125] : % 14.44/14.53 ( pred_attacker(VAR_V_125) % 14.44/14.53 => pred_attacker(tuple_client_B_out_6(VAR_V_125)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax114,axiom, % 14.44/14.53 ! [VAR_V_128] : % 14.44/14.53 ( pred_attacker(tuple_client_B_out_6(VAR_V_128)) % 14.44/14.53 => pred_attacker(VAR_V_128) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax115,axiom, % 14.44/14.53 ! [VAR_V_131] : % 14.44/14.53 ( pred_attacker(VAR_V_131) % 14.44/14.53 => pred_attacker(tuple_client_B_out_4(VAR_V_131)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax116,axiom, % 14.44/14.53 ! [VAR_V_134] : % 14.44/14.53 ( pred_attacker(tuple_client_B_out_4(VAR_V_134)) % 14.44/14.53 => pred_attacker(VAR_V_134) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax117,axiom, % 14.44/14.53 ! [VAR_V_138,VAR_V_139] : % 14.44/14.53 ( ( pred_attacker(VAR_V_138) % 14.44/14.53 & pred_attacker(VAR_V_139) ) % 14.44/14.53 => pred_attacker(tuple_client_B_out_1(VAR_V_138,VAR_V_139)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax118,axiom, % 14.44/14.53 ! [VAR_V_146,VAR_V_147] : % 14.44/14.53 ( pred_attacker(tuple_client_B_out_1(VAR_V_146,VAR_V_147)) % 14.44/14.53 => pred_attacker(VAR_V_146) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax119,axiom, % 14.44/14.53 ! [VAR_V_149,VAR_V_150X30] : % 14.44/14.53 ( pred_attacker(tuple_client_B_out_1(VAR_V_149,VAR_V_150X30)) % 14.44/14.53 => pred_attacker(VAR_V_150X30) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax120,axiom, % 14.44/14.53 ! [VAR_V_153] : % 14.44/14.53 ( pred_attacker(VAR_V_153) % 14.44/14.53 => pred_attacker(tuple_client_B_in_5(VAR_V_153)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax121,axiom, % 14.44/14.53 ! [VAR_V_156] : % 14.44/14.53 ( pred_attacker(tuple_client_B_in_5(VAR_V_156)) % 14.44/14.53 => pred_attacker(VAR_V_156) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax122,axiom, % 14.44/14.53 ! [VAR_V_159] : % 14.44/14.53 ( pred_attacker(VAR_V_159) % 14.44/14.53 => pred_attacker(tuple_client_B_in_3(VAR_V_159)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax123,axiom, % 14.44/14.53 ! [VAR_V_162] : % 14.44/14.53 ( pred_attacker(tuple_client_B_in_3(VAR_V_162)) % 14.44/14.53 => pred_attacker(VAR_V_162) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax124,axiom, % 14.44/14.53 ! [VAR_V_165] : % 14.44/14.53 ( pred_attacker(VAR_V_165) % 14.44/14.53 => pred_attacker(tuple_client_B_in_2(VAR_V_165)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax125,axiom, % 14.44/14.53 ! [VAR_V_168] : % 14.44/14.53 ( pred_attacker(tuple_client_B_in_2(VAR_V_168)) % 14.44/14.53 => pred_attacker(VAR_V_168) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax126,axiom, % 14.44/14.53 ! [VAR_V_171] : % 14.44/14.53 ( pred_attacker(VAR_V_171) % 14.44/14.53 => pred_attacker(tuple_client_A_out_5(VAR_V_171)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax127,axiom, % 14.44/14.53 ! [VAR_V_174] : % 14.44/14.53 ( pred_attacker(tuple_client_A_out_5(VAR_V_174)) % 14.44/14.53 => pred_attacker(VAR_V_174) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax128,axiom, % 14.44/14.53 ! [VAR_V_177] : % 14.44/14.53 ( pred_attacker(VAR_V_177) % 14.44/14.53 => pred_attacker(tuple_client_A_out_3(VAR_V_177)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax129,axiom, % 14.44/14.53 ! [VAR_V_180X30] : % 14.44/14.53 ( pred_attacker(tuple_client_A_out_3(VAR_V_180X30)) % 14.44/14.53 => pred_attacker(VAR_V_180X30) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax130,axiom, % 14.44/14.53 ! [VAR_V_184,VAR_V_185] : % 14.44/14.53 ( ( pred_attacker(VAR_V_184) % 14.44/14.53 & pred_attacker(VAR_V_185) ) % 14.44/14.53 => pred_attacker(tuple_client_A_out_1(VAR_V_184,VAR_V_185)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax131,axiom, % 14.44/14.53 ! [VAR_V_192,VAR_V_193] : % 14.44/14.53 ( pred_attacker(tuple_client_A_out_1(VAR_V_192,VAR_V_193)) % 14.44/14.53 => pred_attacker(VAR_V_192) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax132,axiom, % 14.44/14.53 ! [VAR_V_195,VAR_V_196] : % 14.44/14.53 ( pred_attacker(tuple_client_A_out_1(VAR_V_195,VAR_V_196)) % 14.44/14.53 => pred_attacker(VAR_V_196) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax133,axiom, % 14.44/14.53 ! [VAR_V_199] : % 14.44/14.53 ( pred_attacker(VAR_V_199) % 14.44/14.53 => pred_attacker(tuple_client_A_in_4(VAR_V_199)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax134,axiom, % 14.44/14.53 ! [VAR_V_20X302] : % 14.44/14.53 ( pred_attacker(tuple_client_A_in_4(VAR_V_20X302)) % 14.44/14.53 => pred_attacker(VAR_V_20X302) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax135,axiom, % 14.44/14.53 ! [VAR_V_20X305] : % 14.44/14.53 ( pred_attacker(VAR_V_20X305) % 14.44/14.53 => pred_attacker(tuple_client_A_in_2(VAR_V_20X305)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax136,axiom, % 14.44/14.53 ! [VAR_V_20X308] : % 14.44/14.53 ( pred_attacker(tuple_client_A_in_2(VAR_V_20X308)) % 14.44/14.53 => pred_attacker(VAR_V_20X308) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax137,axiom, % 14.44/14.53 ! [VAR_V_212,VAR_V_213] : % 14.44/14.53 ( ( pred_attacker(VAR_V_212) % 14.44/14.53 & pred_attacker(VAR_V_213) ) % 14.44/14.53 => pred_attacker(constr_checksign(VAR_V_212,VAR_V_213)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax138,axiom, % 14.44/14.53 ! [VAR_V_215] : % 14.44/14.53 ( pred_attacker(VAR_V_215) % 14.44/14.53 => pred_attacker(constr_assoc_pair_2_get_1_bitstring(VAR_V_215)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax139,axiom, % 14.44/14.53 ! [VAR_V_217] : % 14.44/14.53 ( pred_attacker(VAR_V_217) % 14.44/14.53 => pred_attacker(constr_assoc_pair_2_get_1(VAR_V_217)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax140,axiom, % 14.44/14.53 ! [VAR_V_219] : % 14.44/14.53 ( pred_attacker(VAR_V_219) % 14.44/14.53 => pred_attacker(constr_assoc_pair_2_get_0x30_bitstring(VAR_V_219)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax141,axiom, % 14.44/14.53 ! [VAR_V_221] : % 14.44/14.53 ( pred_attacker(VAR_V_221) % 14.44/14.53 => pred_attacker(constr_assoc_pair_2_get_0x30(VAR_V_221)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax142,axiom, % 14.44/14.53 ! [VAR_V_224,VAR_V_225] : % 14.44/14.53 ( ( pred_attacker(VAR_V_224) % 14.44/14.53 & pred_attacker(VAR_V_225) ) % 14.44/14.53 => pred_attacker(tuple_assoc_pair(VAR_V_224,VAR_V_225)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax143,axiom, % 14.44/14.53 ! [VAR_V_232,VAR_V_233] : % 14.44/14.53 ( pred_attacker(tuple_assoc_pair(VAR_V_232,VAR_V_233)) % 14.44/14.53 => pred_attacker(VAR_V_232) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax144,axiom, % 14.44/14.53 ! [VAR_V_235,VAR_V_236] : % 14.44/14.53 ( pred_attacker(tuple_assoc_pair(VAR_V_235,VAR_V_236)) % 14.44/14.53 => pred_attacker(VAR_V_236) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax145,axiom, % 14.44/14.53 ! [VAR_V_240X30,VAR_V_241] : % 14.44/14.53 ( ( pred_attacker(VAR_V_240X30) % 14.44/14.53 & pred_attacker(VAR_V_241) ) % 14.44/14.53 => pred_attacker(constr_aenc(VAR_V_240X30,VAR_V_241)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax146,axiom, % 14.44/14.53 ! [VAR_V_244,VAR_V_245] : % 14.44/14.53 ( ( pred_attacker(VAR_V_244) % 14.44/14.53 & pred_attacker(VAR_V_245) ) % 14.44/14.53 => pred_attacker(constr_adec(VAR_V_244,VAR_V_245)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax147,axiom, % 14.44/14.53 pred_attacker(constr_CONST_4) ). % 14.44/14.53 % 14.44/14.53 fof(ax148,axiom, % 14.44/14.53 pred_attacker(constr_CONST_3) ). % 14.44/14.53 % 14.44/14.53 fof(ax149,axiom, % 14.44/14.53 pred_attacker(constr_CONST_2) ). % 14.44/14.53 % 14.44/14.53 fof(ax150,axiom, % 14.44/14.53 pred_attacker(constr_CONST_1) ). % 14.44/14.53 % 14.44/14.53 fof(ax151,axiom, % 14.44/14.53 pred_attacker(constr_CONST_0x30) ). % 14.44/14.53 % 14.44/14.53 fof(ax152,axiom, % 14.44/14.53 ! [VAR_V_252,VAR_V_253] : % 14.44/14.53 ( ( pred_attacker(VAR_V_252) % 14.44/14.53 & pred_attacker(VAR_V_253) ) % 14.44/14.53 => pred_attacker(tuple_2(VAR_V_252,VAR_V_253)) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax153,axiom, % 14.44/14.53 ! [VAR_V_260X30,VAR_V_261] : % 14.44/14.53 ( pred_attacker(tuple_2(VAR_V_260X30,VAR_V_261)) % 14.44/14.53 => pred_attacker(VAR_V_260X30) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax154,axiom, % 14.44/14.53 ! [VAR_V_263,VAR_V_264] : % 14.44/14.53 ( pred_attacker(tuple_2(VAR_V_263,VAR_V_264)) % 14.44/14.53 => pred_attacker(VAR_V_264) ) ). % 14.44/14.53 % 14.44/14.53 fof(ax155,axiom, % 14.44/14.53 ! [VAR_V_266,VAR_V_267] : % 14.44/14.53 ( ( pred_mess(VAR_V_267,VAR_V_266) % 14.44/14.53 & pred_attacker(VAR_V_267) ) % 14.44/14.54 => pred_attacker(VAR_V_266) ) ). % 14.44/14.54 % 14.44/14.54 fof(ax156,axiom, % 14.44/14.54 ! [VAR_V_268,VAR_V_269] : % 14.44/14.54 ( ( pred_attacker(VAR_V_269) % 14.44/14.54 & pred_attacker(VAR_V_268) ) % 14.44/14.54 => pred_mess(VAR_V_269,VAR_V_268) ) ). % 14.44/14.54 % 14.44/14.54 fof(ax157,axiom, % 14.44/14.54 pred_attacker(name_c) ). % 14.44/14.54 % 14.44/14.54 fof(ax158,axiom, % 14.44/14.54 pred_attacker(name_I) ). % 14.44/14.54 % 14.44/14.54 fof(ax159,axiom, % 14.44/14.54 pred_attacker(name_B) ). % 14.44/14.54 % 14.44/14.54 fof(ax160,axiom, % 14.44/14.54 pred_attacker(name_A) ). % 14.44/14.54 % 14.44/14.54 fof(ax161,axiom, % 14.44/14.54 ! [VAR_V_271] : pred_equal(VAR_V_271,VAR_V_271) ). % 14.44/14.54 % 14.44/14.54 fof(ax162,axiom, % 14.44/14.54 ! [VAR_V_272] : pred_attacker(name_new0x2Dname(VAR_V_272)) ). % 14.44/14.54 % 14.44/14.54 fof(ax163,axiom, % 14.44/14.54 pred_table(tuple_keys(name_A,constr_pkey(name_skA))) ). % 14.44/14.54 % 14.44/14.54 fof(ax164,axiom, % 14.44/14.54 pred_table(tuple_keys(name_B,constr_pkey(name_skB))) ). % 14.44/14.54 % 14.44/14.54 fof(ax165,axiom, % 14.44/14.54 pred_attacker(tuple_out_1(constr_pkey(name_skA))) ). % 14.44/14.54 % 14.44/14.54 fof(ax166,axiom, % 14.44/14.54 pred_attacker(tuple_out_2(constr_pkey(name_skB))) ). % 14.44/14.54 % 14.44/14.54 fof(ax167,axiom, % 14.44/14.54 pred_attacker(tuple_out_3(constr_pkey(name_skS))) ). % 14.44/14.54 % 14.44/14.54 fof(ax168,axiom, % 14.44/14.54 pred_attacker(tuple_client_A_out_1(name_A,name_I)) ). % 14.44/14.54 % 14.44/14.54 fof(ax169,axiom, % 14.44/14.54 ! [VAR_0X40SID_392,VAR_SIGN_I_PKI_391] : % 14.44/14.54 ( ( pred_eq_bitstring_bitstring(name_I,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_I_PKI_391,constr_pkey(name_skS)))) % 14.44/14.54 & pred_attacker(tuple_client_A_in_2(VAR_SIGN_I_PKI_391)) ) % 14.44/14.54 => pred_attacker(tuple_client_A_out_3(constr_aenc(tuple_assoc_pair(name_Na(VAR_0X40SID_392),name_A),constr_tuple_2_get_1_bitstring(constr_checksign(VAR_SIGN_I_PKI_391,constr_pkey(name_skS)))))) ) ). % 14.44/14.54 % 14.44/14.54 fof(ax170,axiom, % 14.44/14.54 ! [VAR_0X40SID_463,VAR_AENC_NA_NI_I_462,VAR_SIGN_I_PKI_464] : % 14.44/14.54 ( ( pred_eq_bitstring_bitstring(name_I,constr_assoc_pair_2_get_1(constr_assoc_pair_2_get_1_bitstring(constr_adec(VAR_AENC_NA_NI_I_462,name_skA)))) % 14.44/14.54 & pred_eq_bitstring_bitstring(name_Na(VAR_0X40SID_463),constr_assoc_pair_2_get_0x30(constr_adec(VAR_AENC_NA_NI_I_462,name_skA))) % 14.44/14.54 & pred_attacker(tuple_client_A_in_4(VAR_AENC_NA_NI_I_462)) % 14.44/14.54 & pred_eq_bitstring_bitstring(name_I,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_I_PKI_464,constr_pkey(name_skS)))) % 14.44/14.54 & pred_attacker(tuple_client_A_in_2(VAR_SIGN_I_PKI_464)) ) % 14.44/14.54 => pred_attacker(tuple_client_A_out_5(constr_aenc(constr_assoc_pair_2_get_0x30_bitstring(constr_assoc_pair_2_get_1_bitstring(constr_adec(VAR_AENC_NA_NI_I_462,name_skA))),constr_tuple_2_get_1_bitstring(constr_checksign(VAR_SIGN_I_PKI_464,constr_pkey(name_skS)))))) ) ). % 14.44/14.54 % 14.44/14.54 fof(ax171,axiom, % 14.44/14.54 pred_attacker(tuple_client_B_out_1(name_B,name_A)) ). % 14.44/14.54 % 14.44/14.54 fof(ax172,axiom, % 14.44/14.54 ! [VAR_0X40SID_581,VAR_AENC_NA_A_579,VAR_SIGN_A_PKA_580X30] : % 14.44/14.54 ( ( pred_eq_bitstring_bitstring(name_A,constr_assoc_pair_2_get_1(constr_adec(VAR_AENC_NA_A_579,name_skB))) % 14.44/14.54 & pred_attacker(tuple_client_B_in_3(VAR_AENC_NA_A_579)) % 14.44/14.54 & pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_580X30,constr_pkey(name_skS)))) % 14.44/14.54 & pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_580X30)) ) % 14.44/14.54 => pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_assoc_pair(constr_assoc_pair_2_get_0x30_bitstring(constr_adec(VAR_AENC_NA_A_579,name_skB)),tuple_assoc_pair(name_Nb(VAR_0X40SID_581),name_B)),constr_tuple_2_get_1_bitstring(constr_checksign(VAR_SIGN_A_PKA_580X30,constr_pkey(name_skS)))))) ) ). % 14.44/14.54 % 14.44/14.54 fof(ax173,axiom, % 14.44/14.54 ! [VAR_0X40SID_60X305,VAR_AENC_NA_A_60X307,VAR_AENC_NB_60X306,VAR_SIGN_A_PKA_60X308] : % 14.44/14.54 ( ( pred_eq_bitstring_bitstring(name_Nb(VAR_0X40SID_60X305),constr_adec(VAR_AENC_NB_60X306,name_skB)) % 14.44/14.54 & pred_attacker(tuple_client_B_in_5(VAR_AENC_NB_60X306)) % 14.44/14.54 & pred_eq_bitstring_bitstring(name_A,constr_assoc_pair_2_get_1(constr_adec(VAR_AENC_NA_A_60X307,name_skB))) % 14.44/14.54 & pred_attacker(tuple_client_B_in_3(VAR_AENC_NA_A_60X307)) % 14.44/14.54 & pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_60X308,constr_pkey(name_skS)))) % 14.44/14.54 & pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_60X308)) ) % 14.44/14.54 => pred_attacker(tuple_client_B_out_6(name_objective)) ) ). % 14.44/14.54 % 14.44/14.54 fof(ax174,axiom, % 14.44/14.54 ! [VAR_DST_647,VAR_PKDST_648,VAR_SRC_649] : % 14.44/14.54 ( ( pred_table(tuple_keys(VAR_DST_647,VAR_PKDST_648)) % 14.44/14.54 & pred_attacker(tuple_key_retrieval_server_in_1(VAR_SRC_649,VAR_DST_647)) ) % 14.44/14.54 => pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(VAR_DST_647,VAR_PKDST_648),name_skS))) ) ). % 14.44/14.54 % 14.44/14.54 fof(ax175,axiom, % 14.44/14.54 ! [VAR_HOST_70X301,VAR_PK_70X302] : % 14.44/14.54 ( ( VAR_HOST_70X301 != name_B % 14.44/14.54 & VAR_HOST_70X301 != name_A % 14.44/14.54 & pred_attacker(tuple_key_register_server_in_1(VAR_HOST_70X301,VAR_PK_70X302)) ) % 14.44/14.54 => pred_table(tuple_keys(VAR_HOST_70X301,VAR_PK_70X302)) ) ). % 14.44/14.54 % 14.44/14.54 fof(co0,conjecture, % 14.44/14.54 pred_attacker(name_objective) ). % 14.44/14.54 % 14.44/14.54 %-------------------------------------------------------------------------- % 14.44/14.54 %------------------------------------------- % 14.44/14.54 % Proof found % 14.44/14.54 % SZS status Theorem for theBenchmark % 14.44/14.54 % SZS output start Proof % 14.44/14.54 %ClaNum:235(EqnAxiom:59) % 14.44/14.54 %VarNum:229(SingletonVarNum:126) % 14.44/14.54 %MaxLitNum:4 % 14.44/14.54 %MaxfuncDepth:5 % 14.44/14.54 %SharedTerms:124 % 14.44/14.54 %goalClause: 169 % 14.44/14.54 %singleGoalClaCount:1 % 14.44/14.54 [60]P1(a1) % 14.44/14.54 [61]P1(a2) % 14.44/14.54 [62]P1(a3) % 14.44/14.54 [63]P1(a4) % 14.44/14.54 [64]P1(a5) % 14.44/14.54 [65]P1(a6) % 14.44/14.54 [66]P1(a21) % 14.44/14.54 [67]P1(a22) % 14.44/14.54 [68]P1(a23) % 14.44/14.54 [69]P1(a26) % 14.44/14.54 [70]P1(a27) % 14.44/14.54 [91]~E(a1,a2) % 14.44/14.54 [92]~E(a1,a3) % 14.44/14.54 [93]~E(a3,a2) % 14.44/14.54 [94]~E(a1,a4) % 14.44/14.54 [95]~E(a4,a2) % 14.44/14.54 [96]~E(a4,a3) % 14.44/14.54 [97]~E(a1,a5) % 14.44/14.54 [98]~E(a5,a2) % 14.44/14.54 [99]~E(a5,a3) % 14.44/14.54 [100]~E(a5,a4) % 14.44/14.54 [101]~E(a1,a6) % 14.44/14.54 [102]~E(a6,a2) % 14.44/14.54 [103]~E(a6,a3) % 14.44/14.54 [104]~E(a6,a4) % 14.44/14.54 [105]~E(a6,a5) % 14.44/14.54 [106]~E(a1,a21) % 14.44/14.54 [107]~E(a21,a2) % 14.44/14.54 [108]~E(a21,a3) % 14.44/14.54 [109]~E(a21,a4) % 14.44/14.54 [110]~E(a21,a5) % 14.44/14.54 [111]~E(a21,a6) % 14.44/14.54 [112]~E(a1,a22) % 14.44/14.54 [113]~E(a22,a2) % 14.44/14.54 [114]~E(a22,a3) % 14.44/14.54 [115]~E(a22,a4) % 14.44/14.54 [116]~E(a22,a5) % 14.44/14.54 [117]~E(a22,a6) % 14.44/14.54 [118]~E(a22,a21) % 14.44/14.54 [119]~E(a1,a23) % 14.44/14.54 [120]~E(a23,a2) % 14.44/14.54 [121]~E(a23,a3) % 14.44/14.54 [122]~E(a23,a4) % 14.44/14.54 [123]~E(a23,a5) % 14.44/14.54 [124]~E(a23,a6) % 14.44/14.54 [125]~E(a23,a21) % 14.44/14.54 [126]~E(a23,a22) % 14.44/14.54 [127]~E(a1,a32) % 14.44/14.54 [128]~E(a32,a2) % 14.44/14.54 [129]~E(a32,a3) % 14.44/14.54 [130]~E(a32,a4) % 14.44/14.54 [131]~E(a32,a5) % 14.44/14.54 [132]~E(a32,a6) % 14.44/14.54 [133]~E(a32,a21) % 14.44/14.54 [134]~E(a32,a22) % 14.44/14.54 [135]~E(a32,a23) % 14.44/14.54 [136]~E(a1,a31) % 14.44/14.54 [137]~E(a31,a2) % 14.44/14.54 [138]~E(a31,a3) % 14.44/14.54 [139]~E(a31,a4) % 14.44/14.54 [140]~E(a31,a5) % 14.44/14.54 [141]~E(a31,a6) % 14.44/14.54 [142]~E(a31,a21) % 14.44/14.54 [143]~E(a31,a22) % 14.44/14.54 [144]~E(a31,a23) % 14.44/14.54 [145]~E(a32,a31) % 14.44/14.54 [146]~E(a1,a30) % 14.44/14.54 [147]~E(a30,a2) % 14.44/14.54 [148]~E(a30,a3) % 14.44/14.54 [149]~E(a30,a4) % 14.44/14.54 [150]~E(a30,a5) % 14.44/14.54 [151]~E(a30,a6) % 14.44/14.54 [152]~E(a30,a21) % 14.44/14.54 [153]~E(a30,a22) % 14.44/14.54 [154]~E(a30,a23) % 14.44/14.54 [155]~E(a32,a30) % 14.44/14.54 [156]~E(a31,a30) % 14.44/14.54 [157]~E(a1,a29) % 14.44/14.54 [158]~E(a29,a2) % 14.44/14.54 [159]~E(a29,a3) % 14.44/14.54 [160]~E(a29,a4) % 14.44/14.54 [161]~E(a29,a5) % 14.44/14.54 [162]~E(a29,a6) % 14.44/14.54 [163]~E(a29,a21) % 14.44/14.54 [164]~E(a29,a22) % 14.44/14.54 [165]~E(a29,a23) % 14.44/14.54 [166]~E(a32,a29) % 14.44/14.54 [167]~E(a31,a29) % 14.44/14.54 [168]~E(a30,a29) % 14.44/14.54 [169]~P1(a32) % 14.44/14.54 [76]P1(f33(a21,a6)) % 14.44/14.54 [77]P1(f34(a6,a22)) % 14.44/14.54 [73]P1(f46(f7(a29))) % 14.44/14.54 [74]P1(f47(f7(a30))) % 14.44/14.54 [75]P1(f48(f7(a31))) % 14.44/14.54 [85]P3(f49(a6,f7(a31))) % 14.44/14.54 [86]P3(f49(a21,f7(a30))) % 14.44/14.54 [72]P2(x721,x721) % 14.44/14.54 [71]P1(f28(x711)) % 14.44/14.54 [78]E(f8(f18(x781,x782)),x781) % 14.44/14.54 [79]E(f9(f35(x791,x792)),x792) % 14.44/14.54 [80]E(f10(f35(x801,x802)),x801) % 14.44/14.54 [81]E(f14(f35(x811,x812)),x812) % 14.44/14.54 [82]E(f11(f35(x821,x822)),x821) % 14.44/14.54 [83]E(f19(f36(x831,x832)),x832) % 14.44/14.54 [84]E(f20(f36(x841,x842)),x841) % 14.44/14.54 [87]E(f16(f15(x871,x872),x872),x871) % 14.44/14.54 [88]E(f17(f18(x881,x882),f7(x882)),x881) % 14.44/14.54 [89]E(f13(f12(x891,f7(x892)),x892),x891) % 14.44/14.54 [90]E(f35(f35(x901,x902),x903),f35(x901,f35(x902,x903))) % 14.44/14.54 [170]~P1(x1701)+P1(f7(x1701)) % 14.44/14.54 [171]~P1(x1711)+P1(f8(x1711)) % 14.44/14.54 [172]~P1(x1721)+P1(f9(x1721)) % 14.44/14.54 [173]~P1(x1731)+P1(f10(x1731)) % 14.44/14.54 [174]~P1(x1741)+P1(f14(x1741)) % 14.44/14.54 [175]~P1(x1751)+P1(f11(x1751)) % 14.44/14.54 [176]~P1(x1761)+P1(f19(x1761)) % 14.44/14.54 [177]~P1(x1771)+P1(f20(x1771)) % 14.44/14.54 [178]~P1(x1781)+P1(f46(x1781)) % 14.44/14.54 [179]~P1(x1791)+P1(f47(x1791)) % 14.44/14.54 [180]~P1(x1801)+P1(f48(x1801)) % 14.44/14.54 [181]~P1(x1811)+P1(f50(x1811)) % 14.44/14.54 [182]~P1(x1821)+P1(f44(x1821)) % 14.44/14.54 [183]~P1(x1831)+P1(f45(x1831)) % 14.44/14.54 [184]~P1(x1841)+P1(f39(x1841)) % 14.44/14.54 [185]~P1(x1851)+P1(f40(x1851)) % 14.44/14.54 [186]~P1(x1861)+P1(f41(x1861)) % 14.44/14.54 [187]~P1(x1871)+P1(f42(x1871)) % 14.44/14.54 [188]~P1(x1881)+P1(f43(x1881)) % 14.44/14.54 [189]~P1(x1891)+P1(f37(x1891)) % 14.44/14.54 [190]~P1(x1901)+P1(f38(x1901)) % 14.44/14.54 [191]P1(x1911)+~P1(f46(x1911)) % 14.44/14.54 [192]P1(x1921)+~P1(f47(x1921)) % 14.44/14.54 [193]P1(x1931)+~P1(f48(x1931)) % 14.44/14.54 [194]P1(x1941)+~P1(f50(x1941)) % 14.44/14.54 [195]P1(x1951)+~P1(f44(x1951)) % 14.44/14.54 [196]P1(x1961)+~P1(f45(x1961)) % 14.44/14.54 [197]P1(x1971)+~P1(f39(x1971)) % 14.44/14.54 [198]P1(x1981)+~P1(f40(x1981)) % 14.44/14.54 [199]P1(x1991)+~P1(f41(x1991)) % 14.44/14.54 [200]P1(x2001)+~P1(f42(x2001)) % 14.44/14.54 [201]P1(x2011)+~P1(f43(x2011)) % 14.44/14.54 [202]P1(x2021)+~P1(f37(x2021)) % 14.44/14.54 [203]P1(x2031)+~P1(f38(x2031)) % 14.44/14.54 [218]P1(x2181)+~P1(f35(x2182,x2181)) % 14.44/14.54 [219]P1(x2191)+~P1(f36(x2192,x2191)) % 14.44/14.54 [220]P1(x2201)+~P1(f51(x2202,x2201)) % 14.44/14.54 [221]P1(x2211)+~P1(f52(x2212,x2211)) % 14.44/14.54 [222]P1(x2221)+~P1(f33(x2222,x2221)) % 14.44/14.54 [223]P1(x2231)+~P1(f34(x2232,x2231)) % 14.44/14.54 [224]P1(x2241)+~P1(f35(x2241,x2242)) % 14.44/14.54 [225]P1(x2251)+~P1(f36(x2251,x2252)) % 14.44/14.54 [226]P1(x2261)+~P1(f51(x2261,x2262)) % 14.44/14.54 [227]P1(x2271)+~P1(f52(x2271,x2272)) % 14.44/14.54 [228]P1(x2281)+~P1(f33(x2281,x2282)) % 14.44/14.54 [229]P1(x2291)+~P1(f34(x2291,x2292)) % 14.44/14.54 [233]~P1(f38(x2332))+P1(f43(f12(f35(f24(x2331),a6),f19(f17(x2332,f7(a29)))))) % 14.44/14.54 [204]~P1(x2042)+~P1(x2041)+P4(x2041,x2042) % 14.44/14.54 [205]~P4(x2052,x2051)+P1(x2051)+~P1(x2052) % 14.44/14.54 [206]~P1(x2062)+~P1(x2061)+P1(f12(x2061,x2062)) % 14.44/14.54 [207]~P1(x2072)+~P1(x2071)+P1(f13(x2071,x2072)) % 14.44/14.54 [208]~P1(x2082)+~P1(x2081)+P1(f15(x2081,x2082)) % 14.44/14.54 [209]~P1(x2092)+~P1(x2091)+P1(f16(x2091,x2092)) % 14.44/14.54 [210]~P1(x2102)+~P1(x2101)+P1(f18(x2101,x2102)) % 14.44/14.54 [211]~P1(x2112)+~P1(x2111)+P1(f17(x2111,x2112)) % 14.44/14.54 [212]~P1(x2122)+~P1(x2121)+P1(f35(x2121,x2122)) % 14.44/14.54 [213]~P1(x2132)+~P1(x2131)+P1(f36(x2131,x2132)) % 14.44/14.54 [214]~P1(x2142)+~P1(x2141)+P1(f51(x2141,x2142)) % 14.44/14.54 [215]~P1(x2152)+~P1(x2151)+P1(f52(x2151,x2152)) % 14.44/14.54 [216]~P1(x2162)+~P1(x2161)+P1(f33(x2161,x2162)) % 14.44/14.54 [217]~P1(x2172)+~P1(x2171)+P1(f34(x2171,x2172)) % 14.44/14.54 [234]~P1(f37(x2341))+~P1(f38(x2342))+P1(f42(f12(f10(f9(f13(x2341,a31))),f19(f17(x2342,f7(a29)))))) % 14.44/14.54 [232]~P3(f49(x2321,x2322))+~P1(f51(x2323,x2321))+P1(f50(f18(f36(x2321,x2322),a29))) % 14.44/14.54 [235]~P1(f40(x2351))+~P1(f41(x2353))+P1(f45(f12(f35(f10(f13(x2351,a30)),f35(f25(x2352),a21)),f19(f17(x2353,f7(a29)))))) % 14.44/14.54 [231]E(x2311,a21)+E(x2311,a6)+~P1(f52(x2311,x2312))+P3(f49(x2311,x2312)) % 14.44/14.54 [230]~P1(f39(x2301))+~P1(f40(x2302))+~P1(f41(x2303))+P1(f44(a32)) % 14.44/14.54 %EqnAxiom % 14.44/14.54 [1]E(x11,x11) % 14.44/14.54 [2]E(x22,x21)+~E(x21,x22) % 14.44/14.54 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 14.44/14.54 [4]~E(x41,x42)+E(f28(x41),f28(x42)) % 14.44/14.54 [5]~E(x51,x52)+E(f7(x51),f7(x52)) % 14.44/14.54 [6]~E(x61,x62)+E(f46(x61),f46(x62)) % 14.44/14.54 [7]~E(x71,x72)+E(f41(x71),f41(x72)) % 14.44/14.54 [8]~E(x81,x82)+E(f47(x81),f47(x82)) % 14.44/14.54 [9]~E(x91,x92)+E(f40(x91),f40(x92)) % 14.44/14.54 [10]~E(x101,x102)+E(f48(x101),f48(x102)) % 14.44/14.54 [11]~E(x111,x112)+E(f33(x111,x113),f33(x112,x113)) % 14.44/14.54 [12]~E(x121,x122)+E(f33(x123,x121),f33(x123,x122)) % 14.44/14.54 [13]~E(x131,x132)+E(f34(x131,x133),f34(x132,x133)) % 14.44/14.54 [14]~E(x141,x142)+E(f34(x143,x141),f34(x143,x142)) % 14.44/14.54 [15]~E(x151,x152)+E(f18(x151,x153),f18(x152,x153)) % 14.44/14.54 [16]~E(x161,x162)+E(f18(x163,x161),f18(x163,x162)) % 14.44/14.54 [17]~E(x171,x172)+E(f8(x171),f8(x172)) % 14.44/14.54 [18]~E(x181,x182)+E(f35(x181,x183),f35(x182,x183)) % 14.44/14.54 [19]~E(x191,x192)+E(f35(x193,x191),f35(x193,x192)) % 14.44/14.54 [20]~E(x201,x202)+E(f9(x201),f9(x202)) % 14.44/14.54 [21]~E(x211,x212)+E(f50(x211),f50(x212)) % 14.44/14.54 [22]~E(x221,x222)+E(f10(x221),f10(x222)) % 14.44/14.54 [23]~E(x231,x232)+E(f49(x231,x233),f49(x232,x233)) % 14.44/14.54 [24]~E(x241,x242)+E(f49(x243,x241),f49(x243,x242)) % 14.44/14.54 [25]~E(x251,x252)+E(f14(x251),f14(x252)) % 14.44/14.54 [26]~E(x261,x262)+E(f36(x261,x263),f36(x262,x263)) % 14.44/14.54 [27]~E(x271,x272)+E(f36(x273,x271),f36(x273,x272)) % 14.44/14.54 [28]~E(x281,x282)+E(f11(x281),f11(x282)) % 14.44/14.54 [29]~E(x291,x292)+E(f51(x291,x293),f51(x292,x293)) % 14.44/14.54 [30]~E(x301,x302)+E(f51(x303,x301),f51(x303,x302)) % 14.44/14.54 [31]~E(x311,x312)+E(f19(x311),f19(x312)) % 14.44/14.54 [32]~E(x321,x322)+E(f12(x321,x323),f12(x322,x323)) % 14.44/14.54 [33]~E(x331,x332)+E(f12(x333,x331),f12(x333,x332)) % 14.44/14.54 [34]~E(x341,x342)+E(f20(x341),f20(x342)) % 14.44/14.54 [35]~E(x351,x352)+E(f45(x351),f45(x352)) % 14.44/14.54 [36]~E(x361,x362)+E(f52(x361,x363),f52(x362,x363)) % 14.44/14.54 [37]~E(x371,x372)+E(f52(x373,x371),f52(x373,x372)) % 14.44/14.54 [38]~E(x381,x382)+E(f37(x381),f37(x382)) % 14.44/14.54 [39]~E(x391,x392)+E(f38(x391),f38(x392)) % 14.44/14.54 [40]~E(x401,x402)+E(f15(x401,x403),f15(x402,x403)) % 14.44/14.54 [41]~E(x411,x412)+E(f15(x413,x411),f15(x413,x412)) % 14.44/14.54 [42]~E(x421,x422)+E(f16(x421,x423),f16(x422,x423)) % 14.44/14.54 [43]~E(x431,x432)+E(f16(x433,x431),f16(x433,x432)) % 14.44/14.54 [44]~E(x441,x442)+E(f42(x441),f42(x442)) % 14.44/14.54 [45]~E(x451,x452)+E(f43(x451),f43(x452)) % 14.44/14.54 [46]~E(x461,x462)+E(f17(x461,x463),f17(x462,x463)) % 14.44/14.54 [47]~E(x471,x472)+E(f17(x473,x471),f17(x473,x472)) % 14.44/14.54 [48]~E(x481,x482)+E(f24(x481),f24(x482)) % 14.44/14.54 [49]~E(x491,x492)+E(f25(x491),f25(x492)) % 14.44/14.54 [50]~E(x501,x502)+E(f13(x501,x503),f13(x502,x503)) % 14.44/14.54 [51]~E(x511,x512)+E(f13(x513,x511),f13(x513,x512)) % 14.44/14.54 [52]~E(x521,x522)+E(f44(x521),f44(x522)) % 14.44/14.54 [53]~E(x531,x532)+E(f39(x531),f39(x532)) % 14.44/14.54 [54]~P1(x541)+P1(x542)+~E(x541,x542) % 14.44/14.54 [55]~P3(x551)+P3(x552)+~E(x551,x552) % 14.44/14.54 [56]P2(x562,x563)+~E(x561,x562)+~P2(x561,x563) % 14.44/14.54 [57]P2(x573,x572)+~E(x571,x572)+~P2(x573,x571) % 14.44/14.54 [58]P4(x582,x583)+~E(x581,x582)+~P4(x581,x583) % 14.44/14.54 [59]P4(x593,x592)+~E(x591,x592)+~P4(x593,x591) % 14.44/14.54 % 14.44/14.54 %------------------------------------------- % 14.44/14.55 cnf(2801,plain, % 14.44/14.55 (P1(f39(f40(a1)))), % 14.44/14.55 inference(scs_inference,[],[60,184,185])). % 14.44/14.55 cnf(2802,plain, % 14.44/14.55 (~P1(f40(x28021))+~P1(f41(x28022))+P1(f44(a32))), % 14.44/14.55 inference(scs_inference,[],[2801,230])). % 14.44/14.55 cnf(2803,plain, % 14.44/14.55 (P1(f40(a1))), % 14.44/14.55 inference(scs_inference,[],[2801,197])). % 14.44/14.55 cnf(2873,plain, % 14.44/14.55 (~P1(f41(x28731))+P1(f44(a32))), % 14.44/14.55 inference(scs_inference,[],[2803,2802])). % 14.44/14.55 cnf(3088,plain, % 14.44/14.55 (P1(f41(f42(a1)))), % 14.44/14.55 inference(scs_inference,[],[60,186,187])). % 14.44/14.55 cnf(3089,plain, % 14.44/14.55 (P1(f44(a32))), % 14.44/14.55 inference(scs_inference,[],[3088,2873])). % 14.44/14.55 cnf(3107,plain, % 14.44/14.55 ($false), % 14.44/14.55 inference(scs_inference,[],[169,3089,195]), % 14.44/14.55 ['proof']). % 14.44/14.55 % SZS output end Proof % 14.44/14.55 % Total time :13.880000s %------------------------------------------------------------------------------