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-chnl30_35_pb.cnf.cr.opb
MD5SUM	b1c5adb5438ceaf1c654cfedb79b695e
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	36
Number of bits of the biggest sum of numbers	6
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.06099
Number of variables	2100
Total number of constraints	130
Number of constraints which are clauses	70
Number of constraints which are cardinality constraints (but not clauses)	60
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	30
Maximum length of a constraint	35
Trace number 5331

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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:        915524 kB
Buffers:         34848 kB
Cached:          64960 kB
SwapCached:         16 kB
Active:          60260 kB
Inactive:        42416 kB
HighTotal:      131008 kB
HighFree:        62132 kB
LowTotal:       903652 kB
LowFree:        853392 kB
SwapTotal:     2097136 kB
SwapFree:      2097120 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            10868 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:51:02 (client local time) WITH STATUS 0 IN 1200.23 SECONDS
stats: 3772 7 1200.23 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 130 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ......................................................................
c ---[  59]---> BDD-cost:   67
c ---[  58]---> BDD-cost:   67
c ---[  57]---> BDD-cost:   67
c ---[  56]---> BDD-cost:   67
c ---[  55]---> BDD-cost:   67
c ---[  54]---> BDD-cost:   67
c ---[  53]---> BDD-cost:   67
c ---[  52]---> BDD-cost:   67
c ---[  51]---> BDD-cost:   67
c ---[  50]---> BDD-cost:   67
c ---[  49]---> BDD-cost:   67
c ---[  48]---> BDD-cost:   67
c ---[  47]---> BDD-cost:   67
c ---[  46]---> BDD-cost:   67
c ---[  45]---> BDD-cost:   67
c ---[  44]---> BDD-cost:   67
c ---[  43]---> BDD-cost:   67
c ---[  42]---> BDD-cost:   67
c ---[  41]---> BDD-cost:   67
c ---[  40]---> BDD-cost:   67
c ---[  39]---> BDD-cost:   67
c ---[  38]---> BDD-cost:   67
c ---[  37]---> BDD-cost:   67
c ---[  36]---> BDD-cost:   67
c ---[  35]---> BDD-cost:   67
c ---[  34]---> BDD-cost:   67
c ---[  33]---> BDD-cost:   67
c ---[  32]---> BDD-cost:   67
c ---[  31]---> BDD-cost:   67
c ---[  30]---> BDD-cost:   67
c ---[  29]---> BDD-cost:   67
c ---[  28]---> BDD-cost:   67
c ---[  27]---> BDD-cost:   67
c ---[  26]---> BDD-cost:   67
c ---[  25]---> BDD-cost:   67
c ---[  24]---> BDD-cost:   67
c ---[  23]---> BDD-cost:   67
c ---[  22]---> BDD-cost:   67
c ---[  21]---> BDD-cost:   67
c ---[  20]---> BDD-cost:   67
c ---[  19]---> BDD-cost:   67
c ---[  18]---> BDD-cost:   67
c ---[  17]---> BDD-cost:   67
c ---[  16]---> BDD-cost:   67
c ---[  15]---> BDD-cost:   67
c ---[  14]---> BDD-cost:   67
c ---[  13]---> BDD-cost:   67
c ---[  12]---> BDD-cost:   67
c ---[  11]---> BDD-cost:   67
c ---[  10]---> BDD-cost:   67
c ---[   9]---> BDD-cost:   67
c ---[   8]---> BDD-cost:   67
c ---[   7]---> BDD-cost:   67
c ---[   6]---> BDD-cost:   67
c ---[   5]---> BDD-cost:   67
c ---[   4]---> BDD-cost:   67
c ---[   3]---> BDD-cost:   67
c ---[   2]---> BDD-cost:   67
c ---[   1]---> BDD-cost:   67
c ---[   0]---> BDD-cost:   67
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   10030    28020 |    3008       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/6060          
c   -- var.elim.:  2000/6060          
c   -- var.elim.:  3000/6060          
c   -- var.elim.:  4000/6060          
c   -- var.elim.:  5000/6060          
c   -- var.elim.:  6000/6060          
c   -- var.elim.:  6060/6060          
c   -- var.elim.:  1000/2350          
c   -- var.elim.:  2000/2350          
c   -- var.elim.:  2350/2350          
c   -- var.elim.:  126/126          
c   -- subsuming                       
c   -- var.elim.:  1000/1368          
c   -- var.elim.:  1368/1368          
c   -- var.elim.:  582/582          
c   -- var.elim.:  194/194          
c   -- var.elim.:  192/192          
c   -- var.elim.:  88/88          
c   -- var.elim.:  80/80          
c   -- var.elim.:  82/82          
c   -- var.elim.:  84/84          
c   -- var.elim.:  86/86          
c   -- var.elim.:  88/88          
c   -- var.elim.:  90/90          
c   -- var.elim.:  92/92          
c   -- var.elim.:  94/94          
c   -- var.elim.:  96/96          
c   -- var.elim.:  98/98          
c   -- var.elim.:  100/100          
c   -- var.elim.:  102/102          
c   -- var.elim.:  104/104          
c   -- var.elim.:  106/106          
c   -- var.elim.:  108/108          
c   -- var.elim.:  110/110          
c   -- var.elim.:  112/112          
c   -- var.elim.:  114/114          
c   -- var.elim.:  116/116          
c   -- var.elim.:  118/118          
c   -- var.elim.:  120/120          
c   -- var.elim.:  122/122          
c   -- var.elim.:  124/124          
c   -- v#### 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.84 0.94 0.90 2/54 29273
Raw data (stat): 29273 (runsolver) R 29272 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421703217 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 3121 0 0 0 990 8 0 0 25 0 1 0 421703217 14417920 3097 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3520 3097 603 41 0 3479 0
vsize: 14080
[startup+20.0012 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 4105 0 0 0 1988 11 0 0 25 0 1 0 421703217 18460672 4081 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4507 4081 603 41 0 4466 0
vsize: 18028
[startup+30.0014 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 4671 0 0 0 2985 13 0 0 25 0 1 0 421703217 20848640 4647 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5090 4647 603 41 0 5049 0
vsize: 20360
[startup+40.0009 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 4955 0 0 0 3985 14 0 0 25 0 1 0 421703217 21979136 4931 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5366 4931 603 41 0 5325 0
vsize: 21464
[startup+50.0017 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 4955 0 0 0 4985 14 0 0 25 0 1 0 421703217 21979136 4931 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5366 4931 603 41 0 5325 0
vsize: 21464
[startup+60.0019 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 5187 0 0 0 5984 15 0 0 25 0 1 0 421703217 22904832 5163 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5592 5163 603 41 0 5551 0
vsize: 22368
[startup+70.0024 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 5563 0 0 0 6984 15 0 0 25 0 1 0 421703217 24481792 5539 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5977 5539 603 41 0 5936 0
vsize: 23908
[startup+80.0022 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 5563 0 0 0 7984 15 0 0 25 0 1 0 421703217 24481792 5539 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5977 5539 603 41 0 5936 0
vsize: 23908
[startup+90.0024 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 5792 0 0 0 8983 16 0 0 25 0 1 0 421703217 25403392 5768 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6202 5768 603 41 0 6161 0
vsize: 24808
[startup+100.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 5795 0 0 0 9983 16 0 0 25 0 1 0 421703217 25403392 5771 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6202 5771 603 41 0 6161 0
vsize: 24808
[startup+110.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 5795 0 0 0 10984 16 0 0 25 0 1 0 421703217 25403392 5771 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6202 5771 603 41 0 6161 0
vsize: 24808
[startup+120.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 5795 0 0 0 11984 16 0 0 25 0 1 0 421703217 25403392 5771 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6202 5771 603 41 0 6161 0
vsize: 24808
[startup+130.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 5795 0 0 0 12984 16 0 0 25 0 1 0 421703217 25403392 5771 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6202 5771 603 41 0 6161 0
vsize: 24808
[startup+140.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 5795 0 0 0 13984 16 0 0 25 0 1 0 421703217 25403392 5771 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6202 5771 603 41 0 6161 0
vsize: 24808
[startup+150.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 5795 0 0 0 14984 16 0 0 25 0 1 0 421703217 25403392 5771 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6202 5771 603 41 0 6161 0
vsize: 24808
[startup+160.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 5795 0 0 0 15985 16 0 0 25 0 1 0 421703217 25403392 5771 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6202 5771 603 41 0 6161 0
vsize: 24808
[startup+170.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 5974 0 0 0 16984 17 0 0 25 0 1 0 421703217 26148864 5950 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6384 5950 603 41 0 6343 0
vsize: 25536
[startup+180.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 6010 0 0 0 17984 17 0 0 25 0 1 0 421703217 26296320 5986 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6420 5986 603 41 0 6379 0
vsize: 25680
[startup+190.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 6045 0 0 0 18984 17 0 0 25 0 1 0 421703217 26476544 6020 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6464 6020 603 41 0 6423 0
vsize: 25856
[startup+200.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 6045 0 0 0 19984 17 0 0 25 0 1 0 421703217 26476544 6020 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6464 6020 603 41 0 6423 0
vsize: 25856
[startup+210.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 6065 0 0 0 20984 17 0 0 25 0 1 0 421703217 26669056 6040 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6511 6040 603 41 0 6470 0
vsize: 26044
[startup+220.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 6085 0 0 0 21985 17 0 0 25 0 1 0 421703217 26669056 6060 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6511 6060 603 41 0 6470 0
vsize: 26044
[startup+230.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 6087 0 0 0 22985 17 0 0 25 0 1 0 421703217 26669056 6062 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6511 6062 603 41 0 6470 0
vsize: 26044
[startup+240.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 6105 0 0 0 23985 17 0 0 25 0 1 0 421703217 26734592 6079 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6527 6079 603 41 0 6486 0
vsize: 26108
[startup+250.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 6119 0 0 0 24985 17 0 0 25 0 1 0 421703217 26734592 6093 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6527 6093 603 41 0 6486 0
vsize: 26108
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 7071 0 0 0 25982 21 0 0 25 0 1 0 421703217 30703616 7045 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7496 7045 603 41 0 7455 0
vsize: 29984
[startup+270.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 7248 0 0 0 26981 21 0 0 25 0 1 0 421703217 31416320 7221 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7670 7221 603 41 0 7629 0
vsize: 30680
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 8115 0 0 0 27980 23 0 0 25 0 1 0 421703217 34988032 8088 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8542 8088 603 41 0 8501 0
vsize: 34168
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 9002 0 0 0 28978 25 0 0 25 0 1 0 421703217 38576128 8975 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9418 8975 603 41 0 9377 0
vsize: 37672
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 9063 0 0 0 29978 25 0 0 25 0 1 0 421703217 38866944 9035 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9489 9035 603 41 0 9448 0
vsize: 37956
[startup+310.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 9063 0 0 0 30978 25 0 0 25 0 1 0 421703217 38866944 9035 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9489 9035 603 41 0 9448 0
vsize: 37956
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 9076 0 0 0 31978 25 0 0 25 0 1 0 421703217 38998016 9048 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9521 9048 603 41 0 9480 0
vsize: 38084
[startup+330.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 9678 0 0 0 32976 27 0 0 25 0 1 0 421703217 41369600 9650 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10100 9650 603 41 0 10059 0
vsize: 40400
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 10130 0 0 0 33975 28 0 0 25 0 1 0 421703217 43225088 10102 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10553 10102 603 41 0 10512 0
vsize: 42212
[startup+350.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 10808 0 0 0 34974 29 0 0 25 0 1 0 421703217 46051328 10779 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11243 10779 603 41 0 11202 0
vsize: 44972
[startup+360.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 10808 0 0 0 35974 29 0 0 25 0 1 0 421703217 46051328 10779 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11243 10779 603 41 0 11202 0
vsize: 44972
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 10809 0 0 0 36975 29 0 0 25 0 1 0 421703217 46051328 10780 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11243 10780 603 41 0 11202 0
vsize: 44972
[startup+380.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11188 0 0 0 37974 30 0 0 25 0 1 0 421703217 47595520 11159 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11620 11159 603 41 0 11579 0
vsize: 46480
[startup+390.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11188 0 0 0 38974 30 0 0 25 0 1 0 421703217 47595520 11159 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11620 11159 603 41 0 11579 0
vsize: 46480
[startup+400.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11188 0 0 0 39974 30 0 0 25 0 1 0 421703217 47595520 11159 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11620 11159 603 41 0 11579 0
vsize: 46480
[startup+410.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11188 0 0 0 40974 30 0 0 25 0 1 0 421703217 47595520 11159 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11620 11159 603 41 0 11579 0
vsize: 46480
[startup+420.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11188 0 0 0 41975 30 0 0 25 0 1 0 421703217 47595520 11159 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11620 11159 603 41 0 11579 0
vsize: 46480
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11188 0 0 0 42975 30 0 0 25 0 1 0 421703217 47595520 11159 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11620 11159 603 41 0 11579 0
vsize: 46480
[startup+440.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11188 0 0 0 43975 30 0 0 25 0 1 0 421703217 47595520 11159 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11620 11159 603 41 0 11579 0
vsize: 46480
[startup+450.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11189 0 0 0 44975 30 0 0 25 0 1 0 421703217 47595520 11160 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11620 11160 603 41 0 11579 0
vsize: 46480
[startup+460.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11189 0 0 0 45975 30 0 0 25 0 1 0 421703217 47595520 11160 4294967295 134512640 134672761 3221224544 3221223584 134612892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11620 11160 603 41 0 11579 0
vsize: 46480
[startup+470.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11189 0 0 0 46976 30 0 0 25 0 1 0 421703217 47595520 11160 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11620 11160 603 41 0 11579 0
vsize: 46480
[startup+480.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11189 0 0 0 47976 30 0 0 25 0 1 0 421703217 47595520 11160 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11620 11160 603 41 0 11579 0
vsize: 46480
[startup+490.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11189 0 0 0 48976 30 0 0 25 0 1 0 421703217 47591424 11159 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11619 11159 603 41 0 11578 0
vsize: 46476
[startup+500.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11189 0 0 0 49976 30 0 0 25 0 1 0 421703217 47591424 11159 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11619 11159 603 41 0 11578 0
vsize: 46476
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11189 0 0 0 50976 30 0 0 25 0 1 0 421703217 47591424 11159 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11619 11159 603 41 0 11578 0
vsize: 46476
[startup+520.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11189 0 0 0 51976 30 0 0 25 0 1 0 421703217 47591424 11159 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11619 11159 603 41 0 11578 0
vsize: 46476
[startup+530.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11189 0 0 0 52977 30 0 0 25 0 1 0 421703217 47591424 11159 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11619 11159 603 41 0 11578 0
vsize: 46476
[startup+540.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11189 0 0 0 53977 30 0 0 25 0 1 0 421703217 47591424 11159 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11619 11159 603 41 0 11578 0
vsize: 46476
[startup+550.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11189 0 0 0 54977 30 0 0 25 0 1 0 421703217 47591424 11159 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11619 11159 603 41 0 11578 0
vsize: 46476
[startup+560.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 55977 30 0 0 25 0 1 0 421703217 47587328 11160 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11618 11160 603 41 0 11577 0
vsize: 46472
[startup+570.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 56977 30 0 0 25 0 1 0 421703217 47587328 11160 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11618 11160 603 41 0 11577 0
vsize: 46472
[startup+580.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 57978 30 0 0 25 0 1 0 421703217 47587328 11160 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11618 11160 603 41 0 11577 0
vsize: 46472
[startup+590.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 58978 30 0 0 25 0 1 0 421703217 47583232 11160 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11617 11160 603 41 0 11576 0
vsize: 46468
[startup+600.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 59978 30 0 0 25 0 1 0 421703217 47583232 11160 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11617 11160 603 41 0 11576 0
vsize: 46468
[startup+610.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 60978 30 0 0 25 0 1 0 421703217 47583232 11160 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11617 11160 603 41 0 11576 0
vsize: 46468
[startup+620.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 61978 30 0 0 25 0 1 0 421703217 47583232 11160 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11617 11160 603 41 0 11576 0
vsize: 46468
[startup+630.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 62978 30 0 0 25 0 1 0 421703217 47583232 11160 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11617 11160 603 41 0 11576 0
vsize: 46468
[startup+640.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 63978 30 0 0 25 0 1 0 421703217 47583232 11160 4294967295 134512640 134672761 3221224544 3221223584 134612665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11617 11160 603 41 0 11576 0
vsize: 46468
[startup+650.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 64979 30 0 0 25 0 1 0 421703217 47583232 11160 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11617 11160 603 41 0 11576 0
vsize: 46468
[startup+660.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 65979 30 0 0 25 0 1 0 421703217 47583232 11160 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11617 11160 603 41 0 11576 0
vsize: 46468
[startup+670.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 66979 30 0 0 25 0 1 0 421703217 47583232 11160 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11617 11160 603 41 0 11576 0
vsize: 46468
[startup+680.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 67979 30 0 0 25 0 1 0 421703217 47583232 11160 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11617 11160 603 41 0 11576 0
vsize: 46468
[startup+690.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 68979 30 0 0 25 0 1 0 421703217 47583232 11160 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11617 11160 603 41 0 11576 0
vsize: 46468
[startup+700.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 69980 30 0 0 25 0 1 0 421703217 47583232 11160 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11617 11160 603 41 0 11576 0
vsize: 46468
[startup+710.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 70980 30 0 0 25 0 1 0 421703217 47583232 11160 4294967295 134512640 134672761 3221224544 3221222976 134645372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11617 11160 603 41 0 11576 0
vsize: 46468
[startup+720.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 71980 30 0 0 25 0 1 0 421703217 47583232 11160 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11617 11160 603 41 0 11576 0
vsize: 46468
[startup+730.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 72980 30 0 0 25 0 1 0 421703217 47583232 11160 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11617 11160 603 41 0 11576 0
vsize: 46468
[startup+740.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 73980 30 0 0 25 0 1 0 421703217 47583232 11160 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11617 11160 603 41 0 11576 0
vsize: 46468
[startup+750.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 74981 30 0 0 25 0 1 0 421703217 47583232 11160 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11617 11160 603 41 0 11576 0
vsize: 46468
[startup+760.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 75981 30 0 0 25 0 1 0 421703217 47583232 11160 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11617 11160 603 41 0 11576 0
vsize: 46468
[startup+770.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 76981 30 0 0 25 0 1 0 421703217 47583232 11160 4294967295 134512640 134672761 3221224544 3221223640 134616203 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11617 11160 603 41 0 11576 0
vsize: 46468
[startup+780.01 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 77981 30 0 0 25 0 1 0 421703217 47583232 11160 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11617 11160 603 41 0 11576 0
vsize: 46468
[startup+790.009 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 78981 30 0 0 25 0 1 0 421703217 47583232 11160 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11617 11160 603 41 0 11576 0
vsize: 46468
[startup+800.009 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 79981 30 0 0 25 0 1 0 421703217 47579136 11160 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11616 11160 603 41 0 11575 0
vsize: 46464
[startup+810.009 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 80981 30 0 0 25 0 1 0 421703217 47579136 11160 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11616 11160 603 41 0 11575 0
vsize: 46464
[startup+820.009 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 81982 30 0 0 25 0 1 0 421703217 47579136 11160 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11616 11160 603 41 0 11575 0
vsize: 46464
[startup+830.009 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 82982 30 0 0 25 0 1 0 421703217 47579136 11160 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11616 11160 603 41 0 11575 0
vsize: 46464
[startup+840.01 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 83982 30 0 0 25 0 1 0 421703217 47575040 11160 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11615 11160 603 41 0 11574 0
vsize: 46460
[startup+850.01 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 84982 30 0 0 25 0 1 0 421703217 47575040 11160 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11615 11160 603 41 0 11574 0
vsize: 46460
[startup+860.01 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 85982 30 0 0 25 0 1 0 421703217 47575040 11160 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11615 11160 603 41 0 11574 0
vsize: 46460
[startup+870.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 86982 30 0 0 25 0 1 0 421703217 47575040 11160 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11615 11160 603 41 0 11574 0
vsize: 46460
[startup+880.009 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11190 0 0 0 87983 30 0 0 25 0 1 0 421703217 47575040 11160 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11615 11160 603 41 0 11574 0
vsize: 46460
[startup+890.009 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11191 0 0 0 88983 30 0 0 25 0 1 0 421703217 47575040 11161 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11615 11161 603 41 0 11574 0
vsize: 46460
[startup+900.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11191 0 0 0 89983 30 0 0 25 0 1 0 421703217 47575040 11161 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11615 11161 603 41 0 11574 0
vsize: 46460
[startup+910.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11191 0 0 0 90983 30 0 0 25 0 1 0 421703217 47575040 11161 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11615 11161 603 41 0 11574 0
vsize: 46460
[startup+920.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11191 0 0 0 91983 30 0 0 25 0 1 0 421703217 47575040 11161 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11615 11161 603 41 0 11574 0
vsize: 46460
[startup+930.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11191 0 0 0 92983 30 0 0 25 0 1 0 421703217 47575040 11161 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11615 11161 603 41 0 11574 0
vsize: 46460
[startup+940.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11191 0 0 0 93984 30 0 0 25 0 1 0 421703217 47575040 11161 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11615 11161 603 41 0 11574 0
vsize: 46460
[startup+950.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11191 0 0 0 94984 30 0 0 25 0 1 0 421703217 47566848 11161 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11613 11161 603 41 0 11572 0
vsize: 46452
[startup+960.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11191 0 0 0 95984 30 0 0 25 0 1 0 421703217 47566848 11161 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11613 11161 603 41 0 11572 0
vsize: 46452
[startup+970.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11191 0 0 0 96984 30 0 0 25 0 1 0 421703217 47566848 11161 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11613 11161 603 41 0 11572 0
vsize: 46452
[startup+980.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11191 0 0 0 97984 30 0 0 25 0 1 0 421703217 47566848 11161 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11613 11161 603 41 0 11572 0
vsize: 46452
[startup+990.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11191 0 0 0 98984 30 0 0 25 0 1 0 421703217 47566848 11161 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11613 11161 603 41 0 11572 0
vsize: 46452
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11501 0 0 0 99984 31 0 0 25 0 1 0 421703217 48844800 11471 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11925 11471 603 41 0 11884 0
vsize: 47700
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11501 0 0 0 100984 31 0 0 25 0 1 0 421703217 48844800 11471 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11925 11471 603 41 0 11884 0
vsize: 47700
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11501 0 0 0 101984 31 0 0 25 0 1 0 421703217 48844800 11471 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11925 11471 603 41 0 11884 0
vsize: 47700
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11501 0 0 0 102984 31 0 0 25 0 1 0 421703217 48844800 11471 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11925 11471 603 41 0 11884 0
vsize: 47700
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11501 0 0 0 103984 31 0 0 25 0 1 0 421703217 48844800 11471 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11925 11471 603 41 0 11884 0
vsize: 47700
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11501 0 0 0 104985 31 0 0 25 0 1 0 421703217 48844800 11471 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11925 11471 603 41 0 11884 0
vsize: 47700
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11611 0 0 0 105985 32 0 0 25 0 1 0 421703217 49369088 11581 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12053 11581 603 41 0 12012 0
vsize: 48212
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 11952 0 0 0 106984 33 0 0 25 0 1 0 421703217 50724864 11922 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12384 11922 603 41 0 12343 0
vsize: 49536
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 12289 0 0 0 107983 34 0 0 25 0 1 0 421703217 52162560 12259 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12735 12259 603 41 0 12694 0
vsize: 50940
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 12714 0 0 0 108981 35 0 0 25 0 1 0 421703217 53862400 12684 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13150 12684 603 41 0 13109 0
vsize: 52600
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 12981 0 0 0 109980 37 0 0 25 0 1 0 421703217 54927360 12950 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13410 12950 603 41 0 13369 0
vsize: 53640
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 12981 0 0 0 110981 37 0 0 25 0 1 0 421703217 54927360 12950 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13410 12950 603 41 0 13369 0
vsize: 53640
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 12981 0 0 0 111981 37 0 0 25 0 1 0 421703217 54927360 12950 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13410 12950 603 41 0 13369 0
vsize: 53640
[startup+1130.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 12981 0 0 0 112981 37 0 0 25 0 1 0 421703217 54927360 12950 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13410 12950 603 41 0 13369 0
vsize: 53640
[startup+1140.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 12981 0 0 0 113981 37 0 0 25 0 1 0 421703217 54927360 12950 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13410 12950 603 41 0 13369 0
vsize: 53640
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 12981 0 0 0 114982 37 0 0 25 0 1 0 421703217 54927360 12950 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13410 12950 603 41 0 13369 0
vsize: 53640
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 12981 0 0 0 115982 37 0 0 25 0 1 0 421703217 54927360 12950 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13410 12950 603 41 0 13369 0
vsize: 53640
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 12981 0 0 0 116982 37 0 0 25 0 1 0 421703217 54927360 12950 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13410 12950 603 41 0 13369 0
vsize: 53640
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 12981 0 0 0 117982 37 0 0 25 0 1 0 421703217 54927360 12950 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13410 12950 603 41 0 13369 0
vsize: 53640
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 12981 0 0 0 118982 37 0 0 25 0 1 0 421703217 54927360 12950 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13410 12950 603 41 0 13369 0
vsize: 53640
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 29273
Raw data (stat): 29273 (minisat+) R 29272 25285 25284 0 -1 0 12981 0 0 0 119982 37 0 0 25 0 1 0 421703217 54927360 12950 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13410 12950 603 41 0 13369 0
vsize: 53640
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 29273
Raw data (stat): 29273 (minisat+) Z 29272 25285 25284 0 -1 12 12981 0 0 0 119983 39 0 0 25 0 1 0 421703217 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.04
CPU time (s): 1200.23
CPU user time (s): 1199.83
CPU system time (s): 0.394939
CPU usage (%): 100.015
Max. virtual memory (Kb): 53640
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####