%------------------------------------------------------------------------------ % File : SETHEO---3.3 % Problem : SWV864-1 : TPTP v5.0.0. Released v4.1.0. % Transfm : add_equality % Format : setheo % Command : setheo-wrapper %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 : Sat Dec 25 00:02:00 EST 2010 % Result : Unknown 0.00s % Output : None % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----NO SOLUTION OUTPUT BY SYSTEM %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % /tmp/SystemOnTPTP26015/SWV SWV864-1+eq_rstfp /tmp/SystemOnTPTP26015/SWV/SWV864-1+eq_rstfp % MUST DELETE /tmp/SystemOnTPTP26015/SWV/SWV864-1+eq_rstfp.hex % MUST DELETE /tmp/SystemOnTPTP26015/SWV/SWV864-1+eq_rstfp.log % MUST DELETE /tmp/SystemOnTPTP26015/SWV/SWV864-1+eq_rstfp.tree % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Warning : c_Natural_Osko__Natural__Xevalc__elim__cases__4__1 token too long % Warning : c_Natural_Osko__Natural__Xevalc__elim__cases__4__1 token too long % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Warning : c_Natural_Osko__Natural__Xevalc__elim__cases__4__1 token too long % Warning : c_Natural_Osko__Natural__Xevalc__elim__cases__4__1 token too long % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Warning : c_Natural_Osko__Natural__Xevalc__elim__cases__4__1 token too long % Warning : c_Natural_Osko__Natural__Xevalc__elim__cases__4__1 token too long % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Warning : c_Natural_Osko__Natural__Xevalc__elim__cases__4__1 token too long % Warning : c_Natural_Osko__Natural__Xevalc__elim__cases__4__1 token too long % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Warning : c_Natural_Osko__Natural__Xevalc__evaln__1__1 token too long % Warning : c_Natural_Osko__Natural__Xevalc__evaln__1__1 token too long % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Warning : c_Natural_Osko__Natural__Xevalc__evaln__1__1 token too long % Warning : c_Natural_Osko__Natural__Xevalc__evaln__1__1 token too long % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Warning : c_Natural_Osko__Natural__Xevalc__evaln__1__1 token too long % Warning : c_Natural_Osko__Natural__Xevalc__evaln__1__1 token too long % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Warning : c_Natural_Osko__Natural__Xevaln__elim__cases__4__1 token too long % Warning : c_Natural_Osko__Natural__Xevaln__elim__cases__4__1 token too long % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Warning : c_Natural_Osko__Natural__Xevaln__elim__cases__4__1 token too long % Warning : c_Natural_Osko__Natural__Xevaln__elim__cases__4__1 token too long % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Warning : c_Natural_Osko__Natural__Xevaln__elim__cases__4__1 token too long % Warning : c_Natural_Osko__Natural__Xevaln__elim__cases__4__1 token too long % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Warning : c_Natural_Osko__Natural__Xevaln__elim__cases__4__1 token too long % Warning : c_Natural_Osko__Natural__Xevaln__elim__cases__4__1 token too long % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Warning : c_Natural_Osko__Natural__Xevaln__elim__cases__4__1 token too long % Warning : c_Natural_Osko__Natural__Xevaln__elim__cases__4__1 token too long % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Warning : v_sko__Hoare__Mirabelle__Xsingle__stateE__1 token too long % Warning : v_sko__Hoare__Mirabelle__Xsingle__stateE__1 token too long % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Warning : c_Natural_Osko__Natural__Xevalc__elim__cases__4__1 token too long % Warning : c_Natural_Osko__Natural__Xevalc__elim__cases__4__1 token too long % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Warning : c_Natural_Osko__Natural__Xevaln__elim__cases__4__1 token too long % Warning : c_Natural_Osko__Natural__Xevaln__elim__cases__4__1 token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Natural_Osko__Natural__Xevalc__evaln__1__1 token too long % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Warning : v_sko__Hoare__Mirabelle__Xstate__not__singleton__def__raw__1 token too long % Warning : v_sko__Hoare__Mirabelle__Xstate__not__singleton__def__raw__2 token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Hoare__Mirabelle_Ostate__not__singleton token too long % Warning : c_Hoare__Mirabelle_Ostate__not__singleton token too long % Non-fatal error : Unknown built-in in line 0 % Warning : v_sko__Hoare__Mirabelle__Xsingle__stateE__1 token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Hoare__Mirabelle_Ostate__not__singleton token too long % Warning : v_sko__Hoare__Mirabelle__Xstate__not__singleton__def__1 token too long % Warning : v_sko__Hoare__Mirabelle__Xstate__not__singleton__def__2 token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Hoare__Mirabelle_Ostate__not__singleton token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Hoare__Mirabelle_Ostate__not__singleton token too long % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % parsing: 73 errors occurred % Error: Too many errors during parsing. Cannot continue. % inwasm V4.02b [wasm-less] Copyright TU Munich 1998 (03/30/98) % Command line: /home/graph/tptp/Systems/SETHEO---3.3/setheo.linux/inwasm -cons -foldup /tmp/SystemOnTPTP26015/SWV/SWV864-1+eq_rstfp % Parsing input-file. % inwasm error: inspect input file /tmp/SystemOnTPTP26015/SWV/SWV864-1+eq_rstfp.lop % Delete /tmp/SystemOnTPTP26015/SWV/SWV864-1+eq_rstfp.hex /tmp/SystemOnTPTP26015/SWV/SWV864-1+eq_rstfp.log /tmp/SystemOnTPTP26015/SWV/SWV864-1+eq_rstfp.tree % That's all folks % Killed 1 orphans % %------------------------------------------------------------------------------