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_45_pb.cnf.cr.opb
MD5SUMdf5f31774bab40070962f7d0b16d093c
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 46
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.107983
Number of variables3600
Total number of constraints170
Number of constraints which are clauses90
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 constraint45

Trace number 6151 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-14 03:31:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4530 boxname=wulflinc11 idbench=18 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  df5f31774bab40070962f7d0b16d093c  /oldhome/oroussel/tmp/wulflinc11/normalized-chnl40_45_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc11/normalized-chnl40_45_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc11/normalized-chnl40_45_pb.cnf.cr.opb
IDLAUNCH: 4530
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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	: 2
cpu MHz		: 451.028
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:        906920 kB
Buffers:         36192 kB
Cached:          67200 kB
SwapCached:       4932 kB
Active:          57312 kB
Inactive:        53836 kB
HighTotal:      131008 kB
HighFree:        59976 kB
LowTotal:       903652 kB
LowFree:        846944 kB
SwapTotal:     2097136 kB
SwapFree:      2092204 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            10900 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:51:13 (client local time) WITH STATUS 0 IN 1200.22 SECONDS
stats: 4530 7 1200.22 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 170 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..........................................................................................
c ---[  79]---> BDD-cost:   87
c ---[  78]---> BDD-cost:   87
c ---[  77]---> BDD-cost:   87
c ---[  76]---> BDD-cost:   87
c ---[  75]---> BDD-cost:   87
c ---[  74]---> BDD-cost:   87
c ---[  73]---> BDD-cost:   87
c ---[  72]---> BDD-cost:   87
c ---[  71]---> BDD-cost:   87
c ---[  70]---> BDD-cost:   87
c ---[  69]---> BDD-cost:   87
c ---[  68]---> BDD-cost:   87
c ---[  67]---> BDD-cost:   87
c ---[  66]---> BDD-cost:   87
c ---[  65]---> BDD-cost:   87
c ---[  64]---> BDD-cost:   87
c ---[  63]---> BDD-cost:   87
c ---[  62]---> BDD-cost:   87
c ---[  61]---> BDD-cost:   87
c ---[  60]---> BDD-cost:   87
c ---[  59]---> BDD-cost:   87
c ---[  58]---> BDD-cost:   87
c ---[  57]---> BDD-cost:   87
c ---[  56]---> BDD-cost:   87
c ---[  55]---> BDD-cost:   87
c ---[  54]---> BDD-cost:   87
c ---[  53]---> BDD-cost:   87
c ---[  52]---> BDD-cost:   87
c ---[  51]---> BDD-cost:   87
c ---[  50]---> BDD-cost:   87
c ---[  49]---> BDD-cost:   87
c ---[  48]---> BDD-cost:   87
c ---[  47]---> BDD-cost:   87
c ---[  46]---> BDD-cost:   87
c ---[  45]---> BDD-cost:   87
c ---[  44]---> BDD-cost:   87
c ---[  43]---> BDD-cost:   87
c ---[  42]---> BDD-cost:   87
c ---[  41]---> BDD-cost:   87
c ---[  40]---> BDD-cost:   87
c ---[  39]---> BDD-cost:   87
c ---[  38]---> BDD-cost:   87
c ---[  37]---> BDD-cost:   87
c ---[  36]---> BDD-cost:   87
c ---[  35]---> BDD-cost:   87
c ---[  34]---> BDD-cost:   87
c ---[  33]---> BDD-cost:   87
c ---[  32]---> BDD-cost:   87
c ---[  31]---> BDD-cost:   87
c ---[  30]---> BDD-cost:   87
c ---[  29]---> BDD-cost:   87
c ---[  28]---> BDD-cost:   87
c ---[  27]---> BDD-cost:   87
c ---[  26]---> BDD-cost:   87
c ---[  25]---> BDD-cost:   87
c ---[  24]---> BDD-cost:   87
c ---[  23]---> BDD-cost:   87
c ---[  22]---> BDD-cost:   87
c ---[  21]---> BDD-cost:   87
c ---[  20]---> BDD-cost:   87
c ---[  19]---> BDD-cost:   87
c ---[  18]---> BDD-cost:   87
c ---[  17]---> BDD-cost:   87
c ---[  16]---> BDD-cost:   87
c ---[  15]---> BDD-cost:   87
c ---[  14]---> BDD-cost:   87
c ---[  13]---> BDD-cost:   87
c ---[  12]---> BDD-cost:   87
c ---[  11]---> BDD-cost:   87
c ---[  10]---> BDD-cost:   87
c ---[   9]---> BDD-cost:   87
c ---[   8]---> BDD-cost:   87
c ---[   7]---> BDD-cost:   87
c ---[   6]---> BDD-cost:   87
c ---[   5]---> BDD-cost:   87
c ---[   4]---> BDD-cost:   87
c ---[   3]---> BDD-cost:   87
c ---[   2]---> BDD-cost:   87
c ---[   1]---> BDD-cost:   87
c ---[   0]---> BDD-cost:   87
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   31050    89440 |   10350       0        0     nan |  0.000 % |
c |       100 |   30745    88525 |   11385       7       15     2.1 |  1.345 % |
c |       250 |   30365    87385 |   12523      18       41     2.3 |  2.055 % |
c |       475 |   29750    85540 |   13775      36       86     2.4 |  3.229 % |
c |       813 |   29305    84205 |   15153     217    25261   116.4 |  4.063 % |
c |      1320 |   28730    82480 |   16668     535    83456   156.0 |  5.152 % |
c |      2079 |   28620    82150 |   18335    1250   268069   214.5 |  5.360 % |
c |      3221 |   28060    80470 |   20169    2162   430715   199.2 |  6.420 % |
c |      4929 |   27495    78775 |   22186    3654   781855   214.0 |  7.491 % |
c |      7493 |   26565    75985 |   24404    5892  1319099   223.9 |  9.252 % |
c |     11338 |   25020    71350 |   26845    9203  2200913   239.2 | 12.178 % |
c |     17104 |   23325    66265 |   29529   14409  3611532   250.6 | 15.388 % |
c |     25753 |   21466    60690 |   32482   22459  6293342   280.2 | 18.911 % |
c |     38727 |   20227    56975 |   35731   35014 10328228   295.0 | 21.259 % |
c |     58188 |   18788    52660 |   39304   25546  8175374   320.0 | 23.987 % |
c |     87383 |   17264    48090 |   43234   24209  8566180   353.8 | 26.875 % |
c |    131172 |   16565    45995 |   47557   33500 12860011   383.9 | 28.201 % |
c |    196856 |   16071    44515 |   52313   17385  6319087   363.5 | 29.138 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.93 2/54 6932
Raw data (stat): 6932 (runsolver) R 6931 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423145402 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.87 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 1609 0 0 0 993 5 0 0 25 0 1 0 423145402 8335360 1584 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2035 1584 603 41 0 1994 0
vsize: 8140
[startup+20.0005 s]
Raw data (loadavg): 0.89 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 2131 0 0 0 1992 6 0 0 25 0 1 0 423145402 10498048 2106 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2563 2106 603 41 0 2522 0
vsize: 10252
[startup+30.0009 s]
Raw data (loadavg): 0.91 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 2804 0 0 0 2990 8 0 0 25 0 1 0 423145402 13332480 2779 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3255 2779 603 41 0 3214 0
vsize: 13020
[startup+40.0007 s]
Raw data (loadavg): 0.92 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 3248 0 0 0 3988 10 0 0 25 0 1 0 423145402 15085568 3223 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3683 3223 603 41 0 3642 0
vsize: 14732
[startup+50.002 s]
Raw data (loadavg): 0.93 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 3618 0 0 0 4987 11 0 0 25 0 1 0 423145402 16703488 3593 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4078 3593 603 41 0 4037 0
vsize: 16312
[startup+60.0023 s]
Raw data (loadavg): 0.94 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 3817 0 0 0 5986 12 0 0 25 0 1 0 423145402 17514496 3792 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4276 3792 603 41 0 4235 0
vsize: 17104
[startup+70.002 s]
Raw data (loadavg): 0.95 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 4063 0 0 0 6985 13 0 0 25 0 1 0 423145402 18456576 4038 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4506 4038 603 41 0 4465 0
vsize: 18024
[startup+80.0033 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 4430 0 0 0 7985 14 0 0 25 0 1 0 423145402 19943424 4405 4294967295 134512640 134672761 3221224544 3221223648 134559877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4869 4405 603 41 0 4828 0
vsize: 19476
[startup+90.0026 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 5019 0 0 0 8983 16 0 0 25 0 1 0 423145402 22364160 4994 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5460 4994 603 41 0 5419 0
vsize: 21840
[startup+100.003 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 5613 0 0 0 9981 18 0 0 25 0 1 0 423145402 24780800 5588 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6050 5588 603 41 0 6009 0
vsize: 24200
[startup+110.005 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 5881 0 0 0 10981 18 0 0 25 0 1 0 423145402 26005504 5856 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6349 5856 603 41 0 6308 0
vsize: 25396
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 6320 0 0 0 11979 20 0 0 25 0 1 0 423145402 27762688 6295 4294967295 134512640 134672761 3221224544 3221223648 134559991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6778 6295 603 41 0 6737 0
vsize: 27112
[startup+130.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 6696 0 0 0 12978 21 0 0 25 0 1 0 423145402 29245440 6671 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7140 6671 603 41 0 7099 0
vsize: 28560
[startup+140.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 7108 0 0 0 13977 22 0 0 25 0 1 0 423145402 31002624 7083 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7569 7083 603 41 0 7528 0
vsize: 30276
[startup+150.004 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 7229 0 0 0 14977 22 0 0 25 0 1 0 423145402 31404032 7204 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7667 7204 603 41 0 7626 0
vsize: 30668
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 7600 0 0 0 15976 23 0 0 25 0 1 0 423145402 33026048 7575 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8063 7575 603 41 0 8022 0
vsize: 32252
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 8218 0 0 0 16975 25 0 0 25 0 1 0 423145402 35450880 8193 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8655 8193 603 41 0 8614 0
vsize: 34620
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 8887 0 0 0 17973 26 0 0 25 0 1 0 423145402 38277120 8862 4294967295 134512640 134672761 3221224544 3221223648 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9345 8862 603 41 0 9304 0
vsize: 37380
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 8889 0 0 0 18972 27 0 0 25 0 1 0 423145402 38277120 8864 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9345 8864 603 41 0 9304 0
vsize: 37380
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 9023 0 0 0 19972 27 0 0 25 0 1 0 423145402 38817792 8998 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9477 8998 603 41 0 9436 0
vsize: 37908
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 9633 0 0 0 20971 28 0 0 25 0 1 0 423145402 41254912 9608 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10072 9608 603 41 0 10031 0
vsize: 40288
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 9940 0 0 0 21970 29 0 0 25 0 1 0 423145402 42471424 9915 4294967295 134512640 134672761 3221224544 3221223648 134559916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10369 9915 603 41 0 10328 0
vsize: 41476
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 10741 0 0 0 22967 32 0 0 25 0 1 0 423145402 45838336 10716 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11191 10716 603 41 0 11150 0
vsize: 44764
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 10985 0 0 0 23966 34 0 0 25 0 1 0 423145402 46780416 10960 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11421 10960 603 41 0 11380 0
vsize: 45684
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 11443 0 0 0 24963 36 0 0 25 0 1 0 423145402 48672768 11418 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11883 11418 603 41 0 11842 0
vsize: 47532
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 11552 0 0 0 25963 37 0 0 25 0 1 0 423145402 49078272 11527 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11982 11527 603 41 0 11941 0
vsize: 47928
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 12166 0 0 0 26961 38 0 0 25 0 1 0 423145402 51765248 12141 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12638 12141 603 41 0 12597 0
vsize: 50552
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 12683 0 0 0 27960 40 0 0 25 0 1 0 423145402 53919744 12658 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13164 12658 603 41 0 13123 0
vsize: 52656
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 12790 0 0 0 28960 40 0 0 25 0 1 0 423145402 54325248 12765 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13263 12765 603 41 0 13222 0
vsize: 53052
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 12897 0 0 0 29959 41 0 0 25 0 1 0 423145402 54734848 12872 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13363 12872 603 41 0 13322 0
vsize: 53452
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 13160 0 0 0 30958 42 0 0 25 0 1 0 423145402 55812096 13135 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13626 13135 603 41 0 13585 0
vsize: 54504
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 13394 0 0 0 31957 43 0 0 25 0 1 0 423145402 56758272 13369 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13857 13369 603 41 0 13816 0
vsize: 55428
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 13702 0 0 0 32956 44 0 0 25 0 1 0 423145402 57970688 13677 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14153 13677 603 41 0 14112 0
vsize: 56612
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 14014 0 0 0 33955 45 0 0 25 0 1 0 423145402 59330560 13989 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14485 13989 603 41 0 14444 0
vsize: 57940
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 14785 0 0 0 34954 47 0 0 25 0 1 0 423145402 62423040 14760 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15240 14760 603 41 0 15199 0
vsize: 60960
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 14785 0 0 0 35954 47 0 0 25 0 1 0 423145402 62423040 14760 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15240 14760 603 41 0 15199 0
vsize: 60960
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 14785 0 0 0 36954 47 0 0 25 0 1 0 423145402 62423040 14760 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15240 14760 603 41 0 15199 0
vsize: 60960
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 14785 0 0 0 37954 47 0 0 25 0 1 0 423145402 62423040 14760 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15240 14760 603 41 0 15199 0
vsize: 60960
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 14785 0 0 0 38954 47 0 0 25 0 1 0 423145402 62423040 14760 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15240 14760 603 41 0 15199 0
vsize: 60960
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 14785 0 0 0 39955 47 0 0 25 0 1 0 423145402 62423040 14760 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15240 14760 603 41 0 15199 0
vsize: 60960
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 14785 0 0 0 40955 47 0 0 25 0 1 0 423145402 62423040 14760 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15240 14760 603 41 0 15199 0
vsize: 60960
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 14785 0 0 0 41955 47 0 0 25 0 1 0 423145402 62423040 14760 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15240 14760 603 41 0 15199 0
vsize: 60960
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 14785 0 0 0 42955 47 0 0 25 0 1 0 423145402 62423040 14760 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15240 14760 603 41 0 15199 0
vsize: 60960
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 14785 0 0 0 43955 47 0 0 25 0 1 0 423145402 62423040 14760 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15240 14760 603 41 0 15199 0
vsize: 60960
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 14785 0 0 0 44955 47 0 0 25 0 1 0 423145402 62423040 14760 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15240 14760 603 41 0 15199 0
vsize: 60960
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 14785 0 0 0 45955 47 0 0 25 0 1 0 423145402 62423040 14760 4294967295 134512640 134672761 3221224544 3221223648 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15240 14760 603 41 0 15199 0
vsize: 60960
[startup+470.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 14826 0 0 0 46955 47 0 0 25 0 1 0 423145402 62558208 14801 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15273 14801 603 41 0 15232 0
vsize: 61092
[startup+480.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 15768 0 0 0 47953 50 0 0 25 0 1 0 423145402 66469888 15743 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16228 15743 603 41 0 16187 0
vsize: 64912
[startup+490.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 16005 0 0 0 48953 50 0 0 25 0 1 0 423145402 67420160 15980 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16460 15980 603 41 0 16419 0
vsize: 65840
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 16005 0 0 0 49953 50 0 0 25 0 1 0 423145402 67420160 15980 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16460 15980 603 41 0 16419 0
vsize: 65840
[startup+510.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 16077 0 0 0 50953 50 0 0 25 0 1 0 423145402 67690496 16052 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16526 16052 603 41 0 16485 0
vsize: 66104
[startup+520.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 16492 0 0 0 51952 51 0 0 25 0 1 0 423145402 69443584 16467 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16954 16467 603 41 0 16913 0
vsize: 67816
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 16517 0 0 0 52953 51 0 0 25 0 1 0 423145402 69582848 16492 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16988 16492 603 41 0 16947 0
vsize: 67952
[startup+540.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 16823 0 0 0 53952 52 0 0 25 0 1 0 423145402 70795264 16798 4294967295 134512640 134672761 3221224544 3221223648 134559979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17284 16798 603 41 0 17243 0
vsize: 69136
[startup+550.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 17034 0 0 0 54951 53 0 0 25 0 1 0 423145402 71606272 17009 4294967295 134512640 134672761 3221224544 3221223728 134558930 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17482 17009 603 41 0 17441 0
vsize: 69928
[startup+560.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 17034 0 0 0 55952 53 0 0 25 0 1 0 423145402 71606272 17009 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17482 17009 603 41 0 17441 0
vsize: 69928
[startup+570.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 17034 0 0 0 56952 53 0 0 25 0 1 0 423145402 71606272 17009 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17482 17009 603 41 0 17441 0
vsize: 69928
[startup+580.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 17034 0 0 0 57952 53 0 0 25 0 1 0 423145402 71606272 17009 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17482 17009 603 41 0 17441 0
vsize: 69928
[startup+590.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 17034 0 0 0 58952 53 0 0 25 0 1 0 423145402 71606272 17009 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17482 17009 603 41 0 17441 0
vsize: 69928
[startup+600.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 17034 0 0 0 59952 53 0 0 25 0 1 0 423145402 71606272 17009 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17482 17009 603 41 0 17441 0
vsize: 69928
[startup+610.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 17034 0 0 0 60952 53 0 0 25 0 1 0 423145402 71606272 17009 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17482 17009 603 41 0 17441 0
vsize: 69928
[startup+620.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 17034 0 0 0 61952 53 0 0 25 0 1 0 423145402 71606272 17009 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17482 17009 603 41 0 17441 0
vsize: 69928
[startup+630.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 17034 0 0 0 62952 53 0 0 25 0 1 0 423145402 71606272 17009 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17482 17009 603 41 0 17441 0
vsize: 69928
[startup+640.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 17034 0 0 0 63953 53 0 0 25 0 1 0 423145402 71606272 17009 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17482 17009 603 41 0 17441 0
vsize: 69928
[startup+650.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 17034 0 0 0 64953 53 0 0 25 0 1 0 423145402 71606272 17009 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17482 17009 603 41 0 17441 0
vsize: 69928
[startup+660.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 18011 0 0 0 65951 55 0 0 25 0 1 0 423145402 75653120 17986 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18470 17986 603 41 0 18429 0
vsize: 73880
[startup+670.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 18310 0 0 0 66950 56 0 0 25 0 1 0 423145402 76886016 18285 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18771 18285 603 41 0 18730 0
vsize: 75084
[startup+680.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 18898 0 0 0 67949 57 0 0 25 0 1 0 423145402 79319040 18873 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19365 18873 603 41 0 19324 0
vsize: 77460
[startup+690.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 19711 0 0 0 68948 58 0 0 25 0 1 0 423145402 82690048 19686 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20188 19686 603 41 0 20147 0
vsize: 80752
[startup+700.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 20760 0 0 0 69946 60 0 0 25 0 1 0 423145402 87015424 20735 4294967295 134512640 134672761 3221224544 3221223648 134559953 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21244 20736 603 41 0 21203 0
vsize: 84976
[startup+710.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 21545 0 0 0 70945 61 0 0 25 0 1 0 423145402 90120192 21520 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22002 21520 603 41 0 21961 0
vsize: 88008
[startup+720.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 21545 0 0 0 71946 61 0 0 25 0 1 0 423145402 90120192 21520 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22002 21520 603 41 0 21961 0
vsize: 88008
[startup+730.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 21545 0 0 0 72946 61 0 0 25 0 1 0 423145402 90120192 21520 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22002 21520 603 41 0 21961 0
vsize: 88008
[startup+740.017 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 21545 0 0 0 73946 61 0 0 25 0 1 0 423145402 90120192 21520 4294967295 134512640 134672761 3221224544 3221223648 134559841 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22002 21520 603 41 0 21961 0
vsize: 88008
[startup+750.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 21545 0 0 0 74946 61 0 0 25 0 1 0 423145402 90120192 21520 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22002 21520 603 41 0 21961 0
vsize: 88008
[startup+760.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 21545 0 0 0 75946 61 0 0 25 0 1 0 423145402 90120192 21520 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22002 21520 603 41 0 21961 0
vsize: 88008
[startup+770.018 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 21545 0 0 0 76947 61 0 0 25 0 1 0 423145402 90120192 21520 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22002 21520 603 41 0 21961 0
vsize: 88008
[startup+780.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 21545 0 0 0 77946 62 0 0 25 0 1 0 423145402 90120192 21520 4294967295 134512640 134672761 3221224544 3221223648 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22002 21520 603 41 0 21961 0
vsize: 88008
[startup+790.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 21545 0 0 0 78946 62 0 0 25 0 1 0 423145402 90120192 21520 4294967295 134512640 134672761 3221224544 3221223648 134560520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22002 21520 603 41 0 21961 0
vsize: 88008
[startup+800.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 21545 0 0 0 79946 62 0 0 25 0 1 0 423145402 90120192 21520 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22002 21520 603 41 0 21961 0
vsize: 88008
[startup+810.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 21545 0 0 0 80947 62 0 0 25 0 1 0 423145402 90120192 21520 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22002 21520 603 41 0 21961 0
vsize: 88008
[startup+820.019 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 21545 0 0 0 81947 62 0 0 25 0 1 0 423145402 90120192 21520 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22002 21520 603 41 0 21961 0
vsize: 88008
[startup+830.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 22103 0 0 0 82946 63 0 0 25 0 1 0 423145402 92536832 22078 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22592 22078 603 41 0 22551 0
vsize: 90368
[startup+840.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 22751 0 0 0 83945 64 0 0 25 0 1 0 423145402 95092736 22726 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23216 22726 603 41 0 23175 0
vsize: 92864
[startup+850.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 23170 0 0 0 84945 65 0 0 25 0 1 0 423145402 96858112 23145 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23647 23145 603 41 0 23606 0
vsize: 94588
[startup+860.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 24275 0 0 0 85942 67 0 0 25 0 1 0 423145402 101421056 24250 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24761 24250 603 41 0 24720 0
vsize: 99044
[startup+870.021 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 24869 0 0 0 86941 69 0 0 25 0 1 0 423145402 103854080 24844 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25355 24844 603 41 0 25314 0
vsize: 101420
[startup+880.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 25715 0 0 0 87939 71 0 0 25 0 1 0 423145402 107225088 25690 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26178 25690 603 41 0 26137 0
vsize: 104712
[startup+890.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26557 0 0 0 88938 72 0 0 25 0 1 0 423145402 110751744 26532 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27039 26532 603 41 0 26998 0
vsize: 108156
[startup+900.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26557 0 0 0 89938 72 0 0 25 0 1 0 423145402 110751744 26532 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27039 26532 603 41 0 26998 0
vsize: 108156
[startup+910.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26557 0 0 0 90938 72 0 0 25 0 1 0 423145402 110751744 26532 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27039 26532 603 41 0 26998 0
vsize: 108156
[startup+920.022 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 91938 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223648 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27039 26533 603 41 0 26998 0
vsize: 108156
[startup+930.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 92938 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27039 26533 603 41 0 26998 0
vsize: 108156
[startup+940.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 93939 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27039 26533 603 41 0 26998 0
vsize: 108156
[startup+950.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 94939 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27039 26533 603 41 0 26998 0
vsize: 108156
[startup+960.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 95939 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27039 26533 603 41 0 26998 0
vsize: 108156
[startup+970.023 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 96939 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27039 26533 603 41 0 26998 0
vsize: 108156
[startup+980.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 97939 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27039 26533 603 41 0 26998 0
vsize: 108156
[startup+990.024 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 98940 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27039 26533 603 41 0 26998 0
vsize: 108156
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 99940 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27039 26533 603 41 0 26998 0
vsize: 108156
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 100940 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27039 26533 603 41 0 26998 0
vsize: 108156
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 101940 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27039 26533 603 41 0 26998 0
vsize: 108156
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 102940 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27039 26533 603 41 0 26998 0
vsize: 108156
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 103940 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27039 26533 603 41 0 26998 0
vsize: 108156
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 104941 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27039 26533 603 41 0 26998 0
vsize: 108156
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 105941 72 0 0 25 0 1 0 423145402 110751744 26533 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27039 26533 603 41 0 26998 0
vsize: 108156
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 106941 72 0 0 25 0 1 0 423145402 110534656 26498 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26986 26498 603 41 0 26945 0
vsize: 107944
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 107941 72 0 0 25 0 1 0 423145402 110534656 26498 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26986 26498 603 41 0 26945 0
vsize: 107944
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26558 0 0 0 108941 73 0 0 25 0 1 0 423145402 110534656 26498 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26986 26498 603 41 0 26945 0
vsize: 107944
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26559 0 0 0 109941 73 0 0 25 0 1 0 423145402 110534656 26499 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26986 26499 603 41 0 26945 0
vsize: 107944
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26559 0 0 0 110941 73 0 0 25 0 1 0 423145402 110534656 26499 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26986 26499 603 41 0 26945 0
vsize: 107944
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26559 0 0 0 111942 73 0 0 25 0 1 0 423145402 110534656 26499 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26986 26499 603 41 0 26945 0
vsize: 107944
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26559 0 0 0 112942 73 0 0 25 0 1 0 423145402 110534656 26499 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26986 26499 603 41 0 26945 0
vsize: 107944
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26559 0 0 0 113942 73 0 0 25 0 1 0 423145402 110534656 26499 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26986 26499 603 41 0 26945 0
vsize: 107944
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26559 0 0 0 114942 73 0 0 25 0 1 0 423145402 110534656 26499 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26986 26499 603 41 0 26945 0
vsize: 107944
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26559 0 0 0 115942 73 0 0 25 0 1 0 423145402 110534656 26499 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26986 26499 603 41 0 26945 0
vsize: 107944
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26559 0 0 0 116943 73 0 0 25 0 1 0 423145402 110534656 26499 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26986 26499 603 41 0 26945 0
vsize: 107944
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26559 0 0 0 117943 73 0 0 25 0 1 0 423145402 110534656 26499 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26986 26499 603 41 0 26945 0
vsize: 107944
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26559 0 0 0 118943 73 0 0 25 0 1 0 423145402 110534656 26499 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26986 26499 603 41 0 26945 0
vsize: 107944
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 6932
Raw data (stat): 6932 (minisat+) R 6931 32461 32460 0 -1 0 26559 0 0 0 119943 73 0 0 25 0 1 0 423145402 110534656 26499 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26986 26499 603 41 0 26945 0
vsize: 107944
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.93 1/54 6932
Raw data (stat): 6932 (minisat+) Z 6931 32461 32460 0 -1 12 26561 0 0 0 119943 77 0 0 25 0 1 0 423145402 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.08
CPU time (s): 1200.22
CPU user time (s): 1199.44
CPU system time (s): 0.779881
CPU usage (%): 100.011
Max. virtual memory (Kb): 108156
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####