PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-timtab2.opb
MD5SUM	e4125be387acbcc645dccab0e301ae8f
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	3027
Biggest coefficient in the objective function	450560000000000
Number of bits for the biggest coefficient in the objective function	49
Sum of the numbers in the objective function	60439117299975427
Number of bits of the sum of numbers in the objective function	56
Biggest number in a constraint	450560000000000
Number of bits of the biggest number in a constraint	49
Biggest sum of numbers in a constraint	60439117299975427
Number of bits of the biggest sum of numbers	56
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.049991
Number of variables	5220
Total number of constraints	952
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	113
Number of constraints which are nor clauses,nor cardinality constraints	839
Minimum length of a constraint	1
Maximum length of a constraint	114
Trace number 31178

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-05-25 22:48:01 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22576 boxname=wulflinc19 idbench=1392 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  e4125be387acbcc645dccab0e301ae8f  /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-timtab2.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-timtab2.opb
IDLAUNCH: 22576
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        881180 kB
Buffers:         30804 kB
Cached:          96760 kB
SwapCached:        752 kB
Active:          23128 kB
Inactive:       106756 kB
HighTotal:      131008 kB
HighFree:        98504 kB
LowTotal:       903652 kB
LowFree:        782676 kB
SwapTotal:     2097892 kB
SwapFree:      2096424 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5404 kB
Slab:            18080 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 23:08:31 (client local time) WITH STATUS 152 IN 1229.88 SECONDS
stats: 22576 7 1229.88 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c PARSE ERROR! [line 679] Integer overflow. Use BigNum-version.
c OK -- Running BigNum-version instead...
c Parsing PB file...
c Converting 1079 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ######################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss................................................................................
c ---[1277]---> BDD-cost:    9
c ---[1276]---> BDD-cost:   12
c ---[1275]---> BDD-cost:   12
c ---[1274]---> BDD-cost:   12
c ---[1270]---> BDD-cost:   12
c ---[1269]---> BDD-cost:   12
c ---[1268]---> BDD-cost:    9
c ---[1262]---> BDD-cost:    9
c ---[1260]---> BDD-cost:   12
c ---[1259]---> BDD-cost:   12
c ---[1249]---> BDD-cost:   12
c ---[1247]---> BDD-cost:    9
c ---[1246]---> BDD-cost:   12
c ---[1242]---> BDD-cost:    9
c ---[1239]---> BDD-cost:    9
c ---[1238]---> BDD-cost:    9
c ---[1231]---> BDD-cost:    9
c ---[1229]---> BDD-cost:   12
c ---[1228]---> BDD-cost:   12
c ---[1225]---> BDD-cost:   12
c ---[1224]---> BDD-cost:   12
c ---[1223]---> BDD-cost:    9
c ---[1222]---> BDD-cost:   12
c ---[1221]---> BDD-cost:   12
c ---[1218]---> BDD-cost:    9
c ---[1213]---> BDD-cost:   12
c ---[1212]---> BDD-cost:   12
c ---[1211]---> BDD-cost:   12
c ---[1208]---> BDD-cost:   12
c ---[1203]---> BDD-cost:    9
c ---[1201]---> BDD-cost:   12
c ---[1200]---> BDD-cost:   12
c ---[1199]---> BDD-cost:   12
c ---[1198]---> BDD-cost:   12
c ---[1195]---> BDD-cost:   12
c ---[1194]---> BDD-cost:   12
c ---[1192]---> BDD-cost:    9
c ---[1191]---> BDD-cost:   12
c ---[1190]---> BDD-cost:   12
c ---[1189]---> BDD-cost:   12
c ---[1188]---> BDD-cost:   12
c ---[1187]---> BDD-cost:    9
c ---[1185]---> BDD-cost:   12
c ---[1184]---> BDD-cost:   12
c ---[1183]---> BDD-cost:   12
c ---[1182]---> BDD-cost:   12
c ---[1179]---> BDD-cost:   12
c ---[1178]---> BDD-cost:   12
c ---[1170]---> BDD-cost:    9
c ---[1169]---> BDD-cost:    9
c ---[1168]---> BDD-cost:   12
c ---[1167]---> BDD-cost:   12
c ---[1165]---> BDD-cost:    9
c ---[1164]---> BDD-cost:   12
c ---[1161]---> BDD-cost:    9
c ---[1156]---> BDD-cost:   12
c ---[1154]---> BDD-cost:   12
c ---[1153]---> BDD-cost:   12
c ---[1152]---> BDD-cost:   12
c ---[1151]---> BDD-cost:    9
c ---[1149]---> BDD-cost:    9
c ---[1147]---> BDD-cost:   12
c ---[1146]---> BDD-cost:   12
c ---[1145]---> BDD-cost:   12
c ---[1143]---> BDD-cost:   12
c ---[1142]---> BDD-cost:   12
c ---[1141]---> BDD-cost:   12
c ---[1140]---> BDD-cost:   12
c ---[1137]---> BDD-cost:    9
c ---[1136]---> BDD-cost:   12
c ---[1134]---> BDD-cost:   12
c ---[1128]---> BDD-cost:   12
c ---[1126]---> BDD-cost:    9
c ---[1125]---> BDD-cost:   12
c ---[1124]---> BDD-cost:   12
c ---[1123]---> BDD-cost:   12
c ---[1122]---> BDD-cost:   12
c ---[1121]---> BDD-cost:   12
c ---[1120]---> BDD-cost:   12
c ---[1119]---> BDD-cost:   12
c ---[1118]---> BDD-cost:   12
c ---[1112]---> BDD-cost:   12
c ---[1111]---> BDD-cost:    9
c ---[1110]---> BDD-cost:   12
c ---[1109]---> BDD-cost:   12
c ---[1108]---> BDD-cost:   12
c ---[1107]---> BDD-cost:   12
c ---[1103]---> BDD-cost:   12
c ---[1102]---> BDD-cost:   12
c ---[1101]---> BDD-cost:   12
c ---[1100]---> BDD-cost:    9
c ---[1096]---> BDD-cost:    9
c ---[1094]---> BDD-cost:   12
c ---[1092]---> BDD-cost:    9
c ---[1089]---> BDD-cost:   12
c ---[1088]---> BDD-cost:    9
c ---[1087]---> BDD-cost:   12
c ---[1086]---> BDD-cost:    9
c ---[1084]---> BDD-cost:   12
c ---[1083]---> BDD-cost:   12
c ---[1082]---> BDD-cost:   12
c ---[1076]---> BDD-cost:    9
c ---[1073]---> BDD-cost:   12
c ---[1072]---> BDD-cost:    9
c ---[1069]---> BDD-cost:   12
c ---[1068]---> BDD-cost:    9
c ---[1063]---> BDD-cost:   12
c ---[1062]---> BDD-cost:    9
c ---[1061]---> BDD-cost:    9
c ---[1060]---> BDD-cost:   12
c ---[1056]---> BDD-cost:    9
c ---[1047]---> BDD-cost:   12
c ---[1046]---> BDD-cost:    9
c ---[1041]---> BDD-cost:    9
c ---[1039]---> BDD-cost:    9
c ---[1035]---> BDD-cost:    9
c ---[1034]---> BDD-cost:    9
c ---[1033]---> BDD-cost:   12
c ---[1032]---> BDD-cost:   12
c ---[1031]---> BDD-cost:    9
c ---[1030]---> BDD-cost:    9
c ---[1026]---> BDD-cost:   12
c ---[1025]---> BDD-cost:   12
c ---[1023]---> BDD-cost:   12
c ---[1022]---> BDD-cost:    9
c ---[1017]---> BDD-cost:   12
c ---[1016]---> BDD-cost:   12
c ---[1015]---> BDD-cost:   12
c ---[1011]---> BDD-cost:   12
c ---[1007]---> BDD-cost:   12
c ---[1006]---> BDD-cost:    9
c ---[1005]---> BDD-cost:    9
c ---[1004]---> BDD-cost:   12
c ---[1003]---> BDD-cost:    9
c ---[1002]---> BDD-cost:    9
c ---[1001]---> BDD-cost:   12
c ---[1000]---> BDD-cost:   12
c ---[ 999]---> BDD-cost:   12
c ---[ 998]---> BDD-cost:    9
c ---[ 997]---> BDD-cost:   12
c ---[ 996]---> BDD-cost:    9
c ---[ 995]---> BDD-cost:    9
c ---[ 994]---> BDD-cost:   12
c ---[ 993]---> BDD-cost:   12
c ---[ 992]---> BDD-cost:    9
c ---[ 990]---> BDD-cost:    9
c ---[ 987]---> BDD-cost:    9
c ---[ 986]---> BDD-cost:   12
c ---[ 985]---> BDD-cost:   12
c ---[ 982]---> BDD-cost:   12
c ---[ 981]---> BDD-cost:    9
c ---[ 980]---> BDD-cost:    9
c ---[ 971]---> BDD-cost:    9
c ---[ 970]---> BDD-cost:   12
c ---[ 969]---> BDD-cost:   12
c ---[ 966]---> BDD-cost:    9
c ---[ 965]---> BDD-cost:   12
c ---[ 962]---> BDD-cost:    9
c ---[ 956]---> BDD-cost:    9
c ---[ 951]---> BDD-cost:    9
c ---[ 946]---> BDD-cost:    9
c ---[ 944]---> BDD-cost:    9
c ---[ 941]---> BDD-cost:    9
c ---[ 934]---> BDD-cost:    9
c ---[ 931]---> BDD-cost:    9
c ---[ 926]---> BDD-cost:    9
c ---[ 925]---> BDD-cost:   12
c ---[ 924]---> BDD-cost:   12
c ---[ 923]---> BDD-cost:    9
c ---[ 922]---> BDD-cost:   12
c ---[ 920]---> BDD-cost:    9
c ---[ 916]---> BDD-cost:   12
c ---[ 915]---> BDD-cost:   12
c ---[ 912]---> BDD-cost:   12
c ---[ 907]---> BDD-cost:    9
c ---[ 906]---> BDD-cost:    9
c ---[ 904]---> BDD-cost:    9
c ---[ 903]---> BDD-cost:   12
c ---[ 902]---> BDD-cost:    9
c ---[ 900]---> BDD-cost:   12
c ---[ 898]---> BDD-cost:   12
c ---[ 897]---> BDD-cost:   12
c ---[ 882]---> BDD-cost:    2
c ---[ 876]---> BDD-cost:    2
c ---[ 873]---> BDD-cost:    2
c ---[ 871]---> BDD-cost:    2
c ---[ 867]---> BDD-cost:    2
c ---[ 863]---> BDD-cost:    2
c ---[ 862]---> BDD-cost:    2
c ---[ 861]---> BDD-cost:    2
c ---[ 860]---> BDD-cost:    2
c ---[ 858]---> BDD-cost:    2
c ---[ 845]---> BDD-cost:    2
c ---[ 842]---> BDD-cost:    2
c ---[ 832]---> BDD-cost:    2
c ---[ 831]---> BDD-cost:    2
c ---[ 823]---> BDD-cost:    2
c ---[ 822]---> BDD-cost:    2
c ---[ 820]---> BDD-cost:    2
c ---[ 818]---> BDD-cost:    2
c ---[ 817]---> BDD-cost:    2
c ---[ 816]---> BDD-cost:    2
c ---[ 815]---> BDD-cost:    2
c ---[ 814]---> BDD-cost:    2
c ---[ 813]---> BDD-cost:    2
c ---[ 812]---> BDD-cost:    2
c ---[ 808]---> BDD-cost:    2
c ---[ 801]---> BDD-cost:    2
c ---[ 800]---> BDD-cost:    2
c ---[ 799]---> BDD-cost:    2
c ---[ 798]---> BDD-cost:    2
c ---[ 796]---> BDD-cost:    2
c ---[ 785]---> BDD-cost:   46
c ---[ 783]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 781]---> Sorter-cost: 1092     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 779]---> Sorter-cost: 1248     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 777]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 775]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 773]---> Sorter-cost:  413     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 771]---> Sorter-cost: 1248     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 769]---> Sorter-cost: 1247     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 767]---> Sorter-cost: 1193     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 765]---> Sorter-cost: 1215     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 763]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 761]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 759]---> Sorter-cost: 1462     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 757]---> Sorter-cost:  621     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 755]---> Sorter-cost: 1747     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 753]---> Sorter-cost: 1727     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 751]---> Sorter-cost: 1727     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 749]---> Sorter-cost:  406     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 747]---> Sorter-cost:  406     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 745]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 743]---> BDD-cost:   70
c ---[ 741]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 739]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 737]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 735]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 733]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 731]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 729]---> BDD-cost:   73
c ---[ 727]---> BDD-cost:   54
c ---[ 725]---> BDD-cost:   60
c ---[ 723]---> BDD-cost:   59
c ---[ 721]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 719]---> BDD-cost:   73
c ---[ 717]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 715]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 713]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 711]---> BDD-cost:   54
c ---[ 709]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 707]---> Sorter-cost:  621     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 705]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 703]---> BDD-cost:   60
c ---[ 701]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 699]---> BDD-cost:   99
c ---[ 697]---> Sorter-cost: 1021     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 695]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 693]---> Sorter-cost:  627     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 691]---> BDD-cost:   54
c ---[ 689]---> Sorter-cost: 1067     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 687]---> BDD-cost:   73
c ---[ 685]---> Sorter-cost: 1297     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 683]---> BDD-cost:  107
c ---[ 681]---> Sorter-cost:  815     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 679]---> Sorter-cost: 1247     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 677]---> Sorter-cost: 1073     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 675]---> Sorter-cost:  789     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 673]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 671]---> Sorter-cost:  709     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 669]---> Sorter-cost: 1066     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 667]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 665]---> Sorter-cost:  830     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 663]---> Sorter-cost:  830     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 661]---> Sorter-cost:  796     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 659]---> Sorter-cost: 1256     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 657]---> Sorter-cost:  816     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 655]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 653]---> Sorter-cost:  575     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 651]---> Sorter-cost:  849     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 649]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 647]---> Sorter-cost:  491     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 645]---> Sorter-cost:  506     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 643]---> Sorter-cost:  795     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 641]---> Sorter-cost: 1003     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 639]---> Sorter-cost: 1256     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 637]---> Sorter-cost:  406     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 635]---> Sorter-cost: 1222     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 633]---> Sorter-cost: 1248     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 631]---> BDD-cost:  101
c ---[ 629]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 627]---> Sorter-cost: 1218     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 625]---> Sorter-cost: 1066     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 623]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 621]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 619]---> Sorter-cost:  407     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 617]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 615]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 613]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 611]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 609]---> Sorter-cost:  312     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 607]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 605]---> BDD-cost:  107
c ---[ 603]---> BDD-cost:   60
c ---[ 601]---> Sorter-cost:  333     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 599]---> Sorter-cost:  823     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 597]---> Sorter-cost:  829     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 595]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 593]---> Sorter-cost:  387     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 591]---> Sorter-cost:  823     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 589]---> Sorter-cost:  823     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 587]---> BDD-cost:  104
c ---[ 585]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 583]---> BDD-cost:  104
c ---[ 581]---> BDD-cost:  107
c ---[ 579]---> Sorter-cost: 2177     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 577]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 575]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 573]---> Sorter-cost: 2260     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 571]---> Sorter-cost: 1014     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 569]---> Sorter-cost:  969     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 567]---> Sorter-cost:  406     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 565]---> Sorter-cost:  989     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 563]---> Sorter-cost:  491     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 561]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 559]---> BDD-cost:  129
c ---[ 557]---> Sorter-cost: 1471     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 555]---> Sorter-cost: 1417     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 553]---> Sorter-cost: 1449     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 551]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 549]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 547]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 545]---> Sorter-cost:  993     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 543]---> Sorter-cost:  984     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 541]---> Sorter-cost:  881     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 539]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 537]---> Sorter-cost:  855     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 535]---> Sorter-cost: 1503     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 533]---> Sorter-cost:  906     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 531]---> Sorter-cost:  990     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 529]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 527]---> BDD-cost:  123
c ---[ 525]---> Sorter-cost: 1066     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 523]---> BDD-cost:   99
c ---[ 521]---> Sorter-cost: 1066     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 519]---> BDD-cost:   60
c ---[ 517]---> Sorter-cost:  491     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 515]---> Sorter-cost:  333     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 513]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 511]---> BDD-cost:  107
c ---[ 509]---> Sorter-cost: 1278     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 507]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 505]---> Sorter-cost:  387     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 503]---> Sorter-cost: 1278     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 501]---> Sorter-cost:  413     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 499]---> Sorter-cost: 1274     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 497]---> Sorter-cost:  413     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 495]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 493]---> Sorter-cost:  993     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 491]---> BDD-cost:   99
c ---[ 489]---> Sorter-cost:  331     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 487]---> Sorter-cost:  413     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 485]---> Sorter-cost:  849     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 483]---> Sorter-cost:  829     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 481]---> Sorter-cost:  407     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 479]---> Sorter-cost: 1067     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 477]---> Sorter-cost: 1282     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 475]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 473]---> Sorter-cost:  581     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 471]---> BDD-cost:   60
c ---[ 469]---> Sorter-cost:  824     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 467]---> BDD-cost:   60
c ---[ 465]---> BDD-cost:   60
c ---[ 463]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 461]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 459]---> Sorter-cost:  491     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 457]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 455]---> BDD-cost:  126
c ---[ 453]---> Sorter-cost: 1092     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 451]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 449]---> BDD-cost:  109
c ---[ 447]---> Sorter-cost: 1072     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 445]---> Sorter-cost:  734     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 443]---> Sorter-cost:  333     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 441]---> Sorter-cost: 1023     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 439]---> BDD-cost:  127
c ---[ 437]---> Sorter-cost:  527     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 435]---> Sorter-cost: 1302     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 433]---> Sorter-cost: 1423     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 431]---> Sorter-cost: 1072     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 429]---> Sorter-cost:  527     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 427]---> Sorter-cost:  986     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 425]---> Sorter-cost: 1423     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 423]---> Sorter-cost: 1417     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 421]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 419]---> Sorter-cost: 1204     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 417]---> Sorter-cost:  581     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 415]---> Sorter-cost: 1205     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 413]---> Sorter-cost:  581     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 411]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 409]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 407]---> Sorter-cost:  850     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 405]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 403]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 401]---> Sorter-cost:  816     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 399]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 397]---> Sorter-cost:  312     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 395]---> Sorter-cost:  796     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 393]---> Sorter-cost:  312     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 391]---> Sorter-cost:  387     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 389]---> Sorter-cost:  816     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 387]---> Sorter-cost:  413     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 385]---> Sorter-cost: 1072     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 383]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 381]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 379]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 377]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 375]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 373]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 371]---> Sorter-cost:  823     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 369]---> Sorter-cost:  790     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 367]---> Sorter-cost:  333     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 365]---> Sorter-cost: 1023     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 363]---> Sorter-cost:  810     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 361]---> Sorter-cost: 1241     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 359]---> Sorter-cost: 1234     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 357]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 355]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 353]---> Sorter-cost:  312     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 351]---> Sorter-cost:  796     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 349]---> Sorter-cost:  413     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 347]---> BDD-cost:  129
c ---[ 345]---> Sorter-cost:  413     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 343]---> Sorter-cost:  413     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 341]---> Sorter-cost:  561     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 339]---> Sorter-cost:  830     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 337]---> Sorter-cost:  387     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 335]---> Sorter-cost:  830     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 333]---> Sorter-cost:  561     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 331]---> Sorter-cost:  830     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 329]---> Sorter-cost:  775     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 327]---> Sorter-cost:  332     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 325]---> Sorter-cost:  816     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 323]---> Sorter-cost:  546     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 321]---> BDD-cost:  117
c ---[ 319]---> Sorter-cost:  849     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 317]---> Sorter-cost:  993     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 315]---> BDD-cost:  114
c ---[ 313]---> Sorter-cost:  581     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 311]---> BDD-cost:  123
c ---[ 309]---> BDD-cost:   60
c ---[ 307]---> Sorter-cost: 1202     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 305]---> BDD-cost:   99
c ---[ 303]---> BDD-cost:   73
c ---[ 301]---> BDD-cost:   54
c ---[ 299]---> BDD-cost:   60
c ---[ 297]---> BDD-cost:   60
c ---[ 295]---> BDD-cost:   62
c ---[ 293]---> BDD-cost:   73
c ---[ 291]---> BDD-cost:   60
c ---[ 289]---> BDD-cost:   60
c ---[ 287]---> BDD-cost:   60
c ---[ 285]---> BDD-cost:   70
c ---[ 283]---> BDD-cost:   62
c ---[ 281]---> BDD-cost:   62
c ---[ 279]---> BDD-cost:   62
c ---[ 277]---> BDD-cost:   52
c ---[ 275]---> BDD-cost:   52
c ---[ 273]---> BDD-cost:   98
c ---[ 271]---> BDD-cost:  112
c ---[ 269]---> BDD-cost:  123
c ---[ 267]---> BDD-cost:  123
c ---[ 265]---> BDD-cost:  106
c ---[ 263]---> Sorter-cost:  824     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 261]---> BDD-cost:  106
c ---[ 259]---> Sorter-cost:  491     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 257]---> Sorter-cost:  471     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[ 255]---> BDD-cost:  110
c ---[ 253]---> BDD-cost:  123
c ---[ 251]---> Sorter-cost:  555     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 249]---> Sorter-cost:  555     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 247]---> Sorter-cost:  555     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 245]---> Sorter-cost:  555     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 243]---> BDD-cost:  112
c ---[ 241]---> Sorter-cost:  770     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 239]---> BDD-cost:  112
c ---[ 237]---> BDD-cost:  114
c ---[ 235]---> BDD-cost:   98
c ---[ 233]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 231]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 229]---> Sorter-cost: 1228     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 227]---> Sorter-cost: 1066     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 225]---> Sorter-cost:  413     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 223]---> Sorter-cost:  413     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 221]---> Sorter-cost: 1339     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 219]---> Sorter-cost:  581     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 217]---> Sorter-cost: 1222     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 215]---> Sorter-cost:  602     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 213]---> Sorter-cost:  849     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 211]---> Sorter-cost: 1222     Base: 2 2 2 2 2 2 2 2 2 2 2 7
c ---[ 209]---> Sorter-cost:  628     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 207]---> Sorter-cost:  413     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 205]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 203]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 201]---> Sorter-cost:  312     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 199]---> BDD-cost:  129
c ---[ 198]---> BDD-cost:   10
c ---[ 197]---> BDD-cost:   10
c ---[ 196]---> BDD-cost:   10
c ---[ 195]---> BDD-cost:   10
c ---[ 194]---> BDD-cost:   10
c ---[ 193]---> BDD-cost:   10
c ---[ 192]---> BDD-cost:   10
c ---[ 191]---> BDD-cost:   10
c ---[ 190]---> BDD-cost:   10
c ---[ 189]---> BDD-cost:   10
c ---[ 188]---> BDD-cost:   10
c ---[ 187]---> BDD-cost:   10
c ---[ 186]---> BDD-cost:   10
c ---[ 185]---> BDD-cost:   10
c ---[ 184]---> BDD-cost:   10
c ---[ 183]---> BDD-cost:   10
c ---[ 182]---> BDD-cost:   10
c ---[ 181]---> BDD-cost:   10
c ---[ 180]---> BDD-cost:   10
c ---[ 179]---> BDD-cost:   10
c ---[ 178]---> BDD-cost:   10
c ---[ 177]---> BDD-cost:   10
c ---[ 176]---> BDD-cost:   10
c ---[ 175]---> BDD-cost:   10
c ---[ 174]---> BDD-cost:   10
c ---[ 173]---> BDD-cost:   10
c ---[ 172]---> BDD-cost:   10
c ---[ 171]---> BDD-cost:   10
c ---[ 170]---> BDD-cost:   10
c ---[ 169]---> BDD-cost:   10
c ---[ 168]---> BDD-cost:   10
c ---[ 167]---> BDD-cost:   10
c ---[ 166]---> BDD-cost:   10
c ---[ 165]---> BDD-cost:   10
c ---[ 164]---> BDD-cost:   10
c ---[ 163]---> BDD-cost:   10
c ---[ 162]---> BDD-cost:   10
c ---[ 161]---> BDD-cost:   10
c ---[ 160]---> BDD-cost:   10
c ---[ 159]---> BDD-cost:   10
c ---[ 158]---> BDD-cost:   10
c ---[ 157]---> BDD-cost:   10
c ---[ 156]---> BDD-cost:   10
c ---[ 155]---> BDD-cost:   10
c ---[ 154]---> BDD-cost:   10
c ---[ 153]---> BDD-cost:   10
c ---[ 152]---> BDD-cost:   10
c ---[ 151]---> BDD-cost:   10
c ---[ 150]---> BDD-cost:   10
c ---[ 149]---> BDD-cost:   10
c ---[ 148]---> BDD-cost:   10
c ---[ 147]---> BDD-cost:   10
c ---[ 146]---> BDD-cost:   10
c ---[ 145]---> BDD-cost:   10
c ---[ 144]---> BDD-cost:   10
c ---[ 143]---> BDD-cost:   10
c ---[ 142]---> BDD-cost:   10
c ---[ 141]---> BDD-cost:   10
c ---[ 140]---> BDD-cost:   10
c ---[ 139]---> BDD-cost:   10
c ---[ 138]---> BDD-cost:   10
c ---[ 137]---> BDD-cost:   10
c ---[ 136]---> BDD-cost:   10
c ---[ 135]---> BDD-cost:   10
c ---[ 134]---> BDD-cost:   10
c ---[ 133]---> BDD-cost:   10
c ---[ 132]---> BDD-cost:   10
c ---[ 131]---> BDD-cost:   10
c ---[ 130]---> BDD-cost:   10
c ---[ 129]---> BDD-cost:   10
c ---[ 128]---> BDD-cost:   10
c ---[ 127]---> BDD-cost:   10
c ---[ 126]---> BDD-cost:   10
c ---[ 125]---> BDD-cost:   10
c ---[ 124]---> BDD-cost:   10
c ---[ 123]---> BDD-cost:   10
c ---[ 122]---> BDD-cost:   10
c ---[ 121]---> BDD-cost:   10
c ---[ 120]---> BDD-cost:   10
c ---[ 119]---> BDD-cost:   10
c ---[ 118]---> BDD-cost:   10
c ---[ 117]---> BDD-cost:   10
c ---[ 116]---> BDD-cost:   10
c ---[ 115]---> BDD-cost:   10
c ---[ 114]---> BDD-cost:   10
c ---[ 113]---> BDD-cost:   10
c ---[ 112]---> BDD-cost:   10
c ---[ 111]---> BDD-cost:   10
c ---[ 110]---> BDD-cost:   10
c ---[ 109]---> BDD-cost:   10
c ---[ 108]---> BDD-cost:   10
c ---[ 107]---> BDD-cost:   10
c ---[ 106]---> BDD-cost:   10
c ---[ 105]---> BDD-cost:   10
c ---[ 104]---> BDD-cost:   10
c ---[ 103]---> BDD-cost:   10
c ---[ 102]---> BDD-cost:   10
c ---[ 101]---> BDD-cost:   10
c ---[ 100]---> BDD-cost:   10
c ---[  99]---> BDD-cost:   10
c ---[  98]---> BDD-cost:   10
c ---[  97]---> BDD-cost:   10
c ---[  96]---> BDD-cost:   10
c ---[  95]---> BDD-cost:   10
c ---[  94]---> BDD-cost:   10
c ---[  93]---> BDD-cost:   10
c ---[  92]---> BDD-cost:   10
c ---[  91]---> BDD-cost:   10
c ---[  90]---> BDD-cost:   10
c ---[  89]---> BDD-cost:   10
c ---[  88]---> BDD-cost:   10
c ---[  87]---> BDD-cost:   10
c ---[  86]---> BDD-cost:   10
c ---[  85]---> BDD-cost:   10
c ---[  84]---> BDD-cost:   10
c ---[  83]---> BDD-cost:   10
c ---[  82]---> BDD-cost:   10
c ---[  81]---> BDD-cost:   10
c ---[  80]---> BDD-cost:   10
c ---[  79]---> BDD-cost:   10
c ---[  78]---> BDD-cost:   10
c ---[  77]---> BDD-cost:   10
c ---[  76]---> BDD-cost:   10
c ---[  75]---> BDD-cost:   10
c ---[  74]---> BDD-cost:   10
c ---[  73]---> BDD-cost:   10
c ---[  72]---> BDD-cost:   10
c ---[  71]---> BDD-cost:   10
c ---[  70]---> BDD-cost:   10
c ---[  69]---> BDD-cost:   10
c ---[  68]---> BDD-cost:   10
c ---[  67]---> BDD-cost:   10
c ---[  66]---> BDD-cost:   10
c ---[  65]---> BDD-cost:   10
c ---[  64]---> BDD-cost:   10
c ---[  63]---> BDD-cost:   10
c ---[  62]---> BDD-cost:   10
c ---[  61]---> BDD-cost:   10
c ---[  60]---> BDD-cost:   10
c ---[  59]---> BDD-cost:   10
c ---[  58]---> BDD-cost:   10
c ---[  57]---> BDD-cost:   10
c ---[  56]---> BDD-cost:   10
c ---[  55]---> BDD-cost:   10
c ---[  54]---> BDD-cost:   10
c ---[  53]---> BDD-cost:   10
c ---[  52]---> BDD-cost:   10
c ---[  51]---> BDD-cost:   10
c ---[  50]---> BDD-cost:   10
c ---[  49]---> BDD-cost:   10
c ---[  48]---> BDD-cost:   10
c ---[  47]---> BDD-cost:   10
c ---[  46]---> BDD-cost:   10
c ---[  45]---> BDD-cost:   10
c ---[  44]---> BDD-cost:   10
c ---[  43]---> BDD-cost:   10
c ---[  42]---> BDD-cost:   10
c ---[  41]---> BDD-cost:   10
c ---[  40]---> BDD-cost:   10
c ---[  39]---> BDD-cost:   10
c ---[  38]---> BDD-cost:   10
c ---[  37]---> BDD-cost:   10
c ---[  36]---> BDD-cost:   10
c ---[  35]---> BDD-cost:   10
c ---[  34]---> BDD-cost:   10
c ---[  33]---> BDD-cost:   10
c ---[  32]---> BDD-cost:   10
c ---[  31]---> BDD-cost:   10
c ---[  30]---> BDD-cost:   10
c ---[  29]---> BDD-cost:   10
c ---[  28]---> BDD-cost:   10
c ---[  27]---> BDD-cost:   10
c ---[  26]---> BDD-cost:   10
c ---[  25]---> BDD-cost:   10
c ---[  24]---> BDD-cost:   10
c ---[  23]---> BDD-cost:   10
c ---[  22]---> BDD-cost:   10
c ---[  21]---> BDD-cost:   10
c ---[  20]---> BDD-cost:   10
c ---[  19]---> BDD-cost:   10
c ---[  18]---> BDD-cost:   10
c ---[  17]---> BDD-cost:   10
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:   10
c ---[  14]---> BDD-cost:   10
c ---[  13]---> BDD-cost:   10
c ---[  12]---> BDD-cost:   10
c ---[  11]---> BDD-cost:   10
c ---[  10]---> BDD-cost:   10
c ---[   9]---> BDD-cost:   10
c ---[   8]---> BDD-cost:   10
c ---[   7]---> BDD-cost:   10
c ---[   6]---> BDD-cost:   10
c ---[   5]---> BDD-cost:   10
c ---[   4]---> BDD-cost:   10
c ---[   3]---> BDD-cost:   10
c ---[   2]---> BDD-cost:   10
c ---[   1]---> BDD-cost:   10
c ---[   0]---> BDD-cost:   10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  425420  1010283 |  141806       0        0     nan |  0.000 % |
c |       101 |  425219  1009837 |  155986      82      329     4.0 |  6.694 % |
c |       251 |  425121  1009619 |  171585     225      876     3.9 |  6.711 % |
c |       478 |  424969  1009282 |  188743     433     2120     4.9 |  6.740 % |
c |       815 |  424770  1008841 |  207618     740     4248     5.7 |  6.777 % |
c |      1321 |  424431  1008088 |  228379    1212     7017     5.8 |  6.838 % |
c |      2080 |  424365  1007944 |  251217    1962    12720     6.5 |  6.851 % |
c |      3219 |  423830  1006755 |  276339    3033    20515     6.8 |  6.952 % |
c |      4927 |  423405  1005809 |  303973    4696    36798     7.8 |  7.030 % |
c |      7489 |  422480  1003744 |  334371    7144    56564     7.9 |  7.197 % |
c |     11333 |  421625  1001843 |  367808   10867    98552     9.1 |  7.358 % |
c |     17099 |  420905  1000240 |  404589   16540   171778    10.4 |  7.491 % |
c |     25748 |  419519   997152 |  445047   25021   279099    11.2 |  7.746 % |
c |     38722 |  417048   991628 |  489552   37706   437110    11.6 |  8.196 % |
c |     58185 |  414778   986558 |  538508   56879   705102    12.4 |  8.608 % |
c |     87379 |  411739   979784 |  592358   85642  1159509    13.5 |  9.168 % |
c |    131169 |  408363   972243 |  651594  129018  2062749    16.0 |  9.788 % |
c |    196854 |  405264   965318 |  716754  194289  3549626    18.3 | 10.350 % |
/oldhome/oroussel/solvers/minisat+_script: line 16: 27814 CPU time limit exceeded $XDIR/minisat+_bignum_static* "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.95 0.95 2/54 27809
Raw data (stat): 27809 (runsolver) R 27808 10795 10794 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 842591102 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.93 0.95 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+20.0092 s]
Raw data (loadavg): 0.94 0.96 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+30.0171 s]
Raw data (loadavg): 0.95 0.96 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+40.0176 s]
Raw data (loadavg): 0.95 0.96 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+50.0188 s]
Raw data (loadavg): 0.96 0.96 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+60.0184 s]
Raw data (loadavg): 0.97 0.96 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+70.0189 s]
Raw data (loadavg): 0.97 0.96 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+80.019 s]
Raw data (loadavg): 0.98 0.96 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+90.0198 s]
Raw data (loadavg): 0.98 0.96 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+100.019 s]
Raw data (loadavg): 0.98 0.96 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+110.019 s]
Raw data (loadavg): 0.98 0.96 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+120.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+130.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+140.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+150.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+160.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+170.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+180.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+190.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+200.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+210.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+220.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+230.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+240.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+250.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+260.024 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+270.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+280.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+290.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+300.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+310.025 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+320.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+330.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+340.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+350.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+360.026 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+370.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+380.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+390.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+400.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+410.027 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+420.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+430.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+440.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+450.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+460.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+470.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+480.028 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+490.029 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+500.029 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+510.029 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+520.029 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+530.029 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+540.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+550.029 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+560.029 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+570.031 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+580.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+590.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+600.031 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+610.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+620.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+630.03 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+640.031 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+650.031 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+660.031 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+670.031 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+680.031 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+690.032 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+700.033 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+710.033 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+720.034 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27814
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+730.033 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27867
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+740.034 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27867
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+750.034 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27867
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+760.033 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27867
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+770.033 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27867
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+780.034 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27867
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+790.035 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27867
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+800.035 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27869
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+810.035 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 27869
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+820.035 s]
Raw data (loadavg): 1.07 0.99 0.95 2/55 27869
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+830.035 s]
Raw data (loadavg): 1.06 0.99 0.95 2/55 27869
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+840.036 s]
Raw data (loadavg): 1.05 0.99 0.95 2/55 27869
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+850.037 s]
Raw data (loadavg): 1.04 0.99 0.95 2/55 27869
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+860.037 s]
Raw data (loadavg): 1.03 0.99 0.95 2/55 27869
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+870.038 s]
Raw data (loadavg): 1.03 0.99 0.95 2/55 27869
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+880.038 s]
Raw data (loadavg): 1.02 0.99 0.95 2/55 27869
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+890.038 s]
Raw data (loadavg): 1.02 0.99 0.95 2/55 27869
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+900.038 s]
Raw data (loadavg): 1.02 0.99 0.95 2/55 27869
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+910.037 s]
Raw data (loadavg): 1.01 0.99 0.95 2/55 27869
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+920.038 s]
Raw data (loadavg): 1.01 0.99 0.95 2/55 27869
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+930.039 s]
Raw data (loadavg): 1.01 0.99 0.95 2/55 27869
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+940.039 s]
Raw data (loadavg): 1.01 0.99 0.95 2/55 27869
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+950.039 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 27869
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+960.039 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 27869
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+970.039 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 27869
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+980.039 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 27869
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+990.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 27869
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 27869
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 27869
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 27869
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 27869
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 27869
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 27871
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 27871
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 27871
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 27871
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 27871
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 27871
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 27871
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 27871
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 27871
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 27871
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 27871
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 27871
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 27871
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 27871
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 27871
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 27871
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1210.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 27871
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1220.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 27871
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 2128
[startup+1229.77 s]
Raw data (loadavg): 1.00 0.99 0.95 1/53 27871
Raw data (stat): 27809 (minisat+_script) S 27808 10795 10794 0 -1 0 300 332 0 0 0 0 0 0 20 0 1 0 842591102 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 532 234 485 147 0 385 0
vsize: 0

Child status: 152
Real time (s): 1229.77
CPU time (s): 1229.88
CPU user time (s): 1229.13
CPU system time (s): 0.743886
CPU usage (%): 100.009
Max. virtual memory (Kb): 2128
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####