%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV857-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 : n019.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:15 PM UTC 2026
% Result : Unsatisfiable 4.65s 3.60s
% Output : Proof 4.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 39
% Syntax : Number of formulae : 189 ( 89 unt; 0 def)
% Number of atoms : 345 ( 78 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 438 ( 282 ~; 156 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 22 ( 22 usr; 8 con; 0-4 aty)
% Number of variables : 415 ( 53 sgn 186 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f547,negated_conjecture,
( ~ hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),V_xb),v_Ga))
| c_Hoare__Mirabelle_Otriple__valid(v_x,V_xb,t_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f547_nnf,plain,
! [V_xb] :
( ~ hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),V_xb),v_Ga))
| c_Hoare__Mirabelle_Otriple__valid(v_x,V_xb,t_a) ),
inference(nnf_transformation,[status(thm)],[f547]) ).
fof(f547_sk,plain,
! [V_xb] :
( ~ hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),V_xb),v_Ga))
| c_Hoare__Mirabelle_Otriple__valid(v_x,V_xb,t_a) ),
inference(skolemisation,[status(esa)],[f547_nnf]) ).
cnf(c547,plain,
( ~ hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),X0),v_Ga))
| c_Hoare__Mirabelle_Otriple__valid(v_x,X0,t_a) ),
inference(cnf_transformation,[status(esa)],[f547_sk]) ).
cnf(t53,plain,
ifeq(hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),X1),v_Ga)),true,c_Hoare__Mirabelle_Otriple__valid(v_x,X1,t_a),true) = true,
inference(equality_encoding,[status(esa)],[c547]) ).
cnf(t179,plain,
ifeq(hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),X1),v_Ga)),true,c_Hoare__Mirabelle_Otriple__valid(v_x,X1,t_a),true) = true,
inference(orient,[status(thm)],[t53]) ).
cnf(f541,axiom,
( ~ hBOOL(hAPP(V_S,V_x))
| hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_S)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mem__def_1) ).
fof(f541_nnf,plain,
! [T_a,V_x,V_S] :
( ~ hBOOL(hAPP(V_S,V_x))
| hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_S)) ),
inference(nnf_transformation,[status(thm)],[f541]) ).
fof(f541_sk,plain,
! [T_a,V_x,V_S] :
( ~ hBOOL(hAPP(V_S,V_x))
| hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_S)) ),
inference(skolemisation,[status(esa)],[f541_nnf]) ).
cnf(c541,plain,
( ~ hBOOL(hAPP(X2,X1))
| hBOOL(hAPP(hAPP(c_in(X0),X1),X2)) ),
inference(cnf_transformation,[status(esa)],[f541_sk]) ).
cnf(t43,plain,
ifeq(hBOOL(hAPP(X1,X2)),true,hBOOL(hAPP(hAPP(c_in(X3),X2),X1)),true) = true,
inference(equality_encoding,[status(esa)],[c541]) ).
cnf(t147,plain,
ifeq(hBOOL(hAPP(X1,X2)),true,hBOOL(hAPP(hAPP(c_in(X3),X2),X1)),true) = true,
inference(orient,[status(thm)],[t43]) ).
cnf(f214,axiom,
( ~ hBOOL(hAPP(V_A,V_x))
| hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),V_x)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_sup1CI_1) ).
fof(f214_nnf,plain,
! [V_A,V_B,T_a,V_x] :
( ~ hBOOL(hAPP(V_A,V_x))
| hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),V_x)) ),
inference(nnf_transformation,[status(thm)],[f214]) ).
fof(f214_sk,plain,
! [V_A,V_B,T_a,V_x] :
( ~ hBOOL(hAPP(V_A,V_x))
| hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)),V_x)) ),
inference(skolemisation,[status(esa)],[f214_nnf]) ).
cnf(c214,plain,
( ~ hBOOL(hAPP(X0,X3))
| hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X0,X1,tc_fun(X2,tc_bool)),X3)) ),
inference(cnf_transformation,[status(esa)],[f214_sk]) ).
cnf(t55,plain,
ifeq(hBOOL(hAPP(X1,X2)),true,hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X1,X3,tc_fun(X4,tc_bool)),X2)),true) = true,
inference(equality_encoding,[status(esa)],[c214]) ).
cnf(t153,plain,
ifeq(hBOOL(hAPP(X1,X2)),true,hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(X1,X3,tc_fun(X4,tc_bool)),X2)),true) = true,
inference(orient,[status(thm)],[t55]) ).
cnf(f542,axiom,
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_S))
| hBOOL(hAPP(V_S,V_x)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mem__def_0) ).
fof(f542_nnf,plain,
! [V_S,V_x,T_a] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_S))
| hBOOL(hAPP(V_S,V_x)) ),
inference(nnf_transformation,[status(thm)],[f542]) ).
fof(f542_sk,plain,
! [V_S,V_x,T_a] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_S))
| hBOOL(hAPP(V_S,V_x)) ),
inference(skolemisation,[status(esa)],[f542_nnf]) ).
cnf(c542,plain,
( ~ hBOOL(hAPP(hAPP(c_in(X2),X1),X0))
| hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f542_sk]) ).
cnf(t44,plain,
ifeq(hBOOL(hAPP(hAPP(c_in(X1),X2),X3)),true,hBOOL(hAPP(X3,X2)),true) = true,
inference(equality_encoding,[status(esa)],[c542]) ).
cnf(t162,plain,
ifeq(hBOOL(hAPP(hAPP(c_in(X1),X2),X3)),true,hBOOL(hAPP(X3,X2)),true) = true,
inference(orient,[status(thm)],[t44]) ).
cnf(f545,negated_conjecture,
hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_tsa)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f545_nnf,plain,
hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_tsa)),
inference(nnf_transformation,[status(thm)],[f545]) ).
cnf(c545,plain,
hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_tsa)),
inference(cnf_transformation,[status(esa)],[f545_nnf]) ).
cnf(t19,plain,
hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_tsa)) = true,
inference(equality_encoding,[status(esa)],[c545]) ).
cnf(t385,plain,
hBOOL(hAPP(hAPP(c_in(tc_Hoare__Mirabelle_Otriple(t_a)),v_xa),v_tsa)) = true,
inference(orient,[status(thm)],[t19]) ).
cnf(t394,plain,
true = ifeq(true,true,hBOOL(hAPP(v_tsa,v_xa)),true),
inference(cp,[status(thm)],[t162,t385]) ).
cnf(t9,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t100,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t9]) ).
cnf(t1172,plain,
true = hBOOL(hAPP(v_tsa,v_xa)),
inference(step,[status(thm)],[t394,t100]) ).
cnf(t805,plain,
hBOOL(hAPP(v_tsa,v_xa)) = true,
inference(orient,[status(thm)],[t1172]) ).
cnf(t811,plain,
true = ifeq(true,true,hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(v_tsa,X1,tc_fun(X2,tc_bool)),v_xa)),true),
inference(cp,[status(thm)],[t153,t805]) ).
cnf(t1205,plain,
true = hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(v_tsa,X1,tc_fun(X2,tc_bool)),v_xa)),
inference(step,[status(thm)],[t811,t100]) ).
cnf(t1104,plain,
hBOOL(hAPP(c_Lattices_Oupper__semilattice__class_Osup(v_tsa,X1,tc_fun(X2,tc_bool)),v_xa)) = true,
inference(orient,[status(thm)],[t1205]) ).
cnf(f446,axiom,
( ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)) = V_B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Un__absorb1_0) ).
fof(f446_nnf,plain,
! [V_A,V_B,T_a] :
( ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)) = V_B ),
inference(nnf_transformation,[status(thm)],[f446]) ).
fof(f446_sk,plain,
! [V_A,V_B,T_a] :
( ~ c_lessequals(V_A,V_B,tc_fun(T_a,tc_bool))
| c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,tc_fun(T_a,tc_bool)) = V_B ),
inference(skolemisation,[status(esa)],[f446_nnf]) ).
cnf(c446,plain,
( ~ c_lessequals(X0,X1,tc_fun(X2,tc_bool))
| c_Lattices_Oupper__semilattice__class_Osup(X0,X1,tc_fun(X2,tc_bool)) = X1 ),
inference(cnf_transformation,[status(esa)],[f446_sk]) ).
cnf(t51,plain,
ifeq(c_lessequals(X1,X2,tc_fun(X3,tc_bool)),true,c_Lattices_Oupper__semilattice__class_Osup(X1,X2,tc_fun(X3,tc_bool)),X2) = X2,
inference(equality_encoding,[status(esa)],[c446]) ).
cnf(t101,plain,
ifeq(c_lessequals(X1,X2,tc_fun(X3,tc_bool)),true,c_Lattices_Oupper__semilattice__class_Osup(X1,X2,tc_fun(X3,tc_bool)),X2) = X2,
inference(orient,[status(thm)],[t51]) ).
cnf(f544,negated_conjecture,
c_lessequals(v_tsa,v_Ga,tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f544_nnf,plain,
c_lessequals(v_tsa,v_Ga,tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),
inference(nnf_transformation,[status(thm)],[f544]) ).
cnf(c544,plain,
c_lessequals(v_tsa,v_Ga,tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),
inference(cnf_transformation,[status(esa)],[f544_nnf]) ).
cnf(t16,plain,
c_lessequals(v_tsa,v_Ga,tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)) = true,
inference(equality_encoding,[status(esa)],[c544]) ).
cnf(t357,plain,
c_lessequals(v_tsa,v_Ga,tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)) = true,
inference(orient,[status(thm)],[t16]) ).
cnf(t358,plain,
v_Ga = ifeq(true,true,c_Lattices_Oupper__semilattice__class_Osup(v_tsa,v_Ga,tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),v_Ga),
inference(cp,[status(thm)],[t101,t357]) ).
cnf(t1179,plain,
v_Ga = c_Lattices_Oupper__semilattice__class_Osup(v_tsa,v_Ga,tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)),
inference(step,[status(thm)],[t358,t100]) ).
cnf(t848,plain,
c_Lattices_Oupper__semilattice__class_Osup(v_tsa,v_Ga,tc_fun(tc_Hoare__Mirabelle_Otriple(t_a),tc_bool)) = v_Ga,
inference(orient,[status(thm)],[t1179]) ).
cnf(t1105,plain,
true = hBOOL(hAPP(v_Ga,v_xa)),
inference(cp,[status(thm)],[t1104,t848]) ).
cnf(t1115,plain,
hBOOL(hAPP(v_Ga,v_xa)) = true,
inference(orient,[status(thm)],[t1105]) ).
cnf(t1122,plain,
true = ifeq(true,true,hBOOL(hAPP(hAPP(c_in(X1),v_xa),v_Ga)),true),
inference(cp,[status(thm)],[t147,t1115]) ).
cnf(t1206,plain,
true = hBOOL(hAPP(hAPP(c_in(X1),v_xa),v_Ga)),
inference(step,[status(thm)],[t1122,t100]) ).
cnf(t1125,plain,
hBOOL(hAPP(hAPP(c_in(X1),v_xa),v_Ga)) = true,
inference(orient,[status(thm)],[t1206]) ).
cnf(t1137,plain,
true = ifeq(true,true,c_Hoare__Mirabelle_Otriple__valid(v_x,v_xa,t_a),true),
inference(cp,[status(thm)],[t179,t1125]) ).
cnf(t1207,plain,
true = c_Hoare__Mirabelle_Otriple__valid(v_x,v_xa,t_a),
inference(step,[status(thm)],[t1137,t100]) ).
cnf(f546,negated_conjecture,
~ c_Hoare__Mirabelle_Otriple__valid(v_x,v_xa,t_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f546_nnf,plain,
~ c_Hoare__Mirabelle_Otriple__valid(v_x,v_xa,t_a),
inference(nnf_transformation,[status(thm)],[f546]) ).
fof(f546_sk,plain,
~ c_Hoare__Mirabelle_Otriple__valid(v_x,v_xa,t_a),
inference(skolemisation,[status(esa)],[f546_nnf]) ).
cnf(c546,plain,
~ c_Hoare__Mirabelle_Otriple__valid(v_x,v_xa,t_a),
inference(cnf_transformation,[status(esa)],[f546_sk]) ).
cnf(t6,plain,
c_Hoare__Mirabelle_Otriple__valid(v_x,v_xa,t_a) = false,
inference(equality_encoding,[status(esa)],[c546]) ).
cnf(t797,plain,
c_Hoare__Mirabelle_Otriple__valid(v_x,v_xa,t_a) = false,
inference(orient,[status(thm)],[t6]) ).
cnf(t1208,plain,
true = false,
inference(step,[status(thm)],[t1207,t797]) ).
cnf(t1147,plain,
false = true,
inference(orient,[status(thm)],[t1208]) ).
cnf(f59,axiom,
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_SetInterval_Oord__class_OatLeastLessThan(V_a,V_b,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_atLeastLessThan__empty__iff2_0) ).
fof(f59_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)],[f59]) ).
fof(f59_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)],[f59_nnf]) ).
cnf(c59,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)],[f59_sk]) ).
cnf(f113,axiom,
~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ex__in__conv_0) ).
fof(f113_nnf,plain,
! [T_a,V_x] : ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
inference(nnf_transformation,[status(thm)],[f113]) ).
fof(f113_sk,plain,
! [T_a,V_x] : ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
inference(skolemisation,[status(esa)],[f113_nnf]) ).
cnf(c113,plain,
~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
inference(cnf_transformation,[status(esa)],[f113_sk]) ).
cnf(f115,axiom,
~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_empty__iff_0) ).
fof(f115_nnf,plain,
! [T_a,V_c] : ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
inference(nnf_transformation,[status(thm)],[f115]) ).
fof(f115_sk,plain,
! [T_a,V_c] : ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
inference(skolemisation,[status(esa)],[f115_nnf]) ).
cnf(c115,plain,
~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
inference(cnf_transformation,[status(esa)],[f115_sk]) ).
cnf(f116,axiom,
~ hBOOL(hAPP(hAPP(c_in(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_emptyE_0) ).
fof(f116_nnf,plain,
! [T_a,V_a] : ~ hBOOL(hAPP(hAPP(c_in(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
inference(nnf_transformation,[status(thm)],[f116]) ).
fof(f116_sk,plain,
! [T_a,V_a] : ~ hBOOL(hAPP(hAPP(c_in(T_a),V_a),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)))),
inference(skolemisation,[status(esa)],[f116_nnf]) ).
cnf(c116,plain,
~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)))),
inference(cnf_transformation,[status(esa)],[f116_sk]) ).
cnf(f122,axiom,
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool))))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),V_B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_DiffE_1) ).
fof(f122_nnf,plain,
! [T_a,V_c,V_B,V_A] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool))))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),V_B)) ),
inference(nnf_transformation,[status(thm)],[f122]) ).
fof(f122_sk,plain,
! [T_a,V_c,V_B,V_A] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool))))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),V_B)) ),
inference(skolemisation,[status(esa)],[f122_nnf]) ).
cnf(c122,plain,
( ~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_HOL_Ominus__class_Ominus(X3,X2,tc_fun(X0,tc_bool))))
| ~ hBOOL(hAPP(hAPP(c_in(X0),X1),X2)) ),
inference(cnf_transformation,[status(esa)],[f122_sk]) ).
cnf(f125,axiom,
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool))))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),V_A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ComplD_0) ).
fof(f125_nnf,plain,
! [T_a,V_c,V_A] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool))))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),V_A)) ),
inference(nnf_transformation,[status(thm)],[f125]) ).
fof(f125_sk,plain,
! [T_a,V_c,V_A] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool))))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_c),V_A)) ),
inference(skolemisation,[status(esa)],[f125_nnf]) ).
cnf(c125,plain,
( ~ hBOOL(hAPP(hAPP(c_in(X0),X1),c_HOL_Ouminus__class_Ouminus(X2,tc_fun(X0,tc_bool))))
| ~ hBOOL(hAPP(hAPP(c_in(X0),X1),X2)) ),
inference(cnf_transformation,[status(esa)],[f125_sk]) ).
cnf(f132,axiom,
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))))
| ~ hBOOL(hAPP(V_P,V_x)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_bex__empty_0) ).
fof(f132_nnf,plain,
! [V_P,V_x,T_a] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))))
| ~ hBOOL(hAPP(V_P,V_x)) ),
inference(nnf_transformation,[status(thm)],[f132]) ).
fof(f132_sk,plain,
! [V_P,V_x,T_a] :
( ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))))
| ~ hBOOL(hAPP(V_P,V_x)) ),
inference(skolemisation,[status(esa)],[f132_nnf]) ).
cnf(c132,plain,
( ~ hBOOL(hAPP(hAPP(c_in(X2),X1),c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool))))
| ~ hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f132_sk]) ).
cnf(f186,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(f186_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)],[f186]) ).
fof(f186_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)],[f186_nnf]) ).
cnf(c186,plain,
c_Set_Oinsert(X0,X1,X2) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
inference(cnf_transformation,[status(esa)],[f186_sk]) ).
cnf(f211,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(f211_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)],[f211]) ).
fof(f211_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)],[f211_nnf]) ).
cnf(c211,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)],[f211_sk]) ).
cnf(f234,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(f234_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)],[f234]) ).
fof(f234_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)],[f234_nnf]) ).
cnf(c234,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f234_sk]) ).
cnf(f239,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))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_A))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_disjoint__iff__not__equal_0) ).
fof(f239_nnf,plain,
! [T_a,V_x,V_B,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))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_A))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_B)) ),
inference(nnf_transformation,[status(thm)],[f239]) ).
fof(f239_sk,plain,
! [T_a,V_x,V_B,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))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_A))
| ~ hBOOL(hAPP(hAPP(c_in(T_a),V_x),V_B)) ),
inference(skolemisation,[status(esa)],[f239_nnf]) ).
cnf(c239,plain,
( c_Lattices_Olower__semilattice__class_Oinf(X3,X2,tc_fun(X0,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))
| ~ hBOOL(hAPP(hAPP(c_in(X0),X1),X3))
| ~ hBOOL(hAPP(hAPP(c_in(X0),X1),X2)) ),
inference(cnf_transformation,[status(esa)],[f239_sk]) ).
cnf(f289,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(f289_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)],[f289]) ).
fof(f289_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)],[f289_nnf]) ).
cnf(c289,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ c_lessequals(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f289_sk]) ).
cnf(f291,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(f291_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)],[f291]) ).
fof(f291_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)],[f291_nnf]) ).
cnf(c291,plain,
( ~ c_lessequals(X2,X1,X0)
| ~ c_HOL_Oord__class_Oless(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f291_sk]) ).
cnf(f293,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(f293_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)],[f293]) ).
fof(f293_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)],[f293_nnf]) ).
cnf(c293,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f293_sk]) ).
cnf(f295,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(f295_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)],[f295]) ).
fof(f295_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)],[f295_nnf]) ).
cnf(c295,plain,
( ~ c_HOL_Oord__class_Oless(X2,X1,X0)
| ~ c_lessequals(X1,X2,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f295_sk]) ).
cnf(f324,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(f324_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)],[f324]) ).
fof(f324_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)],[f324_nnf]) ).
cnf(c324,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)],[f324_sk]) ).
cnf(f345,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(f345_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)],[f345]) ).
fof(f345_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)],[f345_nnf]) ).
cnf(c345,plain,
~ c_HOL_Oord__class_Oless(X0,X0,tc_fun(X1,tc_bool)),
inference(cnf_transformation,[status(esa)],[f345_sk]) ).
cnf(f346,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(f346_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)],[f346]) ).
fof(f346_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)],[f346_nnf]) ).
cnf(c346,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f346_sk]) ).
cnf(f347,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(f347_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)],[f347]) ).
fof(f347_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)],[f347_nnf]) ).
cnf(c347,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(esa)],[f347_sk]) ).
cnf(f348,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(f348_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)],[f348]) ).
fof(f348_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)],[f348_nnf]) ).
cnf(c348,plain,
( ~ c_HOL_Oord__class_Oless(X1,X1,X0)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(esa)],[f348_sk]) ).
cnf(f374,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(f374_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)],[f374]) ).
fof(f374_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)],[f374_nnf]) ).
cnf(c374,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)],[f374_sk]) ).
cnf(f375,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(f375_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)],[f375]) ).
fof(f375_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)],[f375_nnf]) ).
cnf(c375,plain,
c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Set_Oinsert(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f375_sk]) ).
cnf(f397,axiom,
c_Suc(V_n) != V_n,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__n__not__n_0) ).
fof(f397_nnf,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(nnf_transformation,[status(thm)],[f397]) ).
fof(f397_sk,plain,
! [V_n] : c_Suc(V_n) != V_n,
inference(skolemisation,[status(esa)],[f397_nnf]) ).
cnf(c397,plain,
c_Suc(X0) != X0,
inference(cnf_transformation,[status(esa)],[f397_sk]) ).
cnf(f398,axiom,
V_n != c_Suc(V_n),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_n__not__Suc__n_0) ).
fof(f398_nnf,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(nnf_transformation,[status(thm)],[f398]) ).
fof(f398_sk,plain,
! [V_n] : V_n != c_Suc(V_n),
inference(skolemisation,[status(esa)],[f398_nnf]) ).
cnf(c398,plain,
X0 != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f398_sk]) ).
cnf(f405,axiom,
( ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a)
| c_SetInterval_Oord__class_OatLeastLessThan(V_a,V_b,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_atLeastLessThan__empty__iff_0) ).
fof(f405_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)],[f405]) ).
fof(f405_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)],[f405_nnf]) ).
cnf(c405,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)],[f405_sk]) ).
cnf(f410,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(f410_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)],[f410]) ).
fof(f410_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)],[f410_nnf]) ).
cnf(c410,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)],[f410_sk]) ).
cnf(f440,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(f440_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)],[f440]) ).
fof(f440_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)],[f440_nnf]) ).
cnf(c440,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)],[f440_sk]) ).
cnf(f441,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(f441_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)],[f441]) ).
fof(f441_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)],[f441_nnf]) ).
cnf(c441,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)],[f441_sk]) ).
cnf(f442,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(f442_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)],[f442]) ).
fof(f442_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)],[f442_nnf]) ).
cnf(c442,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)],[f442_sk]) ).
cnf(f443,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(f443_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)],[f443]) ).
fof(f443_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)],[f443_nnf]) ).
cnf(c443,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)],[f443_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c59,c113,c115,c116,c122,c125,c132,c186,c211,c234,c239,c289,c291,c293,c295,c324,c345,c346,c347,c348,c374,c375,c397,c398,c405,c410,c440,c441,c442,c443,c546]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t1147]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV857-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.36 % Computer : n019.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 21:11:20 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 4.65/3.60 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.65/3.60 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------