%------------------------------------------------------------------------------ % File : SRASS---0.1 % Problem : SWW203+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 01:00:26 EST 2011 % Result : Timeout 300.02s % 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/SystemOnTPTP32156/SWW203+1.tptp % Adding relevance values % Extracting the conjecture % Sorting axioms by relevance % Looking for THM ... % WARNING: TreeLimitedRun lost 0.68s, total lost is 0.68s % 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__sqrt__ge__abs1: % CSA axiom fact_real__sqrt__ge__abs1 found % Looking for CSA axiom ... fact_real__sqrt__ge__abs2: % CSA axiom fact_real__sqrt__ge__abs2 found % Looking for CSA axiom ... fact_real__sqrt__sum__squares__ge1: % CSA axiom fact_real__sqrt__sum__squares__ge1 found % ---- Iteration 2 (3 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_real__sqrt__sum__squares__ge2: % CSA axiom fact_real__sqrt__sum__squares__ge2 found % Looking for CSA axiom ... fact_real__sqrt__sum__squares__triangle__ineq: % WARNING: TreeLimitedRun lost 0.02s, total lost is 0.70s % CSA axiom fact_real__sqrt__sum__squares__triangle__ineq found % Looking for CSA axiom ... fact_real__sqrt__le__mono: % CSA axiom fact_real__sqrt__le__mono found % ---- Iteration 3 (6 axioms selected) % Looking for TBU SAT ... % WARNING: TreeLimitedRun lost 0.29s, total lost is 0.99s % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_real__sqrt__le__iff: % WARNING: TreeLimitedRun lost 0.28s, total lost is 1.27s % CSA axiom fact_real__sqrt__le__iff found % Looking for CSA axiom ... fact_real__le__refl: % CSA axiom fact_real__le__refl found % Looking for CSA axiom ... fact_real__le__linear: % WARNING: TreeLimitedRun lost 0.15s, total lost is 1.42s % CSA axiom fact_real__le__linear found % ---- Iteration 4 (9 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % WARNING: TreeLimitedRun lost 0.02s, total lost is 1.44s % not found % Looking for CSA axiom ... fact_real__le__trans: % CSA axiom fact_real__le__trans found % Looking for CSA axiom ... fact_real__add__left__mono: % CSA axiom fact_real__add__left__mono found % Looking for CSA axiom ... fact_add__leE: % WARNING: TreeLimitedRun lost 0.07s, total lost is 1.51s % CSA axiom fact_add__leE found % ---- Iteration 5 (12 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % WARNING: TreeLimitedRun lost 0.28s, total lost is 1.79s % not found % Looking for CSA axiom ... fact_add__leD1: % WARNING: TreeLimitedRun lost 0.23s, total lost is 2.02s % fact_add__leD2: % fact_le__diff__iff: % CSA axiom fact_le__diff__iff found % Looking for CSA axiom ... fact_add__le__mono: % CSA axiom fact_add__le__mono found % Looking for CSA axiom ... fact_le__trans: % WARNING: TreeLimitedRun lost 0.30s, total lost is 2.32s % CSA axiom fact_le__trans found % ---- Iteration 6 (15 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_add__leD1: % fact_add__leD2: % WARNING: TreeLimitedRun lost 0.19s, total lost is 2.51s % fact_le__diff__conv2: % WARNING: TreeLimitedRun lost 0.21s, total lost is 2.72s % CSA axiom fact_le__diff__conv2 found % Looking for CSA axiom ... fact_diff__le__mono: % CSA axiom fact_diff__le__mono found % Looking for CSA axiom ... fact_diff__le__mono2: % CSA axiom fact_diff__le__mono2 found % ---- Iteration 7 (18 axioms selected) % Looking for TBU SAT ... % WARNING: TreeLimitedRun lost 0.18s, total lost is 2.90s % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_add__leD1: % WARNING: TreeLimitedRun lost 0.29s, total lost is 3.19s % fact_add__leD2: % WARNING: TreeLimitedRun lost 0.04s, total lost is 3.23s % fact_add__le__mono1:WARNING: TreeLimitedRun lost 0.04s, total lost is 3.27s % CSA axiom fact_add__le__mono1 found % Looking for CSA axiom ... fact_le__add__diff: % WARNING: TreeLimitedRun lost 0.28s, total lost is 3.55s % CSA axiom fact_le__add__diff found % Looking for CSA axiom ... fact_trans__le__add2: % CSA axiom fact_trans__le__add2 found % ---- Iteration 8 (21 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_add__leD1:WARNING: TreeLimitedRun lost 0.14s, total lost is 3.69s % WARNING: TreeLimitedRun lost 0.16s, total lost is 3.85s % fact_add__leD2: % fact_trans__le__add1: % WARNING: TreeLimitedRun lost 0.22s, total lost is 4.07s % fact_nat__add__left__cancel__le: % WARNING: TreeLimitedRun lost 0.17s, total lost is 4.24s % CSA axiom fact_nat__add__left__cancel__le found % Looking for CSA axiom ... fact_le__diff__conv: % CSA axiom fact_le__diff__conv found % Looking for CSA axiom ... fact_nat__le__linear: % CSA axiom fact_nat__le__linear found % ---- Iteration 9 (24 axioms selected) % Looking for TBU SAT ... % WARNING: TreeLimitedRun lost 0.26s, total lost is 4.50s % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_add__leD1: % WARNING: TreeLimitedRun lost 0.32s, total lost is 4.82s % fact_add__leD2: % WARNING: TreeLimitedRun lost 0.14s, total lost is 4.96s % fact_trans__le__add1: % WARNING: TreeLimitedRun lost 0.09s, total lost is 5.05s % fact_diff__le__self: % WARNING: TreeLimitedRun lost 0.11s, total lost is 5.16s % fact_le__add1: % WARNING: TreeLimitedRun lost 0.22s, total lost is 5.38s % fact_le__add2: % fact_le__refl: % fact__096sqrt_A_I_IRe_Ax_A_N_ARe_Ay_A_L_A0_J_A_094_A2_A_L_A_I0_A_L_A_IIm_Ax_A_N_AIm_Ay_J_J_A_094_A2_J_060_061_Asqrt_A_I_IRe_Ax_A_N_ARe_Ay_J_A_094_A2_A_L_A0_A_094_A2_J_A_L_Asqrt_A_I0_A_094_A2_A_L_A_IIm_Ax_A_N_AIm_Ay_J_A_094_A2_J_096:Opening file: File name too long % Deleting file/directory: File name too long % Opening file: File name too long % Deleting file/directory: File name too long % ERROR: Could not open file /tmp/fact_nat__le__linear.CSA.fact__096sqrt_A_I_IRe_Ax_A_N_ARe_Ay_A_L_A0_J_A_094_A2_A_L_A_I0_A_L_A_IIm_Ax_A_N_AIm_Ay_J_J_A_094_A2_J_060_061_Asqrt_A_I_IRe_Ax_A_N_ARe_Ay_J_A_094_A2_A_L_A0_A_094_A2_J_A_L_Asqrt_A_I0_A_094_A2_A_L_A_IIm_Ax_A_N_AIm_Ay_J_A_094_A2_J_096.p in w mode % ERROR: Could not delete /tmp/fact_nat__le__linear.CSA.fact__096sqrt_A_I_IRe_Ax_A_N_ARe_Ay_A_L_A0_J_A_094_A2_A_L_A_I0_A_L_A_IIm_Ax_A_N_AIm_Ay_J_J_A_094_A2_J_060_061_Asqrt_A_I_IRe_Ax_A_N_ARe_Ay_J_A_094_A2_A_L_A0_A_094_A2_J_A_L_Asqrt_A_I0_A_094_A2_A_L_A_IIm_Ax_A_N_AIm_Ay_J_A_094_A2_J_096.p % ERROR: Could not open file /tmp/fact_nat__le__linear.CSA.fact__096sqrt_A_I_IRe_Ax_A_N_ARe_Ay_A_L_A0_J_A_094_A2_A_L_A_I0_A_L_A_IIm_Ax_A_N_AIm_Ay_J_J_A_094_A2_J_060_061_Asqrt_A_I_IRe_Ax_A_N_ARe_Ay_J_A_094_A2_A_L_A0_A_094_A2_J_A_L_Asqrt_A_I0_A_094_A2_A_L_A_IIm_Ax_A_N_AIm_Ay_J_A_094_A2_J_096.p in w mode % ERROR: Could not delete /tmp/fact_nat__le__linear.CSA.fact__096sqrt_A_I_IRe_Ax_A_N_ARe_Ay_A_L_A0_J_A_094_A2_A_L_A_I0_A_L_A_IIm_Ax_A_N_AIm_Ay_J_J_A_094_A2_J_060_061_Asqrt_A_I_IRe_Ax_A_N_ARe_Ay_J_A_094_A2_A_L_A0_A_094_A2_J_A_L_Asqrt_A_I0_A_094_A2_A_L_A_IIm_Ax_A_N_AIm_Ay_J_A_094_A2_J_096.p % fact_real__sqrt__abs: % WARNING: TreeLimitedRun lost 0.24s, total lost is 5.62s % CSA axiom fact_real__sqrt__abs found % Looking for CSA axiom ... fact_real__sqrt__sum__squares__ge__zero: % CSA axiom fact_real__sqrt__sum__squares__ge__zero found % Looking for CSA axiom ... fact_real__sqrt__two__ge__zero: % WARNING: TreeLimitedRun lost 0.09s, total lost is 5.71s % CSA axiom fact_real__sqrt__two__ge__zero found % ---- Iteration 10 (27 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_add__leD1: % WARNING: TreeLimitedRun lost 0.02s, total lost is 5.73s % fact_add__leD2: % WARNING: TreeLimitedRun lost 0.09s, total lost is 5.82s % fact_trans__le__add1: % WARNING: TreeLimitedRun lost 0.21s, total lost is 6.03s % fact_diff__le__self: % WARNING: TreeLimitedRun lost 0.26s, total lost is 6.29s % fact_le__add1: % WARNING: TreeLimitedRun lost 0.28s, total lost is 6.57s % fact_le__add2: % WARNING: TreeLimitedRun lost 0.19s, total lost is 6.76s % fact_le__refl: % WARNING: TreeLimitedRun lost 0.17s, total lost is 6.93s % fact__096sqrt_A_I_IRe_Ax_A_N_ARe_Ay_A_L_A0_J_A_094_A2_A_L_A_I0_A_L_A_IIm_Ax_A_N_AIm_Ay_J_J_A_094_A2_J_060_061_Asqrt_A_I_IRe_Ax_A_N_ARe_Ay_J_A_094_A2_A_L_A0_A_094_A2_J_A_L_Asqrt_A_I0_A_094_A2_A_L_A_IIm_Ax_A_N_AIm_Ay_J_A_094_A2_J_096:Opening file: File name too long % Deleting file/directory: File name too long % Opening file: File name too long % Deleting file/directory: File name too long % ERROR: Could not open file /tmp/fact_real__sqrt__two__ge__zero.CSA.fact__096sqrt_A_I_IRe_Ax_A_N_ARe_Ay_A_L_A0_J_A_094_A2_A_L_A_I0_A_L_A_IIm_Ax_A_N_AIm_Ay_J_J_A_094_A2_J_060_061_Asqrt_A_I_IRe_Ax_A_N_ARe_Ay_J_A_094_A2_A_L_A0_A_094_A2_J_A_L_Asqrt_A_I0_A_094_A2_A_L_A_IIm_Ax_A_N_AIm_Ay_J_A_094_A2_J_096.p in w mode % ERROR: Could not delete /tmp/fact_real__sqrt__two__ge__zero.CSA.fact__096sqrt_A_I_IRe_Ax_A_N_ARe_Ay_A_L_A0_J_A_094_A2_A_L_A_I0_A_L_A_IIm_Ax_A_N_AIm_Ay_J_J_A_094_A2_J_060_061_Asqrt_A_I_IRe_Ax_A_N_ARe_Ay_J_A_094_A2_A_L_A0_A_094_A2_J_A_L_Asqrt_A_I0_A_094_A2_A_L_A_IIm_Ax_A_N_AIm_Ay_J_A_094_A2_J_096.p % ERROR: Could not open file /tmp/fact_real__sqrt__two__ge__zero.CSA.fact__096sqrt_A_I_IRe_Ax_A_N_ARe_Ay_A_L_A0_J_A_094_A2_A_L_A_I0_A_L_A_IIm_Ax_A_N_AIm_Ay_J_J_A_094_A2_J_060_061_Asqrt_A_I_IRe_Ax_A_N_ARe_Ay_J_A_094_A2_A_L_A0_A_094_A2_J_A_L_Asqrt_A_I0_A_094_A2_A_L_A_IIm_Ax_A_N_AIm_Ay_J_A_094_A2_J_096.p in w mode % ERROR: Could not delete /tmp/fact_real__sqrt__two__ge__zero.CSA.fact__096sqrt_A_I_IRe_Ax_A_N_ARe_Ay_A_L_A0_J_A_094_A2_A_L_A_I0_A_L_A_IIm_Ax_A_N_AIm_Ay_J_J_A_094_A2_J_060_061_Asqrt_A_I_IRe_Ax_A_N_ARe_Ay_J_A_094_A2_A_L_A0_A_094_A2_J_A_L_Asqrt_A_I0_A_094_A2_A_L_A_IIm_Ax_A_N_AIm_Ay_J_A_094_A2_J_096.p % fact_Im_Odiff: % CSA axiom fact_Im_Odiff found % Looking for CSA axiom ... fact_Re_Odiff: % WARNING: TreeLimitedRun lost 0.32s, total lost is 7.25s % CSA axiom fact_Re_Odiff found % Looking for CSA axiom ... fact_Re_Oadd: % %------------------------------------------------------------------------------