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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. 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.
  4. 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

Namemps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-neos6.opb
MD5SUM0633214154e8bab02f648560b9bfa54f
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 4460
Biggest coefficient in the objective function 524288
Number of bits for the biggest coefficient in the objective function 20
Sum of the numbers in the objective function 233832225
Number of bits of the sum of numbers in the objective function 28
Biggest number in a constraint 524288
Number of bits of the biggest number in a constraint 20
Biggest sum of numbers in a constraint 233832225
Number of bits of the biggest sum of numbers28
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables17260
Total number of constraints9376
Number of constraints which are clauses48
Number of constraints which are cardinality constraints (but not clauses)9095
Number of constraints which are nor clauses,nor cardinality constraints233
Minimum length of a constraint1
Maximum length of a constraint834

Trace number 6312

Launcher Data

LAUNCH ON wulflinc15 THE 2005-09-20 05:26:31 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3473 boxname=wulflinc15 idbench=1129 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  0633214154e8bab02f648560b9bfa54f  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-neos6.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-neos6.opb
IDLAUNCH: 3473
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 2
cpu MHz		: 450.999
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:        888736 kB
Buffers:         11960 kB
Cached:         104256 kB
SwapCached:        744 kB
Active:          37988 kB
Inactive:        80912 kB
HighTotal:      131008 kB
HighFree:        24948 kB
LowTotal:       903652 kB
LowFree:        863788 kB
SwapTotal:     2097136 kB
SwapFree:      2095884 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5720 kB
Slab:            21300 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 05:46:42 (client local time) WITH STATUS 0 IN 1207.02 SECONDS
stats: 3473 7 1207.02 0

Solver Data

c Parsing PB file...
c Converting 1259 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###############################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ................................................
c ---[1258]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1257]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1256]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1255]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1254]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1253]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1252]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1251]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1250]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1249]---> Adder-cost: 2812   maxlim: 5135   bits: 13/13
c ---[1248]---> BDD-cost:  173
c ---[1247]---> BDD-cost:  353
c ---[1246]---> BDD-cost:  533
c ---[1245]---> BDD-cost:  678
c ---[1244]---> BDD-cost:  893
c ---[1243]---> BDD-cost:  984
c ---[1242]---> BDD-cost: 1182
c ---[1241]---> Adder-cost: 899   maxlim: 5   bits: 4/3
c ---[1240]---> Adder-cost: 879   maxlim: 5   bits: 4/3
c ---[1239]---> Adder-cost: 937   maxlim: 5   bits: 4/3
c ---[1238]---> BDD-cost: 2467
c ---[1237]---> BDD-cost: 2502
c ---[1236]---> BDD-cost: 2722
c ---[1235]---> BDD-cost: 2778
c ---[1234]---> BDD-cost: 2922
c ---[1233]---> Adder-cost: 1354   maxlim: 5   bits: 4/3
c ---[1232]---> Adder-cost: 1267   maxlim: 5   bits: 4/3
c ---[1231]---> Adder-cost: 1200   maxlim: 5   bits: 4/3
c ---[1230]---> Adder-cost: 1201   maxlim: 5   bits: 4/3
c ---[1229]---> BDD-cost: 2262
c ---[1228]---> BDD-cost: 2213
c ---[1227]---> BDD-cost: 2115
c ---[1226]---> BDD-cost: 2063
c ---[1225]---> BDD-cost: 1917
c ---[1224]---> BDD-cost: 1853
c ---[1223]---> BDD-cost: 1680
c ---[1222]---> BDD-cost: 1572
c ---[1221]---> BDD-cost: 1395
c ---[1220]---> BDD-cost: 1242
c ---[1219]---> BDD-cost: 1044
c ---[1218]---> BDD-cost:  891
c ---[1217]---> BDD-cost:  699
c ---[1216]---> BDD-cost:  533
c ---[1215]---> BDD-cost:  233
c ---[1214]---> BDD-cost:  117
c ---[1213]---> BDD-cost:  173
c ---[1212]---> BDD-cost:  353
c ---[1211]---> BDD-cost:  533
c ---[1210]---> BDD-cost:  663
c ---[1209]---> BDD-cost:  893
c ---[1208]---> BDD-cost: 1005
c ---[1207]---> BDD-cost: 1253
c ---[1206]---> BDD-cost: 1854
c ---[1205]---> BDD-cost: 1994
c ---[1204]---> BDD-cost: 2242
c ---[1203]---> BDD-cost: 2426
c ---[1202]---> BDD-cost: 2494
c ---[1201]---> BDD-cost: 2730
c ---[1200]---> BDD-cost: 2064
c ---[1199]---> BDD-cost: 2208
c ---[1198]---> Adder-cost: 1424   maxlim: 5   bits: 4/3
c ---[1197]---> Adder-cost: 1267   maxlim: 5   bits: 4/3
c ---[1196]---> Adder-cost: 1230   maxlim: 5   bits: 4/3
c ---[1195]---> Adder-cost: 1161   maxlim: 5   bits: 4/3
c ---[1194]---> BDD-cost: 2273
c ---[1193]---> BDD-cost: 2202
c ---[1192]---> BDD-cost: 2103
c ---[1191]---> BDD-cost: 2052
c ---[1190]---> BDD-cost: 1920
c ---[1189]---> BDD-cost: 1842
c ---[1188]---> BDD-cost: 1722
c ---[1187]---> BDD-cost: 1578
c ---[1186]---> BDD-cost: 1407
c ---[1185]---> BDD-cost: 1248
c ---[1184]---> BDD-cost: 1053
c ---[1183]---> BDD-cost:  893
c ---[1182]---> BDD-cost:  705
c ---[1181]---> BDD-cost:  533
c ---[1180]---> BDD-cost:  237
c ---[1179]---> BDD-cost:  117
c ---[1178]---> BDD-cost:  173
c ---[1177]---> BDD-cost:  353
c ---[1176]---> BDD-cost:  533
c ---[1175]---> BDD-cost:  713
c ---[1174]---> BDD-cost:  879
c ---[1173]---> BDD-cost: 1073
c ---[1172]---> BDD-cost: 1149
c ---[1171]---> BDD-cost: 1821
c ---[1170]---> BDD-cost: 1515
c ---[1169]---> BDD-cost: 1647
c ---[1168]---> BDD-cost: 1821
c ---[1167]---> BDD-cost: 1973
c ---[1166]---> Adder-cost: 1291   maxlim: 5   bits: 4/3
c ---[1165]---> Adder-cost: 1201   maxlim: 5   bits: 4/3
c ---[1164]---> Adder-cost: 1163   maxlim: 5   bits: 4/3
c ---[1163]---> Adder-cost: 1208   maxlim: 5   bits: 4/3
c ---[1162]---> Adder-cost: 1153   maxlim: 5   bits: 4/3
c ---[1161]---> Adder-cost: 1148   maxlim: 5   bits: 4/3
c ---[1160]---> Adder-cost: 1157   maxlim: 5   bits: 4/3
c ---[1159]---> Adder-cost: 1136   maxlim: 5   bits: 4/3
c ---[1158]---> Adder-cost: 1095   maxlim: 4   bits: 4/3
c ---[1157]---> BDD-cost: 2153
c ---[1156]---> BDD-cost: 2019
c ---[1155]---> BDD-cost: 1973
c ---[1154]---> BDD-cost: 1800
c ---[1153]---> BDD-cost: 1731
c ---[1152]---> BDD-cost: 1557
c ---[1151]---> BDD-cost: 1428
c ---[1150]---> BDD-cost: 1221
c ---[1149]---> BDD-cost: 1068
c ---[1148]---> BDD-cost:  876
c ---[1147]---> BDD-cost:  713
c ---[1146]---> BDD-cost:  522
c ---[1145]---> BDD-cost:  237
c ---[1144]---> BDD-cost:  115
c ---[1143]---> BDD-cost:  173
c ---[1142]---> BDD-cost:  353
c ---[1141]---> BDD-cost:  492
c ---[1140]---> BDD-cost:  690
c ---[1139]---> BDD-cost:  834
c ---[1138]---> BDD-cost: 1050
c ---[1137]---> BDD-cost: 1230
c ---[1136]---> BDD-cost: 1902
c ---[1135]---> BDD-cost: 2078
c ---[1134]---> BDD-cost: 2166
c ---[1133]---> BDD-cost: 2438
c ---[1132]---> BDD-cost: 2558
c ---[1131]---> BDD-cost: 2718
c ---[1130]---> BDD-cost: 2061
c ---[1129]---> BDD-cost: 2190
c ---[1128]---> BDD-cost: 2273
c ---[1127]---> BDD-cost: 2250
c ---[1126]---> BDD-cost: 2333
c ---[1125]---> BDD-cost: 2256
c ---[1124]---> BDD-cost: 2273
c ---[1123]---> BDD-cost: 2208
c ---[1122]---> BDD-cost: 2153
c ---[1121]---> BDD-cost: 2043
c ---[1120]---> BDD-cost: 1973
c ---[1119]---> BDD-cost: 1836
c ---[1118]---> BDD-cost: 1733
c ---[1117]---> BDD-cost: 1583
c ---[1116]---> BDD-cost: 1386
c ---[1115]---> BDD-cost: 1245
c ---[1114]---> BDD-cost: 1038
c ---[1113]---> BDD-cost:  893
c ---[1112]---> BDD-cost:  699
c ---[1111]---> BDD-cost:  533
c ---[1110]---> BDD-cost:  233
c ---[1109]---> BDD-cost:  117
c ---[1108]---> BDD-cost:  173
c ---[1107]---> BDD-cost:  353
c ---[1106]---> BDD-cost:  533
c ---[1105]---> BDD-cost:  663
c ---[1104]---> BDD-cost:  893
c ---[1103]---> BDD-cost: 1005
c ---[1102]---> BDD-cost: 1185
c ---[1101]---> BDD-cost: 1857
c ---[1100]---> BDD-cost: 2107
c ---[1099]---> BDD-cost: 2242
c ---[1098]---> BDD-cost: 2467
c ---[1097]---> BDD-cost: 2518
c ---[1096]---> BDD-cost: 2698
c ---[1095]---> BDD-cost: 2076
c ---[1094]---> BDD-cost: 2175
c ---[1093]---> Adder-cost: 1424   maxlim: 5   bits: 4/3
c ---[1092]---> Adder-cost: 1299   maxlim: 5   bits: 4/3
c ---[1091]---> Adder-cost: 1204   maxlim: 5   bits: 4/3
c ---[1090]---> Adder-cost: 1165   maxlim: 5   bits: 4/3
c ---[1089]---> BDD-cost: 2262
c ---[1088]---> BDD-cost: 2213
c ---[1087]---> BDD-cost: 2133
c ---[1086]---> BDD-cost: 2063
c ---[1085]---> BDD-cost: 1941
c ---[1084]---> BDD-cost: 1848
c ---[1083]---> BDD-cost: 1728
c ---[1082]---> BDD-cost: 1572
c ---[1081]---> BDD-cost: 1407
c ---[1080]---> BDD-cost: 1242
c ---[1079]---> BDD-cost: 1053
c ---[1078]---> BDD-cost:  893
c ---[1077]---> BDD-cost:  705
c ---[1076]---> BDD-cost:  533
c ---[1075]---> BDD-cost:  237
c ---[1074]---> BDD-cost:  117
c ---[1024]---> Adder-cost: 156   maxlim: 1055615   bits: 22/21
c ---[1022]---> Adder-cost: 274   maxlim: 1063295   bits: 22/21
c ---[1020]---> Adder-cost: 334   maxlim: 1070975   bits: 22/21
c ---[1018]---> Adder-cost: 398   maxlim: 1078655   bits: 22/21
c ---[1016]---> Adder-cost: 462   maxlim: 1086335   bits: 22/21
c ---[1014]---> Adder-cost: 510   maxlim: 1093887   bits: 22/21
c ---[1012]---> Adder-cost: 548   maxlim: 1101567   bits: 22/21
c ---[1010]---> Adder-cost: 616   maxlim: 1109247   bits: 22/21
c ---[1008]---> Adder-cost: 758   maxlim: 1115647   bits: 22/21
c ---[1006]---> Adder-cost: 818   maxlim: 1122047   bits: 22/21
c ---[1004]---> Adder-cost: 874   maxlim: 1127423   bits: 22/21
c ---[1002]---> Adder-cost: 964   maxlim: 1132543   bits: 22/21
c ---[1000]---> Adder-cost: 1024   maxlim: 1136383   bits: 22/21
c ---[ 998]---> Adder-cost: 1096   maxlim: 1140223   bits: 22/21
c ---[ 996]---> Adder-cost: 1070   maxlim: 1142783   bits: 22/21
c ---[ 994]---> Adder-cost: 1140   maxlim: 1145087   bits: 22/21
c ---[ 992]---> Adder-cost: 1110   maxlim: 1146367   bits: 22/21
c ---[ 990]---> Adder-cost: 1136   maxlim: 1147647   bits: 22/21
c ---[ 988]---> Adder-cost: 1212   maxlim: 1146367   bits: 22/21
c ---[ 986]---> Adder-cost: 1128   maxlim: 1145471   bits: 22/21
c ---[ 984]---> Adder-cost: 1208   maxlim: 1142911   bits: 22/21
c ---[ 982]---> Adder-cost: 1196   maxlim: 1140351   bits: 22/21
c ---[ 980]---> Adder-cost: 1144   maxlim: 1136511   bits: 22/21
c ---[ 978]---> Adder-cost: 1110   maxlim: 1132415   bits: 22/21
c ---[ 976]---> Adder-cost: 1060   maxlim: 1127295   bits: 22/21
c ---[ 974]---> Adder-cost: 976   maxlim: 1122175   bits: 22/21
c ---[ 972]---> Adder-cost: 952   maxlim: 1116031   bits: 22/21
c ---[ 970]---> Adder-cost: 848   maxlim: 1109631   bits: 22/21
c ---[ 968]---> Adder-cost: 756   maxlim: 1101951   bits: 22/21
c ---[ 966]---> Adder-cost: 636   maxlim: 1094271   bits: 22/21
c ---[ 964]---> Adder-cost: 570   maxlim: 1086591   bits: 22/21
c ---[ 962]---> Adder-cost: 486   maxlim: 1078527   bits: 22/21
c ---[ 960]---> Adder-cost: 380   maxlim: 1070847   bits: 22/21
c ---[ 958]---> Adder-cost: 284   maxlim: 1063679   bits: 22/21
c ---[ 956]---> Adder-cost: 168   maxlim: 1055999   bits: 22/21
c ---[ 954]---> Adder-cost: 176   maxlim: 1055615   bits: 22/21
c ---[ 952]---> Adder-cost: 274   maxlim: 1063295   bits: 22/21
c ---[ 950]---> Adder-cost: 348   maxlim: 1070975   bits: 22/21
c ---[ 948]---> Adder-cost: 416   maxlim: 1078655   bits: 22/21
c ---[ 946]---> Adder-cost: 488   maxlim: 1086335   bits: 22/21
c ---[ 944]---> Adder-cost: 544   maxlim: 1094143   bits: 22/21
c ---[ 942]---> Adder-cost: 594   maxlim: 1101823   bits: 22/21
c ---[ 940]---> Adder-cost: 648   maxlim: 1109503   bits: 22/21
c ---[ 938]---> Adder-cost: 928   maxlim: 1115903   bits: 22/21
c ---[ 936]---> Adder-cost: 1026   maxlim: 1122303   bits: 22/21
c ---[ 934]---> Adder-cost: 942   maxlim: 1127423   bits: 22/21
c ---[ 932]---> Adder-cost: 984   maxlim: 1132543   bits: 22/21
c ---[ 930]---> Adder-cost: 1080   maxlim: 1136383   bits: 22/21
c ---[ 928]---> Adder-cost: 1104   maxlim: 1140351   bits: 22/21
c ---[ 926]---> Adder-cost: 1096   maxlim: 1142911   bits: 22/21
c ---[ 924]---> Adder-cost: 1100   maxlim: 1145087   bits: 22/21
c ---[ 922]---> Adder-cost: 1150   maxlim: 1146367   bits: 22/21
c ---[ 920]---> Adder-cost: 1174   maxlim: 1147647   bits: 22/21
c ---[ 918]---> Adder-cost: 1164   maxlim: 1146367   bits: 22/21
c ---[ 916]---> Adder-cost: 1184   maxlim: 1145471   bits: 22/21
c ---[ 914]---> Adder-cost: 1186   maxlim: 1142911   bits: 22/21
c ---[ 912]---> Adder-cost: 1202   maxlim: 1140351   bits: 22/21
c ---[ 910]---> Adder-cost: 1160   maxlim: 1136511   bits: 22/21
c ---[ 908]---> Adder-cost: 1110   maxlim: 1132415   bits: 22/21
c ---[ 906]---> Adder-cost: 1054   maxlim: 1127295   bits: 22/21
c ---[ 904]---> Adder-cost: 982   maxlim: 1122175   bits: 22/21
c ---[ 902]---> Adder-cost: 940   maxlim: 1116031   bits: 22/21
c ---[ 900]---> Adder-cost: 848   maxlim: 1109631   bits: 22/21
c ---[ 898]---> Adder-cost: 758   maxlim: 1101951   bits: 22/21
c ---[ 896]---> Adder-cost: 638   maxlim: 1094271   bits: 22/21
c ---[ 894]---> Adder-cost: 586   maxlim: 1086591   bits: 22/21
c ---[ 892]---> Adder-cost: 506   maxlim: 1078527   bits: 22/21
c ---[ 890]---> Adder-cost: 374   maxlim: 1070847   bits: 22/21
c ---[ 888]---> Adder-cost: 284   maxlim: 1063679   bits: 22/21
c ---[ 886]---> Adder-cost: 174   maxlim: 1055999   bits: 22/21
c ---[ 884]---> Adder-cost: 176   maxlim: 1055615   bits: 22/21
c ---[ 882]---> Adder-cost: 274   maxlim: 1063295   bits: 22/21
c ---[ 880]---> Adder-cost: 348   maxlim: 1070975   bits: 22/21
c ---[ 878]---> Adder-cost: 406   maxlim: 1078655   bits: 22/21
c ---[ 876]---> Adder-cost: 478   maxlim: 1086335   bits: 22/21
c ---[ 874]---> Adder-cost: 550   maxlim: 1094015   bits: 22/21
c ---[ 872]---> Adder-cost: 566   maxlim: 1101823   bits: 22/21
c ---[ 870]---> Adder-cost: 646   maxlim: 1109503   bits: 22/21
c ---[ 868]---> Adder-cost: 868   maxlim: 1116031   bits: 22/21
c ---[ 866]---> Adder-cost: 890   maxlim: 1122431   bits: 22/21
c ---[ 864]---> Adder-cost: 882   maxlim: 1127551   bits: 22/21
c ---[ 862]---> Adder-cost: 944   maxlim: 1132671   bits: 22/21
c ---[ 860]---> Adder-cost: 982   maxlim: 1136127   bits: 22/21
c ---[ 858]---> Adder-cost: 998   maxlim: 1139967   bits: 22/21
c ---[ 856]---> Adder-cost: 1036   maxlim: 1142527   bits: 22/21
c ---[ 854]---> Adder-cost: 1050   maxlim: 1145087   bits: 22/21
c ---[ 852]---> Adder-cost: 1086   maxlim: 1146367   bits: 22/21
c ---[ 850]---> Adder-cost: 1106   maxlim: 1147647   bits: 22/21
c ---[ 848]---> Adder-cost: 1126   maxlim: 1146367   bits: 22/21
c ---[ 846]---> Adder-cost: 1116   maxlim: 1145087   bits: 22/21
c ---[ 844]---> Adder-cost: 1140   maxlim: 1142655   bits: 22/21
c ---[ 842]---> Adder-cost: 1106   maxlim: 1140095   bits: 22/21
c ---[ 840]---> Adder-cost: 1120   maxlim: 1136255   bits: 22/21
c ---[ 838]---> Adder-cost: 1110   maxlim: 1132415   bits: 22/21
c ---[ 836]---> Adder-cost: 1052   maxlim: 1127295   bits: 22/21
c ---[ 834]---> Adder-cost: 1012   maxlim: 1122175   bits: 22/21
c ---[ 832]---> Adder-cost: 920   maxlim: 1116031   bits: 22/21
c ---[ 830]---> Adder-cost: 846   maxlim: 1109631   bits: 22/21
c ---[ 828]---> Adder-cost: 762   maxlim: 1101951   bits: 22/21
c ---[ 826]---> Adder-cost: 690   maxlim: 1094271   bits: 22/21
c ---[ 824]---> Adder-cost: 586   maxlim: 1086591   bits: 22/21
c ---[ 822]---> Adder-cost: 476   maxlim: 1078527   bits: 22/21
c ---[ 820]---> Adder-cost: 388   maxlim: 1070847   bits: 22/21
c ---[ 818]---> Adder-cost: 284   maxlim: 1063679   bits: 22/21
c ---[ 816]---> Adder-cost: 176   maxlim: 1055999   bits: 22/21
c ---[ 814]---> Adder-cost: 176   maxlim: 1055615   bits: 22/21
c ---[ 812]---> Adder-cost: 274   maxlim: 1063295   bits: 22/21
c ---[ 810]---> Adder-cost: 350   maxlim: 1070975   bits: 22/21
c ---[ 808]---> Adder-cost: 422   maxlim: 1078655   bits: 22/21
c ---[ 806]---> Adder-cost: 486   maxlim: 1086335   bits: 22/21
c ---[ 804]---> Adder-cost: 570   maxlim: 1094143   bits: 22/21
c ---[ 802]---> Adder-cost: 624   maxlim: 1101823   bits: 22/21
c ---[ 800]---> Adder-cost: 658   maxlim: 1109503   bits: 22/21
c ---[ 798]---> Adder-cost: 1000   maxlim: 1115903   bits: 22/21
c ---[ 796]---> Adder-cost: 966   maxlim: 1122303   bits: 22/21
c ---[ 794]---> Adder-cost: 1084   maxlim: 1127423   bits: 22/21
c ---[ 792]---> Adder-cost: 1088   maxlim: 1132543   bits: 22/21
c ---[ 790]---> Adder-cost: 1150   maxlim: 1136383   bits: 22/21
c ---[ 788]---> Adder-cost: 1158   maxlim: 1140351   bits: 22/21
c ---[ 786]---> Adder-cost: 1236   maxlim: 1142911   bits: 22/21
c ---[ 784]---> Adder-cost: 1334   maxlim: 1145471   bits: 22/21
c ---[ 782]---> Adder-cost: 1220   maxlim: 1146751   bits: 22/21
c ---[ 780]---> Adder-cost: 1358   maxlim: 1148031   bits: 22/21
c ---[ 778]---> Adder-cost: 1294   maxlim: 1146751   bits: 22/21
c ---[ 776]---> Adder-cost: 1270   maxlim: 1145471   bits: 22/21
c ---[ 774]---> Adder-cost: 1242   maxlim: 1142911   bits: 22/21
c ---[ 772]---> Adder-cost: 1226   maxlim: 1140351   bits: 22/21
c ---[ 770]---> Adder-cost: 1148   maxlim: 1136511   bits: 22/21
c ---[ 768]---> Adder-cost: 1122   maxlim: 1132415   bits: 22/21
c ---[ 766]---> Adder-cost: 1064   maxlim: 1127295   bits: 22/21
c ---[ 764]---> Adder-cost: 1038   maxlim: 1122175   bits: 22/21
c ---[ 762]---> Adder-cost: 932   maxlim: 1116031   bits: 22/21
c ---[ 760]---> Adder-cost: 858   maxlim: 1109631   bits: 22/21
c ---[ 758]---> Adder-cost: 754   maxlim: 1101951   bits: 22/21
c ---[ 756]---> Adder-cost: 642   maxlim: 1094271   bits: 22/21
c ---[ 754]---> Adder-cost: 560   maxlim: 1086591   bits: 22/21
c ---[ 752]---> Adder-cost: 494   maxlim: 1078527   bits: 22/21
c ---[ 750]---> Adder-cost: 378   maxlim: 1070847   bits: 22/21
c ---[ 748]---> Adder-cost: 284   maxlim: 1063679   bits: 22/21
c ---[ 746]---> Adder-cost: 174   maxlim: 1055999   bits: 22/21
c ---[ 744]---> Adder-cost: 176   maxlim: 1055615   bits: 22/21
c ---[ 742]---> Adder-cost: 274   maxlim: 1063295   bits: 22/21
c ---[ 740]---> Adder-cost: 352   maxlim: 1070975   bits: 22/21
c ---[ 738]---> Adder-cost: 416   maxlim: 1078655   bits: 22/21
c ---[ 736]---> Adder-cost: 490   maxlim: 1086335   bits: 22/21
c ---[ 734]---> Adder-cost: 550   maxlim: 1094015   bits: 22/21
c ---[ 732]---> Adder-cost: 628   maxlim: 1101695   bits: 22/21
c ---[ 730]---> Adder-cost: 658   maxlim: 1109503   bits: 22/21
c ---[ 728]---> Adder-cost: 942   maxlim: 1115903   bits: 22/21
c ---[ 726]---> Adder-cost: 968   maxlim: 1122303   bits: 22/21
c ---[ 724]---> Adder-cost: 948   maxlim: 1127423   bits: 22/21
c ---[ 722]---> Adder-cost: 1004   maxlim: 1132543   bits: 22/21
c ---[ 720]---> Adder-cost: 1086   maxlim: 1136383   bits: 22/21
c ---[ 718]---> Adder-cost: 1088   maxlim: 1140351   bits: 22/21
c ---[ 716]---> Adder-cost: 1110   maxlim: 1142911   bits: 22/21
c ---[ 714]---> Adder-cost: 1072   maxlim: 1145087   bits: 22/21
c ---[ 712]---> Adder-cost: 1192   maxlim: 1146367   bits: 22/21
c ---[ 710]---> Adder-cost: 1182   maxlim: 1147647   bits: 22/21
c ---[ 708]---> Adder-cost: 1200   maxlim: 1146367   bits: 22/21
c ---[ 706]---> Adder-cost: 1182   maxlim: 1145471   bits: 22/21
c ---[ 704]---> Adder-cost: 1194   maxlim: 1142911   bits: 22/21
c ---[ 702]---> Adder-cost: 1212   maxlim: 1140351   bits: 22/21
c ---[ 700]---> Adder-cost: 1120   maxlim: 1136511   bits: 22/21
c ---[ 698]---> Adder-cost: 1120   maxlim: 1132415   bits: 22/21
c ---[ 696]---> Adder-cost: 1082   maxlim: 1127295   bits: 22/21
c ---[ 694]---> Adder-cost: 984   maxlim: 1122175   bits: 22/21
c ---[ 692]---> Adder-cost: 960   maxlim: 1116031   bits: 22/21
c ---[ 690]---> Adder-cost: 834   maxlim: 1109631   bits: 22/21
c ---[ 688]---> Adder-cost: 774   maxlim: 1101951   bits: 22/21
c ---[ 686]---> Adder-cost: 658   maxlim: 1094271   bits: 22/21
c ---[ 684]---> Adder-cost: 566   maxlim: 1086591   bits: 22/21
c ---[ 682]---> Adder-cost: 486   maxlim: 1078527   bits: 22/21
c ---[ 680]---> Adder-cost: 386   maxlim: 1070847   bits: 22/21
c ---[ 678]---> Adder-cost: 290   maxlim: 1063679   bits: 22/21
c ---[ 676]---> Adder-cost: 174   maxlim: 1055999   bits: 22/21
c ---[ 674]---> Adder-cost: 176   maxlim: 1055999   bits: 22/21
c ---[ 672]---> Adder-cost: 272   maxlim: 1063679   bits: 22/21
c ---[ 670]---> Adder-cost: 416   maxlim: 1071359   bits: 22/21
c ---[ 668]---> Adder-cost: 404   maxlim: 1079039   bits: 22/21
c ---[ 666]---> Adder-cost: 456   maxlim: 1086719   bits: 22/21
c ---[ 664]---> Adder-cost: 542   maxlim: 1094399   bits: 22/21
c ---[ 662]---> Adder-cost: 598   maxlim: 1102079   bits: 22/21
c ---[ 660]---> Adder-cost: 826   maxlim: 1108479   bits: 22/21
c ---[ 658]---> Adder-cost: 794   maxlim: 1113599   bits: 22/21
c ---[ 656]---> Adder-cost: 916   maxlim: 1117439   bits: 22/21
c ---[ 654]---> Adder-cost: 914   maxlim: 1119999   bits: 22/21
c ---[ 652]---> Adder-cost: 968   maxlim: 1121279   bits: 22/21
c ---[ 650]---> Adder-cost: 944   maxlim: 1121279   bits: 22/21
c ---[ 648]---> Adder-cost: 884   maxlim: 1119999   bits: 22/21
c ---[ 646]---> Adder-cost: 878   maxlim: 1117439   bits: 22/21
c ---[ 644]---> Adder-cost: 876   maxlim: 1113599   bits: 22/21
c ---[ 642]---> Adder-cost: 834   maxlim: 1108479   bits: 22/21
c ---[ 640]---> Adder-cost: 752   maxlim: 1102079   bits: 22/21
c ---[ 638]---> Adder-cost: 656   maxlim: 1094399   bits: 22/21
c ---[ 636]---> Adder-cost: 574   maxlim: 1086719   bits: 22/21
c ---[ 634]---> Adder-cost: 496   maxlim: 1079039   bits: 22/21
c ---[ 632]---> Adder-cost: 394   maxlim: 1071359   bits: 22/21
c ---[ 630]---> Adder-cost: 286   maxlim: 1063679   bits: 22/21
c ---[ 628]---> Adder-cost: 168   maxlim: 1055999   bits: 22/21
c ---[ 626]---> Adder-cost: 176   maxlim: 1055999   bits: 22/21
c ---[ 624]---> Adder-cost: 272   maxlim: 1063679   bits: 22/21
c ---[ 622]---> Adder-cost: 348   maxlim: 1071359   bits: 22/21
c ---[ 620]---> Adder-cost: 424   maxlim: 1079039   bits: 22/21
c ---[ 618]---> Adder-cost: 490   maxlim: 1086719   bits: 22/21
c ---[ 616]---> Adder-cost: 544   maxlim: 1094399   bits: 22/21
c ---[ 614]---> Adder-cost: 620   maxlim: 1102079   bits: 22/21
c ---[ 612]---> Adder-cost: 930   maxlim: 1108479   bits: 22/21
c ---[ 610]---> Adder-cost: 908   maxlim: 1113599   bits: 22/21
c ---[ 608]---> Adder-cost: 924   maxlim: 1117439   bits: 22/21
c ---[ 606]---> Adder-cost: 894   maxlim: 1119999   bits: 22/21
c ---[ 604]---> Adder-cost: 944   maxlim: 1121279   bits: 22/21
c ---[ 602]---> Adder-cost: 952   maxlim: 1121151   bits: 22/21
c ---[ 600]---> Adder-cost: 886   maxlim: 1119871   bits: 22/21
c ---[ 598]---> Adder-cost: 894   maxlim: 1117311   bits: 22/21
c ---[ 596]---> Adder-cost: 860   maxlim: 1113471   bits: 22/21
c ---[ 594]---> Adder-cost: 812   maxlim: 1108351   bits: 22/21
c ---[ 592]---> Adder-cost: 766   maxlim: 1101951   bits: 22/21
c ---[ 590]---> Adder-cost: 658   maxlim: 1094271   bits: 22/21
c ---[ 588]---> Adder-cost: 580   maxlim: 1086591   bits: 22/21
c ---[ 586]---> Adder-cost: 488   maxlim: 1078911   bits: 22/21
c ---[ 584]---> Adder-cost: 368   maxlim: 1071231   bits: 22/21
c ---[ 582]---> Adder-cost: 282   maxlim: 1063551   bits: 22/21
c ---[ 580]---> Adder-cost: 170   maxlim: 1055871   bits: 22/21
c ---[ 579]---> BDD-cost:   21
c ---[ 578]---> BDD-cost:   33
c ---[ 577]---> BDD-cost:   45
c ---[ 576]---> BDD-cost:   57
c ---[ 575]---> BDD-cost:   69
c ---[ 574]---> BDD-cost:   81
c ---[ 573]---> BDD-cost:   93
c ---[ 572]---> BDD-cost:   95
c ---[ 571]---> BDD-cost:  117
c ---[ 570]---> BDD-cost:   21
c ---[ 569]---> BDD-cost:   33
c ---[ 568]---> BDD-cost:   45
c ---[ 567]---> BDD-cost:   57
c ---[ 566]---> BDD-cost:   69
c ---[ 565]---> BDD-cost:   81
c ---[ 564]---> BDD-cost:   93
c ---[ 563]---> BDD-cost:  105
c ---[ 562]---> BDD-cost:  117
c ---[ 561]---> BDD-cost:   21
c ---[ 560]---> BDD-cost:   33
c ---[ 559]---> BDD-cost:   45
c ---[ 558]---> BDD-cost:   57
c ---[ 557]---> BDD-cost:   69
c ---[ 556]---> BDD-cost:   81
c ---[ 555]---> BDD-cost:   93
c ---[ 554]---> BDD-cost:  105
c ---[ 553]---> BDD-cost:  117
c ---[ 552]---> BDD-cost:    9
c ---[ 551]---> BDD-cost:    9
c ---[ 550]---> BDD-cost:    9
c ---[ 549]---> BDD-cost:    9
c ---[ 548]---> BDD-cost:    9
c ---[ 547]---> BDD-cost:   21
c ---[ 546]---> BDD-cost:   33
c ---[ 545]---> BDD-cost:   45
c ---[ 544]---> BDD-cost:   47
c ---[ 543]---> BDD-cost:   21
c ---[ 542]---> BDD-cost:   33
c ---[ 541]---> BDD-cost:   45
c ---[ 540]---> BDD-cost:   57
c ---[ 539]---> BDD-cost:   69
c ---[ 538]---> BDD-cost:   81
c ---[ 537]---> BDD-cost:   93
c ---[ 536]---> BDD-cost:  105
c ---[ 535]---> BDD-cost:  117
c ---[ 534]---> BDD-cost:    9
c ---[ 533]---> BDD-cost:    9
c ---[ 532]---> BDD-cost:    9
c ---[ 531]---> BDD-cost:   21
c ---[ 530]---> BDD-cost:   33
c ---[ 529]---> BDD-cost:   45
c ---[ 528]---> BDD-cost:   47
c ---[ 527]---> BDD-cost:   61
c ---[ 526]---> BDD-cost:   81
c ---[ 525]---> BDD-cost:   83
c ---[ 524]---> BDD-cost:  105
c ---[ 523]---> BDD-cost:  107
c ---[ 522]---> BDD-cost:   21
c ---[ 521]---> BDD-cost:   33
c ---[ 520]---> BDD-cost:   45
c ---[ 519]---> BDD-cost:   57
c ---[ 518]---> BDD-cost:   69
c ---[ 517]---> BDD-cost:   81
c ---[ 516]---> BDD-cost:   47
c ---[ 515]---> BDD-cost:   59
c ---[ 514]---> BDD-cost:   71
c ---[ 513]---> BDD-cost:   21
c ---[ 512]---> BDD-cost:   33
c ---[ 511]---> BDD-cost:   45
c ---[ 510]---> BDD-cost:   57
c ---[ 509]---> BDD-cost:   69
c ---[ 508]---> BDD-cost:   81
c ---[ 507]---> BDD-cost:   93
c ---[ 506]---> BDD-cost:  105
c ---[ 505]---> BDD-cost:  117
c ---[ 504]---> BDD-cost:    9
c ---[ 503]---> BDD-cost:    9
c ---[ 502]---> BDD-cost:    9
c ---[ 501]---> BDD-cost:    9
c ---[ 500]---> BDD-cost:    9
c ---[ 499]---> BDD-cost:   21
c ---[ 498]---> BDD-cost:   33
c ---[ 497]---> BDD-cost:   45
c ---[ 496]---> BDD-cost:   57
c ---[ 495]---> BDD-cost:   21
c ---[ 494]---> BDD-cost:   33
c ---[ 493]---> BDD-cost:   23
c ---[ 492]---> BDD-cost:   35
c ---[ 491]---> BDD-cost:   69
c ---[ 490]---> BDD-cost:   81
c ---[ 489]---> BDD-cost:   71
c ---[ 488]---> BDD-cost:   83
c ---[ 487]---> BDD-cost:   71
c ---[ 486]---> BDD-cost:    9
c ---[ 485]---> BDD-cost:    9
c ---[ 484]---> BDD-cost:    9
c ---[ 483]---> BDD-cost:   21
c ---[ 482]---> BDD-cost:   33
c ---[ 481]---> BDD-cost:   45
c ---[ 480]---> BDD-cost:   57
c ---[ 479]---> BDD-cost:   69
c ---[ 478]---> BDD-cost:   81
c ---[ 477]---> BDD-cost:   93
c ---[ 476]---> BDD-cost:  105
c ---[ 475]---> BDD-cost:  117
c ---[ 474]---> BDD-cost:   21
c ---[ 473]---> BDD-cost:   33
c ---[ 472]---> BDD-cost:   45
c ---[ 471]---> BDD-cost:   57
c ---[ 470]---> BDD-cost:   69
c ---[ 469]---> BDD-cost:   81
c ---[ 468]---> BDD-cost:   93
c ---[ 467]---> BDD-cost:  105
c ---[ 466]---> BDD-cost:  117
c ---[ 465]---> BDD-cost:   21
c ---[ 464]---> BDD-cost:   33
c ---[ 463]---> BDD-cost:   45
c ---[ 462]---> BDD-cost:   57
c ---[ 461]---> BDD-cost:   69
c ---[ 460]---> BDD-cost:   81
c ---[ 459]---> BDD-cost:   93
c ---[ 458]---> BDD-cost:  105
c ---[ 457]---> BDD-cost:  117
c ---[ 456]---> BDD-cost:    9
c ---[ 455]---> BDD-cost:    9
c ---[ 454]---> BDD-cost:    9
c ---[ 453]---> BDD-cost:    9
c ---[ 452]---> BDD-cost:    9
c ---[ 451]---> BDD-cost:   21
c ---[ 450]---> BDD-cost:   33
c ---[ 449]---> BDD-cost:   45
c ---[ 448]---> BDD-cost:   57
c ---[ 447]---> BDD-cost:   21
c ---[ 446]---> BDD-cost:   33
c ---[ 445]---> BDD-cost:   35
c ---[ 444]---> BDD-cost:   47
c ---[ 443]---> BDD-cost:   59
c ---[ 442]---> BDD-cost:   71
c ---[ 441]---> BDD-cost:   83
c ---[ 440]---> BDD-cost:   95
c ---[ 439]---> BDD-cost:  107
c ---[ 438]---> BDD-cost:    9
c ---[ 437]---> BDD-cost:    9
c ---[ 436]---> BDD-cost:    9
c ---[ 435]---> BDD-cost:   21
c ---[ 434]---> BDD-cost:   33
c ---[ 433]---> BDD-cost:   45
c ---[ 432]---> BDD-cost:   47
c ---[ 431]---> BDD-cost:   69
c ---[ 430]---> BDD-cost:   81
c ---[ 429]---> BDD-cost:   93
c ---[ 428]---> BDD-cost:   95
c ---[ 427]---> BDD-cost:  117
c ---[ 426]---> BDD-cost:   21
c ---[ 425]---> BDD-cost:   33
c ---[ 424]---> BDD-cost:   45
c ---[ 423]---> BDD-cost:   57
c ---[ 422]---> BDD-cost:   69
c ---[ 421]---> BDD-cost:   81
c ---[ 420]---> BDD-cost:   93
c ---[ 419]---> BDD-cost:  101
c ---[ 418]---> BDD-cost:   95
c ---[ 417]---> BDD-cost:   21
c ---[ 416]---> BDD-cost:   33
c ---[ 415]---> BDD-cost:   45
c ---[ 414]---> BDD-cost:   57
c ---[ 413]---> BDD-cost:   69
c ---[ 412]---> BDD-cost:   81
c ---[ 411]---> BDD-cost:   93
c ---[ 410]---> BDD-cost:  105
c ---[ 409]---> BDD-cost:  117
c ---[ 408]---> BDD-cost:    9
c ---[ 407]---> BDD-cost:    9
c ---[ 406]---> BDD-cost:    9
c ---[ 405]---> BDD-cost:    9
c ---[ 404]---> BDD-cost:    9
c ---[ 403]---> BDD-cost:   21
c ---[ 402]---> BDD-cost:   33
c ---[ 401]---> BDD-cost:   45
c ---[ 400]---> BDD-cost:   57
c ---[ 399]---> BDD-cost:   21
c ---[ 398]---> BDD-cost:   33
c ---[ 397]---> BDD-cost:   45
c ---[ 396]---> BDD-cost:   57
c ---[ 395]---> BDD-cost:   69
c ---[ 394]---> BDD-cost:   81
c ---[ 393]---> BDD-cost:   71
c ---[ 392]---> BDD-cost:   83
c ---[ 391]---> BDD-cost:   71
c ---[ 390]---> BDD-cost:    9
c ---[ 389]---> BDD-cost:    9
c ---[ 388]---> BDD-cost:    9
c ---[ 387]---> BDD-cost:   21
c ---[ 386]---> BDD-cost:   33
c ---[ 385]---> BDD-cost:   35
c ---[ 384]---> BDD-cost:   57
c ---[ 383]---> BDD-cost:   59
c ---[ 382]---> BDD-cost:   81
c ---[ 381]---> BDD-cost:   83
c ---[ 380]---> BDD-cost:  105
c ---[ 379]---> BDD-cost:  107
c ---[ 378]---> BDD-cost:   21
c ---[ 377]---> BDD-cost:   33
c ---[ 376]---> BDD-cost:   45
c ---[ 375]---> BDD-cost:   57
c ---[ 374]---> BDD-cost:   69
c ---[ 373]---> BDD-cost:   81
c ---[ 372]---> BDD-cost:   93
c ---[ 371]---> BDD-cost:  105
c ---[ 370]---> BDD-cost:  117
c ---[ 369]---> BDD-cost:   21
c ---[ 368]---> BDD-cost:   33
c ---[ 367]---> BDD-cost:   45
c ---[ 366]---> BDD-cost:   57
c ---[ 365]---> BDD-cost:   69
c ---[ 364]---> BDD-cost:   81
c ---[ 363]---> BDD-cost:   93
c ---[ 362]---> BDD-cost:  105
c ---[ 361]---> BDD-cost:  117
c ---[ 360]---> BDD-cost:    9
c ---[ 359]---> BDD-cost:    9
c ---[ 358]---> BDD-cost:    9
c ---[ 357]---> BDD-cost:    9
c ---[ 356]---> BDD-cost:    9
c ---[ 355]---> BDD-cost:   21
c ---[ 354]---> BDD-cost:   33
c ---[ 353]---> BDD-cost:   45
c ---[ 352]---> BDD-cost:   57
c ---[ 351]---> BDD-cost:   11
c ---[ 350]---> BDD-cost:   11
c ---[ 349]---> BDD-cost:   23
c ---[ 348]---> BDD-cost:   35
c ---[ 347]---> BDD-cost:   47
c ---[ 346]---> BDD-cost:   35
c ---[ 345]---> BDD-cost:   71
c ---[ 344]---> BDD-cost:   59
c ---[ 343]---> BDD-cost:   95
c ---[ 342]---> BDD-cost:    9
c ---[ 341]---> BDD-cost:    9
c ---[ 340]---> BDD-cost:    9
c ---[ 339]---> BDD-cost:   21
c ---[ 338]---> BDD-cost:   33
c ---[ 337]---> BDD-cost:   45
c ---[ 336]---> BDD-cost:   47
c ---[ 335]---> BDD-cost:   69
c ---[ 334]---> BDD-cost:   81
c ---[ 333]---> BDD-cost:   93
c ---[ 332]---> BDD-cost:   95
c ---[ 331]---> BDD-cost:  117
c ---[ 330]---> BDD-cost:   21
c ---[ 329]---> BDD-cost:   33
c ---[ 328]---> BDD-cost:   45
c ---[ 327]---> BDD-cost:   57
c ---[ 326]---> BDD-cost:   69
c ---[ 325]---> BDD-cost:   81
c ---[ 324]---> BDD-cost:   93
c ---[ 323]---> BDD-cost:  105
c ---[ 322]---> BDD-cost:   95
c ---[ 321]---> BDD-cost:   21
c ---[ 320]---> BDD-cost:   33
c ---[ 319]---> BDD-cost:   45
c ---[ 318]---> BDD-cost:   57
c ---[ 317]---> BDD-cost:   69
c ---[ 316]---> BDD-cost:   71
c ---[ 315]---> BDD-cost:   83
c ---[ 314]---> BDD-cost:   95
c ---[ 313]---> BDD-cost:   83
c ---[ 312]---> BDD-cost:    9
c ---[ 311]---> BDD-cost:    9
c ---[ 310]---> BDD-cost:    9
c ---[ 309]---> BDD-cost:    9
c ---[ 308]---> BDD-cost:    9
c ---[ 307]---> BDD-cost:   21
c ---[ 306]---> BDD-cost:   33
c ---[ 305]---> BDD-cost:   45
c ---[ 304]---> BDD-cost:   57
c ---[ 303]---> BDD-cost:   21
c ---[ 302]---> BDD-cost:   33
c ---[ 301]---> BDD-cost:   45
c ---[ 300]---> BDD-cost:   57
c ---[ 299]---> BDD-cost:   69
c ---[ 298]---> BDD-cost:   81
c ---[ 297]---> BDD-cost:   71
c ---[ 296]---> BDD-cost:   83
c ---[ 295]---> BDD-cost:   71
c ---[ 294]---> BDD-cost:    9
c ---[ 293]---> BDD-cost:    9
c ---[ 292]---> BDD-cost:    9
c ---[ 291]---> BDD-cost:   11
c ---[ 290]---> BDD-cost:   23
c ---[ 289]---> BDD-cost:   45
c ---[ 288]---> BDD-cost:   47
c ---[ 287]---> BDD-cost:   69
c ---[ 286]---> BDD-cost:   71
c ---[ 285]---> BDD-cost:   93
c ---[ 284]---> BDD-cost:   95
c ---[ 283]---> BDD-cost:  117
c ---[ 282]---> BDD-cost:   21
c ---[ 281]---> BDD-cost:   33
c ---[ 280]---> BDD-cost:   45
c ---[ 279]---> BDD-cost:   57
c ---[ 278]---> BDD-cost:   69
c ---[ 277]---> BDD-cost:   81
c ---[ 276]---> BDD-cost:   93
c ---[ 275]---> BDD-cost:  105
c ---[ 274]---> BDD-cost:  117
c ---[ 273]---> BDD-cost:   21
c ---[ 272]---> BDD-cost:   33
c ---[ 271]---> BDD-cost:   45
c ---[ 270]---> BDD-cost:   57
c ---[ 269]---> BDD-cost:   69
c ---[ 268]---> BDD-cost:   81
c ---[ 267]---> BDD-cost:   93
c ---[ 266]---> BDD-cost:  105
c ---[ 265]---> BDD-cost:  117
c ---[ 264]---> BDD-cost:    9
c ---[ 263]---> BDD-cost:    9
c ---[ 262]---> BDD-cost:    9
c ---[ 261]---> BDD-cost:    9
c ---[ 260]---> BDD-cost:    9
c ---[ 259]---> BDD-cost:   21
c ---[ 258]---> BDD-cost:   33
c ---[ 257]---> BDD-cost:   45
c ---[ 256]---> BDD-cost:   57
c ---[ 255]---> BDD-cost:   21
c ---[ 254]---> BDD-cost:   33
c ---[ 253]---> BDD-cost:   23
c ---[ 252]---> BDD-cost:   35
c ---[ 251]---> BDD-cost:   47
c ---[ 250]---> BDD-cost:   35
c ---[ 249]---> BDD-cost:   71
c ---[ 248]---> BDD-cost:   59
c ---[ 247]---> BDD-cost:   95
c ---[ 246]---> BDD-cost:    9
c ---[ 245]---> BDD-cost:    9
c ---[ 244]---> BDD-cost:    9
c ---[ 243]---> BDD-cost:   21
c ---[ 242]---> BDD-cost:   33
c ---[ 241]---> BDD-cost:   45
c ---[ 240]---> BDD-cost:   57
c ---[ 239]---> BDD-cost:   69
c ---[ 238]---> BDD-cost:   81
c ---[ 237]---> BDD-cost:   93
c ---[ 236]---> BDD-cost:   95
c ---[ 235]---> BDD-cost:  117
c ---[ 234]---> BDD-cost:   21
c ---[ 233]---> BDD-cost:   33
c ---[ 232]---> BDD-cost:   45
c ---[ 231]---> BDD-cost:   57
c ---[ 230]---> BDD-cost:   69
c ---[ 229]---> BDD-cost:   81
c ---[ 228]---> BDD-cost:   93
c ---[ 227]---> BDD-cost:  105
c ---[ 226]---> BDD-cost:  117
c ---[ 225]---> BDD-cost:   21
c ---[ 224]---> BDD-cost:   33
c ---[ 223]---> BDD-cost:   45
c ---[ 222]---> BDD-cost:   57
c ---[ 221]---> BDD-cost:   69
c ---[ 220]---> BDD-cost:   81
c ---[ 219]---> BDD-cost:   71
c ---[ 218]---> BDD-cost:  105
c ---[ 217]---> BDD-cost:   95
c ---[ 216]---> BDD-cost:    9
c ---[ 215]---> BDD-cost:    9
c ---[ 214]---> BDD-cost:    9
c ---[ 213]---> BDD-cost:    9
c ---[ 212]---> BDD-cost:    9
c ---[ 211]---> BDD-cost:   21
c ---[ 210]---> BDD-cost:   33
c ---[ 209]---> BDD-cost:   45
c ---[ 208]---> BDD-cost:   43
c ---[ 207]---> BDD-cost:   21
c ---[ 206]---> BDD-cost:   33
c ---[ 205]---> BDD-cost:   45
c ---[ 204]---> BDD-cost:   57
c ---[ 203]---> BDD-cost:   69
c ---[ 202]---> BDD-cost:   81
c ---[ 201]---> BDD-cost:   71
c ---[ 200]---> BDD-cost:   83
c ---[ 199]---> BDD-cost:   71
c ---[ 198]---> BDD-cost:    9
c ---[ 197]---> BDD-cost:    9
c ---[ 196]---> BDD-cost:    9
c ---[ 195]---> BDD-cost:   21
c ---[ 194]---> BDD-cost:   33
c ---[ 193]---> BDD-cost:   45
c ---[ 192]---> BDD-cost:   47
c ---[ 191]---> BDD-cost:   69
c ---[ 190]---> BDD-cost:   71
c ---[ 189]---> BDD-cost:   93
c ---[ 188]---> BDD-cost:   95
c ---[ 187]---> BDD-cost:  117
c ---[ 186]---> BDD-cost:   11
c ---[ 185]---> BDD-cost:   17
c ---[ 184]---> BDD-cost:   29
c ---[ 183]---> BDD-cost:   29
c ---[ 182]---> BDD-cost:   29
c ---[ 181]---> BDD-cost:   41
c ---[ 180]---> BDD-cost:   53
c ---[ 179]---> BDD-cost:   65
c ---[ 178]---> BDD-cost:   77
c ---[ 177]---> BDD-cost:   21
c ---[ 176]---> BDD-cost:   33
c ---[ 175]---> BDD-cost:   45
c ---[ 174]---> BDD-cost:   57
c ---[ 173]---> BDD-cost:   59
c ---[ 172]---> BDD-cost:   81
c ---[ 171]---> BDD-cost:   83
c ---[ 170]---> BDD-cost:  105
c ---[ 169]---> BDD-cost:  107
c ---[ 168]---> BDD-cost:    9
c ---[ 167]---> BDD-cost:    9
c ---[ 166]---> BDD-cost:    9
c ---[ 165]---> BDD-cost:    9
c ---[ 164]---> BDD-cost:    9
c ---[ 163]---> BDD-cost:   21
c ---[ 162]---> BDD-cost:   33
c ---[ 161]---> BDD-cost:   45
c ---[ 160]---> BDD-cost:   57
c ---[ 159]---> BDD-cost:   21
c ---[ 158]---> BDD-cost:   33
c ---[ 157]---> BDD-cost:   23
c ---[ 156]---> BDD-cost:   35
c ---[ 155]---> BDD-cost:   47
c ---[ 154]---> BDD-cost:   81
c ---[ 153]---> BDD-cost:   83
c ---[ 152]---> BDD-cost:   95
c ---[ 151]---> BDD-cost:  107
c ---[ 150]---> BDD-cost:    9
c ---[ 149]---> BDD-cost:    9
c ---[ 148]---> BDD-cost:    9
c ---[ 147]---> BDD-cost:   21
c ---[ 146]---> BDD-cost:   33
c ---[ 145]---> BDD-cost:   45
c ---[ 144]---> BDD-cost:   47
c ---[ 143]---> BDD-cost:   69
c ---[ 142]---> BDD-cost:   71
c ---[ 141]---> BDD-cost:   93
c ---[ 140]---> BDD-cost:   95
c ---[ 139]---> BDD-cost:  107
c ---[ 138]---> BDD-cost:   21
c ---[ 137]---> BDD-cost:   33
c ---[ 136]---> BDD-cost:   23
c ---[ 135]---> BDD-cost:   35
c ---[ 134]---> BDD-cost:   23
c ---[ 133]---> BDD-cost:   35
c ---[ 132]---> BDD-cost:   47
c ---[ 131]---> BDD-cost:   59
c ---[ 130]---> BDD-cost:   71
c ---[ 129]---> BDD-cost:   21
c ---[ 128]---> BDD-cost:   23
c ---[ 127]---> BDD-cost:   45
c ---[ 126]---> BDD-cost:   47
c ---[ 125]---> BDD-cost:   69
c ---[ 124]---> BDD-cost:   71
c ---[ 123]---> BDD-cost:   93
c ---[ 122]---> BDD-cost:   95
c ---[ 121]---> BDD-cost:  117
c ---[ 120]---> BDD-cost:    9
c ---[ 119]---> BDD-cost:    9
c ---[ 118]---> BDD-cost:    9
c ---[ 117]---> BDD-cost:    9
c ---[ 116]---> BDD-cost:    9
c ---[ 115]---> BDD-cost:   21
c ---[ 114]---> BDD-cost:   33
c ---[ 113]---> BDD-cost:   45
c ---[ 112]---> BDD-cost:   57
c ---[ 111]---> BDD-cost:   21
c ---[ 110]---> BDD-cost:   33
c ---[ 109]---> BDD-cost:   25
c ---[ 108]---> BDD-cost:   35
c ---[ 107]---> BDD-cost:   59
c ---[ 106]---> BDD-cost:   71
c ---[ 105]---> BDD-cost:   83
c ---[ 104]---> BDD-cost:   95
c ---[ 103]---> BDD-cost:   83
c ---[ 102]---> BDD-cost:    9
c ---[ 101]---> BDD-cost:    9
c ---[ 100]---> BDD-cost:    9
c ---[  99]---> BDD-cost:  273
c ---[  98]---> BDD-cost:  273
c ---[  97]---> BDD-cost:  273
c ---[  96]---> BDD-cost:  273
c ---[  95]---> BDD-cost:  269
c ---[  94]---> BDD-cost:  141
c ---[  93]---> BDD-cost:  141
c ---[  92]---> BDD-cost:  271
c ---[  91]---> BDD-cost:  273
c ---[  90]---> BDD-cost:  269
c ---[  89]---> BDD-cost:  273
c ---[  88]---> BDD-cost:  263
c ---[  87]---> BDD-cost:  141
c ---[  86]---> BDD-cost:  141
c ---[  85]---> BDD-cost:  273
c ---[  84]---> BDD-cost:  263
c ---[  83]---> BDD-cost:  265
c ---[  82]---> BDD-cost:  273
c ---[  81]---> BDD-cost:  273
c ---[  80]---> BDD-cost:  141
c ---[  79]---> BDD-cost:  141
c ---[  78]---> BDD-cost:  263
c ---[  77]---> BDD-cost:  273
c ---[  76]---> BDD-cost:  273
c ---[  75]---> BDD-cost:  239
c ---[  74]---> BDD-cost:  263
c ---[  73]---> BDD-cost:  141
c ---[  72]---> BDD-cost:  141
c ---[  71]---> BDD-cost:  269
c ---[  70]---> BDD-cost:  227
c ---[  69]---> BDD-cost:  263
c ---[  68]---> BDD-cost:  267
c ---[  67]---> BDD-cost:  263
c ---[  66]---> BDD-cost:  141
c ---[  65]---> BDD-cost:  141
c ---[  64]---> BDD-cost:  239
c ---[  63]---> BDD-cost:  265
c ---[  62]---> BDD-cost:  251
c ---[  61]---> BDD-cost:  273
c ---[  60]---> BDD-cost:  273
c ---[  59]---> BDD-cost:  141
c ---[  58]---> BDD-cost:  141
c ---[  57]---> BDD-cost:  273
c ---[  56]---> BDD-cost:  273
c ---[  55]---> BDD-cost:  273
c ---[  54]---> BDD-cost:  273
c ---[  53]---> BDD-cost:  251
c ---[  52]---> BDD-cost:  141
c ---[  51]---> BDD-cost:  141
c ---[  50]---> BDD-cost:  263
c ---[  49]---> BDD-cost:  273
c ---[  48]---> BDD-cost:  273
c ---[  47]---> BDD-cost:  273
c ---[  46]---> BDD-cost:  273
c ---[  45]---> BDD-cost:  115
c ---[  44]---> BDD-cost:  141
c ---[  43]---> BDD-cost:  263
c ---[  42]---> BDD-cost:  263
c ---[  41]---> BDD-cost:  273
c ---[  40]---> BDD-cost:  233
c ---[  39]---> BDD-cost:  273
c ---[  38]---> BDD-cost:  141
c ---[  37]---> BDD-cost:  141
c ---[  36]---> BDD-cost:  261
c ---[  35]---> BDD-cost:  239
c ---[  34]---> BDD-cost:  263
c ---[  33]---> BDD-cost:  273
c ---[  32]---> BDD-cost:  263
c ---[  31]---> BDD-cost:  141
c ---[  30]---> BDD-cost:  141
c ---[  29]---> Adder-cost: 1446   maxlim: 828   bits: 10/10
c ---[  28]---> Adder-cost: 1416   maxlim: 828   bits: 10/10
c ---[  27]---> Adder-cost: 1412   maxlim: 828   bits: 10/10
c ---[  26]---> Adder-cost: 1448   maxlim: 828   bits: 10/10
c ---[  25]---> Adder-cost: 1428   maxlim: 828   bits: 10/10
c ---[  24]---> Adder-cost: 1438   maxlim: 828   bits: 10/10
c ---[  23]---> Adder-cost: 1438   maxlim: 828   bits: 10/10
c ---[  22]---> Adder-cost: 1388   maxlim: 828   bits: 10/10
c ---[  21]---> Adder-cost: 1470   maxlim: 828   bits: 10/10
c ---[  20]---> Adder-cost: 1388   maxlim: 828   bits: 10/10
c ---[  19]---> BDD-cost: 1307
c ---[  18]---> BDD-cost: 1302
c ---[  17]---> BDD-cost: 1303
c ---[  16]---> BDD-cost: 1305
c ---[  15]---> BDD-cost: 1302
c ---[  14]---> BDD-cost: 1299
c ---[  13]---> BDD-cost: 1307
c ---[  12]---> BDD-cost: 1307
c ---[  11]---> BDD-cost: 1305
c ---[  10]---> BDD-cost: 1307
c ---[   9]---> BDD-cost:  721
c ---[   8]---> BDD-cost:  716
c ---[   7]---> BDD-cost:  716
c ---[   6]---> BDD-cost:  721
c ---[   5]---> BDD-cost:  717
c ---[   4]---> BDD-cost:  731
c ---[   3]---> BDD-cost:  675
c ---[   2]---> BDD-cost:  714
c ---[   1]---> BDD-cost:  723
c ---[   0]---> BDD-cost:  731
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 2307742  7817718 |  769247       0        0     nan |  0.000 % |
c |       102 | 2307715  7817623 |  846171     100      538     5.4 |  1.956 % |
c |       264 | 2307712  7817614 |  930788     257    11092    43.2 |  1.956 % |
c |       490 | 2307703  7817587 | 1023867     474    15162    32.0 |  1.957 % |
c |       828 | 2307703  7817587 | 1126254     812    28025    34.5 |  1.957 % |
c |      1335 | 2307635  7817347 | 1238879    1306    63664    48.7 |  1.957 % |
c |      2094 | 2307635  7817347 | 1362767    2065    92386    44.7 |  1.957 % |
c |      3234 | 2307451  7816689 | 1499044    3185   179837    56.5 |  1.959 % |
c |      4943 | 2307299  7816151 | 1648949    4839   319898    66.1 |  1.961 % |
c |      7507 | 2306792  7814328 | 1813844    7361   559199    76.0 |  1.965 % |
c |     11351 | 2306394  7812896 | 1995228   11168   872187    78.1 |  1.969 % |
c |     17117 | 2306106  7811868 | 2194751   16900  1534364    90.8 |  1.971 % |
c |     25767 | 2305918  7811204 | 2414226   25531  2567240   100.6 |  1.973 % |
c |     38742 | 2305589  7810019 | 2655649   38464  4263347   110.8 |  1.977 % |
c |     58203 | 2304913  7807599 | 2921214   57819  6790674   117.4 |  1.983 % |

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/31832/stat): 31832 (minisat+_script) R 31831 31832 31778 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1797769385 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/31832/statm): 174 3 169 147 0 27 0
[pid=31832] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=31833
New process pid=31834
New process pid=31835
execve syscall for /bin/sed executable
One traced child (pid=31834) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=31835) exited with status: 0
One traced child (pid=31833) exited with status: 0
New process pid=31836
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-neos6.opb

[startup+10.0039 s]
Raw data (loadavg): 0.94 0.98 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 8933 0 0 0 922 37 0 0 25 0 1 0 1797769389 38002688 8320 4294967295 134512640 135094434 3221224432 3221223120 134596558 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 9278 8320 145 145 0 9133 0
[pid=31836] vsize: 37112
Current children cumulated CPU time (s) 9.61
Current children cumulated vsize (Kb) 39236

[startup+20.0048 s]
Raw data (loadavg): 0.95 0.98 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 10859 0 0 0 1915 42 0 0 25 0 1 0 1797769389 42303488 9587 4294967295 134512640 135094434 3221224432 3221221188 134519104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31836/statm): 10328 9587 145 145 0 10183 0
[pid=31836] vsize: 41312
Current children cumulated CPU time (s) 19.59
Current children cumulated vsize (Kb) 43436

[startup+30.0066 s]
Raw data (loadavg): 0.96 0.98 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 11467 0 0 0 2912 45 0 0 25 0 1 0 1797769389 43868160 10195 4294967295 134512640 135094434 3221224432 3221220384 134778841 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 10710 10195 145 145 0 10565 0
[pid=31836] vsize: 42840
Current children cumulated CPU time (s) 29.59
Current children cumulated vsize (Kb) 44964

[startup+40.0074 s]
Raw data (loadavg): 0.96 0.98 0.95 1/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) T 31832 31832 31778 0 -1 0 15717 0 0 0 3885 60 0 0 18 0 1 0 1797769389 67854336 14445 4294967295 134512640 135094434 3221224432 3221190300 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/31836/statm): 16566 14445 145 145 0 16421 0
[pid=31836] vsize: 66264
Current children cumulated CPU time (s) 39.47
Current children cumulated vsize (Kb) 68388

[startup+50.0082 s]
Raw data (loadavg): 1.04 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 48846 0 0 0 4588 196 0 0 20 0 1 0 1797769389 215498752 47574 4294967295 134512640 135094434 3221224432 3221222160 134552168 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31836/statm): 52612 47574 145 145 0 52467 0
[pid=31836] vsize: 210448
Current children cumulated CPU time (s) 47.86
Current children cumulated vsize (Kb) 212572

[startup+60.009 s]
Raw data (loadavg): 1.04 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 52585 0 0 0 5549 214 0 0 25 0 1 0 1797769389 260071424 51313 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 63494 51313 145 145 0 63349 0
[pid=31836] vsize: 253976
Current children cumulated CPU time (s) 57.65
Current children cumulated vsize (Kb) 256100

[startup+70.0099 s]
Raw data (loadavg): 1.03 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 52716 0 0 0 6546 215 0 0 25 0 1 0 1797769389 260612096 51444 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 63626 51444 145 145 0 63481 0
[pid=31836] vsize: 254504
Current children cumulated CPU time (s) 67.63
Current children cumulated vsize (Kb) 256628

[startup+80.0117 s]
Raw data (loadavg): 1.02 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 52795 0 0 0 7545 215 0 0 25 0 1 0 1797769389 260935680 51523 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 63705 51523 145 145 0 63560 0
[pid=31836] vsize: 254820
Current children cumulated CPU time (s) 77.62
Current children cumulated vsize (Kb) 256944

[startup+90.0125 s]
Raw data (loadavg): 1.02 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 52836 0 0 0 8544 216 0 0 25 0 1 0 1797769389 261103616 51564 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 63746 51564 145 145 0 63601 0
[pid=31836] vsize: 254984
Current children cumulated CPU time (s) 87.62
Current children cumulated vsize (Kb) 257108

[startup+100.013 s]
Raw data (loadavg): 1.02 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 52871 0 0 0 9544 216 0 0 25 0 1 0 1797769389 261246976 51599 4294967295 134512640 135094434 3221224432 3221223088 134557890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 63781 51599 145 145 0 63636 0
[pid=31836] vsize: 255124
Current children cumulated CPU time (s) 97.62
Current children cumulated vsize (Kb) 257248

[startup+110.015 s]
Raw data (loadavg): 1.01 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 52912 0 0 0 10543 216 0 0 25 0 1 0 1797769389 261414912 51640 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 63822 51640 145 145 0 63677 0
[pid=31836] vsize: 255288
Current children cumulated CPU time (s) 107.61
Current children cumulated vsize (Kb) 257412

[startup+120.016 s]
Raw data (loadavg): 1.01 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 52988 0 0 0 11541 217 0 0 25 0 1 0 1797769389 261738496 51716 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 63901 51716 145 145 0 63756 0
[pid=31836] vsize: 255604
Current children cumulated CPU time (s) 117.6
Current children cumulated vsize (Kb) 257728

[startup+130.018 s]
Raw data (loadavg): 1.01 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 53054 0 0 0 12541 217 0 0 25 0 1 0 1797769389 262004736 51782 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 63966 51782 145 145 0 63821 0
[pid=31836] vsize: 255864
Current children cumulated CPU time (s) 127.6
Current children cumulated vsize (Kb) 257988

[startup+140.019 s]
Raw data (loadavg): 1.01 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 53095 0 0 0 13541 217 0 0 25 0 1 0 1797769389 262172672 51823 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 64007 51823 145 145 0 63862 0
[pid=31836] vsize: 256028
Current children cumulated CPU time (s) 137.6
Current children cumulated vsize (Kb) 258152

[startup+150.019 s]
Raw data (loadavg): 1.01 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 53154 0 0 0 14540 218 0 0 25 0 1 0 1797769389 262410240 51882 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 64065 51882 145 145 0 63920 0
[pid=31836] vsize: 256260
Current children cumulated CPU time (s) 147.6
Current children cumulated vsize (Kb) 258384

[startup+160.02 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 53237 0 0 0 15539 219 0 0 25 0 1 0 1797769389 262746112 51965 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 64147 51965 145 145 0 64002 0
[pid=31836] vsize: 256588
Current children cumulated CPU time (s) 157.6
Current children cumulated vsize (Kb) 258712

[startup+170.021 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 53313 0 0 0 16538 220 0 0 25 0 1 0 1797769389 263057408 52041 4294967295 134512640 135094434 3221224432 3221223092 134553444 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 64223 52041 145 145 0 64078 0
[pid=31836] vsize: 256892
Current children cumulated CPU time (s) 167.6
Current children cumulated vsize (Kb) 259016

[startup+180.023 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 53380 0 0 0 17537 220 0 0 25 0 1 0 1797769389 263360512 52108 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 64297 52108 145 145 0 64152 0
[pid=31836] vsize: 257188
Current children cumulated CPU time (s) 177.59
Current children cumulated vsize (Kb) 259312

[startup+190.025 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 53429 0 0 0 18536 220 0 0 25 0 1 0 1797769389 263557120 52157 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 64345 52157 145 145 0 64200 0
[pid=31836] vsize: 257380
Current children cumulated CPU time (s) 187.58
Current children cumulated vsize (Kb) 259504

[startup+200.026 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 53544 0 0 0 19535 221 0 0 25 0 1 0 1797769389 264024064 52272 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 64459 52272 145 145 0 64314 0
[pid=31836] vsize: 257836
Current children cumulated CPU time (s) 197.58
Current children cumulated vsize (Kb) 259960

[startup+210.026 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 53663 0 0 0 20533 222 0 0 25 0 1 0 1797769389 264503296 52391 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 64576 52391 145 145 0 64431 0
[pid=31836] vsize: 258304
Current children cumulated CPU time (s) 207.57
Current children cumulated vsize (Kb) 260428

[startup+220.027 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 53733 0 0 0 21531 223 0 0 25 0 1 0 1797769389 264790016 52461 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 64646 52461 145 145 0 64501 0
[pid=31836] vsize: 258584
Current children cumulated CPU time (s) 217.56
Current children cumulated vsize (Kb) 260708

[startup+230.029 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 53826 0 0 0 22530 224 0 0 25 0 1 0 1797769389 265166848 52554 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 64738 52554 145 145 0 64593 0
[pid=31836] vsize: 258952
Current children cumulated CPU time (s) 227.56
Current children cumulated vsize (Kb) 261076

[startup+240.03 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 53872 0 0 0 23530 224 0 0 25 0 1 0 1797769389 265351168 52600 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 64783 52600 145 145 0 64638 0
[pid=31836] vsize: 259132
Current children cumulated CPU time (s) 237.56
Current children cumulated vsize (Kb) 261256

[startup+250.031 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 53913 0 0 0 24529 224 0 0 25 0 1 0 1797769389 265519104 52641 4294967295 134512640 135094434 3221224432 3221223104 134556519 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 64824 52641 145 145 0 64679 0
[pid=31836] vsize: 259296
Current children cumulated CPU time (s) 247.55
Current children cumulated vsize (Kb) 261420

[startup+260.032 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 53960 0 0 0 25528 224 0 0 25 0 1 0 1797769389 265707520 52688 4294967295 134512640 135094434 3221224432 3221223056 134557648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 64870 52688 145 145 0 64725 0
[pid=31836] vsize: 259480
Current children cumulated CPU time (s) 257.54
Current children cumulated vsize (Kb) 261604

[startup+270.033 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 54012 0 0 0 26528 225 0 0 25 0 1 0 1797769389 265920512 52740 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 64922 52740 145 145 0 64777 0
[pid=31836] vsize: 259688
Current children cumulated CPU time (s) 267.55
Current children cumulated vsize (Kb) 261812

[startup+280.035 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 54090 0 0 0 27527 225 0 0 25 0 1 0 1797769389 266235904 52818 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 64999 52818 145 145 0 64854 0
[pid=31836] vsize: 259996
Current children cumulated CPU time (s) 277.54
Current children cumulated vsize (Kb) 262120

[startup+290.036 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 54212 0 0 0 28525 226 0 0 25 0 1 0 1797769389 266735616 52940 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 65121 52940 145 145 0 64976 0
[pid=31836] vsize: 260484
Current children cumulated CPU time (s) 287.53
Current children cumulated vsize (Kb) 262608

[startup+300.037 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 54320 0 0 0 29524 227 0 0 25 0 1 0 1797769389 267239424 53048 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 65244 53048 145 145 0 65099 0
[pid=31836] vsize: 260976
Current children cumulated CPU time (s) 297.53
Current children cumulated vsize (Kb) 263100

[startup+310.039 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 54416 0 0 0 30523 228 0 0 25 0 1 0 1797769389 267628544 53144 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 65339 53144 145 145 0 65194 0
[pid=31836] vsize: 261356
Current children cumulated CPU time (s) 307.53
Current children cumulated vsize (Kb) 263480

[startup+320.039 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 54506 0 0 0 31521 228 0 0 25 0 1 0 1797769389 267997184 53234 4294967295 134512640 135094434 3221224432 3221223120 134554687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 65429 53234 145 145 0 65284 0
[pid=31836] vsize: 261716
Current children cumulated CPU time (s) 317.51
Current children cumulated vsize (Kb) 263840

[startup+330.041 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 54567 0 0 0 32520 229 0 0 25 0 1 0 1797769389 268242944 53295 4294967295 134512640 135094434 3221224432 3221223088 134558029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 65489 53295 145 145 0 65344 0
[pid=31836] vsize: 261956
Current children cumulated CPU time (s) 327.51
Current children cumulated vsize (Kb) 264080

[startup+340.042 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 54673 0 0 0 33518 230 0 0 25 0 1 0 1797769389 268677120 53401 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 65595 53401 145 145 0 65450 0
[pid=31836] vsize: 262380
Current children cumulated CPU time (s) 337.5
Current children cumulated vsize (Kb) 264504

[startup+350.043 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 54761 0 0 0 34516 231 0 0 25 0 1 0 1797769389 269033472 53489 4294967295 134512640 135094434 3221224432 3221223024 134557404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 65682 53489 145 145 0 65537 0
[pid=31836] vsize: 262728
Current children cumulated CPU time (s) 347.49
Current children cumulated vsize (Kb) 264852

[startup+360.045 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 54915 0 0 0 35513 232 0 0 25 0 1 0 1797769389 269660160 53643 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 65835 53643 145 145 0 65690 0
[pid=31836] vsize: 263340
Current children cumulated CPU time (s) 357.47
Current children cumulated vsize (Kb) 265464

[startup+370.046 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 55112 0 0 0 36509 234 0 0 25 0 1 0 1797769389 270462976 53840 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 66031 53840 145 145 0 65886 0
[pid=31836] vsize: 264124
Current children cumulated CPU time (s) 367.45
Current children cumulated vsize (Kb) 266248

[startup+380.047 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 55169 0 0 0 37508 234 0 0 25 0 1 0 1797769389 270692352 53897 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 66087 53897 145 145 0 65942 0
[pid=31836] vsize: 264348
Current children cumulated CPU time (s) 377.44
Current children cumulated vsize (Kb) 266472

[startup+390.048 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 55224 0 0 0 38507 235 0 0 25 0 1 0 1797769389 270917632 53952 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 66142 53952 145 145 0 65997 0
[pid=31836] vsize: 264568
Current children cumulated CPU time (s) 387.44
Current children cumulated vsize (Kb) 266692

[startup+400.049 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 55288 0 0 0 39507 235 0 0 25 0 1 0 1797769389 271175680 54016 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 66205 54016 145 145 0 66060 0
[pid=31836] vsize: 264820
Current children cumulated CPU time (s) 397.44
Current children cumulated vsize (Kb) 266944

[startup+410.05 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 55391 0 0 0 40505 236 0 0 25 0 1 0 1797769389 271593472 54119 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 66307 54119 145 145 0 66162 0
[pid=31836] vsize: 265228
Current children cumulated CPU time (s) 407.43
Current children cumulated vsize (Kb) 267352

[startup+420.051 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 55459 0 0 0 41503 237 0 0 25 0 1 0 1797769389 271872000 54187 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 66375 54187 145 145 0 66230 0
[pid=31836] vsize: 265500
Current children cumulated CPU time (s) 417.42
Current children cumulated vsize (Kb) 267624

[startup+430.052 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 55556 0 0 0 42502 238 0 0 25 0 1 0 1797769389 272265216 54284 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 66471 54284 145 145 0 66326 0
[pid=31836] vsize: 265884
Current children cumulated CPU time (s) 427.42
Current children cumulated vsize (Kb) 268008

[startup+440.053 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 55664 0 0 0 43500 239 0 0 25 0 1 0 1797769389 272703488 54392 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31836/statm): 66578 54392 145 145 0 66433 0
[pid=31836] vsize: 266312
Current children cumulated CPU time (s) 437.41
Current children cumulated vsize (Kb) 268436

[startup+450.065 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 55768 0 0 0 44496 240 0 0 25 0 1 0 1797769389 273129472 54496 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 66682 54496 145 145 0 66537 0
[pid=31836] vsize: 266728
Current children cumulated CPU time (s) 447.38
Current children cumulated vsize (Kb) 268852

[startup+460.066 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 55850 0 0 0 45494 241 0 0 25 0 1 0 1797769389 273461248 54578 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 66763 54578 145 145 0 66618 0
[pid=31836] vsize: 267052
Current children cumulated CPU time (s) 457.37
Current children cumulated vsize (Kb) 269176

[startup+470.067 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 55926 0 0 0 46493 242 0 0 25 0 1 0 1797769389 273780736 54654 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 66841 54654 145 145 0 66696 0
[pid=31836] vsize: 267364
Current children cumulated CPU time (s) 467.37
Current children cumulated vsize (Kb) 269488

[startup+480.068 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 56007 0 0 0 47492 242 0 0 25 0 1 0 1797769389 274112512 54735 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 66922 54735 145 145 0 66777 0
[pid=31836] vsize: 267688
Current children cumulated CPU time (s) 477.36
Current children cumulated vsize (Kb) 269812

[startup+490.068 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 56092 0 0 0 48490 243 0 0 25 0 1 0 1797769389 274456576 54820 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 67006 54820 145 145 0 66861 0
[pid=31836] vsize: 268024
Current children cumulated CPU time (s) 487.35
Current children cumulated vsize (Kb) 270148

[startup+500.069 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 56174 0 0 0 49489 243 0 0 25 0 1 0 1797769389 274788352 54902 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 67087 54902 145 145 0 66942 0
[pid=31836] vsize: 268348
Current children cumulated CPU time (s) 497.34
Current children cumulated vsize (Kb) 270472

[startup+510.07 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 56259 0 0 0 50487 244 0 0 25 0 1 0 1797769389 275136512 54987 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 67172 54987 145 145 0 67027 0
[pid=31836] vsize: 268688
Current children cumulated CPU time (s) 507.33
Current children cumulated vsize (Kb) 270812

[startup+520.071 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 56297 0 0 0 51487 244 0 0 25 0 1 0 1797769389 275292160 55025 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 67210 55025 145 145 0 67065 0
[pid=31836] vsize: 268840
Current children cumulated CPU time (s) 517.33
Current children cumulated vsize (Kb) 270964

[startup+530.072 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 56380 0 0 0 52486 245 0 0 25 0 1 0 1797769389 275623936 55108 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 67291 55108 145 145 0 67146 0
[pid=31836] vsize: 269164
Current children cumulated CPU time (s) 527.33
Current children cumulated vsize (Kb) 271288

[startup+540.072 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 56459 0 0 0 53485 246 0 0 25 0 1 0 1797769389 275947520 55187 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 67370 55187 145 145 0 67225 0
[pid=31836] vsize: 269480
Current children cumulated CPU time (s) 537.33
Current children cumulated vsize (Kb) 271604

[startup+550.073 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 56531 0 0 0 54484 246 0 0 25 0 1 0 1797769389 276242432 55259 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 67442 55259 145 145 0 67297 0
[pid=31836] vsize: 269768
Current children cumulated CPU time (s) 547.32
Current children cumulated vsize (Kb) 271892

[startup+560.074 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 56620 0 0 0 55483 247 0 0 25 0 1 0 1797769389 276733952 55348 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 67562 55348 145 145 0 67417 0
[pid=31836] vsize: 270248
Current children cumulated CPU time (s) 557.32
Current children cumulated vsize (Kb) 272372

[startup+570.075 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 56717 0 0 0 56482 247 0 0 25 0 1 0 1797769389 277127168 55445 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 67658 55445 145 145 0 67513 0
[pid=31836] vsize: 270632
Current children cumulated CPU time (s) 567.31
Current children cumulated vsize (Kb) 272756

[startup+580.076 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 56800 0 0 0 57481 248 0 0 25 0 1 0 1797769389 277467136 55528 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 67741 55528 145 145 0 67596 0
[pid=31836] vsize: 270964
Current children cumulated CPU time (s) 577.31
Current children cumulated vsize (Kb) 273088

[startup+590.077 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 56867 0 0 0 58480 249 0 0 25 0 1 0 1797769389 277737472 55595 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 67807 55595 145 145 0 67662 0
[pid=31836] vsize: 271228
Current children cumulated CPU time (s) 587.31
Current children cumulated vsize (Kb) 273352

[startup+600.077 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 56941 0 0 0 59479 249 0 0 25 0 1 0 1797769389 278040576 55669 4294967295 134512640 135094434 3221224432 3221223092 134553519 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 67881 55669 145 145 0 67736 0
[pid=31836] vsize: 271524
Current children cumulated CPU time (s) 597.3
Current children cumulated vsize (Kb) 273648

[startup+610.079 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 57001 0 0 0 60478 250 0 0 25 0 1 0 1797769389 278282240 55729 4294967295 134512640 135094434 3221224432 3221223088 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 67940 55729 145 145 0 67795 0
[pid=31836] vsize: 271760
Current children cumulated CPU time (s) 607.3
Current children cumulated vsize (Kb) 273884

[startup+620.08 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 57173 0 0 0 61474 252 0 0 25 0 1 0 1797769389 278982656 55901 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 68111 55901 145 145 0 67966 0
[pid=31836] vsize: 272444
Current children cumulated CPU time (s) 617.28
Current children cumulated vsize (Kb) 274568

[startup+630.081 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 57299 0 0 0 62472 252 0 0 25 0 1 0 1797769389 279494656 56027 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 68236 56027 145 145 0 68091 0
[pid=31836] vsize: 272944
Current children cumulated CPU time (s) 627.26
Current children cumulated vsize (Kb) 275068

[startup+640.082 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 57423 0 0 0 63470 253 0 0 25 0 1 0 1797769389 280002560 56151 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31836/statm): 68360 56151 145 145 0 68215 0
[pid=31836] vsize: 273440
Current children cumulated CPU time (s) 637.25
Current children cumulated vsize (Kb) 275564

[startup+650.083 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 57534 0 0 0 64467 254 0 0 25 0 1 0 1797769389 280453120 56262 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 68470 56262 145 145 0 68325 0
[pid=31836] vsize: 273880
Current children cumulated CPU time (s) 647.23
Current children cumulated vsize (Kb) 276004

[startup+660.083 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 57650 0 0 0 65466 255 0 0 25 0 1 0 1797769389 280928256 56378 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 68586 56378 145 145 0 68441 0
[pid=31836] vsize: 274344
Current children cumulated CPU time (s) 657.23
Current children cumulated vsize (Kb) 276468

[startup+670.084 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 57731 0 0 0 66464 255 0 0 25 0 1 0 1797769389 281255936 56459 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 68666 56459 145 145 0 68521 0
[pid=31836] vsize: 274664
Current children cumulated CPU time (s) 667.21
Current children cumulated vsize (Kb) 276788

[startup+680.085 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 57828 0 0 0 67463 256 0 0 25 0 1 0 1797769389 281653248 56556 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 68763 56556 145 145 0 68618 0
[pid=31836] vsize: 275052
Current children cumulated CPU time (s) 677.21
Current children cumulated vsize (Kb) 277176

[startup+690.086 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 57915 0 0 0 68462 256 0 0 25 0 1 0 1797769389 282005504 56643 4294967295 134512640 135094434 3221224432 3221223120 134554687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 68849 56643 145 145 0 68704 0
[pid=31836] vsize: 275396
Current children cumulated CPU time (s) 687.2
Current children cumulated vsize (Kb) 277520

[startup+700.087 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 57989 0 0 0 69461 257 0 0 25 0 1 0 1797769389 282308608 56717 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 68923 56717 145 145 0 68778 0
[pid=31836] vsize: 275692
Current children cumulated CPU time (s) 697.2
Current children cumulated vsize (Kb) 277816

[startup+710.088 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 58092 0 0 0 70459 257 0 0 25 0 1 0 1797769389 282726400 56820 4294967295 134512640 135094434 3221224432 3221223044 134563049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 69025 56820 145 145 0 68880 0
[pid=31836] vsize: 276100
Current children cumulated CPU time (s) 707.18
Current children cumulated vsize (Kb) 278224

[startup+720.089 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 58183 0 0 0 71458 258 0 0 25 0 1 0 1797769389 283099136 56911 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 69116 56911 145 145 0 68971 0
[pid=31836] vsize: 276464
Current children cumulated CPU time (s) 717.18
Current children cumulated vsize (Kb) 278588

[startup+730.09 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 58258 0 0 0 72457 258 0 0 25 0 1 0 1797769389 283402240 56986 4294967295 134512640 135094434 3221224432 3221223088 134557835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 69190 56986 145 145 0 69045 0
[pid=31836] vsize: 276760
Current children cumulated CPU time (s) 727.17
Current children cumulated vsize (Kb) 278884

[startup+740.091 s]
Raw data (loadavg): 1.00 1.00 0.95 3/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 58297 0 0 0 73456 259 0 0 25 0 1 0 1797769389 283561984 57025 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 69229 57025 145 145 0 69084 0
[pid=31836] vsize: 276916
Current children cumulated CPU time (s) 737.17
Current children cumulated vsize (Kb) 279040

[startup+750.092 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 58319 0 0 0 74456 259 0 0 25 0 1 0 1797769389 283648000 57047 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 69250 57047 145 145 0 69105 0
[pid=31836] vsize: 277000
Current children cumulated CPU time (s) 747.17
Current children cumulated vsize (Kb) 279124

[startup+760.093 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 58343 0 0 0 75456 259 0 0 25 0 1 0 1797769389 283746304 57071 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 69274 57071 145 145 0 69129 0
[pid=31836] vsize: 277096
Current children cumulated CPU time (s) 757.17
Current children cumulated vsize (Kb) 279220

[startup+770.093 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 58387 0 0 0 76456 259 0 0 25 0 1 0 1797769389 283930624 57115 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 69319 57115 145 145 0 69174 0
[pid=31836] vsize: 277276
Current children cumulated CPU time (s) 767.17
Current children cumulated vsize (Kb) 279400

[startup+780.094 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 58584 0 0 0 77453 261 0 0 25 0 1 0 1797769389 284610560 57312 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 69485 57312 145 145 0 69340 0
[pid=31836] vsize: 277940
Current children cumulated CPU time (s) 777.16
Current children cumulated vsize (Kb) 280064

[startup+790.095 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 58642 0 0 0 78452 261 0 0 25 0 1 0 1797769389 284848128 57370 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 69543 57370 145 145 0 69398 0
[pid=31836] vsize: 278172
Current children cumulated CPU time (s) 787.15
Current children cumulated vsize (Kb) 280296

[startup+800.096 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 58706 0 0 0 79451 262 0 0 25 0 1 0 1797769389 285110272 57434 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31836/statm): 69607 57434 145 145 0 69462 0
[pid=31836] vsize: 278428
Current children cumulated CPU time (s) 797.15
Current children cumulated vsize (Kb) 280552

[startup+810.098 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 58827 0 0 0 80448 264 0 0 25 0 1 0 1797769389 285605888 57555 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31836/statm): 69728 57555 145 145 0 69583 0
[pid=31836] vsize: 278912
Current children cumulated CPU time (s) 807.14
Current children cumulated vsize (Kb) 281036

[startup+820.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 58910 0 0 0 81445 265 0 0 25 0 1 0 1797769389 285945856 57638 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31836/statm): 69811 57638 145 145 0 69666 0
[pid=31836] vsize: 279244
Current children cumulated CPU time (s) 817.12
Current children cumulated vsize (Kb) 281368

[startup+830.1 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 59076 0 0 0 82441 266 0 0 25 0 1 0 1797769389 286625792 57804 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31836/statm): 69977 57804 145 145 0 69832 0
[pid=31836] vsize: 279908
Current children cumulated CPU time (s) 827.09
Current children cumulated vsize (Kb) 282032

[startup+840.101 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 59191 0 0 0 83439 267 0 0 25 0 1 0 1797769389 287088640 57919 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31836/statm): 70090 57919 145 145 0 69945 0
[pid=31836] vsize: 280360
Current children cumulated CPU time (s) 837.08
Current children cumulated vsize (Kb) 282484

[startup+850.103 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 59296 0 0 0 84437 268 0 0 25 0 1 0 1797769389 287518720 58024 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31836/statm): 70195 58024 145 145 0 70050 0
[pid=31836] vsize: 280780
Current children cumulated CPU time (s) 847.07
Current children cumulated vsize (Kb) 282904

[startup+860.105 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 59364 0 0 0 85436 269 0 0 25 0 1 0 1797769389 287805440 58092 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31836/statm): 70265 58092 145 145 0 70120 0
[pid=31836] vsize: 281060
Current children cumulated CPU time (s) 857.07
Current children cumulated vsize (Kb) 283184

[startup+870.106 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 59439 0 0 0 86434 270 0 0 25 0 1 0 1797769389 288116736 58167 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31836/statm): 70341 58167 145 145 0 70196 0
[pid=31836] vsize: 281364
Current children cumulated CPU time (s) 867.06
Current children cumulated vsize (Kb) 283488

[startup+880.107 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 59518 0 0 0 87432 271 0 0 25 0 1 0 1797769389 288432128 58246 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31836/statm): 70418 58246 145 145 0 70273 0
[pid=31836] vsize: 281672
Current children cumulated CPU time (s) 877.05
Current children cumulated vsize (Kb) 283796

[startup+890.107 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 59631 0 0 0 88430 272 0 0 25 0 1 0 1797769389 288899072 58359 4294967295 134512640 135094434 3221224432 3221223168 134559634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31836/statm): 70532 58359 145 145 0 70387 0
[pid=31836] vsize: 282128
Current children cumulated CPU time (s) 887.04
Current children cumulated vsize (Kb) 284252

[startup+900.108 s]
Raw data (loadavg): 1.00 1.00 0.95 3/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 59738 0 0 0 89428 274 0 0 25 0 1 0 1797769389 289333248 58466 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 70638 58466 145 145 0 70493 0
[pid=31836] vsize: 282552
Current children cumulated CPU time (s) 897.04
Current children cumulated vsize (Kb) 284676

[startup+910.111 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 59842 0 0 0 90426 275 0 0 25 0 1 0 1797769389 289759232 58570 4294967295 134512640 135094434 3221224432 3221223076 134558040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 70742 58570 145 145 0 70597 0
[pid=31836] vsize: 282968
Current children cumulated CPU time (s) 907.03
Current children cumulated vsize (Kb) 285092

[startup+920.112 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 59913 0 0 0 91425 276 0 0 25 0 1 0 1797769389 290045952 58641 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 70812 58641 145 145 0 70667 0
[pid=31836] vsize: 283248
Current children cumulated CPU time (s) 917.03
Current children cumulated vsize (Kb) 285372

[startup+930.113 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 59921 0 0 0 92425 276 0 0 25 0 1 0 1797769389 290078720 58649 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 70820 58649 145 145 0 70675 0
[pid=31836] vsize: 283280
Current children cumulated CPU time (s) 927.03
Current children cumulated vsize (Kb) 285404

[startup+940.113 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 59992 0 0 0 93424 276 0 0 25 0 1 0 1797769389 290365440 58720 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 70890 58720 145 145 0 70745 0
[pid=31836] vsize: 283560
Current children cumulated CPU time (s) 937.02
Current children cumulated vsize (Kb) 285684

[startup+950.114 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 60106 0 0 0 94422 277 0 0 25 0 1 0 1797769389 290828288 58834 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 71003 58834 145 145 0 70858 0
[pid=31836] vsize: 284012
Current children cumulated CPU time (s) 947.01
Current children cumulated vsize (Kb) 286136

[startup+960.115 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 60183 0 0 0 95421 278 0 0 25 0 1 0 1797769389 291139584 58911 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 71079 58911 145 145 0 70934 0
[pid=31836] vsize: 284316
Current children cumulated CPU time (s) 957.01
Current children cumulated vsize (Kb) 286440

[startup+970.116 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 60265 0 0 0 96420 278 0 0 25 0 1 0 1797769389 291471360 58993 4294967295 134512640 135094434 3221224432 3221223120 134554751 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 71160 58993 145 145 0 71015 0
[pid=31836] vsize: 284640
Current children cumulated CPU time (s) 967
Current children cumulated vsize (Kb) 286764

[startup+980.117 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 60312 0 0 0 97419 279 0 0 25 0 1 0 1797769389 291663872 59040 4294967295 134512640 135094434 3221224432 3221223072 134562108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 71207 59040 145 145 0 71062 0
[pid=31836] vsize: 284828
Current children cumulated CPU time (s) 977
Current children cumulated vsize (Kb) 286952

[startup+990.118 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 60335 0 0 0 98419 279 0 0 25 0 1 0 1797769389 291758080 59063 4294967295 134512640 135094434 3221224432 3221223072 134562098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/31836/statm): 71230 59063 145 145 0 71085 0
[pid=31836] vsize: 284920
Current children cumulated CPU time (s) 987
Current children cumulated vsize (Kb) 287044

[startup+1000.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 60394 0 0 0 99417 280 0 0 25 0 1 0 1797769389 291995648 59122 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 71288 59122 145 145 0 71143 0
[pid=31836] vsize: 285152
Current children cumulated CPU time (s) 996.99
Current children cumulated vsize (Kb) 287276

[startup+1010.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 60420 0 0 0 100417 280 0 0 25 0 1 0 1797769389 292102144 59148 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 71314 59148 145 145 0 71169 0
[pid=31836] vsize: 285256
Current children cumulated CPU time (s) 1006.99
Current children cumulated vsize (Kb) 287380

[startup+1020.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 60453 0 0 0 101416 280 0 0 25 0 1 0 1797769389 292233216 59181 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 71346 59181 145 145 0 71201 0
[pid=31836] vsize: 285384
Current children cumulated CPU time (s) 1016.98
Current children cumulated vsize (Kb) 287508

[startup+1030.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 60503 0 0 0 102416 281 0 0 25 0 1 0 1797769389 292433920 59231 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 71395 59231 145 145 0 71250 0
[pid=31836] vsize: 285580
Current children cumulated CPU time (s) 1026.99
Current children cumulated vsize (Kb) 287704

[startup+1040.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 60555 0 0 0 103414 281 0 0 25 0 1 0 1797769389 292646912 59283 4294967295 134512640 135094434 3221224432 3221223088 134558405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 71447 59283 145 145 0 71302 0
[pid=31836] vsize: 285788
Current children cumulated CPU time (s) 1036.97
Current children cumulated vsize (Kb) 287912

[startup+1050.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 60602 0 0 0 104413 282 0 0 25 0 1 0 1797769389 292835328 59330 4294967295 134512640 135094434 3221224432 3221223120 134558987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 71493 59330 145 145 0 71348 0
[pid=31836] vsize: 285972
Current children cumulated CPU time (s) 1046.97
Current children cumulated vsize (Kb) 288096

[startup+1060.12 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 60650 0 0 0 105413 282 0 0 25 0 1 0 1797769389 293031936 59378 4294967295 134512640 135094434 3221224432 3221223128 134558980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 71541 59378 145 145 0 71396 0
[pid=31836] vsize: 286164
Current children cumulated CPU time (s) 1056.97
Current children cumulated vsize (Kb) 288288

[startup+1070.13 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 60684 0 0 0 106412 282 0 0 25 0 1 0 1797769389 293167104 59412 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 71574 59412 145 145 0 71429 0
[pid=31836] vsize: 286296
Current children cumulated CPU time (s) 1066.96
Current children cumulated vsize (Kb) 288420

[startup+1080.13 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 60735 0 0 0 107411 283 0 0 25 0 1 0 1797769389 293376000 59463 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 71625 59463 145 145 0 71480 0
[pid=31836] vsize: 286500
Current children cumulated CPU time (s) 1076.96
Current children cumulated vsize (Kb) 288624

[startup+1090.13 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 60806 0 0 0 108411 283 0 0 25 0 1 0 1797769389 293662720 59534 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 71695 59534 145 145 0 71550 0
[pid=31836] vsize: 286780
Current children cumulated CPU time (s) 1086.96
Current children cumulated vsize (Kb) 288904

[startup+1100.13 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 60846 0 0 0 109410 283 0 0 25 0 1 0 1797769389 293826560 59574 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 71735 59574 145 145 0 71590 0
[pid=31836] vsize: 286940
Current children cumulated CPU time (s) 1096.95
Current children cumulated vsize (Kb) 289064

[startup+1110.13 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 60905 0 0 0 110409 284 0 0 25 0 1 0 1797769389 294064128 59633 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 71793 59633 145 145 0 71648 0
[pid=31836] vsize: 287172
Current children cumulated CPU time (s) 1106.95
Current children cumulated vsize (Kb) 289296

[startup+1120.13 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 60940 0 0 0 111409 284 0 0 25 0 1 0 1797769389 294469632 59668 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 71892 59668 145 145 0 71747 0
[pid=31836] vsize: 287568
Current children cumulated CPU time (s) 1116.95
Current children cumulated vsize (Kb) 289692

[startup+1130.13 s]
Raw data (loadavg): 1.00 1.00 0.95 3/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 60992 0 0 0 112408 285 0 0 25 0 1 0 1797769389 294678528 59720 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 71943 59720 145 145 0 71798 0
[pid=31836] vsize: 287772
Current children cumulated CPU time (s) 1126.95
Current children cumulated vsize (Kb) 289896

[startup+1140.13 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 61056 0 0 0 113408 285 0 0 25 0 1 0 1797769389 294936576 59784 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 72006 59784 145 145 0 71861 0
[pid=31836] vsize: 288024
Current children cumulated CPU time (s) 1136.95
Current children cumulated vsize (Kb) 290148

[startup+1150.13 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 61101 0 0 0 114407 286 0 0 25 0 1 0 1797769389 295120896 59829 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 72051 59829 145 145 0 71906 0
[pid=31836] vsize: 288204
Current children cumulated CPU time (s) 1146.95
Current children cumulated vsize (Kb) 290328

[startup+1160.13 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 61177 0 0 0 115406 287 0 0 25 0 1 0 1797769389 295428096 59905 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 72126 59905 145 145 0 71981 0
[pid=31836] vsize: 288504
Current children cumulated CPU time (s) 1156.95
Current children cumulated vsize (Kb) 290628

[startup+1170.13 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 61237 0 0 0 116404 287 0 0 25 0 1 0 1797769389 295673856 59965 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 72186 59965 145 145 0 72041 0
[pid=31836] vsize: 288744
Current children cumulated CPU time (s) 1166.93
Current children cumulated vsize (Kb) 290868

[startup+1180.13 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 61311 0 0 0 117403 288 0 0 25 0 1 0 1797769389 295972864 60039 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 72259 60039 145 145 0 72114 0
[pid=31836] vsize: 289036
Current children cumulated CPU time (s) 1176.93
Current children cumulated vsize (Kb) 291160

[startup+1190.13 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 61369 0 0 0 118402 288 0 0 25 0 1 0 1797769389 296210432 60097 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 72317 60097 145 145 0 72172 0
[pid=31836] vsize: 289268
Current children cumulated CPU time (s) 1186.92
Current children cumulated vsize (Kb) 291392

[startup+1200.14 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 61418 0 0 0 119402 288 0 0 25 0 1 0 1797769389 296407040 60146 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 72365 60146 145 145 0 72220 0
[pid=31836] vsize: 289460
Current children cumulated CPU time (s) 1196.92
Current children cumulated vsize (Kb) 291584

[startup+1210.14 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 61485 0 0 0 120401 288 0 0 25 0 1 0 1797769389 296681472 60213 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 72432 60213 145 145 0 72287 0
[pid=31836] vsize: 289728
Current children cumulated CPU time (s) 1206.91
Current children cumulated vsize (Kb) 291852



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.14 s]
Raw data (loadavg): 1.00 1.00 0.95 2/57 31836
Raw data (/proc/31832/stat): 31832 (minisat+_script) S 31831 31832 31778 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1797769385 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/31832/statm): 531 226 485 147 0 384 0
[pid=31832] vsize: 2124
Raw data (/proc/31836/stat): 31836 (minisat+_64-bit) R 31832 31832 31778 0 -1 0 61485 0 0 0 120401 288 0 0 25 0 1 0 1797769389 296681472 60213 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31836/statm): 72432 60213 145 145 0 72287 0
[pid=31836] vsize: 289728
Current children cumulated CPU time (s) 1206.91
Current children cumulated vsize (Kb) 291852

Sending SIGTERM to -31832
Sleeping 2 seconds
One traced child (pid=31832) ended because it received signal 15 (SIGTERM)
One traced child (pid=31836) exited with status: 0
All traced children have exited ! Game is over.

Child status: 0
Real time (s): 1210.26
CPU time (s): 1207.02
CPU user time (s): 1204.02
CPU system time (s): 3.00654
CPU usage (%): 99.7326
Max. virtual memory (cumulated for all children) (Kb): 291852

Verifier Data

ERROR: no interpretation found !