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-chnl35_36_pb.cnf.cr.opb
MD5SUMc779424bd1795a1e1adf6f4e7f38e307
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 37
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.075987
Number of variables2520
Total number of constraints142
Number of constraints which are clauses72
Number of constraints which are cardinality constraints (but not clauses)70
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint35
Maximum length of a constraint36

Trace number 5713 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-14 01:38:08 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4150 boxname=wulflinc31 idbench=14 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c779424bd1795a1e1adf6f4e7f38e307  /oldhome/oroussel/tmp/wulflinc31/normalized-chnl35_36_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc31/normalized-chnl35_36_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc31/normalized-chnl35_36_pb.cnf.cr.opb
IDLAUNCH: 4150
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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.153
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:        905968 kB
Buffers:         36016 kB
Cached:          54168 kB
SwapCached:        392 kB
Active:          51684 kB
Inactive:        41680 kB
HighTotal:      131008 kB
HighFree:        73164 kB
LowTotal:       903652 kB
LowFree:        832804 kB
SwapTotal:     2097892 kB
SwapFree:      2097452 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6832 kB
Slab:            29824 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:58:10 (client local time) WITH STATUS 0 IN 1200.19 SECONDS
stats: 4150 7 1200.19 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 142 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ........................................................................
c ---[  69]---> BDD-cost:   69
c ---[  68]---> BDD-cost:   69
c ---[  67]---> BDD-cost:   69
c ---[  66]---> BDD-cost:   69
c ---[  65]---> BDD-cost:   69
c ---[  64]---> BDD-cost:   69
c ---[  63]---> BDD-cost:   69
c ---[  62]---> BDD-cost:   69
c ---[  61]---> BDD-cost:   69
c ---[  60]---> BDD-cost:   69
c ---[  59]---> BDD-cost:   69
c ---[  58]---> BDD-cost:   69
c ---[  57]---> BDD-cost:   69
c ---[  56]---> BDD-cost:   69
c ---[  55]---> BDD-cost:   69
c ---[  54]---> BDD-cost:   69
c ---[  53]---> BDD-cost:   69
c ---[  52]---> BDD-cost:   69
c ---[  51]---> BDD-cost:   69
c ---[  50]---> BDD-cost:   69
c ---[  49]---> BDD-cost:   69
c ---[  48]---> BDD-cost:   69
c ---[  47]---> BDD-cost:   69
c ---[  46]---> BDD-cost:   69
c ---[  45]---> BDD-cost:   69
c ---[  44]---> BDD-cost:   69
c ---[  43]---> BDD-cost:   69
c ---[  42]---> BDD-cost:   69
c ---[  41]---> BDD-cost:   69
c ---[  40]---> BDD-cost:   69
c ---[  39]---> BDD-cost:   69
c ---[  38]---> BDD-cost:   69
c ---[  37]---> BDD-cost:   69
c ---[  36]---> BDD-cost:   69
c ---[  35]---> BDD-cost:   69
c ---[  34]---> BDD-cost:   69
c ---[  33]---> BDD-cost:   69
c ---[  32]---> BDD-cost:   69
c ---[  31]---> BDD-cost:   69
c ---[  30]---> BDD-cost:   69
c ---[  29]---> BDD-cost:   69
c ---[  28]---> BDD-cost:   69
c ---[  27]---> BDD-cost:   69
c ---[  26]---> BDD-cost:   69
c ---[  25]---> BDD-cost:   69
c ---[  24]---> BDD-cost:   69
c ---[  23]---> BDD-cost:   69
c ---[  22]---> BDD-cost:   69
c ---[  21]---> BDD-cost:   69
c ---[  20]---> BDD-cost:   69
c ---[  19]---> BDD-cost:   69
c ---[  18]---> BDD-cost:   69
c ---[  17]---> BDD-cost:   69
c ---[  16]---> BDD-cost:   69
c ---[  15]---> BDD-cost:   69
c ---[  14]---> BDD-cost:   69
c ---[  13]---> BDD-cost:   69
c ---[  12]---> BDD-cost:   69
c ---[  11]---> BDD-cost:   69
c ---[  10]---> BDD-cost:   69
c ---[   9]---> BDD-cost:   69
c ---[   8]---> BDD-cost:   69
c ---[   7]---> BDD-cost:   69
c ---[   6]---> BDD-cost:   69
c ---[   5]---> BDD-cost:   69
c ---[   4]---> BDD-cost:   69
c ---[   3]---> BDD-cost:   69
c ---[   2]---> BDD-cost:   69
c ---[   1]---> BDD-cost:   69
c ---[   0]---> BDD-cost:   69
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   12042    33670 |    4014       0        0     nan |  0.000 % |
c |       103 |   12042    33670 |    4415     103    13175   127.9 |  0.952 % |
c |       253 |   12042    33670 |    4856     253    36698   145.1 |  0.952 % |
c |       478 |   12042    33670 |    5342     478    73515   153.8 |  0.952 % |
c |       816 |   12042    33670 |    5876     816   124220   152.2 |  0.952 % |
c |      1323 |   12042    33670 |    6464    1323   237099   179.2 |  0.952 % |
c |      2083 |   12042    33670 |    7111    2083   367493   176.4 |  0.952 % |
c |      3225 |   12042    33670 |    7822    3225   569304   176.5 |  0.952 % |
c |      4933 |   12042    33670 |    8604    4933  1027352   208.3 |  0.952 % |
c |      7495 |   12042    33670 |    9464    7495  1634731   218.1 |  0.952 % |
c |     11342 |   12042    33670 |   10411   11342  3084149   271.9 |  0.952 % |
c |     17110 |   12042    33670 |   11452   11439  4029479   352.3 |  0.952 % |
c |     25760 |   12042    33670 |   12597   12884  4578033   355.3 |  0.952 % |
c |     38736 |   12042    33670 |   13857   11512  2855889   248.1 |  0.952 % |
c |     58197 |   12042    33670 |   15243   12764  3195585   250.4 |  0.952 % |
c |     87390 |   12042    33670 |   16767   15005  7262335   484.0 |  0.952 % |
c |    131179 |   12042    33670 |   18444   15052  4995126   331.9 |  0.952 % |
c |    196863 |   12042    33670 |   20288   15714  4807012   305.9 |  0.952 % |
c |    295389 |   12042    33670 |   22317   19548  5950976   304.4 |  0.952 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/54 28886
Raw data (stat): 28886 (runsolver) R 28885 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480677654 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0009 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 2939 0 0 0 992 6 0 0 25 0 1 0 480677654 13680640 2916 4294967295 134512640 134672761 3221224528 3221223680 134541817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3340 2916 603 41 0 3299 0
vsize: 13360
[startup+20.0014 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 4138 0 0 0 1988 8 0 0 25 0 1 0 480677654 18522112 4115 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4522 4115 603 41 0 4481 0
vsize: 18088
[startup+30.0017 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 5030 0 0 0 2986 10 0 0 25 0 1 0 480677654 22155264 5007 4294967295 134512640 134672761 3221224528 3221223632 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5409 5007 603 41 0 5368 0
vsize: 21636
[startup+40.0024 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 6172 0 0 0 3983 13 0 0 25 0 1 0 480677654 26882048 6149 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6563 6149 603 41 0 6522 0
vsize: 26252
[startup+50.0031 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 6172 0 0 0 4983 13 0 0 25 0 1 0 480677654 26882048 6149 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6563 6149 603 41 0 6522 0
vsize: 26252
[startup+60.0033 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 6172 0 0 0 5983 13 0 0 25 0 1 0 480677654 26882048 6149 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6563 6149 603 41 0 6522 0
vsize: 26252
[startup+70.0043 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 6173 0 0 0 6983 13 0 0 25 0 1 0 480677654 26882048 6150 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6563 6150 603 41 0 6522 0
vsize: 26252
[startup+80.0039 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 6173 0 0 0 7983 13 0 0 25 0 1 0 480677654 26882048 6150 4294967295 134512640 134672761 3221224528 3221223632 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6563 6150 603 41 0 6522 0
vsize: 26252
[startup+90.0041 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 6173 0 0 0 8984 13 0 0 25 0 1 0 480677654 26882048 6150 4294967295 134512640 134672761 3221224528 3221223632 134560379 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6563 6150 603 41 0 6522 0
vsize: 26252
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 6173 0 0 0 9984 13 0 0 25 0 1 0 480677654 26882048 6150 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6563 6150 603 41 0 6522 0
vsize: 26252
[startup+110.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 6310 0 0 0 10983 14 0 0 25 0 1 0 480677654 27422720 6287 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6695 6287 603 41 0 6654 0
vsize: 26780
[startup+120.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 6916 0 0 0 11982 16 0 0 25 0 1 0 480677654 29982720 6893 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7320 6893 603 41 0 7279 0
vsize: 29280
[startup+130.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 6916 0 0 0 12982 16 0 0 25 0 1 0 480677654 29982720 6893 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7320 6893 603 41 0 7279 0
vsize: 29280
[startup+140.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 6916 0 0 0 13982 16 0 0 25 0 1 0 480677654 29982720 6893 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7320 6893 603 41 0 7279 0
vsize: 29280
[startup+150.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 6916 0 0 0 14982 16 0 0 25 0 1 0 480677654 29982720 6893 4294967295 134512640 134672761 3221224528 3221223712 134559583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7320 6893 603 41 0 7279 0
vsize: 29280
[startup+160.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 6916 0 0 0 15982 16 0 0 25 0 1 0 480677654 29982720 6893 4294967295 134512640 134672761 3221224528 3221223712 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7320 6893 603 41 0 7279 0
vsize: 29280
[startup+170.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 7507 0 0 0 16980 18 0 0 25 0 1 0 480677654 32440320 7484 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7920 7484 603 41 0 7879 0
vsize: 31680
[startup+180.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 8093 0 0 0 17979 20 0 0 25 0 1 0 480677654 34902016 8070 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8521 8070 603 41 0 8480 0
vsize: 34084
[startup+190.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 8193 0 0 0 18979 20 0 0 25 0 1 0 480677654 35307520 8170 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8620 8170 603 41 0 8579 0
vsize: 34480
[startup+200.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 8194 0 0 0 19979 20 0 0 25 0 1 0 480677654 35307520 8171 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8620 8171 603 41 0 8579 0
vsize: 34480
[startup+210.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 8795 0 0 0 20977 22 0 0 25 0 1 0 480677654 37892096 8772 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9251 8772 603 41 0 9210 0
vsize: 37004
[startup+220.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 9548 0 0 0 21976 24 0 0 25 0 1 0 480677654 40882176 9525 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9981 9525 603 41 0 9940 0
vsize: 39924
[startup+230.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 10368 0 0 0 22974 26 0 0 25 0 1 0 480677654 44277760 10345 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10810 10345 603 41 0 10769 0
vsize: 43240
[startup+240.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 10734 0 0 0 23973 27 0 0 25 0 1 0 480677654 45764608 10711 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11173 10711 603 41 0 11132 0
vsize: 44692
[startup+250.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 10734 0 0 0 24973 27 0 0 25 0 1 0 480677654 45764608 10711 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11173 10711 603 41 0 11132 0
vsize: 44692
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 10735 0 0 0 25973 27 0 0 25 0 1 0 480677654 45764608 10712 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11173 10712 603 41 0 11132 0
vsize: 44692
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 10735 0 0 0 26972 27 0 0 25 0 1 0 480677654 45764608 10712 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11173 10712 603 41 0 11132 0
vsize: 44692
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11368 0 0 0 27971 29 0 0 25 0 1 0 480677654 48463872 11345 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11345 603 41 0 11791 0
vsize: 47328
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11369 0 0 0 28971 29 0 0 25 0 1 0 480677654 48463872 11346 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11346 603 41 0 11791 0
vsize: 47328
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11372 0 0 0 29971 29 0 0 25 0 1 0 480677654 48463872 11349 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11349 603 41 0 11791 0
vsize: 47328
[startup+310.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11372 0 0 0 30971 29 0 0 25 0 1 0 480677654 48463872 11349 4294967295 134512640 134672761 3221224528 3221223632 134559916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11349 603 41 0 11791 0
vsize: 47328
[startup+320.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11373 0 0 0 31971 29 0 0 25 0 1 0 480677654 48463872 11350 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11350 603 41 0 11791 0
vsize: 47328
[startup+330.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 32971 29 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 33972 29 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223632 134559908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+350.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 34972 29 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223632 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+360.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 35972 29 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 36972 29 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 37972 29 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223712 134559170 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+390.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 38972 29 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+400.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 39973 29 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223632 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+410.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 40973 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+420.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 41972 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223632 134560237 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+430.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 42973 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+440.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 43973 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+450.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 44973 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+460.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 45974 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+470.026 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 46974 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+480.026 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 47974 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+490.027 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 48974 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+500.027 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 49974 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+510.028 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 50974 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+520.028 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 51974 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+530.027 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 52974 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+540.028 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 53975 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+550.027 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 54975 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+560.028 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 55975 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+570.028 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 56975 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+580.028 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 57975 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+590.029 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 58975 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+600.029 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 59976 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+610.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 60976 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223632 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+620.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 61976 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223632 134559985 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+630.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 62976 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+640.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 63976 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+650.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 64977 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+660.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 65977 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223632 134560322 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+670.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 66977 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+680.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 67977 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+690.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 68977 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223664 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+700.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 69977 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+710.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 70978 30 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+720.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 71978 31 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+730.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 72977 31 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223632 134554926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+740.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 73977 31 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223712 134559616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+750.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11374 0 0 0 74977 31 0 0 25 0 1 0 480677654 48463872 11351 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11351 603 41 0 11791 0
vsize: 47328
[startup+760.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11385 0 0 0 75977 31 0 0 25 0 1 0 480677654 48463872 11362 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11362 603 41 0 11791 0
vsize: 47328
[startup+770.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11385 0 0 0 76977 31 0 0 25 0 1 0 480677654 48463872 11362 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11362 603 41 0 11791 0
vsize: 47328
[startup+780.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11385 0 0 0 77978 31 0 0 25 0 1 0 480677654 48463872 11362 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11362 603 41 0 11791 0
vsize: 47328
[startup+790.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11385 0 0 0 78978 31 0 0 25 0 1 0 480677654 48463872 11362 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11832 11362 603 41 0 11791 0
vsize: 47328
[startup+800.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11785 0 0 0 79976 33 0 0 25 0 1 0 480677654 50102272 11762 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12232 11762 603 41 0 12191 0
vsize: 48928
[startup+810.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11785 0 0 0 80977 33 0 0 25 0 1 0 480677654 50102272 11762 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12232 11762 603 41 0 12191 0
vsize: 48928
[startup+820.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11785 0 0 0 81977 33 0 0 25 0 1 0 480677654 50102272 11762 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12232 11762 603 41 0 12191 0
vsize: 48928
[startup+830.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11785 0 0 0 82977 33 0 0 25 0 1 0 480677654 50102272 11762 4294967295 134512640 134672761 3221224528 3221223632 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12232 11762 603 41 0 12191 0
vsize: 48928
[startup+840.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 11785 0 0 0 83977 33 0 0 25 0 1 0 480677654 50102272 11762 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12232 11762 603 41 0 12191 0
vsize: 48928
[startup+850.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 12429 0 0 0 84975 35 0 0 25 0 1 0 480677654 52785152 12406 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12887 12406 603 41 0 12846 0
vsize: 51548
[startup+860.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 12810 0 0 0 85974 36 0 0 25 0 1 0 480677654 54403072 12787 4294967295 134512640 134672761 3221224528 3221223632 134559927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13282 12787 603 41 0 13241 0
vsize: 53128
[startup+870.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 12811 0 0 0 86975 36 0 0 25 0 1 0 480677654 54403072 12788 4294967295 134512640 134672761 3221224528 3221223632 134560057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13282 12788 603 41 0 13241 0
vsize: 53128
[startup+880.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 12811 0 0 0 87975 36 0 0 25 0 1 0 480677654 54403072 12788 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13282 12788 603 41 0 13241 0
vsize: 53128
[startup+890.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 12811 0 0 0 88975 36 0 0 25 0 1 0 480677654 54403072 12788 4294967295 134512640 134672761 3221224528 3221223632 134560022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13282 12788 603 41 0 13241 0
vsize: 53128
[startup+900.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 12811 0 0 0 89975 36 0 0 25 0 1 0 480677654 54403072 12788 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13282 12788 603 41 0 13241 0
vsize: 53128
[startup+910.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 13527 0 0 0 90973 38 0 0 25 0 1 0 480677654 57409536 13504 4294967295 134512640 134672761 3221224528 3221223528 1075353072 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14016 13504 603 41 0 13975 0
vsize: 56064
[startup+920.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 14286 0 0 0 91971 41 0 0 25 0 1 0 480677654 60506112 14263 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14772 14263 603 41 0 14731 0
vsize: 59088
[startup+930.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 14288 0 0 0 92971 41 0 0 25 0 1 0 480677654 60506112 14265 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14772 14265 603 41 0 14731 0
vsize: 59088
[startup+940.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 14289 0 0 0 93971 41 0 0 25 0 1 0 480677654 60506112 14266 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14772 14266 603 41 0 14731 0
vsize: 59088
[startup+950.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 14289 0 0 0 94971 41 0 0 25 0 1 0 480677654 60506112 14266 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14772 14266 603 41 0 14731 0
vsize: 59088
[startup+960.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 14290 0 0 0 95971 41 0 0 25 0 1 0 480677654 60506112 14267 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14772 14267 603 41 0 14731 0
vsize: 59088
[startup+970.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 14290 0 0 0 96971 41 0 0 25 0 1 0 480677654 60506112 14267 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14772 14267 603 41 0 14731 0
vsize: 59088
[startup+980.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 14291 0 0 0 97972 41 0 0 25 0 1 0 480677654 60506112 14268 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14772 14268 603 41 0 14731 0
vsize: 59088
[startup+990.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 14493 0 0 0 98971 41 0 0 25 0 1 0 480677654 61317120 14470 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14970 14470 603 41 0 14929 0
vsize: 59880
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 14815 0 0 0 99970 42 0 0 25 0 1 0 480677654 62685184 14792 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15304 14792 603 41 0 15263 0
vsize: 61216
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 15056 0 0 0 100970 43 0 0 25 0 1 0 480677654 63647744 15033 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15539 15033 603 41 0 15498 0
vsize: 62156
[startup+1020.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 15318 0 0 0 101970 43 0 0 25 0 1 0 480677654 64921600 15295 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15850 15295 603 41 0 15809 0
vsize: 63400
[startup+1030.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 15635 0 0 0 102969 44 0 0 25 0 1 0 480677654 66318336 15612 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16191 15612 603 41 0 16150 0
vsize: 64764
[startup+1040.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 15899 0 0 0 103968 45 0 0 25 0 1 0 480677654 67399680 15876 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16455 15876 603 41 0 16414 0
vsize: 65820
[startup+1050.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 16208 0 0 0 104968 46 0 0 25 0 1 0 480677654 68612096 16185 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16751 16185 603 41 0 16710 0
vsize: 67004
[startup+1060.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 16208 0 0 0 105968 46 0 0 25 0 1 0 480677654 68612096 16185 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16751 16185 603 41 0 16710 0
vsize: 67004
[startup+1070.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 16208 0 0 0 106968 46 0 0 25 0 1 0 480677654 68612096 16185 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16751 16185 603 41 0 16710 0
vsize: 67004
[startup+1080.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 16208 0 0 0 107968 46 0 0 25 0 1 0 480677654 68612096 16185 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16751 16185 603 41 0 16710 0
vsize: 67004
[startup+1090.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 16208 0 0 0 108968 46 0 0 25 0 1 0 480677654 68612096 16185 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16751 16185 603 41 0 16710 0
vsize: 67004
[startup+1100.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 16208 0 0 0 109968 46 0 0 25 0 1 0 480677654 68612096 16185 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16751 16185 603 41 0 16710 0
vsize: 67004
[startup+1110.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 16208 0 0 0 110969 46 0 0 25 0 1 0 480677654 68612096 16185 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16751 16185 603 41 0 16710 0
vsize: 67004
[startup+1120.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 16208 0 0 0 111969 46 0 0 25 0 1 0 480677654 68612096 16185 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16751 16185 603 41 0 16710 0
vsize: 67004
[startup+1130.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 16208 0 0 0 112969 46 0 0 25 0 1 0 480677654 68612096 16185 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16751 16185 603 41 0 16710 0
vsize: 67004
[startup+1140.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 16208 0 0 0 113969 46 0 0 25 0 1 0 480677654 68612096 16185 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16751 16185 603 41 0 16710 0
vsize: 67004
[startup+1150.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 16208 0 0 0 114969 46 0 0 25 0 1 0 480677654 68612096 16185 4294967295 134512640 134672761 3221224528 3221223712 134559622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16751 16185 603 41 0 16710 0
vsize: 67004
[startup+1160.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 16208 0 0 0 115969 47 0 0 25 0 1 0 480677654 68612096 16185 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16751 16185 603 41 0 16710 0
vsize: 67004
[startup+1170.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 16208 0 0 0 116968 47 0 0 25 0 1 0 480677654 68612096 16185 4294967295 134512640 134672761 3221224528 3221223632 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16751 16185 603 41 0 16710 0
vsize: 67004
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 16208 0 0 0 117968 47 0 0 25 0 1 0 480677654 68612096 16185 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16751 16185 603 41 0 16710 0
vsize: 67004
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 16208 0 0 0 118968 47 0 0 25 0 1 0 480677654 68612096 16185 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16751 16185 603 41 0 16710 0
vsize: 67004
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 28886
Raw data (stat): 28886 (minisat+) R 28885 23176 23175 0 -1 0 16208 0 0 0 119968 47 0 0 25 0 1 0 480677654 68612096 16185 4294967295 134512640 134672761 3221224528 3221223712 134558941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16751 16185 603 41 0 16710 0
vsize: 67004
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 28886
Raw data (stat): 28886 (minisat+) Z 28885 23176 23175 0 -1 12 16210 0 0 0 119968 50 0 0 25 0 1 0 480677654 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.08
CPU time (s): 1200.19
CPU user time (s): 1199.69
CPU system time (s): 0.503923
CPU usage (%): 100.009
Max. virtual memory (Kb): 67004
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####