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-fpga35_33_sat_pb.cnf.cr.opb
MD5SUM	d4fd8917eebbcee2e1b2df9714e1fab8
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	36
Number of bits of the biggest sum of numbers	6
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.59276
Number of variables	1733
Total number of constraints	1256
Number of constraints which are clauses	1188
Number of constraints which are cardinality constraints (but not clauses)	68
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	17
Maximum length of a constraint	35
Trace number 5397

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-04-13 23:39:34 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3809 boxname=wulflinc24 idbench=49 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  d4fd8917eebbcee2e1b2df9714e1fab8  /oldhome/oroussel/tmp/wulflinc24/normalized-fpga35_33_sat_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc24/normalized-fpga35_33_sat_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc24/normalized-fpga35_33_sat_pb.cnf.cr.opb
IDLAUNCH: 3809
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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:        844544 kB
Buffers:         34072 kB
Cached:         113672 kB
SwapCached:       3828 kB
Active:          50140 kB
Inactive:       104288 kB
HighTotal:      131008 kB
HighFree:        15064 kB
LowTotal:       903652 kB
LowFree:        829480 kB
SwapTotal:     2097892 kB
SwapFree:      2094064 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            30168 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:59:36 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 3809 7 1200.24 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1256 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  67]---> BDD-cost:   63
c ---[  66]---> BDD-cost:   63
c ---[  65]---> BDD-cost:   63
c ---[  64]---> BDD-cost:   63
c ---[  63]---> BDD-cost:   63
c ---[  62]---> BDD-cost:   63
c ---[  61]---> BDD-cost:   63
c ---[  60]---> BDD-cost:   63
c ---[  59]---> BDD-cost:   63
c ---[  58]---> BDD-cost:   63
c ---[  57]---> BDD-cost:   63
c ---[  56]---> BDD-cost:   63
c ---[  55]---> BDD-cost:   63
c ---[  54]---> BDD-cost:   63
c ---[  53]---> BDD-cost:   63
c ---[  52]---> BDD-cost:   63
c ---[  51]---> BDD-cost:   63
c ---[  50]---> BDD-cost:   63
c ---[  49]---> BDD-cost:   63
c ---[  48]---> BDD-cost:   63
c ---[  47]---> BDD-cost:   63
c ---[  46]---> BDD-cost:   63
c ---[  45]---> BDD-cost:   63
c ---[  44]---> BDD-cost:   63
c ---[  43]---> BDD-cost:   63
c ---[  42]---> BDD-cost:   63
c ---[  41]---> BDD-cost:   63
c ---[  40]---> BDD-cost:   63
c ---[  39]---> BDD-cost:   63
c ---[  38]---> BDD-cost:   63
c ---[  37]---> BDD-cost:   63
c ---[  36]---> BDD-cost:   63
c ---[  35]---> BDD-cost:   63
c ---[  34]---> BDD-cost:   63
c ---[  33]---> BDD-cost:   63
c ---[  32]---> BDD-cost:   31
c ---[  31]---> BDD-cost:   31
c ---[  30]---> BDD-cost:   31
c ---[  29]---> BDD-cost:   31
c ---[  28]---> BDD-cost:   31
c ---[  27]---> BDD-cost:   31
c ---[  26]---> BDD-cost:   31
c ---[  25]---> BDD-cost:   31
c ---[  24]---> BDD-cost:   31
c ---[  23]---> BDD-cost:   31
c ---[  22]---> BDD-cost:   31
c ---[  21]---> BDD-cost:   31
c ---[  20]---> BDD-cost:   31
c ---[  19]---> BDD-cost:   31
c ---[  18]---> BDD-cost:   31
c ---[  17]---> BDD-cost:   31
c ---[  16]---> BDD-cost:   33
c ---[  15]---> BDD-cost:   33
c ---[  14]---> BDD-cost:   33
c ---[  13]---> BDD-cost:   33
c ---[  12]---> BDD-cost:   33
c ---[  11]---> BDD-cost:   33
c ---[  10]---> BDD-cost:   33
c ---[   9]---> BDD-cost:   33
c ---[   8]---> BDD-cost:   33
c ---[   7]---> BDD-cost:   33
c ---[   6]---> BDD-cost:   33
c ---[   5]---> BDD-cost:   33
c ---[   4]---> BDD-cost:   33
c ---[   3]---> BDD-cost:   33
c ---[   2]---> BDD-cost:   33
c ---[   1]---> BDD-cost:   33
c ---[   0]---> BDD-cost:   33
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    9241    42349 |    2772       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/4927          
c   -- var.elim.:  2000/4927          
c   -- var.elim.:  3000/4927          
c   -- var.elim.:  4000/4927          
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.79 0.92 0.89 2/54 372
Raw data (stat): 372 (runsolver) R 371 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479975379 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.99971 s]
Raw data (loadavg): 0.82 0.93 0.90 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 3397 0 0 0 989 9 0 0 25 0 1 0 479975379 15552512 3353 4294967295 134512640 134672761 3221224528 3221223568 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3797 3353 603 41 0 3756 0
vsize: 15188
[startup+20.0007 s]
Raw data (loadavg): 0.85 0.93 0.90 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 4430 0 0 0 1986 12 0 0 25 0 1 0 479975379 19771392 4386 4294967295 134512640 134672761 3221224528 3221223360 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4827 4386 603 41 0 4786 0
vsize: 19308
[startup+30.0008 s]
Raw data (loadavg): 0.87 0.93 0.90 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 5388 0 0 0 2984 15 0 0 25 0 1 0 479975379 23719936 5344 4294967295 134512640 134672761 3221224528 3221223712 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5791 5344 603 41 0 5750 0
vsize: 23164
[startup+40.0008 s]
Raw data (loadavg): 0.89 0.93 0.90 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 6032 0 0 0 3982 17 0 0 25 0 1 0 479975379 26345472 5988 4294967295 134512640 134672761 3221224528 3221223712 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6432 5988 603 41 0 6391 0
vsize: 25728
[startup+50.0014 s]
Raw data (loadavg): 0.91 0.93 0.90 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 6444 0 0 0 4981 18 0 0 25 0 1 0 479975379 28053504 6400 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6849 6400 603 41 0 6808 0
vsize: 27396
[startup+60.0009 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 6452 0 0 0 5981 18 0 0 25 0 1 0 479975379 28053504 6408 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6849 6408 603 41 0 6808 0
vsize: 27396
[startup+70.0019 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 6452 0 0 0 6981 18 0 0 25 0 1 0 479975379 28053504 6408 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6849 6408 603 41 0 6808 0
vsize: 27396
[startup+80.0025 s]
Raw data (loadavg): 0.94 0.94 0.90 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 6528 0 0 0 7982 18 0 0 25 0 1 0 479975379 28385280 6484 4294967295 134512640 134672761 3221224528 3221223712 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6930 6484 603 41 0 6889 0
vsize: 27720
[startup+90.002 s]
Raw data (loadavg): 0.95 0.94 0.90 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 6822 0 0 0 8981 18 0 0 25 0 1 0 479975379 29581312 6778 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7222 6778 603 41 0 7181 0
vsize: 28888
[startup+100.002 s]
Raw data (loadavg): 0.96 0.94 0.90 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 6925 0 0 0 9981 19 0 0 25 0 1 0 479975379 29978624 6881 4294967295 134512640 134672761 3221224528 3221223712 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7319 6881 603 41 0 7278 0
vsize: 29276
[startup+110.002 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7115 0 0 0 10981 19 0 0 25 0 1 0 479975379 30765056 7071 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7511 7071 603 41 0 7470 0
vsize: 30044
[startup+120.002 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7115 0 0 0 11981 19 0 0 25 0 1 0 479975379 30765056 7071 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7511 7071 603 41 0 7470 0
vsize: 30044
[startup+130.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7115 0 0 0 12981 19 0 0 25 0 1 0 479975379 30765056 7071 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7511 7071 603 41 0 7470 0
vsize: 30044
[startup+140.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7115 0 0 0 13981 19 0 0 25 0 1 0 479975379 30765056 7071 4294967295 134512640 134672761 3221224528 3221223712 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7511 7071 603 41 0 7470 0
vsize: 30044
[startup+150.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7115 0 0 0 14982 19 0 0 25 0 1 0 479975379 30765056 7071 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7511 7071 603 41 0 7470 0
vsize: 30044
[startup+160.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7127 0 0 0 15982 19 0 0 25 0 1 0 479975379 30838784 7083 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7529 7083 603 41 0 7488 0
vsize: 30116
[startup+170.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7127 0 0 0 16982 19 0 0 25 0 1 0 479975379 30838784 7083 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7529 7083 603 41 0 7488 0
vsize: 30116
[startup+180.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7127 0 0 0 17982 19 0 0 25 0 1 0 479975379 30838784 7083 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7529 7083 603 41 0 7488 0
vsize: 30116
[startup+190.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7132 0 0 0 18982 19 0 0 25 0 1 0 479975379 30838784 7088 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7529 7088 603 41 0 7488 0
vsize: 30116
[startup+200.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7132 0 0 0 19982 19 0 0 25 0 1 0 479975379 30838784 7088 4294967295 134512640 134672761 3221224528 3221223712 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7529 7088 603 41 0 7488 0
vsize: 30116
[startup+210.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7132 0 0 0 20983 19 0 0 25 0 1 0 479975379 30838784 7088 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7529 7088 603 41 0 7488 0
vsize: 30116
[startup+220.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7537 0 0 0 21982 20 0 0 25 0 1 0 479975379 32522240 7493 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7940 7493 603 41 0 7899 0
vsize: 31760
[startup+230.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7561 0 0 0 22982 21 0 0 25 0 1 0 479975379 32751616 7517 4294967295 134512640 134672761 3221224528 3221223304 1075351236 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7996 7517 603 41 0 7955 0
vsize: 31984
[startup+240.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7580 0 0 0 23982 21 0 0 25 0 1 0 479975379 32751616 7536 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7996 7536 603 41 0 7955 0
vsize: 31984
[startup+250.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7590 0 0 0 24982 21 0 0 25 0 1 0 479975379 32784384 7545 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8004 7545 603 41 0 7963 0
vsize: 32016
[startup+260.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7590 0 0 0 25982 21 0 0 25 0 1 0 479975379 32784384 7545 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8004 7545 603 41 0 7963 0
vsize: 32016
[startup+270.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7590 0 0 0 26982 21 0 0 25 0 1 0 479975379 32784384 7545 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8004 7545 603 41 0 7963 0
vsize: 32016
[startup+280.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7598 0 0 0 27982 21 0 0 25 0 1 0 479975379 32817152 7553 4294967295 134512640 134672761 3221224528 3221223548 134565024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8012 7553 603 41 0 7971 0
vsize: 32048
[startup+290.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7598 0 0 0 28983 21 0 0 25 0 1 0 479975379 32817152 7553 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8012 7553 603 41 0 7971 0
vsize: 32048
[startup+300.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7598 0 0 0 29983 21 0 0 25 0 1 0 479975379 32817152 7553 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8012 7553 603 41 0 7971 0
vsize: 32048
[startup+310.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7598 0 0 0 30983 21 0 0 25 0 1 0 479975379 32817152 7553 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8012 7553 603 41 0 7971 0
vsize: 32048
[startup+320.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7598 0 0 0 31983 21 0 0 25 0 1 0 479975379 32817152 7553 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8012 7553 603 41 0 7971 0
vsize: 32048
[startup+330.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7598 0 0 0 32983 21 0 0 25 0 1 0 479975379 32817152 7553 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8012 7553 603 41 0 7971 0
vsize: 32048
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7598 0 0 0 33984 21 0 0 25 0 1 0 479975379 32817152 7553 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8012 7553 603 41 0 7971 0
vsize: 32048
[startup+350.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7598 0 0 0 34984 21 0 0 25 0 1 0 479975379 32817152 7553 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8012 7553 603 41 0 7971 0
vsize: 32048
[startup+360.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7598 0 0 0 35984 21 0 0 25 0 1 0 479975379 32817152 7553 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8012 7553 603 41 0 7971 0
vsize: 32048
[startup+370.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7598 0 0 0 36984 21 0 0 25 0 1 0 479975379 32817152 7553 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8012 7553 603 41 0 7971 0
vsize: 32048
[startup+380.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7598 0 0 0 37984 21 0 0 25 0 1 0 479975379 32817152 7553 4294967295 134512640 134672761 3221224528 3221223568 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8012 7553 603 41 0 7971 0
vsize: 32048
[startup+390.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7598 0 0 0 38985 21 0 0 25 0 1 0 479975379 32817152 7553 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8012 7553 603 41 0 7971 0
vsize: 32048
[startup+400.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7598 0 0 0 39985 21 0 0 25 0 1 0 479975379 32817152 7553 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8012 7553 603 41 0 7971 0
vsize: 32048
[startup+410.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 7599 0 0 0 40985 21 0 0 25 0 1 0 479975379 32817152 7554 4294967295 134512640 134672761 3221224528 3221223568 134612608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8012 7554 603 41 0 7971 0
vsize: 32048
[startup+420.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 8141 0 0 0 41984 22 0 0 25 0 1 0 479975379 35065856 8096 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8561 8096 603 41 0 8520 0
vsize: 34244
[startup+430.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 8955 0 0 0 42983 23 0 0 25 0 1 0 479975379 38375424 8909 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9369 8909 603 41 0 9328 0
vsize: 37476
[startup+440.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 8955 0 0 0 43983 23 0 0 25 0 1 0 479975379 38375424 8909 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9369 8909 603 41 0 9328 0
vsize: 37476
[startup+450.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 8957 0 0 0 44983 23 0 0 25 0 1 0 479975379 38375424 8911 4294967295 134512640 134672761 3221224528 3221223712 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9369 8911 603 41 0 9328 0
vsize: 37476
[startup+460.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 9278 0 0 0 45982 24 0 0 25 0 1 0 479975379 39698432 9232 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9692 9232 603 41 0 9651 0
vsize: 38768
[startup+470.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 9946 0 0 0 46981 26 0 0 25 0 1 0 479975379 42536960 9900 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10385 9900 603 41 0 10344 0
vsize: 41540
[startup+480.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10620 0 0 0 47980 27 0 0 25 0 1 0 479975379 45350912 10574 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11072 10574 603 41 0 11031 0
vsize: 44288
[startup+490.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10777 0 0 0 48980 27 0 0 25 0 1 0 479975379 45953024 10730 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11219 10730 603 41 0 11178 0
vsize: 44876
[startup+500.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10777 0 0 0 49980 27 0 0 25 0 1 0 479975379 45953024 10730 4294967295 134512640 134672761 3221224528 3221223712 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11219 10730 603 41 0 11178 0
vsize: 44876
[startup+510.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10777 0 0 0 50980 27 0 0 25 0 1 0 479975379 45953024 10730 4294967295 134512640 134672761 3221224528 3221223712 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11219 10730 603 41 0 11178 0
vsize: 44876
[startup+520.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10777 0 0 0 51980 27 0 0 25 0 1 0 479975379 45953024 10730 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11219 10730 603 41 0 11178 0
vsize: 44876
[startup+530.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10780 0 0 0 52980 27 0 0 25 0 1 0 479975379 45953024 10733 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11219 10733 603 41 0 11178 0
vsize: 44876
[startup+540.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10799 0 0 0 53981 27 0 0 25 0 1 0 479975379 46018560 10751 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11235 10751 603 41 0 11194 0
vsize: 44940
[startup+550.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10799 0 0 0 54981 27 0 0 25 0 1 0 479975379 46018560 10751 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11235 10751 603 41 0 11194 0
vsize: 44940
[startup+560.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10800 0 0 0 55981 27 0 0 25 0 1 0 479975379 46018560 10752 4294967295 134512640 134672761 3221224528 3221223712 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11235 10752 603 41 0 11194 0
vsize: 44940
[startup+570.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10801 0 0 0 56981 27 0 0 25 0 1 0 479975379 46018560 10753 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11235 10753 603 41 0 11194 0
vsize: 44940
[startup+580.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10801 0 0 0 57981 27 0 0 25 0 1 0 479975379 46018560 10753 4294967295 134512640 134672761 3221224528 3221223712 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11235 10753 603 41 0 11194 0
vsize: 44940
[startup+590.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10801 0 0 0 58981 27 0 0 25 0 1 0 479975379 46018560 10753 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11235 10753 603 41 0 11194 0
vsize: 44940
[startup+600.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10801 0 0 0 59982 27 0 0 25 0 1 0 479975379 46018560 10753 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11235 10753 603 41 0 11194 0
vsize: 44940
[startup+610.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10802 0 0 0 60982 27 0 0 25 0 1 0 479975379 46018560 10754 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11235 10754 603 41 0 11194 0
vsize: 44940
[startup+620.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10802 0 0 0 61982 27 0 0 25 0 1 0 479975379 46018560 10754 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11235 10754 603 41 0 11194 0
vsize: 44940
[startup+630.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10802 0 0 0 62982 27 0 0 25 0 1 0 479975379 46018560 10754 4294967295 134512640 134672761 3221224528 3221223568 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11235 10754 603 41 0 11194 0
vsize: 44940
[startup+640.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10802 0 0 0 63982 27 0 0 25 0 1 0 479975379 46018560 10754 4294967295 134512640 134672761 3221224528 3221223632 134604307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11235 10754 603 41 0 11194 0
vsize: 44940
[startup+650.005 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10859 0 0 0 64983 27 0 0 25 0 1 0 479975379 46280704 10811 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11299 10811 603 41 0 11258 0
vsize: 45196
[startup+660.005 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10893 0 0 0 65983 27 0 0 25 0 1 0 479975379 46387200 10845 4294967295 134512640 134672761 3221224528 3221223568 134612604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11325 10845 603 41 0 11284 0
vsize: 45300
[startup+670.006 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10893 0 0 0 66983 27 0 0 25 0 1 0 479975379 46387200 10845 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11325 10845 603 41 0 11284 0
vsize: 45300
[startup+680.006 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10893 0 0 0 67983 27 0 0 25 0 1 0 479975379 46387200 10845 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11325 10845 603 41 0 11284 0
vsize: 45300
[startup+690.005 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10922 0 0 0 68983 27 0 0 25 0 1 0 479975379 46510080 10874 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11355 10874 603 41 0 11314 0
vsize: 45420
[startup+700.006 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10922 0 0 0 69983 27 0 0 25 0 1 0 479975379 46510080 10874 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11355 10874 603 41 0 11314 0
vsize: 45420
[startup+710.006 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10922 0 0 0 70984 27 0 0 25 0 1 0 479975379 46510080 10874 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11355 10874 603 41 0 11314 0
vsize: 45420
[startup+720.006 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10922 0 0 0 71984 27 0 0 25 0 1 0 479975379 46510080 10874 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11355 10874 603 41 0 11314 0
vsize: 45420
[startup+730.006 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10922 0 0 0 72984 27 0 0 25 0 1 0 479975379 46510080 10874 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11355 10874 603 41 0 11314 0
vsize: 45420
[startup+740.006 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10922 0 0 0 73984 27 0 0 25 0 1 0 479975379 46510080 10874 4294967295 134512640 134672761 3221224528 3221223712 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11355 10874 603 41 0 11314 0
vsize: 45420
[startup+750.006 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10922 0 0 0 74984 27 0 0 25 0 1 0 479975379 46510080 10874 4294967295 134512640 134672761 3221224528 3221223568 134612694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11355 10874 603 41 0 11314 0
vsize: 45420
[startup+760.006 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10922 0 0 0 75985 27 0 0 25 0 1 0 479975379 46510080 10874 4294967295 134512640 134672761 3221224528 3221223584 134644269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11355 10874 603 41 0 11314 0
vsize: 45420
[startup+770.007 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10922 0 0 0 76985 27 0 0 25 0 1 0 479975379 46501888 10873 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11353 10873 603 41 0 11312 0
vsize: 45412
[startup+780.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10922 0 0 0 77985 27 0 0 25 0 1 0 479975379 46501888 10873 4294967295 134512640 134672761 3221224528 3221223712 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11353 10873 603 41 0 11312 0
vsize: 45412
[startup+790.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10922 0 0 0 78985 27 0 0 25 0 1 0 479975379 46501888 10873 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11353 10873 603 41 0 11312 0
vsize: 45412
[startup+800.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10927 0 0 0 79985 27 0 0 25 0 1 0 479975379 46501888 10878 4294967295 134512640 134672761 3221224528 3221223712 134615673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11353 10878 603 41 0 11312 0
vsize: 45412
[startup+810.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10927 0 0 0 80985 27 0 0 25 0 1 0 479975379 46501888 10878 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11353 10878 603 41 0 11312 0
vsize: 45412
[startup+820.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10927 0 0 0 81986 27 0 0 25 0 1 0 479975379 46501888 10878 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11353 10878 603 41 0 11312 0
vsize: 45412
[startup+830.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10927 0 0 0 82986 27 0 0 25 0 1 0 479975379 46501888 10878 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11353 10878 603 41 0 11312 0
vsize: 45412
[startup+840.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10927 0 0 0 83986 27 0 0 25 0 1 0 479975379 46473216 10877 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11346 10877 603 41 0 11305 0
vsize: 45384
[startup+850.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10927 0 0 0 84986 27 0 0 25 0 1 0 479975379 46473216 10877 4294967295 134512640 134672761 3221224528 3221223304 1075352052 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11346 10877 603 41 0 11305 0
vsize: 45384
[startup+860.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10927 0 0 0 85986 27 0 0 25 0 1 0 479975379 46473216 10877 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11346 10877 603 41 0 11305 0
vsize: 45384
[startup+870.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10927 0 0 0 86987 27 0 0 25 0 1 0 479975379 46473216 10877 4294967295 134512640 134672761 3221224528 3221223520 134565110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11346 10877 603 41 0 11305 0
vsize: 45384
[startup+880.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10928 0 0 0 87987 27 0 0 25 0 1 0 479975379 46473216 10878 4294967295 134512640 134672761 3221224528 3221223728 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11346 10878 603 41 0 11305 0
vsize: 45384
[startup+890.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10928 0 0 0 88987 27 0 0 25 0 1 0 479975379 46473216 10878 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11346 10878 603 41 0 11305 0
vsize: 45384
[startup+900.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10928 0 0 0 89987 27 0 0 25 0 1 0 479975379 46473216 10878 4294967295 134512640 134672761 3221224528 3221223712 134615794 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11346 10878 603 41 0 11305 0
vsize: 45384
[startup+910.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10928 0 0 0 90987 27 0 0 25 0 1 0 479975379 46473216 10878 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11346 10878 603 41 0 11305 0
vsize: 45384
[startup+920.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10928 0 0 0 91988 27 0 0 25 0 1 0 479975379 46473216 10878 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11346 10878 603 41 0 11305 0
vsize: 45384
[startup+930.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10929 0 0 0 92988 27 0 0 25 0 1 0 479975379 46473216 10879 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11346 10879 603 41 0 11305 0
vsize: 45384
[startup+940.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10929 0 0 0 93988 27 0 0 25 0 1 0 479975379 46473216 10879 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11346 10879 603 41 0 11305 0
vsize: 45384
[startup+950.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10929 0 0 0 94988 27 0 0 25 0 1 0 479975379 46473216 10879 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11346 10879 603 41 0 11305 0
vsize: 45384
[startup+960.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10929 0 0 0 95988 27 0 0 25 0 1 0 479975379 46473216 10879 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11346 10879 603 41 0 11305 0
vsize: 45384
[startup+970.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10929 0 0 0 96989 27 0 0 25 0 1 0 479975379 46473216 10879 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11346 10879 603 41 0 11305 0
vsize: 45384
[startup+980.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10929 0 0 0 97989 27 0 0 25 0 1 0 479975379 46473216 10879 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11346 10879 603 41 0 11305 0
vsize: 45384
[startup+990.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10929 0 0 0 98989 27 0 0 25 0 1 0 479975379 46473216 10879 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11346 10879 603 41 0 11305 0
vsize: 45384
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10929 0 0 0 99989 27 0 0 25 0 1 0 479975379 46473216 10879 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11346 10879 603 41 0 11305 0
vsize: 45384
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10929 0 0 0 100989 27 0 0 25 0 1 0 479975379 46469120 10878 4294967295 134512640 134672761 3221224528 3221223568 134612684 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11345 10878 603 41 0 11304 0
vsize: 45380
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10929 0 0 0 101989 27 0 0 25 0 1 0 479975379 46469120 10878 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11345 10878 603 41 0 11304 0
vsize: 45380
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10929 0 0 0 102990 28 0 0 25 0 1 0 479975379 46469120 10878 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11345 10878 603 41 0 11304 0
vsize: 45380
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10929 0 0 0 103990 28 0 0 25 0 1 0 479975379 46444544 10874 4294967295 134512640 134672761 3221224528 3221223712 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11339 10874 603 41 0 11298 0
vsize: 45356
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10929 0 0 0 104990 28 0 0 25 0 1 0 479975379 46444544 10874 4294967295 134512640 134672761 3221224528 3221223712 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11339 10874 603 41 0 11298 0
vsize: 45356
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10929 0 0 0 105990 28 0 0 25 0 1 0 479975379 46444544 10874 4294967295 134512640 134672761 3221224528 3221223712 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11339 10874 603 41 0 11298 0
vsize: 45356
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10929 0 0 0 106990 28 0 0 25 0 1 0 479975379 46444544 10874 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11339 10874 603 41 0 11298 0
vsize: 45356
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10929 0 0 0 107991 28 0 0 25 0 1 0 479975379 46444544 10874 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11339 10874 603 41 0 11298 0
vsize: 45356
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10929 0 0 0 108991 28 0 0 25 0 1 0 479975379 46440448 10873 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11338 10873 603 41 0 11297 0
vsize: 45352
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10929 0 0 0 109991 28 0 0 25 0 1 0 479975379 46440448 10873 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11338 10873 603 41 0 11297 0
vsize: 45352
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10929 0 0 0 110991 28 0 0 25 0 1 0 479975379 46440448 10873 4294967295 134512640 134672761 3221224528 3221223712 134615755 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11338 10873 603 41 0 11297 0
vsize: 45352
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10929 0 0 0 111991 28 0 0 25 0 1 0 479975379 46440448 10873 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11338 10873 603 41 0 11297 0
vsize: 45352
[startup+1130.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10929 0 0 0 112992 28 0 0 25 0 1 0 479975379 46440448 10873 4294967295 134512640 134672761 3221224528 3221223568 134603536 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11338 10873 603 41 0 11297 0
vsize: 45352
[startup+1140.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10929 0 0 0 113992 28 0 0 25 0 1 0 479975379 46440448 10873 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11338 10873 603 41 0 11297 0
vsize: 45352
[startup+1150.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10929 0 0 0 114992 28 0 0 25 0 1 0 479975379 46440448 10873 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11338 10873 603 41 0 11297 0
vsize: 45352
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10929 0 0 0 115992 28 0 0 25 0 1 0 479975379 46440448 10873 4294967295 134512640 134672761 3221224528 3221223568 134614223 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11338 10873 603 41 0 11297 0
vsize: 45352
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10929 0 0 0 116992 28 0 0 25 0 1 0 479975379 46436352 10872 4294967295 134512640 134672761 3221224528 3221223584 134644266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11337 10872 603 41 0 11296 0
vsize: 45348
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10929 0 0 0 117992 28 0 0 25 0 1 0 479975379 46436352 10872 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11337 10872 603 41 0 11296 0
vsize: 45348
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10929 0 0 0 118993 28 0 0 25 0 1 0 479975379 46436352 10872 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11337 10872 603 41 0 11296 0
vsize: 45348
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 372
Raw data (stat): 372 (minisat+) R 371 28546 28545 0 -1 0 10929 0 0 0 119993 28 0 0 25 0 1 0 479975379 46436352 10872 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11337 10872 603 41 0 11296 0
vsize: 45348
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 372
Raw data (stat): 372 (minisat+) Z 371 28546 28545 0 -1 12 10929 0 0 0 119993 30 0 0 25 0 1 0 479975379 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.24
CPU user time (s): 1199.93
CPU system time (s): 0.301954
CPU usage (%): 100.017
Max. virtual memory (Kb): 45420
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####