%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW358+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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 03:09:01 PM UTC 2026
% Result : Theorem 27.19s 4.51s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW358+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.41 % Computer : n016.cluster.edu
% 0.16/0.41 % Model : x86_64 x86_64
% 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41 % Memory : 8046.5625MB
% 0.16/0.41 % OS : Linux 6.8.0-71-generic
% 0.16/0.41 % CPULimit : 300
% 0.16/0.41 % WCLimit : 300
% 0.16/0.41 % DateTime : Mon Sep 21 09:54:08 UTC 2026
% 0.16/0.41 % CPUTime :
% 0.65/1.04 % Drodi V4.1.1
% 27.19/4.51 % Refutation found
% 27.19/4.51 % SZS status Theorem for theBenchmark: Theorem is valid
% 27.19/4.51 % SZS output start CNFRefutation for theBenchmark
% 27.19/4.51 fof(f3,axiom,(
% 27.19/4.51 (! [V_h_2,T_c,V_F_2,T_b] :( hBOOL(hAPP(c_Finite__Set_Ofinite(T_b),V_F_2))=> hBOOL(hAPP(c_Finite__Set_Ofinite(T_c),hAPP(c_Set_Oimage(T_b,T_c,V_h_2),V_F_2))) ) )),
% 27.19/4.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.19/4.51 fof(f11,axiom,(
% 27.19/4.51 (! [V_g_2,V_f_2,T_b,T_c] :( class_Orderings_Oord(T_c)=> ( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,T_c)),V_f_2),V_g_2))<=> (! [B_x] : hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(T_c),hAPP(V_f_2,B_x)),hAPP(V_g_2,B_x))) )) ) )),
% 27.19/4.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.19/4.51 fof(f14,axiom,(
% 27.19/4.51 (! [V_A_2,V_B_2,T_b] :( hBOOL(hAPP(c_Finite__Set_Ofinite(T_b),V_B_2))=> ( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_A_2),V_B_2))=> ( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(T_b),V_B_2)),hAPP(c_Finite__Set_Ocard(T_b),V_A_2)))=> V_A_2 = V_B_2 ) ) ) )),
% 27.19/4.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.19/4.51 fof(f15,axiom,(
% 27.19/4.51 (! [V_A_2,V_B_2,T_b] :( hBOOL(hAPP(c_Finite__Set_Ofinite(T_b),V_B_2))=> ( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_A_2),V_B_2))=> hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(T_b),V_A_2)),hAPP(c_Finite__Set_Ocard(T_b),V_B_2))) ) ) )),
% 27.19/4.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.19/4.51 fof(f32,axiom,(
% 27.19/4.51 (! [T_b,V_B_2,V_A_2] :( V_A_2 = V_B_2=> ~ ( hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_A_2),V_B_2))=> ~ hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_B_2),V_A_2)) ) ) )),
% 27.19/4.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.19/4.51 fof(f4993,axiom,(
% 27.19/4.51 (! [T_2,T_1] :( class_Orderings_Opreorder(T_1)=> class_Orderings_Opreorder(tc_fun(T_2,T_1)) ) )),
% 27.19/4.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.19/4.51 fof(f4996,axiom,(
% 27.19/4.51 (! [T_2,T_1] :( class_Orderings_Oorder(T_1)=> class_Orderings_Oorder(tc_fun(T_2,T_1)) ) )),
% 27.19/4.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.19/4.51 fof(f5132,axiom,(
% 27.19/4.51 class_Orderings_Opreorder(tc_HOL_Obool) ),
% 27.19/4.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.19/4.51 fof(f5135,axiom,(
% 27.19/4.51 class_Orderings_Oorder(tc_HOL_Obool) ),
% 27.19/4.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.19/4.51 fof(f5137,axiom,(
% 27.19/4.51 class_Orderings_Oord(tc_HOL_Obool) ),
% 27.19/4.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.19/4.51 fof(f5224,hypothesis,(
% 27.19/4.51 hBOOL(hAPP(c_Finite__Set_Ofinite(tc_Com_Opname),v_U)) ),
% 27.19/4.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.19/4.51 fof(f5225,hypothesis,(
% 27.19/4.51 hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),v_G),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U))) ),
% 27.19/4.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.19/4.51 fof(f5226,hypothesis,(
% 27.19/4.51 hAPP(c_Finite__Set_Ocard(t_a),v_G) = hAPP(c_Finite__Set_Ocard(t_a),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)) ),
% 27.19/4.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.19/4.51 fof(f5228,conjecture,(
% 27.19/4.51 v_G = hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U) ),
% 27.19/4.51 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 27.19/4.51 fof(f5229,negated_conjecture,(
% 27.19/4.51 ~(v_G = hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U) )),
% 27.19/4.51 inference(negated_conjecture,[status(cth)],[f5228])).
% 27.19/4.51 fof(f5235,plain,(
% 27.19/4.51 ![V_h_2,T_c,V_F_2,T_b]: (~hBOOL(hAPP(c_Finite__Set_Ofinite(T_b),V_F_2))|hBOOL(hAPP(c_Finite__Set_Ofinite(T_c),hAPP(c_Set_Oimage(T_b,T_c,V_h_2),V_F_2))))),
% 27.19/4.51 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 27.19/4.51 fof(f5236,plain,(
% 27.19/4.51 ![V_F_2,T_b]: (~hBOOL(hAPP(c_Finite__Set_Ofinite(T_b),V_F_2))|(![V_h_2,T_c]: hBOOL(hAPP(c_Finite__Set_Ofinite(T_c),hAPP(c_Set_Oimage(T_b,T_c,V_h_2),V_F_2)))))),
% 27.19/4.51 inference(miniscoping,[status(thm)],[f5235])).
% 27.19/4.51 fof(f5237,plain,(
% 27.19/4.51 ![X0,X1,X2,X3]: (~hBOOL(hAPP(c_Finite__Set_Ofinite(X0),X1))|hBOOL(hAPP(c_Finite__Set_Ofinite(X2),hAPP(c_Set_Oimage(X0,X2,X3),X1))))),
% 27.19/4.51 inference(cnf_transformation,[status(thm)],[f5236])).
% 27.19/4.51 fof(f5260,plain,(
% 27.19/4.51 ![V_g_2,V_f_2,T_b,T_c]: (~class_Orderings_Oord(T_c)|(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,T_c)),V_f_2),V_g_2))<=>(![B_x]: hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(T_c),hAPP(V_f_2,B_x)),hAPP(V_g_2,B_x))))))),
% 27.19/4.51 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 27.19/4.51 fof(f5261,plain,(
% 27.19/4.51 ![V_g_2,V_f_2,T_b,T_c]: (~class_Orderings_Oord(T_c)|((~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,T_c)),V_f_2),V_g_2))|(![B_x]: hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(T_c),hAPP(V_f_2,B_x)),hAPP(V_g_2,B_x)))))&(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,T_c)),V_f_2),V_g_2))|(?[B_x]: ~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(T_c),hAPP(V_f_2,B_x)),hAPP(V_g_2,B_x)))))))),
% 27.19/4.51 inference(NNF_transformation,[status(thm)],[f5260])).
% 27.19/4.51 fof(f5262,plain,(
% 27.19/4.51 ![T_c]: (~class_Orderings_Oord(T_c)|((![V_g_2,V_f_2]: ((![T_b]: ~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,T_c)),V_f_2),V_g_2)))|(![B_x]: hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(T_c),hAPP(V_f_2,B_x)),hAPP(V_g_2,B_x))))))&(![V_g_2,V_f_2]: ((![T_b]: hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,T_c)),V_f_2),V_g_2)))|(?[B_x]: ~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(T_c),hAPP(V_f_2,B_x)),hAPP(V_g_2,B_x))))))))),
% 27.19/4.51 inference(miniscoping,[status(thm)],[f5261])).
% 27.19/4.51 fof(f5263,plain,(
% 27.19/4.51 ![T_c]: (~class_Orderings_Oord(T_c)|((![V_g_2,V_f_2]: ((![T_b]: ~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,T_c)),V_f_2),V_g_2)))|(![B_x]: hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(T_c),hAPP(V_f_2,B_x)),hAPP(V_g_2,B_x))))))&(![V_g_2,V_f_2]: ((![T_b]: hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,T_c)),V_f_2),V_g_2)))|~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(T_c),hAPP(V_f_2,sK2_skl(V_f_2,V_g_2,T_c))),hAPP(V_g_2,sK2_skl(V_f_2,V_g_2,T_c))))))))),
% 27.19/4.51 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(B_x,sK2_skl(V_f_2,V_g_2,T_c))],[f5262])).
% 27.19/4.51 fof(f5264,plain,(
% 27.19/4.51 ![X0,X1,X2,X3,X4]: (~class_Orderings_Oord(X0)|~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X1,X0)),X2),X3))|hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(X0),hAPP(X2,X4)),hAPP(X3,X4))))),
% 27.19/4.51 inference(cnf_transformation,[status(thm)],[f5263])).
% 27.19/4.51 fof(f5265,plain,(
% 27.19/4.51 ![X0,X1,X2,X3]: (~class_Orderings_Oord(X0)|hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X1,X0)),X2),X3))|~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(X0),hAPP(X2,sK2_skl(X2,X3,X0))),hAPP(X3,sK2_skl(X2,X3,X0)))))),
% 27.19/4.51 inference(cnf_transformation,[status(thm)],[f5263])).
% 27.19/4.51 fof(f5272,plain,(
% 27.19/4.51 ![V_A_2,V_B_2,T_b]: (~hBOOL(hAPP(c_Finite__Set_Ofinite(T_b),V_B_2))|(~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_A_2),V_B_2))|(~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(T_b),V_B_2)),hAPP(c_Finite__Set_Ocard(T_b),V_A_2)))|V_A_2=V_B_2)))),
% 27.19/4.51 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 27.19/4.51 fof(f5273,plain,(
% 27.19/4.51 ![V_B_2,T_b]: (~hBOOL(hAPP(c_Finite__Set_Ofinite(T_b),V_B_2))|(![V_A_2]: (~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_A_2),V_B_2))|(~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(T_b),V_B_2)),hAPP(c_Finite__Set_Ocard(T_b),V_A_2)))|V_A_2=V_B_2))))),
% 27.19/4.51 inference(miniscoping,[status(thm)],[f5272])).
% 27.19/4.51 fof(f5274,plain,(
% 27.19/4.51 ![X0,X1,X2]: (~hBOOL(hAPP(c_Finite__Set_Ofinite(X0),X1))|~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool)),X2),X1))|~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(X0),X1)),hAPP(c_Finite__Set_Ocard(X0),X2)))|X2=X1)),
% 27.19/4.51 inference(cnf_transformation,[status(thm)],[f5273])).
% 27.19/4.51 fof(f5275,plain,(
% 27.19/4.51 ![V_A_2,V_B_2,T_b]: (~hBOOL(hAPP(c_Finite__Set_Ofinite(T_b),V_B_2))|(~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_A_2),V_B_2))|hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(T_b),V_A_2)),hAPP(c_Finite__Set_Ocard(T_b),V_B_2)))))),
% 27.19/4.51 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 27.19/4.51 fof(f5276,plain,(
% 27.19/4.51 ![V_B_2,T_b]: (~hBOOL(hAPP(c_Finite__Set_Ofinite(T_b),V_B_2))|(![V_A_2]: (~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_A_2),V_B_2))|hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(T_b),V_A_2)),hAPP(c_Finite__Set_Ocard(T_b),V_B_2))))))),
% 27.19/4.51 inference(miniscoping,[status(thm)],[f5275])).
% 27.19/4.51 fof(f5277,plain,(
% 27.19/4.51 ![X0,X1,X2]: (~hBOOL(hAPP(c_Finite__Set_Ofinite(X0),X1))|~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool)),X2),X1))|hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(X0),X2)),hAPP(c_Finite__Set_Ocard(X0),X1))))),
% 27.19/4.51 inference(cnf_transformation,[status(thm)],[f5276])).
% 27.19/4.51 fof(f5331,plain,(
% 27.19/4.51 ![T_b,V_B_2,V_A_2]: (~V_A_2=V_B_2|(hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_A_2),V_B_2))&hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_B_2),V_A_2))))),
% 27.19/4.51 inference(pre_NNF_transformation,[status(thm)],[f32])).
% 27.19/4.51 fof(f5332,plain,(
% 27.19/4.51 ![V_B_2,V_A_2]: (~V_A_2=V_B_2|((![T_b]: hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_A_2),V_B_2)))&(![T_b]: hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(T_b,tc_HOL_Obool)),V_B_2),V_A_2)))))),
% 27.19/4.51 inference(miniscoping,[status(thm)],[f5331])).
% 27.19/4.51 fof(f5333,plain,(
% 27.19/4.51 ![X0,X1,X2]: (~X0=X1|hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X2,tc_HOL_Obool)),X0),X1)))),
% 27.19/4.51 inference(cnf_transformation,[status(thm)],[f5332])).
% 27.19/4.51 fof(f19881,plain,(
% 27.19/4.51 ![T_2,T_1]: (~class_Orderings_Opreorder(T_1)|class_Orderings_Opreorder(tc_fun(T_2,T_1)))),
% 27.19/4.51 inference(pre_NNF_transformation,[status(thm)],[f4993])).
% 27.19/4.51 fof(f19882,plain,(
% 27.19/4.51 ![T_1]: (~class_Orderings_Opreorder(T_1)|(![T_2]: class_Orderings_Opreorder(tc_fun(T_2,T_1))))),
% 27.19/4.51 inference(miniscoping,[status(thm)],[f19881])).
% 27.19/4.51 fof(f19883,plain,(
% 27.19/4.51 ![X0,X1]: (~class_Orderings_Opreorder(X0)|class_Orderings_Opreorder(tc_fun(X1,X0)))),
% 27.19/4.51 inference(cnf_transformation,[status(thm)],[f19882])).
% 27.19/4.51 fof(f19889,plain,(
% 27.19/4.51 ![T_2,T_1]: (~class_Orderings_Oorder(T_1)|class_Orderings_Oorder(tc_fun(T_2,T_1)))),
% 27.19/4.51 inference(pre_NNF_transformation,[status(thm)],[f4996])).
% 27.19/4.51 fof(f19890,plain,(
% 27.19/4.51 ![T_1]: (~class_Orderings_Oorder(T_1)|(![T_2]: class_Orderings_Oorder(tc_fun(T_2,T_1))))),
% 27.19/4.51 inference(miniscoping,[status(thm)],[f19889])).
% 27.19/4.51 fof(f19891,plain,(
% 27.19/4.51 ![X0,X1]: (~class_Orderings_Oorder(X0)|class_Orderings_Oorder(tc_fun(X1,X0)))),
% 27.19/4.51 inference(cnf_transformation,[status(thm)],[f19890])).
% 27.19/4.51 fof(f20038,plain,(
% 27.19/4.51 class_Orderings_Opreorder(tc_HOL_Obool)),
% 27.19/4.51 inference(cnf_transformation,[status(thm)],[f5132])).
% 27.19/4.51 fof(f20041,plain,(
% 27.19/4.51 class_Orderings_Oorder(tc_HOL_Obool)),
% 27.19/4.51 inference(cnf_transformation,[status(thm)],[f5135])).
% 27.19/4.51 fof(f20043,plain,(
% 27.19/4.51 class_Orderings_Oord(tc_HOL_Obool)),
% 27.19/4.51 inference(cnf_transformation,[status(thm)],[f5137])).
% 27.19/4.51 fof(f20146,plain,(
% 27.19/4.51 hBOOL(hAPP(c_Finite__Set_Ofinite(tc_Com_Opname),v_U))),
% 27.19/4.51 inference(cnf_transformation,[status(thm)],[f5224])).
% 27.19/4.51 fof(f20147,plain,(
% 27.19/4.51 hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),v_G),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)))),
% 27.19/4.51 inference(cnf_transformation,[status(thm)],[f5225])).
% 27.19/4.51 fof(f20148,plain,(
% 27.19/4.51 hAPP(c_Finite__Set_Ocard(t_a),v_G)=hAPP(c_Finite__Set_Ocard(t_a),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U))),
% 27.19/4.51 inference(cnf_transformation,[status(thm)],[f5226])).
% 27.19/4.51 fof(f20150,plain,(
% 27.19/4.51 ~v_G=hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)),
% 27.19/4.51 inference(cnf_transformation,[status(thm)],[f5229])).
% 27.19/4.51 fof(f20480,plain,(
% 27.19/4.51 ![X0,X1]: (hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool)),X1),X1)))),
% 27.19/4.51 inference(destructive_equality_resolution,[status(thm)],[f5333])).
% 27.19/4.51 fof(f20986,plain,(
% 27.19/4.51 ![X0,X1]: (hBOOL(hAPP(c_Finite__Set_Ofinite(X0),hAPP(c_Set_Oimage(tc_Com_Opname,X0,X1),v_U))))),
% 27.19/4.51 inference(resolution,[status(thm)],[f5237,f20146])).
% 27.19/4.51 fof(f21029,definition,(
% 27.19/4.51 sQ15_spl <=> (hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)=v_G)),
% 27.19/4.51 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 27.19/4.51 fof(f21030,plain,(
% 27.19/4.51 hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)=v_G|~sQ15_spl),
% 27.19/4.51 inference(component_clause,[status(thm)],[f21029])).
% 27.19/4.51 fof(f21251,definition,(
% 27.19/4.51 sQ24_spl <=> (hBOOL(hAPP(c_Finite__Set_Ofinite(t_a),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U))))),
% 27.19/4.51 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 27.19/4.51 fof(f21253,plain,(
% 27.19/4.51 ~hBOOL(hAPP(c_Finite__Set_Ofinite(t_a),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)))|sQ24_spl),
% 27.19/4.51 inference(component_clause,[status(thm)],[f21251])).
% 27.19/4.51 fof(f21256,plain,(
% 27.19/4.51 ![X0]: (~class_Orderings_Oord(tc_HOL_Obool)|hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool),hAPP(v_G,X0)),hAPP(hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U),X0))))),
% 27.19/4.51 inference(resolution,[status(thm)],[f5264,f20147])).
% 27.19/4.51 fof(f21259,definition,(
% 27.19/4.51 sQ25_spl <=> (class_Orderings_Oord(tc_HOL_Obool))),
% 27.19/4.51 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 27.19/4.51 fof(f21261,plain,(
% 27.19/4.51 ~class_Orderings_Oord(tc_HOL_Obool)|sQ25_spl),
% 27.19/4.51 inference(component_clause,[status(thm)],[f21259])).
% 27.19/4.51 fof(f21266,definition,(
% 27.19/4.51 ![X0]: (sQ27_spl <=> (hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool),hAPP(v_G,X0)),hAPP(hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U),X0)))))),
% 27.19/4.51 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 27.19/4.51 fof(f21267,plain,(
% 27.19/4.51 ![X0]: (hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_HOL_Obool),hAPP(v_G,X0)),hAPP(hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U),X0)))|~sQ27_spl)),
% 27.19/4.51 inference(component_clause,[status(thm)],[f21266])).
% 27.19/4.51 fof(f21269,plain,(
% 27.19/4.51 ~sQ25_spl|sQ27_spl),
% 27.19/4.51 inference(split_clause,[status(thm)],[f21256,f21259,f21266])).
% 27.19/4.51 fof(f21340,plain,(
% 27.19/4.51 $false|sQ24_spl),
% 27.19/4.51 inference(forward_subsumption_resolution,[status(thm)],[f21253,f20986])).
% 27.19/4.51 fof(f21341,plain,(
% 27.19/4.51 sQ24_spl),
% 27.19/4.51 inference(contradiction_clause,[status(thm)],[f21340])).
% 27.19/4.51 fof(f21924,plain,(
% 27.19/4.51 ![X0]: (~hBOOL(hAPP(c_Finite__Set_Ofinite(t_a),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)))|~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),X0),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)))|~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(t_a),v_G)),hAPP(c_Finite__Set_Ocard(t_a),X0)))|X0=hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U))),
% 27.19/4.51 inference(paramodulation,[status(thm)],[f20148,f5274])).
% 27.19/4.51 fof(f21926,definition,(
% 27.19/4.51 ![X0]: (sQ35_spl <=> (~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),X0),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)))|~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(t_a),v_G)),hAPP(c_Finite__Set_Ocard(t_a),X0)))|X0=hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)))),
% 27.19/4.51 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 27.19/4.51 fof(f21927,plain,(
% 27.19/4.51 ![X0]: (~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),X0),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)))|~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(t_a),v_G)),hAPP(c_Finite__Set_Ocard(t_a),X0)))|X0=hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)|~sQ35_spl)),
% 27.19/4.51 inference(component_clause,[status(thm)],[f21926])).
% 27.19/4.51 fof(f21929,plain,(
% 27.19/4.51 ~sQ24_spl|sQ35_spl),
% 27.19/4.51 inference(split_clause,[status(thm)],[f21924,f21251,f21926])).
% 27.19/4.51 fof(f21931,plain,(
% 27.19/4.51 ~hBOOL(hAPP(c_Finite__Set_Ofinite(t_a),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)))|hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(t_a),v_G)),hAPP(c_Finite__Set_Ocard(t_a),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U))))),
% 27.19/4.51 inference(resolution,[status(thm)],[f5277,f20147])).
% 27.19/4.51 fof(f21939,definition,(
% 27.19/4.51 sQ37_spl <=> (hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(t_a),v_G)),hAPP(c_Finite__Set_Ocard(t_a),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)))))),
% 27.19/4.51 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 27.19/4.51 fof(f21940,plain,(
% 27.19/4.51 hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(t_a),v_G)),hAPP(c_Finite__Set_Ocard(t_a),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U))))|~sQ37_spl),
% 27.19/4.51 inference(component_clause,[status(thm)],[f21939])).
% 27.19/4.51 fof(f21942,plain,(
% 27.19/4.51 ~sQ24_spl|sQ37_spl),
% 27.19/4.51 inference(split_clause,[status(thm)],[f21931,f21251,f21939])).
% 27.19/4.51 fof(f21944,plain,(
% 27.19/4.51 hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(t_a),v_G)),hAPP(c_Finite__Set_Ocard(t_a),v_G)))|~sQ37_spl),
% 27.19/4.51 inference(forward_demodulation,[status(thm)],[f20148,f21940])).
% 27.19/4.51 fof(f21960,definition,(
% 27.19/4.51 sQ38_spl <=> (hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),v_G),v_G)))),
% 27.19/4.51 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 27.19/4.51 fof(f21962,plain,(
% 27.19/4.51 ~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(t_a,tc_HOL_Obool)),v_G),v_G))|sQ38_spl),
% 27.19/4.51 inference(component_clause,[status(thm)],[f21960])).
% 27.19/4.51 fof(f22146,definition,(
% 27.19/4.51 sQ51_spl <=> (class_Orderings_Oorder(tc_fun(tc_Com_Opname,tc_HOL_Obool)))),
% 27.19/4.51 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 27.19/4.51 fof(f22148,plain,(
% 27.19/4.51 ~class_Orderings_Oorder(tc_fun(tc_Com_Opname,tc_HOL_Obool))|sQ51_spl),
% 27.19/4.51 inference(component_clause,[status(thm)],[f22146])).
% 27.19/4.51 fof(f22153,definition,(
% 27.19/4.51 sQ53_spl <=> (class_Orderings_Oorder(tc_fun(t_a,tc_HOL_Obool)))),
% 27.19/4.51 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 27.19/4.51 fof(f22155,plain,(
% 27.19/4.51 ~class_Orderings_Oorder(tc_fun(t_a,tc_HOL_Obool))|sQ53_spl),
% 27.19/4.51 inference(component_clause,[status(thm)],[f22153])).
% 27.19/4.51 fof(f22194,plain,(
% 27.19/4.51 $false|~sQ15_spl),
% 27.19/4.51 inference(forward_subsumption_resolution,[status(thm)],[f21030,f20150])).
% 27.19/4.51 fof(f22195,plain,(
% 27.19/4.51 ~sQ15_spl),
% 27.19/4.51 inference(contradiction_clause,[status(thm)],[f22194])).
% 27.19/4.51 fof(f22224,definition,(
% 27.19/4.51 sQ67_spl <=> (hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(t_a),v_G)),hAPP(c_Finite__Set_Ocard(t_a),v_G))))),
% 27.19/4.51 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 27.19/4.51 fof(f22226,plain,(
% 27.19/4.51 ~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(t_a),v_G)),hAPP(c_Finite__Set_Ocard(t_a),v_G)))|sQ67_spl),
% 27.19/4.51 inference(component_clause,[status(thm)],[f22224])).
% 27.19/4.51 fof(f22449,definition,(
% 27.19/4.51 sQ82_spl <=> (class_Orderings_Opreorder(tc_fun(tc_Com_Opname,tc_HOL_Obool)))),
% 27.19/4.51 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 27.19/4.51 fof(f22451,plain,(
% 27.19/4.51 ~class_Orderings_Opreorder(tc_fun(tc_Com_Opname,tc_HOL_Obool))|sQ82_spl),
% 27.19/4.51 inference(component_clause,[status(thm)],[f22449])).
% 27.19/4.51 fof(f22456,definition,(
% 27.19/4.51 sQ84_spl <=> (class_Orderings_Opreorder(tc_fun(t_a,tc_HOL_Obool)))),
% 27.19/4.51 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 27.19/4.51 fof(f22458,plain,(
% 27.19/4.51 ~class_Orderings_Opreorder(tc_fun(t_a,tc_HOL_Obool))|sQ84_spl),
% 27.19/4.51 inference(component_clause,[status(thm)],[f22456])).
% 27.19/4.51 fof(f22687,plain,(
% 27.19/4.51 $false|~sQ37_spl|sQ67_spl),
% 27.19/4.51 inference(forward_subsumption_resolution,[status(thm)],[f22226,f21944])).
% 27.19/4.51 fof(f22688,plain,(
% 27.19/4.51 ~sQ37_spl|sQ67_spl),
% 27.19/4.51 inference(contradiction_clause,[status(thm)],[f22687])).
% 27.19/4.51 fof(f23616,plain,(
% 27.19/4.51 $false|sQ25_spl),
% 27.19/4.51 inference(forward_subsumption_resolution,[status(thm)],[f20043,f21261])).
% 27.19/4.51 fof(f23617,plain,(
% 27.19/4.51 sQ25_spl),
% 27.19/4.51 inference(contradiction_clause,[status(thm)],[f23616])).
% 27.19/4.51 fof(f23662,definition,(
% 27.19/4.51 sQ110_spl <=> (class_Orderings_Opreorder(tc_HOL_Obool))),
% 27.19/4.51 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 27.19/4.51 fof(f23664,plain,(
% 27.19/4.51 ~class_Orderings_Opreorder(tc_HOL_Obool)|sQ110_spl),
% 27.19/4.51 inference(component_clause,[status(thm)],[f23662])).
% 27.19/4.51 fof(f23669,definition,(
% 27.19/4.51 sQ112_spl <=> (class_Orderings_Oorder(tc_HOL_Obool))),
% 27.19/4.51 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 27.19/4.51 fof(f23671,plain,(
% 27.19/4.51 ~class_Orderings_Oorder(tc_HOL_Obool)|sQ112_spl),
% 27.19/4.51 inference(component_clause,[status(thm)],[f23669])).
% 27.19/4.51 fof(f23680,plain,(
% 27.19/4.51 $false|sQ112_spl),
% 27.19/4.51 inference(forward_subsumption_resolution,[status(thm)],[f23671,f20041])).
% 27.19/4.51 fof(f23681,plain,(
% 27.19/4.51 sQ112_spl),
% 27.19/4.51 inference(contradiction_clause,[status(thm)],[f23680])).
% 27.19/4.51 fof(f23682,plain,(
% 27.19/4.51 $false|sQ110_spl),
% 27.19/4.51 inference(forward_subsumption_resolution,[status(thm)],[f23664,f20038])).
% 27.19/4.51 fof(f23683,plain,(
% 27.19/4.51 sQ110_spl),
% 27.19/4.51 inference(contradiction_clause,[status(thm)],[f23682])).
% 27.19/4.51 fof(f23820,plain,(
% 27.19/4.51 ![X0]: (~class_Orderings_Oord(tc_HOL_Obool)|hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool)),v_G),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)))|~sQ27_spl)),
% 27.19/4.51 inference(resolution,[status(thm)],[f21267,f5265])).
% 27.19/4.51 fof(f23824,definition,(
% 27.19/4.51 ![X0]: (sQ117_spl <=> (hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool)),v_G),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)))))),
% 27.19/4.51 introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 27.19/4.51 fof(f23825,plain,(
% 27.19/4.51 ![X0]: (hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(X0,tc_HOL_Obool)),v_G),hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)))|~sQ117_spl)),
% 27.19/4.51 inference(component_clause,[status(thm)],[f23824])).
% 27.19/4.51 fof(f23827,plain,(
% 27.19/4.51 ~sQ25_spl|sQ117_spl|~sQ27_spl),
% 27.19/4.51 inference(split_clause,[status(thm)],[f23820,f21259,f23824,f21266])).
% 27.19/4.51 fof(f25409,definition,(
% 27.19/4.51 sQ137_spl <=> (hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(tc_Com_Opname,tc_HOL_Obool)),v_U),v_U)))),
% 27.19/4.51 introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition])).
% 27.19/4.51 fof(f25411,plain,(
% 27.19/4.51 ~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_fun(tc_Com_Opname,tc_HOL_Obool)),v_U),v_U))|sQ137_spl),
% 27.19/4.51 inference(component_clause,[status(thm)],[f25409])).
% 27.19/4.51 fof(f25461,plain,(
% 27.19/4.51 $false|sQ137_spl),
% 27.19/4.51 inference(forward_subsumption_resolution,[status(thm)],[f25411,f20480])).
% 27.19/4.51 fof(f25462,plain,(
% 27.19/4.51 sQ137_spl),
% 27.19/4.51 inference(contradiction_clause,[status(thm)],[f25461])).
% 27.19/4.51 fof(f25463,plain,(
% 27.19/4.51 $false|sQ38_spl),
% 27.19/4.51 inference(forward_subsumption_resolution,[status(thm)],[f21962,f20480])).
% 27.19/4.51 fof(f25464,plain,(
% 27.19/4.51 sQ38_spl),
% 27.19/4.51 inference(contradiction_clause,[status(thm)],[f25463])).
% 27.19/4.51 fof(f32141,definition,(
% 27.19/4.51 sQ204_spl <=> (hBOOL(hAPP(c_Finite__Set_Ofinite(tc_Com_Opname),hAPP(c_Set_Oimage(tc_Com_Opname,tc_Com_Opname,c_Fun_Oid(tc_Com_Opname)),v_U))))),
% 27.19/4.51 introduced(definition,[new_symbols(definition,[sQ204_spl])],[split_symbol_definition])).
% 27.19/4.51 fof(f32143,plain,(
% 27.19/4.51 ~hBOOL(hAPP(c_Finite__Set_Ofinite(tc_Com_Opname),hAPP(c_Set_Oimage(tc_Com_Opname,tc_Com_Opname,c_Fun_Oid(tc_Com_Opname)),v_U)))|sQ204_spl),
% 27.19/4.51 inference(component_clause,[status(thm)],[f32141])).
% 27.19/4.51 fof(f32150,plain,(
% 27.19/4.51 $false|sQ204_spl),
% 27.19/4.51 inference(forward_subsumption_resolution,[status(thm)],[f32143,f20986])).
% 27.19/4.51 fof(f32151,plain,(
% 27.19/4.51 sQ204_spl),
% 27.19/4.51 inference(contradiction_clause,[status(thm)],[f32150])).
% 27.19/4.51 fof(f34714,plain,(
% 27.19/4.51 ![X0]: (class_Orderings_Opreorder(tc_fun(X0,tc_HOL_Obool)))),
% 27.19/4.51 inference(resolution,[status(thm)],[f19883,f20038])).
% 27.19/4.51 fof(f34719,plain,(
% 27.19/4.51 $false|sQ82_spl),
% 27.19/4.51 inference(backward_subsumption_resolution,[status(thm)],[f22451,f34714])).
% 27.19/4.51 fof(f34720,plain,(
% 27.19/4.51 $false|sQ84_spl),
% 27.19/4.51 inference(backward_subsumption_resolution,[status(thm)],[f22458,f34714])).
% 27.19/4.51 fof(f34723,plain,(
% 27.19/4.51 sQ82_spl),
% 27.19/4.51 inference(contradiction_clause,[status(thm)],[f34719])).
% 27.19/4.51 fof(f34724,plain,(
% 27.19/4.51 sQ84_spl),
% 27.19/4.51 inference(contradiction_clause,[status(thm)],[f34720])).
% 27.19/4.51 fof(f34742,plain,(
% 27.19/4.51 ![X0]: (class_Orderings_Oorder(tc_fun(X0,tc_HOL_Obool)))),
% 27.19/4.51 inference(resolution,[status(thm)],[f19891,f20041])).
% 27.19/4.51 fof(f34747,plain,(
% 27.19/4.51 $false|sQ51_spl),
% 27.19/4.51 inference(backward_subsumption_resolution,[status(thm)],[f22148,f34742])).
% 27.19/4.51 fof(f34748,plain,(
% 27.19/4.51 $false|sQ53_spl),
% 27.19/4.51 inference(backward_subsumption_resolution,[status(thm)],[f22155,f34742])).
% 27.19/4.51 fof(f34751,plain,(
% 27.19/4.51 sQ51_spl),
% 27.19/4.51 inference(contradiction_clause,[status(thm)],[f34747])).
% 27.19/4.51 fof(f34752,plain,(
% 27.19/4.51 sQ53_spl),
% 27.19/4.51 inference(contradiction_clause,[status(thm)],[f34748])).
% 27.19/4.51 fof(f35061,definition,(
% 27.19/4.51 ![X0]: (sQ226_spl <=> (v_G=X0))),
% 27.19/4.51 introduced(definition,[new_symbols(definition,[sQ226_spl])],[split_symbol_definition])).
% 28.00/4.61 fof(f35062,plain,(
% 28.00/4.61 ![X0]: (v_G=X0|~sQ226_spl)),
% 28.00/4.61 inference(component_clause,[status(thm)],[f35061])).
% 28.00/4.61 fof(f35068,plain,(
% 28.00/4.61 $false|~sQ226_spl),
% 28.00/4.61 inference(backward_subsumption_resolution,[status(thm)],[f20150,f35062])).
% 28.00/4.61 fof(f35139,plain,(
% 28.00/4.61 ~sQ226_spl),
% 28.00/4.61 inference(contradiction_clause,[status(thm)],[f35068])).
% 28.00/4.61 fof(f35261,plain,(
% 28.00/4.61 ~hBOOL(hAPP(hAPP(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat),hAPP(c_Finite__Set_Ocard(t_a),v_G)),hAPP(c_Finite__Set_Ocard(t_a),v_G)))|v_G=hAPP(c_Set_Oimage(tc_Com_Opname,t_a,v_mgt__call),v_U)|~sQ35_spl|~sQ117_spl),
% 28.00/4.61 inference(resolution,[status(thm)],[f21927,f23825])).
% 28.00/4.61 fof(f35273,plain,(
% 28.00/4.61 ~sQ67_spl|sQ15_spl|~sQ35_spl|~sQ117_spl),
% 28.00/4.61 inference(split_clause,[status(thm)],[f35261,f22224,f21029,f21926,f23824])).
% 28.00/4.61 fof(f35280,plain,(
% 28.00/4.61 $false),
% 28.00/4.61 inference(sat_refutation,[status(thm)],[f21269,f21341,f21929,f21942,f22195,f22688,f23617,f23681,f23683,f23827,f25462,f25464,f32151,f34723,f34724,f34751,f34752,f35139,f35273])).
% 28.00/4.61 % SZS output end CNFRefutation for theBenchmark.p
% 28.00/4.63 % Elapsed time: 4.208980 seconds
% 28.00/4.63 % CPU time: 28.239601 seconds
% 28.00/4.63 % Total memory used: 882.955 MB
% 28.00/4.63 % Net memory used: 871.434 MB
%------------------------------------------------------------------------------