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_30_pb.cnf.cr.opb
MD5SUMafcc4289aafaea265ed2d465965a3342
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 31
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.036993
Number of variables1200
Total number of constraints100
Number of constraints which are clauses60
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 constraint30

Trace number 6089 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-04-14 03:25:02 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4522 boxname=wulflinc26 idbench=10 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  afcc4289aafaea265ed2d465965a3342  /oldhome/oroussel/tmp/wulflinc26/normalized-chnl20_30_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc26/normalized-chnl20_30_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc26/normalized-chnl20_30_pb.cnf.cr.opb
IDLAUNCH: 4522
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        824436 kB
Buffers:         35544 kB
Cached:         134224 kB
SwapCached:       2476 kB
Active:          56072 kB
Inactive:       119012 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        824184 kB
SwapTotal:     2097892 kB
SwapFree:      2095416 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            29284 kB
Committed_AS:    63616 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:45:05 (client local time) WITH STATUS 0 IN 1200.2 SECONDS
stats: 4522 7 1200.2 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 100 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ............................................................
c ---[  39]---> BDD-cost:   57
c ---[  38]---> BDD-cost:   57
c ---[  37]---> BDD-cost:   57
c ---[  36]---> BDD-cost:   57
c ---[  35]---> BDD-cost:   57
c ---[  34]---> BDD-cost:   57
c ---[  33]---> BDD-cost:   57
c ---[  32]---> BDD-cost:   57
c ---[  31]---> BDD-cost:   57
c ---[  30]---> BDD-cost:   57
c ---[  29]---> BDD-cost:   57
c ---[  28]---> BDD-cost:   57
c ---[  27]---> BDD-cost:   57
c ---[  26]---> BDD-cost:   57
c ---[  25]---> BDD-cost:   57
c ---[  24]---> BDD-cost:   57
c ---[  23]---> BDD-cost:   57
c ---[  22]---> BDD-cost:   57
c ---[  21]---> BDD-cost:   57
c ---[  20]---> BDD-cost:   57
c ---[  19]---> BDD-cost:   57
c ---[  18]---> BDD-cost:   57
c ---[  17]---> BDD-cost:   57
c ---[  16]---> BDD-cost:   57
c ---[  15]---> BDD-cost:   57
c ---[  14]---> BDD-cost:   57
c ---[  13]---> BDD-cost:   57
c ---[  12]---> BDD-cost:   57
c ---[  11]---> BDD-cost:   57
c ---[  10]---> BDD-cost:   57
c ---[   9]---> BDD-cost:   57
c ---[   8]---> BDD-cost:   57
c ---[   7]---> BDD-cost:   57
c ---[   6]---> BDD-cost:   57
c ---[   5]---> BDD-cost:   57
c ---[   4]---> BDD-cost:   57
c ---[   3]---> BDD-cost:   57
c ---[   2]---> BDD-cost:   57
c ---[   1]---> BDD-cost:   57
c ---[   0]---> BDD-cost:   57
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   10140    29120 |    3380       0        0     nan |  0.000 % |
c |       100 |   10060    28880 |    3718      45     1428    31.7 |  1.609 % |
c |       250 |    9995    28685 |    4089     157    12518    79.7 |  1.983 % |
c |       476 |    9945    28535 |    4498     321    25460    79.3 |  2.270 % |
c |       813 |    9885    28355 |    4948     636    57118    89.8 |  2.615 % |
c |      1319 |    9835    28205 |    5443    1121   113000   100.8 |  2.902 % |
c |      2079 |    9745    27935 |    5987    1841   220239   119.6 |  3.420 % |
c |      3218 |    9635    27605 |    6586    2934   348194   118.7 |  4.052 % |
c |      4929 |    9565    27395 |    7245    4603   585979   127.3 |  4.454 % |
c |      7495 |    9340    26720 |    7969    7065   862921   122.1 |  5.747 % |
c |     11341 |    9085    25955 |    8766    6555   772943   117.9 |  7.213 % |
c |     17108 |    8775    25025 |    9643    7574  1074386   141.9 |  8.994 % |
c |     25759 |    8335    23705 |   10607    5718   770059   134.7 | 11.523 % |
c |     38735 |    7975    22625 |   11668    7507  1087730   144.9 | 13.592 % |
c |     58198 |    7815    22145 |   12835    7698  1269200   164.9 | 14.512 % |
c |     87390 |    7270    20510 |   14119    9593  1418247   147.8 | 17.644 % |
c |    131180 |    6755    18965 |   15531    7669  1346972   175.6 | 20.603 % |
c |    196864 |    6385    17855 |   17084   14960  3047064   203.7 | 22.730 % |
c |    295392 |    5500    15200 |   18792   11502  2210671   192.2 | 27.816 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/54 30584
Raw data (stat): 30584 (runsolver) R 30583 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481336738 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 1848 0 0 0 994 4 0 0 25 0 1 0 481336738 9097216 1826 4294967295 134512640 134672761 3221224544 3221223672 1075347105 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2221 1826 603 41 0 2180 0
vsize: 8884
[startup+20.0008 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 2001 0 0 0 1994 5 0 0 25 0 1 0 481336738 9768960 1979 4294967295 134512640 134672761 3221224544 3221223648 134560174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2385 1979 603 41 0 2344 0
vsize: 9540
[startup+30.002 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 2374 0 0 0 2993 6 0 0 25 0 1 0 481336738 11243520 2352 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2745 2352 603 41 0 2704 0
vsize: 10980
[startup+40.0026 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 2706 0 0 0 3992 7 0 0 25 0 1 0 481336738 12718080 2684 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3105 2684 603 41 0 3064 0
vsize: 12420
[startup+50.0029 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 2892 0 0 0 4991 8 0 0 25 0 1 0 481336738 13393920 2870 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3270 2870 603 41 0 3229 0
vsize: 13080
[startup+60.003 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 2893 0 0 0 5991 8 0 0 25 0 1 0 481336738 13393920 2871 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3270 2871 603 41 0 3229 0
vsize: 13080
[startup+70.0037 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 2894 0 0 0 6990 9 0 0 25 0 1 0 481336738 13393920 2872 4294967295 134512640 134672761 3221224544 3221223728 134559572 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3270 2872 603 41 0 3229 0
vsize: 13080
[startup+80.0039 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 3168 0 0 0 7989 10 0 0 25 0 1 0 481336738 14598144 3146 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3564 3146 603 41 0 3523 0
vsize: 14256
[startup+90.0039 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 3508 0 0 0 8988 11 0 0 25 0 1 0 481336738 15941632 3486 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3892 3486 603 41 0 3851 0
vsize: 15568
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 3578 0 0 0 9988 12 0 0 25 0 1 0 481336738 16211968 3556 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3958 3556 603 41 0 3917 0
vsize: 15832
[startup+110.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 3700 0 0 0 10987 12 0 0 25 0 1 0 481336738 16752640 3678 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4090 3678 603 41 0 4049 0
vsize: 16360
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 3700 0 0 0 11987 13 0 0 25 0 1 0 481336738 16752640 3678 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4090 3678 603 41 0 4049 0
vsize: 16360
[startup+130.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 3702 0 0 0 12986 13 0 0 25 0 1 0 481336738 16752640 3680 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4090 3680 603 41 0 4049 0
vsize: 16360
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 3702 0 0 0 13986 14 0 0 25 0 1 0 481336738 16752640 3680 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4090 3680 603 41 0 4049 0
vsize: 16360
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 3702 0 0 0 14986 14 0 0 25 0 1 0 481336738 16752640 3680 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4090 3680 603 41 0 4049 0
vsize: 16360
[startup+160.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 3702 0 0 0 15986 14 0 0 25 0 1 0 481336738 16752640 3680 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4090 3680 603 41 0 4049 0
vsize: 16360
[startup+170.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 3702 0 0 0 16985 15 0 0 25 0 1 0 481336738 16752640 3680 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4090 3680 603 41 0 4049 0
vsize: 16360
[startup+180.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 3702 0 0 0 17985 15 0 0 25 0 1 0 481336738 16752640 3680 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4090 3680 603 41 0 4049 0
vsize: 16360
[startup+190.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 3984 0 0 0 18983 17 0 0 25 0 1 0 481336738 18006016 3962 4294967295 134512640 134672761 3221224544 3221223648 134559890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4396 3962 603 41 0 4355 0
vsize: 17584
[startup+200.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 4491 0 0 0 19982 18 0 0 25 0 1 0 481336738 20017152 4469 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4887 4469 603 41 0 4846 0
vsize: 19548
[startup+210.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 4692 0 0 0 20982 19 0 0 25 0 1 0 481336738 20992000 4670 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5125 4670 603 41 0 5084 0
vsize: 20500
[startup+220.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 4725 0 0 0 21981 19 0 0 25 0 1 0 481336738 21127168 4703 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5158 4703 603 41 0 5117 0
vsize: 20632
[startup+230.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 4824 0 0 0 22980 21 0 0 25 0 1 0 481336738 21528576 4802 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5256 4802 603 41 0 5215 0
vsize: 21024
[startup+240.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 4824 0 0 0 23980 21 0 0 25 0 1 0 481336738 21528576 4802 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5256 4802 603 41 0 5215 0
vsize: 21024
[startup+250.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5050 0 0 0 24979 22 0 0 25 0 1 0 481336738 22470656 5028 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5486 5028 603 41 0 5445 0
vsize: 21944
[startup+260.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5050 0 0 0 25979 22 0 0 25 0 1 0 481336738 22470656 5028 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5486 5028 603 41 0 5445 0
vsize: 21944
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5050 0 0 0 26979 22 0 0 25 0 1 0 481336738 22470656 5028 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5486 5028 603 41 0 5445 0
vsize: 21944
[startup+280.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5050 0 0 0 27979 22 0 0 25 0 1 0 481336738 22470656 5028 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5486 5028 603 41 0 5445 0
vsize: 21944
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5050 0 0 0 28979 23 0 0 25 0 1 0 481336738 22470656 5028 4294967295 134512640 134672761 3221224544 3221223728 134558853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5486 5028 603 41 0 5445 0
vsize: 21944
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5138 0 0 0 29978 23 0 0 25 0 1 0 481336738 22740992 5116 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5552 5116 603 41 0 5511 0
vsize: 22208
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5377 0 0 0 30977 24 0 0 25 0 1 0 481336738 23818240 5355 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5815 5355 603 41 0 5774 0
vsize: 23260
[startup+320.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5377 0 0 0 31977 25 0 0 25 0 1 0 481336738 23818240 5355 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5815 5355 603 41 0 5774 0
vsize: 23260
[startup+330.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5377 0 0 0 32977 25 0 0 25 0 1 0 481336738 23818240 5355 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5815 5355 603 41 0 5774 0
vsize: 23260
[startup+340.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5377 0 0 0 33977 25 0 0 25 0 1 0 481336738 23818240 5355 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5815 5355 603 41 0 5774 0
vsize: 23260
[startup+350.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5441 0 0 0 34977 25 0 0 25 0 1 0 481336738 23953408 5419 4294967295 134512640 134672761 3221224544 3221223648 134560212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5848 5419 603 41 0 5807 0
vsize: 23392
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5493 0 0 0 35977 25 0 0 25 0 1 0 481336738 24223744 5471 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5914 5471 603 41 0 5873 0
vsize: 23656
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5496 0 0 0 36977 25 0 0 25 0 1 0 481336738 24223744 5474 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5914 5474 603 41 0 5873 0
vsize: 23656
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5496 0 0 0 37978 25 0 0 25 0 1 0 481336738 24223744 5474 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5914 5474 603 41 0 5873 0
vsize: 23656
[startup+390.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5496 0 0 0 38978 25 0 0 25 0 1 0 481336738 24223744 5474 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5914 5474 603 41 0 5873 0
vsize: 23656
[startup+400.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5497 0 0 0 39978 25 0 0 25 0 1 0 481336738 24223744 5475 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5914 5475 603 41 0 5873 0
vsize: 23656
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5497 0 0 0 40978 25 0 0 25 0 1 0 481336738 24223744 5475 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5914 5475 603 41 0 5873 0
vsize: 23656
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5515 0 0 0 41978 25 0 0 25 0 1 0 481336738 24387584 5493 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5954 5493 603 41 0 5913 0
vsize: 23816
[startup+430.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5527 0 0 0 42978 26 0 0 25 0 1 0 481336738 24387584 5505 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5954 5505 603 41 0 5913 0
vsize: 23816
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5528 0 0 0 43978 26 0 0 25 0 1 0 481336738 24387584 5506 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5954 5506 603 41 0 5913 0
vsize: 23816
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5528 0 0 0 44979 26 0 0 25 0 1 0 481336738 24387584 5506 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5954 5506 603 41 0 5913 0
vsize: 23816
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5528 0 0 0 45979 26 0 0 25 0 1 0 481336738 24387584 5506 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5954 5506 603 41 0 5913 0
vsize: 23816
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5529 0 0 0 46979 26 0 0 25 0 1 0 481336738 24387584 5507 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5954 5507 603 41 0 5913 0
vsize: 23816
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5529 0 0 0 47979 26 0 0 25 0 1 0 481336738 24387584 5507 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5954 5507 603 41 0 5913 0
vsize: 23816
[startup+490.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5543 0 0 0 48979 26 0 0 25 0 1 0 481336738 24387584 5521 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5954 5521 603 41 0 5913 0
vsize: 23816
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5589 0 0 0 49979 26 0 0 25 0 1 0 481336738 24715264 5567 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6034 5567 603 41 0 5993 0
vsize: 24136
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5591 0 0 0 50979 26 0 0 25 0 1 0 481336738 24715264 5569 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6034 5569 603 41 0 5993 0
vsize: 24136
[startup+520.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5591 0 0 0 51979 26 0 0 25 0 1 0 481336738 24715264 5569 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6034 5569 603 41 0 5993 0
vsize: 24136
[startup+530.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5591 0 0 0 52979 26 0 0 25 0 1 0 481336738 24715264 5569 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6034 5569 603 41 0 5993 0
vsize: 24136
[startup+540.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5591 0 0 0 53980 26 0 0 25 0 1 0 481336738 24715264 5569 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6034 5569 603 41 0 5993 0
vsize: 24136
[startup+550.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5591 0 0 0 54980 26 0 0 25 0 1 0 481336738 24715264 5569 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6034 5569 603 41 0 5993 0
vsize: 24136
[startup+560.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5591 0 0 0 55980 26 0 0 25 0 1 0 481336738 24715264 5569 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6034 5569 603 41 0 5993 0
vsize: 24136
[startup+570.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5608 0 0 0 56980 26 0 0 25 0 1 0 481336738 24715264 5586 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6034 5586 603 41 0 5993 0
vsize: 24136
[startup+580.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5617 0 0 0 57979 27 0 0 25 0 1 0 481336738 24911872 5595 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6082 5595 603 41 0 6041 0
vsize: 24328
[startup+590.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5617 0 0 0 58978 27 0 0 25 0 1 0 481336738 24911872 5595 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6082 5595 603 41 0 6041 0
vsize: 24328
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5627 0 0 0 59979 27 0 0 25 0 1 0 481336738 24911872 5605 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6082 5605 603 41 0 6041 0
vsize: 24328
[startup+610.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5703 0 0 0 60979 27 0 0 25 0 1 0 481336738 25182208 5681 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6148 5681 603 41 0 6107 0
vsize: 24592
[startup+620.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5786 0 0 0 61979 27 0 0 25 0 1 0 481336738 25587712 5764 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6247 5764 603 41 0 6206 0
vsize: 24988
[startup+630.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5892 0 0 0 62979 27 0 0 25 0 1 0 481336738 25993216 5870 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6346 5870 603 41 0 6305 0
vsize: 25384
[startup+640.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5936 0 0 0 63979 27 0 0 25 0 1 0 481336738 26157056 5914 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6386 5914 603 41 0 6345 0
vsize: 25544
[startup+650.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5936 0 0 0 64979 28 0 0 25 0 1 0 481336738 26157056 5914 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6386 5914 603 41 0 6345 0
vsize: 25544
[startup+660.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5936 0 0 0 65979 28 0 0 25 0 1 0 481336738 26157056 5914 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6386 5914 603 41 0 6345 0
vsize: 25544
[startup+670.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5936 0 0 0 66979 28 0 0 25 0 1 0 481336738 26157056 5914 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6386 5914 603 41 0 6345 0
vsize: 25544
[startup+680.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5936 0 0 0 67980 28 0 0 25 0 1 0 481336738 26157056 5914 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6386 5914 603 41 0 6345 0
vsize: 25544
[startup+690.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5936 0 0 0 68980 28 0 0 25 0 1 0 481336738 26157056 5914 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6386 5914 603 41 0 6345 0
vsize: 25544
[startup+700.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5936 0 0 0 69980 28 0 0 25 0 1 0 481336738 26157056 5914 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6386 5914 603 41 0 6345 0
vsize: 25544
[startup+710.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5942 0 0 0 70980 28 0 0 25 0 1 0 481336738 26157056 5920 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6386 5920 603 41 0 6345 0
vsize: 25544
[startup+720.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5942 0 0 0 71980 28 0 0 25 0 1 0 481336738 26157056 5920 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6386 5920 603 41 0 6345 0
vsize: 25544
[startup+730.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5943 0 0 0 72980 28 0 0 25 0 1 0 481336738 26157056 5921 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6386 5921 603 41 0 6345 0
vsize: 25544
[startup+740.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5943 0 0 0 73980 28 0 0 25 0 1 0 481336738 26157056 5921 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6386 5921 603 41 0 6345 0
vsize: 25544
[startup+750.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5943 0 0 0 74980 28 0 0 25 0 1 0 481336738 26157056 5921 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6386 5921 603 41 0 6345 0
vsize: 25544
[startup+760.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5943 0 0 0 75981 28 0 0 25 0 1 0 481336738 26157056 5921 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6386 5921 603 41 0 6345 0
vsize: 25544
[startup+770.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5949 0 0 0 76981 28 0 0 25 0 1 0 481336738 26312704 5927 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6424 5927 603 41 0 6383 0
vsize: 25696
[startup+780.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5949 0 0 0 77981 28 0 0 25 0 1 0 481336738 26312704 5927 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6424 5927 603 41 0 6383 0
vsize: 25696
[startup+790.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5949 0 0 0 78981 28 0 0 25 0 1 0 481336738 26312704 5927 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6424 5927 603 41 0 6383 0
vsize: 25696
[startup+800.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5971 0 0 0 79981 28 0 0 25 0 1 0 481336738 26312704 5949 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6424 5949 603 41 0 6383 0
vsize: 25696
[startup+810.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 5982 0 0 0 80981 29 0 0 25 0 1 0 481336738 26476544 5960 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6464 5960 603 41 0 6423 0
vsize: 25856
[startup+820.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 6003 0 0 0 81981 29 0 0 25 0 1 0 481336738 26476544 5981 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6464 5981 603 41 0 6423 0
vsize: 25856
[startup+830.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 6004 0 0 0 82981 29 0 0 25 0 1 0 481336738 26476544 5982 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6464 5982 603 41 0 6423 0
vsize: 25856
[startup+840.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 6009 0 0 0 83981 29 0 0 25 0 1 0 481336738 26640384 5987 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6504 5987 603 41 0 6463 0
vsize: 26016
[startup+850.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 6020 0 0 0 84982 29 0 0 25 0 1 0 481336738 26640384 5998 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6504 5998 603 41 0 6463 0
vsize: 26016
[startup+860.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 6020 0 0 0 85982 29 0 0 25 0 1 0 481336738 26640384 5998 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6504 5998 603 41 0 6463 0
vsize: 26016
[startup+870.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 6020 0 0 0 86982 29 0 0 25 0 1 0 481336738 26640384 5998 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6504 5998 603 41 0 6463 0
vsize: 26016
[startup+880.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 6033 0 0 0 87982 29 0 0 25 0 1 0 481336738 26640384 6011 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6504 6011 603 41 0 6463 0
vsize: 26016
[startup+890.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 6068 0 0 0 88982 30 0 0 25 0 1 0 481336738 26968064 6046 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6584 6046 603 41 0 6543 0
vsize: 26336
[startup+900.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 6068 0 0 0 89982 30 0 0 25 0 1 0 481336738 26968064 6046 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6584 6046 603 41 0 6543 0
vsize: 26336
[startup+910.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 6068 0 0 0 90982 30 0 0 25 0 1 0 481336738 26968064 6046 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6584 6046 603 41 0 6543 0
vsize: 26336
[startup+920.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 6068 0 0 0 91982 30 0 0 25 0 1 0 481336738 26968064 6046 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6584 6046 603 41 0 6543 0
vsize: 26336
[startup+930.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 6068 0 0 0 92982 30 0 0 25 0 1 0 481336738 26968064 6046 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6584 6046 603 41 0 6543 0
vsize: 26336
[startup+940.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 6068 0 0 0 93982 30 0 0 25 0 1 0 481336738 26968064 6046 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6584 6046 603 41 0 6543 0
vsize: 26336
[startup+950.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 6068 0 0 0 94982 30 0 0 25 0 1 0 481336738 26968064 6046 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6584 6046 603 41 0 6543 0
vsize: 26336
[startup+960.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 6068 0 0 0 95983 30 0 0 25 0 1 0 481336738 26968064 6046 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6584 6046 603 41 0 6543 0
vsize: 26336
[startup+970.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 6068 0 0 0 96983 30 0 0 25 0 1 0 481336738 26968064 6046 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6584 6046 603 41 0 6543 0
vsize: 26336
[startup+980.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 6342 0 0 0 97982 31 0 0 25 0 1 0 481336738 28033024 6320 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6844 6320 603 41 0 6803 0
vsize: 27376
[startup+990.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 6474 0 0 0 98982 32 0 0 25 0 1 0 481336738 28557312 6452 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6972 6452 603 41 0 6931 0
vsize: 27888
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 6486 0 0 0 99982 32 0 0 25 0 1 0 481336738 28708864 6464 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7009 6464 603 41 0 6968 0
vsize: 28036
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 6694 0 0 0 100982 32 0 0 25 0 1 0 481336738 29499392 6672 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7202 6672 603 41 0 7161 0
vsize: 28808
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 6984 0 0 0 101981 33 0 0 25 0 1 0 481336738 30703616 6962 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7496 6962 603 41 0 7455 0
vsize: 29984
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 7071 0 0 0 102981 33 0 0 25 0 1 0 481336738 31113216 7049 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7596 7049 603 41 0 7555 0
vsize: 30384
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 7071 0 0 0 103981 33 0 0 25 0 1 0 481336738 31113216 7049 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7596 7049 603 41 0 7555 0
vsize: 30384
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 7115 0 0 0 104981 33 0 0 25 0 1 0 481336738 31244288 7093 4294967295 134512640 134672761 3221224544 3221223264 134565768 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7628 7093 603 41 0 7587 0
vsize: 30512
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 7115 0 0 0 105981 33 0 0 25 0 1 0 481336738 31244288 7093 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7628 7093 603 41 0 7587 0
vsize: 30512
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 7115 0 0 0 106982 33 0 0 25 0 1 0 481336738 31244288 7093 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7628 7093 603 41 0 7587 0
vsize: 30512
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 7271 0 0 0 107981 34 0 0 25 0 1 0 481336738 31948800 7249 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7800 7249 603 41 0 7759 0
vsize: 31200
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 7276 0 0 0 108981 34 0 0 25 0 1 0 481336738 31948800 7254 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7800 7254 603 41 0 7759 0
vsize: 31200
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 7297 0 0 0 109981 35 0 0 25 0 1 0 481336738 32088064 7275 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7834 7275 603 41 0 7793 0
vsize: 31336
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 7297 0 0 0 110981 35 0 0 25 0 1 0 481336738 32088064 7275 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7834 7275 603 41 0 7793 0
vsize: 31336
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 7297 0 0 0 111981 35 0 0 25 0 1 0 481336738 32088064 7275 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7834 7275 603 41 0 7793 0
vsize: 31336
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 7366 0 0 0 112981 35 0 0 25 0 1 0 481336738 32550912 7344 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7947 7344 603 41 0 7906 0
vsize: 31788
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 7375 0 0 0 113981 35 0 0 25 0 1 0 481336738 32550912 7353 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7947 7353 603 41 0 7906 0
vsize: 31788
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 7401 0 0 0 114981 35 0 0 25 0 1 0 481336738 32714752 7379 4294967295 134512640 134672761 3221224544 3221223712 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7987 7379 603 41 0 7946 0
vsize: 31948
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 7412 0 0 0 115981 35 0 0 25 0 1 0 481336738 32714752 7390 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7987 7390 603 41 0 7946 0
vsize: 31948
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 7412 0 0 0 116982 35 0 0 25 0 1 0 481336738 32714752 7390 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7987 7390 603 41 0 7946 0
vsize: 31948
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 7412 0 0 0 117982 35 0 0 25 0 1 0 481336738 32714752 7390 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7987 7390 603 41 0 7946 0
vsize: 31948
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 7412 0 0 0 118982 35 0 0 25 0 1 0 481336738 32714752 7390 4294967295 134512640 134672761 3221224544 3221223712 134561226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7987 7390 603 41 0 7946 0
vsize: 31948
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30584
Raw data (stat): 30584 (minisat+) R 30583 22612 22611 0 -1 0 7412 0 0 0 119982 35 0 0 25 0 1 0 481336738 32714752 7390 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7987 7390 603 41 0 7946 0
vsize: 31948
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 30584
Raw data (stat): 30584 (minisat+) Z 30583 22612 22611 0 -1 12 7414 0 0 0 119982 37 0 0 25 0 1 0 481336738 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): 1200.05
CPU time (s): 1200.2
CPU user time (s): 1199.82
CPU system time (s): 0.371943
CPU usage (%): 100.013
Max. virtual memory (Kb): 31948
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####