PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/aloul/FPGA_SAT05/normalized-fpga30_28_sat_pb.cnf.cr.opb
MD5SUM	888577ab8fe81abf9fdd366d65e4c3b7
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	YES
(Un)Satisfiability was proved	YES
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	31
Number of bits of the biggest sum of numbers	5
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.810876
Number of variables	1260
Total number of constraints	926
Number of constraints which are clauses	868
Number of constraints which are cardinality constraints (but not clauses)	58
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	15
Maximum length of a constraint	30
Trace number 5396

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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:        895512 kB
Buffers:         34620 kB
Cached:          68532 kB
SwapCached:          4 kB
Active:          51588 kB
Inactive:        54436 kB
HighTotal:      131008 kB
HighFree:        58856 kB
LowTotal:       903652 kB
LowFree:        836656 kB
SwapTotal:     2097640 kB
SwapFree:      2097636 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            27600 kB
Committed_AS:    63476 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:59:16 (client local time) WITH STATUS 0 IN 1200.22 SECONDS
stats: 3806 7 1200.22 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 926 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  57]---> BDD-cost:   53
c ---[  56]---> BDD-cost:   53
c ---[  55]---> BDD-cost:   53
c ---[  54]---> BDD-cost:   53
c ---[  53]---> BDD-cost:   53
c ---[  52]---> BDD-cost:   53
c ---[  51]---> BDD-cost:   53
c ---[  50]---> BDD-cost:   53
c ---[  49]---> BDD-cost:   53
c ---[  48]---> BDD-cost:   53
c ---[  47]---> BDD-cost:   53
c ---[  46]---> BDD-cost:   53
c ---[  45]---> BDD-cost:   53
c ---[  44]---> BDD-cost:   53
c ---[  43]---> BDD-cost:   53
c ---[  42]---> BDD-cost:   53
c ---[  41]---> BDD-cost:   53
c ---[  40]---> BDD-cost:   53
c ---[  39]---> BDD-cost:   53
c ---[  38]---> BDD-cost:   53
c ---[  37]---> BDD-cost:   53
c ---[  36]---> BDD-cost:   53
c ---[  35]---> BDD-cost:   53
c ---[  34]---> BDD-cost:   53
c ---[  33]---> BDD-cost:   53
c ---[  32]---> BDD-cost:   53
c ---[  31]---> BDD-cost:   53
c ---[  30]---> BDD-cost:   53
c ---[  29]---> BDD-cost:   53
c ---[  28]---> BDD-cost:   53
c ---[  27]---> BDD-cost:   27
c ---[  26]---> BDD-cost:   27
c ---[  25]---> BDD-cost:   27
c ---[  24]---> BDD-cost:   27
c ---[  23]---> BDD-cost:   27
c ---[  22]---> BDD-cost:   27
c ---[  21]---> BDD-cost:   27
c ---[  20]---> BDD-cost:   27
c ---[  19]---> BDD-cost:   27
c ---[  18]---> BDD-cost:   27
c ---[  17]---> BDD-cost:   27
c ---[  16]---> BDD-cost:   27
c ---[  15]---> BDD-cost:   27
c ---[  14]---> BDD-cost:   27
c ---[  13]---> BDD-cost:   27
c ---[  12]---> BDD-cost:   27
c ---[  11]---> BDD-cost:   27
c ---[  10]---> BDD-cost:   27
c ---[   9]---> BDD-cost:   27
c ---[   8]---> BDD-cost:   27
c ---[   7]---> BDD-cost:   27
c ---[   6]---> BDD-cost:   27
c ---[   5]---> BDD-cost:   27
c ---[   4]---> BDD-cost:   27
c ---[   3]---> BDD-cost:   27
c ---[   2]---> BDD-cost:   27
c ---[   1]---> BDD-cost:   27
c ---[   0]---> BDD-cost:   27
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    6646    28486 |    1993       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3548          
c   -- var.elim.:  2000/3548          
c   -- var.elim.:  3000/3548          
c   -- var.elim.:  3548/3548          
c   -- var.elim.:  1000/1273          
c   -- var.elim.:  1273/1273          
c   -- subsuming                       
c   -- var.elim.:  1000/1086          
c   -- var.elim.:  1086/1086          
c   -- var.elim.:  1000/1228          
c   -- var.elim.:  1228/1228          
c   -- subsuming                       
c   -- var.elim.:  530/530          
c   -- var.elim.:  973/973          
c   -- subsuming                       
c   -- var.elim.:  886/886          
c |         0 |    6212    29459 |      --       0       --      -- |     --   | -434/1147
c |         0 |    6212    29459 |    2484       0        0     nan |  0.000 % |
c#### 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.38 0.73 0.85 2/54 16672
Raw data (stat): 16672 (runsolver) R 16671 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479981419 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+9.99965 s]
Raw data (loadavg): 0.48 0.74 0.85 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 2621 0 0 0 990 7 0 0 25 0 1 0 479981419 12271616 2598 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2996 2598 603 41 0 2955 0
vsize: 11984
[startup+20 s]
Raw data (loadavg): 0.56 0.75 0.85 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 2986 0 0 0 1989 8 0 0 25 0 1 0 479981419 13688832 2963 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3342 2964 603 41 0 3301 0
vsize: 13368
[startup+30 s]
Raw data (loadavg): 0.62 0.75 0.85 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 3685 0 0 0 2987 10 0 0 25 0 1 0 479981419 16576512 3662 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4047 3662 603 41 0 4006 0
vsize: 16188
[startup+40.001 s]
Raw data (loadavg): 0.68 0.76 0.85 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 3685 0 0 0 3987 11 0 0 25 0 1 0 479981419 16576512 3662 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4047 3662 603 41 0 4006 0
vsize: 16188
[startup+50.0011 s]
Raw data (loadavg): 0.73 0.77 0.85 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 3715 0 0 0 4988 11 0 0 25 0 1 0 479981419 16707584 3692 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4079 3692 603 41 0 4038 0
vsize: 16316
[startup+60.0011 s]
Raw data (loadavg): 0.77 0.78 0.85 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 3738 0 0 0 5988 11 0 0 25 0 1 0 479981419 16838656 3715 4294967295 134512640 134672761 3221224528 3221223712 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4111 3715 603 41 0 4070 0
vsize: 16444
[startup+70.0017 s]
Raw data (loadavg): 0.81 0.78 0.85 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 3897 0 0 0 6987 11 0 0 25 0 1 0 479981419 17502208 3874 4294967295 134512640 134672761 3221224528 3221223520 134565089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4273 3874 603 41 0 4232 0
vsize: 17092
[startup+80.0021 s]
Raw data (loadavg): 0.83 0.79 0.86 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 4078 0 0 0 7986 12 0 0 25 0 1 0 479981419 18268160 4055 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4460 4055 603 41 0 4419 0
vsize: 17840
[startup+90.0031 s]
Raw data (loadavg): 0.86 0.80 0.86 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 4288 0 0 0 8986 13 0 0 25 0 1 0 479981419 19140608 4265 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4673 4265 603 41 0 4632 0
vsize: 18692
[startup+100.003 s]
Raw data (loadavg): 0.88 0.80 0.86 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 4514 0 0 0 9986 13 0 0 25 0 1 0 479981419 20025344 4491 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4889 4491 603 41 0 4848 0
vsize: 19556
[startup+110.003 s]
Raw data (loadavg): 0.90 0.81 0.86 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 4955 0 0 0 10985 14 0 0 25 0 1 0 479981419 21831680 4932 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5330 4932 603 41 0 5289 0
vsize: 21320
[startup+120.004 s]
Raw data (loadavg): 0.91 0.81 0.86 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 4955 0 0 0 11985 14 0 0 25 0 1 0 479981419 21831680 4932 4294967295 134512640 134672761 3221224528 3221223712 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5330 4932 603 41 0 5289 0
vsize: 21320
[startup+130.004 s]
Raw data (loadavg): 0.93 0.82 0.86 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 4975 0 0 0 12985 14 0 0 25 0 1 0 479981419 21917696 4952 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5351 4952 603 41 0 5310 0
vsize: 21404
[startup+140.003 s]
Raw data (loadavg): 0.94 0.83 0.86 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 4975 0 0 0 13985 14 0 0 25 0 1 0 479981419 21901312 4952 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5347 4952 603 41 0 5306 0
vsize: 21388
[startup+150.004 s]
Raw data (loadavg): 0.95 0.83 0.86 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 4975 0 0 0 14986 14 0 0 25 0 1 0 479981419 21901312 4952 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5347 4952 603 41 0 5306 0
vsize: 21388
[startup+160.004 s]
Raw data (loadavg): 0.95 0.84 0.86 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 4975 0 0 0 15986 14 0 0 25 0 1 0 479981419 21901312 4952 4294967295 134512640 134672761 3221224528 3221223624 134616139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5347 4952 603 41 0 5306 0
vsize: 21388
[startup+170.004 s]
Raw data (loadavg): 0.96 0.84 0.86 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 4975 0 0 0 16986 14 0 0 25 0 1 0 479981419 21901312 4952 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5347 4952 603 41 0 5306 0
vsize: 21388
[startup+180.004 s]
Raw data (loadavg): 0.97 0.85 0.87 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 4975 0 0 0 17986 14 0 0 25 0 1 0 479981419 21901312 4952 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5347 4952 603 41 0 5306 0
vsize: 21388
[startup+190.004 s]
Raw data (loadavg): 0.97 0.85 0.87 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 4976 0 0 0 18986 14 0 0 25 0 1 0 479981419 21901312 4953 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5347 4953 603 41 0 5306 0
vsize: 21388
[startup+200.003 s]
Raw data (loadavg): 0.98 0.85 0.87 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 5288 0 0 0 19985 16 0 0 25 0 1 0 479981419 23195648 5265 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5663 5265 603 41 0 5622 0
vsize: 22652
[startup+210.003 s]
Raw data (loadavg): 0.98 0.86 0.87 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 5909 0 0 0 20984 17 0 0 25 0 1 0 479981419 25686016 5886 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6271 5886 603 41 0 6230 0
vsize: 25084
[startup+220.004 s]
Raw data (loadavg): 0.98 0.86 0.87 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6159 0 0 0 21983 18 0 0 25 0 1 0 479981419 26738688 6136 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6528 6136 603 41 0 6487 0
vsize: 26112
[startup+230.004 s]
Raw data (loadavg): 0.98 0.87 0.87 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6344 0 0 0 22983 18 0 0 25 0 1 0 479981419 27521024 6321 4294967295 134512640 134672761 3221224528 3221223712 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6719 6321 603 41 0 6678 0
vsize: 26876
[startup+240.004 s]
Raw data (loadavg): 0.99 0.87 0.87 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6344 0 0 0 23983 18 0 0 25 0 1 0 479981419 27521024 6321 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6719 6321 603 41 0 6678 0
vsize: 26876
[startup+250.004 s]
Raw data (loadavg): 0.99 0.87 0.87 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6345 0 0 0 24983 18 0 0 25 0 1 0 479981419 27521024 6322 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6719 6322 603 41 0 6678 0
vsize: 26876
[startup+260.003 s]
Raw data (loadavg): 0.99 0.88 0.87 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6345 0 0 0 25983 18 0 0 25 0 1 0 479981419 27521024 6322 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6719 6322 603 41 0 6678 0
vsize: 26876
[startup+270.004 s]
Raw data (loadavg): 0.99 0.88 0.87 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6346 0 0 0 26984 18 0 0 25 0 1 0 479981419 27521024 6323 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6719 6323 603 41 0 6678 0
vsize: 26876
[startup+280.004 s]
Raw data (loadavg): 0.99 0.89 0.87 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6359 0 0 0 27984 18 0 0 25 0 1 0 479981419 27607040 6336 4294967295 134512640 134672761 3221224528 3221223712 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6740 6336 603 41 0 6699 0
vsize: 26960
[startup+290.003 s]
Raw data (loadavg): 0.99 0.89 0.88 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6466 0 0 0 28984 19 0 0 25 0 1 0 479981419 28004352 6443 4294967295 134512640 134672761 3221224528 3221223624 134616320 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6443 603 41 0 6796 0
vsize: 27348
[startup+300.004 s]
Raw data (loadavg): 0.99 0.89 0.88 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6468 0 0 0 29984 19 0 0 25 0 1 0 479981419 28004352 6445 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6445 603 41 0 6796 0
vsize: 27348
[startup+310.004 s]
Raw data (loadavg): 0.99 0.89 0.88 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6468 0 0 0 30984 19 0 0 25 0 1 0 479981419 28004352 6445 4294967295 134512640 134672761 3221224528 3221223712 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6445 603 41 0 6796 0
vsize: 27348
[startup+320.005 s]
Raw data (loadavg): 0.99 0.90 0.88 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6468 0 0 0 31984 19 0 0 25 0 1 0 479981419 28004352 6445 4294967295 134512640 134672761 3221224528 3221223712 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6445 603 41 0 6796 0
vsize: 27348
[startup+330.005 s]
Raw data (loadavg): 0.99 0.90 0.88 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6468 0 0 0 32984 19 0 0 25 0 1 0 479981419 28004352 6445 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6445 603 41 0 6796 0
vsize: 27348
[startup+340.004 s]
Raw data (loadavg): 0.99 0.90 0.88 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6468 0 0 0 33985 19 0 0 25 0 1 0 479981419 28004352 6445 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6445 603 41 0 6796 0
vsize: 27348
[startup+350.005 s]
Raw data (loadavg): 0.99 0.91 0.88 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6468 0 0 0 34985 19 0 0 25 0 1 0 479981419 28004352 6445 4294967295 134512640 134672761 3221224528 3221223568 134612701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6445 603 41 0 6796 0
vsize: 27348
[startup+360.005 s]
Raw data (loadavg): 0.99 0.91 0.88 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6468 0 0 0 35985 19 0 0 25 0 1 0 479981419 28004352 6445 4294967295 134512640 134672761 3221224528 3221223712 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6445 603 41 0 6796 0
vsize: 27348
[startup+370.005 s]
Raw data (loadavg): 0.99 0.91 0.88 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6468 0 0 0 36985 19 0 0 25 0 1 0 479981419 28004352 6445 4294967295 134512640 134672761 3221224528 3221223712 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6445 603 41 0 6796 0
vsize: 27348
[startup+380.005 s]
Raw data (loadavg): 0.99 0.91 0.88 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6468 0 0 0 37985 19 0 0 25 0 1 0 479981419 28004352 6445 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6445 603 41 0 6796 0
vsize: 27348
[startup+390.005 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6468 0 0 0 38985 19 0 0 25 0 1 0 479981419 28004352 6445 4294967295 134512640 134672761 3221224528 3221223712 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6445 603 41 0 6796 0
vsize: 27348
[startup+400.005 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6468 0 0 0 39986 19 0 0 25 0 1 0 479981419 28004352 6445 4294967295 134512640 134672761 3221224528 3221223712 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6445 603 41 0 6796 0
vsize: 27348
[startup+410.004 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6468 0 0 0 40986 19 0 0 25 0 1 0 479981419 28004352 6445 4294967295 134512640 134672761 3221224528 3221223568 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6445 603 41 0 6796 0
vsize: 27348
[startup+420.005 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6468 0 0 0 41986 19 0 0 25 0 1 0 479981419 28004352 6445 4294967295 134512640 134672761 3221224528 3221223712 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6445 603 41 0 6796 0
vsize: 27348
[startup+430.004 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6468 0 0 0 42986 19 0 0 25 0 1 0 479981419 28004352 6445 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6445 603 41 0 6796 0
vsize: 27348
[startup+440.004 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6468 0 0 0 43986 19 0 0 25 0 1 0 479981419 28004352 6445 4294967295 134512640 134672761 3221224528 3221223712 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6445 603 41 0 6796 0
vsize: 27348
[startup+450.005 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6468 0 0 0 44986 19 0 0 25 0 1 0 479981419 28004352 6445 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6445 603 41 0 6796 0
vsize: 27348
[startup+460.005 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6468 0 0 0 45987 19 0 0 25 0 1 0 479981419 28004352 6445 4294967295 134512640 134672761 3221224528 3221223712 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6445 603 41 0 6796 0
vsize: 27348
[startup+470.005 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6469 0 0 0 46987 19 0 0 25 0 1 0 479981419 28004352 6446 4294967295 134512640 134672761 3221224528 3221223712 134615635 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6446 603 41 0 6796 0
vsize: 27348
[startup+480.005 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6470 0 0 0 47987 19 0 0 25 0 1 0 479981419 28004352 6447 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6447 603 41 0 6796 0
vsize: 27348
[startup+490.004 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6470 0 0 0 48987 19 0 0 25 0 1 0 479981419 28004352 6447 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6447 603 41 0 6796 0
vsize: 27348
[startup+500.005 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6470 0 0 0 49987 19 0 0 25 0 1 0 479981419 28004352 6447 4294967295 134512640 134672761 3221224528 3221223712 134615773 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6447 603 41 0 6796 0
vsize: 27348
[startup+510.005 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6470 0 0 0 50988 19 0 0 25 0 1 0 479981419 28004352 6447 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6447 603 41 0 6796 0
vsize: 27348
[startup+520.006 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6470 0 0 0 51988 19 0 0 25 0 1 0 479981419 28004352 6447 4294967295 134512640 134672761 3221224528 3221223712 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6447 603 41 0 6796 0
vsize: 27348
[startup+530.006 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6470 0 0 0 52988 19 0 0 25 0 1 0 479981419 28004352 6447 4294967295 134512640 134672761 3221224528 3221223568 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6447 603 41 0 6796 0
vsize: 27348
[startup+540.006 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6471 0 0 0 53988 19 0 0 25 0 1 0 479981419 28004352 6448 4294967295 134512640 134672761 3221224528 3221223728 134610644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6448 603 41 0 6796 0
vsize: 27348
[startup+550.006 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6471 0 0 0 54988 19 0 0 25 0 1 0 479981419 28004352 6448 4294967295 134512640 134672761 3221224528 3221223712 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6448 603 41 0 6796 0
vsize: 27348
[startup+560.006 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6471 0 0 0 55989 19 0 0 25 0 1 0 479981419 28004352 6448 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6448 603 41 0 6796 0
vsize: 27348
[startup+570.006 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6471 0 0 0 56989 19 0 0 25 0 1 0 479981419 28004352 6448 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6837 6448 603 41 0 6796 0
vsize: 27348
[startup+580.006 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6833 0 0 0 57988 19 0 0 25 0 1 0 479981419 29544448 6810 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7213 6810 603 41 0 7172 0
vsize: 28852
[startup+590.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6855 0 0 0 58989 19 0 0 25 0 1 0 479981419 29642752 6832 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7237 6832 603 41 0 7196 0
vsize: 28948
[startup+600.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6855 0 0 0 59989 19 0 0 25 0 1 0 479981419 29642752 6832 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7237 6832 603 41 0 7196 0
vsize: 28948
[startup+610.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6855 0 0 0 60989 19 0 0 25 0 1 0 479981419 29642752 6832 4294967295 134512640 134672761 3221224528 3221223712 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7237 6832 603 41 0 7196 0
vsize: 28948
[startup+620.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6855 0 0 0 61989 19 0 0 25 0 1 0 479981419 29642752 6832 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7237 6832 603 41 0 7196 0
vsize: 28948
[startup+630.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6855 0 0 0 62989 19 0 0 25 0 1 0 479981419 29642752 6832 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7237 6832 603 41 0 7196 0
vsize: 28948
[startup+640.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6855 0 0 0 63989 19 0 0 25 0 1 0 479981419 29642752 6832 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7237 6832 603 41 0 7196 0
vsize: 28948
[startup+650.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6855 0 0 0 64990 19 0 0 25 0 1 0 479981419 29642752 6832 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7237 6832 603 41 0 7196 0
vsize: 28948
[startup+660.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6855 0 0 0 65990 19 0 0 25 0 1 0 479981419 29642752 6832 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7237 6832 603 41 0 7196 0
vsize: 28948
[startup+670.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6855 0 0 0 66990 19 0 0 25 0 1 0 479981419 29642752 6832 4294967295 134512640 134672761 3221224528 3221223712 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7237 6832 603 41 0 7196 0
vsize: 28948
[startup+680.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6855 0 0 0 67990 19 0 0 25 0 1 0 479981419 29642752 6832 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7237 6832 603 41 0 7196 0
vsize: 28948
[startup+690.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6855 0 0 0 68990 19 0 0 25 0 1 0 479981419 29642752 6832 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7237 6832 603 41 0 7196 0
vsize: 28948
[startup+700.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6855 0 0 0 69991 19 0 0 25 0 1 0 479981419 29642752 6832 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7237 6832 603 41 0 7196 0
vsize: 28948
[startup+710.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6855 0 0 0 70991 19 0 0 25 0 1 0 479981419 29642752 6832 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7237 6832 603 41 0 7196 0
vsize: 28948
[startup+720.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6855 0 0 0 71991 19 0 0 25 0 1 0 479981419 29642752 6832 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7237 6832 603 41 0 7196 0
vsize: 28948
[startup+730.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6855 0 0 0 72991 19 0 0 25 0 1 0 479981419 29642752 6832 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7237 6832 603 41 0 7196 0
vsize: 28948
[startup+740.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6855 0 0 0 73991 19 0 0 25 0 1 0 479981419 29642752 6832 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7237 6832 603 41 0 7196 0
vsize: 28948
[startup+750.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6855 0 0 0 74991 19 0 0 25 0 1 0 479981419 29642752 6832 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7237 6832 603 41 0 7196 0
vsize: 28948
[startup+760.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6855 0 0 0 75992 19 0 0 25 0 1 0 479981419 29642752 6832 4294967295 134512640 134672761 3221224528 3221223568 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7237 6832 603 41 0 7196 0
vsize: 28948
[startup+770.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6855 0 0 0 76992 19 0 0 25 0 1 0 479981419 29642752 6832 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7237 6832 603 41 0 7196 0
vsize: 28948
[startup+780.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6855 0 0 0 77992 19 0 0 25 0 1 0 479981419 29642752 6832 4294967295 134512640 134672761 3221224528 3221223568 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7237 6832 603 41 0 7196 0
vsize: 28948
[startup+790.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6855 0 0 0 78992 19 0 0 25 0 1 0 479981419 29642752 6832 4294967295 134512640 134672761 3221224528 3221223712 134615611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7237 6832 603 41 0 7196 0
vsize: 28948
[startup+800.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6855 0 0 0 79992 19 0 0 25 0 1 0 479981419 29642752 6832 4294967295 134512640 134672761 3221224528 3221223568 134612694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7237 6832 603 41 0 7196 0
vsize: 28948
[startup+810.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 6972 0 0 0 80992 20 0 0 25 0 1 0 479981419 30187520 6949 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7370 6949 603 41 0 7329 0
vsize: 29480
[startup+820.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 7554 0 0 0 81990 22 0 0 25 0 1 0 479981419 32567296 7531 4294967295 134512640 134672761 3221224528 3221223624 134616161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7951 7531 603 41 0 7910 0
vsize: 31804
[startup+830.005 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 7569 0 0 0 82990 22 0 0 25 0 1 0 479981419 32534528 7546 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7943 7546 603 41 0 7902 0
vsize: 31772
[startup+840.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8070 0 0 0 83989 24 0 0 25 0 1 0 479981419 34672640 8047 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8465 8047 603 41 0 8424 0
vsize: 33860
[startup+850.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8192 0 0 0 84989 24 0 0 25 0 1 0 479981419 35176448 8169 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8588 8169 603 41 0 8547 0
vsize: 34352
[startup+860.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8198 0 0 0 85989 24 0 0 25 0 1 0 479981419 35176448 8175 4294967295 134512640 134672761 3221224528 3221223712 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8588 8175 603 41 0 8547 0
vsize: 34352
[startup+870.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8584 0 0 0 86988 25 0 0 25 0 1 0 479981419 36786176 8561 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8981 8561 603 41 0 8940 0
vsize: 35924
[startup+880.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8584 0 0 0 87988 25 0 0 25 0 1 0 479981419 36786176 8561 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8981 8561 603 41 0 8940 0
vsize: 35924
[startup+890.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8584 0 0 0 88988 25 0 0 25 0 1 0 479981419 36786176 8561 4294967295 134512640 134672761 3221224528 3221223624 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8981 8561 603 41 0 8940 0
vsize: 35924
[startup+900.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8584 0 0 0 89989 25 0 0 25 0 1 0 479981419 36786176 8561 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8981 8561 603 41 0 8940 0
vsize: 35924
[startup+910.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8584 0 0 0 90989 25 0 0 25 0 1 0 479981419 36786176 8561 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8981 8561 603 41 0 8940 0
vsize: 35924
[startup+920.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8587 0 0 0 91989 25 0 0 25 0 1 0 479981419 36786176 8564 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8981 8564 603 41 0 8940 0
vsize: 35924
[startup+930.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8587 0 0 0 92989 25 0 0 25 0 1 0 479981419 36786176 8564 4294967295 134512640 134672761 3221224528 3221223712 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8981 8564 603 41 0 8940 0
vsize: 35924
[startup+940.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8589 0 0 0 93989 25 0 0 25 0 1 0 479981419 36753408 8561 4294967295 134512640 134672761 3221224528 3221223712 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8973 8561 603 41 0 8932 0
vsize: 35892
[startup+950.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8591 0 0 0 94989 25 0 0 25 0 1 0 479981419 36753408 8563 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8973 8563 603 41 0 8932 0
vsize: 35892
[startup+960.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8593 0 0 0 95990 25 0 0 25 0 1 0 479981419 36753408 8565 4294967295 134512640 134672761 3221224528 3221223712 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8973 8565 603 41 0 8932 0
vsize: 35892
[startup+970.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8593 0 0 0 96990 25 0 0 25 0 1 0 479981419 36753408 8565 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8973 8565 603 41 0 8932 0
vsize: 35892
[startup+980.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8593 0 0 0 97990 25 0 0 25 0 1 0 479981419 36753408 8565 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8973 8565 603 41 0 8932 0
vsize: 35892
[startup+990.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8593 0 0 0 98990 25 0 0 25 0 1 0 479981419 36753408 8565 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8973 8565 603 41 0 8932 0
vsize: 35892
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8593 0 0 0 99990 25 0 0 25 0 1 0 479981419 36753408 8565 4294967295 134512640 134672761 3221224528 3221223712 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8973 8565 603 41 0 8932 0
vsize: 35892
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8593 0 0 0 100991 25 0 0 25 0 1 0 479981419 36753408 8565 4294967295 134512640 134672761 3221224528 3221223712 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8973 8565 603 41 0 8932 0
vsize: 35892
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8593 0 0 0 101991 25 0 0 25 0 1 0 479981419 36753408 8565 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8973 8565 603 41 0 8932 0
vsize: 35892
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8593 0 0 0 102991 25 0 0 25 0 1 0 479981419 36753408 8565 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8973 8565 603 41 0 8932 0
vsize: 35892
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8593 0 0 0 103991 25 0 0 25 0 1 0 479981419 36753408 8565 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8973 8565 603 41 0 8932 0
vsize: 35892
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8593 0 0 0 104991 25 0 0 25 0 1 0 479981419 36753408 8565 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8973 8565 603 41 0 8932 0
vsize: 35892
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8593 0 0 0 105991 25 0 0 25 0 1 0 479981419 36753408 8565 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8973 8565 603 41 0 8932 0
vsize: 35892
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8593 0 0 0 106992 25 0 0 25 0 1 0 479981419 36753408 8565 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8973 8565 603 41 0 8932 0
vsize: 35892
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8593 0 0 0 107992 25 0 0 25 0 1 0 479981419 36753408 8565 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8973 8565 603 41 0 8932 0
vsize: 35892
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8593 0 0 0 108992 25 0 0 25 0 1 0 479981419 36753408 8565 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8973 8565 603 41 0 8932 0
vsize: 35892
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8593 0 0 0 109992 25 0 0 25 0 1 0 479981419 36753408 8565 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8973 8565 603 41 0 8932 0
vsize: 35892
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8593 0 0 0 110993 25 0 0 25 0 1 0 479981419 36753408 8565 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8973 8565 603 41 0 8932 0
vsize: 35892
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8593 0 0 0 111993 25 0 0 25 0 1 0 479981419 36753408 8565 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8973 8565 603 41 0 8932 0
vsize: 35892
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8593 0 0 0 112993 25 0 0 25 0 1 0 479981419 36753408 8565 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8973 8565 603 41 0 8932 0
vsize: 35892
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8593 0 0 0 113993 25 0 0 25 0 1 0 479981419 36753408 8565 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8973 8565 603 41 0 8932 0
vsize: 35892
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8593 0 0 0 114994 25 0 0 25 0 1 0 479981419 36753408 8565 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8973 8565 603 41 0 8932 0
vsize: 35892
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8593 0 0 0 115994 25 0 0 25 0 1 0 479981419 36753408 8565 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8973 8565 603 41 0 8932 0
vsize: 35892
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8593 0 0 0 116994 25 0 0 25 0 1 0 479981419 36753408 8565 4294967295 134512640 134672761 3221224528 3221223712 134615523 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8973 8565 603 41 0 8932 0
vsize: 35892
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8593 0 0 0 117994 25 0 0 25 0 1 0 479981419 36753408 8565 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8973 8565 603 41 0 8932 0
vsize: 35892
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8593 0 0 0 118994 25 0 0 25 0 1 0 479981419 36753408 8565 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8973 8565 603 41 0 8932 0
vsize: 35892
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 16672
Raw data (stat): 16672 (minisat+) R 16671 10614 10613 0 -1 0 8593 0 0 0 119994 25 0 0 25 0 1 0 479981419 36753408 8565 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8973 8565 603 41 0 8932 0
vsize: 35892
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 16672
Raw data (stat): 16672 (minisat+) Z 16671 10614 10613 0 -1 12 8593 0 0 0 119994 27 0 0 25 0 1 0 479981419 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.03
CPU time (s): 1200.22
CPU user time (s): 1199.95
CPU system time (s): 0.270958
CPU usage (%): 100.016
Max. virtual memory (Kb): 35924
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####