%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL748-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n018.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 : Fri Sep 25 02:02:46 PM UTC 2026
% Result : Unsatisfiable 11.18s 1.83s
% Output : Proof 11.18s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t191,axiom,
sF0 = c_InductTermi_OIT(v_r),
introduced(definition) ).
cnf(f342,negated_conjecture,
c_InductTermi_OIT(v_r),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f342_nnf,plain,
c_InductTermi_OIT(v_r),
inference(nnf_transformation,[status(thm)],[f342]) ).
cnf(c342,plain,
c_InductTermi_OIT(v_r),
inference(cnf_transformation,[status(esa)],[f342_nnf]) ).
cnf(t0,plain,
c_InductTermi_OIT(v_r) = true,
inference(equality_encoding,[status(esa)],[c342]) ).
cnf(t198,plain,
c_InductTermi_OIT(v_r) = true,
inference(orient,[status(thm)],[t0]) ).
cnf(t683,plain,
sF0 = true,
inference(step,[status(thm)],[t191,t198]) ).
cnf(t199,plain,
true = sF0,
inference(orient,[status(thm)],[t683]) ).
cnf(t196,axiom,
sF5 = c_InductTermi_OIT(c_Lambda_Olift(c_Lambda_OdB_OAbs(v_r),v_ia)),
introduced(definition) ).
cnf(t194,axiom,
sF3 = c_Lambda_OdB_OAbs(v_r),
introduced(definition) ).
cnf(t202,plain,
c_Lambda_OdB_OAbs(v_r) = sF3,
inference(orient,[status(thm)],[t194]) ).
cnf(t698,plain,
sF5 = c_InductTermi_OIT(c_Lambda_Olift(sF3,v_ia)),
inference(step,[status(thm)],[t196,t202]) ).
cnf(t195,axiom,
sF4 = c_Lambda_Olift(c_Lambda_OdB_OAbs(v_r),v_ia),
introduced(definition) ).
cnf(t695,plain,
sF4 = c_Lambda_Olift(sF3,v_ia),
inference(step,[status(thm)],[t195,t202]) ).
cnf(t214,plain,
c_Lambda_Olift(sF3,v_ia) = sF4,
inference(orient,[status(thm)],[t695]) ).
cnf(t699,plain,
sF5 = c_InductTermi_OIT(sF4),
inference(step,[status(thm)],[t698,t214]) ).
cnf(f344,negated_conjecture,
~ c_InductTermi_OIT(c_Lambda_Olift(c_Lambda_OdB_OAbs(v_r),v_ia)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f344_nnf,plain,
~ c_InductTermi_OIT(c_Lambda_Olift(c_Lambda_OdB_OAbs(v_r),v_ia)),
inference(nnf_transformation,[status(thm)],[f344]) ).
fof(f344_sk,plain,
~ c_InductTermi_OIT(c_Lambda_Olift(c_Lambda_OdB_OAbs(v_r),v_ia)),
inference(skolemisation,[status(esa)],[f344_nnf]) ).
cnf(c344,plain,
~ c_InductTermi_OIT(c_Lambda_Olift(c_Lambda_OdB_OAbs(v_r),v_ia)),
inference(cnf_transformation,[status(esa)],[f344_sk]) ).
cnf(t17,plain,
c_InductTermi_OIT(c_Lambda_Olift(c_Lambda_OdB_OAbs(v_r),v_ia)) = false,
inference(equality_encoding,[status(esa)],[c344]) ).
cnf(t696,plain,
c_InductTermi_OIT(c_Lambda_Olift(sF3,v_ia)) = false,
inference(step,[status(thm)],[t17,t202]) ).
cnf(t697,plain,
c_InductTermi_OIT(sF4) = false,
inference(step,[status(thm)],[t696,t214]) ).
cnf(t219,plain,
c_InductTermi_OIT(sF4) = false,
inference(orient,[status(thm)],[t697]) ).
cnf(t700,plain,
sF5 = false,
inference(step,[status(thm)],[t699,t219]) ).
cnf(t230,plain,
false = sF5,
inference(orient,[status(thm)],[t700]) ).
cnf(f338,axiom,
( ~ c_InductTermi_OIT(V_r)
| c_InductTermi_OIT(c_Lambda_OdB_OAbs(V_r)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Lambda_0) ).
fof(f338_nnf,plain,
! [V_r] :
( ~ c_InductTermi_OIT(V_r)
| c_InductTermi_OIT(c_Lambda_OdB_OAbs(V_r)) ),
inference(nnf_transformation,[status(thm)],[f338]) ).
fof(f338_sk,plain,
! [V_r] :
( ~ c_InductTermi_OIT(V_r)
| c_InductTermi_OIT(c_Lambda_OdB_OAbs(V_r)) ),
inference(skolemisation,[status(esa)],[f338_nnf]) ).
cnf(c338,plain,
( ~ c_InductTermi_OIT(X0)
| c_InductTermi_OIT(c_Lambda_OdB_OAbs(X0)) ),
inference(cnf_transformation,[status(esa)],[f338_sk]) ).
cnf(t53,plain,
ifeq(c_InductTermi_OIT(X1),true,c_InductTermi_OIT(c_Lambda_OdB_OAbs(X1)),true) = true,
inference(equality_encoding,[status(esa)],[c338]) ).
cnf(t742,plain,
ifeq(c_InductTermi_OIT(X1),sF0,c_InductTermi_OIT(c_Lambda_OdB_OAbs(X1)),true) = true,
inference(step,[status(thm)],[t53,t199]) ).
cnf(t743,plain,
ifeq(c_InductTermi_OIT(X1),sF0,c_InductTermi_OIT(c_Lambda_OdB_OAbs(X1)),sF0) = true,
inference(step,[status(thm)],[t742,t199]) ).
cnf(t744,plain,
ifeq(c_InductTermi_OIT(X1),sF0,c_InductTermi_OIT(c_Lambda_OdB_OAbs(X1)),sF0) = sF0,
inference(step,[status(thm)],[t743,t199]) ).
cnf(t495,plain,
ifeq(c_InductTermi_OIT(X1),sF0,c_InductTermi_OIT(c_Lambda_OdB_OAbs(X1)),sF0) = sF0,
inference(orient,[status(thm)],[t744]) ).
cnf(f331,axiom,
c_Lambda_Olift(c_Lambda_OdB_OAbs(V_s),V_k) = c_Lambda_OdB_OAbs(c_Lambda_Olift(V_s,c_HOL_Oplus__class_Oplus(V_k,c_HOL_Oone__class_Oone(tc_nat),tc_nat))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_lift_Osimps_I3_J_0) ).
fof(f331_nnf,plain,
! [V_s,V_k] : c_Lambda_Olift(c_Lambda_OdB_OAbs(V_s),V_k) = c_Lambda_OdB_OAbs(c_Lambda_Olift(V_s,c_HOL_Oplus__class_Oplus(V_k,c_HOL_Oone__class_Oone(tc_nat),tc_nat))),
inference(nnf_transformation,[status(thm)],[f331]) ).
fof(f331_sk,plain,
! [V_s,V_k] : c_Lambda_Olift(c_Lambda_OdB_OAbs(V_s),V_k) = c_Lambda_OdB_OAbs(c_Lambda_Olift(V_s,c_HOL_Oplus__class_Oplus(V_k,c_HOL_Oone__class_Oone(tc_nat),tc_nat))),
inference(skolemisation,[status(esa)],[f331_nnf]) ).
cnf(c331,plain,
c_Lambda_Olift(c_Lambda_OdB_OAbs(X0),X1) = c_Lambda_OdB_OAbs(c_Lambda_Olift(X0,c_HOL_Oplus__class_Oplus(X1,c_HOL_Oone__class_Oone(tc_nat),tc_nat))),
inference(cnf_transformation,[status(esa)],[f331_sk]) ).
cnf(t84,plain,
c_Lambda_OdB_OAbs(c_Lambda_Olift(X1,c_HOL_Oplus__class_Oplus(X2,c_HOL_Oone__class_Oone(tc_nat),tc_nat))) = c_Lambda_Olift(c_Lambda_OdB_OAbs(X1),X2),
inference(equality_encoding,[status(esa)],[c331]) ).
cnf(t534,plain,
c_Lambda_OdB_OAbs(c_Lambda_Olift(X1,c_HOL_Oplus__class_Oplus(X2,c_HOL_Oone__class_Oone(tc_nat),tc_nat))) = c_Lambda_Olift(c_Lambda_OdB_OAbs(X1),X2),
inference(orient,[status(thm)],[t84]) ).
cnf(t192,axiom,
sF1(X1) = c_Lambda_Olift(v_r,X1),
introduced(definition) ).
cnf(t208,plain,
c_Lambda_Olift(v_r,X1) = sF1(X1),
inference(orient,[status(thm)],[t192]) ).
cnf(t535,plain,
c_Lambda_Olift(c_Lambda_OdB_OAbs(v_r),X1) = c_Lambda_OdB_OAbs(sF1(c_HOL_Oplus__class_Oplus(X1,c_HOL_Oone__class_Oone(tc_nat),tc_nat))),
inference(cp,[status(thm)],[t534,t208]) ).
cnf(t771,plain,
c_Lambda_Olift(sF3,X1) = c_Lambda_OdB_OAbs(sF1(c_HOL_Oplus__class_Oplus(X1,c_HOL_Oone__class_Oone(tc_nat),tc_nat))),
inference(step,[status(thm)],[t535,t202]) ).
cnf(t582,plain,
c_Lambda_OdB_OAbs(sF1(c_HOL_Oplus__class_Oplus(X1,c_HOL_Oone__class_Oone(tc_nat),tc_nat))) = c_Lambda_Olift(sF3,X1),
inference(orient,[status(thm)],[t771]) ).
cnf(t597,plain,
sF0 = ifeq(c_InductTermi_OIT(sF1(c_HOL_Oplus__class_Oplus(X1,c_HOL_Oone__class_Oone(tc_nat),tc_nat))),sF0,c_InductTermi_OIT(c_Lambda_Olift(sF3,X1)),sF0),
inference(cp,[status(thm)],[t495,t582]) ).
cnf(f343,negated_conjecture,
c_InductTermi_OIT(c_Lambda_Olift(v_r,V_i)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f343_nnf,plain,
! [V_i] : c_InductTermi_OIT(c_Lambda_Olift(v_r,V_i)),
inference(nnf_transformation,[status(thm)],[f343]) ).
fof(f343_sk,plain,
! [V_i] : c_InductTermi_OIT(c_Lambda_Olift(v_r,V_i)),
inference(skolemisation,[status(esa)],[f343_nnf]) ).
cnf(c343,plain,
c_InductTermi_OIT(c_Lambda_Olift(v_r,X0)),
inference(cnf_transformation,[status(esa)],[f343_sk]) ).
cnf(t8,plain,
c_InductTermi_OIT(c_Lambda_Olift(v_r,X1)) = true,
inference(equality_encoding,[status(esa)],[c343]) ).
cnf(t691,plain,
c_InductTermi_OIT(sF1(X1)) = true,
inference(step,[status(thm)],[t8,t208]) ).
cnf(t692,plain,
c_InductTermi_OIT(sF1(X1)) = sF0,
inference(step,[status(thm)],[t691,t199]) ).
cnf(t210,plain,
c_InductTermi_OIT(sF1(X1)) = sF0,
inference(orient,[status(thm)],[t692]) ).
cnf(t772,plain,
sF0 = ifeq(sF0,sF0,c_InductTermi_OIT(c_Lambda_Olift(sF3,X1)),sF0),
inference(step,[status(thm)],[t597,t210]) ).
cnf(t22,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t228,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t22]) ).
cnf(t773,plain,
sF0 = c_InductTermi_OIT(c_Lambda_Olift(sF3,X1)),
inference(step,[status(thm)],[t772,t228]) ).
cnf(t603,plain,
c_InductTermi_OIT(c_Lambda_Olift(sF3,X1)) = sF0,
inference(orient,[status(thm)],[t773]) ).
cnf(t605,plain,
sF0 = c_InductTermi_OIT(sF4),
inference(cp,[status(thm)],[t603,t214]) ).
cnf(t709,plain,
c_InductTermi_OIT(sF4) = sF5,
inference(step,[status(thm)],[t219,t230]) ).
cnf(t239,plain,
c_InductTermi_OIT(sF4) = sF5,
inference(orient,[status(thm)],[t709]) ).
cnf(t775,plain,
sF0 = sF5,
inference(step,[status(thm)],[t605,t239]) ).
cnf(t606,plain,
sF5 = sF0,
inference(orient,[status(thm)],[t775]) ).
cnf(t792,plain,
false = sF0,
inference(step,[status(thm)],[t230,t606]) ).
cnf(t623,plain,
false = sF0,
inference(orient,[status(thm)],[t792]) ).
cnf(f9,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,T_a),c_HOL_Otimes__class_Otimes(V_y,V_y,T_a),T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__sum__squares__lt__zero_0) ).
fof(f9_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,T_a),c_HOL_Otimes__class_Otimes(V_y,V_y,T_a),T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,T_a),c_HOL_Otimes__class_Otimes(V_y,V_y,T_a),T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X1,X1,X0),c_HOL_Otimes__class_Otimes(X2,X2,X0),X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__ring__strict(X0) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(f10,axiom,
( c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_one__neq__zero_0) ).
fof(f10_nnf,plain,
! [T_a] :
( c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [T_a] :
( c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( c_HOL_Oone__class_Oone(X0) != c_HOL_Ozero__class_Ozero(X0)
| ~ class_Ring__and__Field_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(f11,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__one__less__zero_0) ).
fof(f11_nnf,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__semidom(T_a) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__semidom(X0) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(f63,axiom,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Zero__neq__Suc_0) ).
fof(f63_nnf,plain,
! [V_m] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
inference(nnf_transformation,[status(thm)],[f63]) ).
fof(f63_sk,plain,
! [V_m] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
inference(skolemisation,[status(esa)],[f63_nnf]) ).
cnf(c63,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f63_sk]) ).
cnf(f64,axiom,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat_Osimps_I2_J_0) ).
fof(f64_nnf,plain,
! [V_nat_H] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
inference(nnf_transformation,[status(thm)],[f64]) ).
fof(f64_sk,plain,
! [V_nat_H] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
inference(skolemisation,[status(esa)],[f64_nnf]) ).
cnf(c64,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f64_sk]) ).
cnf(f81,axiom,
~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat__less__le_1) ).
fof(f81_nnf,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
inference(nnf_transformation,[status(thm)],[f81]) ).
fof(f81_sk,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
inference(skolemisation,[status(esa)],[f81_nnf]) ).
cnf(c81,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f81_sk]) ).
cnf(f82,axiom,
~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_less__not__refl_0) ).
fof(f82_nnf,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
inference(nnf_transformation,[status(thm)],[f82]) ).
fof(f82_sk,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
inference(skolemisation,[status(esa)],[f82_nnf]) ).
cnf(c82,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f82_sk]) ).
cnf(f83,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__le_1) ).
fof(f83_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f83]) ).
fof(f83_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f83_nnf]) ).
cnf(c83,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f83_sk]) ).
cnf(f84,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__neq__iff_1) ).
fof(f84_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f84]) ).
fof(f84_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f84_nnf]) ).
cnf(c84,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f84_sk]) ).
cnf(f85,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__irrefl_0) ).
fof(f85_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f85]) ).
fof(f85_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f85_nnf]) ).
cnf(c85,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f85_sk]) ).
cnf(f100,axiom,
c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat_Osimps_I3_J_0) ).
fof(f100_nnf,plain,
! [V_nat_H] : c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(nnf_transformation,[status(thm)],[f100]) ).
fof(f100_sk,plain,
! [V_nat_H] : c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(skolemisation,[status(esa)],[f100_nnf]) ).
cnf(c100,plain,
c_Suc(X0) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(esa)],[f100_sk]) ).
cnf(f101,axiom,
c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc__neq__Zero_0) ).
fof(f101_nnf,plain,
! [V_m] : c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(nnf_transformation,[status(thm)],[f101]) ).
fof(f101_sk,plain,
! [V_m] : c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(skolemisation,[status(esa)],[f101_nnf]) ).
cnf(c101,plain,
c_Suc(X0) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(esa)],[f101_sk]) ).
cnf(f115,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) ).
fof(f115_nnf,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(nnf_transformation,[status(thm)],[f115]) ).
fof(f115_sk,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f115_nnf]) ).
cnf(c115,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f115_sk]) ).
cnf(f121,axiom,
~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_i,V_j,tc_nat),V_i,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__add__less1_0) ).
fof(f121_nnf,plain,
! [V_i,V_j] : ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_i,V_j,tc_nat),V_i,tc_nat),
inference(nnf_transformation,[status(thm)],[f121]) ).
fof(f121_sk,plain,
! [V_i,V_j] : ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_i,V_j,tc_nat),V_i,tc_nat),
inference(skolemisation,[status(esa)],[f121_nnf]) ).
cnf(c121,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f121_sk]) ).
cnf(f122,axiom,
~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_j,V_i,tc_nat),V_i,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__add__less2_0) ).
fof(f122_nnf,plain,
! [V_j,V_i] : ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_j,V_i,tc_nat),V_i,tc_nat),
inference(nnf_transformation,[status(thm)],[f122]) ).
fof(f122_sk,plain,
! [V_j,V_i] : ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_j,V_i,tc_nat),V_i,tc_nat),
inference(skolemisation,[status(esa)],[f122_nnf]) ).
cnf(c122,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X1,tc_nat),
inference(cnf_transformation,[status(esa)],[f122_sk]) ).
cnf(f128,axiom,
c_Suc(V_n) != V_n,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc__n__not__n_0) ).
fof(f128_nnf,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(nnf_transformation,[status(thm)],[f128]) ).
fof(f128_sk,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(skolemisation,[status(esa)],[f128_nnf]) ).
cnf(c128,plain,
c_Suc(X0) != X0,
inference(cnf_transformation,[status(esa)],[f128_sk]) ).
cnf(f129,axiom,
V_n != c_Suc(V_n),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_n__not__Suc__n_0) ).
fof(f129_nnf,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(nnf_transformation,[status(thm)],[f129]) ).
fof(f129_sk,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(skolemisation,[status(esa)],[f129_nnf]) ).
cnf(c129,plain,
X0 != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f129_sk]) ).
cnf(f167,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('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_xt1_I9_J_0) ).
fof(f167_nnf,plain,
! [T_a,V_a,V_b] :
( ~ 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) ),
inference(nnf_transformation,[status(thm)],[f167]) ).
fof(f167_sk,plain,
! [T_a,V_a,V_b] :
( ~ 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) ),
inference(skolemisation,[status(esa)],[f167_nnf]) ).
cnf(c167,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f167_sk]) ).
cnf(f168,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('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less__iff__gr__or__eq_1) ).
fof(f168_nnf,plain,
! [T_a,V_x,V_y] :
( ~ 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) ),
inference(nnf_transformation,[status(thm)],[f168]) ).
fof(f168_sk,plain,
! [T_a,V_x,V_y] :
( ~ 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) ),
inference(skolemisation,[status(esa)],[f168_nnf]) ).
cnf(c168,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f168_sk]) ).
cnf(f169,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('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__asym_0) ).
fof(f169_nnf,plain,
! [T_a,V_y,V_x] :
( ~ 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) ),
inference(nnf_transformation,[status(thm)],[f169]) ).
fof(f169_sk,plain,
! [T_a,V_y,V_x] :
( ~ 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) ),
inference(skolemisation,[status(esa)],[f169_nnf]) ).
cnf(c169,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f169_sk]) ).
cnf(f170,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('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__asym_H_0) ).
fof(f170_nnf,plain,
! [T_a,V_b,V_a] :
( ~ 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) ),
inference(nnf_transformation,[status(thm)],[f170]) ).
fof(f170_sk,plain,
! [T_a,V_b,V_a] :
( ~ 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) ),
inference(skolemisation,[status(esa)],[f170_nnf]) ).
cnf(c170,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f170_sk]) ).
cnf(f188,axiom,
~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_gr__implies__not0_0) ).
fof(f188_nnf,plain,
! [V_m] : ~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(nnf_transformation,[status(thm)],[f188]) ).
fof(f188_sk,plain,
! [V_m] : ~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f188_nnf]) ).
cnf(c188,plain,
~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f188_sk]) ).
cnf(f189,axiom,
~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less0_0) ).
fof(f189_nnf,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(nnf_transformation,[status(thm)],[f189]) ).
fof(f189_sk,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f189_nnf]) ).
cnf(c189,plain,
~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f189_sk]) ).
cnf(f195,axiom,
( c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_zero__neq__one_0) ).
fof(f195_nnf,plain,
! [T_a] :
( c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(nnf_transformation,[status(thm)],[f195]) ).
fof(f195_sk,plain,
! [T_a] :
( c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(skolemisation,[status(esa)],[f195_nnf]) ).
cnf(c195,plain,
( c_HOL_Ozero__class_Ozero(X0) != c_HOL_Oone__class_Oone(X0)
| ~ class_Ring__and__Field_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(esa)],[f195_sk]) ).
cnf(f212,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__square__less__zero_0) ).
fof(f212_nnf,plain,
! [T_a,V_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(nnf_transformation,[status(thm)],[f212]) ).
fof(f212_sk,plain,
! [T_a,V_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(skolemisation,[status(esa)],[f212_nnf]) ).
cnf(c212,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(X1,X1,X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__ring__strict(X0) ),
inference(cnf_transformation,[status(esa)],[f212_sk]) ).
cnf(f220,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('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_of__nat__less__0__iff_0) ).
fof(f220_nnf,plain,
! [T_a,V_m] :
( ~ 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) ),
inference(nnf_transformation,[status(thm)],[f220]) ).
fof(f220_sk,plain,
! [T_a,V_m] :
( ~ 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) ),
inference(skolemisation,[status(esa)],[f220_nnf]) ).
cnf(c220,plain,
( ~ c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(X1,X0),c_HOL_Ozero__class_Ozero(X0),X0)
| ~ class_Ring__and__Field_Oordered__semidom(X0) ),
inference(cnf_transformation,[status(esa)],[f220_sk]) ).
cnf(f230,axiom,
( ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat)
| ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less__eq_1) ).
fof(f230_nnf,plain,
! [V_m,V_n] :
( ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat)
| ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ),
inference(nnf_transformation,[status(thm)],[f230]) ).
fof(f230_sk,plain,
! [V_m,V_n] :
( ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat)
| ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ),
inference(skolemisation,[status(esa)],[f230_nnf]) ).
cnf(c230,plain,
( ~ c_HOL_Oord__class_Oless(X1,c_Suc(X0),tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_nat) ),
inference(cnf_transformation,[status(esa)],[f230_sk]) ).
cnf(f258,axiom,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_sum__squares__gt__zero__iff_0) ).
fof(f258_nnf,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(nnf_transformation,[status(thm)],[f258]) ).
fof(f258_sk,plain,
! [T_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),T_a),T_a)
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(skolemisation,[status(esa)],[f258_nnf]) ).
cnf(c258,plain,
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),c_HOL_Ozero__class_Ozero(X0),X0),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),c_HOL_Ozero__class_Ozero(X0),X0),X0),X0)
| ~ class_Ring__and__Field_Oordered__ring__strict(X0) ),
inference(cnf_transformation,[status(esa)],[f258_sk]) ).
cnf(f271,axiom,
c_Lambda_OdB_OApp(V_dB1_H,V_dB2_H) != c_Lambda_OdB_OVar(V_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dB_Osimps_I5_J_0) ).
fof(f271_nnf,plain,
! [V_dB1_H,V_dB2_H,V_nat] : c_Lambda_OdB_OApp(V_dB1_H,V_dB2_H) != c_Lambda_OdB_OVar(V_nat),
inference(nnf_transformation,[status(thm)],[f271]) ).
fof(f271_sk,plain,
! [V_dB1_H,V_dB2_H,V_nat] : c_Lambda_OdB_OApp(V_dB1_H,V_dB2_H) != c_Lambda_OdB_OVar(V_nat),
inference(skolemisation,[status(esa)],[f271_nnf]) ).
cnf(c271,plain,
c_Lambda_OdB_OApp(X0,X1) != c_Lambda_OdB_OVar(X2),
inference(cnf_transformation,[status(esa)],[f271_sk]) ).
cnf(f314,axiom,
c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OApp(V_dB1_H,V_dB2_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dB_Osimps_I4_J_0) ).
fof(f314_nnf,plain,
! [V_nat,V_dB1_H,V_dB2_H] : c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OApp(V_dB1_H,V_dB2_H),
inference(nnf_transformation,[status(thm)],[f314]) ).
fof(f314_sk,plain,
! [V_nat,V_dB1_H,V_dB2_H] : c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OApp(V_dB1_H,V_dB2_H),
inference(skolemisation,[status(esa)],[f314_nnf]) ).
cnf(c314,plain,
c_Lambda_OdB_OVar(X0) != c_Lambda_OdB_OApp(X1,X2),
inference(cnf_transformation,[status(esa)],[f314_sk]) ).
cnf(f321,axiom,
~ c_Lambda_Obeta(c_Lambda_OdB_OVar(V_i),V_t),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_beta__cases_I1_J_0) ).
fof(f321_nnf,plain,
! [V_i,V_t] : ~ c_Lambda_Obeta(c_Lambda_OdB_OVar(V_i),V_t),
inference(nnf_transformation,[status(thm)],[f321]) ).
fof(f321_sk,plain,
! [V_i,V_t] : ~ c_Lambda_Obeta(c_Lambda_OdB_OVar(V_i),V_t),
inference(skolemisation,[status(esa)],[f321_nnf]) ).
cnf(c321,plain,
~ c_Lambda_Obeta(c_Lambda_OdB_OVar(X0),X1),
inference(cnf_transformation,[status(esa)],[f321_sk]) ).
cnf(f332,axiom,
c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dB_Osimps_I7_J_0) ).
fof(f332_nnf,plain,
! [V_dB_H,V_nat] : c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat),
inference(nnf_transformation,[status(thm)],[f332]) ).
fof(f332_sk,plain,
! [V_dB_H,V_nat] : c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat),
inference(skolemisation,[status(esa)],[f332_nnf]) ).
cnf(c332,plain,
c_Lambda_OdB_OAbs(X0) != c_Lambda_OdB_OVar(X1),
inference(cnf_transformation,[status(esa)],[f332_sk]) ).
cnf(f333,axiom,
c_Lambda_OdB_OApp(V_dB1,V_dB2) != c_Lambda_OdB_OAbs(V_dB_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dB_Osimps_I8_J_0) ).
fof(f333_nnf,plain,
! [V_dB1,V_dB2,V_dB_H] : c_Lambda_OdB_OApp(V_dB1,V_dB2) != c_Lambda_OdB_OAbs(V_dB_H),
inference(nnf_transformation,[status(thm)],[f333]) ).
fof(f333_sk,plain,
! [V_dB1,V_dB2,V_dB_H] : c_Lambda_OdB_OApp(V_dB1,V_dB2) != c_Lambda_OdB_OAbs(V_dB_H),
inference(skolemisation,[status(esa)],[f333_nnf]) ).
cnf(c333,plain,
c_Lambda_OdB_OApp(X0,X1) != c_Lambda_OdB_OAbs(X2),
inference(cnf_transformation,[status(esa)],[f333_sk]) ).
cnf(f334,axiom,
c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OApp(V_dB1,V_dB2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dB_Osimps_I9_J_0) ).
fof(f334_nnf,plain,
! [V_dB_H,V_dB1,V_dB2] : c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OApp(V_dB1,V_dB2),
inference(nnf_transformation,[status(thm)],[f334]) ).
fof(f334_sk,plain,
! [V_dB_H,V_dB1,V_dB2] : c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OApp(V_dB1,V_dB2),
inference(skolemisation,[status(esa)],[f334_nnf]) ).
cnf(c334,plain,
c_Lambda_OdB_OAbs(X0) != c_Lambda_OdB_OApp(X1,X2),
inference(cnf_transformation,[status(esa)],[f334_sk]) ).
cnf(f336,axiom,
c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_dB_Osimps_I6_J_0) ).
fof(f336_nnf,plain,
! [V_nat,V_dB_H] : c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H),
inference(nnf_transformation,[status(thm)],[f336]) ).
fof(f336_sk,plain,
! [V_nat,V_dB_H] : c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H),
inference(skolemisation,[status(esa)],[f336_nnf]) ).
cnf(c336,plain,
c_Lambda_OdB_OVar(X0) != c_Lambda_OdB_OAbs(X1),
inference(cnf_transformation,[status(esa)],[f336_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c9,c10,c11,c63,c64,c81,c82,c83,c84,c85,c100,c101,c115,c121,c122,c128,c129,c167,c168,c169,c170,c188,c189,c195,c212,c220,c230,c258,c271,c314,c321,c332,c333,c334,c336,c344]) ).
cnf(g0_0,plain,
sF0 != false,
inference(rw,[status(thm)],[goal_0,t199]) ).
cnf(g0_1,plain,
sF0 != sF0,
inference(rw,[status(thm)],[g0_0,t623]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL748-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n018.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 00:27:36 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 11.18/1.83 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.18/1.83 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------