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