%------------------------------------------------------------------------------ % File : SRASS---0.1 % Problem : SWW191+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 : art11.cs.miami.edu % Model : i686 i686 % CPU : Intel(R) Pentium(R) 4 CPU 3.00GHz @ 3000MHz % Memory : 2006MB % OS : Linux 2.6.31.5-127.fc12.i686.PAE % CPULimit : 300s % DateTime : Mon Mar 7 00:50:14 EST 2011 % Result : Timeout 272.14s % 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/SystemOnTPTP19287/SWW191+1.tptp % Adding relevance values % Extracting the conjecture % Sorting axioms by relevance % Looking for THM ... % WARNING: TreeLimitedRun lost 0.44s, total lost is 0.44s % not found % Adding ~C to TBU ... ~conj_0: % ---- Iteration 1 (0 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_real__le__refl:WARNING: TreeLimitedRun lost 0.07s, total lost is 0.51s % CSA axiom fact_real__le__refl found % Looking for CSA axiom ... fact_real__le__linear: % CSA axiom fact_real__le__linear found % Looking for CSA axiom ... fact_real__le__trans: % CSA axiom fact_real__le__trans found % ---- Iteration 2 (3 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_yL_I1_J: % CSA axiom fact_yL_I1_J found % Looking for CSA axiom ... fact_real__le__antisym: % CSA axiom fact_real__le__antisym found % Looking for CSA axiom ... fact__096L_A_060_061_AY_096: % CSA axiom fact__096L_A_060_061_AY_096 found % ---- Iteration 3 (6 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_real__add__left__mono: % WARNING: TreeLimitedRun lost 0.02s, total lost is 0.53s % CSA axiom fact_real__add__left__mono found % Looking for CSA axiom ... fact_less__eq__real__def: % CSA axiom fact_less__eq__real__def found % Looking for CSA axiom ... fact_real__less__def: % WARNING: TreeLimitedRun lost 0.01s, total lost is 0.54s % CSA axiom fact_real__less__def found % ---- Iteration 4 (9 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_ex: % CSA axiom fact_ex found % Looking for CSA axiom ... fact_le__trans: % WARNING: TreeLimitedRun lost 0.05s, total lost is 0.59s % CSA axiom fact_le__trans found % Looking for CSA axiom ... fact_nat__le__linear: % CSA axiom fact_nat__le__linear found % ---- Iteration 5 (12 axioms selected) % Looking for TBU SAT ... % WARNING: TreeLimitedRun lost 0.02s, total lost is 0.61s % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_le__refl: % arity_RealDef__Oreal__Orderings_Oorder: % CSA axiom arity_RealDef__Oreal__Orderings_Oorder found % Looking for CSA axiom ... fact_natceiling__mono: % CSA axiom fact_natceiling__mono found % Looking for CSA axiom ... fact_natfloor__mono: % CSA axiom fact_natfloor__mono found % ---- Iteration 6 (15 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_le__refl: % fact_real__of__nat__le__iff: % CSA axiom fact_real__of__nat__le__iff found % Looking for CSA axiom ... fact_real__le__eq__diff: % CSA axiom fact_real__le__eq__diff found % Looking for CSA axiom ... arity_RealDef__Oreal__Lattices_Osemilattice__sup: % WARNING: TreeLimitedRun lost 0.10s, total lost is 0.71s % CSA axiom arity_RealDef__Oreal__Lattices_Osemilattice__sup found % ---- Iteration 7 (18 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % WARNING: TreeLimitedRun lost 0.19s, total lost is 0.90s % not found % Looking for CSA axiom ... fact_le__refl: % WARNING: TreeLimitedRun lost 0.24s, total lost is 1.14s % arity_RealDef__Oreal__Lattices_Osemilattice__inf: % CSA axiom arity_RealDef__Oreal__Lattices_Osemilattice__inf found % Looking for CSA axiom ... arity_RealDef__Oreal__Orderings_Olinorder: % WARNING: TreeLimitedRun lost 0.27s, total lost is 1.41s % CSA axiom arity_RealDef__Oreal__Orderings_Olinorder found % Looking for CSA axiom ... arity_RealDef__Oreal__Orderings_Oord: % CSA axiom arity_RealDef__Oreal__Orderings_Oord found % ---- Iteration 8 (21 axioms selected) % Looking for TBU SAT ... % WARNING: TreeLimitedRun lost 0.17s, total lost is 1.58s % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_le__refl: % WARNING: TreeLimitedRun lost 0.16s, total lost is 1.74s % fact_nox: % WARNING: TreeLimitedRun lost 0.09s, total lost is 1.83s % CSA axiom fact_nox found % Looking for CSA axiom ... fact_L_H: % CSA axiom fact_L_H found % Looking for CSA axiom ... arity_RealDef__Oreal__Rings_Oidom: % CSA axiom arity_RealDef__Oreal__Rings_Oidom found % ---- Iteration 9 (24 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_le__refl: % arity_RealDef__Oreal__Groups_Ocancel__comm__monoid__add: % CSA axiom arity_RealDef__Oreal__Groups_Ocancel__comm__monoid__add found % Looking for CSA axiom ... arity_RealDef__Oreal__Rings_Ocomm__semiring__0: % CSA axiom arity_RealDef__Oreal__Rings_Ocomm__semiring__0 found % Looking for CSA axiom ... arity_RealDef__Oreal__Rings_Ocomm__ring__1: % WARNING: TreeLimitedRun lost 0.18s, total lost is 2.01s % CSA axiom arity_RealDef__Oreal__Rings_Ocomm__ring__1 found % ---- Iteration 10 (27 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % WARNING: TreeLimitedRun lost 0.31s, total lost is 2.32s % not found % Looking for CSA axiom ... fact_le__refl: % WARNING: TreeLimitedRun lost 0.27s, total lost is 2.59s % arity_RealDef__Oreal__Rings_Ocomm__ring: % CSA axiom arity_RealDef__Oreal__Rings_Ocomm__ring found % Looking for CSA axiom ... arity_RealDef__Oreal__Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct: % WARNING: TreeLimitedRun lost 0.14s, total lost is 2.73s % CSA axiom arity_RealDef__Oreal__Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct found % Looking for CSA axiom ... arity_RealDef__Oreal__Groups_Oordered__cancel__ab__semigroup__add: % CSA axiom arity_RealDef__Oreal__Groups_Oordered__cancel__ab__semigroup__add found % ---- Iteration 11 (30 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_le__refl: % arity_RealDef__Oreal__Groups_Oordered__ab__semigroup__add__imp__le:WARNING: TreeLimitedRun lost 0.02s, total lost is 2.75s % CSA axiom arity_RealDef__Oreal__Groups_Oordered__ab__semigroup__add__imp__le found % Looking for CSA axiom ... arity_RealDef__Oreal__Rings_Olinordered__comm__semiring__strict: % WARNING: TreeLimitedRun lost 0.19s, total lost is 2.94s % CSA axiom arity_RealDef__Oreal__Rings_Olinordered__comm__semiring__strict found % Looking for CSA axiom ... arity_RealDef__Oreal__Rings_Olinordered__semiring__1__strict: % CSA axiom arity_RealDef__Oreal__Rings_Olinordered__semiring__1__strict found % ---- Iteration 12 (33 axioms selected) % Looking for TBU SAT ... % WARNING: TreeLimitedRun lost 0.30s, total lost is 3.24s % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_le__refl: % WARNING: TreeLimitedRun lost 0.26s, total lost is 3.50s % arity_RealDef__Oreal__Rings_Olinordered__semiring__strict: % WARNING: TreeLimitedRun lost 0.15s, total lost is 3.65s % CSA axiom arity_RealDef__Oreal__Rings_Olinordered__semiring__strict found % Looking for CSA axiom ... arity_RealDef__Oreal__Groups_Oordered__ab__semigroup__add: % CSA axiom arity_RealDef__Oreal__Groups_Oordered__ab__semigroup__add found % Looking for CSA axiom ... arity_RealDef__Oreal__Groups_Oordered__comm__monoid__add: % CSA axiom arity_RealDef__Oreal__Groups_Oordered__comm__monoid__add found % ---- Iteration 13 (36 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_le__refl: % arity_RealDef__Oreal__Groups_Olinordered__ab__group__add: % WARNING: TreeLimitedRun lost 0.28s, total lost is 3.93s % CSA axiom arity_RealDef__Oreal__Groups_Olinordered__ab__group__add found % Looking for CSA axiom ... arity_RealDef__Oreal__Groups_Ocancel__ab__semigroup__add: % CSA axiom arity_RealDef__Oreal__Groups_Ocancel__ab__semigroup__add found % Looking for CSA axiom ... arity_RealDef__Oreal__Rings_Olinordered__ring__strict: % WARNING: TreeLimitedRun lost 0.20s, total lost is 4.13s % CSA axiom arity_RealDef__Oreal__Rings_Olinordered__ring__strict found % ---- Iteration 14 (39 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % WARNING: TreeLimitedRun lost 0.06s, total lost is 4.19s % not found % Looking for CSA axiom ... fact_le__refl: % WARNING: TreeLimitedRun lost 0.01s, total lost is 4.20s % arity_RealDef__Oreal__Rings_Oring__no__zero__divisors: % CSA axiom arity_RealDef__Oreal__Rings_Oring__no__zero__divisors found % Looking for CSA axiom ... arity_RealDef__Oreal__Groups_Oordered__ab__group__add: % CSA axiom arity_RealDef__Oreal__Groups_Oordered__ab__group__add found % Looking for CSA axiom ... arity_RealDef__Oreal__Groups_Ocancel__semigroup__add: % CSA axiom arity_RealDef__Oreal__Groups_Ocancel__semigroup__add found % ---- Iteration 15 (42 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % WARNING: TreeLimitedRun lost 0.25s, total lost is 4.45s % not found % Looking for CSA axiom ... fact_le__refl: % WARNING: TreeLimitedRun lost 0.31s, total lost is 4.76s % arity_RealDef__Oreal__Rings_Olinordered__semidom: % CSA axiom arity_RealDef__Oreal__Rings_Olinordered__semidom found % Looking for CSA axiom ... arity_RealDef__Oreal__Orderings_Odense__linorder: % WARNING: TreeLimitedRun lost 0.11s, total lost is 4.87s % CSA axiom arity_RealDef__Oreal__Orderings_Odense__linorder found % Looking for CSA axiom ... arity_RealDef__Oreal__Lattices_Odistrib__lattice: % CSA axiom arity_RealDef__Oreal__Lattices_Odistrib__lattice found % ---- Iteration 16 (45 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_le__refl: % arity_RealDef__Oreal__Groups_Oab__semigroup__mult:WARNING: TreeLimitedRun lost 0.01s, total lost is 4.88s % CSA axiom arity_RealDef__Oreal__Groups_Oab__semigroup__mult found % Looking for CSA axiom ... arity_RealDef__Oreal__Groups_Ocomm__monoid__mult: % WARNING: TreeLimitedRun lost 0.28s, total lost is 5.16s % CSA axiom arity_RealDef__Oreal__Groups_Ocomm__monoid__mult found % Looking for CSA axiom ... arity_RealDef__Oreal__Groups_Oab__semigroup__add: % CSA axiom arity_RealDef__Oreal__Groups_Oab__semigroup__add found % ---- Iteration 17 (48 axioms selected) % Looking for TBU SAT ... % WARNING: TreeLimitedRun lost 0.18s, total lost is 5.34s % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_le__refl: % WARNING: TreeLimitedRun lost 0.16s, total lost is 5.50s % arity_RealDef__Oreal__Rings_Ono__zero__divisors: % CSA axiom arity_RealDef__Oreal__Rings_Ono__zero__divisors found % Looking for CSA axiom ... arity_RealDef__Oreal__Groups_Ocomm__monoid__add: % CSA axiom arity_RealDef__Oreal__Groups_Ocomm__monoid__add found % Looking for CSA axiom ... arity_RealDef__Oreal__Rings_Olinordered__idom: % CSA axiom arity_RealDef__Oreal__Rings_Olinordered__idom found % ---- Iteration 18 (51 axioms selected) % Looking for TBU SAT ... % WARNING: TreeLimitedRun lost 0.15s, total lost is 5.65s % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_le__refl: % WARNING: TreeLimitedRun lost 0.23s, total lost is 5.88s % arity_RealDef__Oreal__Rings_Ocomm__semiring__1: % WARNING: TreeLimitedRun lost 0.25s, total lost is 6.13s % CSA axiom arity_RealDef__Oreal__Rings_Ocomm__semiring__1 found % Looking for CSA axiom ... arity_RealDef__Oreal__Rings_Ocomm__semiring: % CSA axiom arity_RealDef__Oreal__Rings_Ocomm__semiring found % Looking for CSA axiom ... arity_RealDef__Oreal__Groups_Oab__group__add: % WARNING: TreeLimitedRun lost 0.08s, total lost is 6.21s % CSA axiom arity_RealDef__Oreal__Groups_Oab__group__add found % ---- Iteration 19 (54 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_le__refl: % arity_RealDef__Oreal__Rings_Ozero__neq__one: % WARNING: TreeLimitedRun lost 0.15s, total lost is 6.36s % CSA axiom arity_RealDef__Oreal__Rings_Ozero__neq__one found % Looking for CSA axiom ... arity_RealDef__Oreal__Orderings_Opreorder: % CSA axiom arity_RealDef__Oreal__Orderings_Opreorder found % Looking for CSA axiom ... arity_RealDef__Oreal__Groups_Omonoid__mult: % WARNING: TreeLimitedRun lost 0.29s, total lost is 6.65s % CSA axiom arity_RealDef__Oreal__Groups_Omonoid__mult found % ---- Iteration 20 (57 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % WARNING: TreeLimitedRun lost 0.09s, total lost is 6.74s % not found % Looking for CSA axiom ... fact_le__refl: % arity_RealDef__Oreal__Groups_Omonoid__add: % CSA axiom arity_RealDef__Oreal__Groups_Omonoid__add found % Looking for CSA axiom ... arity_RealDef__Oreal__Rings_Osemiring__1: % CSA axiom arity_RealDef__Oreal__Rings_Osemiring__1 found % Looking for CSA axiom ... arity_RealDef__Oreal__Lattices_Olattice: % %------------------------------------------------------------------------------