PB'05 competition: run trace

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

Name	normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl30_31_pb.cnf.cr.opb
MD5SUM	79bafd08ddd684356ab9abc8fabf88a7
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	NO
(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 numbers	6
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.05399
Number of variables	1860
Total number of constraints	122
Number of constraints which are clauses	62
Number of constraints which are cardinality constraints (but not clauses)	60
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	30
Maximum length of a constraint	31
Trace number 4747

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        894060 kB
Buffers:         33288 kB
Cached:          73620 kB
SwapCached:         56 kB
Active:          44260 kB
Inactive:        65680 kB
HighTotal:      131008 kB
HighFree:        53312 kB
LowTotal:       903652 kB
LowFree:        840748 kB
SwapTotal:     2097892 kB
SwapFree:      2097836 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7028 kB
Slab:            25020 kB
Committed_AS:    63708 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 20:30:05 (client local time) WITH STATUS 0 IN 1200.21 SECONDS
stats: 95 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.85 0.95 0.88 2/55 25564
Raw data (stat): 25564 (runsolver) R 25563 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478716967 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 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.0004 s]
Raw data (loadavg): 0.87 0.95 0.89 2/55 25564
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 2520 0 0 0 992 7 0 0 25 0 1 0 478716967 11960320 2498 4294967295 134512640 134672761 3221224624 3221223728 134560504 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2920 2498 603 41 0 2879 0
vsize: 11680
[startup+20.0009 s]
Raw data (loadavg): 0.89 0.96 0.89 2/55 25564
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 3415 0 0 0 1989 9 0 0 25 0 1 0 478716967 15663104 3393 4294967295 134512640 134672761 3221224624 3221223792 134561014 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.0014 s]
Raw data (loadavg): 0.91 0.96 0.89 2/55 25564
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 3713 0 0 0 2988 10 0 0 25 0 1 0 478716967 16875520 3691 4294967295 134512640 134672761 3221224624 3221223792 134561218 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.0015 s]
Raw data (loadavg): 0.92 0.96 0.89 2/55 25564
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 3902 0 0 0 3987 11 0 0 25 0 1 0 478716967 17686528 3880 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4318 3880 603 41 0 4277 0
vsize: 17272
[startup+50.0013 s]
Raw data (loadavg): 0.93 0.96 0.89 2/55 25564
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 4531 0 0 0 4986 12 0 0 25 0 1 0 478716967 20250624 4509 4294967295 134512640 134672761 3221224624 3221223792 134560983 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.0008 s]
Raw data (loadavg): 0.94 0.96 0.89 2/55 25564
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 4824 0 0 0 5985 13 0 0 25 0 1 0 478716967 21463040 4802 4294967295 134512640 134672761 3221224624 3221223792 134561188 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.0009 s]
Raw data (loadavg): 0.95 0.96 0.89 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 4991 0 0 0 6984 14 0 0 25 0 1 0 478716967 22138880 4969 4294967295 134512640 134672761 3221224624 3221223120 134565829 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.0014 s]
Raw data (loadavg): 0.96 0.96 0.89 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 4991 0 0 0 7985 14 0 0 25 0 1 0 478716967 22138880 4969 4294967295 134512640 134672761 3221224624 3221223808 134559616 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.0015 s]
Raw data (loadavg): 0.96 0.96 0.89 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 4991 0 0 0 8985 14 0 0 25 0 1 0 478716967 22138880 4969 4294967295 134512640 134672761 3221224624 3221223808 134559594 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.002 s]
Raw data (loadavg): 0.97 0.96 0.89 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 4991 0 0 0 9985 14 0 0 25 0 1 0 478716967 22130688 4969 4294967295 134512640 134672761 3221224624 3221223728 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5403 4969 603 41 0 5362 0
vsize: 21612
[startup+110.002 s]
Raw data (loadavg): 0.97 0.96 0.90 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 4991 0 0 0 10984 14 0 0 25 0 1 0 478716967 22130688 4969 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5403 4969 603 41 0 5362 0
vsize: 21612
[startup+120.002 s]
Raw data (loadavg): 0.98 0.97 0.90 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 5174 0 0 0 11984 15 0 0 25 0 1 0 478716967 22806528 5152 4294967295 134512640 134672761 3221224624 3221223792 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5568 5152 603 41 0 5527 0
vsize: 22272
[startup+130.003 s]
Raw data (loadavg): 0.98 0.97 0.90 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 5326 0 0 0 12984 15 0 0 25 0 1 0 478716967 23486464 5304 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5734 5304 603 41 0 5693 0
vsize: 22936
[startup+140.002 s]
Raw data (loadavg): 0.98 0.97 0.90 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 5337 0 0 0 13984 15 0 0 25 0 1 0 478716967 23633920 5315 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5770 5315 603 41 0 5729 0
vsize: 23080
[startup+150.002 s]
Raw data (loadavg): 0.98 0.97 0.90 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 5543 0 0 0 14984 16 0 0 25 0 1 0 478716967 24514560 5521 4294967295 134512640 134672761 3221224624 3221223792 134561118 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.003 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 5617 0 0 0 15983 16 0 0 25 0 1 0 478716967 24784896 5595 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6051 5595 603 41 0 6010 0
vsize: 24204
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 6168 0 0 0 16982 17 0 0 25 0 1 0 478716967 27078656 6146 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6611 6146 603 41 0 6570 0
vsize: 26444
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 6430 0 0 0 17981 18 0 0 25 0 1 0 478716967 28160000 6408 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6875 6408 603 41 0 6834 0
vsize: 27500
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 7602 0 0 0 18980 20 0 0 25 0 1 0 478716967 32894976 7580 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8031 7580 603 41 0 7990 0
vsize: 32124
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.90 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 8061 0 0 0 19978 22 0 0 25 0 1 0 478716967 34787328 8039 4294967295 134512640 134672761 3221224624 3221223728 134560150 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8493 8039 603 41 0 8452 0
vsize: 33972
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 8062 0 0 0 20978 22 0 0 25 0 1 0 478716967 34787328 8040 4294967295 134512640 134672761 3221224624 3221223696 134553549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8493 8040 603 41 0 8452 0
vsize: 33972
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 8917 0 0 0 21976 24 0 0 25 0 1 0 478716967 38334464 8895 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9359 8895 603 41 0 9318 0
vsize: 37436
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 8917 0 0 0 22976 24 0 0 25 0 1 0 478716967 38334464 8895 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9359 8895 603 41 0 9318 0
vsize: 37436
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 8917 0 0 0 23976 24 0 0 25 0 1 0 478716967 38334464 8895 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9359 8895 603 41 0 9318 0
vsize: 37436
[startup+250.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 8917 0 0 0 24977 24 0 0 25 0 1 0 478716967 38334464 8895 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9359 8895 603 41 0 9318 0
vsize: 37436
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 8917 0 0 0 25977 24 0 0 25 0 1 0 478716967 38334464 8895 4294967295 134512640 134672761 3221224624 3221223728 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9359 8895 603 41 0 9318 0
vsize: 37436
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 8917 0 0 0 26977 24 0 0 25 0 1 0 478716967 38334464 8895 4294967295 134512640 134672761 3221224624 3221223792 134561261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9359 8895 603 41 0 9318 0
vsize: 37436
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 8917 0 0 0 27977 24 0 0 25 0 1 0 478716967 38334464 8895 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9359 8895 603 41 0 9318 0
vsize: 37436
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 8918 0 0 0 28977 24 0 0 25 0 1 0 478716967 38334464 8896 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 8918 0 0 0 29977 24 0 0 25 0 1 0 478716967 38334464 8896 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 8918 0 0 0 30977 24 0 0 25 0 1 0 478716967 38334464 8896 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+320.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 8918 0 0 0 31977 24 0 0 25 0 1 0 478716967 38334464 8896 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 8918 0 0 0 32978 24 0 0 25 0 1 0 478716967 38334464 8896 4294967295 134512640 134672761 3221224624 3221223728 134560364 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+340.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 8918 0 0 0 33978 24 0 0 25 0 1 0 478716967 38334464 8896 4294967295 134512640 134672761 3221224624 3221223792 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 8918 0 0 0 34978 24 0 0 25 0 1 0 478716967 38334464 8896 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+360.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25566
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 8918 0 0 0 35978 25 0 0 25 0 1 0 478716967 38334464 8896 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 8918 0 0 0 36978 25 0 0 25 0 1 0 478716967 38334464 8896 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+380.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 8918 0 0 0 37978 25 0 0 25 0 1 0 478716967 38334464 8896 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+390.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 8918 0 0 0 38978 25 0 0 25 0 1 0 478716967 38334464 8896 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+400.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 8918 0 0 0 39978 25 0 0 25 0 1 0 478716967 38334464 8896 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+410.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 8918 0 0 0 40979 25 0 0 25 0 1 0 478716967 38334464 8896 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+420.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 8918 0 0 0 41979 25 0 0 25 0 1 0 478716967 38334464 8896 4294967295 134512640 134672761 3221224624 3221223728 134559821 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 8918 0 0 0 42979 25 0 0 25 0 1 0 478716967 38334464 8896 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+440.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 8918 0 0 0 43979 25 0 0 25 0 1 0 478716967 38334464 8896 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+450.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 8918 0 0 0 44979 25 0 0 25 0 1 0 478716967 38334464 8896 4294967295 134512640 134672761 3221224624 3221223792 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+460.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 8918 0 0 0 45979 25 0 0 25 0 1 0 478716967 38334464 8896 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+470.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 8918 0 0 0 46979 25 0 0 25 0 1 0 478716967 38334464 8896 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9359 8896 603 41 0 9318 0
vsize: 37436
[startup+480.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 9302 0 0 0 47978 26 0 0 25 0 1 0 478716967 39952384 9280 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9754 9280 603 41 0 9713 0
vsize: 39016
[startup+490.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 9302 0 0 0 48978 26 0 0 25 0 1 0 478716967 39952384 9280 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9754 9280 603 41 0 9713 0
vsize: 39016
[startup+500.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 9327 0 0 0 49978 26 0 0 25 0 1 0 478716967 40087552 9305 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9787 9305 603 41 0 9746 0
vsize: 39148
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 10482 0 0 0 50975 29 0 0 25 0 1 0 478716967 44822528 10460 4294967295 134512640 134672761 3221224624 3221223760 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10943 10460 603 41 0 10902 0
vsize: 43772
[startup+520.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 10670 0 0 0 51975 30 0 0 25 0 1 0 478716967 45633536 10648 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11141 10648 603 41 0 11100 0
vsize: 44564
[startup+530.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 10670 0 0 0 52975 30 0 0 25 0 1 0 478716967 45633536 10648 4294967295 134512640 134672761 3221224624 3221223728 134559877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11141 10648 603 41 0 11100 0
vsize: 44564
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 11440 0 0 0 53973 32 0 0 25 0 1 0 478716967 48754688 11418 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11903 11418 603 41 0 11862 0
vsize: 47612
[startup+550.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 11440 0 0 0 54973 32 0 0 25 0 1 0 478716967 48754688 11418 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11903 11418 603 41 0 11862 0
vsize: 47612
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 11440 0 0 0 55973 32 0 0 25 0 1 0 478716967 48754688 11418 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11903 11418 603 41 0 11862 0
vsize: 47612
[startup+570.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 11440 0 0 0 56973 32 0 0 25 0 1 0 478716967 48754688 11418 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11903 11418 603 41 0 11862 0
vsize: 47612
[startup+580.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 11440 0 0 0 57973 32 0 0 25 0 1 0 478716967 48754688 11418 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11903 11418 603 41 0 11862 0
vsize: 47612
[startup+590.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 11503 0 0 0 58974 32 0 0 25 0 1 0 478716967 49025024 11481 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11969 11481 603 41 0 11928 0
vsize: 47876
[startup+600.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 11503 0 0 0 59974 32 0 0 25 0 1 0 478716967 49025024 11481 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11969 11481 603 41 0 11928 0
vsize: 47876
[startup+610.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 11503 0 0 0 60974 32 0 0 25 0 1 0 478716967 49025024 11481 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11969 11481 603 41 0 11928 0
vsize: 47876
[startup+620.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 11503 0 0 0 61974 33 0 0 25 0 1 0 478716967 49025024 11481 4294967295 134512640 134672761 3221224624 3221223728 134559821 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11969 11481 603 41 0 11928 0
vsize: 47876
[startup+630.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 11503 0 0 0 62974 33 0 0 25 0 1 0 478716967 49025024 11481 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11969 11481 603 41 0 11928 0
vsize: 47876
[startup+640.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 11503 0 0 0 63974 33 0 0 25 0 1 0 478716967 49025024 11481 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11969 11481 603 41 0 11928 0
vsize: 47876
[startup+650.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 11503 0 0 0 64974 33 0 0 25 0 1 0 478716967 49025024 11481 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11969 11481 603 41 0 11928 0
vsize: 47876
[startup+660.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25568
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 11503 0 0 0 65975 33 0 0 25 0 1 0 478716967 49025024 11481 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11969 11481 603 41 0 11928 0
vsize: 47876
[startup+670.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 11590 0 0 0 66975 33 0 0 25 0 1 0 478716967 49430528 11568 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12068 11568 603 41 0 12027 0
vsize: 48272
[startup+680.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 11590 0 0 0 67975 33 0 0 25 0 1 0 478716967 49430528 11568 4294967295 134512640 134672761 3221224624 3221223808 134559363 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12068 11568 603 41 0 12027 0
vsize: 48272
[startup+690.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 11590 0 0 0 68975 33 0 0 25 0 1 0 478716967 49430528 11568 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12068 11568 603 41 0 12027 0
vsize: 48272
[startup+700.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 11845 0 0 0 69975 33 0 0 25 0 1 0 478716967 50372608 11823 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12298 11823 603 41 0 12257 0
vsize: 49192
[startup+710.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 11845 0 0 0 70975 33 0 0 25 0 1 0 478716967 50372608 11823 4294967295 134512640 134672761 3221224624 3221223728 134560008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12298 11823 603 41 0 12257 0
vsize: 49192
[startup+720.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 11845 0 0 0 71975 34 0 0 25 0 1 0 478716967 50372608 11823 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12298 11823 603 41 0 12257 0
vsize: 49192
[startup+730.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 11845 0 0 0 72975 34 0 0 25 0 1 0 478716967 50372608 11823 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12298 11823 603 41 0 12257 0
vsize: 49192
[startup+740.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 11845 0 0 0 73975 34 0 0 25 0 1 0 478716967 50372608 11823 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12298 11823 603 41 0 12257 0
vsize: 49192
[startup+750.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 11928 0 0 0 74975 34 0 0 25 0 1 0 478716967 50778112 11906 4294967295 134512640 134672761 3221224624 3221223808 134559618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12397 11906 603 41 0 12356 0
vsize: 49588
[startup+760.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 11928 0 0 0 75975 34 0 0 25 0 1 0 478716967 50778112 11906 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12397 11906 603 41 0 12356 0
vsize: 49588
[startup+770.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 11937 0 0 0 76975 34 0 0 25 0 1 0 478716967 50778112 11915 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12397 11915 603 41 0 12356 0
vsize: 49588
[startup+780.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12244 0 0 0 77975 35 0 0 25 0 1 0 478716967 52162560 12222 4294967295 134512640 134672761 3221224624 3221223728 134554656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+790.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12244 0 0 0 78975 35 0 0 25 0 1 0 478716967 52162560 12222 4294967295 134512640 134672761 3221224624 3221223728 134560059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+800.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12244 0 0 0 79975 35 0 0 25 0 1 0 478716967 52162560 12222 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+810.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12244 0 0 0 80975 35 0 0 25 0 1 0 478716967 52162560 12222 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+820.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12244 0 0 0 81975 35 0 0 25 0 1 0 478716967 52162560 12222 4294967295 134512640 134672761 3221224624 3221223792 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+830.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12244 0 0 0 82975 35 0 0 25 0 1 0 478716967 52162560 12222 4294967295 134512640 134672761 3221224624 3221223728 134560235 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.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12244 0 0 0 83975 35 0 0 25 0 1 0 478716967 52162560 12222 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+850.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12244 0 0 0 84975 35 0 0 25 0 1 0 478716967 52162560 12222 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+860.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12244 0 0 0 85976 35 0 0 25 0 1 0 478716967 52162560 12222 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+870.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12244 0 0 0 86976 35 0 0 25 0 1 0 478716967 52162560 12222 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+880.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12244 0 0 0 87976 35 0 0 25 0 1 0 478716967 52162560 12222 4294967295 134512640 134672761 3221224624 3221223728 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+890.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12244 0 0 0 88976 35 0 0 25 0 1 0 478716967 52162560 12222 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+900.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12244 0 0 0 89976 35 0 0 25 0 1 0 478716967 52162560 12222 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+910.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12244 0 0 0 90976 35 0 0 25 0 1 0 478716967 52162560 12222 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+920.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12244 0 0 0 91976 36 0 0 25 0 1 0 478716967 52162560 12222 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+930.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12244 0 0 0 92977 36 0 0 25 0 1 0 478716967 52162560 12222 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+940.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12244 0 0 0 93977 36 0 0 25 0 1 0 478716967 52162560 12222 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+950.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12244 0 0 0 94977 36 0 0 25 0 1 0 478716967 52162560 12222 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+960.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25570
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12244 0 0 0 95977 36 0 0 25 0 1 0 478716967 52162560 12222 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+970.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25572
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12244 0 0 0 96977 36 0 0 25 0 1 0 478716967 52162560 12222 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+980.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25572
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12244 0 0 0 97977 36 0 0 25 0 1 0 478716967 52162560 12222 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+990.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25572
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12244 0 0 0 98978 36 0 0 25 0 1 0 478716967 52162560 12222 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12735 12222 603 41 0 12694 0
vsize: 50940
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25572
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12371 0 0 0 99978 36 0 0 25 0 1 0 478716967 52703232 12349 4294967295 134512640 134672761 3221224624 3221223728 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12867 12349 603 41 0 12826 0
vsize: 51468
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25572
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12371 0 0 0 100978 36 0 0 25 0 1 0 478716967 52703232 12349 4294967295 134512640 134672761 3221224624 3221223808 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12867 12349 603 41 0 12826 0
vsize: 51468
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25572
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12371 0 0 0 101978 36 0 0 25 0 1 0 478716967 52690944 12349 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12864 12349 603 41 0 12823 0
vsize: 51456
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25572
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12371 0 0 0 102978 36 0 0 25 0 1 0 478716967 52690944 12349 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12864 12349 603 41 0 12823 0
vsize: 51456
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25572
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12371 0 0 0 103978 36 0 0 25 0 1 0 478716967 52690944 12349 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12864 12349 603 41 0 12823 0
vsize: 51456
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25572
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12371 0 0 0 104978 36 0 0 25 0 1 0 478716967 52162560 12248 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12735 12248 603 41 0 12694 0
vsize: 50940
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25572
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12371 0 0 0 105978 36 0 0 25 0 1 0 478716967 52162560 12248 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12735 12248 603 41 0 12694 0
vsize: 50940
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25572
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12371 0 0 0 106979 36 0 0 25 0 1 0 478716967 52162560 12248 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12735 12248 603 41 0 12694 0
vsize: 50940
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25572
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12371 0 0 0 107979 36 0 0 25 0 1 0 478716967 52162560 12248 4294967295 134512640 134672761 3221224624 3221223792 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12735 12248 603 41 0 12694 0
vsize: 50940
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25572
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12371 0 0 0 108979 36 0 0 25 0 1 0 478716967 52162560 12248 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12735 12248 603 41 0 12694 0
vsize: 50940
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25572
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12371 0 0 0 109979 37 0 0 25 0 1 0 478716967 52162560 12248 4294967295 134512640 134672761 3221224624 3221223728 134559902 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12735 12248 603 41 0 12694 0
vsize: 50940
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25572
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12640 0 0 0 110978 37 0 0 25 0 1 0 478716967 53370880 12517 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13030 12517 603 41 0 12989 0
vsize: 52120
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25572
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12834 0 0 0 111978 38 0 0 25 0 1 0 478716967 54173696 12711 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13226 12711 603 41 0 13185 0
vsize: 52904
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25572
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12834 0 0 0 112978 38 0 0 25 0 1 0 478716967 54173696 12711 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13226 12711 603 41 0 13185 0
vsize: 52904
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25572
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12834 0 0 0 113978 38 0 0 25 0 1 0 478716967 54173696 12711 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13226 12711 603 41 0 13185 0
vsize: 52904
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25572
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12834 0 0 0 114979 38 0 0 25 0 1 0 478716967 54173696 12711 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13226 12711 603 41 0 13185 0
vsize: 52904
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25572
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 12834 0 0 0 115979 38 0 0 25 0 1 0 478716967 54173696 12711 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13226 12711 603 41 0 13185 0
vsize: 52904
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25572
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 13075 0 0 0 116979 38 0 0 25 0 1 0 478716967 55115776 12952 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13456 12952 603 41 0 13415 0
vsize: 53824
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25572
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 13518 0 0 0 117977 40 0 0 25 0 1 0 478716967 57036800 13395 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13925 13395 603 41 0 13884 0
vsize: 55700
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25572
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 13620 0 0 0 118977 40 0 0 25 0 1 0 478716967 57442304 13497 4294967295 134512640 134672761 3221224624 3221223728 134560326 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14024 13497 603 41 0 13983 0
vsize: 56096
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 25572
Raw data (stat): 25564 (minisat+) R 25563 22929 22928 0 -1 0 13620 0 0 0 119977 40 0 0 25 0 1 0 478716967 57442304 13497 4294967295 134512640 134672761 3221224624 3221223792 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14024 13497 603 41 0 13983 0
vsize: 56096
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 25572
Raw data (stat): 25564 (minisat+) Z 25563 22929 22928 0 -1 12 13622 0 0 0 119977 43 0 0 25 0 1 0 478716967 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

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