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-chnl35_45_pb.cnf.cr.opb
MD5SUM	1f5fb3c191c2c77719f10f35e4f5f992
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	46
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.094985
Number of variables	3150
Total number of constraints	160
Number of constraints which are clauses	90
Number of constraints which are cardinality constraints (but not clauses)	70
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	35
Maximum length of a constraint	45
Trace number 5715

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-04-14 01:38:15 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4152 boxname=wulflinc4 idbench=16 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  1f5fb3c191c2c77719f10f35e4f5f992  /oldhome/oroussel/tmp/wulflinc4/normalized-chnl35_45_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc4/normalized-chnl35_45_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc4/normalized-chnl35_45_pb.cnf.cr.opb
IDLAUNCH: 4152
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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	: 2
cpu MHz		: 451.169
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:        898220 kB
Buffers:         36080 kB
Cached:          80404 kB
SwapCached:          0 kB
Active:          54760 kB
Inactive:        64564 kB
HighTotal:      131008 kB
HighFree:        46844 kB
LowTotal:       903652 kB
LowFree:        851376 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11496 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:58:17 (client local time) WITH STATUS 0 IN 1200.2 SECONDS
stats: 4152 7 1200.2 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 160 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..........................................................................................
c ---[  69]---> BDD-cost:   87
c ---[  68]---> BDD-cost:   87
c ---[  67]---> BDD-cost:   87
c ---[  66]---> BDD-cost:   87
c ---[  65]---> BDD-cost:   87
c ---[  64]---> BDD-cost:   87
c ---[  63]---> BDD-cost:   87
c ---[  62]---> BDD-cost:   87
c ---[  61]---> BDD-cost:   87
c ---[  60]---> BDD-cost:   87
c ---[  59]---> BDD-cost:   87
c ---[  58]---> BDD-cost:   87
c ---[  57]---> BDD-cost:   87
c ---[  56]---> BDD-cost:   87
c ---[  55]---> BDD-cost:   87
c ---[  54]---> BDD-cost:   87
c ---[  53]---> BDD-cost:   87
c ---[  52]---> BDD-cost:   87
c ---[  51]---> BDD-cost:   87
c ---[  50]---> BDD-cost:   87
c ---[  49]---> BDD-cost:   87
c ---[  48]---> BDD-cost:   87
c ---[  47]---> BDD-cost:   87
c ---[  46]---> BDD-cost:   87
c ---[  45]---> BDD-cost:   87
c ---[  44]---> BDD-cost:   87
c ---[  43]---> BDD-cost:   87
c ---[  42]---> BDD-cost:   87
c ---[  41]---> BDD-cost:   87
c ---[  40]---> BDD-cost:   87
c ---[  39]---> BDD-cost:   87
c ---[  38]---> BDD-cost:   87
c ---[  37]---> BDD-cost:   87
c ---[  36]---> BDD-cost:   87
c ---[  35]---> BDD-cost:   87
c ---[  34]---> BDD-cost:   87
c ---[  33]---> BDD-cost:   87
c ---[  32]---> BDD-cost:   87
c ---[  31]---> BDD-cost:   87
c ---[  30]---> BDD-cost:   87
c ---[  29]---> BDD-cost:   87
c ---[  28]---> BDD-cost:   87
c ---[  27]---> BDD-cost:   87
c ---[  26]---> BDD-cost:   87
c ---[  25]---> BDD-cost:   87
c ---[  24]---> BDD-cost:   87
c ---[  23]---> BDD-cost:   87
c ---[  22]---> BDD-cost:   87
c ---[  21]---> BDD-cost:   87
c ---[  20]---> BDD-cost:   87
c ---[  19]---> BDD-cost:   87
c ---[  18]---> BDD-cost:   87
c ---[  17]---> BDD-cost:   87
c ---[  16]---> BDD-cost:   87
c ---[  15]---> BDD-cost:   87
c ---[  14]---> BDD-cost:   87
c ---[  13]---> BDD-cost:   87
c ---[  12]---> BDD-cost:   87
c ---[  11]---> BDD-cost:   87
c ---[  10]---> BDD-cost:   87
c ---[   9]---> BDD-cost:   87
c ---[   8]---> BDD-cost:   87
c ---[   7]---> BDD-cost:   87
c ---[   6]---> BDD-cost:   87
c ---[   5]---> BDD-cost:   87
c ---[   4]---> BDD-cost:   87
c ---[   3]---> BDD-cost:   87
c ---[   2]---> BDD-cost:   87
c ---[   1]---> BDD-cost:   87
c ---[   0]---> BDD-cost:   87
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   15210    42490 |    5070       0        0     nan |  0.000 % |
c |       101 |   15210    42490 |    5577     101    13595   134.6 |  0.758 % |
c |       253 |   15210    42490 |    6134     253    41155   162.7 |  0.758 % |
c |       480 |   15210    42490 |    6748     480    87737   182.8 |  0.758 % |
c |       819 |   15210    42490 |    7422     819   152105   185.7 |  0.758 % |
c |      1328 |   15210    42490 |    8165    1328   233504   175.8 |  0.758 % |
c |      2088 |   15210    42490 |    8981    2088   381775   182.8 |  0.758 % |
c |      3227 |   15210    42490 |    9879    3227   722388   223.9 |  0.758 % |
c |      4937 |   15210    42490 |   10867    4937  1190498   241.1 |  0.758 % |
c |      7499 |   15210    42490 |   11954    7499  1875349   250.1 |  0.758 % |
c |     11348 |   15210    42490 |   13150   11348  2998324   264.2 |  0.758 % |
c |     17114 |   15210    42490 |   14465    8729  2872831   329.1 |  0.758 % |
c |     25764 |   15210    42490 |   15911   17379  5578930   321.0 |  0.758 % |
c |     38739 |   15210    42490 |   17503   11971  5497632   459.2 |  0.758 % |
c |     58200 |   15210    42490 |   19253   10805  3533507   327.0 |  0.758 % |
c |     87395 |   15210    42490 |   21178   25607  7805831   304.8 |  0.758 % |
c |    131185 |   15210    42490 |   23296   15826  7858090   496.5 |  0.758 % |
c |    196870 |   15210    42490 |   25626   23958 10195199   425.5 |  0.758 % |
#### 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.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (runsolver) R 10903 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422466021 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.001 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 2947 0 0 0 990 7 0 0 25 0 1 0 422466021 13930496 2921 4294967295 134512640 134672761 3221224544 3221223728 134559482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3401 2921 603 41 0 3360 0
vsize: 13604
[startup+20.0014 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 4861 0 0 0 1984 12 0 0 25 0 1 0 422466021 21757952 4835 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5312 4835 603 41 0 5271 0
vsize: 21248
[startup+30.0027 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 6196 0 0 0 2981 15 0 0 25 0 1 0 422466021 27222016 6170 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6646 6170 603 41 0 6605 0
vsize: 26584
[startup+40.0034 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 6278 0 0 0 3980 15 0 0 25 0 1 0 422466021 27627520 6252 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6745 6252 603 41 0 6704 0
vsize: 26980
[startup+50.0029 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 6283 0 0 0 4980 15 0 0 25 0 1 0 422466021 27627520 6257 4294967295 134512640 134672761 3221224544 3221223648 134560489 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6745 6257 603 41 0 6704 0
vsize: 26980
[startup+60.0033 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 7004 0 0 0 5979 17 0 0 25 0 1 0 422466021 30605312 6978 4294967295 134512640 134672761 3221224544 3221223648 134559835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7472 6978 603 41 0 7431 0
vsize: 29888
[startup+70.0039 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 7004 0 0 0 6979 17 0 0 25 0 1 0 422466021 30605312 6978 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7472 6978 603 41 0 7431 0
vsize: 29888
[startup+80.0044 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 7597 0 0 0 7977 18 0 0 25 0 1 0 422466021 33042432 7571 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8067 7571 603 41 0 8026 0
vsize: 32268
[startup+90.0046 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 8611 0 0 0 8974 21 0 0 25 0 1 0 422466021 37236736 8585 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9091 8585 603 41 0 9050 0
vsize: 36364
[startup+100.005 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 8816 0 0 0 9974 22 0 0 25 0 1 0 422466021 38043648 8790 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9288 8790 603 41 0 9247 0
vsize: 37152
[startup+110.005 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 8816 0 0 0 10974 22 0 0 25 0 1 0 422466021 38043648 8790 4294967295 134512640 134672761 3221224544 3221223728 134559254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9288 8790 603 41 0 9247 0
vsize: 37152
[startup+120.006 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 9236 0 0 0 11973 23 0 0 25 0 1 0 422466021 39809024 9210 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9719 9210 603 41 0 9678 0
vsize: 38876
[startup+130.007 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 10152 0 0 0 12971 25 0 0 25 0 1 0 422466021 43585536 10126 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10641 10126 603 41 0 10600 0
vsize: 42564
[startup+140.007 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 10356 0 0 0 13971 26 0 0 25 0 1 0 422466021 44396544 10330 4294967295 134512640 134672761 3221224544 3221223640 1075347344 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10839 10330 603 41 0 10798 0
vsize: 43356
[startup+150.007 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 10356 0 0 0 14971 26 0 0 25 0 1 0 422466021 44396544 10330 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10839 10330 603 41 0 10798 0
vsize: 43356
[startup+160.008 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 10357 0 0 0 15971 26 0 0 25 0 1 0 422466021 44396544 10331 4294967295 134512640 134672761 3221224544 3221223648 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10839 10331 603 41 0 10798 0
vsize: 43356
[startup+170.007 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 10357 0 0 0 16971 26 0 0 25 0 1 0 422466021 44396544 10331 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10839 10331 603 41 0 10798 0
vsize: 43356
[startup+180.008 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 10357 0 0 0 17971 26 0 0 25 0 1 0 422466021 44396544 10331 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10839 10331 603 41 0 10798 0
vsize: 43356
[startup+190.009 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 10357 0 0 0 18972 26 0 0 25 0 1 0 422466021 44396544 10331 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10839 10331 603 41 0 10798 0
vsize: 43356
[startup+200.009 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 10358 0 0 0 19972 26 0 0 25 0 1 0 422466021 44396544 10332 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10839 10332 603 41 0 10798 0
vsize: 43356
[startup+210.01 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 10360 0 0 0 20972 26 0 0 25 0 1 0 422466021 44396544 10334 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10839 10334 603 41 0 10798 0
vsize: 43356
[startup+220.01 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 10361 0 0 0 21972 26 0 0 25 0 1 0 422466021 44396544 10335 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10839 10335 603 41 0 10798 0
vsize: 43356
[startup+230.011 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 10361 0 0 0 22973 26 0 0 25 0 1 0 422466021 44396544 10335 4294967295 134512640 134672761 3221224544 3221223648 134560501 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10839 10335 603 41 0 10798 0
vsize: 43356
[startup+240.01 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 10361 0 0 0 23973 26 0 0 25 0 1 0 422466021 44396544 10335 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10839 10335 603 41 0 10798 0
vsize: 43356
[startup+250.01 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 10361 0 0 0 24973 26 0 0 25 0 1 0 422466021 44396544 10335 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10839 10335 603 41 0 10798 0
vsize: 43356
[startup+260.011 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 10361 0 0 0 25973 26 0 0 25 0 1 0 422466021 44396544 10335 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10839 10335 603 41 0 10798 0
vsize: 43356
[startup+270.011 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 10361 0 0 0 26973 26 0 0 25 0 1 0 422466021 44396544 10335 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10839 10335 603 41 0 10798 0
vsize: 43356
[startup+280.012 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 10361 0 0 0 27973 26 0 0 25 0 1 0 422466021 44396544 10335 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10839 10335 603 41 0 10798 0
vsize: 43356
[startup+290.013 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 10361 0 0 0 28974 26 0 0 25 0 1 0 422466021 44396544 10335 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10839 10335 603 41 0 10798 0
vsize: 43356
[startup+300.012 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 10404 0 0 0 29973 26 0 0 25 0 1 0 422466021 44531712 10378 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10872 10378 603 41 0 10831 0
vsize: 43488
[startup+310.012 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 10404 0 0 0 30973 26 0 0 25 0 1 0 422466021 44531712 10378 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10872 10378 603 41 0 10831 0
vsize: 43488
[startup+320.013 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 10404 0 0 0 31974 26 0 0 25 0 1 0 422466021 44531712 10378 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10872 10378 603 41 0 10831 0
vsize: 43488
[startup+330.014 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 10685 0 0 0 32973 26 0 0 25 0 1 0 422466021 45740032 10659 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11167 10659 603 41 0 11126 0
vsize: 44668
[startup+340.014 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 10685 0 0 0 33974 26 0 0 25 0 1 0 422466021 45740032 10659 4294967295 134512640 134672761 3221224544 3221223616 134553549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11167 10659 603 41 0 11126 0
vsize: 44668
[startup+350.014 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 10685 0 0 0 34974 26 0 0 25 0 1 0 422466021 45740032 10659 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11167 10659 603 41 0 11126 0
vsize: 44668
[startup+360.014 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 10685 0 0 0 35974 26 0 0 25 0 1 0 422466021 45740032 10659 4294967295 134512640 134672761 3221224544 3221223728 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11167 10659 603 41 0 11126 0
vsize: 44668
[startup+370.015 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 10685 0 0 0 36974 26 0 0 25 0 1 0 422466021 45740032 10659 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11167 10659 603 41 0 11126 0
vsize: 44668
[startup+380.015 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 11163 0 0 0 37973 28 0 0 25 0 1 0 422466021 47632384 11137 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11629 11137 603 41 0 11588 0
vsize: 46516
[startup+390.016 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 11706 0 0 0 38972 29 0 0 25 0 1 0 422466021 49963008 11680 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12198 11680 603 41 0 12157 0
vsize: 48792
[startup+400.016 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 12378 0 0 0 39970 31 0 0 25 0 1 0 422466021 52682752 12352 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12862 12352 603 41 0 12821 0
vsize: 51448
[startup+410.017 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 12986 0 0 0 40969 33 0 0 25 0 1 0 422466021 55250944 12960 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13489 12960 603 41 0 13448 0
vsize: 53956
[startup+420.017 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 13590 0 0 0 41967 34 0 0 25 0 1 0 422466021 57696256 13564 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14086 13564 603 41 0 14045 0
vsize: 56344
[startup+430.018 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 14144 0 0 0 42966 36 0 0 25 0 1 0 422466021 60002304 14118 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14649 14118 603 41 0 14608 0
vsize: 58596
[startup+440.018 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 14431 0 0 0 43966 36 0 0 25 0 1 0 422466021 61083648 14405 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14913 14405 603 41 0 14872 0
vsize: 59652
[startup+450.017 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 14431 0 0 0 44966 36 0 0 25 0 1 0 422466021 61083648 14405 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14913 14405 603 41 0 14872 0
vsize: 59652
[startup+460.018 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 14431 0 0 0 45966 36 0 0 25 0 1 0 422466021 61083648 14405 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14913 14405 603 41 0 14872 0
vsize: 59652
[startup+470.019 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 14432 0 0 0 46966 36 0 0 25 0 1 0 422466021 61083648 14406 4294967295 134512640 134672761 3221224544 3221223648 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14913 14406 603 41 0 14872 0
vsize: 59652
[startup+480.019 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 14432 0 0 0 47966 36 0 0 25 0 1 0 422466021 61083648 14406 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14913 14406 603 41 0 14872 0
vsize: 59652
[startup+490.019 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 14432 0 0 0 48967 36 0 0 25 0 1 0 422466021 61083648 14406 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14913 14406 603 41 0 14872 0
vsize: 59652
[startup+500.019 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 14432 0 0 0 49967 36 0 0 25 0 1 0 422466021 61083648 14406 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14913 14406 603 41 0 14872 0
vsize: 59652
[startup+510.019 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 14432 0 0 0 50967 36 0 0 25 0 1 0 422466021 61083648 14406 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14913 14406 603 41 0 14872 0
vsize: 59652
[startup+520.019 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 14701 0 0 0 51966 38 0 0 25 0 1 0 422466021 62300160 14675 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15210 14675 603 41 0 15169 0
vsize: 60840
[startup+530.021 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 15264 0 0 0 52964 39 0 0 25 0 1 0 422466021 64606208 15238 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15773 15238 603 41 0 15732 0
vsize: 63092
[startup+540.021 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 15763 0 0 0 53963 41 0 0 25 0 1 0 422466021 66633728 15737 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16268 15737 603 41 0 16227 0
vsize: 65072
[startup+550.021 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 16422 0 0 0 54961 43 0 0 25 0 1 0 422466021 69238784 16396 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16904 16396 603 41 0 16863 0
vsize: 67616
[startup+560.022 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17112 0 0 0 55960 44 0 0 25 0 1 0 422466021 72073216 17086 4294967295 134512640 134672761 3221224544 3221223648 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17086 603 41 0 17555 0
vsize: 70384
[startup+570.022 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17112 0 0 0 56960 44 0 0 25 0 1 0 422466021 72073216 17086 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17086 603 41 0 17555 0
vsize: 70384
[startup+580.024 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17112 0 0 0 57960 45 0 0 25 0 1 0 422466021 72073216 17086 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17596 17086 603 41 0 17555 0
vsize: 70384
[startup+590.025 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17112 0 0 0 58959 45 0 0 25 0 1 0 422466021 72073216 17086 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17086 603 41 0 17555 0
vsize: 70384
[startup+600.025 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17113 0 0 0 59959 45 0 0 25 0 1 0 422466021 72073216 17087 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17087 603 41 0 17555 0
vsize: 70384
[startup+610.025 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 60959 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+620.025 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 61960 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+630.026 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 62960 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+640.027 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 63960 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+650.027 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 64960 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+660.027 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 65960 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+670.027 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 66961 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+680.028 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 67961 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+690.028 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 68961 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+700.028 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 69961 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+710.029 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 70961 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+720.029 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 71962 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+730.03 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 72962 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+740.031 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 73962 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+750.031 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 74962 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+760.031 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 75962 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223648 134560231 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+770.031 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 76963 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+780.033 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 77963 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+790.033 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 78963 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+800.032 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 79963 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+810.033 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 80963 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+820.033 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 81964 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223728 134559542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+830.034 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 82964 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+840.035 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 83964 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+850.035 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 84964 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223648 134560010 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+860.035 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 85965 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+870.035 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 86965 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+880.036 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 87965 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+890.036 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 88965 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+900.036 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17114 0 0 0 89965 45 0 0 25 0 1 0 422466021 72073216 17088 4294967295 134512640 134672761 3221224544 3221223648 134560506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17596 17088 603 41 0 17555 0
vsize: 70384
[startup+910.037 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17116 0 0 0 90965 45 0 0 25 0 1 0 422466021 72073216 17090 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17090 603 41 0 17555 0
vsize: 70384
[startup+920.037 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17116 0 0 0 91965 45 0 0 25 0 1 0 422466021 72073216 17090 4294967295 134512640 134672761 3221224544 3221223728 134559583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17090 603 41 0 17555 0
vsize: 70384
[startup+930.039 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17116 0 0 0 92965 45 0 0 25 0 1 0 422466021 72073216 17090 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17090 603 41 0 17555 0
vsize: 70384
[startup+940.038 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17117 0 0 0 93965 45 0 0 25 0 1 0 422466021 72073216 17091 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17091 603 41 0 17555 0
vsize: 70384
[startup+950.038 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17117 0 0 0 94966 45 0 0 25 0 1 0 422466021 72073216 17091 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17091 603 41 0 17555 0
vsize: 70384
[startup+960.039 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17117 0 0 0 95966 45 0 0 25 0 1 0 422466021 72073216 17091 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17091 603 41 0 17555 0
vsize: 70384
[startup+970.039 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17117 0 0 0 96966 45 0 0 25 0 1 0 422466021 72073216 17091 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17091 603 41 0 17555 0
vsize: 70384
[startup+980.04 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17117 0 0 0 97966 45 0 0 25 0 1 0 422466021 72073216 17091 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17091 603 41 0 17555 0
vsize: 70384
[startup+990.041 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17117 0 0 0 98966 45 0 0 25 0 1 0 422466021 72073216 17091 4294967295 134512640 134672761 3221224544 3221223648 134559927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17091 603 41 0 17555 0
vsize: 70384
[startup+1000.04 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17117 0 0 0 99967 45 0 0 25 0 1 0 422466021 72073216 17091 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17091 603 41 0 17555 0
vsize: 70384
[startup+1010.04 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17117 0 0 0 100967 45 0 0 25 0 1 0 422466021 72073216 17091 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17091 603 41 0 17555 0
vsize: 70384
[startup+1020.04 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17117 0 0 0 101967 45 0 0 25 0 1 0 422466021 72073216 17091 4294967295 134512640 134672761 3221224544 3221223648 134559853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17091 603 41 0 17555 0
vsize: 70384
[startup+1030.04 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17117 0 0 0 102967 45 0 0 25 0 1 0 422466021 72073216 17091 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17091 603 41 0 17555 0
vsize: 70384
[startup+1040.04 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17117 0 0 0 103968 45 0 0 25 0 1 0 422466021 72073216 17091 4294967295 134512640 134672761 3221224544 3221223696 134542720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17091 603 41 0 17555 0
vsize: 70384
[startup+1050.04 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17117 0 0 0 104968 45 0 0 25 0 1 0 422466021 72073216 17091 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17091 603 41 0 17555 0
vsize: 70384
[startup+1060.04 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17117 0 0 0 105968 45 0 0 25 0 1 0 422466021 72073216 17091 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17091 603 41 0 17555 0
vsize: 70384
[startup+1070.04 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17117 0 0 0 106968 45 0 0 25 0 1 0 422466021 72073216 17091 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17091 603 41 0 17555 0
vsize: 70384
[startup+1080.05 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17117 0 0 0 107968 45 0 0 25 0 1 0 422466021 72073216 17091 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17091 603 41 0 17555 0
vsize: 70384
[startup+1090.05 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17117 0 0 0 108969 45 0 0 25 0 1 0 422466021 72073216 17091 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17091 603 41 0 17555 0
vsize: 70384
[startup+1100.05 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17117 0 0 0 109969 45 0 0 25 0 1 0 422466021 72073216 17091 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17091 603 41 0 17555 0
vsize: 70384
[startup+1110.05 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17117 0 0 0 110969 45 0 0 25 0 1 0 422466021 72073216 17091 4294967295 134512640 134672761 3221224544 3221223696 134565137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17091 603 41 0 17555 0
vsize: 70384
[startup+1120.05 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17117 0 0 0 111969 45 0 0 25 0 1 0 422466021 72073216 17091 4294967295 134512640 134672761 3221224544 3221223648 134559998 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17091 603 41 0 17555 0
vsize: 70384
[startup+1130.05 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17117 0 0 0 112969 45 0 0 25 0 1 0 422466021 72073216 17091 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17091 603 41 0 17555 0
vsize: 70384
[startup+1140.05 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17117 0 0 0 113969 45 0 0 25 0 1 0 422466021 72073216 17091 4294967295 134512640 134672761 3221224544 3221223648 134554671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17091 603 41 0 17555 0
vsize: 70384
[startup+1150.05 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17117 0 0 0 114970 45 0 0 25 0 1 0 422466021 72073216 17091 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17091 603 41 0 17555 0
vsize: 70384
[startup+1160.05 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17117 0 0 0 115970 45 0 0 25 0 1 0 422466021 72073216 17091 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17091 603 41 0 17555 0
vsize: 70384
[startup+1170.05 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17117 0 0 0 116970 45 0 0 25 0 1 0 422466021 72073216 17091 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17091 603 41 0 17555 0
vsize: 70384
[startup+1180.05 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17117 0 0 0 117970 45 0 0 25 0 1 0 422466021 72073216 17091 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17091 603 41 0 17555 0
vsize: 70384
[startup+1190.05 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17117 0 0 0 118970 45 0 0 25 0 1 0 422466021 72073216 17091 4294967295 134512640 134672761 3221224544 3221223696 134565213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17091 603 41 0 17555 0
vsize: 70384
[startup+1200.05 s]
Raw data (loadavg): 0.99 1.00 0.96 2/54 10904
Raw data (stat): 10904 (minisat+) R 10903 5897 5896 0 -1 0 17117 0 0 0 119970 45 0 0 25 0 1 0 422466021 72073216 17091 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17596 17091 603 41 0 17555 0
vsize: 70384
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 1.00 0.96 1/54 10904
Raw data (stat): 10904 (minisat+) Z 10903 5897 5896 0 -1 12 17119 0 0 0 119971 48 0 0 25 0 1 0 422466021 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.2
CPU user time (s): 1199.71
CPU system time (s): 0.484926
CPU usage (%): 100.009
Max. virtual memory (Kb): 70384
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####