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-fpga40_39_sat_pb.cnf.cr.opb
MD5SUMb0b9c98556325dcf5a5811fc2d17a816
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 0
Optimality of the best value was proved NO
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 41
Number of bits of the biggest sum of numbers6
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark4.5833
Number of variables2340
Total number of constraints1678
Number of constraints which are clauses1599
Number of constraints which are cardinality constraints (but not clauses)79
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint20
Maximum length of a constraint40

Trace number 4649 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-04-13 19:28:11 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3437 boxname=wulflinc9 idbench=53 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b0b9c98556325dcf5a5811fc2d17a816  /oldhome/oroussel/tmp/wulflinc9/normalized-fpga40_39_sat_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc9/normalized-fpga40_39_sat_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc9/normalized-fpga40_39_sat_pb.cnf.cr.opb
IDLAUNCH: 3437
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
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:        915612 kB
Buffers:         33332 kB
Cached:          65996 kB
SwapCached:        564 kB
Active:          47960 kB
Inactive:        54788 kB
HighTotal:      131008 kB
HighFree:        61068 kB
LowTotal:       903652 kB
LowFree:        854544 kB
SwapTotal:     2097136 kB
SwapFree:      2096572 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10796 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 19:48:14 (client local time) WITH STATUS 0 IN 1200.11 SECONDS
stats: 3437 7 1200.11 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1678 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  78]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  77]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  76]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  75]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  74]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  73]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  72]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  71]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  70]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  69]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  68]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  67]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  66]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  65]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  64]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  63]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  62]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  61]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  60]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  59]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  58]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  57]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  56]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  55]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  54]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  53]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  52]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  51]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  50]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  49]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  48]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  47]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  46]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  45]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  44]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  43]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  42]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  41]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  40]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  39]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[  38]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  37]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  36]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  35]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  34]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  33]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  32]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  31]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  30]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  29]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  28]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  27]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  26]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  25]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  24]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  23]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  22]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  21]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  20]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  19]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  18]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  17]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  16]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  15]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  14]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  13]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  12]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  11]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[  10]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   9]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   8]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   7]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   6]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   5]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   4]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   3]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   2]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   1]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ---[   0]---> Adder-cost: 36   maxlim: 18   bits: 5/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   27385   125221 |    9128       0        0     nan |  0.000 % |
c |       100 |   27377   125191 |   10040      99      346     3.5 | 10.132 % |
c |       250 |   27353   125101 |   11044     246      883     3.6 | 10.177 % |
c |       476 |   27311   124945 |   12149     466     1683     3.6 | 10.267 % |
c |       814 |   27230   124636 |   13364     794     2916     3.7 | 10.447 % |
c |      1320 |   27015   123875 |   14700    1272     5751     4.5 | 11.033 % |
c |      2079 |   26265   121177 |   16170    1922     9363     4.9 | 12.804 % |
c |      3218 |   23732   112404 |   17787    2635    14543     5.5 | 19.469 % |
c |      4926 |   18420    94440 |   19566    3315   275621    83.1 | 34.014 % |
c |      7492 |   18271    93935 |   21523    5846   901871   154.3 | 34.419 % |
c |     11338 |   18172    93602 |   23675    9673  1855724   191.8 | 34.689 % |
c |     17104 |   18017    93070 |   26043   15404  5714454   371.0 | 35.065 % |
c |     25753 |   17896    92649 |   28647   24034  9570917   398.2 | 35.335 % |
c |     38727 |   17830    92422 |   31512   16540  7872141   475.9 | 35.485 % |
c |     58188 |   17798    92318 |   34663   13544 11068502   817.2 | 35.575 % |
c |     87380 |   16154    86759 |   38129   16002 13187535   824.1 | 39.733 % |
c |    131169 |   15750    85393 |   41942   30445 22132687   727.0 | 40.799 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.00 0.00 0.00 2/54 32265
Raw data (stat): 32265 (runsolver) R 32264 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420249260 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.0003 s]
Raw data (loadavg): 0.15 0.03 0.01 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 992 0 1 0 983 3 0 0 25 0 1 0 420249260 5640192 971 4294967295 134512640 134672761 3221224544 3221223712 134565153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 1377 971 603 41 0 1336 0
vsize: 5508
[startup+20.001 s]
Raw data (loadavg): 0.28 0.06 0.02 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 2699 0 1 0 1979 7 0 0 25 0 1 0 420249260 12582912 2678 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3072 2678 603 41 0 3031 0
vsize: 12288
[startup+30.0022 s]
Raw data (loadavg): 0.39 0.09 0.03 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 4829 0 1 0 2975 11 0 0 25 0 1 0 420249260 21368832 4808 4294967295 134512640 134672761 3221224544 3221223648 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5217 4808 603 41 0 5176 0
vsize: 20868
[startup+40.0025 s]
Raw data (loadavg): 0.49 0.12 0.04 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 6752 0 1 0 3970 16 0 0 25 0 1 0 420249260 29143040 6731 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7115 6731 603 41 0 7074 0
vsize: 28460
[startup+50.0022 s]
Raw data (loadavg): 0.56 0.15 0.05 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 8119 0 1 0 4965 20 0 0 25 0 1 0 420249260 34828288 8098 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8503 8098 603 41 0 8462 0
vsize: 34012
[startup+60.0027 s]
Raw data (loadavg): 0.63 0.18 0.06 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 9782 0 1 0 5960 25 0 0 25 0 1 0 420249260 41590784 9761 4294967295 134512640 134672761 3221224544 3221223648 134560177 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10154 9761 603 41 0 10113 0
vsize: 40616
[startup+70.0027 s]
Raw data (loadavg): 0.69 0.21 0.07 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 11023 0 1 0 6957 29 0 0 25 0 1 0 420249260 46735360 11002 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11410 11002 603 41 0 11369 0
vsize: 45640
[startup+80.0035 s]
Raw data (loadavg): 0.73 0.23 0.08 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 12331 0 1 0 7953 33 0 0 25 0 1 0 420249260 52129792 12310 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12727 12310 603 41 0 12686 0
vsize: 50908
[startup+90.0036 s]
Raw data (loadavg): 0.77 0.26 0.09 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 13630 0 1 0 8950 36 0 0 25 0 1 0 420249260 57397248 13609 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14013 13609 603 41 0 13972 0
vsize: 56052
[startup+100.003 s]
Raw data (loadavg): 0.81 0.28 0.10 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 14877 0 1 0 9945 40 0 0 25 0 1 0 420249260 62529536 14856 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15266 14856 603 41 0 15225 0
vsize: 61064
[startup+110.004 s]
Raw data (loadavg): 0.84 0.30 0.11 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 15934 0 1 0 10942 43 0 0 25 0 1 0 420249260 66965504 15913 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16349 15913 603 41 0 16308 0
vsize: 65396
[startup+120.005 s]
Raw data (loadavg): 0.86 0.33 0.12 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 15935 0 1 0 11942 43 0 0 25 0 1 0 420249260 66965504 15914 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16349 15914 603 41 0 16308 0
vsize: 65396
[startup+130.005 s]
Raw data (loadavg): 0.88 0.35 0.12 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 15936 0 1 0 12942 44 0 0 25 0 1 0 420249260 66965504 15915 4294967295 134512640 134672761 3221224544 3221223648 134555225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16349 15915 603 41 0 16308 0
vsize: 65396
[startup+140.005 s]
Raw data (loadavg): 0.90 0.37 0.13 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 15936 0 1 0 13942 44 0 0 25 0 1 0 420249260 66965504 15915 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16349 15915 603 41 0 16308 0
vsize: 65396
[startup+150.005 s]
Raw data (loadavg): 0.92 0.39 0.14 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 15936 0 1 0 14942 44 0 0 25 0 1 0 420249260 66965504 15915 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16349 15915 603 41 0 16308 0
vsize: 65396
[startup+160.005 s]
Raw data (loadavg): 0.93 0.41 0.15 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 16857 0 1 0 15939 47 0 0 25 0 1 0 420249260 70750208 16836 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17273 16836 603 41 0 17232 0
vsize: 69092
[startup+170.005 s]
Raw data (loadavg): 0.94 0.43 0.16 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 18633 0 1 0 16934 51 0 0 25 0 1 0 420249260 78032896 18612 4294967295 134512640 134672761 3221224544 3221223728 134559373 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19051 18612 603 41 0 19010 0
vsize: 76204
[startup+180.006 s]
Raw data (loadavg): 0.95 0.45 0.17 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 20410 0 1 0 17930 56 0 0 25 0 1 0 420249260 85356544 20389 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20839 20389 603 41 0 20798 0
vsize: 83356
[startup+190.007 s]
Raw data (loadavg): 0.95 0.46 0.18 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 21583 0 1 0 18926 59 0 0 25 0 1 0 420249260 90210304 21562 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22024 21562 603 41 0 21983 0
vsize: 88096
[startup+200.006 s]
Raw data (loadavg): 0.96 0.48 0.19 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 22925 0 1 0 19923 63 0 0 25 0 1 0 420249260 95748096 22904 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23376 22904 603 41 0 23335 0
vsize: 93504
[startup+210.006 s]
Raw data (loadavg): 0.97 0.50 0.19 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 24415 0 1 0 20919 67 0 0 25 0 1 0 420249260 101818368 24394 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24858 24394 603 41 0 24817 0
vsize: 99432
[startup+220.006 s]
Raw data (loadavg): 0.97 0.51 0.20 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 25685 0 1 0 21915 71 0 0 25 0 1 0 420249260 107094016 25664 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26146 25664 603 41 0 26105 0
vsize: 104584
[startup+230.007 s]
Raw data (loadavg): 0.98 0.53 0.21 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 26528 0 1 0 22913 73 0 0 25 0 1 0 420249260 110460928 26507 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26968 26507 603 41 0 26927 0
vsize: 107872
[startup+240.007 s]
Raw data (loadavg): 0.98 0.54 0.22 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 26528 0 1 0 23913 73 0 0 25 0 1 0 420249260 110460928 26507 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26968 26507 603 41 0 26927 0
vsize: 107872
[startup+250.007 s]
Raw data (loadavg): 0.98 0.56 0.22 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 26528 0 1 0 24913 73 0 0 25 0 1 0 420249260 110460928 26507 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26968 26507 603 41 0 26927 0
vsize: 107872
[startup+260.007 s]
Raw data (loadavg): 0.98 0.57 0.23 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 26528 0 1 0 25913 73 0 0 25 0 1 0 420249260 110460928 26507 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26968 26507 603 41 0 26927 0
vsize: 107872
[startup+270.007 s]
Raw data (loadavg): 0.99 0.59 0.24 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 26528 0 1 0 26913 74 0 0 25 0 1 0 420249260 110460928 26507 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26968 26507 603 41 0 26927 0
vsize: 107872
[startup+280.008 s]
Raw data (loadavg): 0.99 0.60 0.25 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 26528 0 1 0 27913 74 0 0 25 0 1 0 420249260 110460928 26507 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26968 26507 603 41 0 26927 0
vsize: 107872
[startup+290.008 s]
Raw data (loadavg): 0.99 0.61 0.26 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 26528 0 1 0 28912 74 0 0 25 0 1 0 420249260 110460928 26507 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26968 26507 603 41 0 26927 0
vsize: 107872
[startup+300.008 s]
Raw data (loadavg): 0.99 0.62 0.26 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 26528 0 1 0 29912 74 0 0 25 0 1 0 420249260 110460928 26507 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26968 26507 603 41 0 26927 0
vsize: 107872
[startup+310.009 s]
Raw data (loadavg): 0.99 0.64 0.27 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 26528 0 1 0 30912 74 0 0 25 0 1 0 420249260 110460928 26507 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26968 26507 603 41 0 26927 0
vsize: 107872
[startup+320.008 s]
Raw data (loadavg): 0.99 0.65 0.28 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 26528 0 1 0 31912 75 0 0 25 0 1 0 420249260 110460928 26507 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26968 26507 603 41 0 26927 0
vsize: 107872
[startup+330.009 s]
Raw data (loadavg): 0.99 0.66 0.29 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 26528 0 1 0 32912 75 0 0 25 0 1 0 420249260 110460928 26507 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26968 26507 603 41 0 26927 0
vsize: 107872
[startup+340.009 s]
Raw data (loadavg): 0.99 0.67 0.29 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 26528 0 1 0 33912 75 0 0 25 0 1 0 420249260 110460928 26507 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26968 26507 603 41 0 26927 0
vsize: 107872
[startup+350.008 s]
Raw data (loadavg): 0.99 0.68 0.30 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 26528 0 1 0 34912 75 0 0 25 0 1 0 420249260 110460928 26507 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26968 26507 603 41 0 26927 0
vsize: 107872
[startup+360.009 s]
Raw data (loadavg): 0.99 0.69 0.31 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 26528 0 1 0 35912 75 0 0 25 0 1 0 420249260 110460928 26507 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26968 26507 603 41 0 26927 0
vsize: 107872
[startup+370.009 s]
Raw data (loadavg): 0.99 0.70 0.31 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 26528 0 1 0 36911 76 0 0 25 0 1 0 420249260 110460928 26507 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26968 26507 603 41 0 26927 0
vsize: 107872
[startup+380.009 s]
Raw data (loadavg): 0.99 0.71 0.32 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 26528 0 1 0 37911 76 0 0 25 0 1 0 420249260 110460928 26507 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26968 26507 603 41 0 26927 0
vsize: 107872
[startup+390.01 s]
Raw data (loadavg): 0.99 0.72 0.33 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 27929 0 1 0 38909 78 0 0 25 0 1 0 420249260 116277248 27908 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28388 27908 603 41 0 28347 0
vsize: 113552
[startup+400.01 s]
Raw data (loadavg): 0.99 0.73 0.33 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 29325 0 1 0 39907 80 0 0 25 0 1 0 420249260 121925632 29304 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29767 29304 603 41 0 29726 0
vsize: 119068
[startup+410.01 s]
Raw data (loadavg): 0.99 0.74 0.34 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 30644 0 1 0 40905 82 0 0 25 0 1 0 420249260 127311872 30623 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31082 30623 603 41 0 31041 0
vsize: 124328
[startup+420.01 s]
Raw data (loadavg): 0.99 0.74 0.35 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 31756 0 1 0 41903 85 0 0 25 0 1 0 420249260 131874816 31735 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32196 31735 603 41 0 32155 0
vsize: 128784
[startup+430.011 s]
Raw data (loadavg): 0.99 0.75 0.35 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 32858 0 1 0 42901 87 0 0 25 0 1 0 420249260 136462336 32837 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33316 32837 603 41 0 33275 0
vsize: 133264
[startup+440.01 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 33217 0 1 0 43900 88 0 0 25 0 1 0 420249260 137949184 33196 4294967295 134512640 134672761 3221224544 3221223728 134559028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33679 33196 603 41 0 33638 0
vsize: 134716
[startup+450.01 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 33217 0 1 0 44901 88 0 0 25 0 1 0 420249260 137949184 33196 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33679 33196 603 41 0 33638 0
vsize: 134716
[startup+460.011 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 33217 0 1 0 45901 88 0 0 25 0 1 0 420249260 137949184 33196 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33679 33196 603 41 0 33638 0
vsize: 134716
[startup+470.011 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 33217 0 1 0 46899 88 0 0 25 0 1 0 420249260 137949184 33196 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33679 33196 603 41 0 33638 0
vsize: 134716
[startup+480.012 s]
Raw data (loadavg): 0.99 0.79 0.38 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 33217 0 1 0 47900 88 0 0 25 0 1 0 420249260 137949184 33196 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33679 33196 603 41 0 33638 0
vsize: 134716
[startup+490.011 s]
Raw data (loadavg): 0.99 0.79 0.39 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 33217 0 1 0 48900 88 0 0 25 0 1 0 420249260 137949184 33196 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33679 33196 603 41 0 33638 0
vsize: 134716
[startup+500.01 s]
Raw data (loadavg): 0.99 0.80 0.40 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 33217 0 1 0 49900 88 0 0 25 0 1 0 420249260 137949184 33196 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33679 33196 603 41 0 33638 0
vsize: 134716
[startup+510.01 s]
Raw data (loadavg): 0.99 0.81 0.40 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 33217 0 1 0 50900 88 0 0 25 0 1 0 420249260 137949184 33196 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33679 33196 603 41 0 33638 0
vsize: 134716
[startup+520.01 s]
Raw data (loadavg): 0.99 0.81 0.41 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 33217 0 1 0 51900 88 0 0 25 0 1 0 420249260 137949184 33196 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33679 33196 603 41 0 33638 0
vsize: 134716
[startup+530.01 s]
Raw data (loadavg): 0.99 0.82 0.41 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 33217 0 1 0 52901 88 0 0 25 0 1 0 420249260 137949184 33196 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33679 33196 603 41 0 33638 0
vsize: 134716
[startup+540.01 s]
Raw data (loadavg): 0.99 0.82 0.42 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 33217 0 1 0 53901 88 0 0 25 0 1 0 420249260 137949184 33196 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33679 33196 603 41 0 33638 0
vsize: 134716
[startup+550.01 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 33217 0 1 0 54901 88 0 0 25 0 1 0 420249260 137949184 33196 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33679 33196 603 41 0 33638 0
vsize: 134716
[startup+560.011 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 33217 0 1 0 55901 88 0 0 25 0 1 0 420249260 137949184 33196 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33679 33196 603 41 0 33638 0
vsize: 134716
[startup+570.01 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 33217 0 1 0 56901 88 0 0 25 0 1 0 420249260 137949184 33196 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33679 33196 603 41 0 33638 0
vsize: 134716
[startup+580.011 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 33217 0 1 0 57901 88 0 0 25 0 1 0 420249260 137949184 33196 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33679 33196 603 41 0 33638 0
vsize: 134716
[startup+590.011 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 33217 0 1 0 58902 88 0 0 25 0 1 0 420249260 137949184 33196 4294967295 134512640 134672761 3221224544 3221223724 134559056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33679 33196 603 41 0 33638 0
vsize: 134716
[startup+600.011 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 33217 0 1 0 59902 88 0 0 25 0 1 0 420249260 137949184 33196 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33679 33196 603 41 0 33638 0
vsize: 134716
[startup+610.011 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 33217 0 1 0 60902 88 0 0 25 0 1 0 420249260 137949184 33196 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33679 33196 603 41 0 33638 0
vsize: 134716
[startup+620.011 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 33217 0 1 0 61902 88 0 0 25 0 1 0 420249260 137949184 33196 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33679 33196 603 41 0 33638 0
vsize: 134716
[startup+630.011 s]
Raw data (loadavg): 0.99 0.86 0.47 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 33246 0 1 0 62902 88 0 0 25 0 1 0 420249260 138084352 33225 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33712 33225 603 41 0 33671 0
vsize: 134848
[startup+640.012 s]
Raw data (loadavg): 0.99 0.87 0.47 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 34469 0 1 0 63900 90 0 0 25 0 1 0 420249260 143097856 34448 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34936 34448 603 41 0 34895 0
vsize: 139744
[startup+650.012 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 35168 0 1 0 64899 91 0 0 25 0 1 0 420249260 145932288 35147 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35628 35147 603 41 0 35587 0
vsize: 142512
[startup+660.012 s]
Raw data (loadavg): 0.99 0.88 0.48 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 35169 0 1 0 65900 91 0 0 25 0 1 0 420249260 145932288 35148 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35628 35148 603 41 0 35587 0
vsize: 142512
[startup+670.012 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 35169 0 1 0 66900 91 0 0 25 0 1 0 420249260 145932288 35148 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35628 35148 603 41 0 35587 0
vsize: 142512
[startup+680.013 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 35169 0 1 0 67900 91 0 0 25 0 1 0 420249260 145932288 35148 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35628 35148 603 41 0 35587 0
vsize: 142512
[startup+690.012 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 35169 0 1 0 68900 91 0 0 25 0 1 0 420249260 145932288 35148 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35628 35148 603 41 0 35587 0
vsize: 142512
[startup+700.012 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 35169 0 1 0 69900 91 0 0 25 0 1 0 420249260 145932288 35148 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35628 35148 603 41 0 35587 0
vsize: 142512
[startup+710.013 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 35170 0 1 0 70901 91 0 0 25 0 1 0 420249260 145932288 35149 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35628 35149 603 41 0 35587 0
vsize: 142512
[startup+720.013 s]
Raw data (loadavg): 0.99 0.90 0.51 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 35170 0 1 0 71901 91 0 0 25 0 1 0 420249260 145932288 35149 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35628 35149 603 41 0 35587 0
vsize: 142512
[startup+730.013 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 35170 0 1 0 72901 91 0 0 25 0 1 0 420249260 145932288 35149 4294967295 134512640 134672761 3221224544 3221223648 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35628 35149 603 41 0 35587 0
vsize: 142512
[startup+740.014 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 35170 0 1 0 73901 91 0 0 25 0 1 0 420249260 145932288 35149 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35628 35149 603 41 0 35587 0
vsize: 142512
[startup+750.013 s]
Raw data (loadavg): 0.99 0.90 0.53 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 35170 0 1 0 74901 91 0 0 25 0 1 0 420249260 145932288 35149 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35628 35149 603 41 0 35587 0
vsize: 142512
[startup+760.013 s]
Raw data (loadavg): 0.99 0.91 0.53 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 35170 0 1 0 75902 91 0 0 25 0 1 0 420249260 145932288 35149 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35628 35149 603 41 0 35587 0
vsize: 142512
[startup+770.014 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 35170 0 1 0 76902 91 0 0 25 0 1 0 420249260 145932288 35149 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35628 35149 603 41 0 35587 0
vsize: 142512
[startup+780.015 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 35170 0 1 0 77902 91 0 0 25 0 1 0 420249260 145932288 35149 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35628 35149 603 41 0 35587 0
vsize: 142512
[startup+790.014 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 35170 0 1 0 78902 91 0 0 25 0 1 0 420249260 145932288 35149 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35628 35149 603 41 0 35587 0
vsize: 142512
[startup+800.014 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 35170 0 1 0 79902 91 0 0 25 0 1 0 420249260 145932288 35149 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35628 35149 603 41 0 35587 0
vsize: 142512
[startup+810.014 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 35170 0 1 0 80902 91 0 0 25 0 1 0 420249260 145932288 35149 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35628 35149 603 41 0 35587 0
vsize: 142512
[startup+820.013 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 35170 0 1 0 81903 91 0 0 25 0 1 0 420249260 145932288 35149 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35628 35149 603 41 0 35587 0
vsize: 142512
[startup+830.014 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 35170 0 1 0 82902 92 0 0 25 0 1 0 420249260 145932288 35149 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35628 35149 603 41 0 35587 0
vsize: 142512
[startup+840.014 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 35170 0 1 0 83902 92 0 0 25 0 1 0 420249260 145932288 35149 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35628 35149 603 41 0 35587 0
vsize: 142512
[startup+850.014 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 35170 0 1 0 84902 92 0 0 25 0 1 0 420249260 145932288 35149 4294967295 134512640 134672761 3221224544 3221223616 134553553 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35628 35149 603 41 0 35587 0
vsize: 142512
[startup+860.014 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 35170 0 1 0 85902 92 0 0 25 0 1 0 420249260 145932288 35149 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35628 35149 603 41 0 35587 0
vsize: 142512
[startup+870.014 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 35170 0 1 0 86902 92 0 0 25 0 1 0 420249260 145932288 35149 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35628 35149 603 41 0 35587 0
vsize: 142512
[startup+880.015 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 35170 0 1 0 87903 92 0 0 25 0 1 0 420249260 145932288 35149 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35628 35149 603 41 0 35587 0
vsize: 142512
[startup+890.015 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 35534 0 1 0 88902 92 0 0 25 0 1 0 420249260 147423232 35513 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35992 35513 603 41 0 35951 0
vsize: 143968
[startup+900.015 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 36874 0 1 0 89899 95 0 0 25 0 1 0 420249260 152952832 36853 4294967295 134512640 134672761 3221224544 3221223560 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37342 36853 603 41 0 37301 0
vsize: 149368
[startup+910.016 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 38426 0 1 0 90896 98 0 0 25 0 1 0 420249260 159305728 38405 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38893 38405 603 41 0 38852 0
vsize: 155572
[startup+920.016 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 39944 0 1 0 91893 102 0 0 25 0 1 0 420249260 165519360 39923 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40410 39923 603 41 0 40369 0
vsize: 161640
[startup+930.016 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 40690 0 1 0 92892 103 0 0 25 0 1 0 420249260 168603648 40669 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41163 40669 603 41 0 41122 0
vsize: 164652
[startup+940.016 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 40690 0 1 0 93892 103 0 0 25 0 1 0 420249260 168603648 40669 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41163 40669 603 41 0 41122 0
vsize: 164652
[startup+950.016 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 40691 0 1 0 94892 103 0 0 25 0 1 0 420249260 168603648 40670 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41163 40670 603 41 0 41122 0
vsize: 164652
[startup+960.016 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 40692 0 1 0 95892 103 0 0 25 0 1 0 420249260 168603648 40671 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41163 40671 603 41 0 41122 0
vsize: 164652
[startup+970.015 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 40692 0 1 0 96892 103 0 0 25 0 1 0 420249260 168603648 40671 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41163 40671 603 41 0 41122 0
vsize: 164652
[startup+980.016 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 40692 0 1 0 97893 103 0 0 25 0 1 0 420249260 168603648 40671 4294967295 134512640 134672761 3221224544 3221223648 134560212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41163 40671 603 41 0 41122 0
vsize: 164652
[startup+990.016 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 40692 0 1 0 98893 103 0 0 25 0 1 0 420249260 168603648 40671 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41163 40671 603 41 0 41122 0
vsize: 164652
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 40695 0 1 0 99893 103 0 0 25 0 1 0 420249260 168603648 40674 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41163 40674 603 41 0 41122 0
vsize: 164652
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 40695 0 1 0 100893 103 0 0 25 0 1 0 420249260 168603648 40674 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41163 40674 603 41 0 41122 0
vsize: 164652
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 40695 0 1 0 101893 103 0 0 25 0 1 0 420249260 168603648 40674 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41163 40674 603 41 0 41122 0
vsize: 164652
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 40695 0 1 0 102893 103 0 0 25 0 1 0 420249260 168603648 40674 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41163 40674 603 41 0 41122 0
vsize: 164652
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 40695 0 1 0 103894 103 0 0 25 0 1 0 420249260 168603648 40674 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41163 40674 603 41 0 41122 0
vsize: 164652
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 40695 0 1 0 104894 103 0 0 25 0 1 0 420249260 168603648 40674 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41163 40674 603 41 0 41122 0
vsize: 164652
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 40695 0 1 0 105894 103 0 0 25 0 1 0 420249260 168603648 40674 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41163 40674 603 41 0 41122 0
vsize: 164652
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.96 0.65 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 40695 0 1 0 106894 103 0 0 25 0 1 0 420249260 168603648 40674 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41163 40674 603 41 0 41122 0
vsize: 164652
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 40695 0 1 0 107894 103 0 0 25 0 1 0 420249260 168603648 40674 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41163 40674 603 41 0 41122 0
vsize: 164652
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 40695 0 1 0 108895 103 0 0 25 0 1 0 420249260 168603648 40674 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41163 40674 603 41 0 41122 0
vsize: 164652
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 40695 0 1 0 109895 103 0 0 25 0 1 0 420249260 168603648 40674 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41163 40674 603 41 0 41122 0
vsize: 164652
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 40695 0 1 0 110895 103 0 0 25 0 1 0 420249260 168603648 40674 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41163 40674 603 41 0 41122 0
vsize: 164652
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 40881 0 1 0 111895 104 0 0 25 0 1 0 420249260 169283584 40860 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41329 40860 603 41 0 41288 0
vsize: 165316
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 41411 0 1 0 112895 104 0 0 25 0 1 0 420249260 171458560 41390 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41860 41390 603 41 0 41819 0
vsize: 167440
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 42285 0 1 0 113893 106 0 0 25 0 1 0 420249260 175132672 42264 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42757 42264 603 41 0 42716 0
vsize: 171028
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 42812 0 1 0 114893 107 0 0 25 0 1 0 420249260 177311744 42791 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43289 42791 603 41 0 43248 0
vsize: 173156
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 44030 0 1 0 115891 109 0 0 25 0 1 0 420249260 182181888 44009 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44478 44009 603 41 0 44437 0
vsize: 177912
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 44995 0 1 0 116889 111 0 0 25 0 1 0 420249260 186236928 44974 4294967295 134512640 134672761 3221224544 3221223560 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45468 44974 603 41 0 45427 0
vsize: 181872
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 45766 0 1 0 117888 113 0 0 25 0 1 0 420249260 189349888 45745 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46228 45746 603 41 0 46187 0
vsize: 184912
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 46651 0 1 0 118887 114 0 0 25 0 1 0 420249260 193019904 46630 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47124 46630 603 41 0 47083 0
vsize: 188496
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 32265
Raw data (stat): 32265 (minisat+) R 32264 30854 30853 0 -1 0 47513 0 1 0 119884 117 0 0 25 0 1 0 420249260 196542464 47492 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47984 47492 603 41 0 47943 0
vsize: 191936
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.69 1/54 32265
Raw data (stat): 32265 (minisat+) Z 32264 30854 30853 0 -1 12 47515 0 1 0 119885 125 0 0 25 0 1 0 420249260 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.12
CPU time (s): 1200.11
CPU user time (s): 1198.85
CPU system time (s): 1.25681
CPU usage (%): 99.9992
Max. virtual memory (Kb): 191936
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####