%------------------------------------------------------------------------------ % File : SRASS---0.1 % Problem : SWW254+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 01:29:26 EST 2011 % Result : Timeout 300s % Output : None % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----NO SOLUTION OUTPUT BY SYSTEM %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % Reading problem from /tmp/SystemOnTPTP10952/SWW254+1.tptp % Adding relevance values % Extracting the conjecture % Sorting axioms by relevance % Looking for THM ... % WARNING: TreeLimitedRun lost 0.69s, total lost is 0.69s % not found % Adding ~C to TBU ... ~conj_0: % ---- Iteration 1 (0 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % WARNING: TreeLimitedRun lost 0.04s, total lost is 0.73s % not found % Looking for CSA axiom ... fact_a00: % CSA axiom fact_a00 found % Looking for CSA axiom ... fact_poly__bound__exists: % CSA axiom fact_poly__bound__exists found % Looking for CSA axiom ... fact_calculation: % CSA axiom fact_calculation found % ---- Iteration 2 (3 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % WARNING: TreeLimitedRun lost 0.02s, total lost is 0.75s % not found % Looking for CSA axiom ... fact_real__zero__not__eq__one: % CSA axiom fact_real__zero__not__eq__one found % Looking for CSA axiom ... fact_real__mult__less__mono2: % WARNING: TreeLimitedRun lost 0.08s, total lost is 0.83s % CSA axiom fact_real__mult__less__mono2 found % Looking for CSA axiom ... fact_real__mult__order: % CSA axiom fact_real__mult__order found % ---- Iteration 3 (6 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % WARNING: TreeLimitedRun lost 0.17s, total lost is 1.00s % not found % Looking for CSA axiom ... fact_real__mult__less__iff1: % CSA axiom fact_real__mult__less__iff1 found % Looking for CSA axiom ... fact_cq0: % WARNING: TreeLimitedRun lost 0.06s, total lost is 1.06s % CSA axiom fact_cq0 found % Looking for CSA axiom ... fact_norm__not__less__zero: % WARNING: TreeLimitedRun lost 0.18s, total lost is 1.24s % CSA axiom fact_norm__not__less__zero found % ---- Iteration 4 (9 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % WARNING: TreeLimitedRun lost 0.16s, total lost is 1.40s % not found % Looking for CSA axiom ... fact_real__0__le__divide__iff: % CSA axiom fact_real__0__le__divide__iff found % Looking for CSA axiom ... fact_qnc: % WARNING: TreeLimitedRun lost 0.12s, total lost is 1.52s % CSA axiom fact_qnc found % Looking for CSA axiom ... fact__096constant_A_Ipoly_Aq_J_A_061_061_062_AFalse_096: % WARNING: TreeLimitedRun lost 0.16s, total lost is 1.68s % CSA axiom fact__096constant_A_Ipoly_Aq_J_A_061_061_062_AFalse_096 found % ---- Iteration 5 (12 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_ln__gt__zero: % CSA axiom fact_ln__gt__zero found % Looking for CSA axiom ... fact_ln__gt__zero__iff: % WARNING: TreeLimitedRun lost 0.18s, total lost is 1.86s % CSA axiom fact_ln__gt__zero__iff found % Looking for CSA axiom ... fact_ln__less__zero__iff: % CSA axiom fact_ln__less__zero__iff found % ---- Iteration 6 (15 axioms selected) % Looking for TBU SAT ... % WARNING: TreeLimitedRun lost 0.18s, total lost is 2.04s % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_ln__less__zero: % WARNING: TreeLimitedRun lost 0.09s, total lost is 2.13s % fact_ln__gt__zero__imp__gt__one: % WARNING: TreeLimitedRun lost 0.11s, total lost is 2.24s % fact_int__0__less__1: % CSA axiom fact_int__0__less__1 found % Looking for CSA axiom ... fact_divide__pos__pos: % WARNING: TreeLimitedRun lost 0.19s, total lost is 2.43s % CSA axiom fact_divide__pos__pos found % Looking for CSA axiom ... fact_divide__pos__neg: % WARNING: TreeLimitedRun lost 0.17s, total lost is 2.60s % CSA axiom fact_divide__pos__neg found % ---- Iteration 7 (18 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % WARNING: TreeLimitedRun lost 0.17s, total lost is 2.77s % not found % Looking for CSA axiom ... fact_ln__less__zero: % fact_ln__gt__zero__imp__gt__one: % WARNING: TreeLimitedRun lost 0.18s, total lost is 2.95s % fact_divide__neg__pos: % CSA axiom fact_divide__neg__pos found % Looking for CSA axiom ... fact_divide__strict__right__mono__neg: % WARNING: TreeLimitedRun lost 0.17s, total lost is 3.12s % CSA axiom fact_divide__strict__right__mono__neg found % Looking for CSA axiom ... fact_divide__strict__right__mono: % WARNING: TreeLimitedRun lost 0.17s, total lost is 3.29s % CSA axiom fact_divide__strict__right__mono found % ---- Iteration 8 (21 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_ln__less__zero: % WARNING: TreeLimitedRun lost 0.11s, total lost is 3.40s % fact_ln__gt__zero__imp__gt__one: % WARNING: TreeLimitedRun lost 0.20s, total lost is 3.60s % fact_divide__neg__neg: % CSA axiom fact_divide__neg__neg found % Looking for CSA axiom ... fact_zero__less__divide__iff: % WARNING: TreeLimitedRun lost 0.19s, total lost is 3.79s % CSA axiom fact_zero__less__divide__iff found % Looking for CSA axiom ... fact_divide__less__0__iff: % CSA axiom fact_divide__less__0__iff found % ---- Iteration 9 (24 axioms selected) % Looking for TBU SAT ... % WARNING: TreeLimitedRun lost 0.03s, total lost is 3.82s % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_ln__less__zero: % WARNING: TreeLimitedRun lost 0.20s, total lost is 4.02s % fact_ln__gt__zero__imp__gt__one: % WARNING: TreeLimitedRun lost 0.02s, total lost is 4.04s % fact_zero__less__one: % CSA axiom fact_zero__less__one found % Looking for CSA axiom ... fact_not__one__less__zero: % CSA axiom fact_not__one__less__zero found % Looking for CSA axiom ... fact_nonzero__norm__divide: % WARNING: TreeLimitedRun lost 0.19s, total lost is 4.23s % CSA axiom fact_nonzero__norm__divide found % ---- Iteration 10 (27 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_ln__less__zero:WARNING: TreeLimitedRun lost 0.10s, total lost is 4.33s % fact_ln__gt__zero__imp__gt__one: % fact_not__real__square__gt__zero: % WARNING: TreeLimitedRun lost 0.17s, total lost is 4.50s % CSA axiom fact_not__real__square__gt__zero found % Looking for CSA axiom ... fact_ln__less__cancel__iff: % CSA axiom fact_ln__less__cancel__iff found % Looking for CSA axiom ... fact_ln__less__self: % WARNING: TreeLimitedRun lost 0.20s, total lost is 4.70s % CSA axiom fact_ln__less__self found % ---- Iteration 11 (30 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % WARNING: TreeLimitedRun lost 0.23s, total lost is 4.93s % not found % Looking for CSA axiom ... fact_ln__less__zero: % fact_ln__gt__zero__imp__gt__one: % fact_zero__less__norm__iff: % CSA axiom fact_zero__less__norm__iff found % Looking for CSA axiom ... fact_r01: % WARNING: TreeLimitedRun lost 0.19s, total lost is 5.12s % CSA axiom fact_r01 found % Looking for CSA axiom ... fact_real__sgn__pos: % CSA axiom fact_real__sgn__pos found % ---- Iteration 12 (33 axioms selected) % Looking for TBU SAT ... % WARNING: TreeLimitedRun lost 0.19s, total lost is 5.31s % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_ln__less__zero: % fact_ln__gt__zero__imp__gt__one: % WARNING: TreeLimitedRun lost 0.06s, total lost is 5.37s % fact_real__mult__le__cancel__iff2: % CSA axiom fact_real__mult__le__cancel__iff2 found % Looking for CSA axiom ... fact_real__mult__le__cancel__iff1: % WARNING: TreeLimitedRun lost 0.04s, total lost is 5.41s % CSA axiom fact_real__mult__le__cancel__iff1 found % Looking for CSA axiom ... fact_divide_Opos__bounded: % CSA axiom fact_divide_Opos__bounded found % ---- Iteration 13 (36 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_ln__less__zero: % WARNING: TreeLimitedRun lost 0.04s, total lost is 5.45s % fact_ln__gt__zero__imp__gt__one: % WARNING: TreeLimitedRun lost 0.22s, total lost is 5.67s % fact_ln__eq__zero__iff: % WARNING: TreeLimitedRun lost 0.24s, total lost is 5.91s % CSA axiom fact_ln__eq__zero__iff found % Looking for CSA axiom ... fact_norm__mult__less: % CSA axiom fact_norm__mult__less found % Looking for CSA axiom ... fact_real__mult__1: % WARNING: TreeLimitedRun lost 0.19s, total lost is 6.10s % CSA axiom fact_real__mult__1 found % ---- Iteration 14 (39 axioms selected) % Looking for TBU SAT ... % WARNING: TreeLimitedRun lost 0.09s, total lost is 6.19s % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_ln__less__zero: % %------------------------------------------------------------------------------