%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWV679-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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 02:53:00 PM UTC 2026
% Result : Unsatisfiable 2.69s 1.03s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWV679-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.44 % Computer : n001.cluster.edu
% 0.16/0.44 % Model : x86_64 x86_64
% 0.16/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.44 % Memory : 8046.5625MB
% 0.16/0.44 % OS : Linux 6.8.0-71-generic
% 0.16/0.44 % CPULimit : 300
% 0.16/0.44 % WCLimit : 300
% 0.16/0.44 % DateTime : Mon Sep 21 09:24:29 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.26/0.51 % Drodi V4.1.1
% 2.69/1.03 % Refutation found
% 2.69/1.03 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 2.69/1.03 % SZS output start CNFRefutation for theBenchmark
% 2.69/1.03 fof(f13,axiom,(
% 2.69/1.03 (![V_k]: (c_Ring__and__Field_Odvd__class_Odvd(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),V_k,tc_nat) ))),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f20,axiom,(
% 2.69/1.03 (![V_x]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(V_x),tc_nat) ))),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f53,axiom,(
% 2.69/1.03 (![V_m]: (c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m) ))),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f55,axiom,(
% 2.69/1.03 (![V_m,V_x]: (c_HOL_Oord__class_Oless(V_m,c_Suc(c_HOL_Oplus__class_Oplus(V_m,V_x,tc_nat)),tc_nat) ))),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f60,axiom,(
% 2.69/1.03 (![V_n,V_m]: (( c_HOL_Oord__class_Oless(V_n,V_m,tc_nat)| ~ c_lessequals(c_Suc(V_n),V_m,tc_nat) ) ))),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f231,axiom,(
% 2.69/1.03 (![T_a,V_a]: (( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a)| c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Oone__class_Oone(T_a),V_a,T_a) ) ))),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f302,axiom,(
% 2.69/1.03 (![V_m]: (~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ))),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f323,axiom,(
% 2.69/1.03 (![V_x]: (c_GCD_Ogcd__class_Ogcd(V_x,V_x,tc_nat) = V_x ))),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f384,axiom,(
% 2.69/1.03 (![V_x,V_y]: (( c_lessequals(V_x,V_y,tc_nat)| ~ c_HOL_Oord__class_Oless(V_x,V_y,tc_nat) ) ))),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f405,axiom,(
% 2.69/1.03 (![V_n]: (c_lessequals(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ))),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f420,axiom,(
% 2.69/1.03 (![V_m]: (c_HOL_Ominus__class_Ominus(V_m,V_m,tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat) ))),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f421,axiom,(
% 2.69/1.03 (![V_m]: (c_HOL_Ominus__class_Ominus(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = V_m ))),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f424,axiom,(
% 2.69/1.03 (![V_n,V_m]: (c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(V_n,V_m,tc_nat),V_n,tc_nat) = V_m ))),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f425,axiom,(
% 2.69/1.03 (![V_m,V_n]: (c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat),V_n,tc_nat) = V_m ))),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f426,axiom,(
% 2.69/1.03 ( ~ class_Ring__and__Field_Ofield(t_a)| v_a != c_HOL_Ozero__class_Ozero(t_a) ) ),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f556,axiom,(
% 2.69/1.03 (![T_a,V_a]: (( ~ class_Ring__and__Field_Ofield(T_a)| c_HOL_Oinverse__class_Oinverse(V_a,T_a) = c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(T_a),V_a,T_a) ) ))),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f568,axiom,(
% 2.69/1.03 (![T_a,V_a,V_n,V_m]: (( ~ class_Ring__and__Field_Ofield(T_a)| c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(V_a,T_a),c_HOL_Ominus__class_Ominus(V_n,V_m,tc_nat),T_a) = c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(V_a,V_m,T_a),c_Power_Opower__class_Opower(V_a,V_n,T_a),T_a)| ~ c_lessequals(V_m,V_n,tc_nat)| V_a = c_HOL_Ozero__class_Ozero(T_a) ) ))),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f604,axiom,(
% 2.69/1.03 (![V_n,V_m]: (( c_lessequals(V_n,V_m,tc_nat)| c_lessequals(V_m,V_n,tc_nat) ) ))),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f608,axiom,(
% 2.69/1.03 (![V_n]: (c_lessequals(V_n,V_n,tc_nat) ))),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f621,axiom,(
% 2.69/1.03 (![V_m,V_n]: (( V_m = V_n| ~ c_lessequals(V_n,V_m,tc_nat)| ~ c_lessequals(V_m,V_n,tc_nat) ) ))),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f628,axiom,(
% 2.69/1.03 ~ c_lessequals(v_n,v_m,tc_nat) ),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f636,axiom,(
% 2.69/1.03 (![V_m,V_n]: (c_lessequals(c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat),V_m,tc_nat) ))),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f641,negated_conjecture,(
% 2.69/1.03 class_Ring__and__Field_Ofield(t_a) ),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f642,negated_conjecture,(
% 2.69/1.03 ( c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(v_a,v_m,t_a),c_Power_Opower__class_Opower(v_a,v_n,t_a),t_a) != c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(t_a),v_a,t_a),c_HOL_Ominus__class_Ominus(v_n,v_m,tc_nat),t_a)| c_lessequals(v_n,v_m,tc_nat) ) ),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f648,axiom,(
% 2.69/1.03 (![T]: (( ~ class_Ring__and__Field_Ofield(T)| class_Ring__and__Field_Ono__zero__divisors(T) ) ))),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f649,axiom,(
% 2.69/1.03 (![T]: (( ~ class_Ring__and__Field_Ofield(T)| class_Ring__and__Field_Ocomm__semiring__1(T) ) ))),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f652,axiom,(
% 2.69/1.03 (![T]: (( ~ class_Ring__and__Field_Ofield(T)| class_OrderedGroup_Ocomm__monoid__add(T) ) ))),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f653,axiom,(
% 2.69/1.03 (![T]: (( ~ class_Ring__and__Field_Ofield(T)| class_Ring__and__Field_Ozero__neq__one(T) ) ))),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f658,axiom,(
% 2.69/1.03 (![T]: (( ~ class_Ring__and__Field_Ofield(T)| class_Ring__and__Field_Omult__zero(T) ) ))),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f664,axiom,(
% 2.69/1.03 (![T]: (( ~ class_Ring__and__Field_Ofield(T)| class_Power_Opower(T) ) ))),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f665,axiom,(
% 2.69/1.03 class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_nat) ),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f671,axiom,(
% 2.69/1.03 class_Ring__and__Field_Ono__zero__divisors(tc_nat) ),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f673,axiom,(
% 2.69/1.03 class_Ring__and__Field_Ocomm__semiring__1(tc_nat) ),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f676,axiom,(
% 2.69/1.03 class_Ring__and__Field_Ozero__neq__one(tc_nat) ),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f679,axiom,(
% 2.69/1.03 class_Ring__and__Field_Omult__zero(tc_nat) ),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f682,axiom,(
% 2.69/1.03 class_Divides_Osemiring__div(tc_nat) ),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f685,axiom,(
% 2.69/1.03 class_Orderings_Olinorder(tc_nat) ),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f687,axiom,(
% 2.69/1.03 class_Power_Opower(tc_nat) ),
% 2.69/1.03 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.69/1.03 fof(f709,plain,(
% 2.69/1.03 ![X0]: (c_Ring__and__Field_Odvd__class_Odvd(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat))),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f13])).
% 2.69/1.03 fof(f720,plain,(
% 2.69/1.03 ![X0]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(X0),tc_nat))),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f20])).
% 2.69/1.03 fof(f767,plain,(
% 2.69/1.03 ![X0]: (~c_HOL_Ozero__class_Ozero(tc_nat)=c_Suc(X0))),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f53])).
% 2.69/1.03 fof(f769,plain,(
% 2.69/1.03 ![X0,X1]: (c_HOL_Oord__class_Oless(X0,c_Suc(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat)),tc_nat))),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f55])).
% 2.69/1.03 fof(f776,plain,(
% 2.69/1.03 ![X0,X1]: (c_HOL_Oord__class_Oless(X0,X1,tc_nat)|~c_lessequals(c_Suc(X0),X1,tc_nat))),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f60])).
% 2.69/1.03 fof(f1044,plain,(
% 2.69/1.03 ![T_a]: (~class_Ring__and__Field_Ocomm__semiring__1(T_a)|(![V_a]: c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Oone__class_Oone(T_a),V_a,T_a)))),
% 2.69/1.03 inference(miniscoping,[status(thm)],[f231])).
% 2.69/1.03 fof(f1045,plain,(
% 2.69/1.03 ![X0,X1]: (~class_Ring__and__Field_Ocomm__semiring__1(X0)|c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Oone__class_Oone(X0),X1,X0))),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f1044])).
% 2.69/1.03 fof(f1161,plain,(
% 2.69/1.03 ![X0]: (~c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat))),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f302])).
% 2.69/1.03 fof(f1186,plain,(
% 2.69/1.03 ![X0]: (c_GCD_Ogcd__class_Ogcd(X0,X0,tc_nat)=X0)),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f323])).
% 2.69/1.03 fof(f1283,plain,(
% 2.69/1.03 ![X0,X1]: (c_lessequals(X0,X1,tc_nat)|~c_HOL_Oord__class_Oless(X0,X1,tc_nat))),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f384])).
% 2.69/1.03 fof(f1314,plain,(
% 2.69/1.03 ![X0]: (c_lessequals(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat))),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f405])).
% 2.69/1.03 fof(f1334,plain,(
% 2.69/1.03 ![X0]: (c_HOL_Ominus__class_Ominus(X0,X0,tc_nat)=c_HOL_Ozero__class_Ozero(tc_nat))),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f420])).
% 2.69/1.03 fof(f1335,plain,(
% 2.69/1.03 ![X0]: (c_HOL_Ominus__class_Ominus(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat)=X0)),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f421])).
% 2.69/1.03 fof(f1338,plain,(
% 2.69/1.03 ![X0,X1]: (c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X0,tc_nat)=X1)),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f424])).
% 2.69/1.03 fof(f1339,plain,(
% 2.69/1.03 ![X0,X1]: (c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X1,tc_nat)=X0)),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f425])).
% 2.69/1.03 fof(f1340,plain,(
% 2.69/1.03 ~class_Ring__and__Field_Ofield(t_a)|~v_a=c_HOL_Ozero__class_Ozero(t_a)),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f426])).
% 2.69/1.03 fof(f1533,plain,(
% 2.69/1.03 ![T_a]: (~class_Ring__and__Field_Ofield(T_a)|(![V_a]: c_HOL_Oinverse__class_Oinverse(V_a,T_a)=c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(T_a),V_a,T_a)))),
% 2.69/1.03 inference(miniscoping,[status(thm)],[f556])).
% 2.69/1.03 fof(f1534,plain,(
% 2.69/1.03 ![X0,X1]: (~class_Ring__and__Field_Ofield(X0)|c_HOL_Oinverse__class_Oinverse(X1,X0)=c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(X0),X1,X0))),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f1533])).
% 2.69/1.03 fof(f1553,plain,(
% 2.69/1.03 ![T_a,V_a]: ((![V_n,V_m]: ((~class_Ring__and__Field_Ofield(T_a)|c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(V_a,T_a),c_HOL_Ominus__class_Ominus(V_n,V_m,tc_nat),T_a)=c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(V_a,V_m,T_a),c_Power_Opower__class_Opower(V_a,V_n,T_a),T_a))|~c_lessequals(V_m,V_n,tc_nat)))|V_a=c_HOL_Ozero__class_Ozero(T_a))),
% 2.69/1.03 inference(miniscoping,[status(thm)],[f568])).
% 2.69/1.03 fof(f1554,plain,(
% 2.69/1.03 ![X0,X1,X2,X3]: (~class_Ring__and__Field_Ofield(X0)|c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(X1,X0),c_HOL_Ominus__class_Ominus(X2,X3,tc_nat),X0)=c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(X1,X3,X0),c_Power_Opower__class_Opower(X1,X2,X0),X0)|~c_lessequals(X3,X2,tc_nat)|X1=c_HOL_Ozero__class_Ozero(X0))),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f1553])).
% 2.69/1.03 fof(f1607,plain,(
% 2.69/1.03 ![X0,X1]: (c_lessequals(X0,X1,tc_nat)|c_lessequals(X1,X0,tc_nat))),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f604])).
% 2.69/1.03 fof(f1613,plain,(
% 2.69/1.03 ![X0]: (c_lessequals(X0,X0,tc_nat))),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f608])).
% 2.69/1.03 fof(f1635,plain,(
% 2.69/1.03 ![X0,X1]: (X0=X1|~c_lessequals(X1,X0,tc_nat)|~c_lessequals(X0,X1,tc_nat))),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f621])).
% 2.69/1.03 fof(f1646,plain,(
% 2.69/1.03 ~c_lessequals(v_n,v_m,tc_nat)),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f628])).
% 2.69/1.03 fof(f1661,plain,(
% 2.69/1.03 ![X0,X1]: (c_lessequals(c_HOL_Ominus__class_Ominus(X0,X1,tc_nat),X0,tc_nat))),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f636])).
% 2.69/1.03 fof(f1667,plain,(
% 2.69/1.03 class_Ring__and__Field_Ofield(t_a)),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f641])).
% 2.69/1.03 fof(f1668,plain,(
% 2.69/1.03 ~c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(v_a,v_m,t_a),c_Power_Opower__class_Opower(v_a,v_n,t_a),t_a)=c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(t_a),v_a,t_a),c_HOL_Ominus__class_Ominus(v_n,v_m,tc_nat),t_a)|c_lessequals(v_n,v_m,tc_nat)),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f642])).
% 2.69/1.03 fof(f1674,plain,(
% 2.69/1.03 ![X0]: (~class_Ring__and__Field_Ofield(X0)|class_Ring__and__Field_Ono__zero__divisors(X0))),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f648])).
% 2.69/1.03 fof(f1675,plain,(
% 2.69/1.03 ![X0]: (~class_Ring__and__Field_Ofield(X0)|class_Ring__and__Field_Ocomm__semiring__1(X0))),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f649])).
% 2.69/1.03 fof(f1678,plain,(
% 2.69/1.03 ![X0]: (~class_Ring__and__Field_Ofield(X0)|class_OrderedGroup_Ocomm__monoid__add(X0))),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f652])).
% 2.69/1.03 fof(f1679,plain,(
% 2.69/1.03 ![X0]: (~class_Ring__and__Field_Ofield(X0)|class_Ring__and__Field_Ozero__neq__one(X0))),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f653])).
% 2.69/1.03 fof(f1684,plain,(
% 2.69/1.03 ![X0]: (~class_Ring__and__Field_Ofield(X0)|class_Ring__and__Field_Omult__zero(X0))),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f658])).
% 2.69/1.03 fof(f1690,plain,(
% 2.69/1.03 ![X0]: (~class_Ring__and__Field_Ofield(X0)|class_Power_Opower(X0))),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f664])).
% 2.69/1.03 fof(f1691,plain,(
% 2.69/1.03 class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_nat)),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f665])).
% 2.69/1.03 fof(f1697,plain,(
% 2.69/1.03 class_Ring__and__Field_Ono__zero__divisors(tc_nat)),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f671])).
% 2.69/1.03 fof(f1699,plain,(
% 2.69/1.03 class_Ring__and__Field_Ocomm__semiring__1(tc_nat)),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f673])).
% 2.69/1.03 fof(f1702,plain,(
% 2.69/1.03 class_Ring__and__Field_Ozero__neq__one(tc_nat)),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f676])).
% 2.69/1.03 fof(f1705,plain,(
% 2.69/1.03 class_Ring__and__Field_Omult__zero(tc_nat)),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f679])).
% 2.69/1.03 fof(f1708,plain,(
% 2.69/1.03 class_Divides_Osemiring__div(tc_nat)),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f682])).
% 2.69/1.03 fof(f1711,plain,(
% 2.69/1.03 class_Orderings_Olinorder(tc_nat)),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f685])).
% 2.69/1.03 fof(f1713,plain,(
% 2.69/1.03 class_Power_Opower(tc_nat)),
% 2.69/1.03 inference(cnf_transformation,[status(thm)],[f687])).
% 2.69/1.03 fof(f1714,definition,(
% 2.69/1.03 sQ0_spl <=> (class_Ring__and__Field_Ofield(t_a))),
% 2.69/1.03 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 2.69/1.03 fof(f1716,plain,(
% 2.69/1.03 ~class_Ring__and__Field_Ofield(t_a)|sQ0_spl),
% 2.69/1.03 inference(component_clause,[status(thm)],[f1714])).
% 2.69/1.03 fof(f1717,definition,(
% 2.69/1.03 sQ1_spl <=> (v_a=c_HOL_Ozero__class_Ozero(t_a))),
% 2.69/1.03 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 2.69/1.03 fof(f1719,plain,(
% 2.69/1.03 ~v_a=c_HOL_Ozero__class_Ozero(t_a)|sQ1_spl),
% 2.69/1.03 inference(component_clause,[status(thm)],[f1717])).
% 2.69/1.03 fof(f1720,plain,(
% 2.69/1.03 ~sQ0_spl|~sQ1_spl),
% 2.69/1.03 inference(split_clause,[status(thm)],[f1340,f1714,f1717])).
% 2.69/1.03 fof(f1722,definition,(
% 2.69/1.03 sQ2_spl <=> (c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(v_a,v_m,t_a),c_Power_Opower__class_Opower(v_a,v_n,t_a),t_a)=c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(t_a),v_a,t_a),c_HOL_Ominus__class_Ominus(v_n,v_m,tc_nat),t_a))),
% 2.69/1.03 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 2.69/1.03 fof(f1724,plain,(
% 2.69/1.03 ~c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(v_a,v_m,t_a),c_Power_Opower__class_Opower(v_a,v_n,t_a),t_a)=c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(t_a),v_a,t_a),c_HOL_Ominus__class_Ominus(v_n,v_m,tc_nat),t_a)|sQ2_spl),
% 2.69/1.03 inference(component_clause,[status(thm)],[f1722])).
% 2.69/1.03 fof(f1725,definition,(
% 2.69/1.03 sQ3_spl <=> (c_lessequals(v_n,v_m,tc_nat))),
% 2.69/1.03 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 2.69/1.03 fof(f1728,plain,(
% 2.69/1.03 ~sQ2_spl|sQ3_spl),
% 2.69/1.03 inference(split_clause,[status(thm)],[f1668,f1722,f1725])).
% 2.69/1.03 fof(f1735,plain,(
% 2.69/1.03 $false|sQ0_spl),
% 2.69/1.03 inference(forward_subsumption_resolution,[status(thm)],[f1716,f1667])).
% 2.69/1.03 fof(f1736,plain,(
% 2.69/1.03 sQ0_spl),
% 2.69/1.03 inference(contradiction_clause,[status(thm)],[f1735])).
% 2.69/1.03 fof(f1840,plain,(
% 2.69/1.03 ![X0]: (c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)=X0)),
% 2.69/1.03 inference(paramodulation,[status(thm)],[f1335,f1338])).
% 2.69/1.03 fof(f1934,definition,(
% 2.69/1.03 sQ28_spl <=> (c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)))=c_HOL_Ozero__class_Ozero(tc_nat))),
% 2.69/1.03 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 2.69/1.03 fof(f1935,plain,(
% 2.69/1.03 c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)))=c_HOL_Ozero__class_Ozero(tc_nat)|~sQ28_spl),
% 2.69/1.03 inference(component_clause,[status(thm)],[f1934])).
% 2.69/1.03 fof(f2003,definition,(
% 2.69/1.03 sQ35_spl <=> (class_Ring__and__Field_Ozero__neq__one(tc_nat))),
% 2.69/1.03 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 2.69/1.03 fof(f2005,plain,(
% 2.69/1.03 ~class_Ring__and__Field_Ozero__neq__one(tc_nat)|sQ35_spl),
% 2.69/1.03 inference(component_clause,[status(thm)],[f2003])).
% 2.69/1.03 fof(f2006,definition,(
% 2.69/1.03 sQ36_spl <=> (class_Ring__and__Field_Ono__zero__divisors(tc_nat))),
% 2.69/1.03 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 2.69/1.03 fof(f2008,plain,(
% 2.69/1.03 ~class_Ring__and__Field_Ono__zero__divisors(tc_nat)|sQ36_spl),
% 2.69/1.03 inference(component_clause,[status(thm)],[f2006])).
% 2.69/1.03 fof(f2009,definition,(
% 2.69/1.03 sQ37_spl <=> (class_Ring__and__Field_Omult__zero(tc_nat))),
% 2.69/1.03 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 2.69/1.03 fof(f2011,plain,(
% 2.69/1.03 ~class_Ring__and__Field_Omult__zero(tc_nat)|sQ37_spl),
% 2.69/1.03 inference(component_clause,[status(thm)],[f2009])).
% 2.69/1.03 fof(f2115,plain,(
% 2.69/1.03 ![X0]: (c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat)=X0)),
% 2.69/1.03 inference(paramodulation,[status(thm)],[f1335,f1339])).
% 2.69/1.03 fof(f2255,plain,(
% 2.69/1.03 class_Ring__and__Field_Ono__zero__divisors(t_a)),
% 2.69/1.03 inference(resolution,[status(thm)],[f1674,f1667])).
% 2.69/1.03 fof(f2256,plain,(
% 2.69/1.03 class_Ring__and__Field_Ocomm__semiring__1(t_a)),
% 2.69/1.03 inference(resolution,[status(thm)],[f1675,f1667])).
% 2.69/1.03 fof(f2468,plain,(
% 2.69/1.03 class_OrderedGroup_Ocomm__monoid__add(t_a)),
% 2.69/1.03 inference(resolution,[status(thm)],[f1678,f1667])).
% 2.69/1.03 fof(f2516,plain,(
% 2.69/1.03 c_lessequals(v_m,v_n,tc_nat)),
% 2.69/1.03 inference(resolution,[status(thm)],[f1607,f1646])).
% 2.69/1.03 fof(f2539,plain,(
% 2.69/1.03 ![X0]: (c_HOL_Oinverse__class_Oinverse(X0,t_a)=c_HOL_Oinverse__class_Odivide(c_HOL_Oone__class_Oone(t_a),X0,t_a))),
% 2.69/1.03 inference(resolution,[status(thm)],[f1534,f1667])).
% 2.69/1.03 fof(f2542,plain,(
% 2.69/1.03 class_Ring__and__Field_Ozero__neq__one(t_a)),
% 2.69/1.03 inference(resolution,[status(thm)],[f1679,f1667])).
% 2.69/1.03 fof(f2566,definition,(
% 2.69/1.03 sQ84_spl <=> (v_m=v_n)),
% 2.69/1.03 introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition])).
% 2.69/1.03 fof(f2567,plain,(
% 2.69/1.03 v_m=v_n|~sQ84_spl),
% 2.69/1.03 inference(component_clause,[status(thm)],[f2566])).
% 2.69/1.03 fof(f2573,plain,(
% 2.69/1.03 ~c_lessequals(v_n,v_n,tc_nat)|~sQ84_spl),
% 2.69/1.03 inference(backward_demodulation,[status(thm)],[f2567,f1646])).
% 2.69/1.03 fof(f2579,plain,(
% 2.69/1.03 $false|~sQ84_spl),
% 2.69/1.03 inference(forward_subsumption_resolution,[status(thm)],[f2573,f1613])).
% 2.69/1.03 fof(f2580,plain,(
% 2.69/1.03 ~sQ84_spl),
% 2.69/1.03 inference(contradiction_clause,[status(thm)],[f2579])).
% 2.69/1.03 fof(f2656,definition,(
% 2.69/1.03 sQ96_spl <=> (class_Power_Opower(t_a))),
% 2.69/1.03 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 2.69/1.03 fof(f2658,plain,(
% 2.69/1.03 ~class_Power_Opower(t_a)|sQ96_spl),
% 2.69/1.03 inference(component_clause,[status(thm)],[f2656])).
% 2.69/1.03 fof(f2663,definition,(
% 2.69/1.03 sQ98_spl <=> (class_Power_Opower(tc_nat))),
% 2.69/1.03 introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition])).
% 2.69/1.03 fof(f2665,plain,(
% 2.69/1.03 ~class_Power_Opower(tc_nat)|sQ98_spl),
% 2.69/1.03 inference(component_clause,[status(thm)],[f2663])).
% 2.69/1.03 fof(f2670,plain,(
% 2.69/1.03 $false|sQ98_spl),
% 2.69/1.03 inference(forward_subsumption_resolution,[status(thm)],[f2665,f1713])).
% 2.69/1.03 fof(f2671,plain,(
% 2.69/1.03 sQ98_spl),
% 2.69/1.03 inference(contradiction_clause,[status(thm)],[f2670])).
% 2.69/1.03 fof(f2676,plain,(
% 2.69/1.03 ![X0,X1,X2]: (c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(X0,t_a),c_HOL_Ominus__class_Ominus(X1,X2,tc_nat),t_a)=c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(X0,X2,t_a),c_Power_Opower__class_Opower(X0,X1,t_a),t_a)|~c_lessequals(X2,X1,tc_nat)|X0=c_HOL_Ozero__class_Ozero(t_a))),
% 2.69/1.03 inference(resolution,[status(thm)],[f1554,f1667])).
% 2.69/1.03 fof(f2702,plain,(
% 2.69/1.03 class_Ring__and__Field_Omult__zero(t_a)),
% 2.69/1.03 inference(resolution,[status(thm)],[f1684,f1667])).
% 2.69/1.03 fof(f2722,plain,(
% 2.69/1.03 ![X0]: (c_HOL_Oord__class_Oless(X0,c_Suc(X0),tc_nat))),
% 2.69/1.03 inference(paramodulation,[status(thm)],[f2115,f769])).
% 2.69/1.03 fof(f2895,plain,(
% 2.69/1.03 ![X0]: (c_lessequals(X0,c_Suc(X0),tc_nat))),
% 2.69/1.03 inference(resolution,[status(thm)],[f2722,f1283])).
% 2.69/1.03 fof(f3078,plain,(
% 2.69/1.03 class_Power_Opower(t_a)),
% 2.69/1.03 inference(resolution,[status(thm)],[f1690,f1667])).
% 2.69/1.03 fof(f3079,plain,(
% 2.69/1.03 $false|sQ96_spl),
% 2.69/1.03 inference(forward_subsumption_resolution,[status(thm)],[f3078,f2658])).
% 2.69/1.03 fof(f3080,plain,(
% 2.69/1.03 sQ96_spl),
% 2.69/1.03 inference(contradiction_clause,[status(thm)],[f3079])).
% 2.69/1.03 fof(f3082,definition,(
% 2.69/1.03 sQ134_spl <=> (class_Ring__and__Field_Ozero__neq__one(t_a))),
% 2.69/1.03 introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition])).
% 2.69/1.03 fof(f3084,plain,(
% 2.69/1.03 ~class_Ring__and__Field_Ozero__neq__one(t_a)|sQ134_spl),
% 2.69/1.03 inference(component_clause,[status(thm)],[f3082])).
% 2.69/1.03 fof(f3085,definition,(
% 2.69/1.03 sQ135_spl <=> (class_Ring__and__Field_Ono__zero__divisors(t_a))),
% 2.69/1.03 introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition])).
% 2.69/1.03 fof(f3087,plain,(
% 2.69/1.03 ~class_Ring__and__Field_Ono__zero__divisors(t_a)|sQ135_spl),
% 2.69/1.03 inference(component_clause,[status(thm)],[f3085])).
% 2.69/1.03 fof(f3088,definition,(
% 2.69/1.03 sQ136_spl <=> (class_Ring__and__Field_Omult__zero(t_a))),
% 2.69/1.03 introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition])).
% 2.69/1.03 fof(f3090,plain,(
% 2.69/1.03 ~class_Ring__and__Field_Omult__zero(t_a)|sQ136_spl),
% 2.69/1.03 inference(component_clause,[status(thm)],[f3088])).
% 2.69/1.03 fof(f3095,plain,(
% 2.69/1.03 $false|sQ136_spl),
% 2.69/1.03 inference(forward_subsumption_resolution,[status(thm)],[f3090,f2702])).
% 2.69/1.03 fof(f3096,plain,(
% 2.69/1.03 sQ136_spl),
% 2.69/1.03 inference(contradiction_clause,[status(thm)],[f3095])).
% 2.69/1.03 fof(f3097,plain,(
% 2.69/1.03 $false|sQ135_spl),
% 2.69/1.03 inference(forward_subsumption_resolution,[status(thm)],[f3087,f2255])).
% 2.69/1.03 fof(f3098,plain,(
% 2.69/1.03 sQ135_spl),
% 2.69/1.03 inference(contradiction_clause,[status(thm)],[f3097])).
% 2.69/1.03 fof(f3099,plain,(
% 2.69/1.03 $false|sQ134_spl),
% 2.69/1.03 inference(forward_subsumption_resolution,[status(thm)],[f3084,f2542])).
% 2.69/1.03 fof(f3100,plain,(
% 2.69/1.03 sQ134_spl),
% 2.69/1.03 inference(contradiction_clause,[status(thm)],[f3099])).
% 2.69/1.03 fof(f3107,plain,(
% 2.69/1.03 ![X0]: (c_HOL_Oord__class_Oless(X0,c_Suc(c_Suc(X0)),tc_nat))),
% 2.69/1.03 inference(resolution,[status(thm)],[f2895,f776])).
% 2.69/1.03 fof(f3207,definition,(
% 2.69/1.03 sQ150_spl <=> (class_OrderedGroup_Ocomm__monoid__add(t_a))),
% 2.69/1.03 introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition])).
% 2.69/1.03 fof(f3209,plain,(
% 2.69/1.03 ~class_OrderedGroup_Ocomm__monoid__add(t_a)|sQ150_spl),
% 2.69/1.03 inference(component_clause,[status(thm)],[f3207])).
% 2.69/1.03 fof(f3224,plain,(
% 2.69/1.03 $false|sQ150_spl),
% 2.69/1.03 inference(forward_subsumption_resolution,[status(thm)],[f3209,f2468])).
% 2.69/1.03 fof(f3225,plain,(
% 2.69/1.03 sQ150_spl),
% 2.69/1.03 inference(contradiction_clause,[status(thm)],[f3224])).
% 2.69/1.03 fof(f3272,definition,(
% 2.69/1.03 sQ154_spl <=> (class_Divides_Osemiring__div(tc_nat))),
% 2.69/1.03 introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition])).
% 2.69/1.03 fof(f3274,plain,(
% 2.69/1.03 ~class_Divides_Osemiring__div(tc_nat)|sQ154_spl),
% 2.69/1.03 inference(component_clause,[status(thm)],[f3272])).
% 2.69/1.03 fof(f3283,plain,(
% 2.69/1.03 $false|sQ154_spl),
% 2.69/1.03 inference(forward_subsumption_resolution,[status(thm)],[f3274,f1708])).
% 2.69/1.03 fof(f3284,plain,(
% 2.69/1.03 sQ154_spl),
% 2.69/1.03 inference(contradiction_clause,[status(thm)],[f3283])).
% 2.69/1.03 fof(f3291,definition,(
% 2.69/1.03 ![X1]: (sQ158_spl <=> (~c_Ring__and__Field_Odvd__class_Odvd(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X1,tc_nat)))),
% 2.69/1.03 introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition])).
% 2.69/1.03 fof(f3292,plain,(
% 2.69/1.03 ![X0]: (~c_Ring__and__Field_Odvd__class_Odvd(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat)|~sQ158_spl)),
% 2.69/1.03 inference(component_clause,[status(thm)],[f3291])).
% 2.69/1.03 fof(f3303,plain,(
% 2.69/1.03 $false|~sQ158_spl),
% 2.69/1.03 inference(forward_subsumption_resolution,[status(thm)],[f3292,f709])).
% 2.69/1.03 fof(f3304,plain,(
% 2.69/1.03 ~sQ158_spl),
% 2.69/1.03 inference(contradiction_clause,[status(thm)],[f3303])).
% 2.69/1.03 fof(f3425,plain,(
% 2.69/1.03 ![X0]: (c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(X0,t_a),c_HOL_Ominus__class_Ominus(v_n,v_m,tc_nat),t_a)=c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(X0,v_m,t_a),c_Power_Opower__class_Opower(X0,v_n,t_a),t_a)|X0=c_HOL_Ozero__class_Ozero(t_a))),
% 2.69/1.03 inference(resolution,[status(thm)],[f2676,f2516])).
% 2.69/1.03 fof(f3520,definition,(
% 2.69/1.03 ![X0]: (sQ179_spl <=> (~X0=X0))),
% 2.69/1.03 introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition])).
% 2.69/1.03 fof(f3521,plain,(
% 2.69/1.03 ![X0]: (~X0=X0|~sQ179_spl)),
% 2.69/1.03 inference(component_clause,[status(thm)],[f3520])).
% 2.69/1.03 fof(f3524,plain,(
% 2.69/1.03 $false|~sQ179_spl),
% 2.69/1.03 inference(trivial_equality_resolution,[status(thm)],[f3521])).
% 2.69/1.03 fof(f3525,plain,(
% 2.69/1.03 ~sQ179_spl),
% 2.69/1.03 inference(contradiction_clause,[status(thm)],[f3524])).
% 2.69/1.03 fof(f3636,plain,(
% 2.69/1.03 ~c_HOL_Oinverse__class_Odivide(c_Power_Opower__class_Opower(v_a,v_m,t_a),c_Power_Opower__class_Opower(v_a,v_n,t_a),t_a)=c_Power_Opower__class_Opower(c_HOL_Oinverse__class_Oinverse(v_a,t_a),c_HOL_Ominus__class_Ominus(v_n,v_m,tc_nat),t_a)|sQ2_spl),
% 2.69/1.03 inference(backward_demodulation,[status(thm)],[f2539,f1724])).
% 2.69/1.03 fof(f3712,definition,(
% 2.69/1.03 sQ191_spl <=> (class_Orderings_Olinorder(tc_nat))),
% 2.69/1.03 introduced(definition,[new_symbols(definition,[sQ191_spl])],[split_symbol_definition])).
% 2.69/1.03 fof(f3714,plain,(
% 2.69/1.03 ~class_Orderings_Olinorder(tc_nat)|sQ191_spl),
% 2.69/1.03 inference(component_clause,[status(thm)],[f3712])).
% 2.69/1.03 fof(f3716,plain,(
% 2.69/1.03 $false|sQ191_spl),
% 2.69/1.03 inference(forward_subsumption_resolution,[status(thm)],[f3714,f1711])).
% 2.69/1.03 fof(f3717,plain,(
% 2.69/1.03 sQ191_spl),
% 2.69/1.03 inference(contradiction_clause,[status(thm)],[f3716])).
% 2.69/1.03 fof(f3725,definition,(
% 2.69/1.03 ![X0]: (sQ192_spl <=> (~X0=c_HOL_Ozero__class_Ozero(tc_nat)))),
% 2.69/1.03 introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition])).
% 2.69/1.03 fof(f3726,plain,(
% 2.69/1.03 ![X0]: (~X0=c_HOL_Ozero__class_Ozero(tc_nat)|~sQ192_spl)),
% 2.69/1.03 inference(component_clause,[status(thm)],[f3725])).
% 2.69/1.03 fof(f3777,plain,(
% 2.69/1.03 $false|~sQ192_spl),
% 2.69/1.03 inference(backward_subsumption_resolution,[status(thm)],[f1334,f3726])).
% 2.69/1.03 fof(f3786,plain,(
% 2.69/1.03 ~sQ192_spl),
% 2.69/1.03 inference(contradiction_clause,[status(thm)],[f3777])).
% 2.69/1.03 fof(f3850,definition,(
% 2.69/1.03 ![X0]: (sQ203_spl <=> (~c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat)=c_HOL_Ozero__class_Ozero(tc_nat)|~c_lessequals(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)))),
% 2.69/1.03 introduced(definition,[new_symbols(definition,[sQ203_spl])],[split_symbol_definition])).
% 2.69/1.03 fof(f3851,plain,(
% 2.69/1.03 ![X0]: (~c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat)=c_HOL_Ozero__class_Ozero(tc_nat)|~c_lessequals(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)|~sQ203_spl)),
% 2.69/1.03 inference(component_clause,[status(thm)],[f3850])).
% 2.69/1.03 fof(f3870,plain,(
% 2.69/1.03 ![X0]: (~X0=c_HOL_Ozero__class_Ozero(tc_nat)|~c_lessequals(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)|~sQ203_spl)),
% 2.69/1.03 inference(forward_demodulation,[status(thm)],[f2115,f3851])).
% 2.69/1.03 fof(f3871,plain,(
% 2.69/1.03 ![X0]: (~X0=c_HOL_Ozero__class_Ozero(tc_nat)|~sQ203_spl)),
% 2.69/1.03 inference(forward_subsumption_resolution,[status(thm)],[f3870,f1314])).
% 2.69/1.03 fof(f3934,plain,(
% 2.69/1.03 $false|~sQ203_spl),
% 2.69/1.03 inference(resolution,[status(thm)],[f3871,f1186])).
% 2.69/1.03 fof(f3942,plain,(
% 2.69/1.03 ~sQ203_spl),
% 2.69/1.03 inference(contradiction_clause,[status(thm)],[f3934])).
% 2.69/1.03 fof(f4012,plain,(
% 2.69/1.03 v_n=v_m|~c_lessequals(v_n,v_m,tc_nat)),
% 2.69/1.03 inference(resolution,[status(thm)],[f1635,f2516])).
% 2.69/1.03 fof(f4027,plain,(
% 2.69/1.03 sQ84_spl|~sQ3_spl),
% 2.69/1.03 inference(split_clause,[status(thm)],[f4012,f2566,f1725])).
% 2.69/1.03 fof(f4325,definition,(
% 2.69/1.03 ![X0]: (sQ232_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)))),
% 2.69/1.03 introduced(definition,[new_symbols(definition,[sQ232_spl])],[split_symbol_definition])).
% 2.69/1.03 fof(f4326,plain,(
% 2.69/1.03 ![X0]: (c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat)|~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)|~sQ232_spl)),
% 2.69/1.03 inference(component_clause,[status(thm)],[f4325])).
% 2.69/1.03 fof(f4352,definition,(
% 2.69/1.03 ![X0]: (sQ238_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat)|~c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat)))),
% 2.69/1.03 introduced(definition,[new_symbols(definition,[sQ238_spl])],[split_symbol_definition])).
% 2.69/1.03 fof(f4353,plain,(
% 2.69/1.03 ![X0]: (c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat)|~c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat)|~sQ238_spl)),
% 2.69/1.03 inference(component_clause,[status(thm)],[f4352])).
% 2.69/1.03 fof(f4360,definition,(
% 2.69/1.03 sQ240_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat))),
% 2.69/1.03 introduced(definition,[new_symbols(definition,[sQ240_spl])],[split_symbol_definition])).
% 2.69/1.03 fof(f4361,plain,(
% 2.69/1.03 c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat)|~sQ240_spl),
% 2.69/1.03 inference(component_clause,[status(thm)],[f4360])).
% 2.69/1.03 fof(f4453,plain,(
% 2.69/1.03 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat)|~sQ240_spl),
% 2.69/1.03 inference(forward_demodulation,[status(thm)],[f1840,f4361])).
% 2.69/1.03 fof(f4454,plain,(
% 2.69/1.03 $false|~sQ240_spl),
% 2.69/1.03 inference(forward_subsumption_resolution,[status(thm)],[f4453,f1161])).
% 2.69/1.03 fof(f4455,plain,(
% 2.69/1.03 ~sQ240_spl),
% 2.69/1.03 inference(contradiction_clause,[status(thm)],[f4454])).
% 2.69/1.03 fof(f4459,plain,(
% 2.69/1.03 ![X0]: (c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat)|~c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat)|~sQ238_spl)),
% 2.69/1.03 inference(forward_demodulation,[status(thm)],[f2115,f4353])).
% 2.69/1.03 fof(f4460,plain,(
% 2.69/1.03 ![X0]: (~c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat)|~sQ238_spl)),
% 2.69/1.03 inference(forward_subsumption_resolution,[status(thm)],[f4459,f1161])).
% 2.69/1.03 fof(f4463,plain,(
% 2.69/1.03 ![X0]: (~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)|~sQ232_spl)),
% 2.69/1.03 inference(forward_subsumption_resolution,[status(thm)],[f4326,f1161])).
% 2.69/1.03 fof(f4485,plain,(
% 2.69/1.03 $false|~sQ238_spl),
% 2.69/1.03 inference(resolution,[status(thm)],[f4460,f1661])).
% 2.69/1.03 fof(f4492,plain,(
% 2.69/1.03 ~sQ238_spl),
% 2.69/1.03 inference(contradiction_clause,[status(thm)],[f4485])).
% 2.69/1.03 fof(f4494,plain,(
% 2.69/1.03 $false|~sQ232_spl),
% 2.69/1.03 inference(backward_subsumption_resolution,[status(thm)],[f720,f4463])).
% 2.69/1.03 fof(f4504,plain,(
% 2.69/1.03 ~sQ232_spl),
% 2.69/1.03 inference(contradiction_clause,[status(thm)],[f4494])).
% 2.69/1.03 fof(f4532,plain,(
% 2.69/1.03 ![X0]: (c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Oone__class_Oone(t_a),X0,t_a))),
% 2.69/1.03 inference(resolution,[status(thm)],[f1045,f2256])).
% 2.69/1.03 fof(f4533,plain,(
% 2.69/1.03 ![X0]: (c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Oone__class_Oone(tc_nat),X0,tc_nat))),
% 2.69/1.03 inference(resolution,[status(thm)],[f1045,f1699])).
% 2.69/1.03 fof(f4539,definition,(
% 2.69/1.03 ![X1]: (sQ256_spl <=> (~c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Oone__class_Oone(t_a),X1,t_a)))),
% 2.69/1.03 introduced(definition,[new_symbols(definition,[sQ256_spl])],[split_symbol_definition])).
% 2.69/1.03 fof(f4540,plain,(
% 2.69/1.03 ![X0]: (~c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Oone__class_Oone(t_a),X0,t_a)|~sQ256_spl)),
% 2.69/1.03 inference(component_clause,[status(thm)],[f4539])).
% 2.69/1.03 fof(f4547,plain,(
% 2.69/1.03 $false|~sQ256_spl),
% 2.69/1.03 inference(forward_subsumption_resolution,[status(thm)],[f4540,f4532])).
% 2.69/1.03 fof(f4548,plain,(
% 2.69/1.03 ~sQ256_spl),
% 2.69/1.03 inference(contradiction_clause,[status(thm)],[f4547])).
% 2.69/1.03 fof(f4558,definition,(
% 2.69/1.03 ![X1]: (sQ259_spl <=> (~c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Oone__class_Oone(tc_nat),X1,tc_nat)))),
% 2.69/1.03 introduced(definition,[new_symbols(definition,[sQ259_spl])],[split_symbol_definition])).
% 2.69/1.03 fof(f4559,plain,(
% 2.69/1.03 ![X0]: (~c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Oone__class_Oone(tc_nat),X0,tc_nat)|~sQ259_spl)),
% 2.69/1.03 inference(component_clause,[status(thm)],[f4558])).
% 2.69/1.03 fof(f4566,plain,(
% 2.69/1.03 $false|~sQ259_spl),
% 2.69/1.03 inference(forward_subsumption_resolution,[status(thm)],[f4559,f4533])).
% 2.69/1.03 fof(f4567,plain,(
% 2.69/1.03 ~sQ259_spl),
% 2.69/1.03 inference(contradiction_clause,[status(thm)],[f4566])).
% 2.69/1.03 fof(f4650,plain,(
% 2.69/1.03 $false|~sQ28_spl),
% 2.69/1.03 inference(forward_subsumption_resolution,[status(thm)],[f1935,f767])).
% 2.69/1.03 fof(f4651,plain,(
% 2.69/1.03 ~sQ28_spl),
% 2.69/1.03 inference(contradiction_clause,[status(thm)],[f4650])).
% 2.69/1.03 fof(f5440,definition,(
% 2.69/1.03 ![X0]: (sQ306_spl <=> (~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)))),
% 2.69/1.03 introduced(definition,[new_symbols(definition,[sQ306_spl])],[split_symbol_definition])).
% 2.69/1.03 fof(f5441,plain,(
% 2.69/1.03 ![X0]: (~c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)|~sQ306_spl)),
% 2.69/1.03 inference(component_clause,[status(thm)],[f5440])).
% 2.69/1.03 fof(f5448,definition,(
% 2.69/1.03 ![X0]: (sQ308_spl <=> (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)))),
% 2.69/1.03 introduced(definition,[new_symbols(definition,[sQ308_spl])],[split_symbol_definition])).
% 2.69/1.03 fof(f5449,plain,(
% 2.69/1.03 ![X0]: (c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)|~sQ308_spl)),
% 3.47/1.05 inference(component_clause,[status(thm)],[f5448])).
% 3.47/1.05 fof(f5524,plain,(
% 3.47/1.05 $false|~sQ306_spl),
% 3.47/1.05 inference(resolution,[status(thm)],[f5441,f3107])).
% 3.47/1.05 fof(f5533,plain,(
% 3.47/1.05 ~sQ306_spl),
% 3.47/1.05 inference(contradiction_clause,[status(thm)],[f5524])).
% 3.47/1.05 fof(f5537,plain,(
% 3.47/1.05 $false|~sQ308_spl),
% 3.47/1.05 inference(resolution,[status(thm)],[f5449,f1161])).
% 3.47/1.05 fof(f5565,plain,(
% 3.47/1.05 ~sQ308_spl),
% 3.47/1.05 inference(contradiction_clause,[status(thm)],[f5537])).
% 3.47/1.05 fof(f5575,definition,(
% 3.47/1.05 sQ311_spl <=> (class_Ring__and__Field_Ocomm__semiring__1(tc_nat))),
% 3.47/1.05 introduced(definition,[new_symbols(definition,[sQ311_spl])],[split_symbol_definition])).
% 3.47/1.05 fof(f5577,plain,(
% 3.47/1.05 ~class_Ring__and__Field_Ocomm__semiring__1(tc_nat)|sQ311_spl),
% 3.47/1.05 inference(component_clause,[status(thm)],[f5575])).
% 3.47/1.05 fof(f5590,definition,(
% 3.47/1.05 sQ315_spl <=> (class_Ring__and__Field_Ocomm__semiring__1(t_a))),
% 3.47/1.05 introduced(definition,[new_symbols(definition,[sQ315_spl])],[split_symbol_definition])).
% 3.47/1.05 fof(f5592,plain,(
% 3.47/1.05 ~class_Ring__and__Field_Ocomm__semiring__1(t_a)|sQ315_spl),
% 3.47/1.05 inference(component_clause,[status(thm)],[f5590])).
% 3.47/1.05 fof(f5617,plain,(
% 3.47/1.05 $false|sQ311_spl),
% 3.47/1.05 inference(forward_subsumption_resolution,[status(thm)],[f5577,f1699])).
% 3.47/1.05 fof(f5618,plain,(
% 3.47/1.05 sQ311_spl),
% 3.47/1.05 inference(contradiction_clause,[status(thm)],[f5617])).
% 3.47/1.05 fof(f5619,plain,(
% 3.47/1.05 $false|sQ315_spl),
% 3.47/1.05 inference(forward_subsumption_resolution,[status(thm)],[f5592,f2256])).
% 3.47/1.05 fof(f5620,plain,(
% 3.47/1.05 sQ315_spl),
% 3.47/1.05 inference(contradiction_clause,[status(thm)],[f5619])).
% 3.47/1.05 fof(f5764,plain,(
% 3.47/1.05 $false|sQ37_spl),
% 3.47/1.05 inference(forward_subsumption_resolution,[status(thm)],[f2011,f1705])).
% 3.47/1.05 fof(f5765,plain,(
% 3.47/1.05 sQ37_spl),
% 3.47/1.05 inference(contradiction_clause,[status(thm)],[f5764])).
% 3.47/1.05 fof(f5766,plain,(
% 3.47/1.05 $false|sQ36_spl),
% 3.47/1.05 inference(forward_subsumption_resolution,[status(thm)],[f2008,f1697])).
% 3.47/1.05 fof(f5767,plain,(
% 3.47/1.05 sQ36_spl),
% 3.47/1.05 inference(contradiction_clause,[status(thm)],[f5766])).
% 3.47/1.05 fof(f5768,plain,(
% 3.47/1.05 $false|sQ35_spl),
% 3.47/1.05 inference(forward_subsumption_resolution,[status(thm)],[f2005,f1702])).
% 3.47/1.05 fof(f5769,plain,(
% 3.47/1.05 sQ35_spl),
% 3.47/1.05 inference(contradiction_clause,[status(thm)],[f5768])).
% 3.47/1.05 fof(f5877,definition,(
% 3.47/1.05 sQ340_spl <=> (v_n=v_n)),
% 3.47/1.05 introduced(definition,[new_symbols(definition,[sQ340_spl])],[split_symbol_definition])).
% 3.47/1.05 fof(f5879,plain,(
% 3.47/1.05 ~v_n=v_n|sQ340_spl),
% 3.47/1.05 inference(component_clause,[status(thm)],[f5877])).
% 3.47/1.05 fof(f5884,plain,(
% 3.47/1.05 $false|sQ340_spl),
% 3.47/1.05 inference(trivial_equality_resolution,[status(thm)],[f5879])).
% 3.47/1.05 fof(f5885,plain,(
% 3.47/1.05 sQ340_spl),
% 3.47/1.05 inference(contradiction_clause,[status(thm)],[f5884])).
% 3.47/1.05 fof(f7877,definition,(
% 3.47/1.05 sQ558_spl <=> (class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_nat))),
% 3.47/1.05 introduced(definition,[new_symbols(definition,[sQ558_spl])],[split_symbol_definition])).
% 3.47/1.05 fof(f7879,plain,(
% 3.47/1.05 ~class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_nat)|sQ558_spl),
% 3.47/1.05 inference(component_clause,[status(thm)],[f7877])).
% 3.47/1.05 fof(f7919,plain,(
% 3.47/1.05 $false|sQ558_spl),
% 3.47/1.05 inference(forward_subsumption_resolution,[status(thm)],[f7879,f1691])).
% 3.47/1.05 fof(f7920,plain,(
% 3.47/1.05 sQ558_spl),
% 3.47/1.05 inference(contradiction_clause,[status(thm)],[f7919])).
% 3.47/1.05 fof(f8178,plain,(
% 3.47/1.05 v_a=c_HOL_Ozero__class_Ozero(t_a)|sQ2_spl),
% 3.47/1.05 inference(resolution,[status(thm)],[f3425,f3636])).
% 3.47/1.05 fof(f8199,plain,(
% 3.47/1.05 $false|sQ1_spl|sQ2_spl),
% 3.47/1.05 inference(forward_subsumption_resolution,[status(thm)],[f8178,f1719])).
% 3.47/1.05 fof(f8200,plain,(
% 3.47/1.05 sQ1_spl|sQ2_spl),
% 3.47/1.05 inference(contradiction_clause,[status(thm)],[f8199])).
% 3.47/1.05 fof(f8201,plain,(
% 3.47/1.05 $false),
% 3.47/1.05 inference(sat_refutation,[status(thm)],[f1720,f1728,f1736,f2580,f2671,f3080,f3096,f3098,f3100,f3225,f3284,f3304,f3525,f3717,f3786,f3942,f4027,f4455,f4492,f4504,f4548,f4567,f4651,f5533,f5565,f5618,f5620,f5765,f5767,f5769,f5885,f7920,f8200])).
% 3.47/1.05 % SZS output end CNFRefutation for theBenchmark.p
% 3.47/1.07 % Elapsed time: 0.602370 seconds
% 3.47/1.07 % CPU time: 4.060961 seconds
% 3.47/1.07 % Total memory used: 179.093 MB
% 3.47/1.07 % Net memory used: 176.665 MB
%------------------------------------------------------------------------------