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_25_pb.cnf.cr.opb
MD5SUM6c328ef6f9d8d5a179eec9bf3550b7fd
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 26
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.027995
Number of variables1000
Total number of constraints90
Number of constraints which are clauses50
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 constraint25

Trace number 4745 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-13 20:09:46 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=77 boxname=wulflinc13 idbench=9 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  6c328ef6f9d8d5a179eec9bf3550b7fd  /oldhome/oroussel/tmp/wulflinc13/normalized-chnl20_25_pb.cnf.cr.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc13/normalized-chnl20_25_pb.cnf.cr.opb
IDLAUNCH: 77
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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:        924696 kB
Buffers:         33924 kB
Cached:          56532 kB
SwapCached:        392 kB
Active:          48816 kB
Inactive:        44896 kB
HighTotal:      131008 kB
HighFree:        70644 kB
LowTotal:       903652 kB
LowFree:        854052 kB
SwapTotal:     2097136 kB
SwapFree:      2096744 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10736 kB
Committed_AS:    63472 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 20:29:48 (client local time) WITH STATUS 0 IN 1200.14 SECONDS
stats: 77 7 1200.14 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 90 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................
c ---[  39]---> BDD-cost:   47
c ---[  38]---> BDD-cost:   47
c ---[  37]---> BDD-cost:   47
c ---[  36]---> BDD-cost:   47
c ---[  35]---> BDD-cost:   47
c ---[  34]---> BDD-cost:   47
c ---[  33]---> BDD-cost:   47
c ---[  32]---> BDD-cost:   47
c ---[  31]---> BDD-cost:   47
c ---[  30]---> BDD-cost:   47
c ---[  29]---> BDD-cost:   47
c ---[  28]---> BDD-cost:   47
c ---[  27]---> BDD-cost:   47
c ---[  26]---> BDD-cost:   47
c ---[  25]---> BDD-cost:   47
c ---[  24]---> BDD-cost:   47
c ---[  23]---> BDD-cost:   47
c ---[  22]---> BDD-cost:   47
c ---[  21]---> BDD-cost:   47
c ---[  20]---> BDD-cost:   47
c ---[  19]---> BDD-cost:   47
c ---[  18]---> BDD-cost:   47
c ---[  17]---> BDD-cost:   47
c ---[  16]---> BDD-cost:   47
c ---[  15]---> BDD-cost:   47
c ---[  14]---> BDD-cost:   47
c ---[  13]---> BDD-cost:   47
c ---[  12]---> BDD-cost:   47
c ---[  11]---> BDD-cost:   47
c ---[  10]---> BDD-cost:   47
c ---[   9]---> BDD-cost:   47
c ---[   8]---> BDD-cost:   47
c ---[   7]---> BDD-cost:   47
c ---[   6]---> BDD-cost:   47
c ---[   5]---> BDD-cost:   47
c ---[   4]---> BDD-cost:   47
c ---[   3]---> BDD-cost:   47
c ---[   2]---> BDD-cost:   47
c ---[   1]---> BDD-cost:   47
c ---[   0]---> BDD-cost:   47
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    4690    13080 |    1563       0        0     nan |  0.000 % |
c |       100 |    4690    13080 |    1719     100     6902    69.0 |  1.389 % |
c |       251 |    4690    13080 |    1891     251    20396    81.3 |  1.389 % |
c |       478 |    4690    13080 |    2080     478    46287    96.8 |  1.389 % |
c |       821 |    4690    13080 |    2288     821    81704    99.5 |  1.389 % |
c |      1327 |    4690    13080 |    2517    1327   146172   110.2 |  1.389 % |
c |      2087 |    4690    13080 |    2768    2087   249403   119.5 |  1.389 % |
c |      3227 |    4690    13080 |    3045    3227   373256   115.7 |  1.389 % |
c |      4936 |    4690    13080 |    3350    3323   444218   133.7 |  1.389 % |
c |      7498 |    4690    13080 |    3685    3680   506490   137.6 |  1.389 % |
c |     11342 |    4690    13080 |    4054    2775   386580   139.3 |  1.389 % |
c |     17109 |    4690    13080 |    4459    3425   492300   143.7 |  1.389 % |
c |     25762 |    4690    13080 |    4905    3891   549706   141.3 |  1.389 % |
c |     38739 |    4690    13080 |    5395    5144  1059065   205.9 |  1.389 % |
c |     58201 |    4690    13080 |    5935    3757   878997   234.0 |  1.389 % |
c |     87393 |    4690    13080 |    6529    3337   680756   204.0 |  1.389 % |
c |    131182 |    4690    13080 |    7181    4075   849512   208.5 |  1.389 % |
c |    196867 |    4690    13080 |    7900    6042   961736   159.2 |  1.389 % |
c |    295397 |    4690    13080 |    8690    8012  1389547   173.4 |  1.389 % |
c |    443187 |    4690    13080 |    9559    4859  1092280   224.8 |  1.389 % |
c |    664873 |    4690    13080 |   10515    6850  1659355   242.2 |  1.389 % |
#### 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.88 2/54 874
Raw data (stat): 874 (runsolver) R 873 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420502304 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0013 s]
Raw data (loadavg): 0.87 0.94 0.88 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 1357 0 0 0 995 4 0 0 25 0 1 0 420502304 7139328 1335 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1743 1335 603 41 0 1702 0
vsize: 6972
[startup+20.0019 s]
Raw data (loadavg): 0.89 0.94 0.88 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 1568 0 0 0 1994 4 0 0 25 0 1 0 420502304 7954432 1546 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1942 1546 603 41 0 1901 0
vsize: 7768
[startup+30.0021 s]
Raw data (loadavg): 0.90 0.94 0.88 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 1750 0 0 0 2993 5 0 0 25 0 1 0 420502304 8761344 1728 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2139 1728 603 41 0 2098 0
vsize: 8556
[startup+40.0022 s]
Raw data (loadavg): 0.92 0.94 0.88 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 2315 0 0 0 3991 7 0 0 25 0 1 0 420502304 11051008 2293 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2698 2293 603 41 0 2657 0
vsize: 10792
[startup+50.0028 s]
Raw data (loadavg): 0.93 0.94 0.88 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 2429 0 0 0 4990 8 0 0 25 0 1 0 420502304 11591680 2407 4294967295 134512640 134672761 3221224624 3221223728 134560412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2830 2407 603 41 0 2789 0
vsize: 11320
[startup+60.0031 s]
Raw data (loadavg): 0.94 0.95 0.88 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 2429 0 0 0 5990 8 0 0 25 0 1 0 420502304 11575296 2407 4294967295 134512640 134672761 3221224624 3221223792 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2826 2407 603 41 0 2785 0
vsize: 11304
[startup+70.0031 s]
Raw data (loadavg): 0.95 0.95 0.88 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 2586 0 0 0 6989 9 0 0 25 0 1 0 420502304 12251136 2564 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2991 2564 603 41 0 2950 0
vsize: 11964
[startup+80.0038 s]
Raw data (loadavg): 0.96 0.95 0.88 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 2587 0 0 0 7989 9 0 0 25 0 1 0 420502304 12251136 2565 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2991 2565 603 41 0 2950 0
vsize: 11964
[startup+90.004 s]
Raw data (loadavg): 0.96 0.95 0.89 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 2597 0 0 0 8988 9 0 0 25 0 1 0 420502304 12251136 2575 4294967295 134512640 134672761 3221224624 3221223800 134559639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2991 2575 603 41 0 2950 0
vsize: 11964
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.89 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 2710 0 0 0 9988 10 0 0 25 0 1 0 420502304 12656640 2688 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3090 2688 603 41 0 3049 0
vsize: 12360
[startup+110.005 s]
Raw data (loadavg): 0.97 0.95 0.89 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 2758 0 0 0 10987 10 0 0 25 0 1 0 420502304 12918784 2736 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3154 2736 603 41 0 3113 0
vsize: 12616
[startup+120.005 s]
Raw data (loadavg): 0.98 0.95 0.89 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 2802 0 0 0 11987 11 0 0 25 0 1 0 420502304 13053952 2780 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3187 2780 603 41 0 3146 0
vsize: 12748
[startup+130.006 s]
Raw data (loadavg): 0.98 0.95 0.89 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3041 0 0 0 12986 12 0 0 25 0 1 0 420502304 13996032 3019 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3417 3019 603 41 0 3376 0
vsize: 13668
[startup+140.007 s]
Raw data (loadavg): 0.98 0.95 0.89 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3041 0 0 0 13986 12 0 0 25 0 1 0 420502304 13996032 3019 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3417 3019 603 41 0 3376 0
vsize: 13668
[startup+150.007 s]
Raw data (loadavg): 0.98 0.95 0.89 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3041 0 0 0 14985 12 0 0 25 0 1 0 420502304 13996032 3019 4294967295 134512640 134672761 3221224624 3221223792 134559068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3417 3019 603 41 0 3376 0
vsize: 13668
[startup+160.007 s]
Raw data (loadavg): 0.99 0.96 0.89 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3041 0 0 0 15985 12 0 0 25 0 1 0 420502304 13996032 3019 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3417 3019 603 41 0 3376 0
vsize: 13668
[startup+170.008 s]
Raw data (loadavg): 0.99 0.96 0.89 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3041 0 0 0 16985 12 0 0 25 0 1 0 420502304 13996032 3019 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3417 3019 603 41 0 3376 0
vsize: 13668
[startup+180.008 s]
Raw data (loadavg): 0.99 0.96 0.89 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3041 0 0 0 17984 13 0 0 25 0 1 0 420502304 13996032 3019 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3417 3019 603 41 0 3376 0
vsize: 13668
[startup+190.009 s]
Raw data (loadavg): 0.99 0.96 0.89 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3042 0 0 0 18984 13 0 0 25 0 1 0 420502304 13996032 3020 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3417 3020 603 41 0 3376 0
vsize: 13668
[startup+200.009 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3042 0 0 0 19984 13 0 0 25 0 1 0 420502304 13967360 3014 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3410 3014 603 41 0 3369 0
vsize: 13640
[startup+210.009 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3042 0 0 0 20983 14 0 0 25 0 1 0 420502304 13967360 3014 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3410 3014 603 41 0 3369 0
vsize: 13640
[startup+220.01 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3042 0 0 0 21983 14 0 0 25 0 1 0 420502304 13967360 3014 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3410 3014 603 41 0 3369 0
vsize: 13640
[startup+230.011 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3042 0 0 0 22983 14 0 0 25 0 1 0 420502304 13967360 3014 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3410 3014 603 41 0 3369 0
vsize: 13640
[startup+240.011 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3043 0 0 0 23982 15 0 0 25 0 1 0 420502304 13967360 3015 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3410 3015 603 41 0 3369 0
vsize: 13640
[startup+250.011 s]
Raw data (loadavg): 0.99 0.96 0.90 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3043 0 0 0 24982 15 0 0 25 0 1 0 420502304 13967360 3015 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3410 3015 603 41 0 3369 0
vsize: 13640
[startup+260.013 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3216 0 0 0 25981 16 0 0 25 0 1 0 420502304 14807040 3188 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3615 3188 603 41 0 3574 0
vsize: 14460
[startup+270.013 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3233 0 0 0 26980 16 0 0 25 0 1 0 420502304 14807040 3205 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3615 3205 603 41 0 3574 0
vsize: 14460
[startup+280.014 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3237 0 0 0 27980 16 0 0 25 0 1 0 420502304 14807040 3209 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3615 3209 603 41 0 3574 0
vsize: 14460
[startup+290.015 s]
Raw data (loadavg): 0.99 0.97 0.90 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3246 0 0 0 28980 17 0 0 25 0 1 0 420502304 14954496 3218 4294967295 134512640 134672761 3221224624 3221223640 1075352737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3651 3218 603 41 0 3610 0
vsize: 14604
[startup+300.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3273 0 0 0 29980 17 0 0 25 0 1 0 420502304 15118336 3245 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3691 3245 603 41 0 3650 0
vsize: 14764
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3622 0 0 0 30979 18 0 0 25 0 1 0 420502304 16470016 3594 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4021 3594 603 41 0 3980 0
vsize: 16084
[startup+320.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3742 0 0 0 31978 18 0 0 25 0 1 0 420502304 17010688 3714 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4153 3714 603 41 0 4112 0
vsize: 16612
[startup+330.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3743 0 0 0 32978 19 0 0 25 0 1 0 420502304 17010688 3715 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4153 3715 603 41 0 4112 0
vsize: 16612
[startup+340.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3743 0 0 0 33977 19 0 0 25 0 1 0 420502304 17010688 3715 4294967295 134512640 134672761 3221224624 3221223808 134558851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4153 3715 603 41 0 4112 0
vsize: 16612
[startup+350.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3743 0 0 0 34977 19 0 0 25 0 1 0 420502304 17010688 3715 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4153 3715 603 41 0 4112 0
vsize: 16612
[startup+360.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3743 0 0 0 35976 20 0 0 25 0 1 0 420502304 17010688 3715 4294967295 134512640 134672761 3221224624 3221223808 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4153 3715 603 41 0 4112 0
vsize: 16612
[startup+370.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3743 0 0 0 36976 20 0 0 25 0 1 0 420502304 17010688 3715 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4153 3715 603 41 0 4112 0
vsize: 16612
[startup+380.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3744 0 0 0 37976 21 0 0 25 0 1 0 420502304 17010688 3716 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4153 3716 603 41 0 4112 0
vsize: 16612
[startup+390.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3744 0 0 0 38975 21 0 0 25 0 1 0 420502304 17010688 3716 4294967295 134512640 134672761 3221224624 3221223728 134560379 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4153 3716 603 41 0 4112 0
vsize: 16612
[startup+400.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3745 0 0 0 39975 21 0 0 25 0 1 0 420502304 17010688 3717 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4153 3717 603 41 0 4112 0
vsize: 16612
[startup+410.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 3804 0 0 0 40975 21 0 0 25 0 1 0 420502304 17293312 3776 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4222 3776 603 41 0 4181 0
vsize: 16888
[startup+420.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4015 0 0 0 41975 22 0 0 25 0 1 0 420502304 18116608 3987 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4423 3987 603 41 0 4382 0
vsize: 17692
[startup+430.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4260 0 0 0 42974 22 0 0 25 0 1 0 420502304 19054592 4232 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4652 4232 603 41 0 4611 0
vsize: 18608
[startup+440.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4355 0 0 0 43974 23 0 0 25 0 1 0 420502304 19488768 4327 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4758 4327 603 41 0 4717 0
vsize: 19032
[startup+450.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4382 0 0 0 44974 23 0 0 25 0 1 0 420502304 19623936 4354 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4791 4354 603 41 0 4750 0
vsize: 19164
[startup+460.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4455 0 0 0 45974 23 0 0 25 0 1 0 420502304 19894272 4427 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4857 4427 603 41 0 4816 0
vsize: 19428
[startup+470.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4484 0 0 0 46974 23 0 0 25 0 1 0 420502304 20029440 4456 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4890 4456 603 41 0 4849 0
vsize: 19560
[startup+480.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4484 0 0 0 47975 23 0 0 25 0 1 0 420502304 20029440 4456 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4890 4456 603 41 0 4849 0
vsize: 19560
[startup+490.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4484 0 0 0 48975 23 0 0 25 0 1 0 420502304 20029440 4456 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4890 4456 603 41 0 4849 0
vsize: 19560
[startup+500.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4484 0 0 0 49975 23 0 0 25 0 1 0 420502304 20029440 4456 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4890 4456 603 41 0 4849 0
vsize: 19560
[startup+510.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4500 0 0 0 50975 23 0 0 25 0 1 0 420502304 20164608 4472 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4923 4472 603 41 0 4882 0
vsize: 19692
[startup+520.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4678 0 0 0 51975 24 0 0 25 0 1 0 420502304 20840448 4650 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5088 4650 603 41 0 5047 0
vsize: 20352
[startup+530.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4678 0 0 0 52975 24 0 0 25 0 1 0 420502304 20840448 4650 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5088 4650 603 41 0 5047 0
vsize: 20352
[startup+540.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4758 0 0 0 53975 24 0 0 25 0 1 0 420502304 21110784 4730 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5154 4730 603 41 0 5113 0
vsize: 20616
[startup+550.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4758 0 0 0 54975 24 0 0 25 0 1 0 420502304 21110784 4730 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5154 4730 603 41 0 5113 0
vsize: 20616
[startup+560.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4758 0 0 0 55976 24 0 0 25 0 1 0 420502304 21110784 4730 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5154 4730 603 41 0 5113 0
vsize: 20616
[startup+570.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4758 0 0 0 56976 24 0 0 25 0 1 0 420502304 21110784 4730 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5154 4730 603 41 0 5113 0
vsize: 20616
[startup+580.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4758 0 0 0 57976 24 0 0 25 0 1 0 420502304 21110784 4730 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5154 4730 603 41 0 5113 0
vsize: 20616
[startup+590.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4758 0 0 0 58976 24 0 0 25 0 1 0 420502304 21110784 4730 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5154 4730 603 41 0 5113 0
vsize: 20616
[startup+600.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4758 0 0 0 59976 24 0 0 25 0 1 0 420502304 21110784 4730 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5154 4730 603 41 0 5113 0
vsize: 20616
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4758 0 0 0 60976 24 0 0 25 0 1 0 420502304 21110784 4730 4294967295 134512640 134672761 3221224624 3221223520 134565852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5154 4730 603 41 0 5113 0
vsize: 20616
[startup+620.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4758 0 0 0 61977 24 0 0 25 0 1 0 420502304 21110784 4730 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5154 4730 603 41 0 5113 0
vsize: 20616
[startup+630.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4758 0 0 0 62977 24 0 0 25 0 1 0 420502304 21110784 4730 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5154 4730 603 41 0 5113 0
vsize: 20616
[startup+640.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4758 0 0 0 63977 24 0 0 25 0 1 0 420502304 21110784 4730 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5154 4730 603 41 0 5113 0
vsize: 20616
[startup+650.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4758 0 0 0 64977 24 0 0 25 0 1 0 420502304 21110784 4730 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5154 4730 603 41 0 5113 0
vsize: 20616
[startup+660.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4758 0 0 0 65977 24 0 0 25 0 1 0 420502304 21110784 4730 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5154 4730 603 41 0 5113 0
vsize: 20616
[startup+670.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4758 0 0 0 66977 24 0 0 25 0 1 0 420502304 21110784 4730 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5154 4730 603 41 0 5113 0
vsize: 20616
[startup+680.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4758 0 0 0 67977 24 0 0 25 0 1 0 420502304 21110784 4730 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5154 4730 603 41 0 5113 0
vsize: 20616
[startup+690.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4758 0 0 0 68977 24 0 0 25 0 1 0 420502304 21110784 4730 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5154 4730 603 41 0 5113 0
vsize: 20616
[startup+700.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4772 0 0 0 69977 24 0 0 25 0 1 0 420502304 21245952 4744 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5187 4744 603 41 0 5146 0
vsize: 20748
[startup+710.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4782 0 0 0 70977 24 0 0 25 0 1 0 420502304 21245952 4754 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5187 4754 603 41 0 5146 0
vsize: 20748
[startup+720.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4782 0 0 0 71977 24 0 0 25 0 1 0 420502304 21245952 4754 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5187 4754 603 41 0 5146 0
vsize: 20748
[startup+730.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4801 0 0 0 72978 24 0 0 25 0 1 0 420502304 21381120 4773 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5220 4773 603 41 0 5179 0
vsize: 20880
[startup+740.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4892 0 0 0 73978 24 0 0 25 0 1 0 420502304 21786624 4864 4294967295 134512640 134672761 3221224624 3221223760 134560628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5319 4864 603 41 0 5278 0
vsize: 21276
[startup+750.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4897 0 0 0 74978 24 0 0 25 0 1 0 420502304 21786624 4869 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5319 4869 603 41 0 5278 0
vsize: 21276
[startup+760.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4943 0 0 0 75978 24 0 0 25 0 1 0 420502304 22102016 4915 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5396 4915 603 41 0 5355 0
vsize: 21584
[startup+770.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4943 0 0 0 76978 24 0 0 25 0 1 0 420502304 22102016 4915 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5396 4915 603 41 0 5355 0
vsize: 21584
[startup+780.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4943 0 0 0 77979 24 0 0 25 0 1 0 420502304 22102016 4915 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5396 4915 603 41 0 5355 0
vsize: 21584
[startup+790.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4943 0 0 0 78979 24 0 0 25 0 1 0 420502304 22102016 4915 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5396 4915 603 41 0 5355 0
vsize: 21584
[startup+800.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4943 0 0 0 79979 24 0 0 25 0 1 0 420502304 22102016 4915 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5396 4915 603 41 0 5355 0
vsize: 21584
[startup+810.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4943 0 0 0 80979 24 0 0 25 0 1 0 420502304 22102016 4915 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5396 4915 603 41 0 5355 0
vsize: 21584
[startup+820.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4943 0 0 0 81980 24 0 0 25 0 1 0 420502304 22102016 4915 4294967295 134512640 134672761 3221224624 3221223792 134564648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5396 4915 603 41 0 5355 0
vsize: 21584
[startup+830.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4943 0 0 0 82980 24 0 0 25 0 1 0 420502304 22102016 4915 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5396 4915 603 41 0 5355 0
vsize: 21584
[startup+840.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4943 0 0 0 83980 24 0 0 25 0 1 0 420502304 22102016 4915 4294967295 134512640 134672761 3221224624 3221223808 134558937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5396 4915 603 41 0 5355 0
vsize: 21584
[startup+850.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4966 0 0 0 84980 24 0 0 25 0 1 0 420502304 22102016 4938 4294967295 134512640 134672761 3221224624 3221223728 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5396 4938 603 41 0 5355 0
vsize: 21584
[startup+860.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4966 0 0 0 85980 24 0 0 25 0 1 0 420502304 22102016 4938 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5396 4938 603 41 0 5355 0
vsize: 21584
[startup+870.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4967 0 0 0 86981 24 0 0 25 0 1 0 420502304 22102016 4939 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5396 4939 603 41 0 5355 0
vsize: 21584
[startup+880.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4967 0 0 0 87981 24 0 0 25 0 1 0 420502304 22102016 4939 4294967295 134512640 134672761 3221224624 3221223808 134559522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5396 4939 603 41 0 5355 0
vsize: 21584
[startup+890.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4967 0 0 0 88981 24 0 0 25 0 1 0 420502304 22102016 4939 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5396 4939 603 41 0 5355 0
vsize: 21584
[startup+900.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4967 0 0 0 89981 24 0 0 25 0 1 0 420502304 22102016 4939 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5396 4939 603 41 0 5355 0
vsize: 21584
[startup+910.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4967 0 0 0 90981 24 0 0 25 0 1 0 420502304 22102016 4939 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5396 4939 603 41 0 5355 0
vsize: 21584
[startup+920.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 4967 0 0 0 91982 24 0 0 25 0 1 0 420502304 22102016 4939 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5396 4939 603 41 0 5355 0
vsize: 21584
[startup+930.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 5308 0 0 0 92981 26 0 0 25 0 1 0 420502304 23638016 5280 4294967295 134512640 134672761 3221224624 3221223728 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5771 5280 603 41 0 5730 0
vsize: 23084
[startup+940.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 5309 0 0 0 93981 26 0 0 25 0 1 0 420502304 23638016 5281 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5771 5281 603 41 0 5730 0
vsize: 23084
[startup+950.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 5309 0 0 0 94981 26 0 0 25 0 1 0 420502304 23638016 5281 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5771 5281 603 41 0 5730 0
vsize: 23084
[startup+960.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 5309 0 0 0 95981 26 0 0 25 0 1 0 420502304 23638016 5281 4294967295 134512640 134672761 3221224624 3221222444 134566339 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5771 5281 603 41 0 5730 0
vsize: 23084
[startup+970.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 5312 0 0 0 96981 26 0 0 25 0 1 0 420502304 23638016 5284 4294967295 134512640 134672761 3221224624 3221223728 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5771 5284 603 41 0 5730 0
vsize: 23084
[startup+980.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 5313 0 0 0 97982 26 0 0 25 0 1 0 420502304 23638016 5285 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5771 5285 603 41 0 5730 0
vsize: 23084
[startup+990.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 5363 0 0 0 98982 26 0 0 25 0 1 0 420502304 23773184 5335 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5804 5335 603 41 0 5763 0
vsize: 23216
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 5427 0 0 0 99982 26 0 0 25 0 1 0 420502304 24043520 5399 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5870 5399 603 41 0 5829 0
vsize: 23480
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 5427 0 0 0 100982 26 0 0 25 0 1 0 420502304 24043520 5399 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5870 5399 603 41 0 5829 0
vsize: 23480
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 5427 0 0 0 101982 26 0 0 25 0 1 0 420502304 24043520 5399 4294967295 134512640 134672761 3221224624 3221223792 134561009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5870 5399 603 41 0 5829 0
vsize: 23480
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 5427 0 0 0 102982 26 0 0 25 0 1 0 420502304 24043520 5399 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5870 5399 603 41 0 5829 0
vsize: 23480
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 5570 0 0 0 103981 27 0 0 25 0 1 0 420502304 24584192 5542 4294967295 134512640 134672761 3221224624 3221223760 134565048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6002 5542 603 41 0 5961 0
vsize: 24008
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 5570 0 0 0 104981 27 0 0 25 0 1 0 420502304 24584192 5542 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6002 5542 603 41 0 5961 0
vsize: 24008
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 5570 0 0 0 105981 27 0 0 25 0 1 0 420502304 24584192 5542 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6002 5542 603 41 0 5961 0
vsize: 24008
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 5570 0 0 0 106981 27 0 0 25 0 1 0 420502304 24584192 5542 4294967295 134512640 134672761 3221224624 3221223808 134558629 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6002 5542 603 41 0 5961 0
vsize: 24008
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 5570 0 0 0 107982 27 0 0 25 0 1 0 420502304 24444928 5510 4294967295 134512640 134672761 3221224624 3221223624 1075349746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5968 5510 603 41 0 5927 0
vsize: 23872
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 5570 0 0 0 108982 27 0 0 25 0 1 0 420502304 24444928 5510 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5968 5510 603 41 0 5927 0
vsize: 23872
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 5570 0 0 0 109982 27 0 0 25 0 1 0 420502304 24444928 5510 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5968 5510 603 41 0 5927 0
vsize: 23872
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 5570 0 0 0 110982 27 0 0 25 0 1 0 420502304 24444928 5510 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5968 5510 603 41 0 5927 0
vsize: 23872
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 5570 0 0 0 111982 27 0 0 25 0 1 0 420502304 24444928 5510 4294967295 134512640 134672761 3221224624 3221223788 134541851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5968 5510 603 41 0 5927 0
vsize: 23872
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 5824 0 0 0 112982 28 0 0 25 0 1 0 420502304 25526272 5764 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6232 5764 603 41 0 6191 0
vsize: 24928
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 5824 0 0 0 113982 28 0 0 25 0 1 0 420502304 25526272 5764 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6232 5764 603 41 0 6191 0
vsize: 24928
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 5971 0 0 0 114982 28 0 0 25 0 1 0 420502304 26206208 5911 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6398 5911 603 41 0 6357 0
vsize: 25592
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 6023 0 0 0 115982 28 0 0 25 0 1 0 420502304 26341376 5963 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6431 5963 603 41 0 6390 0
vsize: 25724
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 6213 0 0 0 116982 29 0 0 25 0 1 0 420502304 27152384 6153 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6629 6153 603 41 0 6588 0
vsize: 26516
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 6224 0 0 0 117982 29 0 0 25 0 1 0 420502304 27152384 6164 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6629 6164 603 41 0 6588 0
vsize: 26516
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 6224 0 0 0 118983 29 0 0 25 0 1 0 420502304 27152384 6164 4294967295 134512640 134672761 3221224624 3221223808 134558914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6629 6164 603 41 0 6588 0
vsize: 26516
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 874
Raw data (stat): 874 (minisat+) R 873 30701 30700 0 -1 0 6224 0 0 0 119983 29 0 0 25 0 1 0 420502304 27152384 6164 4294967295 134512640 134672761 3221224624 3221223728 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6629 6164 603 41 0 6588 0
vsize: 26516
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 874
Raw data (stat): 874 (minisat+) Z 873 30701 30700 0 -1 12 6226 0 0 0 119983 30 0 0 25 0 1 0 420502304 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.14
CPU user time (s): 1199.83
CPU system time (s): 0.302953
CPU usage (%): 100.007
Max. virtual memory (Kb): 26516
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####