%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWW959+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 : n003.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:37 EDT 2024 % Result : Theorem 2.17s 2.28s % Output : CNFRefutation 2.17s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.11 % Problem : SWW959+1 : TPTP v8.2.0. Released v7.4.0. % 0.09/0.11 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.32 % Computer : n003.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 300 % 0.12/0.32 % DateTime : Wed Jun 19 07:40:54 EDT 2024 % 0.12/0.32 % CPUTime : % 0.19/0.54 start to proof:theBenchmark % 2.17/2.25 %------------------------------------------- % 2.17/2.25 % File :CSE---1.7 % 2.17/2.25 % Problem :theBenchmark % 2.17/2.25 % Transform :cnf % 2.17/2.25 % Format :tptp:raw % 2.17/2.25 % Command :java -jar mcs_scs.jar %d %s % 2.17/2.25 % 2.17/2.26 % Result :Theorem 1.670000s % 2.17/2.26 % Output :CNFRefutation 1.670000s % 2.17/2.26 %------------------------------------------- % 2.17/2.26 %-------------------------------------------------------------------------- % 2.17/2.26 % File : SWW959+1 : TPTP v8.2.0. Released v7.4.0. % 2.17/2.26 % Domain : Software Verification % 2.17/2.26 % Problem : Attack on Needham-Schroeder Public Key Protocol % 2.17/2.26 % Version : [LT19] axioms : Especial. % 2.17/2.26 % English : Attack demonstrates an impersonation attack, violating weak % 2.17/2.26 % agreement property of A to B. % 2.17/2.26 % 2.17/2.26 % Refs : [BO97] Bull & Otway (1997), The Authentication Protocol % 2.17/2.26 % : [RS98] Ryan & Schneider (1998), An Attack on a Recursive Auth % 2.17/2.26 % : [LT19] Li & Tiu (2019), Combining ProVerif and Automated Theo % 2.17/2.26 % : [Li20] Li (2020), Email to Geoff Sutcliffe % 2.17/2.26 % Source : [Li20] % 2.17/2.26 % Names : NSPK-agree-A-to-B.p [LT20] % 2.17/2.26 % 2.17/2.26 % Status : Theorem % 2.17/2.26 % Rating : 0.42 v8.2.0, 0.36 v8.1.0, 0.33 v7.5.0, 0.38 v7.4.0 % 2.17/2.26 % Syntax : Number of formulae : 169 ( 108 unt; 0 def) % 2.17/2.26 % Number of atoms : 258 ( 88 equ) % 2.17/2.26 % Maximal formula atoms : 7 ( 1 avg) % 2.17/2.26 % Number of connectives : 169 ( 80 ~; 0 |; 28 &) % 2.17/2.26 % ( 0 <=>; 61 =>; 0 <=; 0 <~>) % 2.17/2.26 % Maximal formula depth : 11 ( 3 avg) % 2.17/2.26 % Maximal term depth : 6 ( 1 avg) % 2.17/2.26 % Number of predicates : 6 ( 5 usr; 0 prp; 1-2 aty) % 2.17/2.26 % Number of functors : 49 ( 49 usr; 15 con; 0-2 aty) % 2.17/2.26 % Number of variables : 115 ( 115 !; 0 ?) % 2.17/2.26 % SPC : FOF_THM_RFO_SEQ % 2.17/2.26 % 2.17/2.26 % Comments : Generated by a modified version of ProVerif used in the % 2.17/2.26 % ProVerif-ATP project [LT19]. % 2.17/2.26 %-------------------------------------------------------------------------- % 2.17/2.26 fof(ax0,axiom, % 2.17/2.26 constr_CONST_0x30 != constr_CONST_1 ). % 2.17/2.26 % 2.17/2.26 fof(ax1,axiom, % 2.17/2.26 constr_CONST_0x30 != constr_CONST_2 ). % 2.17/2.26 % 2.17/2.26 fof(ax2,axiom, % 2.17/2.26 constr_CONST_0x30 != constr_CONST_3 ). % 2.17/2.26 % 2.17/2.26 fof(ax3,axiom, % 2.17/2.26 constr_CONST_0x30 != constr_CONST_4 ). % 2.17/2.26 % 2.17/2.26 fof(ax4,axiom, % 2.17/2.26 constr_CONST_0x30 != name_A ). % 2.17/2.26 % 2.17/2.26 fof(ax5,axiom, % 2.17/2.26 constr_CONST_0x30 != name_B ). % 2.17/2.26 % 2.17/2.26 fof(ax6,axiom, % 2.17/2.26 constr_CONST_0x30 != name_I ). % 2.17/2.26 % 2.17/2.26 fof(ax7,axiom, % 2.17/2.26 constr_CONST_0x30 != name_c ). % 2.17/2.26 % 2.17/2.26 fof(ax8,axiom, % 2.17/2.26 constr_CONST_0x30 != name_objective ). % 2.17/2.26 % 2.17/2.26 fof(ax9,axiom, % 2.17/2.26 constr_CONST_0x30 != name_skA ). % 2.17/2.26 % 2.17/2.26 fof(ax10,axiom, % 2.17/2.26 constr_CONST_0x30 != name_skB ). % 2.17/2.26 % 2.17/2.26 fof(ax11,axiom, % 2.17/2.26 constr_CONST_0x30 != name_skS ). % 2.17/2.26 % 2.17/2.26 fof(ax12,axiom, % 2.17/2.26 constr_CONST_1 != constr_CONST_2 ). % 2.17/2.26 % 2.17/2.26 fof(ax13,axiom, % 2.17/2.26 constr_CONST_1 != constr_CONST_3 ). % 2.17/2.26 % 2.17/2.26 fof(ax14,axiom, % 2.17/2.26 constr_CONST_1 != constr_CONST_4 ). % 2.17/2.26 % 2.17/2.26 fof(ax15,axiom, % 2.17/2.26 constr_CONST_1 != name_A ). % 2.17/2.26 % 2.17/2.26 fof(ax16,axiom, % 2.17/2.26 constr_CONST_1 != name_B ). % 2.17/2.26 % 2.17/2.26 fof(ax17,axiom, % 2.17/2.26 constr_CONST_1 != name_I ). % 2.17/2.26 % 2.17/2.26 fof(ax18,axiom, % 2.17/2.26 constr_CONST_1 != name_c ). % 2.17/2.26 % 2.17/2.26 fof(ax19,axiom, % 2.17/2.26 constr_CONST_1 != name_objective ). % 2.17/2.26 % 2.17/2.26 fof(ax20,axiom, % 2.17/2.26 constr_CONST_1 != name_skA ). % 2.17/2.26 % 2.17/2.26 fof(ax21,axiom, % 2.17/2.26 constr_CONST_1 != name_skB ). % 2.17/2.26 % 2.17/2.26 fof(ax22,axiom, % 2.17/2.26 constr_CONST_1 != name_skS ). % 2.17/2.26 % 2.17/2.26 fof(ax23,axiom, % 2.17/2.26 constr_CONST_2 != constr_CONST_3 ). % 2.17/2.26 % 2.17/2.26 fof(ax24,axiom, % 2.17/2.26 constr_CONST_2 != constr_CONST_4 ). % 2.17/2.26 % 2.17/2.26 fof(ax25,axiom, % 2.17/2.26 constr_CONST_2 != name_A ). % 2.17/2.26 % 2.17/2.26 fof(ax26,axiom, % 2.17/2.26 constr_CONST_2 != name_B ). % 2.17/2.26 % 2.17/2.26 fof(ax27,axiom, % 2.17/2.26 constr_CONST_2 != name_I ). % 2.17/2.26 % 2.17/2.26 fof(ax28,axiom, % 2.17/2.26 constr_CONST_2 != name_c ). % 2.17/2.26 % 2.17/2.26 fof(ax29,axiom, % 2.17/2.26 constr_CONST_2 != name_objective ). % 2.17/2.26 % 2.17/2.26 fof(ax30,axiom, % 2.17/2.26 constr_CONST_2 != name_skA ). % 2.17/2.26 % 2.17/2.26 fof(ax31,axiom, % 2.17/2.26 constr_CONST_2 != name_skB ). % 2.17/2.26 % 2.17/2.26 fof(ax32,axiom, % 2.17/2.27 constr_CONST_2 != name_skS ). % 2.17/2.27 % 2.17/2.27 fof(ax33,axiom, % 2.17/2.27 constr_CONST_3 != constr_CONST_4 ). % 2.17/2.27 % 2.17/2.27 fof(ax34,axiom, % 2.17/2.27 constr_CONST_3 != name_A ). % 2.17/2.27 % 2.17/2.27 fof(ax35,axiom, % 2.17/2.27 constr_CONST_3 != name_B ). % 2.17/2.27 % 2.17/2.27 fof(ax36,axiom, % 2.17/2.27 constr_CONST_3 != name_I ). % 2.17/2.27 % 2.17/2.27 fof(ax37,axiom, % 2.17/2.27 constr_CONST_3 != name_c ). % 2.17/2.27 % 2.17/2.27 fof(ax38,axiom, % 2.17/2.27 constr_CONST_3 != name_objective ). % 2.17/2.27 % 2.17/2.27 fof(ax39,axiom, % 2.17/2.27 constr_CONST_3 != name_skA ). % 2.17/2.27 % 2.17/2.27 fof(ax40,axiom, % 2.17/2.27 constr_CONST_3 != name_skB ). % 2.17/2.27 % 2.17/2.27 fof(ax41,axiom, % 2.17/2.27 constr_CONST_3 != name_skS ). % 2.17/2.27 % 2.17/2.27 fof(ax42,axiom, % 2.17/2.27 constr_CONST_4 != name_A ). % 2.17/2.27 % 2.17/2.27 fof(ax43,axiom, % 2.17/2.27 constr_CONST_4 != name_B ). % 2.17/2.27 % 2.17/2.27 fof(ax44,axiom, % 2.17/2.27 constr_CONST_4 != name_I ). % 2.17/2.27 % 2.17/2.27 fof(ax45,axiom, % 2.17/2.27 constr_CONST_4 != name_c ). % 2.17/2.27 % 2.17/2.27 fof(ax46,axiom, % 2.17/2.27 constr_CONST_4 != name_objective ). % 2.17/2.27 % 2.17/2.27 fof(ax47,axiom, % 2.17/2.27 constr_CONST_4 != name_skA ). % 2.17/2.27 % 2.17/2.27 fof(ax48,axiom, % 2.17/2.27 constr_CONST_4 != name_skB ). % 2.17/2.27 % 2.17/2.27 fof(ax49,axiom, % 2.17/2.27 constr_CONST_4 != name_skS ). % 2.17/2.27 % 2.17/2.27 fof(ax50,axiom, % 2.17/2.27 name_A != name_B ). % 2.17/2.27 % 2.17/2.27 fof(ax51,axiom, % 2.17/2.27 name_A != name_I ). % 2.17/2.27 % 2.17/2.27 fof(ax52,axiom, % 2.17/2.27 name_A != name_c ). % 2.17/2.27 % 2.17/2.27 fof(ax53,axiom, % 2.17/2.27 name_A != name_objective ). % 2.17/2.27 % 2.17/2.27 fof(ax54,axiom, % 2.17/2.27 name_A != name_skA ). % 2.17/2.27 % 2.17/2.27 fof(ax55,axiom, % 2.17/2.27 name_A != name_skB ). % 2.17/2.27 % 2.17/2.27 fof(ax56,axiom, % 2.17/2.27 name_A != name_skS ). % 2.17/2.27 % 2.17/2.27 fof(ax57,axiom, % 2.17/2.27 name_B != name_I ). % 2.17/2.27 % 2.17/2.27 fof(ax58,axiom, % 2.17/2.27 name_B != name_c ). % 2.17/2.27 % 2.17/2.27 fof(ax59,axiom, % 2.17/2.27 name_B != name_objective ). % 2.17/2.27 % 2.17/2.27 fof(ax60,axiom, % 2.17/2.27 name_B != name_skA ). % 2.17/2.27 % 2.17/2.27 fof(ax61,axiom, % 2.17/2.27 name_B != name_skB ). % 2.17/2.27 % 2.17/2.27 fof(ax62,axiom, % 2.17/2.27 name_B != name_skS ). % 2.17/2.27 % 2.17/2.27 fof(ax63,axiom, % 2.17/2.27 name_I != name_c ). % 2.17/2.27 % 2.17/2.27 fof(ax64,axiom, % 2.17/2.27 name_I != name_objective ). % 2.17/2.27 % 2.17/2.27 fof(ax65,axiom, % 2.17/2.27 name_I != name_skA ). % 2.17/2.27 % 2.17/2.27 fof(ax66,axiom, % 2.17/2.27 name_I != name_skB ). % 2.17/2.27 % 2.17/2.27 fof(ax67,axiom, % 2.17/2.27 name_I != name_skS ). % 2.17/2.27 % 2.17/2.27 fof(ax68,axiom, % 2.17/2.27 name_c != name_objective ). % 2.17/2.27 % 2.17/2.27 fof(ax69,axiom, % 2.17/2.27 name_c != name_skA ). % 2.17/2.27 % 2.17/2.27 fof(ax70,axiom, % 2.17/2.27 name_c != name_skB ). % 2.17/2.27 % 2.17/2.27 fof(ax71,axiom, % 2.17/2.27 name_c != name_skS ). % 2.17/2.27 % 2.17/2.27 fof(ax72,axiom, % 2.17/2.27 name_objective != name_skA ). % 2.17/2.27 % 2.17/2.27 fof(ax73,axiom, % 2.17/2.27 name_objective != name_skB ). % 2.17/2.27 % 2.17/2.27 fof(ax74,axiom, % 2.17/2.27 name_objective != name_skS ). % 2.17/2.27 % 2.17/2.27 fof(ax75,axiom, % 2.17/2.27 name_skA != name_skB ). % 2.17/2.27 % 2.17/2.27 fof(ax76,axiom, % 2.17/2.27 name_skA != name_skS ). % 2.17/2.27 % 2.17/2.27 fof(ax77,axiom, % 2.17/2.27 name_skB != name_skS ). % 2.17/2.27 % 2.17/2.27 fof(ax78,axiom, % 2.17/2.27 ! [VAR_K_18,VAR_M_17] : constr_adec(constr_aenc(VAR_M_17,constr_pkey(VAR_K_18)),VAR_K_18) = VAR_M_17 ). % 2.17/2.27 % 2.17/2.27 fof(ax79,axiom, % 2.17/2.27 ! [VAR_K_16,VAR_M_15] : constr_dec(constr_enc(VAR_M_15,VAR_K_16),VAR_K_16) = VAR_M_15 ). % 2.17/2.27 % 2.17/2.27 fof(ax80,axiom, % 2.17/2.27 ! [VAR_K_14,VAR_M_13] : constr_getmess(constr_sign(VAR_M_13,VAR_K_14)) = VAR_M_13 ). % 2.17/2.27 % 2.17/2.27 fof(ax81,axiom, % 2.17/2.27 ! [VAR_K_0X30,VAR_M_0X30] : constr_checksign(constr_sign(VAR_M_0X30,VAR_K_0X30),constr_pkey(VAR_K_0X30)) = VAR_M_0X30 ). % 2.17/2.27 % 2.17/2.27 fof(ax82,axiom, % 2.17/2.27 ! [VAR_X0X30_11,VAR_X1_12] : constr_tuple_2_get_1_bitstring(tuple_2(VAR_X0X30_11,VAR_X1_12)) = VAR_X1_12 ). % 2.17/2.27 % 2.17/2.27 fof(ax83,axiom, % 2.17/2.27 ! [VAR_X0X30_9,VAR_X1_10X30] : constr_tuple_2_get_0x30_bitstring(tuple_2(VAR_X0X30_9,VAR_X1_10X30)) = VAR_X0X30_9 ). % 2.17/2.27 % 2.17/2.27 fof(ax84,axiom, % 2.17/2.27 ! [VAR_X0X30_7,VAR_X1_8] : constr_tuple_2_get_1(tuple_2(VAR_X0X30_7,VAR_X1_8)) = VAR_X1_8 ). % 2.17/2.27 % 2.17/2.27 fof(ax85,axiom, % 2.17/2.27 ! [VAR_X0X30_0X30,VAR_X1_0X30] : constr_tuple_2_get_0x30(tuple_2(VAR_X0X30_0X30,VAR_X1_0X30)) = VAR_X0X30_0X30 ). % 2.17/2.27 % 2.17/2.27 fof(ax86,axiom, % 2.17/2.27 ! [VAR_X_35,VAR_Y_36] : pred_eq_bitstring_bitstring(VAR_X_35,VAR_Y_36) ). % 2.17/2.27 % 2.17/2.27 fof(ax87,axiom, % 2.17/2.27 ! [VAR_V_42] : % 2.17/2.27 ( pred_attacker(VAR_V_42) % 2.17/2.27 => pred_attacker(constr_tuple_2_get_1_bitstring(VAR_V_42)) ) ). % 2.17/2.27 % 2.17/2.27 fof(ax88,axiom, % 2.17/2.27 ! [VAR_V_44] : % 2.17/2.27 ( pred_attacker(VAR_V_44) % 2.17/2.27 => pred_attacker(constr_tuple_2_get_1(VAR_V_44)) ) ). % 2.17/2.27 % 2.17/2.27 fof(ax89,axiom, % 2.17/2.27 ! [VAR_V_46] : % 2.17/2.27 ( pred_attacker(VAR_V_46) % 2.17/2.27 => pred_attacker(constr_tuple_2_get_0x30_bitstring(VAR_V_46)) ) ). % 2.17/2.27 % 2.17/2.27 fof(ax90,axiom, % 2.17/2.27 ! [VAR_V_48] : % 2.17/2.27 ( pred_attacker(VAR_V_48) % 2.17/2.27 => pred_attacker(constr_tuple_2_get_0x30(VAR_V_48)) ) ). % 2.17/2.27 % 2.17/2.27 fof(ax91,axiom, % 2.17/2.27 pred_attacker(tuple_true) ). % 2.17/2.27 % 2.17/2.27 fof(ax92,axiom, % 2.17/2.27 ! [VAR_V_51,VAR_V_52] : % 2.17/2.27 ( ( pred_attacker(VAR_V_51) % 2.17/2.27 & pred_attacker(VAR_V_52) ) % 2.17/2.27 => pred_attacker(constr_sign(VAR_V_51,VAR_V_52)) ) ). % 2.17/2.27 % 2.17/2.27 fof(ax93,axiom, % 2.17/2.27 ! [VAR_V_54] : % 2.17/2.27 ( pred_attacker(VAR_V_54) % 2.17/2.27 => pred_attacker(constr_pkey(VAR_V_54)) ) ). % 2.17/2.27 % 2.17/2.27 fof(ax94,axiom, % 2.17/2.27 ! [VAR_V_56] : % 2.17/2.27 ( pred_attacker(VAR_V_56) % 2.17/2.27 => pred_attacker(tuple_out_3(VAR_V_56)) ) ). % 2.17/2.27 % 2.17/2.27 fof(ax95,axiom, % 2.17/2.27 ! [VAR_V_59] : % 2.17/2.27 ( pred_attacker(tuple_out_3(VAR_V_59)) % 2.17/2.27 => pred_attacker(VAR_V_59) ) ). % 2.17/2.27 % 2.17/2.27 fof(ax96,axiom, % 2.17/2.27 ! [VAR_V_62] : % 2.17/2.27 ( pred_attacker(VAR_V_62) % 2.17/2.27 => pred_attacker(tuple_out_2(VAR_V_62)) ) ). % 2.17/2.27 % 2.17/2.27 fof(ax97,axiom, % 2.17/2.27 ! [VAR_V_65] : % 2.17/2.27 ( pred_attacker(tuple_out_2(VAR_V_65)) % 2.17/2.27 => pred_attacker(VAR_V_65) ) ). % 2.17/2.27 % 2.17/2.27 fof(ax98,axiom, % 2.17/2.27 ! [VAR_V_68] : % 2.17/2.27 ( pred_attacker(VAR_V_68) % 2.17/2.27 => pred_attacker(tuple_out_1(VAR_V_68)) ) ). % 2.17/2.27 % 2.17/2.27 fof(ax99,axiom, % 2.17/2.27 ! [VAR_V_71] : % 2.17/2.27 ( pred_attacker(tuple_out_1(VAR_V_71)) % 2.17/2.27 => pred_attacker(VAR_V_71) ) ). % 2.17/2.27 % 2.17/2.27 fof(ax100,axiom, % 2.17/2.27 ! [VAR_V_75] : % 2.17/2.27 ( pred_attacker(VAR_V_75) % 2.17/2.27 => pred_attacker(tuple_key_retrieval_server_out_2(VAR_V_75)) ) ). % 2.17/2.27 % 2.17/2.27 fof(ax101,axiom, % 2.17/2.27 ! [VAR_V_78] : % 2.17/2.27 ( pred_attacker(tuple_key_retrieval_server_out_2(VAR_V_78)) % 2.17/2.27 => pred_attacker(VAR_V_78) ) ). % 2.17/2.27 % 2.17/2.27 fof(ax102,axiom, % 2.17/2.27 ! [VAR_V_82,VAR_V_83] : % 2.17/2.27 ( ( pred_attacker(VAR_V_82) % 2.17/2.27 & pred_attacker(VAR_V_83) ) % 2.17/2.27 => pred_attacker(tuple_key_retrieval_server_in_1(VAR_V_82,VAR_V_83)) ) ). % 2.17/2.27 % 2.17/2.27 fof(ax103,axiom, % 2.17/2.27 ! [VAR_V_90X30,VAR_V_91] : % 2.17/2.27 ( pred_attacker(tuple_key_retrieval_server_in_1(VAR_V_90X30,VAR_V_91)) % 2.17/2.27 => pred_attacker(VAR_V_90X30) ) ). % 2.17/2.27 % 2.17/2.27 fof(ax104,axiom, % 2.17/2.27 ! [VAR_V_93,VAR_V_94] : % 2.17/2.27 ( pred_attacker(tuple_key_retrieval_server_in_1(VAR_V_93,VAR_V_94)) % 2.17/2.27 => pred_attacker(VAR_V_94) ) ). % 2.17/2.27 % 2.17/2.27 fof(ax105,axiom, % 2.17/2.27 ! [VAR_V_98,VAR_V_99] : % 2.17/2.27 ( ( pred_attacker(VAR_V_98) % 2.17/2.27 & pred_attacker(VAR_V_99) ) % 2.17/2.27 => pred_attacker(tuple_key_register_server_in_1(VAR_V_98,VAR_V_99)) ) ). % 2.17/2.27 % 2.17/2.27 fof(ax106,axiom, % 2.17/2.27 ! [VAR_V_10X306,VAR_V_10X307] : % 2.17/2.27 ( pred_attacker(tuple_key_register_server_in_1(VAR_V_10X306,VAR_V_10X307)) % 2.17/2.27 => pred_attacker(VAR_V_10X306) ) ). % 2.17/2.27 % 2.17/2.27 fof(ax107,axiom, % 2.17/2.27 ! [VAR_V_10X309,VAR_V_110X30] : % 2.17/2.27 ( pred_attacker(tuple_key_register_server_in_1(VAR_V_10X309,VAR_V_110X30)) % 2.17/2.27 => pred_attacker(VAR_V_110X30) ) ). % 2.17/2.27 % 2.17/2.27 fof(ax108,axiom, % 2.17/2.27 ! [VAR_V_113] : % 2.17/2.27 ( pred_attacker(VAR_V_113) % 2.17/2.27 => pred_attacker(constr_getmess(VAR_V_113)) ) ). % 2.17/2.27 % 2.17/2.27 fof(ax109,axiom, % 2.17/2.27 pred_attacker(tuple_false) ). % 2.17/2.27 % 2.17/2.27 fof(ax110,axiom, % 2.17/2.27 ! [VAR_V_116,VAR_V_117] : % 2.17/2.27 ( ( pred_attacker(VAR_V_116) % 2.17/2.27 & pred_attacker(VAR_V_117) ) % 2.17/2.28 => pred_attacker(constr_enc(VAR_V_116,VAR_V_117)) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax111,axiom, % 2.17/2.28 ! [VAR_V_120X30,VAR_V_121] : % 2.17/2.28 ( ( pred_attacker(VAR_V_120X30) % 2.17/2.28 & pred_attacker(VAR_V_121) ) % 2.17/2.28 => pred_attacker(constr_dec(VAR_V_120X30,VAR_V_121)) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax112,axiom, % 2.17/2.28 ! [VAR_V_123] : % 2.17/2.28 ( pred_attacker(VAR_V_123) % 2.17/2.28 => pred_attacker(tuple_client_B_out_6(VAR_V_123)) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax113,axiom, % 2.17/2.28 ! [VAR_V_126] : % 2.17/2.28 ( pred_attacker(tuple_client_B_out_6(VAR_V_126)) % 2.17/2.28 => pred_attacker(VAR_V_126) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax114,axiom, % 2.17/2.28 ! [VAR_V_129] : % 2.17/2.28 ( pred_attacker(VAR_V_129) % 2.17/2.28 => pred_attacker(tuple_client_B_out_4(VAR_V_129)) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax115,axiom, % 2.17/2.28 ! [VAR_V_132] : % 2.17/2.28 ( pred_attacker(tuple_client_B_out_4(VAR_V_132)) % 2.17/2.28 => pred_attacker(VAR_V_132) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax116,axiom, % 2.17/2.28 ! [VAR_V_136,VAR_V_137] : % 2.17/2.28 ( ( pred_attacker(VAR_V_136) % 2.17/2.28 & pred_attacker(VAR_V_137) ) % 2.17/2.28 => pred_attacker(tuple_client_B_out_1(VAR_V_136,VAR_V_137)) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax117,axiom, % 2.17/2.28 ! [VAR_V_144,VAR_V_145] : % 2.17/2.28 ( pred_attacker(tuple_client_B_out_1(VAR_V_144,VAR_V_145)) % 2.17/2.28 => pred_attacker(VAR_V_144) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax118,axiom, % 2.17/2.28 ! [VAR_V_147,VAR_V_148] : % 2.17/2.28 ( pred_attacker(tuple_client_B_out_1(VAR_V_147,VAR_V_148)) % 2.17/2.28 => pred_attacker(VAR_V_148) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax119,axiom, % 2.17/2.28 ! [VAR_V_151] : % 2.17/2.28 ( pred_attacker(VAR_V_151) % 2.17/2.28 => pred_attacker(tuple_client_B_in_5(VAR_V_151)) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax120,axiom, % 2.17/2.28 ! [VAR_V_154] : % 2.17/2.28 ( pred_attacker(tuple_client_B_in_5(VAR_V_154)) % 2.17/2.28 => pred_attacker(VAR_V_154) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax121,axiom, % 2.17/2.28 ! [VAR_V_157] : % 2.17/2.28 ( pred_attacker(VAR_V_157) % 2.17/2.28 => pred_attacker(tuple_client_B_in_3(VAR_V_157)) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax122,axiom, % 2.17/2.28 ! [VAR_V_160X30] : % 2.17/2.28 ( pred_attacker(tuple_client_B_in_3(VAR_V_160X30)) % 2.17/2.28 => pred_attacker(VAR_V_160X30) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax123,axiom, % 2.17/2.28 ! [VAR_V_163] : % 2.17/2.28 ( pred_attacker(VAR_V_163) % 2.17/2.28 => pred_attacker(tuple_client_B_in_2(VAR_V_163)) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax124,axiom, % 2.17/2.28 ! [VAR_V_166] : % 2.17/2.28 ( pred_attacker(tuple_client_B_in_2(VAR_V_166)) % 2.17/2.28 => pred_attacker(VAR_V_166) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax125,axiom, % 2.17/2.28 ! [VAR_V_169] : % 2.17/2.28 ( pred_attacker(VAR_V_169) % 2.17/2.28 => pred_attacker(tuple_client_A_out_5(VAR_V_169)) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax126,axiom, % 2.17/2.28 ! [VAR_V_172] : % 2.17/2.28 ( pred_attacker(tuple_client_A_out_5(VAR_V_172)) % 2.17/2.28 => pred_attacker(VAR_V_172) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax127,axiom, % 2.17/2.28 ! [VAR_V_175] : % 2.17/2.28 ( pred_attacker(VAR_V_175) % 2.17/2.28 => pred_attacker(tuple_client_A_out_3(VAR_V_175)) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax128,axiom, % 2.17/2.28 ! [VAR_V_178] : % 2.17/2.28 ( pred_attacker(tuple_client_A_out_3(VAR_V_178)) % 2.17/2.28 => pred_attacker(VAR_V_178) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax129,axiom, % 2.17/2.28 ! [VAR_V_182,VAR_V_183] : % 2.17/2.28 ( ( pred_attacker(VAR_V_182) % 2.17/2.28 & pred_attacker(VAR_V_183) ) % 2.17/2.28 => pred_attacker(tuple_client_A_out_1(VAR_V_182,VAR_V_183)) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax130,axiom, % 2.17/2.28 ! [VAR_V_190X30,VAR_V_191] : % 2.17/2.28 ( pred_attacker(tuple_client_A_out_1(VAR_V_190X30,VAR_V_191)) % 2.17/2.28 => pred_attacker(VAR_V_190X30) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax131,axiom, % 2.17/2.28 ! [VAR_V_193,VAR_V_194] : % 2.17/2.28 ( pred_attacker(tuple_client_A_out_1(VAR_V_193,VAR_V_194)) % 2.17/2.28 => pred_attacker(VAR_V_194) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax132,axiom, % 2.17/2.28 ! [VAR_V_197] : % 2.17/2.28 ( pred_attacker(VAR_V_197) % 2.17/2.28 => pred_attacker(tuple_client_A_in_4(VAR_V_197)) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax133,axiom, % 2.17/2.28 ! [VAR_V_20X300X30] : % 2.17/2.28 ( pred_attacker(tuple_client_A_in_4(VAR_V_20X300X30)) % 2.17/2.28 => pred_attacker(VAR_V_20X300X30) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax134,axiom, % 2.17/2.28 ! [VAR_V_20X303] : % 2.17/2.28 ( pred_attacker(VAR_V_20X303) % 2.17/2.28 => pred_attacker(tuple_client_A_in_2(VAR_V_20X303)) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax135,axiom, % 2.17/2.28 ! [VAR_V_20X306] : % 2.17/2.28 ( pred_attacker(tuple_client_A_in_2(VAR_V_20X306)) % 2.17/2.28 => pred_attacker(VAR_V_20X306) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax136,axiom, % 2.17/2.28 ! [VAR_V_210X30,VAR_V_211] : % 2.17/2.28 ( ( pred_attacker(VAR_V_210X30) % 2.17/2.28 & pred_attacker(VAR_V_211) ) % 2.17/2.28 => pred_attacker(constr_checksign(VAR_V_210X30,VAR_V_211)) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax137,axiom, % 2.17/2.28 ! [VAR_V_214,VAR_V_215] : % 2.17/2.28 ( ( pred_attacker(VAR_V_214) % 2.17/2.28 & pred_attacker(VAR_V_215) ) % 2.17/2.28 => pred_attacker(constr_aenc(VAR_V_214,VAR_V_215)) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax138,axiom, % 2.17/2.28 ! [VAR_V_218,VAR_V_219] : % 2.17/2.28 ( ( pred_attacker(VAR_V_218) % 2.17/2.28 & pred_attacker(VAR_V_219) ) % 2.17/2.28 => pred_attacker(constr_adec(VAR_V_218,VAR_V_219)) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax139,axiom, % 2.17/2.28 pred_attacker(constr_CONST_4) ). % 2.17/2.28 % 2.17/2.28 fof(ax140,axiom, % 2.17/2.28 pred_attacker(constr_CONST_3) ). % 2.17/2.28 % 2.17/2.28 fof(ax141,axiom, % 2.17/2.28 pred_attacker(constr_CONST_2) ). % 2.17/2.28 % 2.17/2.28 fof(ax142,axiom, % 2.17/2.28 pred_attacker(constr_CONST_1) ). % 2.17/2.28 % 2.17/2.28 fof(ax143,axiom, % 2.17/2.28 pred_attacker(constr_CONST_0x30) ). % 2.17/2.28 % 2.17/2.28 fof(ax144,axiom, % 2.17/2.28 ! [VAR_V_226,VAR_V_227] : % 2.17/2.28 ( ( pred_attacker(VAR_V_226) % 2.17/2.28 & pred_attacker(VAR_V_227) ) % 2.17/2.28 => pred_attacker(tuple_2(VAR_V_226,VAR_V_227)) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax145,axiom, % 2.17/2.28 ! [VAR_V_234,VAR_V_235] : % 2.17/2.28 ( pred_attacker(tuple_2(VAR_V_234,VAR_V_235)) % 2.17/2.28 => pred_attacker(VAR_V_234) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax146,axiom, % 2.17/2.28 ! [VAR_V_237,VAR_V_238] : % 2.17/2.28 ( pred_attacker(tuple_2(VAR_V_237,VAR_V_238)) % 2.17/2.28 => pred_attacker(VAR_V_238) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax147,axiom, % 2.17/2.28 ! [VAR_V_240X30,VAR_V_241] : % 2.17/2.28 ( ( pred_mess(VAR_V_241,VAR_V_240X30) % 2.17/2.28 & pred_attacker(VAR_V_241) ) % 2.17/2.28 => pred_attacker(VAR_V_240X30) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax148,axiom, % 2.17/2.28 ! [VAR_V_242,VAR_V_243] : % 2.17/2.28 ( ( pred_attacker(VAR_V_243) % 2.17/2.28 & pred_attacker(VAR_V_242) ) % 2.17/2.28 => pred_mess(VAR_V_243,VAR_V_242) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax149,axiom, % 2.17/2.28 pred_attacker(name_c) ). % 2.17/2.28 % 2.17/2.28 fof(ax150,axiom, % 2.17/2.28 pred_attacker(name_I) ). % 2.17/2.28 % 2.17/2.28 fof(ax151,axiom, % 2.17/2.28 pred_attacker(name_B) ). % 2.17/2.28 % 2.17/2.28 fof(ax152,axiom, % 2.17/2.28 pred_attacker(name_A) ). % 2.17/2.28 % 2.17/2.28 fof(ax153,axiom, % 2.17/2.28 ! [VAR_V_245] : pred_equal(VAR_V_245,VAR_V_245) ). % 2.17/2.28 % 2.17/2.28 fof(ax154,axiom, % 2.17/2.28 ! [VAR_V_246] : pred_attacker(name_new0x2Dname(VAR_V_246)) ). % 2.17/2.28 % 2.17/2.28 fof(ax155,axiom, % 2.17/2.28 pred_table(tuple_keys(name_A,constr_pkey(name_skA))) ). % 2.17/2.28 % 2.17/2.28 fof(ax156,axiom, % 2.17/2.28 pred_table(tuple_keys(name_B,constr_pkey(name_skB))) ). % 2.17/2.28 % 2.17/2.28 fof(ax157,axiom, % 2.17/2.28 pred_attacker(tuple_out_1(constr_pkey(name_skA))) ). % 2.17/2.28 % 2.17/2.28 fof(ax158,axiom, % 2.17/2.28 pred_attacker(tuple_out_2(constr_pkey(name_skB))) ). % 2.17/2.28 % 2.17/2.28 fof(ax159,axiom, % 2.17/2.28 pred_attacker(tuple_out_3(constr_pkey(name_skS))) ). % 2.17/2.28 % 2.17/2.28 fof(ax160,axiom, % 2.17/2.28 pred_attacker(tuple_client_A_out_1(name_A,name_I)) ). % 2.17/2.28 % 2.17/2.28 fof(ax161,axiom, % 2.17/2.28 ! [VAR_0X40SID_366,VAR_SIGN_I_PKI_365] : % 2.17/2.28 ( ( pred_eq_bitstring_bitstring(name_I,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_I_PKI_365,constr_pkey(name_skS)))) % 2.17/2.28 & pred_attacker(tuple_client_A_in_2(VAR_SIGN_I_PKI_365)) ) % 2.17/2.28 => pred_attacker(tuple_client_A_out_3(constr_aenc(tuple_2(name_Na(VAR_0X40SID_366),name_A),constr_tuple_2_get_1_bitstring(constr_checksign(VAR_SIGN_I_PKI_365,constr_pkey(name_skS)))))) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax162,axiom, % 2.17/2.28 ! [VAR_0X40SID_414,VAR_AENC_NA_NI_415,VAR_SIGN_I_PKI_416] : % 2.17/2.28 ( ( pred_eq_bitstring_bitstring(name_Na(VAR_0X40SID_414),constr_tuple_2_get_0x30(constr_adec(VAR_AENC_NA_NI_415,name_skA))) % 2.17/2.28 & pred_attacker(tuple_client_A_in_4(VAR_AENC_NA_NI_415)) % 2.17/2.28 & pred_eq_bitstring_bitstring(name_I,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_I_PKI_416,constr_pkey(name_skS)))) % 2.17/2.28 & pred_attacker(tuple_client_A_in_2(VAR_SIGN_I_PKI_416)) ) % 2.17/2.28 => pred_attacker(tuple_client_A_out_5(constr_aenc(constr_tuple_2_get_1_bitstring(constr_adec(VAR_AENC_NA_NI_415,name_skA)),constr_tuple_2_get_1_bitstring(constr_checksign(VAR_SIGN_I_PKI_416,constr_pkey(name_skS)))))) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax163,axiom, % 2.17/2.28 pred_attacker(tuple_client_B_out_1(name_B,name_A)) ). % 2.17/2.28 % 2.17/2.28 fof(ax164,axiom, % 2.17/2.28 ! [VAR_0X40SID_523,VAR_AENC_NA_A_521,VAR_SIGN_A_PKA_522] : % 2.17/2.28 ( ( pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(VAR_AENC_NA_A_521,name_skB))) % 2.17/2.28 & pred_attacker(tuple_client_B_in_3(VAR_AENC_NA_A_521)) % 2.17/2.28 & pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_522,constr_pkey(name_skS)))) % 2.17/2.28 & pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_522)) ) % 2.17/2.28 => pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_tuple_2_get_0x30_bitstring(constr_adec(VAR_AENC_NA_A_521,name_skB)),name_Nb(VAR_0X40SID_523)),constr_tuple_2_get_1_bitstring(constr_checksign(VAR_SIGN_A_PKA_522,constr_pkey(name_skS)))))) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax165,axiom, % 2.17/2.28 ! [VAR_0X40SID_545,VAR_AENC_NA_A_547,VAR_AENC_NB_546,VAR_SIGN_A_PKA_548] : % 2.17/2.28 ( ( pred_eq_bitstring_bitstring(name_Nb(VAR_0X40SID_545),constr_adec(VAR_AENC_NB_546,name_skB)) % 2.17/2.28 & pred_attacker(tuple_client_B_in_5(VAR_AENC_NB_546)) % 2.17/2.28 & pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(VAR_AENC_NA_A_547,name_skB))) % 2.17/2.28 & pred_attacker(tuple_client_B_in_3(VAR_AENC_NA_A_547)) % 2.17/2.28 & pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_548,constr_pkey(name_skS)))) % 2.17/2.28 & pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_548)) ) % 2.17/2.28 => pred_attacker(tuple_client_B_out_6(name_objective)) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax166,axiom, % 2.17/2.28 ! [VAR_DST_587,VAR_PKDST_588,VAR_SRC_589] : % 2.17/2.28 ( ( pred_table(tuple_keys(VAR_DST_587,VAR_PKDST_588)) % 2.17/2.28 & pred_attacker(tuple_key_retrieval_server_in_1(VAR_SRC_589,VAR_DST_587)) ) % 2.17/2.28 => pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(VAR_DST_587,VAR_PKDST_588),name_skS))) ) ). % 2.17/2.28 % 2.17/2.28 fof(ax167,axiom, % 2.17/2.28 ! [VAR_HOST_641,VAR_PK_642] : % 2.17/2.28 ( ( VAR_HOST_641 != name_B % 2.17/2.28 & VAR_HOST_641 != name_A % 2.17/2.28 & pred_attacker(tuple_key_register_server_in_1(VAR_HOST_641,VAR_PK_642)) ) % 2.17/2.28 => pred_table(tuple_keys(VAR_HOST_641,VAR_PK_642)) ) ). % 2.17/2.28 % 2.17/2.28 fof(co0,conjecture, % 2.17/2.28 pred_attacker(name_objective) ). % 2.17/2.28 % 2.17/2.28 %-------------------------------------------------------------------------- % 2.17/2.28 %------------------------------------------- % 2.17/2.28 % Proof found % 2.17/2.28 % SZS status Theorem for theBenchmark % 2.17/2.28 % SZS output start Proof % 2.17/2.28 %ClaNum:223(EqnAxiom:55) % 2.17/2.28 %VarNum:203(SingletonVarNum:111) % 2.17/2.28 %MaxLitNum:4 % 2.17/2.28 %MaxfuncDepth:5 % 2.17/2.28 %SharedTerms:124 % 2.17/2.28 %goalClause: 162 % 2.17/2.28 %singleGoalClaCount:1 % 2.17/2.28 [56]P1(a1) % 2.17/2.28 [57]P1(a2) % 2.17/2.28 [58]P1(a3) % 2.17/2.28 [59]P1(a4) % 2.17/2.28 [60]P1(a5) % 2.17/2.28 [61]P1(a6) % 2.17/2.28 [62]P1(a19) % 2.17/2.28 [63]P1(a20) % 2.17/2.28 [64]P1(a21) % 2.17/2.28 [65]P1(a24) % 2.17/2.28 [66]P1(a25) % 2.17/2.28 [84]~E(a1,a2) % 2.17/2.28 [85]~E(a1,a3) % 2.17/2.28 [86]~E(a3,a2) % 2.17/2.28 [87]~E(a1,a4) % 2.17/2.28 [88]~E(a4,a2) % 2.17/2.28 [89]~E(a4,a3) % 2.17/2.28 [90]~E(a1,a5) % 2.17/2.28 [91]~E(a5,a2) % 2.17/2.28 [92]~E(a5,a3) % 2.17/2.28 [93]~E(a5,a4) % 2.17/2.28 [94]~E(a1,a6) % 2.17/2.28 [95]~E(a6,a2) % 2.17/2.28 [96]~E(a6,a3) % 2.17/2.28 [97]~E(a6,a4) % 2.17/2.28 [98]~E(a6,a5) % 2.17/2.28 [99]~E(a1,a19) % 2.17/2.28 [100]~E(a19,a2) % 2.17/2.28 [101]~E(a19,a3) % 2.17/2.28 [102]~E(a19,a4) % 2.17/2.28 [103]~E(a19,a5) % 2.17/2.28 [104]~E(a19,a6) % 2.17/2.28 [105]~E(a1,a20) % 2.17/2.28 [106]~E(a20,a2) % 2.17/2.28 [107]~E(a20,a3) % 2.17/2.28 [108]~E(a20,a4) % 2.17/2.28 [109]~E(a20,a5) % 2.17/2.28 [110]~E(a20,a6) % 2.17/2.28 [111]~E(a20,a19) % 2.17/2.28 [112]~E(a1,a21) % 2.17/2.28 [113]~E(a21,a2) % 2.17/2.28 [114]~E(a21,a3) % 2.17/2.28 [115]~E(a21,a4) % 2.17/2.28 [116]~E(a21,a5) % 2.17/2.28 [117]~E(a21,a6) % 2.17/2.28 [118]~E(a21,a19) % 2.17/2.28 [119]~E(a21,a20) % 2.17/2.28 [120]~E(a1,a30) % 2.17/2.28 [121]~E(a30,a2) % 2.17/2.28 [122]~E(a30,a3) % 2.17/2.28 [123]~E(a30,a4) % 2.17/2.28 [124]~E(a30,a5) % 2.17/2.28 [125]~E(a30,a6) % 2.17/2.28 [126]~E(a30,a19) % 2.17/2.28 [127]~E(a30,a20) % 2.17/2.28 [128]~E(a30,a21) % 2.17/2.28 [129]~E(a1,a29) % 2.17/2.28 [130]~E(a29,a2) % 2.17/2.28 [131]~E(a29,a3) % 2.17/2.28 [132]~E(a29,a4) % 2.17/2.28 [133]~E(a29,a5) % 2.17/2.28 [134]~E(a29,a6) % 2.17/2.28 [135]~E(a29,a19) % 2.17/2.28 [136]~E(a29,a20) % 2.17/2.28 [137]~E(a29,a21) % 2.17/2.28 [138]~E(a30,a29) % 2.17/2.28 [139]~E(a1,a28) % 2.17/2.28 [140]~E(a28,a2) % 2.17/2.28 [141]~E(a28,a3) % 2.17/2.28 [142]~E(a28,a4) % 2.17/2.28 [143]~E(a28,a5) % 2.17/2.28 [144]~E(a28,a6) % 2.17/2.28 [145]~E(a28,a19) % 2.17/2.28 [146]~E(a28,a20) % 2.17/2.28 [147]~E(a28,a21) % 2.17/2.28 [148]~E(a30,a28) % 2.17/2.28 [149]~E(a29,a28) % 2.17/2.28 [150]~E(a1,a27) % 2.17/2.28 [151]~E(a27,a2) % 2.17/2.28 [152]~E(a27,a3) % 2.17/2.28 [153]~E(a27,a4) % 2.17/2.28 [154]~E(a27,a5) % 2.17/2.28 [155]~E(a27,a6) % 2.17/2.28 [156]~E(a27,a19) % 2.17/2.28 [157]~E(a27,a20) % 2.17/2.28 [158]~E(a27,a21) % 2.17/2.28 [159]~E(a30,a27) % 2.17/2.28 [160]~E(a29,a27) % 2.17/2.28 [161]~E(a28,a27) % 2.17/2.28 [162]~P1(a30) % 2.17/2.28 [72]P1(f31(a19,a6)) % 2.17/2.28 [73]P1(f32(a6,a20)) % 2.17/2.28 [69]P1(f43(f7(a27))) % 2.17/2.28 [70]P1(f44(f7(a28))) % 2.17/2.28 [71]P1(f45(f7(a29))) % 2.17/2.28 [79]P3(f46(a6,f7(a29))) % 2.17/2.28 [80]P3(f46(a19,f7(a28))) % 2.17/2.28 [68]P2(x681,x681) % 2.17/2.28 [67]P1(f26(x671)) % 2.17/2.28 [74]E(f8(f14(x741,x742)),x741) % 2.17/2.28 [75]E(f15(f33(x751,x752)),x752) % 2.17/2.28 [76]E(f16(f33(x761,x762)),x761) % 2.17/2.28 [77]E(f18(f33(x771,x772)),x772) % 2.17/2.28 [78]E(f17(f33(x781,x782)),x781) % 2.17/2.28 [81]E(f10(f9(x811,x812),x812),x811) % 2.17/2.28 [82]E(f11(f14(x821,x822),f7(x822)),x821) % 2.17/2.28 [83]E(f13(f12(x831,f7(x832)),x832),x831) % 2.17/2.28 [163]~P1(x1631)+P1(f7(x1631)) % 2.17/2.28 [164]~P1(x1641)+P1(f8(x1641)) % 2.17/2.28 [165]~P1(x1651)+P1(f15(x1651)) % 2.17/2.28 [166]~P1(x1661)+P1(f16(x1661)) % 2.17/2.28 [167]~P1(x1671)+P1(f18(x1671)) % 2.17/2.28 [168]~P1(x1681)+P1(f17(x1681)) % 2.17/2.28 [169]~P1(x1691)+P1(f43(x1691)) % 2.17/2.28 [170]~P1(x1701)+P1(f44(x1701)) % 2.17/2.28 [171]~P1(x1711)+P1(f45(x1711)) % 2.17/2.28 [172]~P1(x1721)+P1(f47(x1721)) % 2.17/2.28 [173]~P1(x1731)+P1(f41(x1731)) % 2.17/2.28 [174]~P1(x1741)+P1(f42(x1741)) % 2.17/2.28 [175]~P1(x1751)+P1(f36(x1751)) % 2.17/2.28 [176]~P1(x1761)+P1(f37(x1761)) % 2.17/2.28 [177]~P1(x1771)+P1(f38(x1771)) % 2.17/2.28 [178]~P1(x1781)+P1(f39(x1781)) % 2.17/2.28 [179]~P1(x1791)+P1(f40(x1791)) % 2.17/2.28 [180]~P1(x1801)+P1(f34(x1801)) % 2.17/2.28 [181]~P1(x1811)+P1(f35(x1811)) % 2.17/2.28 [182]P1(x1821)+~P1(f43(x1821)) % 2.17/2.28 [183]P1(x1831)+~P1(f44(x1831)) % 2.17/2.28 [184]P1(x1841)+~P1(f45(x1841)) % 2.17/2.28 [185]P1(x1851)+~P1(f47(x1851)) % 2.17/2.28 [186]P1(x1861)+~P1(f41(x1861)) % 2.17/2.28 [187]P1(x1871)+~P1(f42(x1871)) % 2.17/2.28 [188]P1(x1881)+~P1(f36(x1881)) % 2.17/2.28 [189]P1(x1891)+~P1(f37(x1891)) % 2.17/2.28 [190]P1(x1901)+~P1(f38(x1901)) % 2.17/2.28 [191]P1(x1911)+~P1(f39(x1911)) % 2.17/2.28 [192]P1(x1921)+~P1(f40(x1921)) % 2.17/2.28 [193]P1(x1931)+~P1(f34(x1931)) % 2.17/2.28 [194]P1(x1941)+~P1(f35(x1941)) % 2.17/2.28 [208]P1(x2081)+~P1(f33(x2082,x2081)) % 2.17/2.28 [209]P1(x2091)+~P1(f48(x2092,x2091)) % 2.17/2.28 [210]P1(x2101)+~P1(f49(x2102,x2101)) % 2.17/2.28 [211]P1(x2111)+~P1(f31(x2112,x2111)) % 2.17/2.28 [212]P1(x2121)+~P1(f32(x2122,x2121)) % 2.17/2.28 [213]P1(x2131)+~P1(f33(x2131,x2132)) % 2.17/2.28 [214]P1(x2141)+~P1(f48(x2141,x2142)) % 2.17/2.28 [215]P1(x2151)+~P1(f49(x2151,x2152)) % 2.17/2.28 [216]P1(x2161)+~P1(f31(x2161,x2162)) % 2.17/2.28 [217]P1(x2171)+~P1(f32(x2171,x2172)) % 2.17/2.28 [221]~P1(f35(x2212))+P1(f40(f12(f33(f22(x2211),a6),f15(f11(x2212,f7(a27)))))) % 2.17/2.28 [195]~P1(x1952)+~P1(x1951)+P4(x1951,x1952) % 2.17/2.28 [196]~P4(x1962,x1961)+P1(x1961)+~P1(x1962) % 2.17/2.28 [197]~P1(x1972)+~P1(x1971)+P1(f12(x1971,x1972)) % 2.17/2.28 [198]~P1(x1982)+~P1(x1981)+P1(f13(x1981,x1982)) % 2.17/2.28 [199]~P1(x1992)+~P1(x1991)+P1(f9(x1991,x1992)) % 2.17/2.28 [200]~P1(x2002)+~P1(x2001)+P1(f10(x2001,x2002)) % 2.17/2.28 [201]~P1(x2012)+~P1(x2011)+P1(f14(x2011,x2012)) % 2.17/2.28 [202]~P1(x2022)+~P1(x2021)+P1(f11(x2021,x2022)) % 2.17/2.28 [203]~P1(x2032)+~P1(x2031)+P1(f33(x2031,x2032)) % 2.17/2.28 [204]~P1(x2042)+~P1(x2041)+P1(f48(x2041,x2042)) % 2.17/2.28 [205]~P1(x2052)+~P1(x2051)+P1(f49(x2051,x2052)) % 2.17/2.28 [206]~P1(x2062)+~P1(x2061)+P1(f31(x2061,x2062)) % 2.17/2.28 [207]~P1(x2072)+~P1(x2071)+P1(f32(x2071,x2072)) % 2.17/2.28 [222]~P1(f34(x2221))+~P1(f35(x2222))+P1(f39(f12(f15(f13(x2221,a29)),f15(f11(x2222,f7(a27)))))) % 2.17/2.28 [220]~P3(f46(x2201,x2202))+~P1(f48(x2203,x2201))+P1(f47(f14(f33(x2201,x2202),a27))) % 2.17/2.28 [223]~P1(f37(x2231))+~P1(f38(x2233))+P1(f42(f12(f33(f16(f13(x2231,a28)),f23(x2232)),f15(f11(x2233,f7(a27)))))) % 2.17/2.28 [219]E(x2191,a19)+E(x2191,a6)+~P1(f49(x2191,x2192))+P3(f46(x2191,x2192)) % 2.17/2.28 [218]~P1(f36(x2181))+~P1(f37(x2182))+~P1(f38(x2183))+P1(f41(a30)) % 2.17/2.28 %EqnAxiom % 2.17/2.28 [1]E(x11,x11) % 2.17/2.28 [2]E(x22,x21)+~E(x21,x22) % 2.17/2.28 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 2.17/2.28 [4]~E(x41,x42)+E(f26(x41),f26(x42)) % 2.17/2.28 [5]~E(x51,x52)+E(f7(x51),f7(x52)) % 2.17/2.28 [6]~E(x61,x62)+E(f43(x61),f43(x62)) % 2.17/2.28 [7]~E(x71,x72)+E(f38(x71),f38(x72)) % 2.17/2.28 [8]~E(x81,x82)+E(f44(x81),f44(x82)) % 2.17/2.28 [9]~E(x91,x92)+E(f37(x91),f37(x92)) % 2.17/2.28 [10]~E(x101,x102)+E(f45(x101),f45(x102)) % 2.17/2.28 [11]~E(x111,x112)+E(f31(x111,x113),f31(x112,x113)) % 2.17/2.28 [12]~E(x121,x122)+E(f31(x123,x121),f31(x123,x122)) % 2.17/2.28 [13]~E(x131,x132)+E(f32(x131,x133),f32(x132,x133)) % 2.17/2.28 [14]~E(x141,x142)+E(f32(x143,x141),f32(x143,x142)) % 2.17/2.28 [15]~E(x151,x152)+E(f14(x151,x153),f14(x152,x153)) % 2.17/2.28 [16]~E(x161,x162)+E(f14(x163,x161),f14(x163,x162)) % 2.17/2.28 [17]~E(x171,x172)+E(f8(x171),f8(x172)) % 2.17/2.29 [18]~E(x181,x182)+E(f33(x181,x183),f33(x182,x183)) % 2.17/2.29 [19]~E(x191,x192)+E(f33(x193,x191),f33(x193,x192)) % 2.17/2.29 [20]~E(x201,x202)+E(f15(x201),f15(x202)) % 2.17/2.29 [21]~E(x211,x212)+E(f49(x211,x213),f49(x212,x213)) % 2.17/2.29 [22]~E(x221,x222)+E(f49(x223,x221),f49(x223,x222)) % 2.17/2.29 [23]~E(x231,x232)+E(f16(x231),f16(x232)) % 2.17/2.29 [24]~E(x241,x242)+E(f46(x241,x243),f46(x242,x243)) % 2.17/2.29 [25]~E(x251,x252)+E(f46(x253,x251),f46(x253,x252)) % 2.17/2.29 [26]~E(x261,x262)+E(f18(x261),f18(x262)) % 2.17/2.29 [27]~E(x271,x272)+E(f12(x271,x273),f12(x272,x273)) % 2.17/2.29 [28]~E(x281,x282)+E(f12(x283,x281),f12(x283,x282)) % 2.17/2.29 [29]~E(x291,x292)+E(f17(x291),f17(x292)) % 2.17/2.29 [30]~E(x301,x302)+E(f42(x301),f42(x302)) % 2.17/2.29 [31]~E(x311,x312)+E(f41(x311),f41(x312)) % 2.17/2.29 [32]~E(x321,x322)+E(f48(x321,x323),f48(x322,x323)) % 2.17/2.29 [33]~E(x331,x332)+E(f48(x333,x331),f48(x333,x332)) % 2.17/2.29 [34]~E(x341,x342)+E(f39(x341),f39(x342)) % 2.17/2.29 [35]~E(x351,x352)+E(f9(x351,x353),f9(x352,x353)) % 2.17/2.29 [36]~E(x361,x362)+E(f9(x363,x361),f9(x363,x362)) % 2.17/2.29 [37]~E(x371,x372)+E(f10(x371,x373),f10(x372,x373)) % 2.17/2.29 [38]~E(x381,x382)+E(f10(x383,x381),f10(x383,x382)) % 2.17/2.29 [39]~E(x391,x392)+E(f36(x391),f36(x392)) % 2.17/2.29 [40]~E(x401,x402)+E(f22(x401),f22(x402)) % 2.17/2.29 [41]~E(x411,x412)+E(f11(x411,x413),f11(x412,x413)) % 2.17/2.29 [42]~E(x421,x422)+E(f11(x423,x421),f11(x423,x422)) % 2.17/2.29 [43]~E(x431,x432)+E(f35(x431),f35(x432)) % 2.17/2.29 [44]~E(x441,x442)+E(f40(x441),f40(x442)) % 2.17/2.29 [45]~E(x451,x452)+E(f13(x451,x453),f13(x452,x453)) % 2.17/2.29 [46]~E(x461,x462)+E(f13(x463,x461),f13(x463,x462)) % 2.17/2.29 [47]~E(x471,x472)+E(f47(x471),f47(x472)) % 2.17/2.29 [48]~E(x481,x482)+E(f34(x481),f34(x482)) % 2.17/2.29 [49]~E(x491,x492)+E(f23(x491),f23(x492)) % 2.17/2.29 [50]~P1(x501)+P1(x502)+~E(x501,x502) % 2.17/2.29 [51]~P3(x511)+P3(x512)+~E(x511,x512) % 2.17/2.29 [52]P2(x522,x523)+~E(x521,x522)+~P2(x521,x523) % 2.17/2.29 [53]P2(x533,x532)+~E(x531,x532)+~P2(x533,x531) % 2.17/2.29 [54]P4(x542,x543)+~E(x541,x542)+~P4(x541,x543) % 2.17/2.29 [55]P4(x553,x552)+~E(x551,x552)+~P4(x553,x551) % 2.17/2.29 % 2.17/2.29 %------------------------------------------- % 2.17/2.29 cnf(698,plain, % 2.17/2.29 (P1(f36(f37(a1)))), % 2.17/2.29 inference(scs_inference,[],[56,175,176])). % 2.17/2.29 cnf(699,plain, % 2.17/2.29 (~P1(f37(x6991))+~P1(f38(x6992))+P1(f41(a30))), % 2.17/2.29 inference(scs_inference,[],[698,218])). % 2.17/2.29 cnf(700,plain, % 2.17/2.29 (P1(f37(a1))), % 2.17/2.29 inference(scs_inference,[],[698,188])). % 2.17/2.29 cnf(706,plain, % 2.17/2.29 (P1(f38(f39(a1)))), % 2.17/2.29 inference(scs_inference,[],[56,177,178])). % 2.17/2.29 cnf(707,plain, % 2.17/2.29 (P1(f41(a30))), % 2.17/2.29 inference(scs_inference,[],[700,706,699])). % 2.17/2.29 cnf(714,plain, % 2.17/2.29 (P1(f40(f34(a1)))), % 2.17/2.29 inference(scs_inference,[],[56,179,180])). % 2.17/2.29 cnf(717,plain, % 2.17/2.29 ($false), % 2.17/2.29 inference(scs_inference,[],[162,714,707,192,186]), % 2.17/2.29 ['proof']). % 2.17/2.29 % SZS output end Proof % 2.17/2.29 % Total time :1.670000s %------------------------------------------------------------------------------