%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV885-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 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 : Thu Sep 24 02:49:43 PM UTC 2026
% Result : Unsatisfiable 45.69s 6.44s
% Output : CNFRefutation 40.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 28
% Syntax : Number of formulae : 100 ( 58 unt; 0 def)
% Number of atoms : 151 ( 68 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 102 ( 51 ~; 51 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 21 ( 21 usr; 9 con; 0-4 aty)
% Number of variables : 145 ( 145 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f34,axiom,
! [V_m] : ~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f100,axiom,
! [V_A,V_a,V_B,T_a] : c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_a,V_B,T_a),tc_fun(T_a,tc_bool)) = c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),c_Set_Oinsert(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f154,axiom,
c_HOL_Oone__class_Oone(tc_nat) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f357,axiom,
! [V_A,T_a] :
( V_A = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ c_Finite__Set_Ofinite(V_A,T_a)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Finite__Set_Ocard(V_A,T_a),tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f566,axiom,
! [T_a,V_x,V_y] :
( ~ c_lessequals(V_x,V_y,T_a)
| c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a) = V_x
| ~ class_Lattices_Olower__semilattice(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f606,axiom,
! [V_A,V_B,T_a] :
( ~ c_Finite__Set_Ofinite(V_A,T_a)
| c_Finite__Set_Ofinite(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f607,axiom,
! [V_F,V_G,T_a] :
( ~ c_Finite__Set_Ofinite(V_G,T_a)
| c_Finite__Set_Ofinite(c_Lattices_Olower__semilattice__class_Oinf(V_F,V_G,tc_fun(T_a,tc_bool)),T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f608,axiom,
! [V_F,V_G,T_a] :
( ~ c_Finite__Set_Ofinite(V_F,T_a)
| c_Finite__Set_Ofinite(c_Lattices_Olower__semilattice__class_Oinf(V_F,V_G,tc_fun(T_a,tc_bool)),T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f630,axiom,
! [V_m,V_n] : c_HOL_Oplus__class_Oplus(c_Suc(V_m),V_n,tc_nat) = c_Suc(c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f631,axiom,
! [V_m,V_n] : c_HOL_Oplus__class_Oplus(V_m,c_Suc(V_n),tc_nat) = c_Suc(c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f636,axiom,
! [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) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f695,axiom,
! [V_n,V_m] :
( c_HOL_Oord__class_Oless(V_m,V_n,tc_nat)
| c_HOL_Oplus__class_Oplus(V_n,c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat),tc_nat) = V_m ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f737,axiom,
! [V_A,V_B,T_a] :
( ~ c_Finite__Set_Ofinite(c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)
| c_Finite__Set_Ocard(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a) = c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(V_A,T_a),c_Finite__Set_Ocard(c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,tc_fun(T_a,tc_bool)),T_a),tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f787,axiom,
! [V_A,T_a] :
( V_A = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ c_Finite__Set_Ofinite(V_A,T_a)
| c_Finite__Set_Ocard(V_A,T_a) != c_HOL_Ozero__class_Ozero(tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f847,axiom,
! [V_n] : c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f853,axiom,
! [V_n,V_m] : c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(V_n,V_m,tc_nat),V_n,tc_nat) = V_m,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f879,axiom,
! [V_m,V_n] :
( ~ c_lessequals(V_m,V_n,tc_nat)
| c_HOL_Oord__class_Oless(V_m,c_Suc(V_n),tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f889,axiom,
! [V_x,V_A,T_a] :
( ~ c_Finite__Set_Ofinite(V_A,T_a)
| c_Finite__Set_Ocard(c_Set_Oinsert(V_x,V_A,T_a),T_a) = c_Suc(c_Finite__Set_Ocard(c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f951,axiom,
! [V_x,V_xa,T_a] :
( c_Finite__Set_Ocard(V_xa,T_a) = c_HOL_Ozero__class_Ozero(tc_nat)
| c_Finite__Set_Ocard(c_Set_Oinsert(V_x,V_xa,T_a),T_a) = c_Suc(c_Finite__Set_Ocard(V_xa,T_a))
| c_in(V_x,V_xa,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f993,axiom,
! [V_h,V_F,T_a,T_b] :
( ~ c_Finite__Set_Ofinite(V_F,T_a)
| c_Finite__Set_Ofinite(c_Set_Oimage(V_h,V_F,T_a,T_b),T_b) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1056,negated_conjecture,
c_Finite__Set_Ofinite(v_U,tc_Com_Opname),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1057,negated_conjecture,
c_lessequals(v_G,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1058,negated_conjecture,
c_lessequals(c_Suc(v_na),c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1059,negated_conjecture,
c_Finite__Set_Ocard(v_G,t_a) = c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),c_Suc(v_na),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1061,negated_conjecture,
~ c_in(hAPP(v_mgt__call,v_pn),v_G,t_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1062,negated_conjecture,
c_Finite__Set_Ocard(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a),t_a) != c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),v_na,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1064,axiom,
! [T_2,T_1] :
( ~ class_Lattices_Olattice(T_1)
| class_Lattices_Olower__semilattice(tc_fun(T_2,T_1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1115,axiom,
class_Lattices_Olattice(tc_bool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1175,plain,
! [X0] : ~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f1284,plain,
! [X0,X1,X2,X3] : c_HOL_Ominus__class_Ominus(X0,c_Set_Oinsert(X1,X2,X3),tc_fun(X3,tc_bool)) = c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(X0,X2,tc_fun(X3,tc_bool)),c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(X3,tc_bool)),X3),tc_fun(X3,tc_bool)),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f1376,plain,
c_HOL_Oone__class_Oone(tc_nat) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f1709,plain,
! [X0,X1] :
( X0 = c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool))
| ~ c_Finite__Set_Ofinite(X0,X1)
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Finite__Set_Ocard(X0,X1),tc_nat) ),
inference(cnf_transformation,[status(thm)],[f357]) ).
fof(f2047,plain,
! [X0,X1,X2] :
( ~ c_lessequals(X1,X2,X0)
| c_Lattices_Olower__semilattice__class_Oinf(X1,X2,X0) = X1
| ~ class_Lattices_Olower__semilattice(X0) ),
inference(cnf_transformation,[status(thm)],[f566]) ).
fof(f2112,plain,
! [V_A,T_a] :
( ~ c_Finite__Set_Ofinite(V_A,T_a)
| ! [V_B] : c_Finite__Set_Ofinite(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a) ),
inference(miniscoping,[status(thm)],[f606]) ).
fof(f2113,plain,
! [X0,X1,X2] :
( ~ c_Finite__Set_Ofinite(X0,X2)
| c_Finite__Set_Ofinite(c_HOL_Ominus__class_Ominus(X0,X1,tc_fun(X2,tc_bool)),X2) ),
inference(cnf_transformation,[status(thm)],[f2112]) ).
fof(f2114,plain,
! [V_G,T_a] :
( ~ c_Finite__Set_Ofinite(V_G,T_a)
| ! [V_F] : c_Finite__Set_Ofinite(c_Lattices_Olower__semilattice__class_Oinf(V_F,V_G,tc_fun(T_a,tc_bool)),T_a) ),
inference(miniscoping,[status(thm)],[f607]) ).
fof(f2115,plain,
! [X0,X1,X2] :
( ~ c_Finite__Set_Ofinite(X1,X2)
| c_Finite__Set_Ofinite(c_Lattices_Olower__semilattice__class_Oinf(X0,X1,tc_fun(X2,tc_bool)),X2) ),
inference(cnf_transformation,[status(thm)],[f2114]) ).
fof(f2116,plain,
! [V_F,T_a] :
( ~ c_Finite__Set_Ofinite(V_F,T_a)
| ! [V_G] : c_Finite__Set_Ofinite(c_Lattices_Olower__semilattice__class_Oinf(V_F,V_G,tc_fun(T_a,tc_bool)),T_a) ),
inference(miniscoping,[status(thm)],[f608]) ).
fof(f2117,plain,
! [X0,X1,X2] :
( ~ c_Finite__Set_Ofinite(X0,X2)
| c_Finite__Set_Ofinite(c_Lattices_Olower__semilattice__class_Oinf(X0,X1,tc_fun(X2,tc_bool)),X2) ),
inference(cnf_transformation,[status(thm)],[f2116]) ).
fof(f2147,plain,
! [X0,X1] : c_HOL_Oplus__class_Oplus(c_Suc(X0),X1,tc_nat) = c_Suc(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat)),
inference(cnf_transformation,[status(thm)],[f630]) ).
fof(f2148,plain,
! [X0,X1] : c_HOL_Oplus__class_Oplus(X0,c_Suc(X1),tc_nat) = c_Suc(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat)),
inference(cnf_transformation,[status(thm)],[f631]) ).
fof(f2153,plain,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(X1,c_Suc(X0),tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_nat) ),
inference(cnf_transformation,[status(thm)],[f636]) ).
fof(f2243,plain,
! [X0,X1] :
( c_HOL_Oord__class_Oless(X1,X0,tc_nat)
| c_HOL_Oplus__class_Oplus(X0,c_HOL_Ominus__class_Ominus(X1,X0,tc_nat),tc_nat) = X1 ),
inference(cnf_transformation,[status(thm)],[f695]) ).
fof(f2312,plain,
! [X0,X1,X2] :
( ~ c_Finite__Set_Ofinite(c_Lattices_Olower__semilattice__class_Oinf(X0,X1,tc_fun(X2,tc_bool)),X2)
| c_Finite__Set_Ocard(c_HOL_Ominus__class_Ominus(X0,X1,tc_fun(X2,tc_bool)),X2) = c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(X0,X2),c_Finite__Set_Ocard(c_Lattices_Olower__semilattice__class_Oinf(X0,X1,tc_fun(X2,tc_bool)),X2),tc_nat) ),
inference(cnf_transformation,[status(thm)],[f737]) ).
fof(f2391,plain,
! [X0,X1] :
( X0 = c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool))
| ~ c_Finite__Set_Ofinite(X0,X1)
| c_Finite__Set_Ocard(X0,X1) != c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(cnf_transformation,[status(thm)],[f787]) ).
fof(f2485,plain,
! [X0] : c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(thm)],[f847]) ).
fof(f2491,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X0,tc_nat) = X1,
inference(cnf_transformation,[status(thm)],[f853]) ).
fof(f2528,plain,
! [X0,X1] :
( ~ c_lessequals(X0,X1,tc_nat)
| c_HOL_Oord__class_Oless(X0,c_Suc(X1),tc_nat) ),
inference(cnf_transformation,[status(thm)],[f879]) ).
fof(f2542,plain,
! [V_A,T_a] :
( ~ c_Finite__Set_Ofinite(V_A,T_a)
| ! [V_x] : c_Finite__Set_Ocard(c_Set_Oinsert(V_x,V_A,T_a),T_a) = c_Suc(c_Finite__Set_Ocard(c_HOL_Ominus__class_Ominus(V_A,c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),tc_fun(T_a,tc_bool)),T_a)) ),
inference(miniscoping,[status(thm)],[f889]) ).
fof(f2543,plain,
! [X0,X1,X2] :
( ~ c_Finite__Set_Ofinite(X1,X2)
| c_Finite__Set_Ocard(c_Set_Oinsert(X0,X1,X2),X2) = c_Suc(c_Finite__Set_Ocard(c_HOL_Ominus__class_Ominus(X1,c_Set_Oinsert(X0,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2),tc_fun(X2,tc_bool)),X2)) ),
inference(cnf_transformation,[status(thm)],[f2542]) ).
fof(f2635,plain,
! [V_xa,T_a] :
( c_Finite__Set_Ocard(V_xa,T_a) = c_HOL_Ozero__class_Ozero(tc_nat)
| ! [V_x] :
( c_Finite__Set_Ocard(c_Set_Oinsert(V_x,V_xa,T_a),T_a) = c_Suc(c_Finite__Set_Ocard(V_xa,T_a))
| c_in(V_x,V_xa,T_a) ) ),
inference(miniscoping,[status(thm)],[f951]) ).
fof(f2636,plain,
! [X0,X1,X2] :
( c_Finite__Set_Ocard(X1,X2) = c_HOL_Ozero__class_Ozero(tc_nat)
| c_Finite__Set_Ocard(c_Set_Oinsert(X0,X1,X2),X2) = c_Suc(c_Finite__Set_Ocard(X1,X2))
| c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f2635]) ).
fof(f2703,plain,
! [V_F,T_a] :
( ~ c_Finite__Set_Ofinite(V_F,T_a)
| ! [V_h,T_b] : c_Finite__Set_Ofinite(c_Set_Oimage(V_h,V_F,T_a,T_b),T_b) ),
inference(miniscoping,[status(thm)],[f993]) ).
fof(f2704,plain,
! [X0,X1,X2,X3] :
( ~ c_Finite__Set_Ofinite(X1,X2)
| c_Finite__Set_Ofinite(c_Set_Oimage(X0,X1,X2,X3),X3) ),
inference(cnf_transformation,[status(thm)],[f2703]) ).
fof(f2802,plain,
c_Finite__Set_Ofinite(v_U,tc_Com_Opname),
inference(cnf_transformation,[status(thm)],[f1056]) ).
fof(f2803,plain,
c_lessequals(v_G,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool)),
inference(cnf_transformation,[status(thm)],[f1057]) ).
fof(f2804,plain,
c_lessequals(c_Suc(v_na),c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),tc_nat),
inference(cnf_transformation,[status(thm)],[f1058]) ).
fof(f2805,plain,
c_Finite__Set_Ocard(v_G,t_a) = c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),c_Suc(v_na),tc_nat),
inference(cnf_transformation,[status(thm)],[f1059]) ).
fof(f2807,plain,
~ c_in(hAPP(v_mgt__call,v_pn),v_G,t_a),
inference(cnf_transformation,[status(thm)],[f1061]) ).
fof(f2808,plain,
c_Finite__Set_Ocard(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a),t_a) != c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),v_na,tc_nat),
inference(cnf_transformation,[status(thm)],[f1062]) ).
fof(f2811,plain,
! [T_1] :
( ~ class_Lattices_Olattice(T_1)
| ! [T_2] : class_Lattices_Olower__semilattice(tc_fun(T_2,T_1)) ),
inference(miniscoping,[status(thm)],[f1064]) ).
fof(f2812,plain,
! [X0,X1] :
( ~ class_Lattices_Olattice(X1)
| class_Lattices_Olower__semilattice(tc_fun(X0,X1)) ),
inference(cnf_transformation,[status(thm)],[f2811]) ).
fof(f2871,plain,
class_Lattices_Olattice(tc_bool),
inference(cnf_transformation,[status(thm)],[f1115]) ).
fof(f3173,plain,
! [X0,X1] : c_Finite__Set_Ofinite(c_Set_Oimage(X0,v_U,tc_Com_Opname,X1),X1),
inference(resolution,[status(thm)],[f2704,f2802]) ).
fof(f3647,plain,
c_HOL_Oord__class_Oless(c_Suc(v_na),c_Suc(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a)),tc_nat),
inference(resolution,[status(thm)],[f2528,f2804]) ).
fof(f3678,plain,
~ c_HOL_Oord__class_Oless(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),c_Suc(v_na),tc_nat),
inference(resolution,[status(thm)],[f3647,f2153]) ).
fof(f3787,plain,
! [X0] : class_Lattices_Olower__semilattice(tc_fun(X0,tc_bool)),
inference(resolution,[status(thm)],[f2812,f2871]) ).
fof(f4066,plain,
! [X0,X1,X2] : c_Finite__Set_Ofinite(c_Lattices_Olower__semilattice__class_Oinf(X0,c_Set_Oimage(X1,v_U,tc_Com_Opname,X2),tc_fun(X2,tc_bool)),X2),
inference(resolution,[status(thm)],[f2115,f3173]) ).
fof(f4772,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(c_Suc(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat)),X0,tc_nat) = c_Suc(X1),
inference(paramodulation,[status(thm)],[f2148,f2491]) ).
fof(f6636,plain,
c_HOL_Oplus__class_Oplus(c_Suc(v_na),c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),c_Suc(v_na),tc_nat),tc_nat) = c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),
inference(resolution,[status(thm)],[f3678,f2243]) ).
fof(f6637,plain,
c_Suc(c_HOL_Oplus__class_Oplus(v_na,c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),c_Suc(v_na),tc_nat),tc_nat)) = c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),
inference(forward_demodulation,[status(thm)],[f2147,f6636]) ).
fof(f6662,plain,
c_Finite__Set_Ocard(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a),t_a) != c_HOL_Ominus__class_Ominus(c_Suc(c_HOL_Oplus__class_Oplus(v_na,c_Finite__Set_Ocard(v_G,t_a),tc_nat)),v_na,tc_nat),
inference(backward_demodulation,[status(thm)],[f6920,f2808]) ).
fof(f6920,plain,
c_Suc(c_HOL_Oplus__class_Oplus(v_na,c_Finite__Set_Ocard(v_G,t_a),tc_nat)) = c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),
inference(forward_demodulation,[status(thm)],[f2805,f6637]) ).
fof(f6924,plain,
c_Finite__Set_Ocard(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a),t_a) != c_Suc(c_Finite__Set_Ocard(v_G,t_a)),
inference(forward_demodulation,[status(thm)],[f4772,f6662]) ).
fof(f15630,plain,
( c_Lattices_Olower__semilattice__class_Oinf(v_G,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool)) = v_G
| ~ class_Lattices_Olower__semilattice(tc_fun(t_a,tc_bool)) ),
inference(resolution,[status(thm)],[f2047,f2803]) ).
fof(f15704,plain,
c_Lattices_Olower__semilattice__class_Oinf(v_G,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool)) = v_G,
inference(forward_subsumption_resolution,[status(thm)],[f15630,f3787]) ).
fof(f15877,plain,
c_Finite__Set_Ofinite(v_G,t_a),
inference(paramodulation,[status(thm)],[f15704,f4066]) ).
fof(f15887,plain,
( v_G = c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool))
| c_Finite__Set_Ocard(v_G,t_a) != c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(resolution,[status(thm)],[f15877,f2391]) ).
fof(f15888,plain,
! [X0] : c_Finite__Set_Ofinite(c_Lattices_Olower__semilattice__class_Oinf(v_G,X0,tc_fun(t_a,tc_bool)),t_a),
inference(resolution,[status(thm)],[f15877,f2117]) ).
fof(f15890,plain,
! [X0] : c_Finite__Set_Ofinite(c_HOL_Ominus__class_Ominus(v_G,X0,tc_fun(t_a,tc_bool)),t_a),
inference(resolution,[status(thm)],[f15877,f2113]) ).
fof(f16333,plain,
! [X0] : c_Finite__Set_Ocard(c_HOL_Ominus__class_Ominus(v_G,X0,tc_fun(t_a,tc_bool)),t_a) = c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(v_G,t_a),c_Finite__Set_Ocard(c_Lattices_Olower__semilattice__class_Oinf(v_G,X0,tc_fun(t_a,tc_bool)),t_a),tc_nat),
inference(resolution,[status(thm)],[f15888,f2312]) ).
fof(f17062,plain,
! [X0,X1] : c_Finite__Set_Ocard(c_Set_Oinsert(X0,c_HOL_Ominus__class_Ominus(v_G,X1,tc_fun(t_a,tc_bool)),t_a),t_a) = c_Suc(c_Finite__Set_Ocard(c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(v_G,X1,tc_fun(t_a,tc_bool)),c_Set_Oinsert(X0,c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a),tc_fun(t_a,tc_bool)),t_a)),
inference(resolution,[status(thm)],[f15890,f2543]) ).
fof(f17068,plain,
! [X0] :
( c_HOL_Ominus__class_Ominus(v_G,X0,tc_fun(t_a,tc_bool)) = c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool))
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Finite__Set_Ocard(c_HOL_Ominus__class_Ominus(v_G,X0,tc_fun(t_a,tc_bool)),t_a),tc_nat) ),
inference(resolution,[status(thm)],[f15890,f1709]) ).
fof(f17074,plain,
! [X0,X1] : c_Finite__Set_Ocard(c_Set_Oinsert(X0,c_HOL_Ominus__class_Ominus(v_G,X1,tc_fun(t_a,tc_bool)),t_a),t_a) = c_Suc(c_Finite__Set_Ocard(c_HOL_Ominus__class_Ominus(v_G,c_Set_Oinsert(X0,X1,t_a),tc_fun(t_a,tc_bool)),t_a)),
inference(forward_demodulation,[status(thm)],[f1284,f17062]) ).
fof(f21126,plain,
( c_Finite__Set_Ocard(v_G,t_a) = c_HOL_Ozero__class_Ozero(tc_nat)
| c_Finite__Set_Ocard(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a),t_a) = c_Suc(c_Finite__Set_Ocard(v_G,t_a)) ),
inference(resolution,[status(thm)],[f2636,f2807]) ).
fof(f21145,plain,
c_Finite__Set_Ocard(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a),t_a) != c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),
inference(backward_demodulation,[status(thm)],[f21168,f6924]) ).
fof(f21153,plain,
! [X0] : c_Finite__Set_Ocard(c_HOL_Ominus__class_Ominus(v_G,X0,tc_fun(t_a,tc_bool)),t_a) = c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_nat),c_Finite__Set_Ocard(c_Lattices_Olower__semilattice__class_Oinf(v_G,X0,tc_fun(t_a,tc_bool)),t_a),tc_nat),
inference(backward_demodulation,[status(thm)],[f21168,f16333]) ).
fof(f21159,plain,
( v_G = c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool))
| c_HOL_Ozero__class_Ozero(tc_nat) != c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(backward_demodulation,[status(thm)],[f21168,f15887]) ).
fof(f21168,plain,
c_Finite__Set_Ocard(v_G,t_a) = c_HOL_Ozero__class_Ozero(tc_nat),
inference(forward_subsumption_resolution,[status(thm)],[f21126,f6924]) ).
fof(f21187,plain,
c_Finite__Set_Ocard(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a),t_a) != c_HOL_Oone__class_Oone(tc_nat),
inference(forward_demodulation,[status(thm)],[f1376,f21145]) ).
fof(f21211,plain,
! [X0,X1] : c_Finite__Set_Ocard(c_Set_Oinsert(X0,c_HOL_Ominus__class_Ominus(v_G,X1,tc_fun(t_a,tc_bool)),t_a),t_a) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),
inference(backward_demodulation,[status(thm)],[f21215,f17074]) ).
fof(f21213,plain,
! [X0] :
( c_HOL_Ominus__class_Ominus(v_G,X0,tc_fun(t_a,tc_bool)) = c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool))
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ),
inference(backward_demodulation,[status(thm)],[f21215,f17068]) ).
fof(f21215,plain,
! [X0] : c_Finite__Set_Ocard(c_HOL_Ominus__class_Ominus(v_G,X0,tc_fun(t_a,tc_bool)),t_a) = c_HOL_Ozero__class_Ozero(tc_nat),
inference(forward_demodulation,[status(thm)],[f2485,f21153]) ).
fof(f21249,plain,
v_G = c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),
inference(trivial_equality_resolution,[status(thm)],[f21159]) ).
fof(f21276,plain,
! [X0,X1] : c_Finite__Set_Ocard(c_Set_Oinsert(X0,c_HOL_Ominus__class_Ominus(v_G,X1,tc_fun(t_a,tc_bool)),t_a),t_a) = c_HOL_Oone__class_Oone(tc_nat),
inference(forward_demodulation,[status(thm)],[f1376,f21211]) ).
fof(f21278,plain,
! [X0] :
( c_HOL_Ominus__class_Ominus(v_G,X0,tc_fun(t_a,tc_bool)) = v_G
| c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ),
inference(forward_demodulation,[status(thm)],[f21249,f21213]) ).
fof(f21281,plain,
! [X0] : c_Finite__Set_Ocard(c_Set_Oinsert(X0,v_G,t_a),t_a) = c_HOL_Oone__class_Oone(tc_nat),
inference(backward_demodulation,[status(thm)],[f21288,f21276]) ).
fof(f21288,plain,
! [X0] : c_HOL_Ominus__class_Ominus(v_G,X0,tc_fun(t_a,tc_bool)) = v_G,
inference(forward_subsumption_resolution,[status(thm)],[f21278,f1175]) ).
fof(f21294,plain,
c_HOL_Oone__class_Oone(tc_nat) != c_HOL_Oone__class_Oone(tc_nat),
inference(backward_demodulation,[status(thm)],[f21281,f21187]) ).
fof(f21299,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f21294]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV885-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n019.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Mon Sep 21 09:30:19 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.27/0.54 % Drodi V4.1.1
% 45.69/6.44 % Refutation found
% 45.69/6.44 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 45.69/6.44 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.40/6.75 % Elapsed time: 6.302831 seconds
% 2.40/6.75 % CPU time: 47.297972 seconds
% 2.40/6.75 % Total memory used: 406.112 MB
% 2.40/6.75 % Net memory used: 384.156 MB
%------------------------------------------------------------------------------