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/een/normalized-air05.opb
MD5SUM	95088621f0c51b4be3bb24a2abf2d630
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	7195
Biggest coefficient in the objective function	2679
Number of bits for the biggest coefficient in the objective function	12
Sum of the numbers in the objective function	3908448
Number of bits of the sum of numbers in the objective function	22
Biggest number in a constraint	2679
Number of bits of the biggest number in a constraint	12
Biggest sum of numbers in a constraint	3908448
Number of bits of the biggest sum of numbers	22
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.35779
Number of variables	7195
Total number of constraints	852
Number of constraints which are clauses	426
Number of constraints which are cardinality constraints (but not clauses)	426
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	3
Maximum length of a constraint	404
Trace number 6918

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-14 20:25:28 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4989 boxname=wulflinc18 idbench=384 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  95088621f0c51b4be3bb24a2abf2d630  /oldhome/oroussel/tmp/wulflinc18/normalized-air05.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc18/normalized-air05.opb /oldhome/oroussel/tmp/wulflinc18/normalized-air05.opb
IDLAUNCH: 4989
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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.177
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:        837528 kB
Buffers:         35708 kB
Cached:         125268 kB
SwapCached:        320 kB
Active:          61200 kB
Inactive:       102964 kB
HighTotal:      131008 kB
HighFree:         1792 kB
LowTotal:       903652 kB
LowFree:        835736 kB
SwapTotal:     2097892 kB
SwapFree:      2097572 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6936 kB
Slab:            27508 kB
Committed_AS:    63704 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 20:45:30 (client local time) WITH STATUS 0 IN 1200.18 SECONDS
stats: 4989 7 1200.18 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 852 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: =================================================================================================================================================================================================================================================================================================================================================================================================================================================
c   -- Clauses(.)/Splits(s): .....
c ---[ 850]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 848]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 846]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 842]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 840]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 838]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 836]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 834]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 830]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 828]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 826]---> Adder-cost: 18   maxlim: 10   bits: 4/4
c ---[ 824]---> Adder-cost: 18   maxlim: 11   bits: 4/4
c ---[ 822]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 820]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 818]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 816]---> Adder-cost: 20   maxlim: 13   bits: 4/4
c ---[ 814]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 812]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 810]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 808]---> Adder-cost: 30   maxlim: 15   bits: 5/4
c ---[ 806]---> Adder-cost: 28   maxlim: 15   bits: 5/4
c ---[ 804]---> Adder-cost: 28   maxlim: 16   bits: 5/5
c ---[ 802]---> Adder-cost: 32   maxlim: 16   bits: 5/5
c ---[ 800]---> Adder-cost: 28   maxlim: 16   bits: 5/5
c ---[ 798]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 796]---> Adder-cost: 28   maxlim: 18   bits: 5/5
c ---[ 790]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 788]---> Adder-cost: 34   maxlim: 19   bits: 5/5
c ---[ 786]---> Adder-cost: 0   maxlim: 19   bits: 5/5
c ---[ 784]---> Adder-cost: 34   maxlim: 20   bits: 5/5
c ---[ 782]---> Adder-cost: 38   maxlim: 20   bits: 5/5
c ---[ 780]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[ 776]---> Adder-cost: 42   maxlim: 22   bits: 5/5
c ---[ 774]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 772]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 770]---> Adder-cost: 38   maxlim: 23   bits: 5/5
c ---[ 768]---> Adder-cost: 44   maxlim: 24   bits: 5/5
c ---[ 766]---> Adder-cost: 44   maxlim: 24   bits: 5/5
c ---[ 764]---> Adder-cost: 40   maxlim: 24   bits: 5/5
c ---[ 762]---> Adder-cost: 46   maxlim: 25   bits: 5/5
c ---[ 760]---> Adder-cost: 44   maxlim: 25   bits: 5/5
c ---[ 758]---> Adder-cost: 46   maxlim: 25   bits: 5/5
c ---[ 756]---> Adder-cost: 0   maxlim: 25   bits: 5/5
c ---[ 754]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 752]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 750]---> Adder-cost: 50   maxlim: 26   bits: 5/5
c ---[ 748]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 746]---> Adder-cost: 50   maxlim: 27   bits: 5/5
c ---[ 744]---> Adder-cost: 50   maxlim: 29   bits: 5/5
c ---[ 742]---> Adder-cost: 60   maxlim: 30   bits: 6/5
c ---[ 740]---> Adder-cost: 48   maxlim: 30   bits: 6/5
c ---[ 738]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[ 736]---> Adder-cost: 54   maxlim: 32   bits: 6/6
c ---[ 734]---> Adder-cost: 64   maxlim: 32   bits: 6/6
c ---[ 732]---> Adder-cost: 62   maxlim: 33   bits: 6/6
c ---[ 730]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[ 728]---> Adder-cost: 64   maxlim: 33   bits: 6/6
c ---[ 726]---> Adder-cost: 68   maxlim: 34   bits: 6/6
c ---[ 724]---> Adder-cost: 66   maxlim: 34   bits: 6/6
c ---[ 722]---> Adder-cost: 68   maxlim: 35   bits: 6/6
c ---[ 720]---> Adder-cost: 68   maxlim: 35   bits: 6/6
c ---[ 718]---> Adder-cost: 68   maxlim: 36   bits: 6/6
c ---[ 716]---> Adder-cost: 66   maxlim: 36   bits: 6/6
c ---[ 714]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[ 712]---> Adder-cost: 70   maxlim: 37   bits: 6/6
c ---[ 710]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[ 708]---> Adder-cost: 76   maxlim: 38   bits: 6/6
c ---[ 706]---> Adder-cost: 76   maxlim: 40   bits: 6/6
c ---[ 704]---> Adder-cost: 76   maxlim: 41   bits: 6/6
c ---[ 700]---> Adder-cost: 64   maxlim: 41   bits: 6/6
c ---[ 698]---> Adder-cost: 82   maxlim: 42   bits: 6/6
c ---[ 696]---> Adder-cost: 62   maxlim: 43   bits: 6/6
c ---[ 694]---> Adder-cost: 82   maxlim: 43   bits: 6/6
c ---[ 692]---> Adder-cost: 84   maxlim: 44   bits: 6/6
c ---[ 690]---> Adder-cost: 84   maxlim: 44   bits: 6/6
c ---[ 688]---> Adder-cost: 84   maxlim: 44   bits: 6/6
c ---[ 686]---> Adder-cost: 78   maxlim: 44   bits: 6/6
c ---[ 684]---> Adder-cost: 84   maxlim: 45   bits: 6/6
c ---[ 682]---> Adder-cost: 90   maxlim: 46   bits: 6/6
c ---[ 680]---> Adder-cost: 80   maxlim: 46   bits: 6/6
c ---[ 678]---> Adder-cost: 90   maxlim: 46   bits: 6/6
c ---[ 676]---> Adder-cost: 92   maxlim: 46   bits: 6/6
c ---[ 674]---> Adder-cost: 0   maxlim: 46   bits: 6/6
c ---[ 672]---> Adder-cost: 88   maxlim: 47   bits: 6/6
c ---[ 670]---> Adder-cost: 90   maxlim: 47   bits: 6/6
c ---[ 668]---> Adder-cost: 92   maxlim: 47   bits: 6/6
c ---[ 666]---> Adder-cost: 98   maxlim: 50   bits: 6/6
c ---[ 664]---> Adder-cost: 98   maxlim: 50   bits: 6/6
c ---[ 662]---> Adder-cost: 92   maxlim: 51   bits: 6/6
c ---[ 660]---> Adder-cost: 98   maxlim: 51   bits: 6/6
c ---[ 658]---> Adder-cost: 98   maxlim: 51   bits: 6/6
c ---[ 656]---> Adder-cost: 98   maxlim: 51   bits: 6/6
c ---[ 654]---> Adder-cost: 98   maxlim: 51   bits: 6/6
c ---[ 652]---> Adder-cost: 100   maxlim: 52   bits: 6/6
c ---[ 650]---> Adder-cost: 80   maxlim: 52   bits: 6/6
c ---[ 648]---> Adder-cost: 96   maxlim: 53   bits: 6/6
c ---[ 646]---> Adder-cost: 80   maxlim: 54   bits: 6/6
c ---[ 644]---> Adder-cost: 106   maxlim: 54   bits: 6/6
c ---[ 642]---> Adder-cost: 104   maxlim: 55   bits: 6/6
c ---[ 640]---> Adder-cost: 92   maxlim: 55   bits: 6/6
c ---[ 638]---> Adder-cost: 106   maxlim: 55   bits: 6/6
c ---[ 636]---> Adder-cost: 0   maxlim: 55   bits: 6/6
c ---[ 634]---> Adder-cost: 84   maxlim: 56   bits: 6/6
c ---[ 632]---> Adder-cost: 106   maxlim: 56   bits: 6/6
c ---[ 630]---> Adder-cost: 108   maxlim: 56   bits: 6/6
c ---[ 628]---> Adder-cost: 82   maxlim: 57   bits: 6/6
c ---[ 626]---> Adder-cost: 104   maxlim: 58   bits: 6/6
c ---[ 624]---> Adder-cost: 98   maxlim: 58   bits: 6/6
c ---[ 622]---> Adder-cost: 94   maxlim: 58   bits: 6/6
c ---[ 620]---> Adder-cost: 86   maxlim: 59   bits: 6/6
c ---[ 618]---> Adder-cost: 110   maxlim: 60   bits: 6/6
c ---[ 616]---> Adder-cost: 112   maxlim: 60   bits: 6/6
c ---[ 614]---> Adder-cost: 124   maxlim: 64   bits: 7/7
c ---[ 612]---> Adder-cost: 126   maxlim: 65   bits: 7/7
c ---[ 610]---> Adder-cost: 128   maxlim: 65   bits: 7/7
c ---[ 608]---> Adder-cost: 116   maxlim: 65   bits: 7/7
c ---[ 606]---> Adder-cost: 128   maxlim: 66   bits: 7/7
c ---[ 604]---> Adder-cost: 110   maxlim: 66   bits: 7/7
c ---[ 602]---> Adder-cost: 0   maxlim: 66   bits: 7/7
c ---[ 600]---> Adder-cost: 132   maxlim: 66   bits: 7/7
c ---[ 598]---> Adder-cost: 118   maxlim: 66   bits: 7/7
c ---[ 596]---> Adder-cost: 128   maxlim: 66   bits: 7/7
c ---[ 594]---> Adder-cost: 122   maxlim: 67   bits: 7/7
c ---[ 592]---> Adder-cost: 134   maxlim: 68   bits: 7/7
c ---[ 590]---> Adder-cost: 134   maxlim: 69   bits: 7/7
c ---[ 588]---> Adder-cost: 116   maxlim: 69   bits: 7/7
c ---[ 586]---> Adder-cost: 134   maxlim: 69   bits: 7/7
c ---[ 584]---> Adder-cost: 114   maxlim: 69   bits: 7/7
c ---[ 582]---> Adder-cost: 132   maxlim: 69   bits: 7/7
c ---[ 580]---> Adder-cost: 140   maxlim: 70   bits: 7/7
c ---[ 578]---> Adder-cost: 140   maxlim: 71   bits: 7/7
c ---[ 576]---> Adder-cost: 120   maxlim: 71   bits: 7/7
c ---[ 574]---> Adder-cost: 114   maxlim: 72   bits: 7/7
c ---[ 572]---> Adder-cost: 110   maxlim: 72   bits: 7/7
c ---[ 570]---> Adder-cost: 118   maxlim: 72   bits: 7/7
c ---[ 568]---> Adder-cost: 142   maxlim: 72   bits: 7/7
c ---[ 567]---> Adder-cost: 146   maxlim: 74   bits: 7/7
c ---[ 565]---> Adder-cost: 146   maxlim: 74   bits: 7/7
c ---[ 563]---> Adder-cost: 124   maxlim: 74   bits: 7/7
c ---[ 561]---> Adder-cost: 136   maxlim: 74   bits: 7/7
c ---[ 557]---> Adder-cost: 0   maxlim: 74   bits: 7/7
c ---[ 555]---> Adder-cost: 146   maxlim: 74   bits: 7/7
c ---[ 553]---> Adder-cost: 142   maxlim: 74   bits: 7/7
c ---[ 551]---> Adder-cost: 54   maxlim: 74   bits: 7/7
c ---[ 548]---> Adder-cost: 146   maxlim: 75   bits: 7/7
c ---[ 546]---> Adder-cost: 146   maxlim: 76   bits: 7/7
c ---[ 544]---> Adder-cost: 146   maxlim: 77   bits: 7/7
c ---[ 542]---> Adder-cost: 148   maxlim: 77   bits: 7/7
c ---[ 540]---> Adder-cost: 84   maxlim: 77   bits: 7/7
c ---[ 538]---> Adder-cost: 156   maxlim: 78   bits: 7/7
c ---[ 536]---> Adder-cost: 90   maxlim: 78   bits: 7/7
c ---[ 534]---> Adder-cost: 156   maxlim: 78   bits: 7/7
c ---[ 532]---> Adder-cost: 152   maxlim: 78   bits: 7/7
c ---[ 530]---> Adder-cost: 156   maxlim: 79   bits: 7/7
c ---[ 528]---> Adder-cost: 154   maxlim: 79   bits: 7/7
c ---[ 526]---> Adder-cost: 146   maxlim: 80   bits: 7/7
c ---[ 524]---> Adder-cost: 158   maxlim: 81   bits: 7/7
c ---[ 522]---> Adder-cost: 162   maxlim: 82   bits: 7/7
c ---[ 520]---> Adder-cost: 162   maxlim: 83   bits: 7/7
c ---[ 518]---> Adder-cost: 144   maxlim: 83   bits: 7/7
c ---[ 516]---> Adder-cost: 160   maxlim: 84   bits: 7/7
c ---[ 514]---> Adder-cost: 164   maxlim: 84   bits: 7/7
c ---[ 512]---> Adder-cost: 164   maxlim: 85   bits: 7/7
c ---[ 510]---> Adder-cost: 160   maxlim: 85   bits: 7/7
c ---[ 508]---> Adder-cost: 150   maxlim: 86   bits: 7/7
c ---[ 506]---> Adder-cost: 148   maxlim: 87   bits: 7/7
c ---[ 504]---> Adder-cost: 158   maxlim: 87   bits: 7/7
c ---[ 502]---> Adder-cost: 170   maxlim: 87   bits: 7/7
c ---[ 500]---> Adder-cost: 166   maxlim: 88   bits: 7/7
c ---[ 498]---> Adder-cost: 160   maxlim: 88   bits: 7/7
c ---[ 496]---> Adder-cost: 116   maxlim: 88   bits: 7/7
c ---[ 494]---> Adder-cost: 156   maxlim: 89   bits: 7/7
c ---[ 492]---> Adder-cost: 128   maxlim: 89   bits: 7/7
c ---[ 490]---> Adder-cost: 172   maxlim: 89   bits: 7/7
c ---[ 488]---> Adder-cost: 174   maxlim: 90   bits: 7/7
c ---[ 486]---> Adder-cost: 176   maxlim: 90   bits: 7/7
c ---[ 484]---> Adder-cost: 176   maxlim: 91   bits: 7/7
c ---[ 482]---> Adder-cost: 176   maxlim: 91   bits: 7/7
c ---[ 480]---> Adder-cost: 170   maxlim: 91   bits: 7/7
c ---[ 478]---> Adder-cost: 176   maxlim: 92   bits: 7/7
c ---[ 476]---> Adder-cost: 178   maxlim: 92   bits: 7/7
c ---[ 474]---> Adder-cost: 150   maxlim: 93   bits: 7/7
c ---[ 472]---> Adder-cost: 188   maxlim: 94   bits: 7/7
c ---[ 470]---> Adder-cost: 186   maxlim: 94   bits: 7/7
c ---[ 468]---> Adder-cost: 186   maxlim: 94   bits: 7/7
c ---[ 464]---> Adder-cost: 188   maxlim: 94   bits: 7/7
c ---[ 462]---> Adder-cost: 174   maxlim: 95   bits: 7/7
c ---[ 460]---> Adder-cost: 186   maxlim: 95   bits: 7/7
c ---[ 458]---> Adder-cost: 156   maxlim: 95   bits: 7/7
c ---[ 456]---> Adder-cost: 190   maxlim: 96   bits: 7/7
c ---[ 454]---> Adder-cost: 190   maxlim: 97   bits: 7/7
c ---[ 452]---> Adder-cost: 194   maxlim: 98   bits: 7/7
c ---[ 450]---> Adder-cost: 166   maxlim: 98   bits: 7/7
c ---[ 448]---> Adder-cost: 120   maxlim: 99   bits: 7/7
c ---[ 446]---> Adder-cost: 172   maxlim: 99   bits: 7/7
c ---[ 444]---> Adder-cost: 194   maxlim: 99   bits: 7/7
c ---[ 442]---> Adder-cost: 190   maxlim: 100   bits: 7/7
c ---[ 440]---> Adder-cost: 196   maxlim: 101   bits: 7/7
c ---[ 438]---> Adder-cost: 146   maxlim: 102   bits: 7/7
c ---[ 436]---> Adder-cost: 196   maxlim: 103   bits: 7/7
c ---[ 434]---> Adder-cost: 202   maxlim: 103   bits: 7/7
c ---[ 432]---> Adder-cost: 202   maxlim: 104   bits: 7/7
c ---[ 430]---> Adder-cost: 204   maxlim: 104   bits: 7/7
c ---[ 429]---> Adder-cost: 174   maxlim: 105   bits: 7/7
c ---[ 427]---> Adder-cost: 156   maxlim: 105   bits: 7/7
c ---[ 425]---> Adder-cost: 196   maxlim: 105   bits: 7/7
c ---[ 422]---> Adder-cost: 202   maxlim: 105   bits: 7/7
c ---[ 420]---> Adder-cost: 204   maxlim: 105   bits: 7/7
c ---[ 418]---> Adder-cost: 208   maxlim: 106   bits: 7/7
c ---[ 416]---> Adder-cost: 208   maxlim: 106   bits: 7/7
c ---[ 414]---> Adder-cost: 176   maxlim: 106   bits: 7/7
c ---[ 412]---> Adder-cost: 152   maxlim: 106   bits: 7/7
c ---[ 410]---> Adder-cost: 188   maxlim: 106   bits: 7/7
c ---[ 408]---> Adder-cost: 202   maxlim: 107   bits: 7/7
c ---[ 406]---> Adder-cost: 160   maxlim: 107   bits: 7/7
c ---[ 404]---> Adder-cost: 182   maxlim: 108   bits: 7/7
c ---[ 402]---> Adder-cost: 182   maxlim: 109   bits: 7/7
c ---[ 400]---> Adder-cost: 216   maxlim: 110   bits: 7/7
c ---[ 398]---> Adder-cost: 214   maxlim: 111   bits: 7/7
c ---[ 395]---> Adder-cost: 220   maxlim: 112   bits: 7/7
c ---[ 393]---> Adder-cost: 216   maxlim: 112   bits: 7/7
c ---[ 391]---> Adder-cost: 196   maxlim: 112   bits: 7/7
c ---[ 390]---> Adder-cost: 212   maxlim: 112   bits: 7/7
c ---[ 388]---> Adder-cost: 188   maxlim: 112   bits: 7/7
c ---[ 386]---> Adder-cost: 184   maxlim: 112   bits: 7/7
c ---[ 384]---> Adder-cost: 130   maxlim: 112   bits: 7/7
c ---[ 382]---> Adder-cost: 220   maxlim: 113   bits: 7/7
c ---[ 380]---> Adder-cost: 142   maxlim: 113   bits: 7/7
c ---[ 378]---> Adder-cost: 222   maxlim: 114   bits: 7/7
c ---[ 376]---> Adder-cost: 224   maxlim: 115   bits: 7/7
c ---[ 374]---> Adder-cost: 190   maxlim: 115   bits: 7/7
c ---[ 372]---> Adder-cost: 224   maxlim: 116   bits: 7/7
c ---[ 370]---> Adder-cost: 206   maxlim: 116   bits: 7/7
c ---[ 368]---> Adder-cost: 146   maxlim: 116   bits: 7/7
c ---[ 366]---> Adder-cost: 214   maxlim: 116   bits: 7/7
c ---[ 364]---> Adder-cost: 202   maxlim: 117   bits: 7/7
c ---[ 362]---> Adder-cost: 218   maxlim: 118   bits: 7/7
c ---[ 360]---> Adder-cost: 194   maxlim: 118   bits: 7/7
c ---[ 358]---> Adder-cost: 228   maxlim: 118   bits: 7/7
c ---[ 356]---> Adder-cost: 162   maxlim: 119   bits: 7/7
c ---[ 354]---> Adder-cost: 210   maxlim: 119   bits: 7/7
c ---[ 352]---> Adder-cost: 230   maxlim: 121   bits: 7/7
c ---[ 350]---> Adder-cost: 214   maxlim: 121   bits: 7/7
c ---[ 348]---> Adder-cost: 234   maxlim: 121   bits: 7/7
c ---[ 346]---> Adder-cost: 198   maxlim: 122   bits: 7/7
c ---[ 344]---> Adder-cost: 186   maxlim: 125   bits: 7/7
c ---[ 342]---> Adder-cost: 234   maxlim: 126   bits: 8/7
c ---[ 340]---> Adder-cost: 254   maxlim: 126   bits: 8/7
c ---[ 338]---> Adder-cost: 248   maxlim: 126   bits: 8/7
c ---[ 335]---> Adder-cost: 228   maxlim: 126   bits: 8/7
c ---[ 333]---> Adder-cost: 232   maxlim: 126   bits: 8/7
c ---[ 331]---> Adder-cost: 252   maxlim: 126   bits: 8/7
c ---[ 330]---> Adder-cost: 254   maxlim: 126   bits: 8/7
c ---[ 328]---> Adder-cost: 190   maxlim: 127   bits: 8/7
c ---[ 326]---> Adder-cost: 212   maxlim: 127   bits: 8/7
c ---[ 324]---> Adder-cost: 188   maxlim: 127   bits: 8/7
c ---[ 322]---> Adder-cost: 256   maxlim: 128   bits: 8/8
c ---[ 320]---> Adder-cost: 254   maxlim: 132   bits: 8/8
c ---[ 318]---> Adder-cost: 218   maxlim: 132   bits: 8/8
c ---[ 314]---> Adder-cost: 264   maxlim: 134   bits: 8/8
c ---[ 312]---> Adder-cost: 266   maxlim: 135   bits: 8/8
c ---[ 310]---> Adder-cost: 260   maxlim: 135   bits: 8/8
c ---[ 308]---> Adder-cost: 270   maxlim: 136   bits: 8/8
c ---[ 306]---> Adder-cost: 262   maxlim: 137   bits: 8/8
c ---[ 304]---> Adder-cost: 264   maxlim: 137   bits: 8/8
c ---[ 302]---> Adder-cost: 260   maxlim: 138   bits: 8/8
c ---[ 300]---> Adder-cost: 272   maxlim: 139   bits: 8/8
c ---[ 298]---> Adder-cost: 224   maxlim: 139   bits: 8/8
c ---[ 296]---> Adder-cost: 276   maxlim: 140   bits: 8/8
c ---[ 294]---> Adder-cost: 266   maxlim: 140   bits: 8/8
c ---[ 290]---> Adder-cost: 276   maxlim: 141   bits: 8/8
c ---[ 288]---> Adder-cost: 268   maxlim: 142   bits: 8/8
c ---[ 286]---> Adder-cost: 282   maxlim: 142   bits: 8/8
c ---[ 284]---> Adder-cost: 284   maxlim: 143   bits: 8/8
c ---[ 282]---> Adder-cost: 216   maxlim: 143   bits: 8/8
c ---[ 280]---> Adder-cost: 266   maxlim: 144   bits: 8/8
c ---[ 278]---> Adder-cost: 284   maxlim: 145   bits: 8/8
c ---[ 276]---> Adder-cost: 288   maxlim: 146   bits: 8/8
c ---[ 274]---> Adder-cost: 276   maxlim: 146   bits: 8/8
c ---[ 272]---> Adder-cost: 264   maxlim: 146   bits: 8/8
c ---[ 270]---> Adder-cost: 242   maxlim: 147   bits: 8/8
c ---[ 268]---> Adder-cost: 234   maxlim: 148   bits: 8/8
c ---[ 266]---> Adder-cost: 284   maxlim: 148   bits: 8/8
c ---[ 264]---> Adder-cost: 270   maxlim: 149   bits: 8/8
c ---[ 262]---> Adder-cost: 266   maxlim: 150   bits: 8/8
c ---[ 260]---> Adder-cost: 292   maxlim: 150   bits: 8/8
c ---[ 258]---> Adder-cost: 218   maxlim: 151   bits: 8/8
c ---[ 256]---> Adder-cost: 260   maxlim: 152   bits: 8/8
c ---[ 254]---> Adder-cost: 300   maxlim: 153   bits: 8/8
c ---[ 252]---> Adder-cost: 292   maxlim: 153   bits: 8/8
c ---[ 250]---> Adder-cost: 300   maxlim: 154   bits: 8/8
c ---[ 248]---> Adder-cost: 298   maxlim: 154   bits: 8/8
c ---[ 246]---> Adder-cost: 180   maxlim: 154   bits: 8/8
c ---[ 244]---> Adder-cost: 240   maxlim: 154   bits: 8/8
c ---[ 242]---> Adder-cost: 292   maxlim: 156   bits: 8/8
c ---[ 240]---> Adder-cost: 260   maxlim: 156   bits: 8/8
c ---[ 238]---> Adder-cost: 296   maxlim: 157   bits: 8/8
c ---[ 236]---> Adder-cost: 234   maxlim: 157   bits: 8/8
c ---[ 234]---> Adder-cost: 274   maxlim: 158   bits: 8/8
c ---[ 232]---> Adder-cost: 306   maxlim: 158   bits: 8/8
c ---[ 230]---> Adder-cost: 314   maxlim: 158   bits: 8/8
c ---[ 226]---> Adder-cost: 314   maxlim: 160   bits: 8/8
c ---[ 224]---> Adder-cost: 262   maxlim: 161   bits: 8/8
c ---[ 222]---> Adder-cost: 288   maxlim: 161   bits: 8/8
c ---[ 220]---> Adder-cost: 262   maxlim: 161   bits: 8/8
c ---[ 218]---> Adder-cost: 296   maxlim: 162   bits: 8/8
c ---[ 216]---> Adder-cost: 276   maxlim: 162   bits: 8/8
c ---[ 214]---> Adder-cost: 312   maxlim: 164   bits: 8/8
c ---[ 212]---> Adder-cost: 288   maxlim: 164   bits: 8/8
c ---[ 210]---> Adder-cost: 308   maxlim: 165   bits: 8/8
c ---[ 208]---> Adder-cost: 282   maxlim: 165   bits: 8/8
c ---[ 206]---> Adder-cost: 326   maxlim: 168   bits: 8/8
c ---[ 204]---> Adder-cost: 202   maxlim: 168   bits: 8/8
c ---[ 202]---> Adder-cost: 234   maxlim: 169   bits: 8/8
c ---[ 200]---> Adder-cost: 326   maxlim: 170   bits: 8/8
c ---[ 198]---> Adder-cost: 310   maxlim: 170   bits: 8/8
c ---[ 196]---> Adder-cost: 330   maxlim: 170   bits: 8/8
c ---[ 194]---> Adder-cost: 320   maxlim: 170   bits: 8/8
c ---[ 192]---> Adder-cost: 298   maxlim: 170   bits: 8/8
c ---[ 190]---> Adder-cost: 328   maxlim: 171   bits: 8/8
c ---[ 188]---> Adder-cost: 236   maxlim: 172   bits: 8/8
c ---[ 186]---> Adder-cost: 294   maxlim: 174   bits: 8/8
c ---[ 184]---> Adder-cost: 330   maxlim: 175   bits: 8/8
c ---[ 182]---> Adder-cost: 340   maxlim: 175   bits: 8/8
c ---[ 180]---> Adder-cost: 342   maxlim: 180   bits: 8/8
c ---[ 178]---> Adder-cost: 324   maxlim: 180   bits: 8/8
c ---[ 176]---> Adder-cost: 348   maxlim: 180   bits: 8/8
c ---[ 174]---> Adder-cost: 250   maxlim: 181   bits: 8/8
c ---[ 172]---> Adder-cost: 306   maxlim: 181   bits: 8/8
c ---[ 170]---> Adder-cost: 334   maxlim: 182   bits: 8/8
c ---[ 168]---> Adder-cost: 352   maxlim: 184   bits: 8/8
c ---[ 166]---> Adder-cost: 308   maxlim: 185   bits: 8/8
c ---[ 164]---> Adder-cost: 342   maxlim: 185   bits: 8/8
c ---[ 162]---> Adder-cost: 354   maxlim: 187   bits: 8/8
c ---[ 160]---> Adder-cost: 352   maxlim: 187   bits: 8/8
c ---[ 158]---> Adder-cost: 354   maxlim: 187   bits: 8/8
c ---[ 156]---> Adder-cost: 360   maxlim: 188   bits: 8/8
c ---[ 154]---> Adder-cost: 286   maxlim: 190   bits: 8/8
c ---[ 152]---> Adder-cost: 364   maxlim: 190   bits: 8/8
c ---[ 150]---> Adder-cost: 296   maxlim: 191   bits: 8/8
c ---[ 148]---> Adder-cost: 346   maxlim: 193   bits: 8/8
c ---[ 146]---> Adder-cost: 362   maxlim: 201   bits: 8/8
c ---[ 144]---> Adder-cost: 332   maxlim: 202   bits: 8/8
c ---[ 142]---> Adder-cost: 390   maxlim: 202   bits: 8/8
c ---[ 140]---> Adder-cost: 376   maxlim: 205   bits: 8/8
c ---[ 138]---> Adder-cost: 404   maxlim: 207   bits: 8/8
c ---[ 136]---> Adder-cost: 398   maxlim: 208   bits: 8/8
c ---[ 134]---> Adder-cost: 360   maxlim: 209   bits: 8/8
c ---[ 132]---> Adder-cost: 402   maxlim: 210   bits: 8/8
c ---[ 130]---> Adder-cost: 382   maxlim: 210   bits: 8/8
c ---[ 128]---> Adder-cost: 404   maxlim: 213   bits: 8/8
c ---[ 126]---> Adder-cost: 416   maxlim: 215   bits: 8/8
c ---[ 124]---> Adder-cost: 342   maxlim: 215   bits: 8/8
c ---[ 122]---> Adder-cost: 406   maxlim: 216   bits: 8/8
c ---[ 120]---> Adder-cost: 412   maxlim: 218   bits: 8/8
c ---[ 118]---> Adder-cost: 376   maxlim: 218   bits: 8/8
c ---[ 116]---> Adder-cost: 430   maxlim: 219   bits: 8/8
c ---[ 114]---> Adder-cost: 382   maxlim: 220   bits: 8/8
c ---[ 112]---> Adder-cost: 382   maxlim: 222   bits: 8/8
c ---[ 110]---> Adder-cost: 402   maxlim: 224   bits: 8/8
c ---[ 108]---> Adder-cost: 410   maxlim: 225   bits: 8/8
c ---[ 106]---> Adder-cost: 436   maxlim: 227   bits: 8/8
c ---[ 104]---> Adder-cost: 428   maxlim: 227   bits: 8/8
c ---[ 102]---> Adder-cost: 420   maxlim: 228   bits: 8/8
c ---[ 100]---> Adder-cost: 416   maxlim: 229   bits: 8/8
c ---[  98]---> Adder-cost: 388   maxlim: 229   bits: 8/8
c ---[  96]---> Adder-cost: 434   maxlim: 231   bits: 8/8
c ---[  94]---> Adder-cost: 414   maxlim: 232   bits: 8/8
c ---[  92]---> Adder-cost: 410   maxlim: 233   bits: 8/8
c ---[  90]---> Adder-cost: 440   maxlim: 237   bits: 8/8
c ---[  88]---> Adder-cost: 440   maxlim: 242   bits: 8/8
c ---[  86]---> Adder-cost: 374   maxlim: 244   bits: 8/8
c ---[  84]---> Adder-cost: 420   maxlim: 246   bits: 8/8
c ---[  82]---> Adder-cost: 466   maxlim: 250   bits: 8/8
c ---[  80]---> Adder-cost: 478   maxlim: 251   bits: 8/8
c ---[  78]---> Adder-cost: 476   maxlim: 254   bits: 9/8
c ---[  76]---> Adder-cost: 484   maxlim: 258   bits: 9/9
c ---[  74]---> Adder-cost: 494   maxlim: 260   bits: 9/9
c ---[  72]---> Adder-cost: 474   maxlim: 261   bits: 9/9
c ---[  70]---> Adder-cost: 504   maxlim: 261   bits: 9/9
c ---[  68]---> Adder-cost: 424   maxlim: 262   bits: 9/9
c ---[  67]---> Adder-cost: 482   maxlim: 266   bits: 9/9
c ---[  65]---> Adder-cost: 506   maxlim: 266   bits: 9/9
c ---[  62]---> Adder-cost: 450   maxlim: 267   bits: 9/9
c ---[  60]---> Adder-cost: 506   maxlim: 270   bits: 9/9
c ---[  58]---> Adder-cost: 502   maxlim: 271   bits: 9/9
c ---[  56]---> Adder-cost: 522   maxlim: 273   bits: 9/9
c ---[  54]---> Adder-cost: 502   maxlim: 273   bits: 9/9
c ---[  52]---> Adder-cost: 472   maxlim: 274   bits: 9/9
c ---[  50]---> Adder-cost: 522   maxlim: 275   bits: 9/9
c ---[  48]---> Adder-cost: 462   maxlim: 281   bits: 9/9
c ---[  46]---> Adder-cost: 526   maxlim: 282   bits: 9/9
c ---[  44]---> Adder-cost: 534   maxlim: 282   bits: 9/9
c ---[  42]---> Adder-cost: 474   maxlim: 285   bits: 9/9
c ---[  40]---> Adder-cost: 400   maxlim: 290   bits: 9/9
c ---[  38]---> Adder-cost: 524   maxlim: 292   bits: 9/9
c ---[  36]---> Adder-cost: 448   maxlim: 292   bits: 9/9
c ---[  34]---> Adder-cost: 528   maxlim: 295   bits: 9/9
c ---[  32]---> Adder-cost: 502   maxlim: 300   bits: 9/9
c ---[  30]---> Adder-cost: 540   maxlim: 300   bits: 9/9
c ---[  28]---> Adder-cost: 604   maxlim: 321   bits: 9/9
c ---[  24]---> Adder-cost: 612   maxlim: 321   bits: 9/9
c ---[  22]---> Adder-cost: 478   maxlim: 328   bits: 9/9
c ---[  20]---> Adder-cost: 620   maxlim: 331   bits: 9/9
c ---[  18]---> Adder-cost: 572   maxlim: 336   bits: 9/9
c ---[  16]---> Adder-cost: 616   maxlim: 343   bits: 9/9
c ---[  14]---> Adder-cost: 604   maxlim: 346   bits: 9/9
c ---[  12]---> Adder-cost: 458   maxlim: 356   bits: 9/9
c ---[  10]---> Adder-cost: 592   maxlim: 356   bits: 9/9
c ---[   8]---> Adder-cost: 684   maxlim: 365   bits: 9/9
c ---[   6]---> Adder-cost: 584   maxlim: 369   bits: 9/9
c ---[   4]---> Adder-cost: 648   maxlim: 372   bits: 9/9
c ---[   2]---> Adder-cost: 584   maxlim: 377   bits: 9/9
c ---[   0]---> Adder-cost: 674   maxlim: 402   bits: 9/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  604646  2156307 |  201548       0        0     nan |  0.000 % |
c |       100 |  604307  2155103 |  221702      58      170     2.9 |  3.499 % |
c |       250 |  603254  2151354 |  243873      79      231     2.9 |  3.698 % |
c |       475 |  601966  2146855 |  268260     153      570     3.7 |  3.952 % |
c |       812 |  599330  2137526 |  295086     197      730     3.7 |  4.468 % |
c |      1318 |  596327  2126974 |  324595     351     1252     3.6 |  5.051 % |
c |      2077 |  591946  2111628 |  357054     581     1950     3.4 |  5.866 % |
c |      3218 |  587045  2094373 |  392760    1120     3940     3.5 |  6.775 % |
c |      4926 |  580506  2071427 |  432036    1964     7344     3.7 |  7.942 % |
c |      7488 |  575291  2053096 |  475239    3722    15546     4.2 |  8.848 % |
c |     11332 |  570838  2037368 |  522763    6903    31020     4.5 |  9.641 % |
c |     17099 |  563064  2009757 |  575039   11559    56462     4.9 | 11.018 % |
#### 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.00 0.00 0.00 2/55 2283
Raw data (stat): 2283 (runsolver) R 2282 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487447670 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0011 s]
Raw data (loadavg): 0.15 0.03 0.01 2/55 2283
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11000 0 0 0 969 29 0 0 25 0 1 0 487447670 49819648 10668 4294967295 134512640 134672761 3221224576 3221223792 134561987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12163 10668 603 41 0 12122 0
vsize: 48652
[startup+20.0009 s]
Raw data (loadavg): 0.28 0.06 0.02 2/55 2283
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11020 0 0 0 1968 30 0 0 25 0 1 0 487447670 49963008 10688 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12198 10688 603 41 0 12157 0
vsize: 48792
[startup+30.0018 s]
Raw data (loadavg): 0.39 0.09 0.03 2/55 2283
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11059 0 0 0 2968 30 0 0 25 0 1 0 487447670 50098176 10727 4294967295 134512640 134672761 3221224576 3221223784 134561960 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12231 10727 603 41 0 12190 0
vsize: 48924
[startup+40.0017 s]
Raw data (loadavg): 0.49 0.12 0.04 2/55 2283
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11083 0 0 0 3967 31 0 0 25 0 1 0 487447670 50233344 10751 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12264 10751 603 41 0 12223 0
vsize: 49056
[startup+50.0026 s]
Raw data (loadavg): 0.56 0.15 0.05 2/55 2283
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11123 0 0 0 4967 32 0 0 25 0 1 0 487447670 50368512 10791 4294967295 134512640 134672761 3221224576 3221223764 134556676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12297 10791 603 41 0 12256 0
vsize: 49188
[startup+60.0031 s]
Raw data (loadavg): 0.63 0.18 0.06 2/55 2283
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11157 0 0 0 5966 32 0 0 25 0 1 0 487447670 50503680 10825 4294967295 134512640 134672761 3221224576 3221223792 134561990 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12330 10825 603 41 0 12289 0
vsize: 49320
[startup+70.0034 s]
Raw data (loadavg): 0.69 0.21 0.07 2/55 2283
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11184 0 0 0 6966 33 0 0 25 0 1 0 487447670 50638848 10852 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12363 10852 603 41 0 12322 0
vsize: 49452
[startup+80.0043 s]
Raw data (loadavg): 0.73 0.23 0.08 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11213 0 0 0 7965 33 0 0 25 0 1 0 487447670 50774016 10881 4294967295 134512640 134672761 3221224576 3221223764 134556588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12396 10881 603 41 0 12355 0
vsize: 49584
[startup+90.0042 s]
Raw data (loadavg): 0.77 0.26 0.09 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11236 0 0 0 8965 34 0 0 25 0 1 0 487447670 50774016 10904 4294967295 134512640 134672761 3221224576 3221223748 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12396 10904 603 41 0 12355 0
vsize: 49584
[startup+100.005 s]
Raw data (loadavg): 0.81 0.28 0.10 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11266 0 0 0 9964 34 0 0 25 0 1 0 487447670 51044352 10934 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12462 10934 603 41 0 12421 0
vsize: 49848
[startup+110.006 s]
Raw data (loadavg): 0.84 0.30 0.11 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11296 0 0 0 10964 35 0 0 25 0 1 0 487447670 51044352 10964 4294967295 134512640 134672761 3221224576 3221223748 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12462 10964 603 41 0 12421 0
vsize: 49848
[startup+120.006 s]
Raw data (loadavg): 0.86 0.33 0.12 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11308 0 0 0 11964 35 0 0 25 0 1 0 487447670 51179520 10976 4294967295 134512640 134672761 3221224576 3221223756 134556674 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12495 10976 603 41 0 12454 0
vsize: 49980
[startup+130.007 s]
Raw data (loadavg): 0.88 0.35 0.12 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11333 0 0 0 12963 36 0 0 25 0 1 0 487447670 51179520 11001 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12495 11001 603 41 0 12454 0
vsize: 49980
[startup+140.007 s]
Raw data (loadavg): 0.90 0.37 0.13 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11351 0 0 0 13963 36 0 0 25 0 1 0 487447670 51314688 11019 4294967295 134512640 134672761 3221224576 3221223748 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12528 11019 603 41 0 12487 0
vsize: 50112
[startup+150.008 s]
Raw data (loadavg): 0.92 0.39 0.14 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11366 0 0 0 14962 37 0 0 25 0 1 0 487447670 51314688 11034 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12528 11034 603 41 0 12487 0
vsize: 50112
[startup+160.008 s]
Raw data (loadavg): 0.93 0.41 0.15 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11379 0 0 0 15962 37 0 0 25 0 1 0 487447670 51449856 11047 4294967295 134512640 134672761 3221224576 3221223748 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12561 11047 603 41 0 12520 0
vsize: 50244
[startup+170.008 s]
Raw data (loadavg): 0.94 0.43 0.16 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11393 0 0 0 16962 38 0 0 25 0 1 0 487447670 51449856 11061 4294967295 134512640 134672761 3221224576 3221223776 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12561 11061 603 41 0 12520 0
vsize: 50244
[startup+180.009 s]
Raw data (loadavg): 0.95 0.45 0.17 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11402 0 0 0 17961 38 0 0 25 0 1 0 487447670 51585024 11070 4294967295 134512640 134672761 3221224576 3221223748 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12594 11070 603 41 0 12553 0
vsize: 50376
[startup+190.009 s]
Raw data (loadavg): 0.95 0.46 0.18 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11417 0 0 0 18961 38 0 0 25 0 1 0 487447670 51585024 11085 4294967295 134512640 134672761 3221224576 3221223748 134556641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12594 11085 603 41 0 12553 0
vsize: 50376
[startup+200.01 s]
Raw data (loadavg): 0.96 0.48 0.19 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11427 0 0 0 19962 38 0 0 25 0 1 0 487447670 51585024 11095 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12594 11095 603 41 0 12553 0
vsize: 50376
[startup+210.01 s]
Raw data (loadavg): 0.97 0.50 0.19 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11438 0 0 0 20962 38 0 0 25 0 1 0 487447670 51585024 11106 4294967295 134512640 134672761 3221224576 3221223776 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12594 11106 603 41 0 12553 0
vsize: 50376
[startup+220.01 s]
Raw data (loadavg): 0.97 0.51 0.20 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11446 0 0 0 21962 38 0 0 25 0 1 0 487447670 51720192 11114 4294967295 134512640 134672761 3221224576 3221223748 134556685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12627 11114 603 41 0 12586 0
vsize: 50508
[startup+230.011 s]
Raw data (loadavg): 0.98 0.53 0.21 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11457 0 0 0 22962 39 0 0 25 0 1 0 487447670 51720192 11125 4294967295 134512640 134672761 3221224576 3221223740 134564522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12627 11125 603 41 0 12586 0
vsize: 50508
[startup+240.01 s]
Raw data (loadavg): 0.98 0.54 0.22 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11464 0 0 0 23961 39 0 0 25 0 1 0 487447670 51720192 11132 4294967295 134512640 134672761 3221224576 3221223744 134564722 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12627 11132 603 41 0 12586 0
vsize: 50508
[startup+250.011 s]
Raw data (loadavg): 0.98 0.56 0.22 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11471 0 0 0 24962 39 0 0 25 0 1 0 487447670 51720192 11139 4294967295 134512640 134672761 3221224576 3221223776 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12627 11139 603 41 0 12586 0
vsize: 50508
[startup+260.012 s]
Raw data (loadavg): 0.98 0.57 0.23 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11475 0 0 0 25962 39 0 0 25 0 1 0 487447670 51720192 11143 4294967295 134512640 134672761 3221224576 3221223748 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12627 11143 603 41 0 12586 0
vsize: 50508
[startup+270.012 s]
Raw data (loadavg): 0.99 0.59 0.24 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11477 0 0 0 26962 39 0 0 25 0 1 0 487447670 51720192 11145 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12627 11145 603 41 0 12586 0
vsize: 50508
[startup+280.013 s]
Raw data (loadavg): 0.99 0.60 0.25 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11478 0 0 0 27962 39 0 0 25 0 1 0 487447670 51855360 11146 4294967295 134512640 134672761 3221224576 3221223748 134556606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12660 11146 603 41 0 12619 0
vsize: 50640
[startup+290.014 s]
Raw data (loadavg): 0.99 0.61 0.26 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11498 0 0 0 28962 39 0 0 25 0 1 0 487447670 51990528 11166 4294967295 134512640 134672761 3221224576 3221223764 134556588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11166 603 41 0 12652 0
vsize: 50772
[startup+300.015 s]
Raw data (loadavg): 0.99 0.62 0.26 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11498 0 0 0 29962 39 0 0 25 0 1 0 487447670 51990528 11166 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11166 603 41 0 12652 0
vsize: 50772
[startup+310.018 s]
Raw data (loadavg): 0.99 0.64 0.27 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11501 0 0 0 30963 39 0 0 25 0 1 0 487447670 51990528 11169 4294967295 134512640 134672761 3221224576 3221223792 134561999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11169 603 41 0 12652 0
vsize: 50772
[startup+320.018 s]
Raw data (loadavg): 0.99 0.65 0.28 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11501 0 0 0 31963 39 0 0 25 0 1 0 487447670 51990528 11169 4294967295 134512640 134672761 3221224576 3221223748 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11169 603 41 0 12652 0
vsize: 50772
[startup+330.019 s]
Raw data (loadavg): 0.99 0.66 0.29 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11504 0 0 0 32963 39 0 0 25 0 1 0 487447670 51990528 11172 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11172 603 41 0 12652 0
vsize: 50772
[startup+340.019 s]
Raw data (loadavg): 0.99 0.67 0.29 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11506 0 0 0 33963 39 0 0 25 0 1 0 487447670 51990528 11174 4294967295 134512640 134672761 3221224576 3221223744 134564496 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11174 603 41 0 12652 0
vsize: 50772
[startup+350.019 s]
Raw data (loadavg): 0.99 0.68 0.30 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11507 0 0 0 34963 39 0 0 25 0 1 0 487447670 51990528 11175 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11175 603 41 0 12652 0
vsize: 50772
[startup+360.019 s]
Raw data (loadavg): 0.99 0.69 0.31 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11510 0 0 0 35964 39 0 0 25 0 1 0 487447670 51990528 11178 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11178 603 41 0 12652 0
vsize: 50772
[startup+370.019 s]
Raw data (loadavg): 0.99 0.70 0.31 2/55 2285
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11511 0 0 0 36964 39 0 0 25 0 1 0 487447670 51990528 11179 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11179 603 41 0 12652 0
vsize: 50772
[startup+380.02 s]
Raw data (loadavg): 0.99 0.71 0.32 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11512 0 0 0 37964 39 0 0 25 0 1 0 487447670 51990528 11180 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11180 603 41 0 12652 0
vsize: 50772
[startup+390.02 s]
Raw data (loadavg): 0.99 0.72 0.33 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11514 0 0 0 38964 39 0 0 25 0 1 0 487447670 51990528 11182 4294967295 134512640 134672761 3221224576 3221223748 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12693 11182 603 41 0 12652 0
vsize: 50772
[startup+400.021 s]
Raw data (loadavg): 0.99 0.73 0.33 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11519 0 0 0 39963 39 0 0 25 0 1 0 487447670 51990528 11187 4294967295 134512640 134672761 3221224576 3221223808 134564429 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12693 11187 603 41 0 12652 0
vsize: 50772
[startup+410.022 s]
Raw data (loadavg): 0.99 0.74 0.34 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11521 0 0 0 40963 39 0 0 25 0 1 0 487447670 51990528 11189 4294967295 134512640 134672761 3221224576 3221223776 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11189 603 41 0 12652 0
vsize: 50772
[startup+420.021 s]
Raw data (loadavg): 0.99 0.74 0.35 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11524 0 0 0 41963 39 0 0 25 0 1 0 487447670 51990528 11192 4294967295 134512640 134672761 3221224576 3221223700 134566065 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11192 603 41 0 12652 0
vsize: 50772
[startup+430.023 s]
Raw data (loadavg): 0.99 0.75 0.35 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11529 0 0 0 42964 39 0 0 25 0 1 0 487447670 51990528 11197 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11197 603 41 0 12652 0
vsize: 50772
[startup+440.022 s]
Raw data (loadavg): 0.99 0.76 0.36 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11529 0 0 0 43964 39 0 0 25 0 1 0 487447670 51990528 11197 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11197 603 41 0 12652 0
vsize: 50772
[startup+450.022 s]
Raw data (loadavg): 0.99 0.77 0.37 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11532 0 0 0 44964 39 0 0 25 0 1 0 487447670 51990528 11200 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11200 603 41 0 12652 0
vsize: 50772
[startup+460.023 s]
Raw data (loadavg): 0.99 0.77 0.37 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11537 0 0 0 45964 39 0 0 25 0 1 0 487447670 51990528 11205 4294967295 134512640 134672761 3221224576 3221223776 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11205 603 41 0 12652 0
vsize: 50772
[startup+470.023 s]
Raw data (loadavg): 0.99 0.78 0.38 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11540 0 0 0 46964 39 0 0 25 0 1 0 487447670 51990528 11208 4294967295 134512640 134672761 3221224576 3221223740 134561028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11208 603 41 0 12652 0
vsize: 50772
[startup+480.023 s]
Raw data (loadavg): 0.99 0.79 0.38 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11540 0 0 0 47965 39 0 0 25 0 1 0 487447670 51990528 11208 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11208 603 41 0 12652 0
vsize: 50772
[startup+490.023 s]
Raw data (loadavg): 0.99 0.79 0.39 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11541 0 0 0 48965 39 0 0 25 0 1 0 487447670 51990528 11209 4294967295 134512640 134672761 3221224576 3221223748 134556669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11209 603 41 0 12652 0
vsize: 50772
[startup+500.024 s]
Raw data (loadavg): 0.99 0.80 0.40 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11543 0 0 0 49965 39 0 0 25 0 1 0 487447670 51990528 11211 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11211 603 41 0 12652 0
vsize: 50772
[startup+510.024 s]
Raw data (loadavg): 0.99 0.81 0.40 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11544 0 0 0 50965 39 0 0 25 0 1 0 487447670 51990528 11212 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11212 603 41 0 12652 0
vsize: 50772
[startup+520.024 s]
Raw data (loadavg): 0.99 0.81 0.41 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11549 0 0 0 51965 39 0 0 25 0 1 0 487447670 51990528 11217 4294967295 134512640 134672761 3221224576 3221223700 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11217 603 41 0 12652 0
vsize: 50772
[startup+530.024 s]
Raw data (loadavg): 0.99 0.82 0.41 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11549 0 0 0 52965 39 0 0 25 0 1 0 487447670 51990528 11217 4294967295 134512640 134672761 3221224576 3221223748 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11217 603 41 0 12652 0
vsize: 50772
[startup+540.024 s]
Raw data (loadavg): 0.99 0.82 0.42 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11551 0 0 0 53966 39 0 0 25 0 1 0 487447670 51990528 11219 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11219 603 41 0 12652 0
vsize: 50772
[startup+550.024 s]
Raw data (loadavg): 0.99 0.83 0.43 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11555 0 0 0 54966 39 0 0 25 0 1 0 487447670 51990528 11223 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11223 603 41 0 12652 0
vsize: 50772
[startup+560.025 s]
Raw data (loadavg): 0.99 0.83 0.43 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11555 0 0 0 55966 39 0 0 25 0 1 0 487447670 51990528 11223 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11223 603 41 0 12652 0
vsize: 50772
[startup+570.025 s]
Raw data (loadavg): 0.99 0.84 0.44 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11555 0 0 0 56966 39 0 0 25 0 1 0 487447670 51990528 11223 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11223 603 41 0 12652 0
vsize: 50772
[startup+580.026 s]
Raw data (loadavg): 0.99 0.84 0.44 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11555 0 0 0 57966 39 0 0 25 0 1 0 487447670 51990528 11223 4294967295 134512640 134672761 3221224576 3221223748 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11223 603 41 0 12652 0
vsize: 50772
[startup+590.026 s]
Raw data (loadavg): 0.99 0.85 0.45 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11556 0 0 0 58967 39 0 0 25 0 1 0 487447670 51990528 11224 4294967295 134512640 134672761 3221224576 3221223744 134564772 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11224 603 41 0 12652 0
vsize: 50772
[startup+600.027 s]
Raw data (loadavg): 0.99 0.85 0.45 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11557 0 0 0 59967 39 0 0 25 0 1 0 487447670 51990528 11225 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11225 603 41 0 12652 0
vsize: 50772
[startup+610.027 s]
Raw data (loadavg): 0.99 0.86 0.46 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11557 0 0 0 60967 39 0 0 25 0 1 0 487447670 51990528 11225 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11225 603 41 0 12652 0
vsize: 50772
[startup+620.027 s]
Raw data (loadavg): 0.99 0.86 0.46 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11557 0 0 0 61967 39 0 0 25 0 1 0 487447670 51990528 11225 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11225 603 41 0 12652 0
vsize: 50772
[startup+630.028 s]
Raw data (loadavg): 0.99 0.86 0.47 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11557 0 0 0 62967 39 0 0 25 0 1 0 487447670 51990528 11225 4294967295 134512640 134672761 3221224576 3221223748 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11225 603 41 0 12652 0
vsize: 50772
[startup+640.028 s]
Raw data (loadavg): 0.99 0.87 0.47 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11558 0 0 0 63967 39 0 0 25 0 1 0 487447670 51990528 11226 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11226 603 41 0 12652 0
vsize: 50772
[startup+650.028 s]
Raw data (loadavg): 0.99 0.87 0.48 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11559 0 0 0 64967 40 0 0 25 0 1 0 487447670 51990528 11227 4294967295 134512640 134672761 3221224576 3221223836 134562226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12693 11227 603 41 0 12652 0
vsize: 50772
[startup+660.028 s]
Raw data (loadavg): 0.99 0.88 0.48 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11559 0 0 0 65966 40 0 0 25 0 1 0 487447670 51990528 11227 4294967295 134512640 134672761 3221224576 3221223720 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11227 603 41 0 12652 0
vsize: 50772
[startup+670.028 s]
Raw data (loadavg): 0.99 0.88 0.49 2/55 2287
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11560 0 0 0 66966 40 0 0 25 0 1 0 487447670 51990528 11228 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11228 603 41 0 12652 0
vsize: 50772
[startup+680.029 s]
Raw data (loadavg): 0.99 0.88 0.49 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11560 0 0 0 67966 40 0 0 25 0 1 0 487447670 51990528 11228 4294967295 134512640 134672761 3221224576 3221223748 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11228 603 41 0 12652 0
vsize: 50772
[startup+690.029 s]
Raw data (loadavg): 0.99 0.89 0.50 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11560 0 0 0 68966 40 0 0 25 0 1 0 487447670 51990528 11228 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11228 603 41 0 12652 0
vsize: 50772
[startup+700.03 s]
Raw data (loadavg): 0.99 0.89 0.50 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11560 0 0 0 69967 40 0 0 25 0 1 0 487447670 51990528 11228 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12693 11228 603 41 0 12652 0
vsize: 50772
[startup+710.03 s]
Raw data (loadavg): 0.99 0.89 0.51 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11570 0 0 0 70967 40 0 0 25 0 1 0 487447670 52129792 11238 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11238 603 41 0 12686 0
vsize: 50908
[startup+720.03 s]
Raw data (loadavg): 0.99 0.90 0.51 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11570 0 0 0 71967 40 0 0 25 0 1 0 487447670 52129792 11238 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11238 603 41 0 12686 0
vsize: 50908
[startup+730.03 s]
Raw data (loadavg): 0.99 0.90 0.52 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11570 0 0 0 72967 40 0 0 25 0 1 0 487447670 52129792 11238 4294967295 134512640 134672761 3221224576 3221223744 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11238 603 41 0 12686 0
vsize: 50908
[startup+740.03 s]
Raw data (loadavg): 0.99 0.90 0.52 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11570 0 0 0 73967 40 0 0 25 0 1 0 487447670 52129792 11238 4294967295 134512640 134672761 3221224576 3221223700 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11238 603 41 0 12686 0
vsize: 50908
[startup+750.031 s]
Raw data (loadavg): 0.99 0.90 0.53 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11571 0 0 0 74967 40 0 0 25 0 1 0 487447670 52129792 11239 4294967295 134512640 134672761 3221224576 3221223772 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11239 603 41 0 12686 0
vsize: 50908
[startup+760.031 s]
Raw data (loadavg): 0.99 0.91 0.53 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11571 0 0 0 75968 40 0 0 25 0 1 0 487447670 52129792 11239 4294967295 134512640 134672761 3221224576 3221223700 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11239 603 41 0 12686 0
vsize: 50908
[startup+770.03 s]
Raw data (loadavg): 0.99 0.91 0.54 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11571 0 0 0 76968 40 0 0 25 0 1 0 487447670 52129792 11239 4294967295 134512640 134672761 3221224576 3221223700 134566052 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11239 603 41 0 12686 0
vsize: 50908
[startup+780.03 s]
Raw data (loadavg): 0.99 0.91 0.54 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11571 0 0 0 77968 40 0 0 25 0 1 0 487447670 52129792 11239 4294967295 134512640 134672761 3221224576 3221223700 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11239 603 41 0 12686 0
vsize: 50908
[startup+790.03 s]
Raw data (loadavg): 0.99 0.91 0.55 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11571 0 0 0 78968 40 0 0 25 0 1 0 487447670 52129792 11239 4294967295 134512640 134672761 3221224576 3221223748 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11239 603 41 0 12686 0
vsize: 50908
[startup+800.031 s]
Raw data (loadavg): 0.99 0.92 0.55 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11572 0 0 0 79968 40 0 0 25 0 1 0 487447670 52129792 11240 4294967295 134512640 134672761 3221224576 3221223760 134556589 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11240 603 41 0 12686 0
vsize: 50908
[startup+810.031 s]
Raw data (loadavg): 0.99 0.92 0.56 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11572 0 0 0 80968 40 0 0 25 0 1 0 487447670 52129792 11240 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11240 603 41 0 12686 0
vsize: 50908
[startup+820.031 s]
Raw data (loadavg): 0.99 0.92 0.56 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11572 0 0 0 81969 40 0 0 25 0 1 0 487447670 52129792 11240 4294967295 134512640 134672761 3221224576 3221223776 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11240 603 41 0 12686 0
vsize: 50908
[startup+830.032 s]
Raw data (loadavg): 0.99 0.92 0.56 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11572 0 0 0 82969 40 0 0 25 0 1 0 487447670 52129792 11240 4294967295 134512640 134672761 3221224576 3221223792 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11240 603 41 0 12686 0
vsize: 50908
[startup+840.032 s]
Raw data (loadavg): 0.99 0.92 0.57 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11572 0 0 0 83969 40 0 0 25 0 1 0 487447670 52129792 11240 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11240 603 41 0 12686 0
vsize: 50908
[startup+850.033 s]
Raw data (loadavg): 0.99 0.93 0.57 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11572 0 0 0 84969 40 0 0 25 0 1 0 487447670 52129792 11240 4294967295 134512640 134672761 3221224576 3221223700 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11240 603 41 0 12686 0
vsize: 50908
[startup+860.032 s]
Raw data (loadavg): 0.99 0.93 0.58 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11573 0 0 0 85969 40 0 0 25 0 1 0 487447670 52129792 11241 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11241 603 41 0 12686 0
vsize: 50908
[startup+870.033 s]
Raw data (loadavg): 0.99 0.93 0.58 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11573 0 0 0 86969 40 0 0 25 0 1 0 487447670 52129792 11241 4294967295 134512640 134672761 3221224576 3221223700 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11241 603 41 0 12686 0
vsize: 50908
[startup+880.033 s]
Raw data (loadavg): 0.99 0.93 0.58 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11573 0 0 0 87969 40 0 0 25 0 1 0 487447670 52129792 11241 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11241 603 41 0 12686 0
vsize: 50908
[startup+890.033 s]
Raw data (loadavg): 0.99 0.93 0.59 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11573 0 0 0 88969 40 0 0 25 0 1 0 487447670 52129792 11241 4294967295 134512640 134672761 3221224576 3221223748 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11241 603 41 0 12686 0
vsize: 50908
[startup+900.033 s]
Raw data (loadavg): 0.99 0.94 0.59 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11573 0 0 0 89970 40 0 0 25 0 1 0 487447670 52129792 11241 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11241 603 41 0 12686 0
vsize: 50908
[startup+910.033 s]
Raw data (loadavg): 0.99 0.94 0.59 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11574 0 0 0 90970 40 0 0 25 0 1 0 487447670 52129792 11242 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11242 603 41 0 12686 0
vsize: 50908
[startup+920.033 s]
Raw data (loadavg): 0.99 0.94 0.60 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11574 0 0 0 91970 40 0 0 25 0 1 0 487447670 52129792 11242 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11242 603 41 0 12686 0
vsize: 50908
[startup+930.033 s]
Raw data (loadavg): 0.99 0.94 0.60 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11574 0 0 0 92970 40 0 0 25 0 1 0 487447670 52129792 11242 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11242 603 41 0 12686 0
vsize: 50908
[startup+940.034 s]
Raw data (loadavg): 0.99 0.94 0.61 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11574 0 0 0 93970 40 0 0 25 0 1 0 487447670 52129792 11242 4294967295 134512640 134672761 3221224576 3221223700 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11242 603 41 0 12686 0
vsize: 50908
[startup+950.035 s]
Raw data (loadavg): 0.99 0.94 0.61 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11574 0 0 0 94971 40 0 0 25 0 1 0 487447670 52129792 11242 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11242 603 41 0 12686 0
vsize: 50908
[startup+960.034 s]
Raw data (loadavg): 0.99 0.94 0.61 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11576 0 0 0 95971 40 0 0 25 0 1 0 487447670 52129792 11244 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11244 603 41 0 12686 0
vsize: 50908
[startup+970.035 s]
Raw data (loadavg): 0.99 0.95 0.62 2/55 2289
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11576 0 0 0 96971 40 0 0 25 0 1 0 487447670 52129792 11244 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11244 603 41 0 12686 0
vsize: 50908
[startup+980.036 s]
Raw data (loadavg): 0.99 0.95 0.62 2/55 2291
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11576 0 0 0 97971 40 0 0 25 0 1 0 487447670 52129792 11244 4294967295 134512640 134672761 3221224576 3221223792 134561999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11244 603 41 0 12686 0
vsize: 50908
[startup+990.035 s]
Raw data (loadavg): 0.99 0.95 0.63 2/55 2291
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11576 0 0 0 98971 40 0 0 25 0 1 0 487447670 52129792 11244 4294967295 134512640 134672761 3221224576 3221223748 134556669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11244 603 41 0 12686 0
vsize: 50908
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.95 0.63 2/55 2291
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11576 0 0 0 99972 40 0 0 25 0 1 0 487447670 52129792 11244 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11244 603 41 0 12686 0
vsize: 50908
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.95 0.63 2/55 2291
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11576 0 0 0 100972 40 0 0 25 0 1 0 487447670 52129792 11244 4294967295 134512640 134672761 3221224576 3221223760 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11244 603 41 0 12686 0
vsize: 50908
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.95 0.64 2/55 2291
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11576 0 0 0 101972 40 0 0 25 0 1 0 487447670 52129792 11244 4294967295 134512640 134672761 3221224576 3221223780 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11244 603 41 0 12686 0
vsize: 50908
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.95 0.64 2/55 2291
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11577 0 0 0 102972 40 0 0 25 0 1 0 487447670 52129792 11245 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11245 603 41 0 12686 0
vsize: 50908
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.95 0.64 2/55 2291
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11577 0 0 0 103972 40 0 0 25 0 1 0 487447670 52129792 11245 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11245 603 41 0 12686 0
vsize: 50908
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.95 0.65 2/55 2291
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11577 0 0 0 104973 40 0 0 25 0 1 0 487447670 52129792 11245 4294967295 134512640 134672761 3221224576 3221223744 134564738 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11245 603 41 0 12686 0
vsize: 50908
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.95 0.65 2/55 2291
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11577 0 0 0 105973 40 0 0 25 0 1 0 487447670 52129792 11245 4294967295 134512640 134672761 3221224576 3221223700 134566068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11245 603 41 0 12686 0
vsize: 50908
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.96 0.65 2/55 2291
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11577 0 0 0 106973 40 0 0 25 0 1 0 487447670 52129792 11245 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11245 603 41 0 12686 0
vsize: 50908
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.96 0.66 2/55 2291
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11577 0 0 0 107973 40 0 0 25 0 1 0 487447670 52129792 11245 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11245 603 41 0 12686 0
vsize: 50908
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.96 0.66 2/55 2291
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11577 0 0 0 108973 40 0 0 25 0 1 0 487447670 52129792 11245 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11245 603 41 0 12686 0
vsize: 50908
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.96 0.66 2/55 2291
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11577 0 0 0 109973 40 0 0 25 0 1 0 487447670 52129792 11245 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11245 603 41 0 12686 0
vsize: 50908
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.96 0.66 2/55 2291
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11578 0 0 0 110974 40 0 0 25 0 1 0 487447670 52129792 11246 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12727 11246 603 41 0 12686 0
vsize: 50908
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.96 0.67 2/55 2291
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11595 0 0 0 111974 40 0 0 25 0 1 0 487447670 52264960 11263 4294967295 134512640 134672761 3221224576 3221223748 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12760 11263 603 41 0 12719 0
vsize: 51040
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.96 0.67 2/55 2291
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11596 0 0 0 112974 40 0 0 25 0 1 0 487447670 52264960 11264 4294967295 134512640 134672761 3221224576 3221223748 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12760 11264 603 41 0 12719 0
vsize: 51040
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.96 0.67 2/55 2291
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11596 0 0 0 113974 40 0 0 25 0 1 0 487447670 52264960 11264 4294967295 134512640 134672761 3221224576 3221223748 134556685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12760 11264 603 41 0 12719 0
vsize: 51040
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.96 0.68 2/55 2291
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11596 0 0 0 114974 40 0 0 25 0 1 0 487447670 52264960 11264 4294967295 134512640 134672761 3221224576 3221223792 134561993 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12760 11264 603 41 0 12719 0
vsize: 51040
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.96 0.68 2/55 2291
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11596 0 0 0 115973 41 0 0 25 0 1 0 487447670 52264960 11264 4294967295 134512640 134672761 3221224576 3221223748 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12760 11264 603 41 0 12719 0
vsize: 51040
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.68 2/55 2291
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11596 0 0 0 116973 41 0 0 25 0 1 0 487447670 52264960 11264 4294967295 134512640 134672761 3221224576 3221223748 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12760 11264 603 41 0 12719 0
vsize: 51040
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.68 2/55 2291
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11598 0 0 0 117974 41 0 0 25 0 1 0 487447670 52264960 11266 4294967295 134512640 134672761 3221224576 3221223772 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12760 11266 603 41 0 12719 0
vsize: 51040
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.69 2/55 2291
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11601 0 0 0 118974 41 0 0 25 0 1 0 487447670 52264960 11269 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12760 11269 603 41 0 12719 0
vsize: 51040
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.69 2/55 2291
Raw data (stat): 2283 (minisat+) R 2282 20024 20023 0 -1 0 11601 0 0 0 119974 41 0 0 25 0 1 0 487447670 52264960 11269 4294967295 134512640 134672761 3221224576 3221223744 134564636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12760 11269 603 41 0 12719 0
vsize: 51040
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.69 1/55 2291
Raw data (stat): 2283 (minisat+) Z 2282 20024 20023 0 -1 12 11603 0 0 0 119974 43 0 0 25 0 1 0 487447670 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.07
CPU time (s): 1200.18
CPU user time (s): 1199.75
CPU system time (s): 0.431934
CPU usage (%): 100.009
Max. virtual memory (Kb): 51040
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####