%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV913-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 : n026.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:30 PM UTC 2026
% Result : Unsatisfiable 16.04s 2.44s
% Output : Proof 16.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 30
% Syntax : Number of formulae : 131 ( 59 unt; 0 def)
% Number of atoms : 239 ( 58 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 326 ( 218 ~; 108 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-4 aty)
% Number of functors : 21 ( 21 usr; 6 con; 0-4 aty)
% Number of variables : 402 ( 73 sgn 190 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f494,negated_conjecture,
~ c_Hoare__Mirabelle_Ohoare__derivs(hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),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_conjecture_0) ).
fof(f494_nnf,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a),
inference(nnf_transformation,[status(thm)],[f494]) ).
fof(f494_sk,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a),
inference(skolemisation,[status(esa)],[f494_nnf]) ).
cnf(c494,plain,
~ c_Hoare__Mirabelle_Ohoare__derivs(hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a),
inference(cnf_transformation,[status(esa)],[f494_sk]) ).
cnf(t123,plain,
c_Hoare__Mirabelle_Ohoare__derivs(hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),hAPP(hAPP(c_Set_Oinsert(tc_Hoare__Mirabelle_Otriple(t_a)),v_t),c_Orderings_Obot__class_Obot(tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool))),t_a) = false,
inference(equality_encoding,[status(esa)],[c494]) ).
cnf(f430,axiom,
( ~ c_lessequals(V_ts,V_G,tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool))
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_asm_0) ).
fof(f430_nnf,plain,
! [V_G,V_ts,T_a] :
( ~ c_lessequals(V_ts,V_G,tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool))
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a) ),
inference(nnf_transformation,[status(thm)],[f430]) ).
fof(f430_sk,plain,
! [V_G,V_ts,T_a] :
( ~ c_lessequals(V_ts,V_G,tc_fun(tc_Hoare__Mirabelle_Otriple(T_a),tc_bool))
| c_Hoare__Mirabelle_Ohoare__derivs(V_G,V_ts,T_a) ),
inference(skolemisation,[status(esa)],[f430_nnf]) ).
cnf(c430,plain,
( ~ c_lessequals(X1,X0,tc_fun(tc_Hoare__Mirabelle_Otriple(X2),tc_bool))
| c_Hoare__Mirabelle_Ohoare__derivs(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f430_sk]) ).
cnf(t53,plain,
ifeq(c_lessequals(X1,X2,tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_bool)),true,c_Hoare__Mirabelle_Ohoare__derivs(X2,X1,X3),true) = true,
inference(equality_encoding,[status(esa)],[c430]) ).
cnf(t421,plain,
ifeq(c_lessequals(X1,X2,tc_fun(tc_Hoare__Mirabelle_Otriple(X3),tc_bool)),true,c_Hoare__Mirabelle_Ohoare__derivs(X2,X1,X3),true) = true,
inference(orient,[status(thm)],[t53]) ).
cnf(f344,axiom,
c_lessequals(V_x,V_x,tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_equalityE_0) ).
fof(f344_nnf,plain,
! [V_x,T_a] : c_lessequals(V_x,V_x,tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f344]) ).
fof(f344_sk,plain,
! [V_x,T_a] : c_lessequals(V_x,V_x,tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f344_nnf]) ).
cnf(c344,plain,
c_lessequals(X0,X0,tc_fun(X1,tc_bool)),
inference(cnf_transformation,[status(esa)],[f344_sk]) ).
cnf(t6,plain,
c_lessequals(X1,X1,tc_fun(X2,tc_bool)) = true,
inference(equality_encoding,[status(esa)],[c344]) ).
cnf(t214,plain,
c_lessequals(X1,X1,tc_fun(X2,tc_bool)) = true,
inference(orient,[status(thm)],[t6]) ).
cnf(t423,plain,
true = ifeq(true,true,c_Hoare__Mirabelle_Ohoare__derivs(X1,X1,X2),true),
inference(cp,[status(thm)],[t421,t214]) ).
cnf(t5,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t212,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t5]) ).
cnf(t6303,plain,
true = c_Hoare__Mirabelle_Ohoare__derivs(X1,X1,X2),
inference(step,[status(thm)],[t423,t212]) ).
cnf(t430,plain,
c_Hoare__Mirabelle_Ohoare__derivs(X1,X1,X2) = true,
inference(orient,[status(thm)],[t6303]) ).
cnf(t6616,plain,
true = false,
inference(step,[status(thm)],[t123,t430]) ).
cnf(t6040,plain,
false = true,
inference(orient,[status(thm)],[t6616]) ).
cnf(f17,axiom,
( ~ c_Orderings_Oorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order_Oless__le_1) ).
fof(f17_nnf,plain,
! [V_less,V_x,V_less__eq,T_a] :
( ~ c_Orderings_Oorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x)) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [V_less,V_x,V_less__eq,T_a] :
( ~ c_Orderings_Oorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x)) ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c17,plain,
( ~ c_Orderings_Oorder(X2,X0,X3)
| ~ hBOOL(hAPP(hAPP(X0,X1),X1)) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(f34,axiom,
( ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a)
| ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder_Oneq__iff_1) ).
fof(f34_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)],[f34]) ).
fof(f34_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)],[f34_nnf]) ).
cnf(c34,plain,
( ~ c_Orderings_Olinorder(X2,X0,X3)
| ~ hBOOL(hAPP(hAPP(X0,X1),X1)) ),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(f35,axiom,
( ~ hBOOL(hAPP(hAPP(V_less,V_x),V_x))
| ~ c_Orderings_Olinorder(V_less__eq,V_less,T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder_Onot__less__iff__gr__or__eq_2) ).
fof(f35_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)],[f35]) ).
fof(f35_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)],[f35_nnf]) ).
cnf(c35,plain,
( ~ hBOOL(hAPP(hAPP(X1,X3),X3))
| ~ c_Orderings_Olinorder(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(f110,axiom,
( ~ hBOOL(hAPP(hAPP(V_less__eq,V_a),V_b))
| ~ c_Orderings_Oorder(V_less__eq,V_less,T_a)
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_SetInterval_Oord_OatLeastAtMost(V_less__eq,V_a,V_b,T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order_OatLeastatMost__empty__iff2_0) ).
fof(f110_nnf,plain,
! [T_a,V_less__eq,V_a,V_b,V_less] :
( ~ hBOOL(hAPP(hAPP(V_less__eq,V_a),V_b))
| ~ c_Orderings_Oorder(V_less__eq,V_less,T_a)
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_SetInterval_Oord_OatLeastAtMost(V_less__eq,V_a,V_b,T_a) ),
inference(nnf_transformation,[status(thm)],[f110]) ).
fof(f110_sk,plain,
! [T_a,V_less__eq,V_a,V_b,V_less] :
( ~ hBOOL(hAPP(hAPP(V_less__eq,V_a),V_b))
| ~ c_Orderings_Oorder(V_less__eq,V_less,T_a)
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_SetInterval_Oord_OatLeastAtMost(V_less__eq,V_a,V_b,T_a) ),
inference(skolemisation,[status(esa)],[f110_nnf]) ).
cnf(c110,plain,
( ~ hBOOL(hAPP(hAPP(X1,X2),X3))
| ~ c_Orderings_Oorder(X1,X4,X0)
| c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_SetInterval_Oord_OatLeastAtMost(X1,X2,X3,X0) ),
inference(cnf_transformation,[status(esa)],[f110_sk]) ).
cnf(f115,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/sandbox/benchmark/theBenchmark.p',cls_DiffE_1) ).
fof(f115_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)],[f115]) ).
fof(f115_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)],[f115_nnf]) ).
cnf(c115,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)],[f115_sk]) ).
cnf(f150,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/sandbox/benchmark/theBenchmark.p',cls_disjoint__iff__not__equal_0) ).
fof(f150_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)],[f150]) ).
fof(f150_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)],[f150_nnf]) ).
cnf(c150,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)],[f150_sk]) ).
cnf(f172,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/sandbox/benchmark/theBenchmark.p',cls_linorder_Onot__less__iff__gr__or__eq_1) ).
fof(f172_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)],[f172]) ).
fof(f172_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)],[f172_nnf]) ).
cnf(c172,plain,
( ~ c_Orderings_Olinorder(X3,X0,X4)
| ~ hBOOL(hAPP(hAPP(X0,X2),X1))
| ~ hBOOL(hAPP(hAPP(X0,X1),X2)) ),
inference(cnf_transformation,[status(esa)],[f172_sk]) ).
cnf(f173,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/sandbox/benchmark/theBenchmark.p',cls_linorder_OleD_0) ).
fof(f173_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)],[f173]) ).
fof(f173_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)],[f173_nnf]) ).
cnf(c173,plain,
( ~ c_Orderings_Olinorder(X3,X0,X4)
| ~ hBOOL(hAPP(hAPP(X3,X2),X1))
| ~ hBOOL(hAPP(hAPP(X0,X1),X2)) ),
inference(cnf_transformation,[status(esa)],[f173_sk]) ).
cnf(f177,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/sandbox/benchmark/theBenchmark.p',cls_linorder_Onot__le_1) ).
fof(f177_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)],[f177]) ).
fof(f177_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)],[f177_nnf]) ).
cnf(c177,plain,
( ~ c_Orderings_Olinorder(X0,X3,X4)
| ~ hBOOL(hAPP(hAPP(X3,X2),X1))
| ~ hBOOL(hAPP(hAPP(X0,X1),X2)) ),
inference(cnf_transformation,[status(esa)],[f177_sk]) ).
cnf(f180,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/sandbox/benchmark/theBenchmark.p',cls_linorder_Oantisym__conv2_1) ).
fof(f180_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)],[f180]) ).
fof(f180_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)],[f180_nnf]) ).
cnf(c180,plain,
( ~ hBOOL(hAPP(hAPP(X2,X1),X1))
| ~ c_Orderings_Olinorder(X0,X2,X3)
| ~ hBOOL(hAPP(hAPP(X0,X1),X1)) ),
inference(cnf_transformation,[status(esa)],[f180_sk]) ).
cnf(f192,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/sandbox/benchmark/theBenchmark.p',cls_atLeastatMost__empty__iff2_0) ).
fof(f192_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)],[f192]) ).
fof(f192_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)],[f192_nnf]) ).
cnf(c192,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)],[f192_sk]) ).
cnf(f232,axiom,
( ~ c_Fun_Oinj__on(V_f,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A),T_a,T_b)
| ~ hBOOL(c_in(hAPP(V_f,V_a),hAPP(c_Set_Oimage(V_f,T_a,T_b),c_HOL_Ominus__class_Ominus(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),tc_fun(T_a,tc_bool))),T_b)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_inj__on__insert_1) ).
fof(f232_nnf,plain,
! [V_f,V_a,T_a,T_b,V_A] :
( ~ c_Fun_Oinj__on(V_f,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A),T_a,T_b)
| ~ hBOOL(c_in(hAPP(V_f,V_a),hAPP(c_Set_Oimage(V_f,T_a,T_b),c_HOL_Ominus__class_Ominus(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),tc_fun(T_a,tc_bool))),T_b)) ),
inference(nnf_transformation,[status(thm)],[f232]) ).
fof(f232_sk,plain,
! [V_f,V_a,T_a,T_b,V_A] :
( ~ c_Fun_Oinj__on(V_f,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),V_A),T_a,T_b)
| ~ hBOOL(c_in(hAPP(V_f,V_a),hAPP(c_Set_Oimage(V_f,T_a,T_b),c_HOL_Ominus__class_Ominus(V_A,hAPP(hAPP(c_Set_Oinsert(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),tc_fun(T_a,tc_bool))),T_b)) ),
inference(skolemisation,[status(esa)],[f232_nnf]) ).
cnf(c232,plain,
( ~ c_Fun_Oinj__on(X0,hAPP(hAPP(c_Set_Oinsert(X2),X1),X4),X2,X3)
| ~ hBOOL(c_in(hAPP(X0,X1),hAPP(c_Set_Oimage(X0,X2,X3),c_HOL_Ominus__class_Ominus(X4,hAPP(hAPP(c_Set_Oinsert(X2),X1),c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool))),tc_fun(X2,tc_bool))),X3)) ),
inference(cnf_transformation,[status(esa)],[f232_sk]) ).
cnf(f264,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(f264_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)],[f264]) ).
fof(f264_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)],[f264_nnf]) ).
cnf(c264,plain,
( ~ hBOOL(hAPP(X1,X2))
| c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Collect(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f264_sk]) ).
cnf(f265,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(f265_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)],[f265]) ).
fof(f265_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)],[f265_nnf]) ).
cnf(c265,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f265_sk]) ).
cnf(f267,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(f267_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)],[f267]) ).
fof(f267_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)],[f267_nnf]) ).
cnf(c267,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f267_sk]) ).
cnf(f268,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(f268_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)],[f268]) ).
fof(f268_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)],[f268_nnf]) ).
cnf(c268,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f268_sk]) ).
cnf(f271,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(f271_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)],[f271]) ).
fof(f271_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)],[f271_nnf]) ).
cnf(c271,plain,
( ~ hBOOL(hAPP(X0,X2))
| c_Collect(X0,X1) != c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) ),
inference(cnf_transformation,[status(esa)],[f271_sk]) ).
cnf(f272,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(f272_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)],[f272]) ).
fof(f272_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)],[f272_nnf]) ).
cnf(c272,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)],[f272_sk]) ).
cnf(f285,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(f285_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)],[f285]) ).
fof(f285_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)],[f285_nnf]) ).
cnf(c285,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)],[f285_sk]) ).
cnf(f308,axiom,
( ~ hBOOL(hAPP(hAPP(V_less__eq,V_a),V_b))
| ~ c_Orderings_Oorder(V_less__eq,V_less,T_a)
| c_SetInterval_Oord_OatLeastAtMost(V_less__eq,V_a,V_b,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order_OatLeastatMost__empty__iff_0) ).
fof(f308_nnf,plain,
! [V_less__eq,V_a,V_b,T_a,V_less] :
( ~ hBOOL(hAPP(hAPP(V_less__eq,V_a),V_b))
| ~ c_Orderings_Oorder(V_less__eq,V_less,T_a)
| c_SetInterval_Oord_OatLeastAtMost(V_less__eq,V_a,V_b,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ),
inference(nnf_transformation,[status(thm)],[f308]) ).
fof(f308_sk,plain,
! [V_less__eq,V_a,V_b,T_a,V_less] :
( ~ hBOOL(hAPP(hAPP(V_less__eq,V_a),V_b))
| ~ c_Orderings_Oorder(V_less__eq,V_less,T_a)
| c_SetInterval_Oord_OatLeastAtMost(V_less__eq,V_a,V_b,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ),
inference(skolemisation,[status(esa)],[f308_nnf]) ).
cnf(c308,plain,
( ~ hBOOL(hAPP(hAPP(X0,X1),X2))
| ~ c_Orderings_Oorder(X0,X4,X3)
| c_SetInterval_Oord_OatLeastAtMost(X0,X1,X2,X3) != c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)) ),
inference(cnf_transformation,[status(esa)],[f308_sk]) ).
cnf(f309,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(f309_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)],[f309]) ).
fof(f309_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)],[f309_nnf]) ).
cnf(c309,plain,
c_Com_Ocom_OSemi(X0,X1) != c_Com_Ocom_OSKIP,
inference(cnf_transformation,[status(esa)],[f309_sk]) ).
cnf(f360,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/sandbox/benchmark/theBenchmark.p',cls_atLeastatMost__empty__iff_0) ).
fof(f360_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)],[f360]) ).
fof(f360_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)],[f360_nnf]) ).
cnf(c360,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)],[f360_sk]) ).
cnf(f392,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(f392_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)],[f392]) ).
fof(f392_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)],[f392_nnf]) ).
cnf(c392,plain,
c_Com_Ocom_OSKIP != c_Com_Ocom_OSemi(X0,X1),
inference(cnf_transformation,[status(esa)],[f392_sk]) ).
cnf(f479,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/sandbox/benchmark/theBenchmark.p',cls_empty__not__insert_0) ).
fof(f479_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)],[f479]) ).
fof(f479_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)],[f479_nnf]) ).
cnf(c479,plain,
c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != hAPP(hAPP(c_Set_Oinsert(X0),X1),X2),
inference(cnf_transformation,[status(esa)],[f479_sk]) ).
cnf(f484,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(f484_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)],[f484]) ).
fof(f484_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)],[f484_nnf]) ).
cnf(c484,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f484_sk]) ).
cnf(f488,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/sandbox/benchmark/theBenchmark.p',cls_insert__not__empty_0) ).
fof(f488_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)],[f488]) ).
fof(f488_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)],[f488_nnf]) ).
cnf(c488,plain,
hAPP(hAPP(c_Set_Oinsert(X0),X1),X2) != c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),
inference(cnf_transformation,[status(esa)],[f488_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c17,c34,c35,c110,c115,c150,c172,c173,c177,c180,c192,c232,c264,c265,c267,c268,c271,c272,c285,c308,c309,c360,c392,c479,c484,c488,c494]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t6040]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV913-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n026.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 21:20:09 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 16.04/2.44 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.04/2.44 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------