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-chnl20_25_pb.cnf.cr.opb
MD5SUM	6c328ef6f9d8d5a179eec9bf3550b7fd
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	26
Number of bits of the biggest sum of numbers	5
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.027995
Number of variables	1000
Total number of constraints	90
Number of constraints which are clauses	50
Number of constraints which are cardinality constraints (but not clauses)	40
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	20
Maximum length of a constraint	25
Trace number 5707

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc32 THE 2005-04-14 01:31:09 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4145 boxname=wulflinc32 idbench=9 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6c328ef6f9d8d5a179eec9bf3550b7fd  /oldhome/oroussel/tmp/wulflinc32/normalized-chnl20_25_pb.cnf.cr.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc32/normalized-chnl20_25_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc32/normalized-chnl20_25_pb.cnf.cr.opb
IDLAUNCH: 4145
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.085
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.085
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:      1034724 kB
MemFree:        705116 kB
Buffers:         35160 kB
Cached:         182656 kB
SwapCached:       1212 kB
Active:         146268 kB
Inactive:       151908 kB
HighTotal:      131072 kB
HighFree:          256 kB
LowTotal:       903652 kB
LowFree:        704860 kB
SwapTotal:     2097892 kB
SwapFree:      2096680 kB
Dirty:            2340 kB
Writeback:           0 kB
Mapped:          81768 kB
Slab:            25616 kB
Committed_AS:   174000 kB
PageTables:        432 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:51:11 (client local time) WITH STATUS 0 IN 1200.19 SECONDS
stats: 4145 7 1200.19 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 90 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................
c ---[  39]---> BDD-cost:   47
c ---[  38]---> BDD-cost:   47
c ---[  37]---> BDD-cost:   47
c ---[  36]---> BDD-cost:   47
c ---[  35]---> BDD-cost:   47
c ---[  34]---> BDD-cost:   47
c ---[  33]---> BDD-cost:   47
c ---[  32]---> BDD-cost:   47
c ---[  31]---> BDD-cost:   47
c ---[  30]---> BDD-cost:   47
c ---[  29]---> BDD-cost:   47
c ---[  28]---> BDD-cost:   47
c ---[  27]---> BDD-cost:   47
c ---[  26]---> BDD-cost:   47
c ---[  25]---> BDD-cost:   47
c ---[  24]---> BDD-cost:   47
c ---[  23]---> BDD-cost:   47
c ---[  22]---> BDD-cost:   47
c ---[  21]---> BDD-cost:   47
c ---[  20]---> BDD-cost:   47
c ---[  19]---> BDD-cost:   47
c ---[  18]---> BDD-cost:   47
c ---[  17]---> BDD-cost:   47
c ---[  16]---> BDD-cost:   47
c ---[  15]---> BDD-cost:   47
c ---[  14]---> BDD-cost:   47
c ---[  13]---> BDD-cost:   47
c ---[  12]---> BDD-cost:   47
c ---[  11]---> BDD-cost:   47
c ---[  10]---> BDD-cost:   47
c ---[   9]---> BDD-cost:   47
c ---[   8]---> BDD-cost:   47
c ---[   7]---> BDD-cost:   47
c ---[   6]---> BDD-cost:   47
c ---[   5]---> BDD-cost:   47
c ---[   4]---> BDD-cost:   47
c ---[   3]---> BDD-cost:   47
c ---[   2]---> BDD-cost:   47
c ---[   1]---> BDD-cost:   47
c ---[   0]---> BDD-cost:   47
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    4690    13080 |    1563       0        0     nan |  0.000 % |
c |       100 |    4690    13080 |    1719     100     6902    69.0 |  1.389 % |
c |       251 |    4690    13080 |    1891     251    20396    81.3 |  1.389 % |
c |       478 |    4690    13080 |    2080     478    46287    96.8 |  1.389 % |
c |       821 |    4690    13080 |    2288     821    81704    99.5 |  1.389 % |
c |      1327 |    4690    13080 |    2517    1327   146172   110.2 |  1.389 % |
c |      2087 |    4690    13080 |    2768    2087   249403   119.5 |  1.389 % |
c |      3227 |    4690    13080 |    3045    3227   373256   115.7 |  1.389 % |
c |      4936 |    4690    13080 |    3350    3323   444218   133.7 |  1.389 % |
c |      7498 |    4690    13080 |    3685    3680   506490   137.6 |  1.389 % |
c |     11342 |    4690    13080 |    4054    2775   386580   139.3 |  1.389 % |
c |     17109 |    4690    13080 |    4459    3425   492300   143.7 |  1.389 % |
c |     25762 |    4690    13080 |    4905    3891   549706   141.3 |  1.389 % |
c |     38739 |    4690    13080 |    5395    5144  1059065   205.9 |  1.389 % |
c |     58201 |    4690    13080 |    5935    3757   878997   234.0 |  1.389 % |
c |     87393 |    4690    13080 |    6529    3337   680756   204.0 |  1.389 % |
c |    131182 |    4690    13080 |    7181    4075   849512   208.5 |  1.389 % |
c |    196867 |    4690    13080 |    7900    6042   961736   159.2 |  1.389 % |
c |    295397 |    4690    13080 |    8690    8012  1389547   173.4 |  1.389 % |
c |    443187 |    4690    13080 |    9559    4859  1092280   224.8 |  1.389 % |
c |    664873 |    4690    13080 |   10515    6850  1659355   242.2 |  1.389 % |
#### 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): 1.01 1.00 0.93 2/53 14033
Raw data (stat): 14033 (runsolver) R 14032 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480643982 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 1346 0 0 0 994 3 0 0 25 0 1 0 480643982 7004160 1324 4294967295 134512640 134672761 3221224528 3221223696 134553603 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1710 1324 603 41 0 1669 0
vsize: 6840
[startup+20.0033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 1562 0 0 0 1993 4 0 0 25 0 1 0 480643982 7954432 1540 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 1942 1540 603 41 0 1901 0
vsize: 7768
[startup+30.0052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 1751 0 0 0 2992 4 0 0 25 0 1 0 480643982 8765440 1729 4294967295 134512640 134672761 3221224528 3221223696 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2140 1729 603 41 0 2099 0
vsize: 8560
[startup+40.0058 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 2315 0 0 0 3991 5 0 0 25 0 1 0 480643982 11059200 2293 4294967295 134512640 134672761 3221224528 3221223632 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2700 2293 603 41 0 2659 0
vsize: 10800
[startup+50.0073 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 2426 0 0 0 4990 6 0 0 25 0 1 0 480643982 11599872 2404 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2832 2404 603 41 0 2791 0
vsize: 11328
[startup+60.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 2426 0 0 0 5990 6 0 0 25 0 1 0 480643982 11534336 2404 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2816 2404 603 41 0 2775 0
vsize: 11264
[startup+70.0088 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 2590 0 0 0 6990 7 0 0 25 0 1 0 480643982 12210176 2568 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2981 2568 603 41 0 2940 0
vsize: 11924
[startup+80.0096 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 2590 0 0 0 7990 7 0 0 25 0 1 0 480643982 12210176 2568 4294967295 134512640 134672761 3221224528 3221223632 134555205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2981 2568 603 41 0 2940 0
vsize: 11924
[startup+90.0104 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 2603 0 0 0 8990 7 0 0 25 0 1 0 480643982 12210176 2581 4294967295 134512640 134672761 3221224528 3221223632 134560418 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2981 2581 603 41 0 2940 0
vsize: 11924
[startup+100.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 2710 0 0 0 9990 7 0 0 25 0 1 0 480643982 12750848 2688 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3113 2688 603 41 0 3072 0
vsize: 12452
[startup+110.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 2756 0 0 0 10989 8 0 0 25 0 1 0 480643982 12881920 2734 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3145 2734 603 41 0 3104 0
vsize: 12580
[startup+120.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 2804 0 0 0 11990 8 0 0 25 0 1 0 480643982 13017088 2782 4294967295 134512640 134672761 3221224528 3221223712 134558423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3178 2782 603 41 0 3137 0
vsize: 12712
[startup+130.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3039 0 0 0 12989 8 0 0 25 0 1 0 480643982 14114816 3017 4294967295 134512640 134672761 3221224528 3221223528 1075350790 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3446 3017 603 41 0 3405 0
vsize: 13784
[startup+140.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3039 0 0 0 13989 8 0 0 25 0 1 0 480643982 14114816 3017 4294967295 134512640 134672761 3221224528 3221223696 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3446 3017 603 41 0 3405 0
vsize: 13784
[startup+150.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3039 0 0 0 14990 8 0 0 25 0 1 0 480643982 14094336 3017 4294967295 134512640 134672761 3221224528 3221223632 134559875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3441 3017 603 41 0 3400 0
vsize: 13764
[startup+160.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3039 0 0 0 15989 9 0 0 25 0 1 0 480643982 14094336 3017 4294967295 134512640 134672761 3221224528 3221223632 134559969 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3441 3017 603 41 0 3400 0
vsize: 13764
[startup+170.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3039 0 0 0 16989 9 0 0 25 0 1 0 480643982 14086144 3017 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3439 3017 603 41 0 3398 0
vsize: 13756
[startup+180.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3039 0 0 0 17990 9 0 0 25 0 1 0 480643982 14086144 3017 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3439 3017 603 41 0 3398 0
vsize: 13756
[startup+190.018 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3040 0 0 0 18990 9 0 0 25 0 1 0 480643982 14069760 3018 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3435 3018 603 41 0 3394 0
vsize: 13740
[startup+200.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3040 0 0 0 19990 9 0 0 25 0 1 0 480643982 14069760 3018 4294967295 134512640 134672761 3221224528 3221223632 134559995 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3435 3018 603 41 0 3394 0
vsize: 13740
[startup+210.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3040 0 0 0 20990 9 0 0 25 0 1 0 480643982 13860864 2987 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3384 2987 603 41 0 3343 0
vsize: 13536
[startup+220.019 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3040 0 0 0 21990 9 0 0 25 0 1 0 480643982 13860864 2987 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3384 2987 603 41 0 3343 0
vsize: 13536
[startup+230.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3040 0 0 0 22991 9 0 0 25 0 1 0 480643982 13860864 2987 4294967295 134512640 134672761 3221224528 3221223712 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3384 2987 603 41 0 3343 0
vsize: 13536
[startup+240.021 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3040 0 0 0 23991 9 0 0 25 0 1 0 480643982 13860864 2987 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3384 2987 603 41 0 3343 0
vsize: 13536
[startup+250.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3040 0 0 0 24991 9 0 0 25 0 1 0 480643982 13860864 2987 4294967295 134512640 134672761 3221224528 3221222604 134566317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3384 2987 603 41 0 3343 0
vsize: 13536
[startup+260.022 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3234 0 0 0 25991 9 0 0 25 0 1 0 480643982 14675968 3181 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3583 3181 603 41 0 3542 0
vsize: 14332
[startup+270.023 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3256 0 0 0 26991 9 0 0 25 0 1 0 480643982 14839808 3203 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3623 3203 603 41 0 3582 0
vsize: 14492
[startup+280.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3256 0 0 0 27991 9 0 0 25 0 1 0 480643982 14839808 3203 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3623 3203 603 41 0 3582 0
vsize: 14492
[startup+290.024 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3263 0 0 0 28991 9 0 0 25 0 1 0 480643982 14839808 3210 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3623 3210 603 41 0 3582 0
vsize: 14492
[startup+300.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3295 0 0 0 29991 9 0 0 25 0 1 0 480643982 14999552 3242 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3662 3242 603 41 0 3621 0
vsize: 14648
[startup+310.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3641 0 0 0 30990 11 0 0 25 0 1 0 480643982 16482304 3588 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4024 3588 603 41 0 3983 0
vsize: 16096
[startup+320.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3771 0 0 0 31990 11 0 0 25 0 1 0 480643982 17018880 3718 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4155 3718 603 41 0 4114 0
vsize: 16620
[startup+330.028 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3772 0 0 0 32990 12 0 0 25 0 1 0 480643982 17018880 3719 4294967295 134512640 134672761 3221224528 3221223632 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4155 3719 603 41 0 4114 0
vsize: 16620
[startup+340.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3772 0 0 0 33990 12 0 0 25 0 1 0 480643982 17018880 3719 4294967295 134512640 134672761 3221224528 3221223712 134558697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4155 3719 603 41 0 4114 0
vsize: 16620
[startup+350.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3772 0 0 0 34990 12 0 0 25 0 1 0 480643982 17018880 3719 4294967295 134512640 134672761 3221224528 3221223696 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4155 3719 603 41 0 4114 0
vsize: 16620
[startup+360.029 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3772 0 0 0 35990 12 0 0 25 0 1 0 480643982 17018880 3719 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4155 3719 603 41 0 4114 0
vsize: 16620
[startup+370.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3772 0 0 0 36991 12 0 0 25 0 1 0 480643982 17018880 3719 4294967295 134512640 134672761 3221224528 3221223696 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4155 3719 603 41 0 4114 0
vsize: 16620
[startup+380.031 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3772 0 0 0 37991 12 0 0 25 0 1 0 480643982 17018880 3719 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4155 3719 603 41 0 4114 0
vsize: 16620
[startup+390.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3772 0 0 0 38990 12 0 0 25 0 1 0 480643982 17018880 3719 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4155 3719 603 41 0 4114 0
vsize: 16620
[startup+400.032 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3773 0 0 0 39989 12 0 0 25 0 1 0 480643982 17018880 3720 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4155 3720 603 41 0 4114 0
vsize: 16620
[startup+410.033 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 3827 0 0 0 40988 13 0 0 25 0 1 0 480643982 17289216 3774 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4221 3774 603 41 0 4180 0
vsize: 16884
[startup+420.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4048 0 0 0 41988 13 0 0 25 0 1 0 480643982 18096128 3995 4294967295 134512640 134672761 3221224528 3221223632 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4418 3995 603 41 0 4377 0
vsize: 17672
[startup+430.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4288 0 0 0 42988 13 0 0 25 0 1 0 480643982 19173376 4235 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4681 4235 603 41 0 4640 0
vsize: 18724
[startup+440.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4383 0 0 0 43988 14 0 0 25 0 1 0 480643982 19574784 4330 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4779 4330 603 41 0 4738 0
vsize: 19116
[startup+450.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4414 0 0 0 44988 14 0 0 25 0 1 0 480643982 19574784 4361 4294967295 134512640 134672761 3221224528 3221223680 134565213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4779 4361 603 41 0 4738 0
vsize: 19116
[startup+460.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4484 0 0 0 45988 14 0 0 25 0 1 0 480643982 19980288 4431 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4878 4431 603 41 0 4837 0
vsize: 19512
[startup+470.037 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4508 0 0 0 46988 14 0 0 25 0 1 0 480643982 19980288 4455 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4878 4455 603 41 0 4837 0
vsize: 19512
[startup+480.038 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4508 0 0 0 47988 14 0 0 25 0 1 0 480643982 19980288 4455 4294967295 134512640 134672761 3221224528 3221223712 134559575 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4878 4455 603 41 0 4837 0
vsize: 19512
[startup+490.039 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4512 0 0 0 48989 14 0 0 25 0 1 0 480643982 20119552 4459 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4912 4459 603 41 0 4871 0
vsize: 19648
[startup+500.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4512 0 0 0 49989 14 0 0 25 0 1 0 480643982 20119552 4459 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4912 4459 603 41 0 4871 0
vsize: 19648
[startup+510.041 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4530 0 0 0 50989 14 0 0 25 0 1 0 480643982 20119552 4477 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4912 4477 603 41 0 4871 0
vsize: 19648
[startup+520.041 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4705 0 0 0 51989 15 0 0 25 0 1 0 480643982 20795392 4652 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5077 4652 603 41 0 5036 0
vsize: 20308
[startup+530.042 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4705 0 0 0 52989 15 0 0 25 0 1 0 480643982 20795392 4652 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5077 4652 603 41 0 5036 0
vsize: 20308
[startup+540.043 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4789 0 0 0 53989 15 0 0 25 0 1 0 480643982 21200896 4736 4294967295 134512640 134672761 3221224528 3221223664 134560611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5176 4736 603 41 0 5135 0
vsize: 20704
[startup+550.045 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4789 0 0 0 54990 15 0 0 25 0 1 0 480643982 21200896 4736 4294967295 134512640 134672761 3221224528 3221223632 134560237 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5176 4736 603 41 0 5135 0
vsize: 20704
[startup+560.045 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4789 0 0 0 55990 15 0 0 25 0 1 0 480643982 21200896 4736 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5176 4736 603 41 0 5135 0
vsize: 20704
[startup+570.046 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4790 0 0 0 56990 15 0 0 25 0 1 0 480643982 21200896 4737 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5176 4737 603 41 0 5135 0
vsize: 20704
[startup+580.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4790 0 0 0 57990 15 0 0 25 0 1 0 480643982 21200896 4737 4294967295 134512640 134672761 3221224528 3221223712 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5176 4737 603 41 0 5135 0
vsize: 20704
[startup+590.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4790 0 0 0 58990 15 0 0 25 0 1 0 480643982 21200896 4737 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5176 4737 603 41 0 5135 0
vsize: 20704
[startup+600.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4790 0 0 0 59991 15 0 0 25 0 1 0 480643982 21200896 4737 4294967295 134512640 134672761 3221224528 3221223712 134559538 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5176 4737 603 41 0 5135 0
vsize: 20704
[startup+610.049 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4790 0 0 0 60991 15 0 0 25 0 1 0 480643982 21200896 4737 4294967295 134512640 134672761 3221224528 3221223664 134565056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5176 4737 603 41 0 5135 0
vsize: 20704
[startup+620.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4790 0 0 0 61991 15 0 0 25 0 1 0 480643982 21200896 4737 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5176 4737 603 41 0 5135 0
vsize: 20704
[startup+630.051 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4790 0 0 0 62991 15 0 0 25 0 1 0 480643982 21200896 4737 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5176 4737 603 41 0 5135 0
vsize: 20704
[startup+640.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4790 0 0 0 63991 15 0 0 25 0 1 0 480643982 21200896 4737 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5176 4737 603 41 0 5135 0
vsize: 20704
[startup+650.052 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4790 0 0 0 64992 15 0 0 25 0 1 0 480643982 21200896 4737 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5176 4737 603 41 0 5135 0
vsize: 20704
[startup+660.053 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4790 0 0 0 65991 15 0 0 25 0 1 0 480643982 21200896 4737 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5176 4737 603 41 0 5135 0
vsize: 20704
[startup+670.055 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4790 0 0 0 66992 15 0 0 25 0 1 0 480643982 21200896 4737 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5176 4737 603 41 0 5135 0
vsize: 20704
[startup+680.055 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4790 0 0 0 67992 15 0 0 25 0 1 0 480643982 21200896 4737 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5176 4737 603 41 0 5135 0
vsize: 20704
[startup+690.055 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4790 0 0 0 68992 15 0 0 25 0 1 0 480643982 21200896 4737 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5176 4737 603 41 0 5135 0
vsize: 20704
[startup+700.056 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4791 0 0 0 69992 15 0 0 25 0 1 0 480643982 21200896 4738 4294967295 134512640 134672761 3221224528 3221223712 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5176 4738 603 41 0 5135 0
vsize: 20704
[startup+710.057 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4810 0 0 0 70992 15 0 0 25 0 1 0 480643982 21336064 4757 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5209 4757 603 41 0 5168 0
vsize: 20836
[startup+720.058 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4810 0 0 0 71992 15 0 0 25 0 1 0 480643982 21331968 4757 4294967295 134512640 134672761 3221224528 3221223696 134561363 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5208 4757 603 41 0 5167 0
vsize: 20832
[startup+730.058 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4826 0 0 0 72993 15 0 0 25 0 1 0 480643982 21331968 4773 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5208 4773 603 41 0 5167 0
vsize: 20832
[startup+740.059 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4925 0 0 0 73993 16 0 0 25 0 1 0 480643982 21753856 4872 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5311 4872 603 41 0 5270 0
vsize: 21244
[startup+750.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4945 0 0 0 74993 16 0 0 25 0 1 0 480643982 21913600 4892 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5350 4892 603 41 0 5309 0
vsize: 21400
[startup+760.061 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4975 0 0 0 75993 16 0 0 25 0 1 0 480643982 22077440 4922 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5390 4922 603 41 0 5349 0
vsize: 21560
[startup+770.061 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4975 0 0 0 76993 16 0 0 25 0 1 0 480643982 22077440 4922 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5390 4922 603 41 0 5349 0
vsize: 21560
[startup+780.062 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4975 0 0 0 77993 16 0 0 25 0 1 0 480643982 22077440 4922 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5390 4922 603 41 0 5349 0
vsize: 21560
[startup+790.063 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4975 0 0 0 78993 16 0 0 25 0 1 0 480643982 22077440 4922 4294967295 134512640 134672761 3221224528 3221223712 134559345 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5390 4922 603 41 0 5349 0
vsize: 21560
[startup+800.063 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4975 0 0 0 79994 16 0 0 25 0 1 0 480643982 22077440 4922 4294967295 134512640 134672761 3221224528 3221223632 134560224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5390 4922 603 41 0 5349 0
vsize: 21560
[startup+810.064 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4975 0 0 0 80994 16 0 0 25 0 1 0 480643982 22077440 4922 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5390 4922 603 41 0 5349 0
vsize: 21560
[startup+820.065 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4975 0 0 0 81994 16 0 0 25 0 1 0 480643982 22077440 4922 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5390 4922 603 41 0 5349 0
vsize: 21560
[startup+830.066 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 4975 0 0 0 82994 16 0 0 25 0 1 0 480643982 22077440 4922 4294967295 134512640 134672761 3221224528 3221223712 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5390 4922 603 41 0 5349 0
vsize: 21560
[startup+840.066 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5001 0 0 0 83994 16 0 0 25 0 1 0 480643982 22220800 4948 4294967295 134512640 134672761 3221224528 3221223696 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5425 4948 603 41 0 5384 0
vsize: 21700
[startup+850.067 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5001 0 0 0 84994 16 0 0 25 0 1 0 480643982 22220800 4948 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5425 4948 603 41 0 5384 0
vsize: 21700
[startup+860.067 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5002 0 0 0 85995 16 0 0 25 0 1 0 480643982 22220800 4949 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5425 4949 603 41 0 5384 0
vsize: 21700
[startup+870.068 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5002 0 0 0 86995 16 0 0 25 0 1 0 480643982 22220800 4949 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5425 4949 603 41 0 5384 0
vsize: 21700
[startup+880.069 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5002 0 0 0 87995 16 0 0 25 0 1 0 480643982 22220800 4949 4294967295 134512640 134672761 3221224528 3221223712 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5425 4949 603 41 0 5384 0
vsize: 21700
[startup+890.069 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5002 0 0 0 88995 17 0 0 25 0 1 0 480643982 22220800 4949 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5425 4949 603 41 0 5384 0
vsize: 21700
[startup+900.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5002 0 0 0 89995 17 0 0 25 0 1 0 480643982 22220800 4949 4294967295 134512640 134672761 3221224528 3221223696 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5425 4949 603 41 0 5384 0
vsize: 21700
[startup+910.071 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5002 0 0 0 90995 17 0 0 25 0 1 0 480643982 22220800 4949 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5425 4949 603 41 0 5384 0
vsize: 21700
[startup+920.072 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5319 0 0 0 91993 18 0 0 25 0 1 0 480643982 23457792 5266 4294967295 134512640 134672761 3221224528 3221223680 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5727 5266 603 41 0 5686 0
vsize: 22908
[startup+930.073 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5326 0 0 0 92993 18 0 0 25 0 1 0 480643982 23597056 5273 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5761 5273 603 41 0 5720 0
vsize: 23044
[startup+940.073 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5326 0 0 0 93993 18 0 0 25 0 1 0 480643982 23597056 5273 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5761 5273 603 41 0 5720 0
vsize: 23044
[startup+950.074 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5326 0 0 0 94993 18 0 0 25 0 1 0 480643982 23597056 5273 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5761 5273 603 41 0 5720 0
vsize: 23044
[startup+960.075 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5331 0 0 0 95993 18 0 0 25 0 1 0 480643982 23597056 5278 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5761 5278 603 41 0 5720 0
vsize: 23044
[startup+970.077 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5331 0 0 0 96994 18 0 0 25 0 1 0 480643982 23597056 5278 4294967295 134512640 134672761 3221224528 3221223712 134559550 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5761 5278 603 41 0 5720 0
vsize: 23044
[startup+980.077 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5386 0 0 0 97994 18 0 0 25 0 1 0 480643982 23732224 5333 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5794 5333 603 41 0 5753 0
vsize: 23176
[startup+990.077 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5457 0 0 0 98994 18 0 0 25 0 1 0 480643982 24018944 5404 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5864 5404 603 41 0 5823 0
vsize: 23456
[startup+1000.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5457 0 0 0 99994 18 0 0 25 0 1 0 480643982 24018944 5404 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5864 5404 603 41 0 5823 0
vsize: 23456
[startup+1010.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5457 0 0 0 100994 18 0 0 25 0 1 0 480643982 24018944 5404 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5864 5404 603 41 0 5823 0
vsize: 23456
[startup+1020.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5457 0 0 0 101994 19 0 0 25 0 1 0 480643982 24018944 5404 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5864 5404 603 41 0 5823 0
vsize: 23456
[startup+1030.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5598 0 0 0 102994 19 0 0 25 0 1 0 480643982 24694784 5545 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6029 5545 603 41 0 5988 0
vsize: 24116
[startup+1040.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5598 0 0 0 103994 19 0 0 25 0 1 0 480643982 24686592 5545 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6027 5545 603 41 0 5986 0
vsize: 24108
[startup+1050.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5598 0 0 0 104994 19 0 0 25 0 1 0 480643982 24686592 5545 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6027 5545 603 41 0 5986 0
vsize: 24108
[startup+1060.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5598 0 0 0 105994 19 0 0 25 0 1 0 480643982 24608768 5545 4294967295 134512640 134672761 3221224528 3221223696 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6008 5545 603 41 0 5967 0
vsize: 24032
[startup+1070.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5598 0 0 0 106995 19 0 0 25 0 1 0 480643982 24604672 5545 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6007 5545 603 41 0 5966 0
vsize: 24028
[startup+1080.08 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5598 0 0 0 107995 19 0 0 25 0 1 0 480643982 24600576 5545 4294967295 134512640 134672761 3221224528 3221223696 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6006 5545 603 41 0 5965 0
vsize: 24024
[startup+1090.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5598 0 0 0 108995 19 0 0 25 0 1 0 480643982 24600576 5545 4294967295 134512640 134672761 3221224528 3221223696 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6006 5545 603 41 0 5965 0
vsize: 24024
[startup+1100.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5598 0 0 0 109995 19 0 0 25 0 1 0 480643982 24600576 5545 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6006 5545 603 41 0 5965 0
vsize: 24024
[startup+1110.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5598 0 0 0 110996 19 0 0 25 0 1 0 480643982 24600576 5545 4294967295 134512640 134672761 3221224528 3221223728 134557892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6006 5545 603 41 0 5965 0
vsize: 24024
[startup+1120.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5818 0 0 0 111996 20 0 0 25 0 1 0 480643982 25583616 5765 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6246 5765 603 41 0 6205 0
vsize: 24984
[startup+1130.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5818 0 0 0 112996 20 0 0 25 0 1 0 480643982 25583616 5765 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6246 5765 603 41 0 6205 0
vsize: 24984
[startup+1140.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 5966 0 0 0 113995 20 0 0 25 0 1 0 480643982 26124288 5913 4294967295 134512640 134672761 3221224528 3221223696 134561014 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6378 5913 603 41 0 6337 0
vsize: 25512
[startup+1150.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 6019 0 0 0 114996 20 0 0 25 0 1 0 480643982 26394624 5966 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6444 5966 603 41 0 6403 0
vsize: 25776
[startup+1160.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 6213 0 0 0 115995 21 0 0 25 0 1 0 480643982 27205632 6160 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6642 6160 603 41 0 6601 0
vsize: 26568
[startup+1170.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 6214 0 0 0 116996 21 0 0 25 0 1 0 480643982 27205632 6161 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6642 6161 603 41 0 6601 0
vsize: 26568
[startup+1180.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 6214 0 0 0 117996 21 0 0 25 0 1 0 480643982 27205632 6161 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6642 6161 603 41 0 6601 0
vsize: 26568
[startup+1190.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 6214 0 0 0 118996 21 0 0 25 0 1 0 480643982 27205632 6161 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6642 6161 603 41 0 6601 0
vsize: 26568
[startup+1200.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14033
Raw data (stat): 14033 (minisat+) R 14032 7987 7986 0 -1 0 6214 0 0 0 119996 21 0 0 25 0 1 0 480643982 27205632 6161 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6642 6161 603 41 0 6601 0
vsize: 26568
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 1.00 0.93 1/53 14033
Raw data (stat): 14033 (minisat+) Z 14032 7987 7986 0 -1 12 6216 0 0 0 119996 22 0 0 25 0 1 0 480643982 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.11
CPU time (s): 1200.19
CPU user time (s): 1199.97
CPU system time (s): 0.225965
CPU usage (%): 100.007
Max. virtual memory (Kb): 26568
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####