%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWW965+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 : n024.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 4.79s 4.80s % Output : CNFRefutation 4.79s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : SWW965+1 : TPTP v8.2.0. Released v7.4.0. % 0.04/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.35 % Computer : n024.cluster.edu % 0.12/0.35 % Model : x86_64 x86_64 % 0.12/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.35 % Memory : 8042.1875MB % 0.12/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.35 % CPULimit : 300 % 0.12/0.35 % WCLimit : 300 % 0.12/0.35 % DateTime : Wed Jun 19 09:38:09 EDT 2024 % 0.20/0.35 % CPUTime : % 0.56/0.58 start to proof:theBenchmark % 4.69/4.78 %------------------------------------------- % 4.69/4.78 % File :CSE---1.7 % 4.69/4.78 % Problem :theBenchmark % 4.69/4.78 % Transform :cnf % 4.69/4.78 % Format :tptp:raw % 4.69/4.78 % Command :java -jar mcs_scs.jar %d %s % 4.69/4.78 % 4.69/4.78 % Result :Theorem 4.130000s % 4.69/4.78 % Output :CNFRefutation 4.130000s % 4.69/4.78 %------------------------------------------- % 4.69/4.78 %-------------------------------------------------------------------------- % 4.69/4.78 % File : SWW965+1 : TPTP v8.2.0. Released v7.4.0. % 4.69/4.78 % Domain : Software Verification % 4.69/4.78 % Problem : Attack on a variant of Needham-Schroeder-Lowe Public Key Protocol % 4.69/4.78 % Version : [LT19] axioms : Especial. % 4.69/4.78 % English : Uses XOR. Attack demonstrates an impersonation attack % 4.69/4.78 % 4.69/4.78 % Refs : [BO97] Bull & Otway (1997), The Authentication Protocol % 4.69/4.78 % : [RS98] Ryan & Schneider (1998), An Attack on a Recursive Auth % 4.69/4.78 % : [LT19] Li & Tiu (2019), Combining ProVerif and Automated Theo % 4.69/4.78 % : [Li20] Li (2020), Email to Geoff Sutcliffe % 4.69/4.78 % Source : [Li20] % 4.69/4.78 % Names : NSLPK-XOR-agree-A-to-B.p [LT20] % 4.69/4.78 % 4.69/4.78 % Status : Theorem % 4.69/4.78 % Rating : 0.39 v8.2.0, 0.36 v8.1.0, 0.33 v7.5.0, 0.38 v7.4.0 % 4.69/4.78 % Syntax : Number of formulae : 188 ( 126 unt; 0 def) % 4.69/4.78 % Number of atoms : 279 ( 105 equ) % 4.69/4.78 % Maximal formula atoms : 7 ( 1 avg) % 4.69/4.78 % Number of connectives : 184 ( 93 ~; 0 |; 29 &) % 4.69/4.78 % ( 0 <=>; 62 =>; 0 <=; 0 <~>) % 4.69/4.78 % Maximal formula depth : 11 ( 3 avg) % 4.69/4.78 % Maximal term depth : 7 ( 1 avg) % 4.69/4.78 % Number of predicates : 6 ( 5 usr; 0 prp; 1-2 aty) % 4.69/4.78 % Number of functors : 51 ( 51 usr; 16 con; 0-2 aty) % 4.69/4.78 % Number of variables : 124 ( 124 !; 0 ?) % 4.69/4.78 % SPC : FOF_THM_RFO_SEQ % 4.69/4.78 % 4.69/4.78 % Comments : Generated by a modified version of ProVerif used in the % 4.69/4.78 % ProVerif-ATP project [LT19]. % 4.69/4.78 %-------------------------------------------------------------------------- % 4.69/4.78 fof(ax0,axiom, % 4.69/4.78 constr_CONST_0x30 != constr_CONST_1 ). % 4.69/4.78 % 4.69/4.78 fof(ax1,axiom, % 4.69/4.78 constr_CONST_0x30 != constr_CONST_2 ). % 4.69/4.78 % 4.69/4.78 fof(ax2,axiom, % 4.69/4.78 constr_CONST_0x30 != constr_CONST_3 ). % 4.69/4.78 % 4.69/4.78 fof(ax3,axiom, % 4.69/4.78 constr_CONST_0x30 != constr_CONST_4 ). % 4.69/4.78 % 4.69/4.78 fof(ax4,axiom, % 4.69/4.78 constr_CONST_0x30 != constr_ZERO ). % 4.69/4.78 % 4.69/4.78 fof(ax5,axiom, % 4.69/4.78 constr_CONST_0x30 != name_A ). % 4.69/4.78 % 4.69/4.78 fof(ax6,axiom, % 4.69/4.78 constr_CONST_0x30 != name_B ). % 4.69/4.78 % 4.69/4.78 fof(ax7,axiom, % 4.69/4.78 constr_CONST_0x30 != name_I ). % 4.69/4.78 % 4.69/4.78 fof(ax8,axiom, % 4.69/4.78 constr_CONST_0x30 != name_c ). % 4.69/4.78 % 4.69/4.78 fof(ax9,axiom, % 4.69/4.78 constr_CONST_0x30 != name_objective ). % 4.69/4.78 % 4.69/4.78 fof(ax10,axiom, % 4.69/4.78 constr_CONST_0x30 != name_skA ). % 4.69/4.78 % 4.69/4.78 fof(ax11,axiom, % 4.69/4.78 constr_CONST_0x30 != name_skB ). % 4.69/4.78 % 4.69/4.78 fof(ax12,axiom, % 4.69/4.78 constr_CONST_0x30 != name_skS ). % 4.69/4.79 % 4.69/4.79 fof(ax13,axiom, % 4.69/4.79 constr_CONST_1 != constr_CONST_2 ). % 4.69/4.79 % 4.69/4.79 fof(ax14,axiom, % 4.69/4.79 constr_CONST_1 != constr_CONST_3 ). % 4.69/4.79 % 4.69/4.79 fof(ax15,axiom, % 4.69/4.79 constr_CONST_1 != constr_CONST_4 ). % 4.69/4.79 % 4.69/4.79 fof(ax16,axiom, % 4.69/4.79 constr_CONST_1 != constr_ZERO ). % 4.69/4.79 % 4.69/4.79 fof(ax17,axiom, % 4.69/4.79 constr_CONST_1 != name_A ). % 4.69/4.79 % 4.69/4.79 fof(ax18,axiom, % 4.69/4.79 constr_CONST_1 != name_B ). % 4.69/4.79 % 4.69/4.79 fof(ax19,axiom, % 4.69/4.79 constr_CONST_1 != name_I ). % 4.69/4.79 % 4.69/4.79 fof(ax20,axiom, % 4.69/4.79 constr_CONST_1 != name_c ). % 4.69/4.79 % 4.69/4.79 fof(ax21,axiom, % 4.69/4.79 constr_CONST_1 != name_objective ). % 4.69/4.79 % 4.69/4.79 fof(ax22,axiom, % 4.69/4.79 constr_CONST_1 != name_skA ). % 4.69/4.79 % 4.69/4.79 fof(ax23,axiom, % 4.69/4.79 constr_CONST_1 != name_skB ). % 4.69/4.79 % 4.69/4.79 fof(ax24,axiom, % 4.69/4.79 constr_CONST_1 != name_skS ). % 4.69/4.79 % 4.69/4.79 fof(ax25,axiom, % 4.69/4.79 constr_CONST_2 != constr_CONST_3 ). % 4.69/4.79 % 4.69/4.79 fof(ax26,axiom, % 4.69/4.79 constr_CONST_2 != constr_CONST_4 ). % 4.69/4.79 % 4.69/4.79 fof(ax27,axiom, % 4.69/4.79 constr_CONST_2 != constr_ZERO ). % 4.69/4.79 % 4.69/4.79 fof(ax28,axiom, % 4.69/4.79 constr_CONST_2 != name_A ). % 4.69/4.79 % 4.69/4.79 fof(ax29,axiom, % 4.69/4.79 constr_CONST_2 != name_B ). % 4.69/4.79 % 4.69/4.79 fof(ax30,axiom, % 4.69/4.79 constr_CONST_2 != name_I ). % 4.69/4.79 % 4.69/4.79 fof(ax31,axiom, % 4.69/4.79 constr_CONST_2 != name_c ). % 4.69/4.79 % 4.69/4.79 fof(ax32,axiom, % 4.69/4.79 constr_CONST_2 != name_objective ). % 4.69/4.79 % 4.69/4.79 fof(ax33,axiom, % 4.69/4.79 constr_CONST_2 != name_skA ). % 4.69/4.79 % 4.69/4.79 fof(ax34,axiom, % 4.69/4.79 constr_CONST_2 != name_skB ). % 4.69/4.79 % 4.69/4.79 fof(ax35,axiom, % 4.69/4.79 constr_CONST_2 != name_skS ). % 4.69/4.79 % 4.69/4.79 fof(ax36,axiom, % 4.69/4.79 constr_CONST_3 != constr_CONST_4 ). % 4.69/4.79 % 4.69/4.79 fof(ax37,axiom, % 4.69/4.79 constr_CONST_3 != constr_ZERO ). % 4.69/4.79 % 4.69/4.79 fof(ax38,axiom, % 4.69/4.79 constr_CONST_3 != name_A ). % 4.69/4.79 % 4.69/4.79 fof(ax39,axiom, % 4.69/4.79 constr_CONST_3 != name_B ). % 4.69/4.79 % 4.69/4.79 fof(ax40,axiom, % 4.69/4.79 constr_CONST_3 != name_I ). % 4.69/4.79 % 4.69/4.79 fof(ax41,axiom, % 4.69/4.79 constr_CONST_3 != name_c ). % 4.69/4.79 % 4.69/4.79 fof(ax42,axiom, % 4.69/4.79 constr_CONST_3 != name_objective ). % 4.69/4.79 % 4.69/4.79 fof(ax43,axiom, % 4.69/4.79 constr_CONST_3 != name_skA ). % 4.69/4.79 % 4.69/4.79 fof(ax44,axiom, % 4.69/4.79 constr_CONST_3 != name_skB ). % 4.69/4.79 % 4.69/4.79 fof(ax45,axiom, % 4.69/4.79 constr_CONST_3 != name_skS ). % 4.69/4.79 % 4.69/4.79 fof(ax46,axiom, % 4.69/4.79 constr_CONST_4 != constr_ZERO ). % 4.69/4.79 % 4.69/4.79 fof(ax47,axiom, % 4.69/4.79 constr_CONST_4 != name_A ). % 4.69/4.79 % 4.69/4.79 fof(ax48,axiom, % 4.69/4.79 constr_CONST_4 != name_B ). % 4.69/4.79 % 4.69/4.79 fof(ax49,axiom, % 4.69/4.79 constr_CONST_4 != name_I ). % 4.69/4.79 % 4.69/4.79 fof(ax50,axiom, % 4.69/4.79 constr_CONST_4 != name_c ). % 4.69/4.79 % 4.69/4.79 fof(ax51,axiom, % 4.69/4.79 constr_CONST_4 != name_objective ). % 4.69/4.79 % 4.69/4.79 fof(ax52,axiom, % 4.69/4.79 constr_CONST_4 != name_skA ). % 4.69/4.79 % 4.69/4.79 fof(ax53,axiom, % 4.69/4.79 constr_CONST_4 != name_skB ). % 4.69/4.79 % 4.69/4.79 fof(ax54,axiom, % 4.69/4.79 constr_CONST_4 != name_skS ). % 4.69/4.79 % 4.69/4.79 fof(ax55,axiom, % 4.69/4.79 constr_ZERO != name_A ). % 4.69/4.79 % 4.69/4.79 fof(ax56,axiom, % 4.69/4.79 constr_ZERO != name_B ). % 4.69/4.79 % 4.69/4.79 fof(ax57,axiom, % 4.69/4.79 constr_ZERO != name_I ). % 4.69/4.79 % 4.69/4.79 fof(ax58,axiom, % 4.69/4.79 constr_ZERO != name_c ). % 4.69/4.79 % 4.69/4.79 fof(ax59,axiom, % 4.69/4.79 constr_ZERO != name_objective ). % 4.69/4.79 % 4.69/4.79 fof(ax60,axiom, % 4.69/4.79 constr_ZERO != name_skA ). % 4.69/4.79 % 4.69/4.79 fof(ax61,axiom, % 4.69/4.79 constr_ZERO != name_skB ). % 4.69/4.79 % 4.69/4.79 fof(ax62,axiom, % 4.69/4.79 constr_ZERO != name_skS ). % 4.69/4.79 % 4.69/4.79 fof(ax63,axiom, % 4.69/4.79 name_A != name_B ). % 4.69/4.79 % 4.69/4.79 fof(ax64,axiom, % 4.69/4.79 name_A != name_I ). % 4.69/4.79 % 4.69/4.79 fof(ax65,axiom, % 4.69/4.79 name_A != name_c ). % 4.69/4.79 % 4.69/4.79 fof(ax66,axiom, % 4.69/4.79 name_A != name_objective ). % 4.69/4.79 % 4.69/4.79 fof(ax67,axiom, % 4.69/4.79 name_A != name_skA ). % 4.69/4.79 % 4.69/4.79 fof(ax68,axiom, % 4.69/4.79 name_A != name_skB ). % 4.69/4.79 % 4.69/4.79 fof(ax69,axiom, % 4.69/4.79 name_A != name_skS ). % 4.69/4.79 % 4.69/4.79 fof(ax70,axiom, % 4.69/4.79 name_B != name_I ). % 4.69/4.79 % 4.69/4.79 fof(ax71,axiom, % 4.69/4.79 name_B != name_c ). % 4.69/4.79 % 4.69/4.79 fof(ax72,axiom, % 4.69/4.79 name_B != name_objective ). % 4.69/4.79 % 4.69/4.79 fof(ax73,axiom, % 4.69/4.79 name_B != name_skA ). % 4.69/4.79 % 4.69/4.79 fof(ax74,axiom, % 4.69/4.79 name_B != name_skB ). % 4.69/4.79 % 4.69/4.79 fof(ax75,axiom, % 4.69/4.79 name_B != name_skS ). % 4.69/4.79 % 4.69/4.79 fof(ax76,axiom, % 4.69/4.79 name_I != name_c ). % 4.69/4.79 % 4.69/4.79 fof(ax77,axiom, % 4.69/4.79 name_I != name_objective ). % 4.69/4.79 % 4.69/4.79 fof(ax78,axiom, % 4.69/4.79 name_I != name_skA ). % 4.69/4.79 % 4.69/4.79 fof(ax79,axiom, % 4.69/4.79 name_I != name_skB ). % 4.69/4.79 % 4.69/4.79 fof(ax80,axiom, % 4.69/4.79 name_I != name_skS ). % 4.69/4.79 % 4.69/4.79 fof(ax81,axiom, % 4.69/4.79 name_c != name_objective ). % 4.69/4.79 % 4.69/4.79 fof(ax82,axiom, % 4.69/4.79 name_c != name_skA ). % 4.69/4.79 % 4.69/4.79 fof(ax83,axiom, % 4.69/4.79 name_c != name_skB ). % 4.69/4.79 % 4.69/4.79 fof(ax84,axiom, % 4.69/4.79 name_c != name_skS ). % 4.69/4.79 % 4.69/4.79 fof(ax85,axiom, % 4.69/4.79 name_objective != name_skA ). % 4.69/4.79 % 4.69/4.79 fof(ax86,axiom, % 4.69/4.79 name_objective != name_skB ). % 4.69/4.79 % 4.69/4.79 fof(ax87,axiom, % 4.69/4.79 name_objective != name_skS ). % 4.69/4.79 % 4.69/4.79 fof(ax88,axiom, % 4.69/4.79 name_skA != name_skB ). % 4.69/4.79 % 4.69/4.79 fof(ax89,axiom, % 4.69/4.79 name_skA != name_skS ). % 4.69/4.79 % 4.69/4.79 fof(ax90,axiom, % 4.69/4.79 name_skB != name_skS ). % 4.69/4.79 % 4.69/4.79 fof(ax91,axiom, % 4.69/4.79 ! [VAR_K_24,VAR_M_23] : constr_adec(constr_aenc(VAR_M_23,constr_pkey(VAR_K_24)),VAR_K_24) = VAR_M_23 ). % 4.69/4.79 % 4.69/4.79 fof(ax92,axiom, % 4.69/4.79 ! [VAR_K_22,VAR_M_21] : constr_dec(constr_enc(VAR_M_21,VAR_K_22),VAR_K_22) = VAR_M_21 ). % 4.69/4.79 % 4.69/4.79 fof(ax93,axiom, % 4.69/4.79 ! [VAR_K_20X30,VAR_M_19] : constr_getmess(constr_sign(VAR_M_19,VAR_K_20X30)) = VAR_M_19 ). % 4.69/4.79 % 4.69/4.79 fof(ax94,axiom, % 4.69/4.79 ! [VAR_K_0X30,VAR_M_0X30] : constr_checksign(constr_sign(VAR_M_0X30,VAR_K_0X30),constr_pkey(VAR_K_0X30)) = VAR_M_0X30 ). % 4.69/4.79 % 4.69/4.79 fof(ax95,axiom, % 4.69/4.79 ! [VAR_X_18] : constr_xor(VAR_X_18,VAR_X_18) = constr_ZERO ). % 4.69/4.79 % 4.69/4.79 fof(ax96,axiom, % 4.69/4.79 ! [VAR_X_17] : constr_xor(VAR_X_17,constr_ZERO) = VAR_X_17 ). % 4.69/4.79 % 4.69/4.79 fof(ax97,axiom, % 4.69/4.79 ! [VAR_X_15,VAR_Y_16] : constr_xor(VAR_X_15,VAR_Y_16) = constr_xor(VAR_Y_16,VAR_X_15) ). % 4.69/4.79 % 4.69/4.79 fof(ax98,axiom, % 4.69/4.79 ! [VAR_X_13,VAR_Y_14,VAR_Z_0X30] : constr_xor(VAR_X_13,constr_xor(VAR_Y_14,VAR_Z_0X30)) = constr_xor(constr_xor(VAR_X_13,VAR_Y_14),VAR_Z_0X30) ). % 4.69/4.79 % 4.69/4.79 fof(ax99,axiom, % 4.69/4.79 ! [VAR_X0X30_11,VAR_X1_12] : constr_tuple_2_get_1_bitstring(tuple_2(VAR_X0X30_11,VAR_X1_12)) = VAR_X1_12 ). % 4.69/4.79 % 4.69/4.79 fof(ax100,axiom, % 4.69/4.79 ! [VAR_X0X30_9,VAR_X1_10X30] : constr_tuple_2_get_0x30_bitstring(tuple_2(VAR_X0X30_9,VAR_X1_10X30)) = VAR_X0X30_9 ). % 4.69/4.79 % 4.69/4.79 fof(ax101,axiom, % 4.69/4.79 ! [VAR_X0X30_7,VAR_X1_8] : constr_tuple_2_get_1(tuple_2(VAR_X0X30_7,VAR_X1_8)) = VAR_X1_8 ). % 4.69/4.79 % 4.69/4.79 fof(ax102,axiom, % 4.69/4.79 ! [VAR_X0X30_0X30,VAR_X1_0X30] : constr_tuple_2_get_0x30(tuple_2(VAR_X0X30_0X30,VAR_X1_0X30)) = VAR_X0X30_0X30 ). % 4.69/4.79 % 4.69/4.79 fof(ax103,axiom, % 4.69/4.79 ! [VAR_X_41,VAR_Y_42] : pred_eq_bitstring_bitstring(VAR_X_41,VAR_Y_42) ). % 4.69/4.79 % 4.69/4.79 fof(ax104,axiom, % 4.69/4.79 ! [VAR_V_49,VAR_V_50X30] : % 4.69/4.79 ( ( pred_attacker(VAR_V_49) % 4.69/4.79 & pred_attacker(VAR_V_50X30) ) % 4.69/4.79 => pred_attacker(constr_xor(VAR_V_49,VAR_V_50X30)) ) ). % 4.69/4.79 % 4.69/4.79 fof(ax105,axiom, % 4.69/4.79 ! [VAR_V_52] : % 4.69/4.79 ( pred_attacker(VAR_V_52) % 4.69/4.79 => pred_attacker(constr_tuple_2_get_1_bitstring(VAR_V_52)) ) ). % 4.69/4.79 % 4.69/4.79 fof(ax106,axiom, % 4.69/4.79 ! [VAR_V_54] : % 4.69/4.79 ( pred_attacker(VAR_V_54) % 4.69/4.79 => pred_attacker(constr_tuple_2_get_1(VAR_V_54)) ) ). % 4.69/4.79 % 4.69/4.79 fof(ax107,axiom, % 4.69/4.79 ! [VAR_V_56] : % 4.79/4.80 ( pred_attacker(VAR_V_56) % 4.79/4.80 => pred_attacker(constr_tuple_2_get_0x30_bitstring(VAR_V_56)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax108,axiom, % 4.79/4.80 ! [VAR_V_58] : % 4.79/4.80 ( pred_attacker(VAR_V_58) % 4.79/4.80 => pred_attacker(constr_tuple_2_get_0x30(VAR_V_58)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax109,axiom, % 4.79/4.80 pred_attacker(tuple_true) ). % 4.79/4.80 % 4.79/4.80 fof(ax110,axiom, % 4.79/4.80 ! [VAR_V_61,VAR_V_62] : % 4.79/4.80 ( ( pred_attacker(VAR_V_61) % 4.79/4.80 & pred_attacker(VAR_V_62) ) % 4.79/4.80 => pred_attacker(constr_sign(VAR_V_61,VAR_V_62)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax111,axiom, % 4.79/4.80 ! [VAR_V_64] : % 4.79/4.80 ( pred_attacker(VAR_V_64) % 4.79/4.80 => pred_attacker(constr_pkey(VAR_V_64)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax112,axiom, % 4.79/4.80 ! [VAR_V_66] : % 4.79/4.80 ( pred_attacker(VAR_V_66) % 4.79/4.80 => pred_attacker(tuple_out_3(VAR_V_66)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax113,axiom, % 4.79/4.80 ! [VAR_V_69] : % 4.79/4.80 ( pred_attacker(tuple_out_3(VAR_V_69)) % 4.79/4.80 => pred_attacker(VAR_V_69) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax114,axiom, % 4.79/4.80 ! [VAR_V_72] : % 4.79/4.80 ( pred_attacker(VAR_V_72) % 4.79/4.80 => pred_attacker(tuple_out_2(VAR_V_72)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax115,axiom, % 4.79/4.80 ! [VAR_V_75] : % 4.79/4.80 ( pred_attacker(tuple_out_2(VAR_V_75)) % 4.79/4.80 => pred_attacker(VAR_V_75) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax116,axiom, % 4.79/4.80 ! [VAR_V_78] : % 4.79/4.80 ( pred_attacker(VAR_V_78) % 4.79/4.80 => pred_attacker(tuple_out_1(VAR_V_78)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax117,axiom, % 4.79/4.80 ! [VAR_V_81] : % 4.79/4.80 ( pred_attacker(tuple_out_1(VAR_V_81)) % 4.79/4.80 => pred_attacker(VAR_V_81) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax118,axiom, % 4.79/4.80 ! [VAR_V_85] : % 4.79/4.80 ( pred_attacker(VAR_V_85) % 4.79/4.80 => pred_attacker(tuple_key_retrieval_server_out_2(VAR_V_85)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax119,axiom, % 4.79/4.80 ! [VAR_V_88] : % 4.79/4.80 ( pred_attacker(tuple_key_retrieval_server_out_2(VAR_V_88)) % 4.79/4.80 => pred_attacker(VAR_V_88) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax120,axiom, % 4.79/4.80 ! [VAR_V_92,VAR_V_93] : % 4.79/4.80 ( ( pred_attacker(VAR_V_92) % 4.79/4.80 & pred_attacker(VAR_V_93) ) % 4.79/4.80 => pred_attacker(tuple_key_retrieval_server_in_1(VAR_V_92,VAR_V_93)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax121,axiom, % 4.79/4.80 ! [VAR_V_10X300X30,VAR_V_10X301] : % 4.79/4.80 ( pred_attacker(tuple_key_retrieval_server_in_1(VAR_V_10X300X30,VAR_V_10X301)) % 4.79/4.80 => pred_attacker(VAR_V_10X300X30) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax122,axiom, % 4.79/4.80 ! [VAR_V_10X303,VAR_V_10X304] : % 4.79/4.80 ( pred_attacker(tuple_key_retrieval_server_in_1(VAR_V_10X303,VAR_V_10X304)) % 4.79/4.80 => pred_attacker(VAR_V_10X304) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax123,axiom, % 4.79/4.80 ! [VAR_V_10X308,VAR_V_10X309] : % 4.79/4.80 ( ( pred_attacker(VAR_V_10X308) % 4.79/4.80 & pred_attacker(VAR_V_10X309) ) % 4.79/4.80 => pred_attacker(tuple_key_register_server_in_1(VAR_V_10X308,VAR_V_10X309)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax124,axiom, % 4.79/4.80 ! [VAR_V_116,VAR_V_117] : % 4.79/4.80 ( pred_attacker(tuple_key_register_server_in_1(VAR_V_116,VAR_V_117)) % 4.79/4.80 => pred_attacker(VAR_V_116) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax125,axiom, % 4.79/4.80 ! [VAR_V_119,VAR_V_120X30] : % 4.79/4.80 ( pred_attacker(tuple_key_register_server_in_1(VAR_V_119,VAR_V_120X30)) % 4.79/4.80 => pred_attacker(VAR_V_120X30) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax126,axiom, % 4.79/4.80 ! [VAR_V_123] : % 4.79/4.80 ( pred_attacker(VAR_V_123) % 4.79/4.80 => pred_attacker(constr_getmess(VAR_V_123)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax127,axiom, % 4.79/4.80 pred_attacker(tuple_false) ). % 4.79/4.80 % 4.79/4.80 fof(ax128,axiom, % 4.79/4.80 ! [VAR_V_126,VAR_V_127] : % 4.79/4.80 ( ( pred_attacker(VAR_V_126) % 4.79/4.80 & pred_attacker(VAR_V_127) ) % 4.79/4.80 => pred_attacker(constr_enc(VAR_V_126,VAR_V_127)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax129,axiom, % 4.79/4.80 ! [VAR_V_130X30,VAR_V_131] : % 4.79/4.80 ( ( pred_attacker(VAR_V_130X30) % 4.79/4.80 & pred_attacker(VAR_V_131) ) % 4.79/4.80 => pred_attacker(constr_dec(VAR_V_130X30,VAR_V_131)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax130,axiom, % 4.79/4.80 ! [VAR_V_133] : % 4.79/4.80 ( pred_attacker(VAR_V_133) % 4.79/4.80 => pred_attacker(tuple_client_B_out_6(VAR_V_133)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax131,axiom, % 4.79/4.80 ! [VAR_V_136] : % 4.79/4.80 ( pred_attacker(tuple_client_B_out_6(VAR_V_136)) % 4.79/4.80 => pred_attacker(VAR_V_136) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax132,axiom, % 4.79/4.80 ! [VAR_V_139] : % 4.79/4.80 ( pred_attacker(VAR_V_139) % 4.79/4.80 => pred_attacker(tuple_client_B_out_4(VAR_V_139)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax133,axiom, % 4.79/4.80 ! [VAR_V_142] : % 4.79/4.80 ( pred_attacker(tuple_client_B_out_4(VAR_V_142)) % 4.79/4.80 => pred_attacker(VAR_V_142) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax134,axiom, % 4.79/4.80 ! [VAR_V_146,VAR_V_147] : % 4.79/4.80 ( ( pred_attacker(VAR_V_146) % 4.79/4.80 & pred_attacker(VAR_V_147) ) % 4.79/4.80 => pred_attacker(tuple_client_B_out_1(VAR_V_146,VAR_V_147)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax135,axiom, % 4.79/4.80 ! [VAR_V_154,VAR_V_155] : % 4.79/4.80 ( pred_attacker(tuple_client_B_out_1(VAR_V_154,VAR_V_155)) % 4.79/4.80 => pred_attacker(VAR_V_154) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax136,axiom, % 4.79/4.80 ! [VAR_V_157,VAR_V_158] : % 4.79/4.80 ( pred_attacker(tuple_client_B_out_1(VAR_V_157,VAR_V_158)) % 4.79/4.80 => pred_attacker(VAR_V_158) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax137,axiom, % 4.79/4.80 ! [VAR_V_161] : % 4.79/4.80 ( pred_attacker(VAR_V_161) % 4.79/4.80 => pred_attacker(tuple_client_B_in_5(VAR_V_161)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax138,axiom, % 4.79/4.80 ! [VAR_V_164] : % 4.79/4.80 ( pred_attacker(tuple_client_B_in_5(VAR_V_164)) % 4.79/4.80 => pred_attacker(VAR_V_164) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax139,axiom, % 4.79/4.80 ! [VAR_V_167] : % 4.79/4.80 ( pred_attacker(VAR_V_167) % 4.79/4.80 => pred_attacker(tuple_client_B_in_3(VAR_V_167)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax140,axiom, % 4.79/4.80 ! [VAR_V_170X30] : % 4.79/4.80 ( pred_attacker(tuple_client_B_in_3(VAR_V_170X30)) % 4.79/4.80 => pred_attacker(VAR_V_170X30) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax141,axiom, % 4.79/4.80 ! [VAR_V_173] : % 4.79/4.80 ( pred_attacker(VAR_V_173) % 4.79/4.80 => pred_attacker(tuple_client_B_in_2(VAR_V_173)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax142,axiom, % 4.79/4.80 ! [VAR_V_176] : % 4.79/4.80 ( pred_attacker(tuple_client_B_in_2(VAR_V_176)) % 4.79/4.80 => pred_attacker(VAR_V_176) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax143,axiom, % 4.79/4.80 ! [VAR_V_179] : % 4.79/4.80 ( pred_attacker(VAR_V_179) % 4.79/4.80 => pred_attacker(tuple_client_A_out_5(VAR_V_179)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax144,axiom, % 4.79/4.80 ! [VAR_V_182] : % 4.79/4.80 ( pred_attacker(tuple_client_A_out_5(VAR_V_182)) % 4.79/4.80 => pred_attacker(VAR_V_182) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax145,axiom, % 4.79/4.80 ! [VAR_V_185] : % 4.79/4.80 ( pred_attacker(VAR_V_185) % 4.79/4.80 => pred_attacker(tuple_client_A_out_3(VAR_V_185)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax146,axiom, % 4.79/4.80 ! [VAR_V_188] : % 4.79/4.80 ( pred_attacker(tuple_client_A_out_3(VAR_V_188)) % 4.79/4.80 => pred_attacker(VAR_V_188) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax147,axiom, % 4.79/4.80 ! [VAR_V_192,VAR_V_193] : % 4.79/4.80 ( ( pred_attacker(VAR_V_192) % 4.79/4.80 & pred_attacker(VAR_V_193) ) % 4.79/4.80 => pred_attacker(tuple_client_A_out_1(VAR_V_192,VAR_V_193)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax148,axiom, % 4.79/4.80 ! [VAR_V_20X300X30,VAR_V_20X301] : % 4.79/4.80 ( pred_attacker(tuple_client_A_out_1(VAR_V_20X300X30,VAR_V_20X301)) % 4.79/4.80 => pred_attacker(VAR_V_20X300X30) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax149,axiom, % 4.79/4.80 ! [VAR_V_20X303,VAR_V_20X304] : % 4.79/4.80 ( pred_attacker(tuple_client_A_out_1(VAR_V_20X303,VAR_V_20X304)) % 4.79/4.80 => pred_attacker(VAR_V_20X304) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax150,axiom, % 4.79/4.80 ! [VAR_V_20X307] : % 4.79/4.80 ( pred_attacker(VAR_V_20X307) % 4.79/4.80 => pred_attacker(tuple_client_A_in_4(VAR_V_20X307)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax151,axiom, % 4.79/4.80 ! [VAR_V_210X30] : % 4.79/4.80 ( pred_attacker(tuple_client_A_in_4(VAR_V_210X30)) % 4.79/4.80 => pred_attacker(VAR_V_210X30) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax152,axiom, % 4.79/4.80 ! [VAR_V_213] : % 4.79/4.80 ( pred_attacker(VAR_V_213) % 4.79/4.80 => pred_attacker(tuple_client_A_in_2(VAR_V_213)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax153,axiom, % 4.79/4.80 ! [VAR_V_216] : % 4.79/4.80 ( pred_attacker(tuple_client_A_in_2(VAR_V_216)) % 4.79/4.80 => pred_attacker(VAR_V_216) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax154,axiom, % 4.79/4.80 ! [VAR_V_220X30,VAR_V_221] : % 4.79/4.80 ( ( pred_attacker(VAR_V_220X30) % 4.79/4.80 & pred_attacker(VAR_V_221) ) % 4.79/4.80 => pred_attacker(constr_checksign(VAR_V_220X30,VAR_V_221)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax155,axiom, % 4.79/4.80 ! [VAR_V_224,VAR_V_225] : % 4.79/4.80 ( ( pred_attacker(VAR_V_224) % 4.79/4.80 & pred_attacker(VAR_V_225) ) % 4.79/4.80 => pred_attacker(constr_aenc(VAR_V_224,VAR_V_225)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax156,axiom, % 4.79/4.80 ! [VAR_V_228,VAR_V_229] : % 4.79/4.80 ( ( pred_attacker(VAR_V_228) % 4.79/4.80 & pred_attacker(VAR_V_229) ) % 4.79/4.80 => pred_attacker(constr_adec(VAR_V_228,VAR_V_229)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax157,axiom, % 4.79/4.80 pred_attacker(constr_ZERO) ). % 4.79/4.80 % 4.79/4.80 fof(ax158,axiom, % 4.79/4.80 pred_attacker(constr_CONST_4) ). % 4.79/4.80 % 4.79/4.80 fof(ax159,axiom, % 4.79/4.80 pred_attacker(constr_CONST_3) ). % 4.79/4.80 % 4.79/4.80 fof(ax160,axiom, % 4.79/4.80 pred_attacker(constr_CONST_2) ). % 4.79/4.80 % 4.79/4.80 fof(ax161,axiom, % 4.79/4.80 pred_attacker(constr_CONST_1) ). % 4.79/4.80 % 4.79/4.80 fof(ax162,axiom, % 4.79/4.80 pred_attacker(constr_CONST_0x30) ). % 4.79/4.80 % 4.79/4.80 fof(ax163,axiom, % 4.79/4.80 ! [VAR_V_236,VAR_V_237] : % 4.79/4.80 ( ( pred_attacker(VAR_V_236) % 4.79/4.80 & pred_attacker(VAR_V_237) ) % 4.79/4.80 => pred_attacker(tuple_2(VAR_V_236,VAR_V_237)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax164,axiom, % 4.79/4.80 ! [VAR_V_244,VAR_V_245] : % 4.79/4.80 ( pred_attacker(tuple_2(VAR_V_244,VAR_V_245)) % 4.79/4.80 => pred_attacker(VAR_V_244) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax165,axiom, % 4.79/4.80 ! [VAR_V_247,VAR_V_248] : % 4.79/4.80 ( pred_attacker(tuple_2(VAR_V_247,VAR_V_248)) % 4.79/4.80 => pred_attacker(VAR_V_248) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax166,axiom, % 4.79/4.80 ! [VAR_V_250X30,VAR_V_251] : % 4.79/4.80 ( ( pred_mess(VAR_V_251,VAR_V_250X30) % 4.79/4.80 & pred_attacker(VAR_V_251) ) % 4.79/4.80 => pred_attacker(VAR_V_250X30) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax167,axiom, % 4.79/4.80 ! [VAR_V_252,VAR_V_253] : % 4.79/4.80 ( ( pred_attacker(VAR_V_253) % 4.79/4.80 & pred_attacker(VAR_V_252) ) % 4.79/4.80 => pred_mess(VAR_V_253,VAR_V_252) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax168,axiom, % 4.79/4.80 pred_attacker(name_c) ). % 4.79/4.80 % 4.79/4.80 fof(ax169,axiom, % 4.79/4.80 pred_attacker(name_I) ). % 4.79/4.80 % 4.79/4.80 fof(ax170,axiom, % 4.79/4.80 pred_attacker(name_B) ). % 4.79/4.80 % 4.79/4.80 fof(ax171,axiom, % 4.79/4.80 pred_attacker(name_A) ). % 4.79/4.80 % 4.79/4.80 fof(ax172,axiom, % 4.79/4.80 ! [VAR_V_255] : pred_equal(VAR_V_255,VAR_V_255) ). % 4.79/4.80 % 4.79/4.80 fof(ax173,axiom, % 4.79/4.80 ! [VAR_V_256] : pred_attacker(name_new0x2Dname(VAR_V_256)) ). % 4.79/4.80 % 4.79/4.80 fof(ax174,axiom, % 4.79/4.80 pred_table(tuple_keys(name_A,constr_pkey(name_skA))) ). % 4.79/4.80 % 4.79/4.80 fof(ax175,axiom, % 4.79/4.80 pred_table(tuple_keys(name_B,constr_pkey(name_skB))) ). % 4.79/4.80 % 4.79/4.80 fof(ax176,axiom, % 4.79/4.80 pred_attacker(tuple_out_1(constr_pkey(name_skA))) ). % 4.79/4.80 % 4.79/4.80 fof(ax177,axiom, % 4.79/4.80 pred_attacker(tuple_out_2(constr_pkey(name_skB))) ). % 4.79/4.80 % 4.79/4.80 fof(ax178,axiom, % 4.79/4.80 pred_attacker(tuple_out_3(constr_pkey(name_skS))) ). % 4.79/4.80 % 4.79/4.80 fof(ax179,axiom, % 4.79/4.80 pred_attacker(tuple_client_A_out_1(name_A,name_I)) ). % 4.79/4.80 % 4.79/4.80 fof(ax180,axiom, % 4.79/4.80 ! [VAR_0X40SID_376,VAR_SIGN_I_PKI_375] : % 4.79/4.80 ( ( pred_eq_bitstring_bitstring(name_I,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_I_PKI_375,constr_pkey(name_skS)))) % 4.79/4.80 & pred_attacker(tuple_client_A_in_2(VAR_SIGN_I_PKI_375)) ) % 4.79/4.80 => pred_attacker(tuple_client_A_out_3(constr_aenc(tuple_2(name_Na(VAR_0X40SID_376),name_A),constr_tuple_2_get_1_bitstring(constr_checksign(VAR_SIGN_I_PKI_375,constr_pkey(name_skS)))))) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax181,axiom, % 4.79/4.80 ! [VAR_0X40SID_435,VAR_AENC_NA_XOR_I_NI_434,VAR_SIGN_I_PKI_436] : % 4.79/4.80 ( ( pred_eq_bitstring_bitstring(name_I,constr_xor(constr_tuple_2_get_0x30_bitstring(constr_adec(VAR_AENC_NA_XOR_I_NI_434,name_skA)),name_Na(VAR_0X40SID_435))) % 4.79/4.80 & pred_attacker(tuple_client_A_in_4(VAR_AENC_NA_XOR_I_NI_434)) % 4.79/4.80 & pred_eq_bitstring_bitstring(name_I,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_I_PKI_436,constr_pkey(name_skS)))) % 4.79/4.80 & pred_attacker(tuple_client_A_in_2(VAR_SIGN_I_PKI_436)) ) % 4.79/4.80 => pred_attacker(tuple_client_A_out_5(constr_aenc(constr_tuple_2_get_1_bitstring(constr_adec(VAR_AENC_NA_XOR_I_NI_434,name_skA)),constr_tuple_2_get_1_bitstring(constr_checksign(VAR_SIGN_I_PKI_436,constr_pkey(name_skS)))))) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax182,axiom, % 4.79/4.80 pred_attacker(tuple_client_B_out_1(name_B,name_A)) ). % 4.79/4.80 % 4.79/4.80 fof(ax183,axiom, % 4.79/4.80 ! [VAR_0X40SID_553,VAR_AENC_NA_A_551,VAR_SIGN_A_PKA_552] : % 4.79/4.80 ( ( pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(VAR_AENC_NA_A_551,name_skB))) % 4.79/4.80 & pred_attacker(tuple_client_B_in_3(VAR_AENC_NA_A_551)) % 4.79/4.80 & pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_552,constr_pkey(name_skS)))) % 4.79/4.80 & pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_552)) ) % 4.79/4.80 => pred_attacker(tuple_client_B_out_4(constr_aenc(tuple_2(constr_xor(constr_tuple_2_get_0x30_bitstring(constr_adec(VAR_AENC_NA_A_551,name_skB)),name_B),name_Nb(VAR_0X40SID_553)),constr_tuple_2_get_1_bitstring(constr_checksign(VAR_SIGN_A_PKA_552,constr_pkey(name_skS)))))) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax184,axiom, % 4.79/4.80 ! [VAR_0X40SID_577,VAR_AENC_NA_A_579,VAR_AENC_NB_578,VAR_SIGN_A_PKA_580X30] : % 4.79/4.80 ( ( pred_eq_bitstring_bitstring(name_Nb(VAR_0X40SID_577),constr_adec(VAR_AENC_NB_578,name_skB)) % 4.79/4.80 & pred_attacker(tuple_client_B_in_5(VAR_AENC_NB_578)) % 4.79/4.80 & pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_1(constr_adec(VAR_AENC_NA_A_579,name_skB))) % 4.79/4.80 & pred_attacker(tuple_client_B_in_3(VAR_AENC_NA_A_579)) % 4.79/4.80 & pred_eq_bitstring_bitstring(name_A,constr_tuple_2_get_0x30(constr_checksign(VAR_SIGN_A_PKA_580X30,constr_pkey(name_skS)))) % 4.79/4.80 & pred_attacker(tuple_client_B_in_2(VAR_SIGN_A_PKA_580X30)) ) % 4.79/4.80 => pred_attacker(tuple_client_B_out_6(name_objective)) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax185,axiom, % 4.79/4.80 ! [VAR_DST_619,VAR_PKDST_620X30,VAR_SRC_621] : % 4.79/4.80 ( ( pred_table(tuple_keys(VAR_DST_619,VAR_PKDST_620X30)) % 4.79/4.80 & pred_attacker(tuple_key_retrieval_server_in_1(VAR_SRC_621,VAR_DST_619)) ) % 4.79/4.80 => pred_attacker(tuple_key_retrieval_server_out_2(constr_sign(tuple_2(VAR_DST_619,VAR_PKDST_620X30),name_skS))) ) ). % 4.79/4.80 % 4.79/4.80 fof(ax186,axiom, % 4.79/4.80 ! [VAR_HOST_673,VAR_PK_674] : % 4.79/4.80 ( ( VAR_HOST_673 != name_B % 4.79/4.80 & VAR_HOST_673 != name_A % 4.79/4.80 & pred_attacker(tuple_key_register_server_in_1(VAR_HOST_673,VAR_PK_674)) ) % 4.79/4.80 => pred_table(tuple_keys(VAR_HOST_673,VAR_PK_674)) ) ). % 4.79/4.80 % 4.79/4.80 fof(co0,conjecture, % 4.79/4.80 pred_attacker(name_objective) ). % 4.79/4.80 % 4.79/4.80 %-------------------------------------------------------------------------- % 4.79/4.80 %------------------------------------------- % 4.79/4.80 % Proof found % 4.79/4.80 % SZS status Theorem for theBenchmark % 4.79/4.80 % SZS output start Proof % 4.79/4.80 %ClaNum:244(EqnAxiom:57) % 4.79/4.80 %VarNum:221(SingletonVarNum:120) % 4.79/4.80 %MaxLitNum:4 % 4.79/4.80 %MaxfuncDepth:5 % 4.79/4.80 %SharedTerms:139 % 4.79/4.80 %goalClause: 182 % 4.79/4.80 %singleGoalClaCount:1 % 4.79/4.80 [58]P1(a1) % 4.79/4.80 [59]P1(a2) % 4.79/4.80 [60]P1(a3) % 4.79/4.80 [61]P1(a4) % 4.79/4.80 [62]P1(a5) % 4.79/4.80 [63]P1(a6) % 4.79/4.80 [64]P1(a7) % 4.79/4.80 [65]P1(a21) % 4.79/4.80 [66]P1(a22) % 4.79/4.80 [67]P1(a23) % 4.79/4.80 [68]P1(a26) % 4.79/4.80 [69]P1(a27) % 4.79/4.80 [91]~E(a2,a1) % 4.79/4.80 [92]~E(a3,a1) % 4.79/4.80 [93]~E(a3,a2) % 4.79/4.80 [94]~E(a4,a1) % 4.79/4.80 [95]~E(a4,a2) % 4.79/4.80 [96]~E(a4,a3) % 4.79/4.80 [97]~E(a5,a1) % 4.79/4.80 [98]~E(a5,a2) % 4.79/4.80 [99]~E(a5,a3) % 4.79/4.80 [100]~E(a5,a4) % 4.79/4.80 [101]~E(a1,a6) % 4.79/4.80 [102]~E(a2,a6) % 4.79/4.80 [103]~E(a3,a6) % 4.79/4.80 [104]~E(a4,a6) % 4.79/4.80 [105]~E(a5,a6) % 4.79/4.80 [106]~E(a7,a1) % 4.79/4.80 [107]~E(a7,a2) % 4.79/4.80 [108]~E(a7,a3) % 4.79/4.80 [109]~E(a7,a4) % 4.79/4.80 [110]~E(a7,a5) % 4.79/4.80 [111]~E(a7,a6) % 4.79/4.80 [112]~E(a21,a1) % 4.79/4.80 [113]~E(a21,a2) % 4.79/4.80 [114]~E(a21,a3) % 4.79/4.80 [115]~E(a21,a4) % 4.79/4.80 [116]~E(a21,a5) % 4.79/4.80 [117]~E(a21,a6) % 4.79/4.80 [118]~E(a21,a7) % 4.79/4.80 [119]~E(a22,a1) % 4.79/4.80 [120]~E(a22,a2) % 4.79/4.80 [121]~E(a22,a3) % 4.79/4.80 [122]~E(a22,a4) % 4.79/4.81 [123]~E(a22,a5) % 4.79/4.81 [124]~E(a22,a6) % 4.79/4.81 [125]~E(a22,a7) % 4.79/4.81 [126]~E(a22,a21) % 4.79/4.81 [127]~E(a23,a1) % 4.79/4.81 [128]~E(a23,a2) % 4.79/4.81 [129]~E(a23,a3) % 4.79/4.81 [130]~E(a23,a4) % 4.79/4.81 [131]~E(a23,a5) % 4.79/4.81 [132]~E(a23,a6) % 4.79/4.81 [133]~E(a23,a7) % 4.79/4.81 [134]~E(a23,a21) % 4.79/4.81 [135]~E(a23,a22) % 4.79/4.81 [136]~E(a32,a1) % 4.79/4.81 [137]~E(a32,a2) % 4.79/4.81 [138]~E(a32,a3) % 4.79/4.81 [139]~E(a32,a4) % 4.79/4.81 [140]~E(a32,a5) % 4.79/4.81 [141]~E(a32,a6) % 4.79/4.81 [142]~E(a32,a7) % 4.79/4.81 [143]~E(a32,a21) % 4.79/4.81 [144]~E(a32,a22) % 4.79/4.81 [145]~E(a32,a23) % 4.79/4.81 [146]~E(a31,a1) % 4.79/4.81 [147]~E(a31,a2) % 4.79/4.81 [148]~E(a31,a3) % 4.79/4.81 [149]~E(a31,a4) % 4.79/4.81 [150]~E(a31,a5) % 4.79/4.81 [151]~E(a31,a6) % 4.79/4.81 [152]~E(a31,a7) % 4.79/4.81 [153]~E(a31,a21) % 4.79/4.81 [154]~E(a31,a22) % 4.79/4.81 [155]~E(a31,a23) % 4.79/4.81 [156]~E(a32,a31) % 4.79/4.81 [157]~E(a30,a1) % 4.79/4.81 [158]~E(a30,a2) % 4.79/4.81 [159]~E(a30,a3) % 4.79/4.81 [160]~E(a30,a4) % 4.79/4.81 [161]~E(a30,a5) % 4.79/4.81 [162]~E(a30,a6) % 4.79/4.81 [163]~E(a30,a7) % 4.79/4.81 [164]~E(a30,a21) % 4.79/4.81 [165]~E(a30,a22) % 4.79/4.81 [166]~E(a30,a23) % 4.79/4.81 [167]~E(a32,a30) % 4.79/4.81 [168]~E(a31,a30) % 4.79/4.81 [169]~E(a29,a1) % 4.79/4.81 [170]~E(a29,a2) % 4.79/4.81 [171]~E(a29,a3) % 4.79/4.81 [172]~E(a29,a4) % 4.79/4.81 [173]~E(a29,a5) % 4.79/4.81 [174]~E(a29,a6) % 4.79/4.81 [175]~E(a29,a7) % 4.79/4.81 [176]~E(a29,a21) % 4.79/4.81 [177]~E(a29,a22) % 4.79/4.81 [178]~E(a29,a23) % 4.79/4.81 [179]~E(a32,a29) % 4.79/4.81 [180]~E(a31,a29) % 4.79/4.81 [181]~E(a30,a29) % 4.79/4.81 [182]~P1(a32) % 4.79/4.81 [77]P1(f33(a21,a7)) % 4.79/4.81 [78]P1(f34(a7,a22)) % 4.79/4.81 [74]P1(f45(f9(a29))) % 4.79/4.81 [75]P1(f46(f9(a30))) % 4.79/4.81 [76]P1(f47(f9(a31))) % 4.79/4.81 [85]P3(f48(a7,f9(a31))) % 4.79/4.81 [86]P3(f48(a21,f9(a30))) % 4.79/4.81 [73]P2(x731,x731) % 4.79/4.81 [70]P1(f28(x701)) % 4.79/4.81 [71]E(f8(x711,a6),x711) % 4.79/4.81 [72]E(f8(x721,x721),a6) % 4.79/4.81 [79]E(f8(x791,x792),f8(x792,x791)) % 4.79/4.81 [80]E(f10(f16(x801,x802)),x801) % 4.79/4.81 [81]E(f17(f35(x811,x812)),x812) % 4.79/4.81 [82]E(f18(f35(x821,x822)),x821) % 4.79/4.81 [83]E(f20(f35(x831,x832)),x832) % 4.79/4.81 [84]E(f19(f35(x841,x842)),x841) % 4.79/4.81 [87]E(f12(f11(x871,x872),x872),x871) % 4.79/4.81 [88]E(f13(f16(x881,x882),f9(x882)),x881) % 4.79/4.81 [89]E(f15(f14(x891,f9(x892)),x892),x891) % 4.79/4.81 [90]E(f8(f8(x901,x902),x903),f8(x901,f8(x902,x903))) % 4.79/4.81 [183]~P1(x1831)+P1(f9(x1831)) % 4.79/4.81 [184]~P1(x1841)+P1(f10(x1841)) % 4.79/4.81 [185]~P1(x1851)+P1(f17(x1851)) % 4.79/4.81 [186]~P1(x1861)+P1(f18(x1861)) % 4.79/4.81 [187]~P1(x1871)+P1(f20(x1871)) % 4.79/4.81 [188]~P1(x1881)+P1(f19(x1881)) % 4.79/4.81 [189]~P1(x1891)+P1(f45(x1891)) % 4.79/4.81 [190]~P1(x1901)+P1(f46(x1901)) % 4.79/4.81 [191]~P1(x1911)+P1(f47(x1911)) % 4.79/4.81 [192]~P1(x1921)+P1(f49(x1921)) % 4.79/4.81 [193]~P1(x1931)+P1(f43(x1931)) % 4.79/4.81 [194]~P1(x1941)+P1(f44(x1941)) % 4.79/4.81 [195]~P1(x1951)+P1(f38(x1951)) % 4.79/4.81 [196]~P1(x1961)+P1(f39(x1961)) % 4.79/4.81 [197]~P1(x1971)+P1(f40(x1971)) % 4.79/4.81 [198]~P1(x1981)+P1(f41(x1981)) % 4.79/4.81 [199]~P1(x1991)+P1(f42(x1991)) % 4.79/4.81 [200]~P1(x2001)+P1(f36(x2001)) % 4.79/4.81 [201]~P1(x2011)+P1(f37(x2011)) % 4.79/4.81 [202]P1(x2021)+~P1(f45(x2021)) % 4.79/4.81 [203]P1(x2031)+~P1(f46(x2031)) % 4.79/4.81 [204]P1(x2041)+~P1(f47(x2041)) % 4.79/4.81 [205]P1(x2051)+~P1(f49(x2051)) % 4.79/4.81 [206]P1(x2061)+~P1(f43(x2061)) % 4.79/4.81 [207]P1(x2071)+~P1(f44(x2071)) % 4.79/4.81 [208]P1(x2081)+~P1(f38(x2081)) % 4.79/4.81 [209]P1(x2091)+~P1(f39(x2091)) % 4.79/4.81 [210]P1(x2101)+~P1(f40(x2101)) % 4.79/4.81 [211]P1(x2111)+~P1(f41(x2111)) % 4.79/4.81 [212]P1(x2121)+~P1(f42(x2121)) % 4.79/4.81 [213]P1(x2131)+~P1(f36(x2131)) % 4.79/4.81 [214]P1(x2141)+~P1(f37(x2141)) % 4.79/4.81 [229]P1(x2291)+~P1(f35(x2292,x2291)) % 4.79/4.81 [230]P1(x2301)+~P1(f50(x2302,x2301)) % 4.79/4.81 [231]P1(x2311)+~P1(f51(x2312,x2311)) % 4.79/4.81 [232]P1(x2321)+~P1(f33(x2322,x2321)) % 4.79/4.81 [233]P1(x2331)+~P1(f34(x2332,x2331)) % 4.79/4.81 [234]P1(x2341)+~P1(f35(x2341,x2342)) % 4.79/4.81 [235]P1(x2351)+~P1(f50(x2351,x2352)) % 4.79/4.81 [236]P1(x2361)+~P1(f51(x2361,x2362)) % 4.79/4.81 [237]P1(x2371)+~P1(f33(x2371,x2372)) % 4.79/4.81 [238]P1(x2381)+~P1(f34(x2381,x2382)) % 4.79/4.81 [242]~P1(f37(x2422))+P1(f42(f14(f35(f24(x2421),a7),f17(f13(x2422,f9(a29)))))) % 4.79/4.81 [215]~P1(x2152)+~P1(x2151)+P4(x2151,x2152) % 4.79/4.81 [216]~P4(x2162,x2161)+P1(x2161)+~P1(x2162) % 4.79/4.81 [217]~P1(x2172)+~P1(x2171)+P1(f14(x2171,x2172)) % 4.79/4.81 [218]~P1(x2182)+~P1(x2181)+P1(f15(x2181,x2182)) % 4.79/4.81 [219]~P1(x2192)+~P1(x2191)+P1(f11(x2191,x2192)) % 4.79/4.81 [220]~P1(x2202)+~P1(x2201)+P1(f12(x2201,x2202)) % 4.79/4.81 [221]~P1(x2212)+~P1(x2211)+P1(f16(x2211,x2212)) % 4.79/4.81 [222]~P1(x2222)+~P1(x2221)+P1(f13(x2221,x2222)) % 4.79/4.81 [223]~P1(x2232)+~P1(x2231)+P1(f8(x2231,x2232)) % 4.79/4.81 [224]~P1(x2242)+~P1(x2241)+P1(f35(x2241,x2242)) % 4.79/4.81 [225]~P1(x2252)+~P1(x2251)+P1(f50(x2251,x2252)) % 4.79/4.81 [226]~P1(x2262)+~P1(x2261)+P1(f51(x2261,x2262)) % 4.79/4.81 [227]~P1(x2272)+~P1(x2271)+P1(f33(x2271,x2272)) % 4.79/4.81 [228]~P1(x2282)+~P1(x2281)+P1(f34(x2281,x2282)) % 4.79/4.81 [243]~P1(f36(x2431))+~P1(f37(x2432))+P1(f41(f14(f17(f15(x2431,a31)),f17(f13(x2432,f9(a29)))))) % 4.79/4.81 [241]~P3(f48(x2411,x2412))+~P1(f50(x2413,x2411))+P1(f49(f16(f35(x2411,x2412),a29))) % 4.79/4.81 [244]~P1(f39(x2441))+~P1(f40(x2443))+P1(f44(f14(f35(f8(f18(f15(x2441,a30)),a21),f25(x2442)),f17(f13(x2443,f9(a29)))))) % 4.79/4.81 [240]E(x2401,a21)+E(x2401,a7)+~P1(f51(x2401,x2402))+P3(f48(x2401,x2402)) % 4.79/4.81 [239]~P1(f38(x2391))+~P1(f39(x2392))+~P1(f40(x2393))+P1(f43(a32)) % 4.79/4.81 %EqnAxiom % 4.79/4.81 [1]E(x11,x11) % 4.79/4.81 [2]E(x22,x21)+~E(x21,x22) % 4.79/4.81 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 4.79/4.81 [4]~E(x41,x42)+E(f28(x41),f28(x42)) % 4.79/4.81 [5]~E(x51,x52)+E(f8(x51,x53),f8(x52,x53)) % 4.79/4.81 [6]~E(x61,x62)+E(f8(x63,x61),f8(x63,x62)) % 4.79/4.81 [7]~E(x71,x72)+E(f40(x71),f40(x72)) % 4.79/4.81 [8]~E(x81,x82)+E(f9(x81),f9(x82)) % 4.79/4.81 [9]~E(x91,x92)+E(f45(x91),f45(x92)) % 4.79/4.81 [10]~E(x101,x102)+E(f37(x101),f37(x102)) % 4.79/4.81 [11]~E(x111,x112)+E(f46(x111),f46(x112)) % 4.79/4.81 [12]~E(x121,x122)+E(f36(x121),f36(x122)) % 4.79/4.81 [13]~E(x131,x132)+E(f47(x131),f47(x132)) % 4.79/4.81 [14]~E(x141,x142)+E(f33(x141,x143),f33(x142,x143)) % 4.79/4.81 [15]~E(x151,x152)+E(f33(x153,x151),f33(x153,x152)) % 4.79/4.81 [16]~E(x161,x162)+E(f34(x161,x163),f34(x162,x163)) % 4.79/4.81 [17]~E(x171,x172)+E(f34(x173,x171),f34(x173,x172)) % 4.79/4.81 [18]~E(x181,x182)+E(f39(x181),f39(x182)) % 4.79/4.81 [19]~E(x191,x192)+E(f44(x191),f44(x192)) % 4.79/4.81 [20]~E(x201,x202)+E(f16(x201,x203),f16(x202,x203)) % 4.79/4.81 [21]~E(x211,x212)+E(f16(x213,x211),f16(x213,x212)) % 4.79/4.81 [22]~E(x221,x222)+E(f10(x221),f10(x222)) % 4.79/4.81 [23]~E(x231,x232)+E(f35(x231,x233),f35(x232,x233)) % 4.79/4.81 [24]~E(x241,x242)+E(f35(x243,x241),f35(x243,x242)) % 4.79/4.81 [25]~E(x251,x252)+E(f17(x251),f17(x252)) % 4.79/4.81 [26]~E(x261,x262)+E(f50(x261,x263),f50(x262,x263)) % 4.79/4.81 [27]~E(x271,x272)+E(f50(x273,x271),f50(x273,x272)) % 4.79/4.81 [28]~E(x281,x282)+E(f18(x281),f18(x282)) % 4.79/4.81 [29]~E(x291,x292)+E(f15(x291,x293),f15(x292,x293)) % 4.79/4.81 [30]~E(x301,x302)+E(f15(x303,x301),f15(x303,x302)) % 4.79/4.81 [31]~E(x311,x312)+E(f20(x311),f20(x312)) % 4.79/4.81 [32]~E(x321,x322)+E(f51(x321,x323),f51(x322,x323)) % 4.79/4.81 [33]~E(x331,x332)+E(f51(x333,x331),f51(x333,x332)) % 4.79/4.81 [34]~E(x341,x342)+E(f19(x341),f19(x342)) % 4.79/4.81 [35]~E(x351,x352)+E(f41(x351),f41(x352)) % 4.79/4.81 [36]~E(x361,x362)+E(f48(x361,x363),f48(x362,x363)) % 4.79/4.81 [37]~E(x371,x372)+E(f48(x373,x371),f48(x373,x372)) % 4.79/4.81 [38]~E(x381,x382)+E(f14(x381,x383),f14(x382,x383)) % 4.79/4.81 [39]~E(x391,x392)+E(f14(x393,x391),f14(x393,x392)) % 4.79/4.81 [40]~E(x401,x402)+E(f42(x401),f42(x402)) % 4.79/4.81 [41]~E(x411,x412)+E(f11(x411,x413),f11(x412,x413)) % 4.79/4.81 [42]~E(x421,x422)+E(f11(x423,x421),f11(x423,x422)) % 4.79/4.81 [43]~E(x431,x432)+E(f12(x431,x433),f12(x432,x433)) % 4.79/4.81 [44]~E(x441,x442)+E(f12(x443,x441),f12(x443,x442)) % 4.79/4.81 [45]~E(x451,x452)+E(f13(x451,x453),f13(x452,x453)) % 4.79/4.81 [46]~E(x461,x462)+E(f13(x463,x461),f13(x463,x462)) % 4.79/4.81 [47]~E(x471,x472)+E(f49(x471),f49(x472)) % 4.79/4.81 [48]~E(x481,x482)+E(f43(x481),f43(x482)) % 4.79/4.81 [49]~E(x491,x492)+E(f38(x491),f38(x492)) % 4.79/4.81 [50]~E(x501,x502)+E(f24(x501),f24(x502)) % 4.79/4.81 [51]~E(x511,x512)+E(f25(x511),f25(x512)) % 4.79/4.81 [52]~P1(x521)+P1(x522)+~E(x521,x522) % 4.79/4.81 [53]~P3(x531)+P3(x532)+~E(x531,x532) % 4.79/4.81 [54]P2(x542,x543)+~E(x541,x542)+~P2(x541,x543) % 4.79/4.81 [55]P2(x553,x552)+~E(x551,x552)+~P2(x553,x551) % 4.79/4.81 [56]P4(x562,x563)+~E(x561,x562)+~P4(x561,x563) % 4.79/4.81 [57]P4(x573,x572)+~E(x571,x572)+~P4(x573,x571) % 4.79/4.81 % 4.79/4.81 %------------------------------------------- % 4.79/4.81 cnf(245,plain, % 4.79/4.81 (P1(f9(a29))), % 4.79/4.81 inference(scs_inference,[],[74,202])). % 4.79/4.81 cnf(731,plain, % 4.79/4.81 (P1(f45(f20(f9(a29))))), % 4.79/4.81 inference(scs_inference,[],[245,189,187])). % 4.79/4.81 cnf(732,plain, % 4.79/4.81 (P1(f20(f9(a29)))), % 4.79/4.81 inference(scs_inference,[],[731,202])). % 4.79/4.81 cnf(1061,plain, % 4.79/4.81 (P1(f38(f39(f20(f9(a29)))))), % 4.79/4.81 inference(scs_inference,[],[732,195,196])). % 4.79/4.81 cnf(1062,plain, % 4.79/4.81 (~P1(f39(x10621))+~P1(f40(x10622))+P1(f43(a32))), % 4.79/4.81 inference(scs_inference,[],[1061,239])). % 4.79/4.81 cnf(1063,plain, % 4.79/4.81 (P1(f39(f20(f9(a29))))), % 4.79/4.81 inference(scs_inference,[],[1061,208])). % 4.79/4.81 cnf(1069,plain, % 4.79/4.81 (~P1(f40(x10691))+P1(f43(a32))), % 4.79/4.81 inference(scs_inference,[],[1063,1062])). % 4.79/4.81 cnf(1133,plain, % 4.79/4.81 (P1(f40(f41(a1)))), % 4.79/4.81 inference(scs_inference,[],[58,197,198])). % 4.79/4.81 cnf(1134,plain, % 4.79/4.81 (P1(f43(a32))), % 4.79/4.81 inference(scs_inference,[],[1133,1069])). % 4.79/4.81 cnf(1142,plain, % 4.79/4.81 ($false), % 4.79/4.81 inference(scs_inference,[],[182,1134,206]), % 4.79/4.81 ['proof']). % 4.79/4.81 % SZS output end Proof % 4.79/4.81 % Total time :4.130000s %------------------------------------------------------------------------------