PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-air04.opb
MD5SUM	ee388359e66788d310d5d5b34d6465c1
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	63236
Optimality of the best value was proved	NO
Number of terms in the objective function	8904
Biggest coefficient in the objective function	2258
Number of bits for the biggest coefficient in the objective function	12
Sum of the numbers in the objective function	5135151
Number of bits of the sum of numbers in the objective function	23
Biggest number in a constraint	2258
Number of bits of the biggest number in a constraint	12
Biggest sum of numbers in a constraint	5135151
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1176.04
Number of variables	8904
Total number of constraints	9727
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	9727
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	368
Trace number 18818

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-21 16:42:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17433 boxname=wulflinc3 idbench=1341 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ee388359e66788d310d5d5b34d6465c1  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-air04.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-air04.opb /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-air04.opb
IDLAUNCH: 17433
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        705576 kB
Buffers:         28560 kB
Cached:         277644 kB
SwapCached:          0 kB
Active:          43460 kB
Inactive:       265532 kB
HighTotal:      131008 kB
HighFree:        58660 kB
LowTotal:       903652 kB
LowFree:        646916 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6844 kB
Slab:            14408 kB
Committed_AS:    71752 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 17:02:13 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 17433 7 1200.24 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1646 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1644]---> BDD-cost:   49
c ---[1642]---> BDD-cost:   67
c ---[1640]---> BDD-cost:  303
c ---[1638]---> BDD-cost:  119
c ---[1636]---> BDD-cost:  145
c ---[1634]---> BDD-cost:  165
c ---[1632]---> BDD-cost:  239
c ---[1630]---> BDD-cost:  223
c ---[1628]---> BDD-cost:   59
c ---[1626]---> BDD-cost:   35
c ---[1624]---> BDD-cost:   93
c ---[1622]---> BDD-cost:   45
c ---[1620]---> BDD-cost:  213
c ---[1618]---> BDD-cost:   73
c ---[1616]---> BDD-cost:   75
c ---[1614]---> BDD-cost:   63
c ---[1612]---> BDD-cost:   99
c ---[1608]---> BDD-cost:  187
c ---[1606]---> BDD-cost:   55
c ---[1604]---> BDD-cost:  107
c ---[1602]---> BDD-cost:   69
c ---[1600]---> BDD-cost:   13
c ---[1598]---> BDD-cost:   75
c ---[1596]---> BDD-cost:    3
c ---[1594]---> BDD-cost:  149
c ---[1592]---> BDD-cost:  137
c ---[1590]---> BDD-cost:  195
c ---[1588]---> BDD-cost:   93
c ---[1586]---> BDD-cost:  157
c ---[1584]---> BDD-cost:  233
c ---[1582]---> BDD-cost:  223
c ---[1580]---> BDD-cost:  225
c ---[1578]---> BDD-cost:  247
c ---[1576]---> BDD-cost:   75
c ---[1574]---> BDD-cost:  179
c ---[1572]---> BDD-cost:  225
c ---[1570]---> BDD-cost:  243
c ---[1568]---> BDD-cost:  199
c ---[1566]---> BDD-cost:   55
c ---[1564]---> BDD-cost:   57
c ---[1562]---> BDD-cost:   99
c ---[1560]---> BDD-cost:    9
c ---[1558]---> BDD-cost:    3
c ---[1556]---> BDD-cost:   23
c ---[1554]---> BDD-cost:   55
c ---[1552]---> BDD-cost:   51
c ---[1550]---> BDD-cost:   25
c ---[1548]---> BDD-cost:   23
c ---[1546]---> BDD-cost:   27
c ---[1544]---> BDD-cost:   15
c ---[1542]---> BDD-cost:   37
c ---[1540]---> BDD-cost:   67
c ---[1538]---> BDD-cost:   67
c ---[1536]---> BDD-cost:  109
c ---[1534]---> BDD-cost:  211
c ---[1532]---> BDD-cost:   15
c ---[1530]---> BDD-cost:    0
c ---[1526]---> BDD-cost:   65
c ---[1524]---> BDD-cost:  117
c ---[1522]---> BDD-cost:   65
c ---[1520]---> BDD-cost:   65
c ---[1518]---> BDD-cost:   49
c ---[1516]---> BDD-cost:  439
c ---[1514]---> BDD-cost:  423
c ---[1512]---> BDD-cost:  287
c ---[1510]---> BDD-cost:   87
c ---[1508]---> BDD-cost:  217
c ---[1506]---> BDD-cost:  195
c ---[1504]---> BDD-cost:   63
c ---[1502]---> BDD-cost:   53
c ---[1500]---> BDD-cost:  359
c ---[1498]---> BDD-cost:  353
c ---[1494]---> BDD-cost:  169
c ---[1492]---> BDD-cost:  139
c ---[1490]---> BDD-cost:  159
c ---[1488]---> BDD-cost:   51
c ---[1486]---> BDD-cost:  223
c ---[1484]---> BDD-cost:  107
c ---[1482]---> BDD-cost:   75
c ---[1480]---> BDD-cost:  109
c ---[1478]---> BDD-cost:   93
c ---[1476]---> BDD-cost:   87
c ---[1474]---> BDD-cost:   87
c ---[1472]---> BDD-cost:    7
c ---[1468]---> BDD-cost:   73
c ---[1466]---> BDD-cost:    1
c ---[1464]---> BDD-cost:   71
c ---[1462]---> BDD-cost:  107
c ---[1460]---> BDD-cost:   77
c ---[1458]---> BDD-cost:    3
c ---[1456]---> BDD-cost:  107
c ---[1454]---> BDD-cost:  131
c ---[1452]---> BDD-cost:  135
c ---[1450]---> BDD-cost:   65
c ---[1448]---> BDD-cost:  165
c ---[1446]---> BDD-cost:  123
c ---[1444]---> BDD-cost:    1
c ---[1442]---> BDD-cost:    1
c ---[1440]---> BDD-cost:   87
c ---[1438]---> BDD-cost:  155
c ---[1436]---> BDD-cost:  167
c ---[1434]---> BDD-cost:  203
c ---[1432]---> BDD-cost:  231
c ---[1430]---> BDD-cost:  147
c ---[1428]---> BDD-cost:  135
c ---[1426]---> BDD-cost:   49
c ---[1424]---> BDD-cost:   31
c ---[1422]---> BDD-cost:   63
c ---[1420]---> BDD-cost:   23
c ---[1418]---> BDD-cost:   95
c ---[1416]---> BDD-cost:  325
c ---[1414]---> BDD-cost:  333
c ---[1412]---> BDD-cost:  173
c ---[1410]---> BDD-cost:  269
c ---[1408]---> BDD-cost:   31
c ---[1406]---> BDD-cost:  413
c ---[1404]---> BDD-cost:  313
c ---[1402]---> BDD-cost:  125
c ---[1400]---> BDD-cost:  113
c ---[1398]---> BDD-cost:   11
c ---[1396]---> BDD-cost:  247
c ---[1394]---> BDD-cost:   57
c ---[1392]---> BDD-cost:  237
c ---[1390]---> BDD-cost:  159
c ---[1388]---> BDD-cost:  117
c ---[1386]---> BDD-cost:   43
c ---[1384]---> BDD-cost:  143
c ---[1382]---> BDD-cost:   65
c ---[1380]---> BDD-cost:  123
c ---[1378]---> BDD-cost:   61
c ---[1376]---> BDD-cost:   39
c ---[1374]---> BDD-cost:  103
c ---[1372]---> BDD-cost:   85
c ---[1370]---> BDD-cost:   77
c ---[1368]---> BDD-cost:   57
c ---[1366]---> BDD-cost:  127
c ---[1364]---> BDD-cost:  157
c ---[1362]---> BDD-cost:  267
c ---[1360]---> BDD-cost:  223
c ---[1358]---> BDD-cost:  229
c ---[1356]---> BDD-cost:  257
c ---[1354]---> BDD-cost:   13
c ---[1352]---> BDD-cost:  241
c ---[1350]---> BDD-cost:  195
c ---[1348]---> BDD-cost:   49
c ---[1346]---> BDD-cost:  117
c ---[1344]---> BDD-cost:  197
c ---[1342]---> BDD-cost:  171
c ---[1340]---> BDD-cost:  287
c ---[1338]---> BDD-cost:   75
c ---[1336]---> BDD-cost:  215
c ---[1334]---> BDD-cost:  119
c ---[1332]---> BDD-cost:   57
c ---[1330]---> BDD-cost:  245
c ---[1328]---> BDD-cost:  257
c ---[1326]---> BDD-cost:  279
c ---[1324]---> BDD-cost:  227
c ---[1322]---> BDD-cost:  201
c ---[1320]---> BDD-cost:  143
c ---[1318]---> BDD-cost:  207
c ---[1316]---> BDD-cost:  131
c ---[1314]---> BDD-cost:  245
c ---[1312]---> BDD-cost:  115
c ---[1310]---> BDD-cost:  259
c ---[1308]---> BDD-cost:   91
c ---[1306]---> BDD-cost:   43
c ---[1304]---> BDD-cost:   39
c ---[1302]---> BDD-cost:   91
c ---[1300]---> BDD-cost:  179
c ---[1298]---> BDD-cost:   73
c ---[1296]---> BDD-cost:   29
c ---[1294]---> BDD-cost:  163
c ---[1292]---> BDD-cost:   81
c ---[1290]---> BDD-cost:   63
c ---[1288]---> BDD-cost:  189
c ---[1286]---> BDD-cost:  103
c ---[1284]---> BDD-cost:  113
c ---[1282]---> BDD-cost:  115
c ---[1280]---> BDD-cost:   19
c ---[1278]---> BDD-cost:   93
c ---[1276]---> BDD-cost:   99
c ---[1274]---> BDD-cost:   99
c ---[1272]---> BDD-cost:  103
c ---[1270]---> BDD-cost:   67
c ---[1268]---> BDD-cost:   23
c ---[1266]---> BDD-cost:  101
c ---[1264]---> BDD-cost:   85
c ---[1262]---> BDD-cost:   87
c ---[1260]---> BDD-cost:    7
c ---[1258]---> BDD-cost:   45
c ---[1256]---> BDD-cost:   43
c ---[1254]---> BDD-cost:   11
c ---[1252]---> BDD-cost:   59
c ---[1250]---> BDD-cost:  185
c ---[1248]---> BDD-cost:  249
c ---[1246]---> BDD-cost:  315
c ---[1244]---> BDD-cost:  137
c ---[1242]---> BDD-cost:  253
c ---[1240]---> BDD-cost:  161
c ---[1238]---> BDD-cost:  257
c ---[1236]---> BDD-cost:  167
c ---[1234]---> BDD-cost:  167
c ---[1232]---> BDD-cost:  141
c ---[1230]---> BDD-cost:   21
c ---[1228]---> BDD-cost:   10
c ---[1226]---> BDD-cost:   95
c ---[1224]---> BDD-cost:  141
c ---[1222]---> BDD-cost:    0
c ---[1220]---> BDD-cost:  123
c ---[1218]---> BDD-cost:   83
c ---[1216]---> BDD-cost:   55
c ---[1214]---> BDD-cost:  183
c ---[1212]---> BDD-cost:  269
c ---[1210]---> BDD-cost:   63
c ---[1208]---> BDD-cost:   45
c ---[1206]---> BDD-cost:   39
c ---[1204]---> BDD-cost:   97
c ---[1202]---> BDD-cost:   51
c ---[1200]---> BDD-cost:   23
c ---[1198]---> BDD-cost:  101
c ---[1196]---> BDD-cost:   45
c ---[1194]---> BDD-cost:   17
c ---[1192]---> BDD-cost:   85
c ---[1190]---> BDD-cost:   35
c ---[1188]---> BDD-cost:   53
c ---[1186]---> BDD-cost:   21
c ---[1184]---> BDD-cost:  115
c ---[1182]---> BDD-cost:   99
c ---[1180]---> BDD-cost:   63
c ---[1178]---> BDD-cost:   77
c ---[1176]---> BDD-cost:   37
c ---[1174]---> BDD-cost:  139
c ---[1172]---> BDD-cost:  109
c ---[1170]---> BDD-cost:  407
c ---[1168]---> BDD-cost:  323
c ---[1166]---> BDD-cost:  109
c ---[1164]---> BDD-cost:   93
c ---[1162]---> BDD-cost:   51
c ---[1160]---> BDD-cost:   79
c ---[1158]---> BDD-cost:   75
c ---[1156]---> BDD-cost:  147
c ---[1154]---> BDD-cost:    0
c ---[1152]---> BDD-cost:  169
c ---[1150]---> BDD-cost:  209
c ---[1148]---> BDD-cost:   69
c ---[1146]---> BDD-cost:   51
c ---[1144]---> BDD-cost:   85
c ---[1140]---> BDD-cost:  103
c ---[1138]---> BDD-cost:  127
c ---[1136]---> BDD-cost:   77
c ---[1134]---> BDD-cost:   77
c ---[1132]---> BDD-cost:  181
c ---[1130]---> BDD-cost:  141
c ---[1128]---> BDD-cost:   89
c ---[1126]---> BDD-cost:   85
c ---[1124]---> BDD-cost:  119
c ---[1122]---> BDD-cost:   69
c ---[1120]---> BDD-cost:   57
c ---[1118]---> BDD-cost:   65
c ---[1116]---> BDD-cost:   47
c ---[1114]---> BDD-cost:   61
c ---[1112]---> BDD-cost:   31
c ---[1110]---> BDD-cost:  283
c ---[1106]---> BDD-cost:  183
c ---[1104]---> BDD-cost:  121
c ---[1102]---> BDD-cost:   89
c ---[1100]---> BDD-cost:  225
c ---[1098]---> BDD-cost:  267
c ---[1094]---> BDD-cost:  159
c ---[1092]---> BDD-cost:  209
c ---[1090]---> BDD-cost:   71
c ---[1088]---> BDD-cost:   99
c ---[1086]---> BDD-cost:  237
c ---[1084]---> BDD-cost:  129
c ---[1082]---> BDD-cost:  365
c ---[1080]---> BDD-cost:  369
c ---[1078]---> BDD-cost:  129
c ---[1076]---> BDD-cost:  101
c ---[1074]---> BDD-cost:  289
c ---[1072]---> BDD-cost:  279
c ---[1070]---> BDD-cost:  345
c ---[1068]---> BDD-cost:   81
c ---[1066]---> BDD-cost:    1
c ---[1064]---> BDD-cost:   69
c ---[1062]---> BDD-cost:   83
c ---[1060]---> BDD-cost:   53
c ---[1058]---> BDD-cost:   67
c ---[1056]---> BDD-cost:   55
c ---[1054]---> BDD-cost:  145
c ---[1052]---> BDD-cost:  149
c ---[1050]---> BDD-cost:  105
c ---[1048]---> BDD-cost:   19
c ---[1046]---> BDD-cost:  105
c ---[1044]---> BDD-cost:  109
c ---[1042]---> BDD-cost:  101
c ---[1040]---> BDD-cost:  147
c ---[1038]---> BDD-cost:  231
c ---[1036]---> BDD-cost:  191
c ---[1034]---> BDD-cost:  157
c ---[1032]---> BDD-cost:  249
c ---[1030]---> BDD-cost:  385
c ---[1028]---> BDD-cost:   67
c ---[1026]---> BDD-cost:   71
c ---[1024]---> BDD-cost:   47
c ---[1022]---> BDD-cost:   75
c ---[1020]---> BDD-cost:  147
c ---[1018]---> BDD-cost:  139
c ---[1016]---> BDD-cost:  273
c ---[1014]---> BDD-cost:  213
c ---[1012]---> BDD-cost:  169
c ---[1010]---> BDD-cost:  239
c ---[1008]---> BDD-cost:  305
c ---[1006]---> BDD-cost:  109
c ---[1004]---> BDD-cost:  105
c ---[1002]---> BDD-cost:  147
c ---[1000]---> BDD-cost:  237
c ---[ 998]---> BDD-cost:  115
c ---[ 996]---> BDD-cost:  115
c ---[ 994]---> BDD-cost:   67
c ---[ 992]---> BDD-cost:  329
c ---[ 990]---> BDD-cost:  295
c ---[ 988]---> BDD-cost:   51
c ---[ 986]---> BDD-cost:   61
c ---[ 984]---> BDD-cost:  317
c ---[ 982]---> BDD-cost:   97
c ---[ 980]---> BDD-cost:   79
c ---[ 978]---> BDD-cost:   29
c ---[ 976]---> BDD-cost:  119
c ---[ 974]---> BDD-cost:   43
c ---[ 972]---> BDD-cost:   85
c ---[ 970]---> BDD-cost:   35
c ---[ 968]---> BDD-cost:   69
c ---[ 964]---> BDD-cost:   45
c ---[ 962]---> BDD-cost:   73
c ---[ 960]---> BDD-cost:   55
c ---[ 956]---> BDD-cost:   33
c ---[ 954]---> BDD-cost:  109
c ---[ 952]---> BDD-cost:   29
c ---[ 950]---> BDD-cost:  245
c ---[ 948]---> BDD-cost:  225
c ---[ 946]---> BDD-cost:  111
c ---[ 944]---> BDD-cost:  117
c ---[ 942]---> BDD-cost:  127
c ---[ 940]---> BDD-cost:  129
c ---[ 938]---> BDD-cost:  259
c ---[ 936]---> BDD-cost:  221
c ---[ 934]---> BDD-cost:  275
c ---[ 932]---> BDD-cost:   83
c ---[ 930]---> BDD-cost:  209
c ---[ 928]---> BDD-cost:  267
c ---[ 926]---> BDD-cost:  171
c ---[ 924]---> BDD-cost:   57
c ---[ 920]---> BDD-cost:  133
c ---[ 918]---> BDD-cost:  185
c ---[ 916]---> BDD-cost:  169
c ---[ 914]---> BDD-cost:  287
c ---[ 912]---> BDD-cost:   81
c ---[ 910]---> BDD-cost:   13
c ---[ 908]---> BDD-cost:  335
c ---[ 906]---> BDD-cost:  365
c ---[ 904]---> BDD-cost:  255
c ---[ 902]---> BDD-cost:  111
c ---[ 900]---> BDD-cost:   57
c ---[ 898]---> BDD-cost:  101
c ---[ 896]---> BDD-cost:  197
c ---[ 894]---> BDD-cost:  383
c ---[ 892]---> BDD-cost:  329
c ---[ 890]---> BDD-cost:  241
c ---[ 888]---> BDD-cost:  157
c ---[ 886]---> BDD-cost:  129
c ---[ 884]---> BDD-cost:   85
c ---[ 882]---> BDD-cost:   71
c ---[ 880]---> BDD-cost:   37
c ---[ 878]---> BDD-cost:   77
c ---[ 876]---> BDD-cost:   49
c ---[ 874]---> BDD-cost:  133
c ---[ 872]---> BDD-cost:  133
c ---[ 870]---> BDD-cost:  377
c ---[ 868]---> BDD-cost:  117
c ---[ 866]---> BDD-cost:  155
c ---[ 862]---> BDD-cost:  119
c ---[ 860]---> BDD-cost:  119
c ---[ 858]---> BDD-cost:  151
c ---[ 856]---> BDD-cost:  221
c ---[ 854]---> BDD-cost:  181
c ---[ 850]---> BDD-cost:   87
c ---[ 848]---> BDD-cost:  127
c ---[ 846]---> BDD-cost:  299
c ---[ 844]---> BDD-cost:  109
c ---[ 842]---> BDD-cost:  331
c ---[ 838]---> BDD-cost:   21
c ---[ 836]---> BDD-cost:  205
c ---[ 834]---> BDD-cost:  217
c ---[ 832]---> BDD-cost:  349
c ---[ 830]---> BDD-cost:  291
c ---[ 828]---> BDD-cost:  165
c ---[ 826]---> BDD-cost:  161
c ---[ 824]---> BDD-cost:   61
c ---[ 822]---> BDD-cost:   77
c ---[ 820]---> BDD-cost:   55
c ---[ 818]---> BDD-cost:  113
c ---[ 816]---> BDD-cost:   23
c ---[ 814]---> BDD-cost:  189
c ---[ 812]---> BDD-cost:  157
c ---[ 810]---> BDD-cost:  149
c ---[ 808]---> BDD-cost:  139
c ---[ 806]---> BDD-cost:  165
c ---[ 804]---> BDD-cost:  181
c ---[ 802]---> BDD-cost:  253
c ---[ 800]---> BDD-cost:    0
c ---[ 798]---> BDD-cost:   43
c ---[ 796]---> BDD-cost:  145
c ---[ 794]---> BDD-cost:  141
c ---[ 792]---> BDD-cost:  105
c ---[ 790]---> BDD-cost:   95
c ---[ 788]---> BDD-cost:   75
c ---[ 786]---> BDD-cost:  103
c ---[ 784]---> BDD-cost:  149
c ---[ 782]---> BDD-cost:  137
c ---[ 780]---> BDD-cost:   59
c ---[ 778]---> BDD-cost:  133
c ---[ 776]---> BDD-cost:    5
c ---[ 774]---> BDD-cost:   35
c ---[ 772]---> BDD-cost:    9
c ---[ 770]---> BDD-cost:   35
c ---[ 768]---> BDD-cost:   47
c ---[ 764]---> BDD-cost:   55
c ---[ 762]---> BDD-cost:  197
c ---[ 760]---> BDD-cost:  191
c ---[ 758]---> BDD-cost:  125
c ---[ 756]---> BDD-cost:    0
c ---[ 754]---> BDD-cost:  103
c ---[ 752]---> BDD-cost:  173
c ---[ 748]---> BDD-cost:   93
c ---[ 746]---> BDD-cost:   29
c ---[ 744]---> BDD-cost:  321
c ---[ 742]---> BDD-cost:  195
c ---[ 740]---> BDD-cost:  163
c ---[ 734]---> BDD-cost:  151
c ---[ 732]---> BDD-cost:  115
c ---[ 730]---> BDD-cost:  253
c ---[ 728]---> BDD-cost:  381
c ---[ 726]---> BDD-cost:  345
c ---[ 724]---> BDD-cost:  185
c ---[ 720]---> BDD-cost:   83
c ---[ 718]---> BDD-cost:   69
c ---[ 716]---> BDD-cost:   51
c ---[ 714]---> BDD-cost:   47
c ---[ 712]---> BDD-cost:   59
c ---[ 710]---> BDD-cost:  185
c ---[ 708]---> BDD-cost:   83
c ---[ 706]---> BDD-cost:  107
c ---[ 704]---> BDD-cost:  363
c ---[ 702]---> BDD-cost:  103
c ---[ 700]---> BDD-cost:  277
c ---[ 698]---> BDD-cost:  341
c ---[ 696]---> BDD-cost:  213
c ---[ 694]---> BDD-cost:  315
c ---[ 692]---> BDD-cost:  275
c ---[ 690]---> BDD-cost:  151
c ---[ 688]---> BDD-cost:  203
c ---[ 686]---> BDD-cost:  111
c ---[ 684]---> BDD-cost:  103
c ---[ 682]---> BDD-cost:   75
c ---[ 680]---> BDD-cost:   27
c ---[ 678]---> BDD-cost:   21
c ---[ 676]---> BDD-cost:   11
c ---[ 674]---> BDD-cost:   31
c ---[ 670]---> BDD-cost:   19
c ---[ 668]---> BDD-cost:  149
c ---[ 666]---> BDD-cost:  167
c ---[ 664]---> BDD-cost:    0
c ---[ 662]---> BDD-cost:   97
c ---[ 660]---> BDD-cost:  149
c ---[ 658]---> BDD-cost:  395
c ---[ 656]---> BDD-cost:   25
c ---[ 654]---> BDD-cost:  389
c ---[ 652]---> BDD-cost:  251
c ---[ 650]---> BDD-cost:  375
c ---[ 648]---> BDD-cost:  343
c ---[ 646]---> BDD-cost:  267
c ---[ 644]---> BDD-cost:  135
c ---[ 642]---> BDD-cost:  135
c ---[ 640]---> BDD-cost:  263
c ---[ 638]---> BDD-cost:  259
c ---[ 636]---> BDD-cost:  245
c ---[ 634]---> BDD-cost:   45
c ---[ 632]---> BDD-cost:   41
c ---[ 630]---> BDD-cost:  127
c ---[ 628]---> BDD-cost:  117
c ---[ 626]---> BDD-cost:   53
c ---[ 624]---> BDD-cost:  149
c ---[ 622]---> BDD-cost:    9
c ---[ 620]---> BDD-cost:  103
c ---[ 618]---> BDD-cost:  215
c ---[ 616]---> BDD-cost:   89
c ---[ 614]---> BDD-cost:  177
c ---[ 612]---> BDD-cost:  343
c ---[ 610]---> BDD-cost:  237
c ---[ 608]---> BDD-cost:  177
c ---[ 606]---> BDD-cost:   85
c ---[ 604]---> BDD-cost:  267
c ---[ 602]---> BDD-cost:  225
c ---[ 600]---> BDD-cost:   85
c ---[ 598]---> BDD-cost:  109
c ---[ 596]---> BDD-cost:  105
c ---[ 594]---> BDD-cost:  113
c ---[ 592]---> BDD-cost:   55
c ---[ 590]---> BDD-cost:  117
c ---[ 588]---> BDD-cost:   83
c ---[ 586]---> BDD-cost:   79
c ---[ 584]---> BDD-cost:   81
c ---[ 582]---> BDD-cost:  263
c ---[ 580]---> BDD-cost:  179
c ---[ 578]---> BDD-cost:  143
c ---[ 576]---> BDD-cost:  281
c ---[ 574]---> BDD-cost:  389
c ---[ 572]---> BDD-cost:  333
c ---[ 570]---> BDD-cost:  357
c ---[ 568]---> BDD-cost:  345
c ---[ 566]---> BDD-cost:  263
c ---[ 564]---> BDD-cost:   89
c ---[ 562]---> BDD-cost:  285
c ---[ 558]---> BDD-cost:  419
c ---[ 556]---> BDD-cost:  135
c ---[ 554]---> BDD-cost:  357
c ---[ 552]---> BDD-cost:  473
c ---[ 550]---> BDD-cost:  455
c ---[ 548]---> BDD-cost:  405
c ---[ 546]---> BDD-cost:  241
c ---[ 544]---> BDD-cost:  211
c ---[ 542]---> BDD-cost:  313
c ---[ 540]---> BDD-cost:  371
c ---[ 538]---> BDD-cost:  389
c ---[ 536]---> BDD-cost:  223
c ---[ 534]---> BDD-cost:   71
c ---[ 532]---> BDD-cost:   63
c ---[ 530]---> BDD-cost:  221
c ---[ 528]---> BDD-cost:  147
c ---[ 526]---> BDD-cost:  131
c ---[ 524]---> BDD-cost:  185
c ---[ 522]---> BDD-cost:  141
c ---[ 520]---> BDD-cost:  249
c ---[ 518]---> BDD-cost:  261
c ---[ 516]---> BDD-cost:  311
c ---[ 514]---> BDD-cost:  261
c ---[ 512]---> BDD-cost:  387
c ---[ 510]---> BDD-cost:   51
c ---[ 508]---> BDD-cost:  247
c ---[ 506]---> BDD-cost:  295
c ---[ 504]---> BDD-cost:   31
c ---[ 502]---> BDD-cost:  355
c ---[ 500]---> BDD-cost:  135
c ---[ 498]---> BDD-cost:  443
c ---[ 496]---> BDD-cost:  653
c ---[ 494]---> BDD-cost:  703
c ---[ 492]---> BDD-cost:  517
c ---[ 490]---> BDD-cost:  441
c ---[ 488]---> BDD-cost:  159
c ---[ 486]---> BDD-cost:  411
c ---[ 484]---> BDD-cost:  289
c ---[ 482]---> BDD-cost:  277
c ---[ 480]---> BDD-cost:  239
c ---[ 478]---> BDD-cost:  201
c ---[ 476]---> BDD-cost:  309
c ---[ 474]---> BDD-cost:  287
c ---[ 472]---> BDD-cost:  177
c ---[ 470]---> BDD-cost:  143
c ---[ 468]---> BDD-cost:  131
c ---[ 466]---> BDD-cost:  155
c ---[ 464]---> BDD-cost:   35
c ---[ 462]---> BDD-cost:  189
c ---[ 460]---> BDD-cost:  219
c ---[ 456]---> BDD-cost:  267
c ---[ 454]---> BDD-cost:  135
c ---[ 452]---> BDD-cost:   69
c ---[ 450]---> BDD-cost:   75
c ---[ 448]---> BDD-cost:   51
c ---[ 446]---> BDD-cost:  117
c ---[ 444]---> BDD-cost:  211
c ---[ 442]---> BDD-cost:  117
c ---[ 436]---> BDD-cost:  189
c ---[ 434]---> BDD-cost:   73
c ---[ 432]---> BDD-cost:   55
c ---[ 430]---> BDD-cost:   57
c ---[ 428]---> BDD-cost:   91
c ---[ 426]---> BDD-cost:  325
c ---[ 424]---> BDD-cost:  223
c ---[ 422]---> BDD-cost:   75
c ---[ 420]---> BDD-cost:   57
c ---[ 418]---> BDD-cost:   43
c ---[ 416]---> BDD-cost:  255
c ---[ 414]---> BDD-cost:  285
c ---[ 412]---> BDD-cost:  187
c ---[ 410]---> BDD-cost:   37
c ---[ 408]---> BDD-cost:   91
c ---[ 406]---> BDD-cost:  211
c ---[ 404]---> BDD-cost:  159
c ---[ 402]---> BDD-cost:   97
c ---[ 400]---> BDD-cost:   37
c ---[ 398]---> BDD-cost:   27
c ---[ 396]---> BDD-cost:  101
c ---[ 394]---> BDD-cost:  141
c ---[ 390]---> BDD-cost:  109
c ---[ 388]---> BDD-cost:  321
c ---[ 386]---> BDD-cost:  305
c ---[ 384]---> BDD-cost:  603
c ---[ 382]---> BDD-cost:  441
c ---[ 380]---> BDD-cost:  391
c ---[ 378]---> BDD-cost:   87
c ---[ 376]---> BDD-cost:  387
c ---[ 374]---> BDD-cost:  289
c ---[ 372]---> BDD-cost:  219
c ---[ 370]---> BDD-cost:  309
c ---[ 368]---> BDD-cost:  241
c ---[ 366]---> BDD-cost:  197
c ---[ 364]---> BDD-cost:  279
c ---[ 362]---> BDD-cost:  167
c ---[ 360]---> BDD-cost:  151
c ---[ 358]---> BDD-cost:   49
c ---[ 356]---> BDD-cost:   79
c ---[ 354]---> BDD-cost:   31
c ---[ 352]---> BDD-cost:  107
c ---[ 350]---> BDD-cost:   55
c ---[ 346]---> BDD-cost:  177
c ---[ 344]---> BDD-cost:  223
c ---[ 342]---> BDD-cost:  119
c ---[ 340]---> BDD-cost:  137
c ---[ 338]---> BDD-cost:  105
c ---[ 336]---> BDD-cost:  183
c ---[ 334]---> BDD-cost:  109
c ---[ 332]---> BDD-cost:  179
c ---[ 330]---> BDD-cost:  285
c ---[ 328]---> BDD-cost:  191
c ---[ 326]---> BDD-cost:  177
c ---[ 324]---> BDD-cost:  145
c ---[ 320]---> BDD-cost:  153
c ---[ 318]---> BDD-cost:  121
c ---[ 316]---> BDD-cost:   95
c ---[ 314]---> BDD-cost:  111
c ---[ 312]---> BDD-cost:   35
c ---[ 310]---> BDD-cost:  115
c ---[ 308]---> BDD-cost:    0
c ---[ 306]---> BDD-cost:  281
c ---[ 304]---> BDD-cost:  265
c ---[ 302]---> BDD-cost:  167
c ---[ 300]---> BDD-cost:  151
c ---[ 298]---> BDD-cost:  167
c ---[ 296]---> BDD-cost:  137
c ---[ 292]---> BDD-cost:  375
c ---[ 290]---> BDD-cost:  287
c ---[ 288]---> BDD-cost:  247
c ---[ 286]---> BDD-cost:  249
c ---[ 284]---> BDD-cost:  131
c ---[ 282]---> BDD-cost:  187
c ---[ 280]---> BDD-cost:  135
c ---[ 278]---> BDD-cost:  129
c ---[ 276]---> BDD-cost:  317
c ---[ 274]---> BDD-cost:  365
c ---[ 272]---> BDD-cost:  235
c ---[ 270]---> BDD-cost:  249
c ---[ 268]---> BDD-cost:  283
c ---[ 266]---> BDD-cost:  105
c ---[ 264]---> BDD-cost:  233
c ---[ 262]---> BDD-cost:  259
c ---[ 260]---> BDD-cost:  287
c ---[ 258]---> BDD-cost:  175
c ---[ 256]---> BDD-cost:  233
c ---[ 254]---> BDD-cost:  167
c ---[ 252]---> BDD-cost:  159
c ---[ 250]---> BDD-cost:   47
c ---[ 246]---> BDD-cost:  135
c ---[ 244]---> BDD-cost:   59
c ---[ 242]---> BDD-cost:  147
c ---[ 240]---> BDD-cost:  167
c ---[ 238]---> BDD-cost:  203
c ---[ 236]---> BDD-cost:  275
c ---[ 234]---> BDD-cost:  263
c ---[ 232]---> BDD-cost:   31
c ---[ 230]---> BDD-cost:   11
c ---[ 228]---> BDD-cost:   31
c ---[ 226]---> BDD-cost:   27
c ---[ 224]---> BDD-cost:  225
c ---[ 222]---> BDD-cost:   71
c ---[ 220]---> BDD-cost:   65
c ---[ 218]---> BDD-cost:  385
c ---[ 216]---> BDD-cost:  361
c ---[ 214]---> BDD-cost:   73
c ---[ 212]---> BDD-cost:   77
c ---[ 208]---> BDD-cost:  131
c ---[ 206]---> BDD-cost:  145
c ---[ 204]---> BDD-cost:  121
c ---[ 202]---> BDD-cost:  117
c ---[ 200]---> BDD-cost:   61
c ---[ 198]---> BDD-cost:  111
c ---[ 196]---> BDD-cost:  123
c ---[ 194]---> BDD-cost:  125
c ---[ 192]---> BDD-cost:  243
c ---[ 190]---> BDD-cost:  143
c ---[ 188]---> BDD-cost:  149
c ---[ 186]---> BDD-cost:  103
c ---[ 184]---> BDD-cost:  155
c ---[ 182]---> BDD-cost:  247
c ---[ 180]---> BDD-cost:  143
c ---[ 178]---> BDD-cost:   89
c ---[ 176]---> BDD-cost:   91
c ---[ 174]---> BDD-cost:   81
c ---[ 172]---> BDD-cost:   79
c ---[ 170]---> BDD-cost:  117
c ---[ 168]---> BDD-cost:   89
c ---[ 166]---> BDD-cost:   61
c ---[ 164]---> BDD-cost:  127
c ---[ 162]---> BDD-cost:  135
c ---[ 160]---> BDD-cost:  161
c ---[ 158]---> BDD-cost:  141
c ---[ 156]---> BDD-cost:   91
c ---[ 154]---> BDD-cost:  437
c ---[ 152]---> BDD-cost:  309
c ---[ 150]---> BDD-cost:  173
c ---[ 148]---> BDD-cost:  441
c ---[ 146]---> BDD-cost:  489
c ---[ 144]---> BDD-cost:  299
c ---[ 142]---> BDD-cost:  455
c ---[ 140]---> BDD-cost:  333
c ---[ 138]---> BDD-cost:  421
c ---[ 136]---> BDD-cost:  375
c ---[ 134]---> BDD-cost:  143
c ---[ 132]---> BDD-cost:  433
c ---[ 130]---> BDD-cost:  405
c ---[ 128]---> BDD-cost:  333
c ---[ 126]---> BDD-cost:  673
c ---[ 124]---> BDD-cost:  685
c ---[ 122]---> BDD-cost:  385
c ---[ 120]---> BDD-cost:  267
c ---[ 118]---> BDD-cost:  345
c ---[ 116]---> BDD-cost:  365
c ---[ 114]---> BDD-cost:  391
c ---[ 112]---> BDD-cost:  111
c ---[ 110]---> BDD-cost:  313
c ---[ 108]---> BDD-cost:  275
c ---[ 106]---> BDD-cost:  257
c ---[ 104]---> BDD-cost:  203
c ---[ 102]---> BDD-cost:  311
c ---[ 100]---> BDD-cost:  227
c ---[  98]---> BDD-cost:  295
c ---[  96]---> BDD-cost:  233
c ---[  94]---> BDD-cost:  247
c ---[  92]---> BDD-cost:  237
c ---[  90]---> BDD-cost:   23
c ---[  88]---> BDD-cost:   95
c ---[  86]---> BDD-cost:    0
c ---[  84]---> BDD-cost:  149
c ---[  80]---> BDD-cost:   99
c ---[  78]---> BDD-cost:   85
c ---[  76]---> BDD-cost:  109
c ---[  74]---> BDD-cost:   43
c ---[  72]---> BDD-cost:   83
c ---[  70]---> BDD-cost:   71
c ---[  68]---> BDD-cost:   67
c ---[  66]---> BDD-cost:  169
c ---[  64]---> BDD-cost:  151
c ---[  62]---> BDD-cost:  147
c ---[  60]---> BDD-cost:  177
c ---[  58]---> BDD-cost:  127
c ---[  56]---> BDD-cost:  131
c ---[  54]---> BDD-cost:  147
c ---[  52]---> BDD-cost:  215
c ---[  50]---> BDD-cost:  181
c ---[  48]---> BDD-cost:  235
c ---[  46]---> BDD-cost:  163
c ---[  44]---> BDD-cost:  101
c ---[  42]---> BDD-cost:   57
c ---[  40]---> BDD-cost:   59
c ---[  38]---> BDD-cost:  139
c ---[  36]---> BDD-cost:   39
c ---[  34]---> BDD-cost:  151
c ---[  32]---> BDD-cost:   67
c ---[  30]---> BDD-cost:   45
c ---[  28]---> BDD-cost:   45
c ---[  26]---> BDD-cost:   45
c ---[  24]---> BDD-cost:   65
c ---[  22]---> BDD-cost:   95
c ---[  20]---> BDD-cost:    0
c ---[  16]---> BDD-cost:   47
c ---[  12]---> BDD-cost:   29
c ---[  10]---> BDD-cost:   27
c ---[   8]---> BDD-cost:   11
c ---[   4]---> BDD-cost:   81
c ---[   2]---> BDD-cost:  223
c ---[   0]---> BDD-cost:  271
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  556705  1546773 |  185568       0        0     nan |  0.000 % |
c |       101 |  556583  1546438 |  204124      97     3860    39.8 |  0.597 % |
c |       253 |  556583  1546438 |  224537     249     8590    34.5 |  0.597 % |
c |       480 |  556583  1546438 |  246991     476    27255    57.3 |  0.597 % |
c |       817 |  556460  1546082 |  271690     807    57537    71.3 |  0.613 % |
c |      1324 |  556460  1546082 |  298859    1314    96333    73.3 |  0.613 % |
c |      2083 |  556435  1546014 |  328745    2072   169245    81.7 |  0.614 % |
c |      3222 |  556306  1545644 |  361619    3193   235735    73.8 |  0.628 % |
c |      4933 |  556143  1545187 |  397781    4887   374517    76.6 |  0.645 % |
c |      7496 |  555762  1544105 |  437559    7324   683691    93.3 |  0.680 % |
c |     11341 |  553381  1537592 |  481315   11000  1016992    92.5 |  0.890 % |
c |     17108 |  553168  1537017 |  529447   16736  2141343   127.9 |  0.905 % |
c |     25760 |  552999  1536551 |  582391   25355  4410378   173.9 |  0.916 % |
c |     38734 |  552412  1534942 |  640631   38256  6250267   163.4 |  0.963 % |
c |     58195 |  551755  1533149 |  704694   57618 10540545   182.9 |  1.002 % |
c |     87388 |  551111  1531403 |  775163   86624 18470644   213.2 |  1.038 % |
#### 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.95 0.92 2/54 14508
Raw data (stat): 14508 (runsolver) R 14507 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488377860 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.001 s]
Raw data (loadavg): 0.93 0.96 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 12967 0 0 0 963 35 0 0 25 0 1 0 488377860 63373312 12599 4294967295 134512640 134672761 3221224544 3221223708 134564522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15472 12599 603 41 0 15431 0
vsize: 61888
[startup+20.0013 s]
Raw data (loadavg): 0.94 0.96 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 13105 0 0 0 1962 35 0 0 25 0 1 0 488377860 63913984 12737 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15604 12737 603 41 0 15563 0
vsize: 62416
[startup+30.0018 s]
Raw data (loadavg): 0.95 0.96 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 13235 0 0 0 2961 36 0 0 25 0 1 0 488377860 64466944 12867 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15739 12867 603 41 0 15698 0
vsize: 62956
[startup+40.0021 s]
Raw data (loadavg): 0.96 0.96 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 13505 0 0 0 3960 38 0 0 25 0 1 0 488377860 65548288 13137 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16003 13137 603 41 0 15962 0
vsize: 64012
[startup+50.0025 s]
Raw data (loadavg): 0.96 0.96 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 13708 0 0 0 4959 39 0 0 25 0 1 0 488377860 66359296 13340 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16201 13340 603 41 0 16160 0
vsize: 64804
[startup+60.0023 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 13846 0 0 0 5958 40 0 0 25 0 1 0 488377860 66953216 13478 4294967295 134512640 134672761 3221224544 3221223668 134566115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16346 13478 603 41 0 16305 0
vsize: 65384
[startup+70.0039 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 14163 0 0 0 6957 41 0 0 25 0 1 0 488377860 68300800 13795 4294967295 134512640 134672761 3221224544 3221223712 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16675 13795 603 41 0 16634 0
vsize: 66700
[startup+80.0054 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 14350 0 0 0 7956 42 0 0 25 0 1 0 488377860 69111808 13982 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16873 13982 603 41 0 16832 0
vsize: 67492
[startup+90.0058 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 14710 0 0 0 8954 44 0 0 25 0 1 0 488377860 70451200 14342 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17200 14342 603 41 0 17159 0
vsize: 68800
[startup+100.006 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 15034 0 0 0 9953 45 0 0 25 0 1 0 488377860 71798784 14666 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17529 14666 603 41 0 17488 0
vsize: 70116
[startup+110.007 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 15313 0 0 0 10952 46 0 0 25 0 1 0 488377860 73023488 14945 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17828 14945 603 41 0 17787 0
vsize: 71312
[startup+120.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 15471 0 0 0 11951 47 0 0 25 0 1 0 488377860 73691136 15103 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17991 15103 603 41 0 17950 0
vsize: 71964
[startup+130.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 15684 0 0 0 12951 48 0 0 25 0 1 0 488377860 74502144 15316 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18189 15316 603 41 0 18148 0
vsize: 72756
[startup+140.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 15884 0 0 0 13950 49 0 0 25 0 1 0 488377860 75313152 15516 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18387 15516 603 41 0 18346 0
vsize: 73548
[startup+150.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 16084 0 0 0 14949 49 0 0 25 0 1 0 488377860 76120064 15716 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18584 15716 603 41 0 18543 0
vsize: 74336
[startup+160.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 16481 0 0 0 15948 50 0 0 25 0 1 0 488377860 77725696 16113 4294967295 134512640 134672761 3221224544 3221223648 134560002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18976 16113 603 41 0 18935 0
vsize: 75904
[startup+170.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 16955 0 0 0 16947 52 0 0 25 0 1 0 488377860 79761408 16587 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19473 16587 603 41 0 19432 0
vsize: 77892
[startup+180.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 17389 0 0 0 17945 54 0 0 25 0 1 0 488377860 81514496 17021 4294967295 134512640 134672761 3221224544 3221223648 134560136 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19901 17021 603 41 0 19860 0
vsize: 79604
[startup+190.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 17652 0 0 0 18944 55 0 0 25 0 1 0 488377860 82591744 17284 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20164 17284 603 41 0 20123 0
vsize: 80656
[startup+200.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 18086 0 0 0 19942 57 0 0 25 0 1 0 488377860 84340736 17718 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20591 17718 603 41 0 20550 0
vsize: 82364
[startup+210.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 18440 0 0 0 20941 58 0 0 25 0 1 0 488377860 85819392 18072 4294967295 134512640 134672761 3221224544 3221223648 134559927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20952 18072 603 41 0 20911 0
vsize: 83808
[startup+220.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 18676 0 0 0 21941 59 0 0 25 0 1 0 488377860 86761472 18308 4294967295 134512640 134672761 3221224544 3221223680 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21182 18308 603 41 0 21141 0
vsize: 84728
[startup+230.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 18862 0 0 0 22940 60 0 0 25 0 1 0 488377860 87560192 18494 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21377 18494 603 41 0 21336 0
vsize: 85508
[startup+240.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 19057 0 0 0 23939 61 0 0 25 0 1 0 488377860 88371200 18689 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21575 18689 603 41 0 21534 0
vsize: 86300
[startup+250.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 19269 0 0 0 24938 62 0 0 25 0 1 0 488377860 89317376 18901 4294967295 134512640 134672761 3221224544 3221223728 134559019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21806 18901 603 41 0 21765 0
vsize: 87224
[startup+260.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 19496 0 0 0 25938 62 0 0 25 0 1 0 488377860 90255360 19128 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22035 19128 603 41 0 21994 0
vsize: 88140
[startup+270.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 19743 0 0 0 26937 63 0 0 25 0 1 0 488377860 91197440 19375 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22265 19375 603 41 0 22224 0
vsize: 89060
[startup+280.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 19992 0 0 0 27936 64 0 0 25 0 1 0 488377860 92278784 19624 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22529 19624 603 41 0 22488 0
vsize: 90116
[startup+290.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 20203 0 0 0 28935 65 0 0 25 0 1 0 488377860 93085696 19835 4294967295 134512640 134672761 3221224544 3221223680 134560716 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22726 19835 603 41 0 22685 0
vsize: 90904
[startup+300.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 20447 0 0 0 29934 66 0 0 25 0 1 0 488377860 94019584 20079 4294967295 134512640 134672761 3221224544 3221223648 134559976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22954 20079 603 41 0 22913 0
vsize: 91816
[startup+310.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 20711 0 0 0 30934 67 0 0 25 0 1 0 488377860 95092736 20343 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23216 20343 603 41 0 23175 0
vsize: 92864
[startup+320.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 20913 0 0 0 31933 68 0 0 25 0 1 0 488377860 96030720 20545 4294967295 134512640 134672761 3221224544 3221223648 134560276 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23445 20545 603 41 0 23404 0
vsize: 93780
[startup+330.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 21204 0 0 0 32932 68 0 0 25 0 1 0 488377860 97116160 20836 4294967295 134512640 134672761 3221224544 3221223680 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23710 20836 603 41 0 23669 0
vsize: 94840
[startup+340.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 21508 0 0 0 33931 70 0 0 25 0 1 0 488377860 98463744 21140 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24039 21140 603 41 0 23998 0
vsize: 96156
[startup+350.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 21773 0 0 0 34930 71 0 0 25 0 1 0 488377860 99536896 21405 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24301 21405 603 41 0 24260 0
vsize: 97204
[startup+360.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 21971 0 0 0 35929 72 0 0 25 0 1 0 488377860 100335616 21603 4294967295 134512640 134672761 3221224544 3221223680 134560667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24496 21603 603 41 0 24455 0
vsize: 97984
[startup+370.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 22206 0 0 0 36928 73 0 0 25 0 1 0 488377860 101281792 21838 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24727 21838 603 41 0 24686 0
vsize: 98908
[startup+380.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 22464 0 0 0 37927 74 0 0 25 0 1 0 488377860 102359040 22096 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24990 22096 603 41 0 24949 0
vsize: 99960
[startup+390.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 22687 0 0 0 38926 75 0 0 25 0 1 0 488377860 103165952 22319 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25187 22319 603 41 0 25146 0
vsize: 100748
[startup+400.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 22941 0 0 0 39925 76 0 0 25 0 1 0 488377860 104243200 22573 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25450 22573 603 41 0 25409 0
vsize: 101800
[startup+410.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 23351 0 0 0 40924 77 0 0 25 0 1 0 488377860 105971712 22983 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25872 22983 603 41 0 25831 0
vsize: 103488
[startup+420.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 23732 0 0 0 41923 78 0 0 25 0 1 0 488377860 107438080 23364 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26230 23364 603 41 0 26189 0
vsize: 104920
[startup+430.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 24043 0 0 0 42923 79 0 0 25 0 1 0 488377860 108777472 23675 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26557 23675 603 41 0 26516 0
vsize: 106228
[startup+440.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 24327 0 0 0 43922 80 0 0 25 0 1 0 488377860 109854720 23959 4294967295 134512640 134672761 3221224544 3221223648 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26820 23959 603 41 0 26779 0
vsize: 107280
[startup+450.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 24527 0 0 0 44921 81 0 0 25 0 1 0 488377860 110661632 24159 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27017 24159 603 41 0 26976 0
vsize: 108068
[startup+460.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 24739 0 0 0 45921 81 0 0 25 0 1 0 488377860 111603712 24371 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27247 24371 603 41 0 27206 0
vsize: 108988
[startup+470.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 24940 0 0 0 46920 82 0 0 25 0 1 0 488377860 112410624 24572 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27444 24572 603 41 0 27403 0
vsize: 109776
[startup+480.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 25186 0 0 0 47919 83 0 0 25 0 1 0 488377860 113344512 24818 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27672 24818 603 41 0 27631 0
vsize: 110688
[startup+490.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 25361 0 0 0 48919 83 0 0 25 0 1 0 488377860 114016256 24993 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27836 24993 603 41 0 27795 0
vsize: 111344
[startup+500.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 25568 0 0 0 49918 84 0 0 25 0 1 0 488377860 114958336 25200 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28066 25200 603 41 0 28025 0
vsize: 112264
[startup+510.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 25783 0 0 0 50917 85 0 0 25 0 1 0 488377860 116031488 25415 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28328 25415 603 41 0 28287 0
vsize: 113312
[startup+520.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 26036 0 0 0 51916 86 0 0 25 0 1 0 488377860 117108736 25668 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28591 25668 603 41 0 28550 0
vsize: 114364
[startup+530.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 26306 0 0 0 52915 87 0 0 25 0 1 0 488377860 118194176 25938 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28856 25938 603 41 0 28815 0
vsize: 115424
[startup+540.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 26627 0 0 0 53915 88 0 0 25 0 1 0 488377860 119566336 26259 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29191 26259 603 41 0 29150 0
vsize: 116764
[startup+550.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 26899 0 0 0 54914 89 0 0 25 0 1 0 488377860 120664064 26531 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29459 26531 603 41 0 29418 0
vsize: 117836
[startup+560.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 27198 0 0 0 55913 90 0 0 25 0 1 0 488377860 121876480 26830 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29755 26830 603 41 0 29714 0
vsize: 119020
[startup+570.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 27456 0 0 0 56912 91 0 0 25 0 1 0 488377860 122822656 27088 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29986 27088 603 41 0 29945 0
vsize: 119944
[startup+580.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 27738 0 0 0 57911 92 0 0 25 0 1 0 488377860 124030976 27370 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30281 27370 603 41 0 30240 0
vsize: 121124
[startup+590.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 28024 0 0 0 58910 93 0 0 25 0 1 0 488377860 125251584 27656 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30579 27656 603 41 0 30538 0
vsize: 122316
[startup+600.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 28332 0 0 0 59910 94 0 0 25 0 1 0 488377860 126451712 27964 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30872 27964 603 41 0 30831 0
vsize: 123488
[startup+610.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 28577 0 0 0 60909 94 0 0 25 0 1 0 488377860 127406080 28209 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31105 28209 603 41 0 31064 0
vsize: 124420
[startup+620.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 28875 0 0 0 61909 95 0 0 25 0 1 0 488377860 128733184 28507 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31429 28507 603 41 0 31388 0
vsize: 125716
[startup+630.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 29200 0 0 0 62909 95 0 0 25 0 1 0 488377860 129941504 28832 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31724 28832 603 41 0 31683 0
vsize: 126896
[startup+640.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 29474 0 0 0 63908 96 0 0 25 0 1 0 488377860 131149824 29106 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32019 29106 603 41 0 31978 0
vsize: 128076
[startup+650.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 29737 0 0 0 64908 97 0 0 25 0 1 0 488377860 132222976 29369 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32281 29369 603 41 0 32240 0
vsize: 129124
[startup+660.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 29956 0 0 0 65907 97 0 0 25 0 1 0 488377860 133165056 29588 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32511 29588 603 41 0 32470 0
vsize: 130044
[startup+670.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 30215 0 0 0 66907 98 0 0 25 0 1 0 488377860 134111232 29847 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32742 29847 603 41 0 32701 0
vsize: 130968
[startup+680.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 30364 0 0 0 67907 98 0 0 25 0 1 0 488377860 134782976 29996 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32906 29996 603 41 0 32865 0
vsize: 131624
[startup+690.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 30595 0 0 0 68906 99 0 0 25 0 1 0 488377860 135729152 30227 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33137 30227 603 41 0 33096 0
vsize: 132548
[startup+700.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 30875 0 0 0 69905 100 0 0 25 0 1 0 488377860 136814592 30507 4294967295 134512640 134672761 3221224544 3221223648 134559964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33402 30507 603 41 0 33361 0
vsize: 133608
[startup+710.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 31067 0 0 0 70905 100 0 0 25 0 1 0 488377860 137625600 30699 4294967295 134512640 134672761 3221224544 3221223728 134558638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33600 30699 603 41 0 33559 0
vsize: 134400
[startup+720.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 31366 0 0 0 71905 101 0 0 25 0 1 0 488377860 138858496 30998 4294967295 134512640 134672761 3221224544 3221223728 134559028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33901 30998 603 41 0 33860 0
vsize: 135604
[startup+730.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 31652 0 0 0 72905 101 0 0 25 0 1 0 488377860 140062720 31284 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34195 31284 603 41 0 34154 0
vsize: 136780
[startup+740.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 31986 0 0 0 73904 102 0 0 25 0 1 0 488377860 141410304 31618 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34524 31618 603 41 0 34483 0
vsize: 138096
[startup+750.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 32258 0 0 0 74903 103 0 0 25 0 1 0 488377860 142491648 31890 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34788 31890 603 41 0 34747 0
vsize: 139152
[startup+760.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 32491 0 0 0 75903 104 0 0 25 0 1 0 488377860 143429632 32123 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35017 32123 603 41 0 34976 0
vsize: 140068
[startup+770.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 32731 0 0 0 76902 104 0 0 25 0 1 0 488377860 144367616 32363 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35246 32363 603 41 0 35205 0
vsize: 140984
[startup+780.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 33050 0 0 0 77901 106 0 0 25 0 1 0 488377860 145719296 32682 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35576 32682 603 41 0 35535 0
vsize: 142304
[startup+790.041 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 33338 0 0 0 78901 106 0 0 25 0 1 0 488377860 146931712 32970 4294967295 134512640 134672761 3221224544 3221223648 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35872 32970 603 41 0 35831 0
vsize: 143488
[startup+800.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 33613 0 0 0 79900 107 0 0 25 0 1 0 488377860 147992576 33245 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36131 33245 603 41 0 36090 0
vsize: 144524
[startup+810.041 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 33920 0 0 0 80899 108 0 0 25 0 1 0 488377860 149204992 33552 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36427 33552 603 41 0 36386 0
vsize: 145708
[startup+820.041 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 34222 0 0 0 81898 109 0 0 25 0 1 0 488377860 150519808 33854 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36748 33854 603 41 0 36707 0
vsize: 146992
[startup+830.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 34471 0 0 0 82897 110 0 0 25 0 1 0 488377860 151449600 34103 4294967295 134512640 134672761 3221224544 3221223560 1075353266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36975 34103 603 41 0 36934 0
vsize: 147900
[startup+840.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 34732 0 0 0 83897 111 0 0 25 0 1 0 488377860 152526848 34364 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37238 34364 603 41 0 37197 0
vsize: 148952
[startup+850.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 34968 0 0 0 84896 112 0 0 25 0 1 0 488377860 153481216 34600 4294967295 134512640 134672761 3221224544 3221223680 134565076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37471 34600 603 41 0 37430 0
vsize: 149884
[startup+860.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 35173 0 0 0 85895 113 0 0 25 0 1 0 488377860 154411008 34805 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37698 34805 603 41 0 37657 0
vsize: 150792
[startup+870.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 35378 0 0 0 86895 114 0 0 25 0 1 0 488377860 155209728 35010 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37893 35010 603 41 0 37852 0
vsize: 151572
[startup+880.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 35621 0 0 0 87894 114 0 0 25 0 1 0 488377860 156143616 35253 4294967295 134512640 134672761 3221224544 3221223648 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38121 35253 603 41 0 38080 0
vsize: 152484
[startup+890.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 35863 0 0 0 88894 115 0 0 25 0 1 0 488377860 157229056 35495 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38386 35495 603 41 0 38345 0
vsize: 153544
[startup+900.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 36096 0 0 0 89893 116 0 0 25 0 1 0 488377860 158171136 35728 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38616 35728 603 41 0 38575 0
vsize: 154464
[startup+910.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 36414 0 0 0 90892 117 0 0 25 0 1 0 488377860 159383552 36046 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38912 36046 603 41 0 38871 0
vsize: 155648
[startup+920.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 36660 0 0 0 91892 117 0 0 25 0 1 0 488377860 160448512 36292 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39172 36292 603 41 0 39131 0
vsize: 156688
[startup+930.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 36837 0 0 0 92892 117 0 0 25 0 1 0 488377860 161116160 36469 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39335 36469 603 41 0 39294 0
vsize: 157340
[startup+940.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 37004 0 0 0 93892 118 0 0 25 0 1 0 488377860 161787904 36636 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39499 36636 603 41 0 39458 0
vsize: 157996
[startup+950.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 37326 0 0 0 94891 119 0 0 25 0 1 0 488377860 163127296 36958 4294967295 134512640 134672761 3221224544 3221223712 134553589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39826 36958 603 41 0 39785 0
vsize: 159304
[startup+960.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 37572 0 0 0 95890 120 0 0 25 0 1 0 488377860 164208640 37204 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40090 37204 603 41 0 40049 0
vsize: 160360
[startup+970.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 37839 0 0 0 96890 120 0 0 25 0 1 0 488377860 165289984 37471 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40354 37471 603 41 0 40313 0
vsize: 161416
[startup+980.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 38097 0 0 0 97890 121 0 0 25 0 1 0 488377860 166363136 37729 4294967295 134512640 134672761 3221224544 3221223648 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40616 37729 603 41 0 40575 0
vsize: 162464
[startup+990.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 38412 0 0 0 98890 121 0 0 25 0 1 0 488377860 167579648 38044 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40913 38044 603 41 0 40872 0
vsize: 163652
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 38641 0 0 0 99889 122 0 0 25 0 1 0 488377860 168529920 38273 4294967295 134512640 134672761 3221224544 3221223696 134565058 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41145 38273 603 41 0 41104 0
vsize: 164580
[startup+1010.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 38862 0 0 0 100888 122 0 0 25 0 1 0 488377860 169476096 38494 4294967295 134512640 134672761 3221224544 3221223744 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41376 38494 603 41 0 41335 0
vsize: 165504
[startup+1020.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 39078 0 0 0 101888 123 0 0 25 0 1 0 488377860 170283008 38710 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41573 38710 603 41 0 41532 0
vsize: 166292
[startup+1030.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 39322 0 0 0 102887 124 0 0 25 0 1 0 488377860 171364352 38954 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41837 38954 603 41 0 41796 0
vsize: 167348
[startup+1040.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 39505 0 0 0 103887 124 0 0 25 0 1 0 488377860 172036096 39137 4294967295 134512640 134672761 3221224544 3221223728 134559041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42001 39137 603 41 0 41960 0
vsize: 168004
[startup+1050.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 39730 0 0 0 104886 125 0 0 25 0 1 0 488377860 172974080 39362 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42230 39362 603 41 0 42189 0
vsize: 168920
[startup+1060.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 39972 0 0 0 105886 126 0 0 25 0 1 0 488377860 173920256 39604 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42461 39604 603 41 0 42420 0
vsize: 169844
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14508
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 40244 0 0 0 106885 127 0 0 25 0 1 0 488377860 175136768 39876 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42758 39876 603 41 0 42717 0
vsize: 171032
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14561
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 40543 0 0 0 107884 128 0 0 25 0 1 0 488377860 176361472 40175 4294967295 134512640 134672761 3221224544 3221223728 134558761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43057 40175 603 41 0 43016 0
vsize: 172228
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14561
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 40792 0 0 0 108884 129 0 0 25 0 1 0 488377860 177307648 40424 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43288 40424 603 41 0 43247 0
vsize: 173152
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14561
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 41103 0 0 0 109883 130 0 0 25 0 1 0 488377860 178647040 40735 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43615 40735 603 41 0 43574 0
vsize: 174460
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14561
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 41432 0 0 0 110882 131 0 0 25 0 1 0 488377860 179994624 41064 4294967295 134512640 134672761 3221224544 3221223648 134559966 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43944 41064 603 41 0 43903 0
vsize: 175776
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14561
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 41732 0 0 0 111881 131 0 0 25 0 1 0 488377860 181215232 41364 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44242 41364 603 41 0 44201 0
vsize: 176968
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14561
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 42016 0 0 0 112881 132 0 0 25 0 1 0 488377860 182292480 41648 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44505 41648 603 41 0 44464 0
vsize: 178020
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14561
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 42279 0 0 0 113880 134 0 0 25 0 1 0 488377860 183369728 41911 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44768 41911 603 41 0 44727 0
vsize: 179072
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14563
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 42577 0 0 0 114879 135 0 0 25 0 1 0 488377860 184586240 42209 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45065 42209 603 41 0 45024 0
vsize: 180260
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14563
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 42844 0 0 0 115878 135 0 0 25 0 1 0 488377860 185790464 42476 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45359 42476 603 41 0 45318 0
vsize: 181436
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14563
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 43166 0 0 0 116878 136 0 0 25 0 1 0 488377860 186994688 42798 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45653 42798 603 41 0 45612 0
vsize: 182612
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14563
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 43485 0 0 0 117877 137 0 0 25 0 1 0 488377860 188354560 43117 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45985 43117 603 41 0 45944 0
vsize: 183940
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14563
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 43648 0 0 0 118877 137 0 0 25 0 1 0 488377860 189026304 43280 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46149 43280 603 41 0 46108 0
vsize: 184596
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 14563
Raw data (stat): 14508 (minisat+) R 14507 10720 10719 0 -1 0 43973 0 0 0 119876 138 0 0 25 0 1 0 488377860 190369792 43605 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46477 43605 603 41 0 46436 0
vsize: 185908
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 14563
Raw data (stat): 14508 (minisat+) Z 14507 10720 10719 0 -1 12 43975 0 0 0 119876 147 0 0 25 0 1 0 488377860 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.14
CPU time (s): 1200.24
CPU user time (s): 1198.77
CPU system time (s): 1.47078
CPU usage (%): 100.008
Max. virtual memory (Kb): 185908
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####