%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW225+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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 03:08:50 PM UTC 2026
% Result : Theorem 1.31s 1.16s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW225+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.85 % Computer : n014.cluster.edu
% 0.10/0.85 % Model : x86_64 x86_64
% 0.10/0.85 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.85 % Memory : 8046.5625MB
% 0.10/0.85 % OS : Linux 6.8.0-71-generic
% 0.10/0.85 % CPULimit : 300
% 0.10/0.85 % WCLimit : 300
% 0.10/0.85 % DateTime : Mon Sep 21 09:42:37 UTC 2026
% 0.10/0.85 % CPUTime :
% 0.15/0.95 % Drodi V4.1.1
% 1.31/1.16 % Refutation found
% 1.31/1.16 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.31/1.16 % SZS output start CNFRefutation for theBenchmark
% 1.31/1.16 fof(f3,axiom,(
% 1.31/1.16 c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____),hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))) ),
% 1.31/1.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.31/1.16 fof(f23,axiom,(
% 1.31/1.16 (! [V_m_2,V_n_2] :( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_OSuc(V_n_2),c_Nat_OSuc(V_m_2))<=> c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_n_2,V_m_2) ) )),
% 1.31/1.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.31/1.16 fof(f69,axiom,(
% 1.31/1.16 (! [V_m_2,V_n_2] :( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(c_RealDef_Oreal(tc_Nat_Onat),V_n_2),hAPP(c_RealDef_Oreal(tc_Nat_Onat),V_m_2))<=> c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_n_2,V_m_2) ) )),
% 1.31/1.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.31/1.16 fof(f1269,conjecture,(
% 1.31/1.16 c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(c_RealDef_Oreal(tc_Nat_Onat),c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))),hAPP(c_RealDef_Oreal(tc_Nat_Onat),c_Nat_OSuc(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))) ),
% 1.31/1.16 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.31/1.16 fof(f1270,negated_conjecture,(
% 1.31/1.16 ~(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(c_RealDef_Oreal(tc_Nat_Onat),c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))),hAPP(c_RealDef_Oreal(tc_Nat_Onat),c_Nat_OSuc(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))) )),
% 1.31/1.16 inference(negated_conjecture,[status(cth)],[f1269])).
% 1.31/1.16 fof(f1275,plain,(
% 1.31/1.16 c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____),hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),
% 1.31/1.16 inference(cnf_transformation,[status(thm)],[f3])).
% 1.31/1.16 fof(f1322,plain,(
% 1.31/1.16 ![V_m_2,V_n_2]: ((~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_OSuc(V_n_2),c_Nat_OSuc(V_m_2))|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_n_2,V_m_2))&(c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_OSuc(V_n_2),c_Nat_OSuc(V_m_2))|~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_n_2,V_m_2)))),
% 1.31/1.16 inference(NNF_transformation,[status(thm)],[f23])).
% 1.31/1.16 fof(f1323,plain,(
% 1.31/1.16 (![V_m_2,V_n_2]: (~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_OSuc(V_n_2),c_Nat_OSuc(V_m_2))|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_n_2,V_m_2)))&(![V_m_2,V_n_2]: (c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_OSuc(V_n_2),c_Nat_OSuc(V_m_2))|~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_n_2,V_m_2)))),
% 1.31/1.16 inference(miniscoping,[status(thm)],[f1322])).
% 1.31/1.16 fof(f1325,plain,(
% 1.31/1.16 ![X0,X1]: (c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_OSuc(X0),c_Nat_OSuc(X1))|~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X0,X1))),
% 1.31/1.16 inference(cnf_transformation,[status(thm)],[f1323])).
% 1.31/1.16 fof(f1465,plain,(
% 1.31/1.16 ![V_m_2,V_n_2]: ((~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(c_RealDef_Oreal(tc_Nat_Onat),V_n_2),hAPP(c_RealDef_Oreal(tc_Nat_Onat),V_m_2))|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_n_2,V_m_2))&(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(c_RealDef_Oreal(tc_Nat_Onat),V_n_2),hAPP(c_RealDef_Oreal(tc_Nat_Onat),V_m_2))|~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_n_2,V_m_2)))),
% 1.31/1.16 inference(NNF_transformation,[status(thm)],[f69])).
% 1.31/1.16 fof(f1466,plain,(
% 1.31/1.16 (![V_m_2,V_n_2]: (~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(c_RealDef_Oreal(tc_Nat_Onat),V_n_2),hAPP(c_RealDef_Oreal(tc_Nat_Onat),V_m_2))|c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_n_2,V_m_2)))&(![V_m_2,V_n_2]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(c_RealDef_Oreal(tc_Nat_Onat),V_n_2),hAPP(c_RealDef_Oreal(tc_Nat_Onat),V_m_2))|~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_n_2,V_m_2)))),
% 1.31/1.16 inference(miniscoping,[status(thm)],[f1465])).
% 1.31/1.16 fof(f1468,plain,(
% 1.31/1.16 ![X0,X1]: (c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(c_RealDef_Oreal(tc_Nat_Onat),X0),hAPP(c_RealDef_Oreal(tc_Nat_Onat),X1))|~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X0,X1))),
% 1.31/1.17 inference(cnf_transformation,[status(thm)],[f1466])).
% 1.31/1.17 fof(f4720,plain,(
% 1.31/1.17 ~c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,hAPP(c_RealDef_Oreal(tc_Nat_Onat),c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))),hAPP(c_RealDef_Oreal(tc_Nat_Onat),c_Nat_OSuc(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))))),
% 1.31/1.17 inference(cnf_transformation,[status(thm)],[f1270])).
% 1.31/1.17 fof(f5656,plain,(
% 1.31/1.17 ~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_OSuc(c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)),c_Nat_OSuc(hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____))))),
% 1.31/1.17 inference(resolution,[status(thm)],[f1468,f4720])).
% 1.31/1.17 fof(f5680,plain,(
% 1.31/1.17 ~c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____),hAPP(v_f____,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_N1____,v_N2____)))),
% 1.31/1.17 inference(resolution,[status(thm)],[f5656,f1325])).
% 1.31/1.17 fof(f5690,plain,(
% 1.31/1.17 $false),
% 1.31/1.17 inference(forward_subsumption_resolution,[status(thm)],[f5680,f1275])).
% 1.31/1.17 % SZS output end CNFRefutation for theBenchmark.p
% 1.31/1.18 % Elapsed time: 0.324431 seconds
% 1.31/1.18 % CPU time: 1.651903 seconds
% 1.31/1.18 % Total memory used: 223.146 MB
% 1.31/1.18 % Net memory used: 220.910 MB
%------------------------------------------------------------------------------