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-chnl15_25_pb.cnf.cr.opb
MD5SUM808390b13d2d87ec4e78f628ed3af9ba
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 26
Number of bits of the biggest sum of numbers5
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.021995
Number of variables750
Total number of constraints80
Number of constraints which are clauses50
Number of constraints which are cardinality constraints (but not clauses)30
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint15
Maximum length of a constraint25

Trace number 4577 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-04-13 19:23:39 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3391 boxname=wulflinc6 idbench=7 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  808390b13d2d87ec4e78f628ed3af9ba  /oldhome/oroussel/tmp/wulflinc6/normalized-chnl15_25_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc6/normalized-chnl15_25_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc6/normalized-chnl15_25_pb.cnf.cr.opb
IDLAUNCH: 3391
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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.042
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:        923832 kB
Buffers:         33944 kB
Cached:          55416 kB
SwapCached:       2644 kB
Active:          47560 kB
Inactive:        47296 kB
HighTotal:      131008 kB
HighFree:        71680 kB
LowTotal:       903652 kB
LowFree:        852152 kB
SwapTotal:     2097136 kB
SwapFree:      2094492 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10404 kB
Committed_AS:    63476 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 19:43:41 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 3391 7 1200.25 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 80 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................
c ---[  29]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  28]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  27]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  26]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  25]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  24]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  23]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  22]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  21]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  20]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  19]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  18]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  17]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  16]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  15]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  14]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  13]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  12]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  11]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[  10]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[   9]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[   8]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[   7]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[   6]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[   5]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[   4]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[   3]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[   2]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[   1]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[   0]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    8180    29460 |    2726       0        0     nan |  0.000 % |
c |       100 |    7293    26405 |    2998      23       72     3.1 | 13.532 % |
c |       250 |    6982    25334 |    3298     138      727     5.3 | 16.517 % |
c |       476 |    6571    23933 |    3628     309     1827     5.9 | 20.100 % |
c |       813 |    5482    20228 |    3991     490     3511     7.2 | 30.000 % |
c |      1319 |    4658    17442 |    4390     877    36134    41.2 | 37.463 % |
c |      2085 |    4658    17442 |    4829    1643   126311    76.9 | 37.463 % |
c |      3224 |    4658    17442 |    5312    2782   272516    98.0 | 37.463 % |
c |      4933 |    4658    17442 |    5843    4491   494758   110.2 | 37.463 % |
c |      7496 |    4658    17442 |    6427    3651   426691   116.9 | 37.463 % |
c |     11340 |    4658    17442 |    7070    3771   429016   113.8 | 37.463 % |
c |     17107 |    4658    17442 |    7777    5516   647801   117.4 | 37.463 % |
c |     25758 |    4658    17442 |    8555    5370   626641   116.7 | 37.463 % |
c |     38732 |    4658    17442 |    9410    8792  1102062   125.3 | 37.463 % |
c |     58194 |    4658    17442 |   10351    7460   875169   117.3 | 37.463 % |
c |     87389 |    4658    17442 |   11387    8254  1018431   123.4 | 37.463 % |
c |    131180 |    4658    17442 |   12525    8748  1019839   116.6 | 37.463 % |
c |    196866 |    4631    17355 |   13778    6836   852807   124.8 | 37.761 % |
c |    295392 |    4622    17326 |   15156    9461  1174219   124.1 | 37.861 % |
c |    443185 |    4517    16985 |   16671   11975  1295494   108.2 | 38.856 % |
c |    664869 |    4494    16910 |   18339   13173  1403232   106.5 | 39.055 % |
#### 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.04 2/54 31347
Raw data (stat): 31347 (runsolver) R 31346 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 420221446 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+9.99992 s]
Raw data (loadavg): 0.15 0.03 0.05 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 1352 0 1 0 983 3 0 0 25 0 1 0 420221446 7057408 1331 4294967295 134512640 134672761 3221224544 3221223604 1075346622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1723 1331 603 41 0 1682 0
vsize: 6892
[startup+20.0003 s]
Raw data (loadavg): 0.28 0.06 0.06 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 1704 0 1 0 1982 4 0 0 25 0 1 0 420221446 8593408 1683 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2098 1683 603 41 0 2057 0
vsize: 8392
[startup+30.0001 s]
Raw data (loadavg): 0.39 0.09 0.07 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 1925 0 1 0 2982 5 0 0 25 0 1 0 420221446 9535488 1904 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2328 1904 603 41 0 2287 0
vsize: 9312
[startup+39.9992 s]
Raw data (loadavg): 0.49 0.12 0.08 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 2119 0 1 0 3982 5 0 0 25 0 1 0 420221446 10346496 2098 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2526 2098 603 41 0 2485 0
vsize: 10104
[startup+49.9997 s]
Raw data (loadavg): 0.56 0.15 0.09 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 2152 0 1 0 4982 5 0 0 25 0 1 0 420221446 10502144 2131 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2564 2131 603 41 0 2523 0
vsize: 10256
[startup+59.9995 s]
Raw data (loadavg): 0.63 0.18 0.10 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 2322 0 1 0 5982 6 0 0 25 0 1 0 420221446 11173888 2301 4294967295 134512640 134672761 3221224544 3221223728 134559572 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2728 2301 603 41 0 2687 0
vsize: 10912
[startup+69.9996 s]
Raw data (loadavg): 0.69 0.21 0.11 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 2395 0 1 0 6982 6 0 0 25 0 1 0 420221446 11444224 2374 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2794 2374 603 41 0 2753 0
vsize: 11176
[startup+80.0001 s]
Raw data (loadavg): 0.73 0.23 0.12 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 2471 0 1 0 7982 6 0 0 25 0 1 0 420221446 11907072 2450 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2907 2450 603 41 0 2866 0
vsize: 11628
[startup+90 s]
Raw data (loadavg): 0.77 0.26 0.13 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 2515 0 1 0 8982 6 0 0 25 0 1 0 420221446 12042240 2494 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2940 2494 603 41 0 2899 0
vsize: 11760
[startup+99.9991 s]
Raw data (loadavg): 0.81 0.28 0.13 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 2679 0 1 0 9982 7 0 0 25 0 1 0 420221446 12734464 2658 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3109 2658 603 41 0 3068 0
vsize: 12436
[startup+110 s]
Raw data (loadavg): 0.84 0.30 0.14 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 2730 0 1 0 10982 7 0 0 25 0 1 0 420221446 13004800 2709 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3175 2709 603 41 0 3134 0
vsize: 12700
[startup+119.999 s]
Raw data (loadavg): 0.86 0.33 0.15 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 2755 0 1 0 11982 7 0 0 25 0 1 0 420221446 13139968 2734 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3208 2734 603 41 0 3167 0
vsize: 12832
[startup+129.999 s]
Raw data (loadavg): 0.88 0.35 0.16 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 2763 0 1 0 12983 7 0 0 25 0 1 0 420221446 13139968 2742 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3208 2742 603 41 0 3167 0
vsize: 12832
[startup+139.998 s]
Raw data (loadavg): 0.90 0.37 0.17 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 2785 0 1 0 13983 7 0 0 25 0 1 0 420221446 13299712 2764 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3247 2764 603 41 0 3206 0
vsize: 12988
[startup+149.998 s]
Raw data (loadavg): 0.92 0.39 0.18 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 2898 0 1 0 14983 8 0 0 25 0 1 0 420221446 13709312 2877 4294967295 134512640 134672761 3221224544 3221223648 134554671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3347 2877 603 41 0 3306 0
vsize: 13388
[startup+159.997 s]
Raw data (loadavg): 0.93 0.41 0.19 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 2996 0 1 0 15983 8 0 0 25 0 1 0 420221446 14114816 2975 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3446 2975 603 41 0 3405 0
vsize: 13784
[startup+169.996 s]
Raw data (loadavg): 0.94 0.43 0.19 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3086 0 1 0 16983 8 0 0 25 0 1 0 420221446 14536704 3065 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3549 3065 603 41 0 3508 0
vsize: 14196
[startup+179.996 s]
Raw data (loadavg): 0.95 0.45 0.20 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3087 0 1 0 17983 8 0 0 25 0 1 0 420221446 14536704 3066 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3549 3066 603 41 0 3508 0
vsize: 14196
[startup+189.996 s]
Raw data (loadavg): 0.95 0.46 0.21 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3087 0 1 0 18983 8 0 0 25 0 1 0 420221446 14536704 3066 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3549 3066 603 41 0 3508 0
vsize: 14196
[startup+199.996 s]
Raw data (loadavg): 0.96 0.48 0.22 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3087 0 1 0 19984 8 0 0 25 0 1 0 420221446 14536704 3066 4294967295 134512640 134672761 3221224544 3221222480 134565768 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3549 3066 603 41 0 3508 0
vsize: 14196
[startup+209.996 s]
Raw data (loadavg): 0.97 0.50 0.23 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3089 0 1 0 20984 8 0 0 25 0 1 0 420221446 14536704 3068 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3549 3068 603 41 0 3508 0
vsize: 14196
[startup+219.996 s]
Raw data (loadavg): 0.97 0.51 0.23 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3089 0 1 0 21984 8 0 0 25 0 1 0 420221446 14536704 3068 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3549 3068 603 41 0 3508 0
vsize: 14196
[startup+229.995 s]
Raw data (loadavg): 0.98 0.53 0.24 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3098 0 1 0 22985 8 0 0 25 0 1 0 420221446 14536704 3077 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3549 3078 603 41 0 3508 0
vsize: 14196
[startup+239.995 s]
Raw data (loadavg): 0.98 0.54 0.25 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3270 0 1 0 23985 8 0 0 25 0 1 0 420221446 15237120 3249 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3720 3249 603 41 0 3679 0
vsize: 14880
[startup+249.994 s]
Raw data (loadavg): 0.98 0.56 0.26 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3286 0 1 0 24985 9 0 0 25 0 1 0 420221446 15396864 3265 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3759 3265 603 41 0 3718 0
vsize: 15036
[startup+259.995 s]
Raw data (loadavg): 0.98 0.57 0.26 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3288 0 1 0 25985 9 0 0 25 0 1 0 420221446 15396864 3267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3759 3267 603 41 0 3718 0
vsize: 15036
[startup+269.995 s]
Raw data (loadavg): 0.99 0.59 0.27 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3292 0 1 0 26985 9 0 0 25 0 1 0 420221446 15396864 3271 4294967295 134512640 134672761 3221224544 3221223728 134559324 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3759 3271 603 41 0 3718 0
vsize: 15036
[startup+279.994 s]
Raw data (loadavg): 0.99 0.60 0.28 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3293 0 1 0 27986 9 0 0 25 0 1 0 420221446 15396864 3272 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3759 3272 603 41 0 3718 0
vsize: 15036
[startup+289.994 s]
Raw data (loadavg): 0.99 0.61 0.29 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3303 0 1 0 28986 9 0 0 25 0 1 0 420221446 15396864 3282 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3759 3282 603 41 0 3718 0
vsize: 15036
[startup+299.994 s]
Raw data (loadavg): 0.99 0.62 0.29 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3323 0 1 0 29986 9 0 0 25 0 1 0 420221446 15560704 3302 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3799 3302 603 41 0 3758 0
vsize: 15196
[startup+309.993 s]
Raw data (loadavg): 0.99 0.64 0.30 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3323 0 1 0 30986 9 0 0 25 0 1 0 420221446 15560704 3302 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3799 3302 603 41 0 3758 0
vsize: 15196
[startup+319.993 s]
Raw data (loadavg): 0.99 0.65 0.31 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3325 0 1 0 31987 9 0 0 25 0 1 0 420221446 15560704 3304 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3799 3304 603 41 0 3758 0
vsize: 15196
[startup+329.993 s]
Raw data (loadavg): 0.99 0.66 0.31 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3335 0 1 0 32987 9 0 0 25 0 1 0 420221446 15560704 3314 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3799 3314 603 41 0 3758 0
vsize: 15196
[startup+339.992 s]
Raw data (loadavg): 0.99 0.67 0.32 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3337 0 1 0 33987 9 0 0 25 0 1 0 420221446 15560704 3316 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3799 3316 603 41 0 3758 0
vsize: 15196
[startup+349.991 s]
Raw data (loadavg): 0.99 0.68 0.33 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3339 0 1 0 34988 9 0 0 25 0 1 0 420221446 15695872 3318 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3832 3318 603 41 0 3791 0
vsize: 15328
[startup+359.991 s]
Raw data (loadavg): 0.99 0.69 0.33 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3359 0 1 0 35988 9 0 0 25 0 1 0 420221446 15695872 3338 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3832 3338 603 41 0 3791 0
vsize: 15328
[startup+369.99 s]
Raw data (loadavg): 0.99 0.70 0.34 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3362 0 1 0 36988 9 0 0 25 0 1 0 420221446 15695872 3341 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3832 3341 603 41 0 3791 0
vsize: 15328
[startup+379.99 s]
Raw data (loadavg): 0.99 0.71 0.35 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3377 0 1 0 37988 9 0 0 25 0 1 0 420221446 15831040 3356 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3865 3356 603 41 0 3824 0
vsize: 15460
[startup+389.989 s]
Raw data (loadavg): 0.99 0.72 0.35 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3519 0 1 0 38988 9 0 0 25 0 1 0 420221446 16375808 3498 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3998 3498 603 41 0 3957 0
vsize: 15992
[startup+399.99 s]
Raw data (loadavg): 0.99 0.73 0.36 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3640 0 1 0 39988 10 0 0 25 0 1 0 420221446 16916480 3619 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4130 3619 603 41 0 4089 0
vsize: 16520
[startup+409.989 s]
Raw data (loadavg): 0.99 0.74 0.37 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3675 0 1 0 40988 10 0 0 25 0 1 0 420221446 17080320 3654 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4170 3654 603 41 0 4129 0
vsize: 16680
[startup+419.989 s]
Raw data (loadavg): 0.99 0.74 0.37 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3676 0 1 0 41989 10 0 0 25 0 1 0 420221446 17080320 3655 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4170 3655 603 41 0 4129 0
vsize: 16680
[startup+429.989 s]
Raw data (loadavg): 0.99 0.75 0.38 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3676 0 1 0 42989 10 0 0 25 0 1 0 420221446 17080320 3655 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4170 3655 603 41 0 4129 0
vsize: 16680
[startup+439.989 s]
Raw data (loadavg): 0.99 0.76 0.39 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3677 0 1 0 43989 10 0 0 25 0 1 0 420221446 17080320 3656 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4170 3656 603 41 0 4129 0
vsize: 16680
[startup+449.988 s]
Raw data (loadavg): 0.99 0.77 0.39 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3677 0 1 0 44989 10 0 0 25 0 1 0 420221446 17080320 3656 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4170 3656 603 41 0 4129 0
vsize: 16680
[startup+459.987 s]
Raw data (loadavg): 0.99 0.77 0.40 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3677 0 1 0 45990 10 0 0 25 0 1 0 420221446 17080320 3656 4294967295 134512640 134672761 3221224544 3221223648 134560412 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4170 3656 603 41 0 4129 0
vsize: 16680
[startup+469.988 s]
Raw data (loadavg): 0.99 0.78 0.40 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3677 0 1 0 46990 10 0 0 25 0 1 0 420221446 17080320 3656 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4170 3656 603 41 0 4129 0
vsize: 16680
[startup+479.987 s]
Raw data (loadavg): 0.99 0.79 0.41 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3709 0 1 0 47990 10 0 0 25 0 1 0 420221446 17215488 3688 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4203 3688 603 41 0 4162 0
vsize: 16812
[startup+489.987 s]
Raw data (loadavg): 0.99 0.79 0.41 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3709 0 1 0 48991 10 0 0 25 0 1 0 420221446 17215488 3688 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4203 3688 603 41 0 4162 0
vsize: 16812
[startup+499.987 s]
Raw data (loadavg): 0.99 0.80 0.42 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3739 0 1 0 49991 10 0 0 25 0 1 0 420221446 17350656 3718 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4236 3718 603 41 0 4195 0
vsize: 16944
[startup+509.987 s]
Raw data (loadavg): 0.99 0.81 0.43 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3744 0 1 0 50991 10 0 0 25 0 1 0 420221446 17350656 3723 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4236 3723 603 41 0 4195 0
vsize: 16944
[startup+519.987 s]
Raw data (loadavg): 0.99 0.81 0.43 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3761 0 1 0 51992 10 0 0 25 0 1 0 420221446 17489920 3740 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4270 3740 603 41 0 4229 0
vsize: 17080
[startup+529.986 s]
Raw data (loadavg): 0.99 0.82 0.44 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3774 0 1 0 52992 10 0 0 25 0 1 0 420221446 17489920 3753 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4270 3753 603 41 0 4229 0
vsize: 17080
[startup+539.987 s]
Raw data (loadavg): 0.99 0.82 0.44 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3795 0 1 0 53992 10 0 0 25 0 1 0 420221446 17637376 3774 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4306 3774 603 41 0 4265 0
vsize: 17224
[startup+549.987 s]
Raw data (loadavg): 0.99 0.83 0.45 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3795 0 1 0 54992 10 0 0 25 0 1 0 420221446 17637376 3774 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4306 3774 603 41 0 4265 0
vsize: 17224
[startup+559.986 s]
Raw data (loadavg): 0.99 0.83 0.46 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3819 0 1 0 55993 10 0 0 25 0 1 0 420221446 17784832 3798 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4342 3798 603 41 0 4301 0
vsize: 17368
[startup+569.986 s]
Raw data (loadavg): 0.99 0.84 0.46 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3820 0 1 0 56993 10 0 0 25 0 1 0 420221446 17784832 3799 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4342 3799 603 41 0 4301 0
vsize: 17368
[startup+579.986 s]
Raw data (loadavg): 0.99 0.84 0.47 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3832 0 1 0 57993 10 0 0 25 0 1 0 420221446 17784832 3811 4294967295 134512640 134672761 3221224544 3221223712 134559068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4342 3811 603 41 0 4301 0
vsize: 17368
[startup+589.985 s]
Raw data (loadavg): 0.99 0.85 0.47 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3855 0 1 0 58993 10 0 0 25 0 1 0 420221446 17948672 3834 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4382 3834 603 41 0 4341 0
vsize: 17528
[startup+599.985 s]
Raw data (loadavg): 0.99 0.85 0.48 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3869 0 1 0 59993 10 0 0 25 0 1 0 420221446 17948672 3848 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4382 3848 603 41 0 4341 0
vsize: 17528
[startup+609.985 s]
Raw data (loadavg): 0.99 0.86 0.48 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3869 0 1 0 60994 10 0 0 25 0 1 0 420221446 17948672 3848 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4382 3848 603 41 0 4341 0
vsize: 17528
[startup+619.984 s]
Raw data (loadavg): 0.99 0.86 0.49 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3869 0 1 0 61994 10 0 0 25 0 1 0 420221446 17948672 3848 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4382 3848 603 41 0 4341 0
vsize: 17528
[startup+629.984 s]
Raw data (loadavg): 0.99 0.86 0.49 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3872 0 1 0 62994 10 0 0 25 0 1 0 420221446 17948672 3851 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4382 3851 603 41 0 4341 0
vsize: 17528
[startup+639.984 s]
Raw data (loadavg): 0.99 0.87 0.50 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3891 0 1 0 63995 10 0 0 25 0 1 0 420221446 18145280 3870 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4430 3870 603 41 0 4389 0
vsize: 17720
[startup+649.984 s]
Raw data (loadavg): 0.99 0.87 0.50 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3891 0 1 0 64995 10 0 0 25 0 1 0 420221446 18145280 3870 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4430 3870 603 41 0 4389 0
vsize: 17720
[startup+659.984 s]
Raw data (loadavg): 0.99 0.88 0.50 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3891 0 1 0 65995 10 0 0 25 0 1 0 420221446 18145280 3870 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4430 3870 603 41 0 4389 0
vsize: 17720
[startup+669.984 s]
Raw data (loadavg): 0.99 0.88 0.51 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3893 0 1 0 66995 11 0 0 25 0 1 0 420221446 18145280 3872 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4430 3872 603 41 0 4389 0
vsize: 17720
[startup+679.984 s]
Raw data (loadavg): 0.99 0.88 0.51 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3911 0 1 0 67995 11 0 0 25 0 1 0 420221446 18341888 3890 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4478 3890 603 41 0 4437 0
vsize: 17912
[startup+689.984 s]
Raw data (loadavg): 0.99 0.89 0.52 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3920 0 1 0 68996 11 0 0 25 0 1 0 420221446 18341888 3899 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4478 3899 603 41 0 4437 0
vsize: 17912
[startup+699.984 s]
Raw data (loadavg): 0.99 0.89 0.52 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3934 0 1 0 69996 11 0 0 25 0 1 0 420221446 18341888 3913 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4478 3913 603 41 0 4437 0
vsize: 17912
[startup+709.984 s]
Raw data (loadavg): 0.99 0.89 0.53 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3934 0 1 0 70996 11 0 0 25 0 1 0 420221446 18341888 3913 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4478 3913 603 41 0 4437 0
vsize: 17912
[startup+719.984 s]
Raw data (loadavg): 0.99 0.90 0.53 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3945 0 1 0 71997 11 0 0 25 0 1 0 420221446 18538496 3924 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4526 3924 603 41 0 4485 0
vsize: 18104
[startup+729.983 s]
Raw data (loadavg): 0.99 0.90 0.54 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3956 0 1 0 72997 11 0 0 25 0 1 0 420221446 18538496 3935 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4526 3935 603 41 0 4485 0
vsize: 18104
[startup+739.984 s]
Raw data (loadavg): 0.99 0.90 0.54 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3972 0 1 0 73997 11 0 0 25 0 1 0 420221446 18538496 3951 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4526 3951 603 41 0 4485 0
vsize: 18104
[startup+749.984 s]
Raw data (loadavg): 0.99 0.90 0.55 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3973 0 1 0 74998 11 0 0 25 0 1 0 420221446 18538496 3952 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4526 3952 603 41 0 4485 0
vsize: 18104
[startup+759.984 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 3984 0 1 0 75998 11 0 0 25 0 1 0 420221446 18735104 3963 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4574 3963 603 41 0 4533 0
vsize: 18296
[startup+769.984 s]
Raw data (loadavg): 0.99 0.91 0.56 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4035 0 1 0 76998 11 0 0 25 0 1 0 420221446 18870272 4014 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4607 4014 603 41 0 4566 0
vsize: 18428
[startup+779.984 s]
Raw data (loadavg): 0.99 0.91 0.56 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4053 0 1 0 77998 11 0 0 25 0 1 0 420221446 19030016 4032 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4646 4032 603 41 0 4605 0
vsize: 18584
[startup+789.984 s]
Raw data (loadavg): 0.99 0.91 0.56 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4063 0 1 0 78999 11 0 0 25 0 1 0 420221446 19030016 4042 4294967295 134512640 134672761 3221224544 3221223648 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4646 4042 603 41 0 4605 0
vsize: 18584
[startup+799.984 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4068 0 1 0 79999 11 0 0 25 0 1 0 420221446 19193856 4047 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4686 4047 603 41 0 4645 0
vsize: 18744
[startup+809.984 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4068 0 1 0 80999 11 0 0 25 0 1 0 420221446 19193856 4047 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4686 4047 603 41 0 4645 0
vsize: 18744
[startup+819.984 s]
Raw data (loadavg): 0.99 0.92 0.58 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4081 0 1 0 82000 11 0 0 25 0 1 0 420221446 19193856 4060 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4686 4060 603 41 0 4645 0
vsize: 18744
[startup+829.984 s]
Raw data (loadavg): 0.99 0.92 0.58 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4085 0 1 0 83000 11 0 0 25 0 1 0 420221446 19193856 4064 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4686 4064 603 41 0 4645 0
vsize: 18744
[startup+839.984 s]
Raw data (loadavg): 0.99 0.92 0.58 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4113 0 1 0 84000 11 0 0 25 0 1 0 420221446 19378176 4092 4294967295 134512640 134672761 3221224544 3221223648 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4731 4092 603 41 0 4690 0
vsize: 18924
[startup+849.984 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4126 0 1 0 85000 11 0 0 25 0 1 0 420221446 19378176 4105 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4731 4105 603 41 0 4690 0
vsize: 18924
[startup+859.985 s]
Raw data (loadavg): 0.99 0.93 0.59 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4138 0 1 0 86001 11 0 0 25 0 1 0 420221446 19574784 4117 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4779 4117 603 41 0 4738 0
vsize: 19116
[startup+869.985 s]
Raw data (loadavg): 0.99 0.93 0.60 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4151 0 1 0 87001 11 0 0 25 0 1 0 420221446 19574784 4130 4294967295 134512640 134672761 3221224544 3221223648 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4779 4130 603 41 0 4738 0
vsize: 19116
[startup+879.985 s]
Raw data (loadavg): 0.99 0.93 0.60 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4153 0 1 0 88001 11 0 0 25 0 1 0 420221446 19574784 4132 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4779 4132 603 41 0 4738 0
vsize: 19116
[startup+889.985 s]
Raw data (loadavg): 0.99 0.93 0.60 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4165 0 1 0 89001 12 0 0 25 0 1 0 420221446 19574784 4144 4294967295 134512640 134672761 3221224544 3221223720 134559059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4779 4144 603 41 0 4738 0
vsize: 19116
[startup+899.985 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4165 0 1 0 90002 12 0 0 25 0 1 0 420221446 19574784 4144 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4779 4144 603 41 0 4738 0
vsize: 19116
[startup+909.985 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4199 0 1 0 91002 12 0 0 25 0 1 0 420221446 19771392 4178 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4827 4178 603 41 0 4786 0
vsize: 19308
[startup+919.986 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4202 0 1 0 92002 12 0 0 25 0 1 0 420221446 19771392 4181 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4827 4181 603 41 0 4786 0
vsize: 19308
[startup+929.986 s]
Raw data (loadavg): 0.99 0.94 0.62 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4212 0 1 0 93003 12 0 0 25 0 1 0 420221446 19968000 4191 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4875 4191 603 41 0 4834 0
vsize: 19500
[startup+939.985 s]
Raw data (loadavg): 0.99 0.94 0.62 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4224 0 1 0 94003 12 0 0 25 0 1 0 420221446 19968000 4203 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4875 4204 603 41 0 4834 0
vsize: 19500
[startup+949.986 s]
Raw data (loadavg): 0.99 0.94 0.63 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4238 0 1 0 95003 12 0 0 25 0 1 0 420221446 19968000 4217 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4875 4217 603 41 0 4834 0
vsize: 19500
[startup+959.986 s]
Raw data (loadavg): 0.99 0.94 0.63 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4238 0 1 0 96004 12 0 0 25 0 1 0 420221446 19968000 4217 4294967295 134512640 134672761 3221224544 3221223712 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4875 4217 603 41 0 4834 0
vsize: 19500
[startup+969.986 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4268 0 1 0 97004 12 0 0 25 0 1 0 420221446 20164608 4247 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4923 4247 603 41 0 4882 0
vsize: 19692
[startup+979.986 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4289 0 1 0 98004 12 0 0 25 0 1 0 420221446 20361216 4268 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4971 4268 603 41 0 4930 0
vsize: 19884
[startup+989.987 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4289 0 1 0 99005 12 0 0 25 0 1 0 420221446 20361216 4268 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4971 4268 603 41 0 4930 0
vsize: 19884
[startup+999.986 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4290 0 1 0 100005 12 0 0 25 0 1 0 420221446 20361216 4269 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4971 4269 603 41 0 4930 0
vsize: 19884
[startup+1009.99 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4290 0 1 0 101005 12 0 0 25 0 1 0 420221446 20361216 4269 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4971 4269 603 41 0 4930 0
vsize: 19884
[startup+1019.99 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4291 0 1 0 102006 12 0 0 25 0 1 0 420221446 20361216 4270 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4971 4270 603 41 0 4930 0
vsize: 19884
[startup+1029.99 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4292 0 1 0 103006 12 0 0 25 0 1 0 420221446 20361216 4271 4294967295 134512640 134672761 3221224544 3221223728 134559365 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4971 4271 603 41 0 4930 0
vsize: 19884
[startup+1039.99 s]
Raw data (loadavg): 0.99 0.95 0.66 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4293 0 1 0 104006 12 0 0 25 0 1 0 420221446 20361216 4272 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4971 4272 603 41 0 4930 0
vsize: 19884
[startup+1049.99 s]
Raw data (loadavg): 0.99 0.95 0.66 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4293 0 1 0 105007 12 0 0 25 0 1 0 420221446 20361216 4272 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4971 4272 603 41 0 4930 0
vsize: 19884
[startup+1059.99 s]
Raw data (loadavg): 0.99 0.95 0.66 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4293 0 1 0 106007 12 0 0 25 0 1 0 420221446 20361216 4272 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4971 4272 603 41 0 4930 0
vsize: 19884
[startup+1069.99 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4293 0 1 0 107007 12 0 0 25 0 1 0 420221446 20361216 4272 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4971 4272 603 41 0 4930 0
vsize: 19884
[startup+1079.99 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4296 0 1 0 108008 12 0 0 25 0 1 0 420221446 20361216 4275 4294967295 134512640 134672761 3221224544 3221223728 134559376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4971 4275 603 41 0 4930 0
vsize: 19884
[startup+1089.99 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4297 0 1 0 109008 12 0 0 25 0 1 0 420221446 20361216 4276 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4971 4276 603 41 0 4930 0
vsize: 19884
[startup+1099.99 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4297 0 1 0 110008 12 0 0 25 0 1 0 420221446 20361216 4276 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4971 4276 603 41 0 4930 0
vsize: 19884
[startup+1109.99 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4297 0 1 0 111008 12 0 0 25 0 1 0 420221446 20361216 4276 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4971 4276 603 41 0 4930 0
vsize: 19884
[startup+1119.99 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4318 0 1 0 112009 12 0 0 25 0 1 0 420221446 20557824 4297 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5019 4297 603 41 0 4978 0
vsize: 20076
[startup+1129.99 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4321 0 1 0 113009 12 0 0 25 0 1 0 420221446 20557824 4300 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5019 4300 603 41 0 4978 0
vsize: 20076
[startup+1139.99 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4336 0 1 0 114009 12 0 0 25 0 1 0 420221446 20557824 4315 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5019 4315 603 41 0 4978 0
vsize: 20076
[startup+1149.99 s]
Raw data (loadavg): 0.99 0.96 0.69 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4340 0 1 0 115010 12 0 0 25 0 1 0 420221446 20557824 4319 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5019 4319 603 41 0 4978 0
vsize: 20076
[startup+1159.99 s]
Raw data (loadavg): 0.99 0.96 0.69 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4340 0 1 0 116010 12 0 0 25 0 1 0 420221446 20557824 4319 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5019 4319 603 41 0 4978 0
vsize: 20076
[startup+1169.99 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4355 0 1 0 117010 12 0 0 25 0 1 0 420221446 20701184 4334 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5054 4334 603 41 0 5013 0
vsize: 20216
[startup+1179.99 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4384 0 1 0 118010 12 0 0 25 0 1 0 420221446 20844544 4363 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5089 4363 603 41 0 5048 0
vsize: 20356
[startup+1189.99 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4384 0 1 0 119011 12 0 0 25 0 1 0 420221446 20844544 4363 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5089 4363 603 41 0 5048 0
vsize: 20356
[startup+1199.99 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 31347
Raw data (stat): 31347 (minisat+) R 31346 29653 29652 0 -1 0 4384 0 1 0 120011 12 0 0 25 0 1 0 420221446 20844544 4363 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5089 4363 603 41 0 5048 0
vsize: 20356
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200 s]
Raw data (loadavg): 0.99 0.97 0.70 1/54 31347
Raw data (stat): 31347 (minisat+) Z 31346 29653 29652 0 -1 12 4386 0 1 0 120011 13 0 0 25 0 1 0 420221446 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
CPU time (s): 1200.25
CPU user time (s): 1200.12
CPU system time (s): 0.137979
CPU usage (%): 100.021
Max. virtual memory (Kb): 20356
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####