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-chnl30_31_pb.cnf.cr.opb
MD5SUM79bafd08ddd684356ab9abc8fabf88a7
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 32
Number of bits of the biggest sum of numbers6
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.05399
Number of variables1860
Total number of constraints122
Number of constraints which are clauses62
Number of constraints which are cardinality constraints (but not clauses)60
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint30
Maximum length of a constraint31

Trace number 5710 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-04-14 01:37:31 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4147 boxname=wulflinc29 idbench=11 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  79bafd08ddd684356ab9abc8fabf88a7  /oldhome/oroussel/tmp/wulflinc29/normalized-chnl30_31_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc29/normalized-chnl30_31_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc29/normalized-chnl30_31_pb.cnf.cr.opb
IDLAUNCH: 4147
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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.020
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        821752 kB
Buffers:         36628 kB
Cached:         138732 kB
SwapCached:         12 kB
Active:          53480 kB
Inactive:       124748 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        821500 kB
SwapTotal:     2097892 kB
SwapFree:      2097880 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            28932 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:57:33 (client local time) WITH STATUS 0 IN 1200.21 SECONDS
stats: 4147 7 1200.21 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 122 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..............................................................
c ---[  59]---> BDD-cost:   59
c ---[  58]---> BDD-cost:   59
c ---[  57]---> BDD-cost:   59
c ---[  56]---> BDD-cost:   59
c ---[  55]---> BDD-cost:   59
c ---[  54]---> BDD-cost:   59
c ---[  53]---> BDD-cost:   59
c ---[  52]---> BDD-cost:   59
c ---[  51]---> BDD-cost:   59
c ---[  50]---> BDD-cost:   59
c ---[  49]---> BDD-cost:   59
c ---[  48]---> BDD-cost:   59
c ---[  47]---> BDD-cost:   59
c ---[  46]---> BDD-cost:   59
c ---[  45]---> BDD-cost:   59
c ---[  44]---> BDD-cost:   59
c ---[  43]---> BDD-cost:   59
c ---[  42]---> BDD-cost:   59
c ---[  41]---> BDD-cost:   59
c ---[  40]---> BDD-cost:   59
c ---[  39]---> BDD-cost:   59
c ---[  38]---> BDD-cost:   59
c ---[  37]---> BDD-cost:   59
c ---[  36]---> BDD-cost:   59
c ---[  35]---> BDD-cost:   59
c ---[  34]---> BDD-cost:   59
c ---[  33]---> BDD-cost:   59
c ---[  32]---> BDD-cost:   59
c ---[  31]---> BDD-cost:   59
c ---[  30]---> BDD-cost:   59
c ---[  29]---> BDD-cost:   59
c ---[  28]---> BDD-cost:   59
c ---[  27]---> BDD-cost:   59
c ---[  26]---> BDD-cost:   59
c ---[  25]---> BDD-cost:   59
c ---[  24]---> BDD-cost:   59
c ---[  23]---> BDD-cost:   59
c ---[  22]---> BDD-cost:   59
c ---[  21]---> BDD-cost:   59
c ---[  20]---> BDD-cost:   59
c ---[  19]---> BDD-cost:   59
c ---[  18]---> BDD-cost:   59
c ---[  17]---> BDD-cost:   59
c ---[  16]---> BDD-cost:   59
c ---[  15]---> BDD-cost:   59
c ---[  14]---> BDD-cost:   59
c ---[  13]---> BDD-cost:   59
c ---[  12]---> BDD-cost:   59
c ---[  11]---> BDD-cost:   59
c ---[  10]---> BDD-cost:   59
c ---[   9]---> BDD-cost:   59
c ---[   8]---> BDD-cost:   59
c ---[   7]---> BDD-cost:   59
c ---[   6]---> BDD-cost:   59
c ---[   5]---> BDD-cost:   59
c ---[   4]---> BDD-cost:   59
c ---[   3]---> BDD-cost:   59
c ---[   2]---> BDD-cost:   59
c ---[   1]---> BDD-cost:   59
c ---[   0]---> BDD-cost:   59
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    8822    24660 |    2940       0        0     nan |  0.000 % |
c |       103 |    8822    24660 |    3234     103    11125   108.0 |  1.111 % |
c |       253 |    8822    24660 |    3557     253    29108   115.1 |  1.111 % |
c |       481 |    8822    24660 |    3913     481    60948   126.7 |  1.111 % |
c |       818 |    8822    24660 |    4304     818   108840   133.1 |  1.111 % |
c |      1324 |    8822    24660 |    4734    1324   188898   142.7 |  1.111 % |
c |      2083 |    8822    24660 |    5208    2083   314214   150.8 |  1.111 % |
c |      3222 |    8822    24660 |    5729    3222   492986   153.0 |  1.111 % |
c |      4931 |    8822    24660 |    6302    4931   860748   174.6 |  1.111 % |
c |      7493 |    8822    24660 |    6932    4279   864687   202.1 |  1.111 % |
c |     11338 |    8822    24660 |    7625    8124  1810763   222.9 |  1.111 % |
c |     17104 |    8822    24660 |    8388    4954  1245773   251.5 |  1.111 % |
c |     25753 |    8822    24660 |    9226    8309  2172756   261.5 |  1.111 % |
c |     38729 |    8822    24660 |   10149   10285  3566365   346.8 |  1.111 % |
c |     58191 |    8822    24660 |   11164    6370  1674827   262.9 |  1.111 % |
c |     87385 |    8822    24660 |   12281    8866  2685374   302.9 |  1.111 % |
c |    131174 |    8822    24660 |   13509   10011  3644159   364.0 |  1.111 % |
c |    196858 |    8822    24660 |   14860   16739  4896164   292.5 |  1.111 % |
c |    295385 |    8822    24660 |   16346   15539  3921113   252.3 |  1.111 % |
#### 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.91 0.97 0.91 2/54 360
Raw data (stat): 360 (runsolver) R 359 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480684077 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99958 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 2559 0 0 0 993 5 0 0 25 0 1 0 480684077 12095488 2537 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2953 2537 603 41 0 2912 0
vsize: 11812
[startup+20.0009 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 3415 0 0 0 1990 7 0 0 25 0 1 0 480684077 15663104 3393 4294967295 134512640 134672761 3221224528 3221223632 134560279 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3824 3393 603 41 0 3783 0
vsize: 15296
[startup+30.0016 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 3713 0 0 0 2989 8 0 0 25 0 1 0 480684077 16875520 3691 4294967295 134512640 134672761 3221224528 3221223712 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4120 3691 603 41 0 4079 0
vsize: 16480
[startup+40.001 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 3969 0 0 0 3988 9 0 0 25 0 1 0 480684077 17956864 3947 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4384 3947 603 41 0 4343 0
vsize: 17536
[startup+50.0022 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 4531 0 0 0 4987 10 0 0 25 0 1 0 480684077 20250624 4509 4294967295 134512640 134672761 3221224528 3221223696 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4944 4509 603 41 0 4903 0
vsize: 19776
[startup+60.002 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 4824 0 0 0 5986 11 0 0 25 0 1 0 480684077 21463040 4802 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5240 4802 603 41 0 5199 0
vsize: 20960
[startup+70.0024 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 4991 0 0 0 6986 12 0 0 25 0 1 0 480684077 22138880 4969 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5405 4969 603 41 0 5364 0
vsize: 21620
[startup+80.0035 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 4991 0 0 0 7986 12 0 0 25 0 1 0 480684077 22138880 4969 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5405 4969 603 41 0 5364 0
vsize: 21620
[startup+90.0033 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 4991 0 0 0 8986 13 0 0 25 0 1 0 480684077 22138880 4969 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5405 4969 603 41 0 5364 0
vsize: 21620
[startup+100.004 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 4991 0 0 0 9985 13 0 0 25 0 1 0 480684077 22130688 4969 4294967295 134512640 134672761 3221224528 3221223632 134560051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5403 4969 603 41 0 5362 0
vsize: 21612
[startup+110.005 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 5063 0 0 0 10985 13 0 0 25 0 1 0 480684077 22401024 5041 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5469 5041 603 41 0 5428 0
vsize: 21876
[startup+120.005 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 5174 0 0 0 11984 14 0 0 25 0 1 0 480684077 22806528 5152 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5568 5152 603 41 0 5527 0
vsize: 22272
[startup+130.005 s]
Raw data (loadavg): 1.02 0.99 0.92 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 5326 0 0 0 12984 14 0 0 25 0 1 0 480684077 23486464 5304 4294967295 134512640 134672761 3221224528 3221223632 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5734 5304 603 41 0 5693 0
vsize: 22936
[startup+140.005 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 5337 0 0 0 13984 14 0 0 25 0 1 0 480684077 23633920 5315 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5770 5315 603 41 0 5729 0
vsize: 23080
[startup+150.006 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 5543 0 0 0 14984 15 0 0 25 0 1 0 480684077 24514560 5521 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5985 5521 603 41 0 5944 0
vsize: 23940
[startup+160.006 s]
Raw data (loadavg): 1.01 0.99 0.92 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 5617 0 0 0 15984 16 0 0 25 0 1 0 480684077 24784896 5595 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6051 5595 603 41 0 6010 0
vsize: 24204
[startup+170.006 s]
Raw data (loadavg): 1.08 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 6219 0 0 0 16982 17 0 0 25 0 1 0 480684077 27213824 6197 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6644 6197 603 41 0 6603 0
vsize: 26576
[startup+180.007 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 6430 0 0 0 17982 18 0 0 25 0 1 0 480684077 28160000 6408 4294967295 134512640 134672761 3221224528 3221223632 134559908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6875 6408 603 41 0 6834 0
vsize: 27500
[startup+190.007 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 7605 0 0 0 18980 20 0 0 25 0 1 0 480684077 32894976 7583 4294967295 134512640 134672761 3221224528 3221223632 134559974 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8031 7583 603 41 0 7990 0
vsize: 32124
[startup+200.007 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 8061 0 0 0 19979 21 0 0 25 0 1 0 480684077 34787328 8039 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8493 8039 603 41 0 8452 0
vsize: 33972
[startup+210.007 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 8062 0 0 0 20979 21 0 0 25 0 1 0 480684077 34787328 8040 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8493 8040 603 41 0 8452 0
vsize: 33972
[startup+220.008 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 8917 0 0 0 21978 23 0 0 25 0 1 0 480684077 38334464 8895 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9359 8895 603 41 0 9318 0
vsize: 37436
[startup+230.009 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 8917 0 0 0 22978 23 0 0 25 0 1 0 480684077 38334464 8895 4294967295 134512640 134672761 3221224528 3221223696 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9359 8895 603 41 0 9318 0
vsize: 37436
[startup+240.009 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 8917 0 0 0 23977 23 0 0 25 0 1 0 480684077 38334464 8895 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9359 8895 603 41 0 9318 0
vsize: 37436
[startup+250.01 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 8917 0 0 0 24978 23 0 0 25 0 1 0 480684077 38334464 8895 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9359 8895 603 41 0 9318 0
vsize: 37436
[startup+260.009 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 8917 0 0 0 25978 23 0 0 25 0 1 0 480684077 38334464 8895 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9359 8895 603 41 0 9318 0
vsize: 37436
[startup+270.009 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 8917 0 0 0 26978 23 0 0 25 0 1 0 480684077 38334464 8895 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9359 8895 603 41 0 9318 0
vsize: 37436
[startup+280.01 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 8917 0 0 0 27978 23 0 0 25 0 1 0 480684077 38334464 8895 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9359 8895 603 41 0 9318 0
vsize: 37436
[startup+290.009 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 8918 0 0 0 28978 23 0 0 25 0 1 0 480684077 38334464 8896 4294967295 134512640 134672761 3221224528 3221223664 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+300.009 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 8918 0 0 0 29978 23 0 0 25 0 1 0 480684077 38334464 8896 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+310.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 8918 0 0 0 30978 23 0 0 25 0 1 0 480684077 38334464 8896 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+320.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 8918 0 0 0 31979 23 0 0 25 0 1 0 480684077 38334464 8896 4294967295 134512640 134672761 3221224528 3221223696 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+330.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 8918 0 0 0 32979 23 0 0 25 0 1 0 480684077 38334464 8896 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+340.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 8918 0 0 0 33979 23 0 0 25 0 1 0 480684077 38334464 8896 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+350.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 8918 0 0 0 34979 23 0 0 25 0 1 0 480684077 38334464 8896 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+360.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 8918 0 0 0 35979 23 0 0 25 0 1 0 480684077 38334464 8896 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+370.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 8918 0 0 0 36980 23 0 0 25 0 1 0 480684077 38334464 8896 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+380.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 8918 0 0 0 37980 23 0 0 25 0 1 0 480684077 38334464 8896 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+390.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 8918 0 0 0 38980 23 0 0 25 0 1 0 480684077 38334464 8896 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+400.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 8918 0 0 0 39980 23 0 0 25 0 1 0 480684077 38334464 8896 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+410.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 8918 0 0 0 40980 23 0 0 25 0 1 0 480684077 38334464 8896 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+420.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 8918 0 0 0 41981 23 0 0 25 0 1 0 480684077 38334464 8896 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+430.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 8918 0 0 0 42981 23 0 0 25 0 1 0 480684077 38334464 8896 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+440.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 8918 0 0 0 43981 23 0 0 25 0 1 0 480684077 38334464 8896 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+450.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 8918 0 0 0 44981 23 0 0 25 0 1 0 480684077 38334464 8896 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+460.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 8918 0 0 0 45981 23 0 0 25 0 1 0 480684077 38334464 8896 4294967295 134512640 134672761 3221224528 3221223632 134554636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+470.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 8918 0 0 0 46981 23 0 0 25 0 1 0 480684077 38334464 8896 4294967295 134512640 134672761 3221224528 3221223696 134560867 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+480.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 9302 0 0 0 47980 25 0 0 25 0 1 0 480684077 39952384 9280 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9754 9280 603 41 0 9713 0
vsize: 39016
[startup+490.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 9302 0 0 0 48980 25 0 0 25 0 1 0 480684077 39952384 9280 4294967295 134512640 134672761 3221224528 3221223696 134560813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9754 9280 603 41 0 9713 0
vsize: 39016
[startup+500.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 9302 0 0 0 49980 25 0 0 25 0 1 0 480684077 39952384 9280 4294967295 134512640 134672761 3221224528 3221223712 134559388 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9754 9280 603 41 0 9713 0
vsize: 39016
[startup+510.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 10165 0 0 0 50978 27 0 0 25 0 1 0 480684077 43470848 10143 4294967295 134512640 134672761 3221224528 3221223528 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10613 10143 603 41 0 10572 0
vsize: 42452
[startup+520.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 10670 0 0 0 51978 28 0 0 25 0 1 0 480684077 45633536 10648 4294967295 134512640 134672761 3221224528 3221223696 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11141 10648 603 41 0 11100 0
vsize: 44564
[startup+530.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 10670 0 0 0 52978 28 0 0 25 0 1 0 480684077 45633536 10648 4294967295 134512640 134672761 3221224528 3221223696 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11141 10648 603 41 0 11100 0
vsize: 44564
[startup+540.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 11255 0 0 0 53977 29 0 0 25 0 1 0 480684077 47943680 11233 4294967295 134512640 134672761 3221224528 3221223696 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11705 11233 603 41 0 11664 0
vsize: 46820
[startup+550.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 11440 0 0 0 54976 30 0 0 25 0 1 0 480684077 48754688 11418 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11903 11418 603 41 0 11862 0
vsize: 47612
[startup+560.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 11440 0 0 0 55976 30 0 0 25 0 1 0 480684077 48754688 11418 4294967295 134512640 134672761 3221224528 3221223700 134559669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11903 11418 603 41 0 11862 0
vsize: 47612
[startup+570.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 11440 0 0 0 56977 30 0 0 25 0 1 0 480684077 48754688 11418 4294967295 134512640 134672761 3221224528 3221223696 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11903 11418 603 41 0 11862 0
vsize: 47612
[startup+580.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 11440 0 0 0 57977 30 0 0 25 0 1 0 480684077 48754688 11418 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11903 11418 603 41 0 11862 0
vsize: 47612
[startup+590.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 11503 0 0 0 58977 30 0 0 25 0 1 0 480684077 49025024 11481 4294967295 134512640 134672761 3221224528 3221223712 134558943 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11969 11481 603 41 0 11928 0
vsize: 47876
[startup+600.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 11503 0 0 0 59977 30 0 0 25 0 1 0 480684077 49025024 11481 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11969 11481 603 41 0 11928 0
vsize: 47876
[startup+610.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 11503 0 0 0 60977 30 0 0 25 0 1 0 480684077 49025024 11481 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11969 11481 603 41 0 11928 0
vsize: 47876
[startup+620.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 11503 0 0 0 61977 30 0 0 25 0 1 0 480684077 49025024 11481 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11969 11481 603 41 0 11928 0
vsize: 47876
[startup+630.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 11503 0 0 0 62978 30 0 0 25 0 1 0 480684077 49025024 11481 4294967295 134512640 134672761 3221224528 3221223632 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11969 11481 603 41 0 11928 0
vsize: 47876
[startup+640.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 11503 0 0 0 63978 30 0 0 25 0 1 0 480684077 49025024 11481 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11969 11481 603 41 0 11928 0
vsize: 47876
[startup+650.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 11503 0 0 0 64978 30 0 0 25 0 1 0 480684077 49025024 11481 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11969 11481 603 41 0 11928 0
vsize: 47876
[startup+660.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 11503 0 0 0 65978 30 0 0 25 0 1 0 480684077 49025024 11481 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11969 11481 603 41 0 11928 0
vsize: 47876
[startup+670.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 11590 0 0 0 66978 30 0 0 25 0 1 0 480684077 49430528 11568 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12068 11568 603 41 0 12027 0
vsize: 48272
[startup+680.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 11590 0 0 0 67978 30 0 0 25 0 1 0 480684077 49430528 11568 4294967295 134512640 134672761 3221224528 3221223632 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12068 11568 603 41 0 12027 0
vsize: 48272
[startup+690.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 11590 0 0 0 68979 30 0 0 25 0 1 0 480684077 49430528 11568 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12068 11568 603 41 0 12027 0
vsize: 48272
[startup+700.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 11845 0 0 0 69978 31 0 0 25 0 1 0 480684077 50372608 11823 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12298 11823 603 41 0 12257 0
vsize: 49192
[startup+710.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 11845 0 0 0 70978 31 0 0 25 0 1 0 480684077 50372608 11823 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12298 11823 603 41 0 12257 0
vsize: 49192
[startup+720.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 11845 0 0 0 71978 31 0 0 25 0 1 0 480684077 50372608 11823 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12298 11823 603 41 0 12257 0
vsize: 49192
[startup+730.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 11845 0 0 0 72978 31 0 0 25 0 1 0 480684077 50372608 11823 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12298 11823 603 41 0 12257 0
vsize: 49192
[startup+740.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 11845 0 0 0 73979 31 0 0 25 0 1 0 480684077 50372608 11823 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12298 11823 603 41 0 12257 0
vsize: 49192
[startup+750.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 11928 0 0 0 74979 31 0 0 25 0 1 0 480684077 50778112 11906 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12397 11906 603 41 0 12356 0
vsize: 49588
[startup+760.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 11928 0 0 0 75979 31 0 0 25 0 1 0 480684077 50778112 11906 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12397 11906 603 41 0 12356 0
vsize: 49588
[startup+770.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 11928 0 0 0 76979 31 0 0 25 0 1 0 480684077 50778112 11906 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12397 11906 603 41 0 12356 0
vsize: 49588
[startup+780.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 11956 0 0 0 77979 31 0 0 25 0 1 0 480684077 50946048 11934 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12438 11934 603 41 0 12397 0
vsize: 49752
[startup+790.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12244 0 0 0 78979 32 0 0 25 0 1 0 480684077 52162560 12222 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+800.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12244 0 0 0 79979 32 0 0 25 0 1 0 480684077 52162560 12222 4294967295 134512640 134672761 3221224528 3221223632 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+810.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12244 0 0 0 80979 32 0 0 25 0 1 0 480684077 52162560 12222 4294967295 134512640 134672761 3221224528 3221223712 134559622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+820.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12244 0 0 0 81979 32 0 0 25 0 1 0 480684077 52162560 12222 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+830.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12244 0 0 0 82979 32 0 0 25 0 1 0 480684077 52162560 12222 4294967295 134512640 134672761 3221224528 3221223664 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+840.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12244 0 0 0 83979 32 0 0 25 0 1 0 480684077 52162560 12222 4294967295 134512640 134672761 3221224528 3221223712 134558831 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+850.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12244 0 0 0 84979 32 0 0 25 0 1 0 480684077 52162560 12222 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+860.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12244 0 0 0 85979 32 0 0 25 0 1 0 480684077 52162560 12222 4294967295 134512640 134672761 3221224528 3221223632 134560276 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+870.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12244 0 0 0 86979 32 0 0 25 0 1 0 480684077 52162560 12222 4294967295 134512640 134672761 3221224528 3221223680 134565213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+880.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12244 0 0 0 87979 32 0 0 25 0 1 0 480684077 52162560 12222 4294967295 134512640 134672761 3221224528 3221223632 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+890.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12244 0 0 0 88980 32 0 0 25 0 1 0 480684077 52162560 12222 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+900.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12244 0 0 0 89980 32 0 0 25 0 1 0 480684077 52162560 12222 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+910.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12244 0 0 0 90980 32 0 0 25 0 1 0 480684077 52162560 12222 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+920.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12244 0 0 0 91980 32 0 0 25 0 1 0 480684077 52162560 12222 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+930.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12244 0 0 0 92980 32 0 0 25 0 1 0 480684077 52162560 12222 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+940.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12244 0 0 0 93981 32 0 0 25 0 1 0 480684077 52162560 12222 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+950.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12244 0 0 0 94981 32 0 0 25 0 1 0 480684077 52162560 12222 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+960.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12244 0 0 0 95981 32 0 0 25 0 1 0 480684077 52162560 12222 4294967295 134512640 134672761 3221224528 3221223632 134559916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+970.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12244 0 0 0 96981 32 0 0 25 0 1 0 480684077 52162560 12222 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+980.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12244 0 0 0 97982 32 0 0 25 0 1 0 480684077 52162560 12222 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+990.025 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12244 0 0 0 98982 32 0 0 25 0 1 0 480684077 52162560 12222 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+1000.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12371 0 0 0 99982 32 0 0 25 0 1 0 480684077 52703232 12349 4294967295 134512640 134672761 3221224528 3221223632 134560194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12867 12349 603 41 0 12826 0
vsize: 51468
[startup+1010.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12371 0 0 0 100982 32 0 0 25 0 1 0 480684077 52703232 12349 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12867 12349 603 41 0 12826 0
vsize: 51468
[startup+1020.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12371 0 0 0 101982 32 0 0 25 0 1 0 480684077 52703232 12349 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12867 12349 603 41 0 12826 0
vsize: 51468
[startup+1030.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12371 0 0 0 102982 32 0 0 25 0 1 0 480684077 52690944 12349 4294967295 134512640 134672761 3221224528 3221223632 134560396 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12864 12349 603 41 0 12823 0
vsize: 51456
[startup+1040.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12371 0 0 0 103983 32 0 0 25 0 1 0 480684077 52690944 12349 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12864 12349 603 41 0 12823 0
vsize: 51456
[startup+1050.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12371 0 0 0 104983 32 0 0 25 0 1 0 480684077 52162560 12248 4294967295 134512640 134672761 3221224528 3221223712 134559564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12248 603 41 0 12694 0
vsize: 50940
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12371 0 0 0 105983 32 0 0 25 0 1 0 480684077 52162560 12248 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12248 603 41 0 12694 0
vsize: 50940
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12371 0 0 0 106983 32 0 0 25 0 1 0 480684077 52162560 12248 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12248 603 41 0 12694 0
vsize: 50940
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12371 0 0 0 107983 32 0 0 25 0 1 0 480684077 52162560 12248 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12248 603 41 0 12694 0
vsize: 50940
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12371 0 0 0 108984 32 0 0 25 0 1 0 480684077 52162560 12248 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12248 603 41 0 12694 0
vsize: 50940
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12371 0 0 0 109984 32 0 0 25 0 1 0 480684077 52162560 12248 4294967295 134512640 134672761 3221224528 3221223696 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12248 603 41 0 12694 0
vsize: 50940
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12371 0 0 0 110984 32 0 0 25 0 1 0 480684077 52162560 12248 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12248 603 41 0 12694 0
vsize: 50940
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12834 0 0 0 111983 34 0 0 25 0 1 0 480684077 54173696 12711 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13226 12711 603 41 0 13185 0
vsize: 52904
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12834 0 0 0 112983 34 0 0 25 0 1 0 480684077 54173696 12711 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13226 12711 603 41 0 13185 0
vsize: 52904
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12834 0 0 0 113983 34 0 0 25 0 1 0 480684077 54173696 12711 4294967295 134512640 134672761 3221224528 3221223632 134560477 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13226 12711 603 41 0 13185 0
vsize: 52904
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12834 0 0 0 114983 34 0 0 25 0 1 0 480684077 54173696 12711 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13226 12711 603 41 0 13185 0
vsize: 52904
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12834 0 0 0 115983 34 0 0 25 0 1 0 480684077 54173696 12711 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13226 12711 603 41 0 13185 0
vsize: 52904
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 12835 0 0 0 116984 34 0 0 25 0 1 0 480684077 54173696 12712 4294967295 134512640 134672761 3221224528 3221223696 134560785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13226 12712 603 41 0 13185 0
vsize: 52904
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 13255 0 0 0 117983 35 0 0 25 0 1 0 480684077 55820288 13132 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13628 13132 603 41 0 13587 0
vsize: 54512
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 13620 0 0 0 118982 36 0 0 25 0 1 0 480684077 57442304 13497 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14024 13497 603 41 0 13983 0
vsize: 56096
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 360
Raw data (stat): 360 (minisat+) R 359 27222 27221 0 -1 0 13620 0 0 0 119982 36 0 0 25 0 1 0 480684077 57442304 13497 4294967295 134512640 134672761 3221224528 3221223696 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14024 13497 603 41 0 13983 0
vsize: 56096
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 360
Raw data (stat): 360 (minisat+) Z 359 27222 27221 0 -1 12 13622 0 0 0 119982 38 0 0 25 0 1 0 480684077 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.06
CPU time (s): 1200.21
CPU user time (s): 1199.83
CPU system time (s): 0.387941
CPU usage (%): 100.013
Max. virtual memory (Kb): 56096
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####