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/submitted/manquinho/logic-synthesis/normalized-e64.b.opb
MD5SUM	bf7f8537c6faa135d25c67c53576abb5
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	49
Optimality of the best value was proved	NO
Number of terms in the objective function	608
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	608
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	608
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03484
Number of variables	607
Total number of constraints	1053
Number of constraints which are clauses	1022
Number of constraints which are cardinality constraints (but not clauses)	31
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	3
Maximum length of a constraint	32
Trace number 4835

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-13 20:29:29 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=590 boxname=wulflinc2 idbench=66 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  bf7f8537c6faa135d25c67c53576abb5  /oldhome/oroussel/tmp/wulflinc2/normalized-e64.b.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc2/normalized-e64.b.opb
IDLAUNCH: 590
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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:        912812 kB
Buffers:         33188 kB
Cached:          68468 kB
SwapCached:          4 kB
Active:          53292 kB
Inactive:        51184 kB
HighTotal:      131008 kB
HighFree:        58800 kB
LowTotal:       903652 kB
LowFree:        854012 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11888 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:49:31 (client local time) WITH STATUS 10 IN 1200.21 SECONDS
stats: 590 7 1200.21 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1022 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    1022     8200 |     340       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: 82[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:27428     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         1 |   32888    82605 |   10962       1       16    16.0 |  0.000 % |
c |       101 |   32731    82280 |   12058      94     1328    14.1 |  0.441 % |
c |       251 |   32731    82280 |   13264     244     4888    20.0 |  0.441 % |
c |       476 |   32693    82200 |   14590     467     9207    19.7 |  0.538 % |
c |       815 |   32655    82120 |   16049     805    14538    18.1 |  0.636 % |
c ==============================================================================
c [1mFound solution: 64[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1118 |   32544    81867 |   10848    1108    20015    18.1 |  0.636 % |
c |      1219 |   32544    81867 |   11932    1209    21890    18.1 |  1.342 % |
c |      1371 |   32544    81867 |   13126    1361    27251    20.0 |  1.342 % |
c |      1597 |   32544    81867 |   14438    1587    32001    20.2 |  1.342 % |
c |      1935 |   32544    81867 |   15882    1925    44062    22.9 |  1.342 % |
c |      2442 |   32526    81825 |   17470    2426    58440    24.1 |  1.397 % |
c |      3201 |   32524    81821 |   19217    3182    81772    25.7 |  1.402 % |
c |      4340 |   32524    81821 |   21139    4321   124438    28.8 |  1.402 % |
c |      6049 |   32524    81821 |   23253    6030   236669    39.2 |  1.402 % |
c |      8611 |   32524    81821 |   25579    8592   404633    47.1 |  1.402 % |
c |     12456 |   32524    81821 |   28136   12437   881628    70.9 |  1.402 % |
c ==============================================================================
c [1mFound solution: 57[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17530 |   32583    81971 |   10861   17511  1261267    72.0 |  1.402 % |
c |     17631 |   32583    81971 |   11947    8857   728551    82.3 |  1.404 % |
c |     17781 |   32557    81915 |   13141    9005   733381    81.4 |  1.474 % |
c |     18007 |   32557    81915 |   14455    9231   741448    80.3 |  1.474 % |
c |     18344 |   32557    81915 |   15901    9568   749366    78.3 |  1.474 % |
c |     18850 |   32557    81915 |   17491   10074   785392    78.0 |  1.474 % |
c |     19609 |   32557    81915 |   19240   10833   859333    79.3 |  1.474 % |
c |     20748 |   32557    81915 |   21165   11972   919844    76.8 |  1.474 % |
c |     22458 |   32557    81915 |   23281   13682  1056358    77.2 |  1.474 % |
c |     25020 |   32557    81915 |   25609   16244  1287855    79.3 |  1.474 % |
c ==============================================================================
c [1mFound solution: 55[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     25537 |   32576    81969 |   10858   16761  1329272    79.3 |  1.474 % |
c |     25637 |   32576    81969 |   11943    8481   589547    69.5 |  1.477 % |
c |     25787 |   32576    81969 |   13138    8631   595037    68.9 |  1.477 % |
c |     26012 |   32576    81969 |   14451    8856   607205    68.6 |  1.477 % |
c |     26349 |   32576    81969 |   15897    9193   625383    68.0 |  1.477 % |
c |     26855 |   32576    81969 |   17486    9699   645599    66.6 |  1.477 % |
c |     27616 |   32576    81969 |   19235   10460   688721    65.8 |  1.477 % |
c |     28755 |   32576    81969 |   21159   11599   760883    65.6 |  1.477 % |
c |     30463 |   32576    81969 |   23275   13307   926598    69.6 |  1.477 % |
c |     33026 |   32576    81969 |   25602   15870  1052589    66.3 |  1.477 % |
c |     36872 |   32576    81969 |   28162   19716  1313125    66.6 |  1.477 % |
c |     42638 |   32540    81893 |   30979   25472  1707177    67.0 |  1.570 % |
c |     51288 |   32540    81893 |   34077   13453   850735    63.2 |  1.570 % |
c |     64262 |   32540    81893 |   37484   26427  1854535    70.2 |  1.570 % |
c ==============================================================================
c [1mFound solution: 53[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     71120 |   32558    81945 |   10852   33285  2473346    74.3 |  1.570 % |
c |     71222 |   32558    81945 |   11937    6680   548160    82.1 |  1.583 % |
c |     71372 |   32558    81945 |   13130    6830   551418    80.7 |  1.583 % |
c |     71597 |   32558    81945 |   14444    7055   563546    79.9 |  1.583 % |
c |     71934 |   32558    81945 |   15888    7392   572407    77.4 |  1.583 % |
c |     72440 |   32558    81945 |   17477    7898   589289    74.6 |  1.583 % |
c |     73199 |   32558    81945 |   19224    8657   630654    72.8 |  1.583 % |
c |     74340 |   32558    81945 |   21147    9798   684750    69.9 |  1.583 % |
c |     76048 |   32558    81945 |   23262   11506   842785    73.2 |  1.583 % |
c |     78611 |   32558    81945 |   25588   14069  1080790    76.8 |  1.583 % |
c |     82457 |   32558    81945 |   28147   17915  1447445    80.8 |  1.583 % |
c |     88223 |   32558    81945 |   30962   23681  1883985    79.6 |  1.583 % |
c |     96872 |   32558    81945 |   34058   32330  2567295    79.4 |  1.583 % |
c |    109848 |   32558    81945 |   37464   21298  1707483    80.2 |  1.583 % |
c |    129309 |   32558    81945 |   41210   13470  1145174    85.0 |  1.583 % |
c |    158501 |   32558    81945 |   45331   42662  3823977    89.6 |  1.583 % |
c |    202290 |   32558    81945 |   49864   18699  1418328    75.9 |  1.583 % |
c |    267976 |   32558    81945 |   54851   46288  3760997    81.3 |  1.583 % |
c |    366502 |   32558    81945 |   60336   17595  1604710    91.2 |  1.583 % |
#### 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.85 0.97 0.91 2/54 22589
Raw data (stat): 22589 (runsolver) R 22588 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420618846 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+9.99983 s]
Raw data (loadavg): 0.87 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 2487 0 0 0 990 7 0 0 25 0 1 0 420618846 12369920 2400 4294967295 134512640 134672761 3221224640 3221223808 134560785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3020 2400 603 41 0 2979 0
vsize: 12080
[startup+20.0008 s]
Raw data (loadavg): 0.89 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 3085 0 0 0 1987 10 0 0 25 0 1 0 420618846 14782464 2998 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3609 2998 603 41 0 3568 0
vsize: 14436
[startup+30.0014 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 3479 0 0 0 2986 12 0 0 25 0 1 0 420618846 16367616 3392 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3996 3392 603 41 0 3955 0
vsize: 15984
[startup+40.0019 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 3479 0 0 0 3986 12 0 0 25 0 1 0 420618846 16367616 3392 4294967295 134512640 134672761 3221224640 3221223808 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3996 3392 603 41 0 3955 0
vsize: 15984
[startup+50.0029 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 3591 0 0 0 4985 12 0 0 25 0 1 0 420618846 16896000 3504 4294967295 134512640 134672761 3221224640 3221223776 134560718 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4125 3504 603 41 0 4084 0
vsize: 16500
[startup+60.0023 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 3592 0 0 0 5986 12 0 0 25 0 1 0 420618846 16896000 3505 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4125 3505 603 41 0 4084 0
vsize: 16500
[startup+70.003 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 4021 0 0 0 6983 14 0 0 25 0 1 0 420618846 18644992 3934 4294967295 134512640 134672761 3221224640 3221223776 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4552 3934 603 41 0 4511 0
vsize: 18208
[startup+80.003 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 4372 0 0 0 7982 16 0 0 25 0 1 0 420618846 19988480 4285 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4880 4285 603 41 0 4839 0
vsize: 19520
[startup+90.0034 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 4716 0 0 0 8980 17 0 0 25 0 1 0 420618846 21585920 4629 4294967295 134512640 134672761 3221224640 3221223632 134565768 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5270 4629 603 41 0 5229 0
vsize: 21080
[startup+100.003 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 4716 0 0 0 9980 17 0 0 25 0 1 0 420618846 21585920 4629 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5270 4629 603 41 0 5229 0
vsize: 21080
[startup+110.003 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 4716 0 0 0 10981 17 0 0 25 0 1 0 420618846 21585920 4629 4294967295 134512640 134672761 3221224640 3221223764 134566075 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5270 4629 603 41 0 5229 0
vsize: 21080
[startup+120.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 4716 0 0 0 11981 17 0 0 25 0 1 0 420618846 21585920 4629 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5270 4629 603 41 0 5229 0
vsize: 21080
[startup+130.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 4983 0 0 0 12980 19 0 0 25 0 1 0 420618846 22654976 4896 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5531 4896 603 41 0 5490 0
vsize: 22124
[startup+140.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 5029 0 0 0 13980 19 0 0 25 0 1 0 420618846 22859776 4942 4294967295 134512640 134672761 3221224640 3221223808 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5581 4942 603 41 0 5540 0
vsize: 22324
[startup+150.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 5029 0 0 0 14980 19 0 0 25 0 1 0 420618846 22859776 4942 4294967295 134512640 134672761 3221224640 3221223792 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5581 4942 603 41 0 5540 0
vsize: 22324
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 5029 0 0 0 15980 19 0 0 25 0 1 0 420618846 22859776 4942 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5581 4942 603 41 0 5540 0
vsize: 22324
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 5029 0 0 0 16980 19 0 0 25 0 1 0 420618846 22859776 4942 4294967295 134512640 134672761 3221224640 3221223808 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5581 4942 603 41 0 5540 0
vsize: 22324
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 5230 0 0 0 17980 19 0 0 25 0 1 0 420618846 23674880 5143 4294967295 134512640 134672761 3221224640 3221223840 134557811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5780 5143 603 41 0 5739 0
vsize: 23120
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 5639 0 0 0 18979 21 0 0 25 0 1 0 420618846 25296896 5552 4294967295 134512640 134672761 3221224640 3221223808 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6176 5552 603 41 0 6135 0
vsize: 24704
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 5639 0 0 0 19979 21 0 0 25 0 1 0 420618846 25296896 5552 4294967295 134512640 134672761 3221224640 3221223824 134559559 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6176 5552 603 41 0 6135 0
vsize: 24704
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 5639 0 0 0 20979 21 0 0 25 0 1 0 420618846 25296896 5552 4294967295 134512640 134672761 3221224640 3221223784 134560555 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6176 5552 603 41 0 6135 0
vsize: 24704
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 5639 0 0 0 21979 21 0 0 25 0 1 0 420618846 25296896 5552 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6176 5552 603 41 0 6135 0
vsize: 24704
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 5639 0 0 0 22980 21 0 0 25 0 1 0 420618846 25296896 5552 4294967295 134512640 134672761 3221224640 3221223808 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6176 5552 603 41 0 6135 0
vsize: 24704
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 5917 0 0 0 23979 22 0 0 25 0 1 0 420618846 26501120 5830 4294967295 134512640 134672761 3221224640 3221223808 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6470 5830 603 41 0 6429 0
vsize: 25880
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 6214 0 0 0 24977 23 0 0 25 0 1 0 420618846 27717632 6127 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6767 6127 603 41 0 6726 0
vsize: 27068
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 6214 0 0 0 25977 23 0 0 25 0 1 0 420618846 27717632 6127 4294967295 134512640 134672761 3221224640 3221223840 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6767 6127 603 41 0 6726 0
vsize: 27068
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 6214 0 0 0 26978 23 0 0 25 0 1 0 420618846 27717632 6127 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6767 6127 603 41 0 6726 0
vsize: 27068
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 6214 0 0 0 27978 23 0 0 25 0 1 0 420618846 27717632 6127 4294967295 134512640 134672761 3221224640 3221223776 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6767 6127 603 41 0 6726 0
vsize: 27068
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 6214 0 0 0 28978 23 0 0 25 0 1 0 420618846 27717632 6127 4294967295 134512640 134672761 3221224640 3221223808 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6767 6127 603 41 0 6726 0
vsize: 27068
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 6214 0 0 0 29978 23 0 0 25 0 1 0 420618846 27717632 6127 4294967295 134512640 134672761 3221224640 3221223808 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6767 6127 603 41 0 6726 0
vsize: 27068
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 6501 0 0 0 30978 24 0 0 25 0 1 0 420618846 28930048 6414 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7063 6414 603 41 0 7022 0
vsize: 28252
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 6888 0 0 0 31977 25 0 0 25 0 1 0 420618846 30408704 6801 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7424 6801 603 41 0 7383 0
vsize: 29696
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7253 0 0 0 32976 26 0 0 25 0 1 0 420618846 32018432 7166 4294967295 134512640 134672761 3221224640 3221223808 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7817 7166 603 41 0 7776 0
vsize: 31268
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7354 0 0 0 33976 26 0 0 25 0 1 0 420618846 32419840 7267 4294967295 134512640 134672761 3221224640 3221223808 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7915 7267 603 41 0 7874 0
vsize: 31660
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7354 0 0 0 34976 26 0 0 25 0 1 0 420618846 32419840 7267 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7915 7267 603 41 0 7874 0
vsize: 31660
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7354 0 0 0 35977 26 0 0 25 0 1 0 420618846 32419840 7267 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7915 7267 603 41 0 7874 0
vsize: 31660
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7354 0 0 0 36977 26 0 0 25 0 1 0 420618846 32419840 7267 4294967295 134512640 134672761 3221224640 3221223808 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7915 7267 603 41 0 7874 0
vsize: 31660
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7363 0 0 0 37977 26 0 0 25 0 1 0 420618846 32419840 7276 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7915 7276 603 41 0 7874 0
vsize: 31660
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7365 0 0 0 38977 26 0 0 25 0 1 0 420618846 32419840 7278 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7915 7278 603 41 0 7874 0
vsize: 31660
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7366 0 0 0 39977 26 0 0 25 0 1 0 420618846 32419840 7279 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7915 7279 603 41 0 7874 0
vsize: 31660
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7379 0 0 0 40978 26 0 0 25 0 1 0 420618846 32563200 7292 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7950 7292 603 41 0 7909 0
vsize: 31800
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7392 0 0 0 41978 27 0 0 25 0 1 0 420618846 32563200 7305 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7950 7305 603 41 0 7909 0
vsize: 31800
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7392 0 0 0 42978 27 0 0 25 0 1 0 420618846 32563200 7305 4294967295 134512640 134672761 3221224640 3221223784 134560555 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7950 7305 603 41 0 7909 0
vsize: 31800
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7392 0 0 0 43978 27 0 0 25 0 1 0 420618846 32563200 7305 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7950 7305 603 41 0 7909 0
vsize: 31800
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7392 0 0 0 44978 27 0 0 25 0 1 0 420618846 32563200 7305 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7950 7305 603 41 0 7909 0
vsize: 31800
[startup+460.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7392 0 0 0 45979 27 0 0 25 0 1 0 420618846 32563200 7305 4294967295 134512640 134672761 3221224640 3221223744 134560347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7950 7305 603 41 0 7909 0
vsize: 31800
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7392 0 0 0 46979 27 0 0 25 0 1 0 420618846 32563200 7305 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7950 7305 603 41 0 7909 0
vsize: 31800
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7392 0 0 0 47979 27 0 0 25 0 1 0 420618846 32563200 7305 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7950 7305 603 41 0 7909 0
vsize: 31800
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7392 0 0 0 48979 27 0 0 25 0 1 0 420618846 32563200 7305 4294967295 134512640 134672761 3221224640 3221223744 134554910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7950 7305 603 41 0 7909 0
vsize: 31800
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7392 0 0 0 49979 27 0 0 25 0 1 0 420618846 32563200 7305 4294967295 134512640 134672761 3221224640 3221223808 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7950 7305 603 41 0 7909 0
vsize: 31800
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7392 0 0 0 50980 27 0 0 25 0 1 0 420618846 32563200 7305 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7950 7305 603 41 0 7909 0
vsize: 31800
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7516 0 0 0 51979 27 0 0 25 0 1 0 420618846 33099776 7429 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8081 7429 603 41 0 8040 0
vsize: 32324
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7718 0 0 0 52979 27 0 0 25 0 1 0 420618846 33910784 7631 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8279 7631 603 41 0 8238 0
vsize: 33116
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7718 0 0 0 53979 27 0 0 25 0 1 0 420618846 33910784 7631 4294967295 134512640 134672761 3221224640 3221223776 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8279 7631 603 41 0 8238 0
vsize: 33116
[startup+550.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7718 0 0 0 54979 27 0 0 25 0 1 0 420618846 33910784 7631 4294967295 134512640 134672761 3221224640 3221223808 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8279 7631 603 41 0 8238 0
vsize: 33116
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7718 0 0 0 55980 27 0 0 25 0 1 0 420618846 33910784 7631 4294967295 134512640 134672761 3221224640 3221223824 134558360 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8279 7631 603 41 0 8238 0
vsize: 33116
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7724 0 0 0 56980 27 0 0 25 0 1 0 420618846 33910784 7637 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8279 7637 603 41 0 8238 0
vsize: 33116
[startup+580.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7730 0 0 0 57980 27 0 0 25 0 1 0 420618846 33910784 7643 4294967295 134512640 134672761 3221224640 3221223744 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8279 7643 603 41 0 8238 0
vsize: 33116
[startup+590.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7730 0 0 0 58980 27 0 0 25 0 1 0 420618846 33910784 7643 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8279 7643 603 41 0 8238 0
vsize: 33116
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7730 0 0 0 59980 27 0 0 25 0 1 0 420618846 33910784 7643 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8279 7643 603 41 0 8238 0
vsize: 33116
[startup+610.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7730 0 0 0 60981 27 0 0 25 0 1 0 420618846 33910784 7643 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8279 7643 603 41 0 8238 0
vsize: 33116
[startup+620.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7730 0 0 0 61981 27 0 0 25 0 1 0 420618846 33910784 7643 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8279 7643 603 41 0 8238 0
vsize: 33116
[startup+630.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7731 0 0 0 62981 27 0 0 25 0 1 0 420618846 33910784 7644 4294967295 134512640 134672761 3221224640 3221223824 134558930 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8279 7644 603 41 0 8238 0
vsize: 33116
[startup+640.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7736 0 0 0 63981 27 0 0 25 0 1 0 420618846 34045952 7649 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8312 7649 603 41 0 8271 0
vsize: 33248
[startup+650.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7737 0 0 0 64981 28 0 0 25 0 1 0 420618846 34045952 7650 4294967295 134512640 134672761 3221224640 3221223824 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8312 7650 603 41 0 8271 0
vsize: 33248
[startup+660.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 7788 0 0 0 65981 28 0 0 25 0 1 0 420618846 34181120 7701 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8345 7701 603 41 0 8304 0
vsize: 33380
[startup+670.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8037 0 0 0 66980 29 0 0 25 0 1 0 420618846 35250176 7950 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8606 7950 603 41 0 8565 0
vsize: 34424
[startup+680.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8283 0 0 0 67979 30 0 0 25 0 1 0 420618846 36184064 8196 4294967295 134512640 134672761 3221224640 3221223808 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8834 8196 603 41 0 8793 0
vsize: 35336
[startup+690.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8307 0 0 0 68980 30 0 0 25 0 1 0 420618846 36315136 8220 4294967295 134512640 134672761 3221224640 3221223732 1075346528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8866 8220 603 41 0 8825 0
vsize: 35464
[startup+700.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8307 0 0 0 69980 30 0 0 25 0 1 0 420618846 36315136 8220 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8866 8220 603 41 0 8825 0
vsize: 35464
[startup+710.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8315 0 0 0 70980 30 0 0 25 0 1 0 420618846 36315136 8228 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8866 8228 603 41 0 8825 0
vsize: 35464
[startup+720.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8315 0 0 0 71980 30 0 0 25 0 1 0 420618846 36315136 8228 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8866 8228 603 41 0 8825 0
vsize: 35464
[startup+730.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8315 0 0 0 72980 30 0 0 25 0 1 0 420618846 36315136 8228 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8866 8228 603 41 0 8825 0
vsize: 35464
[startup+740.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8322 0 0 0 73980 30 0 0 25 0 1 0 420618846 36462592 8235 4294967295 134512640 134672761 3221224640 3221223824 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8902 8235 603 41 0 8861 0
vsize: 35608
[startup+750.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8323 0 0 0 74981 30 0 0 25 0 1 0 420618846 36462592 8236 4294967295 134512640 134672761 3221224640 3221223824 134559182 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8902 8236 603 41 0 8861 0
vsize: 35608
[startup+760.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8329 0 0 0 75981 30 0 0 25 0 1 0 420618846 36462592 8242 4294967295 134512640 134672761 3221224640 3221223744 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8902 8242 603 41 0 8861 0
vsize: 35608
[startup+770.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8329 0 0 0 76981 30 0 0 25 0 1 0 420618846 36462592 8242 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8902 8242 603 41 0 8861 0
vsize: 35608
[startup+780.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8329 0 0 0 77981 30 0 0 25 0 1 0 420618846 36462592 8242 4294967295 134512640 134672761 3221224640 3221223840 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8902 8242 603 41 0 8861 0
vsize: 35608
[startup+790.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8341 0 0 0 78981 30 0 0 25 0 1 0 420618846 36462592 8254 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8902 8254 603 41 0 8861 0
vsize: 35608
[startup+800.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8489 0 0 0 79981 30 0 0 25 0 1 0 420618846 37150720 8402 4294967295 134512640 134672761 3221224640 3221223840 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9070 8402 603 41 0 9029 0
vsize: 36280
[startup+810.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8741 0 0 0 80980 31 0 0 25 0 1 0 420618846 38219776 8654 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9331 8654 603 41 0 9290 0
vsize: 37324
[startup+820.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 8991 0 0 0 81980 31 0 0 25 0 1 0 420618846 39161856 8904 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9561 8904 603 41 0 9520 0
vsize: 38244
[startup+830.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9044 0 0 0 82981 31 0 0 25 0 1 0 420618846 39428096 8957 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9626 8957 603 41 0 9585 0
vsize: 38504
[startup+840.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9044 0 0 0 83981 31 0 0 25 0 1 0 420618846 39428096 8957 4294967295 134512640 134672761 3221224640 3221223824 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9626 8957 603 41 0 9585 0
vsize: 38504
[startup+850.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9054 0 0 0 84981 31 0 0 25 0 1 0 420618846 39428096 8967 4294967295 134512640 134672761 3221224640 3221223808 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9626 8967 603 41 0 9585 0
vsize: 38504
[startup+860.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9064 0 0 0 85981 31 0 0 25 0 1 0 420618846 39587840 8977 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9665 8977 603 41 0 9624 0
vsize: 38660
[startup+870.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9070 0 0 0 86982 31 0 0 25 0 1 0 420618846 39587840 8983 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9665 8983 603 41 0 9624 0
vsize: 38660
[startup+880.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9070 0 0 0 87982 31 0 0 25 0 1 0 420618846 39587840 8983 4294967295 134512640 134672761 3221224640 3221223824 134559345 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9665 8983 603 41 0 9624 0
vsize: 38660
[startup+890.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9070 0 0 0 88982 31 0 0 25 0 1 0 420618846 39587840 8983 4294967295 134512640 134672761 3221224640 3221223744 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9665 8983 603 41 0 9624 0
vsize: 38660
[startup+900.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9071 0 0 0 89982 31 0 0 25 0 1 0 420618846 39587840 8984 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9665 8984 603 41 0 9624 0
vsize: 38660
[startup+910.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9071 0 0 0 90982 31 0 0 25 0 1 0 420618846 39587840 8984 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9665 8984 603 41 0 9624 0
vsize: 38660
[startup+920.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9083 0 0 0 91983 31 0 0 25 0 1 0 420618846 39587840 8996 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9665 8996 603 41 0 9624 0
vsize: 38660
[startup+930.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9084 0 0 0 92983 31 0 0 25 0 1 0 420618846 39587840 8997 4294967295 134512640 134672761 3221224640 3221223808 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9665 8997 603 41 0 9624 0
vsize: 38660
[startup+940.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9085 0 0 0 93983 31 0 0 25 0 1 0 420618846 39587840 8998 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9665 8998 603 41 0 9624 0
vsize: 38660
[startup+950.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9085 0 0 0 94983 31 0 0 25 0 1 0 420618846 39587840 8998 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9665 8998 603 41 0 9624 0
vsize: 38660
[startup+960.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9086 0 0 0 95983 31 0 0 25 0 1 0 420618846 39587840 8999 4294967295 134512640 134672761 3221224640 3221223840 134557814 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9665 8999 603 41 0 9624 0
vsize: 38660
[startup+970.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9087 0 0 0 96983 31 0 0 25 0 1 0 420618846 39587840 9000 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9665 9000 603 41 0 9624 0
vsize: 38660
[startup+980.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9281 0 0 0 97983 32 0 0 25 0 1 0 420618846 40407040 9194 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9865 9194 603 41 0 9824 0
vsize: 39460
[startup+990.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9429 0 0 0 98983 32 0 0 25 0 1 0 420618846 40947712 9342 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9997 9342 603 41 0 9956 0
vsize: 39988
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9429 0 0 0 99982 33 0 0 25 0 1 0 420618846 40947712 9342 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9997 9342 603 41 0 9956 0
vsize: 39988
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9429 0 0 0 100982 33 0 0 25 0 1 0 420618846 40947712 9342 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9997 9342 603 41 0 9956 0
vsize: 39988
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9429 0 0 0 101982 33 0 0 25 0 1 0 420618846 40947712 9342 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9997 9342 603 41 0 9956 0
vsize: 39988
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9429 0 0 0 102982 33 0 0 25 0 1 0 420618846 40947712 9342 4294967295 134512640 134672761 3221224640 3221223824 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9997 9342 603 41 0 9956 0
vsize: 39988
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9429 0 0 0 103982 33 0 0 25 0 1 0 420618846 40947712 9342 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9997 9342 603 41 0 9956 0
vsize: 39988
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9430 0 0 0 104983 33 0 0 25 0 1 0 420618846 40947712 9343 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9997 9343 603 41 0 9956 0
vsize: 39988
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9430 0 0 0 105983 33 0 0 25 0 1 0 420618846 40947712 9343 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9997 9343 603 41 0 9956 0
vsize: 39988
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9431 0 0 0 106983 33 0 0 25 0 1 0 420618846 40947712 9344 4294967295 134512640 134672761 3221224640 3221223808 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9997 9344 603 41 0 9956 0
vsize: 39988
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9431 0 0 0 107983 33 0 0 25 0 1 0 420618846 40947712 9344 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9997 9344 603 41 0 9956 0
vsize: 39988
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9431 0 0 0 108983 33 0 0 25 0 1 0 420618846 40947712 9344 4294967295 134512640 134672761 3221224640 3221223840 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9997 9344 603 41 0 9956 0
vsize: 39988
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9431 0 0 0 109983 33 0 0 25 0 1 0 420618846 40947712 9344 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9997 9344 603 41 0 9956 0
vsize: 39988
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9431 0 0 0 110984 33 0 0 25 0 1 0 420618846 40947712 9344 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9997 9344 603 41 0 9956 0
vsize: 39988
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9440 0 0 0 111984 33 0 0 25 0 1 0 420618846 41144320 9353 4294967295 134512640 134672761 3221224640 3221223808 134561256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10045 9353 603 41 0 10004 0
vsize: 40180
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9452 0 0 0 112984 33 0 0 25 0 1 0 420618846 41144320 9365 4294967295 134512640 134672761 3221224640 3221223784 134560555 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10045 9365 603 41 0 10004 0
vsize: 40180
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9462 0 0 0 113984 33 0 0 25 0 1 0 420618846 41144320 9375 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10045 9375 603 41 0 10004 0
vsize: 40180
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9474 0 0 0 114984 33 0 0 25 0 1 0 420618846 41340928 9387 4294967295 134512640 134672761 3221224640 3221223808 134561264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10093 9387 603 41 0 10052 0
vsize: 40372
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9484 0 0 0 115985 33 0 0 25 0 1 0 420618846 41340928 9397 4294967295 134512640 134672761 3221224640 3221223744 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10093 9397 603 41 0 10052 0
vsize: 40372
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9486 0 0 0 116985 33 0 0 25 0 1 0 420618846 41340928 9399 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10093 9399 603 41 0 10052 0
vsize: 40372
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9534 0 0 0 117985 33 0 0 25 0 1 0 420618846 41611264 9447 4294967295 134512640 134672761 3221224640 3221223808 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10159 9447 603 41 0 10118 0
vsize: 40636
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9715 0 0 0 118984 33 0 0 25 0 1 0 420618846 42278912 9628 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10322 9628 603 41 0 10281 0
vsize: 41288
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22589
Raw data (stat): 22589 (minisat+) R 22588 20937 20936 0 -1 0 9941 0 0 0 119984 34 0 0 25 0 1 0 420618846 43216896 9854 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10551 9854 603 41 0 10510 0
vsize: 42204
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 22589
Raw data (stat): 22589 (minisat+) Z 22588 20937 20936 0 -1 12 9944 0 0 0 119984 36 0 0 25 0 1 0 420618846 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: 10
Real time (s): 1200.05
CPU time (s): 1200.21
CPU user time (s): 1199.84
CPU system time (s): 0.365944
CPU usage (%): 100.013
Max. virtual memory (Kb): 42204
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####