%------------------------------------------------------------------------------ % File : SETHEO---3.3 % Problem : SWV774-1 : TPTP v5.0.0. Released v4.1.0. % Transfm : add_equality % Format : setheo % Command : setheo-wrapper %s % Computer : art04.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 : Fri Dec 24 23:48:57 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/SystemOnTPTP3132/SWV SWV774-1+eq_rstfp /tmp/SystemOnTPTP3132/SWV/SWV774-1+eq_rstfp % MUST DELETE /tmp/SystemOnTPTP3132/SWV/SWV774-1+eq_rstfp.hex % MUST DELETE /tmp/SystemOnTPTP3132/SWV/SWV774-1+eq_rstfp.log % MUST DELETE /tmp/SystemOnTPTP3132/SWV/SWV774-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 % 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 % 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_Event_Osko__Event__Xknows__imp__Says__Gets__Notes__initState__1__1 token too long % Warning : c_Event_Osko__Event__Xknows__imp__Says__Gets__Notes__initState__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_Event_Osko__Event__Xknows__imp__Says__Gets__Notes__initState__1__1 token too long % Warning : c_Event_Osko__Event__Xknows__imp__Says__Gets__Notes__initState__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_Event_Osko__Event__Xknows__imp__Says__Gets__Notes__initState__1__1 token too long % Warning : c_Event_Osko__Event__Xknows__imp__Says__Gets__Notes__initState__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 % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup 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 % 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 % 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 % 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_List_Osko__List__XCons__eq__append__conv__1__1 token too long % Warning : c_List_Osko__List__XCons__eq__append__conv__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_List_Osko__List__XCons__eq__append__conv__1__1 token too long % Warning : c_List_Osko__List__XCons__eq__append__conv__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_List_Osko__List__XCons__eq__append__conv__1__1 token too long % Warning : c_List_Osko__List__XCons__eq__append__conv__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_List_Osko__List__XCons__eq__append__conv__1__1 token too long % Warning : c_List_Osko__List__XCons__eq__append__conv__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_List_Osko__List__XCons__eq__append__conv__1__1 token too long % Warning : c_List_Osko__List__XCons__eq__append__conv__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_List_Osko__List__Xappend__eq__Cons__conv__1__1 token too long % Warning : c_List_Osko__List__Xappend__eq__Cons__conv__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_List_Osko__List__Xappend__eq__Cons__conv__1__1 token too long % Warning : c_List_Osko__List__Xappend__eq__Cons__conv__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_List_Osko__List__Xappend__eq__Cons__conv__1__1 token too long % Warning : c_List_Osko__List__Xappend__eq__Cons__conv__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_List_Osko__List__Xappend__eq__Cons__conv__1__1 token too long % Warning : c_List_Osko__List__Xappend__eq__Cons__conv__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_List_Osko__List__Xappend__eq__Cons__conv__1__1 token too long % Warning : c_List_Osko__List__Xappend__eq__Cons__conv__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_List_Osko__List__Xlinorder__class__Xinsort__is__Cons__1__1 token too long % Warning : c_List_Osko__List__Xlinorder__class__Xinsort__is__Cons__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_List_Osko__List__Xlinorder__class__Xinsort__is__Cons__1__1 token too long % Warning : c_List_Osko__List__Xlinorder__class__Xinsort__is__Cons__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_List_Osko__List__Xlinorder__class__Xinsort__is__Cons__1__1 token too long % Warning : c_List_Osko__List__Xlinorder__class__Xinsort__is__Cons__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_List_Osko__List__Xlinorder__class__Xinsort__is__Cons__1__1 token too long % Warning : c_List_Osko__List__Xlinorder__class__Xinsort__is__Cons__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_List_Osko__List__Xlinorder__class__Xinsort__is__Cons__1__1 token too long % Warning : c_List_Osko__List__Xlinorder__class__Xinsort__is__Cons__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_List_Osko__List__Xlinorder__class__Xsorted__Cons__1__1 token too long % Warning : c_List_Osko__List__Xlinorder__class__Xsorted__Cons__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_List_Osko__List__Xlinorder__class__Xsorted__Cons__1__1 token too long % Warning : c_List_Osko__List__Xlinorder__class__Xsorted__Cons__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_List_Osko__List__Xlinorder__class__Xsorted__Cons__1__1 token too long % Warning : c_List_Osko__List__Xlinorder__class__Xsorted__Cons__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 % 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_List_Osko__List__Xsplit__list__first__prop__iff__1__5 token too long % Warning : c_List_Osko__List__Xsplit__list__first__prop__iff__1__5 token too long % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Warning : c_List_Osko__List__Xsplit__list__first__prop__iff__1__5 token too long % Warning : c_List_Osko__List__Xsplit__list__first__prop__iff__1__5 token too long % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Warning : c_List_Osko__List__Xsplit__list__first__prop__iff__1__5 token too long % Warning : c_List_Osko__List__Xsplit__list__first__prop__iff__1__5 token too long % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Warning : c_List_Osko__List__Xsplit__list__last__prop__iff__1__5 token too long % Warning : c_List_Osko__List__Xsplit__list__last__prop__iff__1__5 token too long % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Warning : c_List_Osko__List__Xsplit__list__last__prop__iff__1__5 token too long % Warning : c_List_Osko__List__Xsplit__list__last__prop__iff__1__5 token too long % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Warning : c_List_Osko__List__Xsplit__list__last__prop__iff__1__5 token too long % Warning : c_List_Osko__List__Xsplit__list__last__prop__iff__1__5 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 % 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_Message_Osko__Message__Xanalz__insert__eq__I__1__1 token too long % Warning : c_Message_Osko__Message__Xanalz__insert__eq__I__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_Message_Osko__Message__Xanalz__insert__eq__I__1__1 token too long % Warning : c_Message_Osko__Message__Xanalz__insert__eq__I__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 % 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 % 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 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup 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 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup 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 : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup 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 : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup token too long % Warning : c_Lattices_Oupper__semilattice__class_Osup 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 % Warning : c_Lattices_Oupper__semilattice__class_Osup 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 % 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_List_Osko__List__Xlinorder__class__Xsorted__Cons__1__1 token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_List_Osko__List__Xlinorder__class__Xinsort__is__Cons__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 % 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 % 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_List_Osko__List__Xsplit__list__last__prop__iff__1__5 token too long % Warning : c_List_Osko__List__Xsplit__list__last__prop__iff__1__5 token too long % Warning : c_List_Osko__List__Xsplit__list__first__prop__iff__1__5 token too long % Warning : c_List_Osko__List__Xsplit__list__first__prop__iff__1__5 token too long % Warning : c_List_Osko__List__Xsplit__list__last__prop__iff__1__5 token too long % Warning : c_List_Osko__List__Xsplit__list__last__prop__iff__1__5 token too long % Warning : c_List_Osko__List__Xsplit__list__first__prop__iff__1__5 token too long % Warning : c_List_Osko__List__Xsplit__list__first__prop__iff__1__5 token too long % Warning : c_List_Osko__List__Xsplit__list__last__prop__iff__1__5 token too long % Warning : c_List_Osko__List__Xsplit__list__last__prop__iff__1__5 token too long % Warning : c_List_Osko__List__Xsplit__list__first__prop__iff__1__5 token too long % Warning : c_List_Osko__List__Xsplit__list__first__prop__iff__1__5 token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_List_Osko__List__Xlinorder__class__Xinsort__is__Cons__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 % 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_Message_Osko__Message__Xanalz__insert__eq__I__1__1 token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Message_Osko__Message__Xanalz__insert__eq__I__1__1 token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_List_Osko__List__Xlinorder__class__Xsorted__Cons__1__1 token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_Event_Osko__Event__Xknows__imp__Says__Gets__Notes__initState__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 % 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 % 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 % 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 % 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 % Non-fatal error : Unknown built-in in line 0 % Warning : c_List_Osko__List__XCons__eq__append__conv__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 : c_List_Osko__List__Xappend__eq__Cons__conv__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 % Non-fatal error : Unknown built-in in line 0 % Warning : c_List_Osko__List__Xsplit__list__first__prop__iff__1__5 token too long % Warning : c_List_Osko__List__Xsplit__list__first__prop__iff__1__5 token too long % Non-fatal error : Unknown built-in in line 0 % Warning : c_List_Osko__List__Xsplit__list__last__prop__iff__1__5 token too long % Warning : c_List_Osko__List__Xsplit__list__last__prop__iff__1__5 token too long % Warning : c_List_Osko__List__XCons__eq__append__conv__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 : c_List_Osko__List__Xappend__eq__Cons__conv__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 % 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_List_Osko__List__XCons__eq__append__conv__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 : c_List_Osko__List__Xappend__eq__Cons__conv__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 % Non-fatal error : Unknown built-in in line 0 % Non-fatal error : Unknown built-in in line 0 % Warning : c_List_Osko__List__Xappend__eq__Cons__conv__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 : c_List_Osko__List__XCons__eq__append__conv__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 % 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 % 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 % 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 % 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 % parsing: 585 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/SystemOnTPTP3132/SWV/SWV774-1+eq_rstfp % Parsing input-file. % inwasm error: inspect input file /tmp/SystemOnTPTP3132/SWV/SWV774-1+eq_rstfp.lop % Delete /tmp/SystemOnTPTP3132/SWV/SWV774-1+eq_rstfp.hex /tmp/SystemOnTPTP3132/SWV/SWV774-1+eq_rstfp.log /tmp/SystemOnTPTP3132/SWV/SWV774-1+eq_rstfp.tree % That's all folks % Killed 1 orphans % %------------------------------------------------------------------------------