Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
  1. LAUNCHER DATA
    These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. WATCHER DATA
    This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
    Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
    When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
  4. VERIFIER DATA
    The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.

General information on the benchmark

Namenormalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl40_41_pb.cnf.cr.opb
MD5SUM3c9e81ddaaf37dd621fe2bc839a3f27f
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 0
Biggest coefficient in the objective function 0
Number of bits for the biggest coefficient in the objective function 0
Sum of the numbers in the objective function 0
Number of bits of the sum of numbers in the objective function 0
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 42
Number of bits of the biggest sum of numbers6
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.098984
Number of variables3280
Total number of constraints162
Number of constraints which are clauses82
Number of constraints which are cardinality constraints (but not clauses)80
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint40
Maximum length of a constraint41

Trace number 4596 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-13 19:26:02 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3401 boxname=wulflinc18 idbench=17 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3c9e81ddaaf37dd621fe2bc839a3f27f  /oldhome/oroussel/tmp/wulflinc18/normalized-chnl40_41_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc18/normalized-chnl40_41_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc18/normalized-chnl40_41_pb.cnf.cr.opb
IDLAUNCH: 3401
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
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:        922124 kB
Buffers:         33876 kB
Cached:          43188 kB
SwapCached:        320 kB
Active:          47372 kB
Inactive:        32892 kB
HighTotal:      131008 kB
HighFree:        83748 kB
LowTotal:       903652 kB
LowFree:        838376 kB
SwapTotal:     2097892 kB
SwapFree:      2097572 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6936 kB
Slab:            26736 kB
Committed_AS:    63700 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 19:46:04 (client local time) WITH STATUS 0 IN 1200.17 SECONDS
stats: 3401 7 1200.17 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 162 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................................................
c ---[  79]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  78]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  77]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  76]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  75]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  74]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  73]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  72]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  71]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  70]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  69]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  68]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  67]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  66]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  65]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  64]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  63]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  62]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  61]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  60]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  59]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  58]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  57]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  56]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  55]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  54]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  53]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  52]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  51]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  50]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  49]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  48]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  47]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  46]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  45]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  44]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  43]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  42]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  41]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  40]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  39]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  38]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  37]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  36]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  35]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  34]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  33]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  32]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  31]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  30]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  29]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  28]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  27]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  26]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  25]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  24]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  23]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  22]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  21]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  20]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  19]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  18]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  17]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  16]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  15]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  14]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  13]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  12]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  11]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[  10]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[   9]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[   8]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[   7]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[   6]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[   5]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[   4]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[   3]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[   2]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[   1]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ---[   0]---> Adder-cost: 76   maxlim: 39   bits: 6/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   38322   139120 |   12774       0        0     nan |  0.000 % |
c |       100 |   37537   136343 |   14051       1        2     2.0 |  6.913 % |
c |       250 |   37102   134806 |   15456      94      326     3.5 |  7.859 % |
c |       475 |   37102   134806 |   17002     319     1184     3.7 |  7.859 % |
c |       812 |   36939   134239 |   18702     638     2558     4.0 |  8.185 % |
c |      1318 |   35523   129197 |   20572     992     5038     5.1 | 11.098 % |
c |      2077 |   33893   123421 |   22629    1558     8194     5.3 | 14.370 % |
c |      3216 |   29780   109238 |   24892    2066    12014     5.8 | 22.196 % |
c |      4924 |   24021    89753 |   27382    2892    19794     6.8 | 33.522 % |
c |      7486 |   17767    68665 |   30120    4491   142502    31.7 | 46.196 % |
c |     11333 |   17697    68439 |   33132    8326  1700816   204.3 | 46.359 % |
c |     17099 |   17672    68358 |   36445   14087  4044961   287.1 | 46.413 % |
c |     25748 |   17654    68300 |   40090   22734 10411007   457.9 | 46.457 % |
c |     38725 |   17654    68300 |   44099   35711 23771650   665.7 | 46.457 % |
c |     58186 |   17654    68300 |   48509   19328 17811091   921.5 | 46.457 % |
c |     87380 |   17654    68300 |   53360   48522 42905688   884.3 | 46.457 % |
#### 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/55 21828
Raw data (stat): 21828 (runsolver) R 21827 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 478450000 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/55 21828
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 1192 0 1 0 984 3 0 0 25 0 1 0 478450000 6807552 1168 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1662 1168 603 41 0 1621 0
vsize: 6648
[startup+20.0006 s]
Raw data (loadavg): 0.28 0.06 0.02 2/55 21828
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 1198 0 1 0 1983 3 0 0 25 0 1 0 478450000 6807552 1174 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1662 1174 603 41 0 1621 0
vsize: 6648
[startup+30.0013 s]
Raw data (loadavg): 0.39 0.09 0.03 2/55 21828
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 1231 0 1 0 2982 3 0 0 25 0 1 0 478450000 6942720 1207 4294967295 134512640 134672761 3221224544 3221223668 134566092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1695 1207 603 41 0 1654 0
vsize: 6780
[startup+40.0012 s]
Raw data (loadavg): 0.49 0.12 0.04 2/55 21828
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 3728 0 1 0 3976 9 0 0 25 0 1 0 478450000 17219584 3704 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4204 3705 603 41 0 4163 0
vsize: 16816
[startup+50.0021 s]
Raw data (loadavg): 0.56 0.15 0.05 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 6781 0 1 0 4969 16 0 0 25 0 1 0 478450000 29741056 6757 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7261 6757 603 41 0 7220 0
vsize: 29044
[startup+60.0023 s]
Raw data (loadavg): 0.63 0.18 0.06 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 9178 0 1 0 5964 22 0 0 25 0 1 0 478450000 39600128 9154 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9668 9154 603 41 0 9627 0
vsize: 38672
[startup+70.0029 s]
Raw data (loadavg): 0.69 0.21 0.07 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 11545 0 1 0 6959 26 0 0 25 0 1 0 478450000 49315840 11521 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12040 11521 603 41 0 11999 0
vsize: 48160
[startup+80.0038 s]
Raw data (loadavg): 0.73 0.23 0.08 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 12900 0 1 0 7956 30 0 0 25 0 1 0 478450000 54845440 12876 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13390 12876 603 41 0 13349 0
vsize: 53560
[startup+90.0037 s]
Raw data (loadavg): 0.77 0.26 0.09 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 14170 0 1 0 8954 32 0 0 25 0 1 0 478450000 59961344 14146 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14639 14146 603 41 0 14598 0
vsize: 58556
[startup+100.005 s]
Raw data (loadavg): 0.81 0.28 0.10 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 15289 0 1 0 9952 34 0 0 25 0 1 0 478450000 64565248 15265 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15763 15265 603 41 0 15722 0
vsize: 63052
[startup+110.006 s]
Raw data (loadavg): 0.84 0.30 0.11 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 16314 0 1 0 10951 36 0 0 25 0 1 0 478450000 68743168 16290 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16783 16290 603 41 0 16742 0
vsize: 67132
[startup+120.006 s]
Raw data (loadavg): 0.86 0.33 0.12 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 17347 0 1 0 11949 38 0 0 25 0 1 0 478450000 73089024 17323 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17844 17323 603 41 0 17803 0
vsize: 71376
[startup+130.006 s]
Raw data (loadavg): 0.88 0.35 0.12 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 18450 0 1 0 12946 41 0 0 25 0 1 0 478450000 77533184 18426 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18929 18426 603 41 0 18888 0
vsize: 75716
[startup+140.006 s]
Raw data (loadavg): 0.90 0.37 0.13 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 19438 0 1 0 13943 44 0 0 25 0 1 0 478450000 81584128 19414 4294967295 134512640 134672761 3221224544 3221223728 134559358 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19918 19415 603 41 0 19877 0
vsize: 79672
[startup+150.007 s]
Raw data (loadavg): 0.92 0.39 0.14 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 20294 0 1 0 14942 46 0 0 25 0 1 0 478450000 85114880 20270 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20780 20270 603 41 0 20739 0
vsize: 83120
[startup+160.007 s]
Raw data (loadavg): 0.93 0.41 0.15 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 21393 0 1 0 15940 47 0 0 25 0 1 0 478450000 89587712 21369 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21872 21369 603 41 0 21831 0
vsize: 87488
[startup+170.007 s]
Raw data (loadavg): 0.94 0.43 0.16 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 22245 0 1 0 16938 49 0 0 25 0 1 0 478450000 93229056 22221 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22761 22221 603 41 0 22720 0
vsize: 91044
[startup+180.008 s]
Raw data (loadavg): 0.95 0.45 0.17 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 22794 0 1 0 17938 50 0 0 25 0 1 0 478450000 95551488 22770 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23328 22770 603 41 0 23287 0
vsize: 93312
[startup+190.009 s]
Raw data (loadavg): 0.95 0.46 0.18 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 23425 0 1 0 18937 51 0 0 25 0 1 0 478450000 98115584 23401 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23954 23401 603 41 0 23913 0
vsize: 95816
[startup+200.01 s]
Raw data (loadavg): 0.96 0.48 0.19 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 24110 0 1 0 19935 53 0 0 25 0 1 0 478450000 100970496 24086 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24651 24086 603 41 0 24610 0
vsize: 98604
[startup+210.01 s]
Raw data (loadavg): 0.97 0.50 0.19 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 24783 0 1 0 20934 54 0 0 25 0 1 0 478450000 103682048 24759 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25313 24759 603 41 0 25272 0
vsize: 101252
[startup+220.01 s]
Raw data (loadavg): 0.97 0.51 0.20 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 25396 0 1 0 21933 56 0 0 25 0 1 0 478450000 106106880 25372 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25905 25372 603 41 0 25864 0
vsize: 103620
[startup+230.01 s]
Raw data (loadavg): 0.98 0.53 0.21 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 25884 0 1 0 22931 57 0 0 25 0 1 0 478450000 108146688 25860 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26403 25860 603 41 0 26362 0
vsize: 105612
[startup+240.011 s]
Raw data (loadavg): 0.98 0.54 0.22 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 26315 0 1 0 23930 58 0 0 25 0 1 0 478450000 109907968 26291 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26833 26291 603 41 0 26792 0
vsize: 107332
[startup+250.012 s]
Raw data (loadavg): 0.98 0.56 0.22 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 26717 0 1 0 24930 59 0 0 25 0 1 0 478450000 111534080 26693 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27230 26693 603 41 0 27189 0
vsize: 108920
[startup+260.013 s]
Raw data (loadavg): 0.98 0.57 0.23 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 27224 0 1 0 25929 60 0 0 25 0 1 0 478450000 113692672 27200 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27757 27200 603 41 0 27716 0
vsize: 111028
[startup+270.013 s]
Raw data (loadavg): 0.99 0.59 0.24 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 27804 0 1 0 26927 62 0 0 25 0 1 0 478450000 115998720 27780 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28320 27780 603 41 0 28279 0
vsize: 113280
[startup+280.014 s]
Raw data (loadavg): 0.99 0.60 0.25 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 28263 0 1 0 27927 63 0 0 25 0 1 0 478450000 117895168 28239 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28783 28239 603 41 0 28742 0
vsize: 115132
[startup+290.015 s]
Raw data (loadavg): 0.99 0.61 0.26 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 28782 0 1 0 28926 64 0 0 25 0 1 0 478450000 120061952 28758 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29312 28758 603 41 0 29271 0
vsize: 117248
[startup+300.015 s]
Raw data (loadavg): 0.99 0.62 0.26 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 29320 0 1 0 29925 65 0 0 25 0 1 0 478450000 122236928 29296 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29843 29296 603 41 0 29802 0
vsize: 119372
[startup+310.016 s]
Raw data (loadavg): 0.99 0.64 0.27 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 30133 0 1 0 30923 67 0 0 25 0 1 0 478450000 125640704 30109 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30674 30109 603 41 0 30633 0
vsize: 122696
[startup+320.015 s]
Raw data (loadavg): 0.99 0.65 0.28 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 30677 0 1 0 31923 68 0 0 25 0 1 0 478450000 127799296 30653 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31201 30653 603 41 0 31160 0
vsize: 124804
[startup+330.015 s]
Raw data (loadavg): 0.99 0.66 0.29 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 31208 0 1 0 32921 69 0 0 25 0 1 0 478450000 129970176 31184 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31731 31184 603 41 0 31690 0
vsize: 126924
[startup+340.015 s]
Raw data (loadavg): 0.99 0.67 0.29 2/55 21830
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 31937 0 1 0 33919 71 0 0 25 0 1 0 478450000 132956160 31913 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32460 31913 603 41 0 32419 0
vsize: 129840
[startup+350.015 s]
Raw data (loadavg): 0.99 0.68 0.30 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 32662 0 1 0 34918 73 0 0 25 0 1 0 478450000 135933952 32638 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33187 32638 603 41 0 33146 0
vsize: 132748
[startup+360.016 s]
Raw data (loadavg): 0.99 0.69 0.31 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 33156 0 1 0 35917 74 0 0 25 0 1 0 478450000 137965568 33132 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33683 33132 603 41 0 33642 0
vsize: 134732
[startup+370.016 s]
Raw data (loadavg): 0.99 0.70 0.31 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 33525 0 1 0 36916 75 0 0 25 0 1 0 478450000 139456512 33501 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34047 33501 603 41 0 34006 0
vsize: 136188
[startup+380.017 s]
Raw data (loadavg): 0.99 0.71 0.32 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 33849 0 1 0 37916 75 0 0 25 0 1 0 478450000 140808192 33825 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34377 33825 603 41 0 34336 0
vsize: 137508
[startup+390.017 s]
Raw data (loadavg): 0.99 0.72 0.33 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 34915 0 1 0 38914 77 0 0 25 0 1 0 478450000 145149952 34891 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35437 34891 603 41 0 35396 0
vsize: 141748
[startup+400.017 s]
Raw data (loadavg): 0.99 0.73 0.33 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 35942 0 1 0 39913 78 0 0 25 0 1 0 478450000 149356544 35918 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36464 35918 603 41 0 36423 0
vsize: 145856
[startup+410.016 s]
Raw data (loadavg): 0.99 0.74 0.34 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 36891 0 1 0 40911 81 0 0 25 0 1 0 478450000 153272320 36867 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37420 36867 603 41 0 37379 0
vsize: 149680
[startup+420.017 s]
Raw data (loadavg): 0.99 0.74 0.35 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 37734 0 1 0 41909 83 0 0 25 0 1 0 478450000 156794880 37710 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38280 37710 603 41 0 38239 0
vsize: 153120
[startup+430.018 s]
Raw data (loadavg): 0.99 0.75 0.35 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 38610 0 1 0 42907 85 0 0 25 0 1 0 478450000 160280576 38586 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39131 38586 603 41 0 39090 0
vsize: 156524
[startup+440.017 s]
Raw data (loadavg): 0.99 0.76 0.36 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 39338 0 1 0 43906 86 0 0 25 0 1 0 478450000 163254272 39314 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39857 39314 603 41 0 39816 0
vsize: 159428
[startup+450.017 s]
Raw data (loadavg): 0.99 0.77 0.37 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40167 0 1 0 44904 88 0 0 25 0 1 0 478450000 166633472 40143 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40682 40143 603 41 0 40641 0
vsize: 162728
[startup+460.018 s]
Raw data (loadavg): 0.99 0.77 0.37 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40421 0 1 0 45904 89 0 0 25 0 1 0 478450000 167706624 40397 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40397 603 41 0 40903 0
vsize: 163776
[startup+470.018 s]
Raw data (loadavg): 0.99 0.78 0.38 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40422 0 1 0 46904 89 0 0 25 0 1 0 478450000 167706624 40398 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40398 603 41 0 40903 0
vsize: 163776
[startup+480.018 s]
Raw data (loadavg): 0.99 0.79 0.38 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 47904 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+490.019 s]
Raw data (loadavg): 0.99 0.79 0.39 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 48904 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+500.019 s]
Raw data (loadavg): 0.99 0.80 0.40 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 49905 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223728 134559538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+510.019 s]
Raw data (loadavg): 0.99 0.81 0.40 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 50905 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+520.019 s]
Raw data (loadavg): 0.99 0.81 0.41 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 51904 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+530.019 s]
Raw data (loadavg): 0.99 0.82 0.41 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 52904 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+540.02 s]
Raw data (loadavg): 0.99 0.82 0.42 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 53905 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+550.019 s]
Raw data (loadavg): 0.99 0.83 0.43 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 54905 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+560.02 s]
Raw data (loadavg): 0.99 0.83 0.43 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 55905 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+570.02 s]
Raw data (loadavg): 0.99 0.84 0.44 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 56905 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+580.021 s]
Raw data (loadavg): 0.99 0.84 0.44 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 57905 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+590.022 s]
Raw data (loadavg): 0.99 0.85 0.45 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 58905 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+600.022 s]
Raw data (loadavg): 0.99 0.85 0.45 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 59905 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+610.023 s]
Raw data (loadavg): 0.99 0.86 0.46 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 60906 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+620.023 s]
Raw data (loadavg): 0.99 0.86 0.46 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 61906 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+630.024 s]
Raw data (loadavg): 0.99 0.86 0.47 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 62906 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+640.024 s]
Raw data (loadavg): 0.99 0.87 0.47 2/55 21832
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 63906 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+650.023 s]
Raw data (loadavg): 0.99 0.87 0.48 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 64906 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+660.025 s]
Raw data (loadavg): 0.99 0.88 0.48 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 65906 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+670.024 s]
Raw data (loadavg): 0.99 0.88 0.49 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 66907 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+680.025 s]
Raw data (loadavg): 0.99 0.88 0.49 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 67907 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+690.025 s]
Raw data (loadavg): 0.99 0.89 0.50 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 68907 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223648 134554900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+700.025 s]
Raw data (loadavg): 0.99 0.89 0.50 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 69907 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+710.026 s]
Raw data (loadavg): 0.99 0.89 0.51 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 70907 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+720.026 s]
Raw data (loadavg): 0.99 0.90 0.51 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 71908 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+730.027 s]
Raw data (loadavg): 0.99 0.90 0.52 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 72908 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+740.026 s]
Raw data (loadavg): 0.99 0.90 0.52 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 73908 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+750.027 s]
Raw data (loadavg): 0.99 0.90 0.53 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 74908 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+760.028 s]
Raw data (loadavg): 0.99 0.91 0.53 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40423 0 1 0 75908 89 0 0 25 0 1 0 478450000 167706624 40399 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40399 603 41 0 40903 0
vsize: 163776
[startup+770.027 s]
Raw data (loadavg): 0.99 0.91 0.54 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40424 0 1 0 76909 89 0 0 25 0 1 0 478450000 167706624 40400 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40400 603 41 0 40903 0
vsize: 163776
[startup+780.028 s]
Raw data (loadavg): 0.99 0.91 0.54 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40424 0 1 0 77909 89 0 0 25 0 1 0 478450000 167706624 40400 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40400 603 41 0 40903 0
vsize: 163776
[startup+790.028 s]
Raw data (loadavg): 0.99 0.91 0.55 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40424 0 1 0 78909 89 0 0 25 0 1 0 478450000 167706624 40400 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40944 40400 603 41 0 40903 0
vsize: 163776
[startup+800.028 s]
Raw data (loadavg): 0.99 0.92 0.55 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 40585 0 1 0 79909 89 0 0 25 0 1 0 478450000 168370176 40561 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41106 40561 603 41 0 41065 0
vsize: 164424
[startup+810.028 s]
Raw data (loadavg): 0.99 0.92 0.56 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 41023 0 1 0 80908 90 0 0 25 0 1 0 478450000 170246144 40999 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41564 40999 603 41 0 41523 0
vsize: 166256
[startup+820.028 s]
Raw data (loadavg): 0.99 0.92 0.56 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 41466 0 1 0 81908 91 0 0 25 0 1 0 478450000 171995136 41442 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41991 41442 603 41 0 41950 0
vsize: 167964
[startup+830.029 s]
Raw data (loadavg): 0.99 0.92 0.56 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 41961 0 1 0 82907 92 0 0 25 0 1 0 478450000 174026752 41937 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42487 41937 603 41 0 42446 0
vsize: 169948
[startup+840.029 s]
Raw data (loadavg): 0.99 0.92 0.57 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 42466 0 1 0 83906 93 0 0 25 0 1 0 478450000 176181248 42442 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43013 42442 603 41 0 42972 0
vsize: 172052
[startup+850.029 s]
Raw data (loadavg): 0.99 0.93 0.57 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 43012 0 1 0 84905 94 0 0 25 0 1 0 478450000 178466816 42988 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43571 42988 603 41 0 43530 0
vsize: 174284
[startup+860.029 s]
Raw data (loadavg): 0.99 0.93 0.58 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 43643 0 1 0 85903 96 0 0 25 0 1 0 478450000 181035008 43619 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44198 43619 603 41 0 44157 0
vsize: 176792
[startup+870.029 s]
Raw data (loadavg): 0.99 0.93 0.58 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 44431 0 1 0 86902 98 0 0 25 0 1 0 478450000 184295424 44407 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44994 44407 603 41 0 44953 0
vsize: 179976
[startup+880.03 s]
Raw data (loadavg): 0.99 0.93 0.58 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 44991 0 1 0 87900 99 0 0 25 0 1 0 478450000 186658816 44967 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45571 44967 603 41 0 45530 0
vsize: 182284
[startup+890.03 s]
Raw data (loadavg): 0.99 0.93 0.59 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 45649 0 1 0 88899 100 0 0 25 0 1 0 478450000 189325312 45625 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46222 45625 603 41 0 46181 0
vsize: 184888
[startup+900.03 s]
Raw data (loadavg): 0.99 0.94 0.59 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 46087 0 1 0 89899 101 0 0 25 0 1 0 478450000 191086592 46063 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46652 46063 603 41 0 46611 0
vsize: 186608
[startup+910.031 s]
Raw data (loadavg): 0.99 0.94 0.59 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 46674 0 1 0 90897 103 0 0 25 0 1 0 478450000 193495040 46650 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47240 46650 603 41 0 47199 0
vsize: 188960
[startup+920.031 s]
Raw data (loadavg): 0.99 0.94 0.60 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 47407 0 1 0 91896 104 0 0 25 0 1 0 478450000 196456448 47383 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47963 47383 603 41 0 47922 0
vsize: 191852
[startup+930.032 s]
Raw data (loadavg): 0.99 0.94 0.60 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 48050 0 1 0 92895 105 0 0 25 0 1 0 478450000 199172096 48026 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48626 48026 603 41 0 48585 0
vsize: 194504
[startup+940.033 s]
Raw data (loadavg): 0.99 0.94 0.61 2/55 21834
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 48845 0 1 0 93894 107 0 0 25 0 1 0 478450000 202416128 48821 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49418 48821 603 41 0 49377 0
vsize: 197672
[startup+950.033 s]
Raw data (loadavg): 0.99 0.94 0.61 2/55 21836
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 49630 0 1 0 94892 109 0 0 25 0 1 0 478450000 205574144 49606 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50189 49606 603 41 0 50148 0
vsize: 200756
[startup+960.034 s]
Raw data (loadavg): 0.99 0.94 0.61 2/55 21836
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 50275 0 1 0 95891 110 0 0 25 0 1 0 478450000 208297984 50251 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50854 50251 603 41 0 50813 0
vsize: 203416
[startup+970.035 s]
Raw data (loadavg): 0.99 0.95 0.62 2/55 21836
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 50941 0 1 0 96890 112 0 0 25 0 1 0 478450000 211148800 50917 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51550 50917 603 41 0 51509 0
vsize: 206200
[startup+980.035 s]
Raw data (loadavg): 0.99 0.95 0.62 2/55 21836
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 51372 0 1 0 97888 113 0 0 25 0 1 0 478450000 212897792 51348 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51977 51348 603 41 0 51936 0
vsize: 207908
[startup+990.035 s]
Raw data (loadavg): 0.99 0.95 0.63 2/55 21836
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 51907 0 1 0 98887 114 0 0 25 0 1 0 478450000 215093248 51883 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52513 51883 603 41 0 52472 0
vsize: 210052
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.95 0.63 2/55 21836
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 52438 0 1 0 99887 115 0 0 25 0 1 0 478450000 217251840 52414 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53040 52414 603 41 0 52999 0
vsize: 212160
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.95 0.63 2/55 21836
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 53020 0 1 0 100885 117 0 0 25 0 1 0 478450000 219590656 52996 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53611 52996 603 41 0 53570 0
vsize: 214444
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.95 0.64 2/55 21836
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 53464 0 1 0 101884 118 0 0 25 0 1 0 478450000 221478912 53440 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54072 53440 603 41 0 54031 0
vsize: 216288
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.95 0.64 2/55 21836
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 53845 0 1 0 102884 118 0 0 25 0 1 0 478450000 222957568 53821 4294967295 134512640 134672761 3221224544 3221223648 134554656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54433 53821 603 41 0 54392 0
vsize: 217732
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.95 0.64 2/55 21836
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 53845 0 1 0 103885 118 0 0 25 0 1 0 478450000 222957568 53821 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54433 53821 603 41 0 54392 0
vsize: 217732
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.95 0.65 2/55 21836
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 53845 0 1 0 104885 118 0 0 25 0 1 0 478450000 222957568 53821 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54433 53821 603 41 0 54392 0
vsize: 217732
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.95 0.65 2/55 21836
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 53846 0 1 0 105885 118 0 0 25 0 1 0 478450000 222957568 53822 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54433 53822 603 41 0 54392 0
vsize: 217732
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.96 0.65 2/55 21836
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 53846 0 1 0 106885 118 0 0 25 0 1 0 478450000 222957568 53822 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54433 53822 603 41 0 54392 0
vsize: 217732
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.96 0.66 2/55 21836
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 53850 0 1 0 107885 118 0 0 25 0 1 0 478450000 222957568 53826 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54433 53826 603 41 0 54392 0
vsize: 217732
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.96 0.66 2/55 21836
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 53850 0 1 0 108886 118 0 0 25 0 1 0 478450000 222957568 53826 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54433 53826 603 41 0 54392 0
vsize: 217732
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.96 0.66 2/55 21836
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 53852 0 1 0 109886 118 0 0 25 0 1 0 478450000 222957568 53828 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54433 53828 603 41 0 54392 0
vsize: 217732
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.96 0.66 2/55 21836
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 53852 0 1 0 110886 118 0 0 25 0 1 0 478450000 222957568 53828 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54433 53828 603 41 0 54392 0
vsize: 217732
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.96 0.67 2/55 21836
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 53854 0 1 0 111886 118 0 0 25 0 1 0 478450000 222957568 53830 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54433 53830 603 41 0 54392 0
vsize: 217732
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.96 0.67 2/55 21836
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 53854 0 1 0 112886 118 0 0 25 0 1 0 478450000 222957568 53830 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54433 53830 603 41 0 54392 0
vsize: 217732
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.96 0.67 2/55 21836
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 53854 0 1 0 113886 118 0 0 25 0 1 0 478450000 222957568 53830 4294967295 134512640 134672761 3221224544 3221223728 134559019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54433 53830 603 41 0 54392 0
vsize: 217732
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.96 0.68 2/55 21836
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 53854 0 1 0 114887 118 0 0 25 0 1 0 478450000 222957568 53830 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54433 53830 603 41 0 54392 0
vsize: 217732
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.96 0.68 2/55 21836
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 53854 0 1 0 115887 118 0 0 25 0 1 0 478450000 222957568 53830 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54433 53830 603 41 0 54392 0
vsize: 217732
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.68 2/55 21836
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 53854 0 1 0 116887 118 0 0 25 0 1 0 478450000 222957568 53830 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54433 53830 603 41 0 54392 0
vsize: 217732
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.68 2/55 21836
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 53854 0 1 0 117887 118 0 0 25 0 1 0 478450000 222957568 53830 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54433 53830 603 41 0 54392 0
vsize: 217732
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.69 2/55 21836
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 53854 0 1 0 118888 118 0 0 25 0 1 0 478450000 222957568 53830 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54433 53830 603 41 0 54392 0
vsize: 217732
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.69 2/55 21836
Raw data (stat): 21828 (minisat+) R 21827 20024 20023 0 -1 0 53854 0 1 0 119888 118 0 0 25 0 1 0 478450000 222957568 53830 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54433 53830 603 41 0 54392 0
vsize: 217732
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.97 0.69 1/55 21836
Raw data (stat): 21828 (minisat+) Z 21827 20024 20023 0 -1 12 53856 0 1 0 119888 128 0 0 25 0 1 0 478450000 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.14
CPU time (s): 1200.17
CPU user time (s): 1198.88
CPU system time (s): 1.2848
CPU usage (%): 100.002
Max. virtual memory (Kb): 217732
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####