%------------------------------------------------------------------------------ % File : SOS---2.0 % Problem : SWV418-1.900 : TPTP v8.1.0. Released v3.5.0. % Transfm : none % Format : tptp:raw % Command : sos-script %s % Computer : n014.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 : 600s % DateTime : Wed Jul 20 21:38:25 EDT 2022 % Result : Unknown 0.28s 0.48s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.13/0.13 % Problem : SWV418-1.900 : TPTP v8.1.0. Released v3.5.0. % 0.13/0.14 % Command : sos-script %s % 0.13/0.36 % Computer : n014.cluster.edu % 0.13/0.36 % Model : x86_64 x86_64 % 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.36 % Memory : 8042.1875MB % 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.36 % CPULimit : 300 % 0.13/0.36 % WCLimit : 600 % 0.13/0.36 % DateTime : Tue Jun 14 16:15:21 EDT 2022 % 0.13/0.36 % CPUTime : % 0.22/0.47 ----- Otter 3.2, August 2001 ----- % 0.22/0.47 The process was started by sandbox on n014.cluster.edu, % 0.22/0.47 Tue Jun 14 16:15:21 2022 % 0.22/0.47 The command was "./sos". The process ID is 7115. % 0.22/0.47 % 0.22/0.47 set(prolog_style_variables). % 0.22/0.47 set(auto). % 0.22/0.47 dependent: set(auto1). % 0.22/0.47 dependent: set(process_input). % 0.22/0.47 dependent: clear(print_kept). % 0.22/0.47 dependent: clear(print_new_demod). % 0.22/0.47 dependent: clear(print_back_demod). % 0.22/0.47 dependent: clear(print_back_sub). % 0.22/0.47 dependent: set(control_memory). % 0.22/0.47 dependent: assign(max_mem, 12000). % 0.22/0.47 dependent: assign(pick_given_ratio, 4). % 0.22/0.47 dependent: assign(stats_level, 1). % 0.22/0.47 dependent: assign(pick_semantic_ratio, 3). % 0.22/0.47 dependent: assign(sos_limit, 5000). % 0.22/0.47 dependent: assign(max_weight, 60). % 0.22/0.47 clear(print_given). % 0.22/0.47 % 0.22/0.47 list(usable). % 0.22/0.47 % 0.22/0.47 ERROR, term too big: % 0.22/0.47 % 0.22/0.47 % 0.22/0.47 ( -loop % 0.22/0.47 | trans(s899,s0) % 0.22/0.47 | trans(s899,s1) % 0.22/0.47 | trans(s899,s2) % 0.22/0.47 | trans(s899,s3) % 0.22/0.47 | trans(s899,s4) % 0.22/0.47 | trans(s899,s5) % 0.22/0.47 | trans(s899,s6) % 0.22/0.47 | trans(s899,s7) % 0.22/0.47 | trans(s899,s8) % 0.22/0.47 | trans(s899,s9) % 0.22/0.47 | trans(s899,s10) % 0.22/0.47 | trans(s899,s11) % 0.22/0.47 | trans(s899,s12) % 0.22/0.47 | trans(s899,s13) % 0.22/0.47 | trans(s899,s14) % 0.22/0.47 | trans(s899,s15) % 0.22/0.47 | trans(s899,s16) % 0.22/0.47 | trans(s899,s17) % 0.22/0.47 | trans(s899,s18) % 0.22/0.47 | trans(s899,s19) % 0.22/0.47 | trans(s899,s20) % 0.22/0.47 | trans(s899,s21) % 0.22/0.47 | trans(s899,s22) % 0.22/0.47 | trans(s899,s23) % 0.22/0.47 | trans(s899,s24) % 0.22/0.47 | trans(s899,s25) % 0.22/0.47 | trans(s899,s26) % 0.22/0.47 | trans(s899,s27) % 0.22/0.47 | trans(s899,s28) % 0.22/0.47 | trans(s899,s29) % 0.22/0.47 | trans(s899,s30) % 0.22/0.47 | trans(s899,s31) % 0.22/0.47 | trans(s899,s32) % 0.22/0.47 | trans(s899,s33) % 0.22/0.47 | trans(s899,s34) % 0.22/0.47 | trans(s899,s35) % 0.22/0.47 | trans(s899,s36) % 0.22/0.47 | trans(s899,s37) % 0.22/0.47 | trans(s899,s38) % 0.22/0.47 | trans(s899,s39) % 0.22/0.47 | trans(s899,s40) % 0.22/0.47 | trans(s899,s41) % 0.22/0.47 | trans(s899,s42) % 0.22/0.47 | trans(s899,s43) % 0.22/0.47 | trans(s899,s44) % 0.22/0.47 | trans(s899,s45) % 0.22/0.47 | trans(s899,s46) % 0.22/0.47 | trans(s899,s47) % 0.22/0.47 | trans(s899,s48) % 0.22/0.47 | trans(s899,s49) % 0.22/0.47 | trans(s899,s50) % 0.22/0.47 | trans(s899,s51) % 0.22/0.47 | trans(s899,s52) % 0.22/0.47 | trans(s899,s53) % 0.22/0.47 | trans(s899,s54) % 0.22/0.47 | trans(s899,s55) % 0.22/0.47 | trans(s899,s56) % 0.22/0.47 | trans(s899,s57) % 0.22/0.47 | trans(s899,s58) % 0.22/0.47 | trans(s899,s59) % 0.22/0.47 | trans(s899,s60) % 0.22/0.47 | trans(s899,s61) % 0.22/0.47 | trans(s899,s62) % 0.22/0.47 | trans(s899,s63) % 0.22/0.47 | trans(s899,s64) % 0.22/0.47 | trans(s899,s65) % 0.22/0.47 | trans(s899,s66) % 0.22/0.47 | trans(s899,s67) % 0.22/0.47 | trans(s899,s68) % 0.22/0.47 | trans(s899,s69) % 0.22/0.47 | trans(s899,s70) % 0.22/0.47 | trans(s899,s71) % 0.22/0.47 | trans(s899,s72) % 0.22/0.47 | trans(s899,s73) % 0.22/0.47 | trans(s899,s74) % 0.22/0.47 | trans(s899,s75) % 0.22/0.47 | trans(s899,s76) % 0.22/0.47 | trans(s899,s77) % 0.22/0.47 | trans(s899,s78) % 0.22/0.47 | trans(s899,s79) % 0.22/0.47 | trans(s899,s80) % 0.22/0.47 | trans(s899,s81) % 0.22/0.47 | trans(s899,s82) % 0.22/0.47 | trans(s899,s83) % 0.22/0.47 | trans(s899,s84) % 0.22/0.47 | trans(s899,s85) % 0.22/0.47 | trans(s899,s86) % 0.22/0.47 | trans(s899,s87) % 0.22/0.47 | trans(s899,s88) % 0.22/0.47 | trans(s899,s89) % 0.22/0.47 | trans(s899,s90) % 0.22/0.47 | trans(s899,s91) % 0.22/0.47 | trans(s899,s92) % 0.22/0.47 | trans(s899,s93) % 0.22/0.47 | trans(s899,s94) % 0.22/0.47 | trans(s899,s95) % 0.22/0.47 | trans(s899,s96) % 0.22/0.47 | trans(s899,s97) % 0.22/0.47 | trans(s899,s98) % 0.22/0.47 | trans(s899,s99) % 0.22/0.47 | trans(s899,s100) % 0.22/0.47 | trans(s899,s101) % 0.22/0.47 | trans(s899,s102) % 0.22/0.47 | trans(s899,s103) % 0.22/0.47 | trans(s899,s104) % 0.22/0.47 | trans(s899,s105) % 0.22/0.47 | trans(s899,s106) % 0.22/0.47 | trans(s899,s107) % 0.22/0.47 | trans(s899,s108) % 0.22/0.47 | trans(s899,s109) % 0.22/0.47 | trans(s899,s110) % 0.22/0.47 | trans(s899,s111) % 0.22/0.47 | trans(s899,s112) % 0.22/0.47 | trans(s899,s113) % 0.22/0.47 | trans(s899,s114) % 0.22/0.47 | trans(s899,s115) % 0.22/0.47 | trans(s899,s116) % 0.22/0.47 | trans(s899,s117) % 0.22/0.47 | trans(s899,s118) % 0.22/0.47 | trans(s899,s119) % 0.22/0.47 | trans(s899,s120) % 0.22/0.47 | trans(s899,s121) % 0.22/0.47 | trans(s899,s122) % 0.22/0.47 | trans(s899,s123) % 0.22/0.47 | trans(s899,s124) % 0.22/0.47 | trans(s899,s125) % 0.22/0.47 | trans(s899,s126) % 0.22/0.47 | trans(s899,s127) % 0.22/0.47 | trans(s899,s128) % 0.22/0.47 | trans(s899,s129) % 0.22/0.47 | trans(s899,s130) % 0.22/0.47 | trans(s899,s131) % 0.22/0.47 | trans(s899,s132) % 0.22/0.47 | trans(s899,s133) % 0.22/0.47 | trans(s899,s134) % 0.22/0.47 | trans(s899,s135) % 0.22/0.47 | trans(s899,s136) % 0.22/0.47 | trans(s899,s137) % 0.22/0.47 | trans(s899,s138) % 0.22/0.47 | trans(s899,s139) % 0.22/0.47 | trans(s899,s140) % 0.22/0.47 | trans(s899,s141) % 0.22/0.47 | trans(s899,s142) % 0.22/0.47 | trans(s899,s143) % 0.22/0.47 | trans(s899,s144) % 0.22/0.47 | trans(s899,s145) % 0.22/0.47 | trans(s899,s146) % 0.22/0.47 | trans(s899,s147) % 0.22/0.47 | trans(s899,s148) % 0.22/0.47 | trans(s899,s149) % 0.22/0.47 | trans(s899,s150) % 0.22/0.47 | trans(s899,s151) % 0.22/0.47 | trans(s899,s152) % 0.22/0.47 | trans(s899,s153) % 0.22/0.47 | trans(s899,s154) % 0.22/0.47 | trans(s899,s155) % 0.22/0.47 | trans(s899,s156) % 0.22/0.47 | trans(s899,s157) % 0.22/0.47 | trans(s899,s158) % 0.22/0.47 | trans(s899,s159) % 0.22/0.47 | trans(s899,s160) % 0.22/0.47 | trans(s899,s161) % 0.22/0.47 | trans(s899,s162) % 0.22/0.47 | trans(s899,s163) % 0.22/0.47 | trans(s899,s164) % 0.22/0.47 | trans(s899,s165) % 0.22/0.47 | trans(s899,s166) % 0.22/0.47 | trans(s899,s167) % 0.22/0.47 | trans(s899,s168) % 0.22/0.47 | trans(s899,s169) % 0.22/0.47 | trans(s899,s170) % 0.22/0.47 | trans(s899,s171) % 0.22/0.47 | trans(s899,s172) % 0.22/0.47 | trans(s899,s173) % 0.22/0.47 | trans(s899,s174) % 0.22/0.47 | trans(s899,s175) % 0.22/0.47 | trans(s899,s176) % 0.22/0.47 | trans(s899,s177) % 0.22/0.47 | trans(s899,s178) % 0.22/0.47 | trans(s899,s179) % 0.22/0.47 | trans(s899,s180) % 0.22/0.47 | trans(s899,s181) % 0.22/0.47 | trans(s899,s182) % 0.22/0.47 | trans(s899,s183) % 0.22/0.47 | trans(s899,s184) % 0.22/0.47 | trans(s899,s185) % 0.22/0.47 | trans(s899,s186) % 0.22/0.47 | trans(s899,s187) % 0.22/0.47 | trans(s899,s188) % 0.22/0.47 | trans(s899,s189) % 0.22/0.47 | trans(s899,s190) % 0.22/0.47 | trans(s899,s191) % 0.22/0.47 | trans(s899,s192) % 0.22/0.47 | trans(s899,s193) % 0.22/0.47 | trans(s899,s194) % 0.22/0.47 | trans(s899,s195) % 0.22/0.47 | trans(s899,s196) % 0.22/0.47 | trans(s899,s197) % 0.22/0.47 | trans(s899,s198) % 0.22/0.47 | trans(s899,s199) % 0.22/0.47 | trans(s899,s200) % 0.22/0.47 | trans(s899,s201) % 0.22/0.47 | trans(s899,s202) % 0.22/0.47 | trans(s899,s203) % 0.22/0.47 | trans(s899,s204) % 0.22/0.47 | trans(s899,s205) % 0.22/0.47 | trans(s899,s206) % 0.22/0.47 | trans(s899,s207) % 0.22/0.47 | trans(s899,s208) % 0.22/0.47 | trans(s899,s209) % 0.22/0.47 | trans(s899,s210) % 0.22/0.47 | trans(s899,s211) % 0.22/0.47 | trans(s899,s212) % 0.22/0.47 | trans(s899,s213) % 0.22/0.47 | trans(s899,s214) % 0.22/0.47 | trans(s899,s215) % 0.22/0.47 | trans(s899,s216) % 0.22/0.47 | trans(s899,s217) % 0.22/0.47 | trans(s899,s218) % 0.22/0.47 | trans(s899,s219) % 0.22/0.47 | trans(s899,s220) % 0.22/0.47 | trans(s899,s221) % 0.22/0.47 | trans(s899,s222) % 0.22/0.47 | trans(s899,s223) % 0.22/0.47 | trans(s899,s224) % 0.22/0.47 | trans(s899,s225) % 0.22/0.47 | trans(s899,s226) % 0.22/0.47 | trans(s899,s227) % 0.22/0.47 | trans(s899,s228) % 0.22/0.47 | trans(s899,s229) % 0.22/0.47 | trans(s899,s230) % 0.22/0.47 | trans(s899,s231) % 0.22/0.47 | trans(s899,s232) % 0.22/0.47 | trans(s899,s233) % 0.22/0.47 | trans(s899,s234) % 0.22/0.47 | trans(s899,s235) % 0.22/0.47 | trans(s899,s236) % 0.22/0.47 | trans(s899,s237) % 0.22/0.47 | trans(s899,s238) % 0.22/0.47 | trans(s899,s239) % 0.22/0.47 | trans(s899,s240) % 0.22/0.47 | trans(s899,s241) % 0.22/0.47 | trans(s899,s242) % 0.22/0.47 | trans(s899,s243) % 0.22/0.47 | trans(s899,s244) % 0.22/0.47 | trans(s899,s245) % 0.22/0.47 | trans(s899,s246) % 0.22/0.47 | trans(s899,s247) % 0.22/0.47 | trans(s899,s248) % 0.22/0.47 | trans(s899,s249) % 0.22/0.47 | trans(s899,s250) % 0.22/0.47 | trans(s899,s251) % 0.22/0.47 | trans(s899,s252) % 0.22/0.47 | trans(s899,s253) % 0.22/0.47 | trans(s899,s254) % 0.22/0.47 | trans(s899,s255) % 0.22/0.47 | trans(s899,s256) % 0.22/0.47 | trans(s899,s257) % 0.22/0.47 | trans(s899,s258) % 0.22/0.47 | trans(s899,s259) % 0.22/0.47 | trans(s899,s260) % 0.22/0.47 | trans(s899,s261) % 0.22/0.47 | trans(s899,s262) % 0.22/0.47 | trans(s899,s263) % 0.22/0.47 | trans(s899,s264) % 0.22/0.47 | trans(s899,s265) % 0.22/0.47 | trans(s899,s266) % 0.22/0.47 | trans(s899,s267) % 0.22/0.47 | trans(s899,s268) % 0.22/0.47 | trans(s899,s269) % 0.22/0.47 | trans(s899,s270) % 0.22/0.47 | trans(s899,s271) % 0.22/0.47 | trans(s899,s272) % 0.22/0.47 | trans(s899,s273) % 0.22/0.47 | trans(s899,s274) % 0.22/0.47 | trans(s899,s275) % 0.22/0.47 | trans(s899,s276) % 0.22/0.47 | trans(s899,s277) % 0.22/0.47 | trans(s899,s278) % 0.22/0.47 | trans(s899,s279) % 0.22/0.47 | trans(s899,s280) % 0.22/0.47 | trans(s899,s281) % 0.22/0.47 | trans(s899,s282) % 0.22/0.47 | trans(s899,s283) % 0.22/0.47 | trans(s899,s284) % 0.22/0.47 | trans(s899,s285) % 0.22/0.47 | trans(s899,s286) % 0.22/0.47 | trans(s899,s287) % 0.22/0.47 | trans(s899,s288) % 0.22/0.47 | trans(s899,s289) % 0.22/0.47 | trans(s899,s290) % 0.22/0.47 | trans(s899,s291) % 0.22/0.47 | trans(s899,s292) % 0.22/0.47 | trans(s899,s293) % 0.22/0.47 | trans(s899,s294) % 0.22/0.47 | trans(s899,s295) % 0.22/0.47 | trans(s899,s296) % 0.22/0.47 | trans(s899,s297) % 0.22/0.47 | trans(s899,s298) % 0.22/0.47 | trans(s899,s299) % 0.22/0.47 | trans(s899,s300) % 0.22/0.47 | trans(s899,s301) % 0.22/0.47 | trans(s899,s302) % 0.22/0.47 | trans(s899,s303) % 0.22/0.47 | trans(s899,s304) % 0.22/0.47 | trans(s899,s305) % 0.22/0.47 | trans(s899,s306) % 0.22/0.47 | trans(s899,s307) % 0.22/0.47 | trans(s899,s308) % 0.22/0.47 | trans(s899,s309) % 0.22/0.47 | trans(s899,s310) % 0.22/0.47 | trans(s899,s311) % 0.22/0.47 | trans(s899,s312) % 0.22/0.47 | trans(s899,s313) % 0.22/0.47 | trans(s899,s314) % 0.22/0.47 | trans(s899,s315) % 0.22/0.47 | trans(s899,s316) % 0.22/0.47 | trans(s899,s317) % 0.22/0.47 | trans(s899,s318) % 0.22/0.47 | trans(s899,s319) % 0.22/0.47 | trans(s899,s320) % 0.22/0.47 | trans(s899,s321) % 0.22/0.47 | trans(s899,s322) % 0.22/0.47 | trans(s899,s323) % 0.22/0.47 | trans(s899,s324) % 0.22/0.47 | trans(s899,s325) % 0.22/0.47 | trans(s899,s326) % 0.22/0.47 | trans(s899,s327) % 0.22/0.47 | trans(s899,s328) % 0.22/0.47 | trans(s899,s329) % 0.22/0.47 | trans(s899,s330) % 0.22/0.47 | trans(s899,s331) % 0.22/0.47 | trans(s899,s332) % 0.22/0.47 | trans(s899,s333) % 0.22/0.47 | trans(s899,s334) % 0.22/0.47 | trans(s899,s335) % 0.22/0.47 | trans(s899,s336) % 0.22/0.47 | trans(s899,s337) % 0.22/0.47 | trans(s899,s338) % 0.22/0.47 | trans(s899,s339) % 0.22/0.47 | trans(s899,s340) % 0.22/0.47 | trans(s899,s341) % 0.22/0.47 | trans(s899,s342) % 0.22/0.47 | trans(s899,s343) % 0.22/0.47 | trans(s899,s344) % 0.22/0.47 | trans(s899,s345) % 0.22/0.47 | trans(s899,s346) % 0.22/0.47 | trans(s899,s347) % 0.22/0.47 | trans(s899,s348) % 0.22/0.47 | trans(s899,s349) % 0.22/0.47 | trans(s899,s350) % 0.22/0.47 | trans(s899,s351) % 0.22/0.47 | trans(s899,s352) % 0.22/0.47 | trans(s899,s353) % 0.22/0.47 | trans(s899,s354) % 0.22/0.47 | trans(s899,s355) % 0.22/0.47 | trans(s899,s356) % 0.22/0.47 | trans(s899,s357) % 0.22/0.47 | trans(s899,s358) % 0.22/0.47 | trans(s899,s359) % 0.22/0.47 | trans(s899,s360) % 0.22/0.47 | trans(s899,s361) % 0.22/0.47 | trans(s899,s362) % 0.22/0.47 | trans(s899,s363) % 0.22/0.47 | trans(s899,s364) % 0.22/0.47 | trans(s899,s365) % 0.22/0.47 | trans(s899,s366) % 0.22/0.47 | trans(s899,s367) % 0.22/0.47 | trans(s899,s368) % 0.22/0.47 | trans(s899,s369) % 0.22/0.47 | trans(s899,s370) % 0.22/0.47 | trans(s899,s371) % 0.22/0.47 | trans(s899,s372) % 0.22/0.47 | trans(s899,s373) % 0.22/0.47 | trans(s899,s374) % 0.22/0.47 | trans(s899,s375) % 0.22/0.47 | trans(s899,s376) % 0.22/0.47 | trans(s899,s377) % 0.22/0.47 | trans(s899,s378) % 0.22/0.47 | trans(s899,s379) % 0.22/0.47 | trans(s899,s380) % 0.22/0.47 | trans(s899,s381) % 0.22/0.47 | trans(s899,s382) % 0.22/0.47 | trans(s899,s383) % 0.22/0.47 | trans(s899,s384) % 0.22/0.47 | trans(s899,s385) % 0.22/0.47 | trans(s899,s386) % 0.22/0.47 | trans(s899,s387) % 0.22/0.47 | trans(s899,s388) % 0.22/0.47 | trans(s899,s389) % 0.22/0.47 | trans(s899,s390) % 0.22/0.47 | trans(s899,s391) % 0.22/0.47 | trans(s899,s392) % 0.22/0.47 | trans(s899,s393) % 0.22/0.47 | trans(s899,s394) % 0.22/0.47 | trans(s899,s395) % 0.22/0.47 | trans(s899,s396) % 0.22/0.47 | trans(s899,s397) % 0.22/0.47 | trans(s899,s398) % 0.22/0.47 | trans(s899,s399) % 0.22/0.47 | trans(s899,s400) % 0.22/0.47 | trans(s899,s401) % 0.22/0.47 | trans(s899,s402) % 0.22/0.47 | trans(s899,s403) % 0.22/0.47 | trans(s899,s404) % 0.22/0.47 | trans(s899,s405) % 0.22/0.47 | trans(s899,s406) % 0.22/0.47 | trans(s899,s407) % 0.22/0.47 | trans(s899,s408) % 0.22/0.47 | trans(s899,s409) % 0.22/0.47 | trans(s899,s410) % 0.22/0.47 | trans(s899,s411) % 0.22/0.47 | trans(s899,s412) % 0.22/0.47 | trans(s899,s413) % 0.22/0.47 | trans(s899,s414) % 0.22/0.47 | trans(s899,s415) % 0.22/0.47 | trans(s899,s416) % 0.22/0.47 | trans(s899,s417) % 0.22/0.47 | trans(s899,s418) % 0.22/0.47 | trans(s899,s419) % 0.22/0.47 | trans(s899,s420) % 0.22/0.47 | trans(s899,s421) % 0.22/0.47 | trans(s899,s422) % 0.22/0.47 | trans(s899,s423) % 0.22/0.47 | trans(s899,s424) % 0.22/0.47 | trans(s899,s425) % 0.22/0.47 | trans(s899,s426) % 0.22/0.47 | trans(s899,s427) % 0.22/0.47 | trans(s899,s428) % 0.22/0.47 | trans(s899,s429) % 0.22/0.47 | trans(s899,s430) % 0.22/0.47 | trans(s899,s431) % 0.22/0.47 | trans(s899,s432) % 0.22/0.47 | trans(s899,s433) % 0.22/0.47 | trans(s899,s434) % 0.22/0.47 | trans(s899,s435) % 0.22/0.47 | trans(s899,s436) % 0.22/0.47 | trans(s899,s437) % 0.22/0.47 | trans(s899,s438) % 0.22/0.47 | trans(s899,s439) % 0.22/0.47 | trans(s899,s440) % 0.22/0.47 | trans(s899,s441) % 0.22/0.47 | trans(s899,s442) % 0.22/0.47 | trans(s899,s443) % 0.22/0.47 | trans(s899,s444) % 0.22/0.47 | trans(s899,s445) % 0.22/0.47 | trans(s899,s446) % 0.22/0.47 | trans(s899,s447) % 0.22/0.47 | trans(s899,s448) % 0.22/0.47 | trans(s899,s449) % 0.22/0.47 | trans(s899,s450) % 0.22/0.47 | trans(s899,s451) % 0.22/0.47 | trans(s899,s452) % 0.22/0.47 | trans(s899,s453) % 0.22/0.47 | trans(s899,s454) % 0.22/0.47 | trans(s899,s455) % 0.22/0.47 | trans(s899,s456) % 0.22/0.47 | trans(s899,s457) % 0.22/0.47 | trans(s899,s458) % 0.22/0.47 | trans(s899,s459) % 0.22/0.47 | trans(s899,s460) % 0.22/0.47 | trans(s899,s461) % 0.22/0.47 | trans(s899,s462) % 0.22/0.47 | trans(s899,s463) % 0.22/0.47 | trans(s899,s464) % 0.22/0.47 | trans(s899,s465) % 0.22/0.47 | trans(s899,s466) % 0.22/0.47 | trans(s899,s467) % 0.22/0.47 | trans(s899,s468) % 0.22/0.47 | trans(s899,s469) % 0.22/0.47 | trans(s899,s470) % 0.22/0.47 | trans(s899,s471) % 0.22/0.47 | trans(s899,s472) % 0.22/0.47 | trans(s899,s473) % 0.22/0.47 | trans(s899,s474) % 0.22/0.47 | trans(s899,s475) % 0.22/0.47 | trans(s899,s476) % 0.22/0.47 | trans(s899,s477) % 0.22/0.47 | trans(s899,s478) % 0.22/0.47 | trans(s899,s479) % 0.22/0.47 | trans(s899,s480) % 0.22/0.47 | trans(s899,s481) % 0.22/0.47 | trans(s899,s482) % 0.22/0.47 | trans(s899,s483) % 0.22/0.47 | trans(s899,s484) % 0.22/0.47 | trans(s899,s485) % 0.22/0.47 | trans(s899,s486) % 0.22/0.47 | trans(s899,s487) % 0.22/0.47 | trans(s899,s488) % 0.22/0.47 | trans(s899,s489) % 0.22/0.47 | trans(s899,s490) % 0.22/0.47 | trans(s899,s491) % 0.22/0.47 | trans(s899,s492) % 0.22/0.47 | trans(s899,s493) % 0.22/0.47 | trans(s899,s494) % 0.22/0.47 | trans(s899,s495) % 0.22/0.47 | trans(s899,s496) % 0.22/0.47 | trans(s899,s497) % 0.22/0.47 | trans(s899,s498) % 0.22/0.47 | ***HERE*** trans(s899,s499) % 0.22/0.47 | trans(s899,s500) % 0.22/0.47 | trans(s899,s501) % 0.22/0.47 | trans(s899,s502) % 0.22/0.47 | trans(s899,s503) % 0.22/0.47 | trans(s899,s504) % 0.22/0.47 | trans(s899,s505) % 0.22/0.47 | trans(s899,s506) % 0.22/0.47 | trans(s899,s507) % 0.22/0.47 | trans(s899,s508) % 0.22/0.47 | trans(s899,s509) % 0.22/0.47 | trans(s899,s510) % 0.22/0.47 | trans(s899,s511) % 0.22/0.47 | trans(s899,s512) % 0.22/0.47 | trans(s899,s513) % 0.22/0.47 | trans(s899,s514) % 0.22/0.47 | trans(s899,s515) % 0.22/0.47 | trans(s899,s516) % 0.22/0.47 | trans(s899,s517) % 0.22/0.47 | trans(s899,s518) % 0.22/0.47 | trans(s899,s519) % 0.22/0.47 | trans(s899,s520) % 0.22/0.47 | trans(s899,s521) % 0.22/0.47 | trans(s899,s522) % 0.22/0.47 | trans(s899,s523) % 0.22/0.47 | trans(s899,s524) % 0.22/0.47 | trans(s899,s525) % 0.22/0.47 | trans(s899,s526) % 0.22/0.47 | trans(s899,s527) % 0.22/0.47 | trans(s899,s528) % 0.22/0.47 | trans(s899,s529) % 0.22/0.47 | trans(s899,s530) % 0.22/0.47 | trans(s899,s531) % 0.22/0.47 | trans(s899,s532) % 0.22/0.47 | trans(s899,s533) % 0.22/0.47 | trans(s899,s534) % 0.22/0.47 | trans(s899,s535) % 0.22/0.47 | trans(s899,s536) % 0.22/0.47 | trans(s899,s537) % 0.22/0.47 | trans(s899,s538) % 0.22/0.47 | trans(s899,s539) % 0.22/0.47 | trans(s899,s540) % 0.22/0.47 | trans(s899,s541) % 0.22/0.47 | trans(s899,s542) % 0.22/0.47 | trans(s899,s543) % 0.22/0.47 | trans(s899,s544) % 0.22/0.47 | trans(s899,s545) % 0.22/0.47 | trans(s899,s546) % 0.22/0.47 | trans(s899,s547) % 0.22/0.47 | trans(s899,s548) % 0.22/0.47 | trans(s899,s549) % 0.22/0.47 | trans(s899,s550) % 0.22/0.47 | trans(s899,s551) % 0.22/0.47 | trans(s899,s552) % 0.22/0.47 | trans(s899,s553) % 0.22/0.47 | trans(s899,s554) % 0.22/0.47 | trans(s899,s555) % 0.22/0.47 | trans(s899,s556) % 0.22/0.47 | trans(s899,s557) % 0.22/0.47 | trans(s899,s558) % 0.22/0.47 | trans(s899,s559) % 0.22/0.47 | trans(s899,s560) % 0.22/0.47 | trans(s899,s561) % 0.22/0.47 | trans(s899,s562) % 0.22/0.47 | trans(s899,s563) % 0.22/0.47 | trans(s899,s564) % 0.22/0.47 | trans(s899,s565) % 0.22/0.47 | trans(s899,s566) % 0.22/0.47 | trans(s899,s567) % 0.22/0.47 | trans(s899,s568) % 0.22/0.47 | trans(s899,s569) % 0.22/0.47 | trans(s899,s570) % 0.22/0.47 | trans(s899,s571) % 0.22/0.47 | trans(s899,s572) % 0.22/0.47 | trans(s899,s573) % 0.22/0.47 | trans(s899,s574) % 0.22/0.47 | trans(s899,s575) % 0.22/0.47 | trans(s899,s576) % 0.22/0.47 | trans(s899,s577) % 0.22/0.47 | trans(s899,s578) % 0.22/0.47 | trans(s899,s579) % 0.22/0.47 | trans(s899,s580) % 0.22/0.47 | trans(s899,s581) % 0.22/0.47 | trans(s899,s582) % 0.22/0.47 | trans(s899,s583) % 0.22/0.47 | trans(s899,s584) % 0.22/0.47 | trans(s899,s585) % 0.22/0.47 | trans(s899,s586) % 0.22/0.47 | trans(s899,s587) % 0.22/0.47 | trans(s899,s588) % 0.22/0.47 | trans(s899,s589) % 0.22/0.47 | trans(s899,s590) % 0.22/0.47 | trans(s899,s591) % 0.22/0.47 | trans(s899,s592) % 0.22/0.47 | trans(s899,s593) % 0.22/0.47 | trans(s899,s594) % 0.22/0.47 | trans(s899,s595) % 0.22/0.47 | trans(s899,s596) % 0.22/0.47 | trans(s899,s597) % 0.22/0.47 | trans(s899,s598) % 0.22/0.47 | trans(s899,s599) % 0.22/0.47 | trans(s899,s600) % 0.22/0.47 | trans(s899,s601) % 0.22/0.47 | trans(s899,s602) % 0.22/0.47 | trans(s899,s603) % 0.22/0.47 | trans(s899,s604) % 0.22/0.47 | trans(s899,s605) % 0.22/0.47 | trans(s899,s606) % 0.22/0.47 | trans(s899,s607) % 0.22/0.47 | trans(s899,s608) % 0.22/0.47 | trans(s899,s609) % 0.22/0.47 | trans(s899,s610) % 0.22/0.47 | trans(s899,s611) % 0.22/0.47 | trans(s899,s612) % 0.22/0.47 | trans(s899,s613) % 0.22/0.47 | trans(s899,s614) % 0.22/0.47 | trans(s899,s615) % 0.22/0.47 | trans(s899,s616) % 0.22/0.47 | trans(s899,s617) % 0.22/0.47 | trans(s899,s618) % 0.22/0.47 | trans(s899,s619) % 0.22/0.47 | trans(s899,s620) % 0.22/0.47 | trans(s899,s621) % 0.22/0.47 | trans(s899,s622) % 0.22/0.47 | trans(s899,s623) % 0.22/0.47 | trans(s899,s624) % 0.22/0.47 | trans(s899,s625) % 0.22/0.47 | trans(s899,s626) % 0.22/0.47 | trans(s899,s627) % 0.22/0.47 | trans(s899,s628) % 0.22/0.47 | trans(s899,s629) % 0.22/0.47 | trans(s899,s630) % 0.22/0.47 | trans(s899,s631) % 0.22/0.47 | trans(s899,s632) % 0.22/0.47 | trans(s899,s633) % 0.22/0.47 | trans(s899,s634) % 0.22/0.47 | trans(s899,s635) % 0.22/0.47 | trans(s899,s636) % 0.22/0.47 | trans(s899,s637) % 0.22/0.47 | trans(s899,s638) % 0.22/0.47 | trans(s899,s639) % 0.22/0.47 | trans(s899,s640) % 0.22/0.47 | trans(s899,s641) % 0.22/0.47 | trans(s899,s642) % 0.22/0.47 | trans(s899,s643) % 0.22/0.47 | trans(s899,s644) % 0.22/0.47 | trans(s899,s645) % 0.22/0.47 | trans(s899,s646) % 0.22/0.47 | trans(s899,s647) % 0.22/0.47 | trans(s899,s648) % 0.22/0.47 | trans(s899,s649) % 0.22/0.47 | trans(s899,s650) % 0.22/0.47 | trans(s899,s651) % 0.22/0.47 | trans(s899,s652) % 0.22/0.47 | trans(s899,s653) % 0.22/0.47 | trans(s899,s654) % 0.22/0.47 | trans(s899,s655) % 0.22/0.47 | trans(s899,s656) % 0.22/0.47 | trans(s899,s657) % 0.22/0.47 | trans(s899,s658) % 0.22/0.47 | trans(s899,s659) % 0.22/0.47 | trans(s899,s660) % 0.22/0.47 | trans(s899,s661) % 0.22/0.47 | trans(s899,s662) % 0.22/0.47 | trans(s899,s663) % 0.22/0.47 | trans(s899,s664) % 0.22/0.47 | trans(s899,s665) % 0.22/0.47 | trans(s899,s666) % 0.22/0.47 | trans(s899,s667) % 0.22/0.47 | trans(s899,s668) % 0.22/0.47 | trans(s899,s669) % 0.22/0.47 | trans(s899,s670) % 0.22/0.47 | trans(s899,s671) % 0.22/0.47 | trans(s899,s672) % 0.22/0.47 | trans(s899,s673) % 0.22/0.47 | trans(s899,s674) % 0.22/0.47 | trans(s899,s675) % 0.22/0.47 | trans(s899,s676) % 0.22/0.47 | trans(s899,s677) % 0.22/0.47 | trans(s899,s678) % 0.22/0.47 | trans(s899,s679) % 0.22/0.47 | trans(s899,s680) % 0.22/0.47 | trans(s899,s681) % 0.22/0.47 | trans(s899,s682) % 0.22/0.47 | trans(s899,s683) % 0.22/0.47 | trans(s899,s684) % 0.22/0.47 | trans(s899,s685) % 0.22/0.47 | trans(s899,s686) % 0.22/0.47 | trans(s899,s687) % 0.22/0.47 | trans(s899,s688) % 0.22/0.47 | trans(s899,s689) % 0.22/0.47 | trans(s899,s690) % 0.22/0.47 | trans(s899,s691) % 0.22/0.47 | trans(s899,s692) % 0.22/0.47 | trans(s899,s693) % 0.22/0.47 | trans(s899,s694) % 0.22/0.47 | trans(s899,s695) % 0.22/0.47 | trans(s899,s696) % 0.22/0.47 | trans(s899,s697) % 0.22/0.47 | trans(s899,s698) % 0.22/0.47 | trans(s899,s699) % 0.22/0.47 | trans(s899,s700) % 0.22/0.47 | trans(s899,s701) % 0.22/0.47 | trans(s899,s702) % 0.22/0.47 | trans(s899,s703) % 0.22/0.47 | trans(s899,s704) % 0.22/0.47 | trans(s899,s705) % 0.22/0.47 | trans(s899,s706) % 0.22/0.47 | trans(s899,s707) % 0.22/0.47 | trans(s899,s708) % 0.22/0.47 | trans(s899,s709) % 0.22/0.47 | trans(s899,s710) % 0.22/0.47 | trans(s899,s711) % 0.22/0.47 | trans(s899,s712) % 0.22/0.47 | trans(s899,s713) % 0.22/0.47 | trans(s899,s714) % 0.22/0.47 | trans(s899,s715) % 0.22/0.47 | trans(s899,s716) % 0.22/0.47 | trans(s899,s717) % 0.22/0.47 | trans(s899,s718) % 0.22/0.47 | trans(s899,s719) % 0.22/0.47 | trans(s899,s720) % 0.22/0.47 | trans(s899,s721) % 0.22/0.47 | trans(s899,s722) % 0.22/0.47 | trans(s899,s723) % 0.22/0.47 | trans(s899,s724) % 0.22/0.47 | trans(s899,s725) % 0.22/0.47 | trans(s899,s726) % 0.22/0.47 | trans(s899,s727) % 0.22/0.47 | trans(s899,s728) % 0.22/0.47 | trans(s899,s729) % 0.22/0.47 | trans(s899,s730) % 0.22/0.47 | trans(s899,s731) % 0.22/0.47 | trans(s899,s732) % 0.22/0.47 | trans(s899,s733) % 0.22/0.47 | trans(s899,s734) % 0.22/0.47 | trans(s899,s735) % 0.22/0.47 | trans(s899,s736) % 0.22/0.47 | trans(s899,s737) % 0.22/0.47 | trans(s899,s738) % 0.22/0.47 | trans(s899,s739) % 0.22/0.47 | trans(s899,s740) % 0.22/0.47 | trans(s899,s741) % 0.22/0.47 | trans(s899,s742) % 0.22/0.47 | trans(s899,s743) % 0.22/0.47 | trans(s899,s744) % 0.22/0.47 | trans(s899,s745) % 0.22/0.47 | trans(s899,s746) % 0.22/0.47 | trans(s899,s747) % 0.22/0.47 | trans(s899,s748) % 0.22/0.47 | trans(s899,s749) % 0.22/0.47 | trans(s899,s750) % 0.22/0.47 | trans(s899,s751) % 0.22/0.47 | trans(s899,s752) % 0.22/0.47 | trans(s899,s753) % 0.22/0.47 | trans(s899,s754) % 0.22/0.47 | trans(s899,s755) % 0.22/0.47 | trans(s899,s756) % 0.22/0.47 | trans(s899,s757) % 0.22/0.47 | trans(s899,s758) % 0.22/0.47 | trans(s899,s759) % 0.22/0.47 | trans(s899,s760) % 0.22/0.47 | trans(s899,s761) % 0.22/0.47 | trans(s899,s762) % 0.22/0.47 | trans(s899,s763) % 0.22/0.47 | trans(s899,s764) % 0.22/0.47 | trans(s899,s765) % 0.22/0.47 | trans(s899,s766) % 0.22/0.47 | trans(s899,s767) % 0.22/0.47 | trans(s899,s768) % 0.22/0.47 | trans(s899,s769) % 0.22/0.47 | trans(s899,s770) % 0.22/0.47 | trans(s899,s771) % 0.22/0.47 | trans(s899,s772) % 0.22/0.47 | trans(s899,s773) % 0.22/0.47 | trans(s899,s774) % 0.22/0.47 | trans(s899,s775) % 0.22/0.47 | trans(s899,s776) % 0.22/0.47 | trans(s899,s777) % 0.22/0.47 | trans(s899,s778) % 0.22/0.47 | trans(s899,s779) % 0.22/0.47 | trans(s899,s780) % 0.22/0.47 | trans(s899,s781) % 0.22/0.47 | trans(s899,s782) % 0.22/0.47 | trans(s899,s783) % 0.22/0.47 | trans(s899,s784) % 0.22/0.47 | trans(s899,s785) % 0.22/0.47 | trans(s899,s786) % 0.22/0.47 | trans(s899,s787) % 0.22/0.47 | trans(s899,s788) % 0.22/0.47 | trans(s899,s789) % 0.22/0.47 | trans(s899,s790) % 0.22/0.47 | trans(s899,s791) % 0.22/0.47 | trans(s899,s792) % 0.22/0.47 | trans(s899,s793) % 0.22/0.47 | trans(s899,s794) % 0.22/0.47 | trans(s899,s795) % 0.22/0.47 | trans(s899,s796) % 0.22/0.47 | trans(s899,s797) % 0.22/0.47 | trans(s899,s798) % 0.22/0.47 | trans(s899,s799) % 0.22/0.47 | trans(s899,s800) % 0.22/0.47 | trans(s899,s801) % 0.22/0.47 | trans(s899,s802) % 0.22/0.47 | trans(s899,s803) % 0.22/0.47 | trans(s899,s804) % 0.22/0.47 | trans(s899,s805) % 0.22/0.47 | trans(s899,s806) % 0.22/0.47 | trans(s899,s807) % 0.22/0.47 | trans(s899,s808) % 0.22/0.47 | trans(s899,s809) % 0.22/0.47 | trans(s899,s810) % 0.22/0.47 | trans(s899,s811) % 0.22/0.47 | trans(s899,s812) % 0.22/0.47 | trans(s899,s813) % 0.22/0.47 | trans(s899,s814) % 0.22/0.47 | trans(s899,s815) % 0.22/0.47 | trans(s899,s816) % 0.22/0.47 | trans(s899,s817) % 0.22/0.47 | trans(s899,s818) % 0.22/0.47 | trans(s899,s819) % 0.22/0.47 | trans(s899,s820) % 0.22/0.47 | trans(s899,s821) % 0.22/0.47 | trans(s899,s822) % 0.22/0.47 | trans(s899,s823) % 0.22/0.47 | trans(s899,s824) % 0.22/0.47 | trans(s899,s825) % 0.22/0.47 | trans(s899,s826) % 0.22/0.47 | trans(s899,s827) % 0.22/0.47 | trans(s899,s828) % 0.22/0.47 | trans(s899,s829) % 0.22/0.47 | trans(s899,s830) % 0.22/0.47 | trans(s899,s831) % 0.22/0.47 | trans(s899,s832) % 0.22/0.47 | trans(s899,s833) % 0.22/0.47 | trans(s899,s834) % 0.22/0.47 | trans(s899,s835) % 0.22/0.47 | trans(s899,s836) % 0.22/0.47 | trans(s899,s837) % 0.22/0.47 | trans(s899,s838) % 0.22/0.47 | trans(s899,s839) % 0.22/0.47 | trans(s899,s840) % 0.22/0.47 | trans(s899,s841) % 0.22/0.47 | trans(s899,s842) % 0.22/0.47 | trans(s899,s843) % 0.22/0.47 | trans(s899,s844) % 0.22/0.47 | trans(s899,s845) % 0.22/0.47 | trans(s899,s846) % 0.22/0.47 | trans(s899,s847) % 0.22/0.47 | trans(s899,s848) % 0.22/0.47 | trans(s899,s849) % 0.22/0.47 | trans(s899,s850) % 0.22/0.47 | trans(s899,s851) % 0.22/0.47 | trans(s899,s852) % 0.22/0.47 | trans(s899,s853) % 0.22/0.47 | trans(s899,s854) % 0.22/0.47 | trans(s899,s855) % 0.22/0.47 | trans(s899,s856) % 0.22/0.47 | trans(s899,s857) % 0.22/0.47 | trans(s899,s858) % 0.22/0.47 | trans(s899,s859) % 0.22/0.47 | trans(s899,s860) % 0.22/0.47 | trans(s899,s861) % 0.22/0.47 | trans(s899,s862) % 0.22/0.47 | trans(s899,s863) % 0.22/0.47 | trans(s899,s864) % 0.22/0.47 | trans(s899,s865) % 0.22/0.47 | trans(s899,s866) % 0.22/0.47 | trans(s899,s867) % 0.22/0.47 | trans(s899,s868) % 0.22/0.47 | trans(s899,s869) % 0.22/0.47 | trans(s899,s870) % 0.22/0.47 | trans(s899,s871) % 0.22/0.47 | trans(s899,s872) % 0.22/0.47 | trans(s899,s873) % 0.22/0.47 | trans(s899,s874) % 0.22/0.47 | trans(s899,s875) % 0.22/0.47 | trans(s899,s876) % 0.22/0.47 | trans(s899,s877) % 0.22/0.47 | trans(s899,s878) % 0.22/0.47 | trans(s899,s879) % 0.22/0.47 | trans(s899,s880) % 0.22/0.47 | trans(s899,s881) % 0.22/0.47 | trans(s899,s882) % 0.22/0.47 | trans(s899,s883) % 0.22/0.47 | trans(s899,s884) % 0.22/0.47 | trans(s899,s885) % 0.22/0.47 | trans(s899,s886) % 0.22/0.47 | trans(s899,s887) % 0.22/0.47 | trans(s899,s888) % 0.22/0.47 | trans(s899,s889) % 0.22/0.47 | trans(s899,s890) % 0.22/0.47 | trans(s899,s891) % 0.22/0.47 | trans(s899,s892) % 0.22/0.47 | trans(s899,s893) % 0.22/0.47 | trans(s899,s894) % 0.22/0.47 | trans(s899,s895) % 0.22/0.47 | trans(s899,s896) % 0.22/0.47 | trans(s899,s897) % 0.22/0.47 | trans(s899,s898) % 0.22/0.47 | trans(s899,s899) ). % 0.22/0.47 % 0.22/0.47 ======= end of input processing ======= % 0.22/0.47 % 0.22/0.47 1 input errors were found. % 0.22/0.47 % 0.22/0.47 1 input errors were found. %------------------------------------------------------------------------------