%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW246+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.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:07:30 PM UTC 2026
% Result : Theorem 0.30s 0.71s
% Output : CNFRefutation 0.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 4
% Syntax : Number of formulae : 22 ( 8 unt; 0 def)
% Number of atoms : 57 ( 33 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 65 ( 30 ~; 23 |; 7 &)
% ( 3 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 5 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 2 con; 0-3 aty)
% Number of variables : 53 ( 49 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f22,axiom,
! [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) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f67,axiom,
( 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)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f69,axiom,
! [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)
<=> ( c_Polynomial_Oorder(T_b,V_a_2,V_pa_2) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| V_pa_2 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1200,hypothesis,
class_Rings_Oidom(t_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1270,plain,
! [V_f_2,T_c,T_b] :
( ( ? [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)
| ~ c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(T_b,T_c,V_f_2) ) ),
inference(NNF_transformation,[status(thm)],[f22]) ).
fof(f1271,plain,
( ! [V_f_2] :
( ? [B_x,B_y] : hAPP(V_f_2,B_x) != hAPP(V_f_2,B_y)
| ! [T_c,T_b] : c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(T_b,T_c,V_f_2) )
& ! [V_f_2] :
( ! [B_x,B_y] : hAPP(V_f_2,B_x) = hAPP(V_f_2,B_y)
| ! [T_c,T_b] : ~ c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(T_b,T_c,V_f_2) ) ),
inference(miniscoping,[status(thm)],[f1270]) ).
fof(f1272,plain,
( ! [V_f_2] :
( hAPP(V_f_2,sK1_skl(V_f_2)) != hAPP(V_f_2,sK2_skl(V_f_2))
| ! [T_c,T_b] : c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(T_b,T_c,V_f_2) )
& ! [V_f_2] :
( ! [B_x,B_y] : hAPP(V_f_2,B_x) = hAPP(V_f_2,B_y)
| ! [T_c,T_b] : ~ c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(T_b,T_c,V_f_2) ) ),
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]) ).
fof(f1274,plain,
! [X0,X1,X2] :
( hAPP(X2,sK1_skl(X2)) != hAPP(X2,sK2_skl(X2))
| c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f1272]) ).
fof(f1422,plain,
( ~ 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))))
| ~ class_Rings_Oidom(t_a) ),
inference(pre_NNF_transformation,[status(thm)],[f67]) ).
fof(f1423,plain,
( ~ 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))))
| ~ class_Rings_Oidom(t_a) ),
inference(cnf_transformation,[status(thm)],[f1422]) ).
fof(f1430,plain,
! [V_a_2,V_pa_2,T_b] :
( ( hAPP(c_Polynomial_Opoly(T_b,V_pa_2),V_a_2) = c_Groups_Ozero__class_Ozero(T_b)
<=> ( c_Polynomial_Oorder(T_b,V_a_2,V_pa_2) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| V_pa_2 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b)) ) )
| ~ class_Rings_Oidom(T_b) ),
inference(pre_NNF_transformation,[status(thm)],[f69]) ).
fof(f1431,plain,
! [V_a_2,V_pa_2,T_b] :
( ( ( ( c_Polynomial_Oorder(T_b,V_a_2,V_pa_2) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
& V_pa_2 != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b)) )
| hAPP(c_Polynomial_Opoly(T_b,V_pa_2),V_a_2) = c_Groups_Ozero__class_Ozero(T_b) )
& ( c_Polynomial_Oorder(T_b,V_a_2,V_pa_2) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| V_pa_2 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))
| hAPP(c_Polynomial_Opoly(T_b,V_pa_2),V_a_2) != c_Groups_Ozero__class_Ozero(T_b) ) )
| ~ class_Rings_Oidom(T_b) ),
inference(NNF_transformation,[status(thm)],[f1430]) ).
fof(f1432,plain,
! [T_b] :
( ( ! [V_a_2,V_pa_2] :
( ( c_Polynomial_Oorder(T_b,V_a_2,V_pa_2) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
& V_pa_2 != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b)) )
| hAPP(c_Polynomial_Opoly(T_b,V_pa_2),V_a_2) = c_Groups_Ozero__class_Ozero(T_b) )
& ! [V_a_2,V_pa_2] :
( c_Polynomial_Oorder(T_b,V_a_2,V_pa_2) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| V_pa_2 = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(T_b))
| hAPP(c_Polynomial_Opoly(T_b,V_pa_2),V_a_2) != c_Groups_Ozero__class_Ozero(T_b) ) )
| ~ class_Rings_Oidom(T_b) ),
inference(miniscoping,[status(thm)],[f1431]) ).
fof(f1434,plain,
! [X0,X1,X2] :
( X1 != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))
| hAPP(c_Polynomial_Opoly(X0,X1),X2) = c_Groups_Ozero__class_Ozero(X0)
| ~ class_Rings_Oidom(X0) ),
inference(cnf_transformation,[status(thm)],[f1432]) ).
fof(f4648,plain,
class_Rings_Oidom(t_a),
inference(cnf_transformation,[status(thm)],[f1200]) ).
fof(f4697,plain,
! [X0,X1] :
( hAPP(c_Polynomial_Opoly(X0,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X0))),X1) = c_Groups_Ozero__class_Ozero(X0)
| ~ class_Rings_Oidom(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f1434]) ).
fof(f4865,plain,
! [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),
inference(resolution,[status(thm)],[f4697,f4648]) ).
fof(f6462,plain,
~ 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)))),
inference(forward_subsumption_resolution,[status(thm)],[f1423,f4648]) ).
fof(f6463,plain,
hAPP(c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),sK1_skl(c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(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))))),
inference(resolution,[status(thm)],[f6462,f1274]) ).
fof(f6464,plain,
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))))),
inference(forward_demodulation,[status(thm)],[f4865,f6463]) ).
fof(f6465,plain,
c_Groups_Ozero__class_Ozero(t_a) != c_Groups_Ozero__class_Ozero(t_a),
inference(forward_demodulation,[status(thm)],[f4865,f6464]) ).
fof(f6466,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f6465]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW246+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n009.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 09:43:13 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.20/0.54 % Drodi V4.1.1
% 0.30/0.71 % Refutation found
% 0.30/0.71 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.30/0.71 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.32/0.76 % Elapsed time: 0.386348 seconds
% 0.32/0.76 % CPU time: 1.598897 seconds
% 0.32/0.76 % Total memory used: 221.873 MB
% 0.32/0.76 % Net memory used: 220.766 MB
%------------------------------------------------------------------------------