%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV875-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 : n011.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:14:21 PM UTC 2026
% Result : Unsatisfiable 33.37s 5.21s
% Output : Proof 33.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 55
% Syntax : Number of formulae : 227 ( 115 unt; 0 def)
% Number of atoms : 403 ( 86 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 566 ( 390 ~; 176 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 31 ( 31 usr; 6 con; 0-5 aty)
% Number of variables : 568 ( 88 sgn 280 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f1045,negated_conjecture,
~ hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OSKIP),v_x),v_x)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1045_nnf,plain,
~ hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OSKIP),v_x),v_x)),
inference(nnf_transformation,[status(thm)],[f1045]) ).
fof(f1045_sk,plain,
~ hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OSKIP),v_x),v_x)),
inference(skolemisation,[status(esa)],[f1045_nnf]) ).
cnf(c1045,plain,
~ hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OSKIP),v_x),v_x)),
inference(cnf_transformation,[status(esa)],[f1045_sk]) ).
cnf(t43,plain,
ifeq(hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OSKIP),v_x),v_x)),true,false,true) = true,
inference(equality_encoding,[status(esa)],[c1045]) ).
cnf(f1019,axiom,
hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OSKIP),V_s),V_s)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_evalc_OSkip_0) ).
fof(f1019_nnf,plain,
! [V_s] : hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OSKIP),V_s),V_s)),
inference(nnf_transformation,[status(thm)],[f1019]) ).
fof(f1019_sk,plain,
! [V_s] : hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OSKIP),V_s),V_s)),
inference(skolemisation,[status(esa)],[f1019_nnf]) ).
cnf(c1019,plain,
hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OSKIP),X0),X0)),
inference(cnf_transformation,[status(esa)],[f1019_sk]) ).
cnf(t17,plain,
hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OSKIP),X1),X1)) = true,
inference(equality_encoding,[status(esa)],[c1019]) ).
cnf(t480,plain,
hBOOL(hAPP(hAPP(c_Natural_Oevalc(c_Com_Ocom_OSKIP),X1),X1)) = true,
inference(orient,[status(thm)],[t17]) ).
cnf(t1578,plain,
ifeq(true,true,false,true) = true,
inference(step,[status(thm)],[t43,t480]) ).
cnf(t9,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t195,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t9]) ).
cnf(t1579,plain,
false = true,
inference(step,[status(thm)],[t1578,t195]) ).
cnf(t1568,plain,
false = true,
inference(orient,[status(thm)],[t1579]) ).
cnf(f42,axiom,
c_Fun_Ofun__upd(V_t,V_k,hAPP(c_Option_Ooption_OSome(T_b),V_x),T_a,tc_Option_Ooption(T_b)) != c_COMBK(c_Option_Ooption_ONone(T_b),tc_Option_Ooption(T_b),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_map__upd__nonempty_0) ).
fof(f42_nnf,plain,
! [V_t,V_k,T_b,V_x,T_a] : c_Fun_Ofun__upd(V_t,V_k,hAPP(c_Option_Ooption_OSome(T_b),V_x),T_a,tc_Option_Ooption(T_b)) != c_COMBK(c_Option_Ooption_ONone(T_b),tc_Option_Ooption(T_b),T_a),
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
! [V_t,V_k,T_b,V_x,T_a] : c_Fun_Ofun__upd(V_t,V_k,hAPP(c_Option_Ooption_OSome(T_b),V_x),T_a,tc_Option_Ooption(T_b)) != c_COMBK(c_Option_Ooption_ONone(T_b),tc_Option_Ooption(T_b),T_a),
inference(skolemisation,[status(esa)],[f42_nnf]) ).
cnf(c42,plain,
c_Fun_Ofun__upd(X0,X1,hAPP(c_Option_Ooption_OSome(X2),X3),X4,tc_Option_Ooption(X2)) != c_COMBK(c_Option_Ooption_ONone(X2),tc_Option_Ooption(X2),X4),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(f95,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),hAPP(hAPP(c_HOL_Otimes__class_Otimes(T_a),V_x),V_x)),hAPP(hAPP(c_HOL_Otimes__class_Otimes(T_a),V_y),V_y))),c_HOL_Ozero__class_Ozero(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(f95_nnf,plain,
! [T_a,V_x,V_y] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),hAPP(hAPP(c_HOL_Otimes__class_Otimes(T_a),V_x),V_x)),hAPP(hAPP(c_HOL_Otimes__class_Otimes(T_a),V_y),V_y))),c_HOL_Ozero__class_Ozero(T_a)))
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(nnf_transformation,[status(thm)],[f95]) ).
fof(f95_sk,plain,
! [T_a,V_x,V_y] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),hAPP(hAPP(c_HOL_Otimes__class_Otimes(T_a),V_x),V_x)),hAPP(hAPP(c_HOL_Otimes__class_Otimes(T_a),V_y),V_y))),c_HOL_Ozero__class_Ozero(T_a)))
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(skolemisation,[status(esa)],[f95_nnf]) ).
cnf(c95,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),hAPP(hAPP(c_HOL_Otimes__class_Otimes(X0),X1),X1)),hAPP(hAPP(c_HOL_Otimes__class_Otimes(X0),X2),X2))),c_HOL_Ozero__class_Ozero(X0)))
| ~ class_Ring__and__Field_Oordered__ring__strict(X0) ),
inference(cnf_transformation,[status(esa)],[f95_sk]) ).
cnf(f131,axiom,
~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_fun(T_a,tc_bool)),V_x),V_x)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_psubset__eq_1) ).
fof(f131_nnf,plain,
! [T_a,V_x] : ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_fun(T_a,tc_bool)),V_x),V_x)),
inference(nnf_transformation,[status(thm)],[f131]) ).
fof(f131_sk,plain,
! [T_a,V_x] : ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_fun(T_a,tc_bool)),V_x),V_x)),
inference(skolemisation,[status(esa)],[f131_nnf]) ).
cnf(c131,plain,
~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_fun(X0,tc_bool)),X1),X1)),
inference(cnf_transformation,[status(esa)],[f131_sk]) ).
cnf(f132,axiom,
~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_x),V_x)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat__less__le_1) ).
fof(f132_nnf,plain,
! [V_x] : ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_x),V_x)),
inference(nnf_transformation,[status(thm)],[f132]) ).
fof(f132_sk,plain,
! [V_x] : ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_x),V_x)),
inference(skolemisation,[status(esa)],[f132_nnf]) ).
cnf(c132,plain,
~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),X0),X0)),
inference(cnf_transformation,[status(esa)],[f132_sk]) ).
cnf(f133,axiom,
~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_n),V_n)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_less__not__refl_0) ).
fof(f133_nnf,plain,
! [V_n] : ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_n),V_n)),
inference(nnf_transformation,[status(thm)],[f133]) ).
fof(f133_sk,plain,
! [V_n] : ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_n),V_n)),
inference(skolemisation,[status(esa)],[f133_nnf]) ).
cnf(c133,plain,
~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),X0),X0)),
inference(cnf_transformation,[status(esa)],[f133_sk]) ).
cnf(f135,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_x))
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__le_1) ).
fof(f135_nnf,plain,
! [T_a,V_x] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_x))
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f135]) ).
fof(f135_sk,plain,
! [T_a,V_x] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_x))
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f135_nnf]) ).
cnf(c135,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X1),X1))
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f135_sk]) ).
cnf(f136,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_x))
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__neq__iff_1) ).
fof(f136_nnf,plain,
! [T_a,V_x] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_x))
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f136]) ).
fof(f136_sk,plain,
! [T_a,V_x] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_x))
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f136_nnf]) ).
cnf(c136,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X1),X1))
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f136_sk]) ).
cnf(f137,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_x))
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__irrefl_0) ).
fof(f137_nnf,plain,
! [T_a,V_x] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_x))
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f137]) ).
fof(f137_sk,plain,
! [T_a,V_x] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_x))
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f137_nnf]) ).
cnf(c137,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X1),X1))
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f137_sk]) ).
cnf(f234,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_x))
| ~ hBOOL(hAPP(hAPP(c_lessequals(T_a),V_x),V_x))
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__antisym__conv2_1) ).
fof(f234_nnf,plain,
! [T_a,V_x] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_x))
| ~ hBOOL(hAPP(hAPP(c_lessequals(T_a),V_x),V_x))
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f234]) ).
fof(f234_sk,plain,
! [T_a,V_x] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_x))
| ~ hBOOL(hAPP(hAPP(c_lessequals(T_a),V_x),V_x))
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f234_nnf]) ).
cnf(c234,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X1),X1))
| ~ hBOOL(hAPP(hAPP(c_lessequals(X0),X1),X1))
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f234_sk]) ).
cnf(f236,axiom,
( ~ hBOOL(hAPP(hAPP(c_lessequals(T_a),V_y),V_x))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_y))
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__not__less_1) ).
fof(f236_nnf,plain,
! [T_a,V_x,V_y] :
( ~ hBOOL(hAPP(hAPP(c_lessequals(T_a),V_y),V_x))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_y))
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f236]) ).
fof(f236_sk,plain,
! [T_a,V_x,V_y] :
( ~ hBOOL(hAPP(hAPP(c_lessequals(T_a),V_y),V_x))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_y))
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f236_nnf]) ).
cnf(c236,plain,
( ~ hBOOL(hAPP(hAPP(c_lessequals(X0),X2),X1))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X1),X2))
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f236_sk]) ).
cnf(f238,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_y),V_x))
| ~ hBOOL(hAPP(hAPP(c_lessequals(T_a),V_x),V_y))
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__not__le_1) ).
fof(f238_nnf,plain,
! [T_a,V_x,V_y] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_y),V_x))
| ~ hBOOL(hAPP(hAPP(c_lessequals(T_a),V_x),V_y))
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f238]) ).
fof(f238_sk,plain,
! [T_a,V_x,V_y] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_y),V_x))
| ~ hBOOL(hAPP(hAPP(c_lessequals(T_a),V_x),V_y))
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f238_nnf]) ).
cnf(c238,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X2),X1))
| ~ hBOOL(hAPP(hAPP(c_lessequals(X0),X1),X2))
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f238_sk]) ).
cnf(f240,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_fun(T_a,T_b)),V_f),V_g))
| ~ hBOOL(hAPP(hAPP(c_lessequals(tc_fun(T_a,T_b)),V_g),V_f))
| ~ class_HOL_Oord(T_b) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_less__fun__def_1) ).
fof(f240_nnf,plain,
! [T_b,T_a,V_g,V_f] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_fun(T_a,T_b)),V_f),V_g))
| ~ hBOOL(hAPP(hAPP(c_lessequals(tc_fun(T_a,T_b)),V_g),V_f))
| ~ class_HOL_Oord(T_b) ),
inference(nnf_transformation,[status(thm)],[f240]) ).
fof(f240_sk,plain,
! [T_b,T_a,V_g,V_f] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_fun(T_a,T_b)),V_f),V_g))
| ~ hBOOL(hAPP(hAPP(c_lessequals(tc_fun(T_a,T_b)),V_g),V_f))
| ~ class_HOL_Oord(T_b) ),
inference(skolemisation,[status(esa)],[f240_nnf]) ).
cnf(c240,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_fun(X1,X0)),X3),X2))
| ~ hBOOL(hAPP(hAPP(c_lessequals(tc_fun(X1,X0)),X2),X3))
| ~ class_HOL_Oord(X0) ),
inference(cnf_transformation,[status(esa)],[f240_sk]) ).
cnf(f241,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_y))
| ~ hBOOL(hAPP(hAPP(c_lessequals(T_a),V_y),V_x))
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_less__le__not__le_1) ).
fof(f241_nnf,plain,
! [T_a,V_y,V_x] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_y))
| ~ hBOOL(hAPP(hAPP(c_lessequals(T_a),V_y),V_x))
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f241]) ).
fof(f241_sk,plain,
! [T_a,V_y,V_x] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_y))
| ~ hBOOL(hAPP(hAPP(c_lessequals(T_a),V_y),V_x))
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f241_nnf]) ).
cnf(c241,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X2),X1))
| ~ hBOOL(hAPP(hAPP(c_lessequals(X0),X1),X2))
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f241_sk]) ).
cnf(f293,axiom,
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less,V_y),V_x))
| ~ hBOOL(hAPP(hAPP(V_less,V_x),V_y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder_Onot__less__iff__gr__or__eq_1) ).
fof(f293_nnf,plain,
! [V_less,V_x,V_y,V_less__eq,T_a] :
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less,V_y),V_x))
| ~ hBOOL(hAPP(hAPP(V_less,V_x),V_y)) ),
inference(nnf_transformation,[status(thm)],[f293]) ).
fof(f293_sk,plain,
! [V_less,V_x,V_y,V_less__eq,T_a] :
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less,V_y),V_x))
| ~ hBOOL(hAPP(hAPP(V_less,V_x),V_y)) ),
inference(skolemisation,[status(esa)],[f293_nnf]) ).
cnf(c293,plain,
( ~ c_Orderings_Olinorder(X3,X0,X4)
| ~ hBOOL(hAPP(hAPP(X0,X2),X1))
| ~ hBOOL(hAPP(hAPP(X0,X1),X2)) ),
inference(cnf_transformation,[status(esa)],[f293_sk]) ).
cnf(f294,axiom,
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less__eq,V_y),V_x))
| ~ hBOOL(hAPP(hAPP(V_less,V_x),V_y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder_OleD_0) ).
fof(f294_nnf,plain,
! [V_less,V_x,V_y,V_less__eq,T_a] :
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less__eq,V_y),V_x))
| ~ hBOOL(hAPP(hAPP(V_less,V_x),V_y)) ),
inference(nnf_transformation,[status(thm)],[f294]) ).
fof(f294_sk,plain,
! [V_less,V_x,V_y,V_less__eq,T_a] :
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less__eq,V_y),V_x))
| ~ hBOOL(hAPP(hAPP(V_less,V_x),V_y)) ),
inference(skolemisation,[status(esa)],[f294_nnf]) ).
cnf(c294,plain,
( ~ c_Orderings_Olinorder(X3,X0,X4)
| ~ hBOOL(hAPP(hAPP(X3,X2),X1))
| ~ hBOOL(hAPP(hAPP(X0,X1),X2)) ),
inference(cnf_transformation,[status(esa)],[f294_sk]) ).
cnf(f298,axiom,
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less,V_y),V_x))
| ~ hBOOL(hAPP(hAPP(V_less__eq,V_x),V_y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder_Onot__le_1) ).
fof(f298_nnf,plain,
! [V_less__eq,V_x,V_y,V_less,T_a] :
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less,V_y),V_x))
| ~ hBOOL(hAPP(hAPP(V_less__eq,V_x),V_y)) ),
inference(nnf_transformation,[status(thm)],[f298]) ).
fof(f298_sk,plain,
! [V_less__eq,V_x,V_y,V_less,T_a] :
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less,V_y),V_x))
| ~ hBOOL(hAPP(hAPP(V_less__eq,V_x),V_y)) ),
inference(skolemisation,[status(esa)],[f298_nnf]) ).
cnf(c298,plain,
( ~ c_Orderings_Olinorder(X0,X3,X4)
| ~ hBOOL(hAPP(hAPP(X3,X2),X1))
| ~ hBOOL(hAPP(hAPP(X0,X1),X2)) ),
inference(cnf_transformation,[status(esa)],[f298_sk]) ).
cnf(f301,axiom,
( ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x))
| ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less__eq,V_x),V_x)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder_Oantisym__conv2_1) ).
fof(f301_nnf,plain,
! [V_less__eq,V_x,V_less,T_a] :
( ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x))
| ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less__eq,V_x),V_x)) ),
inference(nnf_transformation,[status(thm)],[f301]) ).
fof(f301_sk,plain,
! [V_less__eq,V_x,V_less,T_a] :
( ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x))
| ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less__eq,V_x),V_x)) ),
inference(skolemisation,[status(esa)],[f301_nnf]) ).
cnf(c301,plain,
( ~ hBOOL(hAPP(hAPP(X2,X1),X1))
| ~ c_Orderings_Olinorder(X0,X2,X3)
| ~ hBOOL(hAPP(hAPP(X0,X1),X1)) ),
inference(cnf_transformation,[status(esa)],[f301_sk]) ).
cnf(f351,axiom,
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder_Oneq__iff_1) ).
fof(f351_nnf,plain,
! [V_less,V_x,V_less__eq,T_a] :
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x)) ),
inference(nnf_transformation,[status(thm)],[f351]) ).
fof(f351_sk,plain,
! [V_less,V_x,V_less__eq,T_a] :
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x)) ),
inference(skolemisation,[status(esa)],[f351_nnf]) ).
cnf(c351,plain,
( ~ c_Orderings_Olinorder(X2,X0,X3)
| ~ hBOOL(hAPP(hAPP(X0,X1),X1)) ),
inference(cnf_transformation,[status(esa)],[f351_sk]) ).
cnf(f352,axiom,
( ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x))
| ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder_Onot__less__iff__gr__or__eq_2) ).
fof(f352_nnf,plain,
! [V_less__eq,V_less,T_a,V_x] :
( ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x))
| ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a) ),
inference(nnf_transformation,[status(thm)],[f352]) ).
fof(f352_sk,plain,
! [V_less__eq,V_less,T_a,V_x] :
( ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x))
| ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a) ),
inference(skolemisation,[status(esa)],[f352_nnf]) ).
cnf(c352,plain,
( ~ hBOOL(hAPP(hAPP(X1,X3),X3))
| ~ c_Orderings_Olinorder(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f352_sk]) ).
cnf(f422,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),hAPP(hAPP(c_HOL_Otimes__class_Otimes(T_a),V_a),V_a)),c_HOL_Ozero__class_Ozero(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(f422_nnf,plain,
! [T_a,V_a] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),hAPP(hAPP(c_HOL_Otimes__class_Otimes(T_a),V_a),V_a)),c_HOL_Ozero__class_Ozero(T_a)))
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(nnf_transformation,[status(thm)],[f422]) ).
fof(f422_sk,plain,
! [T_a,V_a] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),hAPP(hAPP(c_HOL_Otimes__class_Otimes(T_a),V_a),V_a)),c_HOL_Ozero__class_Ozero(T_a)))
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(skolemisation,[status(esa)],[f422_nnf]) ).
cnf(c422,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),hAPP(hAPP(c_HOL_Otimes__class_Otimes(X0),X1),X1)),c_HOL_Ozero__class_Ozero(X0)))
| ~ class_Ring__and__Field_Oordered__ring__strict(X0) ),
inference(cnf_transformation,[status(esa)],[f422_sk]) ).
cnf(f457,axiom,
c_Suc(V_n) != V_n,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__n__not__n_0) ).
fof(f457_nnf,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(nnf_transformation,[status(thm)],[f457]) ).
fof(f457_sk,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(skolemisation,[status(esa)],[f457_nnf]) ).
cnf(c457,plain,
c_Suc(X0) != X0,
inference(cnf_transformation,[status(esa)],[f457_sk]) ).
cnf(f458,axiom,
V_n != c_Suc(V_n),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_n__not__Suc__n_0) ).
fof(f458_nnf,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(nnf_transformation,[status(thm)],[f458]) ).
fof(f458_sk,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(skolemisation,[status(esa)],[f458_nnf]) ).
cnf(c458,plain,
X0 != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f458_sk]) ).
cnf(f554,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_n),c_Suc(V_m)))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_m),V_n)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__less__eq_1) ).
fof(f554_nnf,plain,
! [V_m,V_n] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_n),c_Suc(V_m)))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_m),V_n)) ),
inference(nnf_transformation,[status(thm)],[f554]) ).
fof(f554_sk,plain,
! [V_m,V_n] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_n),c_Suc(V_m)))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),V_m),V_n)) ),
inference(skolemisation,[status(esa)],[f554_nnf]) ).
cnf(c554,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),X1),c_Suc(X0)))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_nat),X0),X1)) ),
inference(cnf_transformation,[status(esa)],[f554_sk]) ).
cnf(f588,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),c_HOL_Ozero__class_Ozero(T_a)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),hAPP(hAPP(c_HOL_Otimes__class_Otimes(T_a),c_HOL_Ozero__class_Ozero(T_a)),c_HOL_Ozero__class_Ozero(T_a))),hAPP(hAPP(c_HOL_Otimes__class_Otimes(T_a),c_HOL_Ozero__class_Ozero(T_a)),c_HOL_Ozero__class_Ozero(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(f588_nnf,plain,
! [T_a] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),c_HOL_Ozero__class_Ozero(T_a)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),hAPP(hAPP(c_HOL_Otimes__class_Otimes(T_a),c_HOL_Ozero__class_Ozero(T_a)),c_HOL_Ozero__class_Ozero(T_a))),hAPP(hAPP(c_HOL_Otimes__class_Otimes(T_a),c_HOL_Ozero__class_Ozero(T_a)),c_HOL_Ozero__class_Ozero(T_a)))))
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(nnf_transformation,[status(thm)],[f588]) ).
fof(f588_sk,plain,
! [T_a] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),c_HOL_Ozero__class_Ozero(T_a)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),hAPP(hAPP(c_HOL_Otimes__class_Otimes(T_a),c_HOL_Ozero__class_Ozero(T_a)),c_HOL_Ozero__class_Ozero(T_a))),hAPP(hAPP(c_HOL_Otimes__class_Otimes(T_a),c_HOL_Ozero__class_Ozero(T_a)),c_HOL_Ozero__class_Ozero(T_a)))))
| ~ class_Ring__and__Field_Oordered__ring__strict(T_a) ),
inference(skolemisation,[status(esa)],[f588_nnf]) ).
cnf(c588,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),c_HOL_Ozero__class_Ozero(X0)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),hAPP(hAPP(c_HOL_Otimes__class_Otimes(X0),c_HOL_Ozero__class_Ozero(X0)),c_HOL_Ozero__class_Ozero(X0))),hAPP(hAPP(c_HOL_Otimes__class_Otimes(X0),c_HOL_Ozero__class_Ozero(X0)),c_HOL_Ozero__class_Ozero(X0)))))
| ~ class_Ring__and__Field_Oordered__ring__strict(X0) ),
inference(cnf_transformation,[status(esa)],[f588_sk]) ).
cnf(f636,axiom,
~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_fun(T_a,tc_bool)),V_A),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__psubset__empty_0) ).
fof(f636_nnf,plain,
! [T_a,V_A] : ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_fun(T_a,tc_bool)),V_A),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
inference(nnf_transformation,[status(thm)],[f636]) ).
fof(f636_sk,plain,
! [T_a,V_A] : ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_fun(T_a,tc_bool)),V_A),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
inference(skolemisation,[status(esa)],[f636_nnf]) ).
cnf(c636,plain,
~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_fun(X0,tc_bool)),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
inference(cnf_transformation,[status(esa)],[f636_sk]) ).
cnf(f659,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_b),V_a))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_a),V_b))
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_xt1_I9_J_0) ).
fof(f659_nnf,plain,
! [T_a,V_a,V_b] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_b),V_a))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_a),V_b))
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f659]) ).
fof(f659_sk,plain,
! [T_a,V_a,V_b] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_b),V_a))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_a),V_b))
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f659_nnf]) ).
cnf(c659,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X2),X1))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X1),X2))
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f659_sk]) ).
cnf(f660,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_y),V_x))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_y))
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__less__iff__gr__or__eq_1) ).
fof(f660_nnf,plain,
! [T_a,V_x,V_y] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_y),V_x))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_y))
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f660]) ).
fof(f660_sk,plain,
! [T_a,V_x,V_y] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_y),V_x))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_y))
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f660_nnf]) ).
cnf(c660,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X2),X1))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X1),X2))
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f660_sk]) ).
cnf(f662,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_y))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_y),V_x))
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__asym_0) ).
fof(f662_nnf,plain,
! [T_a,V_y,V_x] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_y))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_y),V_x))
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f662]) ).
fof(f662_sk,plain,
! [T_a,V_y,V_x] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_y))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_y),V_x))
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f662_nnf]) ).
cnf(c662,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X2),X1))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X1),X2))
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f662_sk]) ).
cnf(f663,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_a),V_b))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_b),V_a))
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__asym_H_0) ).
fof(f663_nnf,plain,
! [T_a,V_b,V_a] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_a),V_b))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_b),V_a))
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f663]) ).
fof(f663_sk,plain,
! [T_a,V_b,V_a] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_a),V_b))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_b),V_a))
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f663_nnf]) ).
cnf(c663,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X2),X1))
| ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X1),X2))
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f663_sk]) ).
cnf(f684,axiom,
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_A))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_disjoint__iff__not__equal_0) ).
fof(f684_nnf,plain,
! [T_a,V_x,V_B,V_A] :
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_A))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_B)) ),
inference(nnf_transformation,[status(thm)],[f684]) ).
fof(f684_sk,plain,
! [T_a,V_x,V_B,V_A] :
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(T_a,tc_bool)),V_A),V_B) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_A))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_B)) ),
inference(skolemisation,[status(esa)],[f684_nnf]) ).
cnf(c684,plain,
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(X0,tc_bool)),X3),X2) != c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))
| ~ hBOOL(hAPP(hAPP(c_in(X0),X1),X3))
| ~ hBOOL(hAPP(hAPP(c_in(X0),X1),X2)) ),
inference(cnf_transformation,[status(esa)],[f684_sk]) ).
cnf(f709,axiom,
( ~ hBOOL(hAPP(hAPP(c_lessequals(T_a),V_a),V_b))
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_SetInterval_Oord__class_OatLeastAtMost(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_atLeastatMost__empty__iff2_0) ).
fof(f709_nnf,plain,
! [T_a,V_a,V_b] :
( ~ hBOOL(hAPP(hAPP(c_lessequals(T_a),V_a),V_b))
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_SetInterval_Oord__class_OatLeastAtMost(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f709]) ).
fof(f709_sk,plain,
! [T_a,V_a,V_b] :
( ~ hBOOL(hAPP(hAPP(c_lessequals(T_a),V_a),V_b))
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_SetInterval_Oord__class_OatLeastAtMost(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f709_nnf]) ).
cnf(c709,plain,
( ~ hBOOL(hAPP(hAPP(c_lessequals(X0),X1),X2))
| c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_SetInterval_Oord__class_OatLeastAtMost(X1,X2,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f709_sk]) ).
cnf(f711,axiom,
( ~ hBOOL(hAPP(hAPP(c_lessequals(T_a),V_a),V_b))
| c_SetInterval_Oord__class_OatLeastAtMost(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/sandbox2/benchmark/theBenchmark.p',cls_atLeastatMost__empty__iff_0) ).
fof(f711_nnf,plain,
! [T_a,V_a,V_b] :
( ~ hBOOL(hAPP(hAPP(c_lessequals(T_a),V_a),V_b))
| c_SetInterval_Oord__class_OatLeastAtMost(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)],[f711]) ).
fof(f711_sk,plain,
! [T_a,V_a,V_b] :
( ~ hBOOL(hAPP(hAPP(c_lessequals(T_a),V_a),V_b))
| c_SetInterval_Oord__class_OatLeastAtMost(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)],[f711_nnf]) ).
cnf(c711,plain,
( ~ hBOOL(hAPP(hAPP(c_lessequals(X0),X1),X2))
| c_SetInterval_Oord__class_OatLeastAtMost(X1,X2,X0) != c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f711_sk]) ).
cnf(f761,axiom,
c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I49_J_0) ).
fof(f761_nnf,plain,
! [V_pname_H,V_com1,V_com2] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(nnf_transformation,[status(thm)],[f761]) ).
fof(f761_sk,plain,
! [V_pname_H,V_com1,V_com2] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(skolemisation,[status(esa)],[f761_nnf]) ).
cnf(c761,plain,
c_Com_Ocom_OBODY(X0) != c_Com_Ocom_OSemi(X1,X2),
inference(cnf_transformation,[status(esa)],[f761_sk]) ).
cnf(f762,axiom,
c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OBODY(V_pname_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I48_J_0) ).
fof(f762_nnf,plain,
! [V_com1,V_com2,V_pname_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OBODY(V_pname_H),
inference(nnf_transformation,[status(thm)],[f762]) ).
fof(f762_sk,plain,
! [V_com1,V_com2,V_pname_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OBODY(V_pname_H),
inference(skolemisation,[status(esa)],[f762_nnf]) ).
cnf(c762,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OBODY(X2),
inference(cnf_transformation,[status(esa)],[f762_sk]) ).
cnf(f763,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I12_J_0) ).
fof(f763_nnf,plain,
! [V_com1_H,V_com2_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
inference(nnf_transformation,[status(thm)],[f763]) ).
fof(f763_sk,plain,
! [V_com1_H,V_com2_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
inference(skolemisation,[status(esa)],[f763_nnf]) ).
cnf(c763,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(X0,X1),
inference(cnf_transformation,[status(esa)],[f763_sk]) ).
cnf(f764,axiom,
c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I13_J_0) ).
fof(f764_nnf,plain,
! [V_com1_H,V_com2_H] : c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP,
inference(nnf_transformation,[status(thm)],[f764]) ).
fof(f764_sk,plain,
! [V_com1_H,V_com2_H] : c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP,
inference(skolemisation,[status(esa)],[f764_nnf]) ).
cnf(c764,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f764_sk]) ).
cnf(f849,axiom,
~ hBOOL(hAPP(c_Finite__Set_Ofold1Set(V_f,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),V_x)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_empty__fold1SetE_0) ).
fof(f849_nnf,plain,
! [V_f,T_a,V_x] : ~ hBOOL(hAPP(c_Finite__Set_Ofold1Set(V_f,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),V_x)),
inference(nnf_transformation,[status(thm)],[f849]) ).
fof(f849_sk,plain,
! [V_f,T_a,V_x] : ~ hBOOL(hAPP(c_Finite__Set_Ofold1Set(V_f,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),V_x)),
inference(skolemisation,[status(esa)],[f849_nnf]) ).
cnf(c849,plain,
~ hBOOL(hAPP(c_Finite__Set_Ofold1Set(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),X2)),
inference(cnf_transformation,[status(esa)],[f849_sk]) ).
cnf(f871,axiom,
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool))))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),V_B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_DiffE_1) ).
fof(f871_nnf,plain,
! [T_a,V_c,V_B,V_A] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool))))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),V_B)) ),
inference(nnf_transformation,[status(thm)],[f871]) ).
fof(f871_sk,plain,
! [T_a,V_c,V_B,V_A] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool))))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),V_B)) ),
inference(skolemisation,[status(esa)],[f871_nnf]) ).
cnf(c871,plain,
( ~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_HOL_Ominus__class_Ominus(X3,X2,tc_fun(X0,tc_bool))))
| ~ hBOOL(hAPP(hAPP(c_in(X0),X1),X2)) ),
inference(cnf_transformation,[status(esa)],[f871_sk]) ).
cnf(f904,axiom,
c_Option_Ooption_ONone(T_a) != hAPP(c_Option_Ooption_OSome(T_a),V_a_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_option_Osimps_I2_J_0) ).
fof(f904_nnf,plain,
! [T_a,V_a_H] : c_Option_Ooption_ONone(T_a) != hAPP(c_Option_Ooption_OSome(T_a),V_a_H),
inference(nnf_transformation,[status(thm)],[f904]) ).
fof(f904_sk,plain,
! [T_a,V_a_H] : c_Option_Ooption_ONone(T_a) != hAPP(c_Option_Ooption_OSome(T_a),V_a_H),
inference(skolemisation,[status(esa)],[f904_nnf]) ).
cnf(c904,plain,
c_Option_Ooption_ONone(X0) != hAPP(c_Option_Ooption_OSome(X0),X1),
inference(cnf_transformation,[status(esa)],[f904_sk]) ).
cnf(f905,axiom,
c_Option_Ooption_ONone(T_a) != hAPP(c_Option_Ooption_OSome(T_a),V_y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__Some__eq_1) ).
fof(f905_nnf,plain,
! [T_a,V_y] : c_Option_Ooption_ONone(T_a) != hAPP(c_Option_Ooption_OSome(T_a),V_y),
inference(nnf_transformation,[status(thm)],[f905]) ).
fof(f905_sk,plain,
! [T_a,V_y] : c_Option_Ooption_ONone(T_a) != hAPP(c_Option_Ooption_OSome(T_a),V_y),
inference(skolemisation,[status(esa)],[f905_nnf]) ).
cnf(c905,plain,
c_Option_Ooption_ONone(X0) != hAPP(c_Option_Ooption_OSome(X0),X1),
inference(cnf_transformation,[status(esa)],[f905_sk]) ).
cnf(f923,axiom,
hAPP(c_Option_Ooption_OSome(T_a),V_a_H) != c_Option_Ooption_ONone(T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_option_Osimps_I3_J_0) ).
fof(f923_nnf,plain,
! [T_a,V_a_H] : hAPP(c_Option_Ooption_OSome(T_a),V_a_H) != c_Option_Ooption_ONone(T_a),
inference(nnf_transformation,[status(thm)],[f923]) ).
fof(f923_sk,plain,
! [T_a,V_a_H] : hAPP(c_Option_Ooption_OSome(T_a),V_a_H) != c_Option_Ooption_ONone(T_a),
inference(skolemisation,[status(esa)],[f923_nnf]) ).
cnf(c923,plain,
hAPP(c_Option_Ooption_OSome(X0),X1) != c_Option_Ooption_ONone(X0),
inference(cnf_transformation,[status(esa)],[f923_sk]) ).
cnf(f924,axiom,
hAPP(c_Option_Ooption_OSome(T_a),V_xa) != c_Option_Ooption_ONone(T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__None__eq_1) ).
fof(f924_nnf,plain,
! [T_a,V_xa] : hAPP(c_Option_Ooption_OSome(T_a),V_xa) != c_Option_Ooption_ONone(T_a),
inference(nnf_transformation,[status(thm)],[f924]) ).
fof(f924_sk,plain,
! [T_a,V_xa] : hAPP(c_Option_Ooption_OSome(T_a),V_xa) != c_Option_Ooption_ONone(T_a),
inference(skolemisation,[status(esa)],[f924_nnf]) ).
cnf(c924,plain,
hAPP(c_Option_Ooption_OSome(X0),X1) != c_Option_Ooption_ONone(X0),
inference(cnf_transformation,[status(esa)],[f924_sk]) ).
cnf(f964,axiom,
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_a),c_Map_Odom(V_m,T_a,T_b)))
| hAPP(V_m,V_a) != c_Option_Ooption_ONone(T_b) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_domIff_0) ).
fof(f964_nnf,plain,
! [V_m,V_a,T_b,T_a] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_a),c_Map_Odom(V_m,T_a,T_b)))
| hAPP(V_m,V_a) != c_Option_Ooption_ONone(T_b) ),
inference(nnf_transformation,[status(thm)],[f964]) ).
fof(f964_sk,plain,
! [V_m,V_a,T_b,T_a] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_a),c_Map_Odom(V_m,T_a,T_b)))
| hAPP(V_m,V_a) != c_Option_Ooption_ONone(T_b) ),
inference(skolemisation,[status(esa)],[f964_nnf]) ).
cnf(c964,plain,
( ~ hBOOL(hAPP(hAPP(c_in(X3),X1),c_Map_Odom(X0,X3,X2)))
| hAPP(X0,X1) != c_Option_Ooption_ONone(X2) ),
inference(cnf_transformation,[status(esa)],[f964_sk]) ).
cnf(f998,axiom,
c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I19_J_0) ).
fof(f998_nnf,plain,
! [V_pname_H] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSKIP,
inference(nnf_transformation,[status(thm)],[f998]) ).
fof(f998_sk,plain,
! [V_pname_H] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSKIP,
inference(skolemisation,[status(esa)],[f998_nnf]) ).
cnf(c998,plain,
c_Com_Ocom_OBODY(X0) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f998_sk]) ).
cnf(f1005,axiom,
~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ex__in__conv_0) ).
fof(f1005_nnf,plain,
! [T_a,V_x] : ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
inference(nnf_transformation,[status(thm)],[f1005]) ).
fof(f1005_sk,plain,
! [T_a,V_x] : ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
inference(skolemisation,[status(esa)],[f1005_nnf]) ).
cnf(c1005,plain,
~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
inference(cnf_transformation,[status(esa)],[f1005_sk]) ).
cnf(f1007,axiom,
~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_empty__iff_0) ).
fof(f1007_nnf,plain,
! [T_a,V_c] : ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
inference(nnf_transformation,[status(thm)],[f1007]) ).
fof(f1007_sk,plain,
! [T_a,V_c] : ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
inference(skolemisation,[status(esa)],[f1007_nnf]) ).
cnf(c1007,plain,
~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
inference(cnf_transformation,[status(esa)],[f1007_sk]) ).
cnf(f1008,axiom,
~ hBOOL(hAPP(hAPP(c_in(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_emptyE_0) ).
fof(f1008_nnf,plain,
! [T_a,V_a] : ~ hBOOL(hAPP(hAPP(c_in(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
inference(nnf_transformation,[status(thm)],[f1008]) ).
fof(f1008_sk,plain,
! [T_a,V_a] : ~ hBOOL(hAPP(hAPP(c_in(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
inference(skolemisation,[status(esa)],[f1008_nnf]) ).
cnf(c1008,plain,
~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
inference(cnf_transformation,[status(esa)],[f1008_sk]) ).
cnf(f1009,axiom,
c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_empty__not__insert_0) ).
fof(f1009_nnf,plain,
! [T_a,V_a,V_A] : c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A),
inference(nnf_transformation,[status(thm)],[f1009]) ).
fof(f1009_sk,plain,
! [T_a,V_a,V_A] : c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A),
inference(skolemisation,[status(esa)],[f1009_nnf]) ).
cnf(c1009,plain,
c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != hAPP(hAPP(c_Set_Oinsert(X0),X1),X2),
inference(cnf_transformation,[status(esa)],[f1009_sk]) ).
cnf(f1021,axiom,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_bot1E_0) ).
fof(f1021_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)],[f1021]) ).
fof(f1021_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)],[f1021_nnf]) ).
cnf(c1021,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f1021_sk]) ).
cnf(f1025,axiom,
hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_insert__not__empty_0) ).
fof(f1025_nnf,plain,
! [T_a,V_a,V_A] : hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f1025]) ).
fof(f1025_sk,plain,
! [T_a,V_a,V_A] : hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f1025_nnf]) ).
cnf(c1025,plain,
hAPP(hAPP(c_Set_Oinsert(X0),X1),X2) != c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),
inference(cnf_transformation,[status(esa)],[f1025_sk]) ).
cnf(f1036,axiom,
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))))
| ~ hBOOL(hAPP(V_P,V_x)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_bex__empty_0) ).
fof(f1036_nnf,plain,
! [V_P,V_x,T_a] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))))
| ~ hBOOL(hAPP(V_P,V_x)) ),
inference(nnf_transformation,[status(thm)],[f1036]) ).
fof(f1036_sk,plain,
! [V_P,V_x,T_a] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))))
| ~ hBOOL(hAPP(V_P,V_x)) ),
inference(skolemisation,[status(esa)],[f1036_nnf]) ).
cnf(c1036,plain,
( ~ hBOOL(hAPP(hAPP(c_in(X2),X1),c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool))))
| ~ hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f1036_sk]) ).
cnf(f1043,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(V_pname_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_com_Osimps_I18_J_0) ).
fof(f1043_nnf,plain,
! [V_pname_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(V_pname_H),
inference(nnf_transformation,[status(thm)],[f1043]) ).
fof(f1043_sk,plain,
! [V_pname_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(V_pname_H),
inference(skolemisation,[status(esa)],[f1043_nnf]) ).
cnf(c1043,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(X0),
inference(cnf_transformation,[status(esa)],[f1043_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c42,c95,c131,c132,c133,c135,c136,c137,c234,c236,c238,c240,c241,c293,c294,c298,c301,c351,c352,c422,c457,c458,c554,c588,c636,c659,c660,c662,c663,c684,c709,c711,c761,c762,c763,c764,c849,c871,c904,c905,c923,c924,c964,c998,c1005,c1007,c1008,c1009,c1021,c1025,c1036,c1043,c1045]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t1568]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV875-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/0.36 % Computer : n011.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 21:13:00 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 33.37/5.21 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 33.37/5.21 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------