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/sorensson/garden/normalized-g15x15.opb
MD5SUM	6a083b86cc55025d2acb3bcf68562064
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	54
Optimality of the best value was proved	NO
Number of terms in the objective function	225
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	225
Number of bits of the sum of numbers in the objective function	8
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	225
Number of bits of the biggest sum of numbers	8
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.01784
Number of variables	225
Total number of constraints	225
Number of constraints which are clauses	225
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	3
Maximum length of a constraint	5
Trace number 6506

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-14 05:28:09 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4964 boxname=wulflinc17 idbench=382 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6a083b86cc55025d2acb3bcf68562064  /oldhome/oroussel/tmp/wulflinc17/normalized-g15x15.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc17/normalized-g15x15.opb /oldhome/oroussel/tmp/wulflinc17/normalized-g15x15.opb
IDLAUNCH: 4964
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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:        815496 kB
Buffers:         36432 kB
Cached:         147988 kB
SwapCached:       2376 kB
Active:          60308 kB
Inactive:       129412 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        815244 kB
SwapTotal:     2097892 kB
SwapFree:      2095516 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7036 kB
Slab:            23688 kB
Committed_AS:    63704 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 05:48:11 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 4964 7 1200.22 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 225 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |     225     1065 |      67       0        0     nan |  0.000 % |
c   -- subsuming                       
c |         0 |     225     1065 |      90       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.016997 s)
c ==============================================================================
c [1mFound solution: 75[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 6660     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    7889    18962 |    2366       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5234          
c   -- var.elim.:  2000/5234          
c   -- var.elim.:  3000/5234          
c   -- var.elim.:  4000/5234          
c   -- var.elim.:  5000/5234          
c   -- var.elim.:  5234/5234          
c   -- var.elim.:  1000/2595          
c   -- var.elim.:  2000/2595          
c   -- var.elim.:  2595/2595          
c   -- subsuming                       
c   -- var.elim.:  1000/2071          
c   -- var.elim.:  2000/2071          
c   -- var.elim.:  2071/2071          
c |         0 |    5328    28873 |      --       0       --      -- |     --   | -2552/9938
c |         0 |    5328    28873 |    2131       0        0     nan |  0.000 % |
c |       100 |    5292    28676 |    2328      97     1970    20.3 |  0.998 % |
c |       250 |    5259    28467 |    2545     245     5538    22.6 |  1.612 % |
c |       478 |    5241    28366 |    2790     471    10432    22.1 |  1.919 % |
c |       816 |    5215    28212 |    3054     806    20351    25.2 |  2.419 % |
c |      1323 |    5215    28212 |    3359    1313    46898    35.7 |  2.419 % |
c |      2082 |    5215    28212 |    3695    2072    64056    30.9 |  2.418 % |
c |      3223 |    5215    28212 |    4065    3213   126428    39.3 |  2.418 % |
c ==============================================================================
c (current CPU-time: 2.77958 s)
c ==============================================================================
c [1mFound solution: 62[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      4508 |    5630    29283 |    1688    4498   183045    40.7 |  2.418 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1023          
c   -- var.elim.:  1023/1023          
c   -- var.elim.:  282/282          
c   -- subsuming                       
c   -- var.elim.:  61/61          
c |      4508 |    5353    29386 |      --    4498       --      -- |     --   | -277/104
c |      4508 |    5353    29386 |    2141    4498   183045    40.7 |  2.418 % |
c |      4608 |    5353    29386 |    2355    2100    76650    36.5 |  2.736 % |
c |      4759 |    5338    29282 |    2583    2248    80013    35.6 |  3.002 % |
c |      4987 |    5310    29127 |    2827    2456    86363    35.2 |  3.457 % |
c |      5325 |    5310    29127 |    3109    2794    92649    33.2 |  3.457 % |
c |      5831 |    5310    29127 |    3420    3300   109525    33.2 |  3.458 % |
c |      6590 |    5310    29127 |    3762    2839    68437    24.1 |  3.457 % |
c |      7729 |    5310    29127 |    4139    3978   115876    29.1 |  3.457 % |
c |      9438 |    5287    28996 |    4533    3912   117304    30.0 |  3.875 % |
c |     12003 |    5287    28996 |    4986    4688   154498    33.0 |  3.875 % |
c |     15848 |    5287    28996 |    5485    4954   132180    26.7 |  3.875 % |
c |     21614 |    5287    28996 |    6033    4488   160658    35.8 |  3.876 % |
c |     30263 |    5281    28942 |    6629    6451   264523    41.0 |  3.990 % |
c |     43237 |    5274    28904 |    7282    6728   362480    53.9 |  4.103 % |
c |     62699 |    5274    28904 |    8011    7168   224537    31.3 |  4.103 % |
c |     91891 |    5272    28889 |    8808    7043   326506    46.4 |  4.141 % |
c |    135683 |    5272    28889 |    9689    6779   495894    73.2 |  4.141 % |
c |    201369 |    5272    28889 |   10658    8264   399678    48.4 |  4.141 % |
c |    299895 |    5244    28735 |   11662    7728   459711    59.5 |  4.635 % |
c ==============================================================================
c (current CPU-time: 222.532 s)
c ==============================================================================
c [1mFound solution: 60[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    343589 |    5354    28990 |    1606   10454   663778    63.5 |  4.635 % |
c   -- subsuming                       
c   -- var.elim.:  893/893          
c   -- var.elim.:  167/167          
c |    343589 |    5279    28974 |      --   10454       --      -- |     --   | -75/-15
c |    343589 |    5279    28974 |    2111    8538   434555    50.9 |  4.635 % |
c |    343689 |    5273    28943 |    2320    1786    38864    21.8 |  4.861 % |
c |    343839 |    5273    28943 |    2552    1936    41058    21.2 |  4.861 % |
c |    344066 |    5273    28943 |    2807    2163    47294    21.9 |  4.861 % |
c |    344403 |    5273    28943 |    3088    2500    53773    21.5 |  4.861 % |
c |    344909 |    5273    28943 |    3396    3006    61983    20.6 |  4.861 % |
c |    345668 |    5273    28943 |    3736    3765   108488    28.8 |  4.861 % |
c |    346809 |    5273    28943 |    4110    3424   115545    33.7 |  4.861 % |
c |    348517 |    5273    28943 |    4521    3549   105342    29.7 |  4.861 % |
c |    351079 |    5273    28943 |    4973    4396   133051    30.3 |  4.861 % |
c |    354923 |    5248    28793 |    5444    4497   229341    51.0 |  5.317 % |
c |    360690 |    5248    28793 |    5989    4137   133627    32.3 |  5.317 % |
c |    369340 |    5248    28793 |    6588    6212   237754    38.3 |  5.317 % |
c |    382316 |    5248    28793 |    7247    5002   335632    67.1 |  5.317 % |
c |    401777 |    5246    28774 |    7968    5945   158134    26.6 |  5.355 % |
c |    430969 |    5246    28774 |    8765    6645   748131   112.6 |  5.355 % |
c |    474758 |    5246    28774 |    9642    6731   422780    62.8 |  5.355 % |
c ==============================================================================
c (current CPU-time: 305.38 s)
c ==============================================================================
c [1mFound solution: #### 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.91 0.97 0.91 2/55 29683
Raw data (stat): 29683 (runsolver) R 29682 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482078128 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99995 s]
Raw data (loadavg): 0.93 0.97 0.91 2/55 29683
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 1428 0 0 0 995 4 0 0 25 0 1 0 482078128 7282688 1331 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1778 1331 603 41 0 1737 0
vsize: 7112
[startup+20.0003 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 29683
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 1691 0 0 0 1993 5 0 0 25 0 1 0 482078128 8351744 1594 4294967295 134512640 134672761 3221224576 3221223560 1075353266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2039 1594 603 41 0 1998 0
vsize: 8156
[startup+30.0005 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 29683
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 1691 0 0 0 2994 5 0 0 25 0 1 0 482078128 8351744 1594 4294967295 134512640 134672761 3221224576 3221223712 134614756 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2039 1594 603 41 0 1998 0
vsize: 8156
[startup+40.0005 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 29683
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 1867 0 0 0 3993 5 0 0 25 0 1 0 482078128 9072640 1770 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2215 1770 603 41 0 2174 0
vsize: 8860
[startup+50.001 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 29683
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 1944 0 0 0 4993 5 0 0 25 0 1 0 482078128 9334784 1847 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2279 1847 603 41 0 2238 0
vsize: 9116
[startup+60.0004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 29683
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 2217 0 0 0 5993 6 0 0 25 0 1 0 482078128 10461184 2120 4294967295 134512640 134672761 3221224576 3221223760 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2554 2120 603 41 0 2513 0
vsize: 10216
[startup+70.0012 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 29683
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 2304 0 0 0 6993 6 0 0 25 0 1 0 482078128 10829824 2207 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2644 2207 603 41 0 2603 0
vsize: 10576
[startup+80.0019 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 29683
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 2365 0 0 0 7993 6 0 0 25 0 1 0 482078128 11063296 2268 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2701 2268 603 41 0 2660 0
vsize: 10804
[startup+90.0022 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 29683
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 2398 0 0 0 8993 6 0 0 25 0 1 0 482078128 11239424 2301 4294967295 134512640 134672761 3221224576 3221223760 134615622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2744 2301 603 41 0 2703 0
vsize: 10976
[startup+100.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 29683
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 2398 0 0 0 9993 6 0 0 25 0 1 0 482078128 11239424 2301 4294967295 134512640 134672761 3221224576 3221223760 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2744 2301 603 41 0 2703 0
vsize: 10976
[startup+110.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 29683
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 2404 0 0 0 10994 6 0 0 25 0 1 0 482078128 11239424 2307 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2744 2307 603 41 0 2703 0
vsize: 10976
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29683
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 2412 0 0 0 11994 7 0 0 25 0 1 0 482078128 11239424 2315 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2744 2315 603 41 0 2703 0
vsize: 10976
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29683
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 2415 0 0 0 12994 7 0 0 25 0 1 0 482078128 11239424 2318 4294967295 134512640 134672761 3221224576 3221223672 134616123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2744 2318 603 41 0 2703 0
vsize: 10976
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29683
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 2423 0 0 0 13994 7 0 0 25 0 1 0 482078128 11317248 2326 4294967295 134512640 134672761 3221224576 3221223616 134612799 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2763 2326 603 41 0 2722 0
vsize: 11052
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 2423 0 0 0 14994 7 0 0 25 0 1 0 482078128 11317248 2326 4294967295 134512640 134672761 3221224576 3221223760 134615585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2763 2326 603 41 0 2722 0
vsize: 11052
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 2435 0 0 0 15995 7 0 0 25 0 1 0 482078128 11464704 2338 4294967295 134512640 134672761 3221224576 3221223740 134614476 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2799 2338 603 41 0 2758 0
vsize: 11196
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 2509 0 0 0 16995 7 0 0 25 0 1 0 482078128 11685888 2412 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2853 2412 603 41 0 2812 0
vsize: 11412
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 2643 0 0 0 17994 7 0 0 25 0 1 0 482078128 12210176 2546 4294967295 134512640 134672761 3221224576 3221223568 134565101 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2981 2546 603 41 0 2940 0
vsize: 11924
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 2644 0 0 0 18994 8 0 0 25 0 1 0 482078128 12210176 2547 4294967295 134512640 134672761 3221224576 3221223760 134615554 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2981 2547 603 41 0 2940 0
vsize: 11924
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 2661 0 0 0 19994 8 0 0 25 0 1 0 482078128 12320768 2564 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3008 2564 603 41 0 2967 0
vsize: 12032
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 2665 0 0 0 20994 8 0 0 25 0 1 0 482078128 12320768 2568 4294967295 134512640 134672761 3221224576 3221223760 134615734 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3008 2568 603 41 0 2967 0
vsize: 12032
[startup+220.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 2803 0 0 0 21993 8 0 0 25 0 1 0 482078128 12845056 2706 4294967295 134512640 134672761 3221224576 3221223760 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3136 2706 603 41 0 3095 0
vsize: 12544
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 3034 0 0 0 22993 9 0 0 25 0 1 0 482078128 13033472 2761 4294967295 134512640 134672761 3221224576 3221223672 134616347 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3182 2761 603 41 0 3141 0
vsize: 12728
[startup+240.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 3034 0 0 0 23993 9 0 0 25 0 1 0 482078128 13033472 2761 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3182 2761 603 41 0 3141 0
vsize: 12728
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 3034 0 0 0 24993 9 0 0 25 0 1 0 482078128 13033472 2761 4294967295 134512640 134672761 3221224576 3221223680 134604323 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3182 2761 603 41 0 3141 0
vsize: 12728
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 3120 0 0 0 25992 10 0 0 25 0 1 0 482078128 13426688 2847 4294967295 134512640 134672761 3221224576 3221223616 134612606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3278 2847 603 41 0 3237 0
vsize: 13112
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 3388 0 0 0 26992 10 0 0 25 0 1 0 482078128 14536704 3115 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3549 3115 603 41 0 3508 0
vsize: 14196
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 3391 0 0 0 27992 10 0 0 25 0 1 0 482078128 14536704 3118 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3549 3118 603 41 0 3508 0
vsize: 14196
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 3391 0 0 0 28992 10 0 0 25 0 1 0 482078128 14536704 3118 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3549 3118 603 41 0 3508 0
vsize: 14196
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 3391 0 0 0 29992 10 0 0 25 0 1 0 482078128 14536704 3118 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3549 3118 603 41 0 3508 0
vsize: 14196
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 3487 0 0 0 30991 11 0 0 25 0 1 0 482078128 14573568 3142 4294967295 134512640 134672761 3221224576 3221223728 134614555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3558 3142 603 41 0 3517 0
vsize: 14232
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 3487 0 0 0 31992 11 0 0 25 0 1 0 482078128 14573568 3142 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3558 3142 603 41 0 3517 0
vsize: 14232
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 3487 0 0 0 32992 11 0 0 25 0 1 0 482078128 14573568 3142 4294967295 134512640 134672761 3221224576 3221223776 134610644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3558 3142 603 41 0 3517 0
vsize: 14232
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 3487 0 0 0 33992 11 0 0 25 0 1 0 482078128 14573568 3142 4294967295 134512640 134672761 3221224576 3221223716 134616883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3558 3142 603 41 0 3517 0
vsize: 14232
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 3487 0 0 0 34992 11 0 0 25 0 1 0 482078128 14573568 3142 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3558 3142 603 41 0 3517 0
vsize: 14232
[startup+360.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 3487 0 0 0 35992 11 0 0 25 0 1 0 482078128 14573568 3142 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3558 3142 603 41 0 3517 0
vsize: 14232
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 3491 0 0 0 36993 11 0 0 25 0 1 0 482078128 14671872 3146 4294967295 134512640 134672761 3221224576 3221223712 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3582 3146 603 41 0 3541 0
vsize: 14328
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 3517 0 0 0 37993 11 0 0 25 0 1 0 482078128 14786560 3172 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3610 3172 603 41 0 3569 0
vsize: 14440
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 3520 0 0 0 38993 11 0 0 25 0 1 0 482078128 14778368 3175 4294967295 134512640 134672761 3221224576 3221223760 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3608 3175 603 41 0 3567 0
vsize: 14432
[startup+400.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 3520 0 0 0 39993 11 0 0 25 0 1 0 482078128 14778368 3175 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3608 3175 603 41 0 3567 0
vsize: 14432
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 3520 0 0 0 40993 11 0 0 25 0 1 0 482078128 14778368 3175 4294967295 134512640 134672761 3221224576 3221223616 134614182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3608 3175 603 41 0 3567 0
vsize: 14432
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 3546 0 0 0 41993 12 0 0 25 0 1 0 482078128 14893056 3201 4294967295 134512640 134672761 3221224576 3221223760 134616004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3636 3201 603 41 0 3595 0
vsize: 14544
[startup+430.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 3546 0 0 0 42993 12 0 0 25 0 1 0 482078128 14872576 3201 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3631 3201 603 41 0 3590 0
vsize: 14524
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29685
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 3546 0 0 0 43993 12 0 0 25 0 1 0 482078128 14872576 3201 4294967295 134512640 134672761 3221224576 3221223616 134614335 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3631 3201 603 41 0 3590 0
vsize: 14524
[startup+450.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 3546 0 0 0 44993 12 0 0 25 0 1 0 482078128 14872576 3201 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3631 3201 603 41 0 3590 0
vsize: 14524
[startup+460.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 3546 0 0 0 45994 12 0 0 25 0 1 0 482078128 14872576 3201 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3631 3201 603 41 0 3590 0
vsize: 14524
[startup+470.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 3546 0 0 0 46994 12 0 0 25 0 1 0 482078128 14872576 3201 4294967295 134512640 134672761 3221224576 3221223760 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3631 3201 603 41 0 3590 0
vsize: 14524
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 3575 0 0 0 47994 12 0 0 25 0 1 0 482078128 14995456 3230 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3661 3230 603 41 0 3620 0
vsize: 14644
[startup+490.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 3767 0 0 0 48994 12 0 0 25 0 1 0 482078128 15790080 3422 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3855 3422 603 41 0 3814 0
vsize: 15420
[startup+500.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4018 0 0 0 49993 13 0 0 25 0 1 0 482078128 16785408 3673 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4098 3673 603 41 0 4057 0
vsize: 16392
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4026 0 0 0 50993 13 0 0 25 0 1 0 482078128 16855040 3681 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4115 3681 603 41 0 4074 0
vsize: 16460
[startup+520.01 s]
Raw data (loadavg): 1.07 0.99 0.92 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4057 0 0 0 51993 13 0 0 25 0 1 0 482078128 16982016 3712 4294967295 134512640 134672761 3221224576 3221223760 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4146 3712 603 41 0 4105 0
vsize: 16584
[startup+530.01 s]
Raw data (loadavg): 1.06 0.99 0.92 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4062 0 0 0 52994 13 0 0 25 0 1 0 482078128 16982016 3717 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4146 3717 603 41 0 4105 0
vsize: 16584
[startup+540.011 s]
Raw data (loadavg): 1.05 0.99 0.92 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4062 0 0 0 53994 13 0 0 25 0 1 0 482078128 16982016 3717 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4146 3717 603 41 0 4105 0
vsize: 16584
[startup+550.011 s]
Raw data (loadavg): 1.04 0.99 0.92 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4062 0 0 0 54994 13 0 0 25 0 1 0 482078128 16982016 3717 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4146 3717 603 41 0 4105 0
vsize: 16584
[startup+560.011 s]
Raw data (loadavg): 1.03 0.99 0.92 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4063 0 0 0 55994 13 0 0 25 0 1 0 482078128 16982016 3718 4294967295 134512640 134672761 3221224576 3221223760 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4146 3718 603 41 0 4105 0
vsize: 16584
[startup+570.011 s]
Raw data (loadavg): 1.03 0.99 0.92 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4088 0 0 0 56994 13 0 0 25 0 1 0 482078128 17113088 3743 4294967295 134512640 134672761 3221224576 3221223760 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4178 3743 603 41 0 4137 0
vsize: 16712
[startup+580.01 s]
Raw data (loadavg): 1.02 0.99 0.92 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4088 0 0 0 57994 13 0 0 25 0 1 0 482078128 17113088 3743 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4178 3743 603 41 0 4137 0
vsize: 16712
[startup+590.01 s]
Raw data (loadavg): 1.02 0.99 0.92 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4280 0 0 0 58994 14 0 0 25 0 1 0 482078128 17887232 3935 4294967295 134512640 134672761 3221224576 3221223760 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4367 3935 603 41 0 4326 0
vsize: 17468
[startup+600.011 s]
Raw data (loadavg): 1.02 0.99 0.92 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4316 0 0 0 59994 15 0 0 25 0 1 0 482078128 18018304 3971 4294967295 134512640 134672761 3221224576 3221223616 134614246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4399 3971 603 41 0 4358 0
vsize: 17596
[startup+610.011 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4316 0 0 0 60994 15 0 0 25 0 1 0 482078128 18018304 3971 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4399 3971 603 41 0 4358 0
vsize: 17596
[startup+620.011 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4356 0 0 0 61994 15 0 0 25 0 1 0 482078128 18149376 4011 4294967295 134512640 134672761 3221224576 3221223776 134610602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4431 4011 603 41 0 4390 0
vsize: 17724
[startup+630.011 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4367 0 0 0 62994 15 0 0 25 0 1 0 482078128 18247680 4022 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4455 4022 603 41 0 4414 0
vsize: 17820
[startup+640.012 s]
Raw data (loadavg): 1.01 0.99 0.92 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4367 0 0 0 63994 15 0 0 25 0 1 0 482078128 18247680 4022 4294967295 134512640 134672761 3221224576 3221223672 134616161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4455 4022 603 41 0 4414 0
vsize: 17820
[startup+650.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4465 0 0 0 64994 15 0 0 25 0 1 0 482078128 18640896 4120 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4551 4120 603 41 0 4510 0
vsize: 18204
[startup+660.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4591 0 0 0 65994 15 0 0 25 0 1 0 482078128 19128320 4246 4294967295 134512640 134672761 3221224576 3221223616 134612992 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4670 4246 603 41 0 4629 0
vsize: 18680
[startup+670.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4594 0 0 0 66994 15 0 0 25 0 1 0 482078128 19128320 4249 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4670 4249 603 41 0 4629 0
vsize: 18680
[startup+680.011 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4594 0 0 0 67994 16 0 0 25 0 1 0 482078128 19128320 4249 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4670 4249 603 41 0 4629 0
vsize: 18680
[startup+690.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4594 0 0 0 68994 16 0 0 25 0 1 0 482078128 19128320 4249 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4670 4249 603 41 0 4629 0
vsize: 18680
[startup+700.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4594 0 0 0 69995 16 0 0 25 0 1 0 482078128 19128320 4249 4294967295 134512640 134672761 3221224576 3221223616 134612827 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4670 4249 603 41 0 4629 0
vsize: 18680
[startup+710.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4594 0 0 0 70995 16 0 0 25 0 1 0 482078128 19128320 4249 4294967295 134512640 134672761 3221224576 3221223616 134612663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4670 4249 603 41 0 4629 0
vsize: 18680
[startup+720.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4599 0 0 0 71995 16 0 0 25 0 1 0 482078128 19210240 4254 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4254 603 41 0 4649 0
vsize: 18760
[startup+730.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4599 0 0 0 72995 16 0 0 25 0 1 0 482078128 19210240 4254 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4254 603 41 0 4649 0
vsize: 18760
[startup+740.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29687
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4599 0 0 0 73995 16 0 0 25 0 1 0 482078128 19210240 4254 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4254 603 41 0 4649 0
vsize: 18760
[startup+750.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4599 0 0 0 74995 16 0 0 25 0 1 0 482078128 19210240 4254 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4254 603 41 0 4649 0
vsize: 18760
[startup+760.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4599 0 0 0 75995 16 0 0 25 0 1 0 482078128 19210240 4254 4294967295 134512640 134672761 3221224576 3221223616 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4254 603 41 0 4649 0
vsize: 18760
[startup+770.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4599 0 0 0 76995 16 0 0 25 0 1 0 482078128 19210240 4254 4294967295 134512640 134672761 3221224576 3221223616 134612764 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4254 603 41 0 4649 0
vsize: 18760
[startup+780.012 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4599 0 0 0 77996 16 0 0 25 0 1 0 482078128 19210240 4254 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4254 603 41 0 4649 0
vsize: 18760
[startup+790.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4599 0 0 0 78996 16 0 0 25 0 1 0 482078128 19210240 4254 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4254 603 41 0 4649 0
vsize: 18760
[startup+800.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4599 0 0 0 79996 16 0 0 25 0 1 0 482078128 19210240 4254 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4254 603 41 0 4649 0
vsize: 18760
[startup+810.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4599 0 0 0 80996 17 0 0 25 0 1 0 482078128 19210240 4254 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4254 603 41 0 4649 0
vsize: 18760
[startup+820.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4599 0 0 0 81996 17 0 0 25 0 1 0 482078128 19210240 4254 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4254 603 41 0 4649 0
vsize: 18760
[startup+830.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4599 0 0 0 82996 17 0 0 25 0 1 0 482078128 19210240 4254 4294967295 134512640 134672761 3221224576 3221223760 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4254 603 41 0 4649 0
vsize: 18760
[startup+840.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4599 0 0 0 83996 17 0 0 25 0 1 0 482078128 19210240 4254 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4254 603 41 0 4649 0
vsize: 18760
[startup+850.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4608 0 0 0 84996 17 0 0 25 0 1 0 482078128 19210240 4263 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4263 603 41 0 4649 0
vsize: 18760
[startup+860.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4610 0 0 0 85997 17 0 0 25 0 1 0 482078128 19210240 4265 4294967295 134512640 134672761 3221224576 3221223760 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4265 603 41 0 4649 0
vsize: 18760
[startup+870.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4610 0 0 0 86997 17 0 0 25 0 1 0 482078128 19210240 4265 4294967295 134512640 134672761 3221224576 3221223740 134614476 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4265 603 41 0 4649 0
vsize: 18760
[startup+880.013 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4610 0 0 0 87997 17 0 0 25 0 1 0 482078128 19210240 4265 4294967295 134512640 134672761 3221224576 3221223604 134612938 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4265 603 41 0 4649 0
vsize: 18760
[startup+890.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4610 0 0 0 88997 17 0 0 25 0 1 0 482078128 19210240 4265 4294967295 134512640 134672761 3221224576 3221223760 134615711 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4265 603 41 0 4649 0
vsize: 18760
[startup+900.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4610 0 0 0 89997 17 0 0 25 0 1 0 482078128 19210240 4265 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4265 603 41 0 4649 0
vsize: 18760
[startup+910.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4610 0 0 0 90997 17 0 0 25 0 1 0 482078128 19210240 4265 4294967295 134512640 134672761 3221224576 3221223760 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4265 603 41 0 4649 0
vsize: 18760
[startup+920.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4610 0 0 0 91997 17 0 0 25 0 1 0 482078128 19210240 4265 4294967295 134512640 134672761 3221224576 3221223712 134614513 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4265 603 41 0 4649 0
vsize: 18760
[startup+930.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4610 0 0 0 92997 18 0 0 25 0 1 0 482078128 19210240 4265 4294967295 134512640 134672761 3221224576 3221223760 134615681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4265 603 41 0 4649 0
vsize: 18760
[startup+940.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4610 0 0 0 93998 18 0 0 25 0 1 0 482078128 19210240 4265 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4265 603 41 0 4649 0
vsize: 18760
[startup+950.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4610 0 0 0 94997 18 0 0 25 0 1 0 482078128 19210240 4265 4294967295 134512640 134672761 3221224576 3221223568 134565119 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4265 603 41 0 4649 0
vsize: 18760
[startup+960.014 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4610 0 0 0 95998 18 0 0 25 0 1 0 482078128 19210240 4265 4294967295 134512640 134672761 3221224576 3221223616 134612551 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4265 603 41 0 4649 0
vsize: 18760
[startup+970.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4610 0 0 0 96998 18 0 0 25 0 1 0 482078128 19210240 4265 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4265 603 41 0 4649 0
vsize: 18760
[startup+980.015 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4610 0 0 0 97998 18 0 0 25 0 1 0 482078128 19210240 4265 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4265 603 41 0 4649 0
vsize: 18760
[startup+990.016 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4610 0 0 0 98998 18 0 0 25 0 1 0 482078128 19210240 4265 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4265 603 41 0 4649 0
vsize: 18760
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4610 0 0 0 99998 18 0 0 25 0 1 0 482078128 19210240 4265 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4690 4265 603 41 0 4649 0
vsize: 18760
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4629 0 0 0 100998 18 0 0 25 0 1 0 482078128 19329024 4284 4294967295 134512640 134672761 3221224576 3221223700 134566077 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4719 4284 603 41 0 4678 0
vsize: 18876
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4633 0 0 0 101998 18 0 0 25 0 1 0 482078128 19329024 4288 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4719 4288 603 41 0 4678 0
vsize: 18876
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4633 0 0 0 102999 18 0 0 25 0 1 0 482078128 19329024 4288 4294967295 134512640 134672761 3221224576 3221223760 134615755 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4719 4288 603 41 0 4678 0
vsize: 18876
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29689
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4838 0 0 0 103998 18 0 0 25 0 1 0 482078128 20123648 4493 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4913 4493 603 41 0 4872 0
vsize: 19652
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29691
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4855 0 0 0 104999 19 0 0 25 0 1 0 482078128 20254720 4510 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4945 4510 603 41 0 4904 0
vsize: 19780
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29691
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4891 0 0 0 105999 19 0 0 25 0 1 0 482078128 20344832 4546 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4967 4546 603 41 0 4926 0
vsize: 19868
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29691
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4892 0 0 0 106999 19 0 0 25 0 1 0 482078128 20197376 4513 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4931 4513 603 41 0 4890 0
vsize: 19724
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29691
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4892 0 0 0 107999 19 0 0 25 0 1 0 482078128 20197376 4513 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4931 4513 603 41 0 4890 0
vsize: 19724
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29691
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4892 0 0 0 108999 19 0 0 25 0 1 0 482078128 20197376 4513 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4931 4513 603 41 0 4890 0
vsize: 19724
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29691
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4892 0 0 0 109999 19 0 0 25 0 1 0 482078128 20197376 4513 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4931 4513 603 41 0 4890 0
vsize: 19724
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29691
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4892 0 0 0 110999 19 0 0 25 0 1 0 482078128 20197376 4513 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4931 4513 603 41 0 4890 0
vsize: 19724
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29691
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4892 0 0 0 111999 19 0 0 25 0 1 0 482078128 20197376 4513 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4931 4513 603 41 0 4890 0
vsize: 19724
[startup+1130.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29691
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4892 0 0 0 112999 19 0 0 25 0 1 0 482078128 20197376 4513 4294967295 134512640 134672761 3221224576 3221223744 134615859 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4931 4513 603 41 0 4890 0
vsize: 19724
[startup+1140.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29691
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4892 0 0 0 113999 20 0 0 25 0 1 0 482078128 20197376 4513 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4931 4513 603 41 0 4890 0
vsize: 19724
[startup+1150.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29691
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4892 0 0 0 114999 20 0 0 25 0 1 0 482078128 20197376 4513 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4931 4513 603 41 0 4890 0
vsize: 19724
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29691
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4892 0 0 0 115999 20 0 0 25 0 1 0 482078128 20197376 4513 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4931 4513 603 41 0 4890 0
vsize: 19724
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29691
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4994 0 0 0 116999 20 0 0 25 0 1 0 482078128 20680704 4615 4294967295 134512640 134672761 3221224576 3221223760 134616011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5049 4615 603 41 0 5008 0
vsize: 20196
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29691
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4996 0 0 0 117999 20 0 0 25 0 1 0 482078128 20668416 4617 4294967295 134512640 134672761 3221224576 3221223760 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5046 4617 603 41 0 5005 0
vsize: 20184
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29691
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 4996 0 0 0 118999 20 0 0 25 0 1 0 482078128 20668416 4617 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5046 4617 603 41 0 5005 0
vsize: 20184
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.99 0.92 2/55 29691
Raw data (stat): 29683 (minisat+) R 29682 20838 20837 0 -1 0 5310 0 0 0 119999 21 0 0 25 0 1 0 482078128 21938176 4931 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5356 4931 603 41 0 5315 0
vsize: 21424
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.92 1/55 29691
Raw data (stat): 29683 (minisat+) Z 29682 20838 20837 0 -1 12 5311 0 0 0 119999 22 0 0 25 0 1 0 482078128 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.03
CPU time (s): 1200.22
CPU user time (s): 1199.99
CPU system time (s): 0.225965
CPU usage (%): 100.016
Max. virtual memory (Kb): 21424
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####