%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : SWW288+1 : TPTP v5.2.0. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art02.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Sun Mar 6 15:45:35 EST 2011
% Result : Theorem 4.40s
% Output : CNFRefutation 4.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 6
% Syntax : Number of formulae : 28 ( 14 unt; 0 def)
% Number of atoms : 47 ( 15 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 35 ( 16 ~; 15 |; 1 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-3 aty)
% Number of variables : 12 ( 1 sgn 9 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(45,axiom,
( ( class_Int_Oring__char__0(t_a)
& class_Rings_Oidom(t_a) )
=> v_p = c_Polynomial_OpCons(t_a,hAPP(c_Polynomial_Opoly(t_a,v_p),c_Groups_Ozero__class_Ozero(t_a)),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))) ),
file('/tmp/tmpORVMpP/sel_SWW288+1.p_1',fact__096p_A_061_A_091_058poly_Ap_A_I0_058_058_Ha_J_058_093_096) ).
fof(310,axiom,
! [X3,X4] :
( class_Groups_Ozero(X4)
=> c_Polynomial_Odegree(X4,c_Polynomial_OpCons(X4,X3,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X4)))) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
file('/tmp/tmpORVMpP/sel_SWW288+1.p_1',fact_degree__pCons__0) ).
fof(445,axiom,
! [X38] :
( class_Int_Oring__char__0(X38)
=> class_Groups_Ozero(X38) ),
file('/tmp/tmpORVMpP/sel_SWW288+1.p_1',clrel_Int_Oring__char__0__Groups_Ozero) ).
fof(603,conjecture,
c_Polynomial_Odegree(t_a,v_p) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
file('/tmp/tmpORVMpP/sel_SWW288+1.p_1',conj_0) ).
fof(1183,axiom,
class_Int_Oring__char__0(t_a),
file('/tmp/tmpORVMpP/sel_SWW288+1.p_1',tfree_0) ).
fof(1184,axiom,
class_Rings_Oidom(t_a),
file('/tmp/tmpORVMpP/sel_SWW288+1.p_1',tfree_1) ).
fof(1219,negated_conjecture,
c_Polynomial_Odegree(t_a,v_p) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(assume_negation,[status(cth)],[603]) ).
fof(1258,negated_conjecture,
c_Polynomial_Odegree(t_a,v_p) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(fof_simplification,[status(thm)],[1219,theory(equality)]) ).
fof(1444,plain,
( ~ class_Int_Oring__char__0(t_a)
| ~ class_Rings_Oidom(t_a)
| v_p = c_Polynomial_OpCons(t_a,hAPP(c_Polynomial_Opoly(t_a,v_p),c_Groups_Ozero__class_Ozero(t_a)),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))) ),
inference(fof_nnf,[status(thm)],[45]) ).
cnf(1445,plain,
( v_p = c_Polynomial_OpCons(t_a,hAPP(c_Polynomial_Opoly(t_a,v_p),c_Groups_Ozero__class_Ozero(t_a)),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a)))
| ~ class_Rings_Oidom(t_a)
| ~ class_Int_Oring__char__0(t_a) ),
inference(split_conjunct,[status(thm)],[1444]) ).
fof(2354,plain,
! [X3,X4] :
( ~ class_Groups_Ozero(X4)
| c_Polynomial_Odegree(X4,c_Polynomial_OpCons(X4,X3,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X4)))) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
inference(fof_nnf,[status(thm)],[310]) ).
fof(2355,plain,
! [X5,X6] :
( ~ class_Groups_Ozero(X6)
| c_Polynomial_Odegree(X6,c_Polynomial_OpCons(X6,X5,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X6)))) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
inference(variable_rename,[status(thm)],[2354]) ).
cnf(2356,plain,
( c_Polynomial_Odegree(X1,c_Polynomial_OpCons(X1,X2,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X1)))) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| ~ class_Groups_Ozero(X1) ),
inference(split_conjunct,[status(thm)],[2355]) ).
fof(2767,plain,
! [X38] :
( ~ class_Int_Oring__char__0(X38)
| class_Groups_Ozero(X38) ),
inference(fof_nnf,[status(thm)],[445]) ).
fof(2768,plain,
! [X39] :
( ~ class_Int_Oring__char__0(X39)
| class_Groups_Ozero(X39) ),
inference(variable_rename,[status(thm)],[2767]) ).
cnf(2769,plain,
( class_Groups_Ozero(X1)
| ~ class_Int_Oring__char__0(X1) ),
inference(split_conjunct,[status(thm)],[2768]) ).
cnf(3261,negated_conjecture,
c_Polynomial_Odegree(t_a,v_p) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(split_conjunct,[status(thm)],[1258]) ).
cnf(5197,plain,
class_Int_Oring__char__0(t_a),
inference(split_conjunct,[status(thm)],[1183]) ).
cnf(5198,plain,
class_Rings_Oidom(t_a),
inference(split_conjunct,[status(thm)],[1184]) ).
cnf(5490,plain,
class_Groups_Ozero(t_a),
inference(spm,[status(thm)],[2769,5197,theory(equality)]) ).
cnf(5938,plain,
( c_Polynomial_OpCons(t_a,hAPP(c_Polynomial_Opoly(t_a,v_p),c_Groups_Ozero__class_Ozero(t_a)),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))) = v_p
| $false
| ~ class_Int_Oring__char__0(t_a) ),
inference(rw,[status(thm)],[1445,5198,theory(equality)]) ).
cnf(5939,plain,
( c_Polynomial_OpCons(t_a,hAPP(c_Polynomial_Opoly(t_a,v_p),c_Groups_Ozero__class_Ozero(t_a)),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))) = v_p
| $false
| $false ),
inference(rw,[status(thm)],[5938,5197,theory(equality)]) ).
cnf(5940,plain,
c_Polynomial_OpCons(t_a,hAPP(c_Polynomial_Opoly(t_a,v_p),c_Groups_Ozero__class_Ozero(t_a)),c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(t_a))) = v_p,
inference(cn,[status(thm)],[5939,theory(equality)]) ).
cnf(6390,plain,
( c_Polynomial_Odegree(t_a,v_p) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| ~ class_Groups_Ozero(t_a) ),
inference(spm,[status(thm)],[2356,5940,theory(equality)]) ).
cnf(6391,plain,
~ class_Groups_Ozero(t_a),
inference(sr,[status(thm)],[6390,3261,theory(equality)]) ).
cnf(69764,plain,
$false,
inference(rw,[status(thm)],[6391,5490,theory(equality)]) ).
cnf(69765,plain,
$false,
inference(cn,[status(thm)],[69764,theory(equality)]) ).
cnf(69766,plain,
$false,
69765,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/SWW/SWW288+1.p
% --creating new selector for []
% -running prover on /tmp/tmpORVMpP/sel_SWW288+1.p_1 with time limit 29
% -prover status Theorem
% Problem SWW288+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/SWW/SWW288+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/SWW/SWW288+1.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% See solution above
% # SZS output end CNFRefutation
%
%------------------------------------------------------------------------------