%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWW950+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 : n013.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:36 EDT 2024 % Result : Theorem 3.26s 3.35s % Output : CNFRefutation 3.26s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWW950+1 : TPTP v8.2.0. Released v7.4.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n013.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Wed Jun 19 05:06:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.20/0.55 start to proof:theBenchmark % 3.26/3.33 %------------------------------------------- % 3.26/3.33 % File :CSE---1.7 % 3.26/3.33 % Problem :theBenchmark % 3.26/3.33 % Transform :cnf % 3.26/3.33 % Format :tptp:raw % 3.26/3.33 % Command :java -jar mcs_scs.jar %d %s % 3.26/3.33 % 3.26/3.33 % Result :Theorem 2.750000s % 3.26/3.33 % Output :CNFRefutation 2.750000s % 3.26/3.33 %------------------------------------------- % 3.26/3.34 %-------------------------------------------------------------------------- % 3.26/3.34 % File : SWW950+1 : TPTP v8.2.0. Released v7.4.0. % 3.26/3.34 % Domain : Software Verification % 3.26/3.34 % Problem : Attack on LD07 protocol % 3.26/3.34 % Version : [LT19] axioms : Especial. % 3.26/3.34 % English : Attack demonstrates violation of aliveness property of tag % 3.26/3.34 % : guaranteed to reader. % 3.26/3.34 % 3.26/3.34 % Refs : [BO97] Bull & Otway (1997), The Authentication Protocol % 3.26/3.34 % : [RS98] Ryan & Schneider (1998), An Attack on a Recursive Auth % 3.26/3.34 % : [LT19] Li & Tiu (2019), Combining ProVerif and Automated Theo % 3.26/3.34 % : [Li20] Li (2020), Email to Geoff Sutcliffe % 3.26/3.34 % Source : [Li20] % 3.26/3.34 % Names : LD07-tag-auth.p [LT20] % 3.26/3.34 % 3.26/3.34 % Status : Theorem % 3.26/3.34 % Rating : 0.36 v8.2.0, 0.39 v7.5.0, 0.41 v7.4.0 % 3.26/3.34 % Syntax : Number of formulae : 76 ( 61 unt; 0 def) % 3.26/3.34 % Number of atoms : 96 ( 49 equ) % 3.26/3.34 % Maximal formula atoms : 3 ( 1 avg) % 3.26/3.34 % Number of connectives : 65 ( 45 ~; 0 |; 5 &) % 3.26/3.34 % ( 0 <=>; 15 =>; 0 <=; 0 <~>) % 3.26/3.34 % Maximal formula depth : 5 ( 2 avg) % 3.26/3.34 % Maximal term depth : 5 ( 1 avg) % 3.26/3.34 % Number of predicates : 4 ( 3 usr; 0 prp; 1-2 aty) % 3.26/3.34 % Number of functors : 19 ( 19 usr; 12 con; 0-2 aty) % 3.26/3.34 % Number of variables : 31 ( 31 !; 0 ?) % 3.26/3.34 % SPC : FOF_THM_RFO_SEQ % 3.26/3.34 % 3.26/3.34 % Comments : Generated by a modified version of ProVerif used in the % 3.26/3.34 % ProVerif-ATP project [LT19]. % 3.26/3.34 %-------------------------------------------------------------------------- % 3.26/3.34 fof(ax0,axiom, % 3.26/3.34 constr_CONST_0x30 != constr_CONST_1 ). % 3.26/3.34 % 3.26/3.34 fof(ax1,axiom, % 3.26/3.34 constr_CONST_0x30 != constr_CONST_2 ). % 3.26/3.34 % 3.26/3.34 fof(ax2,axiom, % 3.26/3.34 constr_CONST_0x30 != constr_CONST_3 ). % 3.26/3.34 % 3.26/3.34 fof(ax3,axiom, % 3.26/3.34 constr_CONST_0x30 != constr_CONST_4 ). % 3.26/3.34 % 3.26/3.34 fof(ax4,axiom, % 3.26/3.34 constr_CONST_0x30 != constr_ZERO ). % 3.26/3.34 % 3.26/3.34 fof(ax5,axiom, % 3.26/3.34 constr_CONST_0x30 != name_c ). % 3.26/3.34 % 3.26/3.34 fof(ax6,axiom, % 3.26/3.34 constr_CONST_0x30 != name_k0x30 ). % 3.26/3.34 % 3.26/3.34 fof(ax7,axiom, % 3.26/3.34 constr_CONST_0x30 != name_ki ). % 3.26/3.34 % 3.26/3.34 fof(ax8,axiom, % 3.26/3.34 constr_CONST_0x30 != name_objective ). % 3.26/3.34 % 3.26/3.34 fof(ax9,axiom, % 3.26/3.34 constr_CONST_1 != constr_CONST_2 ). % 3.26/3.34 % 3.26/3.34 fof(ax10,axiom, % 3.26/3.34 constr_CONST_1 != constr_CONST_3 ). % 3.26/3.34 % 3.26/3.34 fof(ax11,axiom, % 3.26/3.34 constr_CONST_1 != constr_CONST_4 ). % 3.26/3.34 % 3.26/3.34 fof(ax12,axiom, % 3.26/3.34 constr_CONST_1 != constr_ZERO ). % 3.26/3.34 % 3.26/3.34 fof(ax13,axiom, % 3.26/3.34 constr_CONST_1 != name_c ). % 3.26/3.34 % 3.26/3.34 fof(ax14,axiom, % 3.26/3.34 constr_CONST_1 != name_k0x30 ). % 3.26/3.34 % 3.26/3.34 fof(ax15,axiom, % 3.26/3.34 constr_CONST_1 != name_ki ). % 3.26/3.34 % 3.26/3.34 fof(ax16,axiom, % 3.26/3.34 constr_CONST_1 != name_objective ). % 3.26/3.34 % 3.26/3.34 fof(ax17,axiom, % 3.26/3.34 constr_CONST_2 != constr_CONST_3 ). % 3.26/3.34 % 3.26/3.34 fof(ax18,axiom, % 3.26/3.34 constr_CONST_2 != constr_CONST_4 ). % 3.26/3.34 % 3.26/3.34 fof(ax19,axiom, % 3.26/3.34 constr_CONST_2 != constr_ZERO ). % 3.26/3.34 % 3.26/3.34 fof(ax20,axiom, % 3.26/3.34 constr_CONST_2 != name_c ). % 3.26/3.34 % 3.26/3.34 fof(ax21,axiom, % 3.26/3.34 constr_CONST_2 != name_k0x30 ). % 3.26/3.34 % 3.26/3.34 fof(ax22,axiom, % 3.26/3.34 constr_CONST_2 != name_ki ). % 3.26/3.34 % 3.26/3.34 fof(ax23,axiom, % 3.26/3.34 constr_CONST_2 != name_objective ). % 3.26/3.34 % 3.26/3.34 fof(ax24,axiom, % 3.26/3.34 constr_CONST_3 != constr_CONST_4 ). % 3.26/3.34 % 3.26/3.34 fof(ax25,axiom, % 3.26/3.34 constr_CONST_3 != constr_ZERO ). % 3.26/3.34 % 3.26/3.34 fof(ax26,axiom, % 3.26/3.34 constr_CONST_3 != name_c ). % 3.26/3.34 % 3.26/3.34 fof(ax27,axiom, % 3.26/3.34 constr_CONST_3 != name_k0x30 ). % 3.26/3.34 % 3.26/3.34 fof(ax28,axiom, % 3.26/3.34 constr_CONST_3 != name_ki ). % 3.26/3.34 % 3.26/3.34 fof(ax29,axiom, % 3.26/3.34 constr_CONST_3 != name_objective ). % 3.26/3.34 % 3.26/3.34 fof(ax30,axiom, % 3.26/3.34 constr_CONST_4 != constr_ZERO ). % 3.26/3.34 % 3.26/3.34 fof(ax31,axiom, % 3.26/3.34 constr_CONST_4 != name_c ). % 3.26/3.34 % 3.26/3.34 fof(ax32,axiom, % 3.26/3.34 constr_CONST_4 != name_k0x30 ). % 3.26/3.34 % 3.26/3.34 fof(ax33,axiom, % 3.26/3.34 constr_CONST_4 != name_ki ). % 3.26/3.34 % 3.26/3.34 fof(ax34,axiom, % 3.26/3.34 constr_CONST_4 != name_objective ). % 3.26/3.34 % 3.26/3.34 fof(ax35,axiom, % 3.26/3.34 constr_ZERO != name_c ). % 3.26/3.34 % 3.26/3.34 fof(ax36,axiom, % 3.26/3.34 constr_ZERO != name_k0x30 ). % 3.26/3.34 % 3.26/3.34 fof(ax37,axiom, % 3.26/3.34 constr_ZERO != name_ki ). % 3.26/3.34 % 3.26/3.34 fof(ax38,axiom, % 3.26/3.34 constr_ZERO != name_objective ). % 3.26/3.34 % 3.26/3.34 fof(ax39,axiom, % 3.26/3.34 name_c != name_k0x30 ). % 3.26/3.34 % 3.26/3.34 fof(ax40,axiom, % 3.26/3.34 name_c != name_ki ). % 3.26/3.34 % 3.26/3.34 fof(ax41,axiom, % 3.26/3.34 name_c != name_objective ). % 3.26/3.34 % 3.26/3.34 fof(ax42,axiom, % 3.26/3.34 name_k0x30 != name_ki ). % 3.26/3.34 % 3.26/3.34 fof(ax43,axiom, % 3.26/3.34 name_k0x30 != name_objective ). % 3.26/3.34 % 3.26/3.34 fof(ax44,axiom, % 3.26/3.34 name_ki != name_objective ). % 3.26/3.34 % 3.26/3.34 fof(ax45,axiom, % 3.26/3.34 ! [VAR_X_10X30] : constr_xor(VAR_X_10X30,VAR_X_10X30) = constr_ZERO ). % 3.26/3.34 % 3.26/3.34 fof(ax46,axiom, % 3.26/3.34 ! [VAR_X_9] : constr_xor(VAR_X_9,constr_ZERO) = VAR_X_9 ). % 3.26/3.34 % 3.26/3.34 fof(ax47,axiom, % 3.26/3.34 ! [VAR_X_7,VAR_Y_8] : constr_xor(VAR_X_7,VAR_Y_8) = constr_xor(VAR_Y_8,VAR_X_7) ). % 3.26/3.34 % 3.26/3.34 fof(ax48,axiom, % 3.26/3.34 ! [VAR_X_0X30,VAR_Y_0X30,VAR_Z_0X30] : constr_xor(VAR_X_0X30,constr_xor(VAR_Y_0X30,VAR_Z_0X30)) = constr_xor(constr_xor(VAR_X_0X30,VAR_Y_0X30),VAR_Z_0X30) ). % 3.26/3.34 % 3.26/3.34 fof(ax49,axiom, % 3.26/3.34 ! [VAR_V_29,VAR_V_30X30] : % 3.26/3.34 ( ( pred_attacker(VAR_V_29) % 3.26/3.34 & pred_attacker(VAR_V_30X30) ) % 3.26/3.34 => pred_attacker(constr_xor(VAR_V_29,VAR_V_30X30)) ) ). % 3.26/3.34 % 3.26/3.34 fof(ax50,axiom, % 3.26/3.34 pred_attacker(tuple_true) ). % 3.26/3.35 % 3.26/3.35 fof(ax51,axiom, % 3.26/3.35 ! [VAR_V_33] : % 3.26/3.35 ( pred_attacker(VAR_V_33) % 3.26/3.35 => pred_attacker(constr_h(VAR_V_33)) ) ). % 3.26/3.35 % 3.26/3.35 fof(ax52,axiom, % 3.26/3.35 pred_attacker(tuple_false) ). % 3.26/3.35 % 3.26/3.35 fof(ax53,axiom, % 3.26/3.35 pred_attacker(constr_ZERO) ). % 3.26/3.35 % 3.26/3.35 fof(ax54,axiom, % 3.26/3.35 ! [VAR_V_35] : % 3.26/3.35 ( pred_attacker(VAR_V_35) % 3.26/3.35 => pred_attacker(tuple_T_out_4(VAR_V_35)) ) ). % 3.26/3.35 % 3.26/3.35 fof(ax55,axiom, % 3.26/3.35 ! [VAR_V_38] : % 3.26/3.35 ( pred_attacker(tuple_T_out_4(VAR_V_38)) % 3.26/3.35 => pred_attacker(VAR_V_38) ) ). % 3.26/3.35 % 3.26/3.35 fof(ax56,axiom, % 3.26/3.35 ! [VAR_V_41] : % 3.26/3.35 ( pred_attacker(VAR_V_41) % 3.26/3.35 => pred_attacker(tuple_T_out_2(VAR_V_41)) ) ). % 3.26/3.35 % 3.26/3.35 fof(ax57,axiom, % 3.26/3.35 ! [VAR_V_44] : % 3.26/3.35 ( pred_attacker(tuple_T_out_2(VAR_V_44)) % 3.26/3.35 => pred_attacker(VAR_V_44) ) ). % 3.26/3.35 % 3.26/3.35 fof(ax58,axiom, % 3.26/3.35 ! [VAR_V_48,VAR_V_49] : % 3.26/3.35 ( ( pred_attacker(VAR_V_48) % 3.26/3.35 & pred_attacker(VAR_V_49) ) % 3.26/3.35 => pred_attacker(tuple_T_in_3(VAR_V_48,VAR_V_49)) ) ). % 3.26/3.35 % 3.26/3.35 fof(ax59,axiom, % 3.26/3.35 ! [VAR_V_56,VAR_V_57] : % 3.26/3.35 ( pred_attacker(tuple_T_in_3(VAR_V_56,VAR_V_57)) % 3.26/3.35 => pred_attacker(VAR_V_56) ) ). % 3.26/3.35 % 3.26/3.35 fof(ax60,axiom, % 3.26/3.35 ! [VAR_V_59,VAR_V_60X30] : % 3.26/3.35 ( pred_attacker(tuple_T_in_3(VAR_V_59,VAR_V_60X30)) % 3.26/3.35 => pred_attacker(VAR_V_60X30) ) ). % 3.26/3.35 % 3.26/3.35 fof(ax61,axiom, % 3.26/3.35 ! [VAR_V_63] : % 3.26/3.35 ( pred_attacker(VAR_V_63) % 3.26/3.35 => pred_attacker(tuple_T_in_1(VAR_V_63)) ) ). % 3.26/3.35 % 3.26/3.35 fof(ax62,axiom, % 3.26/3.35 ! [VAR_V_66] : % 3.26/3.35 ( pred_attacker(tuple_T_in_1(VAR_V_66)) % 3.26/3.35 => pred_attacker(VAR_V_66) ) ). % 3.26/3.35 % 3.26/3.35 fof(ax63,axiom, % 3.26/3.35 pred_attacker(constr_CONST_4) ). % 3.26/3.35 % 3.26/3.35 fof(ax64,axiom, % 3.26/3.35 pred_attacker(constr_CONST_3) ). % 3.26/3.35 % 3.26/3.35 fof(ax65,axiom, % 3.26/3.35 pred_attacker(constr_CONST_2) ). % 3.26/3.35 % 3.26/3.35 fof(ax66,axiom, % 3.26/3.35 pred_attacker(constr_CONST_1) ). % 3.26/3.35 % 3.26/3.35 fof(ax67,axiom, % 3.26/3.35 pred_attacker(constr_CONST_0x30) ). % 3.26/3.35 % 3.26/3.35 fof(ax68,axiom, % 3.26/3.35 ! [VAR_V_72,VAR_V_73] : % 3.26/3.35 ( ( pred_mess(VAR_V_73,VAR_V_72) % 3.26/3.35 & pred_attacker(VAR_V_73) ) % 3.26/3.35 => pred_attacker(VAR_V_72) ) ). % 3.26/3.35 % 3.26/3.35 fof(ax69,axiom, % 3.26/3.35 ! [VAR_V_74,VAR_V_75] : % 3.26/3.35 ( ( pred_attacker(VAR_V_75) % 3.26/3.35 & pred_attacker(VAR_V_74) ) % 3.26/3.35 => pred_mess(VAR_V_75,VAR_V_74) ) ). % 3.26/3.35 % 3.26/3.35 fof(ax70,axiom, % 3.26/3.35 pred_attacker(name_c) ). % 3.26/3.35 % 3.26/3.35 fof(ax71,axiom, % 3.26/3.35 ! [VAR_V_77] : pred_equal(VAR_V_77,VAR_V_77) ). % 3.26/3.35 % 3.26/3.35 fof(ax72,axiom, % 3.26/3.35 ! [VAR_V_78] : pred_attacker(name_new0x2Dname(VAR_V_78)) ). % 3.26/3.35 % 3.26/3.35 fof(ax73,axiom, % 3.26/3.35 ! [VAR_R_10X308] : % 3.26/3.35 ( pred_attacker(tuple_T_in_1(VAR_R_10X308)) % 3.26/3.35 => pred_attacker(tuple_T_out_2(constr_h(constr_xor(VAR_R_10X308,constr_xor(name_k0x30,name_ki))))) ) ). % 3.26/3.35 % 3.26/3.35 fof(ax74,axiom, % 3.26/3.35 ! [VAR_A_143,VAR_R_144] : % 3.26/3.35 ( ( pred_attacker(tuple_T_in_3(VAR_A_143,constr_h(constr_xor(VAR_A_143,constr_xor(name_k0x30,name_ki))))) % 3.26/3.35 & pred_attacker(tuple_T_in_1(VAR_R_144)) ) % 3.26/3.35 => pred_attacker(tuple_T_out_4(name_objective)) ) ). % 3.26/3.35 % 3.26/3.35 fof(co0,conjecture, % 3.26/3.35 pred_attacker(name_objective) ). % 3.26/3.35 % 3.26/3.35 %-------------------------------------------------------------------------- % 3.26/3.35 %------------------------------------------- % 3.26/3.35 % Proof found % 3.26/3.35 % SZS status Theorem for theBenchmark % 3.26/3.35 % SZS output start Proof % 3.26/3.35 %ClaNum:93(EqnAxiom:17) % 3.26/3.35 %VarNum:58(SingletonVarNum:31) % 3.26/3.35 %MaxLitNum:3 % 3.26/3.35 %MaxfuncDepth:4 % 3.26/3.35 %SharedTerms:70 % 3.26/3.35 %goalClause: 78 % 3.26/3.35 %singleGoalClaCount:1 % 3.26/3.35 [18]P1(a1) % 3.26/3.35 [19]P1(a2) % 3.26/3.35 [20]P1(a3) % 3.26/3.35 [21]P1(a4) % 3.26/3.35 [22]P1(a5) % 3.26/3.35 [23]P1(a6) % 3.26/3.35 [24]P1(a7) % 3.26/3.35 [25]P1(a10) % 3.26/3.35 [26]P1(a11) % 3.26/3.35 [33]~E(a2,a1) % 3.26/3.35 [34]~E(a3,a1) % 3.26/3.35 [35]~E(a3,a2) % 3.26/3.35 [36]~E(a4,a1) % 3.26/3.35 [37]~E(a4,a2) % 3.26/3.35 [38]~E(a4,a3) % 3.26/3.35 [39]~E(a5,a1) % 3.26/3.35 [40]~E(a5,a2) % 3.26/3.35 [41]~E(a5,a3) % 3.26/3.35 [42]~E(a5,a4) % 3.26/3.35 [43]~E(a1,a6) % 3.26/3.35 [44]~E(a2,a6) % 3.26/3.35 [45]~E(a3,a6) % 3.26/3.35 [46]~E(a4,a6) % 3.26/3.35 [47]~E(a5,a6) % 3.26/3.35 [48]~E(a7,a1) % 3.26/3.35 [49]~E(a7,a2) % 3.26/3.35 [50]~E(a7,a3) % 3.26/3.35 [51]~E(a7,a4) % 3.26/3.35 [52]~E(a7,a5) % 3.26/3.35 [53]~E(a7,a6) % 3.26/3.35 [54]~E(a13,a1) % 3.26/3.35 [55]~E(a13,a2) % 3.26/3.35 [56]~E(a13,a3) % 3.26/3.35 [57]~E(a13,a4) % 3.26/3.35 [58]~E(a13,a5) % 3.26/3.35 [59]~E(a13,a6) % 3.26/3.35 [60]~E(a13,a7) % 3.26/3.35 [61]~E(a14,a1) % 3.26/3.35 [62]~E(a14,a2) % 3.26/3.35 [63]~E(a14,a3) % 3.26/3.35 [64]~E(a14,a4) % 3.26/3.35 [65]~E(a14,a5) % 3.26/3.35 [66]~E(a14,a6) % 3.26/3.35 [67]~E(a14,a7) % 3.26/3.35 [68]~E(a14,a13) % 3.26/3.35 [69]~E(a15,a1) % 3.26/3.35 [70]~E(a15,a2) % 3.26/3.35 [71]~E(a15,a3) % 3.26/3.35 [72]~E(a15,a4) % 3.26/3.35 [73]~E(a15,a5) % 3.26/3.35 [74]~E(a15,a6) % 3.26/3.35 [75]~E(a15,a7) % 3.26/3.35 [76]~E(a15,a13) % 3.26/3.35 [77]~E(a15,a14) % 3.26/3.35 [78]~P1(a15) % 3.26/3.35 [30]P2(x301,x301) % 3.26/3.35 [27]P1(f12(x271)) % 3.26/3.35 [28]E(f8(x281,a6),x281) % 3.26/3.35 [29]E(f8(x291,x291),a6) % 3.26/3.35 [31]E(f8(x311,x312),f8(x312,x311)) % 3.26/3.35 [32]E(f8(f8(x321,x322),x323),f8(x321,f8(x322,x323))) % 3.26/3.35 [79]~P1(x791)+P1(f9(x791)) % 3.26/3.35 [80]~P1(x801)+P1(f16(x801)) % 3.26/3.35 [81]~P1(x811)+P1(f17(x811)) % 3.26/3.35 [82]~P1(x821)+P1(f18(x821)) % 3.26/3.35 [83]P1(x831)+~P1(f16(x831)) % 3.26/3.35 [84]P1(x841)+~P1(f17(x841)) % 3.26/3.35 [85]P1(x851)+~P1(f18(x851)) % 3.26/3.35 [92]~P1(f18(x921))+P1(f17(f9(f8(x921,f8(a13,a14))))) % 3.26/3.35 [90]P1(x901)+~P1(f19(x902,x901)) % 3.26/3.35 [91]P1(x911)+~P1(f19(x911,x912)) % 3.26/3.35 [86]~P1(x862)+~P1(x861)+P3(x861,x862) % 3.26/3.35 [87]~P3(x872,x871)+P1(x871)+~P1(x872) % 3.26/3.35 [88]~P1(x882)+~P1(x881)+P1(f8(x881,x882)) % 3.26/3.35 [89]~P1(x892)+~P1(x891)+P1(f19(x891,x892)) % 3.26/3.35 [93]~P1(f18(x931))+P1(f16(a15))+~P1(f19(x932,f9(f8(x932,f8(a13,a14))))) % 3.26/3.35 %EqnAxiom % 3.26/3.35 [1]E(x11,x11) % 3.26/3.35 [2]E(x22,x21)+~E(x21,x22) % 3.26/3.35 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 3.26/3.35 [4]~E(x41,x42)+E(f12(x41),f12(x42)) % 3.26/3.35 [5]~E(x51,x52)+E(f8(x51,x53),f8(x52,x53)) % 3.26/3.35 [6]~E(x61,x62)+E(f8(x63,x61),f8(x63,x62)) % 3.26/3.35 [7]~E(x71,x72)+E(f19(x71,x73),f19(x72,x73)) % 3.26/3.35 [8]~E(x81,x82)+E(f19(x83,x81),f19(x83,x82)) % 3.26/3.35 [9]~E(x91,x92)+E(f9(x91),f9(x92)) % 3.26/3.35 [10]~E(x101,x102)+E(f18(x101),f18(x102)) % 3.26/3.35 [11]~E(x111,x112)+E(f16(x111),f16(x112)) % 3.26/3.35 [12]~E(x121,x122)+E(f17(x121),f17(x122)) % 3.26/3.35 [13]~P1(x131)+P1(x132)+~E(x131,x132) % 3.26/3.35 [14]P3(x142,x143)+~E(x141,x142)+~P3(x141,x143) % 3.26/3.35 [15]P3(x153,x152)+~E(x151,x152)+~P3(x153,x151) % 3.26/3.35 [16]P2(x162,x163)+~E(x161,x162)+~P2(x161,x163) % 3.26/3.35 [17]P2(x173,x172)+~E(x171,x172)+~P2(x173,x171) % 3.26/3.35 % 3.26/3.35 %------------------------------------------- % 3.26/3.35 cnf(94,plain, % 3.26/3.35 (E(x941,f8(x941,a6))), % 3.26/3.35 inference(scs_inference,[],[28,2])). % 3.26/3.35 cnf(97,plain, % 3.26/3.35 (~P1(f8(a15,a6))), % 3.26/3.35 inference(scs_inference,[],[78,28,18,2,87,13])). % 3.26/3.35 cnf(98,plain, % 3.26/3.35 (E(f8(x981,a6),x981)), % 3.26/3.35 inference(rename_variables,[],[28])). % 3.26/3.35 cnf(101,plain, % 3.26/3.35 (P2(f8(x1011,x1012),f8(x1012,x1011))), % 3.26/3.35 inference(scs_inference,[],[78,31,28,98,18,30,33,2,87,13,3,16])). % 3.26/3.35 cnf(105,plain, % 3.26/3.35 (E(x1051,f8(x1051,a6))), % 3.26/3.35 inference(rename_variables,[],[94])). % 3.26/3.35 cnf(109,plain, % 3.26/3.35 (P1(f8(a2,a6))), % 3.26/3.35 inference(scs_inference,[],[78,101,94,105,19,29,43,2,17,3,87,13])). % 3.26/3.35 cnf(403,plain, % 3.26/3.35 (P1(f8(f8(a2,a6),a6))), % 3.26/3.35 inference(scs_inference,[],[97,109,94,87,13])). % 3.26/3.35 cnf(415,plain, % 3.26/3.35 (P1(f8(a2,f8(a6,a6)))), % 3.26/3.35 inference(scs_inference,[],[78,403,32,87,13])). % 3.26/3.35 cnf(424,plain, % 3.26/3.35 (P1(f17(f18(f8(a2,f8(a6,a6)))))), % 3.26/3.35 inference(scs_inference,[],[415,81,82])). % 3.26/3.35 cnf(425,plain, % 3.26/3.35 (P1(f18(f8(a2,f8(a6,a6))))), % 3.26/3.35 inference(scs_inference,[],[424,84])). % 3.26/3.35 cnf(438,plain, % 3.26/3.35 (P1(f16(a15))+~P1(f19(x4381,f9(f8(x4381,f8(a13,a14)))))), % 3.26/3.35 inference(scs_inference,[],[425,93])). % 3.26/3.35 cnf(1523,plain, % 3.26/3.35 (P1(f17(f9(f8(a1,f8(a13,a14)))))), % 3.26/3.35 inference(scs_inference,[],[18,92,82])). % 3.26/3.35 cnf(1524,plain, % 3.26/3.35 (P1(f9(f8(a1,f8(a13,a14))))), % 3.26/3.35 inference(scs_inference,[],[1523,84])). % 3.26/3.35 cnf(1598,plain, % 3.26/3.35 (P1(f16(a15))), % 3.26/3.35 inference(scs_inference,[],[1524,18,438,89])). % 3.26/3.35 cnf(1599,plain, % 3.26/3.35 ($false), % 3.26/3.35 inference(scs_inference,[],[78,1598,83]), % 3.26/3.35 ['proof']). % 3.26/3.35 % SZS output end Proof % 3.26/3.35 % Total time :2.750000s %------------------------------------------------------------------------------