%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV880-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:14:23 PM UTC 2026
% Result : Unsatisfiable 28.30s 4.41s
% Output : Proof 28.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 32
% Syntax : Number of formulae : 153 ( 81 unt; 0 def)
% Number of atoms : 269 ( 49 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 338 ( 222 ~; 116 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-4 aty)
% Number of functors : 18 ( 18 usr; 9 con; 0-4 aty)
% Number of variables : 350 ( 32 sgn 158 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f410,axiom,
( ~ c_in(V_x,V_B,T_a)
| ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| c_lessequals(c_Set_Oinsert(V_x,V_A,T_a),V_B,tc_fun(T_a,tc_bool)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_insert__subset_2) ).
fof(f410_nnf,plain,
! [V_x,V_A,T_a,V_B] :
( ~ c_in(V_x,V_B,T_a)
| ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| c_lessequals(c_Set_Oinsert(V_x,V_A,T_a),V_B,tc_fun(T_a,tc_bool)) ),
inference(nnf_transformation,[status(thm)],[f410]) ).
fof(f410_sk,plain,
! [V_x,V_A,T_a,V_B] :
( ~ c_in(V_x,V_B,T_a)
| ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| c_lessequals(c_Set_Oinsert(V_x,V_A,T_a),V_B,tc_fun(T_a,tc_bool)) ),
inference(skolemisation,[status(esa)],[f410_nnf]) ).
cnf(c410,plain,
( ~ c_in(X0,X3,X2)
| ~ c_lessequals(X1,X3,tc_fun(X2,tc_bool))
| c_lessequals(c_Set_Oinsert(X0,X1,X2),X3,tc_fun(X2,tc_bool)) ),
inference(cnf_transformation,[status(esa)],[f410_sk]) ).
cnf(t164,plain,
ifeq(c_lessequals(X1,X2,tc_fun(X3,tc_bool)),true,ifeq(c_in(X4,X2,X3),true,c_lessequals(c_Set_Oinsert(X4,X1,X3),X2,tc_fun(X3,tc_bool)),true),true) = true,
inference(equality_encoding,[status(esa)],[c410]) ).
cnf(t303,plain,
ifeq(c_lessequals(X1,X2,tc_fun(X3,tc_bool)),true,ifeq(c_in(X4,X2,X3),true,c_lessequals(c_Set_Oinsert(X4,X1,X3),X2,tc_fun(X3,tc_bool)),true),true) = true,
inference(orient,[status(thm)],[t164]) ).
cnf(f477,negated_conjecture,
~ c_lessequals(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a),c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f477_nnf,plain,
~ c_lessequals(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a),c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f477]) ).
fof(f477_sk,plain,
~ c_lessequals(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a),c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool)),
inference(skolemisation,[status(esa)],[f477_nnf]) ).
cnf(c477,plain,
~ c_lessequals(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a),c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool)),
inference(cnf_transformation,[status(esa)],[f477_sk]) ).
cnf(t89,plain,
c_lessequals(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a),c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool)) = false,
inference(equality_encoding,[status(esa)],[c477]) ).
cnf(t2069,plain,
c_lessequals(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a),c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool)) = false,
inference(orient,[status(thm)],[t89]) ).
cnf(f475,negated_conjecture,
v_G = c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f475_nnf,plain,
v_G = c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),
inference(nnf_transformation,[status(thm)],[f475]) ).
cnf(c475,plain,
v_G = c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),
inference(cnf_transformation,[status(esa)],[f475_nnf]) ).
cnf(t7,plain,
c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a) = v_G,
inference(equality_encoding,[status(esa)],[c475]) ).
cnf(t2294,plain,
c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a) = v_G,
inference(orient,[status(thm)],[t7]) ).
cnf(t5370,plain,
c_lessequals(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a),v_G,tc_fun(t_a,tc_bool)) = false,
inference(step,[status(thm)],[t2069,t2294]) ).
cnf(t2335,plain,
c_lessequals(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a),v_G,tc_fun(t_a,tc_bool)) = false,
inference(rw,[status(thm)],[t5370]) ).
cnf(t5253,plain,
c_lessequals(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a),v_G,tc_fun(t_a,tc_bool)) = false,
inference(orient,[status(thm)],[t2335]) ).
cnf(t5274,plain,
true = ifeq(c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),v_G,tc_fun(t_a,tc_bool)),true,ifeq(c_in(hAPP(v_mgt__call,v_pn),v_G,t_a),true,false,true),true),
inference(cp,[status(thm)],[t303,t5253]) ).
cnf(f440,axiom,
c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_A,tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_empty__subsetI_0) ).
fof(f440_nnf,plain,
! [T_a,V_A] : c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_A,tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f440]) ).
fof(f440_sk,plain,
! [T_a,V_A] : c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_A,tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f440_nnf]) ).
cnf(c440,plain,
c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1,tc_fun(X0,tc_bool)),
inference(cnf_transformation,[status(esa)],[f440_sk]) ).
cnf(t28,plain,
c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X2,tc_fun(X1,tc_bool)) = true,
inference(equality_encoding,[status(esa)],[c440]) ).
cnf(t779,plain,
c_lessequals(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X2,tc_fun(X1,tc_bool)) = true,
inference(orient,[status(thm)],[t28]) ).
cnf(t5545,plain,
true = ifeq(true,true,ifeq(c_in(hAPP(v_mgt__call,v_pn),v_G,t_a),true,false,true),true),
inference(step,[status(thm)],[t5274,t779]) ).
cnf(t8,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t216,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t8]) ).
cnf(t5546,plain,
true = ifeq(c_in(hAPP(v_mgt__call,v_pn),v_G,t_a),true,false,true),
inference(step,[status(thm)],[t5545,t216]) ).
cnf(f469,axiom,
( c_in(hAPP(V_f,V_x),c_Set_Oimage(V_f,V_A,T_aa,T_a),T_a)
| ~ c_in(V_x,V_A,T_aa) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rev__image__eqI_0) ).
fof(f469_nnf,plain,
! [V_x,V_A,T_aa,V_f,T_a] :
( c_in(hAPP(V_f,V_x),c_Set_Oimage(V_f,V_A,T_aa,T_a),T_a)
| ~ c_in(V_x,V_A,T_aa) ),
inference(nnf_transformation,[status(thm)],[f469]) ).
fof(f469_sk,plain,
! [V_x,V_A,T_aa,V_f,T_a] :
( c_in(hAPP(V_f,V_x),c_Set_Oimage(V_f,V_A,T_aa,T_a),T_a)
| ~ c_in(V_x,V_A,T_aa) ),
inference(skolemisation,[status(esa)],[f469_nnf]) ).
cnf(c469,plain,
( c_in(hAPP(X3,X0),c_Set_Oimage(X3,X1,X2,X4),X4)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f469_sk]) ).
cnf(t82,plain,
ifeq(c_in(X1,X2,X3),true,c_in(hAPP(X4,X1),c_Set_Oimage(X4,X2,X3,X5),X5),true) = true,
inference(equality_encoding,[status(esa)],[c469]) ).
cnf(t369,plain,
ifeq(c_in(X1,X2,X3),true,c_in(hAPP(X4,X1),c_Set_Oimage(X4,X2,X3,X5),X5),true) = true,
inference(orient,[status(thm)],[t82]) ).
cnf(f476,negated_conjecture,
c_in(v_pn,v_U,tc_Com_Opname),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f476_nnf,plain,
c_in(v_pn,v_U,tc_Com_Opname),
inference(nnf_transformation,[status(thm)],[f476]) ).
cnf(c476,plain,
c_in(v_pn,v_U,tc_Com_Opname),
inference(cnf_transformation,[status(esa)],[f476_nnf]) ).
cnf(t6,plain,
c_in(v_pn,v_U,tc_Com_Opname) = true,
inference(equality_encoding,[status(esa)],[c476]) ).
cnf(t1153,plain,
c_in(v_pn,v_U,tc_Com_Opname) = true,
inference(orient,[status(thm)],[t6]) ).
cnf(t1156,plain,
true = ifeq(true,true,c_in(hAPP(X1,v_pn),c_Set_Oimage(X1,v_U,tc_Com_Opname,X2),X2),true),
inference(cp,[status(thm)],[t369,t1153]) ).
cnf(t5419,plain,
true = c_in(hAPP(X1,v_pn),c_Set_Oimage(X1,v_U,tc_Com_Opname,X2),X2),
inference(step,[status(thm)],[t1156,t216]) ).
cnf(t3159,plain,
c_in(hAPP(X1,v_pn),c_Set_Oimage(X1,v_U,tc_Com_Opname,X2),X2) = true,
inference(orient,[status(thm)],[t5419]) ).
cnf(t3166,plain,
true = c_in(hAPP(v_mgt__call,v_pn),v_G,t_a),
inference(cp,[status(thm)],[t3159,t2294]) ).
cnf(t3209,plain,
c_in(hAPP(v_mgt__call,v_pn),v_G,t_a) = true,
inference(orient,[status(thm)],[t3166]) ).
cnf(t5547,plain,
true = ifeq(true,true,false,true),
inference(step,[status(thm)],[t5546,t3209]) ).
cnf(t5548,plain,
true = false,
inference(step,[status(thm)],[t5547,t216]) ).
cnf(t5302,plain,
false = true,
inference(orient,[status(thm)],[t5548]) ).
cnf(f97,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(f97_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)],[f97]) ).
fof(f97_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)],[f97_nnf]) ).
cnf(c97,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_fun(X1,tc_bool)),
inference(cnf_transformation,[status(esa)],[f97_sk]) ).
cnf(f98,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(f98_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)],[f98]) ).
fof(f98_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)],[f98_nnf]) ).
cnf(c98,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f98_sk]) ).
cnf(f99,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(f99_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)],[f99]) ).
fof(f99_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)],[f99_nnf]) ).
cnf(c99,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f99_sk]) ).
cnf(f100,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(f100_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)],[f100]) ).
fof(f100_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)],[f100_nnf]) ).
cnf(c100,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f100_sk]) ).
cnf(f135,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(f135_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)],[f135]) ).
fof(f135_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)],[f135_nnf]) ).
cnf(c135,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)],[f135_sk]) ).
cnf(f136,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(f136_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)],[f136]) ).
fof(f136_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)],[f136_nnf]) ).
cnf(c136,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)],[f136_sk]) ).
cnf(f137,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(f137_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)],[f137]) ).
fof(f137_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)],[f137_nnf]) ).
cnf(c137,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)],[f137_sk]) ).
cnf(f138,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(f138_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)],[f138]) ).
fof(f138_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)],[f138_nnf]) ).
cnf(c138,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)],[f138_sk]) ).
cnf(f140,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))
| ~ 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(f140_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))
| ~ c_in(V_x,V_A,T_a)
| ~ c_in(V_x,V_B,T_a) ),
inference(nnf_transformation,[status(thm)],[f140]) ).
fof(f140_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))
| ~ c_in(V_x,V_A,T_a)
| ~ c_in(V_x,V_B,T_a) ),
inference(skolemisation,[status(esa)],[f140_nnf]) ).
cnf(c140,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))
| ~ c_in(X0,X3,X2)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f140_sk]) ).
cnf(f224,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(f224_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)],[f224]) ).
fof(f224_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)],[f224_nnf]) ).
cnf(c224,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ c_lessequals(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f224_sk]) ).
cnf(f226,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(f226_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)],[f226]) ).
fof(f226_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)],[f226_nnf]) ).
cnf(c226,plain,
( ~ c_lessequals(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f226_sk]) ).
cnf(f228,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(f228_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)],[f228]) ).
fof(f228_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)],[f228_nnf]) ).
cnf(c228,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f228_sk]) ).
cnf(f230,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(f230_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)],[f230]) ).
fof(f230_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)],[f230_nnf]) ).
cnf(c230,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f230_sk]) ).
cnf(f247,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(f247_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)],[f247]) ).
fof(f247_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)],[f247_nnf]) ).
cnf(c247,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)],[f247_sk]) ).
cnf(f248,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(f248_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)],[f248]) ).
fof(f248_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)],[f248_nnf]) ).
cnf(c248,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)],[f248_sk]) ).
cnf(f257,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(f257_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)],[f257]) ).
fof(f257_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)],[f257_nnf]) ).
cnf(c257,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)],[f257_sk]) ).
cnf(f342,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(f342_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)],[f342]) ).
fof(f342_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)],[f342_nnf]) ).
cnf(c342,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)],[f342_sk]) ).
cnf(f368,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(f368_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)],[f368]) ).
fof(f368_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)],[f368_nnf]) ).
cnf(c368,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)],[f368_sk]) ).
cnf(f413,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(f413_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)],[f413]) ).
fof(f413_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)],[f413_nnf]) ).
cnf(c413,plain,
~ c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),
inference(cnf_transformation,[status(esa)],[f413_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(f416,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(f416_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)],[f416]) ).
fof(f416_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)],[f416_nnf]) ).
cnf(c416,plain,
~ c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),
inference(cnf_transformation,[status(esa)],[f416_sk]) ).
cnf(f417,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(f417_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)],[f417]) ).
fof(f417_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)],[f417_nnf]) ).
cnf(c417,plain,
c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Set_Oinsert(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f417_sk]) ).
cnf(f431,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(f431_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)],[f431]) ).
fof(f431_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)],[f431_nnf]) ).
cnf(c431,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f431_sk]) ).
cnf(f438,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(f438_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)],[f438]) ).
fof(f438_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)],[f438_nnf]) ).
cnf(c438,plain,
c_Set_Oinsert(X0,X1,X2) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
inference(cnf_transformation,[status(esa)],[f438_sk]) ).
cnf(f456,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(f456_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)],[f456]) ).
fof(f456_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)],[f456_nnf]) ).
cnf(c456,plain,
( ~ c_in(X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2)
| ~ hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f456_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c97,c98,c99,c100,c135,c136,c137,c138,c140,c224,c226,c228,c230,c247,c248,c257,c342,c368,c413,c415,c416,c417,c431,c438,c456,c477]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t5302]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV880-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n011.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:14:13 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 28.30/4.41 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 28.30/4.41 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------