%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV836-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 : n014.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:10 PM UTC 2026
% Result : Unsatisfiable 27.16s 4.00s
% Output : Proof 27.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 38
% Syntax : Number of formulae : 165 ( 65 unt; 0 def)
% Number of atoms : 333 ( 62 equ)
% Maximal formula atoms : 3 ( 2 avg)
% Number of connectives : 474 ( 306 ~; 168 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 22 ( 22 usr; 7 con; 0-4 aty)
% Number of variables : 398 ( 36 sgn 192 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f510,axiom,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(V_t,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(T_a)),T_a)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a)
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(V_t,V_ts,tc_Hoare__Mirabelle_Otriple(T_a)),T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_hoare__derivs_Oinsert_0) ).
fof(f510_nnf,plain,
! [V_G,V_t,V_ts,T_a] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(V_t,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(T_a)),T_a)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a)
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(V_t,V_ts,tc_Hoare__Mirabelle_Otriple(T_a)),T_a) ),
inference(nnf_transformation,[status(thm)],[f510]) ).
fof(f510_sk,plain,
! [V_G,V_t,V_ts,T_a] :
( ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(V_t,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(T_a)),T_a)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a)
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,c_Set_Oinsert(V_t,V_ts,tc_Hoare__Mirabelle_Otriple(T_a)),T_a) ),
inference(skolemisation,[status(esa)],[f510_nnf]) ).
cnf(c510,plain,
( ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_bool)),tc_Hoare__Mirabelle_Otriple(X3)),X3)
| ~ c_Hoare__Mirabelle_Ohoare__derivs(X0,X2,X3)
| c_Hoare__Mirabelle_Ohoare__derivs(X0,c_Set_Oinsert(X1,X2,tc_Hoare__Mirabelle_Otriple(X3)),X3) ),
inference(cnf_transformation,[status(esa)],[f510_sk]) ).
cnf(t182,plain,
ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X1,X2,X3),true,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X1,c_Set_Oinsert(X4,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_bool)),tc_Hoare__Mirabelle_Otriple(X3)),X3),true,c_Hoare__Mirabelle_Ohoare__derivs(X1,c_Set_Oinsert(X4,X2,tc_Hoare__Mirabelle_Otriple(X3)),X3),true),true) = true,
inference(equality_encoding,[status(esa)],[c510]) ).
cnf(t2784,plain,
ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X1,X2,X3),true,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(X1,c_Set_Oinsert(X4,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_bool)),tc_Hoare__Mirabelle_Otriple(X3)),X3),true,c_Hoare__Mirabelle_Ohoare__derivs(X1,c_Set_Oinsert(X4,X2,tc_Hoare__Mirabelle_Otriple(X3)),X3),true),true) = true,
inference(orient,[status(thm)],[t182]) ).
cnf(f557,negated_conjecture,
~ c_Hoare__Mirabelle_Ohoare__derivs(v_Ga,c_Set_Oinsert(v_t,v_tsa,tc_Hoare__Mirabelle_Otriple(t_a)),t_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_5) ).
fof(f557_nnf,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(v_Ga,c_Set_Oinsert(v_t,v_tsa,tc_Hoare__Mirabelle_Otriple(t_a)),t_a),
inference(nnf_transformation,[status(thm)],[f557]) ).
fof(f557_sk,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(v_Ga,c_Set_Oinsert(v_t,v_tsa,tc_Hoare__Mirabelle_Otriple(t_a)),t_a),
inference(skolemisation,[status(esa)],[f557_nnf]) ).
cnf(c557,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(v_Ga,c_Set_Oinsert(v_t,v_tsa,tc_Hoare__Mirabelle_Otriple(t_a)),t_a),
inference(cnf_transformation,[status(esa)],[f557_sk]) ).
cnf(t23,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_Ga,c_Set_Oinsert(v_t,v_tsa,tc_Hoare__Mirabelle_Otriple(t_a)),t_a) = false,
inference(equality_encoding,[status(esa)],[c557]) ).
cnf(t3541,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_Ga,c_Set_Oinsert(v_t,v_tsa,tc_Hoare__Mirabelle_Otriple(t_a)),t_a) = false,
inference(orient,[status(thm)],[t23]) ).
cnf(t3549,plain,
true = ifeq(c_Hoare__Mirabelle_Ohoare__derivs(v_Ga,v_tsa,t_a),true,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(v_Ga,c_Set_Oinsert(v_t,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a),true,false,true),true),
inference(cp,[status(thm)],[t2784,t3541]) ).
cnf(f556,negated_conjecture,
c_Hoare__Mirabelle_Ohoare__derivs(v_Ga,v_tsa,t_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f556_nnf,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_Ga,v_tsa,t_a),
inference(nnf_transformation,[status(thm)],[f556]) ).
cnf(c556,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_Ga,v_tsa,t_a),
inference(cnf_transformation,[status(esa)],[f556_nnf]) ).
cnf(t4,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_Ga,v_tsa,t_a) = true,
inference(equality_encoding,[status(esa)],[c556]) ).
cnf(t3152,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_Ga,v_tsa,t_a) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(t3597,plain,
true = ifeq(true,true,ifeq(c_Hoare__Mirabelle_Ohoare__derivs(v_Ga,c_Set_Oinsert(v_t,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a),true,false,true),true),
inference(step,[status(thm)],[t3549,t3152]) ).
cnf(t9,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t225,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t9]) ).
cnf(t3598,plain,
true = ifeq(c_Hoare__Mirabelle_Ohoare__derivs(v_Ga,c_Set_Oinsert(v_t,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a),true,false,true),
inference(step,[status(thm)],[t3597,t225]) ).
cnf(f555,negated_conjecture,
c_Hoare__Mirabelle_Ohoare__derivs(v_Ga,c_Set_Oinsert(v_t,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f555_nnf,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_Ga,c_Set_Oinsert(v_t,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a),
inference(nnf_transformation,[status(thm)],[f555]) ).
cnf(c555,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_Ga,c_Set_Oinsert(v_t,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a),
inference(cnf_transformation,[status(esa)],[f555_nnf]) ).
cnf(t57,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_Ga,c_Set_Oinsert(v_t,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a) = true,
inference(equality_encoding,[status(esa)],[c555]) ).
cnf(t3143,plain,
c_Hoare__Mirabelle_Ohoare__derivs(v_Ga,c_Set_Oinsert(v_t,c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),tc_Hoare__Mirabelle_Otriple(t_a)),t_a) = true,
inference(orient,[status(thm)],[t57]) ).
cnf(t3599,plain,
true = ifeq(true,true,false,true),
inference(step,[status(thm)],[t3598,t3143]) ).
cnf(t3600,plain,
true = false,
inference(step,[status(thm)],[t3599,t225]) ).
cnf(t3560,plain,
false = true,
inference(orient,[status(thm)],[t3600]) ).
cnf(f14,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(c_in(V_x,V_A,T_a))
| ~ hBOOL(c_in(V_x,V_B,T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_disjoint__iff__not__equal_0) ).
fof(f14_nnf,plain,
! [V_x,V_B,T_a,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(c_in(V_x,V_A,T_a))
| ~ hBOOL(c_in(V_x,V_B,T_a)) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [V_x,V_B,T_a,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(c_in(V_x,V_A,T_a))
| ~ hBOOL(c_in(V_x,V_B,T_a)) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( hAPP(hAPP(c_Lattices_Olower__semilattice__class_Oinf(tc_fun(X2,tc_bool)),X3),X1) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool))
| ~ hBOOL(c_in(X0,X3,X2))
| ~ hBOOL(c_in(X0,X1,X2)) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(f176,axiom,
( ~ c_HOL_Oord__class_Oless(V_f,V_g,tc_fun(T_a,T_b))
| ~ c_lessequals(V_g,V_f,tc_fun(T_a,T_b))
| ~ class_HOL_Oord(T_b) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_less__fun__def_1) ).
fof(f176_nnf,plain,
! [T_b,V_g,V_f,T_a] :
( ~ c_HOL_Oord__class_Oless(V_f,V_g,tc_fun(T_a,T_b))
| ~ c_lessequals(V_g,V_f,tc_fun(T_a,T_b))
| ~ class_HOL_Oord(T_b) ),
inference(nnf_transformation,[status(thm)],[f176]) ).
fof(f176_sk,plain,
! [T_b,V_g,V_f,T_a] :
( ~ c_HOL_Oord__class_Oless(V_f,V_g,tc_fun(T_a,T_b))
| ~ c_lessequals(V_g,V_f,tc_fun(T_a,T_b))
| ~ class_HOL_Oord(T_b) ),
inference(skolemisation,[status(esa)],[f176_nnf]) ).
cnf(c176,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,tc_fun(X3,X0))
| ~ c_lessequals(X1,X2,tc_fun(X3,X0))
| ~ class_HOL_Oord(X0) ),
inference(cnf_transformation,[status(esa)],[f176_sk]) ).
cnf(f179,axiom,
~ c_HOL_Oord__class_Oless(V_A,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__psubset__empty_0) ).
fof(f179_nnf,plain,
! [V_A,T_a] : ~ c_HOL_Oord__class_Oless(V_A,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f179]) ).
fof(f179_sk,plain,
! [V_A,T_a] : ~ c_HOL_Oord__class_Oless(V_A,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f179_nnf]) ).
cnf(c179,plain,
~ c_HOL_Oord__class_Oless(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),tc_fun(X1,tc_bool)),
inference(cnf_transformation,[status(esa)],[f179_sk]) ).
cnf(f180,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_less__le__not__le_1) ).
fof(f180_nnf,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f180]) ).
fof(f180_sk,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_lessequals(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f180_nnf]) ).
cnf(c180,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f180_sk]) ).
cnf(f182,axiom,
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__not__le_1) ).
fof(f182_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f182]) ).
fof(f182_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_lessequals(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f182_nnf]) ).
cnf(c182,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f182_sk]) ).
cnf(f184,axiom,
( ~ c_lessequals(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__not__less_1) ).
fof(f184_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_lessequals(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f184]) ).
fof(f184_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_lessequals(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f184_nnf]) ).
cnf(c184,plain,
( ~ c_lessequals(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f184_sk]) ).
cnf(f186,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__antisym__conv2_1) ).
fof(f186_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f186]) ).
fof(f186_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ c_lessequals(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f186_nnf]) ).
cnf(c186,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ c_lessequals(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f186_sk]) ).
cnf(f216,axiom,
~ c_HOL_Oord__class_Oless(V_x,V_x,tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_psubset__eq_1) ).
fof(f216_nnf,plain,
! [V_x,T_a] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f216]) ).
fof(f216_sk,plain,
! [V_x,T_a] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f216_nnf]) ).
cnf(c216,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_fun(X1,tc_bool)),
inference(cnf_transformation,[status(esa)],[f216_sk]) ).
cnf(f217,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__le_1) ).
fof(f217_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f217]) ).
fof(f217_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f217_nnf]) ).
cnf(c217,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f217_sk]) ).
cnf(f218,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_linorder__neq__iff_1) ).
fof(f218_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f218]) ).
fof(f218_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f218_nnf]) ).
cnf(c218,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f218_sk]) ).
cnf(f219,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__irrefl_0) ).
fof(f219_nnf,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f219]) ).
fof(f219_sk,plain,
! [T_a,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f219_nnf]) ).
cnf(c219,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f219_sk]) ).
cnf(f229,axiom,
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_xt1_I9_J_0) ).
fof(f229_nnf,plain,
! [T_a,V_a,V_b] :
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f229]) ).
fof(f229_sk,plain,
! [T_a,V_a,V_b] :
( ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f229_nnf]) ).
cnf(c229,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f229_sk]) ).
cnf(f230,axiom,
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_not__less__iff__gr__or__eq_1) ).
fof(f230_nnf,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f230]) ).
fof(f230_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f230_nnf]) ).
cnf(c230,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f230_sk]) ).
cnf(f231,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__asym_0) ).
fof(f231_nnf,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f231]) ).
fof(f231_sk,plain,
! [T_a,V_y,V_x] :
( ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a)
| ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f231_nnf]) ).
cnf(c231,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f231_sk]) ).
cnf(f232,axiom,
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_order__less__asym_H_0) ).
fof(f232_nnf,plain,
! [T_a,V_b,V_a] :
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f232]) ).
fof(f232_sk,plain,
! [T_a,V_b,V_a] :
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f232_nnf]) ).
cnf(c232,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f232_sk]) ).
cnf(f241,axiom,
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| 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/sandbox2/benchmark/theBenchmark.p',cls_atLeastLessThan__empty__iff2_0) ).
fof(f241_nnf,plain,
! [T_a,V_a,V_b] :
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| 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)],[f241]) ).
fof(f241_sk,plain,
! [T_a,V_a,V_b] :
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| 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)],[f241_nnf]) ).
cnf(c241,plain,
( ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| 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)],[f241_sk]) ).
cnf(f243,axiom,
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| 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/sandbox2/benchmark/theBenchmark.p',cls_atLeastLessThan__empty__iff_0) ).
fof(f243_nnf,plain,
! [T_a,V_a,V_b] :
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| 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)],[f243]) ).
fof(f243_sk,plain,
! [T_a,V_a,V_b] :
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| 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)],[f243_nnf]) ).
cnf(c243,plain,
( ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| 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)],[f243_sk]) ).
cnf(f247,axiom,
( ~ c_HOL_Oord__class_Oless(V_k,V_l,T_a)
| 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/sandbox2/benchmark/theBenchmark.p',cls_greaterThanAtMost__empty__iff_0) ).
fof(f247_nnf,plain,
! [T_a,V_k,V_l] :
( ~ c_HOL_Oord__class_Oless(V_k,V_l,T_a)
| 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)],[f247]) ).
fof(f247_sk,plain,
! [T_a,V_k,V_l] :
( ~ c_HOL_Oord__class_Oless(V_k,V_l,T_a)
| 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)],[f247_nnf]) ).
cnf(c247,plain,
( ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| 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)],[f247_sk]) ).
cnf(f249,axiom,
( ~ c_HOL_Oord__class_Oless(V_k,V_l,T_a)
| 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/sandbox2/benchmark/theBenchmark.p',cls_greaterThanAtMost__empty__iff2_0) ).
fof(f249_nnf,plain,
! [T_a,V_k,V_l] :
( ~ c_HOL_Oord__class_Oless(V_k,V_l,T_a)
| 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)],[f249]) ).
fof(f249_sk,plain,
! [T_a,V_k,V_l] :
( ~ c_HOL_Oord__class_Oless(V_k,V_l,T_a)
| 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)],[f249_nnf]) ).
cnf(c249,plain,
( ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| 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)],[f249_sk]) ).
cnf(f295,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/sandbox2/benchmark/theBenchmark.p',cls_empty__Collect__eq_0) ).
fof(f295_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)],[f295]) ).
fof(f295_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)],[f295_nnf]) ).
cnf(c295,plain,
( ~ hBOOL(hAPP(X1,X2))
| c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Collect(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f295_sk]) ).
cnf(f296,axiom,
~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ex__in__conv_0) ).
fof(f296_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)],[f296]) ).
fof(f296_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)],[f296_nnf]) ).
cnf(c296,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f296_sk]) ).
cnf(f298,axiom,
~ hBOOL(c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_empty__iff_0) ).
fof(f298_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)],[f298]) ).
fof(f298_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)],[f298_nnf]) ).
cnf(c298,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f298_sk]) ).
cnf(f299,axiom,
~ hBOOL(c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_emptyE_0) ).
fof(f299_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)],[f299]) ).
fof(f299_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)],[f299_nnf]) ).
cnf(c299,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f299_sk]) ).
cnf(f300,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/sandbox2/benchmark/theBenchmark.p',cls_Collect__empty__eq_0) ).
fof(f300_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)],[f300]) ).
fof(f300_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)],[f300_nnf]) ).
cnf(c300,plain,
( ~ hBOOL(hAPP(X0,X2))
| c_Collect(X0,X1) != c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) ),
inference(cnf_transformation,[status(esa)],[f300_sk]) ).
cnf(f301,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(f301_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)],[f301]) ).
fof(f301_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)],[f301_nnf]) ).
cnf(c301,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)],[f301_sk]) ).
cnf(f307,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/sandbox2/benchmark/theBenchmark.p',cls_bex__empty_0) ).
fof(f307_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)],[f307]) ).
fof(f307_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)],[f307_nnf]) ).
cnf(c307,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)],[f307_sk]) ).
cnf(f349,axiom,
( ~ c_lessequals(V_a,V_b,T_a)
| 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(f349_nnf,plain,
! [T_a,V_a,V_b] :
( ~ c_lessequals(V_a,V_b,T_a)
| 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)],[f349]) ).
fof(f349_sk,plain,
! [T_a,V_a,V_b] :
( ~ c_lessequals(V_a,V_b,T_a)
| 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)],[f349_nnf]) ).
cnf(c349,plain,
( ~ c_lessequals(X1,X2,X0)
| 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)],[f349_sk]) ).
cnf(f351,axiom,
( ~ c_lessequals(V_a,V_b,T_a)
| 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(f351_nnf,plain,
! [T_a,V_a,V_b] :
( ~ c_lessequals(V_a,V_b,T_a)
| 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)],[f351]) ).
fof(f351_sk,plain,
! [T_a,V_a,V_b] :
( ~ c_lessequals(V_a,V_b,T_a)
| 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)],[f351_nnf]) ).
cnf(c351,plain,
( ~ c_lessequals(X1,X2,X0)
| 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)],[f351_sk]) ).
cnf(f405,axiom,
( ~ hBOOL(c_in(V_c,c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(c_in(V_c,V_A,T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ComplD_0) ).
fof(f405_nnf,plain,
! [V_c,V_A,T_a] :
( ~ hBOOL(c_in(V_c,c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(c_in(V_c,V_A,T_a)) ),
inference(nnf_transformation,[status(thm)],[f405]) ).
fof(f405_sk,plain,
! [V_c,V_A,T_a] :
( ~ hBOOL(c_in(V_c,c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(c_in(V_c,V_A,T_a)) ),
inference(skolemisation,[status(esa)],[f405_nnf]) ).
cnf(c405,plain,
( ~ hBOOL(c_in(X0,c_HOL_Ouminus__class_Ouminus(X1,tc_fun(X2,tc_bool)),X2))
| ~ hBOOL(c_in(X0,X1,X2)) ),
inference(cnf_transformation,[status(esa)],[f405_sk]) ).
cnf(f414,axiom,
( ~ hBOOL(c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(c_in(V_c,V_B,T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_DiffE_1) ).
fof(f414_nnf,plain,
! [V_c,V_B,T_a,V_A] :
( ~ hBOOL(c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(c_in(V_c,V_B,T_a)) ),
inference(nnf_transformation,[status(thm)],[f414]) ).
fof(f414_sk,plain,
! [V_c,V_B,T_a,V_A] :
( ~ hBOOL(c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(c_in(V_c,V_B,T_a)) ),
inference(skolemisation,[status(esa)],[f414_nnf]) ).
cnf(c414,plain,
( ~ hBOOL(c_in(X0,c_HOL_Ominus__class_Ominus(X3,X1,tc_fun(X2,tc_bool)),X2))
| ~ hBOOL(c_in(X0,X1,X2)) ),
inference(cnf_transformation,[status(esa)],[f414_sk]) ).
cnf(f524,axiom,
c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Set_Oinsert(V_a,V_A,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_empty__not__insert_0) ).
fof(f524_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)],[f524]) ).
fof(f524_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)],[f524_nnf]) ).
cnf(c524,plain,
c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Set_Oinsert(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f524_sk]) ).
cnf(f536,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(f536_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)],[f536]) ).
fof(f536_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)],[f536_nnf]) ).
cnf(c536,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f536_sk]) ).
cnf(f541,axiom,
c_Set_Oinsert(V_a,V_A,T_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(f541_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)],[f541]) ).
fof(f541_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)],[f541_nnf]) ).
cnf(c541,plain,
c_Set_Oinsert(X0,X1,X2) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
inference(cnf_transformation,[status(esa)],[f541_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c14,c176,c179,c180,c182,c184,c186,c216,c217,c218,c219,c229,c230,c231,c232,c241,c243,c247,c249,c295,c296,c298,c299,c300,c301,c307,c349,c351,c405,c414,c524,c536,c541,c557]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t3560]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV836-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 : n014.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:08:33 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 27.16/4.00 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 27.16/4.00 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------