%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : LCL844-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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 : Thu Sep 24 08:50:14 AM UTC 2026
% Result : Unsatisfiable 0.15s 5.42s
% Output : Proof 0.15s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(cls_of__nat__less__0__iff_0,axiom,
( ~ 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)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
file('theBenchmark.p',cls_of__nat__less__0__iff_0) ).
cnf(cls_of__nat__0_0,axiom,
( c_Nat_Osemiring__1__class_Oof__nat(c_HOL_Ozero__class_Ozero(tc_nat),T_a) = c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Osemiring__1(T_a) ),
file('theBenchmark.p',cls_of__nat__0_0) ).
cnf(cls_of__nat__eq__iff_0,axiom,
( V_m = V_n
| c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a) != c_Nat_Osemiring__1__class_Oof__nat(V_n,T_a)
| ~ class_Nat_Osemiring__char__0(T_a) ),
file('theBenchmark.p',cls_of__nat__eq__iff_0) ).
cnf(cls_of__nat__less__iff_1,axiom,
( ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat)
| 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)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
file('theBenchmark.p',cls_of__nat__less__iff_1) ).
cnf(cls_of__nat__less__iff_0,axiom,
( ~ 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)
| c_HOL_Oord__class_Oless(V_m,V_n,tc_nat)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
file('theBenchmark.p',cls_of__nat__less__iff_0) ).
cnf(cls_order__less__asym_H_0,axiom,
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('theBenchmark.p',cls_order__less__asym_H_0) ).
cnf(cls_order__less__asym_0,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('theBenchmark.p',cls_order__less__asym_0) ).
cnf(cls_not__less__iff__gr__or__eq_1,axiom,
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('theBenchmark.p',cls_not__less__iff__gr__or__eq_1) ).
cnf(cls_xt1_I9_J_0,axiom,
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('theBenchmark.p',cls_xt1_I9_J_0) ).
cnf(cls_subst__App_0,axiom,
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)),
file('theBenchmark.p',cls_subst__App_0) ).
cnf(cls_subst__eq_0,axiom,
c_Lambda_Osubst(c_Lambda_OdB_OVar(V_k),V_u,V_k) = V_u,
file('theBenchmark.p',cls_subst__eq_0) ).
cnf(cls_subst__lt_0,axiom,
( ~ c_HOL_Oord__class_Oless(V_j,V_i,tc_nat)
| c_Lambda_Osubst(c_Lambda_OdB_OVar(V_j),V_u,V_i) = c_Lambda_OdB_OVar(V_j) ),
file('theBenchmark.p',cls_subst__lt_0) ).
cnf(cls_neq0__conv_1,axiom,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('theBenchmark.p',cls_neq0__conv_1) ).
cnf(cls_gr0I_0,axiom,
( V_n = c_HOL_Ozero__class_Ozero(tc_nat)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ),
file('theBenchmark.p',cls_gr0I_0) ).
cnf(cls_of__nat__0__less__iff_0,axiom,
( ~ 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)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
file('theBenchmark.p',cls_of__nat__0__less__iff_0) ).
cnf(cls_of__nat__0__less__iff_1,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat)
| 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)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
file('theBenchmark.p',cls_of__nat__0__less__iff_1) ).
cnf(cls_linorder__antisym__conv3_0,axiom,
( c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| V_x = V_y
| ~ class_Orderings_Olinorder(T_a) ),
file('theBenchmark.p',cls_linorder__antisym__conv3_0) ).
cnf(cls_linorder__less__linear_0,axiom,
( c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| V_x = V_y
| c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('theBenchmark.p',cls_linorder__less__linear_0) ).
cnf(cls_linorder__neqE_0,axiom,
( V_x = V_y
| c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('theBenchmark.p',cls_linorder__neqE_0) ).
cnf(cls_linorder__neqE__nat_0,axiom,
( V_x = V_y
| c_HOL_Oord__class_Oless(V_x,V_y,tc_nat)
| c_HOL_Oord__class_Oless(V_y,V_x,tc_nat) ),
file('theBenchmark.p',cls_linorder__neqE__nat_0) ).
cnf(cls_nat__neq__iff_0,axiom,
( V_m = V_n
| c_HOL_Oord__class_Oless(V_m,V_n,tc_nat)
| c_HOL_Oord__class_Oless(V_n,V_m,tc_nat) ),
file('theBenchmark.p',cls_nat__neq__iff_0) ).
cnf(cls_not__less__iff__gr__or__eq_0,axiom,
( c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| V_x = V_y
| ~ class_Orderings_Olinorder(T_a) ),
file('theBenchmark.p',cls_not__less__iff__gr__or__eq_0) ).
cnf(cls_linorder__neqE__ordered__idom_0,axiom,
( V_x = V_y
| c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Ring__and__Field_Oordered__idom(T_a) ),
file('theBenchmark.p',cls_linorder__neqE__ordered__idom_0) ).
cnf(cls_order__less__irrefl_0,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('theBenchmark.p',cls_order__less__irrefl_0) ).
cnf(cls_linorder__neq__iff_1,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('theBenchmark.p',cls_linorder__neq__iff_1) ).
cnf(cls_order__less__le_1,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('theBenchmark.p',cls_order__less__le_1) ).
cnf(cls_less__not__refl_0,axiom,
~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
file('theBenchmark.p',cls_less__not__refl_0) ).
cnf(cls_nat__less__le_1,axiom,
~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
file('theBenchmark.p',cls_nat__less__le_1) ).
cnf(cls_subst__preserves__beta_0,axiom,
( ~ c_Lambda_Obeta(V_r,V_s)
| c_Lambda_Obeta(c_Lambda_Osubst(V_r,V_t,V_i),c_Lambda_Osubst(V_s,V_t,V_i)) ),
file('theBenchmark.p',cls_subst__preserves__beta_0) ).
cnf(cls_subst__Var_2,axiom,
( c_HOL_Oord__class_Oless(V_k,V_i,tc_nat)
| V_i = V_k
| c_Lambda_Osubst(c_Lambda_OdB_OVar(V_i),V_s,V_k) = c_Lambda_OdB_OVar(V_i) ),
file('theBenchmark.p',cls_subst__Var_2) ).
cnf(cls_order__less__trans_0,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_z,T_a)
| c_HOL_Oord__class_Oless(V_x,V_z,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('theBenchmark.p',cls_order__less__trans_0) ).
cnf(cls_xt1_I10_J_0,axiom,
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_z,V_y,T_a)
| c_HOL_Oord__class_Oless(V_z,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('theBenchmark.p',cls_xt1_I10_J_0) ).
cnf(cls_gr__implies__not0_0,axiom,
~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('theBenchmark.p',cls_gr__implies__not0_0) ).
cnf(cls_not__less0_0,axiom,
~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('theBenchmark.p',cls_not__less0_0) ).
cnf(cls_subst__Var_1,axiom,
( c_Lambda_Osubst(c_Lambda_OdB_OVar(V_x),V_s,V_x) = V_s
| c_HOL_Oord__class_Oless(V_x,V_x,tc_nat) ),
file('theBenchmark.p',cls_subst__Var_1) ).
cnf(cls_subst__lift_0,axiom,
c_Lambda_Osubst(c_Lambda_Olift(V_t,V_k),V_s,V_k) = V_t,
file('theBenchmark.p',cls_subst__lift_0) ).
cnf(cls_dB_Osimps_I5_J_0,axiom,
c_Lambda_OdB_OApp(V_dB1_H,V_dB2_H) != c_Lambda_OdB_OVar(V_nat),
file('theBenchmark.p',cls_dB_Osimps_I5_J_0) ).
cnf(cls_beta__cases_I2_J_0,axiom,
( ~ c_Lambda_Obeta(c_Lambda_OdB_OAbs(V_r),V_s)
| V_s = c_Lambda_OdB_OAbs(c_Lambda_Osko__Lambda__Xbeta__cases__2__1(V_r,V_s)) ),
file('theBenchmark.p',cls_beta__cases_I2_J_0) ).
cnf(cls_app__Var__IT_0,axiom,
( ~ c_InductTermi_OIT(V_t)
| c_InductTermi_OIT(c_Lambda_OdB_OApp(V_t,c_Lambda_OdB_OVar(V_i))) ),
file('theBenchmark.p',cls_app__Var__IT_0) ).
cnf(cls_lift__preserves__beta_0,axiom,
( ~ c_Lambda_Obeta(V_r,V_s)
| c_Lambda_Obeta(c_Lambda_Olift(V_r,V_i),c_Lambda_Olift(V_s,V_i)) ),
file('theBenchmark.p',cls_lift__preserves__beta_0) ).
cnf(cls_lift_Osimps_I1_J_0,axiom,
( ~ c_HOL_Oord__class_Oless(V_i,V_k,tc_nat)
| c_Lambda_Olift(c_Lambda_OdB_OVar(V_i),V_k) = c_Lambda_OdB_OVar(V_i) ),
file('theBenchmark.p',cls_lift_Osimps_I1_J_0) ).
cnf(cls_appL_0,axiom,
( ~ c_Lambda_Obeta(V_s,V_t)
| c_Lambda_Obeta(c_Lambda_OdB_OApp(V_s,V_u),c_Lambda_OdB_OApp(V_t,V_u)) ),
file('theBenchmark.p',cls_appL_0) ).
cnf(cls_appR_0,axiom,
( ~ c_Lambda_Obeta(V_s,V_t)
| c_Lambda_Obeta(c_Lambda_OdB_OApp(V_u,V_s),c_Lambda_OdB_OApp(V_u,V_t)) ),
file('theBenchmark.p',cls_appR_0) ).
cnf(cls_lift_Osimps_I2_J_0,axiom,
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)),
file('theBenchmark.p',cls_lift_Osimps_I2_J_0) ).
cnf(cls_dB_Osimps_I4_J_0,axiom,
c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OApp(V_dB1_H,V_dB2_H),
file('theBenchmark.p',cls_dB_Osimps_I4_J_0) ).
cnf(cls_beta_0,axiom,
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))),
file('theBenchmark.p',cls_beta_0) ).
cnf(cls_dB_Osimps_I2_J_1,axiom,
( V_dB2 = V_dB2_H
| c_Lambda_OdB_OApp(V_dB1,V_dB2) != c_Lambda_OdB_OApp(V_dB1_H,V_dB2_H) ),
file('theBenchmark.p',cls_dB_Osimps_I2_J_1) ).
cnf(cls_dB_Osimps_I2_J_0,axiom,
( V_dB1 = V_dB1_H
| c_Lambda_OdB_OApp(V_dB1,V_dB2) != c_Lambda_OdB_OApp(V_dB1_H,V_dB2_H) ),
file('theBenchmark.p',cls_dB_Osimps_I2_J_0) ).
cnf(cls_beta__cases_I1_J_0,axiom,
~ c_Lambda_Obeta(c_Lambda_OdB_OVar(V_i),V_t),
file('theBenchmark.p',cls_beta__cases_I1_J_0) ).
cnf(cls_beta__cases_I2_J_1,axiom,
( ~ c_Lambda_Obeta(c_Lambda_OdB_OAbs(V_r),V_s)
| c_Lambda_Obeta(V_r,c_Lambda_Osko__Lambda__Xbeta__cases__2__1(V_r,V_s)) ),
file('theBenchmark.p',cls_beta__cases_I2_J_1) ).
cnf(cls_subst__Var__IT_0,axiom,
( ~ c_InductTermi_OIT(V_r)
| c_InductTermi_OIT(c_Lambda_Osubst(V_r,c_Lambda_OdB_OVar(V_i),V_j)) ),
file('theBenchmark.p',cls_subst__Var__IT_0) ).
cnf(cls_dB_Osimps_I1_J_0,axiom,
( V_nat = V_nat_H
| c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OVar(V_nat_H) ),
file('theBenchmark.p',cls_dB_Osimps_I1_J_0) ).
cnf(cls_dB_Osimps_I7_J_0,axiom,
c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat),
file('theBenchmark.p',cls_dB_Osimps_I7_J_0) ).
cnf(cls_dB_Osimps_I8_J_0,axiom,
c_Lambda_OdB_OApp(V_dB1,V_dB2) != c_Lambda_OdB_OAbs(V_dB_H),
file('theBenchmark.p',cls_dB_Osimps_I8_J_0) ).
cnf(cls_dB_Osimps_I9_J_0,axiom,
c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OApp(V_dB1,V_dB2),
file('theBenchmark.p',cls_dB_Osimps_I9_J_0) ).
cnf(cls_Abs_I2_J_0,axiom,
c_InductTermi_OIT(v_ta______),
file('theBenchmark.p',cls_Abs_I2_J_0) ).
cnf(cls_dB_Osimps_I3_J_0,axiom,
( V_dB = V_dB_H
| c_Lambda_OdB_OAbs(V_dB) != c_Lambda_OdB_OAbs(V_dB_H) ),
file('theBenchmark.p',cls_dB_Osimps_I3_J_0) ).
cnf(cls_lift__IT_0,axiom,
( ~ c_InductTermi_OIT(V_t)
| c_InductTermi_OIT(c_Lambda_Olift(V_t,V_i)) ),
file('theBenchmark.p',cls_lift__IT_0) ).
cnf(cls_dB_Osimps_I6_J_0,axiom,
c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H),
file('theBenchmark.p',cls_dB_Osimps_I6_J_0) ).
cnf(cls_Var__IT_0,axiom,
c_InductTermi_OIT(c_Lambda_OdB_OVar(V_n)),
file('theBenchmark.p',cls_Var__IT_0) ).
cnf(cls_Lambda_0,axiom,
( ~ c_InductTermi_OIT(V_r)
| c_InductTermi_OIT(c_Lambda_OdB_OAbs(V_r)) ),
file('theBenchmark.p',cls_Lambda_0) ).
cnf(cls_abs_0,axiom,
( ~ c_Lambda_Obeta(V_s,V_t)
| c_Lambda_Obeta(c_Lambda_OdB_OAbs(V_s),c_Lambda_OdB_OAbs(V_t)) ),
file('theBenchmark.p',cls_abs_0) ).
cnf(cls_conjecture_0,negated_conjecture,
~ c_InductTermi_OIT(c_Lambda_OdB_OAbs(v_ta______)),
file('theBenchmark.p',cls_conjecture_0) ).
cnf(clsarity_nat__Ring__and__Field_Oordered__semidom,axiom,
class_Ring__and__Field_Oordered__semidom(tc_nat),
file('theBenchmark.p',clsarity_nat__Ring__and__Field_Oordered__semidom) ).
cnf(clsarity_nat__Ring__and__Field_Osemiring__1,axiom,
class_Ring__and__Field_Osemiring__1(tc_nat),
file('theBenchmark.p',clsarity_nat__Ring__and__Field_Osemiring__1) ).
cnf(clsarity_nat__Nat_Osemiring__char__0,axiom,
class_Nat_Osemiring__char__0(tc_nat),
file('theBenchmark.p',clsarity_nat__Nat_Osemiring__char__0) ).
cnf(clsarity_nat__Orderings_Opreorder,axiom,
class_Orderings_Opreorder(tc_nat),
file('theBenchmark.p',clsarity_nat__Orderings_Opreorder) ).
cnf(clsarity_nat__Orderings_Olinorder,axiom,
class_Orderings_Olinorder(tc_nat),
file('theBenchmark.p',clsarity_nat__Orderings_Olinorder) ).
cnf(clsarity_nat__Orderings_Oorder,axiom,
class_Orderings_Oorder(tc_nat),
file('theBenchmark.p',clsarity_nat__Orderings_Oorder) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( c_Nat_Osemiring__1__class_Oof__nat(Eq_x_0,Eq_x_1) = c_Nat_Osemiring__1__class_Oof__nat(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( c_HOL_Ozero__class_Ozero(Eq_x_0) = c_HOL_Ozero__class_Ozero(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( c_Lambda_OdB_OApp(Eq_x_0,Eq_x_1) = c_Lambda_OdB_OApp(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( c_Lambda_Osubst(Eq_x_0,Eq_x_1,Eq_x_2) = c_Lambda_Osubst(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( c_Lambda_OdB_OVar(Eq_x_0) = c_Lambda_OdB_OVar(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_9,axiom,
( c_Lambda_Olift(Eq_x_0,Eq_x_1) = c_Lambda_Olift(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_10,axiom,
( c_Lambda_Osko__Lambda__Xbeta__cases__2__1(Eq_x_0,Eq_x_1) = c_Lambda_Osko__Lambda__Xbeta__cases__2__1(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_11,axiom,
( c_Lambda_OdB_OAbs(Eq_x_0) = c_Lambda_OdB_OAbs(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_12,axiom,
( class_Ring__and__Field_Oordered__semidom(Eq_y_0)
| ~ class_Ring__and__Field_Oordered__semidom(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_13,axiom,
( c_HOL_Oord__class_Oless(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ c_HOL_Oord__class_Oless(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_14,axiom,
( class_Ring__and__Field_Osemiring__1(Eq_y_0)
| ~ class_Ring__and__Field_Osemiring__1(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_15,axiom,
( class_Nat_Osemiring__char__0(Eq_y_0)
| ~ class_Nat_Osemiring__char__0(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_16,axiom,
( class_Orderings_Opreorder(Eq_y_0)
| ~ class_Orderings_Opreorder(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_17,axiom,
( class_Orderings_Olinorder(Eq_y_0)
| ~ class_Orderings_Olinorder(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_18,axiom,
( class_Orderings_Oorder(Eq_y_0)
| ~ class_Orderings_Oorder(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_19,axiom,
( class_Ring__and__Field_Oordered__idom(Eq_y_0)
| ~ class_Ring__and__Field_Oordered__idom(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_20,axiom,
( c_Lambda_Obeta(Eq_y_0,Eq_y_1)
| ~ c_Lambda_Obeta(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_21,axiom,
( c_InductTermi_OIT(Eq_y_0)
| ~ c_InductTermi_OIT(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL844-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 This is a CNF_UNS_RFO_SEQ_NHN problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/5.38 % Computer : n020.cluster.edu
% 0.12/5.38 % Model : x86_64 x86_64
% 0.12/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/5.38 % Memory : 8046.5625MB
% 0.12/5.38 % OS : Linux 6.8.0-71-generic
% 0.12/5.38 % CPULimit : 300
% 0.12/5.38 % WCLimit : 300
% 0.12/5.38 % DateTime : Sat Sep 19 15:57:09 UTC 2026
% 0.12/5.39 % CPUTime :
% 0.15/5.42 % SZS status Unsatisfiable for theBenchmark
% 0.15/5.42 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------