%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LCL798-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/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 : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 11:19:52 AM UTC 2026 % Result : Unsatisfiable 0.24s 0.52s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL798-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.02 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.07/0.33 % Computer : n013.cluster.edu % 0.07/0.33 % Model : x86_64 x86_64 % 0.07/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.33 % Memory : 8046.5625MB % 0.07/0.33 % OS : Linux 6.8.0-71-generic % 0.07/0.33 % CPULimit : 300 % 0.07/0.33 % WCLimit : 300 % 0.07/0.33 % DateTime : Sat Sep 5 20:41:49 UTC 2026 % 0.07/0.34 % CPUTime : % 0.24/0.50 start to proof:theBenchmark % 0.24/0.50 %------------------------------------------- % 0.24/0.50 % File :CSE---1.7 % 0.24/0.50 % Problem :theBenchmark % 0.24/0.50 % Transform :cnf % 0.24/0.50 % Format :tptp:raw % 0.24/0.50 % Command :java -jar mcs_scs.jar %d %s % 0.24/0.50 % 0.24/0.50 % Result :Theorem 0.006950s % 0.24/0.50 % Output :CNFRefutation 0.006950s % 0.24/0.50 %------------------------------------------- % 0.24/0.50 %------------------------------------------------------------------------------ % 0.24/0.50 % File : LCL798-1 : TPTP v9.3.1. Released v4.1.0. % 0.24/0.50 % Domain : Logic Calculi % 0.24/0.50 % Problem : Strong normalization of typed lambda calculus 148_51 % 0.24/0.50 % Version : Especial. % 0.24/0.50 % English : % 0.24/0.50 % 0.24/0.50 % Refs : [vON99] von Oheimb & Nipkow (1999), Machine-Checking the Java % 0.24/0.50 % : [Nip10] Nipkow (2010), Email to Geoff Sutcliffe % 0.24/0.50 % : [BN10] Boehme & Nipkow (2010), Sledgehammer: Judgement Day % 0.24/0.50 % Source : [Nip10] % 0.24/0.50 % Names : StrongNorm-148_51 [Nip10] % 0.24/0.50 % 0.24/0.50 % Status : Unsatisfiable % 0.24/0.50 % Rating : 0.17 v9.3.0, 0.09 v9.1.0, 0.10 v8.1.0, 0.05 v7.5.0, 0.11 v7.4.0, 0.12 v7.3.0, 0.08 v7.1.0, 0.00 v7.0.0, 0.07 v6.4.0, 0.00 v6.2.0, 0.10 v6.1.0, 0.00 v5.5.0, 0.10 v5.3.0, 0.11 v5.2.0, 0.19 v5.1.0, 0.24 v5.0.0, 0.14 v4.1.0 % 0.24/0.50 % Syntax : Number of clauses : 80 ( 34 unt; 10 nHn; 56 RR) % 0.24/0.50 % Number of literals : 154 ( 43 equ; 79 neg) % 0.24/0.50 % Maximal clause size : 4 ( 1 avg) % 0.24/0.51 % Maximal term depth : 3 ( 1 avg) % 0.24/0.51 % Number of predicates : 12 ( 11 usr; 0 prp; 1-3 aty) % 0.24/0.51 % Number of functors : 23 ( 23 usr; 13 con; 0-4 aty) % 0.24/0.51 % Number of variables : 168 ( 42 sgn) % 0.24/0.51 % SPC : CNF_UNS_RFO_SEQ_NHN % 0.24/0.51 % 0.24/0.51 % Comments : % 0.24/0.51 %------------------------------------------------------------------------------ % 0.24/0.51 cnf(cls_of__nat__less__0__iff_0,axiom, % 0.24/0.51 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.24/0.51 | ~ c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_of__nat__0_0,axiom, % 0.24/0.51 ( ~ class_Ring__and__Field_Osemiring__1(T_a) % 0.24/0.51 | c_Nat_Osemiring__1__class_Oof__nat(c_HOL_Ozero__class_Ozero(tc_nat),T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_of__nat__eq__iff_0,axiom, % 0.24/0.51 ( ~ class_Nat_Osemiring__char__0(T_a) % 0.24/0.51 | c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a) != c_Nat_Osemiring__1__class_Oof__nat(V_n,T_a) % 0.24/0.51 | V_m = V_n ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_of__nat__less__iff_1,axiom, % 0.24/0.51 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.24/0.51 | c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a),c_Nat_Osemiring__1__class_Oof__nat(V_n,T_a),T_a) % 0.24/0.51 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_of__nat__less__iff_0,axiom, % 0.24/0.51 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.24/0.51 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.24/0.51 | ~ c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a),c_Nat_Osemiring__1__class_Oof__nat(V_n,T_a),T_a) ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_order__less__asym_H_0,axiom, % 0.24/0.51 ( ~ class_Orderings_Opreorder(T_a) % 0.24/0.51 | ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a) % 0.24/0.51 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_order__less__asym_0,axiom, % 0.24/0.51 ( ~ class_Orderings_Opreorder(T_a) % 0.24/0.51 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.24/0.51 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_not__less__iff__gr__or__eq_1,axiom, % 0.24/0.51 ( ~ class_Orderings_Olinorder(T_a) % 0.24/0.51 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.24/0.51 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_xt1_I9_J_0,axiom, % 0.24/0.51 ( ~ class_Orderings_Oorder(T_a) % 0.24/0.51 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.24/0.51 | ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a) ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_neq0__conv_1,axiom, % 0.24/0.51 ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_gr0I_0,axiom, % 0.24/0.51 ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) % 0.24/0.51 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_of__nat__0__less__iff_0,axiom, % 0.24/0.51 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.24/0.51 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) % 0.24/0.51 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_Nat_Osemiring__1__class_Oof__nat(V_n,T_a),T_a) ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_of__nat__0__less__iff_1,axiom, % 0.24/0.51 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.24/0.51 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_Nat_Osemiring__1__class_Oof__nat(V_n,T_a),T_a) % 0.24/0.51 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_linorder__antisym__conv3_0,axiom, % 0.24/0.51 ( ~ class_Orderings_Olinorder(T_a) % 0.24/0.51 | V_x = V_y % 0.24/0.51 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.24/0.51 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_linorder__less__linear_0,axiom, % 0.24/0.51 ( ~ class_Orderings_Olinorder(T_a) % 0.24/0.51 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.24/0.51 | V_x = V_y % 0.24/0.51 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_linorder__neqE_0,axiom, % 0.24/0.51 ( ~ class_Orderings_Olinorder(T_a) % 0.24/0.51 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.24/0.51 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.24/0.51 | V_x = V_y ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_linorder__neqE__nat_0,axiom, % 0.24/0.51 ( c_HOL_Oord__class_Oless(V_y,V_x,tc_nat) % 0.24/0.51 | c_HOL_Oord__class_Oless(V_x,V_y,tc_nat) % 0.24/0.51 | V_x = V_y ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_nat__neq__iff_0,axiom, % 0.24/0.51 ( c_HOL_Oord__class_Oless(V_n,V_m,tc_nat) % 0.24/0.51 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.24/0.51 | V_m = V_n ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_not__less__iff__gr__or__eq_0,axiom, % 0.24/0.51 ( ~ class_Orderings_Olinorder(T_a) % 0.24/0.51 | V_x = V_y % 0.24/0.51 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.24/0.51 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_linorder__neqE__ordered__idom_0,axiom, % 0.24/0.51 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.24/0.51 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.24/0.51 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.24/0.51 | V_x = V_y ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_order__less__irrefl_0,axiom, % 0.24/0.51 ( ~ class_Orderings_Opreorder(T_a) % 0.24/0.51 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_linorder__neq__iff_1,axiom, % 0.24/0.51 ( ~ class_Orderings_Olinorder(T_a) % 0.24/0.51 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_order__less__le_1,axiom, % 0.24/0.51 ( ~ class_Orderings_Oorder(T_a) % 0.24/0.51 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_less__not__refl_0,axiom, % 0.24/0.51 ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_nat__less__le_1,axiom, % 0.24/0.51 ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_order__less__trans_0,axiom, % 0.24/0.51 ( ~ class_Orderings_Opreorder(T_a) % 0.24/0.51 | c_HOL_Oord__class_Oless(V_x,V_z,T_a) % 0.24/0.51 | ~ c_HOL_Oord__class_Oless(V_y,V_z,T_a) % 0.24/0.51 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_xt1_I10_J_0,axiom, % 0.24/0.51 ( ~ class_Orderings_Oorder(T_a) % 0.24/0.51 | c_HOL_Oord__class_Oless(V_z,V_x,T_a) % 0.24/0.51 | ~ c_HOL_Oord__class_Oless(V_z,V_y,T_a) % 0.24/0.51 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_gr__implies__not0_0,axiom, % 0.24/0.51 ~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_not__less0_0,axiom, % 0.24/0.51 ~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_dB_Osimps_I5_J_0,axiom, % 0.24/0.51 c_Lambda_OdB_OApp(V_dB1_H,V_dB2_H) != c_Lambda_OdB_OVar(V_nat) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_abs_0,axiom, % 0.24/0.51 ( c_Lambda_Obeta(c_Lambda_OdB_OAbs(V_s),c_Lambda_OdB_OAbs(V_t)) % 0.24/0.51 | ~ c_Lambda_Obeta(V_s,V_t) ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_beta__cases_I2_J_0,axiom, % 0.24/0.51 ( V_s = c_Lambda_OdB_OAbs(c_Lambda_Osko__Lambda__Xbeta__cases__2__1(V_r,V_s)) % 0.24/0.51 | ~ c_Lambda_Obeta(c_Lambda_OdB_OAbs(V_r),V_s) ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_app__Var__IT_0,axiom, % 0.24/0.51 ( c_InductTermi_OIT(c_Lambda_OdB_OApp(V_t,c_Lambda_OdB_OVar(V_i))) % 0.24/0.51 | ~ c_InductTermi_OIT(V_t) ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_not__Cons__self_0,axiom, % 0.24/0.51 V_xs != c_List_Olist_OCons(V_x,V_xs,T_a) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_not__Cons__self2_0,axiom, % 0.24/0.51 c_List_Olist_OCons(V_x,V_t,T_a) != V_t ). % 0.24/0.51 % 0.24/0.51 cnf(cls_lift__preserves__beta_0,axiom, % 0.24/0.51 ( c_Lambda_Obeta(c_Lambda_Olift(V_r,V_i),c_Lambda_Olift(V_s,V_i)) % 0.24/0.51 | ~ c_Lambda_Obeta(V_r,V_s) ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_lift_Osimps_I1_J_0,axiom, % 0.24/0.51 ( c_Lambda_Olift(c_Lambda_OdB_OVar(V_i),V_k) = c_Lambda_OdB_OVar(V_i) % 0.24/0.51 | ~ c_HOL_Oord__class_Oless(V_i,V_k,tc_nat) ) ). % 0.24/0.51 % 0.24/0.51 cnf(cls_appL_0,axiom, % 0.24/0.51 ( c_Lambda_Obeta(c_Lambda_OdB_OApp(V_s,V_u),c_Lambda_OdB_OApp(V_t,V_u)) % 0.24/0.51 | ~ c_Lambda_Obeta(V_s,V_t) ) ). % 0.24/0.51 % 0.24/0.52 cnf(cls_appR_0,axiom, % 0.24/0.52 ( c_Lambda_Obeta(c_Lambda_OdB_OApp(V_u,V_s),c_Lambda_OdB_OApp(V_u,V_t)) % 0.24/0.52 | ~ c_Lambda_Obeta(V_s,V_t) ) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_subst__Var_1,axiom, % 0.24/0.52 ( c_HOL_Oord__class_Oless(V_x,V_x,tc_nat) % 0.24/0.52 | c_Lambda_Osubst(c_Lambda_OdB_OVar(V_x),V_s,V_x) = V_s ) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_subst__Var_2,axiom, % 0.24/0.52 ( c_Lambda_Osubst(c_Lambda_OdB_OVar(V_i),V_s,V_k) = c_Lambda_OdB_OVar(V_i) % 0.24/0.52 | V_i = V_k % 0.24/0.52 | c_HOL_Oord__class_Oless(V_k,V_i,tc_nat) ) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_lift_Osimps_I2_J_0,axiom, % 0.24/0.52 c_Lambda_Olift(c_Lambda_OdB_OApp(V_s,V_t),V_k) = c_Lambda_OdB_OApp(c_Lambda_Olift(V_s,V_k),c_Lambda_Olift(V_t,V_k)) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_dB_Osimps_I6_J_0,axiom, % 0.24/0.52 c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_dB_Osimps_I3_J_0,axiom, % 0.24/0.52 ( c_Lambda_OdB_OAbs(V_dB) != c_Lambda_OdB_OAbs(V_dB_H) % 0.24/0.52 | V_dB = V_dB_H ) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_dB_Osimps_I4_J_0,axiom, % 0.24/0.52 c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OApp(V_dB1_H,V_dB2_H) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_beta_0,axiom, % 0.24/0.52 c_Lambda_Obeta(c_Lambda_OdB_OApp(c_Lambda_OdB_OAbs(V_s),V_t),c_Lambda_Osubst(V_s,V_t,c_HOL_Ozero__class_Ozero(tc_nat))) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_dB_Osimps_I2_J_1,axiom, % 0.24/0.52 ( c_Lambda_OdB_OApp(V_dB1,V_dB2) != c_Lambda_OdB_OApp(V_dB1_H,V_dB2_H) % 0.24/0.52 | V_dB2 = V_dB2_H ) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_dB_Osimps_I2_J_0,axiom, % 0.24/0.52 ( c_Lambda_OdB_OApp(V_dB1,V_dB2) != c_Lambda_OdB_OApp(V_dB1_H,V_dB2_H) % 0.24/0.52 | V_dB1 = V_dB1_H ) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_beta__cases_I1_J_0,axiom, % 0.24/0.52 ~ c_Lambda_Obeta(c_Lambda_OdB_OVar(V_i),V_t) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_beta__cases_I2_J_1,axiom, % 0.24/0.52 ( c_Lambda_Obeta(V_r,c_Lambda_Osko__Lambda__Xbeta__cases__2__1(V_r,V_s)) % 0.24/0.52 | ~ c_Lambda_Obeta(c_Lambda_OdB_OAbs(V_r),V_s) ) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_subst__lt_0,axiom, % 0.24/0.52 ( c_Lambda_Osubst(c_Lambda_OdB_OVar(V_j),V_u,V_i) = c_Lambda_OdB_OVar(V_j) % 0.24/0.52 | ~ c_HOL_Oord__class_Oless(V_j,V_i,tc_nat) ) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_list_Oinject_0,axiom, % 0.24/0.52 ( c_List_Olist_OCons(V_a,V_list,T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a) % 0.24/0.52 | V_a = V_a_H ) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_list_Oinject_1,axiom, % 0.24/0.52 ( c_List_Olist_OCons(V_a,V_list,T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a) % 0.24/0.52 | V_list = V_list_H ) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_dB_Osimps_I9_J_0,axiom, % 0.24/0.52 c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OApp(V_dB1,V_dB2) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_dB_Osimps_I1_J_0,axiom, % 0.24/0.52 ( c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OVar(V_nat_H) % 0.24/0.52 | V_nat = V_nat_H ) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_dB_Osimps_I8_J_0,axiom, % 0.24/0.52 c_Lambda_OdB_OApp(V_dB1,V_dB2) != c_Lambda_OdB_OAbs(V_dB_H) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_dB_Osimps_I7_J_0,axiom, % 0.24/0.52 c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_subst__App_0,axiom, % 0.24/0.52 c_Lambda_Osubst(c_Lambda_OdB_OApp(V_t,V_u),V_s,V_k) = c_Lambda_OdB_OApp(c_Lambda_Osubst(V_t,V_s,V_k),c_Lambda_Osubst(V_u,V_s,V_k)) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_subst__eq_0,axiom, % 0.24/0.52 c_Lambda_Osubst(c_Lambda_OdB_OVar(V_k),V_u,V_k) = V_u ). % 0.24/0.52 % 0.24/0.52 cnf(cls_subst__Var__IT_0,axiom, % 0.24/0.52 ( c_InductTermi_OIT(c_Lambda_Osubst(V_r,c_Lambda_OdB_OVar(V_i),V_j)) % 0.24/0.52 | ~ c_InductTermi_OIT(V_r) ) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_lift__IT_0,axiom, % 0.24/0.52 ( c_InductTermi_OIT(c_Lambda_Olift(V_t,V_i)) % 0.24/0.52 | ~ c_InductTermi_OIT(V_t) ) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_True_0,axiom, % 0.24/0.52 v_n____ = v_i____ ). % 0.24/0.52 % 0.24/0.52 cnf(cls_Var__IT_0,axiom, % 0.24/0.52 c_InductTermi_OIT(c_Lambda_OdB_OVar(V_n)) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_subst__preserves__beta_0,axiom, % 0.24/0.52 ( c_Lambda_Obeta(c_Lambda_Osubst(V_r,V_t,V_i),c_Lambda_Osubst(V_s,V_t,V_i)) % 0.24/0.52 | ~ c_Lambda_Obeta(V_r,V_s) ) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_Var_I3_J_0,axiom, % 0.24/0.52 c_InductTermi_OIT(v_ua______) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_Lambda_0,axiom, % 0.24/0.52 ( c_InductTermi_OIT(c_Lambda_OdB_OAbs(V_r)) % 0.24/0.52 | ~ c_InductTermi_OIT(V_r) ) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_uIT_0,axiom, % 0.24/0.52 c_InductTermi_OIT(v_u____) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_subst__lift_0,axiom, % 0.24/0.52 c_Lambda_Osubst(c_Lambda_Olift(V_t,V_k),V_s,V_k) = V_t ). % 0.24/0.52 % 0.24/0.52 cnf(cls_Cons_0,axiom, % 0.24/0.52 v_rs____ = c_List_Olist_OCons(v_a____,v_as____,tc_Lambda_OdB) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_CHAINED_0,axiom, % 0.24/0.52 ( c_InductTermi_OIT(c_Lambda_Osubst(v_a____,V_u,V_i)) % 0.24/0.52 | ~ c_Type_Otyping(V_e,V_u,v_T____) % 0.24/0.52 | ~ c_InductTermi_OIT(V_u) % 0.24/0.52 | ~ c_Type_Otyping(c_Type_Oshift(V_e,V_i,v_T____,tc_Type_Otype),v_a____,V_T_H) ) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_CHAINED_0_01,axiom, % 0.24/0.52 c_Type_Otyping(v_e____,v_u____,v_T____) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_CHAINED_0_02,axiom, % 0.24/0.52 c_InductTermi_OIT(v_u____) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_CHAINED_0_03,axiom, % 0.24/0.52 c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_a____,v_T_H_H____) ). % 0.24/0.52 % 0.24/0.52 cnf(cls_conjecture_0,negated_conjecture, % 0.24/0.52 ~ c_InductTermi_OIT(c_Lambda_Osubst(v_a____,v_u____,v_i____)) ). % 0.24/0.52 % 0.24/0.52 cnf(clsarity_nat__Ring__and__Field_Oordered__semidom,axiom, % 0.24/0.52 class_Ring__and__Field_Oordered__semidom(tc_nat) ). % 0.24/0.52 % 0.24/0.52 cnf(clsarity_nat__Ring__and__Field_Osemiring__1,axiom, % 0.24/0.52 class_Ring__and__Field_Osemiring__1(tc_nat) ). % 0.24/0.52 % 0.24/0.52 cnf(clsarity_nat__Nat_Osemiring__char__0,axiom, % 0.24/0.52 class_Nat_Osemiring__char__0(tc_nat) ). % 0.24/0.52 % 0.24/0.52 cnf(clsarity_nat__Orderings_Opreorder,axiom, % 0.24/0.52 class_Orderings_Opreorder(tc_nat) ). % 0.24/0.52 % 0.24/0.52 cnf(clsarity_nat__Orderings_Olinorder,axiom, % 0.24/0.52 class_Orderings_Olinorder(tc_nat) ). % 0.24/0.52 % 0.24/0.52 cnf(clsarity_nat__Orderings_Oorder,axiom, % 0.24/0.52 class_Orderings_Oorder(tc_nat) ). % 0.24/0.52 % 0.24/0.52 %------------------------------------------------------------------------------ % 0.24/0.52 %------------------------------------------- % 0.24/0.52 % Proof found % 0.24/0.52 % SZS status Theorem for theBenchmark % 0.24/0.52 % SZS output start Proof % 0.24/0.52 %ClaNum:120(EqnAxiom:40) % 0.24/0.52 %VarNum:291(SingletonVarNum:145) % 0.24/0.52 %MaxLitNum:4 % 0.24/0.52 %MaxfuncDepth:2 % 0.24/0.52 %SharedTerms:31 % 0.24/0.52 %goalClause: 74 % 0.24/0.52 %singleGoalClaCount:1 % 0.24/0.52 [41]E(a1,a20) % 0.24/0.52 [42]P1(a2) % 0.24/0.52 [43]P11(a2) % 0.24/0.52 [44]P2(a2) % 0.24/0.52 [45]P7(a2) % 0.24/0.52 [46]P8(a2) % 0.24/0.52 [47]P9(a2) % 0.24/0.52 [48]P3(a21) % 0.24/0.52 [50]P3(a22) % 0.24/0.52 [53]P5(a19,a22,a16) % 0.24/0.52 [52]E(f8(a15,a18,a7),a23) % 0.24/0.52 [59]P5(f12(a19,a1,a16,a14),a15,a17) % 0.24/0.52 [74]~P3(f9(a15,a22,a1)) % 0.24/0.52 [68]~P4(x681,x681,a2) % 0.24/0.52 [51]P3(f3(x511)) % 0.24/0.52 [72]~P4(x721,f6(a2),a2) % 0.24/0.52 [61]~E(f5(x611),f3(x612)) % 0.24/0.52 [66]~P6(f3(x661),x662) % 0.24/0.52 [54]E(f9(f3(x541),x542,x541),x542) % 0.24/0.52 [57]P6(f4(f5(x571),x572),f9(x571,x572,f6(a2))) % 0.24/0.52 [62]~E(f3(x621),f4(x622,x623)) % 0.24/0.52 [63]~E(f5(x631),f4(x632,x633)) % 0.24/0.52 [64]~E(f4(x641,x642),f3(x643)) % 0.24/0.52 [65]~E(f4(x651,x652),f5(x653)) % 0.24/0.52 [70]~E(f8(x701,x702,x703),x702) % 0.24/0.52 [55]E(f9(f10(x551,x552),x553,x552),x551) % 0.24/0.52 [56]E(f4(f10(x561,x562),f10(x563,x562)),f10(f4(x561,x563),x562)) % 0.24/0.52 [58]E(f4(f9(x581,x582,x583),f9(x584,x582,x583)),f9(f4(x581,x584),x582,x583)) % 0.24/0.52 [77]~P3(x771)+P3(f5(x771)) % 0.24/0.52 [85]E(x851,f6(a2))+P4(f6(a2),x851,a2) % 0.24/0.52 [78]~P11(x781)+E(f13(f6(a2),x781),f6(x781)) % 0.24/0.52 [91]~P4(x912,x912,x911)+~P7(x911) % 0.24/0.52 [92]~P4(x922,x922,x921)+~P8(x921) % 0.24/0.52 [93]~P4(x932,x932,x931)+~P9(x931) % 0.24/0.52 [75]E(x751,x752)+~E(f3(x751),f3(x752)) % 0.24/0.52 [76]E(x761,x762)+~E(f5(x761),f5(x762)) % 0.24/0.52 [79]~P3(x791)+P3(f10(x791,x792)) % 0.24/0.52 [82]~P6(x821,x822)+P6(f5(x821),f5(x822)) % 0.24/0.52 [87]~P6(f5(x871),x872)+P6(x871,f11(x871,x872)) % 0.24/0.52 [105]~P1(x1051)+~P4(f13(x1052,x1051),f6(x1051),x1051) % 0.24/0.52 [83]~P3(x831)+P3(f4(x831,f3(x832))) % 0.24/0.52 [86]~P6(f5(x861),x862)+E(f5(f11(x861,x862)),x862) % 0.24/0.52 [94]~P4(x941,x942,a2)+E(f10(f3(x941),x942),f3(x941)) % 0.24/0.52 [88]~P6(x881,x883)+P6(f4(x881,x882),f4(x883,x882)) % 0.24/0.52 [89]~P6(x892,x893)+P6(f4(x891,x892),f4(x891,x893)) % 0.24/0.52 [90]~P6(x901,x903)+P6(f10(x901,x902),f10(x903,x902)) % 0.24/0.52 [104]~P3(x1041)+P3(f9(x1041,f3(x1042),x1043)) % 0.24/0.52 [106]~P4(x1061,x1063,a2)+E(f9(f3(x1061),x1062,x1063),f3(x1061)) % 0.24/0.52 [80]E(x801,x802)+~E(f4(x803,x801),f4(x804,x802)) % 0.24/0.52 [81]E(x811,x812)+~E(f4(x811,x813),f4(x812,x814)) % 0.24/0.52 [119]~P6(x1191,x1194)+P6(f9(x1191,x1192,x1193),f9(x1194,x1192,x1193)) % 0.24/0.52 [107]E(x1071,x1072)+~E(f8(x1073,x1071,x1074),f8(x1075,x1072,x1074)) % 0.24/0.52 [108]E(x1081,x1082)+~E(f8(x1081,x1083,x1084),f8(x1082,x1085,x1084)) % 0.24/0.52 [96]E(x961,x962)+P4(x962,x961,a2)+P4(x961,x962,a2) % 0.24/0.52 [113]~P1(x1131)+P4(f6(x1131),f13(x1132,x1131),x1131)+~P4(f6(a2),x1132,a2) % 0.24/0.52 [115]~P1(x1152)+~P4(f6(x1152),f13(x1151,x1152),x1152)+P4(f6(a2),x1151,a2) % 0.24/0.52 [110]~P4(x1103,x1102,x1101)+~P7(x1101)+~P4(x1102,x1103,x1101) % 0.24/0.52 [111]~P4(x1113,x1112,x1111)+~P8(x1111)+~P4(x1112,x1113,x1111) % 0.24/0.52 [112]~P4(x1123,x1122,x1121)+~P9(x1121)+~P4(x1122,x1123,x1121) % 0.24/0.52 [84]~P2(x843)+E(x841,x842)+~E(f13(x841,x843),f13(x842,x843)) % 0.24/0.52 [114]~P1(x1142)+~P4(x1141,x1143,a2)+P4(f13(x1141,x1142),f13(x1143,x1142),x1142) % 0.24/0.52 [116]~P1(x1163)+~P4(f13(x1161,x1163),f13(x1162,x1163),x1163)+P4(x1161,x1162,a2) % 0.24/0.52 [103]E(x1031,x1032)+P4(x1032,x1031,a2)+E(f9(f3(x1031),x1033,x1032),f3(x1031)) % 0.24/0.52 [101]P4(x1011,x1012,x1013)+~P8(x1013)+E(x1011,x1012)+P4(x1012,x1011,x1013) % 0.24/0.52 [102]P4(x1021,x1022,x1023)+~P10(x1023)+E(x1021,x1022)+P4(x1022,x1021,x1023) % 0.24/0.52 [117]~P7(x1173)+~P4(x1171,x1174,x1173)+P4(x1171,x1172,x1173)+~P4(x1174,x1172,x1173) % 0.24/0.52 [118]~P9(x1183)+~P4(x1181,x1184,x1183)+P4(x1181,x1182,x1183)+~P4(x1184,x1182,x1183) % 0.24/0.52 [120]~P3(x1201)+~P5(x1203,x1201,a16)+~P5(f12(x1203,x1202,a16,a14),a15,x1204)+P3(f9(a15,x1201,x1202)) % 0.24/0.52 %EqnAxiom % 0.24/0.52 [1]E(x11,x11) % 0.24/0.52 [2]E(x22,x21)+~E(x21,x22) % 0.24/0.52 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.24/0.52 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 0.24/0.52 [5]~E(x51,x52)+E(f8(x51,x53,x54),f8(x52,x53,x54)) % 0.24/0.52 [6]~E(x61,x62)+E(f8(x63,x61,x64),f8(x63,x62,x64)) % 0.24/0.52 [7]~E(x71,x72)+E(f8(x73,x74,x71),f8(x73,x74,x72)) % 0.24/0.52 [8]~E(x81,x82)+E(f12(x81,x83,x84,x85),f12(x82,x83,x84,x85)) % 0.24/0.52 [9]~E(x91,x92)+E(f12(x93,x91,x94,x95),f12(x93,x92,x94,x95)) % 0.24/0.52 [10]~E(x101,x102)+E(f12(x103,x104,x101,x105),f12(x103,x104,x102,x105)) % 0.24/0.52 [11]~E(x111,x112)+E(f12(x113,x114,x115,x111),f12(x113,x114,x115,x112)) % 0.24/0.52 [12]~E(x121,x122)+E(f9(x121,x123,x124),f9(x122,x123,x124)) % 0.24/0.52 [13]~E(x131,x132)+E(f9(x133,x131,x134),f9(x133,x132,x134)) % 0.24/0.52 [14]~E(x141,x142)+E(f9(x143,x144,x141),f9(x143,x144,x142)) % 0.24/0.52 [15]~E(x151,x152)+E(f10(x151,x153),f10(x152,x153)) % 0.24/0.52 [16]~E(x161,x162)+E(f10(x163,x161),f10(x163,x162)) % 0.24/0.52 [17]~E(x171,x172)+E(f13(x171,x173),f13(x172,x173)) % 0.24/0.52 [18]~E(x181,x182)+E(f13(x183,x181),f13(x183,x182)) % 0.24/0.52 [19]~E(x191,x192)+E(f4(x191,x193),f4(x192,x193)) % 0.24/0.52 [20]~E(x201,x202)+E(f4(x203,x201),f4(x203,x202)) % 0.24/0.52 [21]~E(x211,x212)+E(f11(x211,x213),f11(x212,x213)) % 0.24/0.52 [22]~E(x221,x222)+E(f11(x223,x221),f11(x223,x222)) % 0.24/0.52 [23]~E(x231,x232)+E(f6(x231),f6(x232)) % 0.24/0.52 [24]~E(x241,x242)+E(f5(x241),f5(x242)) % 0.24/0.52 [25]~P1(x251)+P1(x252)+~E(x251,x252) % 0.24/0.52 [26]~P11(x261)+P11(x262)+~E(x261,x262) % 0.24/0.52 [27]~P2(x271)+P2(x272)+~E(x271,x272) % 0.24/0.52 [28]~P7(x281)+P7(x282)+~E(x281,x282) % 0.24/0.52 [29]~P8(x291)+P8(x292)+~E(x291,x292) % 0.24/0.52 [30]~P9(x301)+P9(x302)+~E(x301,x302) % 0.24/0.52 [31]~P3(x311)+P3(x312)+~E(x311,x312) % 0.24/0.53 [32]P4(x322,x323,x324)+~E(x321,x322)+~P4(x321,x323,x324) % 0.24/0.53 [33]P4(x333,x332,x334)+~E(x331,x332)+~P4(x333,x331,x334) % 0.24/0.53 [34]P4(x343,x344,x342)+~E(x341,x342)+~P4(x343,x344,x341) % 0.24/0.53 [35]P5(x352,x353,x354)+~E(x351,x352)+~P5(x351,x353,x354) % 0.24/0.53 [36]P5(x363,x362,x364)+~E(x361,x362)+~P5(x363,x361,x364) % 0.24/0.53 [37]P5(x373,x374,x372)+~E(x371,x372)+~P5(x373,x374,x371) % 0.24/0.53 [38]~P10(x381)+P10(x382)+~E(x381,x382) % 0.24/0.53 [39]P6(x392,x393)+~E(x391,x392)+~P6(x391,x393) % 0.24/0.53 [40]P6(x403,x402)+~E(x401,x402)+~P6(x403,x401) % 0.24/0.53 % 0.24/0.53 %------------------------------------------- % 0.24/0.53 cnf(144,plain, % 0.24/0.53 ($false), % 0.24/0.53 inference(scs_inference,[],[74,41,50,53,54,59,68,70,61,66,72,42,86,2,87,31,3,115,116,120]), % 0.24/0.53 ['proof']). % 0.24/0.53 % SZS output end Proof % 0.24/0.53 % Total time :0.006950s %------------------------------------------------------------------------------