1#!/usr/bin/env python2.7 2# ---------------------------------- 3# 4# e_scheduler.py 5# 6# Determine the problem class of a problem and run E using a suitable 7# schedule. 8# 9# Version history: 10# 1.0 Mon May 8 23:34:30 CEST 2006 11# Draft version 12 13""" 14e_scheduler.py 15 16Usage: e_scheduler.py [Options] <tptpfile> 17 18Read a TPTP input file, determine the problem class, select a suitable 19schedule and run E accordingly. 20 21Restriction: The initial version only reads a fixed format and does 22not support extra options. 23 24Options: 25 26-h 27 Print this information and exit. 28 29Copyright 2006 Stephan Schulz, schulz@eprover.org 30 31This program is free software; you can redistribute it and/or modify 32it under the terms of the GNU General Public License as published by 33the Free Software Foundation; either version 2 of the License, or 34(at your option) any later version. 35 36This program is distributed in the hope that it will be useful, 37but WITHOUT ANY WARRANTY; without even the implied warranty of 38MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 39GNU General Public License for more details. 40 41You should have received a copy of the GNU General Public License 42along with this program ; if not, write to the Free Software 43Foundation, Inc., 59 Temple Place, Suite 330, Boston, 44MA 02111-1307 USA 45 46The original copyright holder can be contacted as 47 48Dr. Stephan Schulz 49Hirschstr. 35 5076144 Karlsruhe 51Germany 52 53or via email (address above). 54""" 55 56 57import sys 58import re 59import string 60import os 61import resource 62 63 64# If necessary, change this to point to your E executable! 65 66classify_command = "classify_problem -ca-aa-aaaaaa-a --tstp-in --ax-some-limit=46 --ax-many-limit=205 --lit-some-limit=212 --lit-many-limit=620 --term-medium-limit=163 --term-large-limit=2270 --farity-medium-limit=4 --farity-large-limit=29 --gpc-few-limit=2 --gpc-many-limit=5 " 67 68colon_pattern = re.compile("\s*:\s*") 69cl_error_exception ="Problem interpreting classify_problem output" 70 71 72def get_options(argv=sys.argv[1:]): 73 """ 74 Filter argument list for arguments starting with a -. 75 """ 76 options = filter(lambda x:x[0:1]=="-", argv) 77 return options 78 79def get_args(argv=sys.argv[1:]): 80 """ 81 Filter argument list for real arguments. 82 """ 83 files = filter(lambda x:x[0:1]!="-", argv) 84 return files 85 86 87def get_problem_class(filename): 88 """ 89 Run classify_problem (from the E distribution) to find out the 90 class of a problem. 91 """ 92 p = os.popen(classify_command+filename, "r"); 93 clres = p.readlines() 94 p.close() 95 res = None 96 97 # There really should be only one line, but let's err on the safe 98 # side anyways... 99 try: 100 for line in clres: 101 if line.startswith(filename): 102 tmp = colon_pattern.split(line) 103 if len(tmp)!=3: 104 raise cl_error_exception 105 res = "CLASS_"+tmp[2][:-1] 106 break; 107 if not res: 108 raise cl_error_exception 109 110 except cl_error_exception: 111 sys.exit("Could not get class of " +filename); 112 113 return res 114strat_options = { 115"protokoll_G-E--_001_B31_F1_PI_AE_S4_CS_OS_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --oriented-simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(10*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 116 117"protokoll_G-E--_001_K18_F1_AE_S4_CS_OS_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --oriented-simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(10*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 118 119"protokoll_G-E--_001_K18_F1_PI_AE_S4_CS_OS_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --oriented-simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(10*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 120 121"protokoll_G-E--_001_K18_F1_PI_AE_S4_CS_OS_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --oriented-simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(10*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 122 123"protokoll_G-E--_001_K18_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(10*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 124 125"protokoll_G-E--_001_K18_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(10*ConjectureSymbolWeight(ConstPrio,10,10,5,5,5,1.5,1.5,1.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 126 127"protokoll_G-E--_002_K18_F1_AE_S4_CS_OS_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --oriented-simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 128 129"protokoll_G-E--_002_K18_F1_PI_AE_S4_CS_OS_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --oriented-simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 130 131"protokoll_G-E--_002_K18_F1_PI_AE_S4_CS_OS_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --oriented-simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 132 133"protokoll_G-E--_003_K18_F1_AE_S4_CS_OS_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --oriented-simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.2, 100, 100, 100, 100, 1.5, 1.5, 1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 134 135"protokoll_G-E--_003_K18_F1_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.2, 100, 100, 100, 100, 1.5, 1.5, 1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 136 137"protokoll_G-E--_003_K18_F1_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.2, 100, 100, 100, 100, 1.5, 1.5, 1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 138 139"protokoll_G-E--_003_K18_F1_PI_AE_S4_CS_OS_S0Y":" --definitional-cnf=24 --tstp-in --prefer-initial-clauses --split-aggressive --split-clauses=4 --oriented-simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.2, 100, 100, 100, 100, 1.5, 1.5, 1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 140 141"protokoll_G-E--_003_K18_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --prefer-initial-clauses --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.2, 100, 100, 100, 100, 1.5, 1.5, 1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 142 143"protokoll_G-E--_003_K18_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --prefer-initial-clauses --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.2, 100, 100, 100, 100, 1.5, 1.5, 1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 144 145"protokoll_G-E--_004_K18_F1_AE_S4_CS_OS_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --oriented-simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.7, 100, 100, 100, 100, 1.5, 1.5, 1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 146 147"protokoll_G-E--_004_K18_F1_PI_AE_S4_CS_OS_S0Y":" --definitional-cnf=24 --tstp-in --prefer-initial-clauses --split-aggressive --split-clauses=4 --oriented-simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.7, 100, 100, 100, 100, 1.5, 1.5, 1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 148 149"protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --oriented-simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.5, 100, 100, 100, 50, 1.5, 1.5, 1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 150 151"protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.5, 100, 100, 100, 50, 1.5, 1.5, 1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 152 153"protokoll_G-E--_006_K18_F1_PI_AE_S4_CS_OS_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --oriented-simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.5, 100, 100, 100, 50, 1.5, 1.5, 1.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 154 155"protokoll_G-E--_006_K18_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.5, 100, 100, 100, 50, 1.5, 1.5, 1.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 156 157"protokoll_G-E--_006_K18_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.5, 100, 100, 100, 50, 1.5, 1.5, 1.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 158 159"protokoll_G-E--_006_K19_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvmodfreqrankmax0 -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.5, 100, 100, 100, 50, 1.5, 1.5, 1.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 160 161"protokoll_G-E--_007_K18_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.2, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 162 163"protokoll_G-E--_008_B07_F1_PI_AE_Q4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-reuse-defs --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 164 165"protokoll_G-E--_008_B31_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 166 167"protokoll_G-E--_008_K18_F1_PI_AE_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 168 169"protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-reuse-defs --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 170 171"protokoll_G-E--_008_K18_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 172 173"protokoll_G-E--_008_K18_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 174 175"protokoll_G-E--_010_B02_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Garity -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 176 177"protokoll_G-E--_010_B07_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 178 179"protokoll_G-E--_010_B31_F1_PI_AE_S4_CS_SP_S00":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --prefer-initial-clauses --destructive-er -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WNoSelection -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 180 181"protokoll_G-E--_010_B31_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --prefer-initial-clauses --destructive-er -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 182 183"protokoll_G-E--_010_B31_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --prefer-initial-clauses --destructive-er -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 184 185"protokoll_G-E--_010_K02_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -wconstant -Garity -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 186"protokoll_G-E--_010_K04_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -warity -Garity -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 187 188"protokoll_G-E--_010_K07_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -wconstant -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 189 190"protokoll_G-E--_010_K08_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -wmodarity -Garity -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 191"protokoll_G-E--_010_K09_F1_PI_AE_Q4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-reuse-defs --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -waritysquared -Garity -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 192 193"protokoll_G-E--_010_K09_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -waritysquared -Garity -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 194 195"protokoll_G-E--_010_K18_F1_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 196 197"protokoll_G-E--_010_K18_F1_PI_AE_CS_OS_S0Y":" --definitional-cnf=24 --tstp-in --oriented-simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 198 199"protokoll_G-E--_010_K18_F1_PI_AE_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 200 201"protokoll_G-E--_010_K18_F1_PI_AE_S4_AB_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr-aggressive --backward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 202 203"protokoll_G-E--_010_K18_F1_PI_AE_S4_AS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr-aggressive --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 204 205"protokoll_G-E--_010_K18_F1_PI_AE_S4_CS_SP_S00":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WNoSelection -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 206 207"protokoll_G-E--_010_K18_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --prefer-initial-clauses --destructive-er -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 208 209"protokoll_G-E--_010_K18_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 210 211"protokoll_G-E--_010_K18_F1_PI_AE_S4_CS_SP_S3S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHPExceptUniqMaxHorn -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 212 213"protokoll_G-E--_010_K18_F1_PI_AE_S4_CS_SP_S3T":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WPSelectNewComplexAHPExceptUniqMaxHorn -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 214 215"protokoll_G-E--_010_K18_F1_PI_AE_S4_CS_SP_SNG":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --prefer-initial-clauses --destructive-er -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WNoGeneration -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 216 217"protokoll_G-E--_010_K18_F2_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F2 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 218 219"protokoll_G-E--_010_K31_F1_PI_AE_S4_CS_SP_S00":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --prefer-initial-clauses --destructive-er -winvfreqrank -c1 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WNoSelection -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 220 221"protokoll_G-E--_010_K31_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --prefer-initial-clauses --destructive-er -winvfreqrank -c1 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 222 223"protokoll_G-E--_010_K31_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --prefer-initial-clauses --destructive-er -winvfreqrank -c1 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 224 225"protokoll_G-E--_010_K32_F1_PI_AE_Q4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-reuse-defs --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -wconstant -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 226 227"protokoll_G-E--_010_K32_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -wconstant -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 228 229"protokoll_G-E--_010_K32_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -wconstant -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(4*ConjectureRelativeSymbolWeight(SimulateSOS,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*ConjectureRelativeSymbolWeight(PreferNonGoals,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 230"protokoll_G-E--_011_B31_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(7*ConjectureRelativeSymbolWeight(ConstPrio,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 231 232"protokoll_G-E--_011_K18_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(7*ConjectureRelativeSymbolWeight(ConstPrio,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 233 234"protokoll_G-E--_011_K18_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(7*ConjectureRelativeSymbolWeight(ConstPrio,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 235 236"protokoll_G-E--_012_B31_F1_PI_AE_Q4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-reuse-defs --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(7*ConjectureRelativeSymbolWeight(ConstPrio,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 237 238"protokoll_G-E--_012_B31_F1_PI_AE_Q4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-reuse-defs --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(7*ConjectureRelativeSymbolWeight(ConstPrio,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 239 240"protokoll_G-E--_012_B31_F1_PI_AE_R4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-reuse-defs --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(7*ConjectureRelativeSymbolWeight(ConstPrio,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 241 242"protokoll_G-E--_012_B31_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(7*ConjectureRelativeSymbolWeight(ConstPrio,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 243 244"protokoll_G-E--_012_B31_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(7*ConjectureRelativeSymbolWeight(ConstPrio,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 245 246"protokoll_G-E--_012_K18_F1_PI_AE_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(7*ConjectureRelativeSymbolWeight(ConstPrio,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 247 248"protokoll_G-E--_012_K18_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(7*ConjectureRelativeSymbolWeight(ConstPrio,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 249 250"protokoll_G-E--_012_K18_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(7*ConjectureRelativeSymbolWeight(ConstPrio,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 251 252"protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(7*ConjectureRelativeSymbolWeight(ConstPrio,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 253 254"protokoll_G-E--_012_K33_F1_PI_AE_Q4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-reuse-defs --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -wprecedence -c1 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(7*ConjectureRelativeSymbolWeight(ConstPrio,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 255 256"protokoll_G-E--_012_K33_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -wprecedence -c1 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(7*ConjectureRelativeSymbolWeight(ConstPrio,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 257 258"protokoll_G-E--_012_K33_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -wprecedence -c1 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(7*ConjectureRelativeSymbolWeight(ConstPrio,0.5, 100, 100, 100, 100, 1.5, 1.5, 1),3*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 259 260"protokoll_G-E--_020_K18_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.5, 100, 100, 100, 50, 1.5, 0.5, 1.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 261 262"protokoll_G-E--_020_K18_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.5, 100, 100, 100, 50, 1.5, 0.5, 1.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 263 264"protokoll_G-E--_021_B31_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS, 100,100,100,50,50,0,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,0,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 265 266"protokoll_G-E--_021_K07_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -wconstant -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS, 100,100,100,50,50,0,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,0,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 267 268"protokoll_G-E--_021_K18_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS, 100,100,100,50,50,0,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,0,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 269 270"protokoll_G-E--_021_K18_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS, 100,100,100,50,50,0,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,0,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 271 272"protokoll_G-E--_021_K31_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS, 100,100,100,50,50,0,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,0,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 273 274"protokoll_G-E--_021_K31_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS, 100,100,100,50,50,0,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,0,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 275 276"protokoll_G-E--_021_K32_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -wconstant -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS, 100,100,100,50,50,0,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,0,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 277 278"protokoll_G-E--_021_K32_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -wconstant -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS, 100,100,100,50,50,0,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,0,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 279 280"protokoll_G-E--_022_K07_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -wconstant -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,5000,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1000,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 281 282"protokoll_G-E--_022_K18_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,5000,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1000,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 283 284"protokoll_G-E--_023_K07_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -wconstant -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,5000,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,5000,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 285 286"protokoll_G-E--_024_B07_F1_PI_AE_Q4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-reuse-defs --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,50,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1000,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 287 288"protokoll_G-E--_024_B31_F1_PI_AE_Q4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-reuse-defs --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,50,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1000,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 289 290"protokoll_G-E--_024_B31_F1_PI_AE_Q4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-reuse-defs --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,50,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1000,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 291 292"protokoll_G-E--_024_K02_F1_PI_AE_Q4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-reuse-defs --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -wconstant -Garity -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,50,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1000,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 293 294"protokoll_G-E--_024_K07_F1_PI_AE_Q4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-reuse-defs --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -wconstant -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,50,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1000,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 295 296"protokoll_G-E--_024_K07_F1_PI_AE_Q4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-reuse-defs --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -wconstant -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,50,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1000,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 297 298"protokoll_G-E--_024_K07_F1_PI_AE_R4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-reuse-defs --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -wconstant -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,50,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1000,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 299 300"protokoll_G-E--_024_K07_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -wconstant -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,50,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1000,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 301 302"protokoll_G-E--_024_K18_F1_PI_AE_Q4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-reuse-defs --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,50,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1000,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 303 304"protokoll_G-E--_025_B31_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 305 306"protokoll_G-E--_025_K07_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -wconstant -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,5000,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,100,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 307 308"protokoll_G-E--_025_K18_F1_PI_AE_CS_SP_S00":" --definitional-cnf=24 --tstp-in --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 309 310"protokoll_G-E--_025_K18_F1_PI_AE_R12_CS_SP_S00":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=12 --split-reuse-defs --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 311 312"protokoll_G-E--_025_K18_F1_PI_AE_S4_CS_SP_S00":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 313 314"protokoll_G-E--_025_K18_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 315 316"protokoll_G-E--_025_K18_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 317 318"protokoll_G-E--_025_K31_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 319 320"protokoll_G-E--_025_K31_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 321 322"protokoll_G-E--_025_K33_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -wprecedence -c1 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 323 324"protokoll_G-E--_026_K18_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(PreferGoals,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 325 326"protokoll_G-E--_027_K18_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,20,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 327 328"protokoll_G-E--_028_K18_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,10,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 329 330"protokoll_G-E--_029_B31_F1_PI_AE_Q4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-reuse-defs --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 331 332"protokoll_G-E--_029_B31_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 333 334"protokoll_G-E--_029_B31_F1_PI_AE_T4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 335 336"protokoll_G-E--_029_K02_F1_PI_AE_R4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -wconstant -Garity -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 337 338"protokoll_G-E--_029_K07_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -wconstant -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 339 340"protokoll_G-E--_029_K18_F1_PI_AE_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 341 342"protokoll_G-E--_029_K18_F1_PI_AE_IO_R4_CS_SP_S0Y":" --definitional-cnf=24 --sos-uses-input-types --tstp-in --split-aggressive --split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 343 344"protokoll_G-E--_029_K18_F1_PI_AE_Q12_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-clauses=12 --split-reuse-defs --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 345 346"protokoll_G-E--_029_K18_F1_PI_AE_Q2_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-clauses=2 --split-reuse-defs --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 347 348"protokoll_G-E--_029_K18_F1_PI_AE_Q4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 349 350"protokoll_G-E--_029_K18_F1_PI_AE_Q4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-reuse-defs --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 351 352"protokoll_G-E--_029_K18_F1_PI_AE_Q8_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-clauses=8 --split-reuse-defs --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 353 354"protokoll_G-E--_029_K18_F1_PI_AE_R12_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=12 --split-reuse-defs --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 355 356"protokoll_G-E--_029_K18_F1_PI_AE_R4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 357 358"protokoll_G-E--_029_K18_F1_PI_AE_R7_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=7 --split-reuse-defs --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 359 360"protokoll_G-E--_029_K18_F1_PI_AE_R8_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-reuse-defs --split-aggressive --split-clauses=8 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 361 362"protokoll_G-E--_029_K18_F1_PI_AE_S12_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=12 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 363 364"protokoll_G-E--_029_K18_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 365 366"protokoll_G-E--_029_K18_F1_PI_AE_S4_CS_SP_S0Y_ne":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 367 368"protokoll_G-E--_029_K18_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 369 370"protokoll_G-E--_029_K18_F1_PI_AE_S8_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=8 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 371 372"protokoll_G-E--_029_K18_F1_PI_AE_SU_R4_CS_SP_S0Y":" --definitional-cnf=24 --simplify-with-unprocessed-units --tstp-in --split-aggressive --split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,10,50,1.5,1.5,1),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 373 374"protokoll_G-E--_030_K16_F1_PI_AE_CS_S4_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --destructive-er-aggressive --destructive-er --split-aggressive --split-clauses=4 -WSelectMaxLComplexAvoidPosPred --prefer-initial-clauses --forward-context-sr -wprecedence -c1 -Ginvfreq --tstp-in -H'(10*ConjectureGeneralSymbolWeight(PreferGroundGoals,100,100,100,50,50,10,50,1.5,1.5,1),1*Clauseweight(ConstPrio,1,1,1),1*Clauseweight(ByCreationDate,2,1,0.8))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 375 376"protokoll_G-E--_030_K16_F1_PI_AE_CS_S4_SP_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --simul-paramod --destructive-er-aggressive --destructive-er --split-aggressive --split-clauses=4 -WSelectMaxLComplexAvoidPosPred --prefer-initial-clauses --forward-context-sr -wprecedence -c1 -Ginvfreq --tstp-in -H'(10*ConjectureGeneralSymbolWeight(PreferGroundGoals,100,100,100,50,50,10,50,1.5,1.5,1),1*Clauseweight(ConstPrio,1,1,1),1*Clauseweight(ByCreationDate,2,1,0.8))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 377 378"protokoll_G-E--_030_K18_F1_PI_AE_CS_S4_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --destructive-er-aggressive --destructive-er --split-aggressive --split-clauses=4 -WSelectMaxLComplexAvoidPosPred --prefer-initial-clauses --forward-context-sr -winvfreqrank -c1 -Ginvfreq --tstp-in -H'(10*ConjectureGeneralSymbolWeight(PreferGroundGoals,100,100,100,50,50,10,50,1.5,1.5,1),1*Clauseweight(ConstPrio,1,1,1),1*Clauseweight(ByCreationDate,2,1,0.8))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 379 380"protokoll_G-E--_030_K18_F1_PI_AE_CS_S4_SP_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --destructive-er-aggressive --destructive-er --simul-paramod --split-aggressive --split-clauses=4 -WSelectMaxLComplexAvoidPosPred --prefer-initial-clauses --forward-context-sr -winvfreqrank -c1 -Ginvfreq --tstp-in -H'(10*ConjectureGeneralSymbolWeight(PreferGroundGoals,100,100,100,50,50,10,50,1.5,1.5,1),1*Clauseweight(ConstPrio,1,1,1),1*Clauseweight(ByCreationDate,2,1,0.8))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 381 382"protokoll_G-E--_031_K18_F1_PI_AE_CS_S4_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --destructive-er-aggressive --destructive-er --split-aggressive --split-clauses=4 -WSelectMaxLComplexAvoidPosPred --prefer-initial-clauses --forward-context-sr -winvfreqrank -c1 -Ginvfreq --tstp-in -H'(10*ConjectureGeneralSymbolWeight(PreferGroundGoals,100,100,100,50,50,10,100,1.5,1.5,1),1*Clauseweight(ConstPrio,1,1,1),1*Clauseweight(ByCreationDate,2,1,0.8))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 383 384"protokoll_G-E--_032_B31_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,20,50,1.5,1.5,1),5*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 385 386"protokoll_G-E--_032_K18_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,20,50,1.5,1.5,1),5*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 387 388"protokoll_G-E--_032_K18_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(4*ConjectureGeneralSymbolWeight(SimulateSOS,100,100,100,50,50,20,50,1.5,1.5,1),5*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 389 390"protokoll_G-E--_033_K18_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*Defaultweight(SimulateSOS),5*ConjectureGeneralSymbolWeight(PreferNonGoals,100,100,100,50,50,1,100,1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 391 392"protokoll_G-E--_040_K18_F1_PI_AE_Q4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-reuse-defs --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.05, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 393 394"protokoll_G-E--_040_K18_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.05, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 395 396"protokoll_G-E--_041_K18_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),3*ConjectureRelativeSymbolWeight(ConstPrio,0.3, 100, 100, 100, 100, 2.5, 1, 1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 397 398"protokoll_G-E--_042_K18_F1_PI_AE_R4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(20*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*Refinedweight(PreferNonGoals,2,1,2,3,0.8),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 399 400"protokoll_G-E--_042_K18_F1_PI_AE_R7_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=7 --split-reuse-defs --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(20*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*Refinedweight(PreferNonGoals,2,1,2,3,0.8),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 401 402"protokoll_G-E--_042_K18_F1_PI_AE_R8_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=8 --split-reuse-defs --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(20*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*Refinedweight(PreferNonGoals,2,1,2,3,0.8),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 403 404"protokoll_G-E--_042_K18_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(20*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*Refinedweight(PreferNonGoals,2,1,2,3,0.8),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 405 406"protokoll_G-E--_042_K18_F1_PI_AE_S8_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=8 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(20*ConjectureRelativeSymbolWeight(ConstPrio,0.1, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*Refinedweight(PreferNonGoals,2,1,2,3,0.8),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 407 408"protokoll_G-E--_044_B31_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --simul-paramod --forward-context-sr --split-aggressive --split-clauses=4 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP --tstp-in -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),2*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 409 410"protokoll_G-E--_044_K18_F1_PI_AE_S4_CS_OS_S1S":" --definitional-cnf=24 --oriented-simul-paramod --forward-context-sr --split-aggressive --split-clauses=4 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectComplexAHP --tstp-in -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),2*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 411 412"protokoll_G-E--_044_K18_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --simul-paramod --forward-context-sr --split-aggressive --split-clauses=4 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP --tstp-in -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),2*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 413 414"protokoll_G-E--_044_K18_F1_PI_AE_S4_S0Y":" --definitional-cnf=24 --split-aggressive --split-clauses=4 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred --tstp-in -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),2*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 415 416"protokoll_G-E--_044_K18_F1_PI_AE_S4_S1S":" --definitional-cnf=24 --split-aggressive --split-clauses=4 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectComplexAHP --tstp-in -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),2*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 417 418"protokoll_G-E--_044_K18_F1_PI_AE_S4_S2S":" --definitional-cnf=24 --split-aggressive --split-clauses=4 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP --tstp-in -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),2*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 419 420"protokoll_G-E--_044_K18_F1_PI_AE_S4_SP_S2S":" --definitional-cnf=24 --split-aggressive --split-clauses=4 --simul-paramod --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP --tstp-in -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),2*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 421 422"protokoll_G-E--_045_B07_F1_PI_AE_Q4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-reuse-defs --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 423 424"protokoll_G-E--_045_B07_F1_PI_AE_Q4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-reuse-defs --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 425 426"protokoll_G-E--_045_B07_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 427 428"protokoll_G-E--_045_B31_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 429 430"protokoll_G-E--_045_B31_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 431 432"protokoll_G-E--_045_B31_F2_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -tLPO4 -Ginvfreqconstmin -F2 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 433 434"protokoll_G-E--_045_K07_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -wconstant -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 435 436"protokoll_G-E--_045_K18_F1_PI_AE_CS_OS_S00":" --definitional-cnf=24 --tstp-in --oriented-simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WNoSelection -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 437 438"protokoll_G-E--_045_K18_F1_PI_AE_CS_OS_S0S":" --definitional-cnf=24 --tstp-in --oriented-simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectComplexG -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 439 440"protokoll_G-E--_045_K18_F1_PI_AE_CS_OS_S0Y":" --definitional-cnf=24 --tstp-in --oriented-simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 441 442"protokoll_G-E--_045_K18_F1_PI_AE_CS_OS_S1S":" --definitional-cnf=24 --tstp-in --oriented-simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectComplexAHP -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 443 444"protokoll_G-E--_045_K18_F1_PI_AE_CS_OS_S2S":" --definitional-cnf=24 --tstp-in --oriented-simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 445 446"protokoll_G-E--_045_K18_F1_PI_AE_CS_S00":" --definitional-cnf=24 --tstp-in --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WNoSelection -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 447 448"protokoll_G-E--_045_K18_F1_PI_AE_CS_S4_SP_S00":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WNoSelection -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 449 450"protokoll_G-E--_045_K18_F1_PI_AE_CS_SP_S00":" --definitional-cnf=24 --tstp-in --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WNoSelection -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 451 452"protokoll_G-E--_045_K18_F1_PI_AE_CS_SP_S0S":" --definitional-cnf=24 --tstp-in --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectComplexG -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 453 454"protokoll_G-E--_045_K18_F1_PI_AE_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 455 456"protokoll_G-E--_045_K18_F1_PI_AE_CS_SP_S1S":" --definitional-cnf=24 --tstp-in --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectComplexAHP -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 457 458"protokoll_G-E--_045_K18_F1_PI_AE_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 459 460"protokoll_G-E--_045_K18_F1_PI_AE_Q4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-reuse-defs --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 461 462"protokoll_G-E--_045_K18_F1_PI_AE_Q7_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --simul-paramod --split-clauses=8 --split-reuse-defs --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 463 464"protokoll_G-E--_045_K18_F1_PI_AE_S4_CS_OS_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --oriented-simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 465 466"protokoll_G-E--_045_K18_F1_PI_AE_S4_CS_OS_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --oriented-simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 467 468"protokoll_G-E--_045_K18_F1_PI_AE_S4_CS_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 469 470"protokoll_G-E--_045_K18_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 471 472"protokoll_G-E--_045_K18_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectNewComplexAHP -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 473 474"protokoll_G-E--_045_K18_F1_PI_AE_S4_OS_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --oriented-simul-paramod --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 475 476"protokoll_G-E--_045_K18_F1_PI_AE_S4_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-aggressive --split-clauses=4 --simul-paramod --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(4*Refinedweight(SimulateSOS,1,1,2,1.5,2),3*Refinedweight(PreferNonGoals,1,1,2,1.5,1.5),1*Clauseweight(PreferProcessed,1,1,1),1*FIFOWeight(PreferProcessed))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 477 478"protokoll_G-E--_050_K18_F1_PI_AE_Q4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -x'(12*SymbolTypeweight(ConstPrio,1,200,2,30,1.5,1.5,0.8),1*FIFOWeight(PreferUnits))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 479 480"protokoll_G-E--_050_K18_F2_PI_AE_Q4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F2 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -x'(12*SymbolTypeweight(ConstPrio,1,200,2,30,1.5,1.5,0.8),1*FIFOWeight(PreferUnits))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 481 482"protokoll_G-E--_051_K18_F1_PI_AE_Q4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-reuse-defs --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(10*ConjectureRelativeSymbolWeight(SimulateSOS,0.05, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 483 484"protokoll_G-E--_052_K18_F1_PI_AE_Q4_CS_SP_S0Y":" --definitional-cnf=24 --tstp-in --split-reuse-defs --split-clauses=4 --simul-paramod --forward-context-sr --destructive-er-aggressive --destructive-er --prefer-initial-clauses -winvfreqrank -c1 -Ginvfreq -F1 --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred -H'(10*ConjectureRelativeSymbolWeight(ConstPrio,0.05, 100, 100, 100, 100, 1.5, 1.5, 1.5),1*FIFOWeight(SimulateSOS))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 485 486"protokoll_G-N--_023_B07_F1_PI_S4_CS_OS_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 --oriented-simul-paramod -F1 -tLPO4 -Ginvfreq --prefer-initial-clauses --forward-context-sr -WSelectMaxLComplexAvoidPosPred --split-aggressive --split-clauses=4 --tstp-in -H'(12*Clauseweight(ConstPrio,3,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 487 488"protokoll_G-N--_023_B07_F1_PI_S4_CS_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 -tLPO4 -Ginvfreq --prefer-initial-clauses --forward-context-sr -WSelectMaxLComplexAvoidPosPred --split-aggressive --split-clauses=4 --tstp-in -H'(12*Clauseweight(ConstPrio,3,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 489 490"protokoll_G-N--_023_B07_F1_PI_S4_CS_SP_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 -tLPO4 -Ginvfreq --prefer-initial-clauses --forward-context-sr -WSelectMaxLComplexAvoidPosPred --split-aggressive --split-clauses=4 --tstp-in -H'(12*Clauseweight(ConstPrio,3,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 491 492"protokoll_G-N--_023_K07_F1_PI_Q4_CS_SP_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 -wconstant -Ginvfreq --prefer-initial-clauses --forward-context-sr -WSelectMaxLComplexAvoidPosPred --split-reuse-defs --split-clauses=4 --tstp-in -H'(12*Clauseweight(ConstPrio,3,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 493 494"protokoll_G-N--_023_K07_F1_PI_R4_CS_SP_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 -wconstant -Ginvfreq --prefer-initial-clauses --forward-context-sr -WSelectMaxLComplexAvoidPosPred --split-reuse-defs --split-aggressive --split-clauses=4 --tstp-in -H'(12*Clauseweight(ConstPrio,3,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 495 496"protokoll_G-N--_023_K07_F1_PI_S4_AB_SP_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 -wconstant -Ginvfreq --prefer-initial-clauses --forward-context-sr-aggressive --backward-context-sr -WSelectMaxLComplexAvoidPosPred --split-aggressive --split-clauses=4 --tstp-in -H'(12*Clauseweight(ConstPrio,3,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 497 498"protokoll_G-N--_023_K07_F1_PI_S4_CS_SP_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 -wconstant -Ginvfreq --prefer-initial-clauses --forward-context-sr -WSelectMaxLComplexAvoidPosPred --split-aggressive --split-clauses=4 --tstp-in -H'(12*Clauseweight(ConstPrio,3,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 499 500"protokoll_G-N--_023_K18_F1_PI_Q4_CS_SP_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 -winvfreqrank -c1 -Ginvfreq --prefer-initial-clauses --forward-context-sr -WSelectMaxLComplexAvoidPosPred --split-reuse-defs --split-clauses=4 --tstp-in -H'(12*Clauseweight(ConstPrio,3,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 501 502"protokoll_H----_011_B31_F1_PI_AE_SP_S1U":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 --destructive-er-aggressive --destructive-er -WSelectComplexAHPExceptRRHorn -tLPO4 -Ginvfreqconstmin --prefer-initial-clauses --tstp-in -H'(8*Refinedweight(PreferGoals,1,2,2,1,0.8),8*Refinedweight(PreferNonGoals,2,1,2,3,0.8),1*Clauseweight(ConstPrio,1,1,0.7),1*FIFOWeight(ByNegLitDist))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 503 504"protokoll_H----_011_B31_F1_PI_AE_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 --destructive-er-aggressive --destructive-er -WSelectNewComplexAHP -tLPO4 -Ginvfreqconstmin --prefer-initial-clauses --tstp-in -H'(8*Refinedweight(PreferGoals,1,2,2,1,0.8),8*Refinedweight(PreferNonGoals,2,1,2,3,0.8),1*Clauseweight(ConstPrio,1,1,0.7),1*FIFOWeight(ByNegLitDist))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 505 506"protokoll_H----_011_K07_F1_PI_AE_OS_R8_SP_S1U":" --definitional-cnf=24 --delete-bad-limit=150000000 --oriented-simul-paramod --split-aggressive --split-clauses=8 --split-reuse-defs -F1 --destructive-er-aggressive --destructive-er -WSelectComplexAHPExceptRRHorn -wconstant -Ginvfreq --prefer-initial-clauses --tstp-in -H'(8*Refinedweight(PreferGoals,1,2,2,1,0.8),8*Refinedweight(PreferNonGoals,2,1,2,3,0.8),1*Clauseweight(ConstPrio,1,1,0.7),1*FIFOWeight(ByNegLitDist))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 507 508"protokoll_H----_011_K07_F1_PI_AE_OS_S1U":" --definitional-cnf=24 --delete-bad-limit=150000000 --oriented-simul-paramod -F1 --destructive-er-aggressive --destructive-er -WSelectComplexAHPExceptRRHorn -wconstant -Ginvfreq --prefer-initial-clauses --tstp-in -H'(8*Refinedweight(PreferGoals,1,2,2,1,0.8),8*Refinedweight(PreferNonGoals,2,1,2,3,0.8),1*Clauseweight(ConstPrio,1,1,0.7),1*FIFOWeight(ByNegLitDist))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 509 510"protokoll_H----_011_K07_F1_PI_AE_Q4_SP_SOV":" --definitional-cnf=24 --split-clauses=4 --split-reuse-defs --delete-bad-limit=150000000 --simul-paramod -F1 --destructive-er-aggressive --destructive-er -WPSelectComplexExceptRRHorn -wconstant -Ginvfreq --prefer-initial-clauses --tstp-in -H'(8*Refinedweight(PreferGoals,1,2,2,1,0.8),8*Refinedweight(PreferNonGoals,2,1,2,3,0.8),1*Clauseweight(ConstPrio,1,1,0.7),1*FIFOWeight(ByNegLitDist))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 511 512"protokoll_H----_011_K07_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 --split-aggressive --split-clauses=4 --forward-context-sr --destructive-er-aggressive --destructive-er -WSelectMaxLComplexAvoidPosPred -wconstant -Ginvfreq --prefer-initial-clauses --tstp-in -H'(8*Refinedweight(PreferGoals,1,2,2,1,0.8),8*Refinedweight(PreferNonGoals,2,1,2,3,0.8),1*Clauseweight(ConstPrio,1,1,0.7),1*FIFOWeight(ByNegLitDist))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 513 514"protokoll_H----_011_K07_F1_PI_AE_S4_CS_SP_S2V":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 --split-aggressive --split-clauses=4 --forward-context-sr --destructive-er-aggressive --destructive-er -WPSelectNewComplexAHPExceptRRHorn -wconstant -Ginvfreq --prefer-initial-clauses --tstp-in -H'(8*Refinedweight(PreferGoals,1,2,2,1,0.8),8*Refinedweight(PreferNonGoals,2,1,2,3,0.8),1*Clauseweight(ConstPrio,1,1,0.7),1*FIFOWeight(ByNegLitDist))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 515 516"protokoll_H----_011_K07_F1_PI_AE_S4_CS_SP_SOV":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 --split-aggressive --split-clauses=4 --forward-context-sr --destructive-er-aggressive --destructive-er -WPSelectComplexExceptRRHorn -wconstant -Ginvfreq --prefer-initial-clauses --tstp-in -H'(8*Refinedweight(PreferGoals,1,2,2,1,0.8),8*Refinedweight(PreferNonGoals,2,1,2,3,0.8),1*Clauseweight(ConstPrio,1,1,0.7),1*FIFOWeight(ByNegLitDist))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 517 518"protokoll_H----_011_K07_F1_PI_AE_SP_S1U":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 --destructive-er-aggressive --destructive-er -WSelectComplexAHPExceptRRHorn -wconstant -Ginvfreq --prefer-initial-clauses --tstp-in -H'(8*Refinedweight(PreferGoals,1,2,2,1,0.8),8*Refinedweight(PreferNonGoals,2,1,2,3,0.8),1*Clauseweight(ConstPrio,1,1,0.7),1*FIFOWeight(ByNegLitDist))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 519 520"protokoll_H----_011_K07_F1_PI_AE_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 --destructive-er-aggressive --destructive-er -WSelectNewComplexAHP -wconstant -Ginvfreq --prefer-initial-clauses --tstp-in -H'(8*Refinedweight(PreferGoals,1,2,2,1,0.8),8*Refinedweight(PreferNonGoals,2,1,2,3,0.8),1*Clauseweight(ConstPrio,1,1,0.7),1*FIFOWeight(ByNegLitDist))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 521 522"protokoll_H----_011_K07_F1_PI_AE_SP_S2U":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 --destructive-er-aggressive --destructive-er -WSelectNewComplexAHPExceptRRHorn -wconstant -Ginvfreq --prefer-initial-clauses --tstp-in -H'(8*Refinedweight(PreferGoals,1,2,2,1,0.8),8*Refinedweight(PreferNonGoals,2,1,2,3,0.8),1*Clauseweight(ConstPrio,1,1,0.7),1*FIFOWeight(ByNegLitDist))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 523 524"protokoll_H----_011_K07_F1_PI_AE_SP_S2V":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 --destructive-er-aggressive --destructive-er -WPSelectNewComplexAHPExceptRRHorn -wconstant -Ginvfreq --prefer-initial-clauses --tstp-in -H'(8*Refinedweight(PreferGoals,1,2,2,1,0.8),8*Refinedweight(PreferNonGoals,2,1,2,3,0.8),1*Clauseweight(ConstPrio,1,1,0.7),1*FIFOWeight(ByNegLitDist))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 525 526"protokoll_H----_011_K07_F1_PI_AE_SP_SOV":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 --destructive-er-aggressive --destructive-er -WPSelectComplexExceptRRHorn -wconstant -Ginvfreq --prefer-initial-clauses --tstp-in -H'(8*Refinedweight(PreferGoals,1,2,2,1,0.8),8*Refinedweight(PreferNonGoals,2,1,2,3,0.8),1*Clauseweight(ConstPrio,1,1,0.7),1*FIFOWeight(ByNegLitDist))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 527 528"protokoll_H----_011_K18_F1_PI_AE_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 --destructive-er-aggressive --destructive-er -WSelectNewComplexAHP -winvfreqrank -c1 -Ginvfreq --prefer-initial-clauses --tstp-in -H'(8*Refinedweight(PreferGoals,1,2,2,1,0.8),8*Refinedweight(PreferNonGoals,2,1,2,3,0.8),1*Clauseweight(ConstPrio,1,1,0.7),1*FIFOWeight(ByNegLitDist))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 529 530"protokoll_H----_014_K18_F1_PI_AE_CS_SP_S2S":" --definitional-cnf=24 --forward-context-sr --simul-paramod --delete-bad-limit=150000000 --tstp-in -winvfreqrank -c1 -Ginvfreq -F1 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -WSelectNewComplexAHP -H'(12*Refinedweight(PreferGoals,1,2,2,1,0.8),12*Refinedweight(PreferNonGoals,2,1,2,3,0.8),2*ClauseWeightAge(ConstPrio,1,1,0.7,3))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 531 532"protokoll_H----_014_K18_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --split-aggressive --split-clauses=4 --forward-context-sr --simul-paramod --delete-bad-limit=150000000 --tstp-in -winvfreqrank -c1 -Ginvfreq -F1 --destructive-er-aggressive --destructive-er --prefer-initial-clauses -WSelectNewComplexAHP -H'(12*Refinedweight(PreferGoals,1,2,2,1,0.8),12*Refinedweight(PreferNonGoals,2,1,2,3,0.8),2*ClauseWeightAge(ConstPrio,1,1,0.7,3))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 533 534"protokoll_H----_024_K18_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 -WSelectNewComplexAHP --prefer-initial-clauses --forward-context-sr --split-aggressive --split-clauses=4 --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq --tstp-in -H'(12*SymbolTypeweight(ConstPrio,7,20,0,0,1.5,5,0.8),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 535 536"protokoll_H----_024_K18_F1_PI_OP_AE_S4_AB_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 -WSelectNewComplexAHP --prefer-initial-clauses --select-on-processing-only --forward-context-sr-aggressive --backward-context-sr --split-aggressive --split-clauses=4 --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq --tstp-in -H'(12*SymbolTypeweight(ConstPrio,7,20,0,0,1.5,5,0.8),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 537 538"protokoll_H----_024_K18_F1_PI_OP_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 -WSelectNewComplexAHP --prefer-initial-clauses --select-on-processing-only --forward-context-sr --split-aggressive --split-clauses=4 --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq --tstp-in -H'(12*SymbolTypeweight(ConstPrio,7,20,0,0,1.5,5,0.8),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 539 540"protokoll_H----_031_K09_F1_PI_AE_SP_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --simul-paramod -WSelectMaxLComplexAvoidPosPred --destructive-er-aggressive --destructive-er -waritysquared -Garity --prefer-initial-clauses --tstp-in -H'(10*Refinedweight(PreferGoals,1,2,2,2,0.5),10*Refinedweight(PreferNonGoals,2,1,2,2,2),1*Clauseweight(ConstPrio,1,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 541 542"protokoll_H----_031_K18_F1_PI_AE_CS_SP_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --simul-paramod --forward-context-sr -WSelectMaxLComplexAvoidPosPred -winvfreqrank -c1 -Ginvfreq --destructive-er-aggressive --destructive-er --prefer-initial-clauses --tstp-in -H'(10*Refinedweight(PreferGoals,1,2,2,2,0.5),10*Refinedweight(PreferNonGoals,2,1,2,2,2),1*Clauseweight(ConstPrio,1,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 543 544"protokoll_H----_031_K18_F1_PI_AE_CS_SP_S3T":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --simul-paramod --forward-context-sr -WPSelectNewComplexAHPExceptUniqMaxHorn -winvfreqrank -c1 -Ginvfreq --destructive-er-aggressive --destructive-er --prefer-initial-clauses --tstp-in -H'(10*Refinedweight(PreferGoals,1,2,2,2,0.5),10*Refinedweight(PreferNonGoals,2,1,2,2,2),1*Clauseweight(ConstPrio,1,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 545 546"protokoll_H----_031_K18_F1_PI_AE_Q4_CS_SP_S3T":" --definitional-cnf=24 --delete-bad-limit=150000000 --split-clauses=4 --split-reuse-defs -F1 --simul-paramod --forward-context-sr -WPSelectNewComplexAHPExceptUniqMaxHorn -winvfreqrank -c1 -Ginvfreq --destructive-er-aggressive --destructive-er --prefer-initial-clauses --tstp-in -H'(10*Refinedweight(PreferGoals,1,2,2,2,0.5),10*Refinedweight(PreferNonGoals,2,1,2,2,2),1*Clauseweight(ConstPrio,1,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 547 548"protokoll_H----_036_K18_F2_PI_AE_R12_SP_S2S":" --definitional-cnf=24 --simul-paramod --delete-bad-limit=150000000 -WSelectNewComplexAHP --split-reuse-defs --split-aggressive --split-clauses=12 --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq --prefer-initial-clauses --tstp-in -H'(10*Refinedweight(PreferGoals,1,2,2,2,0.5),10*Refinedweight(PreferNonGoals,2,1,2,2,2),2*ClauseWeightAge(ConstPrio,1,1,1,3))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 549 550"protokoll_H----_036_K18_F2_PI_AE_R4_SP_S2S":" --definitional-cnf=24 --simul-paramod --delete-bad-limit=150000000 -WSelectNewComplexAHP --split-reuse-defs --split-aggressive --split-clauses=4 --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq --prefer-initial-clauses --tstp-in -H'(10*Refinedweight(PreferGoals,1,2,2,2,0.5),10*Refinedweight(PreferNonGoals,2,1,2,2,2),2*ClauseWeightAge(ConstPrio,1,1,1,3))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 551"protokoll_H----_036_K18_F2_PI_AE_S4_SP_S2S":" --definitional-cnf=24 --simul-paramod --delete-bad-limit=150000000 -WSelectNewComplexAHP --split-aggressive --split-clauses=4 --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq --prefer-initial-clauses --tstp-in -H'(10*Refinedweight(PreferGoals,1,2,2,2,0.5),10*Refinedweight(PreferNonGoals,2,1,2,2,2),2*ClauseWeightAge(ConstPrio,1,1,1,3))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 552 553"protokoll_H----_042_B01_F1_PI_AE_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --simul-paramod -WSelectNewComplexAHP --destructive-er-aggressive --destructive-er -tLPO4 --prefer-initial-clauses --tstp-in -H'(10*Refinedweight(PreferGoals,1,2,2,2,0.5),10*Refinedweight(PreferNonGoals,2,1,2,2,2),5*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 554 555"protokoll_H----_042_B03_F1_PI_AE_SP_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --simul-paramod -WSelectMaxLComplexAvoidPosPred --destructive-er-aggressive --destructive-er -tLPO4 -Ginvarity --prefer-initial-clauses --tstp-in -H'(10*Refinedweight(PreferGoals,1,2,2,2,0.5),10*Refinedweight(PreferNonGoals,2,1,2,2,2),5*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 556 557"protokoll_H----_042_B03_F1_PI_AE_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --simul-paramod -WSelectNewComplexAHP --destructive-er-aggressive --destructive-er -tLPO4 -Ginvarity --prefer-initial-clauses --tstp-in -H'(10*Refinedweight(PreferGoals,1,2,2,2,0.5),10*Refinedweight(PreferNonGoals,2,1,2,2,2),5*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 558 559"protokoll_H----_042_B07_F1_PI_AE_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --simul-paramod -WSelectNewComplexAHP --destructive-er-aggressive --destructive-er -tLPO4 -Ginvfreq --prefer-initial-clauses --tstp-in -H'(10*Refinedweight(PreferGoals,1,2,2,2,0.5),10*Refinedweight(PreferNonGoals,2,1,2,2,2),5*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 560 561"protokoll_H----_042_B30_F1_PI_AE_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --simul-paramod -WSelectNewComplexAHP --destructive-er-aggressive --destructive-er -tLPO4 -Ginvfreqhack --prefer-initial-clauses --tstp-in -H'(10*Refinedweight(PreferGoals,1,2,2,2,0.5),10*Refinedweight(PreferNonGoals,2,1,2,2,2),5*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 562 563"protokoll_H----_042_B31_F1_PI_AE_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --simul-paramod -WSelectNewComplexAHP --destructive-er-aggressive --destructive-er -tLPO4 -Ginvfreqconstmin --prefer-initial-clauses --tstp-in -H'(10*Refinedweight(PreferGoals,1,2,2,2,0.5),10*Refinedweight(PreferNonGoals,2,1,2,2,2),5*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 564 565"protokoll_H----_047_B31_F1_PI_AE_R4_CS_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 -WSelectNewComplexAHP --forward-context-sr --split-aggressive --split-clauses=4 --split-reuse-defs --destructive-er-aggressive --destructive-er -tLPO4 -Ginvfreqconstmin --prefer-initial-clauses --tstp-in -H'(10*PNRefinedweight(PreferGoals,1,1,1,2,2,2,0.5),10*PNRefinedweight(PreferNonGoals,2,1,1,1,2,2,2),5*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 566 567"protokoll_H----_047_K02_F1_PI_AE_Q12_CS_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 -WSelectNewComplexAHP --forward-context-sr --split-clauses=12 --split-reuse-defs --destructive-er-aggressive --destructive-er -wconstant -Garity --prefer-initial-clauses --tstp-in -H'(10*PNRefinedweight(PreferGoals,1,1,1,2,2,2,0.5),10*PNRefinedweight(PreferNonGoals,2,1,1,1,2,2,2),5*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 568 569"protokoll_H----_047_K02_F1_PI_AE_Q4_CS_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 -WSelectNewComplexAHP --forward-context-sr --split-clauses=4 --split-reuse-defs --destructive-er-aggressive --destructive-er -wconstant -Garity --prefer-initial-clauses --tstp-in -H'(10*PNRefinedweight(PreferGoals,1,1,1,2,2,2,0.5),10*PNRefinedweight(PreferNonGoals,2,1,1,1,2,2,2),5*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 570 571"protokoll_H----_047_K18_F1_PI_AE_Q4_CS_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 -WSelectNewComplexAHP --forward-context-sr --split-clauses=4 --split-reuse-defs --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq --prefer-initial-clauses --tstp-in -H'(10*PNRefinedweight(PreferGoals,1,1,1,2,2,2,0.5),10*PNRefinedweight(PreferNonGoals,2,1,1,1,2,2,2),5*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 572 573"protokoll_H----_047_K18_F1_PI_AE_R4_CS_SP_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 -WSelectMaxLComplexAvoidPosPred --forward-context-sr --split-aggressive --split-clauses=4 --split-reuse-defs --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq --prefer-initial-clauses --tstp-in -H'(10*PNRefinedweight(PreferGoals,1,1,1,2,2,2,0.5),10*PNRefinedweight(PreferNonGoals,2,1,1,1,2,2,2),5*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 574 575"protokoll_H----_047_K18_F1_PI_AE_R4_CS_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 -WSelectNewComplexAHP --forward-context-sr --split-aggressive --split-clauses=4 --split-reuse-defs --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq --prefer-initial-clauses --tstp-in -H'(10*PNRefinedweight(PreferGoals,1,1,1,2,2,2,0.5),10*PNRefinedweight(PreferNonGoals,2,1,1,1,2,2,2),5*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 576 577"protokoll_H----_047_K18_F1_PI_AE_R7_CS_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 -WSelectNewComplexAHP --forward-context-sr --split-aggressive --split-clauses=7 --split-reuse-defs --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq --prefer-initial-clauses --tstp-in -H'(10*PNRefinedweight(PreferGoals,1,1,1,2,2,2,0.5),10*PNRefinedweight(PreferNonGoals,2,1,1,1,2,2,2),5*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 578 579"protokoll_H----_047_K18_F1_PI_AE_R8_CS_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 -WSelectNewComplexAHP --forward-context-sr --split-aggressive --split-clauses=8 --split-reuse-defs --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq --prefer-initial-clauses --tstp-in -H'(10*PNRefinedweight(PreferGoals,1,1,1,2,2,2,0.5),10*PNRefinedweight(PreferNonGoals,2,1,1,1,2,2,2),5*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 580 581"protokoll_H----_047_K18_F1_PI_AE_S12_CS_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 -WSelectNewComplexAHP --forward-context-sr --split-aggressive --split-clauses=12 --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq --prefer-initial-clauses --tstp-in -H'(10*PNRefinedweight(PreferGoals,1,1,1,2,2,2,0.5),10*PNRefinedweight(PreferNonGoals,2,1,1,1,2,2,2),5*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 582 583"protokoll_H----_047_K18_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 -WSelectNewComplexAHP --forward-context-sr --split-aggressive --split-clauses=4 --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq --prefer-initial-clauses --tstp-in -H'(10*PNRefinedweight(PreferGoals,1,1,1,2,2,2,0.5),10*PNRefinedweight(PreferNonGoals,2,1,1,1,2,2,2),5*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 584 585"protokoll_H----_047_K18_F1_PI_AE_S8_CS_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 --simul-paramod -F1 -WSelectNewComplexAHP --forward-context-sr --split-aggressive --split-clauses=8 --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq --prefer-initial-clauses --tstp-in -H'(10*PNRefinedweight(PreferGoals,1,1,1,2,2,2,0.5),10*PNRefinedweight(PreferNonGoals,2,1,1,1,2,2,2),5*OrientLMaxWeight(ConstPrio,2,1,2,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 586 587"protokoll_H----_072_B31_F1_PI_AE_CS_S4_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --simul-paramod --destructive-er-aggressive --destructive-er --split-aggressive --split-clauses=4 -WSelectMaxLComplexAvoidPosPred --prefer-initial-clauses --forward-context-sr -tLPO4 -Ginvfreqconstmin --tstp-in -H'(10*Refinedweight(PreferGroundGoals,2,1,2,1.0,1),1*Clauseweight(ConstPrio,1,1,1),1*Clauseweight(ByCreationDate,2,1,0.8))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 588 589"protokoll_H----_072_K16_F1_PI_AE_CS_R4_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --destructive-er-aggressive --destructive-er --split-aggressive --split-clauses=4 --split-reuse-defs -WSelectMaxLComplexAvoidPosPred --prefer-initial-clauses --forward-context-sr -wprecedence -c1 -Ginvfreq --tstp-in -H'(10*Refinedweight(PreferGroundGoals,2,1,2,1.0,1),1*Clauseweight(ConstPrio,1,1,1),1*Clauseweight(ByCreationDate,2,1,0.8))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 590 591"protokoll_H----_072_K16_F1_PI_AE_CS_R7_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --destructive-er-aggressive --destructive-er --split-aggressive --split-clauses=7 --split-reuse-defs -WSelectMaxLComplexAvoidPosPred --prefer-initial-clauses --forward-context-sr -wprecedence -c1 -Ginvfreq --tstp-in -H'(10*Refinedweight(PreferGroundGoals,2,1,2,1.0,1),1*Clauseweight(ConstPrio,1,1,1),1*Clauseweight(ByCreationDate,2,1,0.8))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 592 593"protokoll_H----_072_K16_F1_PI_AE_CS_R8_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --destructive-er-aggressive --destructive-er --split-aggressive --split-clauses=8 --split-reuse-defs -WSelectMaxLComplexAvoidPosPred --prefer-initial-clauses --forward-context-sr -wprecedence -c1 -Ginvfreq --tstp-in -H'(10*Refinedweight(PreferGroundGoals,2,1,2,1.0,1),1*Clauseweight(ConstPrio,1,1,1),1*Clauseweight(ByCreationDate,2,1,0.8))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 594 595"protokoll_H----_072_K16_F1_PI_AE_CS_S4_OS_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --oriented-simul-paramod --destructive-er-aggressive --destructive-er --split-aggressive --split-clauses=4 -WSelectMaxLComplexAvoidPosPred --prefer-initial-clauses --forward-context-sr -wprecedence -c1 -Ginvfreq --tstp-in -H'(10*Refinedweight(PreferGroundGoals,2,1,2,1.0,1),1*Clauseweight(ConstPrio,1,1,1),1*Clauseweight(ByCreationDate,2,1,0.8))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 596 597"protokoll_H----_072_K16_F1_PI_AE_CS_S4_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --destructive-er-aggressive --destructive-er --split-aggressive --split-clauses=4 -WSelectMaxLComplexAvoidPosPred --prefer-initial-clauses --forward-context-sr -wprecedence -c1 -Ginvfreq --tstp-in -H'(10*Refinedweight(PreferGroundGoals,2,1,2,1.0,1),1*Clauseweight(ConstPrio,1,1,1),1*Clauseweight(ByCreationDate,2,1,0.8))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 598 599"protokoll_H----_072_K16_F1_PI_AE_CS_S4_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --destructive-er-aggressive --destructive-er --split-aggressive --split-clauses=4 -WSelectNewComplexAHP --prefer-initial-clauses --forward-context-sr -wprecedence -c1 -Ginvfreq --tstp-in -H'(10*Refinedweight(PreferGroundGoals,2,1,2,1.0,1),1*Clauseweight(ConstPrio,1,1,1),1*Clauseweight(ByCreationDate,2,1,0.8))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 600 601"protokoll_H----_072_K16_F1_PI_AE_CS_S4_SP_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --simul-paramod --destructive-er-aggressive --destructive-er --split-aggressive --split-clauses=4 -WSelectMaxLComplexAvoidPosPred --prefer-initial-clauses --forward-context-sr -wprecedence -c1 -Ginvfreq --tstp-in -H'(10*Refinedweight(PreferGroundGoals,2,1,2,1.0,1),1*Clauseweight(ConstPrio,1,1,1),1*Clauseweight(ByCreationDate,2,1,0.8))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 602 603"protokoll_H----_072_K16_F1_PI_AE_CS_S4_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --simul-paramod --destructive-er-aggressive --destructive-er --split-aggressive --split-clauses=4 -WSelectMaxLComplexAvoidPosPred --prefer-initial-clauses --forward-context-sr -wprecedence -c1 -Ginvfreq --tstp-in -H'(10*Refinedweight(PreferGroundGoals,2,1,2,1.0,1),1*Clauseweight(ConstPrio,1,1,1),1*Clauseweight(ByCreationDate,2,1,0.8))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 604 605"protokoll_H----_072_K18_F1_PI_AE_CS_Q4_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --simul-paramod --destructive-er-aggressive --destructive-er --split-reuse-defs --split-clauses=4 -WSelectMaxLComplexAvoidPosPred --prefer-initial-clauses --forward-context-sr -winvfreqrank -c1 -Ginvfreq --tstp-in -H'(10*Refinedweight(PreferGroundGoals,2,1,2,1.0,1),1*Clauseweight(ConstPrio,1,1,1),1*Clauseweight(ByCreationDate,2,1,0.8))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 606 607"protokoll_H----_072_K18_F1_PI_AE_CS_S4_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --simul-paramod --destructive-er-aggressive --destructive-er --split-aggressive --split-clauses=4 -WSelectMaxLComplexAvoidPosPred --prefer-initial-clauses --forward-context-sr -winvfreqrank -c1 -Ginvfreq --tstp-in -H'(10*Refinedweight(PreferGroundGoals,2,1,2,1.0,1),1*Clauseweight(ConstPrio,1,1,1),1*Clauseweight(ByCreationDate,2,1,0.8))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 608 609"protokoll_H----_081_B02_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --prefer-initial-clauses --simul-paramod --forward-context-sr --split-aggressive --split-clauses=4 --destructive-er-aggressive --destructive-er -F1 -tLPO4 -Garity --delete-bad-limit=150000000 -WSelectNewComplex --tstp-in -H'(8*Refinedweight(PreferGoals,1,2,2,2,2),8*Refinedweight(PreferNonGoals,2,1,2,2,0.5),1*Clauseweight(PreferUnitGroundGoals,1,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 610 611"protokoll_H----_081_B07_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --prefer-initial-clauses --simul-paramod --forward-context-sr --split-aggressive --split-clauses=4 --destructive-er-aggressive --destructive-er -F1 -tLPO4 -Ginvfreq --delete-bad-limit=150000000 -WSelectNewComplex --tstp-in -H'(8*Refinedweight(PreferGoals,1,2,2,2,2),8*Refinedweight(PreferNonGoals,2,1,2,2,0.5),1*Clauseweight(PreferUnitGroundGoals,1,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 612 613"protokoll_H----_081_B31_F1_PI_AE_Q4_CS_SP_S2S":" --definitional-cnf=24 --prefer-initial-clauses --simul-paramod --forward-context-sr --split-reuse-defs --split-clauses=4 --destructive-er-aggressive --destructive-er -F1 -tLPO4 -Ginvfreqconstmin --delete-bad-limit=150000000 -WSelectNewComplex --tstp-in -H'(8*Refinedweight(PreferGoals,1,2,2,2,2),8*Refinedweight(PreferNonGoals,2,1,2,2,0.5),1*Clauseweight(PreferUnitGroundGoals,1,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 614 615"protokoll_H----_081_B31_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --prefer-initial-clauses --simul-paramod --forward-context-sr --split-aggressive --split-clauses=4 --destructive-er-aggressive --destructive-er -F1 -tLPO4 -Ginvfreqconstmin --delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred --tstp-in -H'(8*Refinedweight(PreferGoals,1,2,2,2,2),8*Refinedweight(PreferNonGoals,2,1,2,2,0.5),1*Clauseweight(PreferUnitGroundGoals,1,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 616 617"protokoll_H----_081_B31_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --prefer-initial-clauses --simul-paramod --forward-context-sr --split-aggressive --split-clauses=4 --destructive-er-aggressive --destructive-er -F1 -tLPO4 -Ginvfreqconstmin --delete-bad-limit=150000000 -WSelectNewComplex --tstp-in -H'(8*Refinedweight(PreferGoals,1,2,2,2,2),8*Refinedweight(PreferNonGoals,2,1,2,2,0.5),1*Clauseweight(PreferUnitGroundGoals,1,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 618 619"protokoll_H----_081_K18_F1_PI_AE_Q12_CS_SP_S2S":" --definitional-cnf=24 --prefer-initial-clauses --simul-paramod --forward-context-sr --split-reuse-defs --split-clauses=12 --destructive-er-aggressive --destructive-er -F1 -winvfreqrank -c1 -Ginvfreq --delete-bad-limit=150000000 -WSelectNewComplex --tstp-in -H'(8*Refinedweight(PreferGoals,1,2,2,2,2),8*Refinedweight(PreferNonGoals,2,1,2,2,0.5),1*Clauseweight(PreferUnitGroundGoals,1,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 620 621"protokoll_H----_081_K18_F1_PI_AE_Q4_CS_SP_S2S":" --definitional-cnf=24 --prefer-initial-clauses --simul-paramod --forward-context-sr --split-reuse-defs --split-clauses=4 --destructive-er-aggressive --destructive-er -F1 -winvfreqrank -c1 -Ginvfreq --delete-bad-limit=150000000 -WSelectNewComplex --tstp-in -H'(8*Refinedweight(PreferGoals,1,2,2,2,2),8*Refinedweight(PreferNonGoals,2,1,2,2,0.5),1*Clauseweight(PreferUnitGroundGoals,1,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 622 623"protokoll_H----_081_K18_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --prefer-initial-clauses --simul-paramod --forward-context-sr --split-aggressive --split-clauses=4 --destructive-er-aggressive --destructive-er -F1 -winvfreqrank -c1 -Ginvfreq --delete-bad-limit=150000000 -WSelectNewComplex --tstp-in -H'(8*Refinedweight(PreferGoals,1,2,2,2,2),8*Refinedweight(PreferNonGoals,2,1,2,2,0.5),1*Clauseweight(PreferUnitGroundGoals,1,1,1),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 624 625"protokoll_H----_102_B01_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --simul-paramod -WSelectNewComplexAHP --split-aggressive --split-clauses=4 --forward-context-sr --destructive-er-aggressive --destructive-er -tLPO4 -Gunary_first --prefer-initial-clauses --tstp-in -H'(10*Refinedweight(PreferGoals,1,2,2,2,0.5),10*Refinedweight(PreferNonGoals,2,1,2,2,2),3*OrientLMaxWeight(ConstPrio,2,1,2,1,1),2*ClauseWeightAge(ConstPrio,1,1,1,3))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 626 627"protokoll_H----_102_B03_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --simul-paramod -WSelectNewComplexAHP --split-aggressive --split-clauses=4 --forward-context-sr --destructive-er-aggressive --destructive-er -tLPO4 -Ginvarity --prefer-initial-clauses --tstp-in -H'(10*Refinedweight(PreferGoals,1,2,2,2,0.5),10*Refinedweight(PreferNonGoals,2,1,2,2,2),3*OrientLMaxWeight(ConstPrio,2,1,2,1,1),2*ClauseWeightAge(ConstPrio,1,1,1,3))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 628 629"protokoll_H----_102_B30_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --simul-paramod -WSelectNewComplexAHP --split-aggressive --split-clauses=4 --forward-context-sr --destructive-er-aggressive --destructive-er -tLPO4 -Ginvfreqhack --prefer-initial-clauses --tstp-in -H'(10*Refinedweight(PreferGoals,1,2,2,2,0.5),10*Refinedweight(PreferNonGoals,2,1,2,2,2),3*OrientLMaxWeight(ConstPrio,2,1,2,1,1),2*ClauseWeightAge(ConstPrio,1,1,1,3))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 630 631"protokoll_H----_102_B31_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --simul-paramod -WSelectNewComplexAHP --split-aggressive --split-clauses=4 --forward-context-sr --destructive-er-aggressive --destructive-er -tLPO4 -Ginvfreqconstmin --prefer-initial-clauses --tstp-in -H'(10*Refinedweight(PreferGoals,1,2,2,2,0.5),10*Refinedweight(PreferNonGoals,2,1,2,2,2),3*OrientLMaxWeight(ConstPrio,2,1,2,1,1),2*ClauseWeightAge(ConstPrio,1,1,1,3))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 632 633"protokoll_H----_102_K18_F1_PI_AE_S4_CS_OS_S1S":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --oriented-simul-paramod -WSelectComplexAHP --split-aggressive --split-clauses=4 --forward-context-sr --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq --prefer-initial-clauses --tstp-in -H'(10*Refinedweight(PreferGoals,1,2,2,2,0.5),10*Refinedweight(PreferNonGoals,2,1,2,2,2),3*OrientLMaxWeight(ConstPrio,2,1,2,1,1),2*ClauseWeightAge(ConstPrio,1,1,1,3))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 634 635"protokoll_H----_102_K18_F1_PI_AE_S4_CS_OS_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --oriented-simul-paramod -WSelectNewComplexAHP --split-aggressive --split-clauses=4 --forward-context-sr --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq --prefer-initial-clauses --tstp-in -H'(10*Refinedweight(PreferGoals,1,2,2,2,0.5),10*Refinedweight(PreferNonGoals,2,1,2,2,2),3*OrientLMaxWeight(ConstPrio,2,1,2,1,1),2*ClauseWeightAge(ConstPrio,1,1,1,3))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 636 637"protokoll_H----_102_K18_F1_PI_AE_S4_CS_S1S":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 -WSelectComplexAHP --split-aggressive --split-clauses=4 --forward-context-sr --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq --prefer-initial-clauses --tstp-in -H'(10*Refinedweight(PreferGoals,1,2,2,2,0.5),10*Refinedweight(PreferNonGoals,2,1,2,2,2),3*OrientLMaxWeight(ConstPrio,2,1,2,1,1),2*ClauseWeightAge(ConstPrio,1,1,1,3))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 638 639"protokoll_H----_102_K18_F1_PI_AE_S4_CS_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 -WSelectNewComplexAHP --split-aggressive --split-clauses=4 --forward-context-sr --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq --prefer-initial-clauses --tstp-in -H'(10*Refinedweight(PreferGoals,1,2,2,2,0.5),10*Refinedweight(PreferNonGoals,2,1,2,2,2),3*OrientLMaxWeight(ConstPrio,2,1,2,1,1),2*ClauseWeightAge(ConstPrio,1,1,1,3))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 640 641"protokoll_H----_102_K18_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --simul-paramod -WSelectMaxLComplexAvoidPosPred --split-aggressive --split-clauses=4 --forward-context-sr --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq --prefer-initial-clauses --tstp-in -H'(10*Refinedweight(PreferGoals,1,2,2,2,0.5),10*Refinedweight(PreferNonGoals,2,1,2,2,2),3*OrientLMaxWeight(ConstPrio,2,1,2,1,1),2*ClauseWeightAge(ConstPrio,1,1,1,3))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 642 643"protokoll_H----_102_K18_F1_PI_AE_S4_CS_SP_S1S":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --simul-paramod -WSelectComplexAHP --split-aggressive --split-clauses=4 --forward-context-sr --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq --prefer-initial-clauses --tstp-in -H'(10*Refinedweight(PreferGoals,1,2,2,2,0.5),10*Refinedweight(PreferNonGoals,2,1,2,2,2),3*OrientLMaxWeight(ConstPrio,2,1,2,1,1),2*ClauseWeightAge(ConstPrio,1,1,1,3))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 644 645"protokoll_H----_102_K18_F1_PI_AE_S4_CS_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 -F1 --simul-paramod -WSelectNewComplexAHP --split-aggressive --split-clauses=4 --forward-context-sr --destructive-er-aggressive --destructive-er -winvfreqrank -c1 -Ginvfreq --prefer-initial-clauses --tstp-in -H'(10*Refinedweight(PreferGoals,1,2,2,2,0.5),10*Refinedweight(PreferNonGoals,2,1,2,2,2),3*OrientLMaxWeight(ConstPrio,2,1,2,1,1),2*ClauseWeightAge(ConstPrio,1,1,1,3))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 646 647"protokoll_U----_043_B07_F1_PI_AE_CS_SP_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 --tstp-in --simul-paramod --destructive-er-aggressive --destructive-er -F1 --forward-context-sr -tLPO4 -Ginvfreq --prefer-initial-clauses -WSelectMaxLComplexAvoidPosPred -H'(4*PNRefinedweight(PreferNonGoals,4,5,5,4,2,1,1),8*PNRefinedweight(PreferGoals,5,2,2,5,2,1,0.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 648 649"protokoll_U----_043_B31_F1_PI_AE_CS_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 --tstp-in --simul-paramod --destructive-er-aggressive --destructive-er -F1 -tLPO4 -winvfreqrank --forward-context-sr --prefer-initial-clauses -WSelectNewComplexAHP -H'(4*PNRefinedweight(PreferNonGoals,4,5,5,4,2,1,1),8*PNRefinedweight(PreferGoals,5,2,2,5,2,1,0.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 650 651"protokoll_U----_043_K07_F1_PI_AE_CS_SP_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 --tstp-in --simul-paramod --destructive-er-aggressive --destructive-er -F1 --forward-context-sr -wconstant -Ginvfreq --prefer-initial-clauses -WSelectMaxLComplexAvoidPosPred -H'(4*PNRefinedweight(PreferNonGoals,4,5,5,4,2,1,1),8*PNRefinedweight(PreferGoals,5,2,2,5,2,1,0.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 652 653"protokoll_U----_043_K09_F1_PI_AE_CS_SP_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 --tstp-in --simul-paramod --destructive-er-aggressive --destructive-er -F1 --forward-context-sr -waritysquared -Garity --prefer-initial-clauses -WSelectMaxLComplexAvoidPosPred -H'(4*PNRefinedweight(PreferNonGoals,4,5,5,4,2,1,1),8*PNRefinedweight(PreferGoals,5,2,2,5,2,1,0.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 654 655"protokoll_U----_043_K18_F1_PI_AE_CS_OS_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 --tstp-in --oriented-simul-paramod --destructive-er-aggressive --destructive-er -F1 -winvfreqrank --forward-context-sr -c1 -Ginvfreq --prefer-initial-clauses -WSelectMaxLComplexAvoidPosPred -H'(4*PNRefinedweight(PreferNonGoals,4,5,5,4,2,1,1),8*PNRefinedweight(PreferGoals,5,2,2,5,2,1,0.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 656 657"protokoll_U----_043_K18_F1_PI_AE_CS_OS_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 --tstp-in --oriented-simul-paramod --destructive-er-aggressive --destructive-er -F1 -winvfreqrank --forward-context-sr -c1 -Ginvfreq --prefer-initial-clauses -WSelectNewComplexAHP -H'(4*PNRefinedweight(PreferNonGoals,4,5,5,4,2,1,1),8*PNRefinedweight(PreferGoals,5,2,2,5,2,1,0.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 658 659"protokoll_U----_043_K18_F1_PI_AE_CS_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 --tstp-in --destructive-er-aggressive --destructive-er -F1 -winvfreqrank --forward-context-sr -c1 -Ginvfreq --prefer-initial-clauses -WSelectMaxLComplexAvoidPosPred -H'(4*PNRefinedweight(PreferNonGoals,4,5,5,4,2,1,1),8*PNRefinedweight(PreferGoals,5,2,2,5,2,1,0.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 660 661"protokoll_U----_043_K18_F1_PI_AE_CS_SP_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 --tstp-in --simul-paramod --destructive-er-aggressive --destructive-er -F1 -winvfreqrank --forward-context-sr -c1 -Ginvfreq --prefer-initial-clauses -WSelectMaxLComplexAvoidPosPred -H'(4*PNRefinedweight(PreferNonGoals,4,5,5,4,2,1,1),8*PNRefinedweight(PreferGoals,5,2,2,5,2,1,0.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 662 663"protokoll_U----_043_K18_F1_PI_AE_CS_SP_S2S":" --definitional-cnf=24 --delete-bad-limit=150000000 --tstp-in --simul-paramod --destructive-er-aggressive --destructive-er -F1 -winvfreqrank --forward-context-sr -c1 -Ginvfreq --prefer-initial-clauses -WSelectNewComplexAHP -H'(4*PNRefinedweight(PreferNonGoals,4,5,5,4,2,1,1),8*PNRefinedweight(PreferGoals,5,2,2,5,2,1,0.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 664 665"protokoll_U----_043_K18_F1_PI_AE_S4_CS_SP_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 --tstp-in --simul-paramod --split-aggressive --split-clauses=4 --destructive-er-aggressive --destructive-er -F1 -winvfreqrank --forward-context-sr -c1 -Ginvfreq --prefer-initial-clauses -WSelectMaxLComplexAvoidPosPred -H'(4*PNRefinedweight(PreferNonGoals,4,5,5,4,2,1,1),8*PNRefinedweight(PreferGoals,5,2,2,5,2,1,0.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 666 667"protokoll_U----_043_K18_F2_PI_AE_CS_SP_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 --tstp-in --simul-paramod --destructive-er-aggressive --destructive-er -F2 -winvfreqrank --forward-context-sr -c1 -Ginvfreq --prefer-initial-clauses -WSelectMaxLComplexAvoidPosPred -H'(4*PNRefinedweight(PreferNonGoals,4,5,5,4,2,1,1),8*PNRefinedweight(PreferGoals,5,2,2,5,2,1,0.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 668 669"protokoll_U----_043_K19_F1_PI_AE_CS_SP_S0Y":" --definitional-cnf=24 --delete-bad-limit=150000000 --tstp-in --simul-paramod --destructive-er-aggressive --destructive-er -F1 -winvmodfreqrankmax0 -c1 -Ginvfreqhack --forward-context-sr --prefer-initial-clauses -WSelectMaxLComplexAvoidPosPred -H'(4*PNRefinedweight(PreferNonGoals,4,5,5,4,2,1,1),8*PNRefinedweight(PreferGoals,5,2,2,5,2,1,0.5),1*FIFOWeight(ConstPrio))' -s --print-statistics --print-pid --resources-info --memory-limit=192", 670} 671 672def run_prover(schedule, filename): 673 """ 674 Run the prover according to the schedule provided. Return 675 success/failure. 676 """ 677 res = "# SZS status: ResourceOut" 678 count=1 679 count2=1 680 total=0 681 rest=0 682 683 for item in schedule: 684 count=count+1 685 686 for strat in schedule: 687 count2=count2+1 688 689 total = total+strat[1] 690 print strat 691 if(count==count2): 692 rest = 600-total 693 print "Additional Time",rest 694 695 696 #option = strat_options[strat[0]] 697 time = int((strat[1]+rest) * e_mark_scale); 698 p=os.popen("eprover "+strat_options[strat[0]]+\ 699 " "+"--tstp-in --cpu-limit="+ str(time)+" "+filename, "r"); 700 #print "pass" 701 res=p.readlines() 702 p.close() 703 for lines in res: 704 #print lines 705 if(lines.rstrip()=="# SZS status: Unsatisfiable" \ 706 or lines.rstrip()=="# SZS status: Satisfiable"\ 707 or lines.rstrip()=="# SZS status: Theorem"\ 708 or lines.rstrip()=="# SZS status: CounterSatisfiable"): 709 return lines 710 break; 711 712 return "SZS status: GaveUp" 713 714 715 716# This should have one entry per class! 717 718schedules = { 719"CLASS_G-SF-FFSS11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 720"CLASS_H-NM-FFMM31-D":[ ("protokoll_H----_011_B31_F1_PI_AE_SP_S1U", 300.0 ) ], 721"CLASS_H-NS-FFSF21-D":[ ("protokoll_H----_011_K07_F1_PI_AE_S4_CS_SP_SOV", 300.0 ) , ("protokoll_H----_102_K18_F1_PI_AE_S4_CS_S1S", 150.0 ) ], 722"CLASS_H-NS-FFSF11-D":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 723"CLASS_G-NF-MMMS00-M":[ ("protokoll_H----_031_K18_F1_PI_AE_CS_SP_S0Y", 300.0 ) ], 724"CLASS_G-SF-FFSS21-M":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 725"CLASS_G-NF-FSMF11-M":[ ("protokoll_H----_031_K09_F1_PI_AE_SP_S0Y", 300.0 ) ], 726"CLASS_G-SF-SSMF32-M":[ ], 727"CLASS_H-SM-FFSF22-M":[ ("protokoll_H----_042_B03_F1_PI_AE_SP_S2S", 300.0 ) ], 728"CLASS_G-SF-SSMF31-M":[ ("protokoll_G-E--_029_K18_F1_PI_AE_R12_CS_SP_S0Y", 300.0 ) ], 729"CLASS_G-NM-SSMS22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 730"CLASS_G-NF-FFSS22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 731"CLASS_G-NF-FFMF31-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 732"CLASS_G-NF-SFMM00-M":[ ("protokoll_H----_102_K18_F1_PI_AE_S4_CS_S1S", 300.0 ) , ("protokoll_G-E--_012_B31_F1_PI_AE_S4_CS_SP_S2S", 150.0 ) , ("protokoll_H----_042_B03_F1_PI_AE_SP_S0Y", 75.0 ) ], 733"CLASS_G-NF-FFMF32-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 734"CLASS_G-SS-MMLM22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 735"CLASS_H-NS-FFSF21-M":[ ("protokoll_H----_011_K07_F1_PI_AE_S4_CS_SP_SOV", 300.0 ) , ("protokoll_H----_102_K18_F1_PI_AE_S4_CS_S1S", 150.0 ) ], 736"CLASS_G-SF-SMMM31-M":[ ("protokoll_G-E--_029_K18_F1_PI_AE_R12_CS_SP_S0Y", 300.0 ) ], 737"CLASS_H-NF-SFMM00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 738"CLASS_G-SS-SSMM32-M":[ ], 739"CLASS_G-SF-SSMS32-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 740"CLASS_G-NF-FFMF11-M":[ ("protokoll_H----_042_B07_F1_PI_AE_SP_S2S", 300.0 ) , ("protokoll_G-E--_010_K08_F1_PI_AE_S4_CS_SP_S0Y", 150.0 ) ], 741"CLASS_H-SF-SFMF11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 742"CLASS_H-NM-FFMS21-D":[ ("protokoll_G-E--_030_K16_F1_PI_AE_CS_S4_S0Y", 300.0 ) , ("protokoll_H----_011_K07_F1_PI_AE_SP_SOV", 150.0 ) , ("protokoll_G-E--_045_K18_F1_PI_AE_CS_SP_S00", 75.0 ) ], 743"CLASS_H-SM-FFSS21-D":[ ("protokoll_H----_102_K18_F1_PI_AE_S4_CS_S1S", 300.0 ) ], 744"CLASS_G-SM-SSMM33-M":[ ("protokoll_G-E--_042_K18_F1_PI_AE_R7_CS_SP_S0Y", 300.0 ) ], 745"CLASS_H-SM-FFSF22-D":[ ("protokoll_H----_036_K18_F2_PI_AE_R12_SP_S2S", 300.0 ) ], 746"CLASS_G-NF-FFMS21-M":[ ("protokoll_H----_102_K18_F1_PI_AE_S4_CS_S2S", 300.0 ) , ("protokoll_H----_042_B03_F1_PI_AE_SP_S2S", 150.0 ) , ("protokoll_H----_011_K07_F1_PI_AE_S4_CS_SP_S0Y", 75.0 ) , ("protokoll_G-E--_020_K18_F1_PI_AE_S4_CS_SP_S0Y", 37.5 ) , ("protokoll_G-E--_045_K18_F1_PI_AE_S4_CS_OS_S2S", 18.75 ) , ("protokoll_G-E--_012_K18_F1_PI_AE_CS_SP_S0Y", 9.375 ) , ("protokoll_H----_042_B30_F1_PI_AE_SP_S2S", 4.6875 ) ], 747"CLASS_G-NS-FFMF32-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 748"CLASS_G-NF-FFSS21-M":[ ("protokoll_G-E--_010_K18_F1_PI_AE_S4_CS_SP_S3T", 300.0 ) ], 749"CLASS_H-PM-FFSF22-M":[ ("protokoll_H----_042_B31_F1_PI_AE_SP_S2S", 300.0 ) ], 750"CLASS_G-NF-FFSS00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 751"CLASS_H-SF-FFSM22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 752"CLASS_G-SM-SFMM33-M":[ ("protokoll_G-E--_045_K18_F1_PI_AE_S4_SP_S0Y", 300.0 ) ], 753"CLASS_H-NM-SSMS22-D":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 754"CLASS_H-SF-FFSF33-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 755"CLASS_G-NF-FFSM00-M":[ ("protokoll_H----_011_B31_F1_PI_AE_SP_S1U", 300.0 ) ], 756"CLASS_G-PF-SFMF00-M":[ ], 757"CLASS_H-PM-FFSF21-D":[ ("protokoll_H----_042_B07_F1_PI_AE_SP_S2S", 300.0 ) ], 758"CLASS_H-PM-FFSF21-M":[ ("protokoll_H----_036_K18_F2_PI_AE_R12_SP_S2S", 300.0 ) ], 759"CLASS_G-SF-SFMM21-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 760"CLASS_G-NF-SSLF21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 761"CLASS_G-SF-SSLF33-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 762"CLASS_G-SM-FFMF32-M":[ ("protokoll_G-E--_010_B31_F1_PI_AE_S4_CS_SP_S2S", 300.0 ) ], 763"CLASS_H-SM-FFSF21-M":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) , ("protokoll_H----_102_B30_F1_PI_AE_S4_CS_SP_S2S", 150.0 ) ], 764"CLASS_G-NM-SFMF22-D":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 765"CLASS_H-NF-FFMF11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 766"CLASS_G-NM-SFMF22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 767"CLASS_H-SM-FFSF21-D":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) , ("protokoll_G-E--_012_B31_F1_PI_AE_S4_CS_SP_S2S", 150.0 ) ], 768"CLASS_G-NM-FFMS22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 769"CLASS_G-NF-MMLM21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 770"CLASS_H-SM-FFSM33-D":[ ], 771"CLASS_G-NS-SSMF32-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 772"CLASS_G-NS-FFMS21-D":[ ("protokoll_G-E--_030_K16_F1_PI_AE_CS_S4_S0Y", 300.0 ) ], 773"CLASS_H-SF-FFSS31-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 774"CLASS_G-NS-FFMM00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 775"CLASS_G-SF-FFMM22-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 776"CLASS_G-NF-FFMS32-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 777"CLASS_G-SS-FFMF21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 778"CLASS_G-PM-FFSF22-M":[ ("protokoll_H----_042_B07_F1_PI_AE_SP_S2S", 300.0 ) ], 779"CLASS_G-SF-SSLM33-M":[ ], 780"CLASS_G-SM-FFSS11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 781"CLASS_G-SM-FFMS33-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 782"CLASS_G-SF-FFMF22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 783"CLASS_G-NF-FFMS31-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 784"CLASS_G-NF-MMLM22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 785"CLASS_G-NS-FFSF11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 786"CLASS_G-SS-SSMS21-M":[ ("protokoll_G-E--_023_K07_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 787"CLASS_G-SF-FFSM00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 788"CLASS_G-NF-FFSF31-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 789"CLASS_G-SM-MSMM22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 790"CLASS_G-SF-FFMM21-M":[ ("protokoll_G-E--_012_B31_F1_PI_AE_S4_CS_SP_S2S", 300.0 ) ], 791"CLASS_H-PM-FFMF21-D":[ ("protokoll_H----_081_K18_F1_PI_AE_Q12_CS_SP_S2S", 300.0 ) ], 792"CLASS_G-NM-SFMM21-D":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 793"CLASS_G-NM-SFMM21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 794"CLASS_G-NS-FFMF11-M":[ ("protokoll_G-E--_010_K08_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 795"CLASS_G-PM-FFSF21-M":[ ("protokoll_G-E--_032_K18_F1_PI_AE_S4_CS_SP_S2S", 300.0 ) , ("protokoll_H----_081_K18_F1_PI_AE_Q12_CS_SP_S2S", 150.0 ) , ("protokoll_G-E--_001_K18_F1_PI_AE_S4_CS_SP_S0Y", 75.0 ) , ("protokoll_G-E--_029_K07_F1_PI_AE_S4_CS_SP_S0Y", 37.5 ) ], 796"CLASS_G-NS-FFMF11-D":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 797"CLASS_G-PM-FFSF21-D":[ ("protokoll_G-E--_012_B31_F1_PI_AE_S4_CS_SP_S2S", 300.0 ) ], 798"CLASS_H-NF-SSMF00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 799"CLASS_G-SM-SMMM21-M":[ ("protokoll_G-E--_044_K18_F1_PI_AE_S4_CS_SP_S2S", 300.0 ) , ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 150.0 ) , ("protokoll_H----_011_K18_F1_PI_AE_SP_S2S", 75.0 ) , ("protokoll_G-E--_045_B07_F1_PI_AE_Q4_CS_SP_S2S", 37.5 ) , ("protokoll_G-E--_021_K07_F1_PI_AE_S4_CS_SP_S0Y", 18.75 ) ], 800"CLASS_G-PF-MSLM22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 801"CLASS_G-SM-SMMM21-D":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 802"CLASS_H-NM-SFMF22-D":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 803"CLASS_H-NM-FFSF11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 804"CLASS_G-NM-FFMS21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 805"CLASS_H-NF-FFSS22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 806"CLASS_G-SF-SFMM32-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 807"CLASS_H-NM-SFMF22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 808"CLASS_G-NM-FFMS21-D":[ ("protokoll_H----_036_K18_F2_PI_AE_R12_SP_S2S", 300.0 ) ], 809"CLASS_H-NF-FFSS21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 810"CLASS_G-PF-MSLM21-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 811"CLASS_G-SF-SFMF31-M":[ ("protokoll_G-E--_012_B31_F1_PI_AE_S4_CS_SP_S2S", 300.0 ) ], 812"CLASS_G-SS-FFMS21-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 813"CLASS_U-PM-FFSF32-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 814"CLASS_G-NF-SFMF11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 815"CLASS_H-SF-SFMM00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 816"CLASS_G-NS-SSMF11-M":[ ("protokoll_G-E--_010_K09_F1_PI_AE_Q4_CS_SP_S0Y", 300.0 ) ], 817"CLASS_G-SS-FFMF22-M":[ ("protokoll_G-E--_012_K18_F1_PI_AE_CS_SP_S0Y", 300.0 ) , ("protokoll_G-N--_023_K07_F1_PI_Q4_CS_SP_S0Y", 150.0 ) ], 818"CLASS_G-NF-MMLM00-M":[ ("protokoll_G-E--_044_K18_F1_PI_AE_S4_S1S", 300.0 ) , ("protokoll_H----_011_K07_F1_PI_AE_Q4_SP_SOV", 150.0 ) , ("protokoll_H----_011_K07_F1_PI_AE_OS_S1U", 75.0 ) ], 819"CLASS_H-PM-FFSS21-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 820"CLASS_H-PM-FFSS22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 821"CLASS_U-PS-FFSF11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 822"CLASS_H-NF-FFMF32-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 823"CLASS_G-SF-SFMF32-M":[ ("protokoll_G-E--_030_K16_F1_PI_AE_CS_S4_SP_S0Y", 300.0 ) , ("protokoll_G-E--_012_B31_F1_PI_AE_S4_CS_SP_S2S", 150.0 ) , ("protokoll_H----_042_B07_F1_PI_AE_SP_S2S", 75.0 ) ], 824"CLASS_G-NF-MMLS32-M":[ ], 825"CLASS_H-NM-FFMS21-M":[ ("protokoll_H----_036_K18_F2_PI_AE_R12_SP_S2S", 300.0 ) ], 826"CLASS_U-NS-FFSF11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 827"CLASS_G-NF-MMLF21-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 828"CLASS_H-SF-FFSF22-M":[ ], 829"CLASS_G-SF-SFMM00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 830"CLASS_G-NF-FFSF32-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 831"CLASS_U-PF-FFSF22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 832"CLASS_H-SM-FFMF32-D":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 833"CLASS_U-PF-FFSF22-D":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 834"CLASS_G-SF-FFMF21-M":[ ("protokoll_G-E--_024_K07_F1_PI_AE_Q4_CS_SP_S0Y", 300.0 ) , ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 150.0 ) ], 835"CLASS_H-SF-FFSS22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 836"CLASS_G-SF-SSMM33-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 837"CLASS_G-NF-FFSM22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 838"CLASS_G-NF-SFMM33-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 839"CLASS_H-NF-FFSS00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 840"CLASS_G-NM-FFMM21-M":[ ("protokoll_H----_036_K18_F2_PI_AE_R12_SP_S2S", 300.0 ) ], 841"CLASS_G-PF-MSMM21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 842"CLASS_G-SM-SFMM31-M":[ ], 843"CLASS_G-PF-FFSF11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 844"CLASS_G-SF-FFSF31-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 845"CLASS_G-PM-FFMF21-D":[ ], 846"CLASS_U-PM-FFMM21-D":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 847"CLASS_U-PF-FFSF21-D":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 848"CLASS_U-PF-FFSF32-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 849"CLASS_H-PF-FFSF21-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 850"CLASS_U-PF-FFSF21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 851"CLASS_U-PF-FFSF11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 852"CLASS_H-SF-SSMM33-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 853"CLASS_H-NM-MMLM00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 854"CLASS_H-NM-FFSF33-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 855"CLASS_G-PF-SSMM22-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 856"CLASS_G-SF-MMMM31-M":[ ("protokoll_H----_031_K18_F1_PI_AE_CS_SP_S0Y", 300.0 ) ], 857"CLASS_G-SM-FFSF11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 858"CLASS_H-PF-FFSS22-M":[ ("protokoll_H----_102_K18_F1_PI_AE_S4_CS_S2S", 300.0 ) ], 859"CLASS_H-NF-FFSF21-D":[ ("protokoll_G-E--_021_B31_F1_PI_AE_S4_CS_SP_S2S", 300.0 ) ], 860"CLASS_G-NF-SMMS00-M":[ ("protokoll_G-E--_023_K07_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 861"CLASS_U-NF-FFSF00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 862"CLASS_H-NF-FFSF21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 863"CLASS_G-NF-MMLF11-M":[ ("protokoll_H----_102_K18_F1_PI_AE_S4_CS_S1S", 300.0 ) , ("protokoll_G-E--_023_K07_F1_PI_AE_S4_CS_SP_S0Y", 150.0 ) ], 864"CLASS_H-NF-FFMM22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 865"CLASS_G-SF-FFMS22-M":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 866"CLASS_G-PF-SFMM21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 867"CLASS_G-SF-MMLM31-D":[ ], 868"CLASS_G-SM-SSMM21-M":[ ("protokoll_G-E--_010_B31_F1_PI_AE_S4_CS_SP_S2S", 300.0 ) , ("protokoll_G-E--_045_K18_F1_PI_AE_CS_SP_S00", 150.0 ) , ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 75.0 ) ], 869"CLASS_G-SF-SFMS32-M":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) , ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 150.0 ) ], 870"CLASS_G-SF-MMLM31-M":[ ("protokoll_G-E--_023_K07_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 871"CLASS_H-NS-FFMF21-D":[ ("protokoll_G-E--_029_K18_F1_PI_AE_R12_CS_SP_S0Y", 300.0 ) ], 872"CLASS_G-SM-SSMM21-D":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 873"CLASS_H-NF-SFMS00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 874"CLASS_G-NF-FFMM22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 875"CLASS_H-PS-FFSS22-M":[ ], 876"CLASS_H-NF-FFMM32-D":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 877"CLASS_H-NF-SFMS11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 878"CLASS_H-NF-FFSF00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 879"CLASS_H-NF-FFSF22-M":[ ("protokoll_G-E--_045_K18_F1_PI_AE_CS_SP_S1S", 300.0 ) , ("protokoll_G-E--_050_K18_F1_PI_AE_Q4_CS_SP_S0Y", 150.0 ) ], 880"CLASS_H-NF-FFSF22-D":[ ("protokoll_G-E--_045_K18_F1_PI_AE_CS_SP_S00", 300.0 ) , ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 150.0 ) ], 881"CLASS_G-SF-MMLM00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 882"CLASS_G-NM-FFMF31-M":[ ("protokoll_H----_036_K18_F2_PI_AE_R12_SP_S2S", 300.0 ) ], 883"CLASS_G-NF-MMLF00-M":[ ("protokoll_G-E--_023_K07_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 884"CLASS_G-NM-FFMF31-D":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 885"CLASS_G-NF-FFSM21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 886"CLASS_G-SS-FFSM21-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 887"CLASS_G-SF-FFSF00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 888"CLASS_G-SM-SFMS33-M":[ ("protokoll_G-E--_044_K18_F1_PI_AE_S4_S1S", 300.0 ) ], 889"CLASS_G-NF-FFSF11-D":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 890"CLASS_G-NF-FFSF11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 891"CLASS_G-SM-SSLM31-D":[ ("protokoll_G-E--_008_K18_F1_PI_AE_CS_SP_S0Y", 300.0 ) , ("protokoll_H----_081_K18_F1_PI_AE_Q12_CS_SP_S2S", 150.0 ) , ("protokoll_H----_102_B03_F1_PI_AE_S4_CS_SP_S2S", 75.0 ) , ("protokoll_G-E--_051_K18_F1_PI_AE_Q4_CS_SP_S0Y", 37.5 ) , ("protokoll_G-E--_040_K18_F1_PI_AE_S4_CS_SP_S0Y", 18.75 ) , ("protokoll_H----_081_B31_F1_PI_AE_S4_CS_SP_S0Y", 9.375 ) ], 892"CLASS_G-NF-FFSF33-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 893"CLASS_G-NF-FFMM00-M":[ ("protokoll_H----_011_B31_F1_PI_AE_SP_S1U", 300.0 ) ], 894"CLASS_G-SM-MMLM21-D":[ ], 895"CLASS_G-SS-SSMF32-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 896"CLASS_G-SM-FFMF21-D":[ ], 897"CLASS_G-SS-FFSS21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 898"CLASS_U-SM-FFMM21-D":[ ("protokoll_H----_102_B30_F1_PI_AE_S4_CS_SP_S2S", 300.0 ) ], 899"CLASS_G-NF-FFMS00-M":[ ("protokoll_G-E--_044_K18_F1_PI_AE_S4_S0Y", 300.0 ) ], 900"CLASS_G-SM-MMMM31-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 901"CLASS_U-PM-FFSF22-M":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 902"CLASS_G-NM-SSMM31-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 903"CLASS_G-SF-FFMS21-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) , ("protokoll_G-E--_012_K18_F1_PI_AE_CS_SP_S0Y", 150.0 ) ], 904"CLASS_G-NM-SSMM31-D":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 905"CLASS_G-NF-SFSM00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 906"CLASS_H-NF-FFMM21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 907"CLASS_U-PM-FFSF22-D":[ ("protokoll_H----_042_B07_F1_PI_AE_SP_S2S", 300.0 ) ], 908"CLASS_G-SM-FFMS22-M":[ ("protokoll_H----_102_K18_F1_PI_AE_S4_CS_S2S", 300.0 ) ], 909"CLASS_H-PS-FFSF22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 910"CLASS_H-PS-FFSF21-D":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 911"CLASS_H-SM-FFMM22-M":[ ("protokoll_G-E--_045_K18_F1_PI_AE_S4_CS_OS_S2S", 300.0 ) ], 912"CLASS_H-PS-FFSF22-D":[ ], 913"CLASS_H-PS-FFSF21-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 914"CLASS_H-NF-SFMM11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 915"CLASS_G-NF-SFMM11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 916"CLASS_G-NF-SSMM11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 917"CLASS_H-SF-FFMM21-M":[ ("protokoll_H----_102_K18_F1_PI_AE_S4_CS_S2S", 300.0 ) ], 918"CLASS_H-NS-FFMM32-D":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 919"CLASS_H-SM-FFSS21-M":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 920"CLASS_G-SS-FFSF22-M":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 921"CLASS_G-NS-FFSF22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 922"CLASS_G-NF-SSMM32-M":[ ], 923"CLASS_H-NS-FFMS11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 924"CLASS_G-SS-SSMS32-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 925"CLASS_H-NM-FFMF31-M":[ ("protokoll_H----_036_K18_F2_PI_AE_R12_SP_S2S", 300.0 ) ], 926"CLASS_G-NS-SFMS00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 927"CLASS_G-NF-SSMS32-M":[ ], 928"CLASS_U-NM-FFSF22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 929"CLASS_G-SF-SSMM31-M":[ ("protokoll_G-E--_042_K18_F1_PI_AE_R7_CS_SP_S0Y", 300.0 ) ], 930"CLASS_G-SF-SSMM31-D":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 931"CLASS_G-SF-SSMM32-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) , ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 150.0 ) ], 932"CLASS_H-NS-FFSF00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 933"CLASS_G-NF-SFMM32-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 934"CLASS_G-NF-SFMS00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 935"CLASS_G-NF-SSMF32-M":[ ], 936"CLASS_G-NS-FFSF21-M":[ ("protokoll_G-N--_023_B07_F1_PI_S4_CS_SP_S0Y", 300.0 ) ], 937"CLASS_G-NS-FFSF21-D":[ ], 938"CLASS_G-PF-MMLM21-M":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) , ("protokoll_G-E--_012_B31_F1_PI_AE_S4_CS_SP_S2S", 150.0 ) ], 939"CLASS_G-SM-MMLM22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 940"CLASS_U-PF-FFSM22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 941"CLASS_H-SS-FFSF21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 942"CLASS_H-SF-FFSS21-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 943"CLASS_H-SF-SSMM11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 944"CLASS_G-SF-SMMM21-D":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 945"CLASS_G-NF-FFSS11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 946"CLASS_H-NM-FFMS31-D":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 947"CLASS_H-SS-FFSF22-M":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 948"CLASS_G-SM-FFMS21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 949"CLASS_G-SF-SMMM21-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) , ("protokoll_G-E--_021_B31_F1_PI_AE_S4_CS_SP_S2S", 150.0 ) , ("protokoll_H----_102_K18_F1_PI_AE_S4_CS_S1S", 75.0 ) , ("protokoll_H----_036_K18_F2_PI_AE_R12_SP_S2S", 37.5 ) , ("protokoll_G-E--_045_K18_F1_PI_AE_CS_SP_S00", 18.75 ) , ("protokoll_H----_011_K07_F1_PI_AE_S4_CS_SP_S0Y", 9.375 ) ], 950"CLASS_H-SS-FFSF22-D":[ ("protokoll_H----_011_K07_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) , ("protokoll_H----_011_B31_F1_PI_AE_SP_S1U", 150.0 ) ], 951"CLASS_H-NM-FFMS31-M":[ ("protokoll_G-E--_045_K18_F1_PI_AE_CS_SP_S00", 300.0 ) ], 952"CLASS_G-NM-FFMS31-D":[ ("protokoll_G-E--_008_K18_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 953"CLASS_U-PS-FFSF21-D":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) , ("protokoll_H----_042_B07_F1_PI_AE_SP_S2S", 150.0 ) ], 954"CLASS_G-NS-FSMF11-M":[ ("protokoll_G-E--_045_K18_F1_PI_AE_S4_SP_S0Y", 300.0 ) , ("protokoll_H----_011_B31_F1_PI_AE_SP_S1U", 150.0 ) ], 955"CLASS_U-PS-FFSF21-M":[ ("protokoll_U----_043_K19_F1_PI_AE_CS_SP_S0Y", 300.0 ) , ("protokoll_G-E--_051_K18_F1_PI_AE_Q4_CS_SP_S0Y", 150.0 ) ], 956"CLASS_G-NS-SFMM00-M":[ ("protokoll_G-E--_045_K18_F1_PI_AE_S4_SP_S0Y", 300.0 ) ], 957"CLASS_G-SS-SSMS31-D":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 958"CLASS_H-NS-FFSF31-M":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 959"CLASS_G-SS-FFSF21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 960"CLASS_G-NM-SSMM00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 961"CLASS_H-SM-FFSS22-M":[ ("protokoll_H----_036_K18_F2_PI_AE_R12_SP_S2S", 300.0 ) ], 962"CLASS_U-NF-FFSM32-D":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 963"CLASS_G-NM-FFSF21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 964"CLASS_G-PF-MMLM22-D":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 965"CLASS_G-SF-SFMS31-M":[ ("protokoll_G-E--_029_K18_F1_PI_AE_R4_CS_SP_S0Y", 300.0 ) , ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 150.0 ) ], 966"CLASS_G-SF-SSMF21-M":[ ], 967"CLASS_G-SM-MSMS32-M":[ ], 968"CLASS_G-PF-MMLM22-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 969"CLASS_H-NM-FFMM00-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 970"CLASS_U-PF-FFSM21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 971"CLASS_H-NM-SFMM21-D":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 972"CLASS_H-NM-SSMF22-D":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 973"CLASS_H-PF-FFSF22-M":[ ], 974"CLASS_U-NS-FFSF22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 975"CLASS_G-NM-FFMF22-D":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 976"CLASS_U-PF-FFSS22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 977"CLASS_U-PS-FFSF22-M":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) , ("protokoll_G-E--_052_K18_F1_PI_AE_Q4_CS_SP_S0Y", 150.0 ) ], 978"CLASS_G-SM-FFMF22-M":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 979"CLASS_G-SF-FFMM31-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 980"CLASS_U-PS-FFSF22-D":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) , ("protokoll_G-E--_024_B07_F1_PI_AE_Q4_CS_SP_S0Y", 150.0 ) ], 981"CLASS_U-SM-SFMM21-M":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 982"CLASS_G-SM-MMLM21-M":[ ("protokoll_G-E--_042_K18_F1_PI_AE_R7_CS_SP_S0Y", 300.0 ) ], 983"CLASS_G-SM-FFMF21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 984"CLASS_H-SM-SFMM21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 985"CLASS_G-NS-FFSS00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 986"CLASS_G-NF-SFMF21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 987"CLASS_G-NF-MMLM31-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 988"CLASS_G-SF-MMLS31-D":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 989"CLASS_G-NS-FFMF21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 990"CLASS_G-NF-SSMM11-D":[ ], 991"CLASS_H-NS-FFSF11-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 992"CLASS_G-NS-FFMM21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 993"CLASS_G-NS-FFMF21-D":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 994"CLASS_G-SM-FFSS21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 995"CLASS_U-SM-SFMM22-M":[ ("protokoll_G-E--_023_K07_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 996"CLASS_G-NF-FFMF22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 997"CLASS_G-NF-FFMF21-M":[ ("protokoll_H----_042_B07_F1_PI_AE_SP_S2S", 300.0 ) ], 998"CLASS_G-SM-MSMM32-M":[ ], 999"CLASS_G-SM-SSMF31-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 1000"CLASS_H-NS-FFSF22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1001"CLASS_G-SM-SFMS21-D":[ ("protokoll_G-E--_042_K18_F1_PI_AE_R8_CS_SP_S0Y", 300.0 ) ], 1002"CLASS_G-SF-FFMM32-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1003"CLASS_U-PF-FFSF00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1004"CLASS_G-NF-FFMF00-M":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 1005"CLASS_H-PM-FFMM21-D":[ ], 1006"CLASS_H-NF-FFMF21-D":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 1007"CLASS_U-PS-FFSS21-D":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1008"CLASS_H-NF-FFMF21-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 1009"CLASS_G-SM-SSMS33-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1010"CLASS_G-SF-FFSM11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1011"CLASS_G-NF-FFSS32-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1012"CLASS_G-SM-SSMS31-M":[ ("protokoll_G-E--_042_K18_F1_PI_AE_R7_CS_SP_S0Y", 300.0 ) ], 1013"CLASS_G-NF-FFMM21-M":[ ("protokoll_H----_102_B31_F1_PI_AE_S4_CS_SP_S2S", 300.0 ) , ("protokoll_G-E--_010_K18_F1_PI_AE_S4_CS_SP_S3S", 150.0 ) , ("protokoll_G-E--_021_B31_F1_PI_AE_S4_CS_SP_S2S", 75.0 ) ], 1014"CLASS_H-NM-FFMF33-M":[ ], 1015"CLASS_G-NF-MMLM32-M":[ ("protokoll_G-E--_012_B31_F1_PI_AE_S4_CS_SP_S2S", 300.0 ) ], 1016"CLASS_H-NS-FFSF33-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1017"CLASS_G-NM-SFMM31-M":[ ], 1018"CLASS_H-NM-SFMM22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1019"CLASS_H-NM-FFSS11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1020"CLASS_G-NM-FFMS11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1021"CLASS_G-NM-SFMM31-D":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 1022"CLASS_G-SS-FFMS33-M":[ ("protokoll_G-E--_024_B31_F1_PI_AE_Q4_CS_SP_S0Y", 300.0 ) , ("protokoll_H----_042_B03_F1_PI_AE_SP_S0Y", 150.0 ) ], 1023"CLASS_G-SF-FFSF21-M":[ ("protokoll_H----_081_B02_F1_PI_AE_S4_CS_SP_S2S", 300.0 ) ], 1024"CLASS_G-SF-FFSF22-D":[ ], 1025"CLASS_H-NS-FFSS11-D":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1026"CLASS_G-NS-FFMS21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1027"CLASS_G-SF-FFSF22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1028"CLASS_G-SF-FFSF11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1029"CLASS_H-SF-SSMM00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1030"CLASS_G-PF-SSLM22-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 1031"CLASS_G-NF-MMLS00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1032"CLASS_U-PM-FFSS21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1033"CLASS_H-SM-FFSF32-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 1034"CLASS_G-NM-FFMF32-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1035"CLASS_G-SF-SSMM21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1036"CLASS_H-SF-FFSS32-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1037"CLASS_G-NF-MMLS31-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 1038"CLASS_H-SF-FFSF21-M":[ ("protokoll_G-E--_012_B31_F1_PI_AE_S4_CS_SP_S2S", 300.0 ) ], 1039"CLASS_G-NF-SSMM00-M":[ ("protokoll_G-E--_045_K18_F1_PI_AE_CS_SP_S1S", 300.0 ) ], 1040"CLASS_U-NF-FFSF11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1041"CLASS_U-NF-FFSF21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1042"CLASS_G-SM-FFSF21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1043"CLASS_G-SF-SMLM33-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1044"CLASS_G-SM-FFSF21-D":[ ], 1045"CLASS_G-SM-SFMM31-D":[ ("protokoll_G-E--_042_K18_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) , ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 150.0 ) , ("protokoll_G-E--_001_B31_F1_PI_AE_S4_CS_OS_S2S", 75.0 ) ], 1046"CLASS_G-NM-FFMS32-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1047"CLASS_H-NF-FFSS32-D":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1048"CLASS_G-SM-FFSF22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1049"CLASS_H-NF-FFSM00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1050"CLASS_U-PM-FFSS22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1051"CLASS_H-NM-FFMM21-D":[ ("protokoll_G-E--_024_B31_F1_PI_AE_Q4_CS_SP_S0Y", 300.0 ) ], 1052"CLASS_G-NM-FFMM32-M":[ ], 1053"CLASS_H-NM-FFMM21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1054"CLASS_G-NF-SMMM00-M":[ ("protokoll_G-E--_022_K18_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) , ("protokoll_G-E--_008_K18_F1_PI_AE_CS_SP_S0Y", 150.0 ) , ("protokoll_H----_036_K18_F2_PI_AE_R12_SP_S2S", 75.0 ) , ("protokoll_U----_043_K19_F1_PI_AE_CS_SP_S0Y", 37.5 ) ], 1055"CLASS_G-SM-SFMM21-D":[ ("protokoll_G-E--_008_K18_F1_PI_AE_CS_SP_S0Y", 300.0 ) ], 1056"CLASS_G-SF-FFMM33-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 1057"CLASS_H-NF-FFSM22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1058"CLASS_G-SF-FFMF11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1059"CLASS_G-NF-SSMF11-M":[ ("protokoll_G-E--_032_K18_F1_PI_AE_S4_CS_SP_S2S", 300.0 ) , ("protokoll_G-E--_010_K08_F1_PI_AE_S4_CS_SP_S0Y", 150.0 ) ], 1060"CLASS_G-NF-SSMM22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1061"CLASS_H-SS-FFSS22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1062"CLASS_G-SM-SSMS32-M":[ ("protokoll_H----_024_K18_F1_PI_OP_AE_S4_CS_SP_S2S", 300.0 ) ], 1063"CLASS_G-NF-MMLM11-M":[ ], 1064"CLASS_H-NF-FFSM21-M":[ ("protokoll_H----_036_K18_F2_PI_AE_R12_SP_S2S", 300.0 ) ], 1065"CLASS_G-SF-MMMM21-D":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 1066"CLASS_G-NF-SFMF00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1067"CLASS_U-PM-FFMS21-M":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) , ("protokoll_H----_042_B07_F1_PI_AE_SP_S2S", 150.0 ) , ("protokoll_H----_081_B07_F1_PI_AE_S4_CS_SP_S2S", 75.0 ) ], 1068"CLASS_H-SM-FFMS21-M":[ ("protokoll_G-E--_045_K18_F1_PI_AE_S4_CS_OS_S2S", 300.0 ) ], 1069"CLASS_G-SM-SSMS31-D":[ ("protokoll_G-E--_030_K16_F1_PI_AE_CS_S4_S0Y", 300.0 ) , ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 150.0 ) ], 1070"CLASS_G-SF-MMMM21-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) , ("protokoll_G-E--_045_K18_F1_PI_AE_CS_SP_S00", 150.0 ) ], 1071"CLASS_U-NF-FFSF22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1072"CLASS_H-NF-SFMF11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1073"CLASS_G-NF-FFSF00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1074"CLASS_G-SM-SMMM31-M":[ ("protokoll_H----_036_K18_F2_PI_AE_R12_SP_S2S", 300.0 ) ], 1075"CLASS_G-SF-FFMS31-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1076"CLASS_H-SM-FFMF21-M":[ ("protokoll_G-E--_012_B31_F1_PI_AE_S4_CS_SP_S2S", 300.0 ) ], 1077"CLASS_H-NS-FFMS21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1078"CLASS_G-NF-MMLM33-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1079"CLASS_H-SM-FFMF21-D":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1080"CLASS_H-SM-FFMF22-M":[ ], 1081"CLASS_H-SS-FFSS21-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 1082"CLASS_G-SF-SFMF21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1083"CLASS_H-NS-FFMS22-M":[ ("protokoll_H----_036_K18_F2_PI_AE_R12_SP_S2S", 300.0 ) ], 1084"CLASS_H-NF-FFMF00-M":[ ("protokoll_G-E--_045_K18_F1_PI_AE_CS_SP_S00", 300.0 ) ], 1085"CLASS_G-PM-FFSS22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1086"CLASS_G-SF-FFMS32-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1087"CLASS_G-NF-SMLF00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1088"CLASS_G-SM-SSMF33-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 1089"CLASS_U-PM-FFMF22-D":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 1090"CLASS_G-NF-FFSF21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1091"CLASS_U-PM-FFMF21-D":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1092"CLASS_G-NF-FFSF21-D":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1093"CLASS_U-PM-FFMF21-M":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) , ("protokoll_H----_042_B07_F1_PI_AE_SP_S2S", 150.0 ) ], 1094"CLASS_H-SF-SFMS11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1095"CLASS_G-SF-FFMF32-M":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 1096"CLASS_H-SF-SSMM22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1097"CLASS_H-SM-FFMM31-M":[ ("protokoll_H----_036_K18_F2_PI_AE_R12_SP_S2S", 300.0 ) ], 1098"CLASS_H-SF-SFMM22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1099"CLASS_G-SS-FFMF33-M":[ ("protokoll_G-E--_020_K18_F1_PI_AE_S4_CS_SP_S2S", 300.0 ) , ("protokoll_G-E--_004_K18_F1_AE_S4_CS_OS_S0Y", 150.0 ) , ("protokoll_G-E--_002_K18_F1_PI_AE_S4_CS_OS_S0Y", 75.0 ) ], 1100"CLASS_G-NF-FFMM33-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1101"CLASS_G-NF-SMMF11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1102"CLASS_H-SF-FFMS32-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1103"CLASS_G-NM-FFMF21-M":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 1104"CLASS_G-NF-SFSS00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1105"CLASS_G-PS-SFMM21-M":[ ("protokoll_H----_102_K18_F1_PI_AE_S4_CS_S2S", 300.0 ) ], 1106"CLASS_G-NM-FFMF21-D":[ ("protokoll_G-E--_010_B31_F1_PI_AE_S4_CS_SP_S2S", 300.0 ) ], 1107"CLASS_G-SF-MMLM21-M":[ ("protokoll_G-E--_003_K18_F1_PI_AE_S4_CS_SP_S2S", 300.0 ) ], 1108"CLASS_G-SF-SFMS21-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 1109"CLASS_G-SF-MMLM21-D":[ ], 1110"CLASS_G-SF-MMLM22-M":[ ("protokoll_G-E--_021_K07_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 1111"CLASS_G-NF-FFSF22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1112"CLASS_G-SF-FFMF31-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1113"CLASS_G-PF-FFMF11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1114"CLASS_H-SM-FFMS22-M":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 1115"CLASS_G-NF-MMMM00-M":[ ("protokoll_G-E--_033_K18_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) , ("protokoll_G-E--_010_K09_F1_PI_AE_Q4_CS_SP_S0Y", 150.0 ) ], 1116"CLASS_H-NM-SFMS22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1117"CLASS_U-PM-FFMF32-M":[ ], 1118"CLASS_G-SM-FFMM31-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1119"CLASS_G-SF-SSLS33-M":[ ("protokoll_H----_031_K18_F1_PI_AE_CS_SP_S3T", 300.0 ) ], 1120"CLASS_G-NM-SSMM22-D":[ ("protokoll_G-E--_023_K07_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 1121"CLASS_G-PF-FFSF00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1122"CLASS_G-NF-FFMF33-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1123"CLASS_G-NF-FFSM11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1124"CLASS_H-NM-FFMF22-D":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 1125"CLASS_G-SM-FFMF33-M":[ ("protokoll_G-E--_012_B31_F1_PI_AE_S4_CS_SP_S2S", 300.0 ) ], 1126"CLASS_H-NM-FFSF21-M":[ ("protokoll_U----_043_K18_F1_PI_AE_CS_OS_S0Y", 300.0 ) , ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 150.0 ) , ("protokoll_G-E--_003_K18_F1_PI_AE_S4_CS_SP_S2S", 75.0 ) ], 1127"CLASS_G-NF-SFMS11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1128"CLASS_G-SM-SSMM32-M":[ ], 1129"CLASS_H-NM-FFMF21-D":[ ("protokoll_H----_024_K18_F1_PI_OP_AE_S4_CS_SP_S2S", 300.0 ) ], 1130"CLASS_H-NF-FFSF11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1131"CLASS_H-NM-FFMF21-M":[ ("protokoll_H----_036_K18_F2_PI_AE_R12_SP_S2S", 300.0 ) ], 1132"CLASS_H-NF-FFSF11-D":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 1133"CLASS_G-SM-FFMM32-M":[ ], 1134"CLASS_G-NS-FFMS00-M":[ ("protokoll_H----_011_B31_F1_PI_AE_SP_S1U", 300.0 ) ], 1135"CLASS_H-NM-SFMF33-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1136"CLASS_H-PM-FFSM22-M":[ ("protokoll_G-E--_012_K31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 1137"CLASS_G-SM-MMMM21-M":[ ("protokoll_G-E--_052_K18_F1_PI_AE_Q4_CS_SP_S0Y", 300.0 ) ], 1138"CLASS_G-NF-SSMS11-M":[ ("protokoll_G-E--_045_K18_F1_PI_AE_S4_SP_S0Y", 300.0 ) ], 1139"CLASS_G-SM-MMMM21-D":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 1140"CLASS_G-SM-SSMM31-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 1141"CLASS_G-NF-FFMM31-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1142"CLASS_G-SM-SSMM31-D":[ ("protokoll_H----_102_B01_F1_PI_AE_S4_CS_SP_S2S", 300.0 ) ], 1143"CLASS_H-SF-SFMM11-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1144"CLASS_G-SF-SFMM31-M":[ ("protokoll_G-E--_008_B07_F1_PI_AE_Q4_CS_SP_S2S", 300.0 ) ], 1145"CLASS_U-PM-FFSF21-D":[ ("protokoll_G-E--_029_K18_F1_PI_AE_R12_CS_SP_S0Y", 300.0 ) ], 1146"CLASS_G-NM-SFMS22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1147"CLASS_G-SF-FFSS22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1148"CLASS_U-PM-FFSF21-M":[ ("protokoll_H----_081_K18_F1_PI_AE_Q12_CS_SP_S2S", 300.0 ) , ("protokoll_H----_102_B01_F1_PI_AE_S4_CS_SP_S2S", 150.0 ) ], 1149"CLASS_G-NM-SFMS22-D":[ ("protokoll_H----_036_K18_F2_PI_AE_R12_SP_S2S", 300.0 ) ], 1150"CLASS_H-NS-FFSF22-D":[ ("protokoll_G-E--_023_K07_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) , ("protokoll_G-E--_024_B07_F1_PI_AE_Q4_CS_SP_S0Y", 150.0 ) ], 1151"CLASS_G-NF-SFMM22-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1152"CLASS_G-SF-SFMM33-M":[ ("protokoll_H----_081_B31_F1_PI_AE_S4_CS_SP_S2S", 300.0 ) ], 1153"CLASS_G-NF-SFMM21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1154"CLASS_G-SF-SSMS31-D":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) , ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 150.0 ) ], 1155"CLASS_H-NM-SFMM31-D":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1156"CLASS_G-SF-SSMS31-M":[ ("protokoll_G-E--_012_B31_F1_PI_AE_Q4_CS_SP_S0Y", 300.0 ) ], 1157"CLASS_G-NF-SFMS32-M":[ ("protokoll_H----_102_B03_F1_PI_AE_S4_CS_SP_S2S", 300.0 ) ], 1158"CLASS_G-SS-FFMM33-M":[ ], 1159"CLASS_H-SS-FFSM22-M":[ ("protokoll_G-E--_021_B31_F1_PI_AE_S4_CS_SP_S2S", 300.0 ) ], 1160"CLASS_G-SF-MMLF33-M":[ ], 1161"CLASS_G-PS-FFMM21-M":[ ("protokoll_G-E--_029_K18_F1_PI_AE_R12_CS_SP_S0Y", 300.0 ) ], 1162"CLASS_H-SF-FFMM32-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 1163"CLASS_G-NF-FFMM32-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1164"CLASS_H-NS-FFMM21-D":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1165"CLASS_G-NF-SSMS00-M":[ ("protokoll_H----_011_K07_F1_PI_AE_OS_S1U", 300.0 ) ], 1166"CLASS_H-NM-FFSF22-M":[ ("protokoll_G-E--_008_K18_F1_PI_AE_R4_CS_SP_S2S", 300.0 ) ], 1167"CLASS_H-NM-FFSF21-D":[ ("protokoll_H----_072_K16_F1_PI_AE_CS_S4_S0Y", 300.0 ) , ("protokoll_G-E--_010_K08_F1_PI_AE_S4_CS_SP_S0Y", 150.0 ) , ("protokoll_H----_011_K07_F1_PI_AE_S4_CS_SP_S0Y", 75.0 ) , ("protokoll_H----_011_K07_F1_PI_AE_S4_CS_SP_SOV", 37.5 ) , ("protokoll_H----_011_K07_F1_PI_AE_OS_S1U", 18.75 ) ], 1168"CLASS_U-NF-FFSM00-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1169"CLASS_H-NM-FFSF22-D":[ ("protokoll_G-E--_012_B31_F1_PI_AE_S4_CS_SP_S0Y", 300.0 ) ], 1170"CLASS_G-SS-SSMF21-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1171"CLASS_G-SM-SFMF33-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1172"CLASS_G-SF-FFMF33-M":[ ("protokoll_G-E--_005_K18_F1_PI_AE_S4_CS_OS_S0Y", 300.0 ) ], 1173"DEFAULT":[("protokoll_G-E--_029_K18_F1_PI_AE_Q4_CS_SP_S0Y",300.0)], 1174} 1175 1176if __name__ == '__main__': 1177 for option in get_options(): 1178 if option == "-h": 1179 print __doc__ 1180 sys.exit() 1181 else: 1182 sys.exit("Unknown option "+ option) 1183 1184 e_mark_scale = 100.0 / 285.646; 1185 args = get_args() 1186 if len(args)!=1: 1187 print "Exactly one file name argument expected" 1188 sys.exit(1); 1189 1190 cl = get_problem_class(args[0]) 1191 try: 1192 #cl="vshsjhfsfhsfjhsfshhh" 1193 schedule = schedules[cl] 1194 if not schedule: 1195 raise schedule_unavailable 1196 1197 except : 1198 schedule = schedules["DEFAULT"]; 1199 1200 1201 res = run_prover(schedule, args[0]) 1202 print res 1203 resuse = resource.getrusage(resource.RUSAGE_CHILDREN) 1204 print """# ------------------------------------------------- 1205# User time : %f s 1206# System time : %f s 1207# Total time : %f s 1208# Maximum resident set size: %d pages 1209""" % (resuse.ru_utime/e_mark_scale, resuse.ru_stime/e_mark_scale, (resuse.ru_utime+resuse.ru_stime)/e_mark_scale,resuse.ru_maxrss) 1210 1211 1212