%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SWW272+1 : TPTP v8.1.0. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n032.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 21 00:47:10 EDT 2022
% Result : Theorem 161.10s 156.23s
% Output : Proof 161.10s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.08 % Problem : SWW272+1 : TPTP v8.1.0. Released v5.2.0.
% 0.00/0.08 % Command : leancop_casc.sh %s %d
% 0.07/0.27 % Computer : n032.cluster.edu
% 0.07/0.27 % Model : x86_64 x86_64
% 0.07/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.27 % Memory : 8042.1875MB
% 0.07/0.27 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.27 % CPULimit : 300
% 0.07/0.27 % WCLimit : 600
% 0.07/0.27 % DateTime : Mon Jun 6 06:37:19 EDT 2022
% 0.07/0.27 % CPUTime :
% 161.10/156.23 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 161.10/156.24 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 161.10/156.24
% 161.10/156.24 %-----------------------------------------------------
% 161.10/156.24 fof(conj_0, conjecture, (! v_s____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', conj_0)).
% 161.10/156.24 fof(fact_pne, axiom, (! v_pa____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', fact_pne)).
% 161.10/156.24 fof(fact_s, axiom, v_pa____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), c_Polynomial_Oorder(tc_Complex_Ocomplex, v_a____, v_pa____))), v_s____), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', fact_s)).
% 161.10/156.24 fof(fact_mult__eq__0__iff, axiom, ! [_633348, _633351, _633354] : (class_Rings_Oring__no__zero__divisors(_633354) => (hAPP(hAPP(c_Groups_Otimes__class_Otimes(_633354), _633351), _633348) = c_Groups_Ozero__class_Ozero(_633354) <=> _633351 = c_Groups_Ozero__class_Ozero(_633354) | _633348 = c_Groups_Ozero__class_Ozero(_633354))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', fact_mult__eq__0__iff)).
% 161.10/156.24 fof(arity_Complex__Ocomplex__Rings_Oidom, axiom, class_Rings_Oidom(tc_Complex_Ocomplex), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', arity_Complex__Ocomplex__Rings_Oidom)).
% 161.10/156.24 fof(arity_Polynomial__Opoly__Rings_Oring__no__zero__divisors, axiom, ! [_634926] : (class_Rings_Oidom(_634926) => class_Rings_Oring__no__zero__divisors(tc_Polynomial_Opoly(_634926))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', arity_Polynomial__Opoly__Rings_Oring__no__zero__divisors)).
% 161.10/156.24
% 161.10/156.24 cnf(1, plain, [-(v_s____ = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))], clausify(conj_0)).
% 161.10/156.24 cnf(2, plain, [-(_63969 = _63971), _63969 = _63970, _63970 = _63971], theory(equality)).
% 161.10/156.24 cnf(3, plain, [v_pa____ = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))], clausify(fact_pne)).
% 161.10/156.24 cnf(4, plain, [-(v_pa____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), c_Polynomial_Oorder(tc_Complex_Ocomplex, v_a____, v_pa____))), v_s____))], clausify(fact_s)).
% 161.10/156.24 cnf(5, plain, [class_Rings_Oring__no__zero__divisors(_79231), -(hAPP(hAPP(c_Groups_Otimes__class_Otimes(_79231), _79230), _79229) = c_Groups_Ozero__class_Ozero(_79231)), _79229 = c_Groups_Ozero__class_Ozero(_79231)], clausify(fact_mult__eq__0__iff)).
% 161.10/156.24 cnf(6, plain, [-(class_Rings_Oidom(tc_Complex_Ocomplex))], clausify(arity_Complex__Ocomplex__Rings_Oidom)).
% 161.10/156.24 cnf(7, plain, [class_Rings_Oidom(_297467), -(class_Rings_Oring__no__zero__divisors(tc_Polynomial_Opoly(_297467)))], clausify(arity_Polynomial__Opoly__Rings_Oring__no__zero__divisors)).
% 161.10/156.24
% 161.10/156.24 cnf('1',plain,[-(v_s____ = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))],start(1)).
% 161.10/156.24 cnf('1.1',plain,[v_s____ = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), class_Rings_Oring__no__zero__divisors(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), -(hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), c_Polynomial_Oorder(tc_Complex_Ocomplex, v_a____, v_pa____))), v_s____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)))],extension(5,bind([[_79230, _79229, _79231], [hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), c_Polynomial_Oorder(tc_Complex_Ocomplex, v_a____, v_pa____)), v_s____, tc_Polynomial_Opoly(tc_Complex_Ocomplex)]]))).
% 161.10/156.24 cnf('1.1.1',plain,[-(class_Rings_Oring__no__zero__divisors(tc_Polynomial_Opoly(tc_Complex_Ocomplex))), class_Rings_Oidom(tc_Complex_Ocomplex)],extension(7,bind([[_297467], [tc_Complex_Ocomplex]]))).
% 161.10/156.24 cnf('1.1.1.1',plain,[-(class_Rings_Oidom(tc_Complex_Ocomplex))],extension(6)).
% 161.10/156.24 cnf('1.1.2',plain,[hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), c_Polynomial_Oorder(tc_Complex_Ocomplex, v_a____, v_pa____))), v_s____) = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), -(v_pa____ = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))), v_pa____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), c_Polynomial_Oorder(tc_Complex_Ocomplex, v_a____, v_pa____))), v_s____)],extension(2,bind([[_63971, _63969, _63970], [c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), v_pa____, hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), c_Polynomial_Oorder(tc_Complex_Ocomplex, v_a____, v_pa____))), v_s____)]]))).
% 161.10/156.24 cnf('1.1.2.1',plain,[v_pa____ = c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))],extension(3)).
% 161.10/156.24 cnf('1.1.2.2',plain,[-(v_pa____ = hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), hAPP(hAPP(c_Power_Opower__class_Opower(tc_Polynomial_Opoly(tc_Complex_Ocomplex)), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Ouminus__class_Ouminus(tc_Complex_Ocomplex, v_a____), c_Polynomial_OpCons(tc_Complex_Ocomplex, c_Groups_Oone__class_Oone(tc_Complex_Ocomplex), c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))))), c_Polynomial_Oorder(tc_Complex_Ocomplex, v_a____, v_pa____))), v_s____))],extension(4)).
% 161.10/156.24 %-----------------------------------------------------
% 161.10/156.25
% 161.10/156.25 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------