%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV580-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 : n020.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:52:51 PM UTC 2026
% Result : Unsatisfiable 0.28s 0.74s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWV580-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.45 % Computer : n020.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Mon Sep 21 09:12:33 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.28/0.59 % Drodi V4.1.1
% 0.28/0.74 % Refutation found
% 0.28/0.74 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.28/0.74 % SZS output start CNFRefutation for theBenchmark
% 0.28/0.74 fof(f187,axiom,(
% 0.28/0.74 (![T_a,V_f,V_m,V_n]: (( ~ class_OrderedGroup_Ocomm__monoid__add(T_a)| c_Finite__Set_Osetsum(V_f,c_SetInterval_Oord__class_OatLeastLessThan(V_m,V_n,tc_nat),tc_nat,T_a) = c_HOL_Oplus__class_Oplus(hAPP(V_f,V_m),c_Finite__Set_Osetsum(V_f,c_SetInterval_Oord__class_OatLeastLessThan(c_Suc(V_m),V_n,tc_nat),tc_nat,T_a),T_a)| ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ))),
% 0.28/0.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.74 fof(f499,axiom,(
% 0.28/0.74 c_HOL_Oord__class_Oless(v_m,v_n,tc_nat) ),
% 0.28/0.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.74 fof(f502,axiom,(
% 0.28/0.74 (![V_l,V_u]: (c_SetInterval_Oord__class_OatLeastLessThan(c_Suc(V_l),V_u,tc_nat) = c_SetInterval_Oord__class_OgreaterThanLessThan(V_l,V_u,tc_nat) ))),
% 0.28/0.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.74 fof(f508,axiom,(
% 0.28/0.74 ( ~ class_OrderedGroup_Ocomm__monoid__add(t_a)| c_HOL_Oplus__class_Oplus(hAPP(v_f,v_m),c_Finite__Set_Osetsum(v_f,c_SetInterval_Oord__class_OgreaterThanLessThan(v_m,v_n,tc_nat),tc_nat,t_a),t_a) = c_Finite__Set_Osetsum(v_f,c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(v_m,c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),c_SetInterval_Oord__class_OgreaterThanLessThan(v_m,v_n,tc_nat),tc_fun(tc_nat,tc_bool)),tc_nat,t_a) ) ),
% 0.28/0.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.74 fof(f553,negated_conjecture,(
% 0.28/0.74 class_OrderedGroup_Ocomm__monoid__add(t_a) ),
% 0.28/0.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.74 fof(f554,negated_conjecture,(
% 0.28/0.74 c_Finite__Set_Osetsum(v_f,c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(v_m,c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),c_SetInterval_Oord__class_OgreaterThanLessThan(v_m,v_n,tc_nat),tc_fun(tc_nat,tc_bool)),tc_nat,t_a) != c_Finite__Set_Osetsum(v_f,c_SetInterval_Oord__class_OatLeastLessThan(v_m,v_n,tc_nat),tc_nat,t_a) ),
% 0.28/0.74 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.74 fof(f902,plain,(
% 0.28/0.74 ![V_m,V_n]: ((![T_a]: (~class_OrderedGroup_Ocomm__monoid__add(T_a)|(![V_f]: c_Finite__Set_Osetsum(V_f,c_SetInterval_Oord__class_OatLeastLessThan(V_m,V_n,tc_nat),tc_nat,T_a)=c_HOL_Oplus__class_Oplus(hAPP(V_f,V_m),c_Finite__Set_Osetsum(V_f,c_SetInterval_Oord__class_OatLeastLessThan(c_Suc(V_m),V_n,tc_nat),tc_nat,T_a),T_a))))|~c_HOL_Oord__class_Oless(V_m,V_n,tc_nat))),
% 0.28/0.74 inference(miniscoping,[status(thm)],[f187])).
% 0.28/0.74 fof(f903,plain,(
% 0.28/0.74 ![X0,X1,X2,X3]: (~class_OrderedGroup_Ocomm__monoid__add(X0)|c_Finite__Set_Osetsum(X1,c_SetInterval_Oord__class_OatLeastLessThan(X2,X3,tc_nat),tc_nat,X0)=c_HOL_Oplus__class_Oplus(hAPP(X1,X2),c_Finite__Set_Osetsum(X1,c_SetInterval_Oord__class_OatLeastLessThan(c_Suc(X2),X3,tc_nat),tc_nat,X0),X0)|~c_HOL_Oord__class_Oless(X2,X3,tc_nat))),
% 0.28/0.74 inference(cnf_transformation,[status(thm)],[f902])).
% 0.28/0.74 fof(f1387,plain,(
% 0.28/0.74 c_HOL_Oord__class_Oless(v_m,v_n,tc_nat)),
% 0.28/0.74 inference(cnf_transformation,[status(thm)],[f499])).
% 0.28/0.74 fof(f1390,plain,(
% 0.28/0.74 ![X0,X1]: (c_SetInterval_Oord__class_OatLeastLessThan(c_Suc(X0),X1,tc_nat)=c_SetInterval_Oord__class_OgreaterThanLessThan(X0,X1,tc_nat))),
% 0.28/0.74 inference(cnf_transformation,[status(thm)],[f502])).
% 0.28/0.74 fof(f1398,plain,(
% 0.28/0.74 ~class_OrderedGroup_Ocomm__monoid__add(t_a)|c_HOL_Oplus__class_Oplus(hAPP(v_f,v_m),c_Finite__Set_Osetsum(v_f,c_SetInterval_Oord__class_OgreaterThanLessThan(v_m,v_n,tc_nat),tc_nat,t_a),t_a)=c_Finite__Set_Osetsum(v_f,c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(v_m,c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),c_SetInterval_Oord__class_OgreaterThanLessThan(v_m,v_n,tc_nat),tc_fun(tc_nat,tc_bool)),tc_nat,t_a)),
% 0.28/0.74 inference(cnf_transformation,[status(thm)],[f508])).
% 0.28/0.74 fof(f1468,plain,(
% 0.28/0.74 class_OrderedGroup_Ocomm__monoid__add(t_a)),
% 0.28/0.74 inference(cnf_transformation,[status(thm)],[f553])).
% 0.28/0.74 fof(f1469,plain,(
% 0.28/0.74 ~c_Finite__Set_Osetsum(v_f,c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(v_m,c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),c_SetInterval_Oord__class_OgreaterThanLessThan(v_m,v_n,tc_nat),tc_fun(tc_nat,tc_bool)),tc_nat,t_a)=c_Finite__Set_Osetsum(v_f,c_SetInterval_Oord__class_OatLeastLessThan(v_m,v_n,tc_nat),tc_nat,t_a)),
% 0.28/0.76 inference(cnf_transformation,[status(thm)],[f554])).
% 0.28/0.76 fof(f1676,plain,(
% 0.28/0.76 ![X0,X1,X2]: (c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,X2,tc_nat),tc_nat,t_a)=c_HOL_Oplus__class_Oplus(hAPP(X0,X1),c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(c_Suc(X1),X2,tc_nat),tc_nat,t_a),t_a)|~c_HOL_Oord__class_Oless(X1,X2,tc_nat))),
% 0.28/0.76 inference(resolution,[status(thm)],[f903,f1468])).
% 0.28/0.76 fof(f1744,plain,(
% 0.28/0.76 ![X0]: (c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(v_m,v_n,tc_nat),tc_nat,t_a)=c_HOL_Oplus__class_Oplus(hAPP(X0,v_m),c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(c_Suc(v_m),v_n,tc_nat),tc_nat,t_a),t_a))),
% 0.28/0.76 inference(resolution,[status(thm)],[f1676,f1387])).
% 0.28/0.76 fof(f2191,plain,(
% 0.28/0.76 ![X0]: (c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(v_m,v_n,tc_nat),tc_nat,t_a)=c_HOL_Oplus__class_Oplus(hAPP(X0,v_m),c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OgreaterThanLessThan(v_m,v_n,tc_nat),tc_nat,t_a),t_a))),
% 0.28/0.76 inference(forward_demodulation,[status(thm)],[f1390,f1744])).
% 0.28/0.76 fof(f2399,plain,(
% 0.28/0.76 ~class_OrderedGroup_Ocomm__monoid__add(t_a)|c_Finite__Set_Osetsum(v_f,c_SetInterval_Oord__class_OatLeastLessThan(v_m,v_n,tc_nat),tc_nat,t_a)=c_Finite__Set_Osetsum(v_f,c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(v_m,c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),c_SetInterval_Oord__class_OgreaterThanLessThan(v_m,v_n,tc_nat),tc_fun(tc_nat,tc_bool)),tc_nat,t_a)),
% 0.28/0.76 inference(forward_demodulation,[status(thm)],[f2191,f1398])).
% 0.28/0.76 fof(f2400,plain,(
% 0.28/0.76 ~c_Finite__Set_Osetsum(v_f,c_SetInterval_Oord__class_OatLeastLessThan(v_m,v_n,tc_nat),tc_nat,t_a)=c_Finite__Set_Osetsum(v_f,c_SetInterval_Oord__class_OatLeastLessThan(v_m,v_n,tc_nat),tc_nat,t_a)),
% 0.28/0.76 inference(backward_demodulation,[status(thm)],[f2401,f1469])).
% 0.28/0.76 fof(f2401,plain,(
% 0.28/0.76 c_Finite__Set_Osetsum(v_f,c_SetInterval_Oord__class_OatLeastLessThan(v_m,v_n,tc_nat),tc_nat,t_a)=c_Finite__Set_Osetsum(v_f,c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(v_m,c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),c_SetInterval_Oord__class_OgreaterThanLessThan(v_m,v_n,tc_nat),tc_fun(tc_nat,tc_bool)),tc_nat,t_a)),
% 0.28/0.76 inference(forward_subsumption_resolution,[status(thm)],[f2399,f1468])).
% 0.28/0.76 fof(f2403,plain,(
% 0.28/0.76 $false),
% 0.28/0.76 inference(trivial_equality_resolution,[status(thm)],[f2400])).
% 0.28/0.76 % SZS output end CNFRefutation for theBenchmark.p
% 0.28/0.79 % Elapsed time: 0.312543 seconds
% 0.28/0.79 % CPU time: 1.347677 seconds
% 0.28/0.79 % Total memory used: 143.116 MB
% 0.28/0.79 % Net memory used: 142.482 MB
%------------------------------------------------------------------------------