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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl20_21_pb.cnf.cr.opb
MD5SUM112c693a7a90a8dc93ad23dc136d9b75
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 0
Biggest coefficient in the objective function 0
Number of bits for the biggest coefficient in the objective function 0
Sum of the numbers in the objective function 0
Number of bits of the sum of numbers in the objective function 0
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 22
Number of bits of the biggest sum of numbers5
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.026995
Number of variables840
Total number of constraints82
Number of constraints which are clauses42
Number of constraints which are cardinality constraints (but not clauses)40
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint20
Maximum length of a constraint21

Trace number 4579 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-04-13 19:23:51 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3392 boxname=wulflinc4 idbench=8 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  112c693a7a90a8dc93ad23dc136d9b75  /oldhome/oroussel/tmp/wulflinc4/normalized-chnl20_21_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc4/normalized-chnl20_21_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc4/normalized-chnl20_21_pb.cnf.cr.opb
IDLAUNCH: 3392
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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:        930752 kB
Buffers:         34036 kB
Cached:          50692 kB
SwapCached:          0 kB
Active:          48640 kB
Inactive:        38968 kB
HighTotal:      131008 kB
HighFree:        76496 kB
LowTotal:       903652 kB
LowFree:        854256 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            10628 kB
Committed_AS:    71664 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 19:44:04 (client local time) WITH STATUS 0 IN 1209.99 SECONDS
stats: 3392 7 1209.99 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 82 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..........................................
c ---[  39]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  38]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  37]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  36]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  35]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  34]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  33]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  32]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  31]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  30]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  29]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  28]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  27]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  26]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  25]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  24]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  23]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  22]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  21]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  20]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  19]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  18]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  17]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  16]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  15]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  14]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  13]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  12]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  11]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[  10]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[   9]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[   8]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[   7]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[   6]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[   5]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[   4]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[   3]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[   2]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[   1]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[   0]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    8402    30480 |    2800       0        0     nan |  0.000 % |
c |       100 |    8027    29155 |    3080      64      252     3.9 | 14.063 % |
c |       250 |    7711    28039 |    3388     179     1100     6.1 | 16.741 % |
c |       475 |    7533    27401 |    3726     384     2607     6.8 | 18.125 % |
c |       812 |    6799    24833 |    4099     617     4496     7.3 | 24.018 % |
c |      1319 |    6354    23364 |    4509    1043    46798    44.9 | 27.679 % |
c |      2079 |    6240    22994 |    4960    1783   174894    98.1 | 28.661 % |
c |      3218 |    6240    22994 |    5456    2922   405213   138.7 | 28.661 % |
c |      4927 |    6240    22994 |    6002    4631   795895   171.9 | 28.661 % |
c |      7491 |    6188    22826 |    6602    7186  1328902   184.9 | 29.152 % |
c |     11335 |    6188    22826 |    7262    7169  1423765   198.6 | 29.152 % |
c |     17102 |    6188    22826 |    7988    4587  1019974   222.4 | 29.152 % |
c |     25752 |    6188    22826 |    8787    8718  1945140   223.1 | 29.152 % |
c |     38726 |    6147    22693 |    9666    6851  1670747   243.9 | 29.509 % |
c |     58189 |    6140    22670 |   10632   10100  2629359   260.3 | 29.554 % |
c |     87381 |    6140    22670 |   11696    9882  2397749   242.6 | 29.554 % |
c |    131173 |    6140    22670 |   12865    8939  2216542   248.0 | 29.554 % |
c |    196859 |    6140    22670 |   14152   11989  2860459   238.6 | 29.554 % |
c |    295387 |    6042    22352 |   15567   11699  2703872   231.1 | 30.402 % |
#### 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.00 0.00 0.00 2/54 7209
Raw data (stat): 7209 (runsolver) R 7208 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420219390 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0007 s]
Raw data (loadavg): 0.15 0.03 0.01 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 2085 0 1 0 982 5 0 0 25 0 1 0 420219390 10133504 2064 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2474 2064 603 41 0 2433 0
vsize: 9896
[startup+20.0015 s]
Raw data (loadavg): 0.28 0.06 0.02 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 2666 0 1 0 1980 6 0 0 25 0 1 0 420219390 12591104 2645 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3074 2645 603 41 0 3033 0
vsize: 12296
[startup+30.0023 s]
Raw data (loadavg): 0.39 0.09 0.03 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 2911 0 1 0 2979 7 0 0 25 0 1 0 420219390 13533184 2890 4294967295 134512640 134672761 3221224544 3221223712 134564448 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3304 2890 603 41 0 3263 0
vsize: 13216
[startup+40.0032 s]
Raw data (loadavg): 0.49 0.12 0.04 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 3204 0 1 0 3977 9 0 0 25 0 1 0 420219390 14749696 3183 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3601 3183 603 41 0 3560 0
vsize: 14404
[startup+50.004 s]
Raw data (loadavg): 0.56 0.15 0.05 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 3277 0 1 0 4977 9 0 0 25 0 1 0 420219390 15020032 3256 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3667 3256 603 41 0 3626 0
vsize: 14668
[startup+60.0048 s]
Raw data (loadavg): 0.63 0.18 0.06 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 3408 0 1 0 5977 9 0 0 25 0 1 0 420219390 15560704 3387 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3799 3387 603 41 0 3758 0
vsize: 15196
[startup+70.0057 s]
Raw data (loadavg): 0.69 0.21 0.07 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 3729 0 1 0 6976 10 0 0 25 0 1 0 420219390 16916480 3708 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4130 3708 603 41 0 4089 0
vsize: 16520
[startup+80.0065 s]
Raw data (loadavg): 0.73 0.23 0.08 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 3834 0 1 0 7976 11 0 0 25 0 1 0 420219390 17321984 3813 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4229 3813 603 41 0 4188 0
vsize: 16916
[startup+90.0074 s]
Raw data (loadavg): 0.77 0.26 0.09 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 3927 0 1 0 8975 11 0 0 25 0 1 0 420219390 17727488 3906 4294967295 134512640 134672761 3221224544 3221223776 134541821 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4328 3906 603 41 0 4287 0
vsize: 17312
[startup+100.007 s]
Raw data (loadavg): 0.81 0.28 0.10 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 3927 0 1 0 9975 12 0 0 25 0 1 0 420219390 17727488 3906 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4328 3906 603 41 0 4287 0
vsize: 17312
[startup+110.008 s]
Raw data (loadavg): 0.84 0.30 0.11 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4191 0 1 0 10974 12 0 0 25 0 1 0 420219390 18808832 4170 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4592 4170 603 41 0 4551 0
vsize: 18368
[startup+120.009 s]
Raw data (loadavg): 0.86 0.33 0.12 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4191 0 1 0 11974 13 0 0 25 0 1 0 420219390 18808832 4170 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4592 4170 603 41 0 4551 0
vsize: 18368
[startup+130.01 s]
Raw data (loadavg): 0.88 0.35 0.12 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4198 0 1 0 12973 13 0 0 25 0 1 0 420219390 18808832 4177 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4592 4177 603 41 0 4551 0
vsize: 18368
[startup+140.011 s]
Raw data (loadavg): 0.90 0.37 0.13 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4216 0 1 0 13973 13 0 0 25 0 1 0 420219390 18944000 4195 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4625 4195 603 41 0 4584 0
vsize: 18500
[startup+150.011 s]
Raw data (loadavg): 0.92 0.39 0.14 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4222 0 1 0 14973 14 0 0 25 0 1 0 420219390 18944000 4201 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4625 4201 603 41 0 4584 0
vsize: 18500
[startup+160.012 s]
Raw data (loadavg): 0.93 0.41 0.15 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4223 0 1 0 15973 14 0 0 25 0 1 0 420219390 18944000 4202 4294967295 134512640 134672761 3221224544 3221223560 1075352664 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4625 4202 603 41 0 4584 0
vsize: 18500
[startup+170.012 s]
Raw data (loadavg): 0.94 0.43 0.16 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4440 0 1 0 16971 15 0 0 25 0 1 0 420219390 19890176 4419 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4856 4419 603 41 0 4815 0
vsize: 19424
[startup+180.013 s]
Raw data (loadavg): 0.95 0.45 0.17 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4451 0 1 0 17971 15 0 0 25 0 1 0 420219390 19890176 4430 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4856 4430 603 41 0 4815 0
vsize: 19424
[startup+190.014 s]
Raw data (loadavg): 0.95 0.46 0.18 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4522 0 1 0 18971 16 0 0 25 0 1 0 420219390 20160512 4501 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4922 4501 603 41 0 4881 0
vsize: 19688
[startup+200.014 s]
Raw data (loadavg): 0.96 0.48 0.19 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4568 0 1 0 19971 16 0 0 25 0 1 0 420219390 20430848 4547 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4988 4547 603 41 0 4947 0
vsize: 19952
[startup+210.014 s]
Raw data (loadavg): 0.97 0.50 0.19 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4568 0 1 0 20970 16 0 0 25 0 1 0 420219390 20430848 4547 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4988 4547 603 41 0 4947 0
vsize: 19952
[startup+220.015 s]
Raw data (loadavg): 0.97 0.51 0.20 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4655 0 1 0 21970 16 0 0 25 0 1 0 420219390 20701184 4634 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5054 4634 603 41 0 5013 0
vsize: 20216
[startup+230.016 s]
Raw data (loadavg): 0.98 0.53 0.21 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4655 0 1 0 22970 17 0 0 25 0 1 0 420219390 20701184 4634 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5054 4634 603 41 0 5013 0
vsize: 20216
[startup+240.017 s]
Raw data (loadavg): 0.98 0.54 0.22 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4687 0 1 0 23969 17 0 0 25 0 1 0 420219390 20836352 4666 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5087 4666 603 41 0 5046 0
vsize: 20348
[startup+250.017 s]
Raw data (loadavg): 0.98 0.56 0.22 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4687 0 1 0 24969 17 0 0 25 0 1 0 420219390 20836352 4666 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5087 4666 603 41 0 5046 0
vsize: 20348
[startup+260.019 s]
Raw data (loadavg): 0.98 0.57 0.23 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4698 0 1 0 25969 18 0 0 25 0 1 0 420219390 20996096 4677 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5126 4677 603 41 0 5085 0
vsize: 20504
[startup+270.02 s]
Raw data (loadavg): 0.99 0.59 0.24 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4699 0 1 0 26968 18 0 0 25 0 1 0 420219390 20996096 4678 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5126 4678 603 41 0 5085 0
vsize: 20504
[startup+280.02 s]
Raw data (loadavg): 0.99 0.60 0.25 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4699 0 1 0 27968 19 0 0 25 0 1 0 420219390 20996096 4678 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5126 4678 603 41 0 5085 0
vsize: 20504
[startup+290.021 s]
Raw data (loadavg): 0.99 0.61 0.26 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4699 0 1 0 28968 19 0 0 25 0 1 0 420219390 20996096 4678 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5126 4678 603 41 0 5085 0
vsize: 20504
[startup+300.021 s]
Raw data (loadavg): 0.99 0.62 0.26 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4700 0 1 0 29967 19 0 0 25 0 1 0 420219390 20996096 4679 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5126 4679 603 41 0 5085 0
vsize: 20504
[startup+310.022 s]
Raw data (loadavg): 0.99 0.64 0.27 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4854 0 1 0 30967 20 0 0 25 0 1 0 420219390 21536768 4833 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5258 4833 603 41 0 5217 0
vsize: 21032
[startup+320.023 s]
Raw data (loadavg): 0.99 0.65 0.28 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4963 0 1 0 31966 20 0 0 25 0 1 0 420219390 22077440 4942 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5390 4942 603 41 0 5349 0
vsize: 21560
[startup+330.024 s]
Raw data (loadavg): 0.99 0.66 0.29 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4963 0 1 0 32966 21 0 0 25 0 1 0 420219390 22077440 4942 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5390 4942 603 41 0 5349 0
vsize: 21560
[startup+340.024 s]
Raw data (loadavg): 0.99 0.67 0.29 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4963 0 1 0 33966 21 0 0 25 0 1 0 420219390 22077440 4942 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5390 4942 603 41 0 5349 0
vsize: 21560
[startup+350.024 s]
Raw data (loadavg): 0.99 0.68 0.30 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4963 0 1 0 34965 21 0 0 25 0 1 0 420219390 22032384 4942 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5379 4942 603 41 0 5338 0
vsize: 21516
[startup+360.025 s]
Raw data (loadavg): 0.99 0.69 0.31 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4963 0 1 0 35965 21 0 0 25 0 1 0 420219390 22032384 4942 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5379 4942 603 41 0 5338 0
vsize: 21516
[startup+370.025 s]
Raw data (loadavg): 0.99 0.70 0.31 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4963 0 1 0 36965 22 0 0 25 0 1 0 420219390 22032384 4942 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5379 4942 603 41 0 5338 0
vsize: 21516
[startup+380.026 s]
Raw data (loadavg): 0.99 0.71 0.32 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4963 0 1 0 37965 22 0 0 25 0 1 0 420219390 22032384 4942 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5379 4942 603 41 0 5338 0
vsize: 21516
[startup+390.027 s]
Raw data (loadavg): 0.99 0.72 0.33 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4963 0 1 0 38964 23 0 0 25 0 1 0 420219390 22032384 4942 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5379 4942 603 41 0 5338 0
vsize: 21516
[startup+400.026 s]
Raw data (loadavg): 0.99 0.73 0.33 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4970 0 1 0 39964 23 0 0 25 0 1 0 420219390 22032384 4949 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5379 4949 603 41 0 5338 0
vsize: 21516
[startup+410.027 s]
Raw data (loadavg): 0.99 0.74 0.34 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 4984 0 1 0 40964 23 0 0 25 0 1 0 420219390 22167552 4963 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5412 4963 603 41 0 5371 0
vsize: 21648
[startup+420.027 s]
Raw data (loadavg): 0.99 0.74 0.35 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5011 0 1 0 41963 24 0 0 25 0 1 0 420219390 22167552 4990 4294967295 134512640 134672761 3221224544 3221223648 134554656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5412 4990 603 41 0 5371 0
vsize: 21648
[startup+430.028 s]
Raw data (loadavg): 0.99 0.75 0.35 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5011 0 1 0 42963 24 0 0 25 0 1 0 420219390 22167552 4990 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5412 4990 603 41 0 5371 0
vsize: 21648
[startup+440.029 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5037 0 1 0 43962 24 0 0 25 0 1 0 420219390 22302720 5016 4294967295 134512640 134672761 3221224544 3221223648 134554636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5445 5016 603 41 0 5404 0
vsize: 21780
[startup+450.029 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5037 0 1 0 44962 24 0 0 25 0 1 0 420219390 22302720 5016 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5445 5016 603 41 0 5404 0
vsize: 21780
[startup+460.03 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5049 0 1 0 45962 25 0 0 25 0 1 0 420219390 22302720 5028 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5445 5028 603 41 0 5404 0
vsize: 21780
[startup+470.029 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5049 0 1 0 46961 25 0 0 25 0 1 0 420219390 22302720 5028 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5445 5028 603 41 0 5404 0
vsize: 21780
[startup+480.03 s]
Raw data (loadavg): 0.99 0.79 0.38 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5049 0 1 0 47961 26 0 0 25 0 1 0 420219390 22302720 5028 4294967295 134512640 134672761 3221224544 3221223492 1075352225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5445 5028 603 41 0 5404 0
vsize: 21780
[startup+490.031 s]
Raw data (loadavg): 0.99 0.79 0.39 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5049 0 1 0 48961 26 0 0 25 0 1 0 420219390 22302720 5028 4294967295 134512640 134672761 3221224544 3221223736 134554697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5445 5028 603 41 0 5404 0
vsize: 21780
[startup+500.032 s]
Raw data (loadavg): 0.99 0.80 0.40 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5049 0 1 0 49961 26 0 0 25 0 1 0 420219390 22302720 5028 4294967295 134512640 134672761 3221224544 3221223648 134554656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5445 5028 603 41 0 5404 0
vsize: 21780
[startup+510.033 s]
Raw data (loadavg): 0.99 0.81 0.40 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5049 0 1 0 50961 26 0 0 25 0 1 0 420219390 22302720 5028 4294967295 134512640 134672761 3221224544 3221223760 134541856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5445 5028 603 41 0 5404 0
vsize: 21780
[startup+520.034 s]
Raw data (loadavg): 0.99 0.81 0.41 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5049 0 1 0 51961 26 0 0 25 0 1 0 420219390 22302720 5028 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5445 5028 603 41 0 5404 0
vsize: 21780
[startup+530.034 s]
Raw data (loadavg): 0.99 0.82 0.41 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5337 0 1 0 52960 27 0 0 25 0 1 0 420219390 23527424 5316 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5744 5316 603 41 0 5703 0
vsize: 22976
[startup+540.035 s]
Raw data (loadavg): 0.99 0.82 0.42 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5338 0 1 0 53959 28 0 0 25 0 1 0 420219390 23527424 5317 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5744 5317 603 41 0 5703 0
vsize: 22976
[startup+550.035 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5356 0 1 0 54959 28 0 0 25 0 1 0 420219390 23666688 5335 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5778 5335 603 41 0 5737 0
vsize: 23112
[startup+560.036 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5397 0 1 0 55959 28 0 0 25 0 1 0 420219390 23801856 5376 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5811 5376 603 41 0 5770 0
vsize: 23244
[startup+570.037 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5397 0 1 0 56959 28 0 0 25 0 1 0 420219390 23801856 5376 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5811 5376 603 41 0 5770 0
vsize: 23244
[startup+580.038 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5397 0 1 0 57959 29 0 0 25 0 1 0 420219390 23801856 5376 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5811 5376 603 41 0 5770 0
vsize: 23244
[startup+590.039 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5430 0 1 0 58958 29 0 0 25 0 1 0 420219390 23937024 5409 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5844 5409 603 41 0 5803 0
vsize: 23376
[startup+600.039 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5440 0 1 0 59958 29 0 0 25 0 1 0 420219390 24072192 5419 4294967295 134512640 134672761 3221224544 3221223728 134559616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5877 5419 603 41 0 5836 0
vsize: 23508
[startup+610.04 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5440 0 1 0 60958 29 0 0 25 0 1 0 420219390 24072192 5419 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5877 5419 603 41 0 5836 0
vsize: 23508
[startup+620.04 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5440 0 1 0 61957 30 0 0 25 0 1 0 420219390 24072192 5419 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5877 5419 603 41 0 5836 0
vsize: 23508
[startup+630.041 s]
Raw data (loadavg): 0.99 0.86 0.47 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5440 0 1 0 62958 30 0 0 25 0 1 0 420219390 24072192 5419 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5877 5419 603 41 0 5836 0
vsize: 23508
[startup+640.042 s]
Raw data (loadavg): 0.99 0.87 0.47 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5440 0 1 0 63957 30 0 0 25 0 1 0 420219390 24072192 5419 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5877 5419 603 41 0 5836 0
vsize: 23508
[startup+650.042 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5519 0 1 0 64956 31 0 0 25 0 1 0 420219390 24342528 5498 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5943 5498 603 41 0 5902 0
vsize: 23772
[startup+660.042 s]
Raw data (loadavg): 0.99 0.88 0.48 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5519 0 1 0 65956 31 0 0 25 0 1 0 420219390 24342528 5498 4294967295 134512640 134672761 3221224544 3221223712 134559068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5943 5498 603 41 0 5902 0
vsize: 23772
[startup+670.043 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5519 0 1 0 66956 31 0 0 25 0 1 0 420219390 24342528 5498 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5943 5498 603 41 0 5902 0
vsize: 23772
[startup+680.044 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5545 0 1 0 67956 32 0 0 25 0 1 0 420219390 24477696 5524 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5976 5524 603 41 0 5935 0
vsize: 23904
[startup+690.044 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5684 0 1 0 68956 32 0 0 25 0 1 0 420219390 25018368 5663 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6108 5663 603 41 0 6067 0
vsize: 24432
[startup+700.044 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5684 0 1 0 69956 32 0 0 25 0 1 0 420219390 25018368 5663 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6108 5663 603 41 0 6067 0
vsize: 24432
[startup+710.044 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5719 0 1 0 70957 32 0 0 25 0 1 0 420219390 25153536 5698 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6141 5698 603 41 0 6100 0
vsize: 24564
[startup+720.044 s]
Raw data (loadavg): 0.99 0.90 0.51 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5733 0 1 0 71957 32 0 0 25 0 1 0 420219390 25288704 5712 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6174 5712 603 41 0 6133 0
vsize: 24696
[startup+730.045 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5734 0 1 0 72957 32 0 0 25 0 1 0 420219390 25288704 5713 4294967295 134512640 134672761 3221224544 3221223648 134560367 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6174 5713 603 41 0 6133 0
vsize: 24696
[startup+740.046 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5734 0 1 0 73957 32 0 0 25 0 1 0 420219390 25260032 5713 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6167 5713 603 41 0 6126 0
vsize: 24668
[startup+750.046 s]
Raw data (loadavg): 0.99 0.90 0.53 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5734 0 1 0 74957 32 0 0 25 0 1 0 420219390 25260032 5713 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6167 5713 603 41 0 6126 0
vsize: 24668
[startup+760.047 s]
Raw data (loadavg): 0.99 0.91 0.53 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5734 0 1 0 75957 32 0 0 25 0 1 0 420219390 25260032 5713 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6167 5713 603 41 0 6126 0
vsize: 24668
[startup+770.046 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5734 0 1 0 76958 32 0 0 25 0 1 0 420219390 25260032 5713 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6167 5713 603 41 0 6126 0
vsize: 24668
[startup+780.047 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5735 0 1 0 77958 32 0 0 25 0 1 0 420219390 25260032 5714 4294967295 134512640 134672761 3221224544 3221223728 134559616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6167 5714 603 41 0 6126 0
vsize: 24668
[startup+790.047 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5735 0 1 0 78958 32 0 0 25 0 1 0 420219390 25260032 5714 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6167 5714 603 41 0 6126 0
vsize: 24668
[startup+800.047 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5735 0 1 0 79958 32 0 0 25 0 1 0 420219390 25260032 5714 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6167 5714 603 41 0 6126 0
vsize: 24668
[startup+810.048 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5735 0 1 0 80958 32 0 0 25 0 1 0 420219390 25260032 5714 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6167 5714 603 41 0 6126 0
vsize: 24668
[startup+820.048 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5735 0 1 0 81958 32 0 0 25 0 1 0 420219390 25260032 5714 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6167 5714 603 41 0 6126 0
vsize: 24668
[startup+830.049 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5735 0 1 0 82959 32 0 0 25 0 1 0 420219390 25260032 5714 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6167 5714 603 41 0 6126 0
vsize: 24668
[startup+840.048 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5735 0 1 0 83959 32 0 0 25 0 1 0 420219390 25260032 5714 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6167 5714 603 41 0 6126 0
vsize: 24668
[startup+850.048 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5735 0 1 0 84959 32 0 0 25 0 1 0 420219390 25260032 5714 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6167 5714 603 41 0 6126 0
vsize: 24668
[startup+860.049 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5735 0 1 0 85959 32 0 0 25 0 1 0 420219390 25260032 5714 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6167 5714 603 41 0 6126 0
vsize: 24668
[startup+870.049 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5735 0 1 0 86959 32 0 0 25 0 1 0 420219390 25260032 5714 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6167 5714 603 41 0 6126 0
vsize: 24668
[startup+880.05 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5735 0 1 0 87960 32 0 0 25 0 1 0 420219390 25260032 5714 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6167 5714 603 41 0 6126 0
vsize: 24668
[startup+890.05 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5735 0 1 0 88959 32 0 0 25 0 1 0 420219390 25260032 5714 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6167 5714 603 41 0 6126 0
vsize: 24668
[startup+900.049 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5735 0 1 0 89959 32 0 0 25 0 1 0 420219390 25260032 5714 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6167 5714 603 41 0 6126 0
vsize: 24668
[startup+910.05 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5735 0 1 0 90959 32 0 0 25 0 1 0 420219390 25260032 5714 4294967295 134512640 134672761 3221224544 3221223712 134560968 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6167 5714 603 41 0 6126 0
vsize: 24668
[startup+920.051 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5735 0 1 0 91959 32 0 0 25 0 1 0 420219390 25260032 5714 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6167 5714 603 41 0 6126 0
vsize: 24668
[startup+930.052 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5735 0 1 0 92959 32 0 0 25 0 1 0 420219390 25260032 5714 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6167 5714 603 41 0 6126 0
vsize: 24668
[startup+940.053 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5942 0 1 0 93959 33 0 0 25 0 1 0 420219390 26243072 5921 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6407 5921 603 41 0 6366 0
vsize: 25628
[startup+950.053 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5942 0 1 0 94959 33 0 0 25 0 1 0 420219390 26243072 5921 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6407 5921 603 41 0 6366 0
vsize: 25628
[startup+960.053 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5962 0 1 0 95960 33 0 0 25 0 1 0 420219390 26243072 5941 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6407 5941 603 41 0 6366 0
vsize: 25628
[startup+970.053 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 5962 0 1 0 96960 33 0 0 25 0 1 0 420219390 26243072 5941 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6407 5941 603 41 0 6366 0
vsize: 25628
[startup+980.054 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 6055 0 1 0 97960 33 0 0 25 0 1 0 420219390 26648576 6034 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6506 6034 603 41 0 6465 0
vsize: 26024
[startup+990.055 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 6141 0 1 0 98959 34 0 0 25 0 1 0 420219390 27054080 6120 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6605 6120 603 41 0 6564 0
vsize: 26420
[startup+1000.05 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 6156 0 1 0 99960 34 0 0 25 0 1 0 420219390 27054080 6135 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6605 6135 603 41 0 6564 0
vsize: 26420
[startup+1010.06 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 6267 0 1 0 100960 34 0 0 25 0 1 0 420219390 27590656 6246 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6736 6246 603 41 0 6695 0
vsize: 26944
[startup+1020.06 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 6267 0 1 0 101960 34 0 0 25 0 1 0 420219390 27590656 6246 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6736 6246 603 41 0 6695 0
vsize: 26944
[startup+1030.06 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 6267 0 1 0 102960 34 0 0 25 0 1 0 420219390 27590656 6246 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6736 6246 603 41 0 6695 0
vsize: 26944
[startup+1040.06 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 6267 0 1 0 103960 34 0 0 25 0 1 0 420219390 27590656 6246 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6736 6246 603 41 0 6695 0
vsize: 26944
[startup+1050.06 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 6267 0 1 0 104960 34 0 0 25 0 1 0 420219390 27590656 6246 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6736 6246 603 41 0 6695 0
vsize: 26944
[startup+1060.06 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 6267 0 1 0 105961 34 0 0 25 0 1 0 420219390 27590656 6246 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6736 6246 603 41 0 6695 0
vsize: 26944
[startup+1070.06 s]
Raw data (loadavg): 0.99 0.96 0.65 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 6267 0 1 0 106961 34 0 0 25 0 1 0 420219390 27590656 6246 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6736 6246 603 41 0 6695 0
vsize: 26944
[startup+1080.06 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 6267 0 1 0 107961 34 0 0 25 0 1 0 420219390 27590656 6246 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6736 6246 603 41 0 6695 0
vsize: 26944
[startup+1090.06 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 6267 0 1 0 108961 34 0 0 25 0 1 0 420219390 27590656 6246 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6736 6246 603 41 0 6695 0
vsize: 26944
[startup+1100.06 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 6268 0 1 0 109961 34 0 0 25 0 1 0 420219390 27590656 6247 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6736 6247 603 41 0 6695 0
vsize: 26944
[startup+1110.06 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 6299 0 1 0 110962 34 0 0 25 0 1 0 420219390 27750400 6278 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6775 6278 603 41 0 6734 0
vsize: 27100
[startup+1120.06 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 6299 0 1 0 111962 34 0 0 25 0 1 0 420219390 27750400 6278 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6775 6278 603 41 0 6734 0
vsize: 27100
[startup+1130.06 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 6299 0 1 0 112962 34 0 0 25 0 1 0 420219390 27750400 6278 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6775 6278 603 41 0 6734 0
vsize: 27100
[startup+1140.06 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 6299 0 1 0 113962 34 0 0 25 0 1 0 420219390 27750400 6278 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6775 6278 603 41 0 6734 0
vsize: 27100
[startup+1150.06 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 6299 0 1 0 114962 34 0 0 25 0 1 0 420219390 27750400 6278 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6775 6278 603 41 0 6734 0
vsize: 27100
[startup+1160.06 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 6299 0 1 0 115962 34 0 0 25 0 1 0 420219390 27750400 6278 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6775 6278 603 41 0 6734 0
vsize: 27100
[startup+1170.06 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 6299 0 1 0 116963 34 0 0 25 0 1 0 420219390 27750400 6278 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6775 6278 603 41 0 6734 0
vsize: 27100
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 6325 0 1 0 117963 34 0 0 25 0 1 0 420219390 27885568 6304 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6808 6304 603 41 0 6767 0
vsize: 27232
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 6333 0 1 0 118962 34 0 0 25 0 1 0 420219390 27885568 6312 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6808 6312 603 41 0 6767 0
vsize: 27232
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 6440 0 1 0 119962 35 0 0 25 0 1 0 420219390 28291072 6419 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6907 6419 603 41 0 6866 0
vsize: 27628
[startup+1210.06 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 7209
Raw data (stat): 7209 (minisat+) R 7208 5897 5896 0 -1 0 6459 0 1 0 120962 35 0 0 25 0 1 0 420219390 28454912 6438 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6947 6438 603 41 0 6906 0
vsize: 27788
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1210.08 s]
Raw data (loadavg): 0.99 0.97 0.69 1/54 7209
Raw data (stat): 7209 (minisat+) Z 7208 5897 5896 0 -1 12 6461 0 1 0 120962 36 0 0 25 0 1 0 420219390 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1210.08
CPU time (s): 1209.99
CPU user time (s): 1209.63
CPU system time (s): 0.364944
CPU usage (%): 99.993
Max. virtual memory (Kb): 27788
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####