%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV578-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 : 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 03:13:44 PM UTC 2026
% Result : Unsatisfiable 100.19s 18.26s
% Output : Proof 100.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 30
% Syntax : Number of formulae : 135 ( 59 unt; 0 def)
% Number of atoms : 255 ( 48 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 342 ( 222 ~; 120 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 9 con; 0-4 aty)
% Number of variables : 247 ( 4 sgn 116 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f1100,negated_conjecture,
hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_f,v_m)),c_Finite__Set_Osetsum(v_f,c_SetInterval_Oord__class_OgreaterThanLessThan(v_m,v_n,tc_nat),tc_nat,t_a)) != c_Finite__Set_Osetsum(v_f,c_SetInterval_Oord__class_OatLeastLessThan(v_m,v_n,tc_nat),tc_nat,t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1100_nnf,plain,
hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_f,v_m)),c_Finite__Set_Osetsum(v_f,c_SetInterval_Oord__class_OgreaterThanLessThan(v_m,v_n,tc_nat),tc_nat,t_a)) != c_Finite__Set_Osetsum(v_f,c_SetInterval_Oord__class_OatLeastLessThan(v_m,v_n,tc_nat),tc_nat,t_a),
inference(nnf_transformation,[status(thm)],[f1100]) ).
fof(f1100_sk,plain,
hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_f,v_m)),c_Finite__Set_Osetsum(v_f,c_SetInterval_Oord__class_OgreaterThanLessThan(v_m,v_n,tc_nat),tc_nat,t_a)) != c_Finite__Set_Osetsum(v_f,c_SetInterval_Oord__class_OatLeastLessThan(v_m,v_n,tc_nat),tc_nat,t_a),
inference(skolemisation,[status(esa)],[f1100_nnf]) ).
cnf(c1100,plain,
hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_f,v_m)),c_Finite__Set_Osetsum(v_f,c_SetInterval_Oord__class_OgreaterThanLessThan(v_m,v_n,tc_nat),tc_nat,t_a)) != c_Finite__Set_Osetsum(v_f,c_SetInterval_Oord__class_OatLeastLessThan(v_m,v_n,tc_nat),tc_nat,t_a),
inference(cnf_transformation,[status(esa)],[f1100_sk]) ).
cnf(t154,plain,
eq(hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_f,v_m)),c_Finite__Set_Osetsum(v_f,c_SetInterval_Oord__class_OgreaterThanLessThan(v_m,v_n,tc_nat),tc_nat,t_a)),c_Finite__Set_Osetsum(v_f,c_SetInterval_Oord__class_OatLeastLessThan(v_m,v_n,tc_nat),tc_nat,t_a)) = false,
inference(equality_encoding,[status(esa)],[c1100]) ).
cnf(t4640,plain,
eq(hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_f,v_m)),c_Finite__Set_Osetsum(v_f,c_SetInterval_Oord__class_OgreaterThanLessThan(v_m,v_n,tc_nat),tc_nat,t_a)),c_Finite__Set_Osetsum(v_f,c_SetInterval_Oord__class_OatLeastLessThan(v_m,v_n,tc_nat),tc_nat,t_a)) = false,
inference(orient,[status(thm)],[t154]) ).
cnf(f1074,axiom,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_m,tc_nat),V_n))
| c_Finite__Set_Osetsum(V_f,c_SetInterval_Oord__class_OatLeastLessThan(V_m,V_n,tc_nat),tc_nat,T_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),hAPP(V_f,V_m)),c_Finite__Set_Osetsum(V_f,c_SetInterval_Oord__class_OatLeastLessThan(hAPP(c_Suc,V_m),V_n,tc_nat),tc_nat,T_a))
| ~ class_OrderedGroup_Ocomm__monoid__add(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_setsum__head__upt__Suc_0) ).
fof(f1074_nnf,plain,
! [T_a,V_f,V_m,V_n] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_m,tc_nat),V_n))
| c_Finite__Set_Osetsum(V_f,c_SetInterval_Oord__class_OatLeastLessThan(V_m,V_n,tc_nat),tc_nat,T_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),hAPP(V_f,V_m)),c_Finite__Set_Osetsum(V_f,c_SetInterval_Oord__class_OatLeastLessThan(hAPP(c_Suc,V_m),V_n,tc_nat),tc_nat,T_a))
| ~ class_OrderedGroup_Ocomm__monoid__add(T_a) ),
inference(nnf_transformation,[status(thm)],[f1074]) ).
fof(f1074_sk,plain,
! [T_a,V_f,V_m,V_n] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_m,tc_nat),V_n))
| c_Finite__Set_Osetsum(V_f,c_SetInterval_Oord__class_OatLeastLessThan(V_m,V_n,tc_nat),tc_nat,T_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),hAPP(V_f,V_m)),c_Finite__Set_Osetsum(V_f,c_SetInterval_Oord__class_OatLeastLessThan(hAPP(c_Suc,V_m),V_n,tc_nat),tc_nat,T_a))
| ~ class_OrderedGroup_Ocomm__monoid__add(T_a) ),
inference(skolemisation,[status(esa)],[f1074_nnf]) ).
cnf(c1074,plain,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X2,tc_nat),X3))
| c_Finite__Set_Osetsum(X1,c_SetInterval_Oord__class_OatLeastLessThan(X2,X3,tc_nat),tc_nat,X0) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),hAPP(X1,X2)),c_Finite__Set_Osetsum(X1,c_SetInterval_Oord__class_OatLeastLessThan(hAPP(c_Suc,X2),X3,tc_nat),tc_nat,X0))
| ~ class_OrderedGroup_Ocomm__monoid__add(X0) ),
inference(cnf_transformation,[status(esa)],[f1074_sk]) ).
cnf(hi1050,axiom,
ifeq(class_OrderedGroup_Ocomm__monoid__add(X0),true,ifeq(hBOOL(hAPP(c_HOL_Oord__class_Oless(X1,tc_nat),X2)),true,c_Finite__Set_Osetsum(X3,c_SetInterval_Oord__class_OatLeastLessThan(X1,X2,tc_nat),tc_nat,X0),hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),hAPP(X3,X1)),c_Finite__Set_Osetsum(X3,c_SetInterval_Oord__class_OatLeastLessThan(hAPP(c_Suc,X1),X2,tc_nat),tc_nat,X0))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),hAPP(X3,X1)),c_Finite__Set_Osetsum(X3,c_SetInterval_Oord__class_OatLeastLessThan(hAPP(c_Suc,X1),X2,tc_nat),tc_nat,X0))) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),hAPP(X3,X1)),c_Finite__Set_Osetsum(X3,c_SetInterval_Oord__class_OatLeastLessThan(hAPP(c_Suc,X1),X2,tc_nat),tc_nat,X0)),
inference(equality_encoding,[status(esa)],[c1074]) ).
cnf(f1099,negated_conjecture,
class_OrderedGroup_Ocomm__monoid__add(t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tfree_tcs) ).
fof(f1099_nnf,plain,
class_OrderedGroup_Ocomm__monoid__add(t_a),
inference(nnf_transformation,[status(thm)],[f1099]) ).
cnf(c1099,plain,
class_OrderedGroup_Ocomm__monoid__add(t_a),
inference(cnf_transformation,[status(esa)],[f1099_nnf]) ).
cnf(hi1075,negated_conjecture,
class_OrderedGroup_Ocomm__monoid__add(t_a) = true,
inference(equality_encoding,[status(esa)],[c1099]) ).
cnf(f1078,axiom,
hBOOL(hAPP(c_HOL_Oord__class_Oless(v_m,tc_nat),v_n)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_less_0) ).
fof(f1078_nnf,plain,
hBOOL(hAPP(c_HOL_Oord__class_Oless(v_m,tc_nat),v_n)),
inference(nnf_transformation,[status(thm)],[f1078]) ).
cnf(c1078,plain,
hBOOL(hAPP(c_HOL_Oord__class_Oless(v_m,tc_nat),v_n)),
inference(cnf_transformation,[status(esa)],[f1078_nnf]) ).
cnf(hi1054,axiom,
hBOOL(hAPP(c_HOL_Oord__class_Oless(v_m,tc_nat),v_n)) = true,
inference(equality_encoding,[status(esa)],[c1078]) ).
cnf(t155,plain,
hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X1,v_m)),c_Finite__Set_Osetsum(X1,c_SetInterval_Oord__class_OatLeastLessThan(hAPP(c_Suc,v_m),v_n,tc_nat),tc_nat,t_a)) = c_Finite__Set_Osetsum(X1,c_SetInterval_Oord__class_OatLeastLessThan(v_m,v_n,tc_nat),tc_nat,t_a),
inference(hyper_resolution,[status(thm)],[hi1050,hi1075,hi1054]) ).
cnf(t1619,plain,
hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X1,v_m)),c_Finite__Set_Osetsum(X1,c_SetInterval_Oord__class_OatLeastLessThan(hAPP(c_Suc,v_m),v_n,tc_nat),tc_nat,t_a)) = c_Finite__Set_Osetsum(X1,c_SetInterval_Oord__class_OatLeastLessThan(v_m,v_n,tc_nat),tc_nat,t_a),
inference(orient,[status(thm)],[t155]) ).
cnf(f1079,axiom,
c_SetInterval_Oord__class_OatLeastLessThan(hAPP(c_Suc,V_l),V_u,tc_nat) = c_SetInterval_Oord__class_OgreaterThanLessThan(V_l,V_u,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_atLeastSucLessThan__greaterThanLessThan_0) ).
fof(f1079_nnf,plain,
! [V_l,V_u] : c_SetInterval_Oord__class_OatLeastLessThan(hAPP(c_Suc,V_l),V_u,tc_nat) = c_SetInterval_Oord__class_OgreaterThanLessThan(V_l,V_u,tc_nat),
inference(nnf_transformation,[status(thm)],[f1079]) ).
fof(f1079_sk,plain,
! [V_l,V_u] : c_SetInterval_Oord__class_OatLeastLessThan(hAPP(c_Suc,V_l),V_u,tc_nat) = c_SetInterval_Oord__class_OgreaterThanLessThan(V_l,V_u,tc_nat),
inference(skolemisation,[status(esa)],[f1079_nnf]) ).
cnf(c1079,plain,
c_SetInterval_Oord__class_OatLeastLessThan(hAPP(c_Suc,X0),X1,tc_nat) = c_SetInterval_Oord__class_OgreaterThanLessThan(X0,X1,tc_nat),
inference(cnf_transformation,[status(esa)],[f1079_sk]) ).
cnf(t32,plain,
c_SetInterval_Oord__class_OatLeastLessThan(hAPP(c_Suc,X1),X2,tc_nat) = c_SetInterval_Oord__class_OgreaterThanLessThan(X1,X2,tc_nat),
inference(equality_encoding,[status(esa)],[c1079]) ).
cnf(t4785,plain,
c_SetInterval_Oord__class_OatLeastLessThan(hAPP(c_Suc,X1),X2,tc_nat) = c_SetInterval_Oord__class_OgreaterThanLessThan(X1,X2,tc_nat),
inference(orient,[status(thm)],[t32]) ).
cnf(t12503,plain,
hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X1,v_m)),c_Finite__Set_Osetsum(X1,c_SetInterval_Oord__class_OgreaterThanLessThan(v_m,v_n,tc_nat),tc_nat,t_a)) = c_Finite__Set_Osetsum(X1,c_SetInterval_Oord__class_OatLeastLessThan(v_m,v_n,tc_nat),tc_nat,t_a),
inference(step,[status(thm)],[t1619,t4785]) ).
cnf(t4809,plain,
hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X1,v_m)),c_Finite__Set_Osetsum(X1,c_SetInterval_Oord__class_OgreaterThanLessThan(v_m,v_n,tc_nat),tc_nat,t_a)) = c_Finite__Set_Osetsum(X1,c_SetInterval_Oord__class_OatLeastLessThan(v_m,v_n,tc_nat),tc_nat,t_a),
inference(rw,[status(thm)],[t12503]) ).
cnf(t12065,plain,
hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X1,v_m)),c_Finite__Set_Osetsum(X1,c_SetInterval_Oord__class_OgreaterThanLessThan(v_m,v_n,tc_nat),tc_nat,t_a)) = c_Finite__Set_Osetsum(X1,c_SetInterval_Oord__class_OatLeastLessThan(v_m,v_n,tc_nat),tc_nat,t_a),
inference(orient,[status(thm)],[t4809]) ).
cnf(t13146,plain,
eq(c_Finite__Set_Osetsum(v_f,c_SetInterval_Oord__class_OatLeastLessThan(v_m,v_n,tc_nat),tc_nat,t_a),c_Finite__Set_Osetsum(v_f,c_SetInterval_Oord__class_OatLeastLessThan(v_m,v_n,tc_nat),tc_nat,t_a)) = false,
inference(step,[status(thm)],[t4640,t12065]) ).
cnf(t4,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t4212,plain,
eq(X1,X1) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(t13147,plain,
true = false,
inference(step,[status(thm)],[t13146,t4212]) ).
cnf(t12375,plain,
true = false,
inference(rw,[status(thm)],[t13147]) ).
cnf(t12406,plain,
false = true,
inference(orient,[status(thm)],[t12375]) ).
cnf(f117,axiom,
V_n != hAPP(c_Suc,V_n),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_n__not__Suc__n_0) ).
fof(f117_nnf,plain,
! [V_n] : V_n != hAPP(c_Suc,V_n),
inference(nnf_transformation,[status(thm)],[f117]) ).
fof(f117_sk,plain,
! [V_n] : V_n != hAPP(c_Suc,V_n),
inference(skolemisation,[status(esa)],[f117_nnf]) ).
cnf(c117,plain,
X0 != hAPP(c_Suc,X0),
inference(cnf_transformation,[status(esa)],[f117_sk]) ).
cnf(f118,axiom,
hAPP(c_Suc,V_n) != V_n,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc__n__not__n_0) ).
fof(f118_nnf,plain,
! [V_n] : hAPP(c_Suc,V_n) != V_n,
inference(nnf_transformation,[status(thm)],[f118]) ).
fof(f118_sk,plain,
! [V_n] : hAPP(c_Suc,V_n) != V_n,
inference(skolemisation,[status(esa)],[f118_nnf]) ).
cnf(c118,plain,
hAPP(c_Suc,X0) != X0,
inference(cnf_transformation,[status(esa)],[f118_sk]) ).
cnf(f135,axiom,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_a,T_a),V_b))
| c_SetInterval_Oord__class_OatLeastLessThan(V_a,V_b,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_atLeastLessThan__empty__iff_0) ).
fof(f135_nnf,plain,
! [T_a,V_a,V_b] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_a,T_a),V_b))
| c_SetInterval_Oord__class_OatLeastLessThan(V_a,V_b,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f135]) ).
fof(f135_sk,plain,
! [T_a,V_a,V_b] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_a,T_a),V_b))
| c_SetInterval_Oord__class_OatLeastLessThan(V_a,V_b,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f135_nnf]) ).
cnf(c135,plain,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X1,X0),X2))
| c_SetInterval_Oord__class_OatLeastLessThan(X1,X2,X0) != c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f135_sk]) ).
cnf(f210,axiom,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_bot1E_0) ).
fof(f210_nnf,plain,
! [T_a,V_x] : ~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)),
inference(nnf_transformation,[status(thm)],[f210]) ).
fof(f210_sk,plain,
! [T_a,V_x] : ~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)),
inference(skolemisation,[status(esa)],[f210_nnf]) ).
cnf(c210,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f210_sk]) ).
cnf(f265,axiom,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),hAPP(c_HOL_Otimes__class_Otimes(V_x,T_a),V_x)),hAPP(c_HOL_Otimes__class_Otimes(V_y,T_a),V_y)),T_a),c_HOL_Ozero__class_Ozero(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(f265_nnf,plain,
! [T_a,V_x,V_y] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),hAPP(c_HOL_Otimes__class_Otimes(V_x,T_a),V_x)),hAPP(c_HOL_Otimes__class_Otimes(V_y,T_a),V_y)),T_a),c_HOL_Ozero__class_Ozero(T_a)))
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(nnf_transformation,[status(thm)],[f265]) ).
fof(f265_sk,plain,
! [T_a,V_x,V_y] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),hAPP(c_HOL_Otimes__class_Otimes(V_x,T_a),V_x)),hAPP(c_HOL_Otimes__class_Otimes(V_y,T_a),V_y)),T_a),c_HOL_Ozero__class_Ozero(T_a)))
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(skolemisation,[status(esa)],[f265_nnf]) ).
cnf(c265,plain,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),hAPP(c_HOL_Otimes__class_Otimes(X1,X0),X1)),hAPP(c_HOL_Otimes__class_Otimes(X2,X0),X2)),X0),c_HOL_Ozero__class_Ozero(X0)))
| ~ class_Ring__and__Field_Oordered__ring__strict(X0) ),
inference(cnf_transformation,[status(esa)],[f265_sk]) ).
cnf(f302,axiom,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),T_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),hAPP(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),T_a),c_HOL_Ozero__class_Ozero(T_a))),hAPP(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),T_a),c_HOL_Ozero__class_Ozero(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(f302_nnf,plain,
! [T_a] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),T_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),hAPP(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),T_a),c_HOL_Ozero__class_Ozero(T_a))),hAPP(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),T_a),c_HOL_Ozero__class_Ozero(T_a)))))
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(nnf_transformation,[status(thm)],[f302]) ).
fof(f302_sk,plain,
! [T_a] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),T_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),hAPP(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),T_a),c_HOL_Ozero__class_Ozero(T_a))),hAPP(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),T_a),c_HOL_Ozero__class_Ozero(T_a)))))
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(skolemisation,[status(esa)],[f302_nnf]) ).
cnf(c302,plain,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),X0),hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),hAPP(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),X0),c_HOL_Ozero__class_Ozero(X0))),hAPP(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(X0),X0),c_HOL_Ozero__class_Ozero(X0)))))
| ~ class_Ring__and__Field_Oordered__ring__strict(X0) ),
inference(cnf_transformation,[status(esa)],[f302_sk]) ).
cnf(f329,axiom,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_n,tc_nat),hAPP(c_Suc,V_m)))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_m,tc_nat),V_n)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less__eq_1) ).
fof(f329_nnf,plain,
! [V_m,V_n] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_n,tc_nat),hAPP(c_Suc,V_m)))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_m,tc_nat),V_n)) ),
inference(nnf_transformation,[status(thm)],[f329]) ).
fof(f329_sk,plain,
! [V_m,V_n] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_n,tc_nat),hAPP(c_Suc,V_m)))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_m,tc_nat),V_n)) ),
inference(skolemisation,[status(esa)],[f329_nnf]) ).
cnf(c329,plain,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X1,tc_nat),hAPP(c_Suc,X0)))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X0,tc_nat),X1)) ),
inference(cnf_transformation,[status(esa)],[f329_sk]) ).
cnf(f397,axiom,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(c_HOL_Otimes__class_Otimes(V_a,T_a),V_a),T_a),c_HOL_Ozero__class_Ozero(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(f397_nnf,plain,
! [T_a,V_a] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(c_HOL_Otimes__class_Otimes(V_a,T_a),V_a),T_a),c_HOL_Ozero__class_Ozero(T_a)))
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(nnf_transformation,[status(thm)],[f397]) ).
fof(f397_sk,plain,
! [T_a,V_a] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(c_HOL_Otimes__class_Otimes(V_a,T_a),V_a),T_a),c_HOL_Ozero__class_Ozero(T_a)))
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(skolemisation,[status(esa)],[f397_nnf]) ).
cnf(c397,plain,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(hAPP(c_HOL_Otimes__class_Otimes(X1,X0),X1),X0),c_HOL_Ozero__class_Ozero(X0)))
| ~ class_Ring__and__Field_Oordered__ring__strict(X0) ),
inference(cnf_transformation,[status(esa)],[f397_sk]) ).
cnf(f599,axiom,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,T_a),V_y))
| ~ hBOOL(hAPP(c_lessequals(V_y,T_a),V_x))
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_less__le__not__le_1) ).
fof(f599_nnf,plain,
! [T_a,V_y,V_x] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,T_a),V_y))
| ~ hBOOL(hAPP(c_lessequals(V_y,T_a),V_x))
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f599]) ).
fof(f599_sk,plain,
! [T_a,V_y,V_x] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,T_a),V_y))
| ~ hBOOL(hAPP(c_lessequals(V_y,T_a),V_x))
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f599_nnf]) ).
cnf(c599,plain,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X2,X0),X1))
| ~ hBOOL(hAPP(c_lessequals(X1,X0),X2))
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f599_sk]) ).
cnf(f601,axiom,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,T_a),V_x))
| ~ hBOOL(hAPP(c_lessequals(V_x,T_a),V_x))
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__antisym__conv2_1) ).
fof(f601_nnf,plain,
! [T_a,V_x] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,T_a),V_x))
| ~ hBOOL(hAPP(c_lessequals(V_x,T_a),V_x))
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f601]) ).
fof(f601_sk,plain,
! [T_a,V_x] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,T_a),V_x))
| ~ hBOOL(hAPP(c_lessequals(V_x,T_a),V_x))
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f601_nnf]) ).
cnf(c601,plain,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X1,X0),X1))
| ~ hBOOL(hAPP(c_lessequals(X1,X0),X1))
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f601_sk]) ).
cnf(f603,axiom,
( ~ hBOOL(hAPP(c_lessequals(V_y,T_a),V_x))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,T_a),V_y))
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__not__less_1) ).
fof(f603_nnf,plain,
! [T_a,V_x,V_y] :
( ~ hBOOL(hAPP(c_lessequals(V_y,T_a),V_x))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,T_a),V_y))
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f603]) ).
fof(f603_sk,plain,
! [T_a,V_x,V_y] :
( ~ hBOOL(hAPP(c_lessequals(V_y,T_a),V_x))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,T_a),V_y))
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f603_nnf]) ).
cnf(c603,plain,
( ~ hBOOL(hAPP(c_lessequals(X2,X0),X1))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X1,X0),X2))
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f603_sk]) ).
cnf(f606,axiom,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_y,T_a),V_x))
| ~ hBOOL(hAPP(c_lessequals(V_x,T_a),V_y))
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__not__le_1) ).
fof(f606_nnf,plain,
! [T_a,V_x,V_y] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_y,T_a),V_x))
| ~ hBOOL(hAPP(c_lessequals(V_x,T_a),V_y))
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f606]) ).
fof(f606_sk,plain,
! [T_a,V_x,V_y] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_y,T_a),V_x))
| ~ hBOOL(hAPP(c_lessequals(V_x,T_a),V_y))
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f606_nnf]) ).
cnf(c606,plain,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X2,X0),X1))
| ~ hBOOL(hAPP(c_lessequals(X1,X0),X2))
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f606_sk]) ).
cnf(f674,axiom,
( ~ hBOOL(hAPP(c_lessequals(hAPP(c_Suc,V_n),tc_nat),V_m))
| ~ hBOOL(hAPP(c_lessequals(V_m,tc_nat),V_n)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less__eq__eq_1) ).
fof(f674_nnf,plain,
! [V_m,V_n] :
( ~ hBOOL(hAPP(c_lessequals(hAPP(c_Suc,V_n),tc_nat),V_m))
| ~ hBOOL(hAPP(c_lessequals(V_m,tc_nat),V_n)) ),
inference(nnf_transformation,[status(thm)],[f674]) ).
fof(f674_sk,plain,
! [V_m,V_n] :
( ~ hBOOL(hAPP(c_lessequals(hAPP(c_Suc,V_n),tc_nat),V_m))
| ~ hBOOL(hAPP(c_lessequals(V_m,tc_nat),V_n)) ),
inference(skolemisation,[status(esa)],[f674_nnf]) ).
cnf(c674,plain,
( ~ hBOOL(hAPP(c_lessequals(hAPP(c_Suc,X1),tc_nat),X0))
| ~ hBOOL(hAPP(c_lessequals(X0,tc_nat),X1)) ),
inference(cnf_transformation,[status(esa)],[f674_sk]) ).
cnf(f761,axiom,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,T_a),V_x))
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__neq__iff_1) ).
fof(f761_nnf,plain,
! [T_a,V_x] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,T_a),V_x))
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f761]) ).
fof(f761_sk,plain,
! [T_a,V_x] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,T_a),V_x))
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f761_nnf]) ).
cnf(c761,plain,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X1,X0),X1))
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f761_sk]) ).
cnf(f762,axiom,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,T_a),V_x))
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__le_1) ).
fof(f762_nnf,plain,
! [T_a,V_x] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,T_a),V_x))
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f762]) ).
fof(f762_sk,plain,
! [T_a,V_x] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,T_a),V_x))
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f762_nnf]) ).
cnf(c762,plain,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X1,X0),X1))
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f762_sk]) ).
cnf(f763,axiom,
~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_n,tc_nat),V_n)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_less__not__refl_0) ).
fof(f763_nnf,plain,
! [V_n] : ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_n,tc_nat),V_n)),
inference(nnf_transformation,[status(thm)],[f763]) ).
fof(f763_sk,plain,
! [V_n] : ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_n,tc_nat),V_n)),
inference(skolemisation,[status(esa)],[f763_nnf]) ).
cnf(c763,plain,
~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X0,tc_nat),X0)),
inference(cnf_transformation,[status(esa)],[f763_sk]) ).
cnf(f764,axiom,
~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,tc_nat),V_x)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat__less__le_1) ).
fof(f764_nnf,plain,
! [V_x] : ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,tc_nat),V_x)),
inference(nnf_transformation,[status(thm)],[f764]) ).
fof(f764_sk,plain,
! [V_x] : ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,tc_nat),V_x)),
inference(skolemisation,[status(esa)],[f764_nnf]) ).
cnf(c764,plain,
~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X0,tc_nat),X0)),
inference(cnf_transformation,[status(esa)],[f764_sk]) ).
cnf(f765,axiom,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,T_a),V_x))
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__irrefl_0) ).
fof(f765_nnf,plain,
! [T_a,V_x] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,T_a),V_x))
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f765]) ).
fof(f765_sk,plain,
! [T_a,V_x] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,T_a),V_x))
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f765_nnf]) ).
cnf(c765,plain,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X1,X0),X1))
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f765_sk]) ).
cnf(f812,axiom,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_a,T_a),V_b))
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_SetInterval_Oord__class_OatLeastLessThan(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_atLeastLessThan__empty__iff2_0) ).
fof(f812_nnf,plain,
! [T_a,V_a,V_b] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_a,T_a),V_b))
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_SetInterval_Oord__class_OatLeastLessThan(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f812]) ).
fof(f812_sk,plain,
! [T_a,V_a,V_b] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_a,T_a),V_b))
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_SetInterval_Oord__class_OatLeastLessThan(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f812_nnf]) ).
cnf(c812,plain,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X1,X0),X2))
| c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_SetInterval_Oord__class_OatLeastLessThan(X1,X2,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f812_sk]) ).
cnf(f912,axiom,
~ hBOOL(hAPP(c_lessequals(hAPP(c_Suc,V_n),tc_nat),V_n)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc__n__not__le__n_0) ).
fof(f912_nnf,plain,
! [V_n] : ~ hBOOL(hAPP(c_lessequals(hAPP(c_Suc,V_n),tc_nat),V_n)),
inference(nnf_transformation,[status(thm)],[f912]) ).
fof(f912_sk,plain,
! [V_n] : ~ hBOOL(hAPP(c_lessequals(hAPP(c_Suc,V_n),tc_nat),V_n)),
inference(skolemisation,[status(esa)],[f912_nnf]) ).
cnf(c912,plain,
~ hBOOL(hAPP(c_lessequals(hAPP(c_Suc,X0),tc_nat),X0)),
inference(cnf_transformation,[status(esa)],[f912_sk]) ).
cnf(f993,axiom,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_a,T_a),V_b))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_b,T_a),V_a))
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__asym_H_0) ).
fof(f993_nnf,plain,
! [T_a,V_b,V_a] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_a,T_a),V_b))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_b,T_a),V_a))
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f993]) ).
fof(f993_sk,plain,
! [T_a,V_b,V_a] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_a,T_a),V_b))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_b,T_a),V_a))
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f993_nnf]) ).
cnf(c993,plain,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X2,X0),X1))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X1,X0),X2))
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f993_sk]) ).
cnf(f994,axiom,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,T_a),V_y))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_y,T_a),V_x))
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__asym_0) ).
fof(f994_nnf,plain,
! [T_a,V_y,V_x] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,T_a),V_y))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_y,T_a),V_x))
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f994]) ).
fof(f994_sk,plain,
! [T_a,V_y,V_x] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,T_a),V_y))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_y,T_a),V_x))
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f994_nnf]) ).
cnf(c994,plain,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X2,X0),X1))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X1,X0),X2))
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f994_sk]) ).
cnf(f997,axiom,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_y,T_a),V_x))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,T_a),V_y))
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less__iff__gr__or__eq_1) ).
fof(f997_nnf,plain,
! [T_a,V_x,V_y] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_y,T_a),V_x))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,T_a),V_y))
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f997]) ).
fof(f997_sk,plain,
! [T_a,V_x,V_y] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_y,T_a),V_x))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_x,T_a),V_y))
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f997_nnf]) ).
cnf(c997,plain,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X2,X0),X1))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X1,X0),X2))
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f997_sk]) ).
cnf(f998,axiom,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_b,T_a),V_a))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_a,T_a),V_b))
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_xt1_I9_J_0) ).
fof(f998_nnf,plain,
! [T_a,V_a,V_b] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_b,T_a),V_a))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_a,T_a),V_b))
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f998]) ).
fof(f998_sk,plain,
! [T_a,V_a,V_b] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_b,T_a),V_a))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(V_a,T_a),V_b))
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f998_nnf]) ).
cnf(c998,plain,
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X2,X0),X1))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X1,X0),X2))
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f998_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c117,c118,c135,c210,c265,c302,c329,c397,c599,c601,c603,c606,c674,c761,c762,c763,c764,c765,c812,c912,c993,c994,c997,c998,c1100]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t12406]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV578-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/5.58 % Computer : n003.cluster.edu
% 0.10/5.58 % Model : x86_64 x86_64
% 0.10/5.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.58 % Memory : 8046.5625MB
% 0.10/5.58 % OS : Linux 6.8.0-71-generic
% 0.10/5.59 % CPULimit : 300
% 0.10/5.59 % WCLimit : 300
% 0.10/5.59 % DateTime : Thu Sep 24 20:39:46 UTC 2026
% 0.10/5.59 % CPUTime :
% 0.10/5.59 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 100.19/18.26 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 100.19/18.26 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------