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/primes-dimacs-cnf/normalized-f2000.opb
MD5SUM	4675a5d50c7e04c9a0597ae768da1a88
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	4000
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	4000
Number of bits of the sum of numbers in the objective function	12
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	4000
Number of bits of the biggest sum of numbers	12
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	4000
Total number of constraints	10500
Number of constraints which are clauses	10500
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	2
Maximum length of a constraint	3
Trace number 5433

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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:        851484 kB
Buffers:         40436 kB
Cached:         118412 kB
SwapCached:          0 kB
Active:         107252 kB
Inactive:        54740 kB
HighTotal:      131008 kB
HighFree:        19880 kB
LowTotal:       903652 kB
LowFree:        831604 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7200 kB
Slab:            15524 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:17:13 (client local time) WITH STATUS 0 IN 1200.2 SECONDS
stats: 3888 7 1200.2 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 10500 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 |   10500    29500 |    3149       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3995          
c   -- var.elim.:  2000/3995          
c   -- var.elim.:  3000/3995          
c   -- var.elim.:  3995/3995          
c |         0 |   10500    29500 |    4200       0        0     nan |  0.000 % |
c |       100 |   10500    29500 |    4620     100     6154    61.5 |  0.000 % |
c |       251 |   10500    29500 |    5082     251    15653    62.4 |  0.000 % |
c |       476 |   10500    29500 |    5590     476    31579    66.3 |  0.000 % |
c |       813 |   10500    29500 |    6149     813    63241    77.8 |  0.000 % |
c |      1319 |   10500    29500 |    6764    1319   107756    81.7 |  0.000 % |
c |      2078 |   10500    29500 |    7440    2078   177188    85.3 |  0.000 % |
c |      3221 |   10500    29500 |    8184    3221   286782    89.0 |  0.000 % |
c |      4930 |   10500    29500 |    9003    4930   431577    87.5 |  0.000 % |
c |      7494 |   10500    29500 |    9903    7494   685418    91.5 |  0.000 % |
c |     11339 |   10500    29500 |   10893    7885   788222   100.0 |  0.000 % |
c |     17106 |   10500    29500 |   11983    9897  1017700   102.8 |  0.000 % |
c |     25755 |   1050#### 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.47 0.76 0.84 2/56 18452
Raw data (stat): 18452 (runsolver) D 18451 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 365008661 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 3225161850 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.55 0.77 0.84 2/56 18452
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 2067 0 0 0 993 5 0 0 25 0 1 0 365008661 10100736 2045 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2466 2045 603 41 0 2425 0
vsize: 9864
[startup+20.0006 s]
Raw data (loadavg): 0.62 0.78 0.84 2/56 18452
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 2372 0 0 0 1993 6 0 0 25 0 1 0 365008661 11280384 2350 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2754 2350 603 41 0 2713 0
vsize: 11016
[startup+30.0009 s]
Raw data (loadavg): 0.68 0.78 0.84 2/56 18452
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 2464 0 0 0 2992 6 0 0 25 0 1 0 365008661 11657216 2442 4294967295 134512640 134672761 3221224576 3221223760 134616011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2846 2442 603 41 0 2805 0
vsize: 11384
[startup+40.0007 s]
Raw data (loadavg): 0.73 0.79 0.84 2/56 18452
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 2710 0 0 0 3992 7 0 0 25 0 1 0 365008661 12668928 2688 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3093 2688 603 41 0 3052 0
vsize: 12372
[startup+50.0015 s]
Raw data (loadavg): 0.77 0.80 0.84 2/56 18452
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 2710 0 0 0 4992 7 0 0 25 0 1 0 365008661 12668928 2688 4294967295 134512640 134672761 3221224576 3221223616 134613754 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3093 2688 603 41 0 3052 0
vsize: 12372
[startup+60.0012 s]
Raw data (loadavg): 0.80 0.80 0.84 2/56 18452
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 2904 0 0 0 5991 8 0 0 25 0 1 0 365008661 13398016 2882 4294967295 134512640 134672761 3221224576 3221223672 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3271 2882 603 41 0 3230 0
vsize: 13084
[startup+70.0011 s]
Raw data (loadavg): 0.83 0.81 0.84 2/56 18452
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 2998 0 0 0 6991 8 0 0 25 0 1 0 365008661 13803520 2976 4294967295 134512640 134672761 3221224576 3221223760 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3370 2976 603 41 0 3329 0
vsize: 13480
[startup+80.0023 s]
Raw data (loadavg): 0.86 0.81 0.84 2/56 18452
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 3206 0 0 0 7991 8 0 0 25 0 1 0 365008661 14741504 3184 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3599 3184 603 41 0 3558 0
vsize: 14396
[startup+90.0017 s]
Raw data (loadavg): 0.88 0.82 0.84 2/56 18452
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 3206 0 0 0 8991 9 0 0 25 0 1 0 365008661 14741504 3184 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3599 3184 603 41 0 3558 0
vsize: 14396
[startup+100.002 s]
Raw data (loadavg): 0.90 0.83 0.85 2/56 18452
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 3217 0 0 0 9991 9 0 0 25 0 1 0 365008661 14741504 3195 4294967295 134512640 134672761 3221224576 3221223760 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3599 3195 603 41 0 3558 0
vsize: 14396
[startup+110.003 s]
Raw data (loadavg): 0.91 0.83 0.85 2/56 18452
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 3290 0 0 0 10990 9 0 0 25 0 1 0 365008661 15085568 3268 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3683 3268 603 41 0 3642 0
vsize: 14732
[startup+120.003 s]
Raw data (loadavg): 0.93 0.84 0.85 2/56 18452
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 3341 0 0 0 11990 10 0 0 25 0 1 0 365008661 15294464 3319 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3734 3319 603 41 0 3693 0
vsize: 14936
[startup+130.003 s]
Raw data (loadavg): 0.94 0.84 0.85 2/56 18452
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 3487 0 0 0 12989 11 0 0 25 0 1 0 365008661 15953920 3465 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3895 3465 603 41 0 3854 0
vsize: 15580
[startup+140.003 s]
Raw data (loadavg): 0.95 0.85 0.85 2/56 18452
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 3573 0 0 0 13989 11 0 0 25 0 1 0 365008661 16224256 3550 4294967295 134512640 134672761 3221224576 3221223760 134616006 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3961 3550 603 41 0 3920 0
vsize: 15844
[startup+150.004 s]
Raw data (loadavg): 0.95 0.85 0.85 2/56 18452
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 3574 0 0 0 14989 11 0 0 25 0 1 0 365008661 16224256 3551 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3961 3551 603 41 0 3920 0
vsize: 15844
[startup+160.004 s]
Raw data (loadavg): 0.96 0.85 0.85 2/56 18452
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 3574 0 0 0 15989 11 0 0 25 0 1 0 365008661 16224256 3551 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3961 3551 603 41 0 3920 0
vsize: 15844
[startup+170.004 s]
Raw data (loadavg): 0.97 0.86 0.85 2/56 18452
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 3574 0 0 0 16989 11 0 0 25 0 1 0 365008661 16224256 3551 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3961 3551 603 41 0 3920 0
vsize: 15844
[startup+180.004 s]
Raw data (loadavg): 1.04 0.88 0.86 2/56 18505
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 3630 0 0 0 17989 12 0 0 25 0 1 0 365008661 16449536 3607 4294967295 134512640 134672761 3221224576 3221223760 134615689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4016 3607 603 41 0 3975 0
vsize: 16064
[startup+190.003 s]
Raw data (loadavg): 1.04 0.88 0.86 2/56 18505
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 3639 0 0 0 18989 12 0 0 25 0 1 0 365008661 16482304 3615 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4024 3615 603 41 0 3983 0
vsize: 16096
[startup+200.003 s]
Raw data (loadavg): 1.03 0.89 0.86 2/56 18505
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 3639 0 0 0 19989 12 0 0 25 0 1 0 365008661 16482304 3615 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4024 3615 603 41 0 3983 0
vsize: 16096
[startup+210.003 s]
Raw data (loadavg): 1.03 0.89 0.86 2/56 18505
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 3643 0 0 0 20989 12 0 0 25 0 1 0 365008661 16482304 3619 4294967295 134512640 134672761 3221224576 3221223568 134565066 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4024 3619 603 41 0 3983 0
vsize: 16096
[startup+220.003 s]
Raw data (loadavg): 1.02 0.89 0.86 2/56 18505
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 3653 0 0 0 21989 12 0 0 25 0 1 0 365008661 16678912 3629 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4072 3629 603 41 0 4031 0
vsize: 16288
[startup+230.003 s]
Raw data (loadavg): 1.10 0.91 0.87 2/56 18507
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 3695 0 0 0 22990 12 0 0 25 0 1 0 365008661 16719872 3670 4294967295 134512640 134672761 3221224576 3221223760 134615635 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4082 3670 603 41 0 4041 0
vsize: 16328
[startup+240.002 s]
Raw data (loadavg): 1.08 0.91 0.87 2/56 18509
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 3695 0 0 0 23990 12 0 0 25 0 1 0 365008661 16719872 3670 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4082 3670 603 41 0 4041 0
vsize: 16328
[startup+250.003 s]
Raw data (loadavg): 1.07 0.92 0.87 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 3783 0 0 0 24990 12 0 0 25 0 1 0 365008661 17080320 3758 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4170 3758 603 41 0 4129 0
vsize: 16680
[startup+260.004 s]
Raw data (loadavg): 1.06 0.92 0.87 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 3917 0 0 0 25989 12 0 0 25 0 1 0 365008661 17629184 3891 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4304 3891 603 41 0 4263 0
vsize: 17216
[startup+270.004 s]
Raw data (loadavg): 1.05 0.92 0.87 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 3917 0 0 0 26989 12 0 0 25 0 1 0 365008661 17629184 3891 4294967295 134512640 134672761 3221224576 3221223760 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4304 3891 603 41 0 4263 0
vsize: 17216
[startup+280.003 s]
Raw data (loadavg): 1.04 0.92 0.87 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 3917 0 0 0 27990 12 0 0 25 0 1 0 365008661 17629184 3891 4294967295 134512640 134672761 3221224576 3221223760 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4304 3891 603 41 0 4263 0
vsize: 17216
[startup+290.003 s]
Raw data (loadavg): 1.03 0.92 0.87 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 3917 0 0 0 28990 12 0 0 25 0 1 0 365008661 17625088 3890 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4303 3890 603 41 0 4262 0
vsize: 17212
[startup+300.003 s]
Raw data (loadavg): 1.03 0.93 0.88 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 3961 0 0 0 29990 13 0 0 25 0 1 0 365008661 17801216 3933 4294967295 134512640 134672761 3221224576 3221223616 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4346 3933 603 41 0 4305 0
vsize: 17384
[startup+310.003 s]
Raw data (loadavg): 1.02 0.93 0.88 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 3961 0 0 0 30990 13 0 0 25 0 1 0 365008661 17801216 3933 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4346 3933 603 41 0 4305 0
vsize: 17384
[startup+320.003 s]
Raw data (loadavg): 1.02 0.93 0.88 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4144 0 0 0 31989 13 0 0 25 0 1 0 365008661 18530304 4115 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4524 4115 603 41 0 4483 0
vsize: 18096
[startup+330.003 s]
Raw data (loadavg): 1.02 0.93 0.88 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4146 0 0 0 32990 13 0 0 25 0 1 0 365008661 18530304 4117 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4524 4117 603 41 0 4483 0
vsize: 18096
[startup+340.003 s]
Raw data (loadavg): 1.01 0.93 0.88 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4146 0 0 0 33990 13 0 0 25 0 1 0 365008661 18530304 4117 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4524 4117 603 41 0 4483 0
vsize: 18096
[startup+350.003 s]
Raw data (loadavg): 1.01 0.94 0.88 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4225 0 0 0 34990 13 0 0 25 0 1 0 365008661 18849792 4195 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4602 4195 603 41 0 4561 0
vsize: 18408
[startup+360.003 s]
Raw data (loadavg): 1.01 0.94 0.88 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4225 0 0 0 35990 13 0 0 25 0 1 0 365008661 18849792 4195 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4602 4195 603 41 0 4561 0
vsize: 18408
[startup+370.003 s]
Raw data (loadavg): 1.01 0.94 0.88 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4311 0 0 0 36990 14 0 0 25 0 1 0 365008661 19197952 4281 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4687 4281 603 41 0 4646 0
vsize: 18748
[startup+380.003 s]
Raw data (loadavg): 1.00 0.94 0.88 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4311 0 0 0 37990 14 0 0 25 0 1 0 365008661 19197952 4281 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4687 4281 603 41 0 4646 0
vsize: 18748
[startup+390.002 s]
Raw data (loadavg): 1.00 0.94 0.88 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4607 0 0 0 38989 15 0 0 25 0 1 0 365008661 20414464 4576 4294967295 134512640 134672761 3221224576 3221223760 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4984 4576 603 41 0 4943 0
vsize: 19936
[startup+400.003 s]
Raw data (loadavg): 1.00 0.94 0.89 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4607 0 0 0 39989 15 0 0 25 0 1 0 365008661 20414464 4576 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4984 4576 603 41 0 4943 0
vsize: 19936
[startup+410.003 s]
Raw data (loadavg): 1.00 0.94 0.89 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4679 0 0 0 40989 15 0 0 25 0 1 0 365008661 20717568 4647 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5058 4647 603 41 0 5017 0
vsize: 20232
[startup+420.002 s]
Raw data (loadavg): 1.00 0.95 0.89 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4679 0 0 0 41989 15 0 0 25 0 1 0 365008661 20717568 4647 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5058 4647 603 41 0 5017 0
vsize: 20232
[startup+430.003 s]
Raw data (loadavg): 1.00 0.95 0.89 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4679 0 0 0 42989 15 0 0 25 0 1 0 365008661 20717568 4647 4294967295 134512640 134672761 3221224576 3221223728 134614555 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5058 4647 603 41 0 5017 0
vsize: 20232
[startup+440.003 s]
Raw data (loadavg): 1.00 0.95 0.89 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4679 0 0 0 43990 15 0 0 25 0 1 0 365008661 20717568 4647 4294967295 134512640 134672761 3221224576 3221223760 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5058 4647 603 41 0 5017 0
vsize: 20232
[startup+450.004 s]
Raw data (loadavg): 1.00 0.95 0.89 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4679 0 0 0 44990 15 0 0 25 0 1 0 365008661 20709376 4646 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5056 4646 603 41 0 5015 0
vsize: 20224
[startup+460.004 s]
Raw data (loadavg): 1.00 0.95 0.89 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4679 0 0 0 45990 15 0 0 25 0 1 0 365008661 20709376 4646 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5056 4646 603 41 0 5015 0
vsize: 20224
[startup+470.003 s]
Raw data (loadavg): 1.00 0.95 0.89 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4680 0 0 0 46990 15 0 0 25 0 1 0 365008661 20709376 4647 4294967295 134512640 134672761 3221224576 3221223760 134616014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5056 4647 603 41 0 5015 0
vsize: 20224
[startup+480.003 s]
Raw data (loadavg): 1.00 0.95 0.89 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4680 0 0 0 47990 15 0 0 25 0 1 0 365008661 20709376 4647 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5056 4647 603 41 0 5015 0
vsize: 20224
[startup+490.003 s]
Raw data (loadavg): 1.00 0.95 0.89 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4680 0 0 0 48990 15 0 0 25 0 1 0 365008661 20709376 4647 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5056 4647 603 41 0 5015 0
vsize: 20224
[startup+500.004 s]
Raw data (loadavg): 1.00 0.95 0.90 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4680 0 0 0 49991 15 0 0 25 0 1 0 365008661 20709376 4647 4294967295 134512640 134672761 3221224576 3221223616 134614348 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5056 4647 603 41 0 5015 0
vsize: 20224
[startup+510.004 s]
Raw data (loadavg): 1.00 0.95 0.90 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4680 0 0 0 50991 15 0 0 25 0 1 0 365008661 20709376 4647 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5056 4647 603 41 0 5015 0
vsize: 20224
[startup+520.003 s]
Raw data (loadavg): 1.00 0.95 0.90 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4683 0 0 0 51991 15 0 0 25 0 1 0 365008661 20709376 4650 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5056 4650 603 41 0 5015 0
vsize: 20224
[startup+530.003 s]
Raw data (loadavg): 1.00 0.96 0.90 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4683 0 0 0 52991 15 0 0 25 0 1 0 365008661 20709376 4650 4294967295 134512640 134672761 3221224576 3221223616 134612975 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5056 4650 603 41 0 5015 0
vsize: 20224
[startup+540.003 s]
Raw data (loadavg): 1.00 0.96 0.90 2/56 18511
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4683 0 0 0 53991 15 0 0 25 0 1 0 365008661 20705280 4649 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5055 4649 603 41 0 5014 0
vsize: 20220
[startup+550.003 s]
Raw data (loadavg): 1.00 0.96 0.90 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4683 0 0 0 54991 15 0 0 25 0 1 0 365008661 20705280 4649 4294967295 134512640 134672761 3221224576 3221223760 134615926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5055 4649 603 41 0 5014 0
vsize: 20220
[startup+560.003 s]
Raw data (loadavg): 1.00 0.96 0.90 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4706 0 0 0 55992 15 0 0 25 0 1 0 365008661 20795392 4672 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5077 4672 603 41 0 5036 0
vsize: 20308
[startup+570.002 s]
Raw data (loadavg): 1.00 0.96 0.90 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4706 0 0 0 56992 15 0 0 25 0 1 0 365008661 20795392 4672 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5077 4672 603 41 0 5036 0
vsize: 20308
[startup+580.002 s]
Raw data (loadavg): 1.00 0.96 0.90 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4798 0 0 0 57992 15 0 0 25 0 1 0 365008661 21192704 4764 4294967295 134512640 134672761 3221224576 3221223760 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5174 4764 603 41 0 5133 0
vsize: 20696
[startup+590.002 s]
Raw data (loadavg): 1.00 0.96 0.90 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4878 0 0 0 58991 16 0 0 25 0 1 0 365008661 21499904 4843 4294967295 134512640 134672761 3221224576 3221223512 1075350763 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5249 4843 603 41 0 5208 0
vsize: 20996
[startup+600.002 s]
Raw data (loadavg): 1.00 0.96 0.91 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4878 0 0 0 59992 16 0 0 25 0 1 0 365008661 21499904 4843 4294967295 134512640 134672761 3221224576 3221223760 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5249 4843 603 41 0 5208 0
vsize: 20996
[startup+610.001 s]
Raw data (loadavg): 1.00 0.96 0.91 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4878 0 0 0 60992 16 0 0 25 0 1 0 365008661 21495808 4842 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5248 4842 603 41 0 5207 0
vsize: 20992
[startup+620.002 s]
Raw data (loadavg): 1.00 0.96 0.91 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4878 0 0 0 61992 16 0 0 25 0 1 0 365008661 21495808 4842 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5248 4842 603 41 0 5207 0
vsize: 20992
[startup+630.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4879 0 0 0 62992 16 0 0 25 0 1 0 365008661 21495808 4843 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5248 4843 603 41 0 5207 0
vsize: 20992
[startup+640.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4879 0 0 0 63992 16 0 0 25 0 1 0 365008661 21495808 4843 4294967295 134512640 134672761 3221224576 3221223760 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5248 4843 603 41 0 5207 0
vsize: 20992
[startup+650.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4879 0 0 0 64992 16 0 0 25 0 1 0 365008661 21487616 4842 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5246 4842 603 41 0 5205 0
vsize: 20984
[startup+660.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4879 0 0 0 65993 16 0 0 25 0 1 0 365008661 21487616 4842 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5246 4842 603 41 0 5205 0
vsize: 20984
[startup+670.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 4965 0 0 0 66993 16 0 0 25 0 1 0 365008661 21880832 4928 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5342 4928 603 41 0 5301 0
vsize: 21368
[startup+680.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5152 0 0 0 67992 16 0 0 25 0 1 0 365008661 22609920 5114 4294967295 134512640 134672761 3221224576 3221223760 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5520 5114 603 41 0 5479 0
vsize: 22080
[startup+690.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5152 0 0 0 68992 16 0 0 25 0 1 0 365008661 22609920 5114 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5520 5114 603 41 0 5479 0
vsize: 22080
[startup+700.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5152 0 0 0 69992 17 0 0 25 0 1 0 365008661 22597632 5113 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5517 5113 603 41 0 5476 0
vsize: 22068
[startup+710.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5152 0 0 0 70993 17 0 0 25 0 1 0 365008661 22597632 5113 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5517 5113 603 41 0 5476 0
vsize: 22068
[startup+720.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5153 0 0 0 71993 17 0 0 25 0 1 0 365008661 22597632 5114 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5517 5114 603 41 0 5476 0
vsize: 22068
[startup+730.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5153 0 0 0 72993 17 0 0 25 0 1 0 365008661 22597632 5114 4294967295 134512640 134672761 3221224576 3221223760 134615689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5517 5114 603 41 0 5476 0
vsize: 22068
[startup+740.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5153 0 0 0 73993 17 0 0 25 0 1 0 365008661 22593536 5113 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5516 5113 603 41 0 5475 0
vsize: 22064
[startup+750.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5153 0 0 0 74993 17 0 0 25 0 1 0 365008661 22593536 5113 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5516 5113 603 41 0 5475 0
vsize: 22064
[startup+760.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5154 0 0 0 75993 17 0 0 25 0 1 0 365008661 22593536 5114 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5516 5114 603 41 0 5475 0
vsize: 22064
[startup+770.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5154 0 0 0 76993 17 0 0 25 0 1 0 365008661 22593536 5114 4294967295 134512640 134672761 3221224576 3221223760 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5516 5114 603 41 0 5475 0
vsize: 22064
[startup+780.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5154 0 0 0 77994 17 0 0 25 0 1 0 365008661 22593536 5114 4294967295 134512640 134672761 3221224576 3221223952 134620485 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5516 5114 603 41 0 5475 0
vsize: 22064
[startup+790.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5158 0 0 0 78994 17 0 0 25 0 1 0 365008661 22593536 5118 4294967295 134512640 134672761 3221224576 3221223760 134615638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5516 5118 603 41 0 5475 0
vsize: 22064
[startup+800.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5158 0 0 0 79994 17 0 0 25 0 1 0 365008661 22593536 5118 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5516 5118 603 41 0 5475 0
vsize: 22064
[startup+810.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5158 0 0 0 80994 17 0 0 25 0 1 0 365008661 22593536 5118 4294967295 134512640 134672761 3221224576 3221223712 134614724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5516 5118 603 41 0 5475 0
vsize: 22064
[startup+820.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5158 0 0 0 81994 17 0 0 25 0 1 0 365008661 22593536 5118 4294967295 134512640 134672761 3221224576 3221223816 134614477 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5516 5118 603 41 0 5475 0
vsize: 22064
[startup+830.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5158 0 0 0 82994 17 0 0 25 0 1 0 365008661 22593536 5118 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5516 5118 603 41 0 5475 0
vsize: 22064
[startup+840.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18513
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5302 0 0 0 83994 17 0 0 25 0 1 0 365008661 23195648 5261 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5663 5261 603 41 0 5622 0
vsize: 22652
[startup+850.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5302 0 0 0 84994 17 0 0 25 0 1 0 365008661 23195648 5261 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5663 5261 603 41 0 5622 0
vsize: 22652
[startup+860.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5302 0 0 0 85995 17 0 0 25 0 1 0 365008661 23195648 5261 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5663 5261 603 41 0 5622 0
vsize: 22652
[startup+870.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5302 0 0 0 86995 17 0 0 25 0 1 0 365008661 23191552 5260 4294967295 134512640 134672761 3221224576 3221223712 134614688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5662 5260 603 41 0 5621 0
vsize: 22648
[startup+880.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5302 0 0 0 87995 17 0 0 25 0 1 0 365008661 23191552 5260 4294967295 134512640 134672761 3221224576 3221223760 134615551 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5662 5260 603 41 0 5621 0
vsize: 22648
[startup+890.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5520 0 0 0 88995 18 0 0 25 0 1 0 365008661 24088576 5478 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5881 5478 603 41 0 5840 0
vsize: 23524
[startup+900.001 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5520 0 0 0 89995 18 0 0 25 0 1 0 365008661 24088576 5478 4294967295 134512640 134672761 3221224576 3221223760 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5881 5478 603 41 0 5840 0
vsize: 23524
[startup+910.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5520 0 0 0 90995 18 0 0 25 0 1 0 365008661 24088576 5478 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5881 5478 603 41 0 5840 0
vsize: 23524
[startup+920.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5541 0 0 0 91995 18 0 0 25 0 1 0 365008661 24170496 5499 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5499 603 41 0 5860 0
vsize: 23604
[startup+930.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5541 0 0 0 92995 18 0 0 25 0 1 0 365008661 24170496 5499 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5499 603 41 0 5860 0
vsize: 23604
[startup+940.002 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5541 0 0 0 93996 18 0 0 25 0 1 0 365008661 24170496 5499 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5499 603 41 0 5860 0
vsize: 23604
[startup+950.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5541 0 0 0 94996 18 0 0 25 0 1 0 365008661 24170496 5499 4294967295 134512640 134672761 3221224576 3221223700 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5499 603 41 0 5860 0
vsize: 23604
[startup+960.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5541 0 0 0 95996 18 0 0 25 0 1 0 365008661 24170496 5499 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5901 5499 603 41 0 5860 0
vsize: 23604
[startup+970.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5541 0 0 0 96996 18 0 0 25 0 1 0 365008661 24158208 5498 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5898 5498 603 41 0 5857 0
vsize: 23592
[startup+980.004 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5541 0 0 0 97996 18 0 0 25 0 1 0 365008661 24158208 5498 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5898 5498 603 41 0 5857 0
vsize: 23592
[startup+990.003 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5542 0 0 0 98996 18 0 0 25 0 1 0 365008661 24154112 5498 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5897 5498 603 41 0 5856 0
vsize: 23588
[startup+1000 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5542 0 0 0 99997 18 0 0 25 0 1 0 365008661 24154112 5498 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5897 5498 603 41 0 5856 0
vsize: 23588
[startup+1010 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5542 0 0 0 100997 18 0 0 25 0 1 0 365008661 24154112 5498 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5897 5498 603 41 0 5856 0
vsize: 23588
[startup+1020 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5543 0 0 0 101997 18 0 0 25 0 1 0 365008661 24154112 5499 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5897 5499 603 41 0 5856 0
vsize: 23588
[startup+1030 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5543 0 0 0 102997 18 0 0 25 0 1 0 365008661 24154112 5499 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5897 5499 603 41 0 5856 0
vsize: 23588
[startup+1040 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5543 0 0 0 103997 18 0 0 25 0 1 0 365008661 24154112 5499 4294967295 134512640 134672761 3221224576 3221223760 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5897 5499 603 41 0 5856 0
vsize: 23588
[startup+1050 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5681 0 0 0 104997 18 0 0 25 0 1 0 365008661 24735744 5636 4294967295 134512640 134672761 3221224576 3221223760 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6039 5636 603 41 0 5998 0
vsize: 24156
[startup+1060 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5681 0 0 0 105997 18 0 0 25 0 1 0 365008661 24735744 5636 4294967295 134512640 134672761 3221224576 3221223840 134618445 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6039 5636 603 41 0 5998 0
vsize: 24156
[startup+1070 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5681 0 0 0 106998 18 0 0 25 0 1 0 365008661 24735744 5636 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6039 5636 603 41 0 5998 0
vsize: 24156
[startup+1080 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5879 0 0 0 107997 18 0 0 25 0 1 0 365008661 25538560 5833 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6235 5833 603 41 0 6194 0
vsize: 24940
[startup+1090 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5879 0 0 0 108997 18 0 0 25 0 1 0 365008661 25538560 5833 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6235 5833 603 41 0 6194 0
vsize: 24940
[startup+1100 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5879 0 0 0 109997 18 0 0 25 0 1 0 365008661 25538560 5833 4294967295 134512640 134672761 3221224576 3221223712 134614560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6235 5833 603 41 0 6194 0
vsize: 24940
[startup+1110 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5896 0 0 0 110997 18 0 0 25 0 1 0 365008661 25604096 5849 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6251 5849 603 41 0 6210 0
vsize: 25004
[startup+1120 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5896 0 0 0 111998 18 0 0 25 0 1 0 365008661 25604096 5849 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6251 5849 603 41 0 6210 0
vsize: 25004
[startup+1130 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5896 0 0 0 112998 18 0 0 25 0 1 0 365008661 25604096 5849 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6251 5849 603 41 0 6210 0
vsize: 25004
[startup+1140 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18515
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5896 0 0 0 113998 18 0 0 25 0 1 0 365008661 25604096 5849 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6251 5849 603 41 0 6210 0
vsize: 25004
[startup+1150 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18517
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5896 0 0 0 114998 18 0 0 25 0 1 0 365008661 25604096 5849 4294967295 134512640 134672761 3221224576 3221223760 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6251 5849 603 41 0 6210 0
vsize: 25004
[startup+1160 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18517
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5896 0 0 0 115998 18 0 0 25 0 1 0 365008661 25604096 5849 4294967295 134512640 134672761 3221224576 3221223760 134615643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6251 5849 603 41 0 6210 0
vsize: 25004
[startup+1170 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18517
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5896 0 0 0 116998 18 0 0 25 0 1 0 365008661 25604096 5849 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6251 5849 603 41 0 6210 0
vsize: 25004
[startup+1180 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18517
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5896 0 0 0 117999 18 0 0 25 0 1 0 365008661 25604096 5849 4294967295 134512640 134672761 3221224576 3221223712 134614518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6251 5849 603 41 0 6210 0
vsize: 25004
[startup+1190 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18517
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5937 0 0 0 118999 19 0 0 25 0 1 0 365008661 25767936 5889 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6291 5889 603 41 0 6250 0
vsize: 25164
[startup+1200 s]
Raw data (loadavg): 1.00 0.97 0.91 2/56 18517
Raw data (stat): 18452 (minisat+) R 18451 12452 12451 0 -1 0 5937 0 0 0 119999 19 0 0 25 0 1 0 365008661 25767936 5889 4294967295 134512640 134672761 3221224576 3221223568 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6291 5889 603 41 0 6250 0
vsize: 25164
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.97 0.91 1/56 18517
Raw data (stat): 18452 (minisat+) Z 18451 12452 12451 0 -1 12 5937 0 0 0 119999 20 0 0 25 0 1 0 365008661 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.02
CPU time (s): 1200.2
CPU user time (s): 1199.99
CPU system time (s): 0.202969
CPU usage (%): 100.015
Max. virtual memory (Kb): 25164
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####