PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl30_31_pb.cnf.cr.opb
MD5SUM	79bafd08ddd684356ab9abc8fabf88a7
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	32
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.05399
Number of variables	1860
Total number of constraints	122
Number of constraints which are clauses	62
Number of constraints which are cardinality constraints (but not clauses)	60
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	30
Maximum length of a constraint	31
Trace number 5330

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-13 23:30:45 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3771 boxname=wulflinc2 idbench=11 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  79bafd08ddd684356ab9abc8fabf88a7  /oldhome/oroussel/tmp/wulflinc2/normalized-chnl30_31_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc2/normalized-chnl30_31_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc2/normalized-chnl30_31_pb.cnf.cr.opb
IDLAUNCH: 3771
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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.191
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:        903860 kB
Buffers:         33960 kB
Cached:          76468 kB
SwapCached:          4 kB
Active:          55780 kB
Inactive:        57536 kB
HighTotal:      131008 kB
HighFree:        50736 kB
LowTotal:       903652 kB
LowFree:        853124 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11996 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:50:47 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 3771 7 1200.24 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 122 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..............................................................
c ---[  59]---> BDD-cost:   59
c ---[  58]---> BDD-cost:   59
c ---[  57]---> BDD-cost:   59
c ---[  56]---> BDD-cost:   59
c ---[  55]---> BDD-cost:   59
c ---[  54]---> BDD-cost:   59
c ---[  53]---> BDD-cost:   59
c ---[  52]---> BDD-cost:   59
c ---[  51]---> BDD-cost:   59
c ---[  50]---> BDD-cost:   59
c ---[  49]---> BDD-cost:   59
c ---[  48]---> BDD-cost:   59
c ---[  47]---> BDD-cost:   59
c ---[  46]---> BDD-cost:   59
c ---[  45]---> BDD-cost:   59
c ---[  44]---> BDD-cost:   59
c ---[  43]---> BDD-cost:   59
c ---[  42]---> BDD-cost:   59
c ---[  41]---> BDD-cost:   59
c ---[  40]---> BDD-cost:   59
c ---[  39]---> BDD-cost:   59
c ---[  38]---> BDD-cost:   59
c ---[  37]---> BDD-cost:   59
c ---[  36]---> BDD-cost:   59
c ---[  35]---> BDD-cost:   59
c ---[  34]---> BDD-cost:   59
c ---[  33]---> BDD-cost:   59
c ---[  32]---> BDD-cost:   59
c ---[  31]---> BDD-cost:   59
c ---[  30]---> BDD-cost:   59
c ---[  29]---> BDD-cost:   59
c ---[  28]---> BDD-cost:   59
c ---[  27]---> BDD-cost:   59
c ---[  26]---> BDD-cost:   59
c ---[  25]---> BDD-cost:   59
c ---[  24]---> BDD-cost:   59
c ---[  23]---> BDD-cost:   59
c ---[  22]---> BDD-cost:   59
c ---[  21]---> BDD-cost:   59
c ---[  20]---> BDD-cost:   59
c ---[  19]---> BDD-cost:   59
c ---[  18]---> BDD-cost:   59
c ---[  17]---> BDD-cost:   59
c ---[  16]---> BDD-cost:   59
c ---[  15]---> BDD-cost:   59
c ---[  14]---> BDD-cost:   59
c ---[  13]---> BDD-cost:   59
c ---[  12]---> BDD-cost:   59
c ---[  11]---> BDD-cost:   59
c ---[  10]---> BDD-cost:   59
c ---[   9]---> BDD-cost:   59
c ---[   8]---> BDD-cost:   59
c ---[   7]---> BDD-cost:   59
c ---[   6]---> BDD-cost:   59
c ---[   5]---> BDD-cost:   59
c ---[   4]---> BDD-cost:   59
c ---[   3]---> BDD-cost:   59
c ---[   2]---> BDD-cost:   59
c ---[   1]---> BDD-cost:   59
c ---[   0]---> BDD-cost:   59
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    8822    24660 |    2646       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5340          
c   -- var.elim.:  2000/5340          
c   -- var.elim.:  3000/5340          
c   -- var.elim.:  4000/5340          
c   -- var.elim.:  5000/5340          
c   -- var.elim.:  5340/5340          
c   -- var.elim.:  1000/2106          
c   -- var.elim.:  2000/2106          
c   -- var.elim.:  2106/2106          
c   -- var.elim.:  126/126          
c   -- subsuming                       
c   -- var.elim.:  1000/1240          
c   -- var.elim.:  1240/1240          
c   -- var.elim.:  582/582          
c   -- var.elim.:  194/194          
c   -- var.elim.:  192/192          
c   -- var.elim.:  88/88          
c   -- var.elim.:  80/80          
c   -- var.elim.:  82/82          
c   -- var.elim.:  84/84          
c   -- var.elim.:  86/86          
c   -- var.elim.:  88/88          
c   -- var.elim.:  90/90          
c   -- var.elim.:  92/92          
c   -- var.elim.:  94/94          
c   -- var.elim.:  96/96          
c   -- var.elim.:  98/98          
c   -- var.elim.:  100/100          
c   -- var.elim.:  102/102          
c   -- var.elim.:  104/104          
c   -- var.elim.:  106/106          
c   -- var.elim.:  108/108          
c   -- var.elim.:  110/110          
c   -- var.elim.:  112/112          
c   -- var.elim.:  114/114          
c   -- var.elim.:  116/116          
c   -- var.elim.:  118/118          
c   -- var.elim.:  120/120          
c   -- var.elim.:  286/286          
c   -- subsuming                       
c   -- var.elim.:  1000/2042          
c   -- var.el#### 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.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (runsolver) R 23752 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421706525 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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+10.0007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 2910 0 0 0 990 7 0 0 25 0 1 0 421706525 13635584 2888 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3329 2888 603 41 0 3288 0
vsize: 13316
[startup+20.0011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 3575 0 0 0 1989 9 0 0 25 0 1 0 421706525 16416768 3553 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4008 3553 603 41 0 3967 0
vsize: 16032
[startup+30.0008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 4098 0 0 0 2989 9 0 0 25 0 1 0 421706525 18538496 4076 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4526 4076 603 41 0 4485 0
vsize: 18104
[startup+40.0008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 4479 0 0 0 3988 10 0 0 25 0 1 0 421706525 20078592 4457 4294967295 134512640 134672761 3221224544 3221223680 134614724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4902 4458 603 41 0 4861 0
vsize: 19608
[startup+50.0015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 4716 0 0 0 4988 11 0 0 25 0 1 0 421706525 21094400 4694 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5150 4694 603 41 0 5109 0
vsize: 20600
[startup+60.0019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 5177 0 0 0 5986 13 0 0 25 0 1 0 421706525 22974464 5155 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5609 5155 603 41 0 5568 0
vsize: 22436
[startup+70.0029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 5223 0 0 0 6987 13 0 0 25 0 1 0 421706525 23236608 5201 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5673 5201 603 41 0 5632 0
vsize: 22692
[startup+80.0026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 5482 0 0 0 7986 13 0 0 25 0 1 0 421706525 24240128 5460 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5918 5460 603 41 0 5877 0
vsize: 23672
[startup+90.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 5482 0 0 0 8986 13 0 0 25 0 1 0 421706525 24211456 5460 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5911 5460 603 41 0 5870 0
vsize: 23644
[startup+100.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 5482 0 0 0 9986 13 0 0 25 0 1 0 421706525 24211456 5460 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5911 5460 603 41 0 5870 0
vsize: 23644
[startup+110.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 5482 0 0 0 10987 13 0 0 25 0 1 0 421706525 24162304 5458 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5899 5458 603 41 0 5858 0
vsize: 23596
[startup+120.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 5750 0 0 0 11986 14 0 0 25 0 1 0 421706525 25329664 5726 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6184 5726 603 41 0 6143 0
vsize: 24736
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 6042 0 0 0 12985 15 0 0 25 0 1 0 421706525 26529792 6018 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6477 6018 603 41 0 6436 0
vsize: 25908
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 6557 0 0 0 13984 16 0 0 25 0 1 0 421706525 28626944 6533 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6989 6533 603 41 0 6948 0
vsize: 27956
[startup+150.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 6557 0 0 0 14984 16 0 0 25 0 1 0 421706525 28626944 6533 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6989 6533 603 41 0 6948 0
vsize: 27956
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 6557 0 0 0 15984 16 0 0 25 0 1 0 421706525 28626944 6533 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6989 6533 603 41 0 6948 0
vsize: 27956
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 6557 0 0 0 16985 16 0 0 25 0 1 0 421706525 28626944 6533 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6989 6533 603 41 0 6948 0
vsize: 27956
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 6557 0 0 0 17985 16 0 0 25 0 1 0 421706525 28626944 6533 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6989 6533 603 41 0 6948 0
vsize: 27956
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 6557 0 0 0 18985 17 0 0 25 0 1 0 421706525 28626944 6533 4294967295 134512640 134672761 3221224544 3221223600 134644246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6989 6533 603 41 0 6948 0
vsize: 27956
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 6557 0 0 0 19985 17 0 0 25 0 1 0 421706525 28622848 6533 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6988 6533 603 41 0 6947 0
vsize: 27952
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 6558 0 0 0 20985 17 0 0 25 0 1 0 421706525 28622848 6534 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6988 6534 603 41 0 6947 0
vsize: 27952
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 6589 0 0 0 21985 17 0 0 25 0 1 0 421706525 28749824 6565 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7019 6565 603 41 0 6978 0
vsize: 28076
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 6589 0 0 0 22986 17 0 0 25 0 1 0 421706525 28749824 6565 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7019 6565 603 41 0 6978 0
vsize: 28076
[startup+240.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 6771 0 0 0 23985 17 0 0 25 0 1 0 421706525 29495296 6747 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7201 6747 603 41 0 7160 0
vsize: 28804
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 7068 0 0 0 24985 18 0 0 25 0 1 0 421706525 30679040 7044 4294967295 134512640 134672761 3221224544 3221223640 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7490 7044 603 41 0 7449 0
vsize: 29960
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 7068 0 0 0 25985 18 0 0 25 0 1 0 421706525 30679040 7044 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7490 7044 603 41 0 7449 0
vsize: 29960
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 7099 0 0 0 26985 18 0 0 25 0 1 0 421706525 30810112 7075 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7522 7075 603 41 0 7481 0
vsize: 30088
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 7099 0 0 0 27985 18 0 0 25 0 1 0 421706525 30810112 7075 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7522 7075 603 41 0 7481 0
vsize: 30088
[startup+290.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 7099 0 0 0 28985 18 0 0 25 0 1 0 421706525 30810112 7075 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7522 7075 603 41 0 7481 0
vsize: 30088
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 7503 0 0 0 29985 18 0 0 25 0 1 0 421706525 32514048 7479 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7938 7479 603 41 0 7897 0
vsize: 31752
[startup+310.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 7533 0 0 0 30985 18 0 0 25 0 1 0 421706525 32645120 7509 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7970 7509 603 41 0 7929 0
vsize: 31880
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 7557 0 0 0 31985 18 0 0 25 0 1 0 421706525 32776192 7533 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8002 7533 603 41 0 7961 0
vsize: 32008
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 8225 0 0 0 32984 20 0 0 25 0 1 0 421706525 35516416 8201 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8671 8201 603 41 0 8630 0
vsize: 34684
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 8225 0 0 0 33984 20 0 0 25 0 1 0 421706525 35516416 8201 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8671 8201 603 41 0 8630 0
vsize: 34684
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 8225 0 0 0 34984 20 0 0 25 0 1 0 421706525 35459072 8201 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8657 8201 603 41 0 8616 0
vsize: 34628
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 8225 0 0 0 35984 20 0 0 25 0 1 0 421706525 35459072 8201 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8657 8201 603 41 0 8616 0
vsize: 34628
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 8225 0 0 0 36984 20 0 0 25 0 1 0 421706525 35250176 8153 4294967295 134512640 134672761 3221224544 3221223376 1075350544 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8606 8153 603 41 0 8565 0
vsize: 34424
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 8225 0 0 0 37984 20 0 0 25 0 1 0 421706525 35250176 8153 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8606 8153 603 41 0 8565 0
vsize: 34424
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 8225 0 0 0 38985 20 0 0 25 0 1 0 421706525 35250176 8153 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8606 8153 603 41 0 8565 0
vsize: 34424
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 8225 0 0 0 39985 20 0 0 25 0 1 0 421706525 35250176 8153 4294967295 134512640 134672761 3221224544 3221223584 134612630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8606 8153 603 41 0 8565 0
vsize: 34424
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 8225 0 0 0 40985 20 0 0 25 0 1 0 421706525 35250176 8153 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8606 8153 603 41 0 8565 0
vsize: 34424
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 8225 0 0 0 41985 20 0 0 25 0 1 0 421706525 35250176 8153 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8606 8153 603 41 0 8565 0
vsize: 34424
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 8225 0 0 0 42985 20 0 0 25 0 1 0 421706525 35250176 8153 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8606 8153 603 41 0 8565 0
vsize: 34424
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 8480 0 0 0 43985 21 0 0 25 0 1 0 421706525 36372480 8407 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8880 8407 603 41 0 8839 0
vsize: 35520
[startup+450.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 8484 0 0 0 44985 21 0 0 25 0 1 0 421706525 36372480 8411 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8880 8411 603 41 0 8839 0
vsize: 35520
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 8498 0 0 0 45985 21 0 0 25 0 1 0 421706525 36536320 8425 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8920 8425 603 41 0 8879 0
vsize: 35680
[startup+470.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 8515 0 0 0 46985 21 0 0 25 0 1 0 421706525 36536320 8442 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8920 8442 603 41 0 8879 0
vsize: 35680
[startup+480.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 8563 0 0 0 47986 21 0 0 25 0 1 0 421706525 36782080 8490 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8980 8490 603 41 0 8939 0
vsize: 35920
[startup+490.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 8564 0 0 0 48986 21 0 0 25 0 1 0 421706525 36782080 8491 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8980 8491 603 41 0 8939 0
vsize: 35920
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 8565 0 0 0 49986 21 0 0 25 0 1 0 421706525 36782080 8492 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8980 8492 603 41 0 8939 0
vsize: 35920
[startup+510.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 8698 0 0 0 50986 22 0 0 25 0 1 0 421706525 37326848 8624 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9113 8624 603 41 0 9072 0
vsize: 36452
[startup+520.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 8698 0 0 0 51986 22 0 0 25 0 1 0 421706525 37326848 8624 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9113 8624 603 41 0 9072 0
vsize: 36452
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 8698 0 0 0 52986 22 0 0 25 0 1 0 421706525 37326848 8624 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9113 8624 603 41 0 9072 0
vsize: 36452
[startup+540.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9074 0 0 0 53985 23 0 0 25 0 1 0 421706525 38862848 9000 4294967295 134512640 134672761 3221224544 3221223728 134615576 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9488 9000 603 41 0 9447 0
vsize: 37952
[startup+550.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9074 0 0 0 54985 23 0 0 25 0 1 0 421706525 38862848 9000 4294967295 134512640 134672761 3221224544 3221223376 1075350790 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9488 9000 603 41 0 9447 0
vsize: 37952
[startup+560.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9085 0 0 0 55985 23 0 0 25 0 1 0 421706525 38862848 9011 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9488 9011 603 41 0 9447 0
vsize: 37952
[startup+570.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9259 0 0 0 56985 24 0 0 25 0 1 0 421706525 39645184 9185 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9679 9185 603 41 0 9638 0
vsize: 38716
[startup+580.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9259 0 0 0 57985 24 0 0 25 0 1 0 421706525 39645184 9185 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9679 9185 603 41 0 9638 0
vsize: 38716
[startup+590.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9259 0 0 0 58986 24 0 0 25 0 1 0 421706525 39645184 9185 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9679 9185 603 41 0 9638 0
vsize: 38716
[startup+600.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9279 0 0 0 59986 24 0 0 25 0 1 0 421706525 39723008 9205 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9698 9205 603 41 0 9657 0
vsize: 38792
[startup+610.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9279 0 0 0 60986 24 0 0 25 0 1 0 421706525 39723008 9205 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9698 9205 603 41 0 9657 0
vsize: 38792
[startup+620.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9279 0 0 0 61986 24 0 0 25 0 1 0 421706525 39723008 9205 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9698 9205 603 41 0 9657 0
vsize: 38792
[startup+630.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9279 0 0 0 62986 24 0 0 25 0 1 0 421706525 39723008 9205 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9698 9205 603 41 0 9657 0
vsize: 38792
[startup+640.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9279 0 0 0 63986 24 0 0 25 0 1 0 421706525 39723008 9205 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9698 9205 603 41 0 9657 0
vsize: 38792
[startup+650.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9281 0 0 0 64987 24 0 0 25 0 1 0 421706525 39723008 9207 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9698 9207 603 41 0 9657 0
vsize: 38792
[startup+660.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9373 0 0 0 65987 24 0 0 25 0 1 0 421706525 40087552 9299 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9787 9299 603 41 0 9746 0
vsize: 39148
[startup+670.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9373 0 0 0 66987 24 0 0 25 0 1 0 421706525 40087552 9299 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9787 9299 603 41 0 9746 0
vsize: 39148
[startup+680.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9373 0 0 0 67987 24 0 0 25 0 1 0 421706525 40087552 9299 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9787 9299 603 41 0 9746 0
vsize: 39148
[startup+690.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9373 0 0 0 68987 24 0 0 25 0 1 0 421706525 40087552 9299 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9787 9299 603 41 0 9746 0
vsize: 39148
[startup+700.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9576 0 0 0 69986 25 0 0 25 0 1 0 421706525 40914944 9501 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9989 9501 603 41 0 9948 0
vsize: 39956
[startup+710.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9576 0 0 0 70987 25 0 0 25 0 1 0 421706525 40914944 9501 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9989 9501 603 41 0 9948 0
vsize: 39956
[startup+720.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 71987 25 0 0 25 0 1 0 421706525 40914944 9503 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9989 9503 603 41 0 9948 0
vsize: 39956
[startup+730.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 72987 25 0 0 25 0 1 0 421706525 40914944 9503 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9989 9503 603 41 0 9948 0
vsize: 39956
[startup+740.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 73987 25 0 0 25 0 1 0 421706525 40914944 9503 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9989 9503 603 41 0 9948 0
vsize: 39956
[startup+750.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 74987 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+760.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 75987 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+770.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 76988 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+780.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 77988 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+790.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 78988 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+800.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 79988 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+810.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 80988 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+820.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 81989 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+830.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 82989 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+840.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 83989 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+850.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 84989 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+860.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 85989 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+870.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 86989 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223600 134644240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+880.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 87990 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+890.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 88990 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+900.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 89990 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+910.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 90990 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+920.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 91991 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+930.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 92991 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+940.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 93991 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+950.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 94991 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+960.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 95991 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+970.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 96991 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+980.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 97992 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+990.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 98992 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 99992 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 100992 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 101992 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 102992 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 103993 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 104993 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 105993 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 106993 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 107993 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 108994 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 109994 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 110994 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 111994 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 112995 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 113995 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9578 0 0 0 114995 25 0 0 25 0 1 0 421706525 40325120 9371 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9845 9371 603 41 0 9804 0
vsize: 39380
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9706 0 0 0 115995 25 0 0 25 0 1 0 421706525 40898560 9498 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9985 9498 603 41 0 9944 0
vsize: 39940
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9706 0 0 0 116995 25 0 0 25 0 1 0 421706525 40898560 9498 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9985 9498 603 41 0 9944 0
vsize: 39940
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9706 0 0 0 117995 25 0 0 25 0 1 0 421706525 40898560 9498 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9985 9498 603 41 0 9944 0
vsize: 39940
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9878 0 0 0 118995 26 0 0 25 0 1 0 421706525 41562112 9670 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10147 9670 603 41 0 10106 0
vsize: 40588
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 23753
Raw data (stat): 23753 (minisat+) R 23752 20937 20936 0 -1 0 9940 0 0 0 119995 26 0 0 25 0 1 0 421706525 41848832 9731 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10217 9731 603 41 0 10176 0
vsize: 40868
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 23753
Raw data (stat): 23753 (minisat+) Z 23752 20937 20936 0 -1 12 9940 0 0 0 119995 28 0 0 25 0 1 0 421706525 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.04
CPU time (s): 1200.24
CPU user time (s): 1199.96
CPU system time (s): 0.281957
CPU usage (%): 100.016
Max. virtual memory (Kb): 40868
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####