%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ANA023-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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 12:02:31 PM UTC 2026
% Result : Unsatisfiable 0.08s 0.37s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ANA023-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n017.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 13:19:42 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 0.08/0.37 % Refutation found
% 0.08/0.37 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.08/0.37 % SZS output start CNFRefutation for theBenchmark
% 0.08/0.37 fof(f1,axiom,(
% 0.08/0.37 (![A,B,C]: (ifeq2(A,A,B,C) = B ))),
% 0.08/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f2,axiom,(
% 0.08/0.37 (![A,B,C]: (ifeq(A,A,B,C) = B ))),
% 0.08/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f3,axiom,(
% 0.08/0.37 (![T_a,V_y]: (ifeq2(class_OrderedGroup_Ocomm__monoid__add(T_a),true,c_plus(c_0,V_y,T_a),V_y) = V_y ))),
% 0.08/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f4,axiom,(
% 0.08/0.37 (![T_a,V_a,V_c,V_b]: (ifeq(class_OrderedGroup_Opordered__ab__group__add(T_a),true,ifeq(c_lessequals(V_a,c_minus(V_c,V_b,T_a),T_a),true,c_lessequals(c_plus(V_a,V_b,T_a),V_c,T_a),true),true) = true ))),
% 0.08/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f5,axiom,(
% 0.08/0.37 (![T_a,V_a,V_b,V_c]: (ifeq(class_OrderedGroup_Opordered__ab__group__add(T_a),true,ifeq(c_lessequals(c_plus(V_a,V_b,T_a),V_c,T_a),true,c_lessequals(V_a,c_minus(V_c,V_b,T_a),T_a),true),true) = true ))),
% 0.08/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f6,axiom,(
% 0.08/0.37 (![T_a,V_x,V_y,V_z]: (ifeq(class_Orderings_Oorder(T_a),true,ifeq(c_lessequals(V_x,V_y,T_a),true,ifeq(c_lessequals(V_y,V_z,T_a),true,c_lessequals(V_x,V_z,T_a),true),true),true) = true ))),
% 0.08/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f7,negated_conjecture,(
% 0.08/0.37 c_lessequals(c_0,c_minus(v_k(v_x),v_g(v_x),t_b),t_b) = true ),
% 0.08/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f8,negated_conjecture,(
% 0.08/0.37 c_lessequals(v_k(v_x),v_f(v_x),t_b) = true ),
% 0.08/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f9,negated_conjecture,(
% 0.08/0.37 c_lessequals(c_0,c_minus(v_f(v_x),v_g(v_x),t_b),t_b) != true ),
% 0.08/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f10,axiom,(
% 0.08/0.37 (![T]: (ifeq(class_Orderings_Olinorder(T),true,class_Orderings_Oorder(T),true) = true ))),
% 0.08/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f11,axiom,(
% 0.08/0.37 (![T]: (ifeq(class_Ring__and__Field_Oordered__idom(T),true,class_OrderedGroup_Ocomm__monoid__add(T),true) = true ))),
% 0.08/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f12,axiom,(
% 0.08/0.37 (![T]: (ifeq(class_Ring__and__Field_Oordered__idom(T),true,class_Orderings_Olinorder(T),true) = true ))),
% 0.08/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f13,axiom,(
% 0.08/0.37 (![T]: (ifeq(class_Ring__and__Field_Oordered__idom(T),true,class_OrderedGroup_Opordered__ab__group__add(T),true) = true ))),
% 0.08/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f14,negated_conjecture,(
% 0.08/0.37 class_Ring__and__Field_Oordered__idom(t_b) = true ),
% 0.08/0.37 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.08/0.37 fof(f15,plain,(
% 0.08/0.37 ![X0,X1,X2]: (ifeq2(X0,X0,X1,X2)=X1)),
% 0.08/0.37 inference(cnf_transformation,[status(thm)],[f1])).
% 0.08/0.37 fof(f16,plain,(
% 0.08/0.37 ![X0,X1,X2]: (ifeq(X0,X0,X1,X2)=X1)),
% 0.08/0.37 inference(cnf_transformation,[status(thm)],[f2])).
% 0.08/0.37 fof(f17,plain,(
% 0.08/0.37 ![X0,X1]: (ifeq2(class_OrderedGroup_Ocomm__monoid__add(X0),true,c_plus(c_0,X1,X0),X1)=X1)),
% 0.08/0.37 inference(cnf_transformation,[status(thm)],[f3])).
% 0.08/0.37 fof(f18,plain,(
% 0.08/0.37 ![X0,X1,X2,X3]: (ifeq(class_OrderedGroup_Opordered__ab__group__add(X0),true,ifeq(c_lessequals(X1,c_minus(X2,X3,X0),X0),true,c_lessequals(c_plus(X1,X3,X0),X2,X0),true),true)=true)),
% 0.08/0.37 inference(cnf_transformation,[status(thm)],[f4])).
% 0.08/0.37 fof(f19,plain,(
% 0.08/0.37 ![X0,X1,X2,X3]: (ifeq(class_OrderedGroup_Opordered__ab__group__add(X0),true,ifeq(c_lessequals(c_plus(X1,X2,X0),X3,X0),true,c_lessequals(X1,c_minus(X3,X2,X0),X0),true),true)=true)),
% 0.08/0.37 inference(cnf_transformation,[status(thm)],[f5])).
% 0.08/0.37 fof(f20,plain,(
% 0.08/0.37 ![X0,X1,X2,X3]: (ifeq(class_Orderings_Oorder(X0),true,ifeq(c_lessequals(X1,X2,X0),true,ifeq(c_lessequals(X2,X3,X0),true,c_lessequals(X1,X3,X0),true),true),true)=true)),
% 0.08/0.37 inference(cnf_transformation,[status(thm)],[f6])).
% 0.08/0.37 fof(f21,plain,(
% 0.08/0.37 c_lessequals(c_0,c_minus(v_k(v_x),v_g(v_x),t_b),t_b)=true),
% 0.08/0.37 inference(cnf_transformation,[status(thm)],[f7])).
% 0.08/0.37 fof(f22,plain,(
% 0.08/0.37 c_lessequals(v_k(v_x),v_f(v_x),t_b)=true),
% 0.08/0.37 inference(cnf_transformation,[status(thm)],[f8])).
% 0.08/0.37 fof(f23,plain,(
% 0.08/0.37 ~c_lessequals(c_0,c_minus(v_f(v_x),v_g(v_x),t_b),t_b)=true),
% 0.08/0.37 inference(cnf_transformation,[status(thm)],[f9])).
% 0.08/0.37 fof(f24,plain,(
% 0.08/0.37 ![X0]: (ifeq(class_Orderings_Olinorder(X0),true,class_Orderings_Oorder(X0),true)=true)),
% 0.08/0.37 inference(cnf_transformation,[status(thm)],[f10])).
% 0.08/0.37 fof(f25,plain,(
% 0.08/0.37 ![X0]: (ifeq(class_Ring__and__Field_Oordered__idom(X0),true,class_OrderedGroup_Ocomm__monoid__add(X0),true)=true)),
% 0.08/0.37 inference(cnf_transformation,[status(thm)],[f11])).
% 0.08/0.37 fof(f26,plain,(
% 0.08/0.37 ![X0]: (ifeq(class_Ring__and__Field_Oordered__idom(X0),true,class_Orderings_Olinorder(X0),true)=true)),
% 0.08/0.37 inference(cnf_transformation,[status(thm)],[f12])).
% 0.08/0.37 fof(f27,plain,(
% 0.08/0.37 ![X0]: (ifeq(class_Ring__and__Field_Oordered__idom(X0),true,class_OrderedGroup_Opordered__ab__group__add(X0),true)=true)),
% 0.08/0.37 inference(cnf_transformation,[status(thm)],[f13])).
% 0.08/0.37 fof(f28,plain,(
% 0.08/0.37 class_Ring__and__Field_Oordered__idom(t_b)=true),
% 0.08/0.37 inference(cnf_transformation,[status(thm)],[f14])).
% 0.08/0.37 fof(f29,definition,(
% 0.08/0.37 sF2_fnc=v_f(v_x)),
% 0.08/0.37 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 0.08/0.37 fof(f30,definition,(
% 0.08/0.37 sF3_fnc=v_g(v_x)),
% 0.08/0.37 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 0.08/0.37 fof(f31,definition,(
% 0.08/0.37 sF1_fnc=c_minus(sF2_fnc,sF3_fnc,t_b)),
% 0.08/0.37 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 0.08/0.37 fof(f32,definition,(
% 0.08/0.37 sF0_fnc=c_lessequals(c_0,sF1_fnc,t_b)),
% 0.08/0.37 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 0.08/0.37 fof(f33,plain,(
% 0.08/0.37 ~sF0_fnc=true),
% 0.08/0.37 inference(definition_folding,[],[f23,f32,f31,f30,f29])).
% 0.08/0.37 fof(f34,plain,(
% 0.08/0.37 c_lessequals(v_k(v_x),sF2_fnc,t_b)=true),
% 0.08/0.37 inference(backward_demodulation,[status(thm)],[f29,f22])).
% 0.08/0.37 fof(f35,plain,(
% 0.08/0.37 c_lessequals(c_0,c_minus(v_k(v_x),sF3_fnc,t_b),t_b)=true),
% 0.08/0.37 inference(backward_demodulation,[status(thm)],[f30,f21])).
% 0.08/0.37 fof(f36,plain,(
% 0.08/0.37 ifeq(true,true,class_OrderedGroup_Ocomm__monoid__add(t_b),true)=true),
% 0.08/0.37 inference(paramodulation,[status(thm)],[f28,f25])).
% 0.08/0.37 fof(f37,plain,(
% 0.08/0.37 class_OrderedGroup_Ocomm__monoid__add(t_b)=true),
% 0.08/0.37 inference(forward_demodulation,[status(thm)],[f16,f36])).
% 0.08/0.37 fof(f40,plain,(
% 0.08/0.37 ifeq(true,true,class_Orderings_Olinorder(t_b),true)=true),
% 0.08/0.37 inference(paramodulation,[status(thm)],[f28,f26])).
% 0.08/0.37 fof(f41,plain,(
% 0.08/0.37 class_Orderings_Olinorder(t_b)=true),
% 0.08/0.37 inference(forward_demodulation,[status(thm)],[f16,f40])).
% 0.08/0.37 fof(f43,plain,(
% 0.08/0.37 ifeq(true,true,class_Orderings_Oorder(t_b),true)=true),
% 0.08/0.37 inference(paramodulation,[status(thm)],[f41,f24])).
% 0.08/0.37 fof(f45,plain,(
% 0.08/0.37 class_Orderings_Oorder(t_b)=true),
% 0.08/0.37 inference(forward_demodulation,[status(thm)],[f16,f43])).
% 0.08/0.37 fof(f48,plain,(
% 0.08/0.37 ifeq(true,true,class_OrderedGroup_Opordered__ab__group__add(t_b),true)=true),
% 0.08/0.37 inference(paramodulation,[status(thm)],[f28,f27])).
% 0.08/0.37 fof(f49,plain,(
% 0.08/0.37 class_OrderedGroup_Opordered__ab__group__add(t_b)=true),
% 0.08/0.37 inference(forward_demodulation,[status(thm)],[f16,f48])).
% 0.08/0.37 fof(f52,plain,(
% 0.08/0.37 ![X0]: (ifeq2(true,true,c_plus(c_0,X0,t_b),X0)=X0)),
% 0.08/0.37 inference(paramodulation,[status(thm)],[f37,f17])).
% 0.08/0.37 fof(f53,plain,(
% 0.08/0.37 ![X0]: (c_plus(c_0,X0,t_b)=X0)),
% 0.08/0.37 inference(forward_demodulation,[status(thm)],[f15,f52])).
% 0.08/0.37 fof(f57,plain,(
% 0.08/0.37 ifeq(class_OrderedGroup_Opordered__ab__group__add(t_b),true,ifeq(true,true,c_lessequals(c_plus(c_0,sF3_fnc,t_b),v_k(v_x),t_b),true),true)=true),
% 0.08/0.37 inference(paramodulation,[status(thm)],[f35,f18])).
% 0.08/0.37 fof(f61,plain,(
% 0.08/0.37 ifeq(true,true,ifeq(true,true,c_lessequals(c_plus(c_0,sF3_fnc,t_b),v_k(v_x),t_b),true),true)=true),
% 0.08/0.37 inference(forward_demodulation,[status(thm)],[f49,f57])).
% 0.08/0.37 fof(f62,plain,(
% 0.08/0.37 ifeq(true,true,c_lessequals(c_plus(c_0,sF3_fnc,t_b),v_k(v_x),t_b),true)=true),
% 0.08/0.37 inference(forward_demodulation,[status(thm)],[f16,f61])).
% 0.08/0.37 fof(f63,plain,(
% 0.08/0.37 c_lessequals(c_plus(c_0,sF3_fnc,t_b),v_k(v_x),t_b)=true),
% 0.08/0.37 inference(forward_demodulation,[status(thm)],[f16,f62])).
% 0.08/0.37 fof(f64,plain,(
% 0.08/0.37 c_lessequals(sF3_fnc,v_k(v_x),t_b)=true),
% 0.08/0.37 inference(forward_demodulation,[status(thm)],[f53,f63])).
% 0.08/0.37 fof(f90,plain,(
% 0.08/0.37 ![X0,X1]: (ifeq(class_OrderedGroup_Opordered__ab__group__add(t_b),true,ifeq(c_lessequals(X0,X1,t_b),true,c_lessequals(c_0,c_minus(X1,X0,t_b),t_b),true),true)=true)),
% 0.08/0.37 inference(paramodulation,[status(thm)],[f53,f19])).
% 0.08/0.37 fof(f94,plain,(
% 0.08/0.37 ![X0,X1]: (ifeq(true,true,ifeq(c_lessequals(X0,X1,t_b),true,c_lessequals(c_0,c_minus(X1,X0,t_b),t_b),true),true)=true)),
% 0.08/0.37 inference(forward_demodulation,[status(thm)],[f49,f90])).
% 0.08/0.37 fof(f95,plain,(
% 0.08/0.37 ![X0,X1]: (ifeq(c_lessequals(X0,X1,t_b),true,c_lessequals(c_0,c_minus(X1,X0,t_b),t_b),true)=true)),
% 0.08/0.37 inference(forward_demodulation,[status(thm)],[f16,f94])).
% 0.08/0.37 fof(f107,plain,(
% 0.08/0.37 ifeq(c_lessequals(sF3_fnc,sF2_fnc,t_b),true,c_lessequals(c_0,sF1_fnc,t_b),true)=true),
% 0.08/0.37 inference(paramodulation,[status(thm)],[f31,f95])).
% 0.08/0.37 fof(f114,plain,(
% 0.08/0.37 ifeq(c_lessequals(sF3_fnc,sF2_fnc,t_b),true,sF0_fnc,true)=true),
% 0.08/0.37 inference(forward_demodulation,[status(thm)],[f32,f107])).
% 0.08/0.37 fof(f232,plain,(
% 0.08/0.37 ![X0]: (ifeq(class_Orderings_Oorder(t_b),true,ifeq(c_lessequals(X0,v_k(v_x),t_b),true,ifeq(true,true,c_lessequals(X0,sF2_fnc,t_b),true),true),true)=true)),
% 0.08/0.37 inference(paramodulation,[status(thm)],[f34,f20])).
% 0.08/0.37 fof(f274,plain,(
% 0.08/0.37 ![X0]: (ifeq(true,true,ifeq(c_lessequals(X0,v_k(v_x),t_b),true,ifeq(true,true,c_lessequals(X0,sF2_fnc,t_b),true),true),true)=true)),
% 0.08/0.37 inference(forward_demodulation,[status(thm)],[f45,f232])).
% 0.08/0.37 fof(f275,plain,(
% 0.08/0.37 ![X0]: (ifeq(c_lessequals(X0,v_k(v_x),t_b),true,ifeq(true,true,c_lessequals(X0,sF2_fnc,t_b),true),true)=true)),
% 0.08/0.37 inference(forward_demodulation,[status(thm)],[f16,f274])).
% 0.08/0.37 fof(f276,plain,(
% 0.08/0.37 ![X0]: (ifeq(c_lessequals(X0,v_k(v_x),t_b),true,c_lessequals(X0,sF2_fnc,t_b),true)=true)),
% 0.08/0.37 inference(forward_demodulation,[status(thm)],[f16,f275])).
% 0.08/0.37 fof(f326,plain,(
% 0.08/0.37 ifeq(true,true,c_lessequals(sF3_fnc,sF2_fnc,t_b),true)=true),
% 0.08/0.37 inference(paramodulation,[status(thm)],[f64,f276])).
% 0.08/0.37 fof(f328,plain,(
% 0.08/0.37 ifeq(true,true,sF0_fnc,true)=true),
% 0.08/0.37 inference(backward_demodulation,[status(thm)],[f330,f114])).
% 0.08/0.37 fof(f330,plain,(
% 0.08/0.37 c_lessequals(sF3_fnc,sF2_fnc,t_b)=true),
% 0.08/0.37 inference(forward_demodulation,[status(thm)],[f16,f326])).
% 0.08/0.37 fof(f331,plain,(
% 0.08/0.37 sF0_fnc=true),
% 0.08/0.37 inference(forward_demodulation,[status(thm)],[f16,f328])).
% 0.08/0.37 fof(f332,plain,(
% 0.08/0.37 $false),
% 0.08/0.37 inference(forward_subsumption_resolution,[status(thm)],[f331,f33])).
% 0.08/0.37 % SZS output end CNFRefutation for theBenchmark.p
% 0.08/0.40 % Elapsed time: 0.036426 seconds
% 0.08/0.40 % CPU time: 0.045948 seconds
% 0.08/0.40 % Total memory used: 2.353 MB
% 0.08/0.40 % Net memory used: 2.278 MB
%------------------------------------------------------------------------------