%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWW956+1 : TPTP v8.2.0. Released v7.4.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n022.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 9.23s 9.29s % Output : CNFRefutation 9.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SWW956+1 : TPTP v8.2.0. Released v7.4.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.11/0.33 % Computer : n022.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Wed Jun 19 04:43:23 EDT 2024 % 0.11/0.33 % CPUTime : % 0.19/0.58 start to proof:theBenchmark % 9.15/9.27 %------------------------------------------- % 9.15/9.27 % File :CSE---1.7 % 9.15/9.27 % Problem :theBenchmark % 9.15/9.27 % Transform :cnf % 9.15/9.27 % Format :tptp:raw % 9.15/9.27 % Command :java -jar mcs_scs.jar %d %s % 9.15/9.27 % 9.15/9.27 % Result :Theorem 8.660000s % 9.15/9.27 % Output :CNFRefutation 8.660000s % 9.15/9.27 %------------------------------------------- % 9.15/9.28 %-------------------------------------------------------------------------- % 9.15/9.28 % File : SWW956+1 : TPTP v8.2.0. Released v7.4.0. % 9.15/9.28 % Domain : Software Verification % 9.15/9.28 % Problem : Attack on Diffie-Hellman Key Exchange Protocol % 9.15/9.28 % Version : [LT19] axioms : Especial. % 9.15/9.28 % English : Attack demonstrates violation of secrecy property. % 9.15/9.28 % 9.15/9.28 % Refs : [BO97] Bull & Otway (1997), The Authentication Protocol % 9.15/9.28 % : [RS98] Ryan & Schneider (1998), An Attack on a Recursive Auth % 9.23/9.28 % : [LT19] Li & Tiu (2019), Combining ProVerif and Automated Theo % 9.23/9.28 % : [Li20] Li (2020), Email to Geoff Sutcliffe % 9.23/9.28 % Source : [Li20] % 9.23/9.28 % Names : DH.p [LT20] % 9.23/9.28 % 9.23/9.28 % Status : Theorem % 9.23/9.28 % Rating : 0.44 v8.1.0, 0.39 v7.5.0, 0.47 v7.4.0 % 9.23/9.28 % Syntax : Number of formulae : 94 ( 70 unt; 0 def) % 9.23/9.28 % Number of atoms : 127 ( 57 equ) % 9.23/9.28 % Maximal formula atoms : 3 ( 1 avg) % 9.23/9.28 % Number of connectives : 88 ( 55 ~; 0 |; 9 &) % 9.23/9.28 % ( 0 <=>; 24 =>; 0 <=; 0 <~>) % 9.23/9.28 % Maximal formula depth : 6 ( 2 avg) % 9.23/9.28 % Maximal term depth : 5 ( 1 avg) % 9.23/9.28 % Number of predicates : 4 ( 3 usr; 0 prp; 1-2 aty) % 9.23/9.28 % Number of functors : 25 ( 25 usr; 13 con; 0-2 aty) % 9.23/9.28 % Number of variables : 46 ( 46 !; 0 ?) % 9.23/9.28 % SPC : FOF_THM_RFO_SEQ % 9.23/9.28 % 9.23/9.28 % Comments : Generated by a modified version of ProVerif used in the % 9.23/9.28 % ProVerif-ATP project [LT19]. % 9.23/9.28 %-------------------------------------------------------------------------- % 9.23/9.28 fof(ax0,axiom, % 9.23/9.28 constr_CONST_0x30 != constr_CONST_1 ). % 9.23/9.28 % 9.23/9.28 fof(ax1,axiom, % 9.23/9.28 constr_CONST_0x30 != constr_CONST_2 ). % 9.23/9.28 % 9.23/9.28 fof(ax2,axiom, % 9.23/9.28 constr_CONST_0x30 != constr_CONST_3 ). % 9.23/9.28 % 9.23/9.28 fof(ax3,axiom, % 9.23/9.28 constr_CONST_0x30 != constr_CONST_4 ). % 9.23/9.28 % 9.23/9.28 fof(ax4,axiom, % 9.23/9.28 constr_CONST_0x30 != name_G_8 ). % 9.23/9.28 % 9.23/9.28 fof(ax5,axiom, % 9.23/9.28 constr_CONST_0x30 != name_Na ). % 9.23/9.28 % 9.23/9.28 fof(ax6,axiom, % 9.23/9.28 constr_CONST_0x30 != name_Nb ). % 9.23/9.28 % 9.23/9.28 fof(ax7,axiom, % 9.23/9.28 constr_CONST_0x30 != name_P_7 ). % 9.23/9.28 % 9.23/9.28 fof(ax8,axiom, % 9.23/9.28 constr_CONST_0x30 != name_c ). % 9.23/9.28 % 9.23/9.28 fof(ax9,axiom, % 9.23/9.28 constr_CONST_0x30 != name_objective ). % 9.23/9.28 % 9.23/9.28 fof(ax10,axiom, % 9.23/9.28 constr_CONST_1 != constr_CONST_2 ). % 9.23/9.28 % 9.23/9.28 fof(ax11,axiom, % 9.23/9.28 constr_CONST_1 != constr_CONST_3 ). % 9.23/9.28 % 9.23/9.28 fof(ax12,axiom, % 9.23/9.28 constr_CONST_1 != constr_CONST_4 ). % 9.23/9.28 % 9.23/9.28 fof(ax13,axiom, % 9.23/9.28 constr_CONST_1 != name_G_8 ). % 9.23/9.28 % 9.23/9.28 fof(ax14,axiom, % 9.23/9.28 constr_CONST_1 != name_Na ). % 9.23/9.28 % 9.23/9.28 fof(ax15,axiom, % 9.23/9.28 constr_CONST_1 != name_Nb ). % 9.23/9.28 % 9.23/9.28 fof(ax16,axiom, % 9.23/9.28 constr_CONST_1 != name_P_7 ). % 9.23/9.28 % 9.23/9.28 fof(ax17,axiom, % 9.23/9.28 constr_CONST_1 != name_c ). % 9.23/9.28 % 9.23/9.28 fof(ax18,axiom, % 9.23/9.28 constr_CONST_1 != name_objective ). % 9.23/9.28 % 9.23/9.28 fof(ax19,axiom, % 9.23/9.28 constr_CONST_2 != constr_CONST_3 ). % 9.23/9.28 % 9.23/9.28 fof(ax20,axiom, % 9.23/9.28 constr_CONST_2 != constr_CONST_4 ). % 9.23/9.28 % 9.23/9.28 fof(ax21,axiom, % 9.23/9.28 constr_CONST_2 != name_G_8 ). % 9.23/9.28 % 9.23/9.28 fof(ax22,axiom, % 9.23/9.28 constr_CONST_2 != name_Na ). % 9.23/9.28 % 9.23/9.28 fof(ax23,axiom, % 9.23/9.28 constr_CONST_2 != name_Nb ). % 9.23/9.28 % 9.23/9.28 fof(ax24,axiom, % 9.23/9.28 constr_CONST_2 != name_P_7 ). % 9.23/9.28 % 9.23/9.28 fof(ax25,axiom, % 9.23/9.28 constr_CONST_2 != name_c ). % 9.23/9.28 % 9.23/9.28 fof(ax26,axiom, % 9.23/9.28 constr_CONST_2 != name_objective ). % 9.23/9.28 % 9.23/9.28 fof(ax27,axiom, % 9.23/9.28 constr_CONST_3 != constr_CONST_4 ). % 9.23/9.28 % 9.23/9.28 fof(ax28,axiom, % 9.23/9.28 constr_CONST_3 != name_G_8 ). % 9.23/9.28 % 9.23/9.28 fof(ax29,axiom, % 9.23/9.28 constr_CONST_3 != name_Na ). % 9.23/9.29 % 9.23/9.29 fof(ax30,axiom, % 9.23/9.29 constr_CONST_3 != name_Nb ). % 9.23/9.29 % 9.23/9.29 fof(ax31,axiom, % 9.23/9.29 constr_CONST_3 != name_P_7 ). % 9.23/9.29 % 9.23/9.29 fof(ax32,axiom, % 9.23/9.29 constr_CONST_3 != name_c ). % 9.23/9.29 % 9.23/9.29 fof(ax33,axiom, % 9.23/9.29 constr_CONST_3 != name_objective ). % 9.23/9.29 % 9.23/9.29 fof(ax34,axiom, % 9.23/9.29 constr_CONST_4 != name_G_8 ). % 9.23/9.29 % 9.23/9.29 fof(ax35,axiom, % 9.23/9.29 constr_CONST_4 != name_Na ). % 9.23/9.29 % 9.23/9.29 fof(ax36,axiom, % 9.23/9.29 constr_CONST_4 != name_Nb ). % 9.23/9.29 % 9.23/9.29 fof(ax37,axiom, % 9.23/9.29 constr_CONST_4 != name_P_7 ). % 9.23/9.29 % 9.23/9.29 fof(ax38,axiom, % 9.23/9.29 constr_CONST_4 != name_c ). % 9.23/9.29 % 9.23/9.29 fof(ax39,axiom, % 9.23/9.29 constr_CONST_4 != name_objective ). % 9.23/9.29 % 9.23/9.29 fof(ax40,axiom, % 9.23/9.29 name_G_8 != name_Na ). % 9.23/9.29 % 9.23/9.29 fof(ax41,axiom, % 9.23/9.29 name_G_8 != name_Nb ). % 9.23/9.29 % 9.23/9.29 fof(ax42,axiom, % 9.23/9.29 name_G_8 != name_P_7 ). % 9.23/9.29 % 9.23/9.29 fof(ax43,axiom, % 9.23/9.29 name_G_8 != name_c ). % 9.23/9.29 % 9.23/9.29 fof(ax44,axiom, % 9.23/9.29 name_G_8 != name_objective ). % 9.23/9.29 % 9.23/9.29 fof(ax45,axiom, % 9.23/9.29 name_Na != name_Nb ). % 9.23/9.29 % 9.23/9.29 fof(ax46,axiom, % 9.23/9.29 name_Na != name_P_7 ). % 9.23/9.29 % 9.23/9.29 fof(ax47,axiom, % 9.23/9.29 name_Na != name_c ). % 9.23/9.29 % 9.23/9.29 fof(ax48,axiom, % 9.23/9.29 name_Na != name_objective ). % 9.23/9.29 % 9.23/9.29 fof(ax49,axiom, % 9.23/9.29 name_Nb != name_P_7 ). % 9.23/9.29 % 9.23/9.29 fof(ax50,axiom, % 9.23/9.29 name_Nb != name_c ). % 9.23/9.29 % 9.23/9.29 fof(ax51,axiom, % 9.23/9.29 name_Nb != name_objective ). % 9.23/9.29 % 9.23/9.29 fof(ax52,axiom, % 9.23/9.29 name_P_7 != name_c ). % 9.23/9.29 % 9.23/9.29 fof(ax53,axiom, % 9.23/9.29 name_P_7 != name_objective ). % 9.23/9.29 % 9.23/9.29 fof(ax54,axiom, % 9.23/9.29 name_c != name_objective ). % 9.23/9.29 % 9.23/9.29 fof(ax55,axiom, % 9.23/9.29 ! [VAR_K_0X30,VAR_M_0X30] : constr_dec(constr_enc(VAR_M_0X30,VAR_K_0X30),VAR_K_0X30) = VAR_M_0X30 ). % 9.23/9.29 % 9.23/9.29 fof(ax56,axiom, % 9.23/9.29 ! [VAR_G_0X30,VAR_P_0X30,VAR_X_0X30,VAR_Y_0X30] : constr_mod(constr_exp(constr_exp(VAR_G_0X30,VAR_X_0X30),VAR_Y_0X30),VAR_P_0X30) = constr_mod(constr_exp(constr_exp(VAR_G_0X30,VAR_Y_0X30),VAR_X_0X30),VAR_P_0X30) ). % 9.23/9.29 % 9.23/9.29 fof(ax57,axiom, % 9.23/9.29 pred_attacker(tuple_true) ). % 9.23/9.29 % 9.23/9.29 fof(ax58,axiom, % 9.23/9.29 ! [VAR_V_30X30,VAR_V_31] : % 9.23/9.29 ( ( pred_attacker(VAR_V_30X30) % 9.23/9.29 & pred_attacker(VAR_V_31) ) % 9.23/9.29 => pred_attacker(constr_mod(VAR_V_30X30,VAR_V_31)) ) ). % 9.23/9.29 % 9.23/9.29 fof(ax59,axiom, % 9.23/9.29 pred_attacker(tuple_false) ). % 9.23/9.29 % 9.23/9.29 fof(ax60,axiom, % 9.23/9.29 ! [VAR_V_34,VAR_V_35] : % 9.23/9.29 ( ( pred_attacker(VAR_V_34) % 9.23/9.29 & pred_attacker(VAR_V_35) ) % 9.23/9.29 => pred_attacker(constr_exp(VAR_V_34,VAR_V_35)) ) ). % 9.23/9.29 % 9.23/9.29 fof(ax61,axiom, % 9.23/9.29 ! [VAR_V_38,VAR_V_39] : % 9.23/9.29 ( ( pred_attacker(VAR_V_38) % 9.23/9.29 & pred_attacker(VAR_V_39) ) % 9.23/9.29 => pred_attacker(constr_enc(VAR_V_38,VAR_V_39)) ) ). % 9.23/9.29 % 9.23/9.29 fof(ax62,axiom, % 9.23/9.29 ! [VAR_V_42,VAR_V_43] : % 9.23/9.29 ( ( pred_attacker(VAR_V_42) % 9.23/9.29 & pred_attacker(VAR_V_43) ) % 9.23/9.29 => pred_attacker(constr_dec(VAR_V_42,VAR_V_43)) ) ). % 9.23/9.29 % 9.23/9.29 fof(ax63,axiom, % 9.23/9.29 pred_attacker(constr_CONST_4) ). % 9.23/9.29 % 9.23/9.29 fof(ax64,axiom, % 9.23/9.29 pred_attacker(constr_CONST_3) ). % 9.23/9.29 % 9.23/9.29 fof(ax65,axiom, % 9.23/9.29 pred_attacker(constr_CONST_2) ). % 9.23/9.29 % 9.23/9.29 fof(ax66,axiom, % 9.23/9.29 pred_attacker(constr_CONST_1) ). % 9.23/9.29 % 9.23/9.29 fof(ax67,axiom, % 9.23/9.29 pred_attacker(constr_CONST_0x30) ). % 9.23/9.29 % 9.23/9.29 fof(ax68,axiom, % 9.23/9.29 ! [VAR_V_45] : % 9.23/9.29 ( pred_attacker(VAR_V_45) % 9.23/9.29 => pred_attacker(tuple_B_out_3(VAR_V_45)) ) ). % 9.23/9.29 % 9.23/9.29 fof(ax69,axiom, % 9.23/9.29 ! [VAR_V_48] : % 9.23/9.29 ( pred_attacker(tuple_B_out_3(VAR_V_48)) % 9.23/9.29 => pred_attacker(VAR_V_48) ) ). % 9.23/9.29 % 9.23/9.29 fof(ax70,axiom, % 9.23/9.29 ! [VAR_V_51] : % 9.23/9.29 ( pred_attacker(VAR_V_51) % 9.23/9.29 => pred_attacker(tuple_B_in_2(VAR_V_51)) ) ). % 9.23/9.29 % 9.23/9.29 fof(ax71,axiom, % 9.23/9.29 ! [VAR_V_54] : % 9.23/9.29 ( pred_attacker(tuple_B_in_2(VAR_V_54)) % 9.23/9.29 => pred_attacker(VAR_V_54) ) ). % 9.23/9.29 % 9.23/9.29 fof(ax72,axiom, % 9.23/9.29 ! [VAR_V_58,VAR_V_59] : % 9.23/9.29 ( ( pred_attacker(VAR_V_58) % 9.23/9.29 & pred_attacker(VAR_V_59) ) % 9.23/9.29 => pred_attacker(tuple_B_in_1(VAR_V_58,VAR_V_59)) ) ). % 9.23/9.29 % 9.23/9.29 fof(ax73,axiom, % 9.23/9.29 ! [VAR_V_66,VAR_V_67] : % 9.23/9.29 ( pred_attacker(tuple_B_in_1(VAR_V_66,VAR_V_67)) % 9.23/9.29 => pred_attacker(VAR_V_66) ) ). % 9.23/9.29 % 9.23/9.29 fof(ax74,axiom, % 9.23/9.29 ! [VAR_V_69,VAR_V_70X30] : % 9.23/9.29 ( pred_attacker(tuple_B_in_1(VAR_V_69,VAR_V_70X30)) % 9.23/9.29 => pred_attacker(VAR_V_70X30) ) ). % 9.23/9.29 % 9.23/9.29 fof(ax75,axiom, % 9.23/9.29 ! [VAR_V_73] : % 9.23/9.29 ( pred_attacker(VAR_V_73) % 9.23/9.29 => pred_attacker(tuple_A_out_4(VAR_V_73)) ) ). % 9.23/9.29 % 9.23/9.29 fof(ax76,axiom, % 9.23/9.29 ! [VAR_V_76] : % 9.23/9.29 ( pred_attacker(tuple_A_out_4(VAR_V_76)) % 9.23/9.29 => pred_attacker(VAR_V_76) ) ). % 9.23/9.29 % 9.23/9.29 fof(ax77,axiom, % 9.23/9.29 ! [VAR_V_79] : % 9.23/9.29 ( pred_attacker(VAR_V_79) % 9.23/9.29 => pred_attacker(tuple_A_out_2(VAR_V_79)) ) ). % 9.23/9.29 % 9.23/9.29 fof(ax78,axiom, % 9.23/9.29 ! [VAR_V_82] : % 9.23/9.29 ( pred_attacker(tuple_A_out_2(VAR_V_82)) % 9.23/9.29 => pred_attacker(VAR_V_82) ) ). % 9.23/9.29 % 9.23/9.29 fof(ax79,axiom, % 9.23/9.29 ! [VAR_V_86,VAR_V_87] : % 9.23/9.29 ( ( pred_attacker(VAR_V_86) % 9.23/9.29 & pred_attacker(VAR_V_87) ) % 9.23/9.29 => pred_attacker(tuple_A_out_1(VAR_V_86,VAR_V_87)) ) ). % 9.23/9.29 % 9.23/9.29 fof(ax80,axiom, % 9.23/9.29 ! [VAR_V_94,VAR_V_95] : % 9.23/9.29 ( pred_attacker(tuple_A_out_1(VAR_V_94,VAR_V_95)) % 9.23/9.29 => pred_attacker(VAR_V_94) ) ). % 9.23/9.29 % 9.23/9.29 fof(ax81,axiom, % 9.23/9.29 ! [VAR_V_97,VAR_V_98] : % 9.23/9.29 ( pred_attacker(tuple_A_out_1(VAR_V_97,VAR_V_98)) % 9.23/9.29 => pred_attacker(VAR_V_98) ) ). % 9.23/9.29 % 9.23/9.29 fof(ax82,axiom, % 9.23/9.29 ! [VAR_V_10X301] : % 9.23/9.29 ( pred_attacker(VAR_V_10X301) % 9.23/9.29 => pred_attacker(tuple_A_in_3(VAR_V_10X301)) ) ). % 9.23/9.29 % 9.23/9.29 fof(ax83,axiom, % 9.23/9.29 ! [VAR_V_10X304] : % 9.23/9.29 ( pred_attacker(tuple_A_in_3(VAR_V_10X304)) % 9.23/9.29 => pred_attacker(VAR_V_10X304) ) ). % 9.23/9.29 % 9.23/9.29 fof(ax84,axiom, % 9.23/9.29 ! [VAR_V_110X30,VAR_V_111] : % 9.23/9.29 ( ( pred_mess(VAR_V_111,VAR_V_110X30) % 9.23/9.29 & pred_attacker(VAR_V_111) ) % 9.23/9.29 => pred_attacker(VAR_V_110X30) ) ). % 9.23/9.29 % 9.23/9.29 fof(ax85,axiom, % 9.23/9.29 ! [VAR_V_112,VAR_V_113] : % 9.23/9.29 ( ( pred_attacker(VAR_V_113) % 9.23/9.29 & pred_attacker(VAR_V_112) ) % 9.23/9.29 => pred_mess(VAR_V_113,VAR_V_112) ) ). % 9.23/9.29 % 9.23/9.29 fof(ax86,axiom, % 9.23/9.29 pred_attacker(name_c) ). % 9.23/9.29 % 9.23/9.29 fof(ax87,axiom, % 9.23/9.29 ! [VAR_V_115] : pred_equal(VAR_V_115,VAR_V_115) ). % 9.23/9.29 % 9.23/9.29 fof(ax88,axiom, % 9.23/9.29 ! [VAR_V_116] : pred_attacker(name_new0x2Dname(VAR_V_116)) ). % 9.23/9.29 % 9.23/9.29 fof(ax89,axiom, % 9.23/9.29 pred_attacker(tuple_A_out_1(name_P_7,name_G_8)) ). % 9.23/9.29 % 9.23/9.29 fof(ax90,axiom, % 9.23/9.29 pred_attacker(tuple_A_out_2(constr_mod(constr_exp(name_G_8,name_Na),name_P_7))) ). % 9.23/9.29 % 9.23/9.29 fof(ax91,axiom, % 9.23/9.29 ! [VAR_B_186] : % 9.23/9.29 ( pred_attacker(tuple_A_in_3(VAR_B_186)) % 9.23/9.29 => pred_attacker(tuple_A_out_4(constr_enc(name_objective,constr_mod(constr_exp(VAR_B_186,name_Na),name_P_7)))) ) ). % 9.23/9.29 % 9.23/9.29 fof(ax92,axiom, % 9.23/9.29 ! [VAR_A_219,VAR_G_221,VAR_P_220X30] : % 9.23/9.29 ( ( pred_attacker(tuple_B_in_2(VAR_A_219)) % 9.23/9.29 & pred_attacker(tuple_B_in_1(VAR_P_220X30,VAR_G_221)) ) % 9.23/9.29 => pred_attacker(tuple_B_out_3(constr_mod(constr_exp(VAR_G_221,name_Nb),VAR_P_220X30))) ) ). % 9.23/9.29 % 9.23/9.29 fof(co0,conjecture, % 9.23/9.29 pred_attacker(name_objective) ). % 9.23/9.29 % 9.23/9.29 %-------------------------------------------------------------------------- % 9.23/9.29 %------------------------------------------- % 9.23/9.29 % Proof found % 9.23/9.29 % SZS status Theorem for theBenchmark % 9.23/9.29 % SZS output start Proof % 9.23/9.29 %ClaNum:120(EqnAxiom:26) % 9.23/9.29 %VarNum:86(SingletonVarNum:46) % 9.23/9.29 %MaxLitNum:3 % 9.23/9.29 %MaxfuncDepth:4 % 9.23/9.29 %SharedTerms:83 % 9.23/9.29 %goalClause: 96 % 9.23/9.29 %singleGoalClaCount:1 % 9.23/9.29 [27]P1(a1) % 9.23/9.29 [28]P1(a2) % 9.23/9.29 [29]P1(a3) % 9.23/9.29 [30]P1(a4) % 9.23/9.29 [31]P1(a5) % 9.23/9.29 [32]P1(a6) % 9.23/9.29 [33]P1(a15) % 9.23/9.29 [34]P1(a16) % 9.23/9.29 [41]~E(a1,a2) % 9.23/9.29 [42]~E(a1,a3) % 9.23/9.29 [43]~E(a3,a2) % 9.23/9.29 [44]~E(a1,a4) % 9.23/9.29 [45]~E(a4,a2) % 9.23/9.29 [46]~E(a4,a3) % 9.23/9.29 [47]~E(a1,a5) % 9.23/9.29 [48]~E(a5,a2) % 9.23/9.29 [49]~E(a5,a3) % 9.23/9.29 [50]~E(a5,a4) % 9.23/9.29 [51]~E(a1,a8) % 9.23/9.29 [52]~E(a8,a2) % 9.23/9.29 [53]~E(a8,a3) % 9.23/9.29 [54]~E(a8,a4) % 9.23/9.29 [55]~E(a8,a5) % 9.23/9.29 [56]~E(a1,a13) % 9.23/9.29 [57]~E(a13,a2) % 9.23/9.29 [58]~E(a13,a3) % 9.23/9.29 [59]~E(a13,a4) % 9.23/9.29 [60]~E(a13,a5) % 9.23/9.29 [61]~E(a13,a8) % 9.23/9.29 [62]~E(a1,a14) % 9.23/9.29 [63]~E(a14,a2) % 9.23/9.29 [64]~E(a14,a3) % 9.23/9.29 [65]~E(a14,a4) % 9.23/9.30 [66]~E(a14,a5) % 9.23/9.30 [67]~E(a14,a8) % 9.23/9.30 [68]~E(a14,a13) % 9.23/9.30 [69]~E(a1,a7) % 9.23/9.30 [70]~E(a7,a2) % 9.23/9.30 [71]~E(a7,a3) % 9.23/9.30 [72]~E(a7,a4) % 9.23/9.30 [73]~E(a7,a5) % 9.23/9.30 [74]~E(a8,a7) % 9.23/9.30 [75]~E(a13,a7) % 9.23/9.30 [76]~E(a14,a7) % 9.23/9.30 [77]~E(a1,a6) % 9.23/9.30 [78]~E(a6,a2) % 9.23/9.30 [79]~E(a6,a3) % 9.23/9.30 [80]~E(a6,a4) % 9.23/9.30 [81]~E(a6,a5) % 9.23/9.30 [82]~E(a8,a6) % 9.23/9.30 [83]~E(a13,a6) % 9.23/9.30 [84]~E(a14,a6) % 9.23/9.30 [85]~E(a7,a6) % 9.23/9.30 [86]~E(a1,a19) % 9.23/9.30 [87]~E(a19,a2) % 9.23/9.30 [88]~E(a19,a3) % 9.23/9.30 [89]~E(a19,a4) % 9.23/9.30 [90]~E(a19,a5) % 9.23/9.30 [91]~E(a19,a8) % 9.23/9.30 [92]~E(a19,a13) % 9.23/9.30 [93]~E(a14,a19) % 9.23/9.30 [94]~E(a19,a7) % 9.23/9.30 [95]~E(a19,a6) % 9.23/9.30 [96]~P1(a19) % 9.23/9.30 [37]P1(f18(a7,a8)) % 9.23/9.30 [39]P1(f21(f12(f11(a8,a13),a7))) % 9.23/9.30 [36]P2(x361,x361) % 9.23/9.30 [35]P1(f17(x351)) % 9.23/9.30 [38]E(f10(f9(x381,x382),x382),x381) % 9.23/9.30 [40]E(f12(f11(f11(x401,x402),x403),x404),f12(f11(f11(x401,x403),x402),x404)) % 9.23/9.30 [97]~P1(x971)+P1(f22(x971)) % 9.23/9.30 [98]~P1(x981)+P1(f23(x981)) % 9.23/9.30 [99]~P1(x991)+P1(f24(x991)) % 9.23/9.30 [100]~P1(x1001)+P1(f21(x1001)) % 9.23/9.30 [101]~P1(x1011)+P1(f20(x1011)) % 9.23/9.30 [102]P1(x1021)+~P1(f22(x1021)) % 9.23/9.30 [103]P1(x1031)+~P1(f23(x1031)) % 9.23/9.30 [104]P1(x1041)+~P1(f24(x1041)) % 9.23/9.30 [105]P1(x1051)+~P1(f21(x1051)) % 9.23/9.30 [106]P1(x1061)+~P1(f20(x1061)) % 9.23/9.30 [120]~P1(f20(x1201))+P1(f24(f9(a19,f12(f11(x1201,a13),a7)))) % 9.23/9.30 [115]P1(x1151)+~P1(f25(x1152,x1151)) % 9.23/9.30 [116]P1(x1161)+~P1(f18(x1162,x1161)) % 9.23/9.30 [117]P1(x1171)+~P1(f25(x1171,x1172)) % 9.23/9.30 [118]P1(x1181)+~P1(f18(x1181,x1182)) % 9.23/9.30 [107]~P1(x1072)+~P1(x1071)+P3(x1071,x1072) % 9.23/9.30 [108]~P3(x1082,x1081)+P1(x1081)+~P1(x1082) % 9.23/9.30 [109]~P1(x1092)+~P1(x1091)+P1(f9(x1091,x1092)) % 9.23/9.30 [110]~P1(x1102)+~P1(x1101)+P1(f10(x1101,x1102)) % 9.23/9.30 [111]~P1(x1112)+~P1(x1111)+P1(f11(x1111,x1112)) % 9.23/9.30 [112]~P1(x1122)+~P1(x1121)+P1(f12(x1121,x1122)) % 9.23/9.30 [113]~P1(x1132)+~P1(x1131)+P1(f25(x1131,x1132)) % 9.23/9.30 [114]~P1(x1142)+~P1(x1141)+P1(f18(x1141,x1142)) % 9.23/9.30 [119]~P1(f25(x1192,x1191))+~P1(f23(x1193))+P1(f22(f12(f11(x1191,a14),x1192))) % 9.23/9.30 %EqnAxiom % 9.23/9.30 [1]E(x11,x11) % 9.23/9.30 [2]E(x22,x21)+~E(x21,x22) % 9.23/9.30 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 9.23/9.30 [4]~E(x41,x42)+E(f17(x41),f17(x42)) % 9.23/9.30 [5]~E(x51,x52)+E(f18(x51,x53),f18(x52,x53)) % 9.23/9.30 [6]~E(x61,x62)+E(f18(x63,x61),f18(x63,x62)) % 9.23/9.30 [7]~E(x71,x72)+E(f9(x71,x73),f9(x72,x73)) % 9.23/9.30 [8]~E(x81,x82)+E(f9(x83,x81),f9(x83,x82)) % 9.23/9.30 [9]~E(x91,x92)+E(f10(x91,x93),f10(x92,x93)) % 9.23/9.30 [10]~E(x101,x102)+E(f10(x103,x101),f10(x103,x102)) % 9.23/9.30 [11]~E(x111,x112)+E(f11(x111,x113),f11(x112,x113)) % 9.23/9.30 [12]~E(x121,x122)+E(f11(x123,x121),f11(x123,x122)) % 9.23/9.30 [13]~E(x131,x132)+E(f12(x131,x133),f12(x132,x133)) % 9.23/9.30 [14]~E(x141,x142)+E(f12(x143,x141),f12(x143,x142)) % 9.23/9.30 [15]~E(x151,x152)+E(f21(x151),f21(x152)) % 9.23/9.30 [16]~E(x161,x162)+E(f23(x161),f23(x162)) % 9.23/9.30 [17]~E(x171,x172)+E(f22(x171),f22(x172)) % 9.23/9.30 [18]~E(x181,x182)+E(f25(x181,x183),f25(x182,x183)) % 9.23/9.30 [19]~E(x191,x192)+E(f25(x193,x191),f25(x193,x192)) % 9.23/9.30 [20]~E(x201,x202)+E(f20(x201),f20(x202)) % 9.23/9.30 [21]~E(x211,x212)+E(f24(x211),f24(x212)) % 9.23/9.30 [22]~P1(x221)+P1(x222)+~E(x221,x222) % 9.23/9.30 [23]P3(x232,x233)+~E(x231,x232)+~P3(x231,x233) % 9.23/9.30 [24]P3(x243,x242)+~E(x241,x242)+~P3(x243,x241) % 9.23/9.30 [25]P2(x252,x253)+~E(x251,x252)+~P2(x251,x253) % 9.23/9.30 [26]P2(x263,x262)+~E(x261,x262)+~P2(x263,x261) % 9.23/9.30 % 9.23/9.30 %------------------------------------------- % 9.23/9.30 cnf(121,plain, % 9.23/9.30 (P1(f12(f11(a8,a13),a7))), % 9.23/9.30 inference(scs_inference,[],[39,105])). % 9.23/9.30 cnf(123,plain, % 9.23/9.30 (P1(a8)), % 9.23/9.30 inference(scs_inference,[],[37,39,105,116])). % 9.23/9.30 cnf(130,plain, % 9.23/9.30 (~P1(f10(f9(a19,x1301),x1301))), % 9.23/9.30 inference(scs_inference,[],[96,27,38,37,39,105,116,118,2,108,22])). % 9.23/9.30 cnf(142,plain, % 9.23/9.30 (~P1(f9(a19,f12(f11(a8,a13),a7)))), % 9.23/9.30 inference(scs_inference,[],[96,130,121,108,110])). % 9.23/9.30 cnf(1256,plain, % 9.23/9.30 (~P1(f20(a8))), % 9.23/9.30 inference(scs_inference,[],[142,104,120])). % 9.23/9.30 cnf(1257,plain, % 9.23/9.30 ($false), % 9.23/9.30 inference(scs_inference,[],[123,1256,101]), % 9.23/9.30 ['proof']). % 9.23/9.30 % SZS output end Proof % 9.23/9.30 % Total time :8.660000s %------------------------------------------------------------------------------