PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-blp-ar98.opb
MD5SUM	53176d06e1e99afe2d28ec1484235311
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	21
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	2097151
Number of bits of the sum of numbers in the objective function	21
Biggest number in a constraint	81920000000
Number of bits of the biggest number in a constraint	37
Biggest sum of numbers in a constraint	40410384871329
Number of bits of the biggest sum of numbers	46
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	6.22305
Number of variables	18824
Total number of constraints	17064
Number of constraints which are clauses	1
Number of constraints which are cardinality constraints (but not clauses)	16718
Number of constraints which are nor clauses,nor cardinality constraints	345
Minimum length of a constraint	1
Maximum length of a constraint	15827
Trace number 31307

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-05-26 00:09:58 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22720 boxname=wulflinc12 idbench=1536 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  53176d06e1e99afe2d28ec1484235311  /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-blp-ar98.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-blp-ar98.opb
IDLAUNCH: 22720
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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:        807276 kB
Buffers:         31272 kB
Cached:         174508 kB
SwapCached:        396 kB
Active:          29816 kB
Inactive:       178192 kB
HighTotal:      131008 kB
HighFree:        57736 kB
LowTotal:       903652 kB
LowFree:        749540 kB
SwapTotal:     2097136 kB
SwapFree:      2096076 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5680 kB
Slab:            13560 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-26 00:20:36 (client local time) WITH STATUS 139 IN 637.578 SECONDS
stats: 22720 7 637.578 139
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1473 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sss.
c ---[1475]---> BDD-cost:    9
c ---[1474]---> BDD-cost:    9
c ---[1473]---> BDD-cost:    9
c ---[1472]---> BDD-cost:   10
c ---[1470]---> BDD-cost:   10
c ---[1469]---> BDD-cost:    9
c ---[1468]---> BDD-cost:   10
c ---[1467]---> BDD-cost:    9
c ---[1466]---> BDD-cost:   10
c ---[1465]---> BDD-cost:   10
c ---[1464]---> BDD-cost:    9
c ---[1463]---> BDD-cost:   10
c ---[1462]---> BDD-cost:   10
c ---[1461]---> BDD-cost:    9
c ---[1460]---> BDD-cost:   10
c ---[1459]---> BDD-cost:   10
c ---[1458]---> BDD-cost:   10
c ---[1457]---> BDD-cost:   10
c ---[1456]---> BDD-cost:   10
c ---[1455]---> BDD-cost:    9
c ---[1454]---> BDD-cost:    8
c ---[1453]---> BDD-cost:    9
c ---[1452]---> BDD-cost:   10
c ---[1451]---> BDD-cost:   10
c ---[1450]---> BDD-cost:   10
c ---[1449]---> BDD-cost:   10
c ---[1448]---> BDD-cost:    9
c ---[1447]---> BDD-cost:   10
c ---[1446]---> BDD-cost:   10
c ---[1445]---> BDD-cost:   10
c ---[1444]---> BDD-cost:   10
c ---[1443]---> BDD-cost:   10
c ---[1442]---> BDD-cost:   10
c ---[1441]---> BDD-cost:   10
c ---[1440]---> BDD-cost:   10
c ---[1439]---> BDD-cost:   10
c ---[1438]---> BDD-cost:   10
c ---[1437]---> BDD-cost:   10
c ---[1436]---> BDD-cost:    9
c ---[1435]---> BDD-cost:   10
c ---[1434]---> BDD-cost:   10
c ---[1433]---> BDD-cost:   10
c ---[1432]---> BDD-cost:   10
c ---[1431]---> BDD-cost:   10
c ---[1430]---> BDD-cost:   10
c ---[1429]---> BDD-cost:   10
c ---[1428]---> BDD-cost:   10
c ---[1427]---> BDD-cost:    9
c ---[1426]---> BDD-cost:   10
c ---[1425]---> BDD-cost:   10
c ---[1424]---> BDD-cost:   10
c ---[1423]---> BDD-cost:    9
c ---[1422]---> BDD-cost:    9
c ---[1421]---> BDD-cost:   10
c ---[1420]---> BDD-cost:   10
c ---[1419]---> BDD-cost:   10
c ---[1418]---> BDD-cost:   10
c ---[1417]---> BDD-cost:   10
c ---[1416]---> BDD-cost:   10
c ---[1415]---> BDD-cost:   10
c ---[1414]---> BDD-cost:   10
c ---[1413]---> BDD-cost:   10
c ---[1412]---> BDD-cost:   10
c ---[1411]---> BDD-cost:   10
c ---[1410]---> BDD-cost:    9
c ---[1409]---> BDD-cost:   10
c ---[1408]---> BDD-cost:   10
c ---[1407]---> BDD-cost:   10
c ---[1406]---> BDD-cost:   10
c ---[1405]---> BDD-cost:   10
c ---[1404]---> BDD-cost:    9
c ---[1403]---> BDD-cost:    9
c ---[1402]---> BDD-cost:   10
c ---[1401]---> BDD-cost:   10
c ---[1400]---> BDD-cost:   10
c ---[1399]---> BDD-cost:    9
c ---[1398]---> BDD-cost:   10
c ---[1397]---> BDD-cost:   10
c ---[1396]---> BDD-cost:   10
c ---[1395]---> BDD-cost:   10
c ---[1394]---> BDD-cost:   10
c ---[1393]---> BDD-cost:    9
c ---[1392]---> BDD-cost:   10
c ---[1391]---> BDD-cost:   10
c ---[1390]---> BDD-cost:   10
c ---[1389]---> BDD-cost:   10
c ---[1388]---> BDD-cost:   10
c ---[1387]---> BDD-cost:   10
c ---[1386]---> BDD-cost:   10
c ---[1385]---> BDD-cost:   10
c ---[1384]---> BDD-cost:   10
c ---[1383]---> BDD-cost:   10
c ---[1381]---> BDD-cost:   10
c ---[1380]---> BDD-cost:   10
c ---[1379]---> BDD-cost:   10
c ---[1378]---> BDD-cost:   10
c ---[1377]---> BDD-cost:   10
c ---[1376]---> BDD-cost:    9
c ---[1375]---> BDD-cost:   10
c ---[1374]---> BDD-cost:   10
c ---[1373]---> BDD-cost:    9
c ---[1372]---> BDD-cost:    9
c ---[1371]---> BDD-cost:    9
c ---[1370]---> BDD-cost:   10
c ---[1369]---> BDD-cost:   10
c ---[1368]---> BDD-cost:   10
c ---[1367]---> BDD-cost:   10
c ---[1366]---> BDD-cost:   10
c ---[1365]---> BDD-cost:    9
c ---[1364]---> BDD-cost:    9
c ---[1362]---> BDD-cost:   10
c ---[1361]---> BDD-cost:   10
c ---[1360]---> BDD-cost:   10
c ---[1359]---> BDD-cost:   10
c ---[1358]---> BDD-cost:   10
c ---[1357]---> BDD-cost:   10
c ---[1356]---> BDD-cost:   10
c ---[1355]---> BDD-cost:   10
c ---[1354]---> BDD-cost:   10
c ---[1353]---> BDD-cost:    8
c ---[1352]---> BDD-cost:   10
c ---[1351]---> BDD-cost:   10
c ---[1350]---> BDD-cost:    9
c ---[1349]---> BDD-cost:   10
c ---[1348]---> BDD-cost:   10
c ---[1347]---> BDD-cost:   10
c ---[1346]---> BDD-cost:   10
c ---[1344]---> Adder-cost: 4370   maxlim: 588928   bits: 20/20
c ---[1342]---> Adder-cost: 3378   maxlim: 552576   bits: 20/20
c ---[1340]---> Adder-cost: 3212   maxlim: 414848   bits: 19/19
c ---[1338]---> Adder-cost: 3118   maxlim: 421760   bits: 19/19
c ---[1336]---> Adder-cost: 2686   maxlim: 365696   bits: 19/19
c ---[1334]---> Adder-cost: 1564   maxlim: 246144   bits: 18/18
c ---[1332]---> Adder-cost: 756   maxlim: 116224   bits: 17/17
c ---[1330]---> Adder-cost: 704   maxlim: 94592   bits: 17/17
c ---[1328]---> Adder-cost: 1236   maxlim: 194560   bits: 18/18
c ---[1326]---> Adder-cost: 2132   maxlim: 281600   bits: 19/19
c ---[1324]---> Adder-cost: 1340   maxlim: 198528   bits: 18/18
c ---[1322]---> Adder-cost: 3828   maxlim: 542848   bits: 20/20
c ---[1320]---> Adder-cost: 1388   maxlim: 204928   bits: 18/18
c ---[1318]---> Adder-cost: 782   maxlim: 99328   bits: 17/17
c ---[1316]---> Adder-cost: 562   maxlim: 94848   bits: 17/17
c ---[1314]---> Adder-cost: 330   maxlim: 51840   bits: 16/16
c ---[1312]---> Adder-cost: 176   maxlim: 26624   bits: 15/15
c ---[1310]---> Adder-cost: 232   maxlim: 28544   bits: 15/15
c ---[1308]---> Adder-cost: 522   maxlim: 70400   bits: 17/17
c ---[1306]---> Adder-cost: 924   maxlim: 136064   bits: 18/18
c ---[1304]---> Adder-cost: 4884   maxlim: 977152   bits: 20/20
c ---[1302]---> Adder-cost: 3826   maxlim: 763392   bits: 20/20
c ---[1300]---> Adder-cost: 776   maxlim: 552576   bits: 20/20
c ---[1298]---> Adder-cost: 2220   maxlim: 424576   bits: 19/19
c ---[1296]---> Adder-cost: 452   maxlim: 56576   bits: 16/16
c ---[1294]---> Adder-cost: 524   maxlim: 66560   bits: 17/17
c ---[1292]---> Adder-cost: 1474   maxlim: 306560   bits: 19/19
c ---[1290]---> Adder-cost: 1944   maxlim: 456832   bits: 19/19
c ---[1288]---> Adder-cost: 362   maxlim: 46208   bits: 16/16
c ---[1286]---> Sorter-cost: 1180     Base: 2 2 2 2 2 2 2 2
c ---[1284]---> Adder-cost: 1814   maxlim: 332544   bits: 19/19
c ---[1282]---> Adder-cost: 1258   maxlim: 256384   bits: 18/18
c ---[1280]---> Adder-cost: 498   maxlim: 67712   bits: 17/17
c ---[1278]---> Adder-cost: 712   maxlim: 107136   bits: 17/17
c ---[1276]---> Adder-cost: 810   maxlim: 148352   bits: 18/18
c ---[1274]---> Adder-cost: 250   maxlim: 33920   bits: 16/16
c ---[1272]---> Adder-cost: 210   maxlim: 33920   bits: 16/16
c ---[1270]---> Adder-cost: 342   maxlim: 61696   bits: 16/16
c ---[1268]---> Adder-cost: 476   maxlim: 69888   bits: 17/17
c ---[1266]---> Adder-cost: 1820   maxlim: 249728   bits: 18/18
c ---[1264]---> Adder-cost: 2086   maxlim: 316800   bits: 19/19
c ---[1262]---> Sorter-cost:  151     Base: 2 2 2 2 2 2 2 2 2
c ---[1260]---> Adder-cost: 224   maxlim: 39808   bits: 16/16
c ---[1258]---> Adder-cost: 258   maxlim: 54144   bits: 16/16
c ---[1256]---> Adder-cost: 896   maxlim: 146944   bits: 18/18
c ---[1254]---> Adder-cost: 1424   maxlim: 190464   bits: 18/18
c ---[1252]---> Adder-cost: 3020   maxlim: 432768   bits: 19/19
c ---[1250]---> Adder-cost: 1796   maxlim: 274816   bits: 19/19
c ---[1248]---> Adder-cost: 4044   maxlim: 679552   bits: 20/20
c ---[1246]---> Adder-cost: 192   maxlim: 33664   bits: 16/16
c ---[1244]---> Adder-cost: 228   maxlim: 36224   bits: 16/16
c ---[1242]---> Adder-cost: 334   maxlim: 62080   bits: 16/16
c ---[1240]---> Sorter-cost:  910     Base: 2 2 2 2 2 2 2 2 2
c ---[1238]---> Adder-cost: 656   maxlim: 103168   bits: 17/17
c ---[1236]---> Adder-cost: 270   maxlim: 103168   bits: 17/17
c ---[1234]---> Sorter-cost:  337     Base: 2 2 2 2 2 2 2 2 2
c ---[1232]---> Adder-cost: 1774   maxlim: 300032   bits: 19/19
c ---[1230]---> Sorter-cost:  568     Base: 2 2 2 2 2 2 2 2 2
c ---[1228]---> Adder-cost: 380   maxlim: 67328   bits: 17/17
c ---[1226]---> Adder-cost: 142   maxlim: 23552   bits: 15/15
c ---[1224]---> Adder-cost: 464   maxlim: 98304   bits: 17/17
c ---[1222]---> Adder-cost: 152   maxlim: 18560   bits: 15/15
c ---[1220]---> Adder-cost: 466   maxlim: 66432   bits: 17/17
c ---[1218]---> Adder-cost: 2418   maxlim: 406656   bits: 19/19
c ---[1216]---> Adder-cost: 1274   maxlim: 209664   bits: 18/18
c ---[1214]---> Adder-cost: 4864   maxlim: 765824   bits: 20/20
c ---[1212]---> Adder-cost: 1392   maxlim: 237440   bits: 18/18
c ---[1210]---> Adder-cost: 3074   maxlim: 509568   bits: 19/19
c ---[1208]---> Adder-cost: 4114   maxlim: 797056   bits: 20/20
c ---[1206]---> Adder-cost: 1758   maxlim: 272896   bits: 19/19
c ---[1204]---> Adder-cost: 2902   maxlim: 481408   bits: 19/19
c ---[1202]---> Adder-cost: 1576   maxlim: 276096   bits: 19/19
c ---[1200]---> Adder-cost: 3600   maxlim: 676736   bits: 20/20
c ---[1198]---> Adder-cost: 232   maxlim: 33920   bits: 16/16
c ---[1196]---> Adder-cost: 156   maxlim: 21760   bits: 15/15
c ---[1194]---> Sorter-cost:  906     Base: 2 2 2 2 2 2 2 2 2
c ---[1192]---> Adder-cost: 1542   maxlim: 256768   bits: 18/18
c ---[1190]---> Adder-cost: 1494   maxlim: 255744   bits: 18/18
c ---[1188]---> Adder-cost: 758   maxlim: 128256   bits: 17/17
c ---[1186]---> Adder-cost: 1014   maxlim: 150528   bits: 18/18
c ---[1184]---> Adder-cost: 1460   maxlim: 267392   bits: 19/19
c ---[1182]---> Adder-cost: 542   maxlim: 750   bits: 10/10
c ---[1180]---> Adder-cost: 860   maxlim: 165888   bits: 18/18
c ---[1178]---> Adder-cost: 600   maxlim: 119040   bits: 17/17
c ---[1176]---> Sorter-cost: 1393     Base: 2 2 2 2 2 2 2 2 2
c ---[1174]---> Adder-cost: 656   maxlim: 110464   bits: 17/17
c ---[1172]---> Adder-cost: 562   maxlim: 89472   bits: 17/17
c ---[1170]---> Adder-cost: 272   maxlim: 46464   bits: 16/16
c ---[1168]---> Adder-cost: 1440   maxlim: 249216   bits: 18/18
c ---[1166]---> Sorter-cost:  459     Base: 2 2 2 2 2 2 2 2 2
c ---[1164]---> Sorter-cost: 1051     Base: 2 2 2 2 2 2 2 2 2
c ---[1162]---> Adder-cost: 246   maxlim: 54272   bits: 16/16
c ---[1160]---> Adder-cost: 608   maxlim: 144768   bits: 18/18
c ---[1158]---> Adder-cost: 1120   maxlim: 302464   bits: 19/19
c ---[1156]---> Adder-cost: 360   maxlim: 45696   bits: 16/16
c ---[1154]---> Adder-cost: 490   maxlim: 64128   bits: 17/16
c ---[1152]---> Sorter-cost:  367     Base: 2 2 2 2 2 2 2 2 2
c ---[1150]---> Adder-cost: 134   maxlim: 19456   bits: 15/15
c ---[1148]---> Sorter-cost: 1434     Base: 2 2 2 2 2 2 2 2 2
c ---[1146]---> Adder-cost: 832   maxlim: 120448   bits: 17/17
c ---[1144]---> Adder-cost: 1850   maxlim: 375424   bits: 19/19
c ---[1142]---> Adder-cost: 1194   maxlim: 333184   bits: 19/19
c ---[1140]---> Adder-cost: 206   maxlim: 30336   bits: 15/15
c ---[1138]---> Adder-cost: 254   maxlim: 491   bits: 9/9
c ---[1136]---> Adder-cost: 758   maxlim: 183424   bits: 18/18
c ---[1134]---> Adder-cost: 120   maxlim: 22272   bits: 15/15
c ---[1132]---> Adder-cost: 192   maxlim: 40576   bits: 16/16
c ---[1130]---> Sorter-cost:  906     Base: 2 2 2 2 2 2 2 2 2
c ---[1128]---> Adder-cost: 1596   maxlim: 337920   bits: 19/19
c ---[1126]---> Adder-cost: 856   maxlim: 139008   bits: 18/18
c ---[1124]---> Adder-cost: 294   maxlim: 41984   bits: 16/16
c ---[1122]---> Adder-cost: 332   maxlim: 52736   bits: 16/16
c ---[1120]---> Adder-cost: 1674   maxlim: 326912   bits: 19/19
c ---[1118]---> Adder-cost: 1610   maxlim: 312320   bits: 19/19
c ---[1116]---> Sorter-cost:  945     Base: 2 2 2 2 2 2 2 2 2
c ---[1114]---> Adder-cost: 172   maxlim: 22784   bits: 15/15
c ---[1112]---> Adder-cost: 130   maxlim: 15488   bits: 15/14
c ---[1110]---> Adder-cost: 1116   maxlim: 202368   bits: 18/18
c ---[1108]---> Adder-cost: 908   maxlim: 164736   bits: 18/18
c ---[1106]---> Sorter-cost:  201     Base: 2 2 2 2 2 2 2 2 2
c ---[1104]---> Adder-cost: 444   maxlim: 68096   bits: 17/17
c ---[1102]---> BDD-cost:   53
c ---[1100]---> Adder-cost: 292   maxlim: 44544   bits: 16/16
c ---[1098]---> Adder-cost: 260   maxlim: 45952   bits: 16/16
c ---[1096]---> Adder-cost: 2140   maxlim: 3369   bits: 12/12
c ---[1094]---> Adder-cost: 1600   maxlim: 385792   bits: 19/19
c ---[1092]---> Sorter-cost:  195     Base: 2 2 2 2 2 2 2 2 /oldhome/oroussel/solvers/minisat+_script: line 9: 17848 Segmentation fault      $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.97 0.94 2/54 17844
Raw data (stat): 17844 (runsolver) R 17843 32284 32283 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 784862163 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.93 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0016 s]
Raw data (loadavg): 0.94 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0016 s]
Raw data (loadavg): 0.95 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0024 s]
Raw data (loadavg): 0.96 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0029 s]
Raw data (loadavg): 0.96 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0031 s]
Raw data (loadavg): 0.97 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.004 s]
Raw data (loadavg): 0.97 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0044 s]
Raw data (loadavg): 0.98 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0058 s]
Raw data (loadavg): 0.98 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.007 s]
Raw data (loadavg): 0.98 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.007 s]
Raw data (loadavg): 0.98 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.008 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.009 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.011 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.016 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.023 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.025 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.026 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.027 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.032 s]
Raw data (loadavg): 1.06 0.99 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.037 s]
Raw data (loadavg): 1.05 0.99 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.039 s]
Raw data (loadavg): 1.04 0.99 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.039 s]
Raw data (loadavg): 1.04 0.99 0.94 2/55 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+637.512 s]
Raw data (loadavg): 1.03 0.99 0.94 1/53 17848
Raw data (stat): 17844 (minisat+_script) S 17843 32284 32283 0 -1 0 274 239 0 0 0 1 0 0 19 0 1 0 784862163 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 139
Real time (s): 637.512
CPU time (s): 637.578
CPU user time (s): 632.36
CPU system time (s): 5.21821
CPU usage (%): 100.01
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####