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/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-tr12-30.opb
MD5SUM	2d8f46b77d84c45a7178d4a463744176
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
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	7560
Biggest coefficient in the objective function	2097152
Number of bits for the biggest coefficient in the objective function	22
Sum of the numbers in the objective function	876993750
Number of bits of the sum of numbers in the objective function	30
Biggest number in a constraint	2097152
Number of bits of the biggest number in a constraint	22
Biggest sum of numbers in a constraint	876993750
Number of bits of the biggest sum of numbers	30
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.128979
Number of variables	14760
Total number of constraints	1110
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	360
Number of constraints which are nor clauses,nor cardinality constraints	750
Minimum length of a constraint	1
Maximum length of a constraint	252
Trace number 15269

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-04-21 03:38:53 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18108 boxname=wulflinc29 idbench=1393 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  2d8f46b77d84c45a7178d4a463744176  /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-tr12-30.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-tr12-30.opb /oldhome/oroussel/tmp/wulflinc29/normalized-mps-v2-13-7-tr12-30.opb
IDLAUNCH: 18108
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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.020
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:        853492 kB
Buffers:         12516 kB
Cached:         140836 kB
SwapCached:        464 kB
Active:          44068 kB
Inactive:       111472 kB
HighTotal:      131008 kB
HighFree:          532 kB
LowTotal:       903652 kB
LowFree:        852960 kB
SwapTotal:     2097892 kB
SwapFree:      2096700 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5296 kB
Slab:            20176 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 03:58:55 (client local time) WITH STATUS 0 IN 1200.47 SECONDS
stats: 18108 7 1200.47 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1110 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1108]---> BDD-cost:   71
c ---[1106]---> BDD-cost:  196
c ---[1104]---> BDD-cost:  193
c ---[1102]---> BDD-cost:  199
c ---[1100]---> BDD-cost:  193
c ---[1098]---> BDD-cost:  199
c ---[1096]---> BDD-cost:  193
c ---[1094]---> BDD-cost:  187
c ---[1092]---> BDD-cost:  190
c ---[1090]---> BDD-cost:  199
c ---[1088]---> BDD-cost:  199
c ---[1086]---> BDD-cost:  187
c ---[1084]---> BDD-cost:  196
c ---[1082]---> BDD-cost:  199
c ---[1080]---> BDD-cost:  193
c ---[1078]---> BDD-cost:  196
c ---[1076]---> BDD-cost:  199
c ---[1074]---> BDD-cost:  199
c ---[1072]---> BDD-cost:  199
c ---[1070]---> BDD-cost:  199
c ---[1068]---> BDD-cost:  196
c ---[1066]---> BDD-cost:  199
c ---[1064]---> BDD-cost:  193
c ---[1062]---> BDD-cost:  190
c ---[1060]---> BDD-cost:  199
c ---[1058]---> BDD-cost:   52
c ---[1056]---> BDD-cost:  185
c ---[1054]---> BDD-cost:  195
c ---[1052]---> BDD-cost:  193
c ---[1050]---> BDD-cost:  193
c ---[1048]---> BDD-cost:  199
c ---[1046]---> BDD-cost:  193
c ---[1044]---> BDD-cost:  196
c ---[1042]---> BDD-cost:  193
c ---[1040]---> BDD-cost:  199
c ---[1038]---> BDD-cost:  199
c ---[1036]---> BDD-cost:  199
c ---[1034]---> BDD-cost:  199
c ---[1032]---> BDD-cost:  199
c ---[1030]---> BDD-cost:  199
c ---[1028]---> BDD-cost:  199
c ---[1026]---> BDD-cost:  196
c ---[1024]---> BDD-cost:  193
c ---[1022]---> BDD-cost:  196
c ---[1020]---> BDD-cost:  199
c ---[1018]---> BDD-cost:  199
c ---[1016]---> BDD-cost:  199
c ---[1014]---> BDD-cost:  199
c ---[1012]---> BDD-cost:  199
c ---[1010]---> BDD-cost:  199
c ---[1008]---> BDD-cost:  196
c ---[1006]---> BDD-cost:  199
c ---[1004]---> BDD-cost:  199
c ---[1002]---> BDD-cost:  199
c ---[1000]---> BDD-cost:  199
c ---[ 998]---> BDD-cost:  199
c ---[ 996]---> BDD-cost:  190
c ---[ 994]---> BDD-cost:  199
c ---[ 992]---> BDD-cost:   65
c ---[ 990]---> BDD-cost:  185
c ---[ 988]---> BDD-cost:  195
c ---[ 986]---> BDD-cost:  166
c ---[ 984]---> BDD-cost:  196
c ---[ 982]---> BDD-cost:  196
c ---[ 980]---> BDD-cost:  193
c ---[ 978]---> BDD-cost:  199
c ---[ 976]---> BDD-cost:  196
c ---[ 974]---> BDD-cost:  199
c ---[ 972]---> BDD-cost:  199
c ---[ 970]---> BDD-cost:  193
c ---[ 968]---> BDD-cost:  199
c ---[ 966]---> BDD-cost:  196
c ---[ 964]---> BDD-cost:  196
c ---[ 962]---> BDD-cost:  193
c ---[ 960]---> BDD-cost:  199
c ---[ 958]---> BDD-cost:  199
c ---[ 956]---> BDD-cost:  196
c ---[ 954]---> BDD-cost:  199
c ---[ 952]---> BDD-cost:  193
c ---[ 950]---> BDD-cost:  190
c ---[ 948]---> BDD-cost:  199
c ---[ 946]---> BDD-cost:  199
c ---[ 944]---> BDD-cost:  196
c ---[ 942]---> BDD-cost:  199
c ---[ 940]---> BDD-cost:  199
c ---[ 938]---> BDD-cost:  193
c ---[ 936]---> BDD-cost:  193
c ---[ 934]---> BDD-cost:  196
c ---[ 932]---> BDD-cost:  199
c ---[ 930]---> BDD-cost:  196
c ---[ 928]---> BDD-cost:  199
c ---[ 926]---> BDD-cost:   67
c ---[ 924]---> BDD-cost:  179
c ---[ 922]---> BDD-cost:  195
c ---[ 920]---> BDD-cost:  166
c ---[ 918]---> BDD-cost:  193
c ---[ 916]---> BDD-cost:  199
c ---[ 914]---> BDD-cost:  199
c ---[ 912]---> BDD-cost:  199
c ---[ 910]---> BDD-cost:  199
c ---[ 908]---> BDD-cost:  196
c ---[ 906]---> BDD-cost:  184
c ---[ 904]---> BDD-cost:  199
c ---[ 902]---> BDD-cost:  199
c ---[ 900]---> BDD-cost:  196
c ---[ 898]---> BDD-cost:  193
c ---[ 896]---> BDD-cost:  196
c ---[ 894]---> BDD-cost:  199
c ---[ 892]---> BDD-cost:  193
c ---[ 890]---> BDD-cost:  184
c ---[ 888]---> BDD-cost:  199
c ---[ 886]---> BDD-cost:  159
c ---[ 884]---> BDD-cost:  190
c ---[ 882]---> BDD-cost:  196
c ---[ 880]---> BDD-cost:  196
c ---[ 878]---> BDD-cost:  196
c ---[ 876]---> BDD-cost:  196
c ---[ 874]---> BDD-cost:  199
c ---[ 872]---> BDD-cost:  196
c ---[ 870]---> BDD-cost:  199
c ---[ 868]---> BDD-cost:  196
c ---[ 866]---> BDD-cost:  199
c ---[ 864]---> BDD-cost:  199
c ---[ 862]---> BDD-cost:  199
c ---[ 860]---> BDD-cost:  196
c ---[ 858]---> BDD-cost:   63
c ---[ 856]---> BDD-cost:  173
c ---[ 854]---> BDD-cost:  195
c ---[ 852]---> BDD-cost:  166
c ---[ 850]---> BDD-cost:  193
c ---[ 848]---> BDD-cost:  199
c ---[ 846]---> BDD-cost:  196
c ---[ 844]---> BDD-cost:  196
c ---[ 842]---> BDD-cost:  196
c ---[ 840]---> BDD-cost:  196
c ---[ 838]---> BDD-cost:  199
c ---[ 836]---> BDD-cost:  196
c ---[ 834]---> BDD-cost:  199
c ---[ 832]---> BDD-cost:  193
c ---[ 830]---> BDD-cost:  193
c ---[ 828]---> BDD-cost:  193
c ---[ 826]---> BDD-cost:  196
c ---[ 824]---> BDD-cost:  199
c ---[ 822]---> BDD-cost:  199
c ---[ 820]---> BDD-cost:  196
c ---[ 818]---> BDD-cost:  193
c ---[ 816]---> BDD-cost:  199
c ---[ 814]---> BDD-cost:  199
c ---[ 812]---> BDD-cost:  199
c ---[ 810]---> BDD-cost:  199
c ---[ 808]---> BDD-cost:  190
c ---[ 806]---> BDD-cost:  199
c ---[ 804]---> BDD-cost:  196
c ---[ 802]---> BDD-cost:  199
c ---[ 800]---> BDD-cost:  196
c ---[ 798]---> BDD-cost:  196
c ---[ 796]---> BDD-cost:  196
c ---[ 794]---> BDD-cost:  196
c ---[ 792]---> BDD-cost:   71
c ---[ 790]---> BDD-cost:  159
c ---[ 788]---> BDD-cost:  192
c ---[ 786]---> BDD-cost:  193
c ---[ 784]---> BDD-cost:  199
c ---[ 782]---> BDD-cost:  199
c ---[ 780]---> BDD-cost:  187
c ---[ 778]---> BDD-cost:  199
c ---[ 776]---> BDD-cost:  187
c ---[ 774]---> BDD-cost:  193
c ---[ 772]---> BDD-cost:  199
c ---[ 770]---> BDD-cost:  199
c ---[ 768]---> BDD-cost:  196
c ---[ 766]---> BDD-cost:  199
c ---[ 764]---> BDD-cost:  193
c ---[ 762]---> BDD-cost:  196
c ---[ 760]---> BDD-cost:  196
c ---[ 758]---> BDD-cost:  199
c ---[ 756]---> BDD-cost:  199
c ---[ 754]---> BDD-cost:  199
c ---[ 752]---> BDD-cost:  196
c ---[ 750]---> BDD-cost:  199
c ---[ 748]---> BDD-cost:  196
c ---[ 746]---> BDD-cost:  199
c ---[ 744]---> BDD-cost:  187
c ---[ 742]---> BDD-cost:  196
c ---[ 740]---> BDD-cost:  199
c ---[ 738]---> BDD-cost:  196
c ---[ 736]---> BDD-cost:  199
c ---[ 734]---> BDD-cost:  199
c ---[ 732]---> BDD-cost:  196
c ---[ 730]---> BDD-cost:  190
c ---[ 728]---> BDD-cost:  193
c ---[ 726]---> BDD-cost:   52
c ---[ 724]---> BDD-cost:  179
c ---[ 722]---> BDD-cost:  164
c ---[ 720]---> BDD-cost:  199
c ---[ 718]---> BDD-cost:  199
c ---[ 716]---> BDD-cost:  199
c ---[ 714]---> BDD-cost:  193
c ---[ 712]---> BDD-cost:  199
c ---[ 710]---> BDD-cost:  199
c ---[ 708]---> BDD-cost:  199
c ---[ 706]---> BDD-cost:  199
c ---[ 704]---> BDD-cost:  190
c ---[ 702]---> BDD-cost:  193
c ---[ 700]---> BDD-cost:  199
c ---[ 698]---> BDD-cost:  199
c ---[ 696]---> BDD-cost:  196
c ---[ 694]---> BDD-cost:  199
c ---[ 692]---> BDD-cost:  199
c ---[ 690]---> BDD-cost:  199
c ---[ 688]---> BDD-cost:  187
c ---[ 686]---> BDD-cost:  196
c ---[ 684]---> BDD-cost:  199
c ---[ 682]---> BDD-cost:  199
c ---[ 680]---> BDD-cost:  190
c ---[ 678]---> BDD-cost:  199
c ---[ 676]---> BDD-cost:  199
c ---[ 674]---> BDD-cost:  199
c ---[ 672]---> BDD-cost:  187
c ---[ 670]---> BDD-cost:  196
c ---[ 668]---> BDD-cost:  193
c ---[ 666]---> BDD-cost:  196
c ---[ 664]---> BDD-cost:  189
c ---[ 662]---> BDD-cost:  199
c ---[ 660]---> BDD-cost:  199
c ---[ 658]---> BDD-cost:   71
c ---[ 656]---> BDD-cost:  182
c ---[ 654]---> BDD-cost:  192
c ---[ 652]---> BDD-cost:  196
c ---[ 650]---> BDD-cost:  199
c ---[ 648]---> BDD-cost:  196
c ---[ 646]---> BDD-cost:  196
c ---[ 644]---> BDD-cost:  184
c ---[ 642]---> BDD-cost:  199
c ---[ 640]---> BDD-cost:   67
c ---[ 638]---> BDD-cost:  196
c ---[ 636]---> BDD-cost:  196
c ---[ 634]---> BDD-cost:  199
c ---[ 632]---> BDD-cost:  199
c ---[ 630]---> BDD-cost:  196
c ---[ 628]---> BDD-cost:  199
c ---[ 626]---> BDD-cost:  196
c ---[ 624]---> BDD-cost:  184
c ---[ 622]---> BDD-cost:  199
c ---[ 620]---> BDD-cost:  199
c ---[ 618]---> BDD-cost:  185
c ---[ 616]---> BDD-cost:  199
c ---[ 614]---> BDD-cost:  196
c ---[ 612]---> BDD-cost:  193
c ---[ 610]---> BDD-cost:  199
c ---[ 608]---> BDD-cost:  199
c ---[ 606]---> BDD-cost:  193
c ---[ 604]---> BDD-cost:  187
c ---[ 602]---> BDD-cost:  199
c ---[ 600]---> BDD-cost:  199
c ---[ 598]---> BDD-cost:  199
c ---[ 596]---> BDD-cost:  189
c ---[ 594]---> BDD-cost:  199
c ---[ 592]---> BDD-cost:   52
c ---[ 590]---> BDD-cost:  188
c ---[ 588]---> BDD-cost:  192
c ---[ 586]---> BDD-cost:  166
c ---[ 584]---> BDD-cost:  193
c ---[ 582]---> BDD-cost:  196
c ---[ 580]---> BDD-cost:  199
c ---[ 578]---> BDD-cost:  193
c ---[ 576]---> BDD-cost:  199
c ---[ 574]---> BDD-cost:  199
c ---[ 572]---> BDD-cost:  190
c ---[ 570]---> BDD-cost:  199
c ---[ 568]---> BDD-cost:  199
c ---[ 566]---> BDD-cost:  199
c ---[ 564]---> BDD-cost:  190
c ---[ 562]---> BDD-cost:  184
c ---[ 560]---> BDD-cost:  196
c ---[ 558]---> BDD-cost:  199
c ---[ 556]---> BDD-cost:  184
c ---[ 554]---> BDD-cost:  199
c ---[ 552]---> BDD-cost:  196
c ---[ 550]---> BDD-cost:  199
c ---[ 548]---> BDD-cost:  199
c ---[ 546]---> BDD-cost:  190
c ---[ 544]---> BDD-cost:  199
c ---[ 542]---> BDD-cost:  193
c ---[ 540]---> BDD-cost:  193
c ---[ 538]---> BDD-cost:  199
c ---[ 536]---> BDD-cost:  196
c ---[ 534]---> BDD-cost:  199
c ---[ 532]---> BDD-cost:  199
c ---[ 530]---> BDD-cost:  199
c ---[ 528]---> BDD-cost:  199
c ---[ 527]---> BDD-cost:   28
c ---[ 526]---> BDD-cost:   28
c ---[ 525]---> BDD-cost:   28
c ---[ 524]---> BDD-cost:   28
c ---[ 523]---> BDD-cost:   28
c ---[ 522]---> BDD-cost:   28
c ---[ 521]---> BDD-cost:   28
c ---[ 520]---> BDD-cost:   28
c ---[ 519]---> BDD-cost:   28
c ---[ 517]---> BDD-cost:  196
c ---[ 516]---> BDD-cost:   28
c ---[ 515]---> BDD-cost:   28
c ---[ 514]---> BDD-cost:   28
c ---[ 513]---> BDD-cost:   28
c ---[ 512]---> BDD-cost:   28
c ---[ 511]---> BDD-cost:   28
c ---[ 510]---> BDD-cost:   28
c ---[ 509]---> BDD-cost:   28
c ---[ 508]---> BDD-cost:   28
c ---[ 507]---> BDD-cost:   28
c ---[ 505]---> BDD-cost:  199
c ---[ 504]---> BDD-cost:   28
c ---[ 503]---> BDD-cost:   28
c ---[ 502]---> BDD-cost:   28
c ---[ 501]---> BDD-cost:   28
c ---[ 500]---> BDD-cost:   28
c ---[ 499]---> BDD-cost:   28
c ---[ 498]---> BDD-cost:   28
c ---[ 497]---> BDD-cost:   28
c ---[ 496]---> BDD-cost:   28
c ---[ 495]---> BDD-cost:   28
c ---[ 493]---> BDD-cost:  193
c ---[ 492]---> BDD-cost:   28
c ---[ 491]---> BDD-cost:   27
c ---[ 490]---> BDD-cost:   27
c ---[ 489]---> BDD-cost:   27
c ---[ 488]---> BDD-cost:   27
c ---[ 487]---> BDD-cost:   27
c ---[ 486]---> BDD-cost:   27
c ---[ 485]---> BDD-cost:   27
c ---[ 484]---> BDD-cost:   27
c ---[ 483]---> BDD-cost:   27
c ---[ 481]---> BDD-cost:  199
c ---[ 479]---> BDD-cost:  184
c ---[ 478]---> BDD-cost:   27
c ---[ 477]---> BDD-cost:   27
c ---[ 476]---> BDD-cost:   27
c ---[ 475]---> BDD-cost:   27
c ---[ 474]---> BDD-cost:   27
c ---[ 473]---> BDD-cost:   27
c ---[ 472]---> BDD-cost:   27
c ---[ 471]---> BDD-cost:   27
c ---[ 470]---> BDD-cost:   27
c ---[ 469]---> BDD-cost:   27
c ---[ 467]---> BDD-cost:  196
c ---[ 466]---> BDD-cost:   27
c ---[ 465]---> BDD-cost:   27
c ---[ 464]---> BDD-cost:   27
c ---[ 463]---> BDD-cost:   27
c ---[ 462]---> BDD-cost:   27
c ---[ 461]---> BDD-cost:   27
c ---[ 460]---> BDD-cost:   27
c ---[ 459]---> BDD-cost:   27
c ---[ 458]---> BDD-cost:   27
c ---[ 457]---> BDD-cost:   27
c ---[ 455]---> BDD-cost:  199
c ---[ 454]---> BDD-cost:   27
c ---[ 453]---> BDD-cost:   25
c ---[ 452]---> BDD-cost:   25
c ---[ 451]---> BDD-cost:   25
c ---[ 450]---> BDD-cost:   25
c ---[ 449]---> BDD-cost:   25
c ---[ 448]---> BDD-cost:   25
c ---[ 447]---> BDD-cost:   25
c ---[ 446]---> BDD-cost:   25
c ---[ 445]---> BDD-cost:   25
c ---[ 443]---> BDD-cost:  187
c ---[ 442]---> BDD-cost:   25
c ---[ 441]---> BDD-cost:   25
c ---[ 440]---> BDD-cost:   25
c ---[ 439]---> BDD-cost:   25
c ---[ 438]---> BDD-cost:   25
c ---[ 437]---> BDD-cost:   25
c ---[ 436]---> BDD-cost:   25
c ---[ 435]---> BDD-cost:   25
c ---[ 434]---> BDD-cost:   25
c ---[ 433]---> BDD-cost:   25
c ---[ 431]---> BDD-cost:  199
c ---[ 430]---> BDD-cost:   25
c ---[ 429]---> BDD-cost:   25
c ---[ 428]---> BDD-cost:   25
c ---[ 427]---> BDD-cost:   25
c ---[ 426]---> BDD-cost:   25
c ---[ 425]---> BDD-cost:   25
c ---[ 424]---> BDD-cost:   25
c ---[ 423]---> BDD-cost:   25
c ---[ 422]---> BDD-cost:   25
c ---[ 421]---> BDD-cost:   25
c ---[ 419]---> BDD-cost:  199
c ---[ 418]---> BDD-cost:   25
c ---[ 417]---> BDD-cost:   28
c ---[ 416]---> BDD-cost:   28
c ---[ 415]---> BDD-cost:   28
c ---[ 414]---> BDD-cost:   28
c ---[ 413]---> BDD-cost:   28
c ---[ 412]---> BDD-cost:   28
c ---[ 411]---> BDD-cost:   28
c ---[ 410]---> BDD-cost:   28
c ---[ 409]---> BDD-cost:   28
c ---[ 407]---> BDD-cost:  196
c ---[ 406]---> BDD-cost:   28
c ---[ 405]---> BDD-cost:   28
c ---[ 404]---> BDD-cost:   28
c ---[ 403]---> BDD-cost:   28
c ---[ 402]---> BDD-cost:   28
c ---[ 401]---> BDD-cost:   28
c ---[ 400]---> BDD-cost:   28
c ---[ 399]---> BDD-cost:   28
c ---[ 398]---> BDD-cost:   28
c ---[ 397]---> BDD-cost:   28
c ---[ 395]---> BDD-cost:  199
c ---[ 394]---> BDD-cost:   28
c ---[ 393]---> BDD-cost:   28
c ---[ 392]---> BDD-cost:   28
c ---[ 391]---> BDD-cost:   28
c ---[ 390]---> BDD-cost:   28
c ---[ 389]---> BDD-cost:   28
c ---[ 388]---> BDD-cost:   28
c ---[ 387]---> BDD-cost:   28
c ---[ 386]---> BDD-cost:   28
c ---[ 385]---> BDD-cost:   28
c ---[ 383]---> BDD-cost:  193
c ---[ 382]---> BDD-cost:   28
c ---[ 381]---> BDD-cost:   28
c ---[ 380]---> BDD-cost:   28
c ---[ 379]---> BDD-cost:   28
c ---[ 378]---> BDD-cost:   28
c ---[ 377]---> BDD-cost:   28
c ---[ 376]---> BDD-cost:   28
c ---[ 375]---> BDD-cost:   28
c ---[ 374]---> BDD-cost:   28
c ---[ 373]---> BDD-cost:   28
c ---[ 371]---> BDD-cost:  193
c ---[ 370]---> BDD-cost:   28
c ---[ 369]---> BDD-cost:   28
c ---[ 368]---> BDD-cost:   28
c ---[ 367]---> BDD-cost:   28
c ---[ 366]---> BDD-cost:   28
c ---[ 365]---> BDD-cost:   28
c ---[ 364]---> BDD-cost:   28
c ---[ 363]---> BDD-cost:   28
c ---[ 362]---> BDD-cost:   28
c ---[ 361]---> BDD-cost:   28
c ---[ 359]---> BDD-cost:  199
c ---[ 357]---> BDD-cost:  199
c ---[ 356]---> BDD-cost:   28
c ---[ 355]---> BDD-cost:   28
c ---[ 354]---> BDD-cost:   28
c ---[ 353]---> BDD-cost:   28
c ---[ 352]---> BDD-cost:   28
c ---[ 351]---> BDD-cost:   28
c ---[ 350]---> BDD-cost:   28
c ---[ 349]---> BDD-cost:   28
c ---[ 348]---> BDD-cost:   28
c ---[ 347]---> BDD-cost:   28
c ---[ 345]---> BDD-cost:  190
c ---[ 344]---> BDD-cost:   28
c ---[ 343]---> BDD-cost:   28
c ---[ 342]---> BDD-cost:   28
c ---[ 341]---> BDD-cost:   28
c ---[ 340]---> BDD-cost:   28
c ---[ 339]---> BDD-cost:   28
c ---[ 338]---> BDD-cost:   28
c ---[ 337]---> BDD-cost:   28
c ---[ 336]---> BDD-cost:   28
c ---[ 335]---> BDD-cost:   28
c ---[ 333]---> BDD-cost:  199
c ---[ 332]---> BDD-cost:   28
c ---[ 331]---> BDD-cost:   28
c ---[ 330]---> BDD-cost:   28
c ---[ 329]---> BDD-cost:   28
c ---[ 328]---> BDD-cost:   28
c ---[ 327]---> BDD-cost:   28
c ---[ 326]---> BDD-cost:   28
c ---[ 325]---> BDD-cost:   28
c ---[ 324]---> BDD-cost:   28
c ---[ 323]---> BDD-cost:   28
c ---[ 321]---> BDD-cost:  196
c ---[ 320]---> BDD-cost:   28
c ---[ 319]---> BDD-cost:   28
c ---[ 318]---> BDD-cost:   28
c ---[ 317]---> BDD-cost:   28
c ---[ 316]---> BDD-cost:   28
c ---[ 315]---> BDD-cost:   28
c ---[ 314]---> BDD-cost:   28
c ---[ 313]---> BDD-cost:   28
c ---[ 312]---> BDD-cost:   28
c ---[ 311]---> BDD-cost:   28
c ---[ 309]---> BDD-cost:  199
c ---[ 308]---> BDD-cost:   28
c ---[ 307]---> BDD-cost:   27
c ---[ 306]---> BDD-cost:   27
c ---[ 305]---> BDD-cost:   27
c ---[ 304]---> BDD-cost:   27
c ---[ 303]---> BDD-cost:   27
c ---[ 302]---> BDD-cost:   27
c ---[ 301]---> BDD-cost:   27
c ---[ 300]---> BDD-cost:   27
c ---[ 299]---> BDD-cost:   27
c ---[ 297]---> BDD-cost:  196
c ---[ 296]---> BDD-cost:   27
c ---[ 295]---> BDD-cost:   27
c ---[ 294]---> BDD-cost:   27
c ---[ 293]---> BDD-cost:   27
c ---[ 292]---> BDD-cost:   27
c ---[ 291]---> BDD-cost:   27
c ---[ 290]---> BDD-cost:   27
c ---[ 289]---> BDD-cost:   27
c ---[ 288]---> BDD-cost:   27
c ---[ 287]---> BDD-cost:   27
c ---[ 285]---> BDD-cost:  193
c ---[ 284]---> BDD-cost:   27
c ---[ 283]---> BDD-cost:   27
c ---[ 282]---> BDD-cost:   27
c ---[ 281]---> BDD-cost:   27
c ---[ 280]---> BDD-cost:   27
c ---[ 279]---> BDD-cost:   27
c ---[ 278]---> BDD-cost:   27
c ---[ 277]---> BDD-cost:   27
c ---[ 276]---> BDD-cost:   27
c ---[ 275]---> BDD-cost:   27
c ---[ 273]---> BDD-cost:  199
c ---[ 272]---> BDD-cost:   27
c ---[ 271]---> BDD-cost:   27
c ---[ 270]---> BDD-cost:   27
c ---[ 269]---> BDD-cost:   27
c ---[ 268]---> BDD-cost:   27
c ---[ 267]---> BDD-cost:   27
c ---[ 266]---> BDD-cost:   27
c ---[ 265]---> BDD-cost:   27
c ---[ 264]---> BDD-cost:   27
c ---[ 263]---> BDD-cost:   27
c ---[ 261]---> BDD-cost:  199
c ---[ 260]---> BDD-cost:   27
c ---[ 259]---> BDD-cost:   27
c ---[ 258]---> BDD-cost:   27
c ---[ 257]---> BDD-cost:   27
c ---[ 256]---> BDD-cost:   27
c ---[ 255]---> BDD-cost:   27
c ---[ 254]---> BDD-cost:   27
c ---[ 253]---> BDD-cost:   27
c ---[ 252]---> BDD-cost:   27
c ---[ 251]---> BDD-cost:   27
c ---[ 249]---> BDD-cost:  193
c ---[ 248]---> BDD-cost:   27
c ---[ 247]---> BDD-cost:   27
c ---[ 246]---> BDD-cost:   27
c ---[ 245]---> BDD-cost:   27
c ---[ 244]---> BDD-cost:   27
c ---[ 243]---> BDD-cost:   27
c ---[ 242]---> BDD-cost:   27
c ---[ 241]---> BDD-cost:   27
c ---[ 240]---> BDD-cost:   27
c ---[ 239]---> BDD-cost:   27
c ---[ 237]---> BDD-cost:  199
c ---[ 235]---> BDD-cost:  196
c ---[ 234]---> BDD-cost:   27
c ---[ 233]---> BDD-cost:   28
c ---[ 232]---> BDD-cost:   28
c ---[ 231]---> BDD-cost:   28
c ---[ 230]---> BDD-cost:   28
c ---[ 229]---> BDD-cost:   28
c ---[ 228]---> BDD-cost:   28
c ---[ 227]---> BDD-cost:   28
c ---[ 226]---> BDD-cost:   28
c ---[ 225]---> BDD-cost:   28
c ---[ 223]---> BDD-cost:   52
c ---[ 222]---> BDD-cost:   28
c ---[ 221]---> BDD-cost:   28
c ---[ 220]---> BDD-cost:   28
c ---[ 219]---> BDD-cost:   28
c ---[ 218]---> BDD-cost:   28
c ---[ 217]---> BDD-cost:   28
c ---[ 216]---> BDD-cost:   28
c ---[ 215]---> BDD-cost:   28
c ---[ 214]---> BDD-cost:   28
c ---[ 213]---> BDD-cost:   28
c ---[ 211]---> BDD-cost:  188
c ---[ 210]---> BDD-cost:   28
c ---[ 209]---> BDD-cost:   28
c ---[ 208]---> BDD-cost:   28
c ---[ 207]---> BDD-cost:   28
c ---[ 206]---> BDD-cost:   28
c ---[ 205]---> BDD-cost:   28
c ---[ 204]---> BDD-cost:   28
c ---[ 203]---> BDD-cost:   28
c ---[ 202]---> BDD-cost:   28
c ---[ 201]---> BDD-cost:   28
c ---[ 199]---> BDD-cost:  195
c ---[ 198]---> BDD-cost:   28
c ---[ 197]---> BDD-cost:   25
c ---[ 196]---> BDD-cost:   25
c ---[ 195]---> BDD-cost:   25
c ---[ 194]---> BDD-cost:   25
c ---[ 193]---> BDD-cost:   25
c ---[ 192]---> BDD-cost:   25
c ---[ 191]---> BDD-cost:   25
c ---[ 190]---> BDD-cost:   25
c ---[ 189]---> BDD-cost:   25
c ---[ 187]---> BDD-cost:  199
c ---[ 186]---> BDD-cost:   25
c ---[ 185]---> BDD-cost:   25
c ---[ 184]---> BDD-cost:   25
c ---[ 183]---> BDD-cost:   25
c ---[ 182]---> BDD-cost:   25
c ---[ 181]---> BDD-cost:   25
c ---[ 180]---> BDD-cost:   25
c ---[ 179]---> BDD-cost:   25
c ---[ 178]---> BDD-cost:   25
c ---[ 177]---> BDD-cost:   25
c ---[ 175]---> BDD-cost:  193
c ---[ 174]---> BDD-cost:   25
c ---[ 173]---> BDD-cost:   25
c ---[ 172]---> BDD-cost:   25
c ---[ 171]---> BDD-cost:   25
c ---[ 170]---> BDD-cost:   25
c ---[ 169]---> BDD-cost:   25
c ---[ 168]---> BDD-cost:   25
c ---[ 167]---> BDD-cost:   25
c ---[ 166]---> BDD-cost:   25
c ---[ 165]---> BDD-cost:   25
c ---[ 163]---> BDD-cost:  187
c ---[ 162]---> BDD-cost:   25
c ---[ 161]---> BDD-cost:   27
c ---[ 160]---> BDD-cost:   27
c ---[ 159]---> BDD-cost:   27
c ---[ 158]---> BDD-cost:   27
c ---[ 157]---> BDD-cost:   27
c ---[ 156]---> BDD-cost:   27
c ---[ 155]---> BDD-cost:   27
c ---[ 154]---> BDD-cost:   27
c ---[ 153]---> BDD-cost:   27
c ---[ 151]---> BDD-cost:  199
c ---[ 150]---> BDD-cost:   27
c ---[ 149]---> BDD-cost:   27
c ---[ 148]---> BDD-cost:   27
c ---[ 147]---> BDD-cost:   27
c ---[ 146]---> BDD-cost:   27
c ---[ 145]---> BDD-cost:   27
c ---[ 144]---> BDD-cost:   27
c ---[ 143]---> BDD-cost:   27
c ---[ 142]---> BDD-cost:   27
c ---[ 141]---> BDD-cost:   27
c ---[ 139]---> BDD-cost:  196
c ---[ 138]---> BDD-cost:   27
c ---[ 137]---> BDD-cost:   27
c ---[ 136]---> BDD-cost:   27
c ---[ 135]---> BDD-cost:   27
c ---[ 134]---> BDD-cost:   27
c ---[ 133]---> BDD-cost:   27
c ---[ 132]---> BDD-cost:   27
c ---[ 131]---> BDD-cost:   27
c ---[ 130]---> BDD-cost:   27
c ---[ 129]---> BDD-cost:   27
c ---[ 127]---> BDD-cost:  199
c ---[ 126]---> BDD-cost:   27
c ---[ 125]---> BDD-cost:   25
c ---[ 124]---> BDD-cost:   25
c ---[ 123]---> BDD-cost:   25
c ---[ 122]---> BDD-cost:   25
c ---[ 121]---> BDD-cost:   25
c ---[ 120]---> BDD-cost:   25
c ---[ 119]---> BDD-cost:   25
c ---[ 118]---> BDD-cost:   25
c ---[ 117]---> BDD-cost:   25
c ---[ 115]---> BDD-cost:  199
c ---[ 113]---> BDD-cost:  190
c ---[ 112]---> BDD-cost:   25
c ---[ 111]---> BDD-cost:   25
c ---[ 110]---> BDD-cost:   25
c ---[ 109]---> BDD-cost:   25
c ---[ 108]---> BDD-cost:   25
c ---[ 107]---> BDD-cost:   25
c ---[ 106]---> BDD-cost:   25
c ---[ 105]---> BDD-cost:   25
c ---[ 104]---> BDD-cost:   25
c ---[ 103]---> BDD-cost:   25
c ---[ 101]---> BDD-cost:  193
c ---[ 100]---> BDD-cost:   25
c ---[  99]---> BDD-cost:   25
c ---[  98]---> BDD-cost:   25
c ---[  97]---> BDD-cost:   25
c ---[  96]---> BDD-cost:   25
c ---[  95]---> BDD-cost:   25
c ---[  94]---> BDD-cost:   25
c ---[  93]---> BDD-cost:   25
c ---[  92]---> BDD-cost:   25
c ---[  91]---> BDD-cost:   25
c ---[  89]---> BDD-cost:  196
c ---[  88]---> BDD-cost:   25
c ---[  87]---> BDD-cost: 9840
c ---[  86]---> BDD-cost: 9840
c ---[  85]---> BDD-cost: 9840
c ---[  84]---> BDD-cost: 9840
c ---[  83]---> BDD-cost: 9840
c ---[  82]---> BDD-cost: 9840
c ---[  81]---> BDD-cost: 9840
c ---[  80]---> BDD-cost: 9840
c ---[  79]---> BDD-cost: 9840
c ---[  77]---> BDD-cost:  199
c ---[  76]---> BDD-cost: 9840
c ---[  75]---> BDD-cost: 9840
c ---[  74]---> BDD-cost: 9840
c ---[  73]---> BDD-cost: 9840
c ---[  72]---> BDD-cost: 9840
c ---[  71]---> BDD-cost: 9840
c ---[  70]---> BDD-cost: 9840
c ---[  69]---> BDD-cost: 9840
c ---[  68]---> BDD-cost: 9840
c ---[  67]---> BDD-cost: 9840
c ---[  65]---> BDD-cost:  199
c ---[  64]---> BDD-cost: 9840
c ---[  63]---> BDD-cost: 9840
c ---[  62]---> BDD-cost: 9840
c ---[  61]---> BDD-cost: 9840
c ---[  60]---> BDD-cost: 9840
c ---[  59]---> BDD-cost: 9840
c ---[  58]---> BDD-cost: 9840
c ---[  57]---> BDD-cost: 9840
c ---[  56]---> BDD-cost: 9840
c ---[  55]---> BDD-cost: 9840
c ---[  53]---> BDD-cost:  199
c ---[  52]---> BDD-cost: 9840
c ---[  50]---> BDD-cost:  190
c ---[  48]---> BDD-cost:  199
c ---[  46]---> BDD-cost:  199
c ---[  44]---> BDD-cost:  199
c ---[  42]---> BDD-cost:  193
c ---[  40]---> BDD-cost:  196
c ---[  38]---> BDD-cost:  199
c ---[  36]---> BDD-cost:  199
c ---[  34]---> BDD-cost:  190
c ---[  32]---> BDD-cost:  199
c ---[  30]---> BDD-cost:  193
c ---[  28]---> BDD-cost:  193
c ---[  26]---> BDD-cost:  199
c ---[  24]---> BDD-cost:  187
c ---[  22]---> BDD-cost:  193
c ---[  20]---> BDD-cost:  187
c ---[  18]---> BDD-cost:  199
c ---[  16]---> BDD-cost:   71
c ---[  14]---> BDD-cost:  185
c ---[  12]---> BDD-cost:  164
c ---[  10]---> BDD-cost:  196
c ---[   8]---> BDD-cost:  196
c ---[   6]---> BDD-cost:  199
c ---[   4]---> BDD-cost:  190
c ---[   2]---> BDD-cost:  196
c ---[   0]---> BDD-cost:  199
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1020841  2968529 |  340280       0        0     nan |  0.000 % |
c |       101 | 1020457  2967665 |  374308      99      953     9.6 |  0.438 % |
c |       252 | 1019991  2966372 |  411738     233     2828    12.1 |  0.458 % |
c |       477 | 1019991  2966372 |  452912     458     7953    17.4 |  0.458 % |
c |       814 | 1019679  2965480 |  498203     782    11213    14.3 |  0.475 % |
c |      1320 | 1019679  2965480 |  548024    1288    21299    16.5 |  0.475 % |
c |      2080 | 1019625  2965328 |  602826    2045    42211    20.6 |  0.476 % |
c |      3219 | 1019161  2964178 |  663109    3167    84208    26.6 |  0.519 % |
c |      4928 | 1019161  2964178 |  729420    4876   142734    29.3 |  0.519 % |
c |      7490 | 1019161  2964178 |  802362    7438   276516    37.2 |  0.519 % |
c |     11334 | 1019145  2964146 |  882598   11274   373627    33.1 |  0.521 % |
c |     17100 | 1019104  2964054 |  970858   17029   508328    29.9 |  0.525 % |
c |     25750 | 1018971  2963760 | 1067944   25607   827771    32.3 |  0.542 % |
c |     38724 | 1018919  2963633 | 1174738   38567  1501444    38.9 |  0.547 % |
c |     58186 | 1018919  2963633 | 1292212   58029  2572521    44.3 |  0.547 % |
c |     87379 | 1018917  2963629 | 1421434   87221  3990816    45.8 |  0.547 % |
c |    131171 | 1018887  2963555 | 1563577  131009  6679866    51.0 |  0.550 % |
c |    196855 | 1018883  2963547 | 1719935  196691 10807086    54.9 |  0.551 % |
c |    295382 | 1018851  2963465 | 1891928  295212 21612116    73.2 |  0.554 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.94 0.90 2/54 21811
Raw data (stat): 21811 (runsolver) R 21810 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541900318 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.88 0.94 0.90 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 32515 0 0 0 918 80 0 0 25 0 1 0 541900318 143736832 31123 4294967295 134512640 134672761 3221224528 3221223696 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35092 31123 603 41 0 35051 0
vsize: 140368
[startup+20.0014 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 33026 0 0 0 1915 81 0 0 25 0 1 0 541900318 145711104 31634 4294967295 134512640 134672761 3221224528 3221223724 134556678 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35574 31634 603 41 0 35533 0
vsize: 142296
[startup+30.0014 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 33424 0 0 0 2914 83 0 0 25 0 1 0 541900318 147324928 32032 4294967295 134512640 134672761 3221224528 3221223672 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35968 32032 603 41 0 35927 0
vsize: 143872
[startup+40.0019 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 33727 0 0 0 3913 83 0 0 25 0 1 0 541900318 148602880 32335 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36280 32335 603 41 0 36239 0
vsize: 145120
[startup+50.0017 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 33913 0 0 0 4913 84 0 0 25 0 1 0 541900318 149397504 32521 4294967295 134512640 134672761 3221224528 3221223700 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36474 32521 603 41 0 36433 0
vsize: 145896
[startup+60.0019 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 34228 0 0 0 5911 85 0 0 25 0 1 0 541900318 150597632 32836 4294967295 134512640 134672761 3221224528 3221223664 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36767 32836 603 41 0 36726 0
vsize: 147068
[startup+70.0023 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 34695 0 0 0 6910 87 0 0 25 0 1 0 541900318 152608768 33303 4294967295 134512640 134672761 3221224528 3221223696 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37258 33303 603 41 0 37217 0
vsize: 149032
[startup+80.002 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 35138 0 0 0 7908 88 0 0 25 0 1 0 541900318 154349568 33746 4294967295 134512640 134672761 3221224528 3221223632 134560299 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37683 33746 603 41 0 37642 0
vsize: 150732
[startup+90.0022 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 35569 0 0 0 8907 90 0 0 25 0 1 0 541900318 156098560 34177 4294967295 134512640 134672761 3221224528 3221223696 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38110 34177 603 41 0 38069 0
vsize: 152440
[startup+100.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 35988 0 0 0 9906 91 0 0 25 0 1 0 541900318 157835264 34596 4294967295 134512640 134672761 3221224528 3221223664 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38534 34596 603 41 0 38493 0
vsize: 154136
[startup+110.003 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 36246 0 0 0 10905 92 0 0 25 0 1 0 541900318 158773248 34854 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38763 34854 603 41 0 38722 0
vsize: 155052
[startup+120.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 36448 0 0 0 11904 93 0 0 25 0 1 0 541900318 159956992 35056 4294967295 134512640 134672761 3221224528 3221223620 1075351262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39052 35056 603 41 0 39011 0
vsize: 156208
[startup+130.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 36621 0 0 0 12902 94 0 0 25 0 1 0 541900318 160612352 35229 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39212 35229 603 41 0 39171 0
vsize: 156848
[startup+140.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 36779 0 0 0 13902 94 0 0 25 0 1 0 541900318 161316864 35387 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39384 35387 603 41 0 39343 0
vsize: 157536
[startup+150.012 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 37032 0 0 0 14902 95 0 0 25 0 1 0 541900318 162279424 35640 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39619 35640 603 41 0 39578 0
vsize: 158476
[startup+160.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 37489 0 0 0 15900 97 0 0 25 0 1 0 541900318 164163584 36097 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40079 36097 603 41 0 40038 0
vsize: 160316
[startup+170.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 37865 0 0 0 16899 99 0 0 25 0 1 0 541900318 165634048 36473 4294967295 134512640 134672761 3221224528 3221223696 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40438 36473 603 41 0 40397 0
vsize: 161752
[startup+180.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 38212 0 0 0 17898 100 0 0 25 0 1 0 541900318 167104512 36820 4294967295 134512640 134672761 3221224528 3221223700 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40797 36820 603 41 0 40756 0
vsize: 163188
[startup+190.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 38408 0 0 0 18898 100 0 0 25 0 1 0 541900318 167907328 37016 4294967295 134512640 134672761 3221224528 3221223728 134557822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40993 37016 603 41 0 40952 0
vsize: 163972
[startup+200.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 38579 0 0 0 19898 100 0 0 25 0 1 0 541900318 168566784 37187 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41154 37187 603 41 0 41113 0
vsize: 164616
[startup+210.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 38747 0 0 0 20897 101 0 0 25 0 1 0 541900318 169242624 37355 4294967295 134512640 134672761 3221224528 3221223632 134560355 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41319 37355 603 41 0 41278 0
vsize: 165276
[startup+220.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 39021 0 0 0 21896 102 0 0 25 0 1 0 541900318 170319872 37629 4294967295 134512640 134672761 3221224528 3221223664 134560714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41582 37629 603 41 0 41541 0
vsize: 166328
[startup+230.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 39433 0 0 0 22895 103 0 0 25 0 1 0 541900318 172060672 38041 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42007 38041 603 41 0 41966 0
vsize: 168028
[startup+240.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 39825 0 0 0 23895 104 0 0 25 0 1 0 541900318 173670400 38433 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42400 38433 603 41 0 42359 0
vsize: 169600
[startup+250.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 40190 0 0 0 24894 105 0 0 25 0 1 0 541900318 175153152 38798 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42762 38798 603 41 0 42721 0
vsize: 171048
[startup+260.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 40404 0 0 0 25894 106 0 0 25 0 1 0 541900318 175955968 39012 4294967295 134512640 134672761 3221224528 3221223652 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42958 39012 603 41 0 42917 0
vsize: 171832
[startup+270.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 40723 0 0 0 26893 107 0 0 25 0 1 0 541900318 177283072 39331 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43282 39331 603 41 0 43241 0
vsize: 173128
[startup+280.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 40952 0 0 0 27893 107 0 0 25 0 1 0 541900318 178778112 39560 4294967295 134512640 134672761 3221224528 3221223696 134561115 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43647 39560 603 41 0 43606 0
vsize: 174588
[startup+290.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 41134 0 0 0 28893 108 0 0 25 0 1 0 541900318 179433472 39742 4294967295 134512640 134672761 3221224528 3221223696 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43807 39742 603 41 0 43766 0
vsize: 175228
[startup+300.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 41320 0 0 0 29892 109 0 0 25 0 1 0 541900318 180232192 39928 4294967295 134512640 134672761 3221224528 3221223712 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44002 39928 603 41 0 43961 0
vsize: 176008
[startup+310.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 41509 0 0 0 30892 109 0 0 25 0 1 0 541900318 181026816 40117 4294967295 134512640 134672761 3221224528 3221223632 134560194 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44196 40117 603 41 0 44155 0
vsize: 176784
[startup+320.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 41746 0 0 0 31891 110 0 0 25 0 1 0 541900318 181993472 40354 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44432 40354 603 41 0 44391 0
vsize: 177728
[startup+330.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 42017 0 0 0 32892 111 0 0 25 0 1 0 541900318 183046144 40625 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44689 40625 603 41 0 44648 0
vsize: 178756
[startup+340.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 42301 0 0 0 33891 111 0 0 25 0 1 0 541900318 184246272 40909 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44982 40909 603 41 0 44941 0
vsize: 179928
[startup+350.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 42595 0 0 0 34893 112 0 0 25 0 1 0 541900318 185450496 41203 4294967295 134512640 134672761 3221224528 3221223696 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45276 41203 603 41 0 45235 0
vsize: 181104
[startup+360.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 42982 0 0 0 35892 113 0 0 25 0 1 0 541900318 186920960 41590 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45635 41590 603 41 0 45594 0
vsize: 182540
[startup+370.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 43512 0 0 0 36891 114 0 0 25 0 1 0 541900318 189054976 42120 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46156 42120 603 41 0 46115 0
vsize: 184624
[startup+380.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 43966 0 0 0 37890 115 0 0 25 0 1 0 541900318 190926848 42574 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46613 42574 603 41 0 46572 0
vsize: 186452
[startup+390.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 44354 0 0 0 38890 116 0 0 25 0 1 0 541900318 192557056 42962 4294967295 134512640 134672761 3221224528 3221223632 134560492 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47011 42962 603 41 0 46970 0
vsize: 188044
[startup+400.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 44768 0 0 0 39889 118 0 0 25 0 1 0 541900318 194166784 43376 4294967295 134512640 134672761 3221224528 3221223696 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47404 43376 603 41 0 47363 0
vsize: 189616
[startup+410.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 45210 0 0 0 40888 119 0 0 25 0 1 0 541900318 196030464 43818 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47859 43818 603 41 0 47818 0
vsize: 191436
[startup+420.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 45594 0 0 0 41886 120 0 0 25 0 1 0 541900318 197623808 44202 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48248 44202 603 41 0 48207 0
vsize: 192992
[startup+430.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 45971 0 0 0 42885 121 0 0 25 0 1 0 541900318 199098368 44579 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48608 44579 603 41 0 48567 0
vsize: 194432
[startup+440.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 46425 0 0 0 43884 122 0 0 25 0 1 0 541900318 200986624 45033 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49069 45033 603 41 0 49028 0
vsize: 196276
[startup+450.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 46869 0 0 0 44883 124 0 0 25 0 1 0 541900318 202739712 45477 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49497 45477 603 41 0 49456 0
vsize: 197988
[startup+460.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 47304 0 0 0 45882 125 0 0 25 0 1 0 541900318 204468224 45912 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49919 45912 603 41 0 49878 0
vsize: 199676
[startup+470.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 47749 0 0 0 46880 126 0 0 25 0 1 0 541900318 206344192 46357 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50377 46357 603 41 0 50336 0
vsize: 201508
[startup+480.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 48194 0 0 0 47880 127 0 0 25 0 1 0 541900318 208093184 46802 4294967295 134512640 134672761 3221224528 3221223696 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50804 46802 603 41 0 50763 0
vsize: 203216
[startup+490.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 48644 0 0 0 48878 129 0 0 25 0 1 0 541900318 209969152 47252 4294967295 134512640 134672761 3221224528 3221223632 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51262 47252 603 41 0 51221 0
vsize: 205048
[startup+500.058 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 49083 0 0 0 49878 130 0 0 25 0 1 0 541900318 211709952 47691 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51687 47691 603 41 0 51646 0
vsize: 206748
[startup+510.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 49500 0 0 0 50876 131 0 0 25 0 1 0 541900318 213434368 48108 4294967295 134512640 134672761 3221224528 3221223696 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52108 48108 603 41 0 52067 0
vsize: 208432
[startup+520.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 49884 0 0 0 51875 133 0 0 25 0 1 0 541900318 215040000 48492 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52500 48492 603 41 0 52459 0
vsize: 210000
[startup+530.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 50274 0 0 0 52874 134 0 0 25 0 1 0 541900318 216653824 48882 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52894 48882 603 41 0 52853 0
vsize: 211576
[startup+540.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 50667 0 0 0 53873 136 0 0 25 0 1 0 541900318 218279936 49275 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53291 49275 603 41 0 53250 0
vsize: 213164
[startup+550.059 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 50971 0 0 0 54872 136 0 0 25 0 1 0 541900318 219488256 49579 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53586 49579 603 41 0 53545 0
vsize: 214344
[startup+560.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 51149 0 0 0 55873 136 0 0 25 0 1 0 541900318 220176384 49757 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53754 49757 603 41 0 53713 0
vsize: 215016
[startup+570.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 51405 0 0 0 56872 137 0 0 25 0 1 0 541900318 221261824 50013 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54019 50013 603 41 0 53978 0
vsize: 216076
[startup+580.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 51627 0 0 0 57872 137 0 0 25 0 1 0 541900318 222203904 50235 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54249 50235 603 41 0 54208 0
vsize: 216996
[startup+590.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 51864 0 0 0 58871 138 0 0 25 0 1 0 541900318 223145984 50472 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54479 50472 603 41 0 54438 0
vsize: 217916
[startup+600.061 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 52083 0 0 0 59871 139 0 0 25 0 1 0 541900318 223985664 50691 4294967295 134512640 134672761 3221224528 3221223664 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54684 50691 603 41 0 54643 0
vsize: 218736
[startup+610.062 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 52367 0 0 0 60870 139 0 0 25 0 1 0 541900318 225193984 50975 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54979 50975 603 41 0 54938 0
vsize: 219916
[startup+620.062 s]
Raw data (loadavg): 1.13 1.00 0.92 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 52632 0 0 0 61870 140 0 0 25 0 1 0 541900318 226263040 51240 4294967295 134512640 134672761 3221224528 3221223632 134560224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55240 51240 603 41 0 55199 0
vsize: 220960
[startup+630.062 s]
Raw data (loadavg): 1.18 1.02 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 52900 0 0 0 62870 140 0 0 25 0 1 0 541900318 227340288 51508 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55503 51508 603 41 0 55462 0
vsize: 222012
[startup+640.063 s]
Raw data (loadavg): 1.15 1.02 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 53186 0 0 0 63869 141 0 0 25 0 1 0 541900318 228540416 51794 4294967295 134512640 134672761 3221224528 3221223696 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55796 51794 603 41 0 55755 0
vsize: 223184
[startup+650.063 s]
Raw data (loadavg): 1.13 1.02 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 53439 0 0 0 64868 142 0 0 25 0 1 0 541900318 230662144 52047 4294967295 134512640 134672761 3221224528 3221223664 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56314 52048 603 41 0 56273 0
vsize: 225256
[startup+660.063 s]
Raw data (loadavg): 1.11 1.02 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 53651 0 0 0 65868 143 0 0 25 0 1 0 541900318 231464960 52259 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56510 52259 603 41 0 56469 0
vsize: 226040
[startup+670.064 s]
Raw data (loadavg): 1.09 1.02 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 53891 0 0 0 66868 143 0 0 25 0 1 0 541900318 232407040 52499 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56740 52499 603 41 0 56699 0
vsize: 226960
[startup+680.064 s]
Raw data (loadavg): 1.08 1.01 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 54147 0 0 0 67867 144 0 0 25 0 1 0 541900318 233476096 52755 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57001 52755 603 41 0 56960 0
vsize: 228004
[startup+690.064 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 54405 0 0 0 68867 144 0 0 25 0 1 0 541900318 234541056 53013 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57261 53013 603 41 0 57220 0
vsize: 229044
[startup+700.063 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 54666 0 0 0 69866 145 0 0 25 0 1 0 541900318 235618304 53274 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57524 53274 603 41 0 57483 0
vsize: 230096
[startup+710.064 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 54935 0 0 0 70866 146 0 0 25 0 1 0 541900318 236683264 53543 4294967295 134512640 134672761 3221224528 3221223708 134559056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57784 53543 603 41 0 57743 0
vsize: 231136
[startup+720.064 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 55174 0 0 0 71865 146 0 0 25 0 1 0 541900318 237617152 53782 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58012 53782 603 41 0 57971 0
vsize: 232048
[startup+730.064 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 55386 0 0 0 72865 147 0 0 25 0 1 0 541900318 238567424 53994 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58244 53994 603 41 0 58203 0
vsize: 232976
[startup+740.064 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 55612 0 0 0 73865 147 0 0 25 0 1 0 541900318 239501312 54220 4294967295 134512640 134672761 3221224528 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58472 54220 603 41 0 58431 0
vsize: 233888
[startup+750.064 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 55868 0 0 0 74864 148 0 0 25 0 1 0 541900318 240553984 54476 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58729 54476 603 41 0 58688 0
vsize: 234916
[startup+760.065 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 56100 0 0 0 75864 149 0 0 25 0 1 0 541900318 241512448 54708 4294967295 134512640 134672761 3221224528 3221223696 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58963 54708 603 41 0 58922 0
vsize: 235852
[startup+770.066 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 56315 0 0 0 76864 149 0 0 25 0 1 0 541900318 242315264 54923 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59159 54923 603 41 0 59118 0
vsize: 236636
[startup+780.066 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 56540 0 0 0 77863 150 0 0 25 0 1 0 541900318 243257344 55148 4294967295 134512640 134672761 3221224528 3221223632 134560184 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59389 55148 603 41 0 59348 0
vsize: 237556
[startup+790.066 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 56766 0 0 0 78863 150 0 0 25 0 1 0 541900318 244199424 55374 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59619 55374 603 41 0 59578 0
vsize: 238476
[startup+800.065 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 57013 0 0 0 79862 151 0 0 25 0 1 0 541900318 245133312 55621 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59847 55621 603 41 0 59806 0
vsize: 239388
[startup+810.066 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 57265 0 0 0 80862 152 0 0 25 0 1 0 541900318 246198272 55873 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60107 55873 603 41 0 60066 0
vsize: 240428
[startup+820.066 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 57472 0 0 0 81861 152 0 0 25 0 1 0 541900318 247009280 56080 4294967295 134512640 134672761 3221224528 3221223696 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60305 56080 603 41 0 60264 0
vsize: 241220
[startup+830.066 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 57718 0 0 0 82861 153 0 0 25 0 1 0 541900318 248070144 56326 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60564 56326 603 41 0 60523 0
vsize: 242256
[startup+840.169 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 57924 0 0 0 83870 154 0 0 25 0 1 0 541900318 248868864 56532 4294967295 134512640 134672761 3221224528 3221223632 134554971 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60759 56532 603 41 0 60718 0
vsize: 243036
[startup+850.168 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 58139 0 0 0 84870 154 0 0 25 0 1 0 541900318 249815040 56747 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60990 56747 603 41 0 60949 0
vsize: 243960
[startup+860.169 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 58352 0 0 0 85869 155 0 0 25 0 1 0 541900318 250617856 56960 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61186 56960 603 41 0 61145 0
vsize: 244744
[startup+870.18 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 58538 0 0 0 86870 155 0 0 25 0 1 0 541900318 251412480 57146 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61380 57146 603 41 0 61339 0
vsize: 245520
[startup+880.18 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 58733 0 0 0 87869 156 0 0 25 0 1 0 541900318 252223488 57341 4294967295 134512640 134672761 3221224528 3221223696 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61578 57341 603 41 0 61537 0
vsize: 246312
[startup+890.18 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 58933 0 0 0 88869 157 0 0 25 0 1 0 541900318 253034496 57541 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61776 57541 603 41 0 61735 0
vsize: 247104
[startup+900.184 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 59118 0 0 0 89868 158 0 0 25 0 1 0 541900318 253841408 57726 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61973 57726 603 41 0 61932 0
vsize: 247892
[startup+910.189 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 59330 0 0 0 90869 158 0 0 25 0 1 0 541900318 254644224 57938 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62169 57938 603 41 0 62128 0
vsize: 248676
[startup+920.189 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 59519 0 0 0 91869 158 0 0 25 0 1 0 541900318 255434752 58127 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62362 58127 603 41 0 62321 0
vsize: 249448
[startup+930.188 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 59718 0 0 0 92869 159 0 0 25 0 1 0 541900318 256221184 58326 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62554 58326 603 41 0 62513 0
vsize: 250216
[startup+940.189 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 59889 0 0 0 93868 159 0 0 25 0 1 0 541900318 256884736 58497 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62716 58497 603 41 0 62675 0
vsize: 250864
[startup+950.189 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 60049 0 0 0 94868 160 0 0 25 0 1 0 541900318 257552384 58657 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62879 58657 603 41 0 62838 0
vsize: 251516
[startup+960.19 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 60219 0 0 0 95868 160 0 0 25 0 1 0 541900318 258224128 58827 4294967295 134512640 134672761 3221224528 3221223696 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63043 58827 603 41 0 63002 0
vsize: 252172
[startup+970.19 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 60475 0 0 0 96867 161 0 0 25 0 1 0 541900318 259371008 59083 4294967295 134512640 134672761 3221224528 3221223700 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63323 59083 603 41 0 63282 0
vsize: 253292
[startup+980.189 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 60645 0 0 0 97866 162 0 0 25 0 1 0 541900318 260050944 59253 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63489 59253 603 41 0 63448 0
vsize: 253956
[startup+990.19 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 60801 0 0 0 98866 163 0 0 25 0 1 0 541900318 260730880 59409 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63655 59409 603 41 0 63614 0
vsize: 254620
[startup+1000.19 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 61021 0 0 0 99865 163 0 0 25 0 1 0 541900318 261668864 59629 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63884 59629 603 41 0 63843 0
vsize: 255536
[startup+1010.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 61285 0 0 0 100866 164 0 0 25 0 1 0 541900318 262737920 59893 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64145 59893 603 41 0 64104 0
vsize: 256580
[startup+1020.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 61534 0 0 0 101865 165 0 0 25 0 1 0 541900318 263671808 60142 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64373 60142 603 41 0 64332 0
vsize: 257492
[startup+1030.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 61762 0 0 0 102864 166 0 0 25 0 1 0 541900318 264617984 60370 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64604 60370 603 41 0 64563 0
vsize: 258416
[startup+1040.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 62003 0 0 0 103864 167 0 0 25 0 1 0 541900318 265666560 60611 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64860 60611 603 41 0 64819 0
vsize: 259440
[startup+1050.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 62251 0 0 0 104863 167 0 0 25 0 1 0 541900318 266600448 60859 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65088 60859 603 41 0 65047 0
vsize: 260352
[startup+1060.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 62491 0 0 0 105863 168 0 0 25 0 1 0 541900318 267653120 61099 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65345 61099 603 41 0 65304 0
vsize: 261380
[startup+1070.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 62723 0 0 0 106863 169 0 0 25 0 1 0 541900318 268578816 61331 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65571 61331 603 41 0 65530 0
vsize: 262284
[startup+1080.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 62954 0 0 0 107862 169 0 0 25 0 1 0 541900318 269512704 61562 4294967295 134512640 134672761 3221224528 3221223712 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65799 61562 603 41 0 65758 0
vsize: 263196
[startup+1090.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 63183 0 0 0 108862 170 0 0 25 0 1 0 541900318 270450688 61791 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66028 61791 603 41 0 65987 0
vsize: 264112
[startup+1100.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 63405 0 0 0 109861 171 0 0 25 0 1 0 541900318 271278080 62013 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66230 62013 603 41 0 66189 0
vsize: 264920
[startup+1110.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 63626 0 0 0 110860 172 0 0 25 0 1 0 541900318 272228352 62234 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66462 62234 603 41 0 66421 0
vsize: 265848
[startup+1120.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 63837 0 0 0 111860 172 0 0 25 0 1 0 541900318 273154048 62445 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66688 62445 603 41 0 66647 0
vsize: 266752
[startup+1130.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 64058 0 0 0 112860 172 0 0 25 0 1 0 541900318 273948672 62666 4294967295 134512640 134672761 3221224528 3221223712 134559415 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66882 62666 603 41 0 66841 0
vsize: 267528
[startup+1140.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 64280 0 0 0 113860 173 0 0 25 0 1 0 541900318 274870272 62888 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67107 62888 603 41 0 67066 0
vsize: 268428
[startup+1150.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 64496 0 0 0 114859 174 0 0 25 0 1 0 541900318 275824640 63104 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67340 63104 603 41 0 67299 0
vsize: 269360
[startup+1160.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 64650 0 0 0 115859 174 0 0 25 0 1 0 541900318 276504576 63258 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67506 63258 603 41 0 67465 0
vsize: 270024
[startup+1170.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 64911 0 0 0 116858 175 0 0 25 0 1 0 541900318 277590016 63519 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67771 63519 603 41 0 67730 0
vsize: 271084
[startup+1180.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 65136 0 0 0 117858 175 0 0 25 0 1 0 541900318 278421504 63744 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67974 63744 603 41 0 67933 0
vsize: 271896
[startup+1190.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 65387 0 0 0 118857 176 0 0 25 0 1 0 541900318 279498752 63995 4294967295 134512640 134672761 3221224528 3221223632 134560051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68237 63995 603 41 0 68196 0
vsize: 272948
[startup+1200.2 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 21811
Raw data (stat): 21811 (minisat+) R 21810 27222 27221 0 -1 0 65674 0 0 0 119857 177 0 0 25 0 1 0 541900318 280702976 64282 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68531 64282 603 41 0 68490 0
vsize: 274124
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.33 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 21811
Raw data (stat): 21811 (minisat+) Z 21810 27222 27221 0 -1 12 65676 0 0 0 119857 189 0 0 25 0 1 0 541900318 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.33
CPU time (s): 1200.47
CPU user time (s): 1198.57
CPU system time (s): 1.89371
CPU usage (%): 100.012
Max. virtual memory (Kb): 274124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####