%------------------------------------------------------------------------------ % File : SOS---2.0 % Problem : SWV418-1.580 : TPTP v8.1.0. Released v3.5.0. % Transfm : none % Format : tptp:raw % Command : sos-script %s % Computer : n006.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:24 EDT 2022 % Result : Unknown 0.19s 0.41s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWV418-1.580 : TPTP v8.1.0. Released v3.5.0. % 0.07/0.13 % Command : sos-script %s % 0.13/0.34 % Computer : n006.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Wed Jun 15 09:49:11 EDT 2022 % 0.13/0.34 % CPUTime : % 0.19/0.40 ----- Otter 3.2, August 2001 ----- % 0.19/0.40 The process was started by sandbox2 on n006.cluster.edu, % 0.19/0.40 Wed Jun 15 09:49:11 2022 % 0.19/0.40 The command was "./sos". The process ID is 26723. % 0.19/0.40 % 0.19/0.40 set(prolog_style_variables). % 0.19/0.40 set(auto). % 0.19/0.40 dependent: set(auto1). % 0.19/0.40 dependent: set(process_input). % 0.19/0.40 dependent: clear(print_kept). % 0.19/0.40 dependent: clear(print_new_demod). % 0.19/0.40 dependent: clear(print_back_demod). % 0.19/0.40 dependent: clear(print_back_sub). % 0.19/0.40 dependent: set(control_memory). % 0.19/0.40 dependent: assign(max_mem, 12000). % 0.19/0.40 dependent: assign(pick_given_ratio, 4). % 0.19/0.40 dependent: assign(stats_level, 1). % 0.19/0.40 dependent: assign(pick_semantic_ratio, 3). % 0.19/0.40 dependent: assign(sos_limit, 5000). % 0.19/0.40 dependent: assign(max_weight, 60). % 0.19/0.40 clear(print_given). % 0.19/0.40 % 0.19/0.40 list(usable). % 0.19/0.40 % 0.19/0.40 ERROR, term too big: % 0.19/0.40 % 0.19/0.40 % 0.19/0.40 ( -loop % 0.19/0.40 | trans(s579,s0) % 0.19/0.40 | trans(s579,s1) % 0.19/0.40 | trans(s579,s2) % 0.19/0.40 | trans(s579,s3) % 0.19/0.40 | trans(s579,s4) % 0.19/0.40 | trans(s579,s5) % 0.19/0.40 | trans(s579,s6) % 0.19/0.40 | trans(s579,s7) % 0.19/0.40 | trans(s579,s8) % 0.19/0.40 | trans(s579,s9) % 0.19/0.40 | trans(s579,s10) % 0.19/0.40 | trans(s579,s11) % 0.19/0.40 | trans(s579,s12) % 0.19/0.40 | trans(s579,s13) % 0.19/0.40 | trans(s579,s14) % 0.19/0.40 | trans(s579,s15) % 0.19/0.40 | trans(s579,s16) % 0.19/0.40 | trans(s579,s17) % 0.19/0.40 | trans(s579,s18) % 0.19/0.40 | trans(s579,s19) % 0.19/0.40 | trans(s579,s20) % 0.19/0.40 | trans(s579,s21) % 0.19/0.40 | trans(s579,s22) % 0.19/0.40 | trans(s579,s23) % 0.19/0.40 | trans(s579,s24) % 0.19/0.40 | trans(s579,s25) % 0.19/0.40 | trans(s579,s26) % 0.19/0.40 | trans(s579,s27) % 0.19/0.40 | trans(s579,s28) % 0.19/0.40 | trans(s579,s29) % 0.19/0.40 | trans(s579,s30) % 0.19/0.40 | trans(s579,s31) % 0.19/0.40 | trans(s579,s32) % 0.19/0.40 | trans(s579,s33) % 0.19/0.40 | trans(s579,s34) % 0.19/0.40 | trans(s579,s35) % 0.19/0.40 | trans(s579,s36) % 0.19/0.40 | trans(s579,s37) % 0.19/0.40 | trans(s579,s38) % 0.19/0.40 | trans(s579,s39) % 0.19/0.40 | trans(s579,s40) % 0.19/0.40 | trans(s579,s41) % 0.19/0.40 | trans(s579,s42) % 0.19/0.40 | trans(s579,s43) % 0.19/0.40 | trans(s579,s44) % 0.19/0.40 | trans(s579,s45) % 0.19/0.40 | trans(s579,s46) % 0.19/0.40 | trans(s579,s47) % 0.19/0.40 | trans(s579,s48) % 0.19/0.40 | trans(s579,s49) % 0.19/0.40 | trans(s579,s50) % 0.19/0.40 | trans(s579,s51) % 0.19/0.40 | trans(s579,s52) % 0.19/0.40 | trans(s579,s53) % 0.19/0.40 | trans(s579,s54) % 0.19/0.40 | trans(s579,s55) % 0.19/0.40 | trans(s579,s56) % 0.19/0.40 | trans(s579,s57) % 0.19/0.40 | trans(s579,s58) % 0.19/0.40 | trans(s579,s59) % 0.19/0.40 | trans(s579,s60) % 0.19/0.40 | trans(s579,s61) % 0.19/0.40 | trans(s579,s62) % 0.19/0.40 | trans(s579,s63) % 0.19/0.40 | trans(s579,s64) % 0.19/0.40 | trans(s579,s65) % 0.19/0.40 | trans(s579,s66) % 0.19/0.40 | trans(s579,s67) % 0.19/0.40 | trans(s579,s68) % 0.19/0.40 | trans(s579,s69) % 0.19/0.40 | trans(s579,s70) % 0.19/0.40 | trans(s579,s71) % 0.19/0.40 | trans(s579,s72) % 0.19/0.40 | trans(s579,s73) % 0.19/0.40 | trans(s579,s74) % 0.19/0.40 | trans(s579,s75) % 0.19/0.40 | trans(s579,s76) % 0.19/0.40 | trans(s579,s77) % 0.19/0.40 | trans(s579,s78) % 0.19/0.40 | trans(s579,s79) % 0.19/0.40 | trans(s579,s80) % 0.19/0.40 | trans(s579,s81) % 0.19/0.40 | trans(s579,s82) % 0.19/0.40 | trans(s579,s83) % 0.19/0.40 | trans(s579,s84) % 0.19/0.40 | trans(s579,s85) % 0.19/0.40 | trans(s579,s86) % 0.19/0.40 | trans(s579,s87) % 0.19/0.40 | trans(s579,s88) % 0.19/0.40 | trans(s579,s89) % 0.19/0.40 | trans(s579,s90) % 0.19/0.40 | trans(s579,s91) % 0.19/0.40 | trans(s579,s92) % 0.19/0.40 | trans(s579,s93) % 0.19/0.40 | trans(s579,s94) % 0.19/0.40 | trans(s579,s95) % 0.19/0.40 | trans(s579,s96) % 0.19/0.40 | trans(s579,s97) % 0.19/0.40 | trans(s579,s98) % 0.19/0.40 | trans(s579,s99) % 0.19/0.40 | trans(s579,s100) % 0.19/0.40 | trans(s579,s101) % 0.19/0.40 | trans(s579,s102) % 0.19/0.40 | trans(s579,s103) % 0.19/0.40 | trans(s579,s104) % 0.19/0.40 | trans(s579,s105) % 0.19/0.40 | trans(s579,s106) % 0.19/0.40 | trans(s579,s107) % 0.19/0.40 | trans(s579,s108) % 0.19/0.40 | trans(s579,s109) % 0.19/0.40 | trans(s579,s110) % 0.19/0.40 | trans(s579,s111) % 0.19/0.40 | trans(s579,s112) % 0.19/0.40 | trans(s579,s113) % 0.19/0.40 | trans(s579,s114) % 0.19/0.40 | trans(s579,s115) % 0.19/0.40 | trans(s579,s116) % 0.19/0.40 | trans(s579,s117) % 0.19/0.40 | trans(s579,s118) % 0.19/0.40 | trans(s579,s119) % 0.19/0.40 | trans(s579,s120) % 0.19/0.40 | trans(s579,s121) % 0.19/0.40 | trans(s579,s122) % 0.19/0.40 | trans(s579,s123) % 0.19/0.40 | trans(s579,s124) % 0.19/0.40 | trans(s579,s125) % 0.19/0.40 | trans(s579,s126) % 0.19/0.40 | trans(s579,s127) % 0.19/0.40 | trans(s579,s128) % 0.19/0.40 | trans(s579,s129) % 0.19/0.40 | trans(s579,s130) % 0.19/0.40 | trans(s579,s131) % 0.19/0.40 | trans(s579,s132) % 0.19/0.40 | trans(s579,s133) % 0.19/0.40 | trans(s579,s134) % 0.19/0.40 | trans(s579,s135) % 0.19/0.40 | trans(s579,s136) % 0.19/0.40 | trans(s579,s137) % 0.19/0.40 | trans(s579,s138) % 0.19/0.40 | trans(s579,s139) % 0.19/0.40 | trans(s579,s140) % 0.19/0.40 | trans(s579,s141) % 0.19/0.40 | trans(s579,s142) % 0.19/0.40 | trans(s579,s143) % 0.19/0.40 | trans(s579,s144) % 0.19/0.40 | trans(s579,s145) % 0.19/0.40 | trans(s579,s146) % 0.19/0.40 | trans(s579,s147) % 0.19/0.40 | trans(s579,s148) % 0.19/0.40 | trans(s579,s149) % 0.19/0.40 | trans(s579,s150) % 0.19/0.40 | trans(s579,s151) % 0.19/0.40 | trans(s579,s152) % 0.19/0.40 | trans(s579,s153) % 0.19/0.40 | trans(s579,s154) % 0.19/0.40 | trans(s579,s155) % 0.19/0.40 | trans(s579,s156) % 0.19/0.40 | trans(s579,s157) % 0.19/0.40 | trans(s579,s158) % 0.19/0.40 | trans(s579,s159) % 0.19/0.40 | trans(s579,s160) % 0.19/0.40 | trans(s579,s161) % 0.19/0.40 | trans(s579,s162) % 0.19/0.40 | trans(s579,s163) % 0.19/0.40 | trans(s579,s164) % 0.19/0.40 | trans(s579,s165) % 0.19/0.40 | trans(s579,s166) % 0.19/0.40 | trans(s579,s167) % 0.19/0.40 | trans(s579,s168) % 0.19/0.40 | trans(s579,s169) % 0.19/0.40 | trans(s579,s170) % 0.19/0.40 | trans(s579,s171) % 0.19/0.40 | trans(s579,s172) % 0.19/0.40 | trans(s579,s173) % 0.19/0.40 | trans(s579,s174) % 0.19/0.40 | trans(s579,s175) % 0.19/0.40 | trans(s579,s176) % 0.19/0.40 | trans(s579,s177) % 0.19/0.40 | trans(s579,s178) % 0.19/0.40 | trans(s579,s179) % 0.19/0.40 | trans(s579,s180) % 0.19/0.40 | trans(s579,s181) % 0.19/0.40 | trans(s579,s182) % 0.19/0.40 | trans(s579,s183) % 0.19/0.40 | trans(s579,s184) % 0.19/0.40 | trans(s579,s185) % 0.19/0.40 | trans(s579,s186) % 0.19/0.40 | trans(s579,s187) % 0.19/0.40 | trans(s579,s188) % 0.19/0.40 | trans(s579,s189) % 0.19/0.40 | trans(s579,s190) % 0.19/0.40 | trans(s579,s191) % 0.19/0.40 | trans(s579,s192) % 0.19/0.40 | trans(s579,s193) % 0.19/0.40 | trans(s579,s194) % 0.19/0.40 | trans(s579,s195) % 0.19/0.40 | trans(s579,s196) % 0.19/0.40 | trans(s579,s197) % 0.19/0.40 | trans(s579,s198) % 0.19/0.40 | trans(s579,s199) % 0.19/0.40 | trans(s579,s200) % 0.19/0.40 | trans(s579,s201) % 0.19/0.40 | trans(s579,s202) % 0.19/0.40 | trans(s579,s203) % 0.19/0.40 | trans(s579,s204) % 0.19/0.40 | trans(s579,s205) % 0.19/0.40 | trans(s579,s206) % 0.19/0.40 | trans(s579,s207) % 0.19/0.40 | trans(s579,s208) % 0.19/0.40 | trans(s579,s209) % 0.19/0.40 | trans(s579,s210) % 0.19/0.40 | trans(s579,s211) % 0.19/0.40 | trans(s579,s212) % 0.19/0.40 | trans(s579,s213) % 0.19/0.40 | trans(s579,s214) % 0.19/0.40 | trans(s579,s215) % 0.19/0.40 | trans(s579,s216) % 0.19/0.40 | trans(s579,s217) % 0.19/0.40 | trans(s579,s218) % 0.19/0.40 | trans(s579,s219) % 0.19/0.40 | trans(s579,s220) % 0.19/0.40 | trans(s579,s221) % 0.19/0.40 | trans(s579,s222) % 0.19/0.40 | trans(s579,s223) % 0.19/0.40 | trans(s579,s224) % 0.19/0.40 | trans(s579,s225) % 0.19/0.40 | trans(s579,s226) % 0.19/0.40 | trans(s579,s227) % 0.19/0.40 | trans(s579,s228) % 0.19/0.40 | trans(s579,s229) % 0.19/0.40 | trans(s579,s230) % 0.19/0.40 | trans(s579,s231) % 0.19/0.40 | trans(s579,s232) % 0.19/0.40 | trans(s579,s233) % 0.19/0.40 | trans(s579,s234) % 0.19/0.40 | trans(s579,s235) % 0.19/0.40 | trans(s579,s236) % 0.19/0.40 | trans(s579,s237) % 0.19/0.40 | trans(s579,s238) % 0.19/0.40 | trans(s579,s239) % 0.19/0.40 | trans(s579,s240) % 0.19/0.40 | trans(s579,s241) % 0.19/0.40 | trans(s579,s242) % 0.19/0.40 | trans(s579,s243) % 0.19/0.40 | trans(s579,s244) % 0.19/0.40 | trans(s579,s245) % 0.19/0.40 | trans(s579,s246) % 0.19/0.40 | trans(s579,s247) % 0.19/0.40 | trans(s579,s248) % 0.19/0.40 | trans(s579,s249) % 0.19/0.40 | trans(s579,s250) % 0.19/0.40 | trans(s579,s251) % 0.19/0.40 | trans(s579,s252) % 0.19/0.40 | trans(s579,s253) % 0.19/0.40 | trans(s579,s254) % 0.19/0.40 | trans(s579,s255) % 0.19/0.40 | trans(s579,s256) % 0.19/0.40 | trans(s579,s257) % 0.19/0.40 | trans(s579,s258) % 0.19/0.40 | trans(s579,s259) % 0.19/0.40 | trans(s579,s260) % 0.19/0.40 | trans(s579,s261) % 0.19/0.40 | trans(s579,s262) % 0.19/0.40 | trans(s579,s263) % 0.19/0.40 | trans(s579,s264) % 0.19/0.40 | trans(s579,s265) % 0.19/0.40 | trans(s579,s266) % 0.19/0.40 | trans(s579,s267) % 0.19/0.40 | trans(s579,s268) % 0.19/0.40 | trans(s579,s269) % 0.19/0.40 | trans(s579,s270) % 0.19/0.40 | trans(s579,s271) % 0.19/0.40 | trans(s579,s272) % 0.19/0.40 | trans(s579,s273) % 0.19/0.40 | trans(s579,s274) % 0.19/0.40 | trans(s579,s275) % 0.19/0.40 | trans(s579,s276) % 0.19/0.40 | trans(s579,s277) % 0.19/0.40 | trans(s579,s278) % 0.19/0.40 | trans(s579,s279) % 0.19/0.40 | trans(s579,s280) % 0.19/0.40 | trans(s579,s281) % 0.19/0.40 | trans(s579,s282) % 0.19/0.40 | trans(s579,s283) % 0.19/0.40 | trans(s579,s284) % 0.19/0.40 | trans(s579,s285) % 0.19/0.40 | trans(s579,s286) % 0.19/0.40 | trans(s579,s287) % 0.19/0.40 | trans(s579,s288) % 0.19/0.40 | trans(s579,s289) % 0.19/0.40 | trans(s579,s290) % 0.19/0.40 | trans(s579,s291) % 0.19/0.40 | trans(s579,s292) % 0.19/0.40 | trans(s579,s293) % 0.19/0.40 | trans(s579,s294) % 0.19/0.40 | trans(s579,s295) % 0.19/0.40 | trans(s579,s296) % 0.19/0.40 | trans(s579,s297) % 0.19/0.40 | trans(s579,s298) % 0.19/0.40 | trans(s579,s299) % 0.19/0.40 | trans(s579,s300) % 0.19/0.40 | trans(s579,s301) % 0.19/0.40 | trans(s579,s302) % 0.19/0.40 | trans(s579,s303) % 0.19/0.40 | trans(s579,s304) % 0.19/0.40 | trans(s579,s305) % 0.19/0.40 | trans(s579,s306) % 0.19/0.40 | trans(s579,s307) % 0.19/0.40 | trans(s579,s308) % 0.19/0.40 | trans(s579,s309) % 0.19/0.40 | trans(s579,s310) % 0.19/0.40 | trans(s579,s311) % 0.19/0.40 | trans(s579,s312) % 0.19/0.40 | trans(s579,s313) % 0.19/0.40 | trans(s579,s314) % 0.19/0.40 | trans(s579,s315) % 0.19/0.40 | trans(s579,s316) % 0.19/0.40 | trans(s579,s317) % 0.19/0.40 | trans(s579,s318) % 0.19/0.40 | trans(s579,s319) % 0.19/0.40 | trans(s579,s320) % 0.19/0.40 | trans(s579,s321) % 0.19/0.40 | trans(s579,s322) % 0.19/0.40 | trans(s579,s323) % 0.19/0.40 | trans(s579,s324) % 0.19/0.40 | trans(s579,s325) % 0.19/0.40 | trans(s579,s326) % 0.19/0.40 | trans(s579,s327) % 0.19/0.40 | trans(s579,s328) % 0.19/0.40 | trans(s579,s329) % 0.19/0.40 | trans(s579,s330) % 0.19/0.40 | trans(s579,s331) % 0.19/0.40 | trans(s579,s332) % 0.19/0.40 | trans(s579,s333) % 0.19/0.40 | trans(s579,s334) % 0.19/0.40 | trans(s579,s335) % 0.19/0.40 | trans(s579,s336) % 0.19/0.40 | trans(s579,s337) % 0.19/0.40 | trans(s579,s338) % 0.19/0.40 | trans(s579,s339) % 0.19/0.40 | trans(s579,s340) % 0.19/0.40 | trans(s579,s341) % 0.19/0.40 | trans(s579,s342) % 0.19/0.40 | trans(s579,s343) % 0.19/0.40 | trans(s579,s344) % 0.19/0.40 | trans(s579,s345) % 0.19/0.40 | trans(s579,s346) % 0.19/0.40 | trans(s579,s347) % 0.19/0.40 | trans(s579,s348) % 0.19/0.40 | trans(s579,s349) % 0.19/0.40 | trans(s579,s350) % 0.19/0.40 | trans(s579,s351) % 0.19/0.40 | trans(s579,s352) % 0.19/0.40 | trans(s579,s353) % 0.19/0.40 | trans(s579,s354) % 0.19/0.40 | trans(s579,s355) % 0.19/0.40 | trans(s579,s356) % 0.19/0.40 | trans(s579,s357) % 0.19/0.40 | trans(s579,s358) % 0.19/0.40 | trans(s579,s359) % 0.19/0.40 | trans(s579,s360) % 0.19/0.40 | trans(s579,s361) % 0.19/0.40 | trans(s579,s362) % 0.19/0.40 | trans(s579,s363) % 0.19/0.40 | trans(s579,s364) % 0.19/0.40 | trans(s579,s365) % 0.19/0.40 | trans(s579,s366) % 0.19/0.40 | trans(s579,s367) % 0.19/0.40 | trans(s579,s368) % 0.19/0.40 | trans(s579,s369) % 0.19/0.40 | trans(s579,s370) % 0.19/0.40 | trans(s579,s371) % 0.19/0.40 | trans(s579,s372) % 0.19/0.40 | trans(s579,s373) % 0.19/0.40 | trans(s579,s374) % 0.19/0.40 | trans(s579,s375) % 0.19/0.40 | trans(s579,s376) % 0.19/0.40 | trans(s579,s377) % 0.19/0.40 | trans(s579,s378) % 0.19/0.40 | trans(s579,s379) % 0.19/0.40 | trans(s579,s380) % 0.19/0.40 | trans(s579,s381) % 0.19/0.40 | trans(s579,s382) % 0.19/0.40 | trans(s579,s383) % 0.19/0.40 | trans(s579,s384) % 0.19/0.40 | trans(s579,s385) % 0.19/0.40 | trans(s579,s386) % 0.19/0.40 | trans(s579,s387) % 0.19/0.40 | trans(s579,s388) % 0.19/0.40 | trans(s579,s389) % 0.19/0.40 | trans(s579,s390) % 0.19/0.40 | trans(s579,s391) % 0.19/0.40 | trans(s579,s392) % 0.19/0.40 | trans(s579,s393) % 0.19/0.40 | trans(s579,s394) % 0.19/0.40 | trans(s579,s395) % 0.19/0.41 | trans(s579,s396) % 0.19/0.41 | trans(s579,s397) % 0.19/0.41 | trans(s579,s398) % 0.19/0.41 | trans(s579,s399) % 0.19/0.41 | trans(s579,s400) % 0.19/0.41 | trans(s579,s401) % 0.19/0.41 | trans(s579,s402) % 0.19/0.41 | trans(s579,s403) % 0.19/0.41 | trans(s579,s404) % 0.19/0.41 | trans(s579,s405) % 0.19/0.41 | trans(s579,s406) % 0.19/0.41 | trans(s579,s407) % 0.19/0.41 | trans(s579,s408) % 0.19/0.41 | trans(s579,s409) % 0.19/0.41 | trans(s579,s410) % 0.19/0.41 | trans(s579,s411) % 0.19/0.41 | trans(s579,s412) % 0.19/0.41 | trans(s579,s413) % 0.19/0.41 | trans(s579,s414) % 0.19/0.41 | trans(s579,s415) % 0.19/0.41 | trans(s579,s416) % 0.19/0.41 | trans(s579,s417) % 0.19/0.41 | trans(s579,s418) % 0.19/0.41 | trans(s579,s419) % 0.19/0.41 | trans(s579,s420) % 0.19/0.41 | trans(s579,s421) % 0.19/0.41 | trans(s579,s422) % 0.19/0.41 | trans(s579,s423) % 0.19/0.41 | trans(s579,s424) % 0.19/0.41 | trans(s579,s425) % 0.19/0.41 | trans(s579,s426) % 0.19/0.41 | trans(s579,s427) % 0.19/0.41 | trans(s579,s428) % 0.19/0.41 | trans(s579,s429) % 0.19/0.41 | trans(s579,s430) % 0.19/0.41 | trans(s579,s431) % 0.19/0.41 | trans(s579,s432) % 0.19/0.41 | trans(s579,s433) % 0.19/0.41 | trans(s579,s434) % 0.19/0.41 | trans(s579,s435) % 0.19/0.41 | trans(s579,s436) % 0.19/0.41 | trans(s579,s437) % 0.19/0.41 | trans(s579,s438) % 0.19/0.41 | trans(s579,s439) % 0.19/0.41 | trans(s579,s440) % 0.19/0.41 | trans(s579,s441) % 0.19/0.41 | trans(s579,s442) % 0.19/0.41 | trans(s579,s443) % 0.19/0.41 | trans(s579,s444) % 0.19/0.41 | trans(s579,s445) % 0.19/0.41 | trans(s579,s446) % 0.19/0.41 | trans(s579,s447) % 0.19/0.41 | trans(s579,s448) % 0.19/0.41 | trans(s579,s449) % 0.19/0.41 | trans(s579,s450) % 0.19/0.41 | trans(s579,s451) % 0.19/0.41 | trans(s579,s452) % 0.19/0.41 | trans(s579,s453) % 0.19/0.41 | trans(s579,s454) % 0.19/0.41 | trans(s579,s455) % 0.19/0.41 | trans(s579,s456) % 0.19/0.41 | trans(s579,s457) % 0.19/0.41 | trans(s579,s458) % 0.19/0.41 | trans(s579,s459) % 0.19/0.41 | trans(s579,s460) % 0.19/0.41 | trans(s579,s461) % 0.19/0.41 | trans(s579,s462) % 0.19/0.41 | trans(s579,s463) % 0.19/0.41 | trans(s579,s464) % 0.19/0.41 | trans(s579,s465) % 0.19/0.41 | trans(s579,s466) % 0.19/0.41 | trans(s579,s467) % 0.19/0.41 | trans(s579,s468) % 0.19/0.41 | trans(s579,s469) % 0.19/0.41 | trans(s579,s470) % 0.19/0.41 | trans(s579,s471) % 0.19/0.41 | trans(s579,s472) % 0.19/0.41 | trans(s579,s473) % 0.19/0.41 | trans(s579,s474) % 0.19/0.41 | trans(s579,s475) % 0.19/0.41 | trans(s579,s476) % 0.19/0.41 | trans(s579,s477) % 0.19/0.41 | trans(s579,s478) % 0.19/0.41 | trans(s579,s479) % 0.19/0.41 | trans(s579,s480) % 0.19/0.41 | trans(s579,s481) % 0.19/0.41 | trans(s579,s482) % 0.19/0.41 | trans(s579,s483) % 0.19/0.41 | trans(s579,s484) % 0.19/0.41 | trans(s579,s485) % 0.19/0.41 | trans(s579,s486) % 0.19/0.41 | trans(s579,s487) % 0.19/0.41 | trans(s579,s488) % 0.19/0.41 | trans(s579,s489) % 0.19/0.41 | trans(s579,s490) % 0.19/0.41 | trans(s579,s491) % 0.19/0.41 | trans(s579,s492) % 0.19/0.41 | trans(s579,s493) % 0.19/0.41 | trans(s579,s494) % 0.19/0.41 | trans(s579,s495) % 0.19/0.41 | trans(s579,s496) % 0.19/0.41 | trans(s579,s497) % 0.19/0.41 | trans(s579,s498) % 0.19/0.41 | ***HERE*** trans(s579,s499) % 0.19/0.41 | trans(s579,s500) % 0.19/0.41 | trans(s579,s501) % 0.19/0.41 | trans(s579,s502) % 0.19/0.41 | trans(s579,s503) % 0.19/0.41 | trans(s579,s504) % 0.19/0.41 | trans(s579,s505) % 0.19/0.41 | trans(s579,s506) % 0.19/0.41 | trans(s579,s507) % 0.19/0.41 | trans(s579,s508) % 0.19/0.41 | trans(s579,s509) % 0.19/0.41 | trans(s579,s510) % 0.19/0.41 | trans(s579,s511) % 0.19/0.41 | trans(s579,s512) % 0.19/0.41 | trans(s579,s513) % 0.19/0.41 | trans(s579,s514) % 0.19/0.41 | trans(s579,s515) % 0.19/0.41 | trans(s579,s516) % 0.19/0.41 | trans(s579,s517) % 0.19/0.41 | trans(s579,s518) % 0.19/0.41 | trans(s579,s519) % 0.19/0.41 | trans(s579,s520) % 0.19/0.41 | trans(s579,s521) % 0.19/0.41 | trans(s579,s522) % 0.19/0.41 | trans(s579,s523) % 0.19/0.41 | trans(s579,s524) % 0.19/0.41 | trans(s579,s525) % 0.19/0.41 | trans(s579,s526) % 0.19/0.41 | trans(s579,s527) % 0.19/0.41 | trans(s579,s528) % 0.19/0.41 | trans(s579,s529) % 0.19/0.41 | trans(s579,s530) % 0.19/0.41 | trans(s579,s531) % 0.19/0.41 | trans(s579,s532) % 0.19/0.41 | trans(s579,s533) % 0.19/0.41 | trans(s579,s534) % 0.19/0.41 | trans(s579,s535) % 0.19/0.41 | trans(s579,s536) % 0.19/0.41 | trans(s579,s537) % 0.19/0.41 | trans(s579,s538) % 0.19/0.41 | trans(s579,s539) % 0.19/0.41 | trans(s579,s540) % 0.19/0.41 | trans(s579,s541) % 0.19/0.41 | trans(s579,s542) % 0.19/0.41 | trans(s579,s543) % 0.19/0.41 | trans(s579,s544) % 0.19/0.41 | trans(s579,s545) % 0.19/0.41 | trans(s579,s546) % 0.19/0.41 | trans(s579,s547) % 0.19/0.41 | trans(s579,s548) % 0.19/0.41 | trans(s579,s549) % 0.19/0.41 | trans(s579,s550) % 0.19/0.41 | trans(s579,s551) % 0.19/0.41 | trans(s579,s552) % 0.19/0.41 | trans(s579,s553) % 0.19/0.41 | trans(s579,s554) % 0.19/0.41 | trans(s579,s555) % 0.19/0.41 | trans(s579,s556) % 0.19/0.41 | trans(s579,s557) % 0.19/0.41 | trans(s579,s558) % 0.19/0.41 | trans(s579,s559) % 0.19/0.41 | trans(s579,s560) % 0.19/0.41 | trans(s579,s561) % 0.19/0.41 | trans(s579,s562) % 0.19/0.41 | trans(s579,s563) % 0.19/0.41 | trans(s579,s564) % 0.19/0.41 | trans(s579,s565) % 0.19/0.41 | trans(s579,s566) % 0.19/0.41 | trans(s579,s567) % 0.19/0.41 | trans(s579,s568) % 0.19/0.41 | trans(s579,s569) % 0.19/0.41 | trans(s579,s570) % 0.19/0.41 | trans(s579,s571) % 0.19/0.41 | trans(s579,s572) % 0.19/0.41 | trans(s579,s573) % 0.19/0.41 | trans(s579,s574) % 0.19/0.41 | trans(s579,s575) % 0.19/0.41 | trans(s579,s576) % 0.19/0.41 | trans(s579,s577) % 0.19/0.41 | trans(s579,s578) % 0.19/0.41 | trans(s579,s579) ). % 0.19/0.41 % 0.19/0.41 ======= end of input processing ======= % 0.19/0.41 % 0.19/0.41 1 input errors were found. % 0.19/0.41 % 0.19/0.41 1 input errors were found. %------------------------------------------------------------------------------