%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : ALG429-1 : TPTP v8.1.0. Released v4.1.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n022.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Thu Jul 14 18:03:38 EDT 2022
% Result : Unsatisfiable 6.24s 6.46s
% Output : Refutation 6.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 14
% Syntax : Number of clauses : 52 ( 13 unt; 30 nHn; 52 RR)
% Number of literals : 143 ( 0 equ; 51 neg)
% Maximal clause size : 4 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 6 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1152,axiom,
~ equal(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v),
file('ALG429-1.p',unknown),
[] ).
cnf(1156,axiom,
( ~ equal(c_Polynomial_Opoly(v,u,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| ~ c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| equal(c_Polynomial_Odegree(v,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_nat))
| equal(c_Polynomial_Opoly(v_q,u,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
file('ALG429-1.p',unknown),
[] ).
cnf(1157,axiom,
( ~ equal(c_Polynomial_Opoly(v_q,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| equal(c_Polynomial_Odegree(v,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_nat))
| equal(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q)
| c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
file('ALG429-1.p',unknown),
[] ).
cnf(1158,axiom,
( ~ equal(c_Polynomial_Opoly(v_q,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| equal(c_Polynomial_Odegree(v,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_nat))
| equal(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v)
| c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
file('ALG429-1.p',unknown),
[] ).
cnf(1159,axiom,
( equal(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q)
| c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| equal(c_Polynomial_Opoly(v,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| equal(c_Polynomial_Odegree(v,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_nat)) ),
file('ALG429-1.p',unknown),
[] ).
cnf(1160,axiom,
( equal(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v)
| c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| equal(c_Polynomial_Opoly(v,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| equal(c_Polynomial_Odegree(v,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_nat)) ),
file('ALG429-1.p',unknown),
[] ).
cnf(1162,axiom,
( ~ equal(c_Polynomial_Opoly(v,u,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| ~ c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| ~ equal(c_Polynomial_Odegree(v,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_nat))
| equal(c_Polynomial_Opoly(v_q,u,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
file('ALG429-1.p',unknown),
[] ).
cnf(1163,axiom,
( ~ equal(c_Polynomial_Opoly(v_q,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| ~ equal(c_Polynomial_Odegree(v,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_nat))
| equal(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q)
| c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
file('ALG429-1.p',unknown),
[] ).
cnf(1164,axiom,
( ~ equal(c_Polynomial_Opoly(v_q,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| ~ equal(c_Polynomial_Odegree(v,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_nat))
| equal(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v)
| c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
file('ALG429-1.p',unknown),
[] ).
cnf(1165,axiom,
( ~ equal(c_Polynomial_Odegree(v,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_nat))
| equal(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q)
| c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| equal(c_Polynomial_Opoly(v,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
file('ALG429-1.p',unknown),
[] ).
cnf(1166,axiom,
( ~ equal(c_Polynomial_Odegree(v,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_nat))
| equal(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v)
| c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| equal(c_Polynomial_Opoly(v,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
file('ALG429-1.p',unknown),
[] ).
cnf(1350,axiom,
( ~ c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| equal(c_Polynomial_Opoly(v,v_x,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
file('ALG429-1.p',unknown),
[] ).
cnf(1351,axiom,
( ~ equal(c_Polynomial_Opoly(v_q,v_x,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| ~ c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
file('ALG429-1.p',unknown),
[] ).
cnf(1354,axiom,
( ~ equal(c_Polynomial_Opoly(v,u,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| equal(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v)
| c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| equal(c_Polynomial_Opoly(v_q,u,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
file('ALG429-1.p',unknown),
[] ).
cnf(1407,plain,
( equal(v_q,v)
| c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| equal(c_Polynomial_Opoly(v,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| equal(c_Polynomial_Odegree(v,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_nat)) ),
inference(rew,[status(thm),theory(equality)],[1159,1160]),
[iquote('0:Rew:1159.0,1160.0')] ).
cnf(1408,plain,
( equal(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v)
| c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| equal(c_Polynomial_Opoly(v,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| equal(c_Polynomial_Odegree(v,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_nat)) ),
inference(rew,[status(thm),theory(equality)],[1407,1159]),
[iquote('0:Rew:1407.0,1159.0')] ).
cnf(1409,plain,
( ~ equal(c_Polynomial_Opoly(v,u,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| equal(c_Polynomial_Opoly(v_q,u,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
inference(mrr,[status(thm)],[1354,1152]),
[iquote('0:MRR:1354.1,1152.0')] ).
cnf(1410,plain,
( c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| equal(c_Polynomial_Opoly(v,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| equal(c_Polynomial_Odegree(v,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_nat)) ),
inference(mrr,[status(thm)],[1408,1152]),
[iquote('0:MRR:1408.0,1152.0')] ).
cnf(1411,plain,
( ~ equal(c_Polynomial_Opoly(v_q,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| equal(c_Polynomial_Odegree(v,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_nat))
| equal(v_q,v)
| c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(rew,[status(thm),theory(equality)],[1157,1158]),
[iquote('0:Rew:1157.2,1158.2')] ).
cnf(1412,plain,
( ~ equal(c_Polynomial_Opoly(v_q,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| equal(c_Polynomial_Odegree(v,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_nat))
| equal(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v)
| c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(rew,[status(thm),theory(equality)],[1411,1157]),
[iquote('0:Rew:1411.2,1157.2')] ).
cnf(1413,plain,
( ~ equal(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat))
| equal(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q)
| c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| equal(c_Polynomial_Opoly(v,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
inference(rew,[status(thm),theory(equality)],[1410,1165]),
[iquote('0:Rew:1410.2,1165.0')] ).
cnf(1414,plain,
( equal(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q)
| c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| equal(c_Polynomial_Opoly(v,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
inference(obv,[status(thm),theory(equality)],[1413]),
[iquote('0:Obv:1413.0')] ).
cnf(1415,plain,
( ~ equal(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat))
| equal(v_q,v)
| c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| equal(c_Polynomial_Opoly(v,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
inference(rew,[status(thm),theory(equality)],[1414,1166,1410]),
[iquote('0:Rew:1414.0,1166.1,1410.2,1166.0')] ).
cnf(1416,plain,
( equal(v_q,v)
| c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| equal(c_Polynomial_Opoly(v,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
inference(obv,[status(thm),theory(equality)],[1415]),
[iquote('0:Obv:1415.0')] ).
cnf(1417,plain,
( equal(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v)
| c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| equal(c_Polynomial_Opoly(v,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
inference(rew,[status(thm),theory(equality)],[1416,1414]),
[iquote('0:Rew:1416.0,1414.0')] ).
cnf(1418,plain,
( equal(c_Polynomial_Opoly(v,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(mrr,[status(thm)],[1417,1152]),
[iquote('0:MRR:1417.0,1152.0')] ).
cnf(1419,plain,
( ~ equal(c_Polynomial_Opoly(v_q,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| equal(c_Polynomial_Odegree(v,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_nat))
| c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(mrr,[status(thm)],[1412,1152]),
[iquote('0:MRR:1412.2,1152.0')] ).
cnf(1421,plain,
( ~ equal(c_Polynomial_Opoly(v,u,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| equal(c_Polynomial_Odegree(v,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_nat))
| equal(c_Polynomial_Opoly(v_q,u,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
inference(mrr,[status(thm)],[1156,1409]),
[iquote('0:MRR:1156.1,1409.1')] ).
cnf(1422,plain,
( ~ equal(c_Polynomial_Opoly(v,u,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_HOL_Ozero__class_Ozero(tc_nat),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| equal(c_Polynomial_Opoly(v_q,u,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
inference(rew,[status(thm),theory(equality)],[1421,1409]),
[iquote('0:Rew:1421.1,1409.1')] ).
cnf(1423,plain,
( ~ equal(c_Polynomial_Opoly(v_q,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| ~ equal(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat))
| equal(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q)
| c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(rew,[status(thm),theory(equality)],[1419,1163]),
[iquote('0:Rew:1419.1,1163.1')] ).
cnf(1424,plain,
( ~ equal(c_Polynomial_Opoly(v_q,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| equal(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v_q)
| c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(obv,[status(thm),theory(equality)],[1423]),
[iquote('0:Obv:1423.1')] ).
cnf(1425,plain,
( ~ equal(c_Polynomial_Opoly(v_q,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| ~ equal(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat))
| equal(v_q,v)
| c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(rew,[status(thm),theory(equality)],[1424,1164,1419]),
[iquote('0:Rew:1424.1,1164.2,1419.1,1164.1')] ).
cnf(1426,plain,
( ~ equal(c_Polynomial_Opoly(v_q,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| equal(v_q,v)
| c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(obv,[status(thm),theory(equality)],[1425]),
[iquote('0:Obv:1425.1')] ).
cnf(1427,plain,
( ~ equal(c_Polynomial_Opoly(v_q,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| equal(c_HOL_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),v)
| c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(rew,[status(thm),theory(equality)],[1426,1424]),
[iquote('0:Rew:1426.1,1424.1')] ).
cnf(1428,plain,
( ~ equal(c_Polynomial_Opoly(v_q,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)) ),
inference(mrr,[status(thm)],[1427,1152]),
[iquote('0:MRR:1427.1,1152.0')] ).
cnf(1431,plain,
( ~ equal(c_Polynomial_Opoly(v,u,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| ~ c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_HOL_Ozero__class_Ozero(tc_nat),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| ~ equal(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat))
| equal(c_Polynomial_Opoly(v_q,u,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
inference(rew,[status(thm),theory(equality)],[1421,1162]),
[iquote('0:Rew:1421.1,1162.2,1421.1,1162.1')] ).
cnf(1432,plain,
( ~ equal(c_Polynomial_Opoly(v,u,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| ~ c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_HOL_Ozero__class_Ozero(tc_nat),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex))
| equal(c_Polynomial_Opoly(v_q,u,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
inference(obv,[status(thm),theory(equality)],[1431]),
[iquote('0:Obv:1431.2')] ).
cnf(1433,plain,
( ~ equal(c_Polynomial_Opoly(v,u,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| equal(c_Polynomial_Opoly(v_q,u,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
inference(mrr,[status(thm)],[1432,1422]),
[iquote('0:MRR:1432.1,1422.1')] ).
cnf(1438,plain,
~ c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(spt,[spt(split,[position(s1)])],[1350]),
[iquote('1:Spt:1350.0')] ).
cnf(1439,plain,
equal(c_Polynomial_Opoly(v,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
inference(mrr,[status(thm)],[1418,1438]),
[iquote('1:MRR:1418.1,1438.0')] ).
cnf(1440,plain,
~ equal(c_Polynomial_Opoly(v_q,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
inference(mrr,[status(thm)],[1428,1438]),
[iquote('1:MRR:1428.1,1438.0')] ).
cnf(29543,plain,
( ~ equal(c_Polynomial_Opoly(v,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| ~ equal(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
inference(spl,[status(thm),theory(equality)],[1433,1440]),
[iquote('1:SpL:1433.1,1440.0')] ).
cnf(29544,plain,
~ equal(c_Polynomial_Opoly(v,v_sko__CHAINED__1(v,v_q),tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
inference(obv,[status(thm),theory(equality)],[29543]),
[iquote('1:Obv:29543.1')] ).
cnf(29545,plain,
~ equal(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
inference(rew,[status(thm),theory(equality)],[1439,29544]),
[iquote('1:Rew:1439.0,29544.0')] ).
cnf(29546,plain,
$false,
inference(obv,[status(thm),theory(equality)],[29545]),
[iquote('1:Obv:29545.0')] ).
cnf(29547,plain,
c_Ring__and__Field_Odvd__class_Odvd(v,c_Power_Opower__class_Opower(v_q,c_Polynomial_Odegree(v,tc_Complex_Ocomplex),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(spt,[spt(split,[position(sa)])],[29546,1438]),
[iquote('1:Spt:29546.0,1350.0,1438.0')] ).
cnf(29548,plain,
equal(c_Polynomial_Opoly(v,v_x,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
inference(spt,[spt(split,[position(s2)])],[1350]),
[iquote('1:Spt:29546.0,1350.1')] ).
cnf(29549,plain,
~ equal(c_Polynomial_Opoly(v_q,v_x,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
inference(mrr,[status(thm)],[1351,29547]),
[iquote('1:MRR:1351.1,29547.0')] ).
cnf(29551,plain,
( ~ equal(c_Polynomial_Opoly(v,v_x,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex))
| ~ equal(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)) ),
inference(spl,[status(thm),theory(equality)],[1433,29549]),
[iquote('1:SpL:1433.1,29549.0')] ).
cnf(29552,plain,
~ equal(c_Polynomial_Opoly(v,v_x,tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
inference(obv,[status(thm),theory(equality)],[29551]),
[iquote('1:Obv:29551.1')] ).
cnf(29553,plain,
~ equal(c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex),c_HOL_Ozero__class_Ozero(tc_Complex_Ocomplex)),
inference(rew,[status(thm),theory(equality)],[29548,29552]),
[iquote('1:Rew:29548.0,29552.0')] ).
cnf(29554,plain,
$false,
inference(obv,[status(thm),theory(equality)],[29553]),
[iquote('1:Obv:29553.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : ALG429-1 : TPTP v8.1.0. Released v4.1.0.
% 0.08/0.13 % Command : run_spass %d %s
% 0.13/0.34 % Computer : n022.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Wed Jun 8 12:16:20 EDT 2022
% 0.13/0.34 % CPUTime :
% 6.24/6.46
% 6.24/6.46 SPASS V 3.9
% 6.24/6.46 SPASS beiseite: Proof found.
% 6.24/6.46 % SZS status Theorem
% 6.24/6.46 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.24/6.46 SPASS derived 24910 clauses, backtracked 5 clauses, performed 1 splits and kept 3719 clauses.
% 6.24/6.46 SPASS allocated 90898 KBytes.
% 6.24/6.46 SPASS spent 0:00:06.09 on the problem.
% 6.24/6.46 0:00:00.10 for the input.
% 6.24/6.46 0:00:00.00 for the FLOTTER CNF translation.
% 6.24/6.46 0:00:00.23 for inferences.
% 6.24/6.46 0:00:00.00 for the backtracking.
% 6.24/6.46 0:00:05.56 for the reduction.
% 6.24/6.46
% 6.24/6.46
% 6.24/6.46 Here is a proof with depth 1, length 52 :
% 6.24/6.46 % SZS output start Refutation
% See solution above
% 6.34/6.58 Formulae used in the proof : cls_pe_0 cls_CHAINED_4 cls_CHAINED_3 cls_CHAINED_2 cls_CHAINED_1 cls_CHAINED_0 cls_CHAINED_4_02 cls_CHAINED_3_03 cls_CHAINED_2_04 cls_CHAINED_1_05 cls_CHAINED_0_06 cls_conjecture_0 cls_conjecture_1 cls_conjecture_4
% 6.34/6.58
%------------------------------------------------------------------------------