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 4594

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        862420 kB
Buffers:         33188 kB
Cached:          99384 kB
SwapCached:       2476 kB
Active:          47292 kB
Inactive:        90604 kB
HighTotal:      131008 kB
HighFree:        28588 kB
LowTotal:       903652 kB
LowFree:        833832 kB
SwapTotal:     2097892 kB
SwapFree:      2095416 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6944 kB
Slab:            28820 kB
Committed_AS:    63616 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 19:46:00 (client local time) WITH STATUS 0 IN 1200.17 SECONDS
stats: 3400 7 1200.17 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]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  68]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  67]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  66]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  65]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  64]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  63]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  62]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  61]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  60]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  59]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  58]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  57]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  56]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  55]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  54]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  53]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  52]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  51]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  50]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  49]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  48]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  47]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  46]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  45]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  44]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  43]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  42]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  41]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  40]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  39]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  38]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  37]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  36]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  35]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  34]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  33]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  32]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  31]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  30]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  29]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  28]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  27]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  26]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  25]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  24]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  23]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  22]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  21]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  20]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  19]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  18]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  17]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  16]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  15]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  14]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  13]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  12]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  11]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[  10]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[   9]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[   8]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[   7]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[   6]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[   5]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[   4]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[   3]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[   2]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[   1]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[   0]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   36980   134400 |   12326       0        0     nan |  0.000 % |
c |       100 |   36652   133308 |   13558      14       28     2.0 |  6.839 % |
c |       253 |   36193   131687 |   14914      79      327     4.1 |  7.615 % |
c |       478 |   35829   130319 |   16405     256     1002     3.9 |  8.200 % |
c |       815 |   35551   129303 |   18046     555     2562     4.6 |  8.718 % |
c |      1321 |   34844   126750 |   19851     987     4886     5.0 | 10.214 % |
c |      2080 |   32705   119153 |   21836    1484     7305     4.9 | 14.601 % |
c |      3219 |   27153    99991 |   24019    1846    10533     5.7 | 25.771 % |
c |      4927 |   19517    74027 |   26421    2395    17057     7.1 | 41.114 % |
c |      7493 |   17760    68226 |   29064    4715   633302   134.3 | 44.994 % |
c |     11337 |   17742    68168 |   31970    8557  3010365   351.8 | 45.039 % |
c |     17103 |   17742    68168 |   35167   14323  7224955   504.4 | 45.039 % |
c |     25752 |   17742    68168 |   38684   22972 13400042   583.3 | 45.039 % |
c |     38726 |   17742    68168 |   42552   35946 23219488   646.0 | 45.039 % |
c |     58202 |   17742    68168 |   46807   20887 14090059   674.6 | 45.039 % |
c |     87395 |   17742    68168 |   51488   50080 35648238   711.8 | 45.039 % |
c |    131192 |   17733    68139 |   56637   51720 39805153   769.6 | 45.062 % |
#### 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.00 0.00 0.00 2/54 24140
Raw data (stat): 24140 (runsolver) R 24139 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478461918 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.15 0.03 0.01 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 1159 0 1 0 985 2 0 0 25 0 1 0 478461918 6737920 1134 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1645 1134 603 41 0 1604 0
vsize: 6580
[startup+20.0005 s]
Raw data (loadavg): 0.28 0.06 0.02 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 1165 0 1 0 1985 2 0 0 25 0 1 0 478461918 6737920 1140 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1645 1140 603 41 0 1604 0
vsize: 6580
[startup+30.0012 s]
Raw data (loadavg): 0.39 0.09 0.03 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 2114 0 1 0 2982 5 0 0 25 0 1 0 478461918 10641408 2089 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2598 2089 603 41 0 2557 0
vsize: 10392
[startup+40.0005 s]
Raw data (loadavg): 0.49 0.12 0.04 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 4611 0 1 0 3976 11 0 0 25 0 1 0 478461918 20836352 4586 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5087 4586 603 41 0 5046 0
vsize: 20348
[startup+50.0015 s]
Raw data (loadavg): 0.56 0.15 0.05 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 6820 0 1 0 4972 15 0 0 25 0 1 0 478461918 29872128 6795 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7293 6795 603 41 0 7252 0
vsize: 29172
[startup+60.0022 s]
Raw data (loadavg): 0.63 0.18 0.06 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 8290 0 1 0 5969 19 0 0 25 0 1 0 478461918 35954688 8265 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8778 8265 603 41 0 8737 0
vsize: 35112
[startup+70.0025 s]
Raw data (loadavg): 0.69 0.21 0.07 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 9917 0 1 0 6965 23 0 0 25 0 1 0 478461918 42496000 9892 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10375 9892 603 41 0 10334 0
vsize: 41500
[startup+80.0036 s]
Raw data (loadavg): 0.73 0.23 0.08 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 11425 0 1 0 7962 26 0 0 25 0 1 0 478461918 48791552 11400 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11912 11400 603 41 0 11871 0
vsize: 47648
[startup+90.0035 s]
Raw data (loadavg): 0.77 0.26 0.09 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 12575 0 1 0 8959 29 0 0 25 0 1 0 478461918 53465088 12550 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13053 12550 603 41 0 13012 0
vsize: 52212
[startup+100.004 s]
Raw data (loadavg): 0.81 0.28 0.10 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 13629 0 1 0 9957 32 0 0 25 0 1 0 478461918 57856000 13604 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14125 13604 603 41 0 14084 0
vsize: 56500
[startup+110.005 s]
Raw data (loadavg): 0.84 0.30 0.11 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 14475 0 1 0 10955 34 0 0 25 0 1 0 478461918 61333504 14450 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14974 14450 603 41 0 14933 0
vsize: 59896
[startup+120.005 s]
Raw data (loadavg): 0.86 0.33 0.12 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 15194 0 1 0 11953 35 0 0 25 0 1 0 478461918 64282624 15169 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15694 15169 603 41 0 15653 0
vsize: 62776
[startup+130.006 s]
Raw data (loadavg): 0.96 0.36 0.13 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 15591 0 1 0 12953 36 0 0 25 0 1 0 478461918 65859584 15566 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16079 15566 603 41 0 16038 0
vsize: 64316
[startup+140.006 s]
Raw data (loadavg): 0.97 0.38 0.14 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 16053 0 1 0 13952 37 0 0 25 0 1 0 478461918 67842048 16028 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16563 16028 603 41 0 16522 0
vsize: 66252
[startup+150.007 s]
Raw data (loadavg): 0.97 0.40 0.15 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 16505 0 1 0 14951 38 0 0 25 0 1 0 478461918 69705728 16480 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17018 16480 603 41 0 16977 0
vsize: 68072
[startup+160.007 s]
Raw data (loadavg): 0.98 0.42 0.16 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 17083 0 1 0 15949 40 0 0 25 0 1 0 478461918 72065024 17058 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17594 17058 603 41 0 17553 0
vsize: 70376
[startup+170.007 s]
Raw data (loadavg): 0.98 0.44 0.16 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 17805 0 1 0 16947 42 0 0 25 0 1 0 478461918 74973184 17780 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18304 17780 603 41 0 18263 0
vsize: 73216
[startup+180.007 s]
Raw data (loadavg): 0.98 0.46 0.17 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 18688 0 1 0 17946 43 0 0 25 0 1 0 478461918 78565376 18663 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19181 18663 603 41 0 19140 0
vsize: 76724
[startup+190.008 s]
Raw data (loadavg): 0.98 0.48 0.18 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 19398 0 1 0 18943 46 0 0 25 0 1 0 478461918 81477632 19373 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19892 19373 603 41 0 19851 0
vsize: 79568
[startup+200.009 s]
Raw data (loadavg): 0.99 0.49 0.19 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 19917 0 1 0 19942 48 0 0 25 0 1 0 478461918 83587072 19892 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20407 19892 603 41 0 20366 0
vsize: 81628
[startup+210.01 s]
Raw data (loadavg): 0.99 0.51 0.20 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 20451 0 1 0 20941 49 0 0 25 0 1 0 478461918 85819392 20426 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20952 20426 603 41 0 20911 0
vsize: 83808
[startup+220.01 s]
Raw data (loadavg): 0.99 0.53 0.21 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 20996 0 1 0 21939 51 0 0 25 0 1 0 478461918 88080384 20971 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21504 20971 603 41 0 21463 0
vsize: 86016
[startup+230.01 s]
Raw data (loadavg): 0.99 0.54 0.21 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 21492 0 1 0 22938 52 0 0 25 0 1 0 478461918 90091520 21467 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21995 21467 603 41 0 21954 0
vsize: 87980
[startup+240.009 s]
Raw data (loadavg): 0.99 0.56 0.22 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 21948 0 1 0 23937 54 0 0 25 0 1 0 478461918 92061696 21923 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22476 21923 603 41 0 22435 0
vsize: 89904
[startup+250.01 s]
Raw data (loadavg): 0.99 0.57 0.23 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 22418 0 1 0 24936 55 0 0 25 0 1 0 478461918 93900800 22393 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22925 22393 603 41 0 22884 0
vsize: 91700
[startup+260.01 s]
Raw data (loadavg): 0.99 0.58 0.24 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 23096 0 1 0 25935 56 0 0 25 0 1 0 478461918 96780288 23071 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23628 23071 603 41 0 23587 0
vsize: 94512
[startup+270.01 s]
Raw data (loadavg): 0.99 0.60 0.24 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 23559 0 1 0 26933 58 0 0 25 0 1 0 478461918 98783232 23534 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24117 23534 603 41 0 24076 0
vsize: 96468
[startup+280.01 s]
Raw data (loadavg): 0.99 0.61 0.25 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 24016 0 1 0 27931 60 0 0 25 0 1 0 478461918 100622336 23991 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24566 23991 603 41 0 24525 0
vsize: 98264
[startup+290.01 s]
Raw data (loadavg): 0.99 0.62 0.26 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 24499 0 1 0 28930 61 0 0 25 0 1 0 478461918 102588416 24474 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25046 24474 603 41 0 25005 0
vsize: 100184
[startup+300.011 s]
Raw data (loadavg): 0.99 0.63 0.27 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 25068 0 1 0 29929 62 0 0 25 0 1 0 478461918 104878080 25043 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25605 25043 603 41 0 25564 0
vsize: 102420
[startup+310.011 s]
Raw data (loadavg): 0.99 0.64 0.28 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 25558 0 1 0 30928 63 0 0 25 0 1 0 478461918 107044864 25533 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26134 25533 603 41 0 26093 0
vsize: 104536
[startup+320.011 s]
Raw data (loadavg): 0.99 0.66 0.28 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 27197 0 1 0 31924 67 0 0 25 0 1 0 478461918 113700864 27172 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27759 27172 603 41 0 27718 0
vsize: 111036
[startup+330.012 s]
Raw data (loadavg): 0.99 0.67 0.29 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 28951 0 1 0 32921 70 0 0 25 0 1 0 478461918 120938496 28926 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29526 28926 603 41 0 29485 0
vsize: 118104
[startup+340.011 s]
Raw data (loadavg): 0.99 0.68 0.30 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 30624 0 1 0 33918 74 0 0 25 0 1 0 478461918 127741952 30599 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31187 30599 603 41 0 31146 0
vsize: 124748
[startup+350.012 s]
Raw data (loadavg): 0.99 0.69 0.30 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 32050 0 1 0 34915 77 0 0 25 0 1 0 478461918 133636096 32025 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32626 32025 603 41 0 32585 0
vsize: 130504
[startup+360.012 s]
Raw data (loadavg): 0.99 0.70 0.31 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 33694 0 1 0 35911 81 0 0 25 0 1 0 478461918 140308480 33669 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34255 33669 603 41 0 34214 0
vsize: 137020
[startup+370.012 s]
Raw data (loadavg): 0.99 0.71 0.32 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 34129 0 1 0 36910 82 0 0 25 0 1 0 478461918 142180352 34104 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34712 34104 603 41 0 34671 0
vsize: 138848
[startup+380.013 s]
Raw data (loadavg): 0.99 0.72 0.32 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 34130 0 1 0 37910 82 0 0 25 0 1 0 478461918 142180352 34105 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34712 34105 603 41 0 34671 0
vsize: 138848
[startup+390.014 s]
Raw data (loadavg): 0.99 0.72 0.33 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 34133 0 1 0 38909 83 0 0 25 0 1 0 478461918 142180352 34108 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34712 34108 603 41 0 34671 0
vsize: 138848
[startup+400.014 s]
Raw data (loadavg): 0.99 0.73 0.34 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 34136 0 1 0 39909 83 0 0 25 0 1 0 478461918 142180352 34111 4294967295 134512640 134672761 3221224544 3221223648 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34712 34111 603 41 0 34671 0
vsize: 138848
[startup+410.015 s]
Raw data (loadavg): 0.99 0.74 0.34 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 34136 0 1 0 40909 83 0 0 25 0 1 0 478461918 142180352 34111 4294967295 134512640 134672761 3221224544 3221223560 1075352757 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34712 34111 603 41 0 34671 0
vsize: 138848
[startup+420.014 s]
Raw data (loadavg): 0.99 0.75 0.35 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 34136 0 1 0 41909 83 0 0 25 0 1 0 478461918 142180352 34111 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34712 34111 603 41 0 34671 0
vsize: 138848
[startup+430.015 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 34136 0 1 0 42909 84 0 0 25 0 1 0 478461918 142180352 34111 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34712 34111 603 41 0 34671 0
vsize: 138848
[startup+440.015 s]
Raw data (loadavg): 0.99 0.77 0.36 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 34136 0 1 0 43909 84 0 0 25 0 1 0 478461918 142180352 34111 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34712 34111 603 41 0 34671 0
vsize: 138848
[startup+450.016 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 34136 0 1 0 44909 84 0 0 25 0 1 0 478461918 142180352 34111 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34712 34111 603 41 0 34671 0
vsize: 138848
[startup+460.016 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 34136 0 1 0 45909 84 0 0 25 0 1 0 478461918 142180352 34111 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34712 34111 603 41 0 34671 0
vsize: 138848
[startup+470.016 s]
Raw data (loadavg): 0.99 0.79 0.38 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 34136 0 1 0 46909 85 0 0 25 0 1 0 478461918 142180352 34111 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34712 34111 603 41 0 34671 0
vsize: 138848
[startup+480.016 s]
Raw data (loadavg): 0.99 0.79 0.39 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 34136 0 1 0 47908 85 0 0 25 0 1 0 478461918 142180352 34111 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34712 34111 603 41 0 34671 0
vsize: 138848
[startup+490.016 s]
Raw data (loadavg): 0.99 0.80 0.39 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 34136 0 1 0 48908 86 0 0 25 0 1 0 478461918 142180352 34111 4294967295 134512640 134672761 3221224544 3221223728 134558632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34712 34111 603 41 0 34671 0
vsize: 138848
[startup+500.017 s]
Raw data (loadavg): 0.99 0.80 0.40 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 34136 0 1 0 49908 86 0 0 25 0 1 0 478461918 142180352 34111 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34712 34111 603 41 0 34671 0
vsize: 138848
[startup+510.017 s]
Raw data (loadavg): 0.99 0.81 0.41 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 34136 0 1 0 50908 86 0 0 25 0 1 0 478461918 142180352 34111 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34712 34111 603 41 0 34671 0
vsize: 138848
[startup+520.016 s]
Raw data (loadavg): 0.99 0.82 0.41 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 34136 0 1 0 51908 86 0 0 25 0 1 0 478461918 142180352 34111 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34712 34111 603 41 0 34671 0
vsize: 138848
[startup+530.017 s]
Raw data (loadavg): 0.99 0.82 0.42 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 34136 0 1 0 52909 86 0 0 25 0 1 0 478461918 142180352 34111 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34712 34111 603 41 0 34671 0
vsize: 138848
[startup+540.016 s]
Raw data (loadavg): 0.99 0.83 0.42 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 34487 0 1 0 53908 86 0 0 25 0 1 0 478461918 143642624 34462 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35069 34462 603 41 0 35028 0
vsize: 140276
[startup+550.016 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 35550 0 1 0 54905 89 0 0 25 0 1 0 478461918 147931136 35525 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36116 35525 603 41 0 36075 0
vsize: 144464
[startup+560.017 s]
Raw data (loadavg): 0.99 0.84 0.43 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 36987 0 1 0 55902 92 0 0 25 0 1 0 478461918 153825280 36962 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37555 36962 603 41 0 37514 0
vsize: 150220
[startup+570.017 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 38288 0 1 0 56899 96 0 0 25 0 1 0 478461918 159141888 38263 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38853 38263 603 41 0 38812 0
vsize: 155412
[startup+580.017 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 39134 0 1 0 57897 98 0 0 25 0 1 0 478461918 162643968 39109 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39708 39109 603 41 0 39667 0
vsize: 158832
[startup+590.018 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 40180 0 1 0 58894 101 0 0 25 0 1 0 478461918 166907904 40155 4294967295 134512640 134672761 3221224544 3221223728 134559548 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40749 40155 603 41 0 40708 0
vsize: 162996
[startup+600.018 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 41192 0 1 0 59892 103 0 0 25 0 1 0 478461918 171036672 41167 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41757 41167 603 41 0 41716 0
vsize: 167028
[startup+610.018 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 42210 0 1 0 60889 106 0 0 25 0 1 0 478461918 175284224 42185 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42794 42185 603 41 0 42753 0
vsize: 171176
[startup+620.018 s]
Raw data (loadavg): 0.99 0.86 0.47 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 43170 0 1 0 61887 109 0 0 25 0 1 0 478461918 179138560 43145 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43735 43145 603 41 0 43694 0
vsize: 174940
[startup+630.019 s]
Raw data (loadavg): 0.99 0.87 0.47 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 62885 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+640.018 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 63885 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+650.019 s]
Raw data (loadavg): 0.99 0.88 0.48 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 64886 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+660.019 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 65886 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+670.019 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 66886 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+680.02 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 67886 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+690.02 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 68886 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+700.02 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 69887 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+710.02 s]
Raw data (loadavg): 0.99 0.90 0.51 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 70887 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+720.02 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 71887 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+730.021 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 72887 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+740.02 s]
Raw data (loadavg): 0.99 0.90 0.53 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 73887 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223648 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+750.021 s]
Raw data (loadavg): 0.99 0.91 0.53 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 74888 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223728 134559417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+760.022 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 75888 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+770.021 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 76888 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+780.022 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 77888 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+790.022 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 78888 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+800.022 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 79889 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+810.022 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 80889 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+820.022 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 81889 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+830.022 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 82889 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+840.022 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 83889 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+850.022 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 84889 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+860.021 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 85890 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+870.021 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 86890 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+880.022 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 87890 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+890.021 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 88890 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+900.022 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 89890 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+910.022 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 90891 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+920.021 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44034 0 1 0 91891 111 0 0 25 0 1 0 478461918 182726656 44009 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44009 603 41 0 44570 0
vsize: 178444
[startup+930.022 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44035 0 1 0 92891 111 0 0 25 0 1 0 478461918 182726656 44010 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44010 603 41 0 44570 0
vsize: 178444
[startup+940.023 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44035 0 1 0 93891 111 0 0 25 0 1 0 478461918 182726656 44010 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44010 603 41 0 44570 0
vsize: 178444
[startup+950.024 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44035 0 1 0 94891 111 0 0 25 0 1 0 478461918 182726656 44010 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44010 603 41 0 44570 0
vsize: 178444
[startup+960.023 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44035 0 1 0 95892 111 0 0 25 0 1 0 478461918 182726656 44010 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44010 603 41 0 44570 0
vsize: 178444
[startup+970.023 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44035 0 1 0 96892 111 0 0 25 0 1 0 478461918 182726656 44010 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44010 603 41 0 44570 0
vsize: 178444
[startup+980.024 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44035 0 1 0 97892 111 0 0 25 0 1 0 478461918 182726656 44010 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44010 603 41 0 44570 0
vsize: 178444
[startup+990.023 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44035 0 1 0 98892 111 0 0 25 0 1 0 478461918 182726656 44010 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44010 603 41 0 44570 0
vsize: 178444
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44035 0 1 0 99892 111 0 0 25 0 1 0 478461918 182726656 44010 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44010 603 41 0 44570 0
vsize: 178444
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44035 0 1 0 100893 111 0 0 25 0 1 0 478461918 182726656 44010 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44010 603 41 0 44570 0
vsize: 178444
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44035 0 1 0 101893 111 0 0 25 0 1 0 478461918 182726656 44010 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44010 603 41 0 44570 0
vsize: 178444
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44035 0 1 0 102893 111 0 0 25 0 1 0 478461918 182726656 44010 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44010 603 41 0 44570 0
vsize: 178444
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44035 0 1 0 103893 111 0 0 25 0 1 0 478461918 182726656 44010 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44010 603 41 0 44570 0
vsize: 178444
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44035 0 1 0 104893 111 0 0 25 0 1 0 478461918 182726656 44010 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44010 603 41 0 44570 0
vsize: 178444
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.96 0.65 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44035 0 1 0 105894 111 0 0 25 0 1 0 478461918 182726656 44010 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44010 603 41 0 44570 0
vsize: 178444
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.96 0.65 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44035 0 1 0 106894 111 0 0 25 0 1 0 478461918 182726656 44010 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44010 603 41 0 44570 0
vsize: 178444
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44035 0 1 0 107894 111 0 0 25 0 1 0 478461918 182726656 44010 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44010 603 41 0 44570 0
vsize: 178444
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44035 0 1 0 108894 111 0 0 25 0 1 0 478461918 182726656 44010 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44010 603 41 0 44570 0
vsize: 178444
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44035 0 1 0 109894 111 0 0 25 0 1 0 478461918 182726656 44010 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44611 44010 603 41 0 44570 0
vsize: 178444
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 44666 0 1 0 110892 112 0 0 25 0 1 0 478461918 185282560 44641 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45235 44641 603 41 0 45194 0
vsize: 180940
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 45525 0 1 0 111890 114 0 0 25 0 1 0 478461918 188882944 45500 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46114 45500 603 41 0 46073 0
vsize: 184456
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 46472 0 1 0 112889 116 0 0 25 0 1 0 478461918 192724992 46447 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47052 46447 603 41 0 47011 0
vsize: 188208
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 47327 0 1 0 113887 118 0 0 25 0 1 0 478461918 196304896 47302 4294967295 134512640 134672761 3221224544 3221223724 134559056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47926 47303 603 41 0 47885 0
vsize: 191704
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 47949 0 1 0 114886 119 0 0 25 0 1 0 478461918 198860800 47924 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48550 47924 603 41 0 48509 0
vsize: 194200
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 48421 0 1 0 115885 120 0 0 25 0 1 0 478461918 200871936 48396 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49041 48396 603 41 0 49000 0
vsize: 196164
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 49113 0 1 0 116884 122 0 0 25 0 1 0 478461918 203677696 49088 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49726 49088 603 41 0 49685 0
vsize: 198904
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 49755 0 1 0 117883 123 0 0 25 0 1 0 478461918 206344192 49730 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50377 49730 603 41 0 50336 0
vsize: 201508
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 50555 0 1 0 118882 124 0 0 25 0 1 0 478461918 209616896 50530 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51176 50530 603 41 0 51135 0
vsize: 204704
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 24140
Raw data (stat): 24140 (minisat+) R 24139 22612 22611 0 -1 0 51421 0 1 0 119880 126 0 0 25 0 1 0 478461918 213180416 51396 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52046 51396 603 41 0 52005 0
vsize: 208184
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.69 1/54 24140
Raw data (stat): 24140 (minisat+) Z 24139 22612 22611 0 -1 12 51423 0 1 0 119880 136 0 0 25 0 1 0 478461918 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.12
CPU time (s): 1200.17
CPU user time (s): 1198.8
CPU system time (s): 1.36379
CPU usage (%): 100.004
Max. virtual memory (Kb): 208184
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####