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-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-neos6.opb
MD5SUM6975fcd4cac18749e2635ee3bd162046
Bench Categoryoptimization, big integers (OPTBIGINT)
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 6690
Biggest coefficient in the objective function 536870912
Number of bits for the biggest coefficient in the objective function 30
Sum of the numbers in the objective function 239444426529
Number of bits of the sum of numbers in the objective function 38
Biggest number in a constraint 536870912
Number of bits of the biggest number in a constraint 30
Biggest sum of numbers in a constraint 239444426529
Number of bits of the biggest sum of numbers38
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables21720
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 constraint840

Trace number 5901

Launcher Data

LAUNCH ON wulflinc23 THE 2005-09-20 01:45:23 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3075 boxname=wulflinc23 idbench=731 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6975fcd4cac18749e2635ee3bd162046  /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-neos6.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-neos6.opb
IDLAUNCH: 3075
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        924108 kB
Buffers:          5308 kB
Cached:          77332 kB
SwapCached:        796 kB
Active:          23760 kB
Inactive:        61468 kB
HighTotal:      131008 kB
HighFree:        50400 kB
LowTotal:       903652 kB
LowFree:        873708 kB
SwapTotal:     2097136 kB
SwapFree:      2095788 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5552 kB
Slab:            19480 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 02:05:34 (client local time) WITH STATUS 0 IN 1206.39 SECONDS
stats: 3075 7 1206.39 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]---> Sorter-cost: 2317     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[1022]---> Adder-cost: 308   maxlim: 1073859583   bits: 32/31
c ---[1020]---> Adder-cost: 368   maxlim: 1073921023   bits: 32/31
c ---[1018]---> Adder-cost: 432   maxlim: 1073982463   bits: 32/31
c ---[1016]---> Adder-cost: 496   maxlim: 1074043903   bits: 32/31
c ---[1014]---> Adder-cost: 544   maxlim: 1074104319   bits: 32/31
c ---[1012]---> Adder-cost: 582   maxlim: 1074165759   bits: 32/31
c ---[1010]---> Adder-cost: 650   maxlim: 1074227199   bits: 32/31
c ---[1008]---> Adder-cost: 792   maxlim: 1074278399   bits: 32/31
c ---[1006]---> Adder-cost: 852   maxlim: 1074329599   bits: 32/31
c ---[1004]---> Adder-cost: 908   maxlim: 1074372607   bits: 32/31
c ---[1002]---> Adder-cost: 998   maxlim: 1074413567   bits: 32/31
c ---[1000]---> Adder-cost: 1058   maxlim: 1074444287   bits: 32/31
c ---[ 998]---> Adder-cost: 1130   maxlim: 1074475007   bits: 32/31
c ---[ 996]---> Adder-cost: 1104   maxlim: 1074495487   bits: 32/31
c ---[ 994]---> Adder-cost: 1174   maxlim: 1074513919   bits: 32/31
c ---[ 992]---> Adder-cost: 1144   maxlim: 1074524159   bits: 32/31
c ---[ 990]---> Adder-cost: 1170   maxlim: 1074534399   bits: 32/31
c ---[ 988]---> Adder-cost: 1246   maxlim: 1074524159   bits: 32/31
c ---[ 986]---> Adder-cost: 1162   maxlim: 1074516991   bits: 32/31
c ---[ 984]---> Adder-cost: 1242   maxlim: 1074496511   bits: 32/31
c ---[ 982]---> Adder-cost: 1230   maxlim: 1074476031   bits: 32/31
c ---[ 980]---> Adder-cost: 1178   maxlim: 1074445311   bits: 32/31
c ---[ 978]---> Adder-cost: 1144   maxlim: 1074412543   bits: 32/31
c ---[ 976]---> Adder-cost: 1094   maxlim: 1074371583   bits: 32/31
c ---[ 974]---> Adder-cost: 1010   maxlim: 1074330623   bits: 32/31
c ---[ 972]---> Adder-cost: 986   maxlim: 1074281471   bits: 32/31
c ---[ 970]---> Adder-cost: 882   maxlim: 1074230271   bits: 32/31
c ---[ 968]---> Adder-cost: 790   maxlim: 1074168831   bits: 32/31
c ---[ 966]---> Adder-cost: 670   maxlim: 1074107391   bits: 32/31
c ---[ 964]---> Adder-cost: 604   maxlim: 1074045951   bits: 32/31
c ---[ 962]---> Adder-cost: 520   maxlim: 1073981439   bits: 32/31
c ---[ 960]---> Adder-cost: 414   maxlim: 1073919999   bits: 32/31
c ---[ 958]---> Adder-cost: 318   maxlim: 1073862655   bits: 32/31
c ---[ 956]---> Sorter-cost: 2316     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 954]---> Sorter-cost: 2317     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 952]---> Adder-cost: 328   maxlim: 1073859583   bits: 32/31
c ---[ 950]---> Adder-cost: 382   maxlim: 1073921023   bits: 32/31
c ---[ 948]---> Adder-cost: 450   maxlim: 1073982463   bits: 32/31
c ---[ 946]---> Adder-cost: 522   maxlim: 1074043903   bits: 32/31
c ---[ 944]---> Adder-cost: 578   maxlim: 1074106367   bits: 32/31
c ---[ 942]---> Adder-cost: 628   maxlim: 1074167807   bits: 32/31
c ---[ 940]---> Adder-cost: 682   maxlim: 1074229247   bits: 32/31
c ---[ 938]---> Adder-cost: 962   maxlim: 1074280447   bits: 32/31
c ---[ 936]---> Adder-cost: 1060   maxlim: 1074331647   bits: 32/31
c ---[ 934]---> Adder-cost: 976   maxlim: 1074372607   bits: 32/31
c ---[ 932]---> Adder-cost: 1018   maxlim: 1074413567   bits: 32/31
c ---[ 930]---> Adder-cost: 1114   maxlim: 1074444287   bits: 32/31
c ---[ 928]---> Adder-cost: 1138   maxlim: 1074476031   bits: 32/31
c ---[ 926]---> Adder-cost: 1130   maxlim: 1074496511   bits: 32/31
c ---[ 924]---> Adder-cost: 1134   maxlim: 1074513919   bits: 32/31
c ---[ 922]---> Adder-cost: 1184   maxlim: 1074524159   bits: 32/31
c ---[ 920]---> Adder-cost: 1208   maxlim: 1074534399   bits: 32/31
c ---[ 918]---> Adder-cost: 1198   maxlim: 1074524159   bits: 32/31
c ---[ 916]---> Adder-cost: 1218   maxlim: 1074516991   bits: 32/31
c ---[ 914]---> Adder-cost: 1220   maxlim: 1074496511   bits: 32/31
c ---[ 912]---> Adder-cost: 1236   maxlim: 1074476031   bits: 32/31
c ---[ 910]---> Adder-cost: 1194   maxlim: 1074445311   bits: 32/31
c ---[ 908]---> Adder-cost: 1144   maxlim: 1074412543   bits: 32/31
c ---[ 906]---> Adder-cost: 1088   maxlim: 1074371583   bits: 32/31
c ---[ 904]---> Adder-cost: 1016   maxlim: 1074330623   bits: 32/31
c ---[ 902]---> Adder-cost: 974   maxlim: 1074281471   bits: 32/31
c ---[ 900]---> Adder-cost: 882   maxlim: 1074230271   bits: 32/31
c ---[ 898]---> Adder-cost: 792   maxlim: 1074168831   bits: 32/31
c ---[ 896]---> Adder-cost: 672   maxlim: 1074107391   bits: 32/31
c ---[ 894]---> Adder-cost: 620   maxlim: 1074045951   bits: 32/31
c ---[ 892]---> Adder-cost: 540   maxlim: 1073981439   bits: 32/31
c ---[ 890]---> Adder-cost: 408   maxlim: 1073919999   bits: 32/31
c ---[ 888]---> Adder-cost: 318   maxlim: 1073862655   bits: 32/31
c ---[ 886]---> Sorter-cost: 2316     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 884]---> Sorter-cost: 2317     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 882]---> Adder-cost: 328   maxlim: 1073859583   bits: 32/31
c ---[ 880]---> Adder-cost: 382   maxlim: 1073921023   bits: 32/31
c ---[ 878]---> Adder-cost: 440   maxlim: 1073982463   bits: 32/31
c ---[ 876]---> Adder-cost: 512   maxlim: 1074043903   bits: 32/31
c ---[ 874]---> Adder-cost: 584   maxlim: 1074105343   bits: 32/31
c ---[ 872]---> Adder-cost: 600   maxlim: 1074167807   bits: 32/31
c ---[ 870]---> Adder-cost: 680   maxlim: 1074229247   bits: 32/31
c ---[ 868]---> Adder-cost: 902   maxlim: 1074281471   bits: 32/31
c ---[ 866]---> Adder-cost: 924   maxlim: 1074332671   bits: 32/31
c ---[ 864]---> Adder-cost: 916   maxlim: 1074373631   bits: 32/31
c ---[ 862]---> Adder-cost: 978   maxlim: 1074414591   bits: 32/31
c ---[ 860]---> Adder-cost: 1016   maxlim: 1074442239   bits: 32/31
c ---[ 858]---> Adder-cost: 1032   maxlim: 1074472959   bits: 32/31
c ---[ 856]---> Adder-cost: 1070   maxlim: 1074493439   bits: 32/31
c ---[ 854]---> Adder-cost: 1084   maxlim: 1074513919   bits: 32/31
c ---[ 852]---> Adder-cost: 1120   maxlim: 1074524159   bits: 32/31
c ---[ 850]---> Adder-cost: 1140   maxlim: 1074534399   bits: 32/31
c ---[ 848]---> Adder-cost: 1160   maxlim: 1074524159   bits: 32/31
c ---[ 846]---> Adder-cost: 1150   maxlim: 1074513919   bits: 32/31
c ---[ 844]---> Adder-cost: 1174   maxlim: 1074494463   bits: 32/31
c ---[ 842]---> Adder-cost: 1140   maxlim: 1074473983   bits: 32/31
c ---[ 840]---> Adder-cost: 1154   maxlim: 1074443263   bits: 32/31
c ---[ 838]---> Adder-cost: 1144   maxlim: 1074412543   bits: 32/31
c ---[ 836]---> Adder-cost: 1086   maxlim: 1074371583   bits: 32/31
c ---[ 834]---> Adder-cost: 1046   maxlim: 1074330623   bits: 32/31
c ---[ 832]---> Adder-cost: 954   maxlim: 1074281471   bits: 32/31
c ---[ 830]---> Adder-cost: 880   maxlim: 1074230271   bits: 32/31
c ---[ 828]---> Adder-cost: 796   maxlim: 1074168831   bits: 32/31
c ---[ 826]---> Adder-cost: 724   maxlim: 1074107391   bits: 32/31
c ---[ 824]---> Adder-cost: 620   maxlim: 1074045951   bits: 32/31
c ---[ 822]---> Adder-cost: 510   maxlim: 1073981439   bits: 32/31
c ---[ 820]---> Adder-cost: 422   maxlim: 1073919999   bits: 32/31
c ---[ 818]---> Adder-cost: 318   maxlim: 1073862655   bits: 32/31
c ---[ 816]---> Sorter-cost: 2316     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 814]---> Sorter-cost: 2317     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 812]---> Adder-cost: 328   maxlim: 1073859583   bits: 32/31
c ---[ 810]---> Adder-cost: 384   maxlim: 1073921023   bits: 32/31
c ---[ 808]---> Adder-cost: 456   maxlim: 1073982463   bits: 32/31
c ---[ 806]---> Adder-cost: 520   maxlim: 1074043903   bits: 32/31
c ---[ 804]---> Adder-cost: 604   maxlim: 1074106367   bits: 32/31
c ---[ 802]---> Adder-cost: 658   maxlim: 1074167807   bits: 32/31
c ---[ 800]---> Adder-cost: 692   maxlim: 1074229247   bits: 32/31
c ---[ 798]---> Adder-cost: 1034   maxlim: 1074280447   bits: 32/31
c ---[ 796]---> Adder-cost: 1000   maxlim: 1074331647   bits: 32/31
c ---[ 794]---> Adder-cost: 1118   maxlim: 1074372607   bits: 32/31
c ---[ 792]---> Adder-cost: 1122   maxlim: 1074413567   bits: 32/31
c ---[ 790]---> Adder-cost: 1184   maxlim: 1074444287   bits: 32/31
c ---[ 788]---> Adder-cost: 1192   maxlim: 1074476031   bits: 32/31
c ---[ 786]---> Adder-cost: 1270   maxlim: 1074496511   bits: 32/31
c ---[ 784]---> Adder-cost: 1368   maxlim: 1074516991   bits: 32/31
c ---[ 782]---> Adder-cost: 1254   maxlim: 1074527231   bits: 32/31
c ---[ 780]---> Adder-cost: 1392   maxlim: 1074537471   bits: 32/31
c ---[ 778]---> Adder-cost: 1328   maxlim: 1074527231   bits: 32/31
c ---[ 776]---> Adder-cost: 1304   maxlim: 1074516991   bits: 32/31
c ---[ 774]---> Adder-cost: 1276   maxlim: 1074496511   bits: 32/31
c ---[ 772]---> Adder-cost: 1260   maxlim: 1074476031   bits: 32/31
c ---[ 770]---> Adder-cost: 1182   maxlim: 1074445311   bits: 32/31
c ---[ 768]---> Adder-cost: 1156   maxlim: 1074412543   bits: 32/31
c ---[ 766]---> Adder-cost: 1098   maxlim: 1074371583   bits: 32/31
c ---[ 764]---> Adder-cost: 1072   maxlim: 1074330623   bits: 32/31
c ---[ 762]---> Adder-cost: 966   maxlim: 1074281471   bits: 32/31
c ---[ 760]---> Adder-cost: 892   maxlim: 1074230271   bits: 32/31
c ---[ 758]---> Adder-cost: 788   maxlim: 1074168831   bits: 32/31
c ---[ 756]---> Adder-cost: 676   maxlim: 1074107391   bits: 32/31
c ---[ 754]---> Adder-cost: 594   maxlim: 1074045951   bits: 32/31
c ---[ 752]---> Adder-cost: 528   maxlim: 1073981439   bits: 32/31
c ---[ 750]---> Adder-cost: 412   maxlim: 1073919999   bits: 32/31
c ---[ 748]---> Adder-cost: 318   maxlim: 1073862655   bits: 32/31
c ---[ 746]---> Sorter-cost: 2316     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 744]---> Sorter-cost: 2317     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 742]---> Adder-cost: 328   maxlim: 1073859583   bits: 32/31
c ---[ 740]---> Adder-cost: 386   maxlim: 1073921023   bits: 32/31
c ---[ 738]---> Adder-cost: 450   maxlim: 1073982463   bits: 32/31
c ---[ 736]---> Adder-cost: 524   maxlim: 1074043903   bits: 32/31
c ---[ 734]---> Adder-cost: 584   maxlim: 1074105343   bits: 32/31
c ---[ 732]---> Adder-cost: 662   maxlim: 1074166783   bits: 32/31
c ---[ 730]---> Adder-cost: 692   maxlim: 1074229247   bits: 32/31
c ---[ 728]---> Adder-cost: 976   maxlim: 1074280447   bits: 32/31
c ---[ 726]---> Adder-cost: 1002   maxlim: 1074331647   bits: 32/31
c ---[ 724]---> Adder-cost: 982   maxlim: 1074372607   bits: 32/31
c ---[ 722]---> Adder-cost: 1038   maxlim: 1074413567   bits: 32/31
c ---[ 720]---> Adder-cost: 1120   maxlim: 1074444287   bits: 32/31
c ---[ 718]---> Adder-cost: 1122   maxlim: 1074476031   bits: 32/31
c ---[ 716]---> Adder-cost: 1144   maxlim: 1074496511   bits: 32/31
c ---[ 714]---> Adder-cost: 1106   maxlim: 1074513919   bits: 32/31
c ---[ 712]---> Adder-cost: 1226   maxlim: 1074524159   bits: 32/31
c ---[ 710]---> Adder-cost: 1216   maxlim: 1074534399   bits: 32/31
c ---[ 708]---> Adder-cost: 1234   maxlim: 1074524159   bits: 32/31
c ---[ 706]---> Adder-cost: 1216   maxlim: 1074516991   bits: 32/31
c ---[ 704]---> Adder-cost: 1228   maxlim: 1074496511   bits: 32/31
c ---[ 702]---> Adder-cost: 1246   maxlim: 1074476031   bits: 32/31
c ---[ 700]---> Adder-cost: 1154   maxlim: 1074445311   bits: 32/31
c ---[ 698]---> Adder-cost: 1154   maxlim: 1074412543   bits: 32/31
c ---[ 696]---> Adder-cost: 1116   maxlim: 1074371583   bits: 32/31
c ---[ 694]---> Adder-cost: 1018   maxlim: 1074330623   bits: 32/31
c ---[ 692]---> Adder-cost: 994   maxlim: 1074281471   bits: 32/31
c ---[ 690]---> Adder-cost: 868   maxlim: 1074230271   bits: 32/31
c ---[ 688]---> Adder-cost: 808   maxlim: 1074168831   bits: 32/31
c ---[ 686]---> Adder-cost: 692   maxlim: 1074107391   bits: 32/31
c ---[ 684]---> Adder-cost: 600   maxlim: 1074045951   bits: 32/31
c ---[ 682]---> Adder-cost: 520   maxlim: 1073981439   bits: 32/31
c ---[ 680]---> Adder-cost: 420   maxlim: 1073919999   bits: 32/31
c ---[ 678]---> Adder-cost: 324   maxlim: 1073862655   bits: 32/31
c ---[ 676]---> Sorter-cost: 2316     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 674]---> Sorter-cost: 2316     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 672]---> Adder-cost: 328   maxlim: 1073862655   bits: 32/31
c ---[ 670]---> Adder-cost: 450   maxlim: 1073924095   bits: 32/31
c ---[ 668]---> Adder-cost: 438   maxlim: 1073985535   bits: 32/31
c ---[ 666]---> Adder-cost: 490   maxlim: 1074046975   bits: 32/31
c ---[ 664]---> Adder-cost: 576   maxlim: 1074108415   bits: 32/31
c ---[ 662]---> Adder-cost: 632   maxlim: 1074169855   bits: 32/31
c ---[ 660]---> Adder-cost: 860   maxlim: 1074221055   bits: 32/31
c ---[ 658]---> Adder-cost: 828   maxlim: 1074262015   bits: 32/31
c ---[ 656]---> Adder-cost: 950   maxlim: 1074292735   bits: 32/31
c ---[ 654]---> Adder-cost: 948   maxlim: 1074313215   bits: 32/31
c ---[ 652]---> Adder-cost: 1002   maxlim: 1074323455   bits: 32/31
c ---[ 650]---> Adder-cost: 978   maxlim: 1074323455   bits: 32/31
c ---[ 648]---> Adder-cost: 918   maxlim: 1074313215   bits: 32/31
c ---[ 646]---> Adder-cost: 912   maxlim: 1074292735   bits: 32/31
c ---[ 644]---> Adder-cost: 910   maxlim: 1074262015   bits: 32/31
c ---[ 642]---> Adder-cost: 868   maxlim: 1074221055   bits: 32/31
c ---[ 640]---> Adder-cost: 786   maxlim: 1074169855   bits: 32/31
c ---[ 638]---> Adder-cost: 690   maxlim: 1074108415   bits: 32/31
c ---[ 636]---> Adder-cost: 608   maxlim: 1074046975   bits: 32/31
c ---[ 634]---> Adder-cost: 530   maxlim: 1073985535   bits: 32/31
c ---[ 632]---> Adder-cost: 428   maxlim: 1073924095   bits: 32/31
c ---[ 630]---> Adder-cost: 320   maxlim: 1073862655   bits: 32/31
c ---[ 628]---> Sorter-cost: 2316     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 626]---> Sorter-cost: 2316     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 624]---> Adder-cost: 328   maxlim: 1073862655   bits: 32/31
c ---[ 622]---> Adder-cost: 382   maxlim: 1073924095   bits: 32/31
c ---[ 620]---> Adder-cost: 458   maxlim: 1073985535   bits: 32/31
c ---[ 618]---> Adder-cost: 524   maxlim: 1074046975   bits: 32/31
c ---[ 616]---> Adder-cost: 578   maxlim: 1074108415   bits: 32/31
c ---[ 614]---> Adder-cost: 654   maxlim: 1074169855   bits: 32/31
c ---[ 612]---> Adder-cost: 964   maxlim: 1074221055   bits: 32/31
c ---[ 610]---> Adder-cost: 942   maxlim: 1074262015   bits: 32/31
c ---[ 608]---> Adder-cost: 958   maxlim: 1074292735   bits: 32/31
c ---[ 606]---> Adder-cost: 928   maxlim: 1074313215   bits: 32/31
c ---[ 604]---> Adder-cost: 978   maxlim: 1074323455   bits: 32/31
c ---[ 602]---> Adder-cost: 986   maxlim: 1074322431   bits: 32/31
c ---[ 600]---> Adder-cost: 920   maxlim: 1074312191   bits: 32/31
c ---[ 598]---> Adder-cost: 928   maxlim: 1074291711   bits: 32/31
c ---[ 596]---> Adder-cost: 894   maxlim: 1074260991   bits: 32/31
c ---[ 594]---> Adder-cost: 846   maxlim: 1074220031   bits: 32/31
c ---[ 592]---> Adder-cost: 800   maxlim: 1074168831   bits: 32/31
c ---[ 590]---> Adder-cost: 692   maxlim: 1074107391   bits: 32/31
c ---[ 588]---> Adder-cost: 614   maxlim: 1074045951   bits: 32/31
c ---[ 586]---> Adder-cost: 522   maxlim: 1073984511   bits: 32/31
c ---[ 584]---> Adder-cost: 402   maxlim: 1073923071   bits: 32/31
c ---[ 582]---> Adder-cost: 316   maxlim: 1073861631   bits: 32/31
c ---[ 580]---> Sorter-cost: 2317     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
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 | 2411357  8078600 |  803785       0        0     nan |  0.000 % |
c |       100 | 2411357  8078600 |  884163     100      950     9.5 |  2.852 % |
c |       250 | 2411343  8078558 |  972579     242     3399    14.0 |  2.852 % |
c |       475 | 2411343  8078558 | 1069837     467    15737    33.7 |  2.852 % |
c |       813 | 2411343  8078558 | 1176821     805    29179    36.2 |  2.852 % |
c |      1319 | 2411312  8078465 | 1294503    1281    60674    47.4 |  2.853 % |
c |      2078 | 2411291  8078414 | 1423954    2037   196368    96.4 |  2.854 % |
c |      3218 | 2411270  8078355 | 1566349    3176   407748   128.4 |  2.855 % |
c |      4927 | 2411209  8078210 | 1722984    4880   864118   177.1 |  2.858 % |
c |      7490 | 2410919  8077192 | 1895282    7407  1028001   138.8 |  2.861 % |
c |     11347 | 2410624  8076163 | 2084811   11215  1321257   117.8 |  2.865 % |
c |     17113 | 2410313  8075056 | 2293292   16948  2198764   129.7 |  2.868 % |
c |     25763 | 2409688  8073126 | 2522621   25529  3920391   153.6 |  2.882 % |
c |     38737 | 2409418  8072170 | 2774883   38458  6228731   162.0 |  2.885 % |
c |     58199 | 2408903  8070389 | 3052372   57828 10556214   182.5 |  2.893 % |

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/26388/stat): 26388 (minisat+_script) R 26387 26388 5299 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1854690391 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/26388/statm): 174 3 169 147 0 27 0
[pid=26388] 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=26389
New process pid=26390
New process pid=26391
execve syscall for /bin/sed executable
One traced child (pid=26390) 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=26391) exited with status: 0
One traced child (pid=26389) exited with status: 0
New process pid=26392
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-neos6.opb

[startup+10.0032 s]
Raw data (loadavg): 0.87 0.95 0.94 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 8993 0 0 0 908 46 0 0 25 0 1 0 1854690398 38494208 8312 4294967295 134512640 135094434 3221224432 3221219696 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26392/statm): 9398 8312 145 145 0 9253 0
[pid=26392] vsize: 37592
Current children cumulated CPU time (s) 9.54
Current children cumulated vsize (Kb) 39716

[startup+20.0049 s]
Raw data (loadavg): 0.89 0.95 0.94 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 10563 0 0 0 1903 50 0 0 25 0 1 0 1854690398 41857024 9223 4294967295 134512640 135094434 3221224432 3221220036 134600159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26392/statm): 10219 9223 145 145 0 10074 0
[pid=26392] vsize: 40876
Current children cumulated CPU time (s) 19.53
Current children cumulated vsize (Kb) 43000

[startup+30.0055 s]
Raw data (loadavg): 0.91 0.95 0.94 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 10952 0 0 0 2899 53 0 0 25 0 1 0 1854690398 42848256 9612 4294967295 134512640 135094434 3221224432 3221220400 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 10461 9612 145 145 0 10316 0
[pid=26392] vsize: 41844
Current children cumulated CPU time (s) 29.52
Current children cumulated vsize (Kb) 43968

[startup+40.0081 s]
Raw data (loadavg): 0.92 0.95 0.94 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 11302 0 0 0 3895 54 0 0 25 0 1 0 1854690398 43753472 9962 4294967295 134512640 135094434 3221224432 3221220224 134677307 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26392/statm): 10682 9962 145 145 0 10537 0
[pid=26392] vsize: 42728
Current children cumulated CPU time (s) 39.49
Current children cumulated vsize (Kb) 44852

[startup+50.0098 s]
Raw data (loadavg): 0.93 0.95 0.94 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 11591 0 0 0 4893 55 0 0 25 0 1 0 1854690398 44498944 10251 4294967295 134512640 135094434 3221224432 3221220320 134676317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26392/statm): 10864 10251 145 145 0 10719 0
[pid=26392] vsize: 43456
Current children cumulated CPU time (s) 49.48
Current children cumulated vsize (Kb) 45580

[startup+60.0104 s]
Raw data (loadavg): 0.94 0.95 0.94 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 11786 0 0 0 5890 58 0 0 25 0 1 0 1854690398 44990464 10446 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26392/statm): 10984 10446 145 145 0 10839 0
[pid=26392] vsize: 43936
Current children cumulated CPU time (s) 59.48
Current children cumulated vsize (Kb) 46060

[startup+70.0121 s]
Raw data (loadavg): 0.95 0.95 0.94 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 12168 0 0 0 6887 59 0 0 25 0 1 0 1854690398 52289536 10828 4294967295 134512640 135094434 3221224432 3221223120 134596445 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26392/statm): 12766 10828 145 145 0 12621 0
[pid=26392] vsize: 51064
Current children cumulated CPU time (s) 69.46
Current children cumulated vsize (Kb) 53188

[startup+80.0137 s]
Raw data (loadavg): 0.96 0.95 0.94 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 12557 0 0 0 7884 61 0 0 25 0 1 0 1854690398 53288960 11217 4294967295 134512640 135094434 3221224432 3221219520 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26392/statm): 13010 11217 145 145 0 12865 0
[pid=26392] vsize: 52040
Current children cumulated CPU time (s) 79.45
Current children cumulated vsize (Kb) 54164

[startup+90.0145 s]
Raw data (loadavg): 0.96 0.96 0.94 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 24801 0 0 0 8805 102 0 0 20 0 1 0 1854690398 102653952 22110 4294967295 134512640 135094434 3221224432 3221168912 134553124 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26392/statm): 25062 22110 145 145 0 24917 0
[pid=26392] vsize: 100248
Current children cumulated CPU time (s) 89.07
Current children cumulated vsize (Kb) 102372

[startup+100.015 s]
Raw data (loadavg): 1.04 0.97 0.95 1/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) T 26388 26388 5299 0 -1 0 56712 0 0 0 9518 237 0 0 20 0 1 0 1854690398 266219520 54021 4294967295 134512640 135094434 3221224432 3221222924 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/26392/statm): 64995 54021 145 145 0 64850 0
[pid=26392] vsize: 259980
Current children cumulated CPU time (s) 97.55
Current children cumulated vsize (Kb) 262104

[startup+110.016 s]
Raw data (loadavg): 1.04 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 59401 0 0 0 10487 251 0 0 25 0 1 0 1854690398 276680704 56710 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26392/statm): 67549 56710 145 145 0 67404 0
[pid=26392] vsize: 270196
Current children cumulated CPU time (s) 107.38
Current children cumulated vsize (Kb) 272320

[startup+120.017 s]
Raw data (loadavg): 1.03 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 59450 0 0 0 11485 252 0 0 25 0 1 0 1854690398 276881408 56759 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 67598 56759 145 145 0 67453 0
[pid=26392] vsize: 270392
Current children cumulated CPU time (s) 117.37
Current children cumulated vsize (Kb) 272516

[startup+130.018 s]
Raw data (loadavg): 1.02 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 59587 0 0 0 12483 253 0 0 25 0 1 0 1854690398 277442560 56896 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 67735 56896 145 145 0 67590 0
[pid=26392] vsize: 270940
Current children cumulated CPU time (s) 127.36
Current children cumulated vsize (Kb) 273064

[startup+140.018 s]
Raw data (loadavg): 1.02 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 59717 0 0 0 13480 253 0 0 25 0 1 0 1854690398 277979136 57026 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 67866 57026 145 145 0 67721 0
[pid=26392] vsize: 271464
Current children cumulated CPU time (s) 137.33
Current children cumulated vsize (Kb) 273588

[startup+150.019 s]
Raw data (loadavg): 1.02 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 59847 0 0 0 14478 255 0 0 25 0 1 0 1854690398 278507520 57156 4294967295 134512640 135094434 3221224432 3221223056 134557616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 67995 57156 145 145 0 67850 0
[pid=26392] vsize: 271980
Current children cumulated CPU time (s) 147.33
Current children cumulated vsize (Kb) 274104

[startup+160.02 s]
Raw data (loadavg): 1.01 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) T 26388 26388 5299 0 -1 0 59942 0 0 0 15475 256 0 0 25 0 1 0 1854690398 278896640 57251 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/26392/statm): 68090 57251 145 145 0 67945 0
[pid=26392] vsize: 272360
Current children cumulated CPU time (s) 157.31
Current children cumulated vsize (Kb) 274484

[startup+170.02 s]
Raw data (loadavg): 1.01 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 60118 0 0 0 16472 258 0 0 25 0 1 0 1854690398 279633920 57427 4294967295 134512640 135094434 3221224432 3221223024 134557119 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 68270 57427 145 145 0 68125 0
[pid=26392] vsize: 273080
Current children cumulated CPU time (s) 167.3
Current children cumulated vsize (Kb) 275204

[startup+180.021 s]
Raw data (loadavg): 1.01 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 60290 0 0 0 17468 260 0 0 25 0 1 0 1854690398 280334336 57599 4294967295 134512640 135094434 3221224432 3221223088 134557934 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 68441 57599 145 145 0 68296 0
[pid=26392] vsize: 273764
Current children cumulated CPU time (s) 177.28
Current children cumulated vsize (Kb) 275888

[startup+190.023 s]
Raw data (loadavg): 1.01 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 60428 0 0 0 18464 263 0 0 25 0 1 0 1854690398 280895488 57737 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 68578 57737 145 145 0 68433 0
[pid=26392] vsize: 274312
Current children cumulated CPU time (s) 187.27
Current children cumulated vsize (Kb) 276436

[startup+200.023 s]
Raw data (loadavg): 1.01 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 60491 0 0 0 19463 263 0 0 25 0 1 0 1854690398 281149440 57800 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 68640 57800 145 145 0 68495 0
[pid=26392] vsize: 274560
Current children cumulated CPU time (s) 197.26
Current children cumulated vsize (Kb) 276684

[startup+210.024 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 60526 0 0 0 20462 264 0 0 25 0 1 0 1854690398 281288704 57835 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 68674 57835 145 145 0 68529 0
[pid=26392] vsize: 274696
Current children cumulated CPU time (s) 207.26
Current children cumulated vsize (Kb) 276820

[startup+220.026 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 60552 0 0 0 21462 264 0 0 25 0 1 0 1854690398 281395200 57861 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 68700 57861 145 145 0 68555 0
[pid=26392] vsize: 274800
Current children cumulated CPU time (s) 217.26
Current children cumulated vsize (Kb) 276924

[startup+230.026 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 60636 0 0 0 22460 265 0 0 25 0 1 0 1854690398 281767936 57945 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 68791 57945 145 145 0 68646 0
[pid=26392] vsize: 275164
Current children cumulated CPU time (s) 227.25
Current children cumulated vsize (Kb) 277288

[startup+240.027 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 60735 0 0 0 23459 266 0 0 25 0 1 0 1854690398 282025984 58044 4294967295 134512640 135094434 3221224432 3221223024 134556864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 68854 58044 145 145 0 68709 0
[pid=26392] vsize: 275416
Current children cumulated CPU time (s) 237.25
Current children cumulated vsize (Kb) 277540

[startup+250.028 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 60798 0 0 0 24457 267 0 0 25 0 1 0 1854690398 282284032 58107 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 68917 58107 145 145 0 68772 0
[pid=26392] vsize: 275668
Current children cumulated CPU time (s) 247.24
Current children cumulated vsize (Kb) 277792

[startup+260.028 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 60827 0 0 0 25457 267 0 0 25 0 1 0 1854690398 282398720 58136 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 68945 58136 145 145 0 68800 0
[pid=26392] vsize: 275780
Current children cumulated CPU time (s) 257.24
Current children cumulated vsize (Kb) 277904

[startup+270.029 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 60898 0 0 0 26456 268 0 0 25 0 1 0 1854690398 282685440 58207 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 69015 58207 145 145 0 68870 0
[pid=26392] vsize: 276060
Current children cumulated CPU time (s) 267.24
Current children cumulated vsize (Kb) 278184

[startup+280.029 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 61013 0 0 0 27454 269 0 0 25 0 1 0 1854690398 283062272 58322 4294967295 134512640 135094434 3221224432 3221223092 134553487 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 69107 58322 145 145 0 68962 0
[pid=26392] vsize: 276428
Current children cumulated CPU time (s) 277.23
Current children cumulated vsize (Kb) 278552

[startup+290.031 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 61060 0 0 0 28453 269 0 0 25 0 1 0 1854690398 283250688 58369 4294967295 134512640 135094434 3221224432 3221223088 134557840 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 69153 58369 145 145 0 69008 0
[pid=26392] vsize: 276612
Current children cumulated CPU time (s) 287.22
Current children cumulated vsize (Kb) 278736

[startup+300.032 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 61097 0 0 0 29452 270 0 0 25 0 1 0 1854690398 283402240 58406 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 69190 58406 145 145 0 69045 0
[pid=26392] vsize: 276760
Current children cumulated CPU time (s) 297.22
Current children cumulated vsize (Kb) 278884

[startup+310.032 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 61134 0 0 0 30452 270 0 0 25 0 1 0 1854690398 283549696 58443 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 69226 58443 145 145 0 69081 0
[pid=26392] vsize: 276904
Current children cumulated CPU time (s) 307.22
Current children cumulated vsize (Kb) 279028

[startup+320.034 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 61200 0 0 0 31452 270 0 0 25 0 1 0 1854690398 283815936 58509 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 69291 58509 145 145 0 69146 0
[pid=26392] vsize: 277164
Current children cumulated CPU time (s) 317.22
Current children cumulated vsize (Kb) 279288

[startup+330.035 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 61330 0 0 0 32449 271 0 0 25 0 1 0 1854690398 284348416 58639 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 69421 58639 145 145 0 69276 0
[pid=26392] vsize: 277684
Current children cumulated CPU time (s) 327.2
Current children cumulated vsize (Kb) 279808

[startup+340.036 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 61523 0 0 0 33447 272 0 0 25 0 1 0 1854690398 285134848 58832 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 69613 58832 145 145 0 69468 0
[pid=26392] vsize: 278452
Current children cumulated CPU time (s) 337.19
Current children cumulated vsize (Kb) 280576

[startup+350.037 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 61743 0 0 0 34443 274 0 0 25 0 1 0 1854690398 286035968 59052 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 69833 59052 145 145 0 69688 0
[pid=26392] vsize: 279332
Current children cumulated CPU time (s) 347.17
Current children cumulated vsize (Kb) 281456

[startup+360.038 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 61880 0 0 0 35441 274 0 0 25 0 1 0 1854690398 286597120 59189 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 69970 59189 145 145 0 69825 0
[pid=26392] vsize: 279880
Current children cumulated CPU time (s) 357.15
Current children cumulated vsize (Kb) 282004

[startup+370.038 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 61939 0 0 0 36439 275 0 0 25 0 1 0 1854690398 286900224 59248 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 70044 59248 145 145 0 69899 0
[pid=26392] vsize: 280176
Current children cumulated CPU time (s) 367.14
Current children cumulated vsize (Kb) 282300

[startup+380.039 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 62001 0 0 0 37439 276 0 0 25 0 1 0 1854690398 287150080 59310 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 70105 59310 145 145 0 69960 0
[pid=26392] vsize: 280420
Current children cumulated CPU time (s) 377.15
Current children cumulated vsize (Kb) 282544

[startup+390.041 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 62087 0 0 0 38437 276 0 0 25 0 1 0 1854690398 287502336 59396 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 70191 59396 145 145 0 70046 0
[pid=26392] vsize: 280764
Current children cumulated CPU time (s) 387.13
Current children cumulated vsize (Kb) 282888

[startup+400.041 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 62128 0 0 0 39437 276 0 0 25 0 1 0 1854690398 287666176 59437 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 70231 59437 145 145 0 70086 0
[pid=26392] vsize: 280924
Current children cumulated CPU time (s) 397.13
Current children cumulated vsize (Kb) 283048

[startup+410.042 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 62209 0 0 0 40435 277 0 0 25 0 1 0 1854690398 287997952 59518 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 70312 59518 145 145 0 70167 0
[pid=26392] vsize: 281248
Current children cumulated CPU time (s) 407.12
Current children cumulated vsize (Kb) 283372

[startup+420.042 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 62344 0 0 0 41433 278 0 0 25 0 1 0 1854690398 288546816 59653 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 70446 59653 145 145 0 70301 0
[pid=26392] vsize: 281784
Current children cumulated CPU time (s) 417.11
Current children cumulated vsize (Kb) 283908

[startup+430.043 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 62458 0 0 0 42431 280 0 0 25 0 1 0 1854690398 289013760 59767 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 70560 59767 145 145 0 70415 0
[pid=26392] vsize: 282240
Current children cumulated CPU time (s) 427.11
Current children cumulated vsize (Kb) 284364

[startup+440.045 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 62624 0 0 0 43427 281 0 0 25 0 1 0 1854690398 289689600 59933 4294967295 134512640 135094434 3221224432 3221223024 134556826 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 70725 59933 145 145 0 70580 0
[pid=26392] vsize: 282900
Current children cumulated CPU time (s) 437.08
Current children cumulated vsize (Kb) 285024

[startup+450.045 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 62775 0 0 0 44424 282 0 0 25 0 1 0 1854690398 290308096 60084 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26392/statm): 70876 60084 145 145 0 70731 0
[pid=26392] vsize: 283504
Current children cumulated CPU time (s) 447.06
Current children cumulated vsize (Kb) 285628

[startup+460.046 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 62913 0 0 0 45422 283 0 0 25 0 1 0 1854690398 290873344 60222 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 71014 60222 145 145 0 70869 0
[pid=26392] vsize: 284056
Current children cumulated CPU time (s) 457.05
Current children cumulated vsize (Kb) 286180

[startup+470.048 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 63051 0 0 0 46420 285 0 0 25 0 1 0 1854690398 291438592 60360 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 71152 60360 145 145 0 71007 0
[pid=26392] vsize: 284608
Current children cumulated CPU time (s) 467.05
Current children cumulated vsize (Kb) 286732

[startup+480.048 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 63180 0 0 0 47417 286 0 0 25 0 1 0 1854690398 291962880 60489 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 71280 60489 145 145 0 71135 0
[pid=26392] vsize: 285120
Current children cumulated CPU time (s) 477.03
Current children cumulated vsize (Kb) 287244

[startup+490.049 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 63314 0 0 0 48415 287 0 0 25 0 1 0 1854690398 292511744 60623 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 71414 60623 145 145 0 71269 0
[pid=26392] vsize: 285656
Current children cumulated CPU time (s) 487.02
Current children cumulated vsize (Kb) 287780

[startup+500.051 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 63391 0 0 0 49414 287 0 0 25 0 1 0 1854690398 292827136 60700 4294967295 134512640 135094434 3221224432 3221223088 134558026 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 71491 60700 145 145 0 71346 0
[pid=26392] vsize: 285964
Current children cumulated CPU time (s) 497.01
Current children cumulated vsize (Kb) 288088

[startup+510.051 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 63442 0 0 0 50413 288 0 0 25 0 1 0 1854690398 293031936 60751 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 71541 60751 145 145 0 71396 0
[pid=26392] vsize: 286164
Current children cumulated CPU time (s) 507.01
Current children cumulated vsize (Kb) 288288

[startup+520.052 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 63491 0 0 0 51413 288 0 0 25 0 1 0 1854690398 293232640 60800 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 71590 60800 145 145 0 71445 0
[pid=26392] vsize: 286360
Current children cumulated CPU time (s) 517.01
Current children cumulated vsize (Kb) 288484

[startup+530.052 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 63545 0 0 0 52412 289 0 0 25 0 1 0 1854690398 293453824 60854 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 71644 60854 145 145 0 71499 0
[pid=26392] vsize: 286576
Current children cumulated CPU time (s) 527.01
Current children cumulated vsize (Kb) 288700

[startup+540.053 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 63612 0 0 0 53411 289 0 0 25 0 1 0 1854690398 293724160 60921 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 71710 60921 145 145 0 71565 0
[pid=26392] vsize: 286840
Current children cumulated CPU time (s) 537
Current children cumulated vsize (Kb) 288964

[startup+550.054 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 63696 0 0 0 54410 290 0 0 25 0 1 0 1854690398 294064128 61005 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 71793 61005 145 145 0 71648 0
[pid=26392] vsize: 287172
Current children cumulated CPU time (s) 547
Current children cumulated vsize (Kb) 289296

[startup+560.054 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 63743 0 0 0 55409 290 0 0 25 0 1 0 1854690398 294256640 61052 4294967295 134512640 135094434 3221224432 3221223092 134553536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 71840 61052 145 145 0 71695 0
[pid=26392] vsize: 287360
Current children cumulated CPU time (s) 556.99
Current children cumulated vsize (Kb) 289484

[startup+570.056 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 63812 0 0 0 56409 290 0 0 25 0 1 0 1854690398 294539264 61121 4294967295 134512640 135094434 3221224432 3221223024 134557004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 71909 61121 145 145 0 71764 0
[pid=26392] vsize: 287636
Current children cumulated CPU time (s) 566.99
Current children cumulated vsize (Kb) 289760

[startup+580.057 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 63876 0 0 0 57407 291 0 0 25 0 1 0 1854690398 294797312 61185 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 71972 61185 145 145 0 71827 0
[pid=26392] vsize: 287888
Current children cumulated CPU time (s) 576.98
Current children cumulated vsize (Kb) 290012

[startup+590.057 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 63966 0 0 0 58405 292 0 0 25 0 1 0 1854690398 295161856 61275 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 72061 61275 145 145 0 71916 0
[pid=26392] vsize: 288244
Current children cumulated CPU time (s) 586.97
Current children cumulated vsize (Kb) 290368

[startup+600.058 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 64050 0 0 0 59403 293 0 0 25 0 1 0 1854690398 295505920 61359 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 72145 61359 145 145 0 72000 0
[pid=26392] vsize: 288580
Current children cumulated CPU time (s) 596.96
Current children cumulated vsize (Kb) 290704

[startup+610.059 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 64141 0 0 0 60402 293 0 0 25 0 1 0 1854690398 295874560 61450 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 72235 61450 145 145 0 72090 0
[pid=26392] vsize: 288940
Current children cumulated CPU time (s) 606.95
Current children cumulated vsize (Kb) 291064

[startup+620.06 s]
Raw data (loadavg): 1.08 0.99 0.95 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 64315 0 0 0 61398 295 0 0 25 0 1 0 1854690398 296587264 61624 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 72409 61624 145 145 0 72264 0
[pid=26392] vsize: 289636
Current children cumulated CPU time (s) 616.93
Current children cumulated vsize (Kb) 291760

[startup+630.061 s]
Raw data (loadavg): 1.14 1.01 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 64563 0 0 0 62395 297 0 0 25 0 1 0 1854690398 297598976 61872 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 72656 61872 145 145 0 72511 0
[pid=26392] vsize: 290624
Current children cumulated CPU time (s) 626.92
Current children cumulated vsize (Kb) 292748

[startup+640.062 s]
Raw data (loadavg): 1.12 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 64840 0 0 0 63390 299 0 0 25 0 1 0 1854690398 298733568 62149 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 72933 62149 145 145 0 72788 0
[pid=26392] vsize: 291732
Current children cumulated CPU time (s) 636.89
Current children cumulated vsize (Kb) 293856

[startup+650.062 s]
Raw data (loadavg): 1.10 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 64915 0 0 0 64388 300 0 0 25 0 1 0 1854690398 299036672 62224 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 73007 62224 145 145 0 72862 0
[pid=26392] vsize: 292028
Current children cumulated CPU time (s) 646.88
Current children cumulated vsize (Kb) 294152

[startup+660.063 s]
Raw data (loadavg): 1.08 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 65043 0 0 0 65386 300 0 0 25 0 1 0 1854690398 299556864 62352 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 73134 62352 145 145 0 72989 0
[pid=26392] vsize: 292536
Current children cumulated CPU time (s) 656.86
Current children cumulated vsize (Kb) 294660

[startup+670.063 s]
Raw data (loadavg): 1.07 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 65171 0 0 0 66384 302 0 0 25 0 1 0 1854690398 300081152 62480 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 73262 62480 145 145 0 73117 0
[pid=26392] vsize: 293048
Current children cumulated CPU time (s) 666.86
Current children cumulated vsize (Kb) 295172

[startup+680.065 s]
Raw data (loadavg): 1.06 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 65258 0 0 0 67383 302 0 0 25 0 1 0 1854690398 300433408 62567 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 73348 62567 145 145 0 73203 0
[pid=26392] vsize: 293392
Current children cumulated CPU time (s) 676.85
Current children cumulated vsize (Kb) 295516

[startup+690.066 s]
Raw data (loadavg): 1.05 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 65357 0 0 0 68381 303 0 0 25 0 1 0 1854690398 300838912 62666 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 73447 62666 145 145 0 73302 0
[pid=26392] vsize: 293788
Current children cumulated CPU time (s) 686.84
Current children cumulated vsize (Kb) 295912

[startup+700.066 s]
Raw data (loadavg): 1.04 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 65437 0 0 0 69380 304 0 0 25 0 1 0 1854690398 301293568 62746 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 73558 62746 145 145 0 73413 0
[pid=26392] vsize: 294232
Current children cumulated CPU time (s) 696.84
Current children cumulated vsize (Kb) 296356

[startup+710.067 s]
Raw data (loadavg): 1.04 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 65539 0 0 0 70379 305 0 0 25 0 1 0 1854690398 301711360 62848 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 73660 62848 145 145 0 73515 0
[pid=26392] vsize: 294640
Current children cumulated CPU time (s) 706.84
Current children cumulated vsize (Kb) 296764

[startup+720.068 s]
Raw data (loadavg): 1.03 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 65624 0 0 0 71377 305 0 0 25 0 1 0 1854690398 302055424 62933 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 73744 62933 145 145 0 73599 0
[pid=26392] vsize: 294976
Current children cumulated CPU time (s) 716.82
Current children cumulated vsize (Kb) 297100

[startup+730.068 s]
Raw data (loadavg): 1.02 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 65697 0 0 0 72376 305 0 0 25 0 1 0 1854690398 302354432 63006 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 73817 63006 145 145 0 73672 0
[pid=26392] vsize: 295268
Current children cumulated CPU time (s) 726.81
Current children cumulated vsize (Kb) 297392

[startup+740.069 s]
Raw data (loadavg): 1.02 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 65782 0 0 0 73374 307 0 0 25 0 1 0 1854690398 302698496 63091 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 73901 63091 145 145 0 73756 0
[pid=26392] vsize: 295604
Current children cumulated CPU time (s) 736.81
Current children cumulated vsize (Kb) 297728

[startup+750.07 s]
Raw data (loadavg): 1.02 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 65875 0 0 0 74373 307 0 0 25 0 1 0 1854690398 303083520 63184 4294967295 134512640 135094434 3221224432 3221223092 134553480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 73995 63184 145 145 0 73850 0
[pid=26392] vsize: 295980
Current children cumulated CPU time (s) 746.8
Current children cumulated vsize (Kb) 298104

[startup+760.07 s]
Raw data (loadavg): 1.01 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 65996 0 0 0 75371 308 0 0 25 0 1 0 1854690398 303575040 63305 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 74115 63305 145 145 0 73970 0
[pid=26392] vsize: 296460
Current children cumulated CPU time (s) 756.79
Current children cumulated vsize (Kb) 298584

[startup+770.071 s]
Raw data (loadavg): 1.01 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 66112 0 0 0 76368 309 0 0 18 0 1 0 1854690398 304046080 63421 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 74230 63421 145 145 0 74085 0
[pid=26392] vsize: 296920
Current children cumulated CPU time (s) 766.77
Current children cumulated vsize (Kb) 299044

[startup+780.072 s]
Raw data (loadavg): 1.01 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 66225 0 0 0 77365 311 0 0 25 0 1 0 1854690398 304504832 63534 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 74342 63534 145 145 0 74197 0
[pid=26392] vsize: 297368
Current children cumulated CPU time (s) 776.76
Current children cumulated vsize (Kb) 299492

[startup+790.072 s]
Raw data (loadavg): 1.01 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 66316 0 0 0 78362 313 0 0 25 0 1 0 1854690398 304877568 63625 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26392/statm): 74433 63625 145 145 0 74288 0
[pid=26392] vsize: 297732
Current children cumulated CPU time (s) 786.75
Current children cumulated vsize (Kb) 299856

[startup+800.074 s]
Raw data (loadavg): 1.01 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 66536 0 0 0 79356 315 0 0 25 0 1 0 1854690398 305774592 63845 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 74652 63845 145 145 0 74507 0
[pid=26392] vsize: 298608
Current children cumulated CPU time (s) 796.71
Current children cumulated vsize (Kb) 300732

[startup+810.074 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 66719 0 0 0 80353 317 0 0 25 0 1 0 1854690398 306524160 64028 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 74835 64028 145 145 0 74690 0
[pid=26392] vsize: 299340
Current children cumulated CPU time (s) 806.7
Current children cumulated vsize (Kb) 301464

[startup+820.075 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 66765 0 0 0 81352 317 0 0 25 0 1 0 1854690398 306712576 64074 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 74881 64074 145 145 0 74736 0
[pid=26392] vsize: 299524
Current children cumulated CPU time (s) 816.69
Current children cumulated vsize (Kb) 301648

[startup+830.076 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 66823 0 0 0 82351 318 0 0 25 0 1 0 1854690398 306946048 64132 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 74938 64132 145 145 0 74793 0
[pid=26392] vsize: 299752
Current children cumulated CPU time (s) 826.69
Current children cumulated vsize (Kb) 301876

[startup+840.076 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 66892 0 0 0 83350 319 0 0 25 0 1 0 1854690398 307228672 64201 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 75007 64201 145 145 0 74862 0
[pid=26392] vsize: 300028
Current children cumulated CPU time (s) 836.69
Current children cumulated vsize (Kb) 302152

[startup+850.077 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 66945 0 0 0 84348 320 0 0 25 0 1 0 1854690398 307441664 64254 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 75059 64254 145 145 0 74914 0
[pid=26392] vsize: 300236
Current children cumulated CPU time (s) 846.68
Current children cumulated vsize (Kb) 302360

[startup+860.078 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 66999 0 0 0 85348 320 0 0 25 0 1 0 1854690398 307662848 64308 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 75113 64308 145 145 0 74968 0
[pid=26392] vsize: 300452
Current children cumulated CPU time (s) 856.68
Current children cumulated vsize (Kb) 302576

[startup+870.079 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 67094 0 0 0 86346 321 0 0 25 0 1 0 1854690398 308047872 64403 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 75207 64403 145 145 0 75062 0
[pid=26392] vsize: 300828
Current children cumulated CPU time (s) 866.67
Current children cumulated vsize (Kb) 302952

[startup+880.08 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 67241 0 0 0 87343 322 0 0 25 0 1 0 1854690398 308645888 64550 4294967295 134512640 135094434 3221224432 3221223124 134558984 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 75353 64550 145 145 0 75208 0
[pid=26392] vsize: 301412
Current children cumulated CPU time (s) 876.65
Current children cumulated vsize (Kb) 303536

[startup+890.081 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 67264 0 0 0 88343 322 0 0 25 0 1 0 1854690398 308740096 64573 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 75376 64573 145 145 0 75231 0
[pid=26392] vsize: 301504
Current children cumulated CPU time (s) 886.65
Current children cumulated vsize (Kb) 303628

[startup+900.082 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 67398 0 0 0 89340 324 0 0 25 0 1 0 1854690398 309288960 64707 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 75510 64707 145 145 0 75365 0
[pid=26392] vsize: 302040
Current children cumulated CPU time (s) 896.64
Current children cumulated vsize (Kb) 304164

[startup+910.083 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 67536 0 0 0 90338 325 0 0 25 0 1 0 1854690398 309850112 64845 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 75647 64845 145 145 0 75502 0
[pid=26392] vsize: 302588
Current children cumulated CPU time (s) 906.63
Current children cumulated vsize (Kb) 304712

[startup+920.084 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 67672 0 0 0 91336 326 0 0 25 0 1 0 1854690398 310407168 64981 4294967295 134512640 135094434 3221224432 3221223088 134557903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 75783 64981 145 145 0 75638 0
[pid=26392] vsize: 303132
Current children cumulated CPU time (s) 916.62
Current children cumulated vsize (Kb) 305256

[startup+930.085 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 67809 0 0 0 92333 327 0 0 25 0 1 0 1854690398 310964224 65118 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 75919 65118 145 145 0 75774 0
[pid=26392] vsize: 303676
Current children cumulated CPU time (s) 926.6
Current children cumulated vsize (Kb) 305800

[startup+940.086 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 67958 0 0 0 93330 329 0 0 25 0 1 0 1854690398 311574528 65267 4294967295 134512640 135094434 3221224432 3221223024 134556809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 76068 65267 145 145 0 75923 0
[pid=26392] vsize: 304272
Current children cumulated CPU time (s) 936.59
Current children cumulated vsize (Kb) 306396

[startup+950.086 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 68121 0 0 0 94328 330 0 0 25 0 1 0 1854690398 312238080 65430 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 76230 65430 145 145 0 76085 0
[pid=26392] vsize: 304920
Current children cumulated CPU time (s) 946.58
Current children cumulated vsize (Kb) 307044

[startup+960.087 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 68287 0 0 0 95325 332 0 0 25 0 1 0 1854690398 312918016 65596 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 76396 65596 145 145 0 76251 0
[pid=26392] vsize: 305584
Current children cumulated CPU time (s) 956.57
Current children cumulated vsize (Kb) 307708

[startup+970.088 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 68426 0 0 0 96322 333 0 0 25 0 1 0 1854690398 313483264 65735 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 76534 65735 145 145 0 76389 0
[pid=26392] vsize: 306136
Current children cumulated CPU time (s) 966.55
Current children cumulated vsize (Kb) 308260

[startup+980.088 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 68591 0 0 0 97319 335 0 0 25 0 1 0 1854690398 314159104 65900 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 76699 65900 145 145 0 76554 0
[pid=26392] vsize: 306796
Current children cumulated CPU time (s) 976.54
Current children cumulated vsize (Kb) 308920

[startup+990.089 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 68745 0 0 0 98316 336 0 0 25 0 1 0 1854690398 314785792 66054 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 76852 66054 145 145 0 76707 0
[pid=26392] vsize: 307408
Current children cumulated CPU time (s) 986.52
Current children cumulated vsize (Kb) 309532

[startup+1000.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 68851 0 0 0 99314 337 0 0 25 0 1 0 1854690398 315219968 66160 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 76958 66160 145 145 0 76813 0
[pid=26392] vsize: 307832
Current children cumulated CPU time (s) 996.51
Current children cumulated vsize (Kb) 309956

[startup+1010.09 s]
Raw data (loadavg): 1.00 1.00 0.96 1/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) T 26388 26388 5299 0 -1 0 69050 0 0 0 100310 338 0 0 25 0 1 0 1854690398 316030976 66359 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/26392/statm): 77156 66359 145 145 0 77011 0
[pid=26392] vsize: 308624
Current children cumulated CPU time (s) 1006.48
Current children cumulated vsize (Kb) 310748

[startup+1020.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 69217 0 0 0 101307 340 0 0 25 0 1 0 1854690398 316710912 66526 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 77322 66526 145 145 0 77177 0
[pid=26392] vsize: 309288
Current children cumulated CPU time (s) 1016.47
Current children cumulated vsize (Kb) 311412

[startup+1030.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 69319 0 0 0 102305 340 0 0 25 0 1 0 1854690398 317124608 66628 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 77423 66628 145 145 0 77278 0
[pid=26392] vsize: 309692
Current children cumulated CPU time (s) 1026.45
Current children cumulated vsize (Kb) 311816

[startup+1040.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 69419 0 0 0 103303 341 0 0 25 0 1 0 1854690398 317534208 66728 4294967295 134512640 135094434 3221224432 3221223120 134554760 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 77523 66728 145 145 0 77378 0
[pid=26392] vsize: 310092
Current children cumulated CPU time (s) 1036.44
Current children cumulated vsize (Kb) 312216

[startup+1050.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 69495 0 0 0 104302 342 0 0 25 0 1 0 1854690398 317841408 66804 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 77598 66804 145 145 0 77453 0
[pid=26392] vsize: 310392
Current children cumulated CPU time (s) 1046.44
Current children cumulated vsize (Kb) 312516

[startup+1060.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 69575 0 0 0 105301 342 0 0 25 0 1 0 1854690398 318169088 66884 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 77678 66884 145 145 0 77533 0
[pid=26392] vsize: 310712
Current children cumulated CPU time (s) 1056.43
Current children cumulated vsize (Kb) 312836

[startup+1070.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 69692 0 0 0 106299 343 0 0 25 0 1 0 1854690398 318644224 67001 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 77794 67001 145 145 0 77649 0
[pid=26392] vsize: 311176
Current children cumulated CPU time (s) 1066.42
Current children cumulated vsize (Kb) 313300

[startup+1080.09 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 69823 0 0 0 107296 345 0 0 25 0 1 0 1854690398 319180800 67132 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 77925 67132 145 145 0 77780 0
[pid=26392] vsize: 311700
Current children cumulated CPU time (s) 1076.41
Current children cumulated vsize (Kb) 313824

[startup+1090.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 69963 0 0 0 108293 347 0 0 25 0 1 0 1854690398 319750144 67272 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 78064 67272 145 145 0 77919 0
[pid=26392] vsize: 312256
Current children cumulated CPU time (s) 1086.4
Current children cumulated vsize (Kb) 314380

[startup+1100.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 70030 0 0 0 109291 347 0 0 25 0 1 0 1854690398 320024576 67339 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 78131 67339 145 145 0 77986 0
[pid=26392] vsize: 312524
Current children cumulated CPU time (s) 1096.38
Current children cumulated vsize (Kb) 314648

[startup+1110.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 70128 0 0 0 110289 349 0 0 25 0 1 0 1854690398 320421888 67437 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 78228 67437 145 145 0 78083 0
[pid=26392] vsize: 312912
Current children cumulated CPU time (s) 1106.38
Current children cumulated vsize (Kb) 315036

[startup+1120.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 70345 0 0 0 111286 350 0 0 25 0 1 0 1854690398 321310720 67654 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 78445 67654 145 145 0 78300 0
[pid=26392] vsize: 313780
Current children cumulated CPU time (s) 1116.36
Current children cumulated vsize (Kb) 315904

[startup+1130.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 70562 0 0 0 112282 352 0 0 25 0 1 0 1854690398 322195456 67871 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 78661 67871 145 145 0 78516 0
[pid=26392] vsize: 314644
Current children cumulated CPU time (s) 1126.34
Current children cumulated vsize (Kb) 316768

[startup+1140.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 70811 0 0 0 113276 355 0 0 25 0 1 0 1854690398 323211264 68120 4294967295 134512640 135094434 3221224432 3221223024 134557248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 78909 68120 145 145 0 78764 0
[pid=26392] vsize: 315636
Current children cumulated CPU time (s) 1136.31
Current children cumulated vsize (Kb) 317760

[startup+1150.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 70956 0 0 0 114273 356 0 0 25 0 1 0 1854690398 323805184 68265 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/26392/statm): 79054 68265 145 145 0 78909 0
[pid=26392] vsize: 316216
Current children cumulated CPU time (s) 1146.29
Current children cumulated vsize (Kb) 318340

[startup+1160.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 71137 0 0 0 115269 357 0 0 21 0 1 0 1854690398 324542464 68446 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 79234 68446 145 145 0 79089 0
[pid=26392] vsize: 316936
Current children cumulated CPU time (s) 1156.26
Current children cumulated vsize (Kb) 319060

[startup+1170.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 71236 0 0 0 116269 358 0 0 25 0 1 0 1854690398 324947968 68545 4294967295 134512640 135094434 3221224432 3221223044 134563071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 79333 68545 145 145 0 79188 0
[pid=26392] vsize: 317332
Current children cumulated CPU time (s) 1166.27
Current children cumulated vsize (Kb) 319456

[startup+1180.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 71268 0 0 0 117268 358 0 0 25 0 1 0 1854690398 325074944 68577 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 79364 68577 145 145 0 79219 0
[pid=26392] vsize: 317456
Current children cumulated CPU time (s) 1176.26
Current children cumulated vsize (Kb) 319580

[startup+1190.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 71305 0 0 0 118267 359 0 0 25 0 1 0 1854690398 325226496 68614 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 79401 68614 145 145 0 79256 0
[pid=26392] vsize: 317604
Current children cumulated CPU time (s) 1186.26
Current children cumulated vsize (Kb) 319728

[startup+1200.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 71393 0 0 0 119265 360 0 0 25 0 1 0 1854690398 325582848 68702 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 79488 68702 145 145 0 79343 0
[pid=26392] vsize: 317952
Current children cumulated CPU time (s) 1196.25
Current children cumulated vsize (Kb) 320076

[startup+1210.1 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 71453 0 0 0 120264 361 0 0 25 0 1 0 1854690398 325828608 68762 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 79548 68762 145 145 0 79403 0
[pid=26392] vsize: 318192
Current children cumulated CPU time (s) 1206.25
Current children cumulated vsize (Kb) 320316



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 1.00 1.00 0.96 2/57 26392
Raw data (/proc/26388/stat): 26388 (minisat+_script) S 26387 26388 5299 0 -1 0 289 239 0 0 0 0 0 0 16 0 1 0 1854690391 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/26388/statm): 531 226 485 147 0 384 0
[pid=26388] vsize: 2124
Raw data (/proc/26392/stat): 26392 (minisat+_64-bit) R 26388 26388 5299 0 -1 0 71453 0 0 0 120264 361 0 0 25 0 1 0 1854690398 325828608 68762 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/26392/statm): 79548 68762 145 145 0 79403 0
[pid=26392] vsize: 318192
Current children cumulated CPU time (s) 1206.25
Current children cumulated vsize (Kb) 320316

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

Child status: 0
Real time (s): 1210.24
CPU time (s): 1206.39
CPU user time (s): 1202.65
CPU system time (s): 3.74543
CPU usage (%): 99.682
Max. virtual memory (cumulated for all children) (Kb): 320316

Verifier Data

ERROR: no interpretation found !