%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : LCL844-1 : TPTP v9.2.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 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 : Tue May 5 04:45:14 PM UTC 2026
% Result : Unsatisfiable 0.28s 1.61s
% Output : CNFRefutation 0.28s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 112)
% Comments :
%------------------------------------------------------------------------------
cnf(cls_subst__App_0,axiom,
c_Lambda_Osubst(c_Lambda_OdB_OApp(X1,X2),X3,X4) = c_Lambda_OdB_OApp(c_Lambda_Osubst(X1,X3,X4),c_Lambda_Osubst(X2,X3,X4)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_subst__App_0) ).
cnf(cls_subst__preserves__beta_0,axiom,
( c_Lambda_Obeta(c_Lambda_Osubst(X1,X2,X3),c_Lambda_Osubst(X4,X2,X3))
| ~ c_Lambda_Obeta(X1,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_subst__preserves__beta_0) ).
cnf(cls_xt1_I10_J_0,axiom,
( c_HOL_Oord__class_Oless(X2,X3,X1)
| ~ class_Orderings_Oorder(X1)
| ~ c_HOL_Oord__class_Oless(X2,X4,X1)
| ~ c_HOL_Oord__class_Oless(X4,X3,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_xt1_I10_J_0) ).
cnf(cls_order__less__trans_0,axiom,
( c_HOL_Oord__class_Oless(X2,X3,X1)
| ~ class_Orderings_Opreorder(X1)
| ~ c_HOL_Oord__class_Oless(X4,X3,X1)
| ~ c_HOL_Oord__class_Oless(X2,X4,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__trans_0) ).
cnf(cls_of__nat__less__iff_0,axiom,
( c_HOL_Oord__class_Oless(X2,X3,tc_nat)
| ~ class_Ring__and__Field_Oordered__semidom(X1)
| ~ c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(X2,X1),c_Nat_Osemiring__1__class_Oof__nat(X3,X1),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_of__nat__less__iff_0) ).
cnf(cls_of__nat__0__less__iff_0,axiom,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X2,tc_nat)
| ~ class_Ring__and__Field_Oordered__semidom(X1)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X1),c_Nat_Osemiring__1__class_Oof__nat(X2,X1),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_of__nat__0__less__iff_0) ).
cnf(cls_of__nat__less__iff_1,axiom,
( c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(X2,X1),c_Nat_Osemiring__1__class_Oof__nat(X3,X1),X1)
| ~ class_Ring__and__Field_Oordered__semidom(X1)
| ~ c_HOL_Oord__class_Oless(X2,X3,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_of__nat__less__iff_1) ).
cnf(cls_of__nat__0__less__iff_1,axiom,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X1),c_Nat_Osemiring__1__class_Oof__nat(X2,X1),X1)
| ~ class_Ring__and__Field_Oordered__semidom(X1)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X2,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_of__nat__0__less__iff_1) ).
cnf(cls_xt1_I9_J_0,axiom,
( ~ class_Orderings_Oorder(X1)
| ~ c_HOL_Oord__class_Oless(X2,X3,X1)
| ~ c_HOL_Oord__class_Oless(X3,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_xt1_I9_J_0) ).
cnf(cls_not__less__iff__gr__or__eq_1,axiom,
( ~ class_Orderings_Olinorder(X1)
| ~ c_HOL_Oord__class_Oless(X2,X3,X1)
| ~ c_HOL_Oord__class_Oless(X3,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less__iff__gr__or__eq_1) ).
cnf(cls_order__less__asym_0,axiom,
( ~ class_Orderings_Opreorder(X1)
| ~ c_HOL_Oord__class_Oless(X2,X3,X1)
| ~ c_HOL_Oord__class_Oless(X3,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__asym_0) ).
cnf(cls_order__less__asym_H_0,axiom,
( ~ class_Orderings_Opreorder(X1)
| ~ c_HOL_Oord__class_Oless(X2,X3,X1)
| ~ c_HOL_Oord__class_Oless(X3,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__asym_H_0) ).
cnf(cls_beta_0,axiom,
c_Lambda_Obeta(c_Lambda_OdB_OApp(c_Lambda_OdB_OAbs(X1),X2),c_Lambda_Osubst(X1,X2,c_HOL_Ozero__class_Ozero(tc_nat))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_beta_0) ).
cnf(cls_subst__lt_0,axiom,
( c_Lambda_Osubst(c_Lambda_OdB_OVar(X1),X2,X3) = c_Lambda_OdB_OVar(X1)
| ~ c_HOL_Oord__class_Oless(X1,X3,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_subst__lt_0) ).
cnf(cls_of__nat__less__0__iff_0,axiom,
( ~ class_Ring__and__Field_Oordered__semidom(X1)
| ~ c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(X2,X1),c_HOL_Ozero__class_Ozero(X1),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_of__nat__less__0__iff_0) ).
cnf(cls_subst__Var__IT_0,axiom,
( c_InductTermi_OIT(c_Lambda_Osubst(X1,c_Lambda_OdB_OVar(X2),X3))
| ~ c_InductTermi_OIT(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_subst__Var__IT_0) ).
cnf(cls_subst__Var_2,axiom,
( c_Lambda_Osubst(c_Lambda_OdB_OVar(X1),X2,X3) = c_Lambda_OdB_OVar(X1)
| X1 = X3
| c_HOL_Oord__class_Oless(X3,X1,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_subst__Var_2) ).
cnf(cls_linorder__neqE__ordered__idom_0,axiom,
( c_HOL_Oord__class_Oless(X2,X3,X1)
| c_HOL_Oord__class_Oless(X3,X2,X1)
| X3 = X2
| ~ class_Ring__and__Field_Oordered__idom(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__neqE__ordered__idom_0) ).
cnf(cls_not__less__iff__gr__or__eq_0,axiom,
( X2 = X3
| c_HOL_Oord__class_Oless(X3,X2,X1)
| c_HOL_Oord__class_Oless(X2,X3,X1)
| ~ class_Orderings_Olinorder(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less__iff__gr__or__eq_0) ).
cnf(cls_linorder__neqE_0,axiom,
( c_HOL_Oord__class_Oless(X2,X3,X1)
| c_HOL_Oord__class_Oless(X3,X2,X1)
| X3 = X2
| ~ class_Orderings_Olinorder(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__neqE_0) ).
cnf(cls_linorder__less__linear_0,axiom,
( c_HOL_Oord__class_Oless(X2,X3,X1)
| X3 = X2
| c_HOL_Oord__class_Oless(X3,X2,X1)
| ~ class_Orderings_Olinorder(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__less__linear_0) ).
cnf(cls_linorder__antisym__conv3_0,axiom,
( X2 = X3
| c_HOL_Oord__class_Oless(X2,X3,X1)
| c_HOL_Oord__class_Oless(X3,X2,X1)
| ~ class_Orderings_Olinorder(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__antisym__conv3_0) ).
cnf(cls_subst__Var_1,axiom,
( c_HOL_Oord__class_Oless(X1,X1,tc_nat)
| c_Lambda_Osubst(c_Lambda_OdB_OVar(X1),X2,X1) = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_subst__Var_1) ).
cnf(cls_nat__neq__iff_0,axiom,
( c_HOL_Oord__class_Oless(X1,X2,tc_nat)
| c_HOL_Oord__class_Oless(X2,X1,tc_nat)
| X2 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat__neq__iff_0) ).
cnf(cls_linorder__neqE__nat_0,axiom,
( c_HOL_Oord__class_Oless(X1,X2,tc_nat)
| c_HOL_Oord__class_Oless(X2,X1,tc_nat)
| X2 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__neqE__nat_0) ).
cnf(cls_lift_Osimps_I1_J_0,axiom,
( c_Lambda_Olift(c_Lambda_OdB_OVar(X1),X2) = c_Lambda_OdB_OVar(X1)
| ~ c_HOL_Oord__class_Oless(X1,X2,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_lift_Osimps_I1_J_0) ).
cnf(cls_lift_Osimps_I2_J_0,axiom,
c_Lambda_Olift(c_Lambda_OdB_OApp(X1,X2),X3) = c_Lambda_OdB_OApp(c_Lambda_Olift(X1,X3),c_Lambda_Olift(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_lift_Osimps_I2_J_0) ).
cnf(cls_order__less__le_1,axiom,
( ~ class_Orderings_Oorder(X1)
| ~ c_HOL_Oord__class_Oless(X2,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__le_1) ).
cnf(cls_linorder__neq__iff_1,axiom,
( ~ class_Orderings_Olinorder(X1)
| ~ c_HOL_Oord__class_Oless(X2,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__neq__iff_1) ).
cnf(cls_order__less__irrefl_0,axiom,
( ~ class_Orderings_Opreorder(X1)
| ~ c_HOL_Oord__class_Oless(X2,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__irrefl_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('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_neq0__conv_1) ).
cnf(cls_lift__preserves__beta_0,axiom,
( c_Lambda_Obeta(c_Lambda_Olift(X1,X2),c_Lambda_Olift(X3,X2))
| ~ c_Lambda_Obeta(X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_lift__preserves__beta_0) ).
cnf(cls_appR_0,axiom,
( c_Lambda_Obeta(c_Lambda_OdB_OApp(X1,X2),c_Lambda_OdB_OApp(X1,X3))
| ~ c_Lambda_Obeta(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_appR_0) ).
cnf(cls_appL_0,axiom,
( c_Lambda_Obeta(c_Lambda_OdB_OApp(X1,X2),c_Lambda_OdB_OApp(X3,X2))
| ~ c_Lambda_Obeta(X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_appL_0) ).
cnf(cls_not__less0_0,axiom,
~ c_HOL_Oord__class_Oless(X1,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less0_0) ).
cnf(cls_gr__implies__not0_0,axiom,
~ c_HOL_Oord__class_Oless(X1,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_gr__implies__not0_0) ).
cnf(cls_nat__less__le_1,axiom,
~ c_HOL_Oord__class_Oless(X1,X1,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat__less__le_1) ).
cnf(cls_less__not__refl_0,axiom,
~ c_HOL_Oord__class_Oless(X1,X1,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_less__not__refl_0) ).
cnf(cls_subst__lift_0,axiom,
c_Lambda_Osubst(c_Lambda_Olift(X1,X2),X3,X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_subst__lift_0) ).
cnf(cls_beta__cases_I2_J_1,axiom,
( c_Lambda_Obeta(X1,c_Lambda_Osko__Lambda__Xbeta__cases__2__1(X1,X2))
| ~ c_Lambda_Obeta(c_Lambda_OdB_OAbs(X1),X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_beta__cases_I2_J_1) ).
cnf(cls_beta__cases_I2_J_0,axiom,
( X1 = c_Lambda_OdB_OAbs(c_Lambda_Osko__Lambda__Xbeta__cases__2__1(X2,X1))
| ~ c_Lambda_Obeta(c_Lambda_OdB_OAbs(X2),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_beta__cases_I2_J_0) ).
cnf(cls_subst__eq_0,axiom,
c_Lambda_Osubst(c_Lambda_OdB_OVar(X1),X2,X1) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_subst__eq_0) ).
cnf(cls_gr0I_0,axiom,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X1,tc_nat)
| X1 = c_HOL_Ozero__class_Ozero(tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_gr0I_0) ).
cnf(cls_of__nat__eq__iff_0,axiom,
( X2 = X3
| ~ class_Nat_Osemiring__char__0(X1)
| c_Nat_Osemiring__1__class_Oof__nat(X2,X1) != c_Nat_Osemiring__1__class_Oof__nat(X3,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_of__nat__eq__iff_0) ).
cnf(cls_app__Var__IT_0,axiom,
( c_InductTermi_OIT(c_Lambda_OdB_OApp(X1,c_Lambda_OdB_OVar(X2)))
| ~ c_InductTermi_OIT(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_app__Var__IT_0) ).
cnf(cls_abs_0,axiom,
( c_Lambda_Obeta(c_Lambda_OdB_OAbs(X1),c_Lambda_OdB_OAbs(X2))
| ~ c_Lambda_Obeta(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_abs_0) ).
cnf(cls_dB_Osimps_I2_J_0,axiom,
( X1 = X3
| c_Lambda_OdB_OApp(X1,X2) != c_Lambda_OdB_OApp(X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dB_Osimps_I2_J_0) ).
cnf(cls_dB_Osimps_I2_J_1,axiom,
( X2 = X4
| c_Lambda_OdB_OApp(X1,X2) != c_Lambda_OdB_OApp(X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dB_Osimps_I2_J_1) ).
cnf(cls_lift__IT_0,axiom,
( c_InductTermi_OIT(c_Lambda_Olift(X1,X2))
| ~ c_InductTermi_OIT(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_lift__IT_0) ).
cnf(cls_beta__cases_I1_J_0,axiom,
~ c_Lambda_Obeta(c_Lambda_OdB_OVar(X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_beta__cases_I1_J_0) ).
cnf(cls_dB_Osimps_I8_J_0,axiom,
c_Lambda_OdB_OApp(X1,X2) != c_Lambda_OdB_OAbs(X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dB_Osimps_I8_J_0) ).
cnf(cls_dB_Osimps_I5_J_0,axiom,
c_Lambda_OdB_OApp(X1,X2) != c_Lambda_OdB_OVar(X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dB_Osimps_I5_J_0) ).
cnf(cls_dB_Osimps_I9_J_0,axiom,
c_Lambda_OdB_OAbs(X1) != c_Lambda_OdB_OApp(X2,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dB_Osimps_I9_J_0) ).
cnf(cls_dB_Osimps_I4_J_0,axiom,
c_Lambda_OdB_OVar(X1) != c_Lambda_OdB_OApp(X2,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dB_Osimps_I4_J_0) ).
cnf(cls_of__nat__0_0,axiom,
( c_Nat_Osemiring__1__class_Oof__nat(c_HOL_Ozero__class_Ozero(tc_nat),X1) = c_HOL_Ozero__class_Ozero(X1)
| ~ class_Ring__and__Field_Osemiring__1(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_of__nat__0_0) ).
cnf(cls_Lambda_0,axiom,
( c_InductTermi_OIT(c_Lambda_OdB_OAbs(X1))
| ~ c_InductTermi_OIT(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Lambda_0) ).
cnf(cls_dB_Osimps_I3_J_0,axiom,
( X1 = X2
| c_Lambda_OdB_OAbs(X1) != c_Lambda_OdB_OAbs(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dB_Osimps_I3_J_0) ).
cnf(cls_dB_Osimps_I1_J_0,axiom,
( X1 = X2
| c_Lambda_OdB_OVar(X1) != c_Lambda_OdB_OVar(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dB_Osimps_I1_J_0) ).
cnf(cls_dB_Osimps_I7_J_0,axiom,
c_Lambda_OdB_OAbs(X1) != c_Lambda_OdB_OVar(X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dB_Osimps_I7_J_0) ).
cnf(cls_dB_Osimps_I6_J_0,axiom,
c_Lambda_OdB_OVar(X1) != c_Lambda_OdB_OAbs(X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dB_Osimps_I6_J_0) ).
cnf(cls_conjecture_0,negated_conjecture,
~ c_InductTermi_OIT(c_Lambda_OdB_OAbs(v_ta______)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
cnf(cls_Var__IT_0,axiom,
c_InductTermi_OIT(c_Lambda_OdB_OVar(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Var__IT_0) ).
cnf(cls_Abs_I2_J_0,axiom,
c_InductTermi_OIT(v_ta______),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Abs_I2_J_0) ).
cnf(clsarity_nat__Orderings_Oorder,axiom,
class_Orderings_Oorder(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_nat__Orderings_Oorder) ).
cnf(clsarity_nat__Orderings_Olinorder,axiom,
class_Orderings_Olinorder(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_nat__Orderings_Olinorder) ).
cnf(clsarity_nat__Orderings_Opreorder,axiom,
class_Orderings_Opreorder(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_nat__Orderings_Opreorder) ).
cnf(clsarity_nat__Nat_Osemiring__char__0,axiom,
class_Nat_Osemiring__char__0(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_nat__Nat_Osemiring__char__0) ).
cnf(clsarity_nat__Ring__and__Field_Osemiring__1,axiom,
class_Ring__and__Field_Osemiring__1(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_nat__Ring__and__Field_Osemiring__1) ).
cnf(clsarity_nat__Ring__and__Field_Oordered__semidom,axiom,
class_Ring__and__Field_Oordered__semidom(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_nat__Ring__and__Field_Oordered__semidom) ).
cnf(i_0_69,axiom,
c_Lambda_Osubst(c_Lambda_OdB_OApp(X1,X2),X3,X4) = c_Lambda_OdB_OApp(c_Lambda_Osubst(X1,X3,X4),c_Lambda_Osubst(X2,X3,X4)),
cls_subst__App_0,
[final] ).
cnf(i_0_70,axiom,
( c_Lambda_Obeta(c_Lambda_Osubst(X1,X2,X3),c_Lambda_Osubst(X4,X2,X3))
| ~ c_Lambda_Obeta(X1,X4) ),
cls_subst__preserves__beta_0,
[final] ).
cnf(i_0_71,axiom,
( c_HOL_Oord__class_Oless(X2,X3,X1)
| ~ class_Orderings_Oorder(X1)
| ~ c_HOL_Oord__class_Oless(X2,X4,X1)
| ~ c_HOL_Oord__class_Oless(X4,X3,X1) ),
cls_xt1_I10_J_0,
[final] ).
cnf(i_0_72,axiom,
( c_HOL_Oord__class_Oless(X2,X3,X1)
| ~ class_Orderings_Opreorder(X1)
| ~ c_HOL_Oord__class_Oless(X4,X3,X1)
| ~ c_HOL_Oord__class_Oless(X2,X4,X1) ),
cls_order__less__trans_0,
[final] ).
cnf(i_0_73,axiom,
( c_HOL_Oord__class_Oless(X2,X3,tc_nat)
| ~ class_Ring__and__Field_Oordered__semidom(X1)
| ~ c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(X2,X1),c_Nat_Osemiring__1__class_Oof__nat(X3,X1),X1) ),
cls_of__nat__less__iff_0,
[final] ).
cnf(i_0_74,axiom,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X2,tc_nat)
| ~ class_Ring__and__Field_Oordered__semidom(X1)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X1),c_Nat_Osemiring__1__class_Oof__nat(X2,X1),X1) ),
cls_of__nat__0__less__iff_0,
[final] ).
cnf(i_0_75,axiom,
( c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(X2,X1),c_Nat_Osemiring__1__class_Oof__nat(X3,X1),X1)
| ~ class_Ring__and__Field_Oordered__semidom(X1)
| ~ c_HOL_Oord__class_Oless(X2,X3,tc_nat) ),
cls_of__nat__less__iff_1,
[final] ).
cnf(i_0_76,axiom,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X1),c_Nat_Osemiring__1__class_Oof__nat(X2,X1),X1)
| ~ class_Ring__and__Field_Oordered__semidom(X1)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X2,tc_nat) ),
cls_of__nat__0__less__iff_1,
[final] ).
cnf(i_0_77,axiom,
( ~ class_Orderings_Oorder(X1)
| ~ c_HOL_Oord__class_Oless(X2,X3,X1)
| ~ c_HOL_Oord__class_Oless(X3,X2,X1) ),
cls_xt1_I9_J_0,
[final] ).
cnf(i_0_78,axiom,
( ~ class_Orderings_Olinorder(X1)
| ~ c_HOL_Oord__class_Oless(X2,X3,X1)
| ~ c_HOL_Oord__class_Oless(X3,X2,X1) ),
cls_not__less__iff__gr__or__eq_1,
[final] ).
cnf(i_0_79,axiom,
( ~ class_Orderings_Opreorder(X1)
| ~ c_HOL_Oord__class_Oless(X2,X3,X1)
| ~ c_HOL_Oord__class_Oless(X3,X2,X1) ),
cls_order__less__asym_0,
[final] ).
cnf(i_0_80,axiom,
( ~ class_Orderings_Opreorder(X1)
| ~ c_HOL_Oord__class_Oless(X2,X3,X1)
| ~ c_HOL_Oord__class_Oless(X3,X2,X1) ),
cls_order__less__asym_H_0,
[final] ).
cnf(i_0_81,axiom,
c_Lambda_Obeta(c_Lambda_OdB_OApp(c_Lambda_OdB_OAbs(X1),X2),c_Lambda_Osubst(X1,X2,c_HOL_Ozero__class_Ozero(tc_nat))),
cls_beta_0,
[final] ).
cnf(i_0_82,axiom,
( c_Lambda_Osubst(c_Lambda_OdB_OVar(X1),X2,X3) = c_Lambda_OdB_OVar(X1)
| ~ c_HOL_Oord__class_Oless(X1,X3,tc_nat) ),
cls_subst__lt_0,
[final] ).
cnf(i_0_83,axiom,
( ~ class_Ring__and__Field_Oordered__semidom(X1)
| ~ c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(X2,X1),c_HOL_Ozero__class_Ozero(X1),X1) ),
cls_of__nat__less__0__iff_0,
[final] ).
cnf(i_0_84,axiom,
( c_InductTermi_OIT(c_Lambda_Osubst(X1,c_Lambda_OdB_OVar(X2),X3))
| ~ c_InductTermi_OIT(X1) ),
cls_subst__Var__IT_0,
[final] ).
cnf(i_0_85,axiom,
( c_Lambda_Osubst(c_Lambda_OdB_OVar(X1),X2,X3) = c_Lambda_OdB_OVar(X1)
| X1 = X3
| c_HOL_Oord__class_Oless(X3,X1,tc_nat) ),
cls_subst__Var_2,
[final] ).
cnf(i_0_86,axiom,
( c_HOL_Oord__class_Oless(X2,X3,X1)
| c_HOL_Oord__class_Oless(X3,X2,X1)
| X3 = X2
| ~ class_Ring__and__Field_Oordered__idom(X1) ),
cls_linorder__neqE__ordered__idom_0,
[final] ).
cnf(i_0_87,axiom,
( X2 = X3
| c_HOL_Oord__class_Oless(X3,X2,X1)
| c_HOL_Oord__class_Oless(X2,X3,X1)
| ~ class_Orderings_Olinorder(X1) ),
cls_not__less__iff__gr__or__eq_0,
[final] ).
cnf(i_0_88,axiom,
( c_HOL_Oord__class_Oless(X2,X3,X1)
| c_HOL_Oord__class_Oless(X3,X2,X1)
| X3 = X2
| ~ class_Orderings_Olinorder(X1) ),
cls_linorder__neqE_0,
[final] ).
cnf(i_0_89,axiom,
( c_HOL_Oord__class_Oless(X2,X3,X1)
| X3 = X2
| c_HOL_Oord__class_Oless(X3,X2,X1)
| ~ class_Orderings_Olinorder(X1) ),
cls_linorder__less__linear_0,
[final] ).
cnf(i_0_90,axiom,
( X2 = X3
| c_HOL_Oord__class_Oless(X2,X3,X1)
| c_HOL_Oord__class_Oless(X3,X2,X1)
| ~ class_Orderings_Olinorder(X1) ),
cls_linorder__antisym__conv3_0,
[final] ).
cnf(i_0_91,axiom,
( c_HOL_Oord__class_Oless(X1,X1,tc_nat)
| c_Lambda_Osubst(c_Lambda_OdB_OVar(X1),X2,X1) = X2 ),
cls_subst__Var_1,
[final] ).
cnf(i_0_92,axiom,
( c_HOL_Oord__class_Oless(X1,X2,tc_nat)
| c_HOL_Oord__class_Oless(X2,X1,tc_nat)
| X2 = X1 ),
cls_nat__neq__iff_0,
[final] ).
cnf(i_0_93,axiom,
( c_HOL_Oord__class_Oless(X1,X2,tc_nat)
| c_HOL_Oord__class_Oless(X2,X1,tc_nat)
| X2 = X1 ),
cls_linorder__neqE__nat_0,
[final] ).
cnf(i_0_94,axiom,
( c_Lambda_Olift(c_Lambda_OdB_OVar(X1),X2) = c_Lambda_OdB_OVar(X1)
| ~ c_HOL_Oord__class_Oless(X1,X2,tc_nat) ),
cls_lift_Osimps_I1_J_0,
[final] ).
cnf(i_0_95,axiom,
c_Lambda_Olift(c_Lambda_OdB_OApp(X1,X2),X3) = c_Lambda_OdB_OApp(c_Lambda_Olift(X1,X3),c_Lambda_Olift(X2,X3)),
cls_lift_Osimps_I2_J_0,
[final] ).
cnf(i_0_96,axiom,
( ~ class_Orderings_Oorder(X1)
| ~ c_HOL_Oord__class_Oless(X2,X2,X1) ),
cls_order__less__le_1,
[final] ).
cnf(i_0_97,axiom,
( ~ class_Orderings_Olinorder(X1)
| ~ c_HOL_Oord__class_Oless(X2,X2,X1) ),
cls_linorder__neq__iff_1,
[final] ).
cnf(i_0_98,axiom,
( ~ class_Orderings_Opreorder(X1)
| ~ c_HOL_Oord__class_Oless(X2,X2,X1) ),
cls_order__less__irrefl_0,
[final] ).
cnf(i_0_99,axiom,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
cls_neq0__conv_1,
[final] ).
cnf(i_0_100,axiom,
( c_Lambda_Obeta(c_Lambda_Olift(X1,X2),c_Lambda_Olift(X3,X2))
| ~ c_Lambda_Obeta(X1,X3) ),
cls_lift__preserves__beta_0,
[final] ).
cnf(i_0_101,axiom,
( c_Lambda_Obeta(c_Lambda_OdB_OApp(X1,X2),c_Lambda_OdB_OApp(X1,X3))
| ~ c_Lambda_Obeta(X2,X3) ),
cls_appR_0,
[final] ).
cnf(i_0_102,axiom,
( c_Lambda_Obeta(c_Lambda_OdB_OApp(X1,X2),c_Lambda_OdB_OApp(X3,X2))
| ~ c_Lambda_Obeta(X1,X3) ),
cls_appL_0,
[final] ).
cnf(i_0_103,axiom,
~ c_HOL_Oord__class_Oless(X1,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
cls_not__less0_0,
[final] ).
cnf(i_0_104,axiom,
~ c_HOL_Oord__class_Oless(X1,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
cls_gr__implies__not0_0,
[final] ).
cnf(i_0_105,axiom,
~ c_HOL_Oord__class_Oless(X1,X1,tc_nat),
cls_nat__less__le_1,
[final] ).
cnf(i_0_106,axiom,
~ c_HOL_Oord__class_Oless(X1,X1,tc_nat),
cls_less__not__refl_0,
[final] ).
cnf(i_0_107,axiom,
c_Lambda_Osubst(c_Lambda_Olift(X1,X2),X3,X2) = X1,
cls_subst__lift_0,
[final] ).
cnf(i_0_108,axiom,
( c_Lambda_Obeta(X1,c_Lambda_Osko__Lambda__Xbeta__cases__2__1(X1,X2))
| ~ c_Lambda_Obeta(c_Lambda_OdB_OAbs(X1),X2) ),
cls_beta__cases_I2_J_1,
[final] ).
cnf(i_0_109,axiom,
( X1 = c_Lambda_OdB_OAbs(c_Lambda_Osko__Lambda__Xbeta__cases__2__1(X2,X1))
| ~ c_Lambda_Obeta(c_Lambda_OdB_OAbs(X2),X1) ),
cls_beta__cases_I2_J_0,
[final] ).
cnf(i_0_110,axiom,
c_Lambda_Osubst(c_Lambda_OdB_OVar(X1),X2,X1) = X2,
cls_subst__eq_0,
[final] ).
cnf(i_0_111,axiom,
( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X1,tc_nat)
| X1 = c_HOL_Ozero__class_Ozero(tc_nat) ),
cls_gr0I_0,
[final] ).
cnf(i_0_112,axiom,
( X2 = X3
| ~ class_Nat_Osemiring__char__0(X1)
| c_Nat_Osemiring__1__class_Oof__nat(X2,X1) != c_Nat_Osemiring__1__class_Oof__nat(X3,X1) ),
cls_of__nat__eq__iff_0,
[final] ).
cnf(i_0_113,axiom,
( c_InductTermi_OIT(c_Lambda_OdB_OApp(X1,c_Lambda_OdB_OVar(X2)))
| ~ c_InductTermi_OIT(X1) ),
cls_app__Var__IT_0,
[final] ).
cnf(i_0_114,axiom,
( c_Lambda_Obeta(c_Lambda_OdB_OAbs(X1),c_Lambda_OdB_OAbs(X2))
| ~ c_Lambda_Obeta(X1,X2) ),
cls_abs_0,
[final] ).
cnf(i_0_115,axiom,
( X1 = X3
| c_Lambda_OdB_OApp(X1,X2) != c_Lambda_OdB_OApp(X3,X4) ),
cls_dB_Osimps_I2_J_0,
[final] ).
cnf(i_0_116,axiom,
( X2 = X4
| c_Lambda_OdB_OApp(X1,X2) != c_Lambda_OdB_OApp(X3,X4) ),
cls_dB_Osimps_I2_J_1,
[final] ).
cnf(i_0_117,axiom,
( c_InductTermi_OIT(c_Lambda_Olift(X1,X2))
| ~ c_InductTermi_OIT(X1) ),
cls_lift__IT_0,
[final] ).
cnf(i_0_118,axiom,
~ c_Lambda_Obeta(c_Lambda_OdB_OVar(X1),X2),
cls_beta__cases_I1_J_0,
[final] ).
cnf(i_0_119,axiom,
c_Lambda_OdB_OApp(X1,X2) != c_Lambda_OdB_OAbs(X3),
cls_dB_Osimps_I8_J_0,
[final] ).
cnf(i_0_120,axiom,
c_Lambda_OdB_OApp(X1,X2) != c_Lambda_OdB_OVar(X3),
cls_dB_Osimps_I5_J_0,
[final] ).
cnf(i_0_121,axiom,
c_Lambda_OdB_OAbs(X1) != c_Lambda_OdB_OApp(X2,X3),
cls_dB_Osimps_I9_J_0,
[final] ).
cnf(i_0_122,axiom,
c_Lambda_OdB_OVar(X1) != c_Lambda_OdB_OApp(X2,X3),
cls_dB_Osimps_I4_J_0,
[final] ).
cnf(i_0_123,axiom,
( c_Nat_Osemiring__1__class_Oof__nat(c_HOL_Ozero__class_Ozero(tc_nat),X1) = c_HOL_Ozero__class_Ozero(X1)
| ~ class_Ring__and__Field_Osemiring__1(X1) ),
cls_of__nat__0_0,
[final] ).
cnf(i_0_124,axiom,
( c_InductTermi_OIT(c_Lambda_OdB_OAbs(X1))
| ~ c_InductTermi_OIT(X1) ),
cls_Lambda_0,
[final] ).
cnf(i_0_125,axiom,
( X1 = X2
| c_Lambda_OdB_OAbs(X1) != c_Lambda_OdB_OAbs(X2) ),
cls_dB_Osimps_I3_J_0,
[final] ).
cnf(i_0_126,axiom,
( X1 = X2
| c_Lambda_OdB_OVar(X1) != c_Lambda_OdB_OVar(X2) ),
cls_dB_Osimps_I1_J_0,
[final] ).
cnf(i_0_127,axiom,
c_Lambda_OdB_OAbs(X1) != c_Lambda_OdB_OVar(X2),
cls_dB_Osimps_I7_J_0,
[final] ).
cnf(i_0_128,axiom,
c_Lambda_OdB_OVar(X1) != c_Lambda_OdB_OAbs(X2),
cls_dB_Osimps_I6_J_0,
[final] ).
cnf(i_0_129,negated_conjecture,
~ c_InductTermi_OIT(c_Lambda_OdB_OAbs(v_ta______)),
cls_conjecture_0,
[final] ).
cnf(i_0_130,axiom,
c_InductTermi_OIT(c_Lambda_OdB_OVar(X1)),
cls_Var__IT_0,
[final] ).
cnf(i_0_131,axiom,
c_InductTermi_OIT(v_ta______),
cls_Abs_I2_J_0,
[final] ).
cnf(i_0_132,axiom,
class_Orderings_Oorder(tc_nat),
clsarity_nat__Orderings_Oorder,
[final] ).
cnf(i_0_133,axiom,
class_Orderings_Olinorder(tc_nat),
clsarity_nat__Orderings_Olinorder,
[final] ).
cnf(i_0_134,axiom,
class_Orderings_Opreorder(tc_nat),
clsarity_nat__Orderings_Opreorder,
[final] ).
cnf(i_0_135,axiom,
class_Nat_Osemiring__char__0(tc_nat),
clsarity_nat__Nat_Osemiring__char__0,
[final] ).
cnf(i_0_136,axiom,
class_Ring__and__Field_Osemiring__1(tc_nat),
clsarity_nat__Ring__and__Field_Osemiring__1,
[final] ).
cnf(i_0_137,axiom,
class_Ring__and__Field_Oordered__semidom(tc_nat),
clsarity_nat__Ring__and__Field_Oordered__semidom,
[final] ).
cnf(i_0_138,axiom,
X1 = X1 ).
cnf(i_0_139,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_140,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_141,axiom,
( X1 != X2
| c_Lambda_Osubst(X1,X3,X4) = c_Lambda_Osubst(X2,X3,X4) ) ).
cnf(i_0_142,axiom,
( X1 != X2
| c_Lambda_Osubst(X3,X1,X4) = c_Lambda_Osubst(X3,X2,X4) ) ).
cnf(i_0_143,axiom,
( X1 != X2
| c_Lambda_Osubst(X3,X4,X1) = c_Lambda_Osubst(X3,X4,X2) ) ).
cnf(i_0_144,axiom,
( X1 != X2
| c_Lambda_OdB_OApp(X1,X3) = c_Lambda_OdB_OApp(X2,X3) ) ).
cnf(i_0_145,axiom,
( X1 != X2
| c_Lambda_OdB_OApp(X3,X1) = c_Lambda_OdB_OApp(X3,X2) ) ).
cnf(i_0_146,axiom,
( X1 != X2
| c_Nat_Osemiring__1__class_Oof__nat(X1,X3) = c_Nat_Osemiring__1__class_Oof__nat(X2,X3) ) ).
cnf(i_0_147,axiom,
( X1 != X2
| c_Nat_Osemiring__1__class_Oof__nat(X3,X1) = c_Nat_Osemiring__1__class_Oof__nat(X3,X2) ) ).
cnf(i_0_148,axiom,
( X1 != X2
| c_HOL_Ozero__class_Ozero(X1) = c_HOL_Ozero__class_Ozero(X2) ) ).
cnf(i_0_149,axiom,
( X1 != X2
| c_Lambda_OdB_OAbs(X1) = c_Lambda_OdB_OAbs(X2) ) ).
cnf(i_0_150,axiom,
( X1 != X2
| c_Lambda_OdB_OVar(X1) = c_Lambda_OdB_OVar(X2) ) ).
cnf(i_0_151,axiom,
( X1 != X2
| c_Lambda_Olift(X1,X3) = c_Lambda_Olift(X2,X3) ) ).
cnf(i_0_152,axiom,
( X1 != X2
| c_Lambda_Olift(X3,X1) = c_Lambda_Olift(X3,X2) ) ).
cnf(i_0_153,axiom,
( X1 != X2
| ~ c_Lambda_Obeta(X1,X3)
| c_Lambda_Obeta(X2,X3) ) ).
cnf(i_0_154,axiom,
( X1 != X2
| ~ c_Lambda_Obeta(X3,X1)
| c_Lambda_Obeta(X3,X2) ) ).
cnf(i_0_155,axiom,
( X1 != X2
| ~ class_Ring__and__Field_Osemiring__1(X1)
| class_Ring__and__Field_Osemiring__1(X2) ) ).
cnf(i_0_156,axiom,
( X1 != X2
| ~ c_HOL_Oord__class_Oless(X1,X3,X4)
| c_HOL_Oord__class_Oless(X2,X3,X4) ) ).
cnf(i_0_157,axiom,
( X1 != X2
| ~ c_HOL_Oord__class_Oless(X3,X1,X4)
| c_HOL_Oord__class_Oless(X3,X2,X4) ) ).
cnf(i_0_158,axiom,
( X1 != X2
| ~ c_HOL_Oord__class_Oless(X3,X4,X1)
| c_HOL_Oord__class_Oless(X3,X4,X2) ) ).
cnf(i_0_159,axiom,
( X1 != X2
| ~ class_Orderings_Oorder(X1)
| class_Orderings_Oorder(X2) ) ).
cnf(i_0_160,axiom,
( X1 != X2
| ~ class_Orderings_Opreorder(X1)
| class_Orderings_Opreorder(X2) ) ).
cnf(i_0_161,axiom,
( X1 != X2
| ~ class_Ring__and__Field_Oordered__semidom(X1)
| class_Ring__and__Field_Oordered__semidom(X2) ) ).
cnf(i_0_162,axiom,
( X1 != X2
| ~ class_Orderings_Olinorder(X1)
| class_Orderings_Olinorder(X2) ) ).
cnf(i_0_163,axiom,
( X1 != X2
| ~ c_InductTermi_OIT(X1)
| c_InductTermi_OIT(X2) ) ).
cnf(i_0_164,axiom,
( X1 != X2
| ~ class_Ring__and__Field_Oordered__idom(X1)
| class_Ring__and__Field_Oordered__idom(X2) ) ).
cnf(i_0_165,axiom,
( X1 != X2
| ~ class_Nat_Osemiring__char__0(X1)
| class_Nat_Osemiring__char__0(X2) ) ).
cnf(i_0_138_001,axiom,
X1 = X1 ).
cnf(i_0_139_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_140_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_141_004,axiom,
( X1 != X2
| c_Lambda_Osubst(X1,X3,X4) = c_Lambda_Osubst(X2,X3,X4) ) ).
cnf(i_0_142_005,axiom,
( X1 != X2
| c_Lambda_Osubst(X3,X1,X4) = c_Lambda_Osubst(X3,X2,X4) ) ).
cnf(i_0_143_006,axiom,
( X1 != X2
| c_Lambda_Osubst(X3,X4,X1) = c_Lambda_Osubst(X3,X4,X2) ) ).
cnf(i_0_144_007,axiom,
( X1 != X2
| c_Lambda_OdB_OApp(X1,X3) = c_Lambda_OdB_OApp(X2,X3) ) ).
cnf(i_0_145_008,axiom,
( X1 != X2
| c_Lambda_OdB_OApp(X3,X1) = c_Lambda_OdB_OApp(X3,X2) ) ).
cnf(i_0_146_009,axiom,
( X1 != X2
| c_Nat_Osemiring__1__class_Oof__nat(X1,X3) = c_Nat_Osemiring__1__class_Oof__nat(X2,X3) ) ).
cnf(i_0_147_010,axiom,
( X1 != X2
| c_Nat_Osemiring__1__class_Oof__nat(X3,X1) = c_Nat_Osemiring__1__class_Oof__nat(X3,X2) ) ).
cnf(i_0_148_011,axiom,
( X1 != X2
| c_HOL_Ozero__class_Ozero(X1) = c_HOL_Ozero__class_Ozero(X2) ) ).
cnf(i_0_149_012,axiom,
( X1 != X2
| c_Lambda_OdB_OAbs(X1) = c_Lambda_OdB_OAbs(X2) ) ).
cnf(i_0_150_013,axiom,
( X1 != X2
| c_Lambda_OdB_OVar(X1) = c_Lambda_OdB_OVar(X2) ) ).
cnf(i_0_151_014,axiom,
( X1 != X2
| c_Lambda_Olift(X1,X3) = c_Lambda_Olift(X2,X3) ) ).
cnf(i_0_152_015,axiom,
( X1 != X2
| c_Lambda_Olift(X3,X1) = c_Lambda_Olift(X3,X2) ) ).
cnf(i_0_153_016,axiom,
( X1 != X2
| ~ c_Lambda_Obeta(X1,X3)
| c_Lambda_Obeta(X2,X3) ) ).
cnf(i_0_154_017,axiom,
( X1 != X2
| ~ c_Lambda_Obeta(X3,X1)
| c_Lambda_Obeta(X3,X2) ) ).
cnf(i_0_155_018,axiom,
( X1 != X2
| ~ class_Ring__and__Field_Osemiring__1(X1)
| class_Ring__and__Field_Osemiring__1(X2) ) ).
cnf(i_0_156_019,axiom,
( X1 != X2
| ~ c_HOL_Oord__class_Oless(X1,X3,X4)
| c_HOL_Oord__class_Oless(X2,X3,X4) ) ).
cnf(i_0_157_020,axiom,
( X1 != X2
| ~ c_HOL_Oord__class_Oless(X3,X1,X4)
| c_HOL_Oord__class_Oless(X3,X2,X4) ) ).
cnf(i_0_158_021,axiom,
( X1 != X2
| ~ c_HOL_Oord__class_Oless(X3,X4,X1)
| c_HOL_Oord__class_Oless(X3,X4,X2) ) ).
cnf(i_0_159_022,axiom,
( X1 != X2
| ~ class_Orderings_Oorder(X1)
| class_Orderings_Oorder(X2) ) ).
cnf(i_0_160_023,axiom,
( X1 != X2
| ~ class_Orderings_Opreorder(X1)
| class_Orderings_Opreorder(X2) ) ).
cnf(i_0_161_024,axiom,
( X1 != X2
| ~ class_Ring__and__Field_Oordered__semidom(X1)
| class_Ring__and__Field_Oordered__semidom(X2) ) ).
cnf(i_0_162_025,axiom,
( X1 != X2
| ~ class_Orderings_Olinorder(X1)
| class_Orderings_Olinorder(X2) ) ).
cnf(i_0_163_026,axiom,
( X1 != X2
| ~ c_InductTermi_OIT(X1)
| c_InductTermi_OIT(X2) ) ).
cnf(i_0_164_027,axiom,
( X1 != X2
| ~ class_Ring__and__Field_Oordered__idom(X1)
| class_Ring__and__Field_Oordered__idom(X2) ) ).
cnf(i_0_165_028,axiom,
( X1 != X2
| ~ class_Nat_Osemiring__char__0(X1)
| class_Nat_Osemiring__char__0(X2) ) ).
cnf(i_0_166,plain,
( X1 = X1
| ~ class_Nat_Osemiring__char__0(X2) ),
inference(equality_inference,[],[112]) ).
cnf(i_0_167,plain,
X1 = X1,
inference(equality_inference,[],[115]) ).
cnf(i_0_168,plain,
X1 = X1,
inference(equality_inference,[],[116]) ).
cnf(i_0_169,plain,
X1 = X1,
inference(equality_inference,[],[125]) ).
cnf(i_0_170,plain,
X1 = X1,
inference(equality_inference,[],[126]) ).
cnf(i_0_171,plain,
$false,
inference(scs_inference,[],[i_0_129,i_0_131,i_0_124]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : LCL844-1 : TPTP v9.2.1. Released v4.1.0.
% 0.00/0.11 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.14/0.32 % Computer : n013.cluster.edu
% 0.14/0.32 % Model : x86_64 x86_64
% 0.14/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.32 % Memory : 8042.1875MB
% 0.14/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.32 % CPULimit : 300
% 0.14/0.32 % WCLimit : 300
% 0.14/0.32 % DateTime : Mon May 4 23:11:41 EDT 2026
% 0.14/0.32 % CPUTime :
% 0.14/0.33 % start to proof: theBenchmark
% 0.28/1.61 % Version : CSE_E---1.7
% 0.28/1.61 % Problem : theBenchmark.p
% 0.28/1.61 % SZS status Unsatisfiable for theBenchmark.p
% 0.28/1.61 % SZS output start CNFRefutation
% See solution above
% 0.28/1.63 % Total time : 1.273s
%------------------------------------------------------------------------------