%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV885-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:53:18 PM UTC 2026
% Result : Unsatisfiable 44.72s 6.46s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV885-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.65 % Computer : n014.cluster.edu
% 0.19/0.65 % Model : x86_64 x86_64
% 0.19/0.65 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.65 % Memory : 8046.5625MB
% 0.19/0.65 % OS : Linux 6.8.0-71-generic
% 0.19/0.65 % CPULimit : 300
% 0.19/0.65 % WCLimit : 300
% 0.19/0.65 % DateTime : Mon Sep 21 09:29:51 UTC 2026
% 0.22/0.65 % CPUTime :
% 0.22/0.77 % Drodi V4.1.1
% 44.72/6.46 % Refutation found
% 44.72/6.46 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 44.72/6.46 % SZS output start CNFRefutation for theBenchmark
% 44.72/6.46 fof(f3,axiom,(
% 44.72/6.46 (![V_n]: (( V_n = c_HOL_Ozero__class_Ozero(tc_nat)| ~ c_HOL_Oord__class_Oless(V_n,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) ) ))),
% 44.72/6.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 44.72/6.46 fof(f154,axiom,(
% 44.72/6.46 c_HOL_Oone__class_Oone(tc_nat) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ),
% 44.72/6.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 44.72/6.46 fof(f356,axiom,(
% 44.72/6.46 (![T_a]: (c_Finite__Set_Ocard(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a) = c_HOL_Ozero__class_Ozero(tc_nat) ))),
% 44.72/6.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 44.72/6.46 fof(f403,axiom,(
% 44.72/6.46 (![V_x,T_a]: (~ c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a) ))),
% 44.72/6.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 44.72/6.46 fof(f556,axiom,(
% 44.72/6.46 (![T_a,V_x]: (( ~ class_Orderings_Obot(T_a)| c_lessequals(c_Orderings_Obot__class_Obot(T_a),V_x,T_a) ) ))),
% 44.72/6.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 44.72/6.46 fof(f566,axiom,(
% 44.72/6.46 (![T_a,V_x,V_y]: (( ~ class_Lattices_Olower__semilattice(T_a)| c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a) = V_x| ~ c_lessequals(V_x,V_y,T_a) ) ))),
% 44.72/6.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 44.72/6.46 fof(f607,axiom,(
% 44.72/6.46 (![V_F,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)| ~ c_Finite__Set_Ofinite(V_G,T_a) ) ))),
% 44.72/6.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 44.72/6.46 fof(f636,axiom,(
% 44.72/6.46 (![V_m,V_n]: (( ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat)| ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat) ) ))),
% 44.72/6.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 44.72/6.46 fof(f637,axiom,(
% 44.72/6.46 (![V_n,V_m]: (( c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat)| c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ))),
% 44.72/6.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 44.72/6.46 fof(f787,axiom,(
% 44.72/6.46 (![V_A,T_a]: (( c_Finite__Set_Ocard(V_A,T_a) != c_HOL_Ozero__class_Ozero(tc_nat)| ~ c_Finite__Set_Ofinite(V_A,T_a)| V_A = c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ) ))),
% 44.72/6.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 44.72/6.46 fof(f879,axiom,(
% 44.72/6.46 (![V_m,V_n]: (( c_HOL_Oord__class_Oless(V_m,c_Suc(V_n),tc_nat)| ~ c_lessequals(V_m,V_n,tc_nat) ) ))),
% 44.72/6.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 44.72/6.46 fof(f950,axiom,(
% 44.72/6.46 (![V_x,T_a]: (( c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)| c_Finite__Set_Ocard(c_Set_Oinsert(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),T_a) = c_Suc(c_Finite__Set_Ocard(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)) ) ))),
% 44.72/6.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 44.72/6.46 fof(f951,axiom,(
% 44.72/6.46 (![V_x,V_xa,T_a]: (( c_in(V_x,V_xa,T_a)| 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_Finite__Set_Ocard(V_xa,T_a) = c_HOL_Ozero__class_Ozero(tc_nat) ) ))),
% 44.72/6.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 44.72/6.46 fof(f993,axiom,(
% 44.72/6.46 (![V_h,V_F,T_a,T_b]: (( c_Finite__Set_Ofinite(c_Set_Oimage(V_h,V_F,T_a,T_b),T_b)| ~ c_Finite__Set_Ofinite(V_F,T_a) ) ))),
% 44.72/6.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 44.72/6.46 fof(f1002,axiom,(
% 44.72/6.46 (![V_m,V_n]: (c_HOL_Ominus__class_Ominus(c_Suc(V_m),c_Suc(V_n),tc_nat) = c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat) ))),
% 44.72/6.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 44.72/6.46 fof(f1009,axiom,(
% 44.72/6.46 (![V_m,V_n]: (( c_HOL_Ominus__class_Ominus(c_Suc(V_m),V_n,tc_nat) = c_Suc(c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat))| ~ c_lessequals(V_n,V_m,tc_nat) ) ))),
% 44.72/6.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 44.72/6.46 fof(f1056,negated_conjecture,(
% 44.72/6.46 c_Finite__Set_Ofinite(v_U,tc_Com_Opname) ),
% 44.72/6.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 44.72/6.46 fof(f1057,negated_conjecture,(
% 44.72/6.46 c_lessequals(v_G,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool)) ),
% 44.72/6.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 44.72/6.46 fof(f1058,negated_conjecture,(
% 44.72/6.46 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) ),
% 44.72/6.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 44.72/6.46 fof(f1059,negated_conjecture,(
% 44.72/6.46 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) ),
% 44.72/6.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 44.72/6.46 fof(f1061,negated_conjecture,(
% 44.72/6.46 ~ c_in(hAPP(v_mgt__call,v_pn),v_G,t_a) ),
% 44.72/6.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 44.72/6.46 fof(f1062,negated_conjecture,(
% 44.72/6.46 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) ),
% 44.72/6.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 44.72/6.46 fof(f1064,axiom,(
% 44.72/6.46 (![T_2,T_1]: (( class_Lattices_Olower__semilattice(tc_fun(T_2,T_1))| ~ class_Lattices_Olattice(T_1) ) ))),
% 44.72/6.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 44.72/6.46 fof(f1108,axiom,(
% 44.72/6.46 class_Orderings_Obot(tc_nat) ),
% 44.72/6.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 44.72/6.46 fof(f1115,axiom,(
% 44.72/6.46 class_Lattices_Olattice(tc_bool) ),
% 44.72/6.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 44.72/6.46 fof(f1124,plain,(
% 44.72/6.46 ![X0]: (X0=c_HOL_Ozero__class_Ozero(tc_nat)|~c_HOL_Oord__class_Oless(X0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat))),
% 44.72/6.46 inference(cnf_transformation,[status(thm)],[f3])).
% 44.72/6.46 fof(f1376,plain,(
% 44.72/6.46 c_HOL_Oone__class_Oone(tc_nat)=c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),
% 44.72/6.46 inference(cnf_transformation,[status(thm)],[f154])).
% 44.72/6.46 fof(f1708,plain,(
% 44.72/6.46 ![X0]: (c_Finite__Set_Ocard(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X0)=c_HOL_Ozero__class_Ozero(tc_nat))),
% 44.72/6.46 inference(cnf_transformation,[status(thm)],[f356])).
% 44.72/6.46 fof(f1786,plain,(
% 44.72/6.46 ![X0,X1]: (~c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1))),
% 44.72/6.46 inference(cnf_transformation,[status(thm)],[f403])).
% 44.72/6.46 fof(f2035,plain,(
% 44.72/6.46 ![T_a]: (~class_Orderings_Obot(T_a)|(![V_x]: c_lessequals(c_Orderings_Obot__class_Obot(T_a),V_x,T_a)))),
% 44.72/6.46 inference(miniscoping,[status(thm)],[f556])).
% 44.72/6.46 fof(f2036,plain,(
% 44.72/6.46 ![X0,X1]: (~class_Orderings_Obot(X0)|c_lessequals(c_Orderings_Obot__class_Obot(X0),X1,X0))),
% 44.72/6.46 inference(cnf_transformation,[status(thm)],[f2035])).
% 44.72/6.46 fof(f2047,plain,(
% 44.72/6.46 ![X0,X1,X2]: (~class_Lattices_Olower__semilattice(X0)|c_Lattices_Olower__semilattice__class_Oinf(X1,X2,X0)=X1|~c_lessequals(X1,X2,X0))),
% 44.72/6.46 inference(cnf_transformation,[status(thm)],[f566])).
% 44.72/6.46 fof(f2114,plain,(
% 44.72/6.46 ![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))|~c_Finite__Set_Ofinite(V_G,T_a))),
% 44.72/6.46 inference(miniscoping,[status(thm)],[f607])).
% 44.72/6.46 fof(f2115,plain,(
% 44.72/6.46 ![X0,X1,X2]: (c_Finite__Set_Ofinite(c_Lattices_Olower__semilattice__class_Oinf(X0,X1,tc_fun(X2,tc_bool)),X2)|~c_Finite__Set_Ofinite(X1,X2))),
% 44.72/6.46 inference(cnf_transformation,[status(thm)],[f2114])).
% 44.72/6.46 fof(f2153,plain,(
% 44.72/6.46 ![X0,X1]: (~c_HOL_Oord__class_Oless(X0,X1,tc_nat)|~c_HOL_Oord__class_Oless(X1,c_Suc(X0),tc_nat))),
% 44.72/6.46 inference(cnf_transformation,[status(thm)],[f636])).
% 44.72/6.46 fof(f2154,plain,(
% 44.72/6.46 ![X0,X1]: (c_HOL_Oord__class_Oless(X0,c_Suc(X1),tc_nat)|c_HOL_Oord__class_Oless(X1,X0,tc_nat))),
% 44.72/6.46 inference(cnf_transformation,[status(thm)],[f637])).
% 44.72/6.46 fof(f2391,plain,(
% 44.72/6.46 ![X0,X1]: (~c_Finite__Set_Ocard(X0,X1)=c_HOL_Ozero__class_Ozero(tc_nat)|~c_Finite__Set_Ofinite(X0,X1)|X0=c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)))),
% 44.72/6.46 inference(cnf_transformation,[status(thm)],[f787])).
% 44.72/6.46 fof(f2528,plain,(
% 44.72/6.46 ![X0,X1]: (c_HOL_Oord__class_Oless(X0,c_Suc(X1),tc_nat)|~c_lessequals(X0,X1,tc_nat))),
% 44.72/6.46 inference(cnf_transformation,[status(thm)],[f879])).
% 44.72/6.46 fof(f2634,plain,(
% 44.72/6.46 ![X0,X1]: (c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)|c_Finite__Set_Ocard(c_Set_Oinsert(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),X1)=c_Suc(c_Finite__Set_Ocard(c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)))),
% 44.72/6.46 inference(cnf_transformation,[status(thm)],[f950])).
% 44.72/6.46 fof(f2635,plain,(
% 44.72/6.46 ![V_xa,T_a]: ((![V_x]: (c_in(V_x,V_xa,T_a)|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_Finite__Set_Ocard(V_xa,T_a)=c_HOL_Ozero__class_Ozero(tc_nat))),
% 44.72/6.46 inference(miniscoping,[status(thm)],[f951])).
% 44.72/6.46 fof(f2636,plain,(
% 44.72/6.46 ![X0,X1,X2]: (c_in(X0,X1,X2)|c_Finite__Set_Ocard(c_Set_Oinsert(X0,X1,X2),X2)=c_Suc(c_Finite__Set_Ocard(X1,X2))|c_Finite__Set_Ocard(X1,X2)=c_HOL_Ozero__class_Ozero(tc_nat))),
% 44.72/6.46 inference(cnf_transformation,[status(thm)],[f2635])).
% 44.72/6.46 fof(f2703,plain,(
% 44.72/6.46 ![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))|~c_Finite__Set_Ofinite(V_F,T_a))),
% 44.72/6.46 inference(miniscoping,[status(thm)],[f993])).
% 44.72/6.46 fof(f2704,plain,(
% 44.72/6.46 ![X0,X1,X2,X3]: (c_Finite__Set_Ofinite(c_Set_Oimage(X0,X1,X2,X3),X3)|~c_Finite__Set_Ofinite(X1,X2))),
% 44.72/6.46 inference(cnf_transformation,[status(thm)],[f2703])).
% 44.72/6.46 fof(f2714,plain,(
% 44.72/6.46 ![X0,X1]: (c_HOL_Ominus__class_Ominus(c_Suc(X0),c_Suc(X1),tc_nat)=c_HOL_Ominus__class_Ominus(X0,X1,tc_nat))),
% 44.72/6.46 inference(cnf_transformation,[status(thm)],[f1002])).
% 44.72/6.46 fof(f2724,plain,(
% 44.72/6.46 ![X0,X1]: (c_HOL_Ominus__class_Ominus(c_Suc(X0),X1,tc_nat)=c_Suc(c_HOL_Ominus__class_Ominus(X0,X1,tc_nat))|~c_lessequals(X1,X0,tc_nat))),
% 44.72/6.46 inference(cnf_transformation,[status(thm)],[f1009])).
% 44.72/6.46 fof(f2802,plain,(
% 44.72/6.46 c_Finite__Set_Ofinite(v_U,tc_Com_Opname)),
% 44.72/6.46 inference(cnf_transformation,[status(thm)],[f1056])).
% 44.72/6.46 fof(f2803,plain,(
% 44.72/6.46 c_lessequals(v_G,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool))),
% 44.72/6.46 inference(cnf_transformation,[status(thm)],[f1057])).
% 44.72/6.46 fof(f2804,plain,(
% 44.72/6.46 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)),
% 44.72/6.46 inference(cnf_transformation,[status(thm)],[f1058])).
% 44.72/6.46 fof(f2805,plain,(
% 44.72/6.46 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)),
% 44.72/6.46 inference(cnf_transformation,[status(thm)],[f1059])).
% 44.72/6.46 fof(f2807,plain,(
% 44.72/6.46 ~c_in(hAPP(v_mgt__call,v_pn),v_G,t_a)),
% 44.72/6.46 inference(cnf_transformation,[status(thm)],[f1061])).
% 44.72/6.46 fof(f2808,plain,(
% 44.72/6.46 ~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)),
% 44.72/6.46 inference(cnf_transformation,[status(thm)],[f1062])).
% 44.72/6.46 fof(f2811,plain,(
% 44.72/6.46 ![T_1]: ((![T_2]: class_Lattices_Olower__semilattice(tc_fun(T_2,T_1)))|~class_Lattices_Olattice(T_1))),
% 44.72/6.46 inference(miniscoping,[status(thm)],[f1064])).
% 44.72/6.46 fof(f2812,plain,(
% 44.72/6.46 ![X0,X1]: (class_Lattices_Olower__semilattice(tc_fun(X0,X1))|~class_Lattices_Olattice(X1))),
% 44.72/6.46 inference(cnf_transformation,[status(thm)],[f2811])).
% 44.72/6.46 fof(f2864,plain,(
% 44.72/6.46 class_Orderings_Obot(tc_nat)),
% 44.72/6.46 inference(cnf_transformation,[status(thm)],[f1108])).
% 44.72/6.46 fof(f2871,plain,(
% 44.72/6.46 class_Lattices_Olattice(tc_bool)),
% 44.72/6.46 inference(cnf_transformation,[status(thm)],[f1115])).
% 44.72/6.46 fof(f3150,plain,(
% 44.72/6.46 ![X0,X1]: (c_Finite__Set_Ofinite(c_Set_Oimage(X0,v_U,tc_Com_Opname,X1),X1))),
% 44.72/6.46 inference(resolution,[status(thm)],[f2704,f2802])).
% 44.72/6.46 fof(f3306,plain,(
% 44.72/6.46 ![X0]: (class_Lattices_Olower__semilattice(tc_fun(X0,tc_bool)))),
% 44.72/6.46 inference(resolution,[status(thm)],[f2812,f2871])).
% 44.72/6.46 fof(f3417,plain,(
% 44.72/6.46 ![X0]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)|X0=c_HOL_Ozero__class_Ozero(tc_nat))),
% 44.72/6.46 inference(resolution,[status(thm)],[f2154,f1124])).
% 44.72/6.46 fof(f4027,plain,(
% 44.72/6.46 ![X0]: (c_lessequals(c_Orderings_Obot__class_Obot(tc_nat),X0,tc_nat))),
% 44.72/6.46 inference(resolution,[status(thm)],[f2036,f2864])).
% 44.72/6.46 fof(f4028,plain,(
% 44.72/6.46 ![X0]: (c_HOL_Oord__class_Oless(c_Orderings_Obot__class_Obot(tc_nat),c_Suc(X0),tc_nat))),
% 44.72/6.46 inference(resolution,[status(thm)],[f4027,f2528])).
% 44.72/6.46 fof(f4059,plain,(
% 44.72/6.46 ![X0]: (~c_HOL_Oord__class_Oless(X0,c_Orderings_Obot__class_Obot(tc_nat),tc_nat))),
% 44.72/6.46 inference(resolution,[status(thm)],[f4028,f2153])).
% 44.72/6.46 fof(f5574,plain,(
% 44.72/6.46 ![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))),
% 44.72/6.46 inference(resolution,[status(thm)],[f2115,f3150])).
% 44.72/6.46 fof(f6404,plain,(
% 44.72/6.46 c_Orderings_Obot__class_Obot(tc_nat)=c_HOL_Ozero__class_Ozero(tc_nat)),
% 44.72/6.46 inference(resolution,[status(thm)],[f3417,f4059])).
% 44.72/6.46 fof(f6470,plain,(
% 44.72/6.46 c_HOL_Oone__class_Oone(tc_nat)=c_Suc(c_Orderings_Obot__class_Obot(tc_nat))),
% 44.72/6.46 inference(backward_demodulation,[status(thm)],[f6404,f1376])).
% 44.72/6.46 fof(f6472,plain,(
% 44.72/6.46 ![X0]: (c_Finite__Set_Ocard(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X0)=c_Orderings_Obot__class_Obot(tc_nat))),
% 44.72/6.46 inference(backward_demodulation,[status(thm)],[f6404,f1708])).
% 44.72/6.46 fof(f9972,plain,(
% 44.72/6.46 ~class_Lattices_Olower__semilattice(tc_fun(t_a,tc_bool))|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),
% 44.72/6.46 inference(resolution,[status(thm)],[f2047,f2803])).
% 44.72/6.46 fof(f10019,plain,(
% 44.72/6.46 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),
% 44.72/6.46 inference(forward_subsumption_resolution,[status(thm)],[f9972,f3306])).
% 44.72/6.46 fof(f11340,plain,(
% 44.72/6.46 c_Finite__Set_Ofinite(v_G,t_a)),
% 44.72/6.46 inference(paramodulation,[status(thm)],[f10019,f5574])).
% 44.72/6.46 fof(f12873,plain,(
% 44.72/6.46 ![X0,X1]: (~c_Finite__Set_Ocard(X0,X1)=c_Orderings_Obot__class_Obot(tc_nat)|~c_Finite__Set_Ofinite(X0,X1)|X0=c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)))),
% 44.72/6.46 inference(forward_demodulation,[status(thm)],[f6404,f2391])).
% 44.72/6.46 fof(f37872,plain,(
% 44.72/6.46 ![X0,X1]: (c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)|c_Finite__Set_Ocard(c_Set_Oinsert(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),X1)=c_Suc(c_Orderings_Obot__class_Obot(tc_nat)))),
% 44.72/6.46 inference(forward_demodulation,[status(thm)],[f6472,f2634])).
% 44.72/6.46 fof(f37873,plain,(
% 44.72/6.46 ![X0,X1]: (c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)|c_Finite__Set_Ocard(c_Set_Oinsert(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),X1)=c_HOL_Oone__class_Oone(tc_nat))),
% 44.72/6.46 inference(forward_demodulation,[status(thm)],[f6470,f37872])).
% 44.72/6.46 fof(f37874,plain,(
% 44.72/6.46 ![X0,X1]: (c_Finite__Set_Ocard(c_Set_Oinsert(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),X1)=c_HOL_Oone__class_Oone(tc_nat))),
% 44.72/6.46 inference(forward_subsumption_resolution,[status(thm)],[f37873,f1786])).
% 44.72/6.46 fof(f37886,plain,(
% 44.72/6.46 ![X0,X1,X2]: (c_in(X0,X1,X2)|c_Finite__Set_Ocard(c_Set_Oinsert(X0,X1,X2),X2)=c_Suc(c_Finite__Set_Ocard(X1,X2))|c_Finite__Set_Ocard(X1,X2)=c_Orderings_Obot__class_Obot(tc_nat))),
% 44.72/6.46 inference(forward_demodulation,[status(thm)],[f6404,f2636])).
% 44.72/6.46 fof(f37887,plain,(
% 44.72/6.46 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))|c_Finite__Set_Ocard(v_G,t_a)=c_Orderings_Obot__class_Obot(tc_nat)),
% 44.72/6.46 inference(resolution,[status(thm)],[f37886,f2807])).
% 44.72/6.46 fof(f43786,plain,(
% 44.72/6.46 c_HOL_Ominus__class_Ominus(c_Suc(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)=c_Suc(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))),
% 44.72/6.46 inference(resolution,[status(thm)],[f2724,f2804])).
% 44.72/6.46 fof(f43871,plain,(
% 44.72/6.46 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)=c_Suc(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))),
% 44.72/6.46 inference(forward_demodulation,[status(thm)],[f2714,f43786])).
% 44.72/6.46 fof(f43872,plain,(
% 44.72/6.46 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)=c_Suc(c_Finite__Set_Ocard(v_G,t_a))),
% 44.72/6.46 inference(forward_demodulation,[status(thm)],[f2805,f43871])).
% 44.72/6.46 fof(f51310,plain,(
% 44.72/6.46 ~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))),
% 44.72/6.46 inference(backward_demodulation,[status(thm)],[f43872,f2808])).
% 44.72/6.46 fof(f52198,plain,(
% 44.72/6.46 c_Finite__Set_Ocard(v_G,t_a)=c_Orderings_Obot__class_Obot(tc_nat)),
% 44.72/6.46 inference(backward_subsumption_resolution,[status(thm)],[f37887,f51310])).
% 44.72/6.46 fof(f52201,plain,(
% 44.72/6.46 ~c_Finite__Set_Ocard(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a),t_a)=c_Suc(c_Orderings_Obot__class_Obot(tc_nat))),
% 44.72/6.46 inference(backward_demodulation,[status(thm)],[f52198,f51310])).
% 44.72/6.46 fof(f52241,plain,(
% 44.72/6.46 ~c_Finite__Set_Ofinite(v_G,t_a)|v_G=c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool))),
% 44.72/6.46 inference(resolution,[status(thm)],[f52198,f12873])).
% 44.72/6.53 fof(f52254,plain,(
% 44.72/6.53 ~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)),
% 44.72/6.53 inference(forward_demodulation,[status(thm)],[f6470,f52201])).
% 44.72/6.53 fof(f52296,plain,(
% 44.72/6.53 v_G=c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool))),
% 44.72/6.53 inference(forward_subsumption_resolution,[status(thm)],[f52241,f11340])).
% 44.72/6.53 fof(f52304,plain,(
% 44.72/6.53 ![X0]: (c_Finite__Set_Ocard(c_Set_Oinsert(X0,v_G,t_a),t_a)=c_HOL_Oone__class_Oone(tc_nat))),
% 44.72/6.53 inference(paramodulation,[status(thm)],[f52296,f37874])).
% 44.72/6.53 fof(f52994,plain,(
% 44.72/6.53 ~c_HOL_Oone__class_Oone(tc_nat)=c_HOL_Oone__class_Oone(tc_nat)),
% 44.72/6.53 inference(backward_demodulation,[status(thm)],[f52304,f52254])).
% 44.72/6.53 fof(f53010,plain,(
% 44.72/6.53 $false),
% 44.72/6.53 inference(trivial_equality_resolution,[status(thm)],[f52994])).
% 44.72/6.53 % SZS output end CNFRefutation for theBenchmark.p
% 14.46/6.57 % Elapsed time: 5.895852 seconds
% 14.46/6.57 % CPU time: 45.471073 seconds
% 14.46/6.57 % Total memory used: 479.671 MB
% 14.46/6.57 % Net memory used: 458.758 MB
%------------------------------------------------------------------------------