%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL754-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n003.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:48 PM UTC 2026
% Result : Unsatisfiable 44.44s 21.80s
% Output : Proof 44.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 58
% Syntax : Number of formulae : 281 ( 177 unt; 0 def)
% Number of atoms : 429 ( 156 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 470 ( 322 ~; 148 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 1 prp; 0-3 aty)
% Number of functors : 23 ( 23 usr; 6 con; 0-4 aty)
% Number of variables : 526 ( 97 sgn 206 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f683,negated_conjecture,
~ c_InductTermi_OIT(c_Lambda_Osubst(c_Lambda_OdB_OAbs(v_ra),c_Lambda_OdB_OVar(v_ia),v_ja)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f683_nnf,plain,
~ c_InductTermi_OIT(c_Lambda_Osubst(c_Lambda_OdB_OAbs(v_ra),c_Lambda_OdB_OVar(v_ia),v_ja)),
inference(nnf_transformation,[status(thm)],[f683]) ).
fof(f683_sk,plain,
~ c_InductTermi_OIT(c_Lambda_Osubst(c_Lambda_OdB_OAbs(v_ra),c_Lambda_OdB_OVar(v_ia),v_ja)),
inference(skolemisation,[status(esa)],[f683_nnf]) ).
cnf(c683,plain,
~ c_InductTermi_OIT(c_Lambda_Osubst(c_Lambda_OdB_OAbs(v_ra),c_Lambda_OdB_OVar(v_ia),v_ja)),
inference(cnf_transformation,[status(esa)],[f683_sk]) ).
cnf(t44,plain,
c_InductTermi_OIT(c_Lambda_Osubst(c_Lambda_OdB_OAbs(v_ra),c_Lambda_OdB_OVar(v_ia),v_ja)) = false,
inference(equality_encoding,[status(esa)],[c683]) ).
cnf(t1922,plain,
c_InductTermi_OIT(c_Lambda_Osubst(c_Lambda_OdB_OAbs(v_ra),c_Lambda_OdB_OVar(v_ia),v_ja)) = false,
inference(orient,[status(thm)],[t44]) ).
cnf(f677,axiom,
( ~ c_InductTermi_OIT(V_r)
| c_InductTermi_OIT(c_Lambda_OdB_OAbs(V_r)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Lambda_0) ).
fof(f677_nnf,plain,
! [V_r] :
( ~ c_InductTermi_OIT(V_r)
| c_InductTermi_OIT(c_Lambda_OdB_OAbs(V_r)) ),
inference(nnf_transformation,[status(thm)],[f677]) ).
fof(f677_sk,plain,
! [V_r] :
( ~ c_InductTermi_OIT(V_r)
| c_InductTermi_OIT(c_Lambda_OdB_OAbs(V_r)) ),
inference(skolemisation,[status(esa)],[f677_nnf]) ).
cnf(c677,plain,
( ~ c_InductTermi_OIT(X0)
| c_InductTermi_OIT(c_Lambda_OdB_OAbs(X0)) ),
inference(cnf_transformation,[status(esa)],[f677_sk]) ).
cnf(t73,plain,
ifeq(c_InductTermi_OIT(X1),true,c_InductTermi_OIT(c_Lambda_OdB_OAbs(X1)),true) = true,
inference(equality_encoding,[status(esa)],[c677]) ).
cnf(t801,plain,
ifeq(c_InductTermi_OIT(X1),true,c_InductTermi_OIT(c_Lambda_OdB_OAbs(X1)),true) = true,
inference(orient,[status(thm)],[t73]) ).
cnf(f682,negated_conjecture,
c_InductTermi_OIT(c_Lambda_Osubst(v_ra,c_Lambda_OdB_OVar(V_i),V_j)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f682_nnf,plain,
! [V_i,V_j] : c_InductTermi_OIT(c_Lambda_Osubst(v_ra,c_Lambda_OdB_OVar(V_i),V_j)),
inference(nnf_transformation,[status(thm)],[f682]) ).
fof(f682_sk,plain,
! [V_i,V_j] : c_InductTermi_OIT(c_Lambda_Osubst(v_ra,c_Lambda_OdB_OVar(V_i),V_j)),
inference(skolemisation,[status(esa)],[f682_nnf]) ).
cnf(c682,plain,
c_InductTermi_OIT(c_Lambda_Osubst(v_ra,c_Lambda_OdB_OVar(X0),X1)),
inference(cnf_transformation,[status(esa)],[f682_sk]) ).
cnf(t26,plain,
c_InductTermi_OIT(c_Lambda_Osubst(v_ra,c_Lambda_OdB_OVar(X1),X2)) = true,
inference(equality_encoding,[status(esa)],[c682]) ).
cnf(t906,plain,
c_InductTermi_OIT(c_Lambda_Osubst(v_ra,c_Lambda_OdB_OVar(X1),X2)) = true,
inference(orient,[status(thm)],[t26]) ).
cnf(t51,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
introduced(definition) ).
cnf(t298,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
inference(orient,[status(thm)],[t51]) ).
cnf(f193,axiom,
( c_HOL_Oord__class_Oless(V_i,V_k,tc_nat)
| c_Lambda_Oliftn(V_n,c_Lambda_OdB_OVar(V_i),V_k) = c_Lambda_OdB_OVar(c_HOL_Oplus__class_Oplus(V_i,V_n,tc_nat)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_liftn_Osimps_I1_J_1) ).
fof(f193_nnf,plain,
! [V_n,V_i,V_k] :
( c_HOL_Oord__class_Oless(V_i,V_k,tc_nat)
| c_Lambda_Oliftn(V_n,c_Lambda_OdB_OVar(V_i),V_k) = c_Lambda_OdB_OVar(c_HOL_Oplus__class_Oplus(V_i,V_n,tc_nat)) ),
inference(nnf_transformation,[status(thm)],[f193]) ).
fof(f193_sk,plain,
! [V_n,V_i,V_k] :
( c_HOL_Oord__class_Oless(V_i,V_k,tc_nat)
| c_Lambda_Oliftn(V_n,c_Lambda_OdB_OVar(V_i),V_k) = c_Lambda_OdB_OVar(c_HOL_Oplus__class_Oplus(V_i,V_n,tc_nat)) ),
inference(skolemisation,[status(esa)],[f193_nnf]) ).
cnf(c193,plain,
( c_HOL_Oord__class_Oless(X1,X2,tc_nat)
| c_Lambda_Oliftn(X0,c_Lambda_OdB_OVar(X1),X2) = c_Lambda_OdB_OVar(c_HOL_Oplus__class_Oplus(X1,X0,tc_nat)) ),
inference(cnf_transformation,[status(esa)],[f193_sk]) ).
cnf(t195,plain,
or(eq(c_Lambda_Oliftn(X1,c_Lambda_OdB_OVar(X2),X3),c_Lambda_OdB_OVar(c_HOL_Oplus__class_Oplus(X2,X1,tc_nat))),c_HOL_Oord__class_Oless(X2,X3,tc_nat)) = true,
inference(equality_encoding,[status(esa)],[c193]) ).
cnf(t859,plain,
or(eq(c_Lambda_Oliftn(X1,c_Lambda_OdB_OVar(X2),X3),c_Lambda_OdB_OVar(c_HOL_Oplus__class_Oplus(X2,X1,tc_nat))),c_HOL_Oord__class_Oless(X2,X3,tc_nat)) = true,
inference(orient,[status(thm)],[t195]) ).
cnf(f613,axiom,
~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat__less__le_1) ).
fof(f613_nnf,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
inference(nnf_transformation,[status(thm)],[f613]) ).
fof(f613_sk,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
inference(skolemisation,[status(esa)],[f613_nnf]) ).
cnf(c613,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f613_sk]) ).
cnf(t7,plain,
c_HOL_Oord__class_Oless(X1,X1,tc_nat) = false,
inference(equality_encoding,[status(esa)],[c613]) ).
cnf(t1235,plain,
c_HOL_Oord__class_Oless(X1,X1,tc_nat) = false,
inference(orient,[status(thm)],[t7]) ).
cnf(t1255,plain,
true = or(eq(c_Lambda_Oliftn(X1,c_Lambda_OdB_OVar(X2),X2),c_Lambda_OdB_OVar(c_HOL_Oplus__class_Oplus(X2,X1,tc_nat))),false),
inference(cp,[status(thm)],[t859,t1235]) ).
cnf(t3,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t308,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t6959,plain,
true = eq(c_Lambda_Oliftn(X1,c_Lambda_OdB_OVar(X2),X2),c_Lambda_OdB_OVar(c_HOL_Oplus__class_Oplus(X2,X1,tc_nat))),
inference(step,[status(thm)],[t1255,t308]) ).
cnf(t3861,plain,
eq(c_Lambda_Oliftn(X1,c_Lambda_OdB_OVar(X2),X2),c_Lambda_OdB_OVar(c_HOL_Oplus__class_Oplus(X2,X1,tc_nat))) = true,
inference(orient,[status(thm)],[t6959]) ).
cnf(t3869,plain,
c_Lambda_OdB_OVar(c_HOL_Oplus__class_Oplus(X1,X2,tc_nat)) = ifeq(true,true,c_Lambda_Oliftn(X2,c_Lambda_OdB_OVar(X1),X1),c_Lambda_OdB_OVar(c_HOL_Oplus__class_Oplus(X1,X2,tc_nat))),
inference(cp,[status(thm)],[t298,t3861]) ).
cnf(t23,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t271,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t23]) ).
cnf(t6960,plain,
c_Lambda_OdB_OVar(c_HOL_Oplus__class_Oplus(X1,X2,tc_nat)) = c_Lambda_Oliftn(X2,c_Lambda_OdB_OVar(X1),X1),
inference(step,[status(thm)],[t3869,t271]) ).
cnf(t3870,plain,
c_Lambda_OdB_OVar(c_HOL_Oplus__class_Oplus(X1,X2,tc_nat)) = c_Lambda_Oliftn(X2,c_Lambda_OdB_OVar(X1),X1),
inference(orient,[status(thm)],[t6960]) ).
cnf(t3919,plain,
true = c_InductTermi_OIT(c_Lambda_Osubst(v_ra,c_Lambda_Oliftn(X1,c_Lambda_OdB_OVar(X2),X2),X3)),
inference(cp,[status(thm)],[t906,t3870]) ).
cnf(t4044,plain,
c_InductTermi_OIT(c_Lambda_Osubst(v_ra,c_Lambda_Oliftn(X1,c_Lambda_OdB_OVar(X2),X2),X3)) = true,
inference(orient,[status(thm)],[t3919]) ).
cnf(f671,axiom,
( V_dB = V_dB_H
| c_Lambda_OdB_OAbs(V_dB) != c_Lambda_OdB_OAbs(V_dB_H) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I3_J_0) ).
fof(f671_nnf,plain,
! [V_dB,V_dB_H] :
( V_dB = V_dB_H
| c_Lambda_OdB_OAbs(V_dB) != c_Lambda_OdB_OAbs(V_dB_H) ),
inference(nnf_transformation,[status(thm)],[f671]) ).
fof(f671_sk,plain,
! [V_dB,V_dB_H] :
( V_dB = V_dB_H
| c_Lambda_OdB_OAbs(V_dB) != c_Lambda_OdB_OAbs(V_dB_H) ),
inference(skolemisation,[status(esa)],[f671_nnf]) ).
cnf(c671,plain,
( X0 = X1
| c_Lambda_OdB_OAbs(X0) != c_Lambda_OdB_OAbs(X1) ),
inference(cnf_transformation,[status(esa)],[f671_sk]) ).
cnf(hi630,axiom,
ifeq(c_Lambda_OdB_OAbs(X0),c_Lambda_OdB_OAbs(X1),X0,X1) = X1,
inference(equality_encoding,[status(esa)],[c671]) ).
cnf(f17,axiom,
c_Lambda_Oliftn(c_Suc(V_n),V_t,V_k) = c_Lambda_Olift(c_Lambda_Oliftn(V_n,V_t,V_k),V_k),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_liftn__lift_0) ).
fof(f17_nnf,plain,
! [V_n,V_t,V_k] : c_Lambda_Oliftn(c_Suc(V_n),V_t,V_k) = c_Lambda_Olift(c_Lambda_Oliftn(V_n,V_t,V_k),V_k),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [V_n,V_t,V_k] : c_Lambda_Oliftn(c_Suc(V_n),V_t,V_k) = c_Lambda_Olift(c_Lambda_Oliftn(V_n,V_t,V_k),V_k),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c17,plain,
c_Lambda_Oliftn(c_Suc(X0),X1,X2) = c_Lambda_Olift(c_Lambda_Oliftn(X0,X1,X2),X2),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(hi17,axiom,
c_Lambda_Oliftn(c_Suc(X0),X1,X2) = c_Lambda_Olift(c_Lambda_Oliftn(X0,X1,X2),X2),
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(f147,axiom,
c_Suc(V_n) = c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),V_n,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__eq__plus1__left_0) ).
fof(f147_nnf,plain,
! [V_n] : c_Suc(V_n) = c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),V_n,tc_nat),
inference(nnf_transformation,[status(thm)],[f147]) ).
fof(f147_sk,plain,
! [V_n] : c_Suc(V_n) = c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),V_n,tc_nat),
inference(skolemisation,[status(esa)],[f147_nnf]) ).
cnf(c147,plain,
c_Suc(X0) = c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f147_sk]) ).
cnf(hi18,axiom,
c_Suc(X0) = c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),X0,tc_nat),
inference(equality_encoding,[status(esa)],[c147]) ).
cnf(t153,plain,
c_Lambda_Oliftn(c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),X1,tc_nat),X2,X3) = c_Lambda_Olift(c_Lambda_Oliftn(X1,X2,X3),X3),
inference(hyper_resolution,[status(thm)],[hi630,hi17,hi18]) ).
cnf(t1885,plain,
c_Lambda_Olift(c_Lambda_Oliftn(X1,X2,X3),X3) = c_Lambda_Oliftn(c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_nat),X1,tc_nat),X2,X3),
inference(orient,[status(thm)],[t153]) ).
cnf(t4046,plain,
true = c_InductTermi_OIT(c_Lambda_Osubst(v_ra,c_Lambda_Olift(c_Lambda_Oliftn(X1,c_Lambda_OdB_OVar(X2),X2),X2),X3)),
inference(cp,[status(thm)],[t4044,t1885]) ).
cnf(t6125,plain,
c_InductTermi_OIT(c_Lambda_Osubst(v_ra,c_Lambda_Olift(c_Lambda_Oliftn(X1,c_Lambda_OdB_OVar(X2),X2),X2),X3)) = true,
inference(orient,[status(thm)],[t4046]) ).
cnf(f238,axiom,
( ~ c_lessequals(V_n,V_m,tc_nat)
| c_HOL_Oplus__class_Oplus(V_n,c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat),tc_nat) = V_m ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_le__add__diff__inverse_0) ).
fof(f238_nnf,plain,
! [V_n,V_m] :
( ~ c_lessequals(V_n,V_m,tc_nat)
| c_HOL_Oplus__class_Oplus(V_n,c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat),tc_nat) = V_m ),
inference(nnf_transformation,[status(thm)],[f238]) ).
fof(f238_sk,plain,
! [V_n,V_m] :
( ~ c_lessequals(V_n,V_m,tc_nat)
| c_HOL_Oplus__class_Oplus(V_n,c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat),tc_nat) = V_m ),
inference(skolemisation,[status(esa)],[f238_nnf]) ).
cnf(c238,plain,
( ~ c_lessequals(X0,X1,tc_nat)
| c_HOL_Oplus__class_Oplus(X0,c_HOL_Ominus__class_Ominus(X1,X0,tc_nat),tc_nat) = X1 ),
inference(cnf_transformation,[status(esa)],[f238_sk]) ).
cnf(hi231,axiom,
ifeq(c_lessequals(X0,X1,tc_nat),true,c_HOL_Oplus__class_Oplus(X0,c_HOL_Ominus__class_Ominus(X1,X0,tc_nat),tc_nat),X1) = X1,
inference(equality_encoding,[status(esa)],[c238]) ).
cnf(f196,axiom,
c_lessequals(V_n,c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_le__add2_0) ).
fof(f196_nnf,plain,
! [V_n,V_m] : c_lessequals(V_n,c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat),tc_nat),
inference(nnf_transformation,[status(thm)],[f196]) ).
fof(f196_sk,plain,
! [V_n,V_m] : c_lessequals(V_n,c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f196_nnf]) ).
cnf(c196,plain,
c_lessequals(X0,c_HOL_Oplus__class_Oplus(X1,X0,tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f196_sk]) ).
cnf(hi192,axiom,
c_lessequals(X0,c_HOL_Oplus__class_Oplus(X1,X0,tc_nat),tc_nat) = true,
inference(equality_encoding,[status(esa)],[c196]) ).
cnf(t139,plain,
c_HOL_Oplus__class_Oplus(X1,c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X2,X1,tc_nat),X1,tc_nat),tc_nat) = c_HOL_Oplus__class_Oplus(X2,X1,tc_nat),
inference(hyper_resolution,[status(thm)],[hi231,hi192]) ).
cnf(f565,axiom,
c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat),V_n,tc_nat) = V_m,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_diff__add__inverse2_0) ).
fof(f565_nnf,plain,
! [V_m,V_n] : c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat),V_n,tc_nat) = V_m,
inference(nnf_transformation,[status(thm)],[f565]) ).
fof(f565_sk,plain,
! [V_m,V_n] : c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat),V_n,tc_nat) = V_m,
inference(skolemisation,[status(esa)],[f565_nnf]) ).
cnf(c565,plain,
c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X1,tc_nat) = X0,
inference(cnf_transformation,[status(esa)],[f565_sk]) ).
cnf(t34,plain,
c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X1,X2,tc_nat),X2,tc_nat) = X1,
inference(equality_encoding,[status(esa)],[c565]) ).
cnf(t269,plain,
c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X1,X2,tc_nat),X2,tc_nat) = X1,
inference(orient,[status(thm)],[t34]) ).
cnf(t6793,plain,
c_HOL_Oplus__class_Oplus(X1,X2,tc_nat) = c_HOL_Oplus__class_Oplus(X2,X1,tc_nat),
inference(step,[status(thm)],[t139,t269]) ).
cnf(t924,plain,
c_HOL_Oplus__class_Oplus(X1,X2,tc_nat) = c_HOL_Oplus__class_Oplus(X2,X1,tc_nat),
inference(orient,[status(thm)],[t6793]) ).
cnf(t3871,plain,
c_Lambda_Oliftn(X1,c_Lambda_OdB_OVar(X2),X2) = c_Lambda_OdB_OVar(c_HOL_Oplus__class_Oplus(X1,X2,tc_nat)),
inference(cp,[status(thm)],[t3870,t924]) ).
cnf(t4198,plain,
c_Lambda_Oliftn(X1,c_Lambda_OdB_OVar(X2),X2) = c_Lambda_OdB_OVar(c_HOL_Oplus__class_Oplus(X1,X2,tc_nat)),
inference(orient,[status(thm)],[t3871]) ).
cnf(t4211,plain,
c_Lambda_Oliftn(X1,c_Lambda_OdB_OVar(X2),X2) = c_Lambda_Oliftn(X2,c_Lambda_OdB_OVar(X1),X1),
inference(cp,[status(thm)],[t4198,t3870]) ).
cnf(t4539,plain,
c_Lambda_Oliftn(X1,c_Lambda_OdB_OVar(X2),X2) = c_Lambda_Oliftn(X2,c_Lambda_OdB_OVar(X1),X1),
inference(orient,[status(thm)],[t4211]) ).
cnf(t6127,plain,
true = c_InductTermi_OIT(c_Lambda_Osubst(v_ra,c_Lambda_Olift(c_Lambda_Oliftn(X1,c_Lambda_OdB_OVar(X2),X2),X1),X3)),
inference(cp,[status(thm)],[t6125,t4539]) ).
cnf(t6500,plain,
c_InductTermi_OIT(c_Lambda_Osubst(v_ra,c_Lambda_Olift(c_Lambda_Oliftn(X1,c_Lambda_OdB_OVar(X2),X2),X1),X3)) = true,
inference(orient,[status(thm)],[t6127]) ).
cnf(f258,axiom,
c_Lambda_Oliftn(c_HOL_Ozero__class_Ozero(tc_nat),V_t,V_k) = V_t,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_liftn__0_0) ).
fof(f258_nnf,plain,
! [V_t,V_k] : c_Lambda_Oliftn(c_HOL_Ozero__class_Ozero(tc_nat),V_t,V_k) = V_t,
inference(nnf_transformation,[status(thm)],[f258]) ).
fof(f258_sk,plain,
! [V_t,V_k] : c_Lambda_Oliftn(c_HOL_Ozero__class_Ozero(tc_nat),V_t,V_k) = V_t,
inference(skolemisation,[status(esa)],[f258_nnf]) ).
cnf(c258,plain,
c_Lambda_Oliftn(c_HOL_Ozero__class_Ozero(tc_nat),X0,X1) = X0,
inference(cnf_transformation,[status(esa)],[f258_sk]) ).
cnf(t19,plain,
c_Lambda_Oliftn(c_HOL_Ozero__class_Ozero(tc_nat),X1,X2) = X1,
inference(equality_encoding,[status(esa)],[c258]) ).
cnf(t312,plain,
c_Lambda_Oliftn(c_HOL_Ozero__class_Ozero(tc_nat),X1,X2) = X1,
inference(orient,[status(thm)],[t19]) ).
cnf(t6502,plain,
true = c_InductTermi_OIT(c_Lambda_Osubst(v_ra,c_Lambda_Olift(c_Lambda_OdB_OVar(X1),c_HOL_Ozero__class_Ozero(tc_nat)),X2)),
inference(cp,[status(thm)],[t6500,t312]) ).
cnf(t6512,plain,
c_InductTermi_OIT(c_Lambda_Osubst(v_ra,c_Lambda_Olift(c_Lambda_OdB_OVar(X1),c_HOL_Ozero__class_Ozero(tc_nat)),X2)) = true,
inference(orient,[status(thm)],[t6502]) ).
cnf(t6517,plain,
true = ifeq(true,true,c_InductTermi_OIT(c_Lambda_OdB_OAbs(c_Lambda_Osubst(v_ra,c_Lambda_Olift(c_Lambda_OdB_OVar(X1),c_HOL_Ozero__class_Ozero(tc_nat)),X2))),true),
inference(cp,[status(thm)],[t801,t6512]) ).
cnf(t7042,plain,
true = c_InductTermi_OIT(c_Lambda_OdB_OAbs(c_Lambda_Osubst(v_ra,c_Lambda_Olift(c_Lambda_OdB_OVar(X1),c_HOL_Ozero__class_Ozero(tc_nat)),X2))),
inference(step,[status(thm)],[t6517,t271]) ).
cnf(t6519,plain,
c_InductTermi_OIT(c_Lambda_OdB_OAbs(c_Lambda_Osubst(v_ra,c_Lambda_Olift(c_Lambda_OdB_OVar(X1),c_HOL_Ozero__class_Ozero(tc_nat)),X2))) = true,
inference(orient,[status(thm)],[t7042]) ).
cnf(f594,axiom,
c_Lambda_Osubst(c_Lambda_OdB_OAbs(V_t),V_s,V_k) = c_Lambda_OdB_OAbs(c_Lambda_Osubst(V_t,c_Lambda_Olift(V_s,c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Oplus__class_Oplus(V_k,c_HOL_Oone__class_Oone(tc_nat),tc_nat))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_subst__Abs_0) ).
fof(f594_nnf,plain,
! [V_t,V_s,V_k] : c_Lambda_Osubst(c_Lambda_OdB_OAbs(V_t),V_s,V_k) = c_Lambda_OdB_OAbs(c_Lambda_Osubst(V_t,c_Lambda_Olift(V_s,c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Oplus__class_Oplus(V_k,c_HOL_Oone__class_Oone(tc_nat),tc_nat))),
inference(nnf_transformation,[status(thm)],[f594]) ).
fof(f594_sk,plain,
! [V_t,V_s,V_k] : c_Lambda_Osubst(c_Lambda_OdB_OAbs(V_t),V_s,V_k) = c_Lambda_OdB_OAbs(c_Lambda_Osubst(V_t,c_Lambda_Olift(V_s,c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Oplus__class_Oplus(V_k,c_HOL_Oone__class_Oone(tc_nat),tc_nat))),
inference(skolemisation,[status(esa)],[f594_nnf]) ).
cnf(c594,plain,
c_Lambda_Osubst(c_Lambda_OdB_OAbs(X0),X1,X2) = c_Lambda_OdB_OAbs(c_Lambda_Osubst(X0,c_Lambda_Olift(X1,c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Oplus__class_Oplus(X2,c_HOL_Oone__class_Oone(tc_nat),tc_nat))),
inference(cnf_transformation,[status(esa)],[f594_sk]) ).
cnf(t189,plain,
c_Lambda_OdB_OAbs(c_Lambda_Osubst(X1,c_Lambda_Olift(X2,c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Oplus__class_Oplus(X3,c_HOL_Oone__class_Oone(tc_nat),tc_nat))) = c_Lambda_Osubst(c_Lambda_OdB_OAbs(X1),X2,X3),
inference(equality_encoding,[status(esa)],[c594]) ).
cnf(t1739,plain,
c_Lambda_OdB_OAbs(c_Lambda_Osubst(X1,c_Lambda_Olift(X2,c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Oplus__class_Oplus(X3,c_HOL_Oone__class_Oone(tc_nat),tc_nat))) = c_Lambda_Osubst(c_Lambda_OdB_OAbs(X1),X2,X3),
inference(orient,[status(thm)],[t189]) ).
cnf(t6520,plain,
true = c_InductTermi_OIT(c_Lambda_Osubst(c_Lambda_OdB_OAbs(v_ra),c_Lambda_OdB_OVar(X1),X2)),
inference(cp,[status(thm)],[t6519,t1739]) ).
cnf(t6527,plain,
c_InductTermi_OIT(c_Lambda_Osubst(c_Lambda_OdB_OAbs(v_ra),c_Lambda_OdB_OVar(X1),X2)) = true,
inference(orient,[status(thm)],[t6520]) ).
cnf(t7043,plain,
true = false,
inference(step,[status(thm)],[t1922,t6527]) ).
cnf(t6534,plain,
true = false,
inference(rw,[status(thm)],[t7043]) ).
cnf(t6535,plain,
false = true,
inference(orient,[status(thm)],[t6534]) ).
cnf(f54,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/sandbox2/benchmark/theBenchmark.p',cls_one__neq__zero_0) ).
fof(f54_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)],[f54]) ).
fof(f54_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)],[f54_nnf]) ).
cnf(c54,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)],[f54_sk]) ).
cnf(f55,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/sandbox2/benchmark/theBenchmark.p',cls_not__sum__squares__lt__zero_0) ).
fof(f55_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)],[f55]) ).
fof(f55_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)],[f55_nnf]) ).
cnf(c55,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)],[f55_sk]) ).
cnf(f122,axiom,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Zero__neq__Suc_0) ).
fof(f122_nnf,plain,
! [V_m] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
inference(nnf_transformation,[status(thm)],[f122]) ).
fof(f122_sk,plain,
! [V_m] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m),
inference(skolemisation,[status(esa)],[f122_nnf]) ).
cnf(c122,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f122_sk]) ).
cnf(f123,axiom,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat_Osimps_I2_J_0) ).
fof(f123_nnf,plain,
! [V_nat_H] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
inference(nnf_transformation,[status(thm)],[f123]) ).
fof(f123_sk,plain,
! [V_nat_H] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H),
inference(skolemisation,[status(esa)],[f123_nnf]) ).
cnf(c123,plain,
c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f123_sk]) ).
cnf(f198,axiom,
( ~ c_lessequals(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/sandbox2/benchmark/theBenchmark.p',cls_not__one__le__zero_0) ).
fof(f198_nnf,plain,
! [T_a] :
( ~ c_lessequals(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)],[f198]) ).
fof(f198_sk,plain,
! [T_a] :
( ~ c_lessequals(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)],[f198_nnf]) ).
cnf(c198,plain,
( ~ c_lessequals(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)],[f198_sk]) ).
cnf(f221,axiom,
c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat_Osimps_I3_J_0) ).
fof(f221_nnf,plain,
! [V_nat_H] : c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(nnf_transformation,[status(thm)],[f221]) ).
fof(f221_sk,plain,
! [V_nat_H] : c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(skolemisation,[status(esa)],[f221_nnf]) ).
cnf(c221,plain,
c_Suc(X0) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(esa)],[f221_sk]) ).
cnf(f222,axiom,
c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__neq__Zero_0) ).
fof(f222_nnf,plain,
! [V_m] : c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(nnf_transformation,[status(thm)],[f222]) ).
fof(f222_sk,plain,
! [V_m] : c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(skolemisation,[status(esa)],[f222_nnf]) ).
cnf(c222,plain,
c_Suc(X0) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(esa)],[f222_sk]) ).
cnf(f261,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/sandbox2/benchmark/theBenchmark.p',cls_neq0__conv_1) ).
fof(f261_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)],[f261]) ).
fof(f261_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)],[f261_nnf]) ).
cnf(c261,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)],[f261_sk]) ).
cnf(f273,axiom,
~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__n__not__le__n_0) ).
fof(f273_nnf,plain,
! [V_n] : ~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
inference(nnf_transformation,[status(thm)],[f273]) ).
fof(f273_sk,plain,
! [V_n] : ~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
inference(skolemisation,[status(esa)],[f273_nnf]) ).
cnf(c273,plain,
~ c_lessequals(c_Suc(X0),X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f273_sk]) ).
cnf(f278,axiom,
~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_i,V_j,tc_nat),V_i,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__add__less1_0) ).
fof(f278_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)],[f278]) ).
fof(f278_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)],[f278_nnf]) ).
cnf(c278,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f278_sk]) ).
cnf(f279,axiom,
~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_j,V_i,tc_nat),V_i,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__add__less2_0) ).
fof(f279_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)],[f279]) ).
fof(f279_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)],[f279_nnf]) ).
cnf(c279,plain,
~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X1,tc_nat),
inference(cnf_transformation,[status(esa)],[f279_sk]) ).
cnf(f296,axiom,
~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_gr__implies__not0_0) ).
fof(f296_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)],[f296]) ).
fof(f296_sk,plain,
! [V_m] : ~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f296_nnf]) ).
cnf(c296,plain,
~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f296_sk]) ).
cnf(f297,axiom,
~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__less0_0) ).
fof(f297_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)],[f297]) ).
fof(f297_sk,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(skolemisation,[status(esa)],[f297_nnf]) ).
cnf(c297,plain,
~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(esa)],[f297_sk]) ).
cnf(f298,axiom,
( c_Power_Opower__class_Opower(V_a,c_HOL_Ozero__class_Ozero(tc_nat),T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Power_Opower(T_a)
| ~ class_Ring__and__Field_Omult__zero(T_a)
| ~ class_Ring__and__Field_Ono__zero__divisors(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_power__eq__0__iff_1) ).
fof(f298_nnf,plain,
! [T_a,V_a] :
( c_Power_Opower__class_Opower(V_a,c_HOL_Ozero__class_Ozero(tc_nat),T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Power_Opower(T_a)
| ~ class_Ring__and__Field_Omult__zero(T_a)
| ~ class_Ring__and__Field_Ono__zero__divisors(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(nnf_transformation,[status(thm)],[f298]) ).
fof(f298_sk,plain,
! [T_a,V_a] :
( c_Power_Opower__class_Opower(V_a,c_HOL_Ozero__class_Ozero(tc_nat),T_a) != c_HOL_Ozero__class_Ozero(T_a)
| ~ class_Power_Opower(T_a)
| ~ class_Ring__and__Field_Omult__zero(T_a)
| ~ class_Ring__and__Field_Ono__zero__divisors(T_a)
| ~ class_Ring__and__Field_Ozero__neq__one(T_a) ),
inference(skolemisation,[status(esa)],[f298_nnf]) ).
cnf(c298,plain,
( c_Power_Opower__class_Opower(X1,c_HOL_Ozero__class_Ozero(tc_nat),X0) != c_HOL_Ozero__class_Ozero(X0)
| ~ class_Power_Opower(X0)
| ~ class_Ring__and__Field_Omult__zero(X0)
| ~ class_Ring__and__Field_Ono__zero__divisors(X0)
| ~ class_Ring__and__Field_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(esa)],[f298_sk]) ).
cnf(f312,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__antisym__conv2_1) ).
fof(f312_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f312]) ).
fof(f312_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f312_nnf]) ).
cnf(c312,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ c_lessequals(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f312_sk]) ).
cnf(f314,axiom,
( ~ c_lessequals(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/sandbox2/benchmark/theBenchmark.p',cls_linorder__not__less_1) ).
fof(f314_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_lessequals(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)],[f314]) ).
fof(f314_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_lessequals(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)],[f314_nnf]) ).
cnf(c314,plain,
( ~ c_lessequals(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f314_sk]) ).
cnf(f316,axiom,
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__not__le_1) ).
fof(f316_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f316]) ).
fof(f316_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f316_nnf]) ).
cnf(c316,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f316_sk]) ).
cnf(f318,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_less__le__not__le_1) ).
fof(f318_nnf,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f318]) ).
fof(f318_sk,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f318_nnf]) ).
cnf(c318,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f318_sk]) ).
cnf(f332,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/sandbox2/benchmark/theBenchmark.p',cls_zero__neq__one_0) ).
fof(f332_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)],[f332]) ).
fof(f332_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)],[f332_nnf]) ).
cnf(c332,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)],[f332_sk]) ).
cnf(f376,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/sandbox2/benchmark/theBenchmark.p',cls_not__square__less__zero_0) ).
fof(f376_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)],[f376]) ).
fof(f376_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)],[f376_nnf]) ).
cnf(c376,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)],[f376_sk]) ).
cnf(f378,axiom,
( ~ c_lessequals(c_Suc(V_n),V_m,tc_nat)
| ~ c_lessequals(V_m,V_n,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__less__eq__eq_1) ).
fof(f378_nnf,plain,
! [V_m,V_n] :
( ~ c_lessequals(c_Suc(V_n),V_m,tc_nat)
| ~ c_lessequals(V_m,V_n,tc_nat) ),
inference(nnf_transformation,[status(thm)],[f378]) ).
fof(f378_sk,plain,
! [V_m,V_n] :
( ~ c_lessequals(c_Suc(V_n),V_m,tc_nat)
| ~ c_lessequals(V_m,V_n,tc_nat) ),
inference(skolemisation,[status(esa)],[f378_nnf]) ).
cnf(c378,plain,
( ~ c_lessequals(c_Suc(X1),X0,tc_nat)
| ~ c_lessequals(X0,X1,tc_nat) ),
inference(cnf_transformation,[status(esa)],[f378_sk]) ).
cnf(f392,axiom,
c_Suc(V_n) != V_n,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__n__not__n_0) ).
fof(f392_nnf,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(nnf_transformation,[status(thm)],[f392]) ).
fof(f392_sk,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(skolemisation,[status(esa)],[f392_nnf]) ).
cnf(c392,plain,
c_Suc(X0) != X0,
inference(cnf_transformation,[status(esa)],[f392_sk]) ).
cnf(f393,axiom,
V_n != c_Suc(V_n),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_n__not__Suc__n_0) ).
fof(f393_nnf,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(nnf_transformation,[status(thm)],[f393]) ).
fof(f393_sk,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(skolemisation,[status(esa)],[f393_nnf]) ).
cnf(c393,plain,
X0 != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f393_sk]) ).
cnf(f506,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/sandbox2/benchmark/theBenchmark.p',cls_of__nat__less__0__iff_0) ).
fof(f506_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)],[f506]) ).
fof(f506_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)],[f506_nnf]) ).
cnf(c506,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)],[f506_sk]) ).
cnf(f521,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/sandbox2/benchmark/theBenchmark.p',cls_not__less__eq_1) ).
fof(f521_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)],[f521]) ).
fof(f521_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)],[f521_nnf]) ).
cnf(c521,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)],[f521_sk]) ).
cnf(f559,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/sandbox2/benchmark/theBenchmark.p',cls_sum__squares__gt__zero__iff_0) ).
fof(f559_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)],[f559]) ).
fof(f559_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)],[f559_nnf]) ).
cnf(c559,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)],[f559_sk]) ).
cnf(f611,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/sandbox2/benchmark/theBenchmark.p',cls_not__one__less__zero_0) ).
fof(f611_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)],[f611]) ).
fof(f611_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)],[f611_nnf]) ).
cnf(c611,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)],[f611_sk]) ).
cnf(f614,axiom,
~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_less__not__refl_0) ).
fof(f614_nnf,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
inference(nnf_transformation,[status(thm)],[f614]) ).
fof(f614_sk,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
inference(skolemisation,[status(esa)],[f614_nnf]) ).
cnf(c614,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f614_sk]) ).
cnf(f615,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__le_1) ).
fof(f615_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)],[f615]) ).
fof(f615_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)],[f615_nnf]) ).
cnf(c615,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f615_sk]) ).
cnf(f616,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__neq__iff_1) ).
fof(f616_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)],[f616]) ).
fof(f616_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)],[f616_nnf]) ).
cnf(c616,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f616_sk]) ).
cnf(f617,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__irrefl_0) ).
fof(f617_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)],[f617]) ).
fof(f617_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)],[f617_nnf]) ).
cnf(c617,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f617_sk]) ).
cnf(f656,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/sandbox2/benchmark/theBenchmark.p',cls_xt1_I9_J_0) ).
fof(f656_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)],[f656]) ).
fof(f656_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)],[f656_nnf]) ).
cnf(c656,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)],[f656_sk]) ).
cnf(f657,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/sandbox2/benchmark/theBenchmark.p',cls_not__less__iff__gr__or__eq_1) ).
fof(f657_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)],[f657]) ).
fof(f657_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)],[f657_nnf]) ).
cnf(c657,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)],[f657_sk]) ).
cnf(f658,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/sandbox2/benchmark/theBenchmark.p',cls_order__less__asym_0) ).
fof(f658_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)],[f658]) ).
fof(f658_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)],[f658_nnf]) ).
cnf(c658,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)],[f658_sk]) ).
cnf(f659,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/sandbox2/benchmark/theBenchmark.p',cls_order__less__asym_H_0) ).
fof(f659_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)],[f659]) ).
fof(f659_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)],[f659_nnf]) ).
cnf(c659,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)],[f659_sk]) ).
cnf(f661,axiom,
c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I7_J_0) ).
fof(f661_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)],[f661]) ).
fof(f661_sk,plain,
! [V_dB_H,V_nat] : c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat),
inference(skolemisation,[status(esa)],[f661_nnf]) ).
cnf(c661,plain,
c_Lambda_OdB_OAbs(X0) != c_Lambda_OdB_OVar(X1),
inference(cnf_transformation,[status(esa)],[f661_sk]) ).
cnf(f662,axiom,
c_Lambda_OdB_OApp(V_dB1,V_dB2) != c_Lambda_OdB_OAbs(V_dB_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I8_J_0) ).
fof(f662_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)],[f662]) ).
fof(f662_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)],[f662_nnf]) ).
cnf(c662,plain,
c_Lambda_OdB_OApp(X0,X1) != c_Lambda_OdB_OAbs(X2),
inference(cnf_transformation,[status(esa)],[f662_sk]) ).
cnf(f664,axiom,
c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OApp(V_dB1,V_dB2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I9_J_0) ).
fof(f664_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)],[f664]) ).
fof(f664_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)],[f664_nnf]) ).
cnf(c664,plain,
c_Lambda_OdB_OAbs(X0) != c_Lambda_OdB_OApp(X1,X2),
inference(cnf_transformation,[status(esa)],[f664_sk]) ).
cnf(f669,axiom,
~ c_Lambda_Obeta(c_Lambda_OdB_OVar(V_i),V_t),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_beta__cases_I1_J_0) ).
fof(f669_nnf,plain,
! [V_i,V_t] : ~ c_Lambda_Obeta(c_Lambda_OdB_OVar(V_i),V_t),
inference(nnf_transformation,[status(thm)],[f669]) ).
fof(f669_sk,plain,
! [V_i,V_t] : ~ c_Lambda_Obeta(c_Lambda_OdB_OVar(V_i),V_t),
inference(skolemisation,[status(esa)],[f669_nnf]) ).
cnf(c669,plain,
~ c_Lambda_Obeta(c_Lambda_OdB_OVar(X0),X1),
inference(cnf_transformation,[status(esa)],[f669_sk]) ).
cnf(f670,axiom,
c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OApp(V_dB1_H,V_dB2_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I4_J_0) ).
fof(f670_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)],[f670]) ).
fof(f670_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)],[f670_nnf]) ).
cnf(c670,plain,
c_Lambda_OdB_OVar(X0) != c_Lambda_OdB_OApp(X1,X2),
inference(cnf_transformation,[status(esa)],[f670_sk]) ).
cnf(f673,axiom,
c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I6_J_0) ).
fof(f673_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)],[f673]) ).
fof(f673_sk,plain,
! [V_nat,V_dB_H] : c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H),
inference(skolemisation,[status(esa)],[f673_nnf]) ).
cnf(c673,plain,
c_Lambda_OdB_OVar(X0) != c_Lambda_OdB_OAbs(X1),
inference(cnf_transformation,[status(esa)],[f673_sk]) ).
cnf(f680,axiom,
c_Lambda_OdB_OApp(V_dB1_H,V_dB2_H) != c_Lambda_OdB_OVar(V_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_dB_Osimps_I5_J_0) ).
fof(f680_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)],[f680]) ).
fof(f680_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)],[f680_nnf]) ).
cnf(c680,plain,
c_Lambda_OdB_OApp(X0,X1) != c_Lambda_OdB_OVar(X2),
inference(cnf_transformation,[status(esa)],[f680_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c54,c55,c122,c123,c198,c221,c222,c261,c273,c278,c279,c296,c297,c298,c312,c314,c316,c318,c332,c376,c378,c392,c393,c506,c521,c559,c611,c613,c614,c615,c616,c617,c656,c657,c658,c659,c661,c662,c664,c669,c670,c673,c680,c683]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t6535]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL754-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/15.39 % Computer : n003.cluster.edu
% 0.09/15.39 % Model : x86_64 x86_64
% 0.09/15.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/15.39 % Memory : 8046.5625MB
% 0.09/15.39 % OS : Linux 6.8.0-71-generic
% 0.09/15.39 % CPULimit : 300
% 0.09/15.39 % WCLimit : 300
% 0.09/15.39 % DateTime : Thu Sep 24 00:27:36 UTC 2026
% 0.09/15.39 % CPUTime :
% 0.09/15.39 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 44.44/21.80 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 44.44/21.80 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------