%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV886-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:53:18 PM UTC 2026
% Result : Unsatisfiable 22.21s 3.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV886-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.43 % Computer : n011.cluster.edu
% 0.15/0.43 % Model : x86_64 x86_64
% 0.15/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.43 % Memory : 8046.5625MB
% 0.15/0.43 % OS : Linux 6.8.0-71-generic
% 0.15/0.43 % CPULimit : 300
% 0.15/0.43 % WCLimit : 300
% 0.15/0.43 % DateTime : Mon Sep 21 09:30:10 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.49 % Drodi V4.1.1
% 22.21/3.38 % Refutation found
% 22.21/3.38 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 22.21/3.38 % SZS output start CNFRefutation for theBenchmark
% 22.21/3.38 fof(f138,axiom,(
% 22.21/3.38 (![V_x,V_A,T_a]: (( c_HOL_Ominus__class_Ominus(c_Set_Oinsert(V_x,V_A,T_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)) = V_A| c_in(V_x,V_A,T_a) ) ))),
% 22.21/3.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.21/3.38 fof(f163,axiom,(
% 22.21/3.38 (![V_m,V_n]: (c_HOL_Oplus__class_Oplus(c_Suc(V_m),V_n,tc_nat) = c_HOL_Oplus__class_Oplus(V_m,c_Suc(V_n),tc_nat) ))),
% 22.21/3.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.21/3.38 fof(f182,axiom,(
% 22.21/3.38 (![V_A,V_B,T_a]: (c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),V_B,tc_fun(T_a,tc_bool)) = c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)) ))),
% 22.21/3.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.21/3.38 fof(f331,axiom,(
% 22.21/3.38 (![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 ))),
% 22.21/3.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.21/3.38 fof(f366,axiom,(
% 22.21/3.38 (![V_x,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))| ~ c_Finite__Set_Ofinite(V_A,T_a) ) ))),
% 22.21/3.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.21/3.38 fof(f377,axiom,(
% 22.21/3.38 (![V_m,V_n]: (( c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat),V_n,tc_nat) = V_m| ~ c_lessequals(V_n,V_m,tc_nat) ) ))),
% 22.21/3.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.21/3.38 fof(f378,axiom,(
% 22.21/3.38 (![V_n,V_m]: (( c_HOL_Oplus__class_Oplus(V_n,c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat),tc_nat) = V_m| ~ c_lessequals(V_n,V_m,tc_nat) ) ))),
% 22.21/3.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.21/3.38 fof(f582,negated_conjecture,(
% 22.21/3.38 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) ),
% 22.21/3.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.21/3.38 fof(f583,negated_conjecture,(
% 22.21/3.38 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) ),
% 22.21/3.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.21/3.38 fof(f585,negated_conjecture,(
% 22.21/3.38 ~ c_in(hAPP(v_mgt__call,v_pn),v_G,t_a) ),
% 22.21/3.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.21/3.38 fof(f586,negated_conjecture,(
% 22.21/3.38 c_Finite__Set_Ofinite(v_G,t_a) ),
% 22.21/3.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.21/3.38 fof(f587,negated_conjecture,(
% 22.21/3.38 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) ),
% 22.21/3.38 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 22.21/3.38 fof(f842,plain,(
% 22.21/3.38 ![X0,X1,X2]: (c_HOL_Ominus__class_Ominus(c_Set_Oinsert(X0,X1,X2),c_Set_Oinsert(X0,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2),tc_fun(X2,tc_bool))=X1|c_in(X0,X1,X2))),
% 22.21/3.38 inference(cnf_transformation,[status(thm)],[f138])).
% 22.21/3.38 fof(f873,plain,(
% 22.21/3.38 ![X0,X1]: (c_HOL_Oplus__class_Oplus(c_Suc(X0),X1,tc_nat)=c_HOL_Oplus__class_Oplus(X0,c_Suc(X1),tc_nat))),
% 22.21/3.38 inference(cnf_transformation,[status(thm)],[f163])).
% 22.21/3.38 fof(f900,plain,(
% 22.21/3.38 ![X0,X1,X2]: (c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(X0,X1,tc_fun(X2,tc_bool)),X1,tc_fun(X2,tc_bool))=c_HOL_Ominus__class_Ominus(X0,X1,tc_fun(X2,tc_bool)))),
% 22.21/3.38 inference(cnf_transformation,[status(thm)],[f182])).
% 22.21/3.38 fof(f1125,plain,(
% 22.21/3.38 ![X0,X1]: (c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X0,tc_nat)=X1)),
% 22.21/3.38 inference(cnf_transformation,[status(thm)],[f331])).
% 22.21/3.38 fof(f1179,plain,(
% 22.21/3.38 ![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)))|~c_Finite__Set_Ofinite(V_A,T_a))),
% 22.21/3.38 inference(miniscoping,[status(thm)],[f366])).
% 22.21/3.38 fof(f1180,plain,(
% 22.21/3.38 ![X0,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))|~c_Finite__Set_Ofinite(X1,X2))),
% 22.21/3.38 inference(cnf_transformation,[status(thm)],[f1179])).
% 22.21/3.38 fof(f1197,plain,(
% 22.21/3.38 ![X0,X1]: (c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(X0,X1,tc_nat),X1,tc_nat)=X0|~c_lessequals(X1,X0,tc_nat))),
% 22.21/3.38 inference(cnf_transformation,[status(thm)],[f377])).
% 22.21/3.38 fof(f1198,plain,(
% 22.21/3.38 ![X0,X1]: (c_HOL_Oplus__class_Oplus(X0,c_HOL_Ominus__class_Ominus(X1,X0,tc_nat),tc_nat)=X1|~c_lessequals(X0,X1,tc_nat))),
% 22.21/3.38 inference(cnf_transformation,[status(thm)],[f378])).
% 22.21/3.38 fof(f1502,plain,(
% 22.21/3.38 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)),
% 22.21/3.38 inference(cnf_transformation,[status(thm)],[f582])).
% 22.21/3.38 fof(f1503,plain,(
% 22.21/3.38 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)),
% 22.21/3.38 inference(cnf_transformation,[status(thm)],[f583])).
% 22.21/3.38 fof(f1505,plain,(
% 22.21/3.38 ~c_in(hAPP(v_mgt__call,v_pn),v_G,t_a)),
% 22.21/3.38 inference(cnf_transformation,[status(thm)],[f585])).
% 22.21/3.38 fof(f1506,plain,(
% 22.21/3.38 c_Finite__Set_Ofinite(v_G,t_a)),
% 22.21/3.38 inference(cnf_transformation,[status(thm)],[f586])).
% 22.21/3.38 fof(f1507,plain,(
% 22.21/3.38 ~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)),
% 22.21/3.38 inference(cnf_transformation,[status(thm)],[f587])).
% 22.21/3.38 fof(f2481,plain,(
% 22.21/3.38 c_HOL_Ominus__class_Ominus(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a),c_Set_Oinsert(hAPP(v_mgt__call,v_pn),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a),tc_fun(t_a,tc_bool))=v_G),
% 22.21/3.38 inference(resolution,[status(thm)],[f842,f1505])).
% 22.21/3.38 fof(f2503,plain,(
% 22.21/3.38 c_HOL_Ominus__class_Ominus(v_G,c_Set_Oinsert(hAPP(v_mgt__call,v_pn),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a),tc_fun(t_a,tc_bool))=c_HOL_Ominus__class_Ominus(c_Set_Oinsert(hAPP(v_mgt__call,v_pn),v_G,t_a),c_Set_Oinsert(hAPP(v_mgt__call,v_pn),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a),tc_fun(t_a,tc_bool))),
% 22.21/3.38 inference(paramodulation,[status(thm)],[f2481,f900])).
% 22.21/3.38 fof(f2512,plain,(
% 22.21/3.38 c_HOL_Ominus__class_Ominus(v_G,c_Set_Oinsert(hAPP(v_mgt__call,v_pn),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a),tc_fun(t_a,tc_bool))=v_G),
% 22.21/3.38 inference(forward_demodulation,[status(thm)],[f2481,f2503])).
% 22.21/3.38 fof(f2887,plain,(
% 22.21/3.38 ![X0]: (c_Finite__Set_Ocard(c_Set_Oinsert(X0,v_G,t_a),t_a)=c_Suc(c_Finite__Set_Ocard(c_HOL_Ominus__class_Ominus(v_G,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)))),
% 22.21/3.38 inference(resolution,[status(thm)],[f1180,f1506])).
% 22.21/3.38 fof(f3364,plain,(
% 22.21/3.38 c_HOL_Oplus__class_Oplus(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),c_Suc(v_na),tc_nat)=c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a)),
% 22.21/3.38 inference(resolution,[status(thm)],[f1197,f1502])).
% 22.21/3.38 fof(f3376,plain,(
% 22.21/3.38 c_HOL_Oplus__class_Oplus(c_Finite__Set_Ocard(v_G,t_a),c_Suc(v_na),tc_nat)=c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a)),
% 22.21/3.38 inference(forward_demodulation,[status(thm)],[f1503,f3364])).
% 22.21/3.38 fof(f3386,plain,(
% 22.21/3.38 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)),
% 22.21/3.38 inference(resolution,[status(thm)],[f1198,f1502])).
% 22.21/3.38 fof(f3398,plain,(
% 22.21/3.38 c_HOL_Oplus__class_Oplus(v_na,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)),tc_nat)=c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a)),
% 22.21/3.38 inference(forward_demodulation,[status(thm)],[f873,f3386])).
% 22.21/3.38 fof(f3399,plain,(
% 22.21/3.38 c_HOL_Oplus__class_Oplus(v_na,c_Suc(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)),
% 22.21/3.42 inference(forward_demodulation,[status(thm)],[f1503,f3398])).
% 22.21/3.42 fof(f3696,plain,(
% 22.21/3.42 ~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_HOL_Oplus__class_Oplus(c_Finite__Set_Ocard(v_G,t_a),c_Suc(v_na),tc_nat),v_na,tc_nat)),
% 22.21/3.42 inference(backward_demodulation,[status(thm)],[f3376,f1507])).
% 22.21/3.42 fof(f4041,plain,(
% 22.21/3.42 c_HOL_Oplus__class_Oplus(c_Finite__Set_Ocard(v_G,t_a),c_Suc(v_na),tc_nat)=c_HOL_Oplus__class_Oplus(v_na,c_Suc(c_Finite__Set_Ocard(v_G,t_a)),tc_nat)),
% 22.21/3.42 inference(backward_demodulation,[status(thm)],[f3399,f3376])).
% 22.21/3.42 fof(f5589,plain,(
% 22.21/3.42 ~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_HOL_Oplus__class_Oplus(v_na,c_Suc(c_Finite__Set_Ocard(v_G,t_a)),tc_nat),v_na,tc_nat)),
% 22.21/3.42 inference(backward_demodulation,[status(thm)],[f4041,f3696])).
% 22.21/3.42 fof(f5636,plain,(
% 22.21/3.42 ~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))),
% 22.21/3.42 inference(forward_demodulation,[status(thm)],[f1125,f5589])).
% 22.21/3.42 fof(f10884,plain,(
% 22.21/3.42 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))),
% 22.21/3.42 inference(paramodulation,[status(thm)],[f2512,f2887])).
% 22.21/3.42 fof(f10911,plain,(
% 22.21/3.42 $false),
% 22.21/3.42 inference(forward_subsumption_resolution,[status(thm)],[f10884,f5636])).
% 22.21/3.42 % SZS output end CNFRefutation for theBenchmark.p
% 10.19/3.44 % Elapsed time: 2.993132 seconds
% 10.19/3.44 % CPU time: 23.011867 seconds
% 10.19/3.44 % Total memory used: 325.973 MB
% 10.19/3.44 % Net memory used: 311.343 MB
%------------------------------------------------------------------------------