%------------------------------------------------------------------------------ % File : SRASS---0.1 % Problem : SWW477+1 : TPTP v5.3.0. Released v5.3.0. % Transfm : none % Format : tptp % Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s % Computer : art03.cs.miami.edu % Model : i686 i686 % CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2800MHz % Memory : 2005MB % OS : Linux 2.6.32.26-175.fc12.i686.PAE % CPULimit : 300s % DateTime : Sun Dec 4 01:21:10 EST 2011 % Result : Timeout 300.77s % 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/SystemOnTPTP12800/SWW477+1.tptp % Adding relevance values % Extracting the conjecture % Sorting axioms by relevance % Looking for THM ... % not found % Adding ~C to TBU ... ~conj_0: % ---- Iteration 1 (0 axioms selected) % Looking for TBU SAT ... WARNING: TreeLimitedRun lost 59.70s, total lost is 59.70s % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... gsy_c_WellTypeRT_OWTrt: % CSA axiom gsy_c_WellTypeRT_OWTrt found % Looking for CSA axiom ... fact_6_WTrtFAccNT: % CSA axiom fact_6_WTrtFAccNT found % Looking for CSA axiom ... fact_0__096P_ME_Mh_A_092_060turnstile_062_Ae_A_058_ANT_096: % CSA axiom fact_0__096P_ME_Mh_A_092_060turnstile_062_Ae_A_058_ANT_096 found % ---- Iteration 2 (3 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_1__096_B_BT_O_AP_ME_Mh_A_092_060turnstile_062_Ae_A_058_AT_A_061_061_062_AEX: % CSA axiom fact_1__096_B_BT_O_AP_ME_Mh_A_092_060turnstile_062_Ae_A_058_AT_A_061_061_062_AEX found % Looking for CSA axiom ... fact_37_WTrt__hext__mono: % CSA axiom fact_37_WTrt__hext__mono found % Looking for CSA axiom ... fact_29_WTrtFAssNT: % CSA axiom fact_29_WTrtFAssNT found % ---- Iteration 3 (6 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... gsy_c_member_000tc__prod_Itc__prod_Itc__Expr__Oexp_Itc__List__Olist_Itc__String_: % CSA axiom gsy_c_member_000tc__prod_Itc__prod_Itc__Expr__Oexp_Itc__List__Olist_Itc__String_ found % Looking for CSA axiom ... gsy_c_hAPP_000tc__prod_Itc__fun_Itc__Nat__Onat_Mtc__Option__Ooption_Itc__prod_It: % CSA axiom gsy_c_hAPP_000tc__prod_Itc__fun_Itc__Nat__Onat_Mtc__Option__Ooption_Itc__prod_It found % Looking for CSA axiom ... gsy_c_member_000tc__prod_Itc__prod_Itc__fun_Itc__Nat__Onat_Mtc__Option__Ooption_: % CSA axiom gsy_c_member_000tc__prod_Itc__prod_Itc__fun_Itc__Nat__Onat_Mtc__Option__Ooption_ found % ---- Iteration 4 (9 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... gsy_c_member_000tc__prod_Itc__prod_Itc__prod_Itc__Expr__Oexp_Itc__List__Olist_It: % CSA axiom gsy_c_member_000tc__prod_Itc__prod_Itc__prod_Itc__Expr__Oexp_Itc__List__Olist_It found % Looking for CSA axiom ... fact_16_widen__refl: % CSA axiom fact_16_widen__refl found % Looking for CSA axiom ... fact_26_widen__trans: % CSA axiom fact_26_widen__trans found % ---- Iteration 5 (12 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_53_hext__refl: % CSA axiom fact_53_hext__refl found % Looking for CSA axiom ... fact_63_hext__trans: % CSA axiom fact_63_hext__trans found % Looking for CSA axiom ... gsy_c_hAPP_000tc__prod_Itc__Expr__Oexp_Itc__List__Olist_Itc__String__Ochar_J_J_M: % CSA axiom gsy_c_hAPP_000tc__prod_Itc__Expr__Oexp_Itc__List__Olist_Itc__String__Ochar_J_J_M found % ---- Iteration 6 (15 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... gsy_c_hAPP_000tc__prod_Itc__prod_Itc__Expr__Oexp_Itc__List__Olist_Itc__String__O: % CSA axiom gsy_c_hAPP_000tc__prod_Itc__prod_Itc__Expr__Oexp_Itc__List__Olist_Itc__String__O found % Looking for CSA axiom ... gsy_c_Conform_Ohconf_000tc__prod_Itc__List__Olist_Itc__List__Olist_Itc__String__: % CSA axiom gsy_c_Conform_Ohconf_000tc__prod_Itc__List__Olist_Itc__List__Olist_Itc__String__ found % Looking for CSA axiom ... gsy_c_Conform_Olconf_000tc__prod_Itc__List__Olist_Itc__List__Olist_Itc__String__: % CSA axiom gsy_c_Conform_Olconf_000tc__prod_Itc__List__Olist_Itc__List__Olist_Itc__String__ found % ---- Iteration 7 (18 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... gsy_c_Objects_Ohext: % CSA axiom gsy_c_Objects_Ohext found % Looking for CSA axiom ... gsy_c_TypeRel_Owiden_000tc__prod_Itc__List__Olist_Itc__List__Olist_Itc__String__: % CSA axiom gsy_c_TypeRel_Owiden_000tc__prod_Itc__List__Olist_Itc__List__Olist_Itc__String__ found % Looking for CSA axiom ... gsy_c_WellForm_Owf__prog_000tc__prod_Itc__List__Olist_Itc__List__Olist_Itc__Stri: % CSA axiom gsy_c_WellForm_Owf__prog_000tc__prod_Itc__List__Olist_Itc__List__Olist_Itc__Stri found % ---- Iteration 8 (21 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... gsy_c_hAPP_000tc__fun_Itc__List__Olist_Itc__String__Ochar_J_Mtc__Option__Ooption: % CSA axiom gsy_c_hAPP_000tc__fun_Itc__List__Olist_Itc__String__Ochar_J_Mtc__Option__Ooption found % Looking for CSA axiom ... gsy_c_hAPP_000tc__prod_Itc__prod_Itc__fun_Itc__Nat__Onat_Mtc__Option__Ooption_It: % CSA axiom gsy_c_hAPP_000tc__prod_Itc__prod_Itc__fun_Itc__Nat__Onat_Mtc__Option__Ooption_It found % Looking for CSA axiom ... gsy_c_hAPP_000tc__prod_Itc__prod_Itc__prod_Itc__Expr__Oexp_Itc__List__Olist_Itc_: % CSA axiom gsy_c_hAPP_000tc__prod_Itc__prod_Itc__prod_Itc__Expr__Oexp_Itc__List__Olist_Itc_ found % ---- Iteration 9 (24 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... gsy_c_member_000tc__prod_Itc__Expr__Oexp_Itc__List__Olist_Itc__String__Ochar_J_J: % CSA axiom gsy_c_member_000tc__prod_Itc__Expr__Oexp_Itc__List__Olist_Itc__String__Ochar_J_J found % Looking for CSA axiom ... gsy_c_member_000tc__prod_Itc__fun_Itc__Nat__Onat_Mtc__Option__Ooption_Itc__prod_: % CSA axiom gsy_c_member_000tc__prod_Itc__fun_Itc__Nat__Onat_Mtc__Option__Ooption_Itc__prod_ found % Looking for CSA axiom ... gsy_c_member_000tc__prod_Itc__prod_Itc__prod_Itc__fun_Itc__Nat__Onat_Mtc__Option: % CSA axiom gsy_c_member_000tc__prod_Itc__prod_Itc__prod_Itc__fun_Itc__Nat__Onat_Mtc__Option found % ---- Iteration 10 (27 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... gsy_c_member_000tc__prod_Itc__prod_Itc__prod_Itc__prod_Itc__Expr__Oexp_Itc__List: % CSA axiom gsy_c_member_000tc__prod_Itc__prod_Itc__prod_Itc__prod_Itc__Expr__Oexp_Itc__List found % Looking for CSA axiom ... fact_2_assms: % CSA axiom fact_2_assms found % Looking for CSA axiom ... fact_11_ty_Osimps_I13_J: % CSA axiom fact_11_ty_Osimps_I13_J found % ---- Iteration 11 (30 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_12_ty_Osimps_I12_J: % fact_22_ty_Osimps_I7_J: % CSA axiom fact_22_ty_Osimps_I7_J found % Looking for CSA axiom ... fact_23_ty_Osimps_I6_J: % CSA axiom fact_23_ty_Osimps_I6_J found % Looking for CSA axiom ... fact_4_conf: % CSA axiom fact_4_conf found % ---- Iteration 12 (33 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_12_ty_Osimps_I12_J: % fact_10_FAssRed1_I3_J: % fact_3_IH: % CSA axiom fact_3_IH found % Looking for CSA axiom ... fact_7_FAssRed1_I2_J: % CSA axiom fact_7_FAssRed1_I2_J found % Looking for CSA axiom ... fact_40_split__paired__All: % CSA axiom fact_40_split__paired__All found % ---- Iteration 13 (36 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_12_ty_Osimps_I12_J: % fact_10_FAssRed1_I3_J: % fact_83_split__paired__Ex: % CSA axiom fact_83_split__paired__Ex found % Looking for CSA axiom ... fact_15_void: % CSA axiom fact_15_void found % Looking for CSA axiom ... fact_24_ty_Osimps_I3_J: % CSA axiom fact_24_ty_Osimps_I3_J found % ---- Iteration 14 (39 axioms selected) % Looking for TBU SAT ... % yes % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_12_ty_Osimps_I12_J: % fact_10_FAssRed1_I3_J: % fact_25_ty_Osimps_I2_J: % fact_27_exp_Osimps_I8_J: % CSA axiom fact_27_exp_Osimps_I8_J found % Looking for CSA axiom ... fact_28_exp_Osimps_I7_J: % CSA axiom fact_28_exp_Osimps_I7_J found % Looking for CSA axiom ... fact_54_lconf__hext: % CSA axiom fact_54_lconf__hext found % ---- Iteration 15 (42 axioms selected) % Looking for TBU SAT ... % no % Looking for TBU UNS ... % no % Looking for TBU model ... % not found % Looking for CSA axiom ... fact_12_ty_Osimps_I12_J: % fact_10_FAssRed1_I3_J: % fact_25_ty_Osimps_I2_J: % fact_5_wt: % fact_9_FAssRed1_I4_J: % fact_41_split__paired__All: % fact_42_split__paired__All: % fact_46_Pair__eq: % fact_51_Pair__inject: % %------------------------------------------------------------------------------