%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG412-1 : TPTP v9.3.1. Released v4.1.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 06:50:09 AM UTC 2026
% Result : Unsatisfiable 245.26s 38.52s
% Output : CNFRefutation 245.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 13
% Syntax : Number of formulae : 47 ( 20 unt; 0 def)
% Number of atoms : 83 ( 66 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 58 ( 22 ~; 36 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 3 con; 0-3 aty)
% Number of variables : 39 ( 0 sgn 11 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(cls_no__zero__divirors__neq0_0,axiom,
! [VAR_0,VAR_1,VAR_2] :
( VAR_2 = c_HOL_Ozero__class_Ozero(VAR_0)
| VAR_1 = c_HOL_Ozero__class_Ozero(VAR_0)
| c_HOL_Otimes__class_Otimes(VAR_1,VAR_2,VAR_0) != c_HOL_Ozero__class_Ozero(VAR_0)
| ~ class_Ring__and__Field_Ono__zero__divisors(VAR_0) ),
file('theBenchmark.p',cls_no__zero__divirors__neq0_0) ).
cnf(c_532,plain,
( C = c_HOL_Ozero__class_Ozero(A)
| B = c_HOL_Ozero__class_Ozero(A)
| c_HOL_Otimes__class_Otimes(B,C,A) != c_HOL_Ozero__class_Ozero(A)
| ~ class_Ring__and__Field_Ono__zero__divisors(A) ),
inference(clausify,[status(thm)],[cls_no__zero__divirors__neq0_0]) ).
fof(clsarity_Complex__Ocomplex__Ring__and__Field_Ono__zero__divisors,axiom,
class_Ring__and__Field_Ono__zero__divisors(tc_Complex_Ocomplex),
file('theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Ono__zero__divisors) ).
cnf(c_535,plain,
class_Ring__and__Field_Ono__zero__divisors(tc_Complex_Ocomplex),
inference(clausify,[status(thm)],[clsarity_Complex__Ocomplex__Ring__and__Field_Ono__zero__divisors]) ).
fof(cls_add__0__left_0,axiom,
! [VAR_0,VAR_1] :
( c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(VAR_0),VAR_1,VAR_0) = VAR_1
| ~ class_OrderedGroup_Omonoid__add(VAR_0) ),
file('theBenchmark.p',cls_add__0__left_0) ).
cnf(c_554,plain,
( c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(A),B,A) = B
| ~ class_OrderedGroup_Omonoid__add(A) ),
inference(clausify,[status(thm)],[cls_add__0__left_0]) ).
fof(clsarity_Complex__Ocomplex__OrderedGroup_Omonoid__add,axiom,
class_OrderedGroup_Omonoid__add(tc_Complex_Ocomplex),
file('theBenchmark.p',clsarity_Complex__Ocomplex__OrderedGroup_Omonoid__add) ).
cnf(c_557,plain,
class_OrderedGroup_Omonoid__add(tc_Complex_Ocomplex),
inference(clausify,[status(thm)],[clsarity_Complex__Ocomplex__OrderedGroup_Omonoid__add]) ).
cnf(c_565,plain,
c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),A,tc_Complex_Ocomplex) = A,
inference(resolve,[status(thm)],[c_554,c_557]) ).
cnf(c_582,plain,
( B = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| A = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_HOL_Otimes__class_Otimes(A,B,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(resolve,[status(thm)],[c_532,c_535]) ).
cnf(c_54304,plain,
( B = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = A
| c_HOL_Otimes__class_Otimes(A,B,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(copy,[status(thm)],[c_582]) ).
cnf(c_583,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = B
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = A
| c_HOL_Otimes__class_Otimes(A,B,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(copy,[status(thm)],[c_54304]) ).
fof(cls_poly__pCons_0,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( c_Polynomial_Opoly(c_Polynomial_OpCons(VAR_1,VAR_2,VAR_0),VAR_3,VAR_0) = c_HOL_Oplus__class_Oplus(VAR_1,c_HOL_Otimes__class_Otimes(VAR_3,c_Polynomial_Opoly(VAR_2,VAR_3,VAR_0),VAR_0),VAR_0)
| ~ class_Ring__and__Field_Ocomm__semiring__0(VAR_0) ),
file('theBenchmark.p',cls_poly__pCons_0) ).
cnf(c_1018,plain,
( c_Polynomial_Opoly(c_Polynomial_OpCons(B,C,A),D,A) = c_HOL_Oplus__class_Oplus(B,c_HOL_Otimes__class_Otimes(D,c_Polynomial_Opoly(C,D,A),A),A)
| ~ class_Ring__and__Field_Ocomm__semiring__0(A) ),
inference(clausify,[status(thm)],[cls_poly__pCons_0]) ).
fof(cls_pCons_Oprems_0,axiom,
! [VAR_0] :
( VAR_0 = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_Polynomial_Opoly(c_Polynomial_OpCons(v_d____,v_ds____,tc_Complex_Ocomplex),VAR_0,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
file('theBenchmark.p',cls_pCons_Oprems_0) ).
cnf(c_1091,plain,
( A = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_Polynomial_Opoly(c_Polynomial_OpCons(v_d____,v_ds____,tc_Complex_Ocomplex),A,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(clausify,[status(thm)],[cls_pCons_Oprems_0]) ).
cnf(c_1092,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = A
| c_Polynomial_Opoly(c_Polynomial_OpCons(v_d____,v_ds____,tc_Complex_Ocomplex),A,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(copy,[status(thm)],[c_1091]) ).
fof(cls_pCons__0__0_0,axiom,
! [VAR_0] :
( c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(VAR_0),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(VAR_0)),VAR_0) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(VAR_0))
| ~ class_HOL_Ozero(VAR_0) ),
file('theBenchmark.p',cls_pCons__0__0_0) ).
cnf(c_1097,plain,
( c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(A),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(A)),A) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(A))
| ~ class_HOL_Ozero(A) ),
inference(clausify,[status(thm)],[cls_pCons__0__0_0]) ).
fof(cls_CHAINED_1,axiom,
( v_ds____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_Polynomial_Opoly(v_ds____,v_sko__CHAINED__1(v_ds____),tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
file('theBenchmark.p',cls_CHAINED_1) ).
cnf(c_1100,plain,
( v_ds____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_Polynomial_Opoly(v_ds____,v_sko__CHAINED__1(v_ds____),tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(clausify,[status(thm)],[cls_CHAINED_1]) ).
fof(cls_CHAINED_0,axiom,
( v_ds____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| v_sko__CHAINED__1(v_ds____) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
file('theBenchmark.p',cls_CHAINED_0) ).
cnf(c_1101,plain,
( v_ds____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| v_sko__CHAINED__1(v_ds____) != c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(clausify,[status(thm)],[cls_CHAINED_0]) ).
fof(cls_CHAINED_0_02,axiom,
v_d____ = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
file('theBenchmark.p',cls_CHAINED_0_02) ).
cnf(c_1103,plain,
v_d____ = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),
inference(clausify,[status(thm)],[cls_CHAINED_0_02]) ).
fof(cls_conjecture_0,axiom,
c_Polynomial_OpCons(v_d____,v_ds____,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
file('theBenchmark.p',cls_conjecture_0) ).
cnf(c_1104,plain,
c_Polynomial_OpCons(v_d____,v_ds____,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(clausify,[status(thm)],[cls_conjecture_0]) ).
cnf(c_1105,plain,
c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),v_ds____,tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(paramod,[status(thm)],[c_1103,c_1104]) ).
fof(clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__0,axiom,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),
file('theBenchmark.p',clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__0) ).
cnf(c_1131,plain,
class_Ring__and__Field_Ocomm__semiring__0(tc_Complex_Ocomplex),
inference(clausify,[status(thm)],[clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__0]) ).
fof(clsarity_Complex__Ocomplex__HOL_Ozero,axiom,
class_HOL_Ozero(tc_Complex_Ocomplex),
file('theBenchmark.p',clsarity_Complex__Ocomplex__HOL_Ozero) ).
cnf(c_1138,plain,
class_HOL_Ozero(tc_Complex_Ocomplex),
inference(clausify,[status(thm)],[clsarity_Complex__Ocomplex__HOL_Ozero]) ).
cnf(c_1881,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = A
| c_Polynomial_Opoly(c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),v_ds____,tc_Complex_Ocomplex),A,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(paramod,[status(thm)],[c_1103,c_1092]) ).
cnf(c_2687,plain,
c_Polynomial_Opoly(c_Polynomial_OpCons(A,B,tc_Complex_Ocomplex),C,tc_Complex_Ocomplex) = c_HOL_Oplus__class_Oplus(A,c_HOL_Otimes__class_Otimes(C,c_Polynomial_Opoly(B,C,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex),
inference(resolve,[status(thm)],[c_1131,c_1018]) ).
cnf(c_54305,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = A
| c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Otimes__class_Otimes(A,c_Polynomial_Opoly(v_ds____,A,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(paramod,[status(thm)],[c_2687,c_1881]) ).
cnf(c_2718,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = A
| c_HOL_Otimes__class_Otimes(A,c_Polynomial_Opoly(v_ds____,A,tc_Complex_Ocomplex),tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(paramod,[status(thm)],[c_565,c_54305]) ).
cnf(c_2763,plain,
c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(resolve,[status(thm)],[c_1138,c_1097]) ).
cnf(c_54306,plain,
( c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_Polynomial_Opoly(v_ds____,A,tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = A
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = A ),
inference(resolve,[status(thm)],[c_2718,c_583]) ).
cnf(c_54307,plain,
( c_Polynomial_Opoly(v_ds____,A,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = A
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = A ),
inference(copy,[status(thm)],[c_54306]) ).
cnf(c_54174,plain,
( c_Polynomial_Opoly(v_ds____,A,tc_Complex_Ocomplex) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = A ),
inference(copy,[status(thm)],[c_54307]) ).
cnf(c_54308,plain,
( v_ds____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) = v_sko__CHAINED__1(v_ds____) ),
inference(resolve,[status(thm)],[c_54174,c_1100]) ).
cnf(c_54284,plain,
( v_ds____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| v_sko__CHAINED__1(v_ds____) = c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(copy,[status(thm)],[c_54308]) ).
cnf(c_54309,plain,
( v_ds____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| v_ds____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(resolve,[status(thm)],[c_54284,c_1101]) ).
cnf(c_54302,plain,
v_ds____ = c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(copy,[status(thm)],[c_54309]) ).
cnf(c_54310,plain,
c_Polynomial_OpCons(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Complex_Ocomplex) != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(paramod,[status(thm)],[c_54302,c_1105]) ).
cnf(c_54311,plain,
c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) != c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(paramod,[status(thm)],[c_2763,c_54310]) ).
cnf(c_54303,plain,
$false,
inference(copy,[status(thm)],[c_54311]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG412-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/5.39 % Computer : n017.cluster.edu
% 0.10/5.39 % Model : x86_64 x86_64
% 0.10/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.39 % Memory : 8046.5625MB
% 0.10/5.39 % OS : Linux 6.8.0-71-generic
% 0.10/5.39 % CPULimit : 300
% 0.10/5.39 % WCLimit : 300
% 0.10/5.39 % DateTime : Sat Sep 26 21:53:39 UTC 2026
% 0.10/5.39 % CPUTime :
% 0.10/5.39 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/5.39 % Process 1729275 was started by sandbox2 on n017,
% 0.10/5.39 % Sat Sep 26 21:53:39 2026
% 0.10/5.39 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.15/5.42
% 0.15/5.42 % From the command line: assign(max_seconds, 300).
% 245.26/38.52
% 245.26/38.52 % given #500 (I,wt=19): 1191 c_HOL_Oord__class_Oless(c_HOL_Oinverse__class_Odivide(A,B,tc_RealDef_Oreal),c_HOL_Oinverse__class_Odivide(C,B,tc_RealDef_Oreal),tc_RealDef_Oreal) | -c_HOL_Oord__class_Oless(B,c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal) | -c_HOL_Oord__class_Oless(C,A,tc_RealDef_Oreal). [resolve(1,a,26,a)].
% 245.26/38.52
% 245.26/38.52 % given #1000 (T,wt=4): 7204 class_OrderedGroup_Ocancel__comm__monoid__add(tc_Polynomial_Opoly(tc_Polynomial_Opoly(tc_RealDef_Oreal))). [resolve(2358,a,1106,b)].
% 245.26/38.52
% 245.26/38.52 % given #1500 (F,wt=20): 7812 -c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(A,c_HOL_Otimes__class_Otimes(B,c_HOL_Ouminus__class_Ouminus(C,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Ouminus__class_Ouminus(A,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(B,C,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal). [para(693(a,1),3635(a,1)),rewrite([1389(10),693(12)])].
% 245.26/38.52
% 245.26/38.52 % given #2000 (T,wt=10): 10083 c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Ouminus__class_Ouminus(A,tc_Polynomial_Opoly(tc_Polynomial_Opoly(tc_Complex_Ocomplex))),A,tc_Polynomial_Opoly(tc_Polynomial_Opoly(tc_Complex_Ocomplex))). [resolve(8021,a,920,c),unit_del(a,7542)].
% 245.26/38.52
% 245.26/38.52 % given #2500 (F,wt=19): 19811 c_HOL_Oplus__class_Oplus(A,c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_Complex_Ocomplex),c_HOL_Oplus__class_Oplus(B,C,tc_Complex_Ocomplex),tc_Complex_Ocomplex),tc_Complex_Ocomplex) != c_HOL_Oplus__class_Oplus(B,c_HOL_Oplus__class_Oplus(A,C,tc_Complex_Ocomplex),tc_Complex_Ocomplex). [para(2651(a,1),14710(a,1,2)),rewrite([618(6)])].
% 245.26/38.52
% 245.26/38.52 % given #3000 (A,wt=28): 2212 c_HOL_Oord__class_Oless(A,B,tc_RealDef_Oreal) | -c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(C,c_HOL_Otimes__class_Otimes(D,B,tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(C,c_HOL_Otimes__class_Otimes(D,A,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) | -c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(C,D,tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal). [para(693(a,1),807(b,1)),rewrite([693(10)])].
% 245.26/38.52
% 245.26/38.52 % given #3500 (T,wt=12): 17790 c_Ring__and__Field_Odvd__class_Odvd(c_HOL_Osgn__class_Osgn(A,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(B,c_HOL_Oplus__class_Oplus(A,A,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal). [resolve(17568,a,823,c),unit_del(a,1118)].
% 245.26/38.52
% 245.26/38.52 % given #4000 (F,wt=19): 34615 c_HOL_Oplus__class_Oplus(A,c_HOL_Oplus__class_Oplus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ouminus__class_Ouminus(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),tc_RealDef_Oreal),A,tc_RealDef_Oreal),B,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal) != B. [para(3192(a,1),18859(a,2,2)),rewrite([562(18)])].
% 245.26/38.52
% 245.26/38.52 % given #4500 (T,wt=12): 44988 -class_Ring__and__Field_Ocomm__ring__1(tc_nat) | c_Ring__and__Field_Odvd__class_Odvd(A,c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(A,A,tc_nat),A,tc_nat),tc_nat). [resolve(7844,c,7830,a)].
% 245.26/38.52
% 245.26/38.52 % given #5000 (F,wt=18): 46819 -c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_HOL_Oabs__class_Oabs(A,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(c_HOL_Oabs__class_Oabs(B,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(C,C,tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),tc_RealDef_Oreal). [para(2570(a,1),46794(a,1,1)),rewrite([693(10)])].
% 245.26/38.52
% 245.26/38.52 % SZS status Unsatisfiable for theBenchmark
% 245.26/38.52
% 245.26/38.52 % Proof 1 at 26.47 (+ 4.70) seconds.
% 245.26/38.52 % Length of proof is 26.
% 245.26/38.52 % Level of proof is 7.
% 245.26/38.52 % Maximum clause weight is 20.000.
% 245.26/38.52 % Given clauses 5231.
% 245.26/38.52
% 245.26/38.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------