%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV898-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:26 PM UTC 2026
% Result : Unsatisfiable 41.75s 5.86s
% Output : Proof 41.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 20
% Syntax : Number of formulae : 96 ( 60 unt; 0 def)
% Number of atoms : 144 ( 52 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 165 ( 117 ~; 48 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 2 prp; 0-4 aty)
% Number of functors : 25 ( 25 usr; 8 con; 0-5 aty)
% Number of variables : 256 ( 41 sgn 102 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f570,axiom,
c_Set_Oimage(V_f,c_Set_Oimage(V_g,V_A,T_c,T_b),T_b,T_a) = c_Set_Oimage(c_COMBB(V_f,V_g,T_b,T_a,T_c),V_A,T_c,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_image__image_0) ).
fof(f570_nnf,plain,
! [V_f,V_g,V_A,T_c,T_b,T_a] : c_Set_Oimage(V_f,c_Set_Oimage(V_g,V_A,T_c,T_b),T_b,T_a) = c_Set_Oimage(c_COMBB(V_f,V_g,T_b,T_a,T_c),V_A,T_c,T_a),
inference(nnf_transformation,[status(thm)],[f570]) ).
fof(f570_sk,plain,
! [V_f,V_g,V_A,T_c,T_b,T_a] : c_Set_Oimage(V_f,c_Set_Oimage(V_g,V_A,T_c,T_b),T_b,T_a) = c_Set_Oimage(c_COMBB(V_f,V_g,T_b,T_a,T_c),V_A,T_c,T_a),
inference(skolemisation,[status(esa)],[f570_nnf]) ).
cnf(c570,plain,
c_Set_Oimage(X0,c_Set_Oimage(X1,X2,X3,X4),X4,X5) = c_Set_Oimage(c_COMBB(X0,X1,X4,X5,X3),X2,X3,X5),
inference(cnf_transformation,[status(esa)],[f570_sk]) ).
cnf(t63,plain,
c_Set_Oimage(c_COMBB(X1,X2,X3,X4,X5),X6,X5,X4) = c_Set_Oimage(X1,c_Set_Oimage(X2,X6,X5,X3),X3,X4),
inference(equality_encoding,[status(esa)],[c570]) ).
cnf(t895,plain,
c_Set_Oimage(X1,c_Set_Oimage(X2,X3,X4,X5),X5,X6) = c_Set_Oimage(c_COMBB(X1,X2,X5,X6,X4),X3,X4,X6),
inference(orient,[status(thm)],[t63]) ).
cnf(f571,axiom,
( ~ c_Finite__Set_Ofinite(V_F,T_a)
| c_Finite__Set_Ofinite(c_Set_Oimage(V_h,V_F,T_a,T_b),T_b) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_finite__imageI_0) ).
fof(f571_nnf,plain,
! [V_h,V_F,T_a,T_b] :
( ~ c_Finite__Set_Ofinite(V_F,T_a)
| c_Finite__Set_Ofinite(c_Set_Oimage(V_h,V_F,T_a,T_b),T_b) ),
inference(nnf_transformation,[status(thm)],[f571]) ).
fof(f571_sk,plain,
! [V_h,V_F,T_a,T_b] :
( ~ c_Finite__Set_Ofinite(V_F,T_a)
| c_Finite__Set_Ofinite(c_Set_Oimage(V_h,V_F,T_a,T_b),T_b) ),
inference(skolemisation,[status(esa)],[f571_nnf]) ).
cnf(c571,plain,
( ~ c_Finite__Set_Ofinite(X1,X2)
| c_Finite__Set_Ofinite(c_Set_Oimage(X0,X1,X2,X3),X3) ),
inference(cnf_transformation,[status(esa)],[f571_sk]) ).
cnf(t45,plain,
ifeq(c_Finite__Set_Ofinite(X1,X2),true,c_Finite__Set_Ofinite(c_Set_Oimage(X3,X1,X2,X4),X4),true) = true,
inference(equality_encoding,[status(esa)],[c571]) ).
cnf(t182,plain,
ifeq(c_Finite__Set_Ofinite(X1,X2),true,c_Finite__Set_Ofinite(c_Set_Oimage(X3,X1,X2,X4),X4),true) = true,
inference(orient,[status(thm)],[t45]) ).
cnf(f555,axiom,
c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_finite__dom__body_0) ).
fof(f555_nnf,plain,
c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname),
inference(nnf_transformation,[status(thm)],[f555]) ).
cnf(c555,plain,
c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname),
inference(cnf_transformation,[status(esa)],[f555_nnf]) ).
cnf(t9,plain,
c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname) = true,
inference(equality_encoding,[status(esa)],[c555]) ).
cnf(t667,plain,
c_Finite__Set_Ofinite(c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname) = true,
inference(orient,[status(thm)],[t9]) ).
cnf(t670,plain,
true = ifeq(true,true,c_Finite__Set_Ofinite(c_Set_Oimage(X1,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,X2),X2),true),
inference(cp,[status(thm)],[t182,t667]) ).
cnf(t7,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t121,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t7]) ).
cnf(t10824,plain,
true = c_Finite__Set_Ofinite(c_Set_Oimage(X1,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,X2),X2),
inference(step,[status(thm)],[t670,t121]) ).
cnf(t1114,plain,
c_Finite__Set_Ofinite(c_Set_Oimage(X1,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,X2),X2) = true,
inference(orient,[status(thm)],[t10824]) ).
cnf(t1115,plain,
true = c_Finite__Set_Ofinite(c_Set_Oimage(X1,c_Set_Oimage(X2,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,X3),X3,X4),X4),
inference(cp,[status(thm)],[t1114,t895]) ).
cnf(t2217,plain,
c_Finite__Set_Ofinite(c_Set_Oimage(X1,c_Set_Oimage(X2,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,X3),X3,X4),X4) = true,
inference(orient,[status(thm)],[t1115]) ).
cnf(t2218,plain,
true = c_Finite__Set_Ofinite(c_Set_Oimage(X1,c_Set_Oimage(X2,c_Set_Oimage(X3,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,X4),X4,X5),X5,X6),X6),
inference(cp,[status(thm)],[t2217,t895]) ).
cnf(t10788,plain,
c_Finite__Set_Ofinite(c_Set_Oimage(X1,c_Set_Oimage(X2,c_Set_Oimage(X3,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,X4),X4,X5),X5,X6),X6) = true,
inference(orient,[status(thm)],[t2218]) ).
cnf(f73,axiom,
( ~ c_in(V_c,c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool)),T_a)
| ~ c_in(V_c,V_A,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ComplD_0) ).
fof(f73_nnf,plain,
! [V_c,V_A,T_a] :
( ~ c_in(V_c,c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool)),T_a)
| ~ c_in(V_c,V_A,T_a) ),
inference(nnf_transformation,[status(thm)],[f73]) ).
fof(f73_sk,plain,
! [V_c,V_A,T_a] :
( ~ c_in(V_c,c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool)),T_a)
| ~ c_in(V_c,V_A,T_a) ),
inference(skolemisation,[status(esa)],[f73_nnf]) ).
cnf(c73,plain,
( ~ c_in(X0,c_HOL_Ouminus__class_Ouminus(X1,tc_fun(X2,tc_bool)),X2)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f73_sk]) ).
cnf(f82,axiom,
( ~ 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(f82_nnf,plain,
! [V_P,V_x,T_a] :
( ~ 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)],[f82]) ).
fof(f82_sk,plain,
! [V_P,V_x,T_a] :
( ~ 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)],[f82_nnf]) ).
cnf(c82,plain,
( ~ c_in(X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2)
| ~ hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f82_sk]) ).
cnf(f151,axiom,
( ~ c_Fun_Oinj__on(V_f,c_Set_Oinsert(V_a,V_A,T_a),T_a,T_b)
| ~ c_in(hAPP(V_f,V_a),c_Set_Oimage(V_f,c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a,T_b),T_b) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_inj__on__insert_1) ).
fof(f151_nnf,plain,
! [V_f,V_a,V_A,T_a,T_b] :
( ~ c_Fun_Oinj__on(V_f,c_Set_Oinsert(V_a,V_A,T_a),T_a,T_b)
| ~ c_in(hAPP(V_f,V_a),c_Set_Oimage(V_f,c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a,T_b),T_b) ),
inference(nnf_transformation,[status(thm)],[f151]) ).
fof(f151_sk,plain,
! [V_f,V_a,V_A,T_a,T_b] :
( ~ c_Fun_Oinj__on(V_f,c_Set_Oinsert(V_a,V_A,T_a),T_a,T_b)
| ~ c_in(hAPP(V_f,V_a),c_Set_Oimage(V_f,c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a,T_b),T_b) ),
inference(skolemisation,[status(esa)],[f151_nnf]) ).
cnf(c151,plain,
( ~ c_Fun_Oinj__on(X0,c_Set_Oinsert(X1,X2,X3),X3,X4)
| ~ c_in(hAPP(X0,X1),c_Set_Oimage(X0,c_HOL_Ominus__class_Ominus(X2,c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)),X3),tc_fun(X3,tc_bool)),X3,X4),X4) ),
inference(cnf_transformation,[status(esa)],[f151_sk]) ).
cnf(f196,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(f196_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)],[f196]) ).
fof(f196_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)],[f196_nnf]) ).
cnf(c196,plain,
c_Set_Oinsert(X0,X1,X2) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
inference(cnf_transformation,[status(esa)],[f196_sk]) ).
cnf(f211,axiom,
( ~ c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)
| ~ c_in(V_c,V_B,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_DiffE_1) ).
fof(f211_nnf,plain,
! [V_c,V_B,T_a,V_A] :
( ~ c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)
| ~ c_in(V_c,V_B,T_a) ),
inference(nnf_transformation,[status(thm)],[f211]) ).
fof(f211_sk,plain,
! [V_c,V_B,T_a,V_A] :
( ~ c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)
| ~ c_in(V_c,V_B,T_a) ),
inference(skolemisation,[status(esa)],[f211_nnf]) ).
cnf(c211,plain,
( ~ c_in(X0,c_HOL_Ominus__class_Ominus(X3,X1,tc_fun(X2,tc_bool)),X2)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f211_sk]) ).
cnf(f272,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(f272_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)],[f272]) ).
fof(f272_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)],[f272_nnf]) ).
cnf(c272,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f272_sk]) ).
cnf(f275,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/sandbox2/benchmark/theBenchmark.p',cls_UNIV__not__empty_0) ).
fof(f275_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)],[f275]) ).
fof(f275_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)],[f275_nnf]) ).
cnf(c275,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)],[f275_sk]) ).
cnf(f277,axiom,
( c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,tc_fun(T_a,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ c_in(V_x,V_A,T_a)
| ~ c_in(V_x,V_B,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_disjoint__iff__not__equal_0) ).
fof(f277_nnf,plain,
! [V_x,V_B,T_a,V_A] :
( c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,tc_fun(T_a,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ c_in(V_x,V_A,T_a)
| ~ c_in(V_x,V_B,T_a) ),
inference(nnf_transformation,[status(thm)],[f277]) ).
fof(f277_sk,plain,
! [V_x,V_B,T_a,V_A] :
( c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,tc_fun(T_a,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ c_in(V_x,V_A,T_a)
| ~ c_in(V_x,V_B,T_a) ),
inference(skolemisation,[status(esa)],[f277_nnf]) ).
cnf(c277,plain,
( c_Lattices_Olower__semilattice__class_Oinf(X3,X1,tc_fun(X2,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool))
| ~ c_in(X0,X3,X2)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f277_sk]) ).
cnf(f411,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(f411_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)],[f411]) ).
fof(f411_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)],[f411_nnf]) ).
cnf(c411,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)],[f411_sk]) ).
cnf(f412,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(f412_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)],[f412]) ).
fof(f412_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)],[f412_nnf]) ).
cnf(c412,plain,
c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Set_Oinsert(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f412_sk]) ).
cnf(f414,axiom,
~ 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(f414_nnf,plain,
! [V_a,T_a] : ~ c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(nnf_transformation,[status(thm)],[f414]) ).
fof(f414_sk,plain,
! [V_a,T_a] : ~ c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(skolemisation,[status(esa)],[f414_nnf]) ).
cnf(c414,plain,
~ c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),
inference(cnf_transformation,[status(esa)],[f414_sk]) ).
cnf(f415,axiom,
~ 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(f415_nnf,plain,
! [V_c,T_a] : ~ c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(nnf_transformation,[status(thm)],[f415]) ).
fof(f415_sk,plain,
! [V_c,T_a] : ~ c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(skolemisation,[status(esa)],[f415_nnf]) ).
cnf(c415,plain,
~ c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),
inference(cnf_transformation,[status(esa)],[f415_sk]) ).
cnf(f417,axiom,
~ 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(f417_nnf,plain,
! [V_x,T_a] : ~ c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(nnf_transformation,[status(thm)],[f417]) ).
fof(f417_sk,plain,
! [V_x,T_a] : ~ c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(skolemisation,[status(esa)],[f417_nnf]) ).
cnf(c417,plain,
~ c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),
inference(cnf_transformation,[status(esa)],[f417_sk]) ).
cnf(f452,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(f452_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)],[f452]) ).
fof(f452_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)],[f452_nnf]) ).
cnf(c452,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)],[f452_sk]) ).
cnf(f515,axiom,
( ~ c_Hoare__Mirabelle_Ostate__not__singleton
| v_sko__Hoare__Mirabelle__Xsingle__stateE__1(V_t) != V_t ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_single__stateE_0) ).
fof(f515_nnf,plain,
! [V_t] :
( ~ c_Hoare__Mirabelle_Ostate__not__singleton
| v_sko__Hoare__Mirabelle__Xsingle__stateE__1(V_t) != V_t ),
inference(nnf_transformation,[status(thm)],[f515]) ).
fof(f515_sk,plain,
! [V_t] :
( ~ c_Hoare__Mirabelle_Ostate__not__singleton
| v_sko__Hoare__Mirabelle__Xsingle__stateE__1(V_t) != V_t ),
inference(skolemisation,[status(esa)],[f515_nnf]) ).
cnf(c515,plain,
( ~ c_Hoare__Mirabelle_Ostate__not__singleton
| v_sko__Hoare__Mirabelle__Xsingle__stateE__1(X0) != X0 ),
inference(cnf_transformation,[status(esa)],[f515_sk]) ).
cnf(f585,negated_conjecture,
~ c_Finite__Set_Ofinite(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f585_nnf,plain,
~ c_Finite__Set_Ofinite(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
inference(nnf_transformation,[status(thm)],[f585]) ).
fof(f585_sk,plain,
~ c_Finite__Set_Ofinite(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
inference(skolemisation,[status(esa)],[f585_nnf]) ).
cnf(c585,plain,
~ c_Finite__Set_Ofinite(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),
inference(cnf_transformation,[status(esa)],[f585_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c73,c82,c151,c196,c211,c272,c275,c277,c411,c412,c414,c415,c417,c452,c515,c585]) ).
cnf(g0_0,plain,
c_Finite__Set_Ofinite(c_Set_Oimage(c_COMBB(c_Hoare__Mirabelle_OMGT,c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate),tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)) != false,
inference(rw,[status(thm)],[goal_0]) ).
cnf(g0_1,plain,
c_Finite__Set_Ofinite(c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_COMBB(c_Option_Othe(tc_Com_Ocom),c_Com_Obody,tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom,tc_Com_Opname),c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)) != false,
inference(rw,[status(thm)],[g0_0,t895]) ).
cnf(g0_2,plain,
c_Finite__Set_Ofinite(c_Set_Oimage(c_Hoare__Mirabelle_OMGT,c_Set_Oimage(c_Option_Othe(tc_Com_Ocom),c_Set_Oimage(c_Com_Obody,c_Map_Odom(c_Com_Obody,tc_Com_Opname,tc_Com_Ocom),tc_Com_Opname,tc_Option_Ooption(tc_Com_Ocom)),tc_Option_Ooption(tc_Com_Ocom),tc_Com_Ocom),tc_Com_Ocom,tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)),tc_Hoare__Mirabelle_Otriple(tc_Com_Ostate)) != false,
inference(rw,[status(thm)],[g0_1,t895]) ).
cnf(g0_3,plain,
true != false,
inference(rw,[status(thm)],[g0_2,t10788]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV898-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.18/0.44 % Computer : n014.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Thu Sep 24 21:15:47 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.44 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 41.75/5.86 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 41.75/5.86 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------