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-chnl40_45_pb.cnf.cr.opb
MD5SUM	df5f31774bab40070962f7d0b16d093c
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	46
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.107983
Number of variables	3600
Total number of constraints	170
Number of constraints which are clauses	90
Number of constraints which are cardinality constraints (but not clauses)	80
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	40
Maximum length of a constraint	45
Trace number 5339

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-04-13 23:35:00 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3778 boxname=wulflinc1 idbench=18 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  df5f31774bab40070962f7d0b16d093c  /oldhome/oroussel/tmp/wulflinc1/normalized-chnl40_45_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc1/normalized-chnl40_45_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc1/normalized-chnl40_45_pb.cnf.cr.opb
IDLAUNCH: 3778
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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.053
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:        853052 kB
Buffers:         40208 kB
Cached:         117348 kB
SwapCached:          0 kB
Active:         106856 kB
Inactive:        53784 kB
HighTotal:      131008 kB
HighFree:        21000 kB
LowTotal:       903652 kB
LowFree:        832052 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7200 kB
Slab:            15256 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:55:02 (client local time) WITH STATUS 0 IN 1200.23 SECONDS
stats: 3778 7 1200.23 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 170 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..........................................................................................
c ---[  79]---> BDD-cost:   87
c ---[  78]---> BDD-cost:   87
c ---[  77]---> BDD-cost:   87
c ---[  76]---> BDD-cost:   87
c ---[  75]---> BDD-cost:   87
c ---[  74]---> BDD-cost:   87
c ---[  73]---> BDD-cost:   87
c ---[  72]---> BDD-cost:   87
c ---[  71]---> BDD-cost:   87
c ---[  70]---> BDD-cost:   87
c ---[  69]---> BDD-cost:   87
c ---[  68]---> BDD-cost:   87
c ---[  67]---> BDD-cost:   87
c ---[  66]---> BDD-cost:   87
c ---[  65]---> BDD-cost:   87
c ---[  64]---> BDD-cost:   87
c ---[  63]---> BDD-cost:   87
c ---[  62]---> BDD-cost:   87
c ---[  61]---> BDD-cost:   87
c ---[  60]---> BDD-cost:   87
c ---[  59]---> BDD-cost:   87
c ---[  58]---> BDD-cost:   87
c ---[  57]---> BDD-cost:   87
c ---[  56]---> BDD-cost:   87
c ---[  55]---> BDD-cost:   87
c ---[  54]---> BDD-cost:   87
c ---[  53]---> BDD-cost:   87
c ---[  52]---> BDD-cost:   87
c ---[  51]---> BDD-cost:   87
c ---[  50]---> BDD-cost:   87
c ---[  49]---> BDD-cost:   87
c ---[  48]---> BDD-cost:   87
c ---[  47]---> BDD-cost:   87
c ---[  46]---> BDD-cost:   87
c ---[  45]---> BDD-cost:   87
c ---[  44]---> BDD-cost:   87
c ---[  43]---> BDD-cost:   87
c ---[  42]---> BDD-cost:   87
c ---[  41]---> BDD-cost:   87
c ---[  40]---> BDD-cost:   87
c ---[  39]---> BDD-cost:   87
c ---[  38]---> BDD-cost:   87
c ---[  37]---> BDD-cost:   87
c ---[  36]---> BDD-cost:   87
c ---[  35]---> BDD-cost:   87
c ---[  34]---> BDD-cost:   87
c ---[  33]---> BDD-cost:   87
c ---[  32]---> BDD-cost:   87
c ---[  31]---> BDD-cost:   87
c ---[  30]---> BDD-cost:   87
c ---[  29]---> BDD-cost:   87
c ---[  28]---> BDD-cost:   87
c ---[  27]---> BDD-cost:   87
c ---[  26]---> BDD-cost:   87
c ---[  25]---> BDD-cost:   87
c ---[  24]---> BDD-cost:   87
c ---[  23]---> BDD-cost:   87
c ---[  22]---> BDD-cost:   87
c ---[  21]---> BDD-cost:   87
c ---[  20]---> BDD-cost:   87
c ---[  19]---> BDD-cost:   87
c ---[  18]---> BDD-cost:   87
c ---[  17]---> BDD-cost:   87
c ---[  16]---> BDD-cost:   87
c ---[  15]---> BDD-cost:   87
c ---[  14]---> BDD-cost:   87
c ---[  13]---> BDD-cost:   87
c ---[  12]---> BDD-cost:   87
c ---[  11]---> BDD-cost:   87
c ---[  10]---> BDD-cost:   87
c ---[   9]---> BDD-cost:   87
c ---[   8]---> BDD-cost:   87
c ---[   7]---> BDD-cost:   87
c ---[   6]---> BDD-cost:   87
c ---[   5]---> BDD-cost:   87
c ---[   4]---> BDD-cost:   87
c ---[   3]---> BDD-cost:   87
c ---[   2]---> BDD-cost:   87
c ---[   1]---> BDD-cost:   87
c ---[   0]---> BDD-cost:   87
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   17370    48560 |    5210       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10480          
c   -- var.elim.:  2000/10480          
c   -- var.elim.:  3000/10480          
c   -- var.elim.:  4000/10480          
c   -- var.elim.:  5000/10480          
c   -- var.elim.:  6000/10480          
c   -- var.elim.:  7000/10480          
c   -- var.elim.:  8000/10480          
c   -- var.elim.:  9000/10480          
c   -- var.elim.:  10000/10480          
c   -- var.elim.:  10480/10480          
c   -- var.elim.:  1000/3940          
c   -- var.elim.:  2000/3940          
c   -- var.elim.:  3000/3940          
c   -- var.elim.:  3940/3940          
c   -- var.elim.:  166/166          
c   -- subsuming                       
c   -- var.elim.:  1000/2228          
c   -- var.elim.:  2000/2228          
c   -- var.elim.:  2228/2228          
c   -- var.elim.:  782/782          
c   -- var.elim.:  254/254          
c   -- var.elim.:  252/2#### 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.91 0.95 0.90 2/56 16987
Raw data (stat): 16987 (runsolver) R 16986 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 364875482 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.93 0.95 0.90 2/56 16987
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 3822 0 0 0 989 9 0 0 25 0 1 0 364875482 17641472 3772 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4307 3772 603 41 0 4266 0
vsize: 17228
[startup+20.0006 s]
Raw data (loadavg): 0.94 0.96 0.91 2/56 16987
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 5837 0 0 0 1985 14 0 0 25 0 1 0 364875482 25886720 5787 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6320 5787 603 41 0 6279 0
vsize: 25280
[startup+30.001 s]
Raw data (loadavg): 0.95 0.96 0.91 2/56 16987
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 7820 0 0 0 2980 19 0 0 25 0 1 0 364875482 33923072 7770 4294967295 134512640 134672761 3221224544 3221223320 1075351236 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8282 7770 603 41 0 8241 0
vsize: 33128
[startup+40.0007 s]
Raw data (loadavg): 0.95 0.96 0.91 2/56 16987
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 9395 0 0 0 3975 24 0 0 25 0 1 0 364875482 40484864 9345 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9884 9345 603 41 0 9843 0
vsize: 39536
[startup+50.0005 s]
Raw data (loadavg): 0.96 0.96 0.91 2/56 16987
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 10454 0 0 0 4973 26 0 0 25 0 1 0 364875482 44838912 10404 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10947 10404 603 41 0 10906 0
vsize: 43788
[startup+60.0003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 16987
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 10542 0 0 0 5973 26 0 0 25 0 1 0 364875482 45137920 10491 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11020 10491 603 41 0 10979 0
vsize: 44080
[startup+70.0001 s]
Raw data (loadavg): 0.97 0.96 0.91 2/56 16987
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 10542 0 0 0 6973 27 0 0 25 0 1 0 364875482 45137920 10491 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11020 10491 603 41 0 10979 0
vsize: 44080
[startup+80.0013 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 10733 0 0 0 7972 27 0 0 25 0 1 0 364875482 45928448 10682 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11213 10682 603 41 0 11172 0
vsize: 44852
[startup+90.0017 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 11859 0 0 0 8968 31 0 0 25 0 1 0 364875482 50540544 11808 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12339 11808 603 41 0 12298 0
vsize: 49356
[startup+100.001 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 12989 0 0 0 9965 34 0 0 25 0 1 0 364875482 55164928 12938 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13468 12938 603 41 0 13427 0
vsize: 53872
[startup+110.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 12990 0 0 0 10965 34 0 0 25 0 1 0 364875482 55164928 12939 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13468 12939 603 41 0 13427 0
vsize: 53872
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 12990 0 0 0 11965 35 0 0 25 0 1 0 364875482 55164928 12939 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13468 12939 603 41 0 13427 0
vsize: 53872
[startup+130.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 12990 0 0 0 12965 35 0 0 25 0 1 0 364875482 55164928 12939 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13468 12939 603 41 0 13427 0
vsize: 53872
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 12990 0 0 0 13965 35 0 0 25 0 1 0 364875482 55164928 12939 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13468 12939 603 41 0 13427 0
vsize: 53872
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 12990 0 0 0 14965 35 0 0 25 0 1 0 364875482 55164928 12939 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13468 12939 603 41 0 13427 0
vsize: 53872
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 13810 0 0 0 15963 38 0 0 25 0 1 0 364875482 58654720 13759 4294967295 134512640 134672761 3221224544 3221221624 134645586 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14320 13759 603 41 0 14279 0
vsize: 57280
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 13810 0 0 0 16963 38 0 0 25 0 1 0 364875482 58523648 13758 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14288 13758 603 41 0 14247 0
vsize: 57152
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 13810 0 0 0 17962 38 0 0 25 0 1 0 364875482 58523648 13758 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14288 13758 603 41 0 14247 0
vsize: 57152
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 13810 0 0 0 18963 38 0 0 25 0 1 0 364875482 58523648 13758 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14288 13758 603 41 0 14247 0
vsize: 57152
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 13810 0 0 0 19962 38 0 0 25 0 1 0 364875482 58523648 13758 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14288 13758 603 41 0 14247 0
vsize: 57152
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 13810 0 0 0 20963 38 0 0 25 0 1 0 364875482 58523648 13758 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14288 13758 603 41 0 14247 0
vsize: 57152
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 14113 0 0 0 21962 39 0 0 25 0 1 0 364875482 59846656 14061 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14611 14061 603 41 0 14570 0
vsize: 58444
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 15705 0 0 0 22960 42 0 0 25 0 1 0 364875482 66285568 15653 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16183 15653 603 41 0 16142 0
vsize: 64732
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 16343 0 0 0 23958 43 0 0 25 0 1 0 364875482 68866048 16291 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16813 16291 603 41 0 16772 0
vsize: 67252
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 16343 0 0 0 24958 43 0 0 25 0 1 0 364875482 68866048 16291 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16813 16291 603 41 0 16772 0
vsize: 67252
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 16343 0 0 0 25959 43 0 0 25 0 1 0 364875482 68866048 16291 4294967295 134512640 134672761 3221224544 3221223584 134614254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16813 16291 603 41 0 16772 0
vsize: 67252
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 16343 0 0 0 26959 43 0 0 25 0 1 0 364875482 68866048 16291 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16813 16291 603 41 0 16772 0
vsize: 67252
[startup+280.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 16343 0 0 0 27959 43 0 0 25 0 1 0 364875482 68866048 16291 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16813 16291 603 41 0 16772 0
vsize: 67252
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 16343 0 0 0 28959 43 0 0 25 0 1 0 364875482 68866048 16291 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16813 16291 603 41 0 16772 0
vsize: 67252
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 17347 0 0 0 29957 46 0 0 25 0 1 0 364875482 73080832 17295 4294967295 134512640 134672761 3221224544 3221223356 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17842 17296 603 41 0 17801 0
vsize: 71368
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 17983 0 0 0 30956 47 0 0 25 0 1 0 364875482 75599872 17930 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18457 17930 603 41 0 18416 0
vsize: 73828
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 17983 0 0 0 31956 47 0 0 25 0 1 0 364875482 75599872 17930 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18457 17930 603 41 0 18416 0
vsize: 73828
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 17983 0 0 0 32956 47 0 0 25 0 1 0 364875482 75599872 17930 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18457 17930 603 41 0 18416 0
vsize: 73828
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 17983 0 0 0 33956 47 0 0 25 0 1 0 364875482 75599872 17930 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18457 17930 603 41 0 18416 0
vsize: 73828
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 17983 0 0 0 34956 47 0 0 25 0 1 0 364875482 75599872 17930 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18457 17930 603 41 0 18416 0
vsize: 73828
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 17983 0 0 0 35957 47 0 0 25 0 1 0 364875482 75599872 17930 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18457 17930 603 41 0 18416 0
vsize: 73828
[startup+370.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16989
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 17983 0 0 0 36957 47 0 0 25 0 1 0 364875482 75599872 17930 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18457 17930 603 41 0 18416 0
vsize: 73828
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 17983 0 0 0 37957 47 0 0 25 0 1 0 364875482 75599872 17930 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18457 17930 603 41 0 18416 0
vsize: 73828
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 18567 0 0 0 38955 48 0 0 25 0 1 0 364875482 78094336 18514 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19066 18514 603 41 0 19025 0
vsize: 76264
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 18963 0 0 0 39955 49 0 0 25 0 1 0 364875482 79679488 18910 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19453 18910 603 41 0 19412 0
vsize: 77812
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 19347 0 0 0 40954 50 0 0 25 0 1 0 364875482 81424384 19294 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19879 19294 603 41 0 19838 0
vsize: 79516
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 19777 0 0 0 41953 51 0 0 25 0 1 0 364875482 83144704 19724 4294967295 134512640 134672761 3221224544 3221223728 134616023 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20299 19724 603 41 0 20258 0
vsize: 81196
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20165 0 0 0 42953 52 0 0 25 0 1 0 364875482 84578304 20077 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20649 20077 603 41 0 20608 0
vsize: 82596
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20165 0 0 0 43953 52 0 0 25 0 1 0 364875482 84578304 20077 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20649 20077 603 41 0 20608 0
vsize: 82596
[startup+450.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20165 0 0 0 44953 52 0 0 25 0 1 0 364875482 84578304 20077 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20649 20077 603 41 0 20608 0
vsize: 82596
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20165 0 0 0 45953 52 0 0 25 0 1 0 364875482 84578304 20077 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20649 20077 603 41 0 20608 0
vsize: 82596
[startup+470.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20165 0 0 0 46953 52 0 0 25 0 1 0 364875482 84578304 20077 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20649 20077 603 41 0 20608 0
vsize: 82596
[startup+480.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20165 0 0 0 47953 52 0 0 25 0 1 0 364875482 84578304 20077 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20649 20077 603 41 0 20608 0
vsize: 82596
[startup+490.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20165 0 0 0 48954 52 0 0 25 0 1 0 364875482 84578304 20077 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20649 20077 603 41 0 20608 0
vsize: 82596
[startup+500.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20165 0 0 0 49954 52 0 0 25 0 1 0 364875482 84578304 20077 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20649 20077 603 41 0 20608 0
vsize: 82596
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20165 0 0 0 50954 52 0 0 25 0 1 0 364875482 84578304 20077 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20649 20077 603 41 0 20608 0
vsize: 82596
[startup+520.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20168 0 0 0 51954 52 0 0 25 0 1 0 364875482 84578304 20080 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20649 20080 603 41 0 20608 0
vsize: 82596
[startup+530.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20168 0 0 0 52954 52 0 0 25 0 1 0 364875482 84578304 20080 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20649 20080 603 41 0 20608 0
vsize: 82596
[startup+540.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20168 0 0 0 53954 52 0 0 25 0 1 0 364875482 84578304 20080 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20649 20080 603 41 0 20608 0
vsize: 82596
[startup+550.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20169 0 0 0 54955 52 0 0 25 0 1 0 364875482 84578304 20081 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20649 20081 603 41 0 20608 0
vsize: 82596
[startup+560.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20170 0 0 0 55955 52 0 0 25 0 1 0 364875482 84578304 20082 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20649 20082 603 41 0 20608 0
vsize: 82596
[startup+570.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20172 0 0 0 56955 52 0 0 25 0 1 0 364875482 84578304 20084 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20649 20084 603 41 0 20608 0
vsize: 82596
[startup+580.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20175 0 0 0 57955 52 0 0 25 0 1 0 364875482 84578304 20087 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20649 20087 603 41 0 20608 0
vsize: 82596
[startup+590.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20175 0 0 0 58955 52 0 0 25 0 1 0 364875482 84578304 20087 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20649 20087 603 41 0 20608 0
vsize: 82596
[startup+600.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20175 0 0 0 59955 52 0 0 25 0 1 0 364875482 84578304 20087 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20649 20087 603 41 0 20608 0
vsize: 82596
[startup+610.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20175 0 0 0 60956 52 0 0 25 0 1 0 364875482 84578304 20087 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20649 20087 603 41 0 20608 0
vsize: 82596
[startup+620.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20175 0 0 0 61956 52 0 0 25 0 1 0 364875482 84578304 20087 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20649 20087 603 41 0 20608 0
vsize: 82596
[startup+630.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20175 0 0 0 62956 52 0 0 25 0 1 0 364875482 84566016 20084 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20646 20084 603 41 0 20605 0
vsize: 82584
[startup+640.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20175 0 0 0 63956 52 0 0 25 0 1 0 364875482 84566016 20084 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20646 20084 603 41 0 20605 0
vsize: 82584
[startup+650.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20175 0 0 0 64956 52 0 0 25 0 1 0 364875482 84566016 20084 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20646 20084 603 41 0 20605 0
vsize: 82584
[startup+660.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20175 0 0 0 65956 52 0 0 25 0 1 0 364875482 84566016 20084 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20646 20084 603 41 0 20605 0
vsize: 82584
[startup+670.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16991
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20175 0 0 0 66957 52 0 0 25 0 1 0 364875482 84566016 20084 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20646 20084 603 41 0 20605 0
vsize: 82584
[startup+680.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20175 0 0 0 67957 52 0 0 25 0 1 0 364875482 84566016 20084 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20646 20084 603 41 0 20605 0
vsize: 82584
[startup+690.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20175 0 0 0 68957 52 0 0 25 0 1 0 364875482 84566016 20084 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20646 20084 603 41 0 20605 0
vsize: 82584
[startup+700.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20175 0 0 0 69957 52 0 0 25 0 1 0 364875482 84566016 20084 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20646 20084 603 41 0 20605 0
vsize: 82584
[startup+710.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20175 0 0 0 70957 52 0 0 25 0 1 0 364875482 84566016 20084 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20646 20084 603 41 0 20605 0
vsize: 82584
[startup+720.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20175 0 0 0 71957 52 0 0 25 0 1 0 364875482 84566016 20084 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20646 20084 603 41 0 20605 0
vsize: 82584
[startup+730.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20175 0 0 0 72958 52 0 0 25 0 1 0 364875482 84566016 20084 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20646 20084 603 41 0 20605 0
vsize: 82584
[startup+740.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20175 0 0 0 73958 52 0 0 25 0 1 0 364875482 84566016 20084 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20646 20084 603 41 0 20605 0
vsize: 82584
[startup+750.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20175 0 0 0 74958 52 0 0 25 0 1 0 364875482 84566016 20084 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20646 20084 603 41 0 20605 0
vsize: 82584
[startup+760.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20176 0 0 0 75958 52 0 0 25 0 1 0 364875482 84566016 20085 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20646 20085 603 41 0 20605 0
vsize: 82584
[startup+770.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20176 0 0 0 76958 52 0 0 25 0 1 0 364875482 84549632 20081 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20642 20081 603 41 0 20601 0
vsize: 82568
[startup+780.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20176 0 0 0 77958 52 0 0 25 0 1 0 364875482 84549632 20081 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20642 20081 603 41 0 20601 0
vsize: 82568
[startup+790.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20176 0 0 0 78959 52 0 0 25 0 1 0 364875482 84549632 20081 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20642 20081 603 41 0 20601 0
vsize: 82568
[startup+800.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20176 0 0 0 79959 52 0 0 25 0 1 0 364875482 84549632 20081 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20642 20081 603 41 0 20601 0
vsize: 82568
[startup+810.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20176 0 0 0 80959 52 0 0 25 0 1 0 364875482 84549632 20081 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20642 20081 603 41 0 20601 0
vsize: 82568
[startup+820.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20176 0 0 0 81959 52 0 0 25 0 1 0 364875482 84549632 20081 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20642 20081 603 41 0 20601 0
vsize: 82568
[startup+830.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20176 0 0 0 82959 52 0 0 25 0 1 0 364875482 84549632 20081 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20642 20081 603 41 0 20601 0
vsize: 82568
[startup+840.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20176 0 0 0 83959 52 0 0 25 0 1 0 364875482 84549632 20081 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20642 20081 603 41 0 20601 0
vsize: 82568
[startup+850.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20176 0 0 0 84960 52 0 0 25 0 1 0 364875482 84549632 20081 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20642 20081 603 41 0 20601 0
vsize: 82568
[startup+860.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20176 0 0 0 85960 52 0 0 25 0 1 0 364875482 84549632 20081 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20642 20081 603 41 0 20601 0
vsize: 82568
[startup+870.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20176 0 0 0 86960 52 0 0 25 0 1 0 364875482 84549632 20081 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20642 20081 603 41 0 20601 0
vsize: 82568
[startup+880.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20176 0 0 0 87960 52 0 0 25 0 1 0 364875482 84549632 20081 4294967295 134512640 134672761 3221224544 3221223728 134615785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20642 20081 603 41 0 20601 0
vsize: 82568
[startup+890.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20176 0 0 0 88960 52 0 0 25 0 1 0 364875482 84549632 20081 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20642 20081 603 41 0 20601 0
vsize: 82568
[startup+900.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20176 0 0 0 89960 52 0 0 25 0 1 0 364875482 84549632 20081 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20642 20081 603 41 0 20601 0
vsize: 82568
[startup+910.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20306 0 0 0 90960 52 0 0 25 0 1 0 364875482 85086208 20211 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20773 20211 603 41 0 20732 0
vsize: 83092
[startup+920.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20837 0 0 0 91959 54 0 0 25 0 1 0 364875482 87367680 20742 4294967295 134512640 134672761 3221224544 3221223640 134616373 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21330 20742 603 41 0 21289 0
vsize: 85320
[startup+930.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20837 0 0 0 92959 54 0 0 25 0 1 0 364875482 87236608 20737 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21298 20737 603 41 0 21257 0
vsize: 85192
[startup+940.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20837 0 0 0 93959 54 0 0 25 0 1 0 364875482 87236608 20737 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21298 20737 603 41 0 21257 0
vsize: 85192
[startup+950.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20837 0 0 0 94959 54 0 0 25 0 1 0 364875482 87236608 20737 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21298 20737 603 41 0 21257 0
vsize: 85192
[startup+960.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20837 0 0 0 95960 54 0 0 25 0 1 0 364875482 87236608 20737 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21298 20737 603 41 0 21257 0
vsize: 85192
[startup+970.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16993
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20837 0 0 0 96960 54 0 0 25 0 1 0 364875482 87236608 20737 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21298 20737 603 41 0 21257 0
vsize: 85192
[startup+980.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16995
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20837 0 0 0 97960 54 0 0 25 0 1 0 364875482 87236608 20737 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21298 20737 603 41 0 21257 0
vsize: 85192
[startup+990.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16995
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20837 0 0 0 98960 54 0 0 25 0 1 0 364875482 87236608 20737 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21298 20737 603 41 0 21257 0
vsize: 85192
[startup+1000 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16995
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20837 0 0 0 99960 54 0 0 25 0 1 0 364875482 87236608 20737 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21298 20737 603 41 0 21257 0
vsize: 85192
[startup+1010 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16995
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20837 0 0 0 100960 54 0 0 25 0 1 0 364875482 87236608 20737 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21298 20737 603 41 0 21257 0
vsize: 85192
[startup+1020 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16995
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20837 0 0 0 101960 54 0 0 25 0 1 0 364875482 87236608 20737 4294967295 134512640 134672761 3221224544 3221223584 134612827 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21298 20737 603 41 0 21257 0
vsize: 85192
[startup+1030 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16995
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20837 0 0 0 102961 54 0 0 25 0 1 0 364875482 87236608 20737 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21298 20737 603 41 0 21257 0
vsize: 85192
[startup+1040 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16995
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20837 0 0 0 103961 54 0 0 25 0 1 0 364875482 87236608 20737 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21298 20737 603 41 0 21257 0
vsize: 85192
[startup+1050 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16995
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20837 0 0 0 104961 54 0 0 25 0 1 0 364875482 87236608 20737 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21298 20737 603 41 0 21257 0
vsize: 85192
[startup+1060 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16995
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 20837 0 0 0 105961 54 0 0 25 0 1 0 364875482 87236608 20737 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21298 20737 603 41 0 21257 0
vsize: 85192
[startup+1070 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16995
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 21107 0 0 0 106961 54 0 0 25 0 1 0 364875482 88440832 21007 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21592 21007 603 41 0 21551 0
vsize: 86368
[startup+1080 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16995
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 21504 0 0 0 107960 56 0 0 25 0 1 0 364875482 90017792 21404 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21977 21404 603 41 0 21936 0
vsize: 87908
[startup+1090 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16995
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 21879 0 0 0 108959 56 0 0 25 0 1 0 364875482 91615232 21779 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22367 21779 603 41 0 22326 0
vsize: 89468
[startup+1100 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16995
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 22170 0 0 0 109958 58 0 0 25 0 1 0 364875482 92803072 22070 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22657 22070 603 41 0 22616 0
vsize: 90628
[startup+1110 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16995
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 22459 0 0 0 110957 59 0 0 25 0 1 0 364875482 93986816 22359 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22946 22359 603 41 0 22905 0
vsize: 91784
[startup+1120 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16995
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 22763 0 0 0 111957 59 0 0 25 0 1 0 364875482 95236096 22663 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23251 22663 603 41 0 23210 0
vsize: 93004
[startup+1130 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16995
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 23099 0 0 0 112956 60 0 0 25 0 1 0 364875482 96681984 22999 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23604 22999 603 41 0 23563 0
vsize: 94416
[startup+1140 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16995
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 23455 0 0 0 113955 61 0 0 25 0 1 0 364875482 98123776 23355 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23956 23355 603 41 0 23915 0
vsize: 95824
[startup+1150 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16995
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 23844 0 0 0 114954 62 0 0 25 0 1 0 364875482 99704832 23744 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24342 23744 603 41 0 24301 0
vsize: 97368
[startup+1160 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16995
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 24274 0 0 0 115953 63 0 0 25 0 1 0 364875482 101543936 24174 4294967295 134512640 134672761 3221224544 3221223728 134615767 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24791 24174 603 41 0 24750 0
vsize: 99164
[startup+1170 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16995
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 24348 0 0 0 116953 63 0 0 25 0 1 0 364875482 101617664 24214 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24809 24214 603 41 0 24768 0
vsize: 99236
[startup+1180 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16995
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 24348 0 0 0 117953 63 0 0 25 0 1 0 364875482 101617664 24214 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24809 24214 603 41 0 24768 0
vsize: 99236
[startup+1190 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16995
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 24348 0 0 0 118954 63 0 0 25 0 1 0 364875482 101617664 24214 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24809 24214 603 41 0 24768 0
vsize: 99236
[startup+1200 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 16995
Raw data (stat): 16987 (minisat+) R 16986 12452 12451 0 -1 0 24348 0 0 0 119954 63 0 0 25 0 1 0 364875482 101617664 24214 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24809 24214 603 41 0 24768 0
vsize: 99236
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/56 16995
Raw data (stat): 16987 (minisat+) Z 16986 12452 12451 0 -1 12 24348 0 0 0 119954 68 0 0 25 0 1 0 364875482 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.05
CPU time (s): 1200.23
CPU user time (s): 1199.54
CPU system time (s): 0.685895
CPU usage (%): 100.015
Max. virtual memory (Kb): 99236
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####