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/miplib/normalized-mps-v2-13-7-air04.opb
MD5SUM	eb0734273e24196dd14c6f237b52fa81
Bench Category	optimization, medium integers (OPTMEDINT)
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	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	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.119981
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 15826

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-04-21 05:50:52 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16645 boxname=wulflinc28 idbench=1281 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  eb0734273e24196dd14c6f237b52fa81  /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-air04.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-air04.opb
IDLAUNCH: 16645
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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	: 3
cpu MHz		: 451.077
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:        738692 kB
Buffers:         21236 kB
Cached:         247328 kB
SwapCached:        104 kB
Active:          55476 kB
Inactive:       215528 kB
HighTotal:      131008 kB
HighFree:        22848 kB
LowTotal:       903652 kB
LowFree:        715844 kB
SwapTotal:     2097640 kB
SwapFree:      2097068 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6056 kB
Slab:            19256 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 06:10:55 (client local time) WITH STATUS 0 IN 1200.42 SECONDS
stats: 16645 7 1200.42 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:   63
c ---[1640]---> BDD-cost:   23
c ---[1638]---> BDD-cost:   29
c ---[1636]---> BDD-cost:    0
c ---[1634]---> BDD-cost:   71
c ---[1632]---> BDD-cost:   55
c ---[1628]---> BDD-cost:   23
c ---[1626]---> BDD-cost:   47
c ---[1624]---> BDD-cost:  213
c ---[1622]---> BDD-cost:   75
c ---[1620]---> BDD-cost:   75
c ---[1618]---> BDD-cost:   55
c ---[1616]---> BDD-cost:   15
c ---[1614]---> BDD-cost:   87
c ---[1612]---> BDD-cost:   51
c ---[1610]---> BDD-cost:    1
c ---[1608]---> BDD-cost:    1
c ---[1606]---> BDD-cost:   23
c ---[1604]---> BDD-cost:   11
c ---[1602]---> BDD-cost:   39
c ---[1600]---> BDD-cost:   13
c ---[1598]---> BDD-cost:   57
c ---[1596]---> BDD-cost:  259
c ---[1594]---> BDD-cost:  189
c ---[1592]---> BDD-cost:  101
c ---[1588]---> BDD-cost:  137
c ---[1586]---> BDD-cost:  101
c ---[1582]---> BDD-cost:   37
c ---[1580]---> BDD-cost:  181
c ---[1578]---> BDD-cost:  283
c ---[1576]---> BDD-cost:   99
c ---[1574]---> BDD-cost:    1
c ---[1572]---> BDD-cost:  109
c ---[1570]---> BDD-cost:   75
c ---[1568]---> BDD-cost:  237
c ---[1566]---> BDD-cost:  119
c ---[1564]---> BDD-cost:  109
c ---[1562]---> BDD-cost:   83
c ---[1560]---> BDD-cost:   13
c ---[1558]---> BDD-cost:  157
c ---[1556]---> BDD-cost:  155
c ---[1554]---> BDD-cost:  109
c ---[1550]---> BDD-cost:   77
c ---[1548]---> BDD-cost:  133
c ---[1546]---> BDD-cost:  103
c ---[1544]---> BDD-cost:  115
c ---[1542]---> BDD-cost:  185
c ---[1540]---> BDD-cost:  203
c ---[1538]---> BDD-cost:  167
c ---[1536]---> BDD-cost:  135
c ---[1534]---> BDD-cost:    9
c ---[1532]---> BDD-cost:   85
c ---[1530]---> BDD-cost:  143
c ---[1528]---> BDD-cost:  135
c ---[1526]---> BDD-cost:   63
c ---[1524]---> BDD-cost:   51
c ---[1522]---> BDD-cost:  159
c ---[1520]---> BDD-cost:  155
c ---[1518]---> BDD-cost:  211
c ---[1516]---> BDD-cost:   75
c ---[1514]---> BDD-cost:   37
c ---[1512]---> BDD-cost:   87
c ---[1510]---> BDD-cost:   79
c ---[1508]---> BDD-cost:  109
c ---[1506]---> BDD-cost:  115
c ---[1504]---> BDD-cost:  247
c ---[1502]---> BDD-cost:  105
c ---[1500]---> BDD-cost:   59
c ---[1498]---> BDD-cost:   71
c ---[1496]---> BDD-cost:   61
c ---[1494]---> BDD-cost:   89
c ---[1492]---> BDD-cost:   91
c ---[1490]---> BDD-cost:  143
c ---[1488]---> BDD-cost:  111
c ---[1486]---> BDD-cost:   95
c ---[1484]---> BDD-cost:  169
c ---[1482]---> BDD-cost:  101
c ---[1480]---> BDD-cost:  151
c ---[1478]---> BDD-cost:   67
c ---[1476]---> BDD-cost:   45
c ---[1474]---> BDD-cost:   45
c ---[1472]---> BDD-cost:   45
c ---[1470]---> BDD-cost:   65
c ---[1468]---> BDD-cost:   95
c ---[1464]---> BDD-cost:   47
c ---[1460]---> BDD-cost:   29
c ---[1458]---> BDD-cost:   27
c ---[1456]---> BDD-cost:   11
c ---[1452]---> BDD-cost:   81
c ---[1450]---> BDD-cost:  233
c ---[1448]---> BDD-cost:  275
c ---[1446]---> BDD-cost:  289
c ---[1444]---> BDD-cost:  119
c ---[1442]---> BDD-cost:  145
c ---[1440]---> BDD-cost:  165
c ---[1438]---> BDD-cost:  239
c ---[1436]---> BDD-cost:  223
c ---[1434]---> BDD-cost:   59
c ---[1432]---> BDD-cost:   35
c ---[1430]---> BDD-cost:   93
c ---[1428]---> BDD-cost:   45
c ---[1426]---> BDD-cost:   73
c ---[1424]---> BDD-cost:   75
c ---[1422]---> BDD-cost:   63
c ---[1420]---> BDD-cost:   99
c ---[1416]---> BDD-cost:  187
c ---[1414]---> BDD-cost:   55
c ---[1412]---> BDD-cost:  107
c ---[1410]---> BDD-cost:   69
c ---[1408]---> BDD-cost:   13
c ---[1406]---> BDD-cost:    3
c ---[1404]---> BDD-cost:  149
c ---[1402]---> BDD-cost:  137
c ---[1400]---> BDD-cost:  195
c ---[1398]---> BDD-cost:   93
c ---[1396]---> BDD-cost:  157
c ---[1394]---> BDD-cost:  233
c ---[1392]---> BDD-cost:  223
c ---[1390]---> BDD-cost:  225
c ---[1388]---> BDD-cost:  247
c ---[1386]---> BDD-cost:  179
c ---[1384]---> BDD-cost:  225
c ---[1382]---> BDD-cost:  243
c ---[1380]---> BDD-cost:  199
c ---[1378]---> BDD-cost:   55
c ---[1376]---> BDD-cost:   57
c ---[1374]---> BDD-cost:   99
c ---[1372]---> BDD-cost:    9
c ---[1370]---> BDD-cost:    3
c ---[1368]---> BDD-cost:   23
c ---[1366]---> BDD-cost:   51
c ---[1364]---> BDD-cost:   25
c ---[1362]---> BDD-cost:   23
c ---[1360]---> BDD-cost:   27
c ---[1358]---> BDD-cost:   15
c ---[1356]---> BDD-cost:   37
c ---[1354]---> BDD-cost:   67
c ---[1352]---> BDD-cost:   67
c ---[1350]---> BDD-cost:  109
c ---[1346]---> BDD-cost:  211
c ---[1342]---> BDD-cost:   65
c ---[1340]---> BDD-cost:  117
c ---[1338]---> BDD-cost:   65
c ---[1336]---> BDD-cost:   65
c ---[1334]---> BDD-cost:   49
c ---[1332]---> BDD-cost:  439
c ---[1330]---> BDD-cost:  423
c ---[1328]---> BDD-cost:  287
c ---[1326]---> BDD-cost:  217
c ---[1324]---> BDD-cost:  195
c ---[1322]---> BDD-cost:   63
c ---[1320]---> BDD-cost:   53
c ---[1318]---> BDD-cost:  359
c ---[1316]---> BDD-cost:  353
c ---[1312]---> BDD-cost:  169
c ---[1310]---> BDD-cost:  139
c ---[1308]---> BDD-cost:  159
c ---[1306]---> BDD-cost:  223
c ---[1304]---> BDD-cost:  107
c ---[1302]---> BDD-cost:   75
c ---[1300]---> BDD-cost:  109
c ---[1298]---> BDD-cost:   93
c ---[1296]---> BDD-cost:   87
c ---[1294]---> BDD-cost:   87
c ---[1292]---> BDD-cost:    7
c ---[1288]---> BDD-cost:   73
c ---[1286]---> BDD-cost:   71
c ---[1284]---> BDD-cost:  107
c ---[1282]---> BDD-cost:   77
c ---[1280]---> BDD-cost:    3
c ---[1278]---> BDD-cost:  107
c ---[1276]---> BDD-cost:  131
c ---[1274]---> BDD-cost:  135
c ---[1272]---> BDD-cost:   65
c ---[1270]---> BDD-cost:  165
c ---[1268]---> BDD-cost:  123
c ---[1266]---> BDD-cost:    1
c ---[1264]---> BDD-cost:   87
c ---[1262]---> BDD-cost:  155
c ---[1260]---> BDD-cost:  167
c ---[1258]---> BDD-cost:  203
c ---[1256]---> BDD-cost:  231
c ---[1254]---> BDD-cost:  147
c ---[1252]---> BDD-cost:  135
c ---[1250]---> BDD-cost:   49
c ---[1248]---> BDD-cost:   31
c ---[1246]---> BDD-cost:   95
c ---[1244]---> BDD-cost:  325
c ---[1242]---> BDD-cost:  333
c ---[1240]---> BDD-cost:  173
c ---[1238]---> BDD-cost:  269
c ---[1236]---> BDD-cost:   31
c ---[1234]---> BDD-cost:  413
c ---[1232]---> BDD-cost:  313
c ---[1230]---> BDD-cost:  125
c ---[1228]---> BDD-cost:  113
c ---[1226]---> BDD-cost:  247
c ---[1224]---> BDD-cost:   57
c ---[1222]---> BDD-cost:  237
c ---[1220]---> BDD-cost:  159
c ---[1218]---> BDD-cost:  117
c ---[1216]---> BDD-cost:   43
c ---[1214]---> BDD-cost:  143
c ---[1212]---> BDD-cost:   65
c ---[1210]---> BDD-cost:  123
c ---[1208]---> BDD-cost:   61
c ---[1206]---> BDD-cost:  103
c ---[1204]---> BDD-cost:   85
c ---[1202]---> BDD-cost:   77
c ---[1200]---> BDD-cost:   57
c ---[1198]---> BDD-cost:  127
c ---[1196]---> BDD-cost:  157
c ---[1194]---> BDD-cost:  267
c ---[1192]---> BDD-cost:  223
c ---[1190]---> BDD-cost:  229
c ---[1188]---> BDD-cost:  257
c ---[1186]---> BDD-cost:  241
c ---[1184]---> BDD-cost:  195
c ---[1182]---> BDD-cost:   49
c ---[1180]---> BDD-cost:  117
c ---[1178]---> BDD-cost:  197
c ---[1176]---> BDD-cost:  171
c ---[1174]---> BDD-cost:  287
c ---[1172]---> BDD-cost:   75
c ---[1170]---> BDD-cost:  215
c ---[1168]---> BDD-cost:  119
c ---[1166]---> BDD-cost:  245
c ---[1164]---> BDD-cost:  257
c ---[1162]---> BDD-cost:  279
c ---[1160]---> BDD-cost:  227
c ---[1158]---> BDD-cost:  201
c ---[1156]---> BDD-cost:  143
c ---[1154]---> BDD-cost:  207
c ---[1152]---> BDD-cost:  131
c ---[1150]---> BDD-cost:  245
c ---[1148]---> BDD-cost:  115
c ---[1146]---> BDD-cost:   91
c ---[1144]---> BDD-cost:   43
c ---[1142]---> BDD-cost:   39
c ---[1140]---> BDD-cost:   91
c ---[1138]---> BDD-cost:  179
c ---[1136]---> BDD-cost:   73
c ---[1134]---> BDD-cost:   29
c ---[1132]---> BDD-cost:  163
c ---[1130]---> BDD-cost:   81
c ---[1128]---> BDD-cost:   63
c ---[1126]---> BDD-cost:  103
c ---[1124]---> BDD-cost:  113
c ---[1122]---> BDD-cost:  115
c ---[1120]---> BDD-cost:   19
c ---[1118]---> BDD-cost:   93
c ---[1116]---> BDD-cost:   99
c ---[1114]---> BDD-cost:   99
c ---[1112]---> BDD-cost:  103
c ---[1110]---> BDD-cost:   67
c ---[1108]---> BDD-cost:   23
c ---[1106]---> BDD-cost:   85
c ---[1104]---> BDD-cost:   87
c ---[1102]---> BDD-cost:    7
c ---[1100]---> BDD-cost:   45
c ---[1098]---> BDD-cost:   43
c ---[1096]---> BDD-cost:   11
c ---[1094]---> BDD-cost:   59
c ---[1092]---> BDD-cost:  185
c ---[1090]---> BDD-cost:  249
c ---[1088]---> BDD-cost:  315
c ---[1086]---> BDD-cost:  253
c ---[1084]---> BDD-cost:  161
c ---[1082]---> BDD-cost:  257
c ---[1080]---> BDD-cost:  167
c ---[1078]---> BDD-cost:  167
c ---[1076]---> BDD-cost:  141
c ---[1074]---> BDD-cost:   21
c ---[1072]---> BDD-cost:   10
c ---[1070]---> BDD-cost:   95
c ---[1068]---> BDD-cost:  141
c ---[1066]---> BDD-cost:  123
c ---[1064]---> BDD-cost:   83
c ---[1062]---> BDD-cost:   55
c ---[1060]---> BDD-cost:  183
c ---[1058]---> BDD-cost:  269
c ---[1056]---> BDD-cost:   63
c ---[1054]---> BDD-cost:   45
c ---[1052]---> BDD-cost:   39
c ---[1050]---> BDD-cost:   97
c ---[1048]---> BDD-cost:   51
c ---[1046]---> BDD-cost:   45
c ---[1044]---> BDD-cost:   17
c ---[1042]---> BDD-cost:   85
c ---[1040]---> BDD-cost:   35
c ---[1038]---> BDD-cost:   53
c ---[1036]---> BDD-cost:   21
c ---[1034]---> BDD-cost:  115
c ---[1032]---> BDD-cost:   99
c ---[1030]---> BDD-cost:   63
c ---[1028]---> BDD-cost:   77
c ---[1026]---> BDD-cost:  139
c ---[1024]---> BDD-cost:  109
c ---[1022]---> BDD-cost:  407
c ---[1020]---> BDD-cost:  323
c ---[1018]---> BDD-cost:  109
c ---[1016]---> BDD-cost:   93
c ---[1014]---> BDD-cost:   51
c ---[1012]---> BDD-cost:   79
c ---[1010]---> BDD-cost:   75
c ---[1008]---> BDD-cost:  147
c ---[1006]---> BDD-cost:  169
c ---[1004]---> BDD-cost:  209
c ---[1002]---> BDD-cost:   69
c ---[1000]---> BDD-cost:   51
c ---[ 998]---> BDD-cost:   85
c ---[ 994]---> BDD-cost:  103
c ---[ 992]---> BDD-cost:  127
c ---[ 990]---> BDD-cost:   77
c ---[ 988]---> BDD-cost:   77
c ---[ 986]---> BDD-cost:  141
c ---[ 984]---> BDD-cost:   89
c ---[ 982]---> BDD-cost:   85
c ---[ 980]---> BDD-cost:  119
c ---[ 978]---> BDD-cost:   69
c ---[ 976]---> BDD-cost:   57
c ---[ 974]---> BDD-cost:   65
c ---[ 972]---> BDD-cost:   47
c ---[ 970]---> BDD-cost:   61
c ---[ 968]---> BDD-cost:   31
c ---[ 964]---> BDD-cost:  183
c ---[ 962]---> BDD-cost:  121
c ---[ 960]---> BDD-cost:   89
c ---[ 958]---> BDD-cost:  225
c ---[ 956]---> BDD-cost:  267
c ---[ 952]---> BDD-cost:  159
c ---[ 950]---> BDD-cost:  209
c ---[ 948]---> BDD-cost:   71
c ---[ 946]---> BDD-cost:  237
c ---[ 944]---> BDD-cost:  129
c ---[ 942]---> BDD-cost:  365
c ---[ 940]---> BDD-cost:  369
c ---[ 938]---> BDD-cost:  129
c ---[ 936]---> BDD-cost:  101
c ---[ 934]---> BDD-cost:  289
c ---[ 932]---> BDD-cost:  279
c ---[ 930]---> BDD-cost:  345
c ---[ 928]---> BDD-cost:   81
c ---[ 926]---> BDD-cost:   69
c ---[ 924]---> BDD-cost:   83
c ---[ 922]---> BDD-cost:   53
c ---[ 920]---> BDD-cost:   67
c ---[ 918]---> BDD-cost:   55
c ---[ 916]---> BDD-cost:  145
c ---[ 914]---> BDD-cost:  149
c ---[ 912]---> BDD-cost:  105
c ---[ 910]---> BDD-cost:   19
c ---[ 908]---> BDD-cost:  105
c ---[ 906]---> BDD-cost:  101
c ---[ 904]---> BDD-cost:  147
c ---[ 902]---> BDD-cost:  231
c ---[ 900]---> BDD-cost:  191
c ---[ 898]---> BDD-cost:  157
c ---[ 896]---> BDD-cost:  249
c ---[ 894]---> BDD-cost:  385
c ---[ 892]---> BDD-cost:   67
c ---[ 890]---> BDD-cost:   71
c ---[ 888]---> BDD-cost:   47
c ---[ 886]---> BDD-cost:  147
c ---[ 884]---> BDD-cost:  139
c ---[ 882]---> BDD-cost:  273
c ---[ 880]---> BDD-cost:  213
c ---[ 878]---> BDD-cost:  169
c ---[ 876]---> BDD-cost:  239
c ---[ 874]---> BDD-cost:  305
c ---[ 872]---> BDD-cost:  109
c ---[ 870]---> BDD-cost:  105
c ---[ 868]---> BDD-cost:  147
c ---[ 866]---> BDD-cost:  115
c ---[ 864]---> BDD-cost:  115
c ---[ 862]---> BDD-cost:   67
c ---[ 860]---> BDD-cost:  329
c ---[ 858]---> BDD-cost:  295
c ---[ 856]---> BDD-cost:   51
c ---[ 854]---> BDD-cost:   61
c ---[ 852]---> BDD-cost:  317
c ---[ 850]---> BDD-cost:   97
c ---[ 848]---> BDD-cost:   79
c ---[ 846]---> BDD-cost:   43
c ---[ 844]---> BDD-cost:   85
c ---[ 842]---> BDD-cost:   35
c ---[ 840]---> BDD-cost:   69
c ---[ 836]---> BDD-cost:   45
c ---[ 834]---> BDD-cost:   73
c ---[ 832]---> BDD-cost:   55
c ---[ 828]---> BDD-cost:   33
c ---[ 826]---> BDD-cost:   29
c ---[ 824]---> BDD-cost:  245
c ---[ 822]---> BDD-cost:  225
c ---[ 820]---> BDD-cost:  111
c ---[ 818]---> BDD-cost:  117
c ---[ 816]---> BDD-cost:  127
c ---[ 814]---> BDD-cost:  129
c ---[ 812]---> BDD-cost:  259
c ---[ 810]---> BDD-cost:  221
c ---[ 808]---> BDD-cost:  275
c ---[ 806]---> BDD-cost:  209
c ---[ 804]---> BDD-cost:  267
c ---[ 802]---> BDD-cost:  171
c ---[ 800]---> BDD-cost:   57
c ---[ 796]---> BDD-cost:  133
c ---[ 794]---> BDD-cost:  185
c ---[ 792]---> BDD-cost:  169
c ---[ 790]---> BDD-cost:  287
c ---[ 788]---> BDD-cost:   81
c ---[ 786]---> BDD-cost:  335
c ---[ 784]---> BDD-cost:  365
c ---[ 782]---> BDD-cost:  255
c ---[ 780]---> BDD-cost:  111
c ---[ 778]---> BDD-cost:   57
c ---[ 776]---> BDD-cost:  101
c ---[ 774]---> BDD-cost:  197
c ---[ 772]---> BDD-cost:  383
c ---[ 770]---> BDD-cost:  329
c ---[ 768]---> BDD-cost:  241
c ---[ 766]---> BDD-cost:  129
c ---[ 764]---> BDD-cost:   85
c ---[ 762]---> BDD-cost:   71
c ---[ 760]---> BDD-cost:   37
c ---[ 758]---> BDD-cost:   77
c ---[ 756]---> BDD-cost:   49
c ---[ 754]---> BDD-cost:  133
c ---[ 752]---> BDD-cost:  133
c ---[ 750]---> BDD-cost:  377
c ---[ 748]---> BDD-cost:  117
c ---[ 744]---> BDD-cost:  119
c ---[ 742]---> BDD-cost:  119
c ---[ 740]---> BDD-cost:  151
c ---[ 738]---> BDD-cost:  221
c ---[ 736]---> BDD-cost:  181
c ---[ 732]---> BDD-cost:   87
c ---[ 730]---> BDD-cost:  127
c ---[ 728]---> BDD-cost:  299
c ---[ 726]---> BDD-cost:  331
c ---[ 722]---> BDD-cost:   21
c ---[ 720]---> BDD-cost:  205
c ---[ 718]---> BDD-cost:  217
c ---[ 716]---> BDD-cost:  349
c ---[ 714]---> BDD-cost:  291
c ---[ 712]---> BDD-cost:  165
c ---[ 710]---> BDD-cost:  161
c ---[ 708]---> BDD-cost:   61
c ---[ 706]---> BDD-cost:   55
c ---[ 704]---> BDD-cost:  113
c ---[ 702]---> BDD-cost:   23
c ---[ 700]---> BDD-cost:  189
c ---[ 698]---> BDD-cost:  157
c ---[ 696]---> BDD-cost:  149
c ---[ 694]---> BDD-cost:  139
c ---[ 692]---> BDD-cost:  165
c ---[ 690]---> BDD-cost:  181
c ---[ 688]---> BDD-cost:  253
c ---[ 686]---> BDD-cost:   43
c ---[ 684]---> BDD-cost:  145
c ---[ 682]---> BDD-cost:  141
c ---[ 680]---> BDD-cost:  105
c ---[ 678]---> BDD-cost:   95
c ---[ 676]---> BDD-cost:   75
c ---[ 674]---> BDD-cost:  103
c ---[ 672]---> BDD-cost:  149
c ---[ 670]---> BDD-cost:  137
c ---[ 668]---> BDD-cost:   59
c ---[ 666]---> BDD-cost:    5
c ---[ 664]---> BDD-cost:   35
c ---[ 662]---> BDD-cost:    9
c ---[ 660]---> BDD-cost:   35
c ---[ 658]---> BDD-cost:   47
c ---[ 654]---> BDD-cost:   55
c ---[ 652]---> BDD-cost:  197
c ---[ 650]---> BDD-cost:  191
c ---[ 648]---> BDD-cost:  125
c ---[ 646]---> BDD-cost:  173
c ---[ 642]---> BDD-cost:   93
c ---[ 640]---> BDD-cost:   29
c ---[ 638]---> BDD-cost:  321
c ---[ 636]---> BDD-cost:  195
c ---[ 634]---> BDD-cost:  163
c ---[ 628]---> BDD-cost:  151
c ---[ 626]---> BDD-cost:  253
c ---[ 624]---> BDD-cost:  381
c ---[ 622]---> BDD-cost:  345
c ---[ 620]---> BDD-cost:  185
c ---[ 616]---> BDD-cost:   83
c ---[ 614]---> BDD-cost:   69
c ---[ 612]---> BDD-cost:   51
c ---[ 610]---> BDD-cost:   47
c ---[ 608]---> BDD-cost:   59
c ---[ 606]---> BDD-cost:   83
c ---[ 604]---> BDD-cost:  107
c ---[ 602]---> BDD-cost:  363
c ---[ 600]---> BDD-cost:  103
c ---[ 598]---> BDD-cost:  277
c ---[ 596]---> BDD-cost:  341
c ---[ 594]---> BDD-cost:  213
c ---[ 592]---> BDD-cost:  315
c ---[ 590]---> BDD-cost:  275
c ---[ 588]---> BDD-cost:  151
c ---[ 586]---> BDD-cost:  111
c ---[ 584]---> BDD-cost:  103
c ---[ 582]---> BDD-cost:   75
c ---[ 580]---> BDD-cost:   27
c ---[ 578]---> BDD-cost:   21
c ---[ 576]---> BDD-cost:   11
c ---[ 574]---> BDD-cost:   31
c ---[ 570]---> BDD-cost:   19
c ---[ 566]---> BDD-cost:  149
c ---[ 564]---> BDD-cost:   97
c ---[ 562]---> BDD-cost:  149
c ---[ 560]---> BDD-cost:  395
c ---[ 558]---> BDD-cost:   25
c ---[ 556]---> BDD-cost:  389
c ---[ 554]---> BDD-cost:  251
c ---[ 552]---> BDD-cost:  375
c ---[ 550]---> BDD-cost:  343
c ---[ 548]---> BDD-cost:  267
c ---[ 546]---> BDD-cost:  135
c ---[ 544]---> BDD-cost:  263
c ---[ 542]---> BDD-cost:  259
c ---[ 540]---> BDD-cost:  245
c ---[ 538]---> BDD-cost:   45
c ---[ 536]---> BDD-cost:   41
c ---[ 534]---> BDD-cost:  127
c ---[ 532]---> BDD-cost:  117
c ---[ 530]---> BDD-cost:   53
c ---[ 528]---> BDD-cost:  149
c ---[ 526]---> BDD-cost:  103
c ---[ 524]---> BDD-cost:  215
c ---[ 522]---> BDD-cost:   89
c ---[ 520]---> BDD-cost:  177
c ---[ 518]---> BDD-cost:  343
c ---[ 516]---> BDD-cost:  237
c ---[ 514]---> BDD-cost:  177
c ---[ 512]---> BDD-cost:   85
c ---[ 510]---> BDD-cost:  267
c ---[ 508]---> BDD-cost:  225
c ---[ 506]---> BDD-cost:  109
c ---[ 504]---> BDD-cost:  105
c ---[ 502]---> BDD-cost:  113
c ---[ 500]---> BDD-cost:   55
c ---[ 498]---> BDD-cost:  117
c ---[ 496]---> BDD-cost:   83
c ---[ 494]---> BDD-cost:   79
c ---[ 492]---> BDD-cost:   81
c ---[ 490]---> BDD-cost:  263
c ---[ 488]---> BDD-cost:  179
c ---[ 486]---> BDD-cost:  281
c ---[ 484]---> BDD-cost:  389
c ---[ 482]---> BDD-cost:  333
c ---[ 480]---> BDD-cost:  357
c ---[ 478]---> BDD-cost:  345
c ---[ 476]---> BDD-cost:  263
c ---[ 474]---> BDD-cost:   89
c ---[ 472]---> BDD-cost:  285
c ---[ 468]---> BDD-cost:  419
c ---[ 466]---> BDD-cost:  357
c ---[ 464]---> BDD-cost:  473
c ---[ 462]---> BDD-cost:  455
c ---[ 460]---> BDD-cost:  405
c ---[ 458]---> BDD-cost:  241
c ---[ 456]---> BDD-cost:  211
c ---[ 454]---> BDD-cost:  313
c ---[ 452]---> BDD-cost:  371
c ---[ 450]---> BDD-cost:  389
c ---[ 448]---> BDD-cost:  223
c ---[ 446]---> BDD-cost:  221
c ---[ 444]---> BDD-cost:  147
c ---[ 442]---> BDD-cost:  131
c ---[ 440]---> BDD-cost:  185
c ---[ 438]---> BDD-cost:  141
c ---[ 436]---> BDD-cost:  249
c ---[ 434]---> BDD-cost:  261
c ---[ 432]---> BDD-cost:  311
c ---[ 430]---> BDD-cost:  261
c ---[ 428]---> BDD-cost:  387
c ---[ 426]---> BDD-cost:  247
c ---[ 424]---> BDD-cost:  295
c ---[ 422]---> BDD-cost:   31
c ---[ 420]---> BDD-cost:  355
c ---[ 418]---> BDD-cost:  135
c ---[ 416]---> BDD-cost:  443
c ---[ 414]---> BDD-cost:  653
c ---[ 412]---> BDD-cost:  703
c ---[ 410]---> BDD-cost:  517
c ---[ 408]---> BDD-cost:  441
c ---[ 406]---> BDD-cost:  411
c ---[ 404]---> BDD-cost:  289
c ---[ 402]---> BDD-cost:  277
c ---[ 400]---> BDD-cost:  239
c ---[ 398]---> BDD-cost:  201
c ---[ 396]---> BDD-cost:  309
c ---[ 394]---> BDD-cost:  287
c ---[ 392]---> BDD-cost:  177
c ---[ 390]---> BDD-cost:  143
c ---[ 388]---> BDD-cost:  131
c ---[ 386]---> BDD-cost:   35
c ---[ 384]---> BDD-cost:  189
c ---[ 382]---> BDD-cost:  219
c ---[ 378]---> BDD-cost:  267
c ---[ 376]---> BDD-cost:  135
c ---[ 374]---> BDD-cost:   69
c ---[ 372]---> BDD-cost:   75
c ---[ 370]---> BDD-cost:   51
c ---[ 368]---> BDD-cost:  117
c ---[ 366]---> BDD-cost:  117
c ---[ 360]---> BDD-cost:  189
c ---[ 358]---> BDD-cost:   73
c ---[ 356]---> BDD-cost:   55
c ---[ 354]---> BDD-cost:   57
c ---[ 352]---> BDD-cost:   91
c ---[ 350]---> BDD-cost:  325
c ---[ 348]---> BDD-cost:  223
c ---[ 346]---> BDD-cost:   57
c ---[ 344]---> BDD-cost:   43
c ---[ 342]---> BDD-cost:  255
c ---[ 340]---> BDD-cost:  285
c ---[ 338]---> BDD-cost:  187
c ---[ 336]---> BDD-cost:   37
c ---[ 334]---> BDD-cost:   91
c ---[ 332]---> BDD-cost:  211
c ---[ 330]---> BDD-cost:  159
c ---[ 328]---> BDD-cost:   97
c ---[ 326]---> BDD-cost:   27
c ---[ 324]---> BDD-cost:  101
c ---[ 322]---> BDD-cost:  141
c ---[ 318]---> BDD-cost:  109
c ---[ 316]---> BDD-cost:  321
c ---[ 314]---> BDD-cost:  305
c ---[ 312]---> BDD-cost:  603
c ---[ 310]---> BDD-cost:  441
c ---[ 308]---> BDD-cost:  391
c ---[ 306]---> BDD-cost:  387
c ---[ 304]---> BDD-cost:  289
c ---[ 302]---> BDD-cost:  219
c ---[ 300]---> BDD-cost:  309
c ---[ 298]---> BDD-cost:  241
c ---[ 296]---> BDD-cost:  197
c ---[ 294]---> BDD-cost:  279
c ---[ 292]---> BDD-cost:  167
c ---[ 290]---> BDD-cost:  151
c ---[ 288]---> BDD-cost:   49
c ---[ 286]---> BDD-cost:   31
c ---[ 284]---> BDD-cost:  107
c ---[ 282]---> BDD-cost:   55
c ---[ 278]---> BDD-cost:  177
c ---[ 276]---> BDD-cost:  223
c ---[ 274]---> BDD-cost:  119
c ---[ 272]---> BDD-cost:  137
c ---[ 270]---> BDD-cost:  105
c ---[ 268]---> BDD-cost:  183
c ---[ 266]---> BDD-cost:  179
c ---[ 264]---> BDD-cost:  285
c ---[ 262]---> BDD-cost:  191
c ---[ 260]---> BDD-cost:  177
c ---[ 258]---> BDD-cost:  145
c ---[ 254]---> BDD-cost:  153
c ---[ 252]---> BDD-cost:  121
c ---[ 250]---> BDD-cost:   95
c ---[ 246]---> BDD-cost:  111
c ---[ 244]---> BDD-cost:  281
c ---[ 242]---> BDD-cost:  265
c ---[ 240]---> BDD-cost:  167
c ---[ 238]---> BDD-cost:  151
c ---[ 236]---> BDD-cost:  167
c ---[ 234]---> BDD-cost:  137
c ---[ 230]---> BDD-cost:  375
c ---[ 228]---> BDD-cost:  287
c ---[ 226]---> BDD-cost:  249
c ---[ 224]---> BDD-cost:  131
c ---[ 222]---> BDD-cost:  187
c ---[ 220]---> BDD-cost:  135
c ---[ 218]---> BDD-cost:  129
c ---[ 216]---> BDD-cost:  317
c ---[ 214]---> BDD-cost:  365
c ---[ 212]---> BDD-cost:  235
c ---[ 210]---> BDD-cost:  249
c ---[ 208]---> BDD-cost:  283
c ---[ 206]---> BDD-cost:  233
c ---[ 204]---> BDD-cost:  259
c ---[ 202]---> BDD-cost:  287
c ---[ 200]---> BDD-cost:  175
c ---[ 198]---> BDD-cost:  233
c ---[ 196]---> BDD-cost:  167
c ---[ 194]---> BDD-cost:  159
c ---[ 192]---> BDD-cost:   47
c ---[ 188]---> BDD-cost:  135
c ---[ 186]---> BDD-cost:  147
c ---[ 184]---> BDD-cost:  167
c ---[ 182]---> BDD-cost:  203
c ---[ 180]---> BDD-cost:  275
c ---[ 178]---> BDD-cost:  263
c ---[ 176]---> BDD-cost:   31
c ---[ 174]---> BDD-cost:   11
c ---[ 172]---> BDD-cost:   31
c ---[ 170]---> BDD-cost:   27
c ---[ 168]---> BDD-cost:  225
c ---[ 166]---> BDD-cost:   65
c ---[ 164]---> BDD-cost:  385
c ---[ 162]---> BDD-cost:  361
c ---[ 160]---> BDD-cost:   73
c ---[ 158]---> BDD-cost:   77
c ---[ 154]---> BDD-cost:  131
c ---[ 152]---> BDD-cost:  145
c ---[ 150]---> BDD-cost:  121
c ---[ 148]---> BDD-cost:  117
c ---[ 146]---> BDD-cost:  111
c ---[ 144]---> BDD-cost:  123
c ---[ 142]---> BDD-cost:  125
c ---[ 140]---> BDD-cost:  243
c ---[ 138]---> BDD-cost:  143
c ---[ 136]---> BDD-cost:  149
c ---[ 134]---> BDD-cost:  103
c ---[ 132]---> BDD-cost:  155
c ---[ 130]---> BDD-cost:  247
c ---[ 128]---> BDD-cost:  143
c ---[ 126]---> BDD-cost:   91
c ---[ 124]---> BDD-cost:   81
c ---[ 122]---> BDD-cost:   79
c ---[ 120]---> BDD-cost:  117
c ---[ 118]---> BDD-cost:   89
c ---[ 116]---> BDD-cost:   61
c ---[ 114]---> BDD-cost:  127
c ---[ 112]---> BDD-cost:  135
c ---[ 110]---> BDD-cost:  161
c ---[ 108]---> BDD-cost:  141
c ---[ 106]---> BDD-cost:  437
c ---[ 104]---> BDD-cost:  309
c ---[ 102]---> BDD-cost:  173
c ---[ 100]---> BDD-cost:  441
c ---[  98]---> BDD-cost:  489
c ---[  96]---> BDD-cost:  299
c ---[  94]---> BDD-cost:  455
c ---[  92]---> BDD-cost:  333
c ---[  90]---> BDD-cost:  421
c ---[  88]---> BDD-cost:  375
c ---[  86]---> BDD-cost:  433
c ---[  84]---> BDD-cost:  405
c ---[  82]---> BDD-cost:  333
c ---[  80]---> BDD-cost:  673
c ---[  78]---> BDD-cost:  685
c ---[  76]---> BDD-cost:  385
c ---[  74]---> BDD-cost:  267
c ---[  72]---> BDD-cost:  345
c ---[  70]---> BDD-cost:  365
c ---[  68]---> BDD-cost:  391
c ---[  66]---> BDD-cost:  313
c ---[  64]---> BDD-cost:  275
c ---[  62]---> BDD-cost:  257
c ---[  60]---> BDD-cost:  203
c ---[  58]---> BDD-cost:  311
c ---[  56]---> BDD-cost:  227
c ---[  54]---> BDD-cost:  295
c ---[  52]---> BDD-cost:  233
c ---[  50]---> BDD-cost:  247
c ---[  46]---> BDD-cost:  237
c ---[  44]---> BDD-cost:  149
c ---[  40]---> BDD-cost:   99
c ---[  38]---> BDD-cost:   85
c ---[  36]---> BDD-cost:  109
c ---[  34]---> BDD-cost:   43
c ---[  32]---> BDD-cost:   83
c ---[  30]---> BDD-cost:   71
c ---[  28]---> BDD-cost:   67
c ---[  26]---> BDD-cost:  151
c ---[  24]---> BDD-cost:  147
c ---[  22]---> BDD-cost:  177
c ---[  20]---> BDD-cost:  127
c ---[  18]---> BDD-cost:  131
c ---[  16]---> BDD-cost:  147
c ---[  14]---> BDD-cost:  215
c ---[  12]---> BDD-cost:  181
c ---[  10]---> BDD-cost:  235
c ---[   8]---> BDD-cost:  163
c ---[   6]---> BDD-cost:   57
c ---[   4]---> BDD-cost:   59
c ---[   2]---> BDD-cost:  139
c ---[   0]---> BDD-cost:   39
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  310358   807732 |  103452       0        0     nan |  0.000 % |
c |       100 |  310358   807732 |  113797     100     2792    27.9 |  0.588 % |
c |       250 |  310331   807657 |  125176     249    12761    51.2 |  0.592 % |
c |       475 |  310198   807286 |  137694     459    35376    77.1 |  0.620 % |
c |       812 |  310052   806901 |  151464     787    48598    61.8 |  0.642 % |
c |      1319 |  309884   806468 |  166610    1289    73251    56.8 |  0.667 % |
c |      2078 |  309785   806192 |  183271    2043   141139    69.1 |  0.692 % |
c |      3217 |  309724   806017 |  201598    3171   279873    88.3 |  0.705 % |
c |      4927 |  309614   805741 |  221758    4872   562380   115.4 |  0.716 % |
c |      7490 |  309614   805741 |  243934    7435  1259451   169.4 |  0.716 % |
c |     11334 |  309475   805377 |  268327   11239  1793736   159.6 |  0.732 % |
c |     17101 |  309226   804713 |  295160   16957  2478519   146.2 |  0.776 % |
c |     25752 |  307768   801003 |  324676   25505  3930547   154.1 |  0.987 % |
c |     38728 |  307515   800363 |  357144   38421  6348349   165.2 |  1.003 % |
c |     58191 |  307356   799958 |  392858   57785 10148314   175.6 |  1.017 % |
c |     87385 |  306886   798753 |  432144   86840 17512694   201.7 |  1.062 % |
c |    131176 |  306715   798313 |  475359  130557 31984227   245.0 |  1.079 % |
#### 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.93 2/54 19905
Raw data (stat): 19905 (runsolver) R 19904 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542700127 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0016 s]
Raw data (loadavg): 0.93 0.96 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 11064 0 0 0 971 27 0 0 25 0 1 0 542700127 54525952 10706 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13312 10706 603 41 0 13271 0
vsize: 53248
[startup+20.002 s]
Raw data (loadavg): 0.94 0.96 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 11315 0 0 0 1970 28 0 0 25 0 1 0 542700127 55472128 10957 4294967295 134512640 134672761 3221224624 3221223728 134559869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13543 10957 603 41 0 13502 0
vsize: 54172
[startup+30.0015 s]
Raw data (loadavg): 0.95 0.96 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 11721 0 0 0 2969 30 0 0 25 0 1 0 542700127 57221120 11363 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13970 11363 603 41 0 13929 0
vsize: 55880
[startup+40.0024 s]
Raw data (loadavg): 0.96 0.96 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 12367 0 0 0 3967 31 0 0 25 0 1 0 542700127 59777024 12009 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14594 12009 603 41 0 14553 0
vsize: 58376
[startup+50.0031 s]
Raw data (loadavg): 0.96 0.96 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 12751 0 0 0 4966 33 0 0 25 0 1 0 542700127 61390848 12393 4294967295 134512640 134672761 3221224624 3221223824 134557959 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14988 12393 603 41 0 14947 0
vsize: 59952
[startup+60.0035 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 13042 0 0 0 5964 34 0 0 25 0 1 0 542700127 62607360 12684 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15285 12684 603 41 0 15244 0
vsize: 61140
[startup+70.0044 s]
Raw data (loadavg): 0.97 0.96 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 13331 0 0 0 6964 36 0 0 25 0 1 0 542700127 63815680 12973 4294967295 134512640 134672761 3221224624 3221223668 1075755419 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15580 12973 603 41 0 15539 0
vsize: 62320
[startup+80.0041 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 13570 0 0 0 7963 36 0 0 25 0 1 0 542700127 64761856 13212 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15811 13212 603 41 0 15770 0
vsize: 63244
[startup+90.0045 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 13931 0 0 0 8962 37 0 0 25 0 1 0 542700127 66322432 13573 4294967295 134512640 134672761 3221224624 3221223808 134558362 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16192 13573 603 41 0 16151 0
vsize: 64768
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 14239 0 0 0 9961 39 0 0 25 0 1 0 542700127 67534848 13881 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16488 13881 603 41 0 16447 0
vsize: 65952
[startup+110.005 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 14656 0 0 0 10961 39 0 0 25 0 1 0 542700127 69152768 14298 4294967295 134512640 134672761 3221224624 3221223792 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16883 14298 603 41 0 16842 0
vsize: 67532
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 14999 0 0 0 11960 40 0 0 25 0 1 0 542700127 70631424 14641 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17244 14641 603 41 0 17203 0
vsize: 68976
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 15286 0 0 0 12959 41 0 0 25 0 1 0 542700127 71843840 14928 4294967295 134512640 134672761 3221224624 3221223748 134566092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17540 14928 603 41 0 17499 0
vsize: 70160
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 15576 0 0 0 13959 42 0 0 25 0 1 0 542700127 72921088 15218 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17803 15218 603 41 0 17762 0
vsize: 71212
[startup+150.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 15978 0 0 0 14957 43 0 0 25 0 1 0 542700127 74543104 15620 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18199 15620 603 41 0 18158 0
vsize: 72796
[startup+160.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 16292 0 0 0 15957 44 0 0 25 0 1 0 542700127 75886592 15934 4294967295 134512640 134672761 3221224624 3221223792 134560828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18527 15934 603 41 0 18486 0
vsize: 74108
[startup+170.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 16609 0 0 0 16956 45 0 0 25 0 1 0 542700127 77103104 16251 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18824 16251 603 41 0 18783 0
vsize: 75296
[startup+180.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 16898 0 0 0 17955 46 0 0 25 0 1 0 542700127 78446592 16540 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19152 16540 603 41 0 19111 0
vsize: 76608
[startup+190.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 17251 0 0 0 18955 47 0 0 25 0 1 0 542700127 79929344 16893 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19514 16893 603 41 0 19473 0
vsize: 78056
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 17614 0 0 0 19954 48 0 0 25 0 1 0 542700127 81399808 17256 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19873 17256 603 41 0 19832 0
vsize: 79492
[startup+210.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 17980 0 0 0 20953 48 0 0 25 0 1 0 542700127 82878464 17622 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20234 17622 603 41 0 20193 0
vsize: 80936
[startup+220.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 18192 0 0 0 21952 49 0 0 25 0 1 0 542700127 83689472 17834 4294967295 134512640 134672761 3221224624 3221223728 134559902 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20432 17834 603 41 0 20391 0
vsize: 81728
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 18419 0 0 0 22952 50 0 0 25 0 1 0 542700127 84631552 18061 4294967295 134512640 134672761 3221224624 3221223580 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20662 18061 603 41 0 20621 0
vsize: 82648
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 18839 0 0 0 23951 51 0 0 25 0 1 0 542700127 86384640 18481 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21090 18481 603 41 0 21049 0
vsize: 84360
[startup+250.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 19199 0 0 0 24951 51 0 0 25 0 1 0 542700127 87744512 18841 4294967295 134512640 134672761 3221224624 3221223760 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21422 18841 603 41 0 21381 0
vsize: 85688
[startup+260.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 19640 0 0 0 25950 53 0 0 25 0 1 0 542700127 89628672 19282 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21882 19282 603 41 0 21841 0
vsize: 87528
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.93 3/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 19933 0 0 0 26950 53 0 0 25 0 1 0 542700127 90841088 19575 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22178 19575 603 41 0 22137 0
vsize: 88712
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 20102 0 0 0 27949 53 0 0 25 0 1 0 542700127 91516928 19744 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22343 19744 603 41 0 22302 0
vsize: 89372
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 20395 0 0 0 28948 54 0 0 25 0 1 0 542700127 92741632 20037 4294967295 134512640 134672761 3221224624 3221223728 134559916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22642 20037 603 41 0 22601 0
vsize: 90568
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 20704 0 0 0 29948 55 0 0 25 0 1 0 542700127 93954048 20346 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22938 20346 603 41 0 22897 0
vsize: 91752
[startup+310.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 21091 0 0 0 30947 57 0 0 25 0 1 0 542700127 95576064 20733 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23334 20733 603 41 0 23293 0
vsize: 93336
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 21357 0 0 0 31946 58 0 0 25 0 1 0 542700127 96657408 20999 4294967295 134512640 134672761 3221224624 3221223792 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23598 20999 603 41 0 23557 0
vsize: 94392
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 21607 0 0 0 32945 58 0 0 25 0 1 0 542700127 97587200 21249 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23825 21249 603 41 0 23784 0
vsize: 95300
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 21920 0 0 0 33945 59 0 0 25 0 1 0 542700127 98914304 21562 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24149 21562 603 41 0 24108 0
vsize: 96596
[startup+350.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 22189 0 0 0 34944 60 0 0 25 0 1 0 542700127 99995648 21831 4294967295 134512640 134672761 3221224624 3221223872 134562135 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24413 21831 603 41 0 24372 0
vsize: 97652
[startup+360.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 22561 0 0 0 35944 60 0 0 25 0 1 0 542700127 101486592 22203 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24777 22203 603 41 0 24736 0
vsize: 99108
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 23215 0 0 0 36942 62 0 0 25 0 1 0 542700127 104202240 22857 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25440 22857 603 41 0 25399 0
vsize: 101760
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 23479 0 0 0 37942 62 0 0 25 0 1 0 542700127 105275392 23121 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25702 23121 603 41 0 25661 0
vsize: 102808
[startup+390.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 23708 0 0 0 38942 63 0 0 25 0 1 0 542700127 106221568 23350 4294967295 134512640 134672761 3221224624 3221223728 134559916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25933 23350 603 41 0 25892 0
vsize: 103732
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 24056 0 0 0 39941 63 0 0 25 0 1 0 542700127 107569152 23698 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26262 23698 603 41 0 26221 0
vsize: 105048
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 24382 0 0 0 40941 64 0 0 25 0 1 0 542700127 109158400 24024 4294967295 134512640 134672761 3221224624 3221223580 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26650 24024 603 41 0 26609 0
vsize: 106600
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 24850 0 0 0 41940 65 0 0 25 0 1 0 542700127 111046656 24492 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27111 24492 603 41 0 27070 0
vsize: 108444
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 25184 0 0 0 42938 67 0 0 25 0 1 0 542700127 112517120 24826 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27470 24826 603 41 0 27429 0
vsize: 109880
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 25477 0 0 0 43938 67 0 0 25 0 1 0 542700127 113733632 25119 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27767 25119 603 41 0 27726 0
vsize: 111068
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 25811 0 0 0 44936 69 0 0 25 0 1 0 542700127 115101696 25453 4294967295 134512640 134672761 3221224624 3221223760 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28101 25453 603 41 0 28060 0
vsize: 112404
[startup+460.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 26010 0 0 0 45936 70 0 0 25 0 1 0 542700127 115908608 25652 4294967295 134512640 134672761 3221224624 3221223728 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28298 25652 603 41 0 28257 0
vsize: 113192
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 26270 0 0 0 46936 70 0 0 25 0 1 0 542700127 116850688 25912 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28528 25912 603 41 0 28487 0
vsize: 114112
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 26608 0 0 0 47935 71 0 0 25 0 1 0 542700127 118312960 26250 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28885 26250 603 41 0 28844 0
vsize: 115540
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 26906 0 0 0 48934 72 0 0 25 0 1 0 542700127 119525376 26548 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29181 26548 603 41 0 29140 0
vsize: 116724
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 27164 0 0 0 49934 73 0 0 25 0 1 0 542700127 120606720 26806 4294967295 134512640 134672761 3221224624 3221223792 134561275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29445 26806 603 41 0 29404 0
vsize: 117780
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 27509 0 0 0 50933 74 0 0 25 0 1 0 542700127 121937920 27151 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29770 27151 603 41 0 29729 0
vsize: 119080
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 27840 0 0 0 51933 74 0 0 25 0 1 0 542700127 123297792 27482 4294967295 134512640 134672761 3221224624 3221223760 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30102 27482 603 41 0 30061 0
vsize: 120408
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 28120 0 0 0 52932 75 0 0 25 0 1 0 542700127 124493824 27762 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30394 27762 603 41 0 30353 0
vsize: 121576
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 28427 0 0 0 53931 76 0 0 25 0 1 0 542700127 125714432 28069 4294967295 134512640 134672761 3221224624 3221223796 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30692 28069 603 41 0 30651 0
vsize: 122768
[startup+550.125 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19905
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 28683 0 0 0 54942 76 0 0 25 0 1 0 542700127 126771200 28325 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30950 28325 603 41 0 30909 0
vsize: 123800
[startup+560.163 s]
Raw data (loadavg): 0.99 0.97 0.93 2/58 19948
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 28979 0 0 0 55944 78 0 0 25 0 1 0 542700127 127983616 28621 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31246 28621 603 41 0 31205 0
vsize: 124984
[startup+570.163 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19958
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 29273 0 0 0 56944 78 0 0 25 0 1 0 542700127 129200128 28915 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31543 28915 603 41 0 31502 0
vsize: 126172
[startup+580.166 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19958
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 29527 0 0 0 57942 79 0 0 25 0 1 0 542700127 130138112 29169 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31772 29169 603 41 0 31731 0
vsize: 127088
[startup+590.167 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19958
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 29883 0 0 0 58941 80 0 0 25 0 1 0 542700127 131612672 29525 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32132 29525 603 41 0 32091 0
vsize: 128528
[startup+600.167 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19958
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 30159 0 0 0 59940 82 0 0 25 0 1 0 542700127 132825088 29801 4294967295 134512640 134672761 3221224624 3221223808 134558925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32428 29801 603 41 0 32387 0
vsize: 129712
[startup+610.167 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19958
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 30572 0 0 0 60939 83 0 0 25 0 1 0 542700127 134438912 30214 4294967295 134512640 134672761 3221224624 3221223728 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32822 30214 603 41 0 32781 0
vsize: 131288
[startup+620.167 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19958
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 30909 0 0 0 61937 84 0 0 25 0 1 0 542700127 135782400 30551 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33150 30551 603 41 0 33109 0
vsize: 132600
[startup+630.166 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19958
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 31254 0 0 0 62937 85 0 0 25 0 1 0 542700127 137273344 30896 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33514 30896 603 41 0 33473 0
vsize: 134056
[startup+640.166 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 31655 0 0 0 63936 86 0 0 25 0 1 0 542700127 138874880 31297 4294967295 134512640 134672761 3221224624 3221223728 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33905 31297 603 41 0 33864 0
vsize: 135620
[startup+650.167 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 31927 0 0 0 64935 87 0 0 25 0 1 0 542700127 139943936 31569 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34166 31569 603 41 0 34125 0
vsize: 136664
[startup+660.167 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 32175 0 0 0 65935 87 0 0 25 0 1 0 542700127 141017088 31817 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34428 31817 603 41 0 34387 0
vsize: 137712
[startup+670.167 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 32514 0 0 0 66934 88 0 0 25 0 1 0 542700127 142364672 32156 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34757 32156 603 41 0 34716 0
vsize: 139028
[startup+680.167 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 32813 0 0 0 67933 89 0 0 25 0 1 0 542700127 143699968 32455 4294967295 134512640 134672761 3221224624 3221223760 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35083 32455 603 41 0 35042 0
vsize: 140332
[startup+690.166 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 33023 0 0 0 68933 90 0 0 25 0 1 0 542700127 144502784 32665 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35279 32665 603 41 0 35238 0
vsize: 141116
[startup+700.166 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 33269 0 0 0 69933 90 0 0 25 0 1 0 542700127 145571840 32911 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35540 32911 603 41 0 35499 0
vsize: 142160
[startup+710.166 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 33587 0 0 0 70933 91 0 0 25 0 1 0 542700127 146788352 33229 4294967295 134512640 134672761 3221224624 3221223760 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35837 33229 603 41 0 35796 0
vsize: 143348
[startup+720.167 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 33872 0 0 0 71932 91 0 0 25 0 1 0 542700127 147992576 33514 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36131 33514 603 41 0 36090 0
vsize: 144524
[startup+730.166 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 34191 0 0 0 72931 92 0 0 25 0 1 0 542700127 149331968 33833 4294967295 134512640 134672761 3221224624 3221223728 134559998 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36458 33833 603 41 0 36417 0
vsize: 145832
[startup+740.167 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 34493 0 0 0 73931 93 0 0 25 0 1 0 542700127 150540288 34135 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36753 34135 603 41 0 36712 0
vsize: 147012
[startup+750.166 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 34787 0 0 0 74930 94 0 0 25 0 1 0 542700127 151740416 34429 4294967295 134512640 134672761 3221224624 3221223728 134560367 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37046 34429 603 41 0 37005 0
vsize: 148184
[startup+760.166 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 35149 0 0 0 75930 94 0 0 25 0 1 0 542700127 153214976 34791 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37406 34791 603 41 0 37365 0
vsize: 149624
[startup+770.167 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 35387 0 0 0 76930 94 0 0 25 0 1 0 542700127 154157056 35029 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37636 35029 603 41 0 37595 0
vsize: 150544
[startup+780.167 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 35723 0 0 0 77929 96 0 0 25 0 1 0 542700127 155504640 35365 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37965 35365 603 41 0 37924 0
vsize: 151860
[startup+790.168 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 36087 0 0 0 78928 96 0 0 25 0 1 0 542700127 156975104 35729 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38324 35729 603 41 0 38283 0
vsize: 153296
[startup+800.167 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 36357 0 0 0 79928 97 0 0 25 0 1 0 542700127 158179328 35999 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38618 35999 603 41 0 38577 0
vsize: 154472
[startup+810.167 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 36639 0 0 0 80927 98 0 0 25 0 1 0 542700127 159256576 36281 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38881 36281 603 41 0 38840 0
vsize: 155524
[startup+820.167 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 36902 0 0 0 81926 99 0 0 25 0 1 0 542700127 160346112 36544 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39147 36544 603 41 0 39106 0
vsize: 156588
[startup+830.167 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 37283 0 0 0 82925 100 0 0 25 0 1 0 542700127 161935360 36925 4294967295 134512640 134672761 3221224624 3221223808 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39535 36925 603 41 0 39494 0
vsize: 158140
[startup+840.167 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 37749 0 0 0 83924 101 0 0 25 0 1 0 542700127 163811328 37391 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39993 37391 603 41 0 39952 0
vsize: 159972
[startup+850.166 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 38129 0 0 0 84924 102 0 0 25 0 1 0 542700127 165302272 37771 4294967295 134512640 134672761 3221224624 3221223728 134559981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40357 37771 603 41 0 40316 0
vsize: 161428
[startup+860.166 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 38451 0 0 0 85923 103 0 0 25 0 1 0 542700127 166649856 38093 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40686 38093 603 41 0 40645 0
vsize: 162744
[startup+870.166 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 38743 0 0 0 86923 103 0 0 25 0 1 0 542700127 167862272 38385 4294967295 134512640 134672761 3221224624 3221223808 134558651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40982 38386 603 41 0 40941 0
vsize: 163928
[startup+880.17 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 39054 0 0 0 87923 104 0 0 25 0 1 0 542700127 169078784 38696 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41279 38696 603 41 0 41238 0
vsize: 165116
[startup+890.176 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 39321 0 0 0 88923 105 0 0 25 0 1 0 542700127 170295296 38963 4294967295 134512640 134672761 3221224624 3221223728 134560036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41576 38963 603 41 0 41535 0
vsize: 166304
[startup+900.176 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 39692 0 0 0 89922 105 0 0 25 0 1 0 542700127 171769856 39334 4294967295 134512640 134672761 3221224624 3221223728 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41936 39334 603 41 0 41895 0
vsize: 167744
[startup+910.176 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 40093 0 0 0 90922 106 0 0 25 0 1 0 542700127 173387776 39735 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42331 39735 603 41 0 42290 0
vsize: 169324
[startup+920.175 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19960
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 40514 0 0 0 91921 107 0 0 25 0 1 0 542700127 175153152 40156 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42762 40156 603 41 0 42721 0
vsize: 171048
[startup+930.175 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19962
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 40899 0 0 0 92920 108 0 0 25 0 1 0 542700127 176619520 40541 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43120 40541 603 41 0 43079 0
vsize: 172480
[startup+940.175 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19962
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 41348 0 0 0 93919 109 0 0 25 0 1 0 542700127 178511872 40990 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43582 40990 603 41 0 43541 0
vsize: 174328
[startup+950.174 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19962
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 41751 0 0 0 94918 110 0 0 25 0 1 0 542700127 180113408 41393 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43973 41393 603 41 0 43932 0
vsize: 175892
[startup+960.174 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19962
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 42154 0 0 0 95918 111 0 0 25 0 1 0 542700127 181837824 41796 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44394 41796 603 41 0 44353 0
vsize: 177576
[startup+970.175 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19962
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 42453 0 0 0 96917 112 0 0 25 0 1 0 542700127 183050240 42095 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44690 42095 603 41 0 44649 0
vsize: 178760
[startup+980.174 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19962
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 42691 0 0 0 97917 112 0 0 25 0 1 0 542700127 183975936 42333 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44916 42333 603 41 0 44875 0
vsize: 179664
[startup+990.174 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19962
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 43008 0 0 0 98916 113 0 0 25 0 1 0 542700127 185327616 42650 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45246 42650 603 41 0 45205 0
vsize: 180984
[startup+1000.17 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19962
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 43334 0 0 0 99915 114 0 0 25 0 1 0 542700127 186675200 42976 4294967295 134512640 134672761 3221224624 3221223728 134559927 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45575 42976 603 41 0 45534 0
vsize: 182300
[startup+1010.17 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19962
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 43684 0 0 0 100914 115 0 0 25 0 1 0 542700127 188026880 43326 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45905 43326 603 41 0 45864 0
vsize: 183620
[startup+1020.17 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19962
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 44034 0 0 0 101914 116 0 0 25 0 1 0 542700127 189497344 43676 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46264 43676 603 41 0 46223 0
vsize: 185056
[startup+1030.17 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19962
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 44429 0 0 0 102913 116 0 0 25 0 1 0 542700127 191107072 44071 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46657 44071 603 41 0 46616 0
vsize: 186628
[startup+1040.17 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19962
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 44691 0 0 0 103912 117 0 0 25 0 1 0 542700127 192716800 44333 4294967295 134512640 134672761 3221224624 3221223792 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47050 44333 603 41 0 47009 0
vsize: 188200
[startup+1050.17 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19962
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 44977 0 0 0 104911 118 0 0 25 0 1 0 542700127 193921024 44619 4294967295 134512640 134672761 3221224624 3221223728 134560036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47344 44619 603 41 0 47303 0
vsize: 189376
[startup+1060.17 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19962
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 45245 0 0 0 105911 119 0 0 25 0 1 0 542700127 194985984 44887 4294967295 134512640 134672761 3221224624 3221223728 134560492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47604 44887 603 41 0 47563 0
vsize: 190416
[startup+1070.17 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19962
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 45524 0 0 0 106910 119 0 0 25 0 1 0 542700127 196067328 45166 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47868 45166 603 41 0 47827 0
vsize: 191472
[startup+1080.17 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19962
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 45813 0 0 0 107909 120 0 0 25 0 1 0 542700127 197283840 45455 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48165 45455 603 41 0 48124 0
vsize: 192660
[startup+1090.17 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19962
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 46163 0 0 0 108909 121 0 0 25 0 1 0 542700127 198750208 45805 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48523 45805 603 41 0 48482 0
vsize: 194092
[startup+1100.18 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19962
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 46520 0 0 0 109909 122 0 0 25 0 1 0 542700127 200228864 46162 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48884 46162 603 41 0 48843 0
vsize: 195536
[startup+1110.17 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19962
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 46845 0 0 0 110908 123 0 0 25 0 1 0 542700127 201568256 46487 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49211 46487 603 41 0 49170 0
vsize: 196844
[startup+1120.17 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19962
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 47100 0 0 0 111907 123 0 0 25 0 1 0 542700127 202514432 46742 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49442 46742 603 41 0 49401 0
vsize: 197768
[startup+1130.17 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19962
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 47315 0 0 0 112907 123 0 0 25 0 1 0 542700127 203448320 46957 4294967295 134512640 134672761 3221224624 3221223748 134566080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49670 46957 603 41 0 49629 0
vsize: 198680
[startup+1140.18 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19962
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 47604 0 0 0 113907 124 0 0 25 0 1 0 542700127 204652544 47246 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49964 47246 603 41 0 49923 0
vsize: 199856
[startup+1150.17 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19962
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 47943 0 0 0 114906 125 0 0 25 0 1 0 542700127 206000128 47585 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50293 47585 603 41 0 50252 0
vsize: 201172
[startup+1160.17 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19962
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 48304 0 0 0 115906 126 0 0 25 0 1 0 542700127 207462400 47946 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50650 47946 603 41 0 50609 0
vsize: 202600
[startup+1170.17 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19962
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 48605 0 0 0 116905 126 0 0 25 0 1 0 542700127 208674816 48247 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50946 48247 603 41 0 50905 0
vsize: 203784
[startup+1180.17 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19962
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 48898 0 0 0 117905 127 0 0 25 0 1 0 542700127 209891328 48540 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51243 48540 603 41 0 51202 0
vsize: 204972
[startup+1190.18 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19962
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 49208 0 0 0 118904 128 0 0 25 0 1 0 542700127 211103744 48850 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51539 48850 603 41 0 51498 0
vsize: 206156
[startup+1200.18 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 19962
Raw data (stat): 19905 (minisat+) R 19904 10614 10613 0 -1 0 49498 0 0 0 119904 129 0 0 25 0 1 0 542700127 212299776 49140 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51831 49140 603 41 0 51790 0
vsize: 207324
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.27 s]
Raw data (loadavg): 0.99 0.97 0.93 1/54 19962
Raw data (stat): 19905 (minisat+) Z 19904 10614 10613 0 -1 12 49500 0 0 0 119904 138 0 0 25 0 1 0 542700127 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.27
CPU time (s): 1200.42
CPU user time (s): 1199.04
CPU system time (s): 1.38079
CPU usage (%): 100.013
Max. virtual memory (Kb): 207324
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####