%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : SWW307+1 : TPTP v9.2.1. Released v5.2.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n015.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Thu May 7 07:38:09 PM UTC 2026 % Result : Unknown 1.96s 1.08s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW307+1 : TPTP v9.2.1. Released v5.2.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.17/0.34 % Computer : n015.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Thu May 7 13:34:48 EDT 2026 % 0.17/0.34 % CPUTime : % 0.17/0.34 SPASS-SCL-FOL version: % 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 1.96/1.02 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 1.96/1.02 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 1.96/1.02 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 1.96/1.02 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 1.96/1.02 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 1.96/1.02 Execution resolution_1 ended with status: gaveup % 1.96/1.02 Execution resolution_3 ended with status: gaveup % 1.96/1.02 Execution lmodel_grow ended with status: gaveup % 1.96/1.02 Execution resolution_2 ended with status: gaveup % 1.96/1.02 Execution normal ended with status: gaveup % 1.96/1.02 No successful execution. % 1.96/1.02 % 1.96/1.02 Input Clauses: % 1.96/1.07 % 1.96/1.07 Predicates: = c_Hoare__Mirabelle_Ohoare__derivs class_Orderings_Obot hBOOL class_Groups_Ominus c_Nitpick_Ofold__graph_H c_Fun_Oinj__on c_Finite__Set_Ofun__left__comm__idem class_Groups_Oab__group__add class_Orderings_Opreorder class_Orderings_Olinorder class_Orderings_Oord class_Orderings_Oorder class_Orderings_Otop class_Groups_Oordered__ab__group__add c_Fun_Obij__betw class_Groups_Ouminus class_Groups_Ogroup__add class_Lattices_Oboolean__algebra class_Groups_Oab__semigroup__mult c_Partial__Function_Omk__less c_Finite__Set_Ofolding__one class_Lattices_Oab__semigroup__idem__mult class_Rings_Oring class_Rings_Oidom class_Finite__Set_Ofinite class_Rings_Olinordered__idom c_Finite__Set_Ofolding c_Finite__Set_Ofolding__image__simple c_Finite__Set_Ofolding__image c_Finite__Set_Ofolding__idem c_Finite__Set_Ofolding__one__idem class_Groups_Oone class_Groups_Omonoid__mult class_Groups_Ocomm__monoid__mult class_Rings_Olinordered__semidom class_Rings_Oring__1__no__zero__divisors class_Rings_Ocomm__ring__1 class_Rings_Ocomm__semiring__1 class_Groups_Ocancel__semigroup__add class_Groups_Ocancel__ab__semigroup__add class_Groups_Oab__semigroup__add class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct class_Groups_Oordered__ab__semigroup__add__imp__le class_Groups_Oordered__ab__semigroup__add class_Groups_Oordered__cancel__ab__semigroup__add class_Rings_Ocomm__semiring class_Rings_Osemiring class_Rings_Oordered__ring class_Rings_Olinordered__semiring__1__strict c_Finite__Set_Ofolding__image__simple__idem class_Groups_Ozero class_Groups_Ocomm__monoid__add class_Groups_Omonoid__add class_Groups_Olinordered__ab__group__add class_Rings_Omult__zero class_Rings_Oring__no__zero__divisors class_Rings_Ono__zero__divisors class_Rings_Ozero__neq__one class_Groups_Oordered__comm__monoid__add class_Rings_Olinordered__ring class_Rings_Olinordered__ring__strict class_Rings_Oordered__cancel__semiring class_Rings_Oordered__semiring class_Rings_Oordered__comm__semiring class_Rings_Olinordered__comm__semiring__strict class_Rings_Olinordered__semiring__strict class_Rings_Olinordered__semiring class_Rings_Olinordered__semiring__1 class_Groups_Osgn__if class_Int_Oring__char__0 class_Rings_Oring__1 class_Int_Onumber class_Int_Onumber__ring c_Finite__Set_Ofun__left__comm c_Int_Oiszero class_Rings_Osemiring__1 class_Nat_Osemiring__char__0 class_Power_Opower class_Rings_Osemiring__0 c_Nat__Transfer_Otransfer__morphism class_Divides_Osemiring__div class_Divides_Oring__div c_Nat__Transfer_Onat__set c_Nat__Transfer_Ois__nat c_Big__Operators_Osemilattice__big c_Big__Operators_Ocomm__monoid__big class_Groups_Olinordered__ab__semigroup__add class_Fields_Ofield class_Rings_Odivision__ring class_Fields_Ofield__inverse__zero class_Rings_Odivision__ring__inverse__zero class_Fields_Olinordered__field__inverse__zero class_Fields_Olinordered__field c_Nitpick_Orefl_H c_FunDef_Oreduction__pair class_Lattices_Osemilattice__sup class_Lattices_Olattice class_Lattices_Obounded__lattice__top class_Lattices_Obounded__lattice__bot class_Lattices_Odistrib__lattice c_Wellfounded_Omax__extp c_Relation_Oirrefl class_Complete__Lattice_Ocomplete__lattice c_Equiv__Relations_Oequiv c_Equiv__Relations_Ocongruent2 c_Equiv__Relations_Ocongruent class_Lattices_Osemilattice__inf c_Equiv__Relations_Oequivp c_Typedef_Otype__definition class_Groups_Oordered__ab__group__add__abs class_Rings_Oordered__ring__abs class_Groups_Oabs__if c_Wellfounded_Owf class_Orderings_Owellorder c_Relation_Orefl__on c_Predicate_Oreflp c_Wellfounded_OwfP c_Wellfounded_Oacyclic c_Nitpick_Owf_H c_Nitpick_Ounknown c_Relation_Osingle__valued c_Relation_Ototal__on class_Rings_Oinverse c_Nitpick_Oless__frac c_Nitpick_Oless__eq__frac c_List_Olistrelp c_List_Onat__list class_Groups_Osemigroup__add c_List_Olist__all2 c_List_Olinorder__class_Osorted class_Enum_Oenum c_List_Olist__ex c_List_Olist__all c_List_Olist__ex1 c_FunDef_Ois__measure class_Nat_Osize class_Lazy__Sequence_Osmall__lazy c_List_Oall__interval__int c_Relation_Otrans c_Predicate_Otransp c_Predicate_Osymp c_Relation_Oantisym c_Relation_Osym c_Equiv__Relations_Opart__equivp c_List_Oall__interval__nat c_Rings_Odvd__class_Odvd class_Rings_Ocomm__ring class_Rings_Odvd class_Lattices_Obounded__lattice ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 ren12 ren13 ren14 ren15 ren16 ren17 ren18 ren19 ren20 ren21 ren22 ren23 ren24 ren25 ren26 ren27 ren28 ren29 ren30 ren31 ren32 ren33 ren34 ren35 ren36 ren37 ren38 ren39 ren40 ren41 ren42 ren43 ren44 ren45 ren46 ren47 ren48 ren49 ren50 ren51 ren52 ren53 ren54 ren55 ren56 ren57 ren58 ren59 ren60 ren61 ren62 ren63 ren64 ren65 ren66 ren67 ren68 ren69 ren70 ren71 ren72 ren73 ren74 ren75 ren76 ren77 ren78 ren79 ren80 ren81 ren82 ren83 ren84 ren85 ren86 ren87 ren88 ren89 ren90 ren91 ren92 ren93 ren94 ren95 ren96 ren97 ren98 ren99 ren100 ren101 ren102 ren103 ren104 ren105 ren106 ren107 ren108 ren109 ren110 ren111 ren112 ren113 ren114 ren115 ren116 ren117 ren118 ren119 ren120 ren121 ren122 ren123 ren124 ren125 ren126 ren127 ren128 ren129 ren130 ren131 ren132 ren133 ren134 ren135 ren136 ren137 ren138 ren139 ren140 ren141 ren142 ren143 ren144 ren145 ren146 ren147 ren148 ren149 ren150 ren151 ren152 ren153 ren154 ren155 ren156 ren157 ren158 ren159 ren160 ren161 ren162 ren163 ren164 ren165 ren166 ren167 ren168 ren169 ren170 ren171 ren172 ren173 ren174 ren175 ren176 ren177 ren178 ren179 ren180 ren181 ren182 ren183 ren184 ren185 ren186 ren187 ren188 ren189 ren190 ren191 ren192 ren193 ren194 ren195 ren196 ren197 ren198 ren199 ren200 ren201 ren202 ren203 ren204 ren205 ren206 ren207 ren208 ren209 ren210 ren211 ren212 ren213 ren214 ren215 ren216 ren217 ren218 ren219 ren220 ren221 ren222 ren223 ren224 ren225 ren226 ren227 ren228 ren229 ren230 ren231 ren232 ren233 ren234 ren235 ren236 ren237 ren238 ren239 ren240 ren241 ren242 ren243 ren244 ren245 ren246 ren247 ren248 ren249 ren250 ren251 ren252 ren253 ren254 ren255 ren256 ren257 ren258 ren259 ren260 ren261 ren262 ren263 ren264 ren265 ren266 ren267 ren268 ren269 ren270 ren271 ren272 ren273 ren274 ren275 ren276 ren277 ren278 ren279 ren280 ren281 ren282 ren283 ren284 ren285 ren286 ren287 ren288 ren289 ren290 ren291 ren292 ren293 ren294 ren295 ren296 ren297 ren298 ren299 ren300 ren301 ren302 ren303 ren304 ren305 ren306 ren307 ren308 ren309 ren310 ren311 ren312 ren313 ren314 ren315 ren316 ren317 ren318 ren319 ren320 ren321 ren322 ren323 ren324 ren325 ren326 ren327 ren328 ren329 ren330 ren331 ren332 ren333 ren334 ren335 ren336 ren337 ren338 ren339 ren340 ren341 ren342 ren343 ren344 ren345 ren346 ren347 ren348 ren349 ren350 ren351 ren352 ren353 ren354 ren355 ren356 ren357 ren358 ren359 ren360 ren361 ren362 ren363 ren364 ren365 ren366 ren367 ren368 ren369 ren370 ren371 ren372 ren373 ren374 ren375 ren376 ren377 ren378 ren379 ren380 ren381 ren382 ren383 ren384 ren385 ren386 ren387 ren388 ren389 ren390 ren391 ren392 ren393 ren394 ren395 ren396 ren397 ren398 ren399 ren400 ren401 ren402 ren403 ren404 ren405 ren406 ren407 ren408 ren409 ren410 ren411 ren412 ren413 ren414 ren415 ren416 ren417 ren418 ren419 ren420 ren421 ren422 ren423 ren424 ren425 ren426 ren427 ren428 ren429 ren430 ren431 ren432 ren433 ren434 ren435 ren436 ren437 ren438 ren439 ren440 ren441 ren442 ren443 ren444 ren445 ren446 ren447 ren448 ren449 ren450 ren451 ren452 ren453 ren454 ren455 ren456 ren457 ren458 ren459 ren460 ren461 ren462 ren463 ren464 ren465 ren466 ren467 ren468 ren469 ren470 ren471 ren472 ren473 ren474 ren475 ren476 ren477 ren478 ren479 ren480 ren481 ren482 ren483 ren484 ren485 ren486 ren487 ren488 ren489 ren490 ren491 ren492 ren493 ren494 ren495 ren496 ren497 ren498 ren499 ren500 ren501 ren502 ren503 ren504 ren505 ren506 ren507 ren508 ren509 ren510 ren511 ren512 ren513 ren514 ren515 ren516 ren517 ren518 ren519 ren520 ren521 ren522 ren523 ren524 ren525 ren526 ren527 ren528 ren529 ren530 ren531 ren532 ren533 ren534 ren535 ren536 ren537 ren538 ren539 ren540 ren541 ren542 ren543 ren544 ren545 ren546 ren547 ren548 ren549 ren550 ren551 ren552 ren553 ren554 ren555 ren556 ren557 ren558 ren559 ren560 ren561 ren562 ren563 ren564 ren565 ren566 ren567 ren568 ren569 ren570 ren571 ren572 ren573 ren574 ren575 ren576 ren577 ren578 ren579 ren580 ren581 ren582 ren583 ren584 ren585 ren586 ren587 ren588 ren589 ren590 ren591 ren592 ren593 ren594 ren595 ren596 ren597 ren598 ren599 ren600 ren601 ren602 ren603 ren604 ren605 ren606 ren607 ren608 ren609 ren610 ren611 ren612 ren613 ren614 ren615 ren616 ren617 ren618 ren619 ren620 ren621 ren622 ren623 ren624 ren625 ren626 ren627 ren628 ren629 ren630 ren631 ren632 ren633 ren634 ren635 ren636 ren637 ren638 ren639 ren640 ren641 ren642 ren643 ren644 ren645 ren646 ren647 ren648 ren649 ren650 ren651 ren652 ren653 ren654 ren655 ren656 ren657 ren658 ren659 ren660 ren661 ren662 ren663 ren664 ren665 ren666 ren667 ren668 ren669 ren670 ren671 ren672 ren673 ren674 ren675 ren676 ren677 ren678 ren679 ren680 ren681 ren682 ren683 ren684 ren685 ren686 ren687 ren688 ren689 ren690 ren691 ren692 ren693 ren694 ren695 ren696 ren697 ren698 ren699 ren700 ren701 ren702 ren703 ren704 ren705 ren706 ren707 ren708 ren709 ren710 ren711 ren712 ren713 ren714 ren715 ren716 ren717 ren718 ren719 ren720 ren721 ren722 ren723 ren724 ren725 ren726 ren727 ren728 ren729 ren730 ren731 ren732 ren733 ren734 ren735 ren736 ren737 ren738 ren739 ren740 ren741 ren742 ren743 ren744 ren745 ren746 ren747 ren748 ren749 ren750 ren751 ren752 ren753 ren754 ren755 ren756 ren757 ren758 ren759 ren760 ren761 ren762 ren763 ren764 ren765 ren766 ren767 ren768 ren769 ren770 ren771 ren772 ren773 ren774 ren775 ren776 ren777 ren778 ren779 ren780 ren781 ren782 ren783 ren784 ren785 ren786 ren787 ren788 ren789 ren790 ren791 ren792 ren793 ren794 ren795 ren796 ren797 ren798 ren799 ren800 ren801 ren802 ren803 ren804 ren805 ren806 ren807 ren808 ren809 ren810 ren811 ren812 ren813 ren814 ren815 ren816 ren817 ren818 ren819 ren820 ren821 ren822 ren823 ren824 ren825 ren826 ren827 ren828 ren829 ren830 ren831 ren832 ren833 ren834 ren835 ren836 ren837 ren838 ren839 ren840 ren841 ren842 ren843 ren844 ren845 ren846 ren847 ren848 ren849 ren850 ren851 ren852 ren853 ren854 ren855 ren856 ren857 ren858 ren859 ren860 ren861 ren862 ren863 ren864 ren865 ren866 ren867 ren868 ren869 ren870 ren871 ren872 ren873 ren874 ren875 ren876 ren877 ren878 ren879 ren880 ren881 ren882 ren883 ren884 ren885 ren886 ren887 ren888 ren889 ren890 ren891 ren892 ren893 ren894 ren895 ren896 ren897 ren898 ren899 ren900 ren901 ren902 ren903 ren904 ren905 ren906 ren907 ren908 ren909 ren910 ren911 ren912 ren913 ren914 ren915 ren916 ren917 ren918 ren919 ren920 ren921 ren922 ren923 ren924 ren925 ren926 ren927 ren928 ren929 ren930 ren931 ren932 ren933 ren934 ren935 ren936 ren937 ren938 ren939 ren940 ren941 ren942 ren943 ren944 ren945 ren946 ren947 ren948 ren949 ren950 ren951 ren952 ren953 ren954 ren955 ren956 ren957 ren958 ren959 ren960 ren961 ren962 ren963 ren964 ren965 ren966 ren967 ren968 ren969 ren970 ren971 ren972 ren973 ren974 ren975 ren976 ren977 ren978 ren979 ren980 ren981 ren982 ren983 ren984 ren985 ren986 ren987 ren988 ren989 ren990 ren991 ren992 ren993 ren994 ren995 ren996 ren997 ren998 ren999 ren1000 ren1001 ren1002 ren1003 ren1004 ren1005 ren1006 ren1007 ren1008 ren1009 ren1010 ren1011 ren1012 ren1013 ren1014 ren1015 ren1016 ren1017 ren1018 ren1019 ren1020 ren1021 ren1022 ren1023 ren1024 ren1025 ren1026 ren1027 ren1028 ren1029 ren1030 ren1031 ren1032 ren1033 ren1034 ren1035 ren1036 ren1037 % 1.96/1.07 Fol Constants: tc_HOL_Obool tc_Com_Ostate c_fequal c_Com_Ocom_OSKIP tc_Nat_Onat tc_Com_Ovname c_Natural_Oupdate c_fconj c_fFalse c_fimplies c_fNot c_fdisj c_fTrue tc_Product__Type_Ounit c_Nat_OSuc tc_Com_Ocom tc_Int_Oint c_Int_OPls c_Nat__Numeral_Oneg c_Int_Onat tc_Code__Numeral_Ocode__numeral c_Int_OMin c_Code__Numeral_Oint__of c_Nitpick_OFrac c_Nitpick_Oint__gcd c_Divides_OnegateSnd c_Divides_OnegDivAlg__rel c_Divides_OposDivAlg__rel c_Nitpick_Onorm__frac__rel c_FunDef_Opair__less c_FunDef_Opair__leq c_FunDef_Omax__strict c_FunDef_Omin__strict c_FunDef_Omin__weak c_FunDef_Omax__weak c_Wellfounded_Oless__than c_Int_Ointrel c_Int_ORep__Integ c_Int_OAbs__Integ c_Int_OInteg c_Nitpick_Onat__gcd__rel c_Wellfounded_Opred__nat c_List_Oupto__rel c_Code__Numeral_Oof__nat c_Code__Numeral_Onat__of c_Code__Numeral_Osubtract__code__numeral c_Lazy__Sequence_Osmall__lazy_H__rel tc_Code__Evaluation_Oterm v_C t_a v_G v_P v_c v_Q % 1.96/1.07 Fol Functions: hAPP tc_Hoare__Mirabelle_Otriple tc_fun c_Orderings_Obot__class_Obot c_Hoare__Mirabelle_Otriple_Otriple c_Set_Oinsert c_Hoare__Mirabelle_Otriple_Otriple__rec c_Hoare__Mirabelle_Otriple_Otriple__case c_COMBK c_COMBC c_Set_Othe__elem c_Com_Ocom_OSemi c_COMBB c_COMBS c_Com_Ocom_OAss c_HOL_OThe c_Set_OCollect c_Set_Oimage c_COMBI c_member c_Fun_Othe__inv__into c_Fun_Ooverride__on c_Set_Ovimage c_Groups_Ominus__class_Ominus c_Fun_Ofun__upd c_Orderings_Oord__class_Oless__eq c_Orderings_Otop__class_Otop c_Partial__Function_Oflat__lub c_Orderings_Oord__class_Oless c_Finite__Set_Ofold__graph c_If c_Groups_Ouminus__class_Ouminus c_Fun_Ocomp c_Finite__Set_Ofold1Set c_Groups_Otimes__class_Otimes c_Hilbert__Choice_Oinv__into c_Finite__Set_Ofinite tc_sum tc_Option_Ooption tc_prod c_Finite__Set_Ocard c_Finite__Set_Ofold1 c_Finite__Set_Ofold__image c_SetInterval_Oord_OgreaterThanAtMost c_SetInterval_Oord_OatLeastLessThan c_SetInterval_Oord_OgreaterThanLessThan c_SetInterval_Oord_OatLeastAtMost c_SetInterval_Oord_OgreaterThan c_SetInterval_Oord_OlessThan c_SetInterval_Oord_OatLeast c_SetInterval_Oord_OatMost c_Groups_Oone__class_Oone c_Groups_Oplus__class_Oplus c_Groups_Ozero__class_Ozero c_Nat_Onat_Onat__case c_Sum__Type_OPlus c_Hoare__Mirabelle_Otriple_Otriple__size c_Nat_Osize__class_Osize c_Com_Ocom_Ocom__size c_Int_Oring__1__class_OInts c_Groups_Osgn__class_Osgn c_Com_Ocom_OCond c_Int_Onumber__class_Onumber__of c_Com_Ocom_OLocal c_Finite__Set_Ofold c_Hoare__Mirabelle_Opeek__and c_Int_Opred c_Com_Ocom_OWhile c_Int_Osucc c_Nat_Osemiring__1__class_ONats c_Nat__Transfer_Otsub c_Int_OBit1 c_Nat_Osemiring__1__class_Oof__nat c_HOL_OLet c_Nat_Osemiring__1__class_Oof__nat__aux c_Power_Opower__class_Opower c_Int_Onat__aux c_Code__Numeral_Onat__of__aux c_Nat_Onat_Onat__rec c_Int_OBit0 c_Divides_Odiv__class_Omod c_Divides_Odiv__class_Odiv c_Power_Opower_Opower c_SMT_Oz3div c_SMT_Oz3mod c_Orderings_Oord__class_Omin c_Code__Numeral_Ocode__numeral_Ocode__numeral__size c_Orderings_Oord_Omax c_Orderings_Oord_Omin c_Code__Numeral_OSuc__code__numeral c_SetInterval_Oord__class_OgreaterThanLessThan c_Big__Operators_Olinorder__class_OMin c_Int_Oring__1__class_Oof__int c_Big__Operators_Olattice_OInf__fin c_Product__Type_Oprod_Oprod__case c_Divides_Odivmod__int c_Big__Operators_Ocomm__monoid__mult__class_Osetprod c_HOL_OEx c_Int_Oint__ge__less__than2 c_Int_Oint__ge__less__than c_Big__Operators_Olinorder__class_OMax c_Divides_Odivmod__int__rel c_Orderings_Oord__class_Omax c_Nitpick_Oprod c_Big__Operators_Olattice_OSup__fin c_Product__Type_OPair c_Rings_Oinverse__class_Odivide c_Divides_Oadjust c_Nitpick_Onorm__frac c_Divides_OnegDivAlg c_FunDef_Oin__rel c_Code__Numeral_Odiv__mod__code__numeral c_Divides_OposDivAlg c_Divides_Odivmod__nat c_Wellfounded_Oaccp c_Divides_Odivmod__nat__rel c_Nat_Onat_Onat__size c_Product__Type_Osnd c_Wellfounded_Omeasure c_Product__Type_Ofst c_Product__Type_Oprod_Oprod__size c_Wellfounded_Omlex__prod c_Wellfounded_Ofinite__psubset c_Product__Type_Oprod_Oprod__rec c_Wellfounded_Olex__prod c_Recdef_Osame__fst c_Wellfounded_Omin__ext c_Relation_Oinv__image c_Lattices_Osemilattice__sup__class_Osup c_FunDef_Orp__inv__image c_Wellfounded_Omax__ext c_Big__Operators_Olattice__class_OInf__fin c_Relation_OField c_SetInterval_Oord__class_OgreaterThanAtMost c_Big__Operators_Olattice__class_OSup__fin c_Complete__Lattice_Ocomplete__lattice__class_OSUPR c_Relation_OId__on c_Set_OPow c_SetInterval_Oord__class_OatLeastAtMost c_Predicate_OPowp c_SetInterval_Oord__class_OatLeastLessThan c_SetInterval_Oord__class_OatMost c_SetInterval_Oord__class_OgreaterThan c_SetInterval_Oord__class_OatLeast c_SetInterval_Oord__class_OlessThan c_Big__Operators_Ocomm__monoid__add__class_Osetsum c_Relation_OImage c_Equiv__Relations_Oquotient c_Lattices_Osemilattice__inf__class_Oinf c_Complete__Lattice_Ocomplete__lattice__class_OINFI c_Code__Numeral_Ocode__numeral_Ocode__numeral__case c_Complete__Lattice_OInf__class_OInf c_Product__Type_Oapsnd c_Divides_Opdivmod c_Groups_Oabs__class_Oabs c_Nitpick_Onat__gcd c_Nitpick_Oint__lcm c_Nitpick_Onat__lcm c_Product__Type_Oapfst c_Wellfounded_Oacc c_Relation_Orel__comp c_Predicate_Opred__comp c_Complete__Lattice_OSup__class_OSup tc_List_Olist c_List_Olenlex c_List_Olex c_List_Olexn c_Nitpick_Ozero__frac c_Nitpick_OAbs__Frac c_Nitpick_Oone__frac c_Nitpick_Onumber__of__frac c_Nitpick_Ofrac c_Relation_ORange c_Predicate_ORangeP c_Relation_ODomain c_Predicate_ODomainP c_Product__Type_OSigma c_Fun_Oid c_Product__Type_Omap__pair c_Set_OBall c_HOL_OAll c_Hilbert__Choice_OEps c_Product__Type_Oscomp c_Random_Oiterate c_Random_Olog c_Random_Ominus__shift c_Random_Oinc__shift c_Random_Orange c_Transitive__Closure_Otrancl c_Transitive__Closure_Ortrancl c_Relation_OId c_Relation_Oconverse c_Nat_Ocompow c_Nat_Ofunpow c_Nitpick_Oplus__frac c_Nitpick_Odenom c_Nitpick_Onum c_Nitpick_Otimes__frac c_Nitpick_Oof__frac c_Nitpick_Oinverse__frac c_Nitpick_Ouminus__frac c_Nitpick_ORep__Frac c_Product__Type_Ointernal__split c_HOL_Obool_Obool__size c_List_Osublist c_List_Olist_OCons c_List_Oset__Cons c_Random_Opick c_Random_Oselect__weight c_List_Olexord c_List_Olistrel1 c_List_Olist_Olist__size c_List_Olistrel c_List_Olists c_List_Onth c_List_Otake c_List_Oset c_List_Ozip c_List_Oupto c_List_Omonoid__add__class_Olistsum c_List_Olist__update c_List_Obutlast c_List_Odistinct c_Nitpick_Ocard_H c_List_Oremove1 c_List_Olist_ONil c_Random_Oselect c_List_Olistset c_List_Olist_Olist__case c_List_Olinorder__class_Osorted__list__of__set c_Lazy__Sequence_Oanamorph c_Option_Ooption_Ooption__case c_List_Oappend c_List_Orotate1 c_List_Odrop c_List_Ohd c_List_Otl c_List_Orotate c_List_Ofoldl c_List_Olinorder__class_Oinsort__key c_List_Olinorder__class_Oinsort__insert__key c_List_Olast c_List_Omap c_Nitpick_Osetsum_H c_New__DSequence_Opos__not__seq c_Lazy__Sequence_Ohb__not__seq c_List_Opartition c_List_Olistsp c_Enum_Oproduct c_Enum_Osublists c_Enum_On__lists c_Enum_Oenum__the c_List_Oremdups c_List_OremoveAll c_List_Oconcat c_List_Olinorder__class_Osort__key c_List_Otranspose c_List_Ofilter c_List_Otranspose__rel c_List_Ofoldr c_List_Oupt c_List_Orev c_List_OtakeWhile c_List_Oreturn__list c_List_Oembed__list c_List_OdropWhile c_List_Oinsert c_List_Omaps c_List_Omeasures c_Enum_Oenum__class_Oenum__ex c_New__Random__Sequence_Opos__not__random__dseq c_Enum_Oenum__class_Oenum__all c_New__DSequence_Oneg__decr__bind c_Lazy__Sequence_Ohit__bound tc_Lazy__Sequence_Olazy__sequence c_Lazy__Sequence_Ohb__bind c_New__Random__Sequence_Oneg__decr__bind c_New__DSequence_Oneg__bind c_New__Random__Sequence_Oneg__bind c_New__DSequence_Opos__decr__bind c_Lazy__Sequence_Oempty c_Lazy__Sequence_Obind c_New__Random__Sequence_Opos__decr__bind c_New__DSequence_Opos__empty c_New__Random__Sequence_Opos__empty c_New__DSequence_Opos__bind c_New__Random__Sequence_Opos__bind c_New__Random__Sequence_Oneg__map c_New__Random__Sequence_Oneg__single c_New__DSequence_Oneg__single c_New__Random__Sequence_Opos__map c_New__Random__Sequence_Opos__single c_Lazy__Sequence_Ohb__single c_New__DSequence_Opos__single c_Lazy__Sequence_Osingle c_List_Osplice c_Lazy__Sequence_Oproduct c_Predicate_Oconversep c_Lazy__Sequence_Osmall__lazy__class_Osmall__lazy c_Lazy__Sequence_Oappend c_List_Oreplicate c_New__DSequence_Opos__union c_New__Random__Sequence_Opos__union c_Lazy__Sequence_Osmall__lazy_H c_Lazy__Sequence_Olazy__sequence_OInsert c_Lazy__Sequence_Olazy__sequence_Olazy__sequence__size c_Lazy__Sequence_Oyield c_Lazy__Sequence_Olazy__sequence_Olazy__sequence__case c_Lazy__Sequence_Oyieldn c_List_Omember c_Nitpick_Opair__box_OPairBox c_Nitpick_Opair__box_Opair__box__size tc_Nitpick_Opair__box c_Nitpick_Opair__box_Opair__box__rec c_Nitpick_Opair__box_Opair__box__case c_FunDef_OTHE__default c_Lazy__Sequence_Olazy__sequence_OEmpty c_Code__Numeral_Ocode__numeral_Ocode__numeral__rec c_Random__Sequence_ORandom c_DSequence_Oempty c_DSequence_Ounion c_DSequence_Osingle c_Random__Sequence_Oempty c_Random__Sequence_Osingle c_Random__Sequence_Omap c_Random__Sequence_Obind c_Set_OBex c_Partial__Function_Ofun__lub c_Lazy__Sequence_Olazy__sequence_Olazy__sequence__rec c_Quickcheck_Obeyond c_Product__Type_Ocurry c_Quotient_ORespects c_Quotient_OBabs c_Com_Ovname_OLoc c_Natural_Ogetlocs c_Com_Ovname_Ovname__size c_Com_Ovname_Ovname__case c_Com_Ovname_OGlb c_Com_Ovname_Ovname__rec c_Lazy__Sequence_Oflat c_Lazy__Sequence_Omap c_New__DSequence_Opos__map skf1 skf2 skf3 skf4 skf5 skf6 skf7 skf8 skf9 skf10 skf11 skf12 skf13 skf14 skf15 skf16 skf17 skf18 skf19 skf20 skf21 skf22 skf23 skf24 skf25 skf26 skf27 skf28 skf29 skf30 skf31 skf32 skf33 skf34 skf35 skf36 skf37 skf38 skf39 skf40 skf41 skf42 skf43 skf44 skf45 skf46 skf47 skf48 skf49 skf50 skf51 skf52 skf53 skf54 skf55 skf56 skf57 skf58 skf59 skf60 skf61 skf62 skf63 skf64 skf65 skf66 skf67 skf68 skf69 skf70 skf71 skf72 skf73 skf74 skf75 skf76 skf77 skf78 skf79 skf80 skf81 skf82 skf83 skf84 skf85 skf86 skf87 skf88 skf89 skf90 skf91 skf92 skf93 skf94 skf95 skf96 skf97 skf98 skf99 skf100 skf101 skf102 skf103 skf104 skf105 skf106 skf107 skf108 skf109 skf110 skf111 skf112 skf113 skf114 skf115 skf116 skf117 skf118 skf119 skf120 skf121 skf122 skf123 skf124 skf125 skf126 skf127 skf128 skf129 skf130 skf131 skf132 skf133 skf134 skf135 skf136 skf137 skf138 skf139 skf140 skf141 skf142 skf143 skf144 skf145 skf146 skf147 skf148 skf149 skf150 skf151 skf152 skf153 skf154 skf155 skf156 skf157 skf158 skf159 skf160 skf161 skf162 skf163 skf164 skf165 skf166 skf167 skf168 skf169 skf170 skf171 skf172 skf173 skf174 skf175 skf176 skf177 skf178 skf179 skf180 skf181 skf182 skf183 skf184 skf185 skf186 skf187 skf188 skf189 skf190 skf191 skf192 skf193 skf194 skf195 skf196 skf197 skf198 skf199 skf200 skf201 skf202 skf203 skf204 skf205 skf206 skf207 skf208 skf209 skf210 skf211 skf212 skf213 skf214 skf215 skf216 skf217 skf218 skf219 skf220 skf221 skf222 skf223 skf224 skf225 skf226 skf227 skf228 skf229 skf230 skf231 skf232 skf233 skf234 skf235 skf236 skf237 skf238 skf239 skf240 skf241 skf242 skf243 skf244 skf245 skf246 skf247 skf248 skf249 skf250 skf251 skf252 skf253 skf254 skf255 skf256 skf257 skf258 skf259 skf260 skf261 skf262 skf263 skf264 skf265 skf266 skf267 skf268 skf269 skf270 skf271 skf272 skf273 skf274 skf275 skf276 skf277 skf278 skf279 skf280 skf281 skf282 skf283 skf284 skf285 skf286 skf287 skf288 skf289 skf290 skf291 skf292 skf293 skf294 skf295 skf296 skf297 skf298 skf299 skf300 skf301 skf302 skf303 skf304 skf305 skf306 skf307 skf308 skf309 skf310 skf311 skf312 skf313 skf314 skf315 skf316 skf317 skf318 skf319 skf320 skf321 skf322 skf323 skf324 skf325 skf326 skf327 skf328 skf329 skf330 skf331 skf332 skf333 skf334 skf335 skf336 skf337 skf338 skf339 skf340 skf341 skf342 skf343 skf344 skf345 skf346 skf347 skf348 skf349 skf350 skf351 skf352 skf353 skf354 skf355 skf356 skf357 skf358 skf359 skf360 skf361 skf362 skf363 skf364 skf365 skf366 skf367 skf368 skf369 skf370 skf371 skf372 skf373 skf374 skf375 skf376 skf377 skf378 skf379 skf380 skf381 skf382 skf383 skf384 skf385 skf386 skf387 skf388 skf389 skf390 skf391 skf392 skf393 skf394 skf395 skf396 skf397 skf398 skf399 skf400 skf401 skf402 skf403 skf404 skf405 skf406 skf407 skf408 skf409 skf410 skf411 skf412 skf413 skf414 skf415 skf416 skf417 skf418 skf419 skf420 skf421 skf422 skf423 skf424 skf425 skf426 skf427 skf428 skf429 skf430 skf431 skf432 skf433 skf434 skf435 skf436 skf437 skf438 skf439 skf440 skf441 skf442 skf443 skf444 skf445 skf446 skf447 skf448 skf449 skf450 skf451 skf452 skf453 skf454 skf455 skf456 skf457 skf458 skf459 skf460 skf461 skf462 skf463 skf464 skf465 skf466 skf467 skf468 skf469 skf470 skf471 skf472 skf473 skf474 skf475 skf476 skf477 skf478 skf479 skf480 skf481 skf482 skf483 skf484 skf485 skf486 skf487 skf488 skf489 skf490 skf491 skf492 skf493 skf494 skf495 skf496 skf497 skf498 skf499 skf500 skf501 skf502 skf503 skf504 skf505 skf506 skf507 skf508 skf509 skf510 skf511 skf512 skf513 skf514 skf515 skf516 skf517 skf518 skf519 skf520 skf521 skf522 skf523 skf524 skf525 skf526 skf527 skf528 skf529 skf530 skf531 skf532 skf533 skf534 skf535 skf536 skf537 skf538 skf539 skf540 skf541 skf542 skf543 skf544 skf545 skf546 skf547 skf548 skf549 skf550 skf551 skf552 skf553 skf554 skf555 skf556 skf557 skf558 skf559 skf560 skf561 skf562 skf563 skf564 skf565 skf566 skf567 skf568 skf569 skf570 skf571 skf572 skf573 skf574 skf575 skf576 skf577 skf578 skf579 skf580 skf581 skf582 skf583 skf584 skf585 skf586 skf587 skf588 skf589 skf590 skf591 skf592 skf593 skf594 skf595 skf596 skf597 skf598 skf599 skf600 skf601 skf602 skf603 skf604 skf605 skf606 skf607 skf608 skf609 skf610 skf611 skf612 skf613 skf614 skf615 skf616 skf617 skf618 skf619 skf620 skf621 skf622 skf623 skf624 skf625 skf626 skf627 % 1.96/1.07 Problem Properties: % 1.96/1.07 This is a full first-order problem with equality. % 1.96/1.07 SZS status GaveUp % 1.96/1.07 SPASS beiseite: SPASS does currently not support non-BS equality problems. % 1.96/1.07 %------------------------------------------------------------------------------