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/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-tr12-30.opb
MD5SUM	9136d330eaa53552ba154b6915193b35
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.131979
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 14213

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-20 23:17:48 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=20292 boxname=wulflinc18 idbench=1561 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  9136d330eaa53552ba154b6915193b35  /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-tr12-30.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-tr12-30.opb /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-tr12-30.opb
IDLAUNCH: 20292
/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:        675960 kB
Buffers:         33580 kB
Cached:         293588 kB
SwapCached:        388 kB
Active:          71640 kB
Inactive:       257976 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        675708 kB
SwapTotal:     2097892 kB
SwapFree:      2096996 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6220 kB
Slab:            23384 kB
Committed_AS:    63816 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-20 23:37:51 (client local time) WITH STATUS 0 IN 1200.3 SECONDS
stats: 20292 7 1200.3 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1110 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1109]---> BDD-cost: 9840
c ---[1108]---> BDD-cost: 9840
c ---[1107]---> BDD-cost: 9840
c ---[1106]---> BDD-cost: 9840
c ---[1105]---> BDD-cost: 9840
c ---[1104]---> BDD-cost: 9840
c ---[1103]---> BDD-cost: 9840
c ---[1102]---> BDD-cost: 9840
c ---[1101]---> BDD-cost: 9840
c ---[1100]---> BDD-cost: 9840
c ---[1099]---> BDD-cost: 9840
c ---[1098]---> BDD-cost: 9840
c ---[1097]---> BDD-cost: 9840
c ---[1096]---> BDD-cost: 9840
c ---[1095]---> BDD-cost: 9840
c ---[1094]---> BDD-cost: 9840
c ---[1093]---> BDD-cost: 9840
c ---[1092]---> BDD-cost: 9840
c ---[1091]---> BDD-cost: 9840
c ---[1090]---> BDD-cost: 9840
c ---[1089]---> BDD-cost: 9840
c ---[1088]---> BDD-cost: 9840
c ---[1087]---> BDD-cost: 9840
c ---[1086]---> BDD-cost: 9840
c ---[1085]---> BDD-cost: 9840
c ---[1084]---> BDD-cost: 9840
c ---[1083]---> BDD-cost: 9840
c ---[1082]---> BDD-cost: 9840
c ---[1081]---> BDD-cost: 9840
c ---[1080]---> BDD-cost: 9840
c ---[1078]---> BDD-cost:   71
c ---[1076]---> BDD-cost:  159
c ---[1074]---> BDD-cost:  189
c ---[1072]---> BDD-cost:  199
c ---[1070]---> BDD-cost:  199
c ---[1068]---> BDD-cost:  199
c ---[1066]---> BDD-cost:  199
c ---[1064]---> BDD-cost:  193
c ---[1062]---> BDD-cost:  187
c ---[1060]---> BDD-cost:  196
c ---[1058]---> BDD-cost:  196
c ---[1056]---> BDD-cost:  190
c ---[1054]---> BDD-cost:  199
c ---[1052]---> BDD-cost:  199
c ---[1050]---> BDD-cost:  190
c ---[1048]---> BDD-cost:  199
c ---[1046]---> BDD-cost:  193
c ---[1044]---> BDD-cost:  196
c ---[1042]---> BDD-cost:  196
c ---[1040]---> BDD-cost:  190
c ---[1038]---> BDD-cost:  199
c ---[1036]---> BDD-cost:  196
c ---[1034]---> BDD-cost:  193
c ---[1032]---> BDD-cost:  196
c ---[1030]---> BDD-cost:  193
c ---[1028]---> BDD-cost:  196
c ---[1026]---> BDD-cost:  190
c ---[1024]---> BDD-cost:  199
c ---[1022]---> BDD-cost:  196
c ---[1020]---> BDD-cost:  199
c ---[1018]---> BDD-cost:   67
c ---[1016]---> BDD-cost:  185
c ---[1014]---> BDD-cost:  189
c ---[1012]---> BDD-cost:  199
c ---[1010]---> BDD-cost:  196
c ---[1008]---> BDD-cost:  199
c ---[1006]---> BDD-cost:  196
c ---[1004]---> BDD-cost:  199
c ---[1002]---> BDD-cost:  193
c ---[1000]---> BDD-cost:  184
c ---[ 998]---> BDD-cost:  196
c ---[ 996]---> BDD-cost:  199
c ---[ 994]---> BDD-cost:  187
c ---[ 992]---> BDD-cost:  199
c ---[ 990]---> BDD-cost:  199
c ---[ 988]---> BDD-cost:  196
c ---[ 986]---> BDD-cost:  199
c ---[ 984]---> BDD-cost:  193
c ---[ 982]---> BDD-cost:  193
c ---[ 980]---> BDD-cost:  199
c ---[ 978]---> BDD-cost:  190
c ---[ 976]---> BDD-cost:  199
c ---[ 974]---> BDD-cost:  196
c ---[ 972]---> BDD-cost:  199
c ---[ 970]---> BDD-cost:  196
c ---[ 968]---> BDD-cost:  193
c ---[ 966]---> BDD-cost:  199
c ---[ 964]---> BDD-cost:  199
c ---[ 962]---> BDD-cost:  193
c ---[ 960]---> BDD-cost:  196
c ---[ 958]---> BDD-cost:   52
c ---[ 956]---> BDD-cost:  188
c ---[ 954]---> BDD-cost:  195
c ---[ 952]---> BDD-cost:  199
c ---[ 950]---> BDD-cost:  193
c ---[ 948]---> BDD-cost:  187
c ---[ 946]---> BDD-cost:  199
c ---[ 944]---> BDD-cost:  196
c ---[ 942]---> BDD-cost:  199
c ---[ 940]---> BDD-cost:  190
c ---[ 938]---> BDD-cost:  193
c ---[ 936]---> BDD-cost:  196
c ---[ 934]---> BDD-cost:  199
c ---[ 932]---> BDD-cost:  199
c ---[ 930]---> BDD-cost:  199
c ---[ 928]---> BDD-cost:  190
c ---[ 926]---> BDD-cost:  199
c ---[ 924]---> BDD-cost:  199
c ---[ 922]---> BDD-cost:  199
c ---[ 920]---> BDD-cost:  196
c ---[ 918]---> BDD-cost:  199
c ---[ 916]---> BDD-cost:  199
c ---[ 914]---> BDD-cost:  190
c ---[ 912]---> BDD-cost:  199
c ---[ 910]---> BDD-cost:  193
c ---[ 908]---> BDD-cost:  193
c ---[ 906]---> BDD-cost:  199
c ---[ 904]---> BDD-cost:  187
c ---[ 902]---> BDD-cost:  193
c ---[ 900]---> BDD-cost:  199
c ---[ 898]---> BDD-cost:   71
c ---[ 896]---> BDD-cost:  185
c ---[ 894]---> BDD-cost:  164
c ---[ 892]---> BDD-cost:  196
c ---[ 890]---> BDD-cost:  196
c ---[ 888]---> BDD-cost:  199
c ---[ 886]---> BDD-cost:  190
c ---[ 884]---> BDD-cost:  196
c ---[ 882]---> BDD-cost:  199
c ---[ 880]---> BDD-cost:  193
c ---[ 878]---> BDD-cost:  199
c ---[ 876]---> BDD-cost:  193
c ---[ 874]---> BDD-cost:  199
c ---[ 872]---> BDD-cost:  193
c ---[ 870]---> BDD-cost:  187
c ---[ 868]---> BDD-cost:  190
c ---[ 866]---> BDD-cost:  199
c ---[ 864]---> BDD-cost:  199
c ---[ 862]---> BDD-cost:  187
c ---[ 860]---> BDD-cost:  199
c ---[ 858]---> BDD-cost:  193
c ---[ 856]---> BDD-cost:  196
c ---[ 854]---> BDD-cost:  199
c ---[ 852]---> BDD-cost:  199
c ---[ 850]---> BDD-cost:  199
c ---[ 848]---> BDD-cost:  199
c ---[ 846]---> BDD-cost:  196
c ---[ 844]---> BDD-cost:  199
c ---[ 842]---> BDD-cost:  193
c ---[ 840]---> BDD-cost:  199
c ---[ 838]---> BDD-cost:   52
c ---[ 836]---> BDD-cost:  185
c ---[ 834]---> BDD-cost:  195
c ---[ 832]---> BDD-cost:  193
c ---[ 830]---> BDD-cost:  193
c ---[ 828]---> BDD-cost:  199
c ---[ 826]---> BDD-cost:  193
c ---[ 824]---> BDD-cost:  196
c ---[ 822]---> BDD-cost:  193
c ---[ 820]---> BDD-cost:  199
c ---[ 818]---> BDD-cost:  199
c ---[ 816]---> BDD-cost:  199
c ---[ 814]---> BDD-cost:  199
c ---[ 812]---> BDD-cost:  199
c ---[ 810]---> BDD-cost:  199
c ---[ 808]---> BDD-cost:  196
c ---[ 806]---> BDD-cost:  193
c ---[ 804]---> BDD-cost:  196
c ---[ 802]---> BDD-cost:  199
c ---[ 800]---> BDD-cost:  199
c ---[ 798]---> BDD-cost:  199
c ---[ 796]---> BDD-cost:  199
c ---[ 794]---> BDD-cost:  199
c ---[ 792]---> BDD-cost:  196
c ---[ 790]---> BDD-cost:  199
c ---[ 788]---> BDD-cost:  199
c ---[ 786]---> BDD-cost:  199
c ---[ 784]---> BDD-cost:  199
c ---[ 782]---> BDD-cost:  199
c ---[ 780]---> BDD-cost:  199
c ---[ 778]---> BDD-cost:   65
c ---[ 776]---> BDD-cost:  185
c ---[ 774]---> BDD-cost:  195
c ---[ 772]---> BDD-cost:  166
c ---[ 770]---> BDD-cost:  196
c ---[ 768]---> BDD-cost:  196
c ---[ 766]---> BDD-cost:  193
c ---[ 764]---> BDD-cost:  199
c ---[ 762]---> BDD-cost:  196
c ---[ 760]---> BDD-cost:  199
c ---[ 758]---> BDD-cost:  193
c ---[ 756]---> BDD-cost:  199
c ---[ 754]---> BDD-cost:  196
c ---[ 752]---> BDD-cost:  196
c ---[ 750]---> BDD-cost:  193
c ---[ 748]---> BDD-cost:  199
c ---[ 746]---> BDD-cost:  199
c ---[ 744]---> BDD-cost:  196
c ---[ 742]---> BDD-cost:  199
c ---[ 740]---> BDD-cost:  190
c ---[ 738]---> BDD-cost:  199
c ---[ 736]---> BDD-cost:  199
c ---[ 734]---> BDD-cost:  196
c ---[ 732]---> BDD-cost:  199
c ---[ 730]---> BDD-cost:  199
c ---[ 728]---> BDD-cost:  193
c ---[ 726]---> BDD-cost:  193
c ---[ 724]---> BDD-cost:  196
c ---[ 722]---> BDD-cost:  199
c ---[ 720]---> BDD-cost:  199
c ---[ 718]---> BDD-cost:   67
c ---[ 716]---> BDD-cost:  179
c ---[ 714]---> BDD-cost:  195
c ---[ 712]---> BDD-cost:  166
c ---[ 710]---> BDD-cost:  193
c ---[ 708]---> BDD-cost:  199
c ---[ 706]---> BDD-cost:  199
c ---[ 704]---> BDD-cost:  199
c ---[ 702]---> BDD-cost:  199
c ---[ 700]---> BDD-cost:  184
c ---[ 698]---> BDD-cost:  199
c ---[ 696]---> BDD-cost:  199
c ---[ 694]---> BDD-cost:  196
c ---[ 692]---> BDD-cost:  193
c ---[ 690]---> BDD-cost:  196
c ---[ 688]---> BDD-cost:  199
c ---[ 686]---> BDD-cost:  193
c ---[ 684]---> BDD-cost:  184
c ---[ 682]---> BDD-cost:  199
c ---[ 680]---> BDD-cost:  196
c ---[ 678]---> BDD-cost:  196
c ---[ 676]---> BDD-cost:  196
c ---[ 674]---> BDD-cost:  196
c ---[ 672]---> BDD-cost:  199
c ---[ 670]---> BDD-cost:  196
c ---[ 668]---> BDD-cost:  199
c ---[ 666]---> BDD-cost:  196
c ---[ 664]---> BDD-cost:  199
c ---[ 662]---> BDD-cost:  199
c ---[ 660]---> BDD-cost:  196
c ---[ 658]---> BDD-cost:   63
c ---[ 656]---> BDD-cost:  173
c ---[ 654]---> BDD-cost:  195
c ---[ 652]---> BDD-cost:  166
c ---[ 650]---> BDD-cost:  193
c ---[ 648]---> BDD-cost:  199
c ---[ 646]---> BDD-cost:  196
c ---[ 644]---> BDD-cost:  196
c ---[ 642]---> BDD-cost:  196
c ---[ 640]---> BDD-cost:  199
c ---[ 638]---> BDD-cost:  196
c ---[ 636]---> BDD-cost:  199
c ---[ 634]---> BDD-cost:  193
c ---[ 632]---> BDD-cost:  193
c ---[ 630]---> BDD-cost:  193
c ---[ 628]---> BDD-cost:  196
c ---[ 626]---> BDD-cost:  199
c ---[ 624]---> BDD-cost:  199
c ---[ 622]---> BDD-cost:  196
c ---[ 620]---> BDD-cost:  199
c ---[ 618]---> BDD-cost:  199
c ---[ 616]---> BDD-cost:  199
c ---[ 614]---> BDD-cost:  199
c ---[ 612]---> BDD-cost:  190
c ---[ 610]---> BDD-cost:  199
c ---[ 608]---> BDD-cost:  196
c ---[ 606]---> BDD-cost:  199
c ---[ 604]---> BDD-cost:  196
c ---[ 602]---> BDD-cost:  196
c ---[ 600]---> BDD-cost:  196
c ---[ 598]---> BDD-cost:   71
c ---[ 596]---> BDD-cost:  159
c ---[ 594]---> BDD-cost:  192
c ---[ 592]---> BDD-cost:  193
c ---[ 590]---> BDD-cost:  199
c ---[ 588]---> BDD-cost:  199
c ---[ 586]---> BDD-cost:  187
c ---[ 584]---> BDD-cost:  199
c ---[ 582]---> BDD-cost:  187
c ---[ 580]---> BDD-cost:  199
c ---[ 578]---> BDD-cost:  199
c ---[ 576]---> BDD-cost:  196
c ---[ 574]---> BDD-cost:  199
c ---[ 572]---> BDD-cost:  193
c ---[ 570]---> BDD-cost:  196
c ---[ 568]---> BDD-cost:  196
c ---[ 566]---> BDD-cost:  199
c ---[ 564]---> BDD-cost:  199
c ---[ 562]---> BDD-cost:  199
c ---[ 560]---> BDD-cost:  199
c ---[ 558]---> BDD-cost:  196
c ---[ 556]---> BDD-cost:  199
c ---[ 554]---> BDD-cost:  187
c ---[ 552]---> BDD-cost:  196
c ---[ 550]---> BDD-cost:  199
c ---[ 548]---> BDD-cost:  196
c ---[ 546]---> BDD-cost:  199
c ---[ 544]---> BDD-cost:  199
c ---[ 542]---> BDD-cost:  196
c ---[ 540]---> BDD-cost:  193
c ---[ 538]---> BDD-cost:   52
c ---[ 536]---> BDD-cost:  179
c ---[ 534]---> BDD-cost:  164
c ---[ 532]---> BDD-cost:  199
c ---[ 530]---> BDD-cost:  199
c ---[ 528]---> BDD-cost:  199
c ---[ 526]---> BDD-cost:  193
c ---[ 524]---> BDD-cost:  199
c ---[ 522]---> BDD-cost:  199
c ---[ 520]---> BDD-cost:  199
c ---[ 518]---> BDD-cost:  190
c ---[ 516]---> BDD-cost:  193
c ---[ 514]---> BDD-cost:  199
c ---[ 512]---> BDD-cost:  199
c ---[ 510]---> BDD-cost:  196
c ---[ 508]---> BDD-cost:  199
c ---[ 506]---> BDD-cost:  199
c ---[ 504]---> BDD-cost:  199
c ---[ 502]---> BDD-cost:  187
c ---[ 500]---> BDD-cost:  199
c ---[ 498]---> BDD-cost:  199
c ---[ 496]---> BDD-cost:  190
c ---[ 494]---> BDD-cost:  199
c ---[ 492]---> BDD-cost:  199
c ---[ 490]---> BDD-cost:  199
c ---[ 488]---> BDD-cost:  187
c ---[ 486]---> BDD-cost:  196
c ---[ 484]---> BDD-cost:  193
c ---[ 482]---> BDD-cost:  196
c ---[ 480]---> BDD-cost:  199
c ---[ 478]---> BDD-cost:   71
c ---[ 476]---> BDD-cost:  182
c ---[ 474]---> BDD-cost:  192
c ---[ 472]---> BDD-cost:  196
c ---[ 470]---> BDD-cost:  199
c ---[ 468]---> BDD-cost:  196
c ---[ 466]---> BDD-cost:  196
c ---[ 464]---> BDD-cost:  184
c ---[ 462]---> BDD-cost:  199
c ---[ 460]---> BDD-cost:  196
c ---[ 458]---> BDD-cost:  196
c ---[ 456]---> BDD-cost:  199
c ---[ 454]---> BDD-cost:  199
c ---[ 452]---> BDD-cost:  196
c ---[ 450]---> BDD-cost:  199
c ---[ 448]---> BDD-cost:  196
c ---[ 446]---> BDD-cost:  184
c ---[ 444]---> BDD-cost:  199
c ---[ 442]---> BDD-cost:  199
c ---[ 440]---> BDD-cost:  199
c ---[ 438]---> BDD-cost:  196
c ---[ 436]---> BDD-cost:  193
c ---[ 434]---> BDD-cost:  199
c ---[ 432]---> BDD-cost:  199
c ---[ 430]---> BDD-cost:  193
c ---[ 428]---> BDD-cost:  187
c ---[ 426]---> BDD-cost:  199
c ---[ 424]---> BDD-cost:  199
c ---[ 422]---> BDD-cost:  199
c ---[ 420]---> BDD-cost:  199
c ---[ 418]---> BDD-cost:   52
c ---[ 416]---> BDD-cost:  188
c ---[ 414]---> BDD-cost:  192
c ---[ 412]---> BDD-cost:  166
c ---[ 410]---> BDD-cost:  193
c ---[ 408]---> BDD-cost:  196
c ---[ 406]---> BDD-cost:  199
c ---[ 404]---> BDD-cost:  193
c ---[ 402]---> BDD-cost:  199
c ---[ 400]---> BDD-cost:  190
c ---[ 398]---> BDD-cost:  199
c ---[ 396]---> BDD-cost:  199
c ---[ 394]---> BDD-cost:  199
c ---[ 392]---> BDD-cost:  190
c ---[ 390]---> BDD-cost:  184
c ---[ 388]---> BDD-cost:  196
c ---[ 386]---> BDD-cost:  199
c ---[ 384]---> BDD-cost:  184
c ---[ 382]---> BDD-cost:  199
c ---[ 380]---> BDD-cost:  199
c ---[ 378]---> BDD-cost:  199
c ---[ 376]---> BDD-cost:  190
c ---[ 374]---> BDD-cost:  199
c ---[ 372]---> BDD-cost:  193
c ---[ 370]---> BDD-cost:  193
c ---[ 368]---> BDD-cost:  199
c ---[ 366]---> BDD-cost:  196
c ---[ 364]---> BDD-cost:  199
c ---[ 362]---> BDD-cost:  199
c ---[ 360]---> BDD-cost:  199
c ---[ 359]---> BDD-cost:   28
c ---[ 358]---> BDD-cost:   28
c ---[ 357]---> BDD-cost:   28
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 ---[ 346]---> BDD-cost:   28
c ---[ 345]---> BDD-cost:   28
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 ---[ 334]---> BDD-cost:   28
c ---[ 333]---> BDD-cost:   28
c ---[ 332]---> BDD-cost:   28
c ---[ 331]---> BDD-cost:   28
c ---[ 330]---> BDD-cost:   28
c ---[ 329]---> BDD-cost:   27
c ---[ 328]---> BDD-cost:   27
c ---[ 327]---> BDD-cost:   27
c ---[ 326]---> BDD-cost:   27
c ---[ 325]---> BDD-cost:   27
c ---[ 324]---> BDD-cost:   27
c ---[ 323]---> BDD-cost:   27
c ---[ 322]---> BDD-cost:   27
c ---[ 321]---> BDD-cost:   27
c ---[ 320]---> BDD-cost:   27
c ---[ 319]---> BDD-cost:   27
c ---[ 318]---> BDD-cost:   27
c ---[ 317]---> BDD-cost:   27
c ---[ 316]---> BDD-cost:   27
c ---[ 315]---> BDD-cost:   27
c ---[ 314]---> BDD-cost:   27
c ---[ 313]---> BDD-cost:   27
c ---[ 312]---> BDD-cost:   27
c ---[ 311]---> BDD-cost:   27
c ---[ 310]---> BDD-cost:   27
c ---[ 309]---> BDD-cost:   27
c ---[ 308]---> BDD-cost:   27
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:   25
c ---[ 298]---> BDD-cost:   25
c ---[ 297]---> BDD-cost:   25
c ---[ 296]---> BDD-cost:   25
c ---[ 295]---> BDD-cost:   25
c ---[ 294]---> BDD-cost:   25
c ---[ 293]---> BDD-cost:   25
c ---[ 292]---> BDD-cost:   25
c ---[ 291]---> BDD-cost:   25
c ---[ 290]---> BDD-cost:   25
c ---[ 289]---> BDD-cost:   25
c ---[ 288]---> BDD-cost:   25
c ---[ 287]---> BDD-cost:   25
c ---[ 286]---> BDD-cost:   25
c ---[ 285]---> BDD-cost:   25
c ---[ 284]---> BDD-cost:   25
c ---[ 283]---> BDD-cost:   25
c ---[ 282]---> BDD-cost:   25
c ---[ 281]---> BDD-cost:   25
c ---[ 280]---> BDD-cost:   25
c ---[ 279]---> BDD-cost:   25
c ---[ 278]---> BDD-cost:   25
c ---[ 277]---> BDD-cost:   25
c ---[ 276]---> BDD-cost:   25
c ---[ 275]---> BDD-cost:   25
c ---[ 274]---> BDD-cost:   25
c ---[ 273]---> BDD-cost:   25
c ---[ 272]---> BDD-cost:   25
c ---[ 271]---> BDD-cost:   25
c ---[ 270]---> BDD-cost:   25
c ---[ 269]---> BDD-cost:   28
c ---[ 268]---> BDD-cost:   28
c ---[ 267]---> BDD-cost:   28
c ---[ 266]---> BDD-cost:   28
c ---[ 265]---> BDD-cost:   28
c ---[ 264]---> BDD-cost:   28
c ---[ 263]---> BDD-cost:   28
c ---[ 262]---> BDD-cost:   28
c ---[ 261]---> BDD-cost:   28
c ---[ 260]---> BDD-cost:   28
c ---[ 259]---> BDD-cost:   28
c ---[ 258]---> BDD-cost:   28
c ---[ 257]---> BDD-cost:   28
c ---[ 256]---> BDD-cost:   28
c ---[ 255]---> BDD-cost:   28
c ---[ 254]---> BDD-cost:   28
c ---[ 253]---> BDD-cost:   28
c ---[ 252]---> BDD-cost:   28
c ---[ 251]---> BDD-cost:   28
c ---[ 250]---> BDD-cost:   28
c ---[ 249]---> BDD-cost:   28
c ---[ 248]---> BDD-cost:   28
c ---[ 247]---> BDD-cost:   28
c ---[ 246]---> BDD-cost:   28
c ---[ 245]---> BDD-cost:   28
c ---[ 244]---> BDD-cost:   28
c ---[ 243]---> BDD-cost:   28
c ---[ 242]---> BDD-cost:   28
c ---[ 241]---> BDD-cost:   28
c ---[ 240]---> BDD-cost:   28
c ---[ 239]---> BDD-cost:   28
c ---[ 238]---> BDD-cost:   28
c ---[ 237]---> BDD-cost:   28
c ---[ 236]---> BDD-cost:   28
c ---[ 235]---> BDD-cost:   28
c ---[ 234]---> BDD-cost:   28
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 ---[ 224]---> BDD-cost:   28
c ---[ 223]---> BDD-cost:   28
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 ---[ 212]---> BDD-cost:   28
c ---[ 211]---> BDD-cost:   28
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 ---[ 200]---> BDD-cost:   28
c ---[ 199]---> BDD-cost:   28
c ---[ 198]---> BDD-cost:   28
c ---[ 197]---> BDD-cost:   28
c ---[ 196]---> BDD-cost:   28
c ---[ 195]---> BDD-cost:   28
c ---[ 194]---> BDD-cost:   28
c ---[ 193]---> BDD-cost:   28
c ---[ 192]---> BDD-cost:   28
c ---[ 191]---> BDD-cost:   28
c ---[ 190]---> BDD-cost:   28
c ---[ 189]---> BDD-cost:   28
c ---[ 188]---> BDD-cost:   28
c ---[ 187]---> BDD-cost:   28
c ---[ 186]---> BDD-cost:   28
c ---[ 185]---> BDD-cost:   28
c ---[ 184]---> BDD-cost:   28
c ---[ 183]---> BDD-cost:   28
c ---[ 182]---> BDD-cost:   28
c ---[ 181]---> BDD-cost:   28
c ---[ 180]---> BDD-cost:   28
c ---[ 179]---> BDD-cost:   27
c ---[ 178]---> BDD-cost:   27
c ---[ 177]---> BDD-cost:   27
c ---[ 176]---> BDD-cost:   27
c ---[ 175]---> BDD-cost:   27
c ---[ 174]---> BDD-cost:   27
c ---[ 173]---> BDD-cost:   27
c ---[ 172]---> BDD-cost:   27
c ---[ 171]---> BDD-cost:   27
c ---[ 170]---> BDD-cost:   27
c ---[ 169]---> BDD-cost:   27
c ---[ 168]---> BDD-cost:   27
c ---[ 167]---> BDD-cost:   27
c ---[ 166]---> BDD-cost:   27
c ---[ 165]---> BDD-cost:   27
c ---[ 164]---> BDD-cost:   27
c ---[ 163]---> BDD-cost:   27
c ---[ 162]---> BDD-cost:   27
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 ---[ 152]---> BDD-cost:   27
c ---[ 151]---> BDD-cost:   27
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 ---[ 140]---> BDD-cost:   27
c ---[ 139]---> BDD-cost:   27
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 ---[ 128]---> BDD-cost:   27
c ---[ 127]---> BDD-cost:   27
c ---[ 126]---> BDD-cost:   27
c ---[ 125]---> BDD-cost:   27
c ---[ 124]---> BDD-cost:   27
c ---[ 123]---> BDD-cost:   27
c ---[ 122]---> BDD-cost:   27
c ---[ 121]---> BDD-cost:   27
c ---[ 120]---> BDD-cost:   27
c ---[ 119]---> BDD-cost:   28
c ---[ 118]---> BDD-cost:   28
c ---[ 117]---> BDD-cost:   28
c ---[ 116]---> BDD-cost:   28
c ---[ 115]---> BDD-cost:   28
c ---[ 114]---> BDD-cost:   28
c ---[ 113]---> BDD-cost:   28
c ---[ 112]---> BDD-cost:   28
c ---[ 111]---> BDD-cost:   28
c ---[ 110]---> BDD-cost:   28
c ---[ 109]---> BDD-cost:   28
c ---[ 108]---> BDD-cost:   28
c ---[ 107]---> BDD-cost:   28
c ---[ 106]---> BDD-cost:   28
c ---[ 105]---> BDD-cost:   28
c ---[ 104]---> BDD-cost:   28
c ---[ 103]---> BDD-cost:   28
c ---[ 102]---> BDD-cost:   28
c ---[ 101]---> BDD-cost:   28
c ---[ 100]---> BDD-cost:   28
c ---[  99]---> BDD-cost:   28
c ---[  98]---> BDD-cost:   28
c ---[  97]---> BDD-cost:   28
c ---[  96]---> BDD-cost:   28
c ---[  95]---> BDD-cost:   28
c ---[  94]---> BDD-cost:   28
c ---[  93]---> BDD-cost:   28
c ---[  92]---> BDD-cost:   28
c ---[  91]---> BDD-cost:   28
c ---[  90]---> BDD-cost:   28
c ---[  89]---> BDD-cost:   25
c ---[  88]---> BDD-cost:   25
c ---[  87]---> BDD-cost:   25
c ---[  86]---> BDD-cost:   25
c ---[  85]---> BDD-cost:   25
c ---[  84]---> BDD-cost:   25
c ---[  83]---> BDD-cost:   25
c ---[  82]---> BDD-cost:   25
c ---[  81]---> BDD-cost:   25
c ---[  80]---> BDD-cost:   25
c ---[  79]---> BDD-cost:   25
c ---[  78]---> BDD-cost:   25
c ---[  77]---> BDD-cost:   25
c ---[  76]---> BDD-cost:   25
c ---[  75]---> BDD-cost:   25
c ---[  74]---> BDD-cost:   25
c ---[  73]---> BDD-cost:   25
c ---[  72]---> BDD-cost:   25
c ---[  71]---> BDD-cost:   25
c ---[  70]---> BDD-cost:   25
c ---[  69]---> BDD-cost:   25
c ---[  68]---> BDD-cost:   25
c ---[  67]---> BDD-cost:   25
c ---[  66]---> BDD-cost:   25
c ---[  65]---> BDD-cost:   25
c ---[  64]---> BDD-cost:   25
c ---[  63]---> BDD-cost:   25
c ---[  62]---> BDD-cost:   25
c ---[  61]---> BDD-cost:   25
c ---[  60]---> BDD-cost:   25
c ---[  59]---> BDD-cost:   27
c ---[  58]---> BDD-cost:   27
c ---[  57]---> BDD-cost:   27
c ---[  56]---> BDD-cost:   27
c ---[  55]---> BDD-cost:   27
c ---[  54]---> BDD-cost:   27
c ---[  53]---> BDD-cost:   27
c ---[  52]---> BDD-cost:   27
c ---[  51]---> BDD-cost:   27
c ---[  50]---> BDD-cost:   27
c ---[  49]---> BDD-cost:   27
c ---[  48]---> BDD-cost:   27
c ---[  47]---> BDD-cost:   27
c ---[  46]---> BDD-cost:   27
c ---[  45]---> BDD-cost:   27
c ---[  44]---> BDD-cost:   27
c ---[  43]---> BDD-cost:   27
c ---[  42]---> BDD-cost:   27
c ---[  41]---> BDD-cost:   27
c ---[  40]---> BDD-cost:   27
c ---[  39]---> BDD-cost:   27
c ---[  38]---> BDD-cost:   27
c ---[  37]---> BDD-cost:   27
c ---[  36]---> BDD-cost:   27
c ---[  35]---> BDD-cost:   27
c ---[  34]---> BDD-cost:   27
c ---[  33]---> BDD-cost:   27
c ---[  32]---> BDD-cost:   27
c ---[  31]---> BDD-cost:   27
c ---[  30]---> BDD-cost:   27
c ---[  29]---> BDD-cost:   25
c ---[  28]---> BDD-cost:   25
c ---[  27]---> BDD-cost:   25
c ---[  26]---> BDD-cost:   25
c ---[  25]---> BDD-cost:   25
c ---[  24]---> BDD-cost:   25
c ---[  23]---> BDD-cost:   25
c ---[  22]---> BDD-cost:   25
c ---[  21]---> BDD-cost:   25
c ---[  20]---> BDD-cost:   25
c ---[  19]---> BDD-cost:   25
c ---[  18]---> BDD-cost:   25
c ---[  17]---> BDD-cost:   25
c ---[  16]---> BDD-cost:   25
c ---[  15]---> BDD-cost:   25
c ---[  14]---> BDD-cost:   25
c ---[  13]---> BDD-cost:   25
c ---[  12]---> BDD-cost:   25
c ---[  11]---> BDD-cost:   25
c ---[  10]---> BDD-cost:   25
c ---[   9]---> BDD-cost:   25
c ---[   8]---> BDD-cost:   25
c ---[   7]---> BDD-cost:   25
c ---[   6]---> BDD-cost:   25
c ---[   5]---> BDD-cost:   25
c ---[   4]---> BDD-cost:   25
c ---[   3]---> BDD-cost:   25
c ---[   2]---> BDD-cost:   25
c ---[   1]---> BDD-cost:   25
c ---[   0]---> BDD-cost:   25
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 |       102 | 1020457  2967665 |  374308     100      955     9.6 |  0.438 % |
c |       252 | 1020216  2967003 |  411738     245     2849    11.6 |  0.445 % |
c |       477 | 1020216  2967003 |  452912     470     6126    13.0 |  0.445 % |
c |       814 | 1019796  2965793 |  498203     794    13289    16.7 |  0.464 % |
c |      1320 | 1019796  2965793 |  548024    1300    20770    16.0 |  0.464 % |
c |      2081 | 1019621  2965315 |  602826    2022    37981    18.8 |  0.476 % |
c |      3220 | 1019621  2965315 |  663109    3161    67044    21.2 |  0.476 % |
c |      4928 | 1019621  2965315 |  729420    4869   108022    22.2 |  0.476 % |
c |      7490 | 1019621  2965315 |  802362    7431   185482    25.0 |  0.476 % |
c |     11334 | 1019612  2965294 |  882598   11273   349661    31.0 |  0.477 % |
c |     17101 | 1019478  2964968 |  970858   17025   690389    40.6 |  0.493 % |
c |     25750 | 1019472  2964956 | 1067944   25671  1124038    43.8 |  0.493 % |
c |     38725 | 1019442  2964889 | 1174738   38639  1842920    47.7 |  0.497 % |
c |     58187 | 1019433  2964868 | 1292212   58100  2707558    46.6 |  0.498 % |
c |     87379 | 1019433  2964868 | 1421434   87292  5997244    68.7 |  0.498 % |
c |    131169 | 1019379  2964744 | 1563577  131068  9991711    76.2 |  0.504 % |
c |    196860 | 1018971  2963720 | 1719935  196755 17575010    89.3 |  0.540 % |
c |    295388 | 1018969  2963716 | 1891928  295282 21921356    74.2 |  0.540 % |
#### 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.72 0.90 0.89 2/55 11931
Raw data (stat): 11931 (runsolver) R 11930 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 540327975 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.0003 s]
Raw data (loadavg): 0.76 0.90 0.89 2/55 11931
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 32819 0 0 0 922 76 0 0 25 0 1 0 540327975 144486400 31423 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35275 31423 603 41 0 35234 0
vsize: 141100
[startup+20.0011 s]
Raw data (loadavg): 0.80 0.90 0.89 2/55 11931
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 33238 0 0 0 1921 78 0 0 25 0 1 0 540327975 146259968 31842 4294967295 134512640 134672761 3221224528 3221223712 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35708 31842 603 41 0 35667 0
vsize: 142832
[startup+30.0015 s]
Raw data (loadavg): 0.83 0.91 0.89 2/55 11931
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 33696 0 0 0 2919 80 0 0 25 0 1 0 540327975 148205568 32300 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36183 32300 603 41 0 36142 0
vsize: 144732
[startup+40.002 s]
Raw data (loadavg): 0.85 0.91 0.89 2/55 11931
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 34088 0 0 0 3918 81 0 0 25 0 1 0 540327975 149676032 32692 4294967295 134512640 134672761 3221224528 3221223712 134559590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36542 32692 603 41 0 36501 0
vsize: 146168
[startup+50.0029 s]
Raw data (loadavg): 0.88 0.91 0.90 2/55 11931
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 34469 0 0 0 4917 82 0 0 25 0 1 0 540327975 151285760 33073 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36935 33073 603 41 0 36894 0
vsize: 147740
[startup+60.0033 s]
Raw data (loadavg): 0.89 0.91 0.90 2/55 11931
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 34870 0 0 0 5916 83 0 0 25 0 1 0 540327975 153026560 33474 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37360 33474 603 41 0 37319 0
vsize: 149440
[startup+70.0038 s]
Raw data (loadavg): 0.91 0.92 0.90 2/55 11931
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 35223 0 0 0 6914 85 0 0 25 0 1 0 540327975 154492928 33827 4294967295 134512640 134672761 3221224528 3221223712 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37718 33827 603 41 0 37677 0
vsize: 150872
[startup+80.0037 s]
Raw data (loadavg): 0.92 0.92 0.90 2/55 11931
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 35534 0 0 0 7913 86 0 0 25 0 1 0 540327975 155684864 34138 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38009 34138 603 41 0 37968 0
vsize: 152036
[startup+90.005 s]
Raw data (loadavg): 0.93 0.92 0.90 2/55 11931
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 35784 0 0 0 8913 87 0 0 25 0 1 0 540327975 156762112 34388 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38272 34388 603 41 0 38231 0
vsize: 153088
[startup+100.006 s]
Raw data (loadavg): 0.94 0.92 0.90 2/55 11931
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 36034 0 0 0 9911 88 0 0 25 0 1 0 540327975 157741056 34638 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38511 34638 603 41 0 38470 0
vsize: 154044
[startup+110.006 s]
Raw data (loadavg): 0.95 0.92 0.90 2/55 11931
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 36390 0 0 0 10910 89 0 0 25 0 1 0 540327975 159215616 34994 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38871 34994 603 41 0 38830 0
vsize: 155484
[startup+120.007 s]
Raw data (loadavg): 0.96 0.93 0.90 2/55 11931
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 36884 0 0 0 11909 91 0 0 25 0 1 0 540327975 161476608 35488 4294967295 134512640 134672761 3221224528 3221223632 134560510 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39423 35488 603 41 0 39382 0
vsize: 157692
[startup+130.006 s]
Raw data (loadavg): 0.96 0.93 0.90 2/55 11931
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 37299 0 0 0 12908 92 0 0 25 0 1 0 540327975 163209216 35903 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39846 35903 603 41 0 39805 0
vsize: 159384
[startup+140.007 s]
Raw data (loadavg): 0.97 0.93 0.90 2/55 11931
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 37719 0 0 0 13907 93 0 0 25 0 1 0 540327975 164810752 36323 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40237 36323 603 41 0 40196 0
vsize: 160948
[startup+150.009 s]
Raw data (loadavg): 0.97 0.93 0.91 2/55 11931
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 38128 0 0 0 14906 94 0 0 25 0 1 0 540327975 166555648 36732 4294967295 134512640 134672761 3221224528 3221223632 134554919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40663 36732 603 41 0 40622 0
vsize: 162652
[startup+160.009 s]
Raw data (loadavg): 0.98 0.93 0.91 2/55 11931
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 38596 0 0 0 15904 96 0 0 25 0 1 0 540327975 168435712 37200 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41122 37200 603 41 0 41081 0
vsize: 164488
[startup+170.009 s]
Raw data (loadavg): 0.98 0.94 0.91 2/55 11931
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 39061 0 0 0 16903 97 0 0 25 0 1 0 540327975 170315776 37665 4294967295 134512640 134672761 3221224528 3221223632 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41581 37665 603 41 0 41540 0
vsize: 166324
[startup+180.009 s]
Raw data (loadavg): 0.98 0.94 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 39467 0 0 0 17901 100 0 0 25 0 1 0 540327975 171921408 38071 4294967295 134512640 134672761 3221224528 3221223632 134560194 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41973 38071 603 41 0 41932 0
vsize: 167892
[startup+190.01 s]
Raw data (loadavg): 0.98 0.94 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 39765 0 0 0 18900 101 0 0 25 0 1 0 540327975 173129728 38369 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42268 38369 603 41 0 42227 0
vsize: 169072
[startup+200.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 40019 0 0 0 19899 102 0 0 25 0 1 0 540327975 174194688 38623 4294967295 134512640 134672761 3221224528 3221223664 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42528 38623 603 41 0 42487 0
vsize: 170112
[startup+210.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 40313 0 0 0 20898 103 0 0 25 0 1 0 540327975 175452160 38917 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42835 38917 603 41 0 42794 0
vsize: 171340
[startup+220.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 40598 0 0 0 21896 105 0 0 25 0 1 0 540327975 176660480 39202 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43130 39202 603 41 0 43089 0
vsize: 172520
[startup+230.011 s]
Raw data (loadavg): 0.99 0.94 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 40892 0 0 0 22895 106 0 0 25 0 1 0 540327975 177729536 39496 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43391 39496 603 41 0 43350 0
vsize: 173564
[startup+240.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 41169 0 0 0 23894 107 0 0 25 0 1 0 540327975 178921472 39773 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43682 39773 603 41 0 43641 0
vsize: 174728
[startup+250.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 41404 0 0 0 24894 108 0 0 25 0 1 0 540327975 179855360 40008 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43910 40008 603 41 0 43869 0
vsize: 175640
[startup+260.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 41658 0 0 0 25893 109 0 0 25 0 1 0 540327975 180912128 40262 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44168 40262 603 41 0 44127 0
vsize: 176672
[startup+270.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 42095 0 0 0 26891 110 0 0 25 0 1 0 540327975 182652928 40699 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44593 40699 603 41 0 44552 0
vsize: 178372
[startup+280.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 42635 0 0 0 27890 112 0 0 25 0 1 0 540327975 184922112 41239 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45147 41239 603 41 0 45106 0
vsize: 180588
[startup+290.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 43110 0 0 0 28888 114 0 0 25 0 1 0 540327975 186785792 41714 4294967295 134512640 134672761 3221224528 3221223696 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45602 41714 603 41 0 45561 0
vsize: 182408
[startup+300.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 43572 0 0 0 29886 116 0 0 25 0 1 0 540327975 188641280 42176 4294967295 134512640 134672761 3221224528 3221223696 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46055 42176 603 41 0 46014 0
vsize: 184220
[startup+310.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 44004 0 0 0 30885 118 0 0 25 0 1 0 540327975 190386176 42608 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46481 42608 603 41 0 46440 0
vsize: 185924
[startup+320.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 44341 0 0 0 31884 119 0 0 25 0 1 0 540327975 192376832 42945 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46967 42945 603 41 0 46926 0
vsize: 187868
[startup+330.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 44682 0 0 0 32882 120 0 0 25 0 1 0 540327975 193708032 43286 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47292 43286 603 41 0 47251 0
vsize: 189168
[startup+340.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 45040 0 0 0 33881 122 0 0 25 0 1 0 540327975 195182592 43644 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47652 43644 603 41 0 47611 0
vsize: 190608
[startup+350.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 45391 0 0 0 34880 123 0 0 25 0 1 0 540327975 196648960 43995 4294967295 134512640 134672761 3221224528 3221223696 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48010 43995 603 41 0 47969 0
vsize: 192040
[startup+360.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 45738 0 0 0 35879 125 0 0 25 0 1 0 540327975 197976064 44342 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48334 44342 603 41 0 48293 0
vsize: 193336
[startup+370.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 46060 0 0 0 36877 126 0 0 25 0 1 0 540327975 199307264 44664 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48659 44664 603 41 0 48618 0
vsize: 194636
[startup+380.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 46356 0 0 0 37876 127 0 0 25 0 1 0 540327975 200511488 44960 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48953 44960 603 41 0 48912 0
vsize: 195812
[startup+390.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 46653 0 0 0 38876 128 0 0 25 0 1 0 540327975 201699328 45257 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49243 45257 603 41 0 49202 0
vsize: 196972
[startup+400.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 46955 0 0 0 39875 129 0 0 25 0 1 0 540327975 203038720 45559 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49570 45559 603 41 0 49529 0
vsize: 198280
[startup+410.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 47258 0 0 0 40874 130 0 0 25 0 1 0 540327975 204230656 45862 4294967295 134512640 134672761 3221224528 3221223696 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49861 45862 603 41 0 49820 0
vsize: 199444
[startup+420.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 47540 0 0 0 41874 130 0 0 25 0 1 0 540327975 205438976 46144 4294967295 134512640 134672761 3221224528 3221223696 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50156 46144 603 41 0 50115 0
vsize: 200624
[startup+430.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 47834 0 0 0 42873 132 0 0 25 0 1 0 540327975 206663680 46438 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50455 46438 603 41 0 50414 0
vsize: 201820
[startup+440.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 48116 0 0 0 43872 133 0 0 25 0 1 0 540327975 207720448 46720 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50713 46720 603 41 0 50672 0
vsize: 202852
[startup+450.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 48365 0 0 0 44870 134 0 0 25 0 1 0 540327975 208785408 46969 4294967295 134512640 134672761 3221224528 3221223696 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50973 46969 603 41 0 50932 0
vsize: 203892
[startup+460.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 48654 0 0 0 45870 135 0 0 25 0 1 0 540327975 209981440 47258 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51265 47258 603 41 0 51224 0
vsize: 205060
[startup+470.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11933
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 48941 0 0 0 46869 136 0 0 25 0 1 0 540327975 211181568 47545 4294967295 134512640 134672761 3221224528 3221223632 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51558 47545 603 41 0 51517 0
vsize: 206232
[startup+480.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 49206 0 0 0 47869 137 0 0 25 0 1 0 540327975 212254720 47810 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51820 47810 603 41 0 51779 0
vsize: 207280
[startup+490.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 49458 0 0 0 48868 137 0 0 25 0 1 0 540327975 213204992 48062 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52052 48062 603 41 0 52011 0
vsize: 208208
[startup+500.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 49694 0 0 0 49868 138 0 0 25 0 1 0 540327975 214142976 48298 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52281 48298 603 41 0 52240 0
vsize: 209124
[startup+510.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 49934 0 0 0 50867 138 0 0 25 0 1 0 540327975 215195648 48538 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52538 48538 603 41 0 52497 0
vsize: 210152
[startup+520.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 50195 0 0 0 51867 139 0 0 25 0 1 0 540327975 216264704 48799 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52799 48799 603 41 0 52758 0
vsize: 211196
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 50427 0 0 0 52866 140 0 0 25 0 1 0 540327975 217231360 49031 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53035 49031 603 41 0 52994 0
vsize: 212140
[startup+540.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 50677 0 0 0 53866 140 0 0 25 0 1 0 540327975 218333184 49281 4294967295 134512640 134672761 3221224528 3221223712 134558883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53304 49281 603 41 0 53263 0
vsize: 213216
[startup+550.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 50919 0 0 0 54865 141 0 0 25 0 1 0 540327975 219283456 49523 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53536 49523 603 41 0 53495 0
vsize: 214144
[startup+560.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 51151 0 0 0 55864 142 0 0 25 0 1 0 540327975 220200960 49755 4294967295 134512640 134672761 3221224528 3221223696 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53760 49755 603 41 0 53719 0
vsize: 215040
[startup+570.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 51357 0 0 0 56864 143 0 0 25 0 1 0 540327975 221044736 49961 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53966 49961 603 41 0 53925 0
vsize: 215864
[startup+580.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 51575 0 0 0 57863 144 0 0 25 0 1 0 540327975 221982720 50179 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54195 50179 603 41 0 54154 0
vsize: 216780
[startup+590.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 51819 0 0 0 58863 144 0 0 25 0 1 0 540327975 223023104 50423 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54449 50423 603 41 0 54408 0
vsize: 217796
[startup+600.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 52044 0 0 0 59863 144 0 0 25 0 1 0 540327975 223944704 50648 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54674 50648 603 41 0 54633 0
vsize: 218696
[startup+610.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 52292 0 0 0 60863 145 0 0 25 0 1 0 540327975 225009664 50896 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54934 50896 603 41 0 54893 0
vsize: 219736
[startup+620.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 52612 0 0 0 61862 145 0 0 25 0 1 0 540327975 226369536 51216 4294967295 134512640 134672761 3221224528 3221223632 134559955 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55266 51216 603 41 0 55225 0
vsize: 221064
[startup+630.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 52722 0 0 0 62862 146 0 0 25 0 1 0 540327975 226799616 51326 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55371 51326 603 41 0 55330 0
vsize: 221484
[startup+640.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 52850 0 0 0 63862 146 0 0 25 0 1 0 540327975 227332096 51454 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55501 51454 603 41 0 55460 0
vsize: 222004
[startup+650.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 52983 0 0 0 64862 146 0 0 25 0 1 0 540327975 227856384 51587 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55629 51587 603 41 0 55588 0
vsize: 222516
[startup+660.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 53141 0 0 0 65861 147 0 0 25 0 1 0 540327975 228429824 51745 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55769 51745 603 41 0 55728 0
vsize: 223076
[startup+670.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 53303 0 0 0 66861 147 0 0 25 0 1 0 540327975 229097472 51907 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55932 51907 603 41 0 55891 0
vsize: 223728
[startup+680.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 53480 0 0 0 67861 148 0 0 25 0 1 0 540327975 229892096 52084 4294967295 134512640 134672761 3221224528 3221223696 134561139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56126 52084 603 41 0 56085 0
vsize: 224504
[startup+690.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 53642 0 0 0 68861 148 0 0 25 0 1 0 540327975 230563840 52246 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56290 52246 603 41 0 56249 0
vsize: 225160
[startup+700.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 53786 0 0 0 69860 148 0 0 25 0 1 0 540327975 231092224 52390 4294967295 134512640 134672761 3221224528 3221223712 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56419 52390 603 41 0 56378 0
vsize: 225676
[startup+710.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 53947 0 0 0 70861 148 0 0 25 0 1 0 540327975 231751680 52551 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56580 52551 603 41 0 56539 0
vsize: 226320
[startup+720.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 54090 0 0 0 71861 149 0 0 25 0 1 0 540327975 232280064 52694 4294967295 134512640 134672761 3221224528 3221223712 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56709 52694 603 41 0 56668 0
vsize: 226836
[startup+730.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 54232 0 0 0 72860 149 0 0 25 0 1 0 540327975 232976384 52836 4294967295 134512640 134672761 3221224528 3221223696 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56879 52836 603 41 0 56838 0
vsize: 227516
[startup+740.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 54372 0 0 0 73860 149 0 0 25 0 1 0 540327975 233504768 52976 4294967295 134512640 134672761 3221224528 3221223692 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57008 52976 603 41 0 56967 0
vsize: 228032
[startup+750.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 54500 0 0 0 74860 150 0 0 25 0 1 0 540327975 234037248 53104 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57138 53104 603 41 0 57097 0
vsize: 228552
[startup+760.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 54649 0 0 0 75859 151 0 0 25 0 1 0 540327975 234561536 53253 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57266 53253 603 41 0 57225 0
vsize: 229064
[startup+770.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11935
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 54770 0 0 0 76859 151 0 0 25 0 1 0 540327975 235089920 53374 4294967295 134512640 134672761 3221224528 3221223696 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57395 53374 603 41 0 57354 0
vsize: 229580
[startup+780.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 54913 0 0 0 77859 152 0 0 25 0 1 0 540327975 235671552 53517 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57537 53517 603 41 0 57496 0
vsize: 230148
[startup+790.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 55038 0 0 0 78858 152 0 0 25 0 1 0 540327975 236204032 53642 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57667 53642 603 41 0 57626 0
vsize: 230668
[startup+800.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 55166 0 0 0 79858 153 0 0 25 0 1 0 540327975 236601344 53770 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57764 53770 603 41 0 57723 0
vsize: 231056
[startup+810.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 55322 0 0 0 80858 153 0 0 25 0 1 0 540327975 237314048 53926 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57938 53926 603 41 0 57897 0
vsize: 231752
[startup+820.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 55450 0 0 0 81858 153 0 0 25 0 1 0 540327975 237924352 54054 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58087 54054 603 41 0 58046 0
vsize: 232348
[startup+830.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 55569 0 0 0 82858 153 0 0 25 0 1 0 540327975 238321664 54173 4294967295 134512640 134672761 3221224528 3221223484 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58184 54173 603 41 0 58143 0
vsize: 232736
[startup+840.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 55699 0 0 0 83858 154 0 0 25 0 1 0 540327975 238993408 54303 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58348 54303 603 41 0 58307 0
vsize: 233392
[startup+850.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 55806 0 0 0 84857 154 0 0 25 0 1 0 540327975 239443968 54410 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58458 54410 603 41 0 58417 0
vsize: 233832
[startup+860.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 55912 0 0 0 85857 155 0 0 25 0 1 0 540327975 240988160 54516 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58835 54516 603 41 0 58794 0
vsize: 235340
[startup+870.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 56027 0 0 0 86857 155 0 0 25 0 1 0 540327975 241381376 54631 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58931 54631 603 41 0 58890 0
vsize: 235724
[startup+880.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 56141 0 0 0 87856 156 0 0 25 0 1 0 540327975 241909760 54745 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59060 54745 603 41 0 59019 0
vsize: 236240
[startup+890.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 56278 0 0 0 88856 156 0 0 25 0 1 0 540327975 242573312 54882 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59222 54882 603 41 0 59181 0
vsize: 236888
[startup+900.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 56359 0 0 0 89856 156 0 0 25 0 1 0 540327975 242843648 54963 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59288 54963 603 41 0 59247 0
vsize: 237152
[startup+910.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 56458 0 0 0 90856 157 0 0 25 0 1 0 540327975 243249152 55062 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59387 55062 603 41 0 59346 0
vsize: 237548
[startup+920.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 56559 0 0 0 91856 157 0 0 25 0 1 0 540327975 243642368 55163 4294967295 134512640 134672761 3221224528 3221223632 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59483 55163 603 41 0 59442 0
vsize: 237932
[startup+930.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 56661 0 0 0 92855 157 0 0 25 0 1 0 540327975 244039680 55265 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59580 55265 603 41 0 59539 0
vsize: 238320
[startup+940.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 56771 0 0 0 93855 158 0 0 25 0 1 0 540327975 244436992 55375 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59677 55375 603 41 0 59636 0
vsize: 238708
[startup+950.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 56881 0 0 0 94855 158 0 0 25 0 1 0 540327975 244842496 55485 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59776 55485 603 41 0 59735 0
vsize: 239104
[startup+960.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 56981 0 0 0 95854 159 0 0 25 0 1 0 540327975 245366784 55585 4294967295 134512640 134672761 3221224528 3221223664 134565110 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59904 55585 603 41 0 59863 0
vsize: 239616
[startup+970.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 57080 0 0 0 96854 160 0 0 25 0 1 0 540327975 245768192 55684 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60002 55684 603 41 0 59961 0
vsize: 240008
[startup+980.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 57183 0 0 0 97854 160 0 0 25 0 1 0 540327975 246169600 55787 4294967295 134512640 134672761 3221224528 3221223696 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60100 55787 603 41 0 60059 0
vsize: 240400
[startup+990.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 57287 0 0 0 98854 160 0 0 25 0 1 0 540327975 246571008 55891 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60198 55891 603 41 0 60157 0
vsize: 240792
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 57383 0 0 0 99854 161 0 0 25 0 1 0 540327975 246964224 55987 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60294 55987 603 41 0 60253 0
vsize: 241176
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 57481 0 0 0 100853 161 0 0 25 0 1 0 540327975 247365632 56085 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60392 56085 603 41 0 60351 0
vsize: 241568
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 57716 0 0 0 101853 162 0 0 25 0 1 0 540327975 248340480 56320 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60630 56320 603 41 0 60589 0
vsize: 242520
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 58036 0 0 0 102851 164 0 0 25 0 1 0 540327975 249540608 56640 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60923 56640 603 41 0 60882 0
vsize: 243692
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 58434 0 0 0 103849 165 0 0 25 0 1 0 540327975 251150336 57038 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61316 57038 603 41 0 61275 0
vsize: 245264
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 58918 0 0 0 104848 166 0 0 25 0 1 0 540327975 253157376 57522 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61806 57522 603 41 0 61765 0
vsize: 247224
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 59254 0 0 0 105848 167 0 0 25 0 1 0 540327975 254480384 57858 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62129 57858 603 41 0 62088 0
vsize: 248516
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11937
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 59653 0 0 0 106847 168 0 0 25 0 1 0 540327975 256217088 58257 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62553 58257 603 41 0 62512 0
vsize: 250212
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11939
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 59941 0 0 0 107845 170 0 0 25 0 1 0 540327975 257286144 58545 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62814 58545 603 41 0 62773 0
vsize: 251256
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11939
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 60355 0 0 0 108845 170 0 0 25 0 1 0 540327975 259031040 58959 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63240 58959 603 41 0 63199 0
vsize: 252960
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11939
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 60703 0 0 0 109844 171 0 0 25 0 1 0 540327975 260370432 59307 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63567 59307 603 41 0 63526 0
vsize: 254268
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11939
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 61023 0 0 0 110843 173 0 0 25 0 1 0 540327975 261705728 59627 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63893 59627 603 41 0 63852 0
vsize: 255572
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11939
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 61444 0 0 0 111842 174 0 0 25 0 1 0 540327975 263458816 60048 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64321 60048 603 41 0 64280 0
vsize: 257284
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11939
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 61867 0 0 0 112841 175 0 0 25 0 1 0 540327975 265183232 60471 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64742 60471 603 41 0 64701 0
vsize: 258968
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11939
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 62254 0 0 0 113840 176 0 0 25 0 1 0 540327975 266645504 60858 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65099 60858 603 41 0 65058 0
vsize: 260396
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11939
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 62369 0 0 0 114840 177 0 0 25 0 1 0 540327975 267284480 60973 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65255 60973 603 41 0 65214 0
vsize: 261020
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11939
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 62580 0 0 0 115839 178 0 0 25 0 1 0 540327975 268083200 61184 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65450 61184 603 41 0 65409 0
vsize: 261800
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11939
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 62853 0 0 0 116838 178 0 0 25 0 1 0 540327975 269279232 61457 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65742 61457 603 41 0 65701 0
vsize: 262968
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11939
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 63158 0 0 0 117838 179 0 0 25 0 1 0 540327975 270479360 61762 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66035 61762 603 41 0 65994 0
vsize: 264140
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11939
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 63445 0 0 0 118837 180 0 0 25 0 1 0 540327975 271687680 62049 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66330 62049 603 41 0 66289 0
vsize: 265320
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11939
Raw data (stat): 11931 (minisat+) R 11930 20024 20023 0 -1 0 63745 0 0 0 119835 182 0 0 25 0 1 0 540327975 272891904 62349 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66624 62349 603 41 0 66583 0
vsize: 266496
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.16 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 11939
Raw data (stat): 11931 (minisat+) Z 11930 20024 20023 0 -1 12 63747 0 0 0 119835 194 0 0 25 0 1 0 540327975 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.16
CPU time (s): 1200.3
CPU user time (s): 1198.36
CPU system time (s): 1.9447
CPU usage (%): 100.012
Max. virtual memory (Kb): 266496
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####