%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV879-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 : 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:21 PM UTC 2026
% Result : Unsatisfiable 28.11s 4.12s
% Output : Proof 28.11s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t191,axiom,
sF0 = c_Finite__Set_Ofinite(v_U,tc_Com_Opname),
introduced(definition) ).
cnf(f860,negated_conjecture,
c_Finite__Set_Ofinite(v_U,tc_Com_Opname),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f860_nnf,plain,
c_Finite__Set_Ofinite(v_U,tc_Com_Opname),
inference(nnf_transformation,[status(thm)],[f860]) ).
cnf(c860,plain,
c_Finite__Set_Ofinite(v_U,tc_Com_Opname),
inference(cnf_transformation,[status(esa)],[f860_nnf]) ).
cnf(t3,plain,
c_Finite__Set_Ofinite(v_U,tc_Com_Opname) = true,
inference(equality_encoding,[status(esa)],[c860]) ).
cnf(t206,plain,
c_Finite__Set_Ofinite(v_U,tc_Com_Opname) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(t2969,plain,
sF0 = true,
inference(step,[status(thm)],[t191,t206]) ).
cnf(t207,plain,
true = sF0,
inference(orient,[status(thm)],[t2969]) ).
cnf(f863,negated_conjecture,
~ hBOOL(hAPP(hAPP(v_P,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a)),c_Set_Oinsert(hAPP(v_mgt__call,v_x),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f863_nnf,plain,
~ hBOOL(hAPP(hAPP(v_P,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a)),c_Set_Oinsert(hAPP(v_mgt__call,v_x),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a))),
inference(nnf_transformation,[status(thm)],[f863]) ).
fof(f863_sk,plain,
~ hBOOL(hAPP(hAPP(v_P,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a)),c_Set_Oinsert(hAPP(v_mgt__call,v_x),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a))),
inference(skolemisation,[status(esa)],[f863_nnf]) ).
cnf(c863,plain,
~ hBOOL(hAPP(hAPP(v_P,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a)),c_Set_Oinsert(hAPP(v_mgt__call,v_x),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a))),
inference(cnf_transformation,[status(esa)],[f863_sk]) ).
cnf(t91,plain,
hBOOL(hAPP(hAPP(v_P,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a)),c_Set_Oinsert(hAPP(v_mgt__call,v_x),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a))) = false,
inference(equality_encoding,[status(esa)],[c863]) ).
cnf(f861,negated_conjecture,
v_G = c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f861_nnf,plain,
v_G = c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),
inference(nnf_transformation,[status(thm)],[f861]) ).
cnf(c861,plain,
v_G = c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),
inference(cnf_transformation,[status(esa)],[f861_nnf]) ).
cnf(t4,plain,
c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a) = v_G,
inference(equality_encoding,[status(esa)],[c861]) ).
cnf(t220,plain,
c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a) = v_G,
inference(orient,[status(thm)],[t4]) ).
cnf(t192,axiom,
sF1 = c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),
introduced(definition) ).
cnf(t2981,plain,
sF1 = v_G,
inference(step,[status(thm)],[t192,t220]) ).
cnf(t223,plain,
v_G = sF1,
inference(orient,[status(thm)],[t2981]) ).
cnf(t2982,plain,
c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a) = sF1,
inference(step,[status(thm)],[t220,t223]) ).
cnf(t224,plain,
c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a) = sF1,
inference(orient,[status(thm)],[t2982]) ).
cnf(t3433,plain,
hBOOL(hAPP(hAPP(v_P,sF1),c_Set_Oinsert(hAPP(v_mgt__call,v_x),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a))) = false,
inference(step,[status(thm)],[t91,t224]) ).
cnf(t195,axiom,
sF4 = hAPP(v_P,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a)),
introduced(definition) ).
cnf(t2997,plain,
sF4 = hAPP(v_P,sF1),
inference(step,[status(thm)],[t195,t224]) ).
cnf(t245,plain,
hAPP(v_P,sF1) = sF4,
inference(orient,[status(thm)],[t2997]) ).
cnf(t3434,plain,
hBOOL(hAPP(sF4,c_Set_Oinsert(hAPP(v_mgt__call,v_x),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a))) = false,
inference(step,[status(thm)],[t3433,t245]) ).
cnf(f816,axiom,
c_Set_Oimage(V_f,c_Set_Oinsert(V_a,V_B,T_b),T_b,T_a) = c_Set_Oinsert(hAPP(V_f,V_a),c_Set_Oimage(V_f,V_B,T_b,T_a),T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_image__insert_0) ).
fof(f816_nnf,plain,
! [V_f,V_a,V_B,T_b,T_a] : c_Set_Oimage(V_f,c_Set_Oinsert(V_a,V_B,T_b),T_b,T_a) = c_Set_Oinsert(hAPP(V_f,V_a),c_Set_Oimage(V_f,V_B,T_b,T_a),T_a),
inference(nnf_transformation,[status(thm)],[f816]) ).
fof(f816_sk,plain,
! [V_f,V_a,V_B,T_b,T_a] : c_Set_Oimage(V_f,c_Set_Oinsert(V_a,V_B,T_b),T_b,T_a) = c_Set_Oinsert(hAPP(V_f,V_a),c_Set_Oimage(V_f,V_B,T_b,T_a),T_a),
inference(skolemisation,[status(esa)],[f816_nnf]) ).
cnf(c816,plain,
c_Set_Oimage(X0,c_Set_Oinsert(X1,X2,X3),X3,X4) = c_Set_Oinsert(hAPP(X0,X1),c_Set_Oimage(X0,X2,X3,X4),X4),
inference(cnf_transformation,[status(esa)],[f816_sk]) ).
cnf(t80,plain,
c_Set_Oinsert(hAPP(X1,X2),c_Set_Oimage(X1,X3,X4,X5),X5) = c_Set_Oimage(X1,c_Set_Oinsert(X2,X3,X4),X4,X5),
inference(equality_encoding,[status(esa)],[c816]) ).
cnf(t2037,plain,
c_Set_Oinsert(hAPP(X1,X2),c_Set_Oimage(X1,X3,X4,X5),X5) = c_Set_Oimage(X1,c_Set_Oinsert(X2,X3,X4),X4,X5),
inference(orient,[status(thm)],[t80]) ).
cnf(f846,axiom,
c_Set_Oimage(V_f,c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)),T_b,T_a) = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_image__empty_0) ).
fof(f846_nnf,plain,
! [V_f,T_b,T_a] : c_Set_Oimage(V_f,c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)),T_b,T_a) = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f846]) ).
fof(f846_sk,plain,
! [V_f,T_b,T_a] : c_Set_Oimage(V_f,c_Orderings_Obot__class_Obot(tc_fun(T_b,tc_bool)),T_b,T_a) = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f846_nnf]) ).
cnf(c846,plain,
c_Set_Oimage(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1,X2) = c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
inference(cnf_transformation,[status(esa)],[f846_sk]) ).
cnf(t31,plain,
c_Set_Oimage(X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2,X3) = c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)),
inference(equality_encoding,[status(esa)],[c846]) ).
cnf(t253,plain,
c_Set_Oimage(X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2,X3) = c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)),
inference(orient,[status(thm)],[t31]) ).
cnf(t197,axiom,
sF6 = tc_fun(t_a,tc_bool),
introduced(definition) ).
cnf(t217,plain,
tc_fun(t_a,tc_bool) = sF6,
inference(orient,[status(thm)],[t197]) ).
cnf(t254,plain,
c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) = c_Set_Oimage(X2,c_Orderings_Obot__class_Obot(sF6),t_a,X1),
inference(cp,[status(thm)],[t253,t217]) ).
cnf(t198,axiom,
sF7 = c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),
introduced(definition) ).
cnf(t2978,plain,
sF7 = c_Orderings_Obot__class_Obot(sF6),
inference(step,[status(thm)],[t198,t217]) ).
cnf(t219,plain,
c_Orderings_Obot__class_Obot(sF6) = sF7,
inference(orient,[status(thm)],[t2978]) ).
cnf(t3000,plain,
c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) = c_Set_Oimage(X2,sF7,t_a,X1),
inference(step,[status(thm)],[t254,t219]) ).
cnf(t255,plain,
c_Set_Oimage(X1,sF7,t_a,X2) = c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
inference(orient,[status(thm)],[t3000]) ).
cnf(t2044,plain,
c_Set_Oimage(X1,c_Set_Oinsert(X2,sF7,t_a),t_a,X3) = c_Set_Oinsert(hAPP(X1,X2),c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)),X3),
inference(cp,[status(thm)],[t2037,t255]) ).
cnf(t2219,plain,
c_Set_Oinsert(hAPP(X1,X2),c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)),X3) = c_Set_Oimage(X1,c_Set_Oinsert(X2,sF7,t_a),t_a,X3),
inference(orient,[status(thm)],[t2044]) ).
cnf(t3435,plain,
hBOOL(hAPP(sF4,c_Set_Oimage(v_mgt__call,c_Set_Oinsert(v_x,sF7,t_a),t_a,t_a))) = false,
inference(step,[status(thm)],[t3434,t2219]) ).
cnf(t2221,plain,
c_Set_Oimage(X1,c_Set_Oinsert(X2,sF7,t_a),t_a,t_a) = c_Set_Oinsert(hAPP(X1,X2),c_Orderings_Obot__class_Obot(sF6),t_a),
inference(cp,[status(thm)],[t2219,t217]) ).
cnf(t3383,plain,
c_Set_Oimage(X1,c_Set_Oinsert(X2,sF7,t_a),t_a,t_a) = c_Set_Oinsert(hAPP(X1,X2),sF7,t_a),
inference(step,[status(thm)],[t2221,t219]) ).
cnf(t2251,plain,
c_Set_Oimage(X1,c_Set_Oinsert(X2,sF7,t_a),t_a,t_a) = c_Set_Oinsert(hAPP(X1,X2),sF7,t_a),
inference(orient,[status(thm)],[t3383]) ).
cnf(t3436,plain,
hBOOL(hAPP(sF4,c_Set_Oinsert(hAPP(v_mgt__call,v_x),sF7,t_a))) = false,
inference(step,[status(thm)],[t3435,t2251]) ).
cnf(t196,axiom,
sF5 = hAPP(v_mgt__call,v_x),
introduced(definition) ).
cnf(t216,plain,
hAPP(v_mgt__call,v_x) = sF5,
inference(orient,[status(thm)],[t196]) ).
cnf(t3437,plain,
hBOOL(hAPP(sF4,c_Set_Oinsert(sF5,sF7,t_a))) = false,
inference(step,[status(thm)],[t3436,t216]) ).
cnf(t199,axiom,
sF8 = c_Set_Oinsert(hAPP(v_mgt__call,v_x),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a),
introduced(definition) ).
cnf(t3046,plain,
sF8 = c_Set_Oinsert(sF5,c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a),
inference(step,[status(thm)],[t199,t216]) ).
cnf(t3047,plain,
sF8 = c_Set_Oinsert(sF5,c_Orderings_Obot__class_Obot(sF6),t_a),
inference(step,[status(thm)],[t3046,t217]) ).
cnf(t3048,plain,
sF8 = c_Set_Oinsert(sF5,sF7,t_a),
inference(step,[status(thm)],[t3047,t219]) ).
cnf(t322,plain,
c_Set_Oinsert(sF5,sF7,t_a) = sF8,
inference(orient,[status(thm)],[t3048]) ).
cnf(t3438,plain,
hBOOL(hAPP(sF4,sF8)) = false,
inference(step,[status(thm)],[t3437,t322]) ).
cnf(f639,axiom,
( ~ c_lessequals(V_ts,V_G,tc_fun(t_a,tc_bool))
| hBOOL(hAPP(hAPP(v_P,V_G),V_ts)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_assms_I1_J_0) ).
fof(f639_nnf,plain,
! [V_G,V_ts] :
( ~ c_lessequals(V_ts,V_G,tc_fun(t_a,tc_bool))
| hBOOL(hAPP(hAPP(v_P,V_G),V_ts)) ),
inference(nnf_transformation,[status(thm)],[f639]) ).
fof(f639_sk,plain,
! [V_G,V_ts] :
( ~ c_lessequals(V_ts,V_G,tc_fun(t_a,tc_bool))
| hBOOL(hAPP(hAPP(v_P,V_G),V_ts)) ),
inference(skolemisation,[status(esa)],[f639_nnf]) ).
cnf(c639,plain,
( ~ c_lessequals(X1,X0,tc_fun(t_a,tc_bool))
| hBOOL(hAPP(hAPP(v_P,X0),X1)) ),
inference(cnf_transformation,[status(esa)],[f639_sk]) ).
cnf(t70,plain,
ifeq(c_lessequals(X1,X2,tc_fun(t_a,tc_bool)),true,hBOOL(hAPP(hAPP(v_P,X2),X1)),true) = true,
inference(equality_encoding,[status(esa)],[c639]) ).
cnf(t3271,plain,
ifeq(c_lessequals(X1,X2,sF6),true,hBOOL(hAPP(hAPP(v_P,X2),X1)),true) = true,
inference(step,[status(thm)],[t70,t217]) ).
cnf(t3272,plain,
ifeq(c_lessequals(X1,X2,sF6),sF0,hBOOL(hAPP(hAPP(v_P,X2),X1)),true) = true,
inference(step,[status(thm)],[t3271,t207]) ).
cnf(t3273,plain,
ifeq(c_lessequals(X1,X2,sF6),sF0,hBOOL(hAPP(hAPP(v_P,X2),X1)),sF0) = true,
inference(step,[status(thm)],[t3272,t207]) ).
cnf(t3274,plain,
ifeq(c_lessequals(X1,X2,sF6),sF0,hBOOL(hAPP(hAPP(v_P,X2),X1)),sF0) = sF0,
inference(step,[status(thm)],[t3273,t207]) ).
cnf(t1420,plain,
ifeq(c_lessequals(X1,X2,sF6),sF0,hBOOL(hAPP(hAPP(v_P,X2),X1)),sF0) = sF0,
inference(orient,[status(thm)],[t3274]) ).
cnf(f532,axiom,
c_lessequals(V_A,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B),tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Un__upper1_0) ).
fof(f532_nnf,plain,
! [V_A,T_a,V_B] : c_lessequals(V_A,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B),tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f532]) ).
fof(f532_sk,plain,
! [V_A,T_a,V_B] : c_lessequals(V_A,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_A),V_B),tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f532_nnf]) ).
cnf(c532,plain,
c_lessequals(X0,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X1,tc_bool)),X0),X2),tc_fun(X1,tc_bool)),
inference(cnf_transformation,[status(esa)],[f532_sk]) ).
cnf(t53,plain,
c_lessequals(X1,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X2,tc_bool)),X1),X3),tc_fun(X2,tc_bool)) = true,
inference(equality_encoding,[status(esa)],[c532]) ).
cnf(t3137,plain,
c_lessequals(X1,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X2,tc_bool)),X1),X3),tc_fun(X2,tc_bool)) = sF0,
inference(step,[status(thm)],[t53,t207]) ).
cnf(t628,plain,
c_lessequals(X1,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X2,tc_bool)),X1),X3),tc_fun(X2,tc_bool)) = sF0,
inference(orient,[status(thm)],[t3137]) ).
cnf(t629,plain,
sF0 = c_lessequals(X1,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF6),X1),X2),tc_fun(t_a,tc_bool)),
inference(cp,[status(thm)],[t628,t217]) ).
cnf(t3153,plain,
sF0 = c_lessequals(X1,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF6),X1),X2),sF6),
inference(step,[status(thm)],[t629,t217]) ).
cnf(t710,plain,
c_lessequals(X1,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF6),X1),X2),sF6) = sF0,
inference(orient,[status(thm)],[t3153]) ).
cnf(f631,axiom,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),c_Set_Oinsert(V_a,V_B,T_a)),V_C) = c_Set_Oinsert(V_a,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_B),V_C),T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Un__insert__left_0) ).
fof(f631_nnf,plain,
! [T_a,V_a,V_B,V_C] : hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),c_Set_Oinsert(V_a,V_B,T_a)),V_C) = c_Set_Oinsert(V_a,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_B),V_C),T_a),
inference(nnf_transformation,[status(thm)],[f631]) ).
fof(f631_sk,plain,
! [T_a,V_a,V_B,V_C] : hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),c_Set_Oinsert(V_a,V_B,T_a)),V_C) = c_Set_Oinsert(V_a,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),V_B),V_C),T_a),
inference(skolemisation,[status(esa)],[f631_nnf]) ).
cnf(c631,plain,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X0,tc_bool)),c_Set_Oinsert(X1,X2,X0)),X3) = c_Set_Oinsert(X1,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X0,tc_bool)),X2),X3),X0),
inference(cnf_transformation,[status(esa)],[f631_sk]) ).
cnf(t126,plain,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X1,tc_bool)),c_Set_Oinsert(X2,X3,X1)),X4) = c_Set_Oinsert(X2,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X1,tc_bool)),X3),X4),X1),
inference(equality_encoding,[status(esa)],[c631]) ).
cnf(t375,plain,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X1,tc_bool)),c_Set_Oinsert(X2,X3,X1)),X4) = c_Set_Oinsert(X2,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X1,tc_bool)),X3),X4),X1),
inference(orient,[status(thm)],[t126]) ).
cnf(t377,plain,
c_Set_Oinsert(sF5,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(t_a,tc_bool)),sF7),X1),t_a) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(t_a,tc_bool)),sF8),X1),
inference(cp,[status(thm)],[t375,t322]) ).
cnf(t3088,plain,
c_Set_Oinsert(sF5,hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF6),sF7),X1),t_a) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(t_a,tc_bool)),sF8),X1),
inference(step,[status(thm)],[t377,t217]) ).
cnf(f612,axiom,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),V_B) = V_B,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Un__empty__left_0) ).
fof(f612_nnf,plain,
! [T_a,V_B] : hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),V_B) = V_B,
inference(nnf_transformation,[status(thm)],[f612]) ).
fof(f612_sk,plain,
! [T_a,V_B] : hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(T_a,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))),V_B) = V_B,
inference(skolemisation,[status(esa)],[f612_nnf]) ).
cnf(c612,plain,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X0,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))),X1) = X1,
inference(cnf_transformation,[status(esa)],[f612_sk]) ).
cnf(t34,plain,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X1,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool))),X2) = X2,
inference(equality_encoding,[status(esa)],[c612]) ).
cnf(t345,plain,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(X1,tc_bool)),c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool))),X2) = X2,
inference(orient,[status(thm)],[t34]) ).
cnf(t346,plain,
X1 = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF6),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool))),X1),
inference(cp,[status(thm)],[t345,t217]) ).
cnf(t3062,plain,
X1 = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF6),c_Orderings_Obot__class_Obot(sF6)),X1),
inference(step,[status(thm)],[t346,t217]) ).
cnf(t3063,plain,
X1 = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF6),sF7),X1),
inference(step,[status(thm)],[t3062,t219]) ).
cnf(t347,plain,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF6),sF7),X1) = X1,
inference(orient,[status(thm)],[t3063]) ).
cnf(t3089,plain,
c_Set_Oinsert(sF5,X1,t_a) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(tc_fun(t_a,tc_bool)),sF8),X1),
inference(step,[status(thm)],[t3088,t347]) ).
cnf(t3090,plain,
c_Set_Oinsert(sF5,X1,t_a) = hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF6),sF8),X1),
inference(step,[status(thm)],[t3089,t217]) ).
cnf(t379,plain,
hAPP(hAPP(c_Lattices_Oupper__semilattice__class_Osup(sF6),sF8),X1) = c_Set_Oinsert(sF5,X1,t_a),
inference(orient,[status(thm)],[t3090]) ).
cnf(t712,plain,
sF0 = c_lessequals(sF8,c_Set_Oinsert(sF5,X1,t_a),sF6),
inference(cp,[status(thm)],[t710,t379]) ).
cnf(t714,plain,
c_lessequals(sF8,c_Set_Oinsert(sF5,X1,t_a),sF6) = sF0,
inference(orient,[status(thm)],[t712]) ).
cnf(f853,axiom,
( ~ hBOOL(c_in(V_a,V_A,T_a))
| c_Set_Oinsert(V_a,V_A,T_a) = V_A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_insert__absorb_0) ).
fof(f853_nnf,plain,
! [V_a,V_A,T_a] :
( ~ hBOOL(c_in(V_a,V_A,T_a))
| c_Set_Oinsert(V_a,V_A,T_a) = V_A ),
inference(nnf_transformation,[status(thm)],[f853]) ).
fof(f853_sk,plain,
! [V_a,V_A,T_a] :
( ~ hBOOL(c_in(V_a,V_A,T_a))
| c_Set_Oinsert(V_a,V_A,T_a) = V_A ),
inference(skolemisation,[status(esa)],[f853_nnf]) ).
cnf(c853,plain,
( ~ hBOOL(c_in(X0,X1,X2))
| c_Set_Oinsert(X0,X1,X2) = X1 ),
inference(cnf_transformation,[status(esa)],[f853_sk]) ).
cnf(t44,plain,
ifeq(hBOOL(c_in(X1,X2,X3)),true,c_Set_Oinsert(X1,X2,X3),X2) = X2,
inference(equality_encoding,[status(esa)],[c853]) ).
cnf(t3107,plain,
ifeq(hBOOL(c_in(X1,X2,X3)),sF0,c_Set_Oinsert(X1,X2,X3),X2) = X2,
inference(step,[status(thm)],[t44,t207]) ).
cnf(t412,plain,
ifeq(hBOOL(c_in(X1,X2,X3)),sF0,c_Set_Oinsert(X1,X2,X3),X2) = X2,
inference(orient,[status(thm)],[t3107]) ).
cnf(f564,axiom,
( ~ hBOOL(hAPP(V_P,V_a))
| hBOOL(c_in(V_a,c_Collect(V_P,T_a),T_a)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_CollectI_0) ).
fof(f564_nnf,plain,
! [V_a,V_P,T_a] :
( ~ hBOOL(hAPP(V_P,V_a))
| hBOOL(c_in(V_a,c_Collect(V_P,T_a),T_a)) ),
inference(nnf_transformation,[status(thm)],[f564]) ).
fof(f564_sk,plain,
! [V_a,V_P,T_a] :
( ~ hBOOL(hAPP(V_P,V_a))
| hBOOL(c_in(V_a,c_Collect(V_P,T_a),T_a)) ),
inference(skolemisation,[status(esa)],[f564_nnf]) ).
cnf(c564,plain,
( ~ hBOOL(hAPP(X1,X0))
| hBOOL(c_in(X0,c_Collect(X1,X2),X2)) ),
inference(cnf_transformation,[status(esa)],[f564_sk]) ).
cnf(u20,axiom,
ifeq(hBOOL(hAPP(X0,X1)),true,hBOOL(c_in(X1,c_Collect(X0,X2),X2)),true) = true,
inference(equality_encoding,[status(esa)],[c564]) ).
cnf(f664,axiom,
c_Collect(V_P,T_a) = V_P,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Collect__def_0) ).
fof(f664_nnf,plain,
! [V_P,T_a] : c_Collect(V_P,T_a) = V_P,
inference(nnf_transformation,[status(thm)],[f664]) ).
fof(f664_sk,plain,
! [V_P,T_a] : c_Collect(V_P,T_a) = V_P,
inference(skolemisation,[status(esa)],[f664_nnf]) ).
cnf(c664,plain,
c_Collect(X0,X1) = X0,
inference(cnf_transformation,[status(esa)],[f664_sk]) ).
cnf(d1,axiom,
c_Collect(X0,X1) = X0,
inference(equality_encoding,[status(esa)],[c664]) ).
cnf(t50,plain,
ifeq(hBOOL(hAPP(X1,X2)),true,hBOOL(c_in(X2,X1,X3)),true) = true,
inference(definition_unfolding,[status(thm)],[u20,d1]) ).
cnf(t3116,plain,
ifeq(hBOOL(hAPP(X1,X2)),sF0,hBOOL(c_in(X2,X1,X3)),true) = true,
inference(step,[status(thm)],[t50,t207]) ).
cnf(t3117,plain,
ifeq(hBOOL(hAPP(X1,X2)),sF0,hBOOL(c_in(X2,X1,X3)),sF0) = true,
inference(step,[status(thm)],[t3116,t207]) ).
cnf(t3118,plain,
ifeq(hBOOL(hAPP(X1,X2)),sF0,hBOOL(c_in(X2,X1,X3)),sF0) = sF0,
inference(step,[status(thm)],[t3117,t207]) ).
cnf(t486,plain,
ifeq(hBOOL(hAPP(X1,X2)),sF0,hBOOL(c_in(X2,X1,X3)),sF0) = sF0,
inference(orient,[status(thm)],[t3118]) ).
cnf(f815,axiom,
hBOOL(hAPP(c_Set_Oinsert(V_x,V_A,T_a),V_x)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_insert__code_1) ).
fof(f815_nnf,plain,
! [V_x,V_A,T_a] : hBOOL(hAPP(c_Set_Oinsert(V_x,V_A,T_a),V_x)),
inference(nnf_transformation,[status(thm)],[f815]) ).
fof(f815_sk,plain,
! [V_x,V_A,T_a] : hBOOL(hAPP(c_Set_Oinsert(V_x,V_A,T_a),V_x)),
inference(skolemisation,[status(esa)],[f815_nnf]) ).
cnf(c815,plain,
hBOOL(hAPP(c_Set_Oinsert(X0,X1,X2),X0)),
inference(cnf_transformation,[status(esa)],[f815_sk]) ).
cnf(t12,plain,
hBOOL(hAPP(c_Set_Oinsert(X1,X2,X3),X1)) = true,
inference(equality_encoding,[status(esa)],[c815]) ).
cnf(t2992,plain,
hBOOL(hAPP(c_Set_Oinsert(X1,X2,X3),X1)) = sF0,
inference(step,[status(thm)],[t12,t207]) ).
cnf(t242,plain,
hBOOL(hAPP(c_Set_Oinsert(X1,X2,X3),X1)) = sF0,
inference(orient,[status(thm)],[t2992]) ).
cnf(t490,plain,
sF0 = ifeq(sF0,sF0,hBOOL(c_in(X1,c_Set_Oinsert(X1,X2,X3),X4)),sF0),
inference(cp,[status(thm)],[t486,t242]) ).
cnf(t6,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t222,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t6]) ).
cnf(t3126,plain,
sF0 = hBOOL(c_in(X1,c_Set_Oinsert(X1,X2,X3),X4)),
inference(step,[status(thm)],[t490,t222]) ).
cnf(t539,plain,
hBOOL(c_in(X1,c_Set_Oinsert(X1,X2,X3),X4)) = sF0,
inference(orient,[status(thm)],[t3126]) ).
cnf(t541,plain,
c_Set_Oinsert(X1,X2,X3) = ifeq(sF0,sF0,c_Set_Oinsert(X1,c_Set_Oinsert(X1,X2,X3),X4),c_Set_Oinsert(X1,X2,X3)),
inference(cp,[status(thm)],[t412,t539]) ).
cnf(t3128,plain,
c_Set_Oinsert(X1,X2,X3) = c_Set_Oinsert(X1,c_Set_Oinsert(X1,X2,X3),X4),
inference(step,[status(thm)],[t541,t222]) ).
cnf(t542,plain,
c_Set_Oinsert(X1,c_Set_Oinsert(X1,X2,X3),X4) = c_Set_Oinsert(X1,X2,X3),
inference(orient,[status(thm)],[t3128]) ).
cnf(t715,plain,
sF0 = c_lessequals(sF8,c_Set_Oinsert(sF5,X1,X2),sF6),
inference(cp,[status(thm)],[t714,t542]) ).
cnf(t718,plain,
c_lessequals(sF8,c_Set_Oinsert(sF5,X1,X2),sF6) = sF0,
inference(orient,[status(thm)],[t715]) ).
cnf(t1426,plain,
sF0 = ifeq(sF0,sF0,hBOOL(hAPP(hAPP(v_P,c_Set_Oinsert(sF5,X1,X2)),sF8)),sF0),
inference(cp,[status(thm)],[t1420,t718]) ).
cnf(t3322,plain,
sF0 = hBOOL(hAPP(hAPP(v_P,c_Set_Oinsert(sF5,X1,X2)),sF8)),
inference(step,[status(thm)],[t1426,t222]) ).
cnf(t1689,plain,
hBOOL(hAPP(hAPP(v_P,c_Set_Oinsert(sF5,X1,X2)),sF8)) = sF0,
inference(orient,[status(thm)],[t3322]) ).
cnf(t2039,plain,
c_Set_Oimage(v_mgt__call,c_Set_Oinsert(X1,v_U,tc_Com_Opname),tc_Com_Opname,t_a) = c_Set_Oinsert(hAPP(v_mgt__call,X1),sF1,t_a),
inference(cp,[status(thm)],[t2037,t224]) ).
cnf(t2087,plain,
c_Set_Oimage(v_mgt__call,c_Set_Oinsert(X1,v_U,tc_Com_Opname),tc_Com_Opname,t_a) = c_Set_Oinsert(hAPP(v_mgt__call,X1),sF1,t_a),
inference(orient,[status(thm)],[t2039]) ).
cnf(t193,axiom,
sF2 = c_in(v_x,v_U,tc_Com_Opname),
introduced(definition) ).
cnf(t218,plain,
c_in(v_x,v_U,tc_Com_Opname) = sF2,
inference(orient,[status(thm)],[t193]) ).
cnf(t413,plain,
v_U = ifeq(hBOOL(sF2),sF0,c_Set_Oinsert(v_x,v_U,tc_Com_Opname),v_U),
inference(cp,[status(thm)],[t412,t218]) ).
cnf(f862,negated_conjecture,
hBOOL(c_in(v_x,v_U,tc_Com_Opname)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f862_nnf,plain,
hBOOL(c_in(v_x,v_U,tc_Com_Opname)),
inference(nnf_transformation,[status(thm)],[f862]) ).
cnf(c862,plain,
hBOOL(c_in(v_x,v_U,tc_Com_Opname)),
inference(cnf_transformation,[status(esa)],[f862_nnf]) ).
cnf(t5,plain,
hBOOL(c_in(v_x,v_U,tc_Com_Opname)) = true,
inference(equality_encoding,[status(esa)],[c862]) ).
cnf(t2979,plain,
hBOOL(sF2) = true,
inference(step,[status(thm)],[t5,t218]) ).
cnf(t2980,plain,
hBOOL(sF2) = sF0,
inference(step,[status(thm)],[t2979,t207]) ).
cnf(t221,plain,
hBOOL(sF2) = sF0,
inference(orient,[status(thm)],[t2980]) ).
cnf(t3108,plain,
v_U = ifeq(sF0,sF0,c_Set_Oinsert(v_x,v_U,tc_Com_Opname),v_U),
inference(step,[status(thm)],[t413,t221]) ).
cnf(t3109,plain,
v_U = c_Set_Oinsert(v_x,v_U,tc_Com_Opname),
inference(step,[status(thm)],[t3108,t222]) ).
cnf(t418,plain,
c_Set_Oinsert(v_x,v_U,tc_Com_Opname) = v_U,
inference(orient,[status(thm)],[t3109]) ).
cnf(t419,plain,
sF0 = hBOOL(hAPP(v_U,v_x)),
inference(cp,[status(thm)],[t242,t418]) ).
cnf(t424,plain,
hBOOL(hAPP(v_U,v_x)) = sF0,
inference(orient,[status(thm)],[t419]) ).
cnf(t509,plain,
sF0 = ifeq(sF0,sF0,hBOOL(c_in(v_x,v_U,X1)),sF0),
inference(cp,[status(thm)],[t486,t424]) ).
cnf(t3123,plain,
sF0 = hBOOL(c_in(v_x,v_U,X1)),
inference(step,[status(thm)],[t509,t222]) ).
cnf(t523,plain,
hBOOL(c_in(v_x,v_U,X1)) = sF0,
inference(orient,[status(thm)],[t3123]) ).
cnf(t525,plain,
v_U = ifeq(sF0,sF0,c_Set_Oinsert(v_x,v_U,X1),v_U),
inference(cp,[status(thm)],[t412,t523]) ).
cnf(t3124,plain,
v_U = c_Set_Oinsert(v_x,v_U,X1),
inference(step,[status(thm)],[t525,t222]) ).
cnf(t526,plain,
c_Set_Oinsert(v_x,v_U,X1) = v_U,
inference(orient,[status(thm)],[t3124]) ).
cnf(t2088,plain,
c_Set_Oinsert(hAPP(v_mgt__call,v_x),sF1,t_a) = c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),
inference(cp,[status(thm)],[t2087,t526]) ).
cnf(t3367,plain,
c_Set_Oinsert(sF5,sF1,t_a) = c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),
inference(step,[status(thm)],[t2088,t216]) ).
cnf(t3368,plain,
c_Set_Oinsert(sF5,sF1,t_a) = sF1,
inference(step,[status(thm)],[t3367,t224]) ).
cnf(t2090,plain,
c_Set_Oinsert(sF5,sF1,t_a) = sF1,
inference(orient,[status(thm)],[t3368]) ).
cnf(t2096,plain,
c_Set_Oinsert(sF5,sF1,t_a) = c_Set_Oinsert(sF5,sF1,X1),
inference(cp,[status(thm)],[t542,t2090]) ).
cnf(t3369,plain,
sF1 = c_Set_Oinsert(sF5,sF1,X1),
inference(step,[status(thm)],[t2096,t2090]) ).
cnf(t2114,plain,
c_Set_Oinsert(sF5,sF1,X1) = sF1,
inference(orient,[status(thm)],[t3369]) ).
cnf(t2134,plain,
sF0 = hBOOL(hAPP(hAPP(v_P,sF1),sF8)),
inference(cp,[status(thm)],[t1689,t2114]) ).
cnf(t3371,plain,
sF0 = hBOOL(hAPP(sF4,sF8)),
inference(step,[status(thm)],[t2134,t245]) ).
cnf(t2139,plain,
hBOOL(hAPP(sF4,sF8)) = sF0,
inference(orient,[status(thm)],[t3371]) ).
cnf(t3439,plain,
sF0 = false,
inference(step,[status(thm)],[t3438,t2139]) ).
cnf(t2900,plain,
false = sF0,
inference(orient,[status(thm)],[t3439]) ).
cnf(f60,axiom,
~ c_HOL_Oord__class_Oless(V_x,V_x,tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_psubset__eq_1) ).
fof(f60_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)],[f60]) ).
fof(f60_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)],[f60_nnf]) ).
cnf(c60,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_fun(X1,tc_bool)),
inference(cnf_transformation,[status(esa)],[f60_sk]) ).
cnf(f61,axiom,
~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat__less__le_1) ).
fof(f61_nnf,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
inference(nnf_transformation,[status(thm)],[f61]) ).
fof(f61_sk,plain,
! [V_x] : ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat),
inference(skolemisation,[status(esa)],[f61_nnf]) ).
cnf(c61,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f61_sk]) ).
cnf(f62,axiom,
~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_less__not__refl_0) ).
fof(f62_nnf,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
inference(nnf_transformation,[status(thm)],[f62]) ).
fof(f62_sk,plain,
! [V_n] : ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat),
inference(skolemisation,[status(esa)],[f62_nnf]) ).
cnf(c62,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f62_sk]) ).
cnf(f64,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__le_1) ).
fof(f64_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)],[f64]) ).
fof(f64_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)],[f64_nnf]) ).
cnf(c64,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f64_sk]) ).
cnf(f65,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linorder__neq__iff_1) ).
fof(f65_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)],[f65]) ).
fof(f65_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)],[f65_nnf]) ).
cnf(c65,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f65_sk]) ).
cnf(f66,axiom,
( ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a)
| ~ class_Orderings_Opreorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_order__less__irrefl_0) ).
fof(f66_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)],[f66]) ).
fof(f66_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)],[f66_nnf]) ).
cnf(c66,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(f119,axiom,
~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc__n__not__le__n_0) ).
fof(f119_nnf,plain,
! [V_n] : ~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
inference(nnf_transformation,[status(thm)],[f119]) ).
fof(f119_sk,plain,
! [V_n] : ~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
inference(skolemisation,[status(esa)],[f119_nnf]) ).
cnf(c119,plain,
~ c_lessequals(c_Suc(X0),X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f119_sk]) ).
cnf(f123,axiom,
c_Suc(V_n) != V_n,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc__n__not__n_0) ).
fof(f123_nnf,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(nnf_transformation,[status(thm)],[f123]) ).
fof(f123_sk,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(skolemisation,[status(esa)],[f123_nnf]) ).
cnf(c123,plain,
c_Suc(X0) != X0,
inference(cnf_transformation,[status(esa)],[f123_sk]) ).
cnf(f124,axiom,
V_n != c_Suc(V_n),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_n__not__Suc__n_0) ).
fof(f124_nnf,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(nnf_transformation,[status(thm)],[f124]) ).
fof(f124_sk,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(skolemisation,[status(esa)],[f124_nnf]) ).
cnf(c124,plain,
X0 != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f124_sk]) ).
cnf(f146,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/sandbox/benchmark/theBenchmark.p',cls_atLeastLessThan__empty__iff_0) ).
fof(f146_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)],[f146]) ).
fof(f146_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)],[f146_nnf]) ).
cnf(c146,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)],[f146_sk]) ).
cnf(f148,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/sandbox/benchmark/theBenchmark.p',cls_greaterThanAtMost__empty__iff2_0) ).
fof(f148_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)],[f148]) ).
fof(f148_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)],[f148_nnf]) ).
cnf(c148,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)],[f148_sk]) ).
cnf(f186,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/sandbox/benchmark/theBenchmark.p',cls_greaterThanAtMost__empty__iff_0) ).
fof(f186_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)],[f186]) ).
fof(f186_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)],[f186_nnf]) ).
cnf(c186,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)],[f186_sk]) ).
cnf(f232,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/sandbox/benchmark/theBenchmark.p',cls_linorder__antisym__conv2_1) ).
fof(f232_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)],[f232]) ).
fof(f232_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)],[f232_nnf]) ).
cnf(c232,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ c_lessequals(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f232_sk]) ).
cnf(f234,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/sandbox/benchmark/theBenchmark.p',cls_linorder__not__less_1) ).
fof(f234_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)],[f234]) ).
fof(f234_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)],[f234_nnf]) ).
cnf(c234,plain,
( ~ c_lessequals(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f234_sk]) ).
cnf(f236,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/sandbox/benchmark/theBenchmark.p',cls_linorder__not__le_1) ).
fof(f236_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)],[f236]) ).
fof(f236_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)],[f236_nnf]) ).
cnf(c236,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f236_sk]) ).
cnf(f238,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/sandbox/benchmark/theBenchmark.p',cls_less__fun__def_1) ).
fof(f238_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)],[f238]) ).
fof(f238_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)],[f238_nnf]) ).
cnf(c238,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)],[f238_sk]) ).
cnf(f239,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/sandbox/benchmark/theBenchmark.p',cls_less__le__not__le_1) ).
fof(f239_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)],[f239]) ).
fof(f239_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)],[f239_nnf]) ).
cnf(c239,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f239_sk]) ).
cnf(f286,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/sandbox/benchmark/theBenchmark.p',cls_xt1_I9_J_0) ).
fof(f286_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)],[f286]) ).
fof(f286_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)],[f286_nnf]) ).
cnf(c286,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)],[f286_sk]) ).
cnf(f287,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/sandbox/benchmark/theBenchmark.p',cls_not__less__iff__gr__or__eq_1) ).
fof(f287_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)],[f287]) ).
fof(f287_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)],[f287_nnf]) ).
cnf(c287,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)],[f287_sk]) ).
cnf(f289,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/sandbox/benchmark/theBenchmark.p',cls_order__less__asym_0) ).
fof(f289_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)],[f289]) ).
fof(f289_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)],[f289_nnf]) ).
cnf(c289,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)],[f289_sk]) ).
cnf(f290,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/sandbox/benchmark/theBenchmark.p',cls_order__less__asym_H_0) ).
fof(f290_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)],[f290]) ).
fof(f290_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)],[f290_nnf]) ).
cnf(c290,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)],[f290_sk]) ).
cnf(f295,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(f295_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)],[f295]) ).
fof(f295_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)],[f295_nnf]) ).
cnf(c295,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)],[f295_sk]) ).
cnf(f372,axiom,
( ~ c_lessequals(c_Suc(V_n),V_m,tc_nat)
| ~ c_lessequals(V_m,V_n,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less__eq__eq_1) ).
fof(f372_nnf,plain,
! [V_m,V_n] :
( ~ c_lessequals(c_Suc(V_n),V_m,tc_nat)
| ~ c_lessequals(V_m,V_n,tc_nat) ),
inference(nnf_transformation,[status(thm)],[f372]) ).
fof(f372_sk,plain,
! [V_m,V_n] :
( ~ c_lessequals(c_Suc(V_n),V_m,tc_nat)
| ~ c_lessequals(V_m,V_n,tc_nat) ),
inference(skolemisation,[status(esa)],[f372_nnf]) ).
cnf(c372,plain,
( ~ c_lessequals(c_Suc(X1),X0,tc_nat)
| ~ c_lessequals(X0,X1,tc_nat) ),
inference(cnf_transformation,[status(esa)],[f372_sk]) ).
cnf(f391,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/sandbox/benchmark/theBenchmark.p',cls_atLeastLessThan__empty__iff2_0) ).
fof(f391_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)],[f391]) ).
fof(f391_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)],[f391_nnf]) ).
cnf(c391,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)],[f391_sk]) ).
cnf(f401,axiom,
( ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat)
| ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less__eq_1) ).
fof(f401_nnf,plain,
! [V_m,V_n] :
( ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat)
| ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ),
inference(nnf_transformation,[status(thm)],[f401]) ).
fof(f401_sk,plain,
! [V_m,V_n] :
( ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat)
| ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ),
inference(skolemisation,[status(esa)],[f401_nnf]) ).
cnf(c401,plain,
( ~ c_HOL_Oord__class_Oless(X1,c_Suc(X0),tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_nat) ),
inference(cnf_transformation,[status(esa)],[f401_sk]) ).
cnf(f432,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/sandbox/benchmark/theBenchmark.p',cls_not__psubset__empty_0) ).
fof(f432_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)],[f432]) ).
fof(f432_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)],[f432_nnf]) ).
cnf(c432,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)],[f432_sk]) ).
cnf(f488,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(f488_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)],[f488]) ).
fof(f488_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)],[f488_nnf]) ).
cnf(c488,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)],[f488_sk]) ).
cnf(f604,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(f604_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)],[f604]) ).
fof(f604_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)],[f604_nnf]) ).
cnf(c604,plain,
( ~ hBOOL(hAPP(X1,X2))
| c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Collect(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f604_sk]) ).
cnf(f607,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(f607_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)],[f607]) ).
fof(f607_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)],[f607_nnf]) ).
cnf(c607,plain,
( ~ hBOOL(hAPP(X0,X2))
| c_Collect(X0,X1) != c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) ),
inference(cnf_transformation,[status(esa)],[f607_sk]) ).
cnf(f608,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(f608_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)],[f608]) ).
fof(f608_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)],[f608_nnf]) ).
cnf(c608,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)],[f608_sk]) ).
cnf(f609,axiom,
c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_UNIV__not__empty_0) ).
fof(f609_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)],[f609]) ).
fof(f609_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)],[f609_nnf]) ).
cnf(c609,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)],[f609_sk]) ).
cnf(f718,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(f718_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)],[f718]) ).
fof(f718_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)],[f718_nnf]) ).
cnf(c718,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)],[f718_sk]) ).
cnf(f745,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(f745_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)],[f745]) ).
fof(f745_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)],[f745_nnf]) ).
cnf(c745,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)],[f745_sk]) ).
cnf(f770,axiom,
( ~ c_Fun_Oinj__on(V_f,c_Set_Oinsert(V_a,V_A,T_a),T_a,T_b)
| ~ hBOOL(c_in(hAPP(V_f,V_a),c_Set_Oimage(V_f,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/sandbox/benchmark/theBenchmark.p',cls_inj__on__insert_1) ).
fof(f770_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)
| ~ hBOOL(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)],[f770]) ).
fof(f770_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)
| ~ hBOOL(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)],[f770_nnf]) ).
cnf(c770,plain,
( ~ c_Fun_Oinj__on(X0,c_Set_Oinsert(X1,X2,X3),X3,X4)
| ~ hBOOL(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)],[f770_sk]) ).
cnf(f817,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(f817_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)],[f817]) ).
fof(f817_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)],[f817_nnf]) ).
cnf(c817,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f817_sk]) ).
cnf(f819,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(f819_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)],[f819]) ).
fof(f819_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)],[f819_nnf]) ).
cnf(c819,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f819_sk]) ).
cnf(f820,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(f820_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)],[f820]) ).
fof(f820_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)],[f820_nnf]) ).
cnf(c820,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f820_sk]) ).
cnf(f821,axiom,
c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Set_Oinsert(V_a,V_A,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_empty__not__insert_0) ).
fof(f821_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)],[f821]) ).
fof(f821_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)],[f821_nnf]) ).
cnf(c821,plain,
c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Set_Oinsert(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f821_sk]) ).
cnf(f829,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(f829_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)],[f829]) ).
fof(f829_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)],[f829_nnf]) ).
cnf(c829,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f829_sk]) ).
cnf(f835,axiom,
c_Set_Oinsert(V_a,V_A,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_insert__not__empty_0) ).
fof(f835_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)],[f835]) ).
fof(f835_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)],[f835_nnf]) ).
cnf(c835,plain,
c_Set_Oinsert(X0,X1,X2) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
inference(cnf_transformation,[status(esa)],[f835_sk]) ).
cnf(f848,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(f848_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)],[f848]) ).
fof(f848_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)],[f848_nnf]) ).
cnf(c848,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)],[f848_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c60,c61,c62,c64,c65,c66,c119,c123,c124,c146,c148,c186,c232,c234,c236,c238,c239,c286,c287,c289,c290,c295,c372,c391,c401,c432,c488,c604,c607,c608,c609,c718,c745,c770,c817,c819,c820,c821,c829,c835,c848,c863]) ).
cnf(g0_0,plain,
sF0 != false,
inference(rw,[status(thm)],[goal_0,t207]) ).
cnf(g0_1,plain,
sF0 != sF0,
inference(rw,[status(thm)],[g0_0,t2900]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV879-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n011.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Thu Sep 24 21:13:14 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 28.11/4.12 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 28.11/4.12 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------