%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWW246+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/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 : Sun Sep 27 09:13:59 AM UTC 2026
% Result : Theorem 187.88s 25.71s
% Output : CNFRefutation 187.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 4
% Syntax : Number of formulae : 19 ( 6 unt; 0 def)
% Number of atoms : 42 ( 20 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 42 ( 19 ~; 16 |; 3 &)
% ( 2 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 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 : 46 ( 8 sgn 26 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_constant__def,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('theBenchmark.p',fact_constant__def) ).
fof(fact__C0_C,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('theBenchmark.p',fact__C0_C) ).
fof(fact_order__root,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('theBenchmark.p',fact_order__root) ).
cnf(c_1124,plain,
( c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(A)) != B
| c_Groups_Ozero__class_Ozero(A) = hAPP(c_Polynomial_Opoly(A,B),C)
| ~ class_Rings_Oidom(A) ),
inference(clausify,[status(thm)],[fact_order__root]) ).
cnf(c_1125,plain,
( c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(A)) != B
| hAPP(c_Polynomial_Opoly(A,B),C) = c_Groups_Ozero__class_Ozero(A)
| ~ class_Rings_Oidom(A) ),
inference(copy,[status(thm)],[c_1124]) ).
fof(nnf_19,plain,
! [V_f_2,T_c,T_b] :
( ( ? [B_x,B_y] : hAPP(V_f_2,B_y) != hAPP(V_f_2,B_x)
| c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(T_b,T_c,V_f_2) )
& ( ! [X0,X1] : hAPP(V_f_2,X1) = hAPP(V_f_2,X0)
| ~ c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(T_b,T_c,V_f_2) ) ),
inference(fof_nnf,[status(thm)],[fact_constant__def]) ).
fof(sk_fact_constant__def_sk,plain,
! [V_f_2,T_c,T_b] :
( ( hAPP(V_f_2,sK0(V_f_2,T_c,T_b)) != hAPP(V_f_2,sK1(V_f_2,T_c,T_b))
| c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(T_b,T_c,V_f_2) )
& ( ! [X0,X1] : hAPP(V_f_2,X1) = hAPP(V_f_2,X0)
| ~ c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(T_b,T_c,V_f_2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(B_x,sK1(V_f_2,T_c,T_b)),skolemize(B_y,sK0(V_f_2,T_c,T_b))],[nnf_19]) ).
fof(sk_fact_constant__def,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( hAPP(VAR_2,sK0(VAR_2,VAR_1,VAR_0)) != hAPP(VAR_2,sK1(VAR_2,VAR_1,VAR_0))
| c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(VAR_0,VAR_1,VAR_2) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( hAPP(VAR_2,VAR_3) = hAPP(VAR_2,VAR_4)
| ~ c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(VAR_0,VAR_1,VAR_2) ) ),
inference(cnf_transformation,[status(thm)],[sk_fact_constant__def_sk]) ).
cnf(c_1677,plain,
( hAPP(C,sK0(C,B,A)) != hAPP(C,sK1(C,B,A))
| c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(A,B,C) ),
inference(split_conjunct,[status(thm)],[sk_fact_constant__def]) ).
cnf(c_1714,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(clausify,[status(thm)],[fact__C0_C]) ).
fof(tfree_0,axiom,
class_Rings_Oidom(t_a),
file('theBenchmark.p',tfree_0) ).
cnf(c_2752,plain,
class_Rings_Oidom(t_a),
inference(clausify,[status(thm)],[tfree_0]) ).
cnf(c_2868,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(resolve,[status(thm)],[c_2752,c_1714]) ).
cnf(c_3310,plain,
( c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)) != A
| hAPP(c_Polynomial_Opoly(t_a,A),B) = c_Groups_Ozero__class_Ozero(t_a) ),
inference(resolve,[status(thm)],[c_1125,c_2752]) ).
cnf(c_2901,plain,
hAPP(c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),A) = c_Groups_Ozero__class_Ozero(t_a),
inference(xxres,[status(thm)],[c_3310]) ).
cnf(c_3311,plain,
( c_Groups_Ozero__class_Ozero(t_a) != hAPP(c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),sK1(c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))),B,A))
| c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(A,B,c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))) ),
inference(paramod,[status(thm)],[c_2901,c_1677]) ).
cnf(c_3312,plain,
( c_Groups_Ozero__class_Ozero(t_a) != c_Groups_Ozero__class_Ozero(t_a)
| c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(A,B,c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))) ),
inference(paramod,[status(thm)],[c_2901,c_3311]) ).
cnf(c_3308,plain,
c_Fundamental__Theorem__Algebra__Mirabelle_Oconstant(A,B,c_Polynomial_Opoly(t_a,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))),
inference(copy,[status(thm)],[c_3312]) ).
cnf(c_3309,plain,
$false,
inference(resolve,[status(thm)],[c_3308,c_2868]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW246+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n017.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 15:26:48 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36 % Process 1074117 was started by sandbox2 on n017,
% 0.09/0.36 % Sat Sep 26 15:26:48 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.21/0.50
% 0.21/0.50 % From the command line: assign(max_seconds, 300).
% 0.21/0.50
% 0.21/0.50 % SInE: 825 to sos, 373 to usable, of 1198 axioms (tolerance 2.00, depth 0 fixpoint).
% 187.88/25.71
% 187.88/25.71 % SZS status Theorem for theBenchmark
% 187.88/25.71
% 187.88/25.71 % Proof 1 at 0.66 (+ 0.12) seconds.
% 187.88/25.71 % Length of proof is 12.
% 187.88/25.71 % Level of proof is 5.
% 187.88/25.71 % Maximum clause weight is 117.000.
% 187.88/25.71 % Given clauses 144.
% 187.88/25.71
% 187.88/25.71 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------