%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SWW288+1 : TPTP v5.2.0. Released v5.2.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %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 : Mon Mar 7 02:03:02 EST 2011
% Result : Theorem 146.22s
% Output : Solution 146.22s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP29163/SWW288+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% WARNING: TreeLimitedRun lost 0.85s, total lost is 0.85s
% found
% SZS status THM for /tmp/SystemOnTPTP29163/SWW288+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP29163/SWW288+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 29395
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% PrfWatch: 1.92 CPU 2.01 WC
% # Preprocessing time : 0.219 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,class_Int_Oring__char__0(t_a),file('/tmp/SRASS.s.p', tfree_0)).
% fof(2, axiom,class_Rings_Oidom(t_a),file('/tmp/SRASS.s.p', tfree_1)).
% fof(49, 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/SRASS.s.p', fact__096p_A_061_A_091_058poly_Ap_A_I0_058_058_Ha_J_058_093_096)).
% fof(96, axiom,![X2]:![X3]:(class_Groups_Ozero(X3)=>c_Polynomial_Odegree(X3,c_Polynomial_OpCons(X3,X2,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X3))))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),file('/tmp/SRASS.s.p', fact_degree__pCons__0)).
% fof(123, axiom,![X39]:(class_Int_Oring__char__0(X39)=>class_Groups_Ozero(X39)),file('/tmp/SRASS.s.p', clrel_Int_Oring__char__0__Groups_Ozero)).
% fof(1218, conjecture,c_Polynomial_Odegree(t_a,v_p)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat),file('/tmp/SRASS.s.p', conj_0)).
% fof(1219, negated_conjecture,~(c_Polynomial_Odegree(t_a,v_p)=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),inference(assume_negation,[status(cth)],[1218])).
% fof(1292, 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)])).
% cnf(1293,plain,(class_Int_Oring__char__0(t_a)),inference(split_conjunct,[status(thm)],[1])).
% cnf(1294,plain,(class_Rings_Oidom(t_a)),inference(split_conjunct,[status(thm)],[2])).
% fof(1422, 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)],[49])).
% cnf(1423,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)],[1422])).
% fof(1615, plain,![X2]:![X3]:(~(class_Groups_Ozero(X3))|c_Polynomial_Odegree(X3,c_Polynomial_OpCons(X3,X2,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X3))))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),inference(fof_nnf,[status(thm)],[96])).
% fof(1616, plain,![X4]:![X5]:(~(class_Groups_Ozero(X5))|c_Polynomial_Odegree(X5,c_Polynomial_OpCons(X5,X4,c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(X5))))=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),inference(variable_rename,[status(thm)],[1615])).
% cnf(1617,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)],[1616])).
% fof(1694, plain,![X39]:(~(class_Int_Oring__char__0(X39))|class_Groups_Ozero(X39)),inference(fof_nnf,[status(thm)],[123])).
% fof(1695, plain,![X40]:(~(class_Int_Oring__char__0(X40))|class_Groups_Ozero(X40)),inference(variable_rename,[status(thm)],[1694])).
% cnf(1696,plain,(class_Groups_Ozero(X1)|~class_Int_Oring__char__0(X1)),inference(split_conjunct,[status(thm)],[1695])).
% cnf(5318,negated_conjecture,(c_Polynomial_Odegree(t_a,v_p)!=c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),inference(split_conjunct,[status(thm)],[1292])).
% cnf(5508,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_Rings_Oidom(t_a)),inference(rw,[status(thm)],[1423,1293,theory(equality)])).
% cnf(5509,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)],[5508,1294,theory(equality)])).
% cnf(5510,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)],[5509,theory(equality)])).
% cnf(5681,plain,(class_Groups_Ozero(t_a)),inference(spm,[status(thm)],[1696,1293,theory(equality)])).
% cnf(6755,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)],[1617,5510,theory(equality)])).
% cnf(6756,plain,(~class_Groups_Ozero(t_a)),inference(sr,[status(thm)],[6755,5318,theory(equality)])).
% cnf(69056,plain,($false),inference(rw,[status(thm)],[6756,5681,theory(equality)])).
% cnf(69057,plain,($false),inference(cn,[status(thm)],[69056,theory(equality)])).
% cnf(69058,plain,($false),69057,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 2962
% # ...of these trivial : 11
% # ...subsumed : 258
% # ...remaining for further processing: 2693
% # Other redundant clauses eliminated : 164
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 3
% # Backward-rewritten : 6
% # Generated clauses : 35722
% # ...of the previous two non-trivial : 32835
% # Contextual simplify-reflections : 21
% # Paramodulations : 35508
% # Factorizations : 8
% # Equation resolutions : 206
% # Current number of processed clauses: 1323
% # Positive orientable unit clauses: 181
% # Positive unorientable unit clauses: 10
% # Negative unit clauses : 13
% # Non-unit-clauses : 1119
% # Current number of unprocessed clauses: 32784
% # ...number of literals in the above : 116315
% # Clause-clause subsumption calls (NU) : 111466
% # Rec. Clause-clause subsumption calls : 56886
% # Unit Clause-clause subsumption calls : 123
% # Rewrite failures with RHS unbound : 2
% # Indexed BW rewrite attempts : 1119
% # Indexed BW rewrite successes : 188
% # Backwards rewriting index: 739 leaves, 2.45+/-4.246 terms/leaf
% # Paramod-from index: 436 leaves, 1.46+/-1.440 terms/leaf
% # Paramod-into index: 642 leaves, 2.02+/-2.995 terms/leaf
% # -------------------------------------------------
% # User time : 1.884 s
% # System time : 0.057 s
% # Total time : 1.941 s
% # Maximum resident set size: 0 pages
% PrfWatch: 3.19 CPU 3.28 WC
% FINAL PrfWatch: 3.19 CPU 3.28 WC
% SZS output end Solution for /tmp/SystemOnTPTP29163/SWW288+1.tptp
%
%------------------------------------------------------------------------------