%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV842-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 : n012.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:12 PM UTC 2026
% Result : Unsatisfiable 32.38s 4.57s
% Output : Proof 32.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 59
% Syntax : Number of formulae : 250 ( 158 unt; 0 def)
% Number of atoms : 402 ( 147 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 529 ( 377 ~; 152 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-4 aty)
% Number of functors : 37 ( 37 usr; 13 con; 0-5 aty)
% Number of variables : 656 ( 172 sgn 320 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f602,axiom,
class_Lattices_Oupper__semilattice(tc_bool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_bool__Lattices_Oupper__semilattice) ).
fof(f602_nnf,plain,
class_Lattices_Oupper__semilattice(tc_bool),
inference(nnf_transformation,[status(thm)],[f602]) ).
cnf(c602,plain,
class_Lattices_Oupper__semilattice(tc_bool),
inference(cnf_transformation,[status(esa)],[f602_nnf]) ).
cnf(t6,plain,
class_Lattices_Oupper__semilattice(tc_bool) = true,
inference(equality_encoding,[status(esa)],[c602]) ).
cnf(t2089,plain,
class_Lattices_Oupper__semilattice(tc_bool) = true,
inference(orient,[status(thm)],[t6]) ).
cnf(f591,axiom,
class_Lattices_Oupper__semilattice(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_nat__Lattices_Oupper__semilattice) ).
fof(f591_nnf,plain,
class_Lattices_Oupper__semilattice(tc_nat),
inference(nnf_transformation,[status(thm)],[f591]) ).
cnf(c591,plain,
class_Lattices_Oupper__semilattice(tc_nat),
inference(cnf_transformation,[status(esa)],[f591_nnf]) ).
cnf(t7,plain,
class_Lattices_Oupper__semilattice(tc_nat) = true,
inference(equality_encoding,[status(esa)],[c591]) ).
cnf(t2090,plain,
class_Lattices_Oupper__semilattice(tc_nat) = true,
inference(orient,[status(thm)],[t7]) ).
cnf(f569,axiom,
c_Set_Oimage(V_f,c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)),T_b,T_a) = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_image__empty_0) ).
fof(f569_nnf,plain,
! [V_f,T_b,T_a] : c_Set_Oimage(V_f,c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)),T_b,T_a) = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f569]) ).
fof(f569_sk,plain,
! [V_f,T_b,T_a] : c_Set_Oimage(V_f,c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)),T_b,T_a) = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f569_nnf]) ).
cnf(c569,plain,
c_Set_Oimage(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1,X2) = c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
inference(cnf_transformation,[status(esa)],[f569_sk]) ).
cnf(t42,plain,
c_Set_Oimage(X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2,X3) = c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)),
inference(equality_encoding,[status(esa)],[c569]) ).
cnf(t2491,plain,
c_Set_Oimage(X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2,X3) = c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)),
inference(orient,[status(thm)],[t42]) ).
cnf(f560,axiom,
c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)),T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_empty_0) ).
fof(f560_nnf,plain,
! [V_G,T_a] : c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)),T_a),
inference(nnf_transformation,[status(thm)],[f560]) ).
fof(f560_sk,plain,
! [V_G,T_a] : c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)),T_a),
inference(skolemisation,[status(esa)],[f560_nnf]) ).
cnf(c560,plain,
c_Hoare__Mirabelle_Ohoare__derivs(X0,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X1),tc_bool)),X1),
inference(cnf_transformation,[status(esa)],[f560_sk]) ).
cnf(t27,plain,
c_Hoare__Mirabelle_Ohoare__derivs(X1,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X2),tc_bool)),X2) = true,
inference(equality_encoding,[status(esa)],[c560]) ).
cnf(t2026,plain,
c_Hoare__Mirabelle_Ohoare__derivs(X1,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X2),tc_bool)),X2) = true,
inference(orient,[status(thm)],[t27]) ).
cnf(t20,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t234,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t20]) ).
cnf(f1,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_x))
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__irrefl_0) ).
fof(f1_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)],[f1]) ).
fof(f1_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)],[f1_nnf]) ).
cnf(c1,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X1),X1))
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(f2,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_x))
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__neq__iff_1) ).
fof(f2_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)],[f2]) ).
fof(f2_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)],[f2_nnf]) ).
cnf(c2,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X1),X1))
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(f3,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_x),V_x))
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__le_1) ).
fof(f3_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)],[f3]) ).
fof(f3_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)],[f3_nnf]) ).
cnf(c3,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X1),X1))
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(f5,axiom,
~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_fun(T_a,tc_bool)),V_x),V_x)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_psubset__eq_1) ).
fof(f5_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)],[f5]) ).
fof(f5_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)],[f5_nnf]) ).
cnf(c5,plain,
~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(tc_fun(X0,tc_bool)),X1),X1)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(f50,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_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(f50_nnf,plain,
! [T_a,V_a,V_b] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_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)],[f50]) ).
fof(f50_sk,plain,
! [T_a,V_a,V_b] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_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)],[f50_nnf]) ).
cnf(c50,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X1),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)],[f50_sk]) ).
cnf(f52,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_k),V_l))
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_SetInterval_Oord__class_OgreaterThanAtMost(V_k,V_l,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_greaterThanAtMost__empty__iff2_0) ).
fof(f52_nnf,plain,
! [T_a,V_k,V_l] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_k),V_l))
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_SetInterval_Oord__class_OgreaterThanAtMost(V_k,V_l,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f52]) ).
fof(f52_sk,plain,
! [T_a,V_k,V_l] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_k),V_l))
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_SetInterval_Oord__class_OgreaterThanAtMost(V_k,V_l,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f52_nnf]) ).
cnf(c52,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X1),X2))
| c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_SetInterval_Oord__class_OgreaterThanAtMost(X1,X2,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
cnf(f68,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/sandbox/benchmark/theBenchmark.p',cls_xt1_I9_J_0) ).
fof(f68_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)],[f68]) ).
fof(f68_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)],[f68_nnf]) ).
cnf(c68,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)],[f68_sk]) ).
cnf(f69,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/sandbox/benchmark/theBenchmark.p',cls_not__less__iff__gr__or__eq_1) ).
fof(f69_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)],[f69]) ).
fof(f69_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)],[f69_nnf]) ).
cnf(c69,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)],[f69_sk]) ).
cnf(f70,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/sandbox/benchmark/theBenchmark.p',cls_order__less__asym_0) ).
fof(f70_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)],[f70]) ).
fof(f70_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)],[f70_nnf]) ).
cnf(c70,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)],[f70_sk]) ).
cnf(f71,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/sandbox/benchmark/theBenchmark.p',cls_order__less__asym_H_0) ).
fof(f71_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)],[f71]) ).
fof(f71_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)],[f71_nnf]) ).
cnf(c71,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)],[f71_sk]) ).
cnf(f128,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_k),V_l))
| c_SetInterval_Oord__class_OgreaterThanAtMost(V_k,V_l,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_greaterThanAtMost__empty__iff_0) ).
fof(f128_nnf,plain,
! [T_a,V_k,V_l] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_k),V_l))
| c_SetInterval_Oord__class_OgreaterThanAtMost(V_k,V_l,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f128]) ).
fof(f128_sk,plain,
! [T_a,V_k,V_l] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_k),V_l))
| c_SetInterval_Oord__class_OgreaterThanAtMost(V_k,V_l,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f128_nnf]) ).
cnf(c128,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X1),X2))
| c_SetInterval_Oord__class_OgreaterThanAtMost(X1,X2,X0) != c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f128_sk]) ).
cnf(f138,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/sandbox/benchmark/theBenchmark.p',cls_linorder__antisym__conv2_1) ).
fof(f138_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)],[f138]) ).
fof(f138_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)],[f138_nnf]) ).
cnf(c138,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)],[f138_sk]) ).
cnf(f140,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/sandbox/benchmark/theBenchmark.p',cls_linorder__not__less_1) ).
fof(f140_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)],[f140]) ).
fof(f140_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)],[f140_nnf]) ).
cnf(c140,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)],[f140_sk]) ).
cnf(f142,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/sandbox/benchmark/theBenchmark.p',cls_linorder__not__le_1) ).
fof(f142_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)],[f142]) ).
fof(f142_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)],[f142_nnf]) ).
cnf(c142,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)],[f142_sk]) ).
cnf(f144,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/sandbox/benchmark/theBenchmark.p',cls_less__fun__def_1) ).
fof(f144_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)],[f144]) ).
fof(f144_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)],[f144_nnf]) ).
cnf(c144,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)],[f144_sk]) ).
cnf(f145,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/sandbox/benchmark/theBenchmark.p',cls_less__le__not__le_1) ).
fof(f145_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)],[f145]) ).
fof(f145_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)],[f145_nnf]) ).
cnf(c145,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)],[f145_sk]) ).
cnf(f162,axiom,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_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(f162_nnf,plain,
! [T_a,V_a,V_b] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_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)],[f162]) ).
fof(f162_sk,plain,
! [T_a,V_a,V_b] :
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(T_a),V_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)],[f162_nnf]) ).
cnf(c162,plain,
( ~ hBOOL(hAPP(hAPP(c_HOL_Oord__class_Oless(X0),X1),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)],[f162_sk]) ).
cnf(f175,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/sandbox/benchmark/theBenchmark.p',cls_not__psubset__empty_0) ).
fof(f175_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)],[f175]) ).
fof(f175_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)],[f175_nnf]) ).
cnf(c175,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)],[f175_sk]) ).
cnf(f226,axiom,
c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OBODY(V_pname_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I48_J_0) ).
fof(f226_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)],[f226]) ).
fof(f226_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)],[f226_nnf]) ).
cnf(c226,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OBODY(X2),
inference(cnf_transformation,[status(esa)],[f226_sk]) ).
cnf(f236,axiom,
c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I49_J_0) ).
fof(f236_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)],[f236]) ).
fof(f236_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)],[f236_nnf]) ).
cnf(c236,plain,
c_Com_Ocom_OBODY(X0) != c_Com_Ocom_OSemi(X1,X2),
inference(cnf_transformation,[status(esa)],[f236_sk]) ).
cnf(f247,axiom,
c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I17_J_0) ).
fof(f247_nnf,plain,
! [V_fun_H,V_com_H] : c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OSKIP,
inference(nnf_transformation,[status(thm)],[f247]) ).
fof(f247_sk,plain,
! [V_fun_H,V_com_H] : c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OSKIP,
inference(skolemisation,[status(esa)],[f247_nnf]) ).
cnf(c247,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f247_sk]) ).
cnf(f248,axiom,
c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OWhile(V_fun,V_com),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I59_J_0) ).
fof(f248_nnf,plain,
! [V_pname_H,V_fun,V_com] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OWhile(V_fun,V_com),
inference(nnf_transformation,[status(thm)],[f248]) ).
fof(f248_sk,plain,
! [V_pname_H,V_fun,V_com] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OWhile(V_fun,V_com),
inference(skolemisation,[status(esa)],[f248_nnf]) ).
cnf(c248,plain,
c_Com_Ocom_OBODY(X0) != c_Com_Ocom_OWhile(X1,X2),
inference(cnf_transformation,[status(esa)],[f248_sk]) ).
cnf(f252,axiom,
c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I46_J_0) ).
fof(f252_nnf,plain,
! [V_com1,V_com2,V_fun_H,V_com_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
inference(nnf_transformation,[status(thm)],[f252]) ).
fof(f252_sk,plain,
! [V_com1,V_com2,V_fun_H,V_com_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
inference(skolemisation,[status(esa)],[f252_nnf]) ).
cnf(c252,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OWhile(X2,X3),
inference(cnf_transformation,[status(esa)],[f252_sk]) ).
cnf(f257,axiom,
( ~ c_Fun_Oinj__on(V_f,c_Set_Oinsert(V_a,V_A,T_a),T_a,T_b)
| ~ hBOOL(c_in(hAPP(V_f,V_a),c_Set_Oimage(V_f,hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_fun(T_a,tc_bool)),V_A),c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),T_a,T_b),T_b)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_inj__on__insert_1) ).
fof(f257_nnf,plain,
! [V_f,V_a,T_a,V_A,T_b] :
( ~ c_Fun_Oinj__on(V_f,c_Set_Oinsert(V_a,V_A,T_a),T_a,T_b)
| ~ hBOOL(c_in(hAPP(V_f,V_a),c_Set_Oimage(V_f,hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_fun(T_a,tc_bool)),V_A),c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),T_a,T_b),T_b)) ),
inference(nnf_transformation,[status(thm)],[f257]) ).
fof(f257_sk,plain,
! [V_f,V_a,T_a,V_A,T_b] :
( ~ c_Fun_Oinj__on(V_f,c_Set_Oinsert(V_a,V_A,T_a),T_a,T_b)
| ~ hBOOL(c_in(hAPP(V_f,V_a),c_Set_Oimage(V_f,hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_fun(T_a,tc_bool)),V_A),c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),T_a,T_b),T_b)) ),
inference(skolemisation,[status(esa)],[f257_nnf]) ).
cnf(c257,plain,
( ~ c_Fun_Oinj__on(X0,c_Set_Oinsert(X1,X3,X2),X2,X4)
| ~ hBOOL(c_in(hAPP(X0,X1),c_Set_Oimage(X0,hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_fun(X2,tc_bool)),X3),c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2)),X2,X4),X4)) ),
inference(cnf_transformation,[status(esa)],[f257_sk]) ).
cnf(f278,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I14_J_0) ).
fof(f278_nnf,plain,
! [V_fun_H,V_com1_H,V_com2_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
inference(nnf_transformation,[status(thm)],[f278]) ).
fof(f278_sk,plain,
! [V_fun_H,V_com1_H,V_com2_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
inference(skolemisation,[status(esa)],[f278_nnf]) ).
cnf(c278,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OCond(X0,X1,X2),
inference(cnf_transformation,[status(esa)],[f278_sk]) ).
cnf(f310,axiom,
c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I15_J_0) ).
fof(f310_nnf,plain,
! [V_fun_H,V_com1_H,V_com2_H] : c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP,
inference(nnf_transformation,[status(thm)],[f310]) ).
fof(f310_sk,plain,
! [V_fun_H,V_com1_H,V_com2_H] : c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP,
inference(skolemisation,[status(esa)],[f310_nnf]) ).
cnf(c310,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f310_sk]) ).
cnf(f313,axiom,
c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I53_J_0) ).
fof(f313_nnf,plain,
! [V_fun_H,V_com_H,V_fun,V_com1,V_com2] : c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
inference(nnf_transformation,[status(thm)],[f313]) ).
fof(f313_sk,plain,
! [V_fun_H,V_com_H,V_fun,V_com1,V_com2] : c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
inference(skolemisation,[status(esa)],[f313_nnf]) ).
cnf(c313,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OCond(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f313_sk]) ).
cnf(f314,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(V_pname_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I18_J_0) ).
fof(f314_nnf,plain,
! [V_pname_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(V_pname_H),
inference(nnf_transformation,[status(thm)],[f314]) ).
fof(f314_sk,plain,
! [V_pname_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(V_pname_H),
inference(skolemisation,[status(esa)],[f314_nnf]) ).
cnf(c314,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OBODY(X0),
inference(cnf_transformation,[status(esa)],[f314_sk]) ).
cnf(f328,axiom,
( ~ hBOOL(hAPP(V_P,V_x))
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Collect(V_P,T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_empty__Collect__eq_0) ).
fof(f328_nnf,plain,
! [T_a,V_P,V_x] :
( ~ hBOOL(hAPP(V_P,V_x))
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Collect(V_P,T_a) ),
inference(nnf_transformation,[status(thm)],[f328]) ).
fof(f328_sk,plain,
! [T_a,V_P,V_x] :
( ~ hBOOL(hAPP(V_P,V_x))
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Collect(V_P,T_a) ),
inference(skolemisation,[status(esa)],[f328_nnf]) ).
cnf(c328,plain,
( ~ hBOOL(hAPP(X1,X2))
| c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Collect(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f328_sk]) ).
cnf(f329,axiom,
~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ex__in__conv_0) ).
fof(f329_nnf,plain,
! [V_x,T_a] : ~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(nnf_transformation,[status(thm)],[f329]) ).
fof(f329_sk,plain,
! [V_x,T_a] : ~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(skolemisation,[status(esa)],[f329_nnf]) ).
cnf(c329,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f329_sk]) ).
cnf(f331,axiom,
~ hBOOL(c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_empty__iff_0) ).
fof(f331_nnf,plain,
! [V_c,T_a] : ~ hBOOL(c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(nnf_transformation,[status(thm)],[f331]) ).
fof(f331_sk,plain,
! [V_c,T_a] : ~ hBOOL(c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(skolemisation,[status(esa)],[f331_nnf]) ).
cnf(c331,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f331_sk]) ).
cnf(f332,axiom,
~ hBOOL(c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_emptyE_0) ).
fof(f332_nnf,plain,
! [V_a,T_a] : ~ hBOOL(c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(nnf_transformation,[status(thm)],[f332]) ).
fof(f332_sk,plain,
! [V_a,T_a] : ~ hBOOL(c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(skolemisation,[status(esa)],[f332_nnf]) ).
cnf(c332,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f332_sk]) ).
cnf(f335,axiom,
( ~ hBOOL(hAPP(V_P,V_x))
| c_Collect(V_P,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Collect__empty__eq_0) ).
fof(f335_nnf,plain,
! [V_P,T_a,V_x] :
( ~ hBOOL(hAPP(V_P,V_x))
| c_Collect(V_P,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ),
inference(nnf_transformation,[status(thm)],[f335]) ).
fof(f335_sk,plain,
! [V_P,T_a,V_x] :
( ~ hBOOL(hAPP(V_P,V_x))
| c_Collect(V_P,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ),
inference(skolemisation,[status(esa)],[f335_nnf]) ).
cnf(c335,plain,
( ~ hBOOL(hAPP(X0,X2))
| c_Collect(X0,X1) != c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) ),
inference(cnf_transformation,[status(esa)],[f335_sk]) ).
cnf(f336,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/sandbox/benchmark/theBenchmark.p',cls_empty__fold1SetE_0) ).
fof(f336_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)],[f336]) ).
fof(f336_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)],[f336_nnf]) ).
cnf(c336,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)],[f336_sk]) ).
cnf(f337,axiom,
c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_UNIV__not__empty_0) ).
fof(f337_nnf,plain,
! [T_a] : c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f337]) ).
fof(f337_sk,plain,
! [T_a] : c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f337_nnf]) ).
cnf(c337,plain,
c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),
inference(cnf_transformation,[status(esa)],[f337_sk]) ).
cnf(f344,axiom,
( ~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(hAPP(V_P,V_x)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_bex__empty_0) ).
fof(f344_nnf,plain,
! [V_P,V_x,T_a] :
( ~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(hAPP(V_P,V_x)) ),
inference(nnf_transformation,[status(thm)],[f344]) ).
fof(f344_sk,plain,
! [V_P,V_x,T_a] :
( ~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(hAPP(V_P,V_x)) ),
inference(skolemisation,[status(esa)],[f344_nnf]) ).
cnf(c344,plain,
( ~ hBOOL(c_in(X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2))
| ~ hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f344_sk]) ).
cnf(f376,axiom,
c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I44_J_0) ).
fof(f376_nnf,plain,
! [V_com1,V_com2,V_fun_H,V_com1_H,V_com2_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
inference(nnf_transformation,[status(thm)],[f376]) ).
fof(f376_sk,plain,
! [V_com1,V_com2,V_fun_H,V_com1_H,V_com2_H] : c_Com_Ocom_OSemi(V_com1,V_com2) != c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H),
inference(skolemisation,[status(esa)],[f376_nnf]) ).
cnf(c376,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OCond(X2,X3,X4),
inference(cnf_transformation,[status(esa)],[f376_sk]) ).
cnf(f378,axiom,
c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I52_J_0) ).
fof(f378_nnf,plain,
! [V_fun,V_com1,V_com2,V_fun_H,V_com_H] : c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
inference(nnf_transformation,[status(thm)],[f378]) ).
fof(f378_sk,plain,
! [V_fun,V_com1,V_com2,V_fun_H,V_com_H] : c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
inference(skolemisation,[status(esa)],[f378_nnf]) ).
cnf(c378,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OWhile(X3,X4),
inference(cnf_transformation,[status(esa)],[f378_sk]) ).
cnf(f380,axiom,
( ~ hBOOL(c_in(V_c,hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_fun(T_a,tc_bool)),V_A),V_B),T_a))
| ~ hBOOL(c_in(V_c,V_B,T_a)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_DiffE_1) ).
fof(f380_nnf,plain,
! [V_c,V_B,T_a,V_A] :
( ~ hBOOL(c_in(V_c,hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_fun(T_a,tc_bool)),V_A),V_B),T_a))
| ~ hBOOL(c_in(V_c,V_B,T_a)) ),
inference(nnf_transformation,[status(thm)],[f380]) ).
fof(f380_sk,plain,
! [V_c,V_B,T_a,V_A] :
( ~ hBOOL(c_in(V_c,hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_fun(T_a,tc_bool)),V_A),V_B),T_a))
| ~ hBOOL(c_in(V_c,V_B,T_a)) ),
inference(skolemisation,[status(esa)],[f380_nnf]) ).
cnf(c380,plain,
( ~ hBOOL(c_in(X0,hAPP(hAPP(c_HOL_Ominus__class_Ominus(tc_fun(X2,tc_bool)),X3),X1),X2))
| ~ hBOOL(c_in(X0,X1,X2)) ),
inference(cnf_transformation,[status(esa)],[f380_sk]) ).
cnf(f384,axiom,
c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I45_J_0) ).
fof(f384_nnf,plain,
! [V_fun_H,V_com1_H,V_com2_H,V_com1,V_com2] : c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(nnf_transformation,[status(thm)],[f384]) ).
fof(f384_sk,plain,
! [V_fun_H,V_com1_H,V_com2_H,V_com1,V_com2] : c_Com_Ocom_OCond(V_fun_H,V_com1_H,V_com2_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(skolemisation,[status(esa)],[f384_nnf]) ).
cnf(c384,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OSemi(X3,X4),
inference(cnf_transformation,[status(esa)],[f384_sk]) ).
cnf(f400,axiom,
c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OBODY(V_pname_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I54_J_0) ).
fof(f400_nnf,plain,
! [V_fun,V_com1,V_com2,V_pname_H] : c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OBODY(V_pname_H),
inference(nnf_transformation,[status(thm)],[f400]) ).
fof(f400_sk,plain,
! [V_fun,V_com1,V_com2,V_pname_H] : c_Com_Ocom_OCond(V_fun,V_com1,V_com2) != c_Com_Ocom_OBODY(V_pname_H),
inference(skolemisation,[status(esa)],[f400_nnf]) ).
cnf(c400,plain,
c_Com_Ocom_OCond(X0,X1,X2) != c_Com_Ocom_OBODY(X3),
inference(cnf_transformation,[status(esa)],[f400_sk]) ).
cnf(f401,axiom,
c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I55_J_0) ).
fof(f401_nnf,plain,
! [V_pname_H,V_fun,V_com1,V_com2] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
inference(nnf_transformation,[status(thm)],[f401]) ).
fof(f401_sk,plain,
! [V_pname_H,V_fun,V_com1,V_com2] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OCond(V_fun,V_com1,V_com2),
inference(skolemisation,[status(esa)],[f401_nnf]) ).
cnf(c401,plain,
c_Com_Ocom_OBODY(X0) != c_Com_Ocom_OCond(X1,X2,X3),
inference(cnf_transformation,[status(esa)],[f401_sk]) ).
cnf(f405,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I16_J_0) ).
fof(f405_nnf,plain,
! [V_fun_H,V_com_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
inference(nnf_transformation,[status(thm)],[f405]) ).
fof(f405_sk,plain,
! [V_fun_H,V_com_H] : c_Com_Ocom_OSKIP != c_Com_Ocom_OWhile(V_fun_H,V_com_H),
inference(skolemisation,[status(esa)],[f405_nnf]) ).
cnf(c405,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OWhile(X0,X1),
inference(cnf_transformation,[status(esa)],[f405_sk]) ).
cnf(f425,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/sandbox/benchmark/theBenchmark.p',cls_atLeastatMost__empty__iff2_0) ).
fof(f425_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)],[f425]) ).
fof(f425_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)],[f425_nnf]) ).
cnf(c425,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)],[f425_sk]) ).
cnf(f431,axiom,
c_Com_Ocom_OSemi(V_com1_H,V_com2_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I13_J_0) ).
fof(f431_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)],[f431]) ).
fof(f431_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)],[f431_nnf]) ).
cnf(c431,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f431_sk]) ).
cnf(f435,axiom,
c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I47_J_0) ).
fof(f435_nnf,plain,
! [V_fun_H,V_com_H,V_com1,V_com2] : c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(nnf_transformation,[status(thm)],[f435]) ).
fof(f435_sk,plain,
! [V_fun_H,V_com_H,V_com1,V_com2] : c_Com_Ocom_OWhile(V_fun_H,V_com_H) != c_Com_Ocom_OSemi(V_com1,V_com2),
inference(skolemisation,[status(esa)],[f435_nnf]) ).
cnf(c435,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OSemi(X2,X3),
inference(cnf_transformation,[status(esa)],[f435_sk]) ).
cnf(f461,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/sandbox/benchmark/theBenchmark.p',cls_atLeastatMost__empty__iff_0) ).
fof(f461_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)],[f461]) ).
fof(f461_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)],[f461_nnf]) ).
cnf(c461,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)],[f461_sk]) ).
cnf(f462,axiom,
c_Com_Ocom_OWhile(V_fun,V_com) != c_Com_Ocom_OBODY(V_pname_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I58_J_0) ).
fof(f462_nnf,plain,
! [V_fun,V_com,V_pname_H] : c_Com_Ocom_OWhile(V_fun,V_com) != c_Com_Ocom_OBODY(V_pname_H),
inference(nnf_transformation,[status(thm)],[f462]) ).
fof(f462_sk,plain,
! [V_fun,V_com,V_pname_H] : c_Com_Ocom_OWhile(V_fun,V_com) != c_Com_Ocom_OBODY(V_pname_H),
inference(skolemisation,[status(esa)],[f462_nnf]) ).
cnf(c462,plain,
c_Com_Ocom_OWhile(X0,X1) != c_Com_Ocom_OBODY(X2),
inference(cnf_transformation,[status(esa)],[f462_sk]) ).
cnf(f463,axiom,
c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSKIP,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I19_J_0) ).
fof(f463_nnf,plain,
! [V_pname_H] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSKIP,
inference(nnf_transformation,[status(thm)],[f463]) ).
fof(f463_sk,plain,
! [V_pname_H] : c_Com_Ocom_OBODY(V_pname_H) != c_Com_Ocom_OSKIP,
inference(skolemisation,[status(esa)],[f463_nnf]) ).
cnf(c463,plain,
c_Com_Ocom_OBODY(X0) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f463_sk]) ).
cnf(f472,axiom,
c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(V_com1_H,V_com2_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_com_Osimps_I12_J_0) ).
fof(f472_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)],[f472]) ).
fof(f472_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)],[f472_nnf]) ).
cnf(c472,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(X0,X1),
inference(cnf_transformation,[status(esa)],[f472_sk]) ).
cnf(f551,axiom,
c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Set_Oinsert(V_a,V_A,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_empty__not__insert_0) ).
fof(f551_nnf,plain,
! [T_a,V_a,V_A] : c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Set_Oinsert(V_a,V_A,T_a),
inference(nnf_transformation,[status(thm)],[f551]) ).
fof(f551_sk,plain,
! [T_a,V_a,V_A] : c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Set_Oinsert(V_a,V_A,T_a),
inference(skolemisation,[status(esa)],[f551_nnf]) ).
cnf(c551,plain,
c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Set_Oinsert(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f551_sk]) ).
cnf(f559,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(f559_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)],[f559]) ).
fof(f559_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)],[f559_nnf]) ).
cnf(c559,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f559_sk]) ).
cnf(f563,axiom,
c_Set_Oinsert(V_a,V_A,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_insert__not__empty_0) ).
fof(f563_nnf,plain,
! [V_a,V_A,T_a] : c_Set_Oinsert(V_a,V_A,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f563]) ).
fof(f563_sk,plain,
! [V_a,V_A,T_a] : c_Set_Oinsert(V_a,V_A,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f563_nnf]) ).
cnf(c563,plain,
c_Set_Oinsert(X0,X1,X2) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
inference(cnf_transformation,[status(esa)],[f563_sk]) ).
cnf(f575,negated_conjecture,
~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_Set_Oimage(c_COMBS(c_COMBS(hAPP(c_COMBB(c_Hoare__Mirabelle_Otriple_Otriple(t_b),tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_bool)),tc_fun(tc_Com_Ocom,tc_fun(tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_bool)),tc_Hoare__Mirabelle_Otriple(t_b))),t_a),v_P),v_c0,t_a,tc_Com_Ocom,tc_fun(tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_bool)),tc_Hoare__Mirabelle_Otriple(t_b))),v_Q,t_a,tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_bool)),tc_Hoare__Mirabelle_Otriple(t_b)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a,tc_Hoare__Mirabelle_Otriple(t_b)),t_b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f575_nnf,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_Set_Oimage(c_COMBS(c_COMBS(hAPP(c_COMBB(c_Hoare__Mirabelle_Otriple_Otriple(t_b),tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_bool)),tc_fun(tc_Com_Ocom,tc_fun(tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_bool)),tc_Hoare__Mirabelle_Otriple(t_b))),t_a),v_P),v_c0,t_a,tc_Com_Ocom,tc_fun(tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_bool)),tc_Hoare__Mirabelle_Otriple(t_b))),v_Q,t_a,tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_bool)),tc_Hoare__Mirabelle_Otriple(t_b)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a,tc_Hoare__Mirabelle_Otriple(t_b)),t_b),
inference(nnf_transformation,[status(thm)],[f575]) ).
fof(f575_sk,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_Set_Oimage(c_COMBS(c_COMBS(hAPP(c_COMBB(c_Hoare__Mirabelle_Otriple_Otriple(t_b),tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_bool)),tc_fun(tc_Com_Ocom,tc_fun(tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_bool)),tc_Hoare__Mirabelle_Otriple(t_b))),t_a),v_P),v_c0,t_a,tc_Com_Ocom,tc_fun(tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_bool)),tc_Hoare__Mirabelle_Otriple(t_b))),v_Q,t_a,tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_bool)),tc_Hoare__Mirabelle_Otriple(t_b)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a,tc_Hoare__Mirabelle_Otriple(t_b)),t_b),
inference(skolemisation,[status(esa)],[f575_nnf]) ).
cnf(c575,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_Set_Oimage(c_COMBS(c_COMBS(hAPP(c_COMBB(c_Hoare__Mirabelle_Otriple_Otriple(t_b),tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_bool)),tc_fun(tc_Com_Ocom,tc_fun(tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_bool)),tc_Hoare__Mirabelle_Otriple(t_b))),t_a),v_P),v_c0,t_a,tc_Com_Ocom,tc_fun(tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_bool)),tc_Hoare__Mirabelle_Otriple(t_b))),v_Q,t_a,tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_bool)),tc_Hoare__Mirabelle_Otriple(t_b)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a,tc_Hoare__Mirabelle_Otriple(t_b)),t_b),
inference(cnf_transformation,[status(esa)],[f575_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c1,c2,c3,c5,c50,c52,c68,c69,c70,c71,c128,c138,c140,c142,c144,c145,c162,c175,c226,c236,c247,c248,c252,c257,c278,c310,c313,c314,c328,c329,c331,c332,c335,c336,c337,c344,c376,c378,c380,c384,c400,c401,c405,c425,c431,c435,c461,c462,c463,c472,c551,c559,c563,c575]) ).
cnf(g0_0,plain,
true != ifeq(c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_Set_Oimage(c_COMBS(c_COMBS(hAPP(c_COMBB(c_Hoare__Mirabelle_Otriple_Otriple(t_b),tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_bool)),tc_fun(tc_Com_Ocom,tc_fun(tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_bool)),tc_Hoare__Mirabelle_Otriple(t_b))),t_a),v_P),v_c0,t_a,tc_Com_Ocom,tc_fun(tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_bool)),tc_Hoare__Mirabelle_Otriple(t_b))),v_Q,t_a,tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_bool)),tc_Hoare__Mirabelle_Otriple(t_b)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a,tc_Hoare__Mirabelle_Otriple(t_b)),t_b),true,false,true),
inference(rw,[status(thm)],[goal_0]) ).
cnf(g0_1,plain,
true != ifeq(c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_Set_Oimage(c_COMBS(c_COMBS(hAPP(c_COMBB(c_Hoare__Mirabelle_Otriple_Otriple(t_b),tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_bool)),tc_fun(tc_Com_Ocom,tc_fun(tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_bool)),tc_Hoare__Mirabelle_Otriple(t_b))),t_a),v_P),v_c0,t_a,tc_Com_Ocom,tc_fun(tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_bool)),tc_Hoare__Mirabelle_Otriple(t_b))),v_Q,t_a,tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_bool)),tc_Hoare__Mirabelle_Otriple(t_b)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a,tc_Hoare__Mirabelle_Otriple(t_b)),t_b),true,false,class_Lattices_Oupper__semilattice(tc_bool)),
inference(rw,[status(thm)],[g0_0,t2089]) ).
cnf(g0_2,plain,
true != ifeq(c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_Set_Oimage(c_COMBS(c_COMBS(hAPP(c_COMBB(c_Hoare__Mirabelle_Otriple_Otriple(t_b),tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_bool)),tc_fun(tc_Com_Ocom,tc_fun(tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_bool)),tc_Hoare__Mirabelle_Otriple(t_b))),t_a),v_P),v_c0,t_a,tc_Com_Ocom,tc_fun(tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_bool)),tc_Hoare__Mirabelle_Otriple(t_b))),v_Q,t_a,tc_fun(t_b,tc_fun(tc_Com_Ostate,tc_bool)),tc_Hoare__Mirabelle_Otriple(t_b)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a,tc_Hoare__Mirabelle_Otriple(t_b)),t_b),class_Lattices_Oupper__semilattice(tc_nat),false,class_Lattices_Oupper__semilattice(tc_bool)),
inference(rw,[status(thm)],[g0_1,t2090]) ).
cnf(g0_3,plain,
true != ifeq(c_Hoare__Mirabelle_Ohoare__derivs(v_G,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_b),tc_bool)),t_b),class_Lattices_Oupper__semilattice(tc_nat),false,class_Lattices_Oupper__semilattice(tc_bool)),
inference(rw,[status(thm)],[g0_2,t2491]) ).
cnf(g0_4,plain,
true != ifeq(true,class_Lattices_Oupper__semilattice(tc_nat),false,class_Lattices_Oupper__semilattice(tc_bool)),
inference(rw,[status(thm)],[g0_3,t2026]) ).
cnf(g0_5,plain,
true != ifeq(true,class_Lattices_Oupper__semilattice(tc_nat),false,true),
inference(rw,[status(thm)],[g0_4,t2089]) ).
cnf(g0_6,plain,
true != ifeq(true,true,false,true),
inference(rw,[status(thm)],[g0_5,t2090]) ).
cnf(g0_7,plain,
true != false,
inference(rw,[status(thm)],[g0_6,t234]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_7]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWV842-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.02 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.04/0.30 % Computer : n012.cluster.edu
% 0.04/0.30 % Model : x86_64 x86_64
% 0.04/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.30 % Memory : 8046.5625MB
% 0.04/0.30 % OS : Linux 6.8.0-71-generic
% 0.04/0.30 % CPULimit : 300
% 0.04/0.30 % WCLimit : 300
% 0.04/0.30 % DateTime : Thu Sep 24 21:08:36 UTC 2026
% 0.04/0.30 % CPUTime :
% 0.04/0.30 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 32.38/4.57 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 32.38/4.57 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------