%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWV888-1 : TPTP v8.2.0. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n001.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 16:48:49 EDT 2024 % Result : Unsatisfiable 0.52s 0.60s % Output : CNFRefutation 0.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWV888-1 : TPTP v8.2.0. Released v4.1.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n001.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 : Thu Jun 20 16:09:23 EDT 2024 % 0.12/0.33 % CPUTime : % 0.18/0.55 start to proof:theBenchmark % 0.52/0.59 %------------------------------------------- % 0.52/0.59 % File :CSE---1.7 % 0.52/0.59 % Problem :theBenchmark % 0.52/0.59 % Transform :cnf % 0.52/0.59 % Format :tptp:raw % 0.52/0.59 % Command :java -jar mcs_scs.jar %d %s % 0.52/0.59 % 0.52/0.59 % Result :Theorem 0.000000s % 0.52/0.59 % Output :CNFRefutation 0.000000s % 0.52/0.59 %------------------------------------------- % 0.52/0.59 %------------------------------------------------------------------------------ % 0.52/0.59 % File : SWV888-1 : TPTP v8.2.0. Released v4.1.0. % 0.52/0.59 % Domain : Software Verification % 0.52/0.59 % Problem : Hoare logic with procedures 395_1 % 0.52/0.59 % Version : Especial. % 0.52/0.59 % English : Completeness is taken relative to completeness of the underlying % 0.52/0.59 % logic. Two versions of completeness proof: nested single recursion % 0.52/0.59 % and simultaneous recursion in call rule. % 0.52/0.59 % 0.52/0.59 % Refs : [Nip10] Nipkow (2010), Email to Geoff Sutcliffe % 0.52/0.59 % : [BN10] Boehme & Nipkow (2010), Sledgehammer: Judgement Day % 0.52/0.59 % Source : [Nip10] % 0.52/0.59 % Names : Hoare-395_1 [Nip10] % 0.52/0.59 % 0.52/0.59 % Status : Unsatisfiable % 0.52/0.59 % Rating : 0.00 v7.0.0, 0.07 v6.4.0, 0.00 v5.5.0, 0.10 v5.3.0, 0.11 v5.2.0, 0.06 v5.1.0, 0.12 v5.0.0, 0.07 v4.1.0 % 0.52/0.59 % Syntax : Number of clauses : 55 ( 20 unt; 5 nHn; 46 RR) % 0.52/0.59 % Number of literals : 95 ( 42 equ; 48 neg) % 0.52/0.59 % Maximal clause size : 3 ( 1 avg) % 0.52/0.59 % Maximal term depth : 3 ( 1 avg) % 0.52/0.59 % Number of predicates : 5 ( 4 usr; 1 prp; 0-4 aty) % 0.52/0.59 % Number of functors : 24 ( 24 usr; 6 con; 0-5 aty) % 0.52/0.59 % Number of variables : 138 ( 28 sgn) % 0.52/0.59 % SPC : CNF_UNS_RFO_SEQ_NHN % 0.52/0.59 % 0.52/0.59 % Comments : % 0.52/0.59 %------------------------------------------------------------------------------ % 0.52/0.59 cnf(cls_id__apply_0,axiom, % 0.52/0.59 c_Fun_Oid(V_x,T_a) = V_x ). % 0.52/0.59 % 0.52/0.59 cnf(cls_evaln__elim__cases_I1_J_0,axiom, % 0.52/0.59 ( V_t = V_s % 0.52/0.59 | ~ c_Natural_Oevaln(c_Com_Ocom_OSKIP,V_s,V_n,V_t) ) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_option_Onchotomy_0,axiom, % 0.52/0.59 ( V_v = c_Option_Ooption_OSome(c_ATP__Linkup_Osko__Option__Xoption__Xnchotomy__1__1(V_v,T_a),T_a) % 0.52/0.59 | V_v = c_Option_Ooption_ONone(T_a) ) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_evaln__elim__cases_I6_J_0,axiom, % 0.52/0.59 ( V_n = c_Suc(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(V_P,V_n,V_s,V_s1)) % 0.52/0.59 | ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(V_P),V_s,V_n,V_s1) ) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_evalc__elim__cases_I4_J_1,axiom, % 0.52/0.59 ( c_Natural_Oevalc(V_c2,c_Natural_Osko__Natural__Xevalc__elim__cases__4__1(V_c1,V_c2,V_s,V_t),V_t) % 0.52/0.59 | ~ c_Natural_Oevalc(c_Com_Ocom_OSemi(V_c1,V_c2),V_s,V_t) ) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_evalc__elim__cases_I4_J_0,axiom, % 0.52/0.59 ( c_Natural_Oevalc(V_c1,V_s,c_Natural_Osko__Natural__Xevalc__elim__cases__4__1(V_c1,V_c2,V_s,V_t)) % 0.52/0.59 | ~ c_Natural_Oevalc(c_Com_Ocom_OSemi(V_c1,V_c2),V_s,V_t) ) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_WT_OSkip_0,axiom, % 0.52/0.59 c_Com_OWT(c_Com_Ocom_OSKIP) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_evaln_OSemi_0,axiom, % 0.52/0.59 ( c_Natural_Oevaln(c_Com_Ocom_OSemi(V_c0,V_c1),V_s0,V_n,V_s2) % 0.52/0.59 | ~ c_Natural_Oevaln(V_c1,V_s1,V_n,V_s2) % 0.52/0.59 | ~ c_Natural_Oevaln(V_c0,V_s0,V_n,V_s1) ) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_option_Osimps_I2_J_0,axiom, % 0.52/0.59 c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_a_H,T_a) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_not__Some__eq_1,axiom, % 0.52/0.59 c_Option_Ooption_ONone(T_a) != c_Option_Ooption_OSome(V_y,T_a) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_eval__eq_0,axiom, % 0.52/0.59 ( c_Natural_Oevaln(V_c,V_s,c_Natural_Osko__Natural__Xeval__eq__1__1(V_c,V_s,V_t),V_t) % 0.52/0.59 | ~ c_Natural_Oevalc(V_c,V_s,V_t) ) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_not__None__eq_0,axiom, % 0.52/0.59 ( V_x = c_Option_Ooption_OSome(c_ATP__Linkup_Osko__Option__Xnot__None__eq__1__1(V_x,T_a),T_a) % 0.52/0.59 | V_x = c_Option_Ooption_ONone(T_a) ) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_com_Osimps_I3_J_1,axiom, % 0.52/0.59 ( c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OSemi(V_com1_H,V_com2_H) % 0.52/0.59 | V_com2 = V_com2_H ) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_com_Osimps_I3_J_0,axiom, % 0.52/0.59 ( c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OSemi(V_com1_H,V_com2_H) % 0.52/0.59 | V_com1 = V_com1_H ) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_option_Osimps_I3_J_0,axiom, % 0.52/0.59 c_Option_Ooption_OSome(V_a_H,T_a) != c_Option_Ooption_ONone(T_a) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_not__None__eq_1,axiom, % 0.52/0.59 c_Option_Ooption_OSome(V_xa,T_a) != c_Option_Ooption_ONone(T_a) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_option_Oinject_0,axiom, % 0.52/0.59 ( c_Option_Ooption_OSome(V_a,T_a) != c_Option_Ooption_OSome(V_a_H,T_a) % 0.52/0.59 | V_a = V_a_H ) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_Suc__inject_0,axiom, % 0.52/0.59 ( c_Suc(V_x) != c_Suc(V_y) % 0.52/0.59 | V_x = V_y ) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_nat_Oinject_0,axiom, % 0.52/0.59 ( c_Suc(V_nat) != c_Suc(V_nat_H) % 0.52/0.59 | V_nat = V_nat_H ) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_evaln__elim__cases_I4_J_1,axiom, % 0.52/0.59 ( c_Natural_Oevaln(V_c2,c_Natural_Osko__Natural__Xevaln__elim__cases__4__1(V_c1,V_c2,V_n,V_s,V_t),V_n,V_t) % 0.52/0.59 | ~ c_Natural_Oevaln(c_Com_Ocom_OSemi(V_c1,V_c2),V_s,V_n,V_t) ) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_evaln__elim__cases_I4_J_0,axiom, % 0.52/0.59 ( c_Natural_Oevaln(V_c1,V_s,V_n,c_Natural_Osko__Natural__Xevaln__elim__cases__4__1(V_c1,V_c2,V_n,V_s,V_t)) % 0.52/0.59 | ~ c_Natural_Oevaln(c_Com_Ocom_OSemi(V_c1,V_c2),V_s,V_n,V_t) ) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_evaln__Suc_0,axiom, % 0.52/0.59 ( c_Natural_Oevaln(V_c,V_s,c_Suc(V_n),V_s_H) % 0.52/0.59 | ~ c_Natural_Oevaln(V_c,V_s,V_n,V_s_H) ) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_not__Some__eq_0,axiom, % 0.52/0.59 ( V_x = c_Option_Ooption_ONone(T_a) % 0.52/0.59 | V_x = c_Option_Ooption_OSome(c_ATP__Linkup_Osko__Option__Xnot__Some__eq__1__1(V_x,T_a),T_a) ) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_evaln_OSkip_0,axiom, % 0.52/0.59 c_Natural_Oevaln(c_Com_Ocom_OSKIP,V_s,V_n,V_s) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_WTs__elim__cases_I4_J_1,axiom, % 0.52/0.59 ( c_Com_OWT(V_c2) % 0.52/0.59 | ~ c_Com_OWT(c_Com_Ocom_OSemi(V_c1,V_c2)) ) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_WTs__elim__cases_I4_J_0,axiom, % 0.52/0.59 ( c_Com_OWT(V_c1) % 0.52/0.59 | ~ c_Com_OWT(c_Com_Ocom_OSemi(V_c1,V_c2)) ) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_com_Osimps_I13_J_0,axiom, % 0.52/0.59 c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP ). % 0.52/0.59 % 0.52/0.59 cnf(cls_evalc__evaln_0,axiom, % 0.52/0.59 ( c_Natural_Oevaln(V_c,V_s,c_Natural_Osko__Natural__Xevalc__evaln__1__1(V_c,V_s,V_t),V_t) % 0.52/0.59 | ~ c_Natural_Oevalc(V_c,V_s,V_t) ) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_WT_OSemi_0,axiom, % 0.52/0.59 ( c_Com_OWT(c_Com_Ocom_OSemi(V_c0,V_c1)) % 0.52/0.59 | ~ c_Com_OWT(V_c1) % 0.52/0.59 | ~ c_Com_OWT(V_c0) ) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_WT__bodiesD_0,axiom, % 0.52/0.59 ( c_Com_Obody(V_pn) != c_Option_Ooption_OSome(V_b,tc_Com_Ocom) % 0.52/0.59 | ~ c_Com_OWT__bodies % 0.52/0.59 | c_Com_OWT(V_b) ) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_Suc__n__not__n_0,axiom, % 0.52/0.59 c_Suc(V_n) != V_n ). % 0.52/0.59 % 0.52/0.59 cnf(cls_n__not__Suc__n_0,axiom, % 0.52/0.59 V_n != c_Suc(V_n) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_option_Oexhaust_0,axiom, % 0.52/0.59 ( V_y = c_Option_Ooption_OSome(c_ATP__Linkup_Osko__Option__Xoption__Xexhaust__1__1(V_y,T_a),T_a) % 0.52/0.59 | V_y = c_Option_Ooption_ONone(T_a) ) ). % 0.52/0.59 % 0.52/0.59 cnf(cls_com_Osimps_I12_J_0,axiom, % 0.52/0.59 c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(V_com1_H,V_com2_H) ). % 0.52/0.59 % 0.52/0.60 cnf(cls_the_Osimps_0,axiom, % 0.52/0.60 c_Option_Othe(c_Option_Ooption_OSome(V_x,T_a),T_a) = V_x ). % 0.52/0.60 % 0.52/0.60 cnf(cls_WT_OBody_0,axiom, % 0.52/0.60 ( c_Com_OWT(c_Com_Ocom_OBODY(V_pn)) % 0.52/0.60 | c_Com_Obody(V_pn) = c_Option_Ooption_ONone(tc_Com_Ocom) ) ). % 0.52/0.60 % 0.52/0.60 cnf(cls_com_Osimps_I19_J_0,axiom, % 0.52/0.60 c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSKIP ). % 0.52/0.60 % 0.52/0.60 cnf(cls_evalc_OBody_0,axiom, % 0.52/0.60 ( c_Natural_Oevalc(c_Com_Ocom_OBODY(V_pn),V_s0,V_s1) % 0.52/0.60 | ~ c_Natural_Oevalc(c_Option_Othe(c_Com_Obody(V_pn),tc_Com_Ocom),V_s0,V_s1) ) ). % 0.52/0.60 % 0.52/0.60 cnf(cls_evalc__elim__cases_I6_J_0,axiom, % 0.52/0.60 ( c_Natural_Oevalc(c_Option_Othe(c_Com_Obody(V_P),tc_Com_Ocom),V_s,V_s1) % 0.52/0.60 | ~ c_Natural_Oevalc(c_Com_Ocom_OBODY(V_P),V_s,V_s1) ) ). % 0.52/0.60 % 0.52/0.60 cnf(cls_com__det_0,axiom, % 0.52/0.60 ( V_u = V_t % 0.52/0.60 | ~ c_Natural_Oevalc(V_c,V_s,V_u) % 0.52/0.60 | ~ c_Natural_Oevalc(V_c,V_s,V_t) ) ). % 0.52/0.60 % 0.52/0.60 cnf(cls_evalc_OSkip_0,axiom, % 0.52/0.60 c_Natural_Oevalc(c_Com_Ocom_OSKIP,V_s,V_s) ). % 0.52/0.60 % 0.52/0.60 cnf(cls_id__def_0,axiom, % 0.52/0.60 c_Fun_Oid(v_x,t_a) = v_x ). % 0.52/0.60 % 0.52/0.60 cnf(cls_evaln__elim__cases_I6_J_1,axiom, % 0.52/0.60 ( c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(V_P),tc_Com_Ocom),V_s,c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(V_P,V_n,V_s,V_s1),V_s1) % 0.52/0.60 | ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(V_P),V_s,V_n,V_s1) ) ). % 0.52/0.60 % 0.52/0.60 cnf(cls_WTs__elim__cases_I7_J_0,axiom, % 0.52/0.60 ( c_Com_Obody(V_P) = c_Option_Ooption_OSome(c_Com_Osko__Com__XWTs__elim__cases__7__1(V_P),tc_Com_Ocom) % 0.52/0.60 | ~ c_Com_OWT(c_Com_Ocom_OBODY(V_P)) ) ). % 0.52/0.60 % 0.52/0.60 cnf(cls_com_Osimps_I49_J_0,axiom, % 0.52/0.60 c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSemi(V_com1,V_com2) ). % 0.52/0.60 % 0.52/0.60 cnf(cls_com_Osimps_I48_J_0,axiom, % 0.52/0.60 c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OBODY(V_pname_H) ). % 0.52/0.60 % 0.52/0.60 cnf(cls_evalc_OSemi_0,axiom, % 0.52/0.60 ( c_Natural_Oevalc(c_Com_Ocom_OSemi(V_c0,V_c1),V_s0,V_s2) % 0.52/0.60 | ~ c_Natural_Oevalc(V_c1,V_s1,V_s2) % 0.52/0.60 | ~ c_Natural_Oevalc(V_c0,V_s0,V_s1) ) ). % 0.52/0.60 % 0.52/0.60 cnf(cls_evaln_OBody_0,axiom, % 0.52/0.60 ( c_Natural_Oevaln(c_Com_Ocom_OBODY(V_pn),V_s0,c_Suc(V_n),V_s1) % 0.52/0.60 | ~ c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(V_pn),tc_Com_Ocom),V_s0,V_n,V_s1) ) ). % 0.52/0.60 % 0.52/0.60 cnf(cls_com_Osimps_I6_J_0,axiom, % 0.52/0.60 ( c_Com_Ocom_OBODY(V_pname) != c_Com_Ocom_OBODY(V_pname_H) % 0.52/0.60 | V_pname = V_pname_H ) ). % 0.52/0.60 % 0.52/0.60 cnf(cls_com_Osimps_I18_J_0,axiom, % 0.52/0.60 c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(V_pname_H) ). % 0.52/0.60 % 0.52/0.60 cnf(cls_evalc__elim__cases_I1_J_0,axiom, % 0.52/0.60 ( V_t = V_s % 0.52/0.60 | ~ c_Natural_Oevalc(c_Com_Ocom_OSKIP,V_s,V_t) ) ). % 0.52/0.60 % 0.52/0.60 cnf(cls_evaln__evalc_0,axiom, % 0.52/0.60 ( c_Natural_Oevalc(V_c,V_s,V_t) % 0.52/0.60 | ~ c_Natural_Oevaln(V_c,V_s,V_n,V_t) ) ). % 0.52/0.60 % 0.52/0.60 cnf(cls_eval__eq_1,axiom, % 0.52/0.60 ( c_Natural_Oevalc(V_c,V_s,V_t) % 0.52/0.60 | ~ c_Natural_Oevaln(V_c,V_s,V_x,V_t) ) ). % 0.52/0.60 % 0.52/0.60 cnf(cls_conjecture_0,negated_conjecture, % 0.52/0.60 c_Natural_Oevalc(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),v_x,v_xa) ). % 0.52/0.60 % 0.52/0.60 cnf(cls_conjecture_1,negated_conjecture, % 0.52/0.60 ~ c_Natural_Oevalc(c_Com_Ocom_OBODY(v_pn),v_x,v_xa) ). % 0.52/0.60 % 0.52/0.60 %------------------------------------------------------------------------------ % 0.52/0.60 %------------------------------------------- % 0.52/0.60 % Proof found % 0.52/0.60 % SZS status Theorem for theBenchmark % 0.52/0.60 % SZS output start Proof % 0.52/0.60 %ClaNum:103(EqnAxiom:50) % 0.52/0.60 %VarNum:250(SingletonVarNum:120) % 0.52/0.60 %MaxLitNum:3 % 0.52/0.60 %MaxfuncDepth:2 % 0.52/0.60 %SharedTerms:14 % 0.52/0.60 %goalClause: 54 68 % 0.52/0.60 %singleGoalClaCount:2 % 0.52/0.60 [51]P1(a1) % 0.52/0.60 [68]~P2(f7(a18),a21,a22) % 0.52/0.60 [54]P2(f17(f2(a18),a19),a21,a22) % 0.52/0.60 [53]P2(a1,x531,x531) % 0.52/0.60 [57]~E(f7(x571),a1) % 0.52/0.60 [59]~E(f20(x591),x591) % 0.52/0.60 [55]P4(a1,x551,x552,x551) % 0.52/0.60 [61]~E(f9(x611,x612),a1) % 0.52/0.60 [66]~E(f8(x661,x662),f10(x662)) % 0.52/0.60 [52]E(f17(f8(x521,x522),x522),x521) % 0.52/0.60 [64]~E(f7(x641),f9(x642,x643)) % 0.52/0.60 [67]~E(f9(x671,x672),f7(x673)) % 0.52/0.60 [72]E(f2(x721),f10(a19))+P1(f7(x721)) % 0.52/0.60 [74]~P1(f7(x741))+E(f8(f11(x741),a19),f2(x741)) % 0.52/0.60 [85]E(x851,x852)+~P2(a1,x852,x851) % 0.52/0.60 [70]E(x701,x702)+~E(f20(x701),f20(x702)) % 0.52/0.60 [71]E(x711,x712)+~E(f7(x711),f7(x712)) % 0.52/0.60 [83]P1(x831)+~P1(f9(x832,x831)) % 0.52/0.60 [84]P1(x841)+~P1(f9(x841,x842)) % 0.52/0.60 [76]E(x761,f10(x762))+E(f8(f3(x761,x762),x762),x761) % 0.52/0.60 [77]E(x771,f10(x772))+E(f8(f4(x771,x772),x772),x771) % 0.52/0.60 [78]E(x781,f10(x782))+E(f8(f5(x781,x782),x782),x781) % 0.52/0.60 [79]E(x791,f10(x792))+E(f8(f6(x791,x792),x792),x791) % 0.52/0.60 [90]E(x901,x902)+~P4(a1,x902,x903,x901) % 0.52/0.60 [81]E(x811,x812)+~E(f8(x811,x813),f8(x812,x813)) % 0.52/0.60 [91]~P2(x911,x912,x913)+P4(x911,x912,f12(x911,x912,x913),x913) % 0.52/0.60 [92]~P2(x921,x922,x923)+P4(x921,x922,f13(x921,x922,x923),x923) % 0.52/0.60 [87]~P2(f7(x871),x872,x873)+P2(f17(f2(x871),a19),x872,x873) % 0.52/0.60 [88]P2(f7(x881),x882,x883)+~P2(f17(f2(x881),a19),x882,x883) % 0.52/0.60 [94]P2(x941,x942,x943)+~P4(x941,x942,x944,x943) % 0.52/0.60 [80]E(x801,x802)+~E(f9(x803,x801),f9(x804,x802)) % 0.52/0.60 [82]E(x821,x822)+~E(f9(x821,x823),f9(x822,x824)) % 0.52/0.60 [95]~P4(x951,x952,x953,x954)+P4(x951,x952,f20(x953),x954) % 0.52/0.60 [96]~P2(f9(x961,x963),x962,x964)+P2(x961,x962,f14(x961,x963,x962,x964)) % 0.52/0.60 [97]~P2(f9(x972,x971),x973,x974)+P2(x971,f14(x972,x971,x973,x974),x974) % 0.52/0.60 [98]P4(f7(x981),x982,f20(x983),x984)+~P4(f17(f2(x981),a19),x982,x983,x984) % 0.52/0.60 [99]~P4(f7(x991),x993,x992,x994)+E(f20(f15(x991,x992,x993,x994)),x992) % 0.52/0.60 [101]~P4(f7(x1011),x1012,x1013,x1014)+P4(f17(f2(x1011),a19),x1012,f15(x1011,x1013,x1012,x1014),x1014) % 0.52/0.60 [102]~P4(f9(x1021,x1024),x1022,x1023,x1025)+P4(x1021,x1022,x1023,f16(x1021,x1024,x1023,x1022,x1025)) % 0.52/0.60 [103]~P4(f9(x1032,x1031),x1034,x1033,x1035)+P4(x1031,f16(x1032,x1031,x1033,x1034,x1035),x1033,x1035) % 0.52/0.60 [73]P1(x731)+~E(f2(x732),f8(x731,a19))+~P3(a5000) % 0.52/0.60 [75]~P1(x752)+~P1(x751)+P1(f9(x751,x752)) % 0.52/0.60 [86]~P2(x863,x864,x861)+E(x861,x862)+~P2(x863,x864,x862) % 0.52/0.60 [89]~P2(x891,x893,x895)+~P2(x892,x895,x894)+P2(f9(x891,x892),x893,x894) % 0.52/0.60 [100]~P4(x1001,x1003,x1004,x1006)+~P4(x1002,x1006,x1004,x1005)+P4(f9(x1001,x1002),x1003,x1004,x1005) % 0.52/0.60 %EqnAxiom % 0.52/0.60 [1]E(x11,x11) % 0.52/0.60 [2]E(x22,x21)+~E(x21,x22) % 0.52/0.60 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.52/0.60 [4]~E(x41,x42)+E(f8(x41,x43),f8(x42,x43)) % 0.52/0.60 [5]~E(x51,x52)+E(f8(x53,x51),f8(x53,x52)) % 0.52/0.60 [6]~E(x61,x62)+E(f17(x61,x63),f17(x62,x63)) % 0.52/0.60 [7]~E(x71,x72)+E(f17(x73,x71),f17(x73,x72)) % 0.52/0.60 [8]~E(x81,x82)+E(f2(x81),f2(x82)) % 0.52/0.60 [9]~E(x91,x92)+E(f14(x91,x93,x94,x95),f14(x92,x93,x94,x95)) % 0.52/0.60 [10]~E(x101,x102)+E(f14(x103,x101,x104,x105),f14(x103,x102,x104,x105)) % 0.52/0.60 [11]~E(x111,x112)+E(f14(x113,x114,x111,x115),f14(x113,x114,x112,x115)) % 0.52/0.60 [12]~E(x121,x122)+E(f14(x123,x124,x125,x121),f14(x123,x124,x125,x122)) % 0.52/0.60 [13]~E(x131,x132)+E(f7(x131),f7(x132)) % 0.52/0.60 [14]~E(x141,x142)+E(f9(x141,x143),f9(x142,x143)) % 0.52/0.60 [15]~E(x151,x152)+E(f9(x153,x151),f9(x153,x152)) % 0.52/0.60 [16]~E(x161,x162)+E(f20(x161),f20(x162)) % 0.52/0.60 [17]~E(x171,x172)+E(f11(x171),f11(x172)) % 0.52/0.60 [18]~E(x181,x182)+E(f6(x181,x183),f6(x182,x183)) % 0.52/0.60 [19]~E(x191,x192)+E(f6(x193,x191),f6(x193,x192)) % 0.52/0.60 [20]~E(x201,x202)+E(f10(x201),f10(x202)) % 0.52/0.60 [21]~E(x211,x212)+E(f5(x211,x213),f5(x212,x213)) % 0.52/0.60 [22]~E(x221,x222)+E(f5(x223,x221),f5(x223,x222)) % 0.52/0.60 [23]~E(x231,x232)+E(f3(x231,x233),f3(x232,x233)) % 0.52/0.60 [24]~E(x241,x242)+E(f3(x243,x241),f3(x243,x242)) % 0.52/0.60 [25]~E(x251,x252)+E(f16(x251,x253,x254,x255,x256),f16(x252,x253,x254,x255,x256)) % 0.52/0.60 [26]~E(x261,x262)+E(f16(x263,x261,x264,x265,x266),f16(x263,x262,x264,x265,x266)) % 0.52/0.60 [27]~E(x271,x272)+E(f16(x273,x274,x271,x275,x276),f16(x273,x274,x272,x275,x276)) % 0.52/0.60 [28]~E(x281,x282)+E(f16(x283,x284,x285,x281,x286),f16(x283,x284,x285,x282,x286)) % 0.52/0.60 [29]~E(x291,x292)+E(f16(x293,x294,x295,x296,x291),f16(x293,x294,x295,x296,x292)) % 0.52/0.60 [30]~E(x301,x302)+E(f15(x301,x303,x304,x305),f15(x302,x303,x304,x305)) % 0.52/0.60 [31]~E(x311,x312)+E(f15(x313,x311,x314,x315),f15(x313,x312,x314,x315)) % 0.52/0.60 [32]~E(x321,x322)+E(f15(x323,x324,x321,x325),f15(x323,x324,x322,x325)) % 0.52/0.60 [33]~E(x331,x332)+E(f15(x333,x334,x335,x331),f15(x333,x334,x335,x332)) % 0.52/0.60 [34]~E(x341,x342)+E(f12(x341,x343,x344),f12(x342,x343,x344)) % 0.52/0.60 [35]~E(x351,x352)+E(f12(x353,x351,x354),f12(x353,x352,x354)) % 0.52/0.60 [36]~E(x361,x362)+E(f12(x363,x364,x361),f12(x363,x364,x362)) % 0.52/0.60 [37]~E(x371,x372)+E(f4(x371,x373),f4(x372,x373)) % 0.52/0.60 [38]~E(x381,x382)+E(f4(x383,x381),f4(x383,x382)) % 0.52/0.60 [39]~E(x391,x392)+E(f13(x391,x393,x394),f13(x392,x393,x394)) % 0.52/0.60 [40]~E(x401,x402)+E(f13(x403,x401,x404),f13(x403,x402,x404)) % 0.52/0.60 [41]~E(x411,x412)+E(f13(x413,x414,x411),f13(x413,x414,x412)) % 0.52/0.60 [42]~P1(x421)+P1(x422)+~E(x421,x422) % 0.52/0.60 [43]P2(x432,x433,x434)+~E(x431,x432)+~P2(x431,x433,x434) % 0.52/0.60 [44]P2(x443,x442,x444)+~E(x441,x442)+~P2(x443,x441,x444) % 0.52/0.60 [45]P2(x453,x454,x452)+~E(x451,x452)+~P2(x453,x454,x451) % 0.52/0.60 [46]P4(x462,x463,x464,x465)+~E(x461,x462)+~P4(x461,x463,x464,x465) % 0.52/0.60 [47]P4(x473,x472,x474,x475)+~E(x471,x472)+~P4(x473,x471,x474,x475) % 0.52/0.60 [48]P4(x483,x484,x482,x485)+~E(x481,x482)+~P4(x483,x484,x481,x485) % 0.52/0.60 [49]P4(x493,x494,x495,x492)+~E(x491,x492)+~P4(x493,x494,x495,x491) % 0.52/0.60 [50]~P3(x501)+P3(x502)+~E(x501,x502) % 0.52/0.60 % 0.52/0.60 %------------------------------------------- % 0.52/0.60 cnf(109,plain, % 0.52/0.60 ($false), % 0.52/0.60 inference(scs_inference,[],[68,54,88]), % 0.52/0.60 ['proof']). % 0.52/0.60 % SZS output end Proof % 0.52/0.60 % Total time :0.000000s %------------------------------------------------------------------------------