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-sao2.b.opb
MD5SUM	3e273bcee52631aeea0b7b1138e7d68d
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	25
Optimality of the best value was proved	NO
Number of terms in the objective function	373
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	373
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	373
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.03784
Number of variables	372
Total number of constraints	779
Number of constraints which are clauses	772
Number of constraints which are cardinality constraints (but not clauses)	7
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	98
Trace number 5427

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-13 23:54:26 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3833 boxname=wulflinc20 idbench=73 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3e273bcee52631aeea0b7b1138e7d68d  /oldhome/oroussel/tmp/wulflinc20/normalized-sao2.b.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc20/normalized-sao2.b.opb /oldhome/oroussel/tmp/wulflinc20/normalized-sao2.b.opb
IDLAUNCH: 3833
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        890428 kB
Buffers:         33844 kB
Cached:          74904 kB
SwapCached:       2636 kB
Active:          48088 kB
Inactive:        66148 kB
HighTotal:      131008 kB
HighFree:        52360 kB
LowTotal:       903652 kB
LowFree:        838068 kB
SwapTotal:     2097892 kB
SwapFree:      2095256 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            24396 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 00:14:28 (client local time) WITH STATUS 10 IN 1200.23 SECONDS
stats: 3833 7 1200.23 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 644 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 |     604    12117 |     181       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  277/277          
c |         0 |     508    11229 |      --       0       --      -- |     --   | -96/-888
c |         0 |     508    11229 |     203       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.12798 s)
c ==============================================================================
c [1mFound solution: 37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:13602     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         1 |   15627    46483 |    4688       1       28    28.0 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10025          
c   -- var.elim.:  2000/10025          
c   -- var.elim.:  3000/10025          
c   -- var.elim.:  4000/10025          
c   -- var.elim.:  5000/10025          
c   -- var.elim.:  6000/10025          
c   -- var.elim.:  7000/10025          
c   -- var.elim.:  8000/10025          
c   -- var.elim.:  9000/10025          
c   -- var.elim.:  10000/10025          
c   -- var.elim.:  10025/10025          
c   -- var.elim.:  1000/5029          
c   -- var.elim.:  2000/5029          
c   -- var.elim.:  3000/5029          
c   -- var.elim.:  4000/5029          
c   -- var.elim.:  5000/5029          
c   -- var.elim.:  5029/5029          
c   -- var.elim.:  1000/2637          
c   -- var.elim.:  2000/2637          
c   -- var.elim.:  2637/2637          
c   -- var.elim.:  1000/2405          
c   -- var.elim.:  2000/2405          
c   -- var.elim.:  2405/2405          
c   -- var.elim.:  974/974          
c   -- subsuming                       
c   -- var.elim.:  1000/3776          
c   -- var.elim.:  2000/3776          
c   -- var.elim.:  3000/3776          
c   -- var.elim.:  3776/3776          
c   -- var.elim.:  28/28          
c |         1 |   10064    64703 |      --       1       --      -- |     --   | -5335/18836
c |         1 |   10064    64703 |    4025       1       28    28.0 |  0.000 % |
c |       101 |   10035    64507 |    4415     100     4187    41.9 |  3.803 % |
c |       251 |   10011    63916 |    4845     245     7403    30.2 |  3.924 % |
c ==============================================================================
c (current CPU-time: 5.32619 s)
c ==============================================================================
c [1mFound solution: 29[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 |       327 |   11809    68999 |    3542     321    10172    31.7 |  3.924 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4543          
c   -- var.elim.:  2000/4543          
c   -- var.elim.:  3000/4543          
c   -- var.elim.:  4000/4543          
c   -- var.elim.:  4543/4543          
c   -- var.elim.:  1000/2917          
c   -- var.elim.:  2000/2917          
c   -- var.elim.:  2917/2917          
c   -- var.elim.:  1000/1715          
c   -- var.elim.:  1715/1715          
c   -- var.elim.:  832/832          
c   -- var.elim.:  185/185          
c   -- subsuming                       
c   -- var.elim.:  879/879          
c |       327 |    9738    59730 |      --     321       --      -- |     --   | -1781/-2658
c |       327 |    9738    59730 |    3895     306     9474    31.0 |  3.924 % |
c |       427 |    9738    59730 |    4284     406    12791    31.5 |  5.120 % |
c |       577 |    9738    59730 |    4713     556    20151    36.2 |  5.120 % |
c |       802 |    9536    57524 |    5076     775    28398    36.6 |  5.963 % |
c |      1140 |    9534    57510 |    5583    1112    42989    38.7 |  5.984 % |
c |      1647 |    9520    57426 |    6132    1605    63154    39.3 |  6.066 % |
c |      2407 |    9520    57426 |    6746    2365   114666    48.5 |  6.066 % |
c |      3547 |    9520    57426 |    7420    3505   217013    61.9 |  6.066 % |
c |      5255 |    9520    57426 |    8162    5213   356633    68.4 |  6.066 % |
c ==============================================================================
c (current CPU-time: 12.1292 s)
c ==============================================================================
c [1mFound solution: 28[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 |      5568 |   11856    64120 |    3556    5526   376901    68.2 |  6.066 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4383          
c   -- var.elim.:  2000/4383          
c   -- var.elim.:  3000/4383          
c   -- var.elim.:  4000/4383          
c   -- var.elim.:  4383/4383          
c   -- var.elim.:  1000/2436          
c   -- var.elim.:  2000/2436          
c   -- var.elim.:  2436/2436          
c   -- var.elim.:  1000/2034          
c   -- var.elim.:  2000/2034          
c   -- var.elim.:  2034/2034          
c   -- var.elim.:  610/610          
c   -- subsuming                       
c   -- var.elim.:  451/451          
c |      5568 |    9447    57878 |      --    5526       --      -- |     --   | -2408/-6239
c |      5568 |    9447    57878 |    3778    5479   373951    68.3 |  6.066 % |
c |      5668 |    9447    57878 |    4156    3753   278305    74.2 |  6.245 % |
c |      5818 |    9447    57878 |    4572    3903   283159    72.5 |  6.245 % |
c |      6043 |    9447    57878 |    5029    4128   294555    71.4 |  6.245 % |
c |      6380 |    9447    57878 |    5532    4465   315040    70.6 |  6.245 % |
c |      6886 |    9447    57878 |    6085    4971   358779    72.2 |  6.245 % |
c |      7647 |    9447    57878 |    6694    5732   436703    76.2 |  6.245 % |
c |      8787 |    9447    57878 |    7363    6872   517750    75.3 |  6.245 % |
c |     10495 |    9447    57878 |    8100    5808   380872    65.6 |  6.245 % |
c |     13061 |    9447    57878 |    8910    8374   591415    70.6 |  6.245 % |
c |     16905 |    9447    57878 |    9801    9007   651404    72.3 |  6.245 % |
c ==============================================================================
c (current CPU-time: 28.9196 s)
c ==============================================================================
c [1mFound solution: 27[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 |     18520 |    9467    57926 |    2840   10622   822416    77.4 |  6.245 % |
c   -- subsuming                       
c   -- var.elim.:  87/87          
c   -- var.elim.:  23/23          
c   -- var.elim.:  7/7          
c |     18520 |    9440    57819 |      --   10622       --      -- |     --   | -13/-13
c |     18520 |    9440    57819 |    3776    9271   690339    74.5 |  6.245 % |
c |     18621 |    9440    57819 |    4153    2849   215508    75.6 |  6.348 % |
c |     18772 |    9440    57819 |    4568    3000   221502    73.8 |  6.348 % |
c |     18997 |    9440    57819 |    5025    3225   234327    72.7 |  6.348 % |
c |     19335 |    9440    57819 |    5528    3563   253208    71.1 |  6.348 % |
c |     19841 |    9440    57819 |    6081    4069   278041    68.3 |  6.348 % |
c |     20601 |    9434    57783 |    6685    4828   330729    68.5 |  6.390 % |
c |     21740 |    9434    57783 |    7353    5967   399251    66.9 |  6.390 % |
c |     23449 |    9434    57783 |    8089    7676   514882    67.1 |  6.390 % |
c |     26012 |    9434    57783 |    8897    6914   448865    64.9 |  6.390 % |
c |     29856 |    9434    57783 |    9787    7527   502952    66.8 |  6.390 % |
c |     35622 |    9434    57783 |   10766    9669   586924    60.7 |  6.390 % |
c |     44272 |    9434    57783 |   11843   10377   665874    64.2 |  6.390 % |
c |     57246 |    9434    57783 |   13027   10737   818214    76.2 |  6.390 % |
c |     76707 |    9434    57783 |   14330   10790   849933    78.8 |  6.390 % |
c |    105900 |    9434    57783 |   15763   13742  1241204    90.3 |  6.390 % |
c |    149691 |    9434    57783 |   17339   11469  1101825    96.1 |  6.390 % |
c ==============================================================================
c (current CPU-time: 283.561 s)
c ==============================================================================
c [1mFound solution: 26[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 |    174427 |   12539    66455 |    3761   17339  1740051   100.4 |  6.390 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5078          
c   -- var.elim.:  2000/5078          
c   -- var.elim.:  3000/5078          
c   -- var.elim.:  4000/5078          
c   -- var.elim.:  5000/5078          
c   -- var.elim.:  5078/5078          
c   -- var.elim.:  1000/2606          
c   -- var.elim.:  2000/2606          
c   -- var.elim.:  2606/2606          
c   -- var.elim.:  1000/2301          
c   -- var.elim.:  2000/2301          
c   -- var.elim.:  2301/2301          
c   -- var.elim.:  916/916          
c   -- subsuming                       
c |    174427 |    9447    57861 |      --   17339       --      -- |     --   | -3089/-8587
c |    174427 |    9447    57861 |    3778   17339  1740051   100.4 |  6.390 % |
c |    174527 |    9447    57861 |    4156    3526   242832    #### 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.84 0.94 0.90 2/54 31893
Raw data (stat): 31893 (runsolver) R 31892 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480067393 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+10.0009 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 2206 0 0 0 990 8 0 0 25 0 1 0 480067393 9568256 1884 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2336 1884 603 41 0 2295 0
vsize: 9344
[startup+20.0003 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 2927 0 0 0 1986 12 0 0 25 0 1 0 480067393 11927552 2465 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2912 2465 603 41 0 2871 0
vsize: 11648
[startup+30.0012 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 3687 0 0 0 2982 15 0 0 25 0 1 0 480067393 14319616 3059 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3496 3059 603 41 0 3455 0
vsize: 13984
[startup+40.0011 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 3687 0 0 0 3981 15 0 0 25 0 1 0 480067393 14319616 3059 4294967295 134512640 134672761 3221224576 3221223672 134616339 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3496 3059 603 41 0 3455 0
vsize: 13984
[startup+50.0015 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 3687 0 0 0 4982 15 0 0 25 0 1 0 480067393 14319616 3059 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3496 3059 603 41 0 3455 0
vsize: 13984
[startup+60.0015 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 3689 0 0 0 5982 16 0 0 25 0 1 0 480067393 14319616 3061 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3496 3061 603 41 0 3455 0
vsize: 13984
[startup+70.0012 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 3689 0 0 0 6982 16 0 0 25 0 1 0 480067393 14319616 3061 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3496 3061 603 41 0 3455 0
vsize: 13984
[startup+80.0017 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 3881 0 0 0 7981 16 0 0 25 0 1 0 480067393 15056896 3253 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3676 3253 603 41 0 3635 0
vsize: 14704
[startup+90.0016 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 3911 0 0 0 8982 16 0 0 25 0 1 0 480067393 15183872 3283 4294967295 134512640 134672761 3221224576 3221223760 134615622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3707 3283 603 41 0 3666 0
vsize: 14828
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 4032 0 0 0 9981 17 0 0 25 0 1 0 480067393 15667200 3404 4294967295 134512640 134672761 3221224576 3221223616 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3825 3404 603 41 0 3784 0
vsize: 15300
[startup+110.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 4071 0 0 0 10982 17 0 0 25 0 1 0 480067393 15798272 3443 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3857 3443 603 41 0 3816 0
vsize: 15428
[startup+120.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 4076 0 0 0 11982 17 0 0 25 0 1 0 480067393 15798272 3448 4294967295 134512640 134672761 3221224576 3221223616 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3857 3448 603 41 0 3816 0
vsize: 15428
[startup+130.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 4076 0 0 0 12982 17 0 0 25 0 1 0 480067393 15798272 3448 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3857 3448 603 41 0 3816 0
vsize: 15428
[startup+140.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 4237 0 0 0 13982 17 0 0 25 0 1 0 480067393 16642048 3609 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4063 3609 603 41 0 4022 0
vsize: 16252
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 4313 0 0 0 14982 17 0 0 25 0 1 0 480067393 16859136 3685 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4116 3685 603 41 0 4075 0
vsize: 16464
[startup+160.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 4501 0 0 0 15981 18 0 0 25 0 1 0 480067393 17637376 3873 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4306 3873 603 41 0 4265 0
vsize: 17224
[startup+170.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 4501 0 0 0 16981 18 0 0 25 0 1 0 480067393 17637376 3873 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4306 3873 603 41 0 4265 0
vsize: 17224
[startup+180.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 4635 0 0 0 17981 18 0 0 25 0 1 0 480067393 18206720 4006 4294967295 134512640 134672761 3221224576 3221223760 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4445 4006 603 41 0 4404 0
vsize: 17780
[startup+190.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 4886 0 0 0 18980 19 0 0 25 0 1 0 480067393 19238912 4257 4294967295 134512640 134672761 3221224576 3221223760 134615611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4697 4257 603 41 0 4656 0
vsize: 18788
[startup+200.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 4891 0 0 0 19980 20 0 0 25 0 1 0 480067393 19238912 4262 4294967295 134512640 134672761 3221224576 3221223700 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4697 4262 603 41 0 4656 0
vsize: 18788
[startup+210.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 4917 0 0 0 20981 20 0 0 25 0 1 0 480067393 19374080 4287 4294967295 134512640 134672761 3221224576 3221223760 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4730 4287 603 41 0 4689 0
vsize: 18920
[startup+220.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 4924 0 0 0 21981 20 0 0 25 0 1 0 480067393 19390464 4293 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4734 4293 603 41 0 4693 0
vsize: 18936
[startup+230.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 4934 0 0 0 22981 20 0 0 25 0 1 0 480067393 19423232 4302 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4742 4302 603 41 0 4701 0
vsize: 18968
[startup+240.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 4934 0 0 0 23981 20 0 0 25 0 1 0 480067393 19423232 4302 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4742 4302 603 41 0 4701 0
vsize: 18968
[startup+250.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5073 0 0 0 24981 20 0 0 25 0 1 0 480067393 19984384 4440 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4879 4440 603 41 0 4838 0
vsize: 19516
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5093 0 0 0 25981 20 0 0 25 0 1 0 480067393 20074496 4460 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4901 4460 603 41 0 4860 0
vsize: 19604
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5093 0 0 0 26981 20 0 0 25 0 1 0 480067393 20074496 4460 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4901 4460 603 41 0 4860 0
vsize: 19604
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5102 0 0 0 27981 21 0 0 25 0 1 0 480067393 20107264 4468 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4909 4468 603 41 0 4868 0
vsize: 19636
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5557 0 0 0 28977 24 0 0 25 0 1 0 480067393 21987328 4757 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4757 603 41 0 5327 0
vsize: 21472
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5557 0 0 0 29977 24 0 0 25 0 1 0 480067393 21987328 4757 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4757 603 41 0 5327 0
vsize: 21472
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5557 0 0 0 30977 25 0 0 25 0 1 0 480067393 21987328 4757 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4757 603 41 0 5327 0
vsize: 21472
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5557 0 0 0 31977 25 0 0 25 0 1 0 480067393 21987328 4757 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4757 603 41 0 5327 0
vsize: 21472
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 31893
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5557 0 0 0 32977 25 0 0 25 0 1 0 480067393 21987328 4757 4294967295 134512640 134672761 3221224576 3221223760 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4757 603 41 0 5327 0
vsize: 21472
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 31929
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5557 0 0 0 33976 26 0 0 25 0 1 0 480067393 21987328 4757 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5368 4757 603 41 0 5327 0
vsize: 21472
[startup+350.013 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 31946
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5557 0 0 0 34976 26 0 0 25 0 1 0 480067393 21987328 4757 4294967295 134512640 134672761 3221224576 3221223616 134612975 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5368 4757 603 41 0 5327 0
vsize: 21472
[startup+360.013 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 31946
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5557 0 0 0 35976 26 0 0 25 0 1 0 480067393 21987328 4757 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5368 4757 603 41 0 5327 0
vsize: 21472
[startup+370.013 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 31946
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5557 0 0 0 36976 27 0 0 25 0 1 0 480067393 21987328 4757 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5368 4757 603 41 0 5327 0
vsize: 21472
[startup+380.014 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 31946
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5557 0 0 0 37976 27 0 0 25 0 1 0 480067393 21987328 4757 4294967295 134512640 134672761 3221224576 3221223712 134614696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4757 603 41 0 5327 0
vsize: 21472
[startup+390.014 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 31946
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5557 0 0 0 38976 27 0 0 25 0 1 0 480067393 21987328 4757 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4757 603 41 0 5327 0
vsize: 21472
[startup+400.015 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 31946
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5557 0 0 0 39976 27 0 0 25 0 1 0 480067393 21987328 4757 4294967295 134512640 134672761 3221224576 3221223760 134615505 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4757 603 41 0 5327 0
vsize: 21472
[startup+410.016 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 31948
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5557 0 0 0 40977 27 0 0 25 0 1 0 480067393 21987328 4757 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4757 603 41 0 5327 0
vsize: 21472
[startup+420.015 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 31948
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5557 0 0 0 41977 27 0 0 25 0 1 0 480067393 21987328 4757 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4757 603 41 0 5327 0
vsize: 21472
[startup+430.016 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 31948
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5558 0 0 0 42977 27 0 0 25 0 1 0 480067393 21987328 4758 4294967295 134512640 134672761 3221224576 3221223712 134614488 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4758 603 41 0 5327 0
vsize: 21472
[startup+440.016 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31948
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5558 0 0 0 43977 27 0 0 25 0 1 0 480067393 21987328 4758 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4758 603 41 0 5327 0
vsize: 21472
[startup+450.017 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31948
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5558 0 0 0 44977 27 0 0 25 0 1 0 480067393 21987328 4758 4294967295 134512640 134672761 3221224576 3221223672 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4758 603 41 0 5327 0
vsize: 21472
[startup+460.018 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31948
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5558 0 0 0 45978 27 0 0 25 0 1 0 480067393 21987328 4758 4294967295 134512640 134672761 3221224576 3221223744 134615859 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4758 603 41 0 5327 0
vsize: 21472
[startup+470.017 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 31948
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5558 0 0 0 46978 27 0 0 25 0 1 0 480067393 21987328 4758 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4758 603 41 0 5327 0
vsize: 21472
[startup+480.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31948
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5558 0 0 0 47978 27 0 0 25 0 1 0 480067393 21987328 4758 4294967295 134512640 134672761 3221224576 3221223712 134614753 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4758 603 41 0 5327 0
vsize: 21472
[startup+490.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31948
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5558 0 0 0 48978 27 0 0 25 0 1 0 480067393 21987328 4758 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4758 603 41 0 5327 0
vsize: 21472
[startup+500.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31948
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5558 0 0 0 49978 27 0 0 25 0 1 0 480067393 21987328 4758 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4758 603 41 0 5327 0
vsize: 21472
[startup+510.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31948
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5558 0 0 0 50979 27 0 0 25 0 1 0 480067393 21987328 4758 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4758 603 41 0 5327 0
vsize: 21472
[startup+520.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31948
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5558 0 0 0 51979 27 0 0 25 0 1 0 480067393 21987328 4758 4294967295 134512640 134672761 3221224576 3221223760 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4758 603 41 0 5327 0
vsize: 21472
[startup+530.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31948
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5559 0 0 0 52979 27 0 0 25 0 1 0 480067393 21987328 4759 4294967295 134512640 134672761 3221224576 3221223712 134614713 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4759 603 41 0 5327 0
vsize: 21472
[startup+540.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31948
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5559 0 0 0 53979 27 0 0 25 0 1 0 480067393 21987328 4759 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4759 603 41 0 5327 0
vsize: 21472
[startup+550.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31948
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5559 0 0 0 54979 27 0 0 25 0 1 0 480067393 21987328 4759 4294967295 134512640 134672761 3221224576 3221223712 134614739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4759 603 41 0 5327 0
vsize: 21472
[startup+560.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31948
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5559 0 0 0 55979 27 0 0 25 0 1 0 480067393 21987328 4759 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4759 603 41 0 5327 0
vsize: 21472
[startup+570.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31948
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5579 0 0 0 56979 27 0 0 25 0 1 0 480067393 22044672 4779 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5382 4779 603 41 0 5341 0
vsize: 21528
[startup+580.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31948
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5579 0 0 0 57980 27 0 0 25 0 1 0 480067393 22044672 4779 4294967295 134512640 134672761 3221224576 3221223760 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5382 4779 603 41 0 5341 0
vsize: 21528
[startup+590.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31948
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5579 0 0 0 58980 27 0 0 25 0 1 0 480067393 22044672 4779 4294967295 134512640 134672761 3221224576 3221223712 134614670 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5382 4779 603 41 0 5341 0
vsize: 21528
[startup+600.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31948
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5579 0 0 0 59980 27 0 0 25 0 1 0 480067393 22044672 4779 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5382 4779 603 41 0 5341 0
vsize: 21528
[startup+610.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31948
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5579 0 0 0 60980 27 0 0 25 0 1 0 480067393 22044672 4779 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5382 4779 603 41 0 5341 0
vsize: 21528
[startup+620.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31948
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5579 0 0 0 61980 27 0 0 25 0 1 0 480067393 22044672 4779 4294967295 134512640 134672761 3221224576 3221223712 134614825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5382 4779 603 41 0 5341 0
vsize: 21528
[startup+630.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31948
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5579 0 0 0 62981 27 0 0 25 0 1 0 480067393 22044672 4779 4294967295 134512640 134672761 3221224576 3221223616 134612832 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5382 4779 603 41 0 5341 0
vsize: 21528
[startup+640.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31948
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5579 0 0 0 63981 27 0 0 25 0 1 0 480067393 22044672 4779 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5382 4779 603 41 0 5341 0
vsize: 21528
[startup+650.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31948
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5579 0 0 0 64981 27 0 0 25 0 1 0 480067393 22044672 4779 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5382 4779 603 41 0 5341 0
vsize: 21528
[startup+660.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31948
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5582 0 0 0 65981 27 0 0 25 0 1 0 480067393 22044672 4782 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5382 4782 603 41 0 5341 0
vsize: 21528
[startup+670.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31948
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5582 0 0 0 66981 27 0 0 25 0 1 0 480067393 22044672 4782 4294967295 134512640 134672761 3221224576 3221223760 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5382 4782 603 41 0 5341 0
vsize: 21528
[startup+680.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5582 0 0 0 67981 27 0 0 25 0 1 0 480067393 22044672 4782 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5382 4782 603 41 0 5341 0
vsize: 21528
[startup+690.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5582 0 0 0 68982 27 0 0 25 0 1 0 480067393 22044672 4782 4294967295 134512640 134672761 3221224576 3221223760 134615526 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5382 4782 603 41 0 5341 0
vsize: 21528
[startup+700.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5582 0 0 0 69982 27 0 0 25 0 1 0 480067393 22044672 4782 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5382 4782 603 41 0 5341 0
vsize: 21528
[startup+710.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5582 0 0 0 70982 27 0 0 25 0 1 0 480067393 22044672 4782 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5382 4782 603 41 0 5341 0
vsize: 21528
[startup+720.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5582 0 0 0 71982 27 0 0 25 0 1 0 480067393 22044672 4782 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5382 4782 603 41 0 5341 0
vsize: 21528
[startup+730.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5582 0 0 0 72982 27 0 0 25 0 1 0 480067393 22044672 4782 4294967295 134512640 134672761 3221224576 3221223632 134644269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5382 4782 603 41 0 5341 0
vsize: 21528
[startup+740.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5582 0 0 0 73983 27 0 0 25 0 1 0 480067393 22044672 4782 4294967295 134512640 134672761 3221224576 3221223760 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5382 4782 603 41 0 5341 0
vsize: 21528
[startup+750.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5582 0 0 0 74983 27 0 0 25 0 1 0 480067393 22044672 4782 4294967295 134512640 134672761 3221224576 3221223760 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5382 4782 603 41 0 5341 0
vsize: 21528
[startup+760.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5683 0 0 0 75983 28 0 0 25 0 1 0 480067393 22450176 4882 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5481 4882 603 41 0 5440 0
vsize: 21924
[startup+770.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5696 0 0 0 76983 28 0 0 25 0 1 0 480067393 22499328 4894 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5493 4894 603 41 0 5452 0
vsize: 21972
[startup+780.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5697 0 0 0 77983 28 0 0 25 0 1 0 480067393 22499328 4895 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5493 4895 603 41 0 5452 0
vsize: 21972
[startup+790.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5800 0 0 0 78983 28 0 0 25 0 1 0 480067393 22913024 4997 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5594 4997 603 41 0 5553 0
vsize: 22376
[startup+800.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5849 0 0 0 79983 28 0 0 25 0 1 0 480067393 23105536 5045 4294967295 134512640 134672761 3221224576 3221223760 134615785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5641 5045 603 41 0 5600 0
vsize: 22564
[startup+810.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5849 0 0 0 80983 28 0 0 25 0 1 0 480067393 23105536 5045 4294967295 134512640 134672761 3221224576 3221223616 134614333 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5641 5045 603 41 0 5600 0
vsize: 22564
[startup+820.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5865 0 0 0 81983 28 0 0 25 0 1 0 480067393 23171072 5060 4294967295 134512640 134672761 3221224576 3221223760 134615848 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5657 5060 603 41 0 5616 0
vsize: 22628
[startup+830.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5877 0 0 0 82983 28 0 0 25 0 1 0 480067393 23203840 5071 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5665 5071 603 41 0 5624 0
vsize: 22660
[startup+840.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5877 0 0 0 83983 28 0 0 25 0 1 0 480067393 23203840 5071 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5665 5071 603 41 0 5624 0
vsize: 22660
[startup+850.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5877 0 0 0 84984 28 0 0 25 0 1 0 480067393 23203840 5071 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5665 5071 603 41 0 5624 0
vsize: 22660
[startup+860.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 5975 0 0 0 85984 28 0 0 25 0 1 0 480067393 23601152 5169 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5762 5169 603 41 0 5721 0
vsize: 23048
[startup+870.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6007 0 0 0 86984 29 0 0 25 0 1 0 480067393 23732224 5201 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5794 5201 603 41 0 5753 0
vsize: 23176
[startup+880.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6007 0 0 0 87985 29 0 0 25 0 1 0 480067393 23732224 5201 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5794 5201 603 41 0 5753 0
vsize: 23176
[startup+890.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6120 0 0 0 88985 29 0 0 25 0 1 0 480067393 24195072 5313 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5907 5313 603 41 0 5866 0
vsize: 23628
[startup+900.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6128 0 0 0 89985 29 0 0 25 0 1 0 480067393 24195072 5321 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5907 5321 603 41 0 5866 0
vsize: 23628
[startup+910.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6389 0 0 0 90984 30 0 0 25 0 1 0 480067393 25313280 5581 4294967295 134512640 134672761 3221224576 3221223776 134610618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6180 5581 603 41 0 6139 0
vsize: 24720
[startup+920.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6389 0 0 0 91984 30 0 0 25 0 1 0 480067393 25313280 5581 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6180 5581 603 41 0 6139 0
vsize: 24720
[startup+930.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6400 0 0 0 92984 30 0 0 25 0 1 0 480067393 25346048 5591 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6188 5591 603 41 0 6147 0
vsize: 24752
[startup+940.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6400 0 0 0 93985 30 0 0 25 0 1 0 480067393 25346048 5591 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6188 5591 603 41 0 6147 0
vsize: 24752
[startup+950.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6408 0 0 0 94985 30 0 0 25 0 1 0 480067393 25378816 5598 4294967295 134512640 134672761 3221224576 3221223748 134615856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5598 603 41 0 6155 0
vsize: 24784
[startup+960.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6408 0 0 0 95985 30 0 0 25 0 1 0 480067393 25378816 5598 4294967295 134512640 134672761 3221224576 3221223760 134615752 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5598 603 41 0 6155 0
vsize: 24784
[startup+970.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6408 0 0 0 96985 30 0 0 25 0 1 0 480067393 25378816 5598 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5598 603 41 0 6155 0
vsize: 24784
[startup+980.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6408 0 0 0 97986 30 0 0 25 0 1 0 480067393 25378816 5598 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5598 603 41 0 6155 0
vsize: 24784
[startup+990.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6408 0 0 0 98986 30 0 0 25 0 1 0 480067393 25378816 5598 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5598 603 41 0 6155 0
vsize: 24784
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6408 0 0 0 99986 30 0 0 25 0 1 0 480067393 25378816 5598 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5598 603 41 0 6155 0
vsize: 24784
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6408 0 0 0 100986 30 0 0 25 0 1 0 480067393 25378816 5598 4294967295 134512640 134672761 3221224576 3221223776 134610709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5598 603 41 0 6155 0
vsize: 24784
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6408 0 0 0 101986 30 0 0 25 0 1 0 480067393 25378816 5598 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5598 603 41 0 6155 0
vsize: 24784
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6408 0 0 0 102987 30 0 0 25 0 1 0 480067393 25378816 5598 4294967295 134512640 134672761 3221224576 3221223712 134614576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5598 603 41 0 6155 0
vsize: 24784
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6408 0 0 0 103987 30 0 0 25 0 1 0 480067393 25378816 5598 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5598 603 41 0 6155 0
vsize: 24784
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6408 0 0 0 104987 30 0 0 25 0 1 0 480067393 25378816 5598 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5598 603 41 0 6155 0
vsize: 24784
[startup+1060.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6408 0 0 0 105987 30 0 0 25 0 1 0 480067393 25378816 5598 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5598 603 41 0 6155 0
vsize: 24784
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6408 0 0 0 106987 30 0 0 25 0 1 0 480067393 25378816 5598 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5598 603 41 0 6155 0
vsize: 24784
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6408 0 0 0 107988 30 0 0 25 0 1 0 480067393 25378816 5598 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5598 603 41 0 6155 0
vsize: 24784
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6408 0 0 0 108988 30 0 0 25 0 1 0 480067393 25378816 5598 4294967295 134512640 134672761 3221224576 3221223840 134618348 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5598 603 41 0 6155 0
vsize: 24784
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6408 0 0 0 109988 30 0 0 25 0 1 0 480067393 25378816 5598 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5598 603 41 0 6155 0
vsize: 24784
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6408 0 0 0 110988 30 0 0 25 0 1 0 480067393 25378816 5598 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5598 603 41 0 6155 0
vsize: 24784
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6408 0 0 0 111988 30 0 0 25 0 1 0 480067393 25378816 5598 4294967295 134512640 134672761 3221224576 3221223760 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5598 603 41 0 6155 0
vsize: 24784
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6408 0 0 0 112989 30 0 0 25 0 1 0 480067393 25378816 5598 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5598 603 41 0 6155 0
vsize: 24784
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6408 0 0 0 113989 30 0 0 25 0 1 0 480067393 25378816 5598 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5598 603 41 0 6155 0
vsize: 24784
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6408 0 0 0 114989 30 0 0 25 0 1 0 480067393 25378816 5598 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5598 603 41 0 6155 0
vsize: 24784
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6408 0 0 0 115989 30 0 0 25 0 1 0 480067393 25378816 5598 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5598 603 41 0 6155 0
vsize: 24784
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6408 0 0 0 116989 30 0 0 25 0 1 0 480067393 25378816 5598 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5598 603 41 0 6155 0
vsize: 24784
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6408 0 0 0 117989 30 0 0 25 0 1 0 480067393 25378816 5598 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5598 603 41 0 6155 0
vsize: 24784
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6408 0 0 0 118990 30 0 0 25 0 1 0 480067393 25378816 5598 4294967295 134512640 134672761 3221224576 3221223760 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5598 603 41 0 6155 0
vsize: 24784
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 31950
Raw data (stat): 31893 (minisat+) R 31892 27565 27564 0 -1 0 6408 0 0 0 119990 30 0 0 25 0 1 0 480067393 25378816 5598 4294967295 134512640 134672761 3221224576 3221223760 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6196 5598 603 41 0 6155 0
vsize: 24784
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 31950
Raw data (stat): 31893 (minisat+) Z 31892 27565 27564 0 -1 12 6409 0 0 0 119990 32 0 0 25 0 1 0 480067393 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.06
CPU time (s): 1200.23
CPU user time (s): 1199.9
CPU system time (s): 0.320951
CPU usage (%): 100.014
Max. virtual memory (Kb): 24784
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####