%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW246+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 : n012.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:52 PM UTC 2026
% Result : Theorem 0.12s 7.65s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW246+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/7.44 % Computer : n012.cluster.edu
% 0.09/7.44 % Model : x86_64 x86_64
% 0.09/7.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/7.44 % Memory : 8046.5625MB
% 0.09/7.44 % OS : Linux 6.8.0-71-generic
% 0.09/7.44 % CPULimit : 300
% 0.09/7.44 % WCLimit : 300
% 0.09/7.44 % DateTime : Mon Sep 21 09:43:06 UTC 2026
% 0.09/7.44 % CPUTime :
% 0.12/7.52 % Drodi V4.1.1
% 0.12/7.65 % Refutation found
% 0.12/7.65 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/7.65 % SZS output start CNFRefutation for theBenchmark
% 0.12/7.65 fof(f22,axiom,(
% 0.12/7.65 (! [V_f_2,T_c,T_b] :( c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(T_b,T_c,V_f_2)<=> (! [B_x,B_y] : hAPP(V_f_2,B_x) = hAPP(V_f_2,B_y) )) )),
% 0.12/7.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/7.65 fof(f67,axiom,(
% 0.12/7.65 ( class_Rings_Oidom(t_a)=> ~ c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(t_a,t_a,c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))) ) ),
% 0.12/7.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/7.65 fof(f69,axiom,(
% 0.12/7.65 (! [V_a_2,V_pa_2,T_b] :( class_Rings_Oidom(T_b)=> ( hAPP(c_Polynomial_Opoly(T_b,V_pa_2),V_a_2) = c_Groups_Ozero__class_Ozero(T_b)<=> ( V_pa_2 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))| c_Polynomial_Oorder(T_b,V_a_2,V_pa_2) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ) ) ) )),
% 0.12/7.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/7.65 fof(f199,axiom,(
% 0.12/7.65 (! [V_z] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint)),V_z) = V_z )),
% 0.12/7.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/7.65 fof(f1200,hypothesis,(
% 0.12/7.65 class_Rings_Oidom(t_a) ),
% 0.12/7.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/7.65 fof(f1270,plain,(
% 0.12/7.65 ![V_f_2,T_c,T_b]: ((~c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(T_b,T_c,V_f_2)|(![B_x,B_y]: hAPP(V_f_2,B_x)=hAPP(V_f_2,B_y)))&(c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(T_b,T_c,V_f_2)|(?[B_x,B_y]: ~hAPP(V_f_2,B_x)=hAPP(V_f_2,B_y))))),
% 0.12/7.65 inference(NNF_transformation,[status(thm)],[f22])).
% 0.12/7.65 fof(f1271,plain,(
% 0.12/7.65 (![V_f_2]: ((![T_c,T_b]: ~c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(T_b,T_c,V_f_2))|(![B_x,B_y]: hAPP(V_f_2,B_x)=hAPP(V_f_2,B_y))))&(![V_f_2]: ((![T_c,T_b]: c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(T_b,T_c,V_f_2))|(?[B_x,B_y]: ~hAPP(V_f_2,B_x)=hAPP(V_f_2,B_y))))),
% 0.12/7.65 inference(miniscoping,[status(thm)],[f1270])).
% 0.12/7.65 fof(f1272,plain,(
% 0.12/7.65 (![V_f_2]: ((![T_c,T_b]: ~c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(T_b,T_c,V_f_2))|(![B_x,B_y]: hAPP(V_f_2,B_x)=hAPP(V_f_2,B_y))))&(![V_f_2]: ((![T_c,T_b]: c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(T_b,T_c,V_f_2))|~hAPP(V_f_2,sK1_skl(V_f_2))=hAPP(V_f_2,sK2_skl(V_f_2))))),
% 0.12/7.65 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl]),skolemize(B_x,sK1_skl(V_f_2)),skolemize(B_y,sK2_skl(V_f_2))],[f1271])).
% 0.12/7.65 fof(f1274,plain,(
% 0.12/7.65 ![X0,X1,X2]: (c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(X0,X1,X2)|~hAPP(X2,sK1_skl(X2))=hAPP(X2,sK2_skl(X2)))),
% 0.12/7.65 inference(cnf_transformation,[status(thm)],[f1272])).
% 0.12/7.65 fof(f1422,plain,(
% 0.12/7.65 ~class_Rings_Oidom(t_a)|~c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(t_a,t_a,c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))))),
% 0.12/7.65 inference(pre_NNF_transformation,[status(thm)],[f67])).
% 0.12/7.65 fof(f1423,plain,(
% 0.12/7.65 ~class_Rings_Oidom(t_a)|~c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(t_a,t_a,c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))))),
% 0.12/7.65 inference(cnf_transformation,[status(thm)],[f1422])).
% 0.12/7.65 fof(f1430,plain,(
% 0.12/7.65 ![V_a_2,V_pa_2,T_b]: (~class_Rings_Oidom(T_b)|(hAPP(c_Polynomial_Opoly(T_b,V_pa_2),V_a_2)=c_Groups_Ozero__class_Ozero(T_b)<=>(V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))|~c_Polynomial_Oorder(T_b,V_a_2,V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))),
% 0.12/7.65 inference(pre_NNF_transformation,[status(thm)],[f69])).
% 0.12/7.65 fof(f1431,plain,(
% 0.12/7.65 ![V_a_2,V_pa_2,T_b]: (~class_Rings_Oidom(T_b)|((~hAPP(c_Polynomial_Opoly(T_b,V_pa_2),V_a_2)=c_Groups_Ozero__class_Ozero(T_b)|(V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))|~c_Polynomial_Oorder(T_b,V_a_2,V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))&(hAPP(c_Polynomial_Opoly(T_b,V_pa_2),V_a_2)=c_Groups_Ozero__class_Ozero(T_b)|(~V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))&c_Polynomial_Oorder(T_b,V_a_2,V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))))),
% 0.12/7.65 inference(NNF_transformation,[status(thm)],[f1430])).
% 0.12/7.65 fof(f1432,plain,(
% 0.12/7.65 ![T_b]: (~class_Rings_Oidom(T_b)|((![V_a_2,V_pa_2]: (~hAPP(c_Polynomial_Opoly(T_b,V_pa_2),V_a_2)=c_Groups_Ozero__class_Ozero(T_b)|(V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))|~c_Polynomial_Oorder(T_b,V_a_2,V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))&(![V_a_2,V_pa_2]: (hAPP(c_Polynomial_Opoly(T_b,V_pa_2),V_a_2)=c_Groups_Ozero__class_Ozero(T_b)|(~V_pa_2=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))&c_Polynomial_Oorder(T_b,V_a_2,V_pa_2)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))))),
% 0.12/7.66 inference(miniscoping,[status(thm)],[f1431])).
% 0.12/7.66 fof(f1434,plain,(
% 0.12/7.66 ![X0,X1,X2]: (~class_Rings_Oidom(X0)|hAPP(c_Polynomial_Opoly(X0,X1),X2)=c_Groups_Ozero__class_Ozero(X0)|~X1=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0)))),
% 0.12/7.66 inference(cnf_transformation,[status(thm)],[f1432])).
% 0.12/7.66 fof(f1824,plain,(
% 0.12/7.66 ![X0]: (hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint)),X0)=X0)),
% 0.12/7.66 inference(cnf_transformation,[status(thm)],[f199])).
% 0.12/7.66 fof(f4648,plain,(
% 0.12/7.66 class_Rings_Oidom(t_a)),
% 0.12/7.66 inference(cnf_transformation,[status(thm)],[f1200])).
% 0.12/7.66 fof(f4776,plain,(
% 0.12/7.66 ![X0,X1]: (hAPP(c_Polynomial_Opoly(t_a,X0),X1)=c_Groups_Ozero__class_Ozero(t_a)|~X0=c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
% 0.12/7.66 inference(resolution,[status(thm)],[f1434,f4648])).
% 0.12/7.66 fof(f5013,plain,(
% 0.12/7.66 ![X0]: (hAPP(c_Polynomial_Opoly(t_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Int_Oint),c_Groups_Oone__class_Oone(tc_Int_Oint)),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),X0)=c_Groups_Ozero__class_Ozero(t_a))),
% 0.12/7.66 inference(resolution,[status(thm)],[f4776,f1824])).
% 0.12/7.66 fof(f5022,plain,(
% 0.12/7.66 ![X0]: (hAPP(c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),X0)=c_Groups_Ozero__class_Ozero(t_a))),
% 0.12/7.66 inference(forward_demodulation,[status(thm)],[f1824,f5013])).
% 0.12/7.66 fof(f5829,plain,(
% 0.12/7.66 ![X0,X1]: (c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(X0,X1,c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))))|~c_Groups_Ozero__class_Ozero(t_a)=hAPP(c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),sK2_skl(c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))))))),
% 0.12/7.66 inference(paramodulation,[status(thm)],[f5022,f1274])).
% 0.12/7.66 fof(f5843,plain,(
% 0.12/7.66 ![X0,X1]: (c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(X0,X1,c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))))|~c_Groups_Ozero__class_Ozero(t_a)=c_Groups_Ozero__class_Ozero(t_a))),
% 0.12/7.66 inference(forward_demodulation,[status(thm)],[f5022,f5829])).
% 0.12/7.66 fof(f5844,plain,(
% 0.12/7.66 ![X0,X1]: (c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(X0,X1,c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))))),
% 0.12/7.66 inference(trivial_equality_resolution,[status(thm)],[f5843])).
% 0.12/7.66 fof(f7906,plain,(
% 0.12/7.66 ~c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(t_a,t_a,c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))))),
% 0.12/7.66 inference(forward_subsumption_resolution,[status(thm)],[f1423,f4648])).
% 0.12/7.66 fof(f7907,plain,(
% 0.12/7.66 $false),
% 0.12/7.66 inference(resolution,[status(thm)],[f7906,f5844])).
% 0.12/7.66 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/7.70 % Elapsed time: 0.256231 seconds
% 0.12/7.70 % CPU time: 1.134121 seconds
% 0.12/7.70 % Total memory used: 223.005 MB
% 0.12/7.70 % Net memory used: 221.777 MB
%------------------------------------------------------------------------------