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-fpga40_38_sat_pb.cnf.cr.opb
MD5SUM	69d239b72e8d1a72f9c55329043493e1
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	41
Number of bits of the biggest sum of numbers	6
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	15.9626
Number of variables	2280
Total number of constraints	1636
Number of constraints which are clauses	1558
Number of constraints which are cardinality constraints (but not clauses)	78
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	20
Maximum length of a constraint	40
Trace number 5401

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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:        853012 kB
Buffers:         33744 kB
Cached:         111132 kB
SwapCached:       3160 kB
Active:          50560 kB
Inactive:       100280 kB
HighTotal:      131008 kB
HighFree:        16520 kB
LowTotal:       903652 kB
LowFree:        836492 kB
SwapTotal:     2097892 kB
SwapFree:      2094732 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            25412 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 00:01:17 (client local time) WITH STATUS 0 IN 1200.19 SECONDS
stats: 3812 7 1200.19 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1636 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  77]---> BDD-cost:   73
c ---[  76]---> BDD-cost:   73
c ---[  75]---> BDD-cost:   73
c ---[  74]---> BDD-cost:   73
c ---[  73]---> BDD-cost:   73
c ---[  72]---> BDD-cost:   73
c ---[  71]---> BDD-cost:   73
c ---[  70]---> BDD-cost:   73
c ---[  69]---> BDD-cost:   73
c ---[  68]---> BDD-cost:   73
c ---[  67]---> BDD-cost:   73
c ---[  66]---> BDD-cost:   73
c ---[  65]---> BDD-cost:   73
c ---[  64]---> BDD-cost:   73
c ---[  63]---> BDD-cost:   73
c ---[  62]---> BDD-cost:   73
c ---[  61]---> BDD-cost:   73
c ---[  60]---> BDD-cost:   73
c ---[  59]---> BDD-cost:   73
c ---[  58]---> BDD-cost:   73
c ---[  57]---> BDD-cost:   73
c ---[  56]---> BDD-cost:   73
c ---[  55]---> BDD-cost:   73
c ---[  54]---> BDD-cost:   73
c ---[  53]---> BDD-cost:   73
c ---[  52]---> BDD-cost:   73
c ---[  51]---> BDD-cost:   73
c ---[  50]---> BDD-cost:   73
c ---[  49]---> BDD-cost:   73
c ---[  48]---> BDD-cost:   73
c ---[  47]---> BDD-cost:   73
c ---[  46]---> BDD-cost:   73
c ---[  45]---> BDD-cost:   73
c ---[  44]---> BDD-cost:   73
c ---[  43]---> BDD-cost:   73
c ---[  42]---> BDD-cost:   73
c ---[  41]---> BDD-cost:   73
c ---[  40]---> BDD-cost:   73
c ---[  39]---> BDD-cost:   73
c ---[  38]---> BDD-cost:   73
c ---[  37]---> BDD-cost:   37
c ---[  36]---> BDD-cost:   37
c ---[  35]---> BDD-cost:   37
c ---[  34]---> BDD-cost:   37
c ---[  33]---> BDD-cost:   37
c ---[  32]---> BDD-cost:   37
c ---[  31]---> BDD-cost:   37
c ---[  30]---> BDD-cost:   37
c ---[  29]---> BDD-cost:   37
c ---[  28]---> BDD-cost:   37
c ---[  27]---> BDD-cost:   37
c ---[  26]---> BDD-cost:   37
c ---[  25]---> BDD-cost:   37
c ---[  24]---> BDD-cost:   37
c ---[  23]---> BDD-cost:   37
c ---[  22]---> BDD-cost:   37
c ---[  21]---> BDD-cost:   37
c ---[  20]---> BDD-cost:   37
c ---[  19]---> BDD-cost:   37
c ---[  18]---> BDD-cost:   37
c ---[  17]---> BDD-cost:   37
c ---[  16]---> BDD-cost:   37
c ---[  15]---> BDD-cost:   37
c ---[  14]---> BDD-cost:   37
c ---[  13]---> BDD-cost:   37
c ---[  12]---> BDD-cost:   37
c ---[  11]---> BDD-cost:   37
c ---[  10]---> BDD-cost:   37
c ---[   9]---> BDD-cost:   37
c ---[   8]---> BDD-cost:   37
c ---[   7]---> BDD-cost:   37
c ---[   6]---> BDD-cost:   37
c ---[   5]---> BDD-cost:   37
c ---[   4]---> BDD-cost:   37
c ---[   3]---> BDD-cost:   37
c ---[   2]---> BDD-c#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.96 0.91 2/54 22391
Raw data (stat): 22391 (runsolver) R 22390 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479986822 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99953 s]
Raw data (loadavg): 0.87 0.96 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 3541 0 0 0 988 11 0 0 25 0 1 0 479986822 16052224 3486 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3919 3486 603 41 0 3878 0
vsize: 15676
[startup+20.0003 s]
Raw data (loadavg): 0.89 0.96 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 5623 0 0 0 1983 15 0 0 25 0 1 0 479986822 24506368 5568 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5983 5568 603 41 0 5942 0
vsize: 23932
[startup+30.0006 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 6437 0 0 0 2981 18 0 0 25 0 1 0 479986822 27918336 6382 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6816 6382 603 41 0 6775 0
vsize: 27264
[startup+40.001 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 7172 0 0 0 3979 20 0 0 25 0 1 0 479986822 30986240 7117 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7565 7117 603 41 0 7524 0
vsize: 30260
[startup+50.0018 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 7710 0 0 0 4978 21 0 0 25 0 1 0 479986822 33124352 7654 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8087 7654 603 41 0 8046 0
vsize: 32348
[startup+60.002 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 7710 0 0 0 5977 22 0 0 25 0 1 0 479986822 33124352 7654 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8087 7654 603 41 0 8046 0
vsize: 32348
[startup+70.0029 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 8003 0 0 0 6976 23 0 0 25 0 1 0 479986822 34316288 7947 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8378 7947 603 41 0 8337 0
vsize: 33512
[startup+80.0033 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 8396 0 0 0 7975 24 0 0 25 0 1 0 479986822 35917824 8339 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8339 603 41 0 8728 0
vsize: 35076
[startup+90.0045 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 8396 0 0 0 8975 25 0 0 25 0 1 0 479986822 35917824 8339 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8339 603 41 0 8728 0
vsize: 35076
[startup+100.005 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 8396 0 0 0 9974 25 0 0 25 0 1 0 479986822 35917824 8339 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8339 603 41 0 8728 0
vsize: 35076
[startup+110.006 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 8396 0 0 0 10974 26 0 0 25 0 1 0 479986822 35917824 8339 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8339 603 41 0 8728 0
vsize: 35076
[startup+120.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 8396 0 0 0 11974 26 0 0 25 0 1 0 479986822 35917824 8339 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8769 8339 603 41 0 8728 0
vsize: 35076
[startup+130.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 8421 0 0 0 12974 26 0 0 25 0 1 0 479986822 36098048 8364 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8813 8364 603 41 0 8772 0
vsize: 35252
[startup+140.006 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 8421 0 0 0 13974 26 0 0 25 0 1 0 479986822 36098048 8364 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8813 8364 603 41 0 8772 0
vsize: 35252
[startup+150.007 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 8421 0 0 0 14974 27 0 0 25 0 1 0 479986822 36098048 8364 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8813 8364 603 41 0 8772 0
vsize: 35252
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 9176 0 0 0 15973 28 0 0 25 0 1 0 479986822 39129088 9119 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9553 9119 603 41 0 9512 0
vsize: 38212
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 9822 0 0 0 16971 30 0 0 25 0 1 0 479986822 41762816 9765 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10196 9765 603 41 0 10155 0
vsize: 40784
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 10492 0 0 0 17969 32 0 0 25 0 1 0 479986822 44539904 10435 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10874 10435 603 41 0 10833 0
vsize: 43496
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11173 0 0 0 18967 33 0 0 25 0 1 0 479986822 47312896 11116 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11551 11116 603 41 0 11510 0
vsize: 46204
[startup+200.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11375 0 0 0 19967 34 0 0 25 0 1 0 479986822 48164864 11317 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11759 11317 603 41 0 11718 0
vsize: 47036
[startup+210.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11375 0 0 0 20967 34 0 0 25 0 1 0 479986822 48164864 11317 4294967295 134512640 134672761 3221224528 3221223712 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11759 11317 603 41 0 11718 0
vsize: 47036
[startup+220.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11375 0 0 0 21967 34 0 0 25 0 1 0 479986822 48164864 11317 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11759 11317 603 41 0 11718 0
vsize: 47036
[startup+230.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11849 0 0 0 22965 36 0 0 25 0 1 0 479986822 50089984 11791 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12229 11791 603 41 0 12188 0
vsize: 48916
[startup+240.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11850 0 0 0 23965 36 0 0 25 0 1 0 479986822 50089984 11792 4294967295 134512640 134672761 3221224528 3221223712 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12229 11792 603 41 0 12188 0
vsize: 48916
[startup+250.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11850 0 0 0 24966 36 0 0 25 0 1 0 479986822 50089984 11792 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12229 11792 603 41 0 12188 0
vsize: 48916
[startup+260.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11850 0 0 0 25965 36 0 0 25 0 1 0 479986822 50089984 11792 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12229 11792 603 41 0 12188 0
vsize: 48916
[startup+270.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11850 0 0 0 26965 36 0 0 25 0 1 0 479986822 50089984 11792 4294967295 134512640 134672761 3221224528 3221223712 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12229 11792 603 41 0 12188 0
vsize: 48916
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11850 0 0 0 27965 37 0 0 25 0 1 0 479986822 50089984 11792 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12229 11792 603 41 0 12188 0
vsize: 48916
[startup+290.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11850 0 0 0 28965 37 0 0 25 0 1 0 479986822 50089984 11792 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12229 11792 603 41 0 12188 0
vsize: 48916
[startup+300.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11850 0 0 0 29965 37 0 0 25 0 1 0 479986822 50073600 11791 4294967295 134512640 134672761 3221224528 3221223712 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12225 11791 603 41 0 12184 0
vsize: 48900
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11850 0 0 0 30965 37 0 0 25 0 1 0 479986822 50073600 11791 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12225 11791 603 41 0 12184 0
vsize: 48900
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11850 0 0 0 31964 38 0 0 25 0 1 0 479986822 50069504 11791 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12224 11791 603 41 0 12183 0
vsize: 48896
[startup+330.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11850 0 0 0 32964 38 0 0 25 0 1 0 479986822 50069504 11791 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12224 11791 603 41 0 12183 0
vsize: 48896
[startup+340.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11850 0 0 0 33964 38 0 0 25 0 1 0 479986822 50069504 11791 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12224 11791 603 41 0 12183 0
vsize: 48896
[startup+350.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11850 0 0 0 34964 39 0 0 25 0 1 0 479986822 50069504 11791 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12224 11791 603 41 0 12183 0
vsize: 48896
[startup+360.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11850 0 0 0 35964 39 0 0 25 0 1 0 479986822 50069504 11791 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12224 11791 603 41 0 12183 0
vsize: 48896
[startup+370.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11852 0 0 0 36963 40 0 0 25 0 1 0 479986822 50065408 11793 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12223 11793 603 41 0 12182 0
vsize: 48892
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11852 0 0 0 37963 40 0 0 25 0 1 0 479986822 50065408 11793 4294967295 134512640 134672761 3221224528 3221223712 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12223 11793 603 41 0 12182 0
vsize: 48892
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11852 0 0 0 38963 40 0 0 25 0 1 0 479986822 50065408 11793 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12223 11793 603 41 0 12182 0
vsize: 48892
[startup+400.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11852 0 0 0 39963 41 0 0 25 0 1 0 479986822 50065408 11793 4294967295 134512640 134672761 3221224528 3221223712 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12223 11793 603 41 0 12182 0
vsize: 48892
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11852 0 0 0 40962 41 0 0 25 0 1 0 479986822 50065408 11793 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12223 11793 603 41 0 12182 0
vsize: 48892
[startup+420.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11852 0 0 0 41963 41 0 0 25 0 1 0 479986822 50065408 11793 4294967295 134512640 134672761 3221224528 3221223568 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12223 11793 603 41 0 12182 0
vsize: 48892
[startup+430.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11852 0 0 0 42963 41 0 0 25 0 1 0 479986822 50065408 11793 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12223 11793 603 41 0 12182 0
vsize: 48892
[startup+440.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11852 0 0 0 43963 41 0 0 25 0 1 0 479986822 50065408 11793 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12223 11793 603 41 0 12182 0
vsize: 48892
[startup+450.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11852 0 0 0 44962 42 0 0 25 0 1 0 479986822 50065408 11793 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12223 11793 603 41 0 12182 0
vsize: 48892
[startup+460.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11852 0 0 0 45962 42 0 0 25 0 1 0 479986822 50065408 11793 4294967295 134512640 134672761 3221224528 3221223568 134612604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12223 11793 603 41 0 12182 0
vsize: 48892
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11852 0 0 0 46962 42 0 0 25 0 1 0 479986822 50065408 11793 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12223 11793 603 41 0 12182 0
vsize: 48892
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11852 0 0 0 47962 43 0 0 25 0 1 0 479986822 50065408 11793 4294967295 134512640 134672761 3221224528 3221223712 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12223 11793 603 41 0 12182 0
vsize: 48892
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11852 0 0 0 48962 43 0 0 25 0 1 0 479986822 50065408 11793 4294967295 134512640 134672761 3221224528 3221223712 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12223 11793 603 41 0 12182 0
vsize: 48892
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11852 0 0 0 49961 43 0 0 25 0 1 0 479986822 50065408 11793 4294967295 134512640 134672761 3221224528 3221223712 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12223 11793 603 41 0 12182 0
vsize: 48892
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11852 0 0 0 50961 44 0 0 25 0 1 0 479986822 50065408 11793 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12223 11793 603 41 0 12182 0
vsize: 48892
[startup+520.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11852 0 0 0 51961 44 0 0 25 0 1 0 479986822 50065408 11793 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12223 11793 603 41 0 12182 0
vsize: 48892
[startup+530.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11852 0 0 0 52961 44 0 0 25 0 1 0 479986822 50065408 11793 4294967295 134512640 134672761 3221224528 3221223712 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12223 11793 603 41 0 12182 0
vsize: 48892
[startup+540.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11852 0 0 0 53961 44 0 0 25 0 1 0 479986822 50053120 11792 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12220 11792 603 41 0 12179 0
vsize: 48880
[startup+550.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11852 0 0 0 54961 45 0 0 25 0 1 0 479986822 50053120 11792 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12220 11792 603 41 0 12179 0
vsize: 48880
[startup+560.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11852 0 0 0 55961 45 0 0 25 0 1 0 479986822 50053120 11792 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12220 11792 603 41 0 12179 0
vsize: 48880
[startup+570.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11852 0 0 0 56961 45 0 0 25 0 1 0 479986822 50053120 11792 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12220 11792 603 41 0 12179 0
vsize: 48880
[startup+580.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11852 0 0 0 57960 46 0 0 25 0 1 0 479986822 50053120 11792 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12220 11792 603 41 0 12179 0
vsize: 48880
[startup+590.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11852 0 0 0 58960 46 0 0 25 0 1 0 479986822 50053120 11792 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12220 11792 603 41 0 12179 0
vsize: 48880
[startup+600.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11852 0 0 0 59960 46 0 0 25 0 1 0 479986822 50053120 11792 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12220 11792 603 41 0 12179 0
vsize: 48880
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11852 0 0 0 60960 46 0 0 25 0 1 0 479986822 50053120 11792 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12220 11792 603 41 0 12179 0
vsize: 48880
[startup+620.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11852 0 0 0 61960 46 0 0 25 0 1 0 479986822 50053120 11792 4294967295 134512640 134672761 3221224528 3221223712 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12220 11792 603 41 0 12179 0
vsize: 48880
[startup+630.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 11852 0 0 0 62960 47 0 0 25 0 1 0 479986822 50053120 11792 4294967295 134512640 134672761 3221224528 3221223712 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12220 11792 603 41 0 12179 0
vsize: 48880
[startup+640.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 12053 0 0 0 63960 47 0 0 25 0 1 0 479986822 50884608 11992 4294967295 134512640 134672761 3221224528 3221223712 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12423 11992 603 41 0 12382 0
vsize: 49692
[startup+650.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 12053 0 0 0 64960 47 0 0 25 0 1 0 479986822 50884608 11992 4294967295 134512640 134672761 3221224528 3221223712 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12423 11992 603 41 0 12382 0
vsize: 49692
[startup+660.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 12053 0 0 0 65960 48 0 0 25 0 1 0 479986822 50884608 11992 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12423 11992 603 41 0 12382 0
vsize: 49692
[startup+670.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 12053 0 0 0 66960 48 0 0 25 0 1 0 479986822 50884608 11992 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12423 11992 603 41 0 12382 0
vsize: 49692
[startup+680.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 12053 0 0 0 67959 48 0 0 25 0 1 0 479986822 50884608 11992 4294967295 134512640 134672761 3221224528 3221223712 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12423 11992 603 41 0 12382 0
vsize: 49692
[startup+690.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 12394 0 0 0 68958 49 0 0 25 0 1 0 479986822 52330496 12333 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12776 12333 603 41 0 12735 0
vsize: 51104
[startup+700.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 12844 0 0 0 69957 50 0 0 25 0 1 0 479986822 54177792 12783 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13227 12783 603 41 0 13186 0
vsize: 52908
[startup+710.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 13134 0 0 0 70956 52 0 0 25 0 1 0 479986822 55394304 13072 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13524 13072 603 41 0 13483 0
vsize: 54096
[startup+720.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 13134 0 0 0 71955 52 0 0 25 0 1 0 479986822 55394304 13072 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13524 13072 603 41 0 13483 0
vsize: 54096
[startup+730.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 13134 0 0 0 72955 53 0 0 25 0 1 0 479986822 55394304 13072 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13524 13072 603 41 0 13483 0
vsize: 54096
[startup+740.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 13134 0 0 0 73955 53 0 0 25 0 1 0 479986822 55394304 13072 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13524 13072 603 41 0 13483 0
vsize: 54096
[startup+750.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 13134 0 0 0 74955 53 0 0 25 0 1 0 479986822 55394304 13072 4294967295 134512640 134672761 3221224528 3221223664 134614724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13524 13072 603 41 0 13483 0
vsize: 54096
[startup+760.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 13134 0 0 0 75954 54 0 0 25 0 1 0 479986822 55394304 13072 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13524 13072 603 41 0 13483 0
vsize: 54096
[startup+770.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 13134 0 0 0 76954 54 0 0 25 0 1 0 479986822 55394304 13072 4294967295 134512640 134672761 3221224528 3221223568 134612835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13524 13072 603 41 0 13483 0
vsize: 54096
[startup+780.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 13134 0 0 0 77954 54 0 0 25 0 1 0 479986822 55394304 13072 4294967295 134512640 134672761 3221224528 3221223712 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13524 13072 603 41 0 13483 0
vsize: 54096
[startup+790.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 13138 0 0 0 78954 54 0 0 25 0 1 0 479986822 55394304 13076 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13524 13076 603 41 0 13483 0
vsize: 54096
[startup+800.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 13335 0 0 0 79954 55 0 0 25 0 1 0 479986822 56320000 13273 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13750 13273 603 41 0 13709 0
vsize: 55000
[startup+810.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 13870 0 0 0 80952 56 0 0 25 0 1 0 479986822 58433536 13808 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14266 13808 603 41 0 14225 0
vsize: 57064
[startup+820.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 13978 0 0 0 81951 57 0 0 25 0 1 0 479986822 58892288 13915 4294967295 134512640 134672761 3221224528 3221223712 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14378 13915 603 41 0 14337 0
vsize: 57512
[startup+830.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 13978 0 0 0 82951 58 0 0 25 0 1 0 479986822 58892288 13915 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14378 13915 603 41 0 14337 0
vsize: 57512
[startup+840.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 13978 0 0 0 83951 58 0 0 25 0 1 0 479986822 58892288 13915 4294967295 134512640 134672761 3221224528 3221223712 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14378 13915 603 41 0 14337 0
vsize: 57512
[startup+850.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 13978 0 0 0 84951 58 0 0 25 0 1 0 479986822 58892288 13915 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14378 13915 603 41 0 14337 0
vsize: 57512
[startup+860.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 13978 0 0 0 85951 58 0 0 25 0 1 0 479986822 58892288 13915 4294967295 134512640 134672761 3221224528 3221223712 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14378 13915 603 41 0 14337 0
vsize: 57512
[startup+870.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 13978 0 0 0 86951 58 0 0 25 0 1 0 479986822 58892288 13915 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14378 13915 603 41 0 14337 0
vsize: 57512
[startup+880.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 13978 0 0 0 87952 58 0 0 25 0 1 0 479986822 58892288 13915 4294967295 134512640 134672761 3221224528 3221223712 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14378 13915 603 41 0 14337 0
vsize: 57512
[startup+890.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 13980 0 0 0 88952 58 0 0 25 0 1 0 479986822 58892288 13917 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14378 13917 603 41 0 14337 0
vsize: 57512
[startup+900.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 13980 0 0 0 89952 58 0 0 25 0 1 0 479986822 58892288 13917 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14378 13917 603 41 0 14337 0
vsize: 57512
[startup+910.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 13991 0 0 0 90952 58 0 0 25 0 1 0 479986822 59088896 13928 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14426 13928 603 41 0 14385 0
vsize: 57704
[startup+920.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 14110 0 0 0 91952 58 0 0 25 0 1 0 479986822 59469824 14047 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14519 14047 603 41 0 14478 0
vsize: 58076
[startup+930.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 14110 0 0 0 92952 58 0 0 25 0 1 0 479986822 59469824 14047 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14519 14047 603 41 0 14478 0
vsize: 58076
[startup+940.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 14110 0 0 0 93952 58 0 0 25 0 1 0 479986822 59469824 14047 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14519 14047 603 41 0 14478 0
vsize: 58076
[startup+950.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 14110 0 0 0 94952 59 0 0 25 0 1 0 479986822 59469824 14047 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14519 14047 603 41 0 14478 0
vsize: 58076
[startup+960.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 14110 0 0 0 95952 59 0 0 25 0 1 0 479986822 59469824 14047 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14519 14047 603 41 0 14478 0
vsize: 58076
[startup+970.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 14110 0 0 0 96952 59 0 0 25 0 1 0 479986822 59469824 14047 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14519 14047 603 41 0 14478 0
vsize: 58076
[startup+980.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 14110 0 0 0 97953 59 0 0 25 0 1 0 479986822 59469824 14047 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14519 14047 603 41 0 14478 0
vsize: 58076
[startup+990.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 14309 0 0 0 98952 60 0 0 25 0 1 0 479986822 60391424 14246 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14744 14246 603 41 0 14703 0
vsize: 58976
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 14580 0 0 0 99951 60 0 0 25 0 1 0 479986822 61390848 14517 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14988 14517 603 41 0 14947 0
vsize: 59952
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 14580 0 0 0 100951 60 0 0 25 0 1 0 479986822 61390848 14517 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14988 14517 603 41 0 14947 0
vsize: 59952
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 14580 0 0 0 101952 60 0 0 25 0 1 0 479986822 61390848 14517 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14988 14517 603 41 0 14947 0
vsize: 59952
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 14580 0 0 0 102952 61 0 0 25 0 1 0 479986822 61390848 14517 4294967295 134512640 134672761 3221224528 3221223568 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14988 14517 603 41 0 14947 0
vsize: 59952
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 14580 0 0 0 103952 61 0 0 25 0 1 0 479986822 61390848 14517 4294967295 134512640 134672761 3221224528 3221223712 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14988 14517 603 41 0 14947 0
vsize: 59952
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 14580 0 0 0 104952 61 0 0 25 0 1 0 479986822 61390848 14517 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14988 14517 603 41 0 14947 0
vsize: 59952
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 14580 0 0 0 105952 61 0 0 25 0 1 0 479986822 61390848 14517 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14988 14517 603 41 0 14947 0
vsize: 59952
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 14580 0 0 0 106952 61 0 0 25 0 1 0 479986822 61390848 14517 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14988 14517 603 41 0 14947 0
vsize: 59952
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 14581 0 0 0 107952 61 0 0 25 0 1 0 479986822 61390848 14518 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14988 14518 603 41 0 14947 0
vsize: 59952
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 14824 0 0 0 108952 61 0 0 25 0 1 0 479986822 62382080 14760 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15230 14760 603 41 0 15189 0
vsize: 60920
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 14824 0 0 0 109952 62 0 0 25 0 1 0 479986822 62382080 14760 4294967295 134512640 134672761 3221224528 3221223712 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15230 14760 603 41 0 15189 0
vsize: 60920
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 14824 0 0 0 110952 62 0 0 25 0 1 0 479986822 62382080 14760 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15230 14760 603 41 0 15189 0
vsize: 60920
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22391
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 14872 0 0 0 111952 62 0 0 25 0 1 0 479986822 62644224 14808 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15294 14808 603 41 0 15253 0
vsize: 61176
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 3/56 22426
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 15915 0 0 0 112950 63 0 0 25 0 1 0 479986822 66875392 15851 4294967295 134512640 134672761 3221224528 3221223712 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16327 15851 603 41 0 16286 0
vsize: 65308
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22444
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 16535 0 0 0 113949 65 0 0 25 0 1 0 479986822 69382144 16470 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16470 603 41 0 16898 0
vsize: 67756
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22444
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 16536 0 0 0 114949 65 0 0 25 0 1 0 479986822 69382144 16471 4294967295 134512640 134672761 3221224528 3221223712 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16471 603 41 0 16898 0
vsize: 67756
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22444
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 16536 0 0 0 115949 65 0 0 25 0 1 0 479986822 69382144 16471 4294967295 134512640 134672761 3221224528 3221223712 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16471 603 41 0 16898 0
vsize: 67756
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22444
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 16536 0 0 0 116950 65 0 0 25 0 1 0 479986822 69382144 16471 4294967295 134512640 134672761 3221224528 3221223712 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16471 603 41 0 16898 0
vsize: 67756
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22444
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 16536 0 0 0 117950 65 0 0 25 0 1 0 479986822 69382144 16471 4294967295 134512640 134672761 3221224528 3221223728 134610644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16471 603 41 0 16898 0
vsize: 67756
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22444
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 16536 0 0 0 118950 65 0 0 25 0 1 0 479986822 69382144 16471 4294967295 134512640 134672761 3221224528 3221223712 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16471 603 41 0 16898 0
vsize: 67756
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 22446
Raw data (stat): 22391 (minisat+) R 22390 18865 18864 0 -1 0 16536 0 0 0 119950 65 0 0 25 0 1 0 479986822 69382144 16471 4294967295 134512640 134672761 3221224528 3221223712 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16939 16471 603 41 0 16898 0
vsize: 67756
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 22446
Raw data (stat): 22391 (minisat+) Z 22390 18865 18864 0 -1 12 16536 0 0 0 119950 68 0 0 25 0 1 0 479986822 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.07
CPU time (s): 1200.19
CPU user time (s): 1199.5
CPU system time (s): 0.685895
CPU usage (%): 100.01
Max. virtual memory (Kb): 67756
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####